Moved action specific predicates to actionWellFormed and fix a conformance failure

src/Ledger/Conway/Conformance/Equivalence.agda

@@ -396,8 +396,8 @@ opaque
           → (record Γ { certState = certState' } , n)
             ⊢ s ⇀⦇ txgov ,GOVn⦈ s'
   castGOV deps (BS-base Id-nop) = BS-base Id-nop
-  castGOV {Γ} deps (BS-ind (C.GOV-Vote {voter = voter} (a , b , c)) rs) =
-    BS-ind (C.GOV-Vote (a , b , cast-isRegistered Γ deps voter c))
+  castGOV {Γ} deps (BS-ind (C.GOV-Vote {voter = voter} (a , b , c , d)) rs) =
+    BS-ind (C.GOV-Vote (a , b , cast-isRegistered Γ deps voter c , d))
            (castGOV deps rs)
   castGOV deps (BS-ind (C.GOV-Propose h) rs) =
     BS-ind (C.GOV-Propose h)

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

@@ -16,12 +16,12 @@ open import Ledger.Conway.Conformance.Equivalence.Certs txs abs
 
 instance
   GovEnvToConf : L.Deposits × L.Deposits ⊢ L.GovEnv ⭆ C.GovEnv
-  GovEnvToConf .convⁱ deposits L.⟦ txid , epoch , pp , policy , enactState , certState ⟧ᵍ =
-    C.⟦ txid , epoch , pp , policy , enactState , deposits ⊢conv certState ⟧ᵍ
+  GovEnvToConf .convⁱ deposits L.⟦ txid , epoch , pp , policy , enactState , certState , stakeDelegs ⟧ᵍ =
+    C.⟦ txid , epoch , pp , policy , enactState , deposits ⊢conv certState , stakeDelegs ⟧ᵍ
 
   GovEnvFromConf : C.GovEnv ⭆ L.GovEnv
-  GovEnvFromConf .convⁱ _ C.⟦ txid , epoch , pp , policy , enactState , certState ⟧ᵍ =
-    L.⟦ txid , epoch , pp , policy , enactState , conv certState ⟧ᵍ
+  GovEnvFromConf .convⁱ _ C.⟦ txid , epoch , pp , policy , enactState , certState , stakeDelegs ⟧ᵍ =
+    L.⟦ txid , epoch , pp , policy , enactState , conv certState , stakeDelegs ⟧ᵍ
 
   opaque
     unfolding L.isRegistered C.isRegistered
@@ -41,7 +41,7 @@ instance
             → L.Deposits × L.Deposits
               ⊢ (Γ , n) L.⊢ s ⇀⦇ votes ,GOV'⦈ s' ⭆ⁱ λ deposits _ →
                 (deposits ⊢conv Γ , n) C.⊢ s ⇀⦇ votes ,GOV'⦈ s'
-  GOV'ToConf .convⁱ deposits (L.GOV-Vote (a , b , c)) = C.GOV-Vote (a , b , deposits ⊢conv c)
+  GOV'ToConf .convⁱ deposits (L.GOV-Vote (a , b , c , d)) = C.GOV-Vote (a , b , deposits ⊢conv c , d)
   GOV'ToConf .convⁱ deposits (L.GOV-Propose h) = C.GOV-Propose h
 
   GOVToConf : ∀ {Γ s votes s' n}
@@ -53,7 +53,7 @@ instance
 
   GOV'FromConf : ∀ {Γ s votes s' n}
             → (Γ , n) C.⊢ s ⇀⦇ votes ,GOV'⦈ s' ⭆ (conv Γ , n) L.⊢ s ⇀⦇ votes ,GOV'⦈ s'
-  GOV'FromConf .convⁱ _ (C.GOV-Vote (a , b , c)) = L.GOV-Vote (a , b , conv c)
+  GOV'FromConf .convⁱ _ (C.GOV-Vote (a , b , c , d)) = L.GOV-Vote (a , b , conv c , d)
   GOV'FromConf .convⁱ _ (C.GOV-Propose h)        = L.GOV-Propose h
 
   GOVFromConf : ∀ {Γ s votes s' n}

src/Ledger/Conway/Conformance/Gov.agda

@@ -33,7 +33,7 @@ GovState : Type
 GovState = List (GovActionID × GovActionState)
 
 record GovEnv : Type where
-  constructor ⟦_,_,_,_,_,_⟧ᵍ
+  constructor ⟦_,_,_,_,_,_,_⟧ᵍ
   field
 
     txid        : TxId
@@ -42,6 +42,7 @@ record GovEnv : Type where
     ppolicy     : Maybe ScriptHash
     enactState  : EnactState
     certState   : CertState
+    rewardCreds : ℙ Credential
 
 private variable
   Γ : GovEnv
@@ -62,7 +63,7 @@ open PState
 
 opaque
   isRegistered : GovEnv → Voter → Type
-  isRegistered ⟦ _ , _ , _ , _ , _ , ⟦ _ , pState , gState ⟧ᶜˢ ⟧ᵍ (r , c) = case r of λ where
+  isRegistered ⟦ _ , _ , _ , _ , _ , ⟦ _ , pState , gState ⟧ᶜˢ , _ ⟧ᵍ (r , c) = case r of λ where
     CC    → just c ∈ range (gState .ccHotKeys)
     DRep  → c ∈ dom (gState .dreps)
     SPO   → c ∈ mapˢ KeyHashObj (dom (pState .pools))
@@ -76,6 +77,7 @@ data _⊢_⇀⦇_,GOV'⦈_  : GovEnv × ℕ → GovState → GovVote ⊎ GovProp
     ∙ (aid , ast) ∈ fromList s
     ∙ canVote pparams (action ast) (proj₁ voter)
     ∙ isRegistered Γ voter
+    ∙ ¬ (expired epoch ast)
       ───────────────────────────────────────
       (Γ , k) ⊢ s ⇀⦇ inj₁ vote ,GOV'⦈ L.addVote s aid voter v
 
@@ -85,15 +87,13 @@ data _⊢_⇀⦇_,GOV'⦈_  : GovEnv × ℕ → GovState → GovVote ⊎ GovProp
                     ; policy = p ; deposit = d ; prevAction = prev }
       s' = L.addAction s (govActionLifetime +ᵉ epoch) (txid , k) addr a prev
     in
-    ∙ actionWellFormed a
+    ∙ L.actionWellFormed a
+    ∙ L.actionValid rewardCreds p ppolicy epoch a
     ∙ d ≡ govActionDeposit
-    ∙ (∃[ u ] a ≡ ChangePParams u ⊎ ∃[ w ] a ≡ TreasuryWdrl w → p ≡ ppolicy)
-    ∙ (¬ (∃[ u ] a ≡ ChangePParams u ⊎ ∃[ w ] a ≡ TreasuryWdrl w) → p ≡ nothing)
-    ∙ (∀ {new rem q} → a ≡ UpdateCommittee new rem q
-       → ∀[ e ∈ range new ]  epoch < e  ×  dom new ∩ rem ≡ᵉ ∅)
     ∙ L.validHFAction prop s enactState
     ∙ L.hasParent enactState s a prev
     ∙ addr .RwdAddr.net ≡ NetworkId
+    ∙ addr .RwdAddr.stake ∈ rewardCreds
       ───────────────────────────────────────
       (Γ , k) ⊢ s ⇀⦇ inj₂ prop ,GOV'⦈ s'
 

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

@@ -36,10 +36,6 @@ open GovActionState
 open Inverse
 
 private
-  lookupActionId : (pparams : PParams) (role : GovRole) (aid : GovActionID) (s : GovState) →
-                   Dec (Any (λ (aid' , ast) → aid ≡ aid' × canVote pparams (action ast) role) s)
-  lookupActionId pparams role aid = any? λ _ → ¿ _ ¿
-
   isUpdateCommittee : (a : GovAction) → Dec (∃[ new ] ∃[ rem ] ∃[ q ] a ≡ UpdateCommittee new rem q)
   isUpdateCommittee NoConfidence                = no λ()
   isUpdateCommittee (UpdateCommittee new rem q) = yes (new , rem , q , refl)
@@ -97,16 +93,16 @@ instance
       module GoVote sig where
         open GovVote sig
 
-        computeProof = case lookupActionId pparams (proj₁ voter) gid s ,′ isRegistered? (proj₁ Γ) voter of λ where
+        computeProof = case L.lookupActionId pparams (proj₁ voter) gid epoch s ,′ isRegistered? (proj₁ Γ) voter of λ where
             (yes p , yes p') → case Any↔ .from p of λ where
-              (_ , mem , refl , cV) → success (_ , GOV-Vote (∈-fromList .to mem , cV , p'))
+              (_ , mem , refl , cV , ¬exp) → success (_ , GOV-Vote (∈-fromList .to mem , cV , p' , ¬exp))
             (yes _ , no ¬p) → failure (genErrors ¬p)
             (no ¬p , _)     → failure (genErrors ¬p)
 
         completeness : ∀ s' → Γ ⊢ s ⇀⦇ inj₁ sig ,GOV'⦈ s' → map proj₁ computeProof ≡ success s'
-        completeness s' (GOV-Vote (mem , cV , reg))
-          with lookupActionId pparams (proj₁ voter) gid s | isRegistered? (proj₁ Γ) voter
-        ... | no ¬p | _ = ⊥-elim (¬p (Any↔ .to (_ , ∈-fromList .from mem , refl , cV)))
+        completeness s' (GOV-Vote (mem , cV , reg , ¬exp))
+          with L.lookupActionId pparams (proj₁ voter) gid epoch s | isRegistered? (proj₁ Γ) voter
+        ... | no ¬p | _ = ⊥-elim (¬p (Any↔ .to (_ , ∈-fromList .from mem , refl , cV , ¬exp)))
         ... | yes _ | no ¬p = ⊥-elim $ ¬p reg
         ... | yes p | yes p' with Any↔ .from p
         ... | (_ , mem , refl , cV) = refl
@@ -117,33 +113,57 @@ instance
         open PParams pparams hiding (a)
 
         instance 
-          Dec-actionWellFormed = actionWellFormed?
+          Dec-actionWellFormed = L.actionWellFormed?
+          Dec-actionValid = L.actionValid?
         {-# INCOHERENT Dec-actionWellFormed #-}
+        {-# INCOHERENT Dec-actionValid #-}
 
-        H = ¿ actionWellFormed a
+        H = ¿ L.actionWellFormed a
+            × L.actionValid rewardCreds p ppolicy epoch a
             × d ≡ govActionDeposit
             × L.validHFAction prop s enactState
-            × (∃[ u ] a ≡ ChangePParams u ⊎ ∃[ w ] a ≡ TreasuryWdrl w → p ≡ ppolicy)
-            × (¬ (∃[ u ] a ≡ ChangePParams u ⊎ ∃[ w ] a ≡ TreasuryWdrl w) → p ≡ nothing)
             × L.hasParent' enactState s a prev
-            × addr .RwdAddr.net ≡ NetworkId ¿
+            × addr .RwdAddr.net ≡ NetworkId
+            × addr .RwdAddr.stake ∈ rewardCreds ¿
             ,′ isUpdateCommittee a
 
+        genErrorsActionWellFormed : ∀ {a} → ¬ (L.actionWellFormed a) → String
+        genErrorsActionWellFormed {NoConfidence} ¬p          = genErrors ¬p
+        genErrorsActionWellFormed {UpdateCommittee _ _ _} ¬p = genErrors ¬p
+        genErrorsActionWellFormed {NewConstitution _ _} ¬p   = genErrors ¬p
+        genErrorsActionWellFormed {TriggerHF _} ¬p           = genErrors ¬p
+        genErrorsActionWellFormed {ChangePParams _} ¬p       = genErrors ¬p
+        genErrorsActionWellFormed {TreasuryWdrl _} ¬p        = genErrors ¬p
+        genErrorsActionWellFormed {Info} ¬p                  = genErrors ¬p
+
+        genErrorsActionValid : ∀ {a} → ¬ (L.actionValid rewardCreds p ppolicy epoch a) → String
+        genErrorsActionValid {NoConfidence} ¬p          = genErrors ¬p
+        genErrorsActionValid {UpdateCommittee _ _ _} ¬p = genErrors ¬p
+        genErrorsActionValid {NewConstitution _ _} ¬p   = genErrors ¬p
+        genErrorsActionValid {TriggerHF _} ¬p           = genErrors ¬p
+        genErrorsActionValid {ChangePParams _} ¬p       = genErrors ¬p
+        genErrorsActionValid {TreasuryWdrl _} ¬p        = genErrors ¬p
+        genErrorsActionValid {Info} ¬p                  = genErrors ¬p
+
         computeProof = case H of λ where
-          (yes (wf , dep , vHFA , pol , ¬pol , L.HasParent' en , goodAddr) , yes (new , rem , q , refl)) →
+          (yes (wf , av , dep , vHFA , L.HasParent' en , goodAddr , regReward) , yes (new , rem , q , refl)) →
             case ¿ ∀[ e ∈ range new ] epoch < e × dom new ∩ rem ≡ᵉ ∅ ¿ of λ where
-              (yes newOk) → success (_ , GOV-Propose (wf , dep , pol , ¬pol , (λ where refl → newOk) , vHFA , en , goodAddr))
+              (yes newOk) → success (_ , GOV-Propose (wf , av , dep , vHFA , en , goodAddr , regReward))
               (no ¬p)     → failure (genErrors ¬p)
-          (yes (wf , dep , vHFA , pol , ¬pol , L.HasParent' en , goodAddr) , no notNewComm) → success
-            (-, GOV-Propose (wf , dep , pol , ¬pol , (λ isNewComm → ⊥-elim (notNewComm (-, -, -, isNewComm))) , vHFA , en , goodAddr))
-          (no ¬p , _) → failure (genErrors ¬p)
+          (yes (wf , av , dep , vHFA , L.HasParent' en , goodAddr) , no notNewComm) → success
+            (-, GOV-Propose (wf , av , dep , vHFA , en , goodAddr))
+          (no ¬p , _) → case dec-de-morgan ¬p of λ where
+            (inj₁ q) → failure (genErrorsActionWellFormed q)
+            (inj₂ q) → case dec-de-morgan q of λ where
+              (inj₁ r) → failure (genErrorsActionValid r)
+              (inj₂ r) → failure (genErrors r)
 
         completeness : ∀ s' → Γ ⊢ s ⇀⦇ inj₂ prop ,GOV'⦈ s' → map proj₁ computeProof ≡ success s'
-        completeness s' (GOV-Propose (wf , dep , pol , ¬pol , newOk , vHFA , en , goodAddr)) with H
-        ... | (no ¬p , _) = ⊥-elim (¬p (wf , dep , vHFA , pol , ¬pol , L.HasParent' en , goodAddr))
-        ... | (yes (_ , _ , _ , _ , _ , L.HasParent' _ , _) , no notNewComm) = refl
-        ... | (yes (_ , _ , _ , _ , _ , L.HasParent' _ , _) , yes (new , rem , q , refl))
-          rewrite dec-yes ¿ ∀[ e ∈ range new ] epoch < e × dom new ∩ rem ≡ᵉ ∅ ¿ (newOk refl) .proj₂ = refl
+        completeness s' (GOV-Propose (wf , av , dep , vHFA , en , goodAddr)) with H
+        ... | (no ¬p , _) = ⊥-elim (¬p (wf , av , dep , vHFA , L.HasParent' en , goodAddr))
+        ... | (yes (_ , _ , _ , _ , L.HasParent' _ , _) , no notNewComm) = refl
+        ... | (yes (_ , (_ , (av₁ , av₂)) , _ , _ , L.HasParent' _ , _) , yes (new , rem , q , refl))
+          rewrite dec-yes ¿ ∀[ e ∈ range new ] epoch < e × dom new ∩ rem ≡ᵉ ∅ ¿ (λ { x → av₁ x , av₂ }) .proj₂ = refl
 
       computeProof : (sig : GovVote ⊎ GovProposal) → _
       computeProof (inj₁ s) = GoVote.computeProof s

src/Ledger/Conway/Conformance/Ledger.agda

@@ -58,8 +58,6 @@ private variable
   tx : Tx
 
 open RwdAddr
-open DState
-open CertState
 open UTxOState
 
 data
@@ -70,12 +68,13 @@ data
 
   LEDGER-V :
     let open LState s; txb = tx .body; open TxBody txb; open LEnv Γ
+        open CertState certState; open DState dState
         utxoSt'' = record utxoSt' { deposits = L.updateDeposits pparams txb (deposits utxoSt') }
      in
     ∙  isValid tx ≡ true
     ∙  record { LEnv Γ } ⊢ utxoSt ⇀⦇ tx ,UTXOW⦈ utxoSt'
     ∙  ⟦ epoch slot , pparams , txvote , txwdrls , allColdCreds govSt enactState ⟧ᶜ ⊢ certState ⇀⦇ txcerts ,CERTS⦈ certState'
-    ∙  ⟦ txid , epoch slot , pparams , ppolicy , enactState , certState' ⟧ᵍ ⊢ govSt |ᵒ certState' ⇀⦇ txgov txb ,GOV⦈ govSt'
+    ∙  ⟦ txid , epoch slot , pparams , ppolicy , enactState , certState' , dom rewards ⟧ᵍ ⊢ govSt |ᵒ certState' ⇀⦇ txgov txb ,GOV⦈ govSt'
        ────────────────────────────────
        Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ ⟦ utxoSt'' , govSt' , certState' ⟧ˡ
 

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

@@ -65,7 +65,7 @@ instance
       utxoΓ = UTxOEnv ∋ record { LEnv Γ }
       certΓ = CertEnv ∋ ⟦ epoch slot , pparams , txvote , txwdrls , _ ⟧ᶜ
       govΓ : CertState → GovEnv
-      govΓ = ⟦ txid , epoch slot , pparams , ppolicy , enactState ,_⟧ᵍ
+      govΓ certState = ⟦ txid , epoch slot , pparams , ppolicy , enactState , certState , _ ⟧ᵍ
 
       computeProof : ComputationResult String (∃[ s' ] Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ s')
       computeProof = case isValid ≟ true of λ where