From e65bce5c7291525176cd9d258d7ba2cefecb364d Mon Sep 17 00:00:00 2001 From: Ulf Norell Date: Tue, 17 Oct 2023 08:57:15 +0200 Subject: [PATCH] Abstract definitions for cleaner Ratify.Properties (#247) Co-authored-by: Orestis Melkonian --- src/Ledger/Chain/Properties.agda | 18 ++-- src/Ledger/NewPP/Properties.agda | 28 ++--- src/Ledger/Ratify.lagda | 109 +++++++++++++------- src/Ledger/Ratify/Properties.agda | 165 ++++++++++++++---------------- 4 files changed, 174 insertions(+), 146 deletions(-) diff --git a/src/Ledger/Chain/Properties.agda b/src/Ledger/Chain/Properties.agda index ad8294cf3..893016264 100644 --- 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 index 8951670db..57868d33e 100644 --- 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 index a66e8fb50..566c4af3b 100644 --- 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 index 13407efc0..c9164f751 100644 --- 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₂)