Skip to content

Commit 90229ae

Browse files
SoupstrawSoupstraw
committed
Added expiry check
1 parent ffc2fe3 commit 90229ae

File tree

6 files changed

+115
-82
lines changed

6 files changed

+115
-82
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: 4 additions & 1 deletion
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

@@ -86,11 +87,13 @@ data _⊢_⇀⦇_,GOV'⦈_ : GovEnv × ℕ → GovState → GovVote ⊎ GovProp
8687
; policy = p ; deposit = d ; prevAction = prev }
8788
s' = L.addAction s (govActionLifetime +ᵉ epoch) (txid , k) addr a prev
8889
in
89-
∙ L.actionWellFormed rewardCreds p ppolicy epoch a
90+
∙ L.actionWellFormed a
91+
∙ L.actionValid rewardCreds p ppolicy epoch a
9092
∙ d ≡ govActionDeposit
9193
∙ L.validHFAction prop s enactState
9294
∙ L.hasParent enactState s a prev
9395
∙ addr .RwdAddr.net ≡ NetworkId
96+
∙ addr .RwdAddr.stake ∈ rewardCreds
9497
───────────────────────────────────────
9598
(Γ , k) ⊢ s ⇀⦇ inj₂ prop ,GOV'⦈ s'
9699

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

Lines changed: 41 additions & 30 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
@@ -118,41 +114,56 @@ instance
118114

119115
instance
120116
Dec-actionWellFormed = L.actionWellFormed?
117+
Dec-actionValid = L.actionValid?
121118
{-# INCOHERENT Dec-actionWellFormed #-}
119+
{-# INCOHERENT Dec-actionValid #-}
122120

123-
H = ¿ L.actionWellFormed rewardCreds p ppolicy epoch a
121+
H = ¿ L.actionWellFormed a
122+
× L.actionValid rewardCreds p ppolicy epoch a
124123
× d ≡ govActionDeposit
125124
× L.validHFAction prop s enactState
126125
× L.hasParent' enactState s a prev
127-
× addr .RwdAddr.net ≡ NetworkId ¿
126+
× addr .RwdAddr.net ≡ NetworkId
127+
× addr .RwdAddr.stake ∈ rewardCreds ¿
128128
,′ isUpdateCommittee a
129129

130-
genErrorsWellFormed : ∀ {a} → ¬ (L.actionWellFormed rewardCreds p ppolicy epoch a) → String
131-
genErrorsWellFormed {NoConfidence} ¬p = genErrors ¬p
132-
genErrorsWellFormed {UpdateCommittee _ _ _} ¬p = genErrors ¬p
133-
genErrorsWellFormed {NewConstitution _ _} ¬p = genErrors ¬p
134-
genErrorsWellFormed {TriggerHF _} ¬p = genErrors ¬p
135-
genErrorsWellFormed {ChangePParams _} ¬p = genErrors ¬p
136-
genErrorsWellFormed {TreasuryWdrl _} ¬p = genErrors ¬p
137-
genErrorsWellFormed {Info} ¬p = genErrors ¬p
130+
genErrorsActionWellFormed : ∀ {a} → ¬ (L.actionWellFormed a) → String
131+
genErrorsActionWellFormed {NoConfidence} ¬p = genErrors ¬p
132+
genErrorsActionWellFormed {UpdateCommittee _ _ _} ¬p = genErrors ¬p
133+
genErrorsActionWellFormed {NewConstitution _ _} ¬p = genErrors ¬p
134+
genErrorsActionWellFormed {TriggerHF _} ¬p = genErrors ¬p
135+
genErrorsActionWellFormed {ChangePParams _} ¬p = genErrors ¬p
136+
genErrorsActionWellFormed {TreasuryWdrl _} ¬p = genErrors ¬p
137+
genErrorsActionWellFormed {Info} ¬p = genErrors ¬p
138+
139+
genErrorsActionValid : ∀ {a} → ¬ (L.actionValid rewardCreds p ppolicy epoch a) → String
140+
genErrorsActionValid {NoConfidence} ¬p = genErrors ¬p
141+
genErrorsActionValid {UpdateCommittee _ _ _} ¬p = genErrors ¬p
142+
genErrorsActionValid {NewConstitution _ _} ¬p = genErrors ¬p
143+
genErrorsActionValid {TriggerHF _} ¬p = genErrors ¬p
144+
genErrorsActionValid {ChangePParams _} ¬p = genErrors ¬p
145+
genErrorsActionValid {TreasuryWdrl _} ¬p = genErrors ¬p
146+
genErrorsActionValid {Info} ¬p = genErrors ¬p
138147

139148
computeProof = case H of λ where
140-
(yes (wf , dep , vHFA , L.HasParent' en , goodAddr) , yes (new , rem , q , refl)) →
149+
(yes (wf , av , dep , vHFA , L.HasParent' en , goodAddr , regReward) , yes (new , rem , q , refl)) →
141150
case ¿ ∀[ e ∈ range new ] epoch < e × dom new ∩ rem ≡ᵉ ∅ ¿ of λ where
142-
(yes newOk) → success (_ , GOV-Propose (wf , dep , vHFA , en , goodAddr))
151+
(yes newOk) → success (_ , GOV-Propose (wf , av , dep , vHFA , en , goodAddr , regReward))
143152
(no ¬p) → failure (genErrors ¬p)
144-
(yes (wf , dep , vHFA , L.HasParent' en , goodAddr) , no notNewComm) → success
145-
(-, GOV-Propose (wf , dep , vHFA , en , goodAddr))
153+
(yes (wf , av , dep , vHFA , L.HasParent' en , goodAddr) , no notNewComm) → success
154+
(-, GOV-Propose (wf , av , dep , vHFA , en , goodAddr))
146155
(no ¬p , _) → case dec-de-morgan ¬p of λ where
147-
(inj₁ q) → failure (genErrorsWellFormed q)
148-
(inj₂ q) → failure (genErrors q)
156+
(inj₁ q) → failure (genErrorsActionWellFormed q)
157+
(inj₂ q) → case dec-de-morgan q of λ where
158+
(inj₁ r) → failure (genErrorsActionValid r)
159+
(inj₂ r) → failure (genErrors r)
149160

150161
completeness : ∀ s' → Γ ⊢ s ⇀⦇ inj₂ prop ,GOV'⦈ s' → map proj₁ computeProof ≡ success s'
151-
completeness s' (GOV-Propose (wf , dep , vHFA , en , goodAddr)) with H
152-
... | (no ¬p , _) = ⊥-elim (¬p (wf , dep , vHFA , L.HasParent' en , goodAddr))
153-
... | (yes (_ , _ , _ , L.HasParent' _ , _) , no notNewComm) = refl
154-
... | (yes ((_ , allOk) , _ , _ , L.HasParent' _ , _) , yes (new , rem , q , refl))
155-
rewrite dec-yes ¿ ∀[ e ∈ range new ] epoch < e × dom new ∩ rem ≡ᵉ ∅ ¿ allOk .proj₂ = refl
162+
completeness s' (GOV-Propose (wf , av , dep , vHFA , en , goodAddr)) with H
163+
... | (no ¬p , _) = ⊥-elim (¬p (wf , av , dep , vHFA , L.HasParent' en , goodAddr))
164+
... | (yes (_ , _ , _ , _ , L.HasParent' _ , _) , no notNewComm) = refl
165+
... | (yes (_ , (_ , (av₁ , av₂)) , _ , _ , L.HasParent' _ , _) , yes (new , rem , q , refl))
166+
rewrite dec-yes ¿ ∀[ e ∈ range new ] epoch < e × dom new ∩ rem ≡ᵉ ∅ ¿ (λ { x → av₁ x , av₂ }) .proj₂ = refl
156167

157168
computeProof : (sig : GovVote ⊎ GovProposal) → _
158169
computeProof (inj₁ s) = GoVote.computeProof s

‎src/Ledger/Gov.lagda‎

Lines changed: 37 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -320,29 +320,39 @@ action is \NoConfidence and the other is an \UpdateCommittee action.
320320

321321
\begin{figure*}
322322
\begin{code}[hide]
323-
actionWellFormed : ℙ Credential → Maybe ScriptHash → Maybe ScriptHash → Epoch → GovAction → Type
324-
actionWellFormed _ p ppolicy _ (ChangePParams x) =
325-
∙ ppdWellFormed x
326-
∙ p ≡ ppolicy
327-
actionWellFormed rewardCreds p ppolicy _ (TreasuryWdrl x) =
328-
∙ ∀[ a ∈ dom x ] RwdAddr.net a ≡ NetworkId
329-
∙ ∃[ v ∈ range x ] ¬ (v ≡ 0)
330-
∙ p ≡ ppolicy
331-
∙ mapˢ RwdAddr.stake (dom x) ⊆ rewardCreds
332-
actionWellFormed _ p _ epoch (UpdateCommittee new rem q) =
333-
∙ p ≡ nothing
334-
∙ ∀[ e ∈ range new ] epoch < e × dom new ∩ rem ≡ᵉ ∅
335-
actionWellFormed _ p _ _ _ =
336-
∙ p ≡ nothing
337-
338-
actionWellFormed? : ∀ {Γ a p ppolicy epoch} → actionWellFormed Γ p ppolicy epoch a ⁇
339-
actionWellFormed? {_} {NoConfidence} = it
340-
actionWellFormed? {_} {UpdateCommittee _ _ _} = it
341-
actionWellFormed? {_} {NewConstitution _ _} = it
342-
actionWellFormed? {_} {TriggerHF _} = it
343-
actionWellFormed? {_} {ChangePParams _} = it
344-
actionWellFormed? {_} {TreasuryWdrl _} = it
345-
actionWellFormed? {_} {Info} = it
323+
actionValid : ℙ Credential → Maybe ScriptHash → Maybe ScriptHash → Epoch → GovAction → Type
324+
actionValid rewardCreds p ppolicy epoch (ChangePParams x) =
325+
p ≡ ppolicy
326+
actionValid rewardCreds p ppolicy epoch (TreasuryWdrl x) =
327+
p ≡ ppolicy × mapˢ RwdAddr.stake (dom x) ⊆ rewardCreds
328+
actionValid rewardCreds p ppolicy epoch (UpdateCommittee new rem q) =
329+
p ≡ nothing × (∀[ e ∈ range new ] epoch < e) × (dom new ∩ rem ≡ᵉ ∅)
330+
actionValid rewardCreds p ppolicy epoch _ =
331+
p ≡ nothing
332+
333+
actionValid? : ∀ {rewardCreds p ppolicy epoch a} → actionValid rewardCreds p ppolicy epoch a ⁇
334+
actionValid? {a = NoConfidence} = it
335+
actionValid? {a = UpdateCommittee _ _ _} = it
336+
actionValid? {a = NewConstitution _ _} = it
337+
actionValid? {a = TriggerHF _} = it
338+
actionValid? {a = ChangePParams _} = it
339+
actionValid? {a = TreasuryWdrl _} = it
340+
actionValid? {a = Info} = it
341+
342+
actionWellFormed : GovAction → Type
343+
actionWellFormed (ChangePParams x) = ppdWellFormed x
344+
actionWellFormed (TreasuryWdrl x) =
345+
(∀[ a ∈ dom x ] RwdAddr.net a ≡ NetworkId) × (∃[ v ∈ range x ] ¬ (v ≡ 0))
346+
actionWellFormed _ = ⊤
347+
348+
actionWellFormed? : ∀ {a} → actionWellFormed a ⁇
349+
actionWellFormed? {NoConfidence} = it
350+
actionWellFormed? {UpdateCommittee _ _ _} = it
351+
actionWellFormed? {NewConstitution _ _} = it
352+
actionWellFormed? {TriggerHF _} = it
353+
actionWellFormed? {ChangePParams _} = it
354+
actionWellFormed? {TreasuryWdrl _} = it
355+
actionWellFormed? {Info} = it
346356

347357
data _⊢_⇀⦇_,GOV'⦈_ where
348358
\end{code}
@@ -354,6 +364,7 @@ data _⊢_⇀⦇_,GOV'⦈_ where
354364
∙ (aid , ast) ∈ fromList s
355365
∙ canVote pparams (action ast) (proj₁ voter)
356366
∙ isRegistered Γ voter
367+
∙ ¬ (expired epoch ast)
357368
───────────────────────────────────────
358369
(Γ , k) ⊢ s ⇀⦇ inj₁ vote ,GOV'⦈ addVote s aid voter v
359370

@@ -363,11 +374,13 @@ data _⊢_⇀⦇_,GOV'⦈_ where
363374
; policy = p ; deposit = d ; prevAction = prev }
364375
s' = addAction s (govActionLifetime +ᵉ epoch) (txid , k) addr a prev
365376
in
366-
∙ actionWellFormed rewardCreds p ppolicy epoch a
377+
∙ actionWellFormed a
378+
∙ actionValid rewardCreds p ppolicy epoch a
367379
∙ d ≡ govActionDeposit
368380
∙ validHFAction prop s enactState
369381
∙ hasParent enactState s a prev
370382
∙ addr .RwdAddr.net ≡ NetworkId
383+
∙ addr .RwdAddr.stake ∈ rewardCreds
371384
───────────────────────────────────────
372385
(Γ , k) ⊢ s ⇀⦇ inj₂ prop ,GOV'⦈ s'
373386

‎src/Ledger/Gov/Properties.agda‎

Lines changed: 29 additions & 23 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
@@ -132,30 +134,34 @@ instance
132134

133135
instance
134136
Dec-actionWellFormed = actionWellFormed?
137+
Dec-actionValid = actionValid?
135138
{-# INCOHERENT Dec-actionWellFormed #-}
139+
{-# INCOHERENT Dec-actionValid #-}
136140

137-
H = ¿ actionWellFormed rewardCreds p ppolicy epoch a
141+
H = ¿ actionWellFormed a
142+
× actionValid rewardCreds p ppolicy epoch a
138143
× d ≡ govActionDeposit
139144
× validHFAction prop s enactState
140145
× hasParent' enactState s a prev
141-
× addr .RwdAddr.net ≡ NetworkId ¿
146+
× addr .RwdAddr.net ≡ NetworkId
147+
× addr .RwdAddr.stake ∈ rewardCreds ¿
142148
,′ isUpdateCommittee a
143149

144150
computeProof = case H of λ where
145-
(yes (wf , dep , vHFA , HasParent' en , goodAddr) , yes (new , rem , q , refl)) →
151+
(yes (wf , av , dep , vHFA , HasParent' en , goodAddr , regReturn) , yes (new , rem , q , refl)) →
146152
case ¿ ∀[ e ∈ range new ] epoch < e × dom new ∩ rem ≡ᵉ ∅ ¿ of λ where
147-
(yes newOk) → success (_ , GOV-Propose (wf , dep , vHFA , en , goodAddr))
153+
(yes newOk) → success (_ , GOV-Propose (wf , av , dep , vHFA , en , goodAddr , regReturn))
148154
(no ¬p) → failure (genErrors ¬p)
149-
(yes (wf , dep , vHFA , HasParent' en , goodAddr) , no notNewComm) → success
150-
(-, GOV-Propose (wf , dep , vHFA , en , goodAddr))
155+
(yes (wf , av , dep , vHFA , HasParent' en , goodAddr , returnReg) , no notNewComm) → success
156+
(-, GOV-Propose (wf , av , dep , vHFA , en , goodAddr , returnReg))
151157
(no ¬p , _) → failure (genErrors ¬p)
152158

153159
completeness : ∀ s' → Γ ⊢ s ⇀⦇ inj₂ prop ,GOV'⦈ s' → map proj₁ computeProof ≡ success s'
154-
completeness s' (GOV-Propose (wf , dep , vHFA , en , goodAddr)) with H
155-
... | (no ¬p , _) = ⊥-elim (¬p (wf , dep , vHFA , HasParent' en , goodAddr))
156-
... | (yes (_ , _ , _ , HasParent' _ , _) , no notNewComm) = refl
157-
... | (yes ((_ , allOk) , _ , _ , HasParent' _ , _) , yes (new , rem , q , refl))
158-
rewrite dec-yes ¿ ∀[ e ∈ range new ] epoch < e × dom new ∩ rem ≡ᵉ ∅ ¿ allOk .proj₂ = refl
160+
completeness s' (GOV-Propose (wf , av , dep , vHFA , en , goodAddr)) with H
161+
... | (no ¬p , _) = ⊥-elim (¬p (wf , av , dep , vHFA , HasParent' en , goodAddr))
162+
... | (yes (_ , _ , _ , _ , HasParent' _ , _) , no notNewComm) = refl
163+
... | (yes (_ , (_ , (av₁ , av₂)) , _ , _ , HasParent' _ , _) , yes (new , rem , q , refl))
164+
rewrite dec-yes ¿ ∀[ e ∈ range new ] epoch < e × dom new ∩ rem ≡ᵉ ∅ ¿ (λ { x → av₁ x , av₂ }) .proj₂ = refl
159165

160166
computeProof : (sig : GovVote ⊎ GovProposal) → _
161167
computeProof (inj₁ s) = GoVote.computeProof s

0 commit comments

Comments
 (0)