Abstract definitions for cleaner Ratify.Properties (#247)

Co-authored-by: Orestis Melkonian <[email protected]>
IntersectMBO · Oct 17, 2023 · e65bce5 · e65bce5
1 parent 972074b
commit e65bce5
Show file tree

Hide file tree

Showing 4 changed files with 174 additions and 146 deletions.
diff --git a/src/Ledger/Chain/Properties.agda b/src/Ledger/Chain/Properties.agda
@@ -26,19 +26,19 @@ module _ {Γ : NewEpochEnv} {nes : NewEpochState} {e : Epoch} where
 
   NEWEPOCH-total : ∃[ nes' ] Γ ⊢ nes ⇀⦇ e ,NEWEPOCH⦈ nes'
   NEWEPOCH-total =
-    let (_ , pFut) = RATIFY-total
-                      {record { currentEpoch = e ; treasury = treasury
-                              ; GState gState ; NewEpochEnv Γ }} {⟦ es , ∅ , false ⟧ʳ} {govSt'} in
     case e ≟ sucᵉ lastEpoch of λ where
       (no ¬p) → -, NEWEPOCH-Not-New ¬p
-      (yes p) → -, NEWEPOCH-New p pFut
+      (yes p) → -, NEWEPOCH-New p (pFut .proj₂)
+    where pFut = RATIFY-total {record { currentEpoch = e ; treasury = treasury
+                                      ; GState gState ; NewEpochEnv Γ }}
+                              {⟦ es , ∅ , false ⟧ʳ} {govSt'}
 
   NEWEPOCH-complete : ∀ nes' → Γ ⊢ nes ⇀⦇ e ,NEWEPOCH⦈ nes' → NEWEPOCH-total .proj₁ ≡ nes'
-  NEWEPOCH-complete nes' _ with e ≟ sucᵉ lastEpoch
-  NEWEPOCH-complete nes' (NEWEPOCH-New next _)    | no ¬next = ⊥-elim (¬next next)
-  NEWEPOCH-complete nes' (NEWEPOCH-Not-New _)     | no _     = refl
-  NEWEPOCH-complete nes' (NEWEPOCH-New _ h)       | yes _    = cong ⟦ _ , _ , _ , _ ,_⟧ⁿᵉ (RATIFY-complete h)
-  NEWEPOCH-complete nes' (NEWEPOCH-Not-New ¬next) | yes next = ⊥-elim (¬next next)
+  NEWEPOCH-complete nes' h with h | e ≟ sucᵉ lastEpoch
+  ... | NEWEPOCH-New next _    | no ¬next = ⊥-elim (¬next next)
+  ... | NEWEPOCH-Not-New _     | no _     = refl
+  ... | NEWEPOCH-New _ h       | yes _    = cong ⟦ _ , _ , _ , _ ,_⟧ⁿᵉ (RATIFY-complete h)
+  ... | NEWEPOCH-Not-New ¬next | yes next = ⊥-elim (¬next next)
 
 instance
   Computational-NEWEPOCH : Computational _⊢_⇀⦇_,NEWEPOCH⦈_

diff --git a/src/Ledger/NewPP/Properties.agda b/src/Ledger/NewPP/Properties.agda
@@ -1,3 +1,4 @@
+{-# OPTIONS --safe #-}
 
 open import Relation.Nullary.Decidable
 
@@ -9,17 +10,20 @@ module Ledger.NewPP.Properties (txs : _) (open TransactionStructure txs) where
 open import Ledger.PPUp txs
 open import Ledger.NewPP txs
 
-open Computational ⦃...⦄
-
 instance
   Computational-NEWPP : Computational _⊢_⇀⦇_,NEWPP⦈_
-  Computational-NEWPP .computeProof Γ s (just upd) =
-    let open NewPParamState s; newpp = applyUpdate pparams upd in
-    case ¿ viablePParams newpp ¿ of λ where
-      (yes p) → just (_ , NEWPP-Accept p)
-      (no _)  → nothing
-  Computational-NEWPP .computeProof Γ s nothing = just (_ , NEWPP-Reject)
-  Computational-NEWPP .completeness Γ s (just upd) s' (NEWPP-Accept p)
-    rewrite (let open NewPParamState s; newpp = applyUpdate pparams upd in
-             dec-yes (¿ viablePParams newpp ¿) p .proj₂) = refl
-  Computational-NEWPP .completeness Γ s nothing s' NEWPP-Reject = refl
+  Computational-NEWPP = record {M} where module M Γ s (open NewPParamState s) where
+    computeProof = λ where
+      nothing → just (_ , NEWPP-Reject)
+      (just upd) → let newpp = applyUpdate pparams upd in
+        case ¿ viablePParams newpp ¿ of λ where
+          (yes p) → just (_ , NEWPP-Accept p)
+          (no _)  → nothing
+
+    completeness : _
+    completeness sig s' h with sig | h
+    ... | nothing  | NEWPP-Reject   = refl
+    ... | just upd | NEWPP-Accept p
+      rewrite let newpp = applyUpdate pparams upd in
+              dec-yes (¿ viablePParams newpp ¿) p .proj₂
+              = refl
diff --git a/src/Ledger/Ratify.lagda b/src/Ledger/Ratify.lagda
@@ -344,46 +344,49 @@ participatingHashes votes r = votedYesHashes votes r ∪ votedHashes Vote.no vot
 The code in Figure~\ref{fig:defs:ratify-ii} defines \votedHashes, which returns the set of delegates who voted a certain way on the given governance role.
 \begin{figure*}[h!]
 {\small
+\begin{code}[hide]
+abstract
+\end{code}
 \begin{code}
-getStakeDist : GovRole → ℙ VDeleg → StakeDistrs → VDeleg ⇀ Coin
-getStakeDist CC    cc  _                             = constMap (filterˢ isCCProp cc) 1
-getStakeDist DRep  _   record { stakeDistr = dist }  = filterᵐ (sp-∘ isDRepProp  proj₁) dist
-getStakeDist SPO   _   record { stakeDistr = dist }  = filterᵐ (sp-∘ isSPOProp   proj₁) dist
-
-acceptedStake : GovRole → ℙ VDeleg → StakeDistrs → (VDeleg ⇀ Vote) → Coin
-acceptedStake r cc dists votes =
-  Σᵐᵛ[ x ← (getStakeDist r cc dists ∣ votedYesHashes votes r) ᶠᵐ ] x
-
-totalStake : GovRole → ℙ VDeleg → StakeDistrs → (VDeleg ⇀ Vote) → Coin
-totalStake r cc dists votes =
-  Σᵐᵛ[ x  ← getStakeDist r cc dists ∣ votedAbstainHashes votes r ᶜ ᶠᵐ ] x
-
-activeVotingStake : ℙ VDeleg → StakeDistrs → (VDeleg ⇀ Vote) → Coin
-activeVotingStake cc dists votes =
-  Σᵐᵛ[ x  ← getStakeDist DRep cc dists ∣ dom votes ᶜ ᶠᵐ ] x
-
-acceptedBy : (Γ : RatifyEnv) (es : EnactState) (gs : GovActionState) → GovRole → Set
-acceptedBy Γ (record { cc = cc , _; pparams = pparams , _ }) gs role =
-  let open RatifyEnv Γ; open GovActionState gs; open PParams pparams
-      votes'         = actualVotes Γ cc votes action pparams
-      cc'            = dom votes'
-      redStakeDistr  = restrictedDists coinThreshold rankThreshold stakeDistrs
-      t              = maybe id R.0ℚ $ threshold pparams (proj₂ <$> cc) action role in
-  case totalStake role cc' redStakeDistr votes' of λ where
-    0 → t ≡ R.0ℚ -- if there's no stake, accept only if threshold is zero
-    x@(suc _) → Z.+ acceptedStake role cc' redStakeDistr votes' R./ x R.≥ t
-
-accepted : (Γ : RatifyEnv) (es : EnactState) (gs : GovActionState) → Set
-accepted Γ es gs = acceptedBy Γ es gs CC ∧ acceptedBy Γ es gs DRep ∧ acceptedBy Γ es gs SPO
-
-expired : Epoch → GovActionState → Set
-expired current record { expiresIn = expiresIn } = expiresIn < current
+  getStakeDist : GovRole → ℙ VDeleg → StakeDistrs → VDeleg ⇀ Coin
+  getStakeDist CC    cc  _                             = constMap (filterˢ isCCProp cc) 1
+  getStakeDist DRep  _   record { stakeDistr = dist }  = filterᵐ (sp-∘ isDRepProp  proj₁) dist
+  getStakeDist SPO   _   record { stakeDistr = dist }  = filterᵐ (sp-∘ isSPOProp   proj₁) dist
+
+  acceptedStake : GovRole → ℙ VDeleg → StakeDistrs → (VDeleg ⇀ Vote) → Coin
+  acceptedStake r cc dists votes =
+    Σᵐᵛ[ x ← (getStakeDist r cc dists ∣ votedYesHashes votes r) ᶠᵐ ] x
+
+  totalStake : GovRole → ℙ VDeleg → StakeDistrs → (VDeleg ⇀ Vote) → Coin
+  totalStake r cc dists votes =
+    Σᵐᵛ[ x  ← getStakeDist r cc dists ∣ votedAbstainHashes votes r ᶜ ᶠᵐ ] x
+
+  activeVotingStake : ℙ VDeleg → StakeDistrs → (VDeleg ⇀ Vote) → Coin
+  activeVotingStake cc dists votes =
+    Σᵐᵛ[ x  ← getStakeDist DRep cc dists ∣ dom votes ᶜ ᶠᵐ ] x
+
+  acceptedBy : (Γ : RatifyEnv) (es : EnactState) (gs : GovActionState) → GovRole → Set
+  acceptedBy Γ (record { cc = cc , _; pparams = pparams , _ }) gs role =
+    let open RatifyEnv Γ; open GovActionState gs; open PParams pparams
+        votes'         = actualVotes Γ cc votes action pparams
+        cc'            = dom votes'
+        redStakeDistr  = restrictedDists coinThreshold rankThreshold stakeDistrs
+        t              = maybe id R.0ℚ $ threshold pparams (proj₂ <$> cc) action role in
+    case totalStake role cc' redStakeDistr votes' of λ where
+      0 → t ≡ R.0ℚ -- if there's no stake, accept only if threshold is zero
+      x@(suc _) → Z.+ acceptedStake role cc' redStakeDistr votes' R./ x R.≥ t
+
+  accepted : (Γ : RatifyEnv) (es : EnactState) (gs : GovActionState) → Set
+  accepted Γ es gs = acceptedBy Γ es gs CC ∧ acceptedBy Γ es gs DRep ∧ acceptedBy Γ es gs SPO
+
+  expired : Epoch → GovActionState → Set
+  expired current record { expiresIn = expiresIn } = expiresIn < current
 \end{code}
 \begin{code}[hide]
-  where -- FIXME: this should be part of a typeclass
-    infix 4 _<_
-    _<_ : Epoch → Epoch → Set
-    a < b = a ≤ b × a ≢ b
+    where -- FIXME: this should be part of a typeclass
+      infix 4 _<_
+      _<_ : Epoch → Epoch → Set
+      a < b = a ≤ b × a ≢ b
 \end{code}
 } %% end small
 \caption{%%Ratify iii:
@@ -427,6 +430,38 @@ delayingAction Info                   = false
 delayed : (a : GovAction) → NeedsHash a → EnactState → Bool → Set
 delayed a h es d = ¬ verifyPrev a h es ⊎ d ≡ true
 \end{code}
+\begin{code}[hide]
+abstract
+  verifyPrev? : ∀ a h es → Dec (verifyPrev a h es)
+  verifyPrev? NoConfidence           h es = it
+  verifyPrev? (NewCommittee x x₁ x₂) h es = it
+  verifyPrev? (NewConstitution x x₁) h es = it
+  verifyPrev? (TriggerHF x)          h es = it
+  verifyPrev? (ChangePParams x)      h es = it
+  verifyPrev? (TreasuryWdrl x)       h es = it
+  verifyPrev? Info                   h es = it
+
+  delayed? : ∀ a h es d → Dec (delayed a h es d)
+  delayed? a h es d = let instance _ = verifyPrev? a h es in it
+
+  acceptedBy? : ∀ Γ es st role → Dec (acceptedBy Γ es st role)
+  acceptedBy? Γ record{ cc = cc , _ ; pparams = pparams , _ } st role
+    with (let open RatifyEnv Γ; open GovActionState st; open PParams pparams
+              votes' = actualVotes Γ cc votes action pparams
+              cc' = dom votes'
+              redStakeDistr = restrictedDists coinThreshold rankThreshold stakeDistrs
+          in totalStake role cc' redStakeDistr votes')
+  ... | zero  = it
+  ... | suc n = it
+
+  accepted? : ∀ Γ es st → Dec (accepted Γ es st)
+  accepted? Γ es st =
+    let instance _ = λ {role} → acceptedBy? Γ es st role
+    in it
+
+  expired? : ∀ e st → Dec (expired e st)
+  expired? e st = ¿ expired e st ¿
+\end{code}
 } %% end small
 \caption{%Ratify iv:
 Determination of the status of ratification of the governance action}

diff --git a/src/Ledger/Ratify/Properties.agda b/src/Ledger/Ratify/Properties.agda
@@ -8,101 +8,90 @@ module Ledger.Ratify.Properties (txs : _) (open TransactionStructure txs) where
 open import Ledger.Gov govStructure
 open import Ledger.Ratify txs
 
-open Computational ⦃...⦄
-
-caseEq_of_ : ∀ {a b} {A : Set a} {B : Set b} → (a : A) → ((a' : A) → a ≡ a' → B) → B
-caseEq a of f = f a refl
-
-verifyPrev? : ∀ a h es → Dec (verifyPrev a h es)
-verifyPrev? NoConfidence           h es = it
-verifyPrev? (NewCommittee x x₁ x₂) h es = it
-verifyPrev? (NewConstitution x x₁) h es = it
-verifyPrev? (TriggerHF x)          h es = it
-verifyPrev? (ChangePParams x)      h es = it
-verifyPrev? (TreasuryWdrl x)       h es = it
-verifyPrev? Info                   h es = it
-
-delayed? : ∀ a h es d → Dec (delayed a h es d)
-delayed? a h es d = let instance _ = verifyPrev? a h es in it
-
-acceptedBy? : ∀ Γ es st role → Dec (acceptedBy Γ es st role)
-acceptedBy? Γ record{ cc = cc , _ ; pparams = pparams , _ } st role
-  with (let open RatifyEnv Γ; open GovActionState st; open PParams pparams
-            votes' = actualVotes Γ cc votes action pparams
-            cc' = dom votes'
-            redStakeDistr = restrictedDists coinThreshold rankThreshold stakeDistrs
-        in totalStake role cc' redStakeDistr votes')
-... | zero  = it
-... | suc n = it
-
-accepted? : ∀ Γ es st → Dec (accepted Γ es st)
-accepted? Γ es st =
-  let instance _ = λ {role} → acceptedBy? Γ es st role
-  in it
-
--- We abstract over the accepted/expired/delayed checks and the enact step to make the completeness proof
--- a little cleaner, and because the normal form of `accepted` is very big, making using `with` impractical.
-module _ {Γ : RatifyEnv} {s : RatifyState} {sig : GovActionID × GovActionState}
-         (let open RatifyEnv Γ; st = proj₂ sig; open GovActionState st)
-         (let ⟦ es , removed , d ⟧ʳ = s)
+open Computational ⦃...⦄ hiding (computeProof; completeness)
+
+module _ {a b} {A : Set a} {B : Set b} where
+  caseMaybe_∣_∣_ : (ma : Maybe A) → (∀ {a} → ma ≡ just a → B) → (ma ≡ nothing → B) → B
+  caseMaybe ma ∣ f ∣ g with ma
+  ... | just _  = f refl
+  ... | nothing = g refl
+
+  caseMaybe-just : ∀ {a} {ma : Maybe A} {f : ∀ {a} → ma ≡ just a → B} {g : ma ≡ nothing → B}
+    → (eq : ma ≡ just a)
+    → caseMaybe ma ∣ f ∣ g ≡ f eq
+  caseMaybe-just refl = refl
+
+  caseMaybe-nothing : ∀ {ma : Maybe A} {f : ∀ {a} → ma ≡ just a → B} {g : ma ≡ nothing → B}
+    → (eq : ma ≡ nothing)
+    → caseMaybe ma ∣ f ∣ g ≡ g eq
+  caseMaybe-nothing refl = refl
+
+pattern RATIFY-Continue₁  x y = RATIFY-Continue (inj₁ (x , y))
+pattern RATIFY-Continue₂  x y = RATIFY-Continue (inj₂ (x , y))
+pattern RATIFY-Continue₂₁ x y = RATIFY-Continue₂ x (inj₁ y)
+pattern RATIFY-Continue₂₂ x y = RATIFY-Continue₂ x (inj₂ y)
+
+private
+  module Implementation
+    Γ (s : RatifyState) (sig : _ × _)
+    (let ⟦ es , removed , d ⟧ʳ = s)
+    (let gid , st = sig)
     where
-
-  RATIFY'-total-helper :
-    (accepted? : Dec (accepted Γ es st))
-    (expired? : Dec (expired currentEpoch st))
-    (delayed? : Dec (delayed action prevAction es d))
-    (enact : Maybe EnactState)
-    (eq : compute ⟦ sig .proj₁ , treasury , currentEpoch ⟧ᵉ es action ≡ enact) →
-    ∃[ s' ] Γ ⊢ s ⇀⦇ sig ,RATIFY'⦈ s'
-  RATIFY'-total-helper (no ¬acc) (no ¬exp) delayed? enact    eq = _ , RATIFY-Continue (inj₁ (¬acc , ¬exp))
-  RATIFY'-total-helper (no ¬acc) (yes exp) delayed? enact    eq = _ , RATIFY-Reject ¬acc exp
-  RATIFY'-total-helper (yes acc) expired? (no ¬del) (just x) eq = _ , RATIFY-Accept acc ¬del (≡-just⇔STS .Equivalence.to eq)
-  RATIFY'-total-helper (yes acc) expired? (no ¬del) nothing  eq = _ , RATIFY-Continue (inj₂ (acc , inj₂ (nothing⇒∀¬STS eq)))
-  RATIFY'-total-helper (yes acc) expired? (yes del) enact    eq = _ , RATIFY-Continue (inj₂ (acc , inj₁ del))
-
-  RATIFY'-completeness-helper :
-    (accepted? : Dec (accepted Γ es st))
-    (expired? : Dec (expired currentEpoch st))
-    (delayed? : Dec (delayed action prevAction es d))
-    (enact : Maybe EnactState)
-    (eq : compute ⟦ sig .proj₁ , treasury , currentEpoch ⟧ᵉ es action ≡ enact) →
-    ∀ s' → Γ ⊢ s ⇀⦇ sig ,RATIFY'⦈ s' → RATIFY'-total-helper accepted? expired? delayed? enact eq .proj₁ ≡ s'
-  RATIFY'-completeness-helper (no _) (no _) _ _ _ _          (RATIFY-Continue _)   = refl
-  RATIFY'-completeness-helper (no _) (yes _) _ _ _ _         (RATIFY-Reject _ _)   = refl
-  RATIFY'-completeness-helper (yes _) _ (no _) (just _) eq _ (RATIFY-Accept _ _ h) = case trans (sym eq) (completeness _ _ _ _ h) of λ where refl → refl
-  RATIFY'-completeness-helper (yes _) _ (no _) nothing _ _   (RATIFY-Continue _)   = refl
-  RATIFY'-completeness-helper (yes _) _ (yes _) _ _ _        (RATIFY-Continue _)   = refl
-
-  RATIFY'-completeness-helper (no ¬acc) _ _ _ _ _ (RATIFY-Accept acc _ _)                 = ⊥-elim (¬acc acc)
-  RATIFY'-completeness-helper _ _ (yes del) _ _ _ (RATIFY-Accept _ ¬del _)                = ⊥-elim (¬del del)
-  RATIFY'-completeness-helper _ _ _ nothing eq _  (RATIFY-Accept _ _ h)                   = ⊥-elim (nothing⇒∀¬STS eq _ h)
-  RATIFY'-completeness-helper (yes acc) _ _ _ _ _ (RATIFY-Reject ¬acc _)                  = ⊥-elim (¬acc acc)
-  RATIFY'-completeness-helper _ (no ¬exp) _ _ _ _ (RATIFY-Reject _ exp)                   = ⊥-elim (¬exp exp)
-  RATIFY'-completeness-helper (yes acc) _ _ _ _ _ (RATIFY-Continue (inj₁ (¬acc , _)))     = ⊥-elim (¬acc acc)
-  RATIFY'-completeness-helper _ (yes exp) _ _ _ _ (RATIFY-Continue (inj₁ (_ , ¬exp)))     = ⊥-elim (¬exp exp)
-  RATIFY'-completeness-helper (no ¬acc) _ _ _ _ _ (RATIFY-Continue (inj₂ (acc , _)))      = ⊥-elim (¬acc acc)
-  RATIFY'-completeness-helper _ _ (no ¬del) _ _ _ (RATIFY-Continue (inj₂ (_ , inj₁ del))) = ⊥-elim (¬del del)
-  RATIFY'-completeness-helper _ _ _ (just _) eq _ (RATIFY-Continue (inj₂ (_ , inj₂ h)))   = ⊥-elim (h _ (≡-just⇔STS .Equivalence.to eq))
-
-RATIFY'-total : ∀ {Γ s sig} → ∃[ s' ] Γ ⊢ s ⇀⦇ sig ,RATIFY'⦈ s'
-RATIFY'-total {Γ} {⟦ es , removed , d ⟧ʳ} {sig} =
-  let open RatifyEnv Γ; st = proj₂ sig; open GovActionState st
-  in RATIFY'-total-helper (accepted? Γ es st) (¿ expired currentEpoch st ¿) (delayed? action prevAction es d)
-                          (compute ⟦ sig .proj₁ , treasury , currentEpoch ⟧ᵉ es action) refl
+    open RatifyEnv Γ; open GovActionState st
+    es'  = compute ⟦ gid , treasury , currentEpoch ⟧ᵉ es action
+    acc? = accepted? Γ es st
+    exp? = expired? currentEpoch st
+    del? = delayed? action prevAction es d
+
+    RATIFY'-total : ∃[ s' ] Γ ⊢ s ⇀⦇ sig ,RATIFY'⦈ s'
+    RATIFY'-total
+      with acc? | exp? | del?
+    ... | no ¬acc | no ¬exp | _ = -, RATIFY-Continue₁ ¬acc ¬exp
+    ... | no ¬acc | yes exp | _ = -, RATIFY-Reject ¬acc exp
+    ... | yes acc | _ | yes del = -, RATIFY-Continue₂₁ acc del
+    ... | yes acc | _ | no ¬del
+      = caseMaybe es'
+        ∣ (λ eq → -, RATIFY-Accept acc ¬del (≡-just⇔STS .Equivalence.to eq))
+        ∣ (λ eq → -, RATIFY-Continue₂₂ acc (nothing⇒∀¬STS eq))
+
+    computeProof = just RATIFY'-total
+
+    RATIFY'-completeness : ∀ s' → Γ ⊢ s ⇀⦇ sig ,RATIFY'⦈ s' → RATIFY'-total .proj₁ ≡ s'
+    RATIFY'-completeness s' (RATIFY-Continue₁ ¬acc ¬exp)
+      rewrite dec-no acc? ¬acc | dec-no exp? ¬exp = refl
+    RATIFY'-completeness s' (RATIFY-Reject ¬acc exp)
+      rewrite dec-no acc? ¬acc | dec-yes exp? exp .proj₂ = refl
+    RATIFY'-completeness s' (RATIFY-Continue₂₁ acc del)
+      rewrite dec-yes acc? acc .proj₂ | dec-yes del? del .proj₂ = refl
+    RATIFY'-completeness s' (RATIFY-Accept acc ¬del eq)
+      rewrite dec-yes acc? acc .proj₂ | dec-no del? ¬del
+      = cong proj₁
+      $ caseMaybe-just
+      $ Computational-ENACT .Computational.completeness _ _ _ _ eq
+    RATIFY'-completeness s' (RATIFY-Continue₂₂ acc h)
+      with del?
+    ... | yes del
+      rewrite dec-yes acc? acc .proj₂ | dec-yes del? del .proj₂ = refl
+    ... | no ¬del
+      rewrite dec-yes acc? acc .proj₂ | dec-no del? ¬del
+      = cong proj₁
+      $ caseMaybe-nothing
+      $ caseMaybe es'
+        ∣ ⊥-elim ∘ h _ ∘ ≡-just⇔STS .Equivalence.to
+        ∣ id
+
+    completeness = cong just ∘₂ RATIFY'-completeness
 
 instance
   Computational-RATIFY' : Computational _⊢_⇀⦇_,RATIFY'⦈_
-  Computational-RATIFY' .computeProof Γ s a = just RATIFY'-total
-  Computational-RATIFY' .completeness Γ ⟦ es , removed , d ⟧ʳ a s' h =
-    let open RatifyEnv Γ; st = proj₂ a; open GovActionState st in
-    cong just (RATIFY'-completeness-helper (accepted? Γ es st) ¿ expired currentEpoch st ¿ (delayed? action prevAction es d)
-                                           (compute ⟦ a .proj₁ , treasury , currentEpoch ⟧ᵉ es action) refl s' h)
+  Computational-RATIFY' = record {Implementation}
 
 Computational-RATIFY : Computational _⊢_⇀⦇_,RATIFY⦈_
 Computational-RATIFY = it
 
 RATIFY-total : ∀ {Γ s sig} → ∃[ s' ] Γ ⊢ s ⇀⦇ sig ,RATIFY⦈ s'
-RATIFY-total = SS⇒BS-total RATIFY'-total
+RATIFY-total = SS⇒BS-total (Implementation.RATIFY'-total _ _ _)
 
-RATIFY-complete : ∀ {Γ s sig s'} → Γ ⊢ s ⇀⦇ sig ,RATIFY⦈ s' → RATIFY-total {Γ} {s} {sig} .proj₁ ≡ s'
-RATIFY-complete h = computational⇒rightUnique it (RATIFY-total .proj₂) h
+RATIFY-complete : ∀ {Γ s sig s'} →
+  Γ ⊢ s ⇀⦇ sig ,RATIFY⦈ s' → RATIFY-total {Γ} {s} {sig} .proj₁ ≡ s'
+RATIFY-complete = computational⇒rightUnique it (RATIFY-total .proj₂)