Reuse ledger code in conformance (#618)

* Reuse updateCertDeposits from Ledger in Conformance * Reuse as much as possible from Ledger in Conformance.Gov --------- Co-authored-by: William DeMeo <[email protected]>
IntersectMBO · Dec 4, 2024 · b184f97 · b184f97
1 parent c59a4e3
commit b184f97
Show file tree

Hide file tree

Showing 5 changed files with 26 additions and 268 deletions.
diff --git a/src/Ledger/Conway/Conformance/Gov.agda b/src/Ledger/Conway/Conformance/Gov.agda
@@ -13,6 +13,7 @@ open import Ledger.GovernanceActions govStructure using (Vote)
 open import Ledger.Enact govStructure
 open import Ledger.Ratify txs hiding (vote)
 open import Ledger.Conway.Conformance.Certs govStructure
+import Ledger.Gov txs as L
 
 open import Data.List.Ext using (subpermutations; sublists)
 open import Data.List.Ext.Properties2
@@ -59,186 +60,14 @@ private variable
 open GState
 open PState
 
-govActionPriority : GovAction → ℕ
-govActionPriority NoConfidence             = 0
-govActionPriority (UpdateCommittee _ _ _)  = 1
-govActionPriority (NewConstitution _ _)    = 2
-govActionPriority (TriggerHF _)            = 3
-govActionPriority (ChangePParams _)        = 4
-govActionPriority (TreasuryWdrl _)         = 5
-govActionPriority Info                     = 6
-
-_∼_ : ℕ → ℕ → Type
-n ∼ m = (n ≡ m) ⊎ (n ≡ 0 × m ≡ 1) ⊎ (n ≡ 1 × m ≡ 0)
-
-_≈ᵍ_ : GovAction → GovAction → Type
-a ≈ᵍ a' = (govActionPriority a) ∼ (govActionPriority a')
-
-_∼?_ : (n m : ℕ) → Dec (n ∼ m)
-n ∼? m = n ≟ m ⊎-dec (n ≟ 0 ×-dec m ≟ 1) ⊎-dec (n ≟ 1 ×-dec m ≟ 0)
-
-_≈?_ : (a a' : GovAction) → Dec (a ≈ᵍ a')
-a ≈? a' = (govActionPriority a) ∼? (govActionPriority a')
-
-
-insertGovAction : GovState → GovActionID × GovActionState → GovState
-insertGovAction [] gaPr = [ gaPr ]
-insertGovAction ((gaID₀ , gaSt₀) ∷ gaPrs) (gaID₁ , gaSt₁)
-  =  if (govActionPriority (action gaSt₀)) ≤? (govActionPriority (action gaSt₁))
-     then (gaID₀ , gaSt₀) ∷ insertGovAction gaPrs (gaID₁ , gaSt₁)
-     else (gaID₁ , gaSt₁) ∷ (gaID₀ , gaSt₀) ∷ gaPrs
-
-mkGovStatePair : Epoch → GovActionID → RwdAddr → (a : GovAction) → NeedsHash a
-                 → GovActionID × GovActionState
-mkGovStatePair e aid addr a prev = (aid , record
-  { votes = ∅ ; returnAddr = addr ; expiresIn = e ; action = a ; prevAction = prev })
-
-addAction : GovState
-          → Epoch → GovActionID → RwdAddr → (a : GovAction) → NeedsHash a
-          → GovState
-addAction s e aid addr a prev = insertGovAction s (mkGovStatePair e aid addr a prev)
-
 opaque
-  addVote : GovState → GovActionID → Voter → Vote → GovState
-  addVote s aid voter v = map modifyVotes s
-    where modifyVotes : GovActionID × GovActionState → GovActionID × GovActionState
-          modifyVotes = λ (gid , s') → gid , record s'
-            { votes = if gid ≡ aid then insert (votes s') voter v else votes s'}
-
   isRegistered : GovEnv → Voter → Type
   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))
 
-  validHFAction : GovProposal → GovState → EnactState → Type
-  validHFAction (record { action = TriggerHF v ; prevAction = prev }) s e =
-    (let (v' , aid) = EnactState.pv e in aid ≡ prev × pvCanFollow v' v)
-    ⊎ ∃₂[ x , v' ] (prev , x) ∈ fromList s × x .action ≡ TriggerHF v' × pvCanFollow v' v
-  validHFAction _ _ _ = ⊤
-
-data
-  _⊢_⇀⦇_,GOV'⦈_  : GovEnv × ℕ → GovState → GovVote ⊎ GovProposal → GovState → Type
-
-_⊢_⇀⦇_,GOV⦈_   : GovEnv → GovState → List (GovVote ⊎ GovProposal) → GovState → Type
-
--- Convert list of (GovActionID,GovActionState)-pairs to list of GovActionID pairs.
-getAidPairsList : GovState → List (GovActionID × GovActionID)
-getAidPairsList aid×states =
-  mapMaybe (λ (aid , aState) → (aid ,_) <$> getHash (prevAction aState)) $ aid×states
-
--- A list of GovActionID pairs connects the first GovActionID to the second.
-_connects_to_ : List (GovActionID × GovActionID) → GovActionID → GovActionID → Type
-[] connects aidNew to aidOld = aidNew ≡ aidOld
-((aid , aidPrev) ∷ s) connects aidNew to aidOld  =
-  aid ≡ aidNew × s connects aidPrev to aidOld ⊎ s connects aidNew to aidOld
-
-enactable  : EnactState → List (GovActionID × GovActionID)
-           → GovActionID × GovActionState → Type
-enactable e aidPairs = λ (aidNew , as) → case getHashES e (action as) of
-
-  λ where
-
-   nothing        → ⊤
-   (just aidOld)  → ∃[ t ]  fromList t ⊆ fromList aidPairs
-                            × Unique t × t connects aidNew to aidOld
-
-allEnactable : EnactState → GovState → Type
-allEnactable e aid×states = All (enactable e (getAidPairsList aid×states)) aid×states
-
-hasParentE : EnactState → GovActionID → GovAction → Type
-hasParentE e aid a = case getHashES e a of
-
-  λ where
-
-   nothing    → ⊤
-   (just id)  → id ≡ aid
-
-hasParent : EnactState → GovState → (a : GovAction) → NeedsHash a → Type
-hasParent e s a aid with getHash aid
-... | just aid' = hasParentE e aid' a
-                  ⊎ Any (λ (gid , gas) → gid ≡ aid' × action gas ≈ᵍ a) s
-... | nothing = ⊤
-
-open Equivalence
-
-hasParentE? : ∀ e aid a → Dec (hasParentE e aid a)
-hasParentE? e aid a with getHashES e a
-... | nothing   = yes _
-... | (just id) = id ≟ aid
-
-hasParent? : ∀ e s a aid → Dec (hasParent e s a aid)
-hasParent? e s a aid with getHash aid
-... | just aid' = hasParentE? e aid' a
-                  ⊎-dec any? (λ (gid , gas) → gid ≟ aid' ×-dec action gas ≈? a) s
-... | nothing = yes _
-
--- newtype to make the instance resolution work
-data hasParent' : EnactState → GovState → (a : GovAction) → NeedsHash a → Type where
-  HasParent' : ∀ {x y z w} → hasParent x y z w → hasParent' x y z w
-
-instance
-  hasParent?' : ∀ {x y z w} → hasParent' x y z w ⁇
-  hasParent?' = ⁇ map′ HasParent' (λ where (HasParent' x) → x) (hasParent? _ _ _ _)
-
-[_connects_to_?] : ∀ l aidNew aidOld → Dec (l connects aidNew to aidOld)
-[ [] connects aidNew to aidOld ?] = aidNew ≟ aidOld
-
-[ (aid , aidPrev) ∷ s connects aidNew to aidOld ?] =
-  ((aid ≟ aidNew) ×-dec [ s connects aidPrev to aidOld ?]) ⊎-dec [ s connects aidNew to aidOld ?]
-
-any?-connecting-subperm : ∀ {u} {v} → ∀ L → Dec (Any(λ l → Unique l × l connects u to v) (subpermutations L))
-any?-connecting-subperm {u} {v} L = any? (λ l → unique? _≟_ l ×-dec [ l connects u to v ?]) (subpermutations L)
-
-∃?-connecting-subperm : ∀ {u} {v} → ∀ L → Dec (∃[ l ] l ∈ˡ subpermutations L × Unique l × l connects u to v)
-∃?-connecting-subperm L = from (map′⇔ (↔⇒ Any↔)) (any?-connecting-subperm L)
-
-∃?-connecting-subset : ∀ {u} {v} → ∀ L → Dec (∃[ l ] l ⊆ˡ L × Unique l × l connects u to v)
-∃?-connecting-subset L = from (map′⇔ ∃uniqueSubset⇔∃uniqueSubperm) (∃?-connecting-subperm L)
-
-enactable? : ∀ eState aidPairs aidNew×st → Dec (enactable eState aidPairs aidNew×st)
-enactable? eState aidPairs (aidNew , as) with getHashES eState (GovActionState.action as)
-... | nothing = yes tt
-... | just aidOld = from (map′⇔ ∃-sublist-⇔) (∃?-connecting-subset aidPairs)
-
-allEnactable? : ∀ eState aid×states → Dec (allEnactable eState aid×states)
-allEnactable? eState aid×states =
-  all? (λ aid×st → enactable? eState (getAidPairsList aid×states) aid×st) aid×states
-
--- newtype to make the instance resolution work
-data allEnactable' : EnactState → GovState → Type where
-  AllEnactable' : ∀ {x y} → allEnactable x y → allEnactable' x y
-
-instance
-  allEnactable?' : ∀ {x y} → allEnactable' x y ⁇
-  allEnactable?' = ⁇ map′ AllEnactable' (λ where (AllEnactable' x) → x) (allEnactable? _ _)
-
--- `maxAllEnactable` returns a list `ls` of sublists of the given
--- list (`aid×states : List (GovActionID × GovActionState)`) such that
---    (i) each sublist `l ∈ ls` satisfies `allEnactable e l` and
---   (ii) each sublist `l ∈ ls` is of maximal length among sublists of `aid×states` satisfying `allEnactable`.
-maxAllEnactable : EnactState → List (GovActionID × GovActionState) → List (List (GovActionID × GovActionState))
-maxAllEnactable e = maxsublists⊧P (allEnactable? e)
-
--- Every sublist returned by `maxAllEnactable` satisfies (i).
-∈-maxAllEnactable→allEnactable : ∀ {e} {aid×states} l
-  → l ∈ˡ maxAllEnactable e aid×states → allEnactable e l
-∈-maxAllEnactable→allEnactable {e} {aid×states} l l∈ =
-  proj₂ (∈-filter⁻ (allEnactable? e) {l} {sublists aid×states}
-          (proj₁ (∈-filter⁻ (λ l → length l ≟ maxlen (sublists⊧P (allEnactable? e) aid×states)) l∈)))
-
--- Every sublist returned by `maxAllEnactable` satisfies (ii).
-∈-maxAllEnactable→maxLength : ∀ {e aid×states l l'}
-                              → l ∈ˡ sublists aid×states → allEnactable e l
-                              → l' ∈ˡ maxAllEnactable e aid×states
-                              → length l ≤ length l'
-∈-maxAllEnactable→maxLength {e} {aid×states} {l} {l'} l∈ el l'∈ =
-  let ls = sublists⊧P (allEnactable? e) aid×states in
-    subst (length l ≤_)
-          (sym (proj₂ (∈-filter⁻ (λ l → length l ≟ maxlen ls) {xs = ls} l'∈)))
-          (∈-maxlen-≤ l (∈-filter⁺ (allEnactable? e) l∈ el))
-
-data _⊢_⇀⦇_,GOV'⦈_ where
+data _⊢_⇀⦇_,GOV'⦈_  : GovEnv × ℕ → GovState → GovVote ⊎ GovProposal → GovState → Type where
 
   GOV-Vote : ∀ {x ast} → let
       open GovEnv Γ
@@ -248,24 +77,25 @@ data _⊢_⇀⦇_,GOV'⦈_ where
     ∙ canVote pparams (action ast) (proj₁ voter)
     ∙ isRegistered Γ voter
       ───────────────────────────────────────
-      (Γ , k) ⊢ s ⇀⦇ inj₁ vote ,GOV'⦈ addVote s aid voter v
+      (Γ , k) ⊢ s ⇀⦇ inj₁ vote ,GOV'⦈ L.addVote s aid voter v
 
   GOV-Propose : ∀ {x} → let
       open GovEnv Γ; open PParams pparams hiding (a)
       prop = record { returnAddr = addr ; action = a ; anchor = x
                     ; policy = p ; deposit = d ; prevAction = prev }
-      s' = addAction s (govActionLifetime +ᵉ epoch) (txid , k) addr a prev
+      s' = L.addAction s (govActionLifetime +ᵉ epoch) (txid , k) addr a prev
     in
     ∙ actionWellFormed 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 ≡ᵉ ∅)
-    ∙ validHFAction prop s enactState
-    ∙ hasParent enactState s a prev
+    ∙ L.validHFAction prop s enactState
+    ∙ L.hasParent enactState s a prev
     ∙ addr .RwdAddr.net ≡ NetworkId
       ───────────────────────────────────────
       (Γ , k) ⊢ s ⇀⦇ inj₂ prop ,GOV'⦈ s'
 
+_⊢_⇀⦇_,GOV⦈_   : GovEnv → GovState → List (GovVote ⊎ GovProposal) → GovState → Type
 _⊢_⇀⦇_,GOV⦈_ = ReflexiveTransitiveClosureᵢ {sts = _⊢_⇀⦇_,GOV'⦈_}
diff --git a/src/Ledger/Conway/Conformance/Gov/Properties.agda b/src/Ledger/Conway/Conformance/Gov/Properties.agda
@@ -27,6 +27,10 @@ open import Relation.Binary using (IsEquivalence)
 open import Tactic.Defaults
 open import Tactic.GenError
 
+private module L where
+  open import Ledger.Gov txs public
+  open import Ledger.Gov.Properties txs public
+
 open Equivalence
 open GovActionState
 open Inverse
@@ -76,25 +80,7 @@ private
   hasPrev record { action = Info }                    v = no λ ()
 
 opaque
-  unfolding validHFAction isRegistered
-
-  instance
-    validHFAction? : ∀ {p s e} → validHFAction p s e ⁇
-    validHFAction? {record { action = NoConfidence }} = Dec-⊤
-    validHFAction? {record { action = UpdateCommittee _ _ _ }} = Dec-⊤
-    validHFAction? {record { action = NewConstitution _ _ }} = Dec-⊤
-    validHFAction? {record { action = TriggerHF v ; prevAction = prev }} {s} {record { pv = (v' , aid') }}
-      with aid' ≟ prev ×-dec pvCanFollow? {v'} {v} | any? (λ (aid , x) → aid ≟ prev ×-dec hasPrev x v) s
-    ... | yes p | _ = ⁇ yes (inj₁ p)
-    ... | no _ | yes p with ((aid , x) , x∈xs , (refl , v , h)) ← P.find p = ⁇ yes (inj₂
-      (x , v , to ∈-fromList x∈xs , h))
-    ... | no ¬p₁ | no ¬p₂ = ⁇ no λ
-      { (inj₁ x) → ¬p₁ x
-      ; (inj₂ (s , v , (h₁ , h₂ , h₃))) → ¬p₂ $
-        ∃∈-Any ((prev , s) , (from ∈-fromList h₁ , refl , (v , h₂ , h₃))) }
-    validHFAction? {record { action = ChangePParams _ }} = Dec-⊤
-    validHFAction? {record { action = TreasuryWdrl _ }} = Dec-⊤
-    validHFAction? {record { action = Info }} = Dec-⊤
+  unfolding isRegistered
 
   isRegistered? : ∀ Γ v → Dec (isRegistered Γ v)
   isRegistered? _ (CC   , _) = ¿ _ ∈ _ ¿
@@ -134,27 +120,27 @@ instance
 
         H = ¿ actionWellFormed a
             × d ≡ govActionDeposit
-            × validHFAction prop s enactState
+            × 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)
-            × hasParent' enactState s a prev
+            × L.hasParent' enactState s a prev
             × addr .RwdAddr.net ≡ NetworkId ¿
             ,′ isUpdateCommittee a
 
         computeProof = case H of λ where
-          (yes (wf , dep , vHFA , pol , ¬pol , HasParent' en , goodAddr) , yes (new , rem , q , refl)) →
+          (yes (wf , dep , vHFA , pol , ¬pol , L.HasParent' en , goodAddr) , 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))
               (no ¬p)     → failure (genErrors ¬p)
-          (yes (wf , dep , vHFA , pol , ¬pol , HasParent' en , goodAddr) , no notNewComm) → success
+          (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)
 
         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 , HasParent' en , goodAddr))
-        ... | (yes (_ , _ , _ , _ , _ , HasParent' _ , _) , no notNewComm) = refl
-        ... | (yes (_ , _ , _ , _ , _ , HasParent' _ , _) , yes (new , rem , q , refl))
+        ... | (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
 
       computeProof : (sig : GovVote ⊎ GovProposal) → _
@@ -167,16 +153,3 @@ instance
 
 Computational-GOV : Computational _⊢_⇀⦇_,GOV⦈_ String
 Computational-GOV = it
-
-allEnactable-singleton : ∀ {aid s es} → getHash (s .prevAction) ≡ getHashES es (s .action)
-  → allEnactable es [ (aid , s) ]
-allEnactable-singleton {aid} {s} {es} eq = helper All.∷ All.[]
-  where
-    module ≡ᵉ = IsEquivalence (≡ᵉ-isEquivalence th)
-
-    helper : enactable es (getAidPairsList [ (aid , s) ]) (aid , s)
-    helper with getHashES es (s .action) | getHash (s .prevAction)
-    ... | just x | just x' with refl <- just-injective eq =
-      [ (aid , x) ] , proj₁ ≡ᵉ.refl , All.[] ∷ [] , inj₁ (refl , refl)
-    ... | just x | nothing = case eq of λ ()
-    ... | nothing | _ = _
diff --git a/src/Ledger/Conway/Conformance/Ledger.agda b/src/Ledger/Conway/Conformance/Ledger.agda
@@ -14,7 +14,7 @@ module Ledger.Conway.Conformance.Ledger
 
 open import Ledger.Enact govStructure
 open import Ledger.Conway.Conformance.Gov txs
-open import Ledger.Conway.Conformance.Utxo txs abs
+open import Ledger.Conway.Conformance.Utxo txs abs hiding (module L)
 open import Ledger.Conway.Conformance.Utxow txs abs
 open import Ledger.Conway.Conformance.Certs govStructure
 
@@ -70,7 +70,7 @@ data
 
   LEDGER-V :
     let open LState s; txb = tx .body; open TxBody txb; open LEnv Γ
-        utxoSt'' = record utxoSt' { deposits = updateDeposits pparams txb (deposits utxoSt') }
+        utxoSt'' = record utxoSt' { deposits = L.updateDeposits pparams txb (deposits utxoSt') }
      in
     ∙  isValid tx ≡ true
     ∙  record { LEnv Γ } ⊢ utxoSt ⇀⦇ tx ,UTXOW⦈ utxoSt'