Skip to content

Commit

Permalink
cleanup: remove unused code; clean up some pdf figures
Browse files Browse the repository at this point in the history
  • Loading branch information
@williamdemeo
williamdemeo committed Nov 13, 2024
1 parent faab68f commit 20ffac4
Show file tree
Hide file tree
Showing 5 changed files with 53 additions and 67 deletions.
17 changes: 1 addition & 16 deletions src/Interface/STS.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -53,21 +53,6 @@ module _ (_⊢_⇀⟦_⟧ᵇ_ : C → S → ⊤ → S → Type) (_⊢_⇀⟦_⟧
───────────────────────────────────────
Γ ⊢ s ⇀⟦ sig ∷ sigs ⟧* s''

module _ {_⊢_⇀⟦_⟧ᵇ_ : C → S → ⊤ → S → Type} {_⊢_⇀⟦_⟧_ : C → S → Sig → S → Type} where
data _⊢_⇀⟦_⟧*ʳ_ : C → S → List Sig → S → Type where

BS-baseʳ :
Γ ⊢ s ⇀⟦ _ ⟧ᵇ s'
───────────────────────────────────────
Γ ⊢ s ⇀⟦ [] ⟧*ʳ s'

BS-indʳ :
Γ ⊢ s' ⇀⟦ sigs ⟧*ʳ s''
→ Γ ⊢ s ⇀⟦ sig ⟧ s'
───────────────────────────────────────
Γ ⊢ s ⇀⟦ sigs ∷ʳ sig ⟧*ʳ s''


module _ (_⊢_⇀⟦_⟧ᵇ_ : C → S → ⊤ → S → Type) (_⊢_⇀⟦_⟧_ : C × ℕ → S → Sig → S → Type) where
data _⊢_⇀⟦_⟧ᵢ*'_ : C × ℕ → S → List Sig → S → Type where

Expand Down Expand Up @@ -116,7 +101,7 @@ ReflexiveTransitiveClosureᵢ-total SS-total = helper SS-total
case SS-total of λ where
(s' , Ps') → map₂′ (BS-ind Ps') $ helper SS-total

ReflexiveTransitiveClosureᵣᵇ = _⊢_⇀⟦_⟧*ʳ_
-- with a given base case
ReflexiveTransitiveClosureᵢᵇ = _⊢_⇀⟦_⟧ᵢ*_
ReflexiveTransitiveClosureᵇ = _⊢_⇀⟦_⟧*_

Expand Down
30 changes: 15 additions & 15 deletions src/Ledger/Certs.lagda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -264,42 +264,41 @@ constitutional committee.
\end{itemize}

\begin{figure*}[h]
\begin{AgdaSuppressSpace}
\begin{AgdaMultiCode}
\begin{code}[hide]
data
\end{code}
\begin{code}
_⊢_⇀⦇_,DELEG⦈_ : DelegEnv → DState → DCert → DState → Type
_⊢_⇀⦇_,DELEG⦈_ : DelegEnv → DState → DCert → DState → Type
\end{code}
\begin{code}[hide]
data
\end{code}
\begin{code}
_⊢_⇀⦇_,POOL⦈_ : PoolEnv → PState → DCert → PState → Type
_⊢_⇀⦇_,POOL⦈_ : PoolEnv → PState → DCert → PState → Type
\end{code}
\begin{code}[hide]
data
\end{code}
\begin{code}
_⊢_⇀⦇_,GOVCERT⦈_ : GovCertEnv → GState → DCert → GState → Type
_⊢_⇀⦇_,GOVCERT⦈_ : GovCertEnv → GState → DCert → GState → Type
\end{code}
\begin{code}[hide]
data
\end{code}
\begin{code}
_⊢_⇀⦇_,CERT⦈_ : CertEnv → CertState → DCert → CertState → Type
_⊢_⇀⦇_,CERT⦈_ : CertEnv → CertState → DCert → CertState → Type
\end{code}
\begin{code}[hide]
data
\end{code}
\begin{code}
_⊢_⇀⦇_,CERTBASE⦈_ : CertEnv → CertState → ⊤ → CertState → Type
\end{code}
\begin{code}
_⊢_⇀⦇_,CERTS⦈_ : CertEnv → CertState → List DCert → CertState → Type
_⊢_⇀⦇_,CERTBASE⦈_ : CertEnv → CertState → ⊤ → CertState → Type

_⊢_⇀⦇_,CERTS⦈_ : CertEnv → CertState → List DCert → CertState → Type
_⊢_⇀⦇_,CERTS⦈_ = ReflexiveTransitiveClosure _⊢_⇀⦇_,CERT⦈_
\end{code}
\end{AgdaSuppressSpace}
\end{AgdaMultiCode}
\caption{Types for the transition systems relating to certificates}
\label{fig:sts:certs-types}
\end{figure*}
Expand All @@ -318,15 +317,15 @@ data _⊢_⇀⦇_,DELEG⦈_ where
fromList ( nothing ∷ just abstainRep ∷ just noConfidenceRep ∷ [] )
∙ mkh ∈ mapˢ just (dom pools) ∪ ❴ nothing ❵
────────────────────────────────
⟦ pp , pools , delegatees ⟧ᵈᵉ ⊢
⟦ vDelegs , sDelegs , rwds ⟧ᵈ ⇀⦇ delegate c mv mkh d ,DELEG⦈
⟦ pp , pools , delegatees ⟧ᵈᵉ ⊢ ⟦ vDelegs , sDelegs , rwds ⟧ᵈ
⇀⦇ delegate c mv mkh d ,DELEG⦈
⟦ insertIfJust c mv vDelegs , insertIfJust c mkh sDelegs , rwds ∪ˡ ❴ c , 0 ❵ ⟧ᵈ

DELEG-dereg :
∙ (c , 0) ∈ rwds
────────────────────────────────
⟦ pp , pools , delegatees ⟧ᵈᵉ ⊢ ⟦ vDelegs , sDelegs , rwds ⟧ᵈ ⇀⦇ dereg c d ,DELEG⦈
⟦ vDelegs ∣ ❴ c ❵ ᶜ , sDelegs ∣ ❴ c ❵ ᶜ , rwds ∣ ❴ c ❵ ᶜ ⟧ᵈ
⟦ pp , pools , delegatees ⟧ᵈᵉ ⊢ ⟦ vDelegs , sDelegs , rwds ⟧ᵈ ⇀⦇ dereg c d ,DELEG⦈
⟦ vDelegs ∣ ❴ c ❵ ᶜ , sDelegs ∣ ❴ c ❵ ᶜ , rwds ∣ ❴ c ❵ ᶜ ⟧ᵈ
\end{code}
\end{AgdaSuppressSpace}
\caption{Auxiliary DELEG transition system}
Expand Down Expand Up @@ -430,7 +429,8 @@ data _⊢_⇀⦇_,CERTBASE⦈_ where
refresh = mapPartial getDRepVote (fromList vs)
refreshedDReps = mapValueRestricted (const (e + drepActivity)) dReps refresh
wdrlCreds = mapˢ stake (dom wdrls)
validVoteDelegs = voteDelegs ∣^ (mapˢ (credVoter DRep) (dom dReps) ∪ fromList (noConfidenceRep ∷ abstainRep ∷ []))
validVoteDelegs = voteDelegs ∣^ ( mapˢ (credVoter DRep) (dom dReps)
∪ fromList (noConfidenceRep ∷ abstainRep ∷ []) )
in
∙ filter isKeyHash wdrlCreds ⊆ dom voteDelegs
∙ mapˢ (map₁ stake) (wdrls ˢ) ⊆ rewards ˢ
Expand Down
10 changes: 5 additions & 5 deletions src/Ledger/Certs/Properties.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -221,7 +221,11 @@ module CERTSpov (Γ : CertEnv)
injOn _ h {record { stake = stakex }} {record { stake = stakey }} x∈ y∈ refl =
cong (λ u → record { net = u ; stake = stakex }) (trans (h x∈) (sym (h y∈)))

module _
CERTS-pov : {s₁ sₙ : CertState} → Γ ⊢ s₁ ⇀⦇ l ,CERTS⦈ sₙ → getCoin s₁ ≡ getCoin sₙ
CERTS-pov (BS-base Id-nop) = refl
CERTS-pov (BS-ind x xs) = trans (CERT-pov x) (CERTS-pov xs)

module CERTBASEpov
-- TODO: prove some or all of the following assumptions, used in roof of `CERTBASE-pov`.
( sumConstZero : {A : Type} ⦃ _ : DecEq A ⦄ {X : ℙ A} → getCoin (constMap X 0) ≡ 0 )
( res-decomp : {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ Coin)
Expand Down Expand Up @@ -281,9 +285,5 @@ module CERTSpov (Γ : CertEnv)
getCoin (zeroMap ∪ˡ rewards) + getCoin wdrls
∎

CERTS-pov : {s₁ sₙ : CertState} → Γ ⊢ s₁ ⇀⦇ l ,CERTS⦈ sₙ → getCoin s₁ ≡ getCoin sₙ
CERTS-pov (BS-base Id-nop) = refl
CERTS-pov (BS-ind x xs) = trans (CERT-pov x) (CERTS-pov xs)

-- TODO: Prove the following property.
-- range vDelegs ⊆ map (credVoter DRep) (dom DReps)
10 changes: 5 additions & 5 deletions src/Ledger/Ledger.lagda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -80,7 +80,7 @@ private variable
s s' s'' : LState
utxoSt' : UTxOState
govSt' : GovState
certState₀ certState₁ certState' : CertState
certState' certState'' : CertState
tx : Tx
\end{code}

Expand Down Expand Up @@ -111,11 +111,11 @@ data
Γᶜ = ⟦ epoch slot , pparams , txvote , txwdrls ⟧ᶜ in
∙ isValid tx ≡ true
∙ record { LEnv Γ } ⊢ utxoSt ⇀⦇ tx ,UTXOW⦈ utxoSt'
∙ Γᶜ ⊢ certState ⇀⦇ _ ,CERTBASE⦈ certState₁
∙ Γᶜ ⊢ certState₁ ⇀⦇ txcerts ,CERTS⦈ certState'
∙ ⟦ txid , epoch slot , pparams , ppolicy , enactState , certState' ⟧ᵍ ⊢ govSt |ᵒ certState' ⇀⦇ txgov txb ,GOV⦈ govSt'
∙ Γᶜ ⊢ certState ⇀⦇ _ ,CERTBASE⦈ certState'
∙ Γᶜ ⊢ certState' ⇀⦇ txcerts ,CERTS⦈ certState''
∙ ⟦ txid , epoch slot , pparams , ppolicy , enactState , certState'' ⟧ᵍ ⊢ govSt |ᵒ certState'' ⇀⦇ txgov txb ,GOV⦈ govSt'
────────────────────────────────
Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ ⟦ utxoSt' , govSt' , certState' ⟧ˡ
Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ ⟦ utxoSt' , govSt' , certState'' ⟧ˡ
\end{code}
\begin{NoConway}
\begin{code}
Expand Down
53 changes: 27 additions & 26 deletions src/Ledger/Ledger/Properties.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -73,9 +73,9 @@ instance
computeProof = case isValid ≟ true of λ where
(yes p) → do
(utxoSt' , utxoStep) ← computeUtxow utxoΓ utxoSt tx
(certState₁ , certStep) ← computeCert certΓ certState _
(certState' , certStep') ← computeCerts certΓ certState₁ txcerts
(govSt' , govStep) ← computeGov (govΓ certState') (govSt |ᵒ certState') (txgov txb)
(certState' , certStep) ← computeCert certΓ certState _
(certState'' , certStep') ← computeCerts certΓ certState' txcerts
(govSt' , govStep) ← computeGov (govΓ certState'') (govSt |ᵒ certState'') (txgov txb)
success (_ , LEDGER-V⋯ p utxoStep certStep certStep' govStep)
(no ¬p) → do
(utxoSt' , utxoStep) ← computeUtxow utxoΓ utxoSt tx
Expand All @@ -89,12 +89,12 @@ instance
with computeUtxow utxoΓ utxoSt tx | complete _ _ _ _ utxoStep
... | success (utxoSt' , _) | refl
with computeCert certΓ certState _ | complete certΓ _ _ _ certStep
... | success (certState₁ , _) | refl
with computeCerts certΓ certState₁ txcerts | complete certΓ _ _ _ certStep'
... | success (certState' , _) | refl
with computeGov (govΓ certState') (govSt |ᵒ certState') (txgov txb) | complete {STS = _⊢_⇀⦇_,GOV⦈_} (govΓ certState') _ _ _ govStep
with computeCerts certΓ certState' txcerts | complete certΓ _ _ _ certStep'
... | success (certState'' , _) | refl
with computeGov (govΓ certState'') (govSt |ᵒ certState'') (txgov txb) | complete {STS = _⊢_⇀⦇_,GOV⦈_} (govΓ certState'') _ _ _ govStep
... | success (govSt' , _) | refl = refl
completeness ⟦ utxoSt' , govSt' , certState' ⟧ˡ (LEDGER-I⋯ i utxoStep)
completeness ⟦ utxoSt' , govSt' , certState'' ⟧ˡ (LEDGER-I⋯ i utxoStep)
with isValid ≟ true
... | yes refl = case i of λ ()
... | no ¬v
Expand Down Expand Up @@ -138,34 +138,35 @@ module _
LEDGER-pov
{s = ⟦ utxoSt , govSt , ⟦ stᵈ , stᵖ , stᵍ ⟧ᶜˢ ⟧ˡ}
{s' = ⟦ utxoSt' , govSt' , ⟦ stᵈ' , stᵖ' , stᵍ' ⟧ᶜˢ ⟧ˡ}
h (LEDGER-V {s = s} {utxoSt' = utxoSt'} {certState₁} ( valid , UTXOW⇒UTXO st@(UTXO-induction r) , h' , h'' , _ )) =
h (LEDGER-V {s = s} {utxoSt' = utxoSt'} {certState'} ( valid , UTXOW⇒UTXO st@(UTXO-induction r) , h' , h'' , _ )) =
let
open ≡-Reasoning
open LState s using (certState)
open CERTSpov ⟦ epoch slot , pparams , txvote , txwdrls ⟧ᶜ indexedSumᵛ'-∪
certState' = ⟦ stᵈ' , stᵖ' , stᵍ' ⟧ᶜˢ
open CERTBASEpov sumConstZero res-decomp getCoin-cong ≡ᵉ-getCoinˢ r
certState'' = ⟦ stᵈ' , stᵖ' , stᵍ' ⟧ᶜˢ
zeroMap = constMap (mapˢ RwdAddr.stake (dom txwdrls)) 0
in
begin
getCoin utxoSt + getCoin certState
≡⟨ cong (getCoin utxoSt +_)
( begin rewardsBalance stᵈ
≡⟨ CERTBASE-pov sumConstZero res-decomp getCoin-cong ≡ᵉ-getCoinˢ r h' ⟩
getCoin certState₁ + getCoin txwdrls
≡⟨ cong (_+ getCoin txwdrls) (CERTS-pov sumConstZero res-decomp getCoin-cong ≡ᵉ-getCoinˢ r h'') ⟩
rewardsBalance (CertState.dState certState') + getCoin txwdrls
≡⟨ CERTBASE-pov h' ⟩
getCoin certState' + getCoin txwdrls
≡⟨ cong (_+ getCoin txwdrls) (CERTS-pov h'') ⟩
rewardsBalance (CertState.dState certState'') + getCoin txwdrls
∎
)
⟩
getCoin utxoSt + (getCoin certState' + getCoin txwdrls)
≡˘⟨ cong (λ u → getCoin utxoSt + (getCoin certState' + φ (getCoin txwdrls , u))) valid ⟩
getCoin utxoSt + (getCoin certState' + φ (getCoin txwdrls , isValid))
≡⟨ cong (getCoin utxoSt +_) (+-comm (getCoin certState') _) ⟩
getCoin utxoSt + (φ (getCoin txwdrls , isValid) + getCoin certState')
≡˘⟨ +-assoc (getCoin utxoSt) (φ (getCoin txwdrls , isValid)) (getCoin certState') ⟩
getCoin utxoSt + φ (getCoin txwdrls , isValid) + getCoin certState'
≡⟨ cong (_+ getCoin certState') (pov h st) ⟩
getCoin utxoSt' + getCoin certState'
getCoin utxoSt + (getCoin certState'' + getCoin txwdrls)
≡˘⟨ cong (λ u → getCoin utxoSt + (getCoin certState'' + φ (getCoin txwdrls , u))) valid ⟩
getCoin utxoSt + (getCoin certState'' + φ (getCoin txwdrls , isValid))
≡⟨ cong (getCoin utxoSt +_) (+-comm (getCoin certState'') _) ⟩
getCoin utxoSt + (φ (getCoin txwdrls , isValid) + getCoin certState'')
≡˘⟨ +-assoc (getCoin utxoSt) (φ (getCoin txwdrls , isValid)) (getCoin certState'') ⟩
getCoin utxoSt + φ (getCoin txwdrls , isValid) + getCoin certState''
≡⟨ cong (_+ getCoin certState'') (pov h st) ⟩
getCoin utxoSt' + getCoin certState''
∎

LEDGER-pov s@{s = ⟦ ⟦ utxo , fees , deposits , donations ⟧ᵘ , govSt , ⟦ dState , pState , gState ⟧ᶜˢ ⟧ˡ}
Expand Down Expand Up @@ -252,7 +253,7 @@ module LEDGER-PROPS (tx : Tx) (Γ : LEnv) (s : LState) where
→ (_⊢_⇀⟦_⟧ᵢ*'_ IdSTS _⊢_⇀⦇_,GOV'⦈_ (⟦ txid , epoch slot , pp , ppolicy , enactState , certSt ⟧ᵍ , k) govSt vps govSt')
→ govSt' ≡ updateGovStates vps k govSt
STS→updateGovSt≡ [] _ (BS-base Id-nop) = refl
STS→updateGovSt≡ (inj₁ v ∷ vps) k {govSt}(BS-ind (GOV-Vote x) h)
STS→updateGovSt≡ (inj₁ v ∷ vps) k (BS-ind (GOV-Vote x) h)
= STS→updateGovSt≡ vps (suc k) h
STS→updateGovSt≡ (inj₂ p ∷ vps) k (BS-ind (GOV-Propose x) h) = STS→updateGovSt≡ vps (suc k) h

Expand Down Expand Up @@ -544,7 +545,7 @@ module SetoidProperties (tx : Tx) (Γ : LEnv) (s : LState) where

LEDGER-govDepsMatch s'@{⟦ .(⟦ ((UTxOState.utxo (LState.utxoSt s) ∣ txins ᶜ) ∪ˡ (outs txb))
, _ , updateDeposits pp txb (UTxOState.deposits (LState.utxoSt s)) , _ ⟧ᵘ)
, govSt' , certState' ⟧ˡ}
, govSt' , certState'' ⟧ˡ}
utxosts@(LEDGER-V⋯ tx-valid (UTXOW-UTXOS (Scripts-Yes x)) _ _ GOV-sts) aprioriMatch = begin
filterˢ isGADeposit (dom (updateDeposits pp txb utxoDeps))
≈⟨ noGACerts txcerts (updateProposalDeposits txprop txid govActionDeposit utxoDeps) ⟩
Expand All @@ -553,8 +554,8 @@ module SetoidProperties (tx : Tx) (Γ : LEnv) (s : LState) where
fromList (dpMap (updateGovStates (map inj₂ txprop) 0 govSt))
≈˘⟨ props-dpMap-votes-invar txvote txprop ⟩
fromList (dpMap (updateGovStates (txgov txb) 0 govSt ))
≈˘⟨ |ᵒ-GAs-pres 0 govSt certState' ⟩
fromList (dpMap (updateGovStates (txgov txb) 0 (govSt |ᵒ certState')))
≈˘⟨ |ᵒ-GAs-pres 0 govSt certState'' ⟩
fromList (dpMap (updateGovStates (txgov txb) 0 (govSt |ᵒ certState'')))
≡˘⟨ cong (fromList ∘ dpMap ) (STS→GovSt≡ utxosts tx-valid) ⟩
fromList (dpMap govSt') ∎

Expand Down

0 comments on commit 20ffac4

Please sign in to comment.