Skip to content

Commit 35e0909

Browse files
SoupstrawSoupstraw
committed
Added expiry check
1 parent ffc2fe3 commit 35e0909

File tree

6 files changed

+37
-33
lines changed

6 files changed

+37
-33
lines changed

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -396,8 +396,8 @@ opaque
396396
→ (record Γ { certState = certState' } , n)
397397
⊢ s ⇀⦇ txgov ,GOVn⦈ s'
398398
castGOV deps (BS-base Id-nop) = BS-base Id-nop
399-
castGOV {Γ} deps (BS-ind (C.GOV-Vote {voter = voter} (a , b , c)) rs) =
400-
BS-ind (C.GOV-Vote (a , b , cast-isRegistered Γ deps voter c))
399+
castGOV {Γ} deps (BS-ind (C.GOV-Vote {voter = voter} (a , b , c , d)) rs) =
400+
BS-ind (C.GOV-Vote (a , b , cast-isRegistered Γ deps voter c , d))
401401
(castGOV deps rs)
402402
castGOV deps (BS-ind (C.GOV-Propose h) rs) =
403403
BS-ind (C.GOV-Propose h)

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -41,7 +41,7 @@ instance
4141
→ L.Deposits × L.Deposits
4242
⊢ (Γ , n) L.⊢ s ⇀⦇ votes ,GOV'⦈ s' ⭆ⁱ λ deposits _ →
4343
(deposits ⊢conv Γ , n) C.⊢ s ⇀⦇ votes ,GOV'⦈ s'
44-
GOV'ToConf .convⁱ deposits (L.GOV-Vote (a , b , c)) = C.GOV-Vote (a , b , deposits ⊢conv c)
44+
GOV'ToConf .convⁱ deposits (L.GOV-Vote (a , b , c , d)) = C.GOV-Vote (a , b , deposits ⊢conv c , d)
4545
GOV'ToConf .convⁱ deposits (L.GOV-Propose h) = C.GOV-Propose h
4646

4747
GOVToConf : ∀ {Γ s votes s' n}
@@ -53,7 +53,7 @@ instance
5353

5454
GOV'FromConf : ∀ {Γ s votes s' n}
5555
→ (Γ , n) C.⊢ s ⇀⦇ votes ,GOV'⦈ s' ⭆ (conv Γ , n) L.⊢ s ⇀⦇ votes ,GOV'⦈ s'
56-
GOV'FromConf .convⁱ _ (C.GOV-Vote (a , b , c)) = L.GOV-Vote (a , b , conv c)
56+
GOV'FromConf .convⁱ _ (C.GOV-Vote (a , b , c , d)) = L.GOV-Vote (a , b , conv c , d)
5757
GOV'FromConf .convⁱ _ (C.GOV-Propose h) = L.GOV-Propose h
5858

5959
GOVFromConf : ∀ {Γ s votes s' n}

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

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -77,6 +77,7 @@ data _⊢_⇀⦇_,GOV'⦈_ : GovEnv × ℕ → GovState → GovVote ⊎ GovProp
7777
∙ (aid , ast) ∈ fromList s
7878
∙ canVote pparams (action ast) (proj₁ voter)
7979
∙ isRegistered Γ voter
80+
∙ ¬ (expired epoch ast)
8081
───────────────────────────────────────
8182
(Γ , k) ⊢ s ⇀⦇ inj₁ vote ,GOV'⦈ L.addVote s aid voter v
8283

@@ -91,6 +92,7 @@ data _⊢_⇀⦇_,GOV'⦈_ : GovEnv × ℕ → GovState → GovVote ⊎ GovProp
9192
∙ L.validHFAction prop s enactState
9293
∙ L.hasParent enactState s a prev
9394
∙ addr .RwdAddr.net ≡ NetworkId
95+
∙ addr .RwdAddr.stake ∈ rewardCreds
9496
───────────────────────────────────────
9597
(Γ , k) ⊢ s ⇀⦇ inj₂ prop ,GOV'⦈ s'
9698

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

Lines changed: 9 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -36,10 +36,6 @@ open GovActionState
3636
open Inverse
3737

3838
private
39-
lookupActionId : (pparams : PParams) (role : GovRole) (aid : GovActionID) (s : GovState) →
40-
Dec (Any (λ (aid' , ast) → aid ≡ aid' × canVote pparams (action ast) role) s)
41-
lookupActionId pparams role aid = any? λ _ → ¿ _ ¿
42-
4339
isUpdateCommittee : (a : GovAction) → Dec (∃[ new ] ∃[ rem ] ∃[ q ] a ≡ UpdateCommittee new rem q)
4440
isUpdateCommittee NoConfidence = no λ()
4541
isUpdateCommittee (UpdateCommittee new rem q) = yes (new , rem , q , refl)
@@ -97,16 +93,16 @@ instance
9793
module GoVote sig where
9894
open GovVote sig
9995

100-
computeProof = case lookupActionId pparams (proj₁ voter) gid s ,′ isRegistered? (proj₁ Γ) voter of λ where
96+
computeProof = case L.lookupActionId pparams (proj₁ voter) gid epoch s ,′ isRegistered? (proj₁ Γ) voter of λ where
10197
(yes p , yes p') → case Any↔ .from p of λ where
102-
(_ , mem , refl , cV) → success (_ , GOV-Vote (∈-fromList .to mem , cV , p'))
98+
(_ , mem , refl , cV , ¬exp) → success (_ , GOV-Vote (∈-fromList .to mem , cV , p' , ¬exp))
10399
(yes _ , no ¬p) → failure (genErrors ¬p)
104100
(no ¬p , _) → failure (genErrors ¬p)
105101

106102
completeness : ∀ s' → Γ ⊢ s ⇀⦇ inj₁ sig ,GOV'⦈ s' → map proj₁ computeProof ≡ success s'
107-
completeness s' (GOV-Vote (mem , cV , reg))
108-
with lookupActionId pparams (proj₁ voter) gid s | isRegistered? (proj₁ Γ) voter
109-
... | no ¬p | _ = ⊥-elim (¬p (Any↔ .to (_ , ∈-fromList .from mem , refl , cV)))
103+
completeness s' (GOV-Vote (mem , cV , reg , ¬exp))
104+
with L.lookupActionId pparams (proj₁ voter) gid epoch s | isRegistered? (proj₁ Γ) voter
105+
... | no ¬p | _ = ⊥-elim (¬p (Any↔ .to (_ , ∈-fromList .from mem , refl , cV , ¬exp)))
110106
... | yes _ | no ¬p = ⊥-elim $ ¬p reg
111107
... | yes p | yes p' with Any↔ .from p
112108
... | (_ , mem , refl , cV) = refl
@@ -124,7 +120,8 @@ instance
124120
× d ≡ govActionDeposit
125121
× L.validHFAction prop s enactState
126122
× L.hasParent' enactState s a prev
127-
× addr .RwdAddr.net ≡ NetworkId ¿
123+
× addr .RwdAddr.net ≡ NetworkId
124+
× addr .RwdAddr.stake ∈ rewardCreds ¿
128125
,′ isUpdateCommittee a
129126

130127
genErrorsWellFormed : ∀ {a} → ¬ (L.actionWellFormed rewardCreds p ppolicy epoch a) → String
@@ -137,9 +134,9 @@ instance
137134
genErrorsWellFormed {Info} ¬p = genErrors ¬p
138135

139136
computeProof = case H of λ where
140-
(yes (wf , dep , vHFA , L.HasParent' en , goodAddr) , yes (new , rem , q , refl)) →
137+
(yes (wf , dep , vHFA , L.HasParent' en , goodAddr , regReward) , yes (new , rem , q , refl)) →
141138
case ¿ ∀[ e ∈ range new ] epoch < e × dom new ∩ rem ≡ᵉ ∅ ¿ of λ where
142-
(yes newOk) → success (_ , GOV-Propose (wf , dep , vHFA , en , goodAddr))
139+
(yes newOk) → success (_ , GOV-Propose (wf , dep , vHFA , en , goodAddr , regReward))
143140
(no ¬p) → failure (genErrors ¬p)
144141
(yes (wf , dep , vHFA , L.HasParent' en , goodAddr) , no notNewComm) → success
145142
(-, GOV-Propose (wf , dep , vHFA , en , goodAddr))

‎src/Ledger/Gov.lagda‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -354,6 +354,7 @@ data _⊢_⇀⦇_,GOV'⦈_ where
354354
∙ (aid , ast) ∈ fromList s
355355
∙ canVote pparams (action ast) (proj₁ voter)
356356
∙ isRegistered Γ voter
357+
∙ ¬ (expired epoch ast)
357358
───────────────────────────────────────
358359
(Γ , k) ⊢ s ⇀⦇ inj₁ vote ,GOV'⦈ addVote s aid voter v
359360

@@ -368,6 +369,7 @@ data _⊢_⇀⦇_,GOV'⦈_ where
368369
∙ validHFAction prop s enactState
369370
∙ hasParent enactState s a prev
370371
∙ addr .RwdAddr.net ≡ NetworkId
372+
∙ addr .RwdAddr.stake ∈ rewardCreds
371373
───────────────────────────────────────
372374
(Γ , k) ⊢ s ⇀⦇ inj₂ prop ,GOV'⦈ s'
373375

‎src/Ledger/Gov/Properties.agda‎

Lines changed: 20 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -31,11 +31,13 @@ open Equivalence
3131
open GovActionState
3232
open Inverse
3333

34-
private
35-
lookupActionId : (pparams : PParams) (role : GovRole) (aid : GovActionID) (s : GovState) →
36-
Dec (Any (λ (aid' , ast) → aid ≡ aid' × canVote pparams (action ast) role) s)
37-
lookupActionId pparams role aid = any? λ _ → ¿ _ ¿
34+
lookupActionId : (pparams : PParams) (role : GovRole) (aid : GovActionID) (epoch : Epoch) (s : GovState) →
35+
Dec (Any (λ (aid' , ast) → aid ≡ aid' × canVote pparams (action ast) role × ¬ (expired epoch ast)) s)
36+
lookupActionId pparams role aid epoch =
37+
let instance _ = λ {e ga} → ⁇ (expired? e ga)
38+
in any? λ _ → ¿ _ ¿
3839

40+
private
3941
isUpdateCommittee : (a : GovAction) → Dec (∃[ new ] ∃[ rem ] ∃[ q ] a ≡ UpdateCommittee new rem q)
4042
isUpdateCommittee NoConfidence = no λ()
4143
isUpdateCommittee (UpdateCommittee new rem q) = yes (new , rem , q , refl)
@@ -111,19 +113,19 @@ instance
111113
module GoVote sig where
112114
open GovVote sig
113115

114-
computeProof = case lookupActionId pparams (proj₁ voter) gid s ,′ isRegistered? (proj₁ Γ) voter of λ where
116+
computeProof = case lookupActionId pparams (proj₁ voter) gid epoch s ,′ isRegistered? (proj₁ Γ) voter of λ where
115117
(yes p , yes p') → case Any↔ .from p of λ where
116-
(_ , mem , refl , cV) → success (_ , GOV-Vote (∈-fromList .to mem , cV , p'))
118+
(_ , mem , refl , cV , ¬exp) → success (_ , GOV-Vote (∈-fromList .to mem , cV , p' , ¬exp))
117119
(yes _ , no ¬p) → failure (genErrors ¬p)
118-
(no ¬p , _) → failure (genErrors ¬p)
120+
(no ¬p , _ ) → failure (genErrors ¬p)
119121

120122
completeness : ∀ s' → Γ ⊢ s ⇀⦇ inj₁ sig ,GOV'⦈ s' → map proj₁ computeProof ≡ success s'
121-
completeness s' (GOV-Vote (mem , cV , reg))
122-
with lookupActionId pparams (proj₁ voter) gid s | isRegistered? (proj₁ Γ) voter
123-
... | no ¬p | _ = ⊥-elim (¬p (Any↔ .to (_ , ∈-fromList .from mem , refl , cV)))
123+
completeness s' (GOV-Vote {ast = ast} (mem , cV , reg , ¬expired))
124+
with lookupActionId pparams (proj₁ voter) gid epoch s | isRegistered? (proj₁ Γ) voter
125+
... | no ¬p | _ = ⊥-elim (¬p (Any↔ .to (_ , ∈-fromList .from mem , refl , cV , ¬expired)))
124126
... | yes _ | no ¬p = ⊥-elim $ ¬p reg
125-
... | yes p | yes p' with Any↔ .from p
126-
... | (_ , mem , refl , cV) = refl
127+
... | yes p | yes q with Any↔ .from p
128+
... | ((_ , ast') , mem , refl , cV) = refl
127129

128130
module GoProp prop where
129131
open GovProposal prop
@@ -138,16 +140,17 @@ instance
138140
× d ≡ govActionDeposit
139141
× validHFAction prop s enactState
140142
× hasParent' enactState s a prev
141-
× addr .RwdAddr.net ≡ NetworkId ¿
143+
× addr .RwdAddr.net ≡ NetworkId
144+
× addr .RwdAddr.stake ∈ rewardCreds ¿
142145
,′ isUpdateCommittee a
143146

144147
computeProof = case H of λ where
145-
(yes (wf , dep , vHFA , HasParent' en , goodAddr) , yes (new , rem , q , refl)) →
148+
(yes (wf , dep , vHFA , HasParent' en , goodAddr , regReturn) , yes (new , rem , q , refl)) →
146149
case ¿ ∀[ e ∈ range new ] epoch < e × dom new ∩ rem ≡ᵉ ∅ ¿ of λ where
147-
(yes newOk) → success (_ , GOV-Propose (wf , dep , vHFA , en , goodAddr))
150+
(yes newOk) → success (_ , GOV-Propose (wf , dep , vHFA , en , goodAddr , regReturn))
148151
(no ¬p) → failure (genErrors ¬p)
149-
(yes (wf , dep , vHFA , HasParent' en , goodAddr) , no notNewComm) → success
150-
(-, GOV-Propose (wf , dep , vHFA , en , goodAddr))
152+
(yes (wf , dep , vHFA , HasParent' en , goodAddr , returnReg) , no notNewComm) → success
153+
(-, GOV-Propose (wf , dep , vHFA , en , goodAddr , returnReg))
151154
(no ¬p , _) → failure (genErrors ¬p)
152155

153156
completeness : ∀ s' → Γ ⊢ s ⇀⦇ inj₂ prop ,GOV'⦈ s' → map proj₁ computeProof ≡ success s'

0 commit comments

Comments
 (0)