Skip to content

Commit 4e33baf

Browse files
SoupstrawSoupstraw
committed
moved a check from CERTS to LEDGER
1 parent 5109173 commit 4e33baf

File tree

10 files changed

+54
-41
lines changed

10 files changed

+54
-41
lines changed

‎default.nix

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -74,7 +74,6 @@ let
7474

7575
in rec
7676
{
77-
7877
agdaWithDeps = agdaWithPkgs deps;
7978

8079
latex = texlive.combine {

‎src/Ledger/Certs.lagda

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -466,7 +466,6 @@ data _⊢_⇀⦇_,CERTBASE⦈_ where
466466
validVoteDelegs = voteDelegs ∣^ ( mapˢ (credVoter DRep) (dom dReps)
467467
∪ fromList (noConfidenceRep ∷ abstainRep ∷ []) )
468468
in
469-
∙ filter isKeyHash wdrlCreds ⊆ dom voteDelegs
470469
∙ mapˢ (map₁ stake) (wdrls ˢ) ⊆ rewards ˢ
471470
────────────────────────────────
472471
⟦ e , pp , vs , wdrls , cc ⟧ ⊢

‎src/Ledger/Certs/Properties.agda

Lines changed: 7 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -148,15 +148,13 @@ instance
148148
open GState (gState cs); open DState (dState cs)
149149
refresh = mapPartial getDRepVote (fromList votes)
150150
refreshedDReps = mapValueRestricted (const (CertEnv.epoch ce + drepActivity)) dreps refresh
151-
in case ¿ filterˢ isKeyHash (mapˢ RwdAddr.stake (dom wdrls)) ⊆ dom voteDelegs
152-
× mapˢ (map₁ RwdAddr.stake) (wdrls ˢ) ⊆ rewards ˢ ¿ of λ where
153-
(yes p) → success (-, CERT-base p)
151+
in case ¿ mapˢ (map₁ RwdAddr.stake) (wdrls ˢ) ⊆ rewards ˢ ¿ of λ where
152+
(yes p) → success (-, CERT-base (p {_}))
154153
(no ¬p) → failure (genErrors ¬p)
155-
Computational-CERTBASE .completeness ce st _ st' (CERT-base p)
156-
rewrite let dState = CertState.dState st; open DState dState in
157-
dec-yes ¿ filterˢ isKeyHash (mapˢ RwdAddr.stake (dom (CertEnv.wdrls ce))) ⊆ dom voteDelegs
158-
× mapˢ (map₁ RwdAddr.stake) (CertEnv.wdrls ce ˢ) ⊆ rewards ˢ ¿
159-
p .proj₂ = refl
154+
Computational-CERTBASE .completeness ce st _ st' (CERT-base p) with
155+
¿ mapˢ (map₁ RwdAddr.stake) (CertEnv.wdrls ce ˢ) ⊆ (st .CertState.dState .DState.rewards) ˢ ¿
156+
... | yes _ = refl
157+
... | no ¬q = ⊥-elim (¬q p)
160158

161159
Computational-CERTS : Computational _⊢_⇀⦇_,CERTS⦈_ String
162160
Computational-CERTS = it
@@ -256,7 +254,7 @@ module _ {Γ : CertEnv}
256254

257255
CERTBASE-pov {s = cs}
258256
{s' = cs'}
259-
(CERT-base {pp}{vs}{e}{dreps}{wdrls} (_ , wdrlsCC⊆rwds)) =
257+
(CERT-base {pp}{vs}{e}{dreps}{wdrls} wdrlsCC⊆rwds) =
260258
let
261259
open DState (dState cs )
262260
open DState (dState cs') renaming (rewards to rewards')

‎src/Ledger/Conway/Conformance/Certs.agda

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -205,7 +205,6 @@ data _⊢_⇀⦇_,CERTBASE⦈_ : CertEnv → CertState → ⊤ → CertState →
205205
wdrlCreds = mapˢ stake (dom wdrls)
206206
validVoteDelegs = voteDelegs ∣^ (mapˢ (credVoter DRep) (dom dReps) ∪ fromList (noConfidenceRep ∷ abstainRep ∷ []))
207207
in
208-
∙ filterˢ isKeyHash wdrlCreds ⊆ dom voteDelegs
209208
∙ mapˢ (map₁ stake) (wdrls ˢ) ⊆ rewards ˢ
210209
────────────────────────────────
211210
⟦ e , pp , vs , wdrls , cc ⟧ ⊢

‎src/Ledger/Conway/Conformance/Certs/Properties.agda

Lines changed: 7 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -194,15 +194,13 @@ instance
194194

195195
goal : ComputationResult String
196196
(∃-syntax (_⊢_⇀⦇_,CERTBASE⦈_ ⟦ CertEnv.epoch ce , pp , votes , wdrls , _ ⟧ st sig))
197-
goal = case ¿ filterˢ isKeyHash (mapˢ RwdAddr.stake (dom wdrls)) ⊆ dom voteDelegs
198-
× mapˢ (map₁ RwdAddr.stake) (wdrls ˢ) ⊆ rewards ˢ ¿ of λ where
199-
(yes p) → success (-, CERT-base p)
200-
(no ¬p) → failure (genErr ¬p)
201-
Computational-CERTBASE .completeness ce st _ st' (CERT-base p)
202-
rewrite let dState = CertState.dState st; open DState dState; open CertEnv ce in
203-
dec-yes ¿ filterˢ isKeyHash (mapˢ RwdAddr.stake (dom wdrls)) ⊆ dom voteDelegs
204-
× mapˢ (map₁ RwdAddr.stake) (wdrls ˢ) ⊆ rewards ˢ ¿
205-
p .proj₂ = refl
197+
goal = case ¿ mapˢ (map₁ RwdAddr.stake) (wdrls ˢ) ⊆ rewards ˢ ¿ of λ where
198+
(yes p) → success (-, CERT-base (p {_}))
199+
(no ¬p) → failure (genErrors ¬p)
200+
Computational-CERTBASE .completeness ce st _ st' (CERT-base p) with
201+
¿ mapˢ (map₁ RwdAddr.stake) (CertEnv.wdrls ce ˢ) ⊆ (st .CertState.dState .DState.rewards) ˢ ¿
202+
... | yes _ = refl
203+
... | no ¬q = ⊥-elim (¬q p)
206204

207205
Computational-CERTS : Computational _⊢_⇀⦇_,CERTS⦈_ String
208206
Computational-CERTS = it

‎src/Ledger/Conway/Conformance/Equivalence.agda

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -104,7 +104,7 @@ lem-cert-deposits-valid : ∀ {Γ s tx s'} (open L.LEnv Γ using (pparams))
104104
→ isValid tx ≡ true
105105
→ Γ L.⊢ s ⇀⦇ tx ,LEDGER⦈ s'
106106
→ updateLedgerDeps pparams tx (certDeposits s) ≡ᵈ certDeposits s'
107-
lem-cert-deposits-valid {Γ} {s} {tx} {s'} refl (L.LEDGER-V⋯ refl utxow certs gov) rewrite sym (lemUpdateDeposits refl utxow) =
107+
lem-cert-deposits-valid {Γ} {s} {tx} {s'} refl (L.LEDGER-V⋯ refl utxow certs u gov) rewrite sym (lemUpdateDeposits refl utxow) =
108108
lem-upd-ddeps pparams deps tx ,
109109
lem-upd-gdeps pparams deps tx
110110
where
@@ -137,7 +137,7 @@ instance
137137
certDeposits-s' ≡ᵈ certDeposits s'
138138
× Γ C.⊢ (certDeposits s ⊢conv s) ⇀⦇ tx ,LEDGER⦈ (certDeposits-s' ⊢conv s')
139139
-- LEDGERToConf {Γ} {s} {tx} {s'} .convⁱ (cdeps , eq-cdeps) r@(L.LEDGER-V⋯ refl utxow certs gov) =
140-
LEDGERToConf {Γ} {s} {tx} {s'} .convⁱ _ r@(L.LEDGER-V⋯ refl utxow certs gov) =
140+
LEDGERToConf {Γ} {s} {tx} {s'} .convⁱ _ r@(L.LEDGER-V⋯ refl utxow certs u gov) =
141141
updateLedgerDeps pparams tx (certDeposits s)
142142
, lem-cert-deposits-valid refl r
143143
, subst₂ (λ • ◆ → Γ C.⊢ getCertDeps* cdeposits ⊢conv s ⇀⦇ tx ,LEDGER⦈ ⟦ • , _ , ◆ ⟧)
@@ -157,7 +157,7 @@ instance
157157
certs' : _ C.⊢ (getCertDeps* cdeposits ⊢conv certState) ⇀⦇ txcerts ,CERTS⦈ certStateC'
158158
certs' = cdeposits ⊢conv certs
159159
ledger' : Γ C.⊢ (getCertDeps* cdeposits ⊢conv s) ⇀⦇ tx ,LEDGER⦈ C.⟦ utxoStC' , govSt' , certStateC' ⟧ˡ
160-
ledger' = C.LEDGER-V⋯ refl utxow' certs' gov
160+
ledger' = C.LEDGER-V⋯ refl utxow' certs' u gov
161161
utxoEq : utxoStC' ≡ utxoSt'
162162
utxoEq = cong (λ • → ⟦ _ , _ , • , _ ⟧)
163163
(lemUpdateDeposits refl utxow)
@@ -228,7 +228,7 @@ instance
228228
⭆ Γ L.⊢ conv s ⇀⦇ tx ,LEDGER⦈ conv s'
229229
LEDGERFromConf .convⁱ _ (C.LEDGER-I⋯ invalid utxow) with inj₁ invalid ⊢conv utxow
230230
... | utxow' rewrite lemInvalidDepositsC invalid utxow = L.LEDGER-I⋯ invalid utxow'
231-
LEDGERFromConf {Γ} {s} {tx} {s'} .convⁱ wf (C.LEDGER-V⋯ refl utxow certs gov) =
231+
LEDGERFromConf {Γ} {s} {tx} {s'} .convⁱ wf (C.LEDGER-V⋯ refl utxow certs u gov) =
232232
subst (λ • → Γ L.⊢ conv s ⇀⦇ tx ,LEDGER⦈ ⟦ • , govSt' , conv certSt' ⟧) eqUtxo ledger'
233233
where
234234
open C.LEnv Γ
@@ -251,7 +251,7 @@ instance
251251
ledger' : Γ L.⊢ conv s ⇀⦇ tx ,LEDGER⦈ L.⟦ setDeposits (utxowDeposits utxow) utxoSt'
252252
, govSt'
253253
, conv certSt' ⟧ˡ
254-
ledger' = L.LEDGER-V⋯ refl utxow' (conv certs) gov
254+
ledger' = L.LEDGER-V⋯ refl utxow' (conv certs) u gov
255255

256256
open IsEquivalence ≡ᵈ-isEquivalence renaming (refl to ≡ᵈ-refl; sym to ≡ᵈ-sym; trans to ≡ᵈ-trans)
257257

@@ -269,7 +269,7 @@ lemCERTS'DepositsC (BS-ind (C.CERT-vdel (C.GOVCERT-deregdrep _)) rs) = lemCERTS'
269269
lemCERTS'DepositsC (BS-ind (C.CERT-vdel (C.GOVCERT-ccreghot _)) rs) = lemCERTS'DepositsC rs
270270

271271
lemWellformed : ∀ {Γ s tx s'} → WellformedLState s → Γ C.⊢ s ⇀⦇ tx ,LEDGER⦈ s' → WellformedLState s'
272-
lemWellformed {Γ} {s = ls} {tx} {s' = ls'} wf (C.LEDGER-V⋯ refl utxo certs gov) = goal
272+
lemWellformed {Γ} {s = ls} {tx} {s' = ls'} wf (C.LEDGER-V⋯ refl utxo certs u gov) = goal
273273
where
274274
open C.LState ls renaming (certState to certSt)
275275
open C.LState ls' renaming (utxoSt to utxoSt'; certState to certSt')
@@ -377,9 +377,9 @@ opaque
377377
→ deps₁ ≡ᵈ deps₂
378378
→ Γ C.⊢ deps₁ ⊢conv s ⇀⦇ tx ,LEDGER⦈ (deps₁' ⊢conv s')
379379
→ ∃[ deps₂' ] deps₁' ≡ᵈ deps₂' × Γ C.⊢ deps₂ ⊢conv s ⇀⦇ tx ,LEDGER⦈ (deps₂' ⊢conv s')
380-
castLEDGER {Γ} {tx} {s} {s'} deps₁ deps₂ deps₁' eqd (C.LEDGER-V⋯ refl utxo certs gov) =
380+
castLEDGER {Γ} {tx} {s} {s'} deps₁ deps₂ deps₁' eqd (C.LEDGER-V⋯ refl utxo certs u gov) =
381381
let deps₂' , eqd' , certs' = castCERTS' deps₁ deps₂ deps₁' eqd certs
382-
in deps₂' , eqd' , C.LEDGER-V⋯ refl utxo certs' gov
382+
in deps₂' , eqd' , C.LEDGER-V⋯ refl utxo certs' u gov
383383
castLEDGER deps₁ deps₂ deps₁' eqd (C.LEDGER-I⋯ refl utxo) = _ , eqd , C.LEDGER-I⋯ refl utxo
384384

385385
---------------------------------------------------------------------------

‎src/Ledger/Conway/Conformance/Ledger.agda

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -54,10 +54,12 @@ data
5454
let open LState s; txb = tx .body; open TxBody txb; open LEnv Γ
5555
open CertState certState; open DState dState
5656
utxoSt'' = record utxoSt' { deposits = updateDeposits pparams txb (deposits utxoSt') }
57+
wdrlCreds = mapˢ RwdAddr.stake (dom txwdrls)
5758
in
5859
∙ isValid tx ≡ true
5960
∙ record { LEnv Γ } ⊢ utxoSt ⇀⦇ tx ,UTXOW⦈ utxoSt'
6061
∙ ⟦ epoch slot , pparams , txvote , txwdrls , allColdCreds govSt enactState ⟧ ⊢ certState ⇀⦇ txcerts ,CERTS⦈ certState'
62+
∙ filterˢ isKeyHash wdrlCreds ⊆ dom voteDelegs
6163
∙ ⟦ txid , epoch slot , pparams , ppolicy , enactState , certState' , dom
6264
rewards ⟧ ⊢ govSt ⇀⦇ txgov txb ,GOVS⦈ govSt'
6365
────────────────────────────────
@@ -70,8 +72,8 @@ data
7072
────────────────────────────────
7173
Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ ⟦ utxoSt' , govSt , certState ⟧
7274

73-
pattern LEDGER-V⋯ w x y z = LEDGER-V (w , x , y , z)
74-
pattern LEDGER-I⋯ y z = LEDGER-I (y , z)
75+
pattern LEDGER-V⋯ w x y z t = LEDGER-V (w , x , y , z , t)
76+
pattern LEDGER-I⋯ y z = LEDGER-I (y , z)
7577

7678
_⊢_⇀⦇_,LEDGERS⦈_ : LEnv → LState → List Tx → LState → Type
7779
_⊢_⇀⦇_,LEDGERS⦈_ = ReflexiveTransitiveClosure {sts = _⊢_⇀⦇_,LEDGER⦈_}

‎src/Ledger/Conway/Conformance/Ledger/Properties.agda

Lines changed: 12 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -36,6 +36,8 @@ open import Data.Nat.Properties using (+-0-monoid; +-identityʳ; +-suc; +-comm)
3636
open import Relation.Binary using (IsEquivalence)
3737
open import Relation.Unary using (Decidable)
3838

39+
open import Tactic.GenError using (genErrors)
40+
3941
open import Ledger.Conway.Conformance.Equivalence.Certs txs abs
4042
open import Ledger.Conway.Conformance.Equivalence.Convert
4143

@@ -75,23 +77,29 @@ instance
7577
(yes p) → do
7678
(utxoSt' , utxoStep) ← computeUtxow utxoΓ utxoSt tx
7779
(certSt' , certStep) ← computeCerts certΓ certState txcerts
80+
let wdrlCreds = mapˢ RwdAddr.stake (dom txwdrls)
81+
wdrlsCheck ← case ¿ filterˢ isKeyHash wdrlCreds ⊆ dom (certState .CertState.dState .DState.voteDelegs) ¿ of λ where
82+
(yes q) → success q
83+
(no ¬q) → failure (genErrors ¬q)
7884
(govSt' , govStep) ← computeGov (govΓ certSt') (rmOrphanDRepVotes (conv certSt') govSt) (txgov txb)
79-
success (_ , LEDGER-V⋯ p utxoStep certStep govStep)
85+
success (_ , LEDGER-V⋯ p utxoStep certStep wdrlsCheck govStep)
8086
(no ¬p) → do
8187
(utxoSt' , utxoStep) ← computeUtxow utxoΓ utxoSt tx
8288
success (_ , LEDGER-I⋯ (¬-not ¬p) utxoStep)
8389

8490
completeness : ∀ s' → Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ s' → (proj₁ <$> computeProof) ≡ success s'
85-
completeness ls' (LEDGER-V⋯ v utxoStep certStep govStep)
91+
completeness ls' (LEDGER-V⋯ v utxoStep certStep u govStep)
8692
with isValid ≟ true
8793
... | no ¬v = contradiction v ¬v
8894
... | yes refl
8995
with computeUtxow utxoΓ utxoSt tx | complete _ _ _ _ utxoStep
9096
... | success (utxoSt' , _) | refl
9197
with computeCerts certΓ certState txcerts | complete _ _ _ _ certStep
9298
... | success (certSt' , _) | refl
93-
with computeGov (govΓ certSt') (rmOrphanDRepVotes (conv certSt') govSt) (txgov txb) | complete {STS = _⊢_⇀⦇_,GOVS⦈_} (govΓ certSt') _ _ _ govStep
94-
... | success (govSt' , _) | refl = refl
99+
with dec-yes ¿ filterˢ isKeyHash (mapˢ RwdAddr.stake (dom txwdrls)) ⊆ dom (certState .CertState.dState .DState.voteDelegs) ¿ (λ { x → u x })
100+
... | (_ , p)
101+
with computeGov (govΓ certSt') (rmOrphanDRepVotes (conv certSt') govSt ) (txgov txb) | complete {STS = _⊢_⇀⦇_,GOVS⦈_} (govΓ certSt') _ _ _ govStep
102+
... | success (govSt' , _) | refl rewrite p = refl
95103
completeness ls' (LEDGER-I⋯ i utxoStep)
96104
with isValid ≟ true
97105
... | yes refl = case i of λ ()

‎src/Ledger/Ledger.lagda

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -116,10 +116,12 @@ data _⊢_⇀⦇_,LEDGER⦈_ : LEnv → LState → Tx → LState → Type where
116116
\end{code}
117117
\begin{code}
118118
rewards = certState .dState .rewards
119+
wdrlCreds = mapˢ RwdAddr.stake (dom txwdrls)
119120
in
120121
∙ isValid tx ≡ true
121122
∙ ⟦ slot , pp , treasury ⟧ ⊢ utxoSt ⇀⦇ tx ,UTXOW⦈ utxoSt'
122123
∙ ⟦ epoch slot , pp , txvote , txwdrls , allColdCreds govSt enactState ⟧ ⊢ certState ⇀⦇ txcerts ,CERTS⦈ certState'
124+
∙ filterˢ isKeyHash wdrlCreds ⊆ dom (certState .dState .voteDelegs)
123125
∙ ⟦ txid , epoch slot , pp , ppolicy , enactState , certState' , dom rewards ⟧ ⊢ rmOrphanDRepVotes certState' govSt ⇀⦇ txgov txb ,GOVS⦈ govSt'
124126
────────────────────────────────
125127
⟦ slot , ppolicy , pp , enactState , treasury ⟧ ⊢ ⟦ utxoSt , govSt , certState ⟧ ⇀⦇ tx ,LEDGER⦈ ⟦ utxoSt' , govSt' , certState' ⟧
@@ -134,7 +136,7 @@ data _⊢_⇀⦇_,LEDGER⦈_ : LEnv → LState → Tx → LState → Type where
134136
\caption{LEDGER transition system}
135137
\end{figure*}
136138
\begin{code}[hide]
137-
pattern LEDGER-V⋯ w x y z = LEDGER-V (w , x , y , z)
139+
pattern LEDGER-V⋯ w x y z a = LEDGER-V (w , x , y , z , a)
138140
pattern LEDGER-I⋯ y z = LEDGER-I (y , z)
139141
\end{code}
140142

‎src/Ledger/Ledger/Properties.agda

Lines changed: 13 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -37,6 +37,8 @@ open import Data.Nat.Properties using (+-0-monoid; +-identityʳ; +-suc; +-comm;
3737
open import Relation.Binary using (IsEquivalence)
3838
open import Relation.Unary using (Decidable)
3939

40+
open import Tactic.GenError using (genErrors)
41+
4042
import Function.Related.Propositional as R
4143

4244
import Relation.Binary.Reasoning.Setoid as SetoidReasoning
@@ -73,23 +75,29 @@ instance
7375
(yes p) → do
7476
(utxoSt' , utxoStep) ← computeUtxow utxoΓ utxoSt tx
7577
(certSt' , certStep) ← computeCerts certΓ certState txcerts
78+
let wdrlCreds = mapˢ RwdAddr.stake (dom txwdrls)
79+
wdrlsCheck ← case ¿ filterˢ isKeyHash wdrlCreds ⊆ dom (certSt' .CertState.dState .DState.voteDelegs) ¿ of λ where
80+
(yes q) → success q
81+
(no ¬q) → failure (genErrors ¬q)
7682
(govSt' , govStep) ← computeGov (govΓ certSt') (rmOrphanDRepVotes certSt' govSt) (txgov txb)
77-
success (_ , LEDGER-V⋯ p utxoStep certStep govStep)
83+
success (_ , LEDGER-V⋯ p utxoStep certStep wdrlsCheck govStep)
7884
(no ¬p) → do
7985
(utxoSt' , utxoStep) ← computeUtxow utxoΓ utxoSt tx
8086
success (_ , LEDGER-I⋯ (¬-not ¬p) utxoStep)
8187

8288
completeness : ∀ s' → Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ s' → (proj₁ <$> computeProof) ≡ success s'
83-
completeness ledgerSt (LEDGER-V⋯ v utxoStep certStep govStep)
89+
completeness ledgerSt (LEDGER-V⋯ v utxoStep certStep u govStep)
8490
with isValid ≟ true
8591
... | no ¬v = contradiction v ¬v
8692
... | yes refl
8793
with computeUtxow utxoΓ utxoSt tx | complete _ _ _ _ utxoStep
8894
... | success (utxoSt' , _) | refl
8995
with computeCerts certΓ certState txcerts | complete _ _ _ _ certStep
9096
... | success (certSt' , _) | refl
97+
with dec-yes ¿ filterˢ isKeyHash (mapˢ RwdAddr.stake (dom txwdrls)) ⊆ dom (certSt' .CertState.dState .DState.voteDelegs) ¿ (λ { x → u x })
98+
... | (_ , p)
9199
with computeGov (govΓ certSt') (rmOrphanDRepVotes certSt' govSt ) (txgov txb) | complete {STS = _⊢_⇀⦇_,GOVS⦈_} (govΓ certSt') _ _ _ govStep
92-
... | success (govSt' , _) | refl = refl
100+
... | success (govSt' , _) | refl rewrite p = refl
93101
completeness ledgerSt (LEDGER-I⋯ i utxoStep)
94102
with isValid ≟ true
95103
... | yes refl = case i of λ ()
@@ -251,7 +259,7 @@ module LEDGER-PROPS (tx : Tx) (Γ : LEnv) (s : LState) where
251259
STS→GovSt≡ : ∀ {s' : LState} → Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ s'
252260
→ isValid ≡ true → LState.govSt s' ≡ updateGovStates (txgov txb) 0 (rmOrphanDRepVotes (LState.certState s') (LState.govSt s))
253261
-- STS→GovSt≡ (LEDGER-V ( _ , _ , _ , x )) refl = STS→updateGovSt≡ (txgov txb) 0 x
254-
STS→GovSt≡ (LEDGER-V x) refl = STS→updateGovSt≡ (txgov txb) 0 (proj₂ (proj₂ (proj₂ x)))
262+
STS→GovSt≡ (LEDGER-V (_ , _ , _ , _ , x)) refl = STS→updateGovSt≡ (txgov txb) 0 x
255263
where
256264
STS→updateGovSt≡ : (vps : List (GovVote ⊎ GovProposal)) (k : ℕ) {certSt : CertState} {govSt govSt' : GovState}
257265
→ (_⊢_⇀⟦_⟧ᵢ*'_ {_⊢_⇀⟦_⟧ᵇ_ = IdSTS}{_⊢_⇀⦇_,GOV⦈_} (⟦ txid , epoch slot , pp , ppolicy , enactState , certSt , dom rewards ⟧ , k) govSt vps govSt')
@@ -536,7 +544,7 @@ module SetoidProperties (tx : Tx) (Γ : LEnv) (s : LState) where
536544
LEDGER-govDepsMatch (LEDGER-I⋯ refl (UTXOW-UTXOS (Scripts-No _))) aprioriMatch = aprioriMatch
537545

538546
LEDGER-govDepsMatch {s' = s'}
539-
utxosts@(LEDGER-V⋯ tx-valid (UTXOW-UTXOS (Scripts-Yes x)) _ GOV-sts) aprioriMatch =
547+
utxosts@(LEDGER-V⋯ tx-valid (UTXOW-UTXOS (Scripts-Yes x)) _ _ GOV-sts) aprioriMatch =
540548
let open LState s' renaming (govSt to govSt'; certState to certState') in
541549
begin
542550
filterˢ isGADeposit (dom (updateDeposits pp txb utxoDeps))

0 commit comments

Comments
 (0)