diff --git a/src/Everything.agda b/src/Everything.agda index 2998e202c..8c25521f8 100644 --- a/src/Everything.agda +++ b/src/Everything.agda @@ -4,6 +4,7 @@ import Ledger.PDF import Ledger.Foreign.HSLedger import Ledger.NewPP +import Ledger.NewPP.Properties -- ^ deprecated in Conway, but keep it around for eventual earlier eras import MidnightExample.PDF diff --git a/src/Interface/ComputationalRelation.agda b/src/Interface/ComputationalRelation.agda index a034d50a1..f9983e187 100644 --- a/src/Interface/ComputationalRelation.agda +++ b/src/Interface/ComputationalRelation.agda @@ -55,6 +55,9 @@ module _ (STS : C → S → Sig → S → Set) where nothing⇒∀¬STS comp≡nothing s' h rewrite ≡-just⇔STS .Equivalence.from h = case comp≡nothing of λ () + recomputeProof : ∀ {Γ s sig s'} → STS Γ s sig s' → Maybe (∃[ s'' ] STS Γ s sig s'') + recomputeProof _ = computeProof _ _ _ + module _ {STS : C → S → Sig → S → Set} (comp : Computational STS) where open Computational comp diff --git a/src/Interface/Decidable/Instance.agda b/src/Interface/Decidable/Instance.agda index 903ee8b0a..175efb299 100644 --- a/src/Interface/Decidable/Instance.agda +++ b/src/Interface/Decidable/Instance.agda @@ -11,6 +11,8 @@ open import Data.Maybe using (Maybe; just; nothing; Is-just) open import Data.Maybe.Relation.Unary.Any using (just) open import Data.Sum using (_⊎_; inj₁; inj₂) open import Data.Sum.Relation.Unary.All using (inj₁; inj₂) renaming (All to All⊎) +import Data.Rational as ℚ using (_≤_) +import Data.Rational.Properties as ℚ using (_≤?_) open import Relation.Binary renaming (Decidable to Decidable²) open import Relation.Binary.PropositionalEquality using (_≡_) @@ -87,3 +89,6 @@ instance with ¿ Q y ¿ ... | yes qy = yes (inj₂ qy) ... | no ¬qy = no λ where (inj₂ qy) → ¬qy qy + + Dec-ℚ≤ : ∀ {q r} → Dec (q ℚ.≤ r) + Dec-ℚ≤ = Decidable²⇒Dec ℚ._≤?_ diff --git a/src/Ledger/Chain.lagda b/src/Ledger/Chain.lagda index fd5c9f9d9..4c499f975 100644 --- a/src/Ledger/Chain.lagda +++ b/src/Ledger/Chain.lagda @@ -181,11 +181,11 @@ data \begin{figure*}[h] \begin{code} CHAIN : - let open ChainState s; open Block b; open NewEpochState nes; open EnactState es in - record { stakeDistrs = calculateStakeDistrs ls } + let open ChainState s; open Block b; open EnactState (newEpochState .NewEpochState.es) in + record { stakeDistrs = calculateStakeDistrs (newEpochState .NewEpochState.ls) } ⊢ newEpochState ⇀⦇ epoch slot ,NEWEPOCH⦈ nes → ⟦ slot , constitution .proj₁ .proj₂ , pparams .proj₁ ⟧ˡᵉ - ⊢ ls ⇀⦇ ts ,LEDGERS⦈ ls' + ⊢ nes .NewEpochState.ls ⇀⦇ ts ,LEDGERS⦈ ls' ──────────────────────────────── _ ⊢ s ⇀⦇ b ,CHAIN⦈ record s { newEpochState = record nes { ls = ls' } } \end{code} diff --git a/src/Ledger/Chain/Properties.agda b/src/Ledger/Chain/Properties.agda index f6224993d..2dd7f2374 100644 --- a/src/Ledger/Chain/Properties.agda +++ b/src/Ledger/Chain/Properties.agda @@ -5,6 +5,7 @@ open import Data.Nat.Properties hiding (_≟_) open import Ledger.Prelude open import Ledger.Transaction open import Ledger.Abstract +import Data.Maybe module Ledger.Chain.Properties (txs : _) (open TransactionStructure txs) @@ -12,28 +13,50 @@ module Ledger.Chain.Properties where open import Ledger.Ratify txs +open import Ledger.Ledger.Properties txs abs open import Ledger.Ratify.Properties txs open import Ledger.Chain txs abs open import Ledger.Ledger txs abs --- TODO: get rid of all of those arguments once we have them globally - -module _ (accepted? : ∀ Γ es st → Dec (accepted Γ es st)) - (expired? : ∀ e st → Dec (expired e st)) - (delayed? : ∀ a p es d → Dec (delayed a p es d)) - (Computational-ENACT : Computational _⊢_⇀⦇_,ENACT⦈_) where - - NEWEPOCH-total : ∀ {Γ s sig} → ∃[ s' ] Γ ⊢ s ⇀⦇ sig ,NEWEPOCH⦈ s' - NEWEPOCH-total {Γ} {nes} {e} = - let open NewEpochState nes hiding (es) - open RatifyState fut using (removed) renaming (es to esW) - open LState ls; open CertState certState; open Acnt acnt - es = record esW { withdrawals = ∅ᵐ } - govSt' = filter (λ x → ¿ ¬ proj₁ x ∈ mapˢ proj₁ removed ¿) govSt - (_ , pFut) = RATIFY-total accepted? expired? delayed? Computational-ENACT - {record { currentEpoch = e ; treasury = treasury - ; GState gState ; NewEpochEnv Γ }} {⟦ es , ∅ , false ⟧ʳ} {govSt'} - in +open Computational ⦃...⦄ + +module _ {Γ : NewEpochEnv} {nes : NewEpochState} {e : Epoch} where + + open NewEpochState nes hiding (es) + open RatifyState fut using (removed) renaming (es to esW) + open LState ls; open CertState certState; open Acnt acnt + es = record esW { withdrawals = ∅ᵐ } + govSt' = filter (λ x → ¿ ¬ proj₁ x ∈ mapˢ proj₁ removed ¿) govSt + + NEWEPOCH-total : ∃[ nes' ] Γ ⊢ nes ⇀⦇ e ,NEWEPOCH⦈ nes' + NEWEPOCH-total = 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' 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⦈_ + Computational-NEWEPOCH .computeProof Γ s sig = just NEWEPOCH-total + Computational-NEWEPOCH .completeness Γ s sig s' h = cong just (NEWEPOCH-complete s' h) + + Computational-CHAIN : Computational _⊢_⇀⦇_,CHAIN⦈_ + Computational-CHAIN .computeProof Γ s b = do + _ , neStep ← computeProof _ _ _ + _ , lsStep ← computeProof _ _ _ + just (_ , CHAIN neStep lsStep) + where open Data.Maybe using (_>>=_) + Computational-CHAIN .completeness Γ s b s' (CHAIN neStep lsStep) + with recomputeProof neStep | completeness _ _ _ _ neStep + ... | _ | refl + with recomputeProof lsStep | completeness _ _ _ _ lsStep + ... | just _ | refl = refl diff --git a/src/Ledger/Introduction.lagda b/src/Ledger/Introduction.lagda index e0b49e6a2..a50f6c6c2 100644 --- a/src/Ledger/Introduction.lagda +++ b/src/Ledger/Introduction.lagda @@ -5,6 +5,9 @@ module Ledger.Introduction where open import Prelude +import Data.Maybe as Maybe +open import Data.Maybe.Properties +open import Relation.Binary.PropositionalEquality \end{code} Repository: https://github.com/input-output-hk/formal-ledger-specifications @@ -39,7 +42,7 @@ other, forming a directed graph that is almost a tree. Since all such state machines need to be evaluated by the node and all nodes should compute the same states, the relations specified by them -should be computable by functions. This is captured by the following +should be computable by functions. This can be captured by the following record, which is parametrized over the step relation. \begin{code}[hide] @@ -55,8 +58,14 @@ record Computational (_⊢_⇀⦇_,X⦈_ : C → S → Sig → S → Set) : Set field compute : C → S → Sig → Maybe S ≡-just⇔STS : compute Γ s b ≡ just s' ⇔ Γ ⊢ s ⇀⦇ b ,X⦈ s' + + nothing⇒∀¬STS : compute Γ s b ≡ nothing → ∀ s' → ¬ Γ ⊢ s ⇀⦇ b ,X⦈ s' \end{code} \end{figure*} +\begin{code}[hide] + nothing⇒∀¬STS comp≡nothing s' h rewrite ≡-just⇔STS .Equivalence.from h = + case comp≡nothing of λ () +\end{code} \subsection{Sets \& maps} diff --git a/src/Ledger/Ledger/Properties.agda b/src/Ledger/Ledger/Properties.agda index 76e7edab1..312ab4a6f 100644 --- a/src/Ledger/Ledger/Properties.agda +++ b/src/Ledger/Ledger/Properties.agda @@ -64,6 +64,9 @@ instance ... | just (govSt' , _) | refl rewrite dec-yes (LEDGER-premises? certSt') h .proj₂ = refl +Computational-LEDGERS : Computational _⊢_⇀⦇_,LEDGERS⦈_ +Computational-LEDGERS = it + instance HasCoin-LState : HasCoin LState HasCoin-LState .getCoin s = getCoin (LState.utxoSt s) diff --git a/src/Ledger/NewPP.lagda b/src/Ledger/NewPP.lagda index 18cc64b15..e03180733 100644 --- a/src/Ledger/NewPP.lagda +++ b/src/Ledger/NewPP.lagda @@ -40,7 +40,6 @@ votedValue pup pparams quorum = private variable Γ : NewPParamEnv s s' : NewPParamState - newpp : PParams upd : PParamsUpdate data _⊢_⇀⦇_,NEWPP⦈_ : NewPParamEnv → NewPParamState → Maybe PParamsUpdate → NewPParamState → Set where @@ -52,8 +51,8 @@ data _⊢_⇀⦇_,NEWPP⦈_ : NewPParamEnv → NewPParamState → Maybe PParamsU ──────────────────────────────── Γ ⊢ s ⇀⦇ just upd ,NEWPP⦈ ⟦ newpp , updatePPUp newpp ppup ⟧ⁿᵖ - NEWPP-Reject : ∀ {Γ} → let open NewPParamState s in - Γ ⊢ s ⇀⦇ nothing ,NEWPP⦈ ⟦ pparams , updatePPUp newpp ppup ⟧ⁿᵖ + NEWPP-Reject : ∀ {Γ} → + Γ ⊢ s ⇀⦇ nothing ,NEWPP⦈ s \end{code} \caption{NEWPP transition system} \end{figure*} diff --git a/src/Ledger/NewPP/Properties.agda b/src/Ledger/NewPP/Properties.agda new file mode 100644 index 000000000..57868d33e --- /dev/null +++ b/src/Ledger/NewPP/Properties.agda @@ -0,0 +1,29 @@ +{-# OPTIONS --safe #-} + +open import Relation.Nullary.Decidable + +open import Ledger.Prelude +open import Ledger.Transaction + +module Ledger.NewPP.Properties (txs : _) (open TransactionStructure txs) where + +open import Ledger.PPUp txs +open import Ledger.NewPP txs + +instance + Computational-NEWPP : Computational _⊢_⇀⦇_,NEWPP⦈_ + 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 b1dc70281..fd15ce2e4 100644 --- a/src/Ledger/Ratify.lagda +++ b/src/Ledger/Ratify.lagda @@ -343,46 +343,43 @@ 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 - -accepted' : RatifyEnv → EnactState → GovActionState → Set -accepted' Γ (record { cc = cc , _ ; pparams = pparams , _ }) gs = - acceptedBy CC ∧ acceptedBy DRep ∧ acceptedBy SPO ∧ meetsMinAVS - where - open RatifyEnv Γ; open GovActionState gs; open PParams pparams - - votes' = actualVotes Γ cc votes action pparams - cc' = dom votes' - redStakeDistr = restrictedDists coinThreshold rankThreshold stakeDistrs - - meetsMinAVS : Set - meetsMinAVS = activeVotingStake cc' redStakeDistr votes' ≥ minimumAVS - - acceptedBy : GovRole → Set - acceptedBy role = - let t = maybe id 0ℚ $ threshold pparams (proj₂ <$> cc) action role in - case totalStake role cc' redStakeDistr votes' of λ where - 0 → t ≡ 0ℚ -- if there's no stake, accept only if threshold is zero - x@(suc _) → ℤ.+ acceptedStake role cc' redStakeDistr votes' ℚ./ x ℚ.≥ t - -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 ℚ.0ℚ $ threshold pparams (proj₂ <$> cc) action role in + case totalStake role cc' redStakeDistr votes' of λ where + 0 → t ≡ ℚ.0ℚ -- if there's no stake, accept only if threshold is zero + x@(suc _) → ℤ.+ acceptedStake role cc' redStakeDistr votes' ℚ./ x ℚ.≥ 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} } %% end small \caption{%%Ratify iii: @@ -426,6 +423,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} @@ -446,11 +475,6 @@ private variable removed : ℙ (GovActionID × GovActionState) d : Bool --- having `accepted` abstract speeds up type checking of RATIFY' a lot -abstract - accepted : RatifyEnv → EnactState → GovActionState → Set - accepted = accepted' - data _⊢_⇀⦇_,RATIFY'⦈_ : RatifyEnv → RatifyState → GovActionID × GovActionState → RatifyState → Set where \end{code} @@ -473,10 +497,9 @@ data _⊢_⇀⦇_,RATIFY'⦈_ : RatifyEnv → RatifyState → GovActionID × Gov RATIFY-Continue : let open RatifyEnv Γ; st = a .proj₂; open GovActionState st in ¬ accepted Γ es st × ¬ expired currentEpoch st - ⊎ delayed action prevAction es d ⊎ accepted Γ es st - × ¬ delayed action prevAction es d - × (∀ es' → ¬ ⟦ a .proj₁ , treasury , currentEpoch ⟧ᵉ ⊢ es ⇀⦇ action ,ENACT⦈ es') + × (delayed action prevAction es d ⊎ + (∀ es' → ¬ ⟦ a .proj₁ , treasury , currentEpoch ⟧ᵉ ⊢ es ⇀⦇ action ,ENACT⦈ es')) ──────────────────────────────── Γ ⊢ ⟦ es , removed , d ⟧ʳ ⇀⦇ a ,RATIFY'⦈ ⟦ es , removed , d ⟧ʳ diff --git a/src/Ledger/Ratify/Properties.agda b/src/Ledger/Ratify/Properties.agda index 715c8c941..c9164f751 100644 --- a/src/Ledger/Ratify/Properties.agda +++ b/src/Ledger/Ratify/Properties.agda @@ -8,31 +8,90 @@ module Ledger.Ratify.Properties (txs : _) (open TransactionStructure txs) where open import Ledger.Gov govStructure open import Ledger.Ratify txs -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 - --- TODO: get rid of all of those arguments once we have them globally - -module _ (accepted? : ∀ Γ es st → Dec (accepted Γ es st)) - (expired? : ∀ e st → Dec (expired e st)) - (delayed? : ∀ a p es d → Dec (delayed a p es d)) - (Computational-ENACT : Computational _⊢_⇀⦇_,ENACT⦈_) where - - - RATIFY'-total : ∀ {Γ s sig} → ∃[ s' ] Γ ⊢ s ⇀⦇ sig ,RATIFY'⦈ s' - RATIFY'-total {Γ} {⟦ es , removed , d ⟧ʳ} {sig} = - let open RatifyEnv Γ; st = proj₂ sig; open GovActionState st - open Computational Computational-ENACT - in - case accepted? Γ es st of λ where - (no ¬p) → case expired? currentEpoch st of λ where - (no ¬q) → -, RATIFY-Continue (inj₁ (¬p , ¬q)) - (yes p) → -, RATIFY-Reject ¬p p - (yes p) → case delayed? action prevAction es d of λ where - (no ¬q) → caseEq (compute ⟦ sig .proj₁ , treasury , currentEpoch ⟧ᵉ es action) of λ where - (just x) eq → -, RATIFY-Accept p ¬q (≡-just⇔STS .Equivalence.to eq) - nothing eq → -, RATIFY-Continue (inj₂ (inj₂ (p , ¬q , nothing⇒∀¬STS eq))) - (yes q) → -, RATIFY-Continue (inj₂ (inj₁ q)) - - RATIFY-total : ∀ {Γ s sig} → ∃[ s' ] Γ ⊢ s ⇀⦇ sig ,RATIFY⦈ s' - RATIFY-total = SS⇒BS-total RATIFY'-total +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 + 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' = record {Implementation} + +Computational-RATIFY : Computational _⊢_⇀⦇_,RATIFY⦈_ +Computational-RATIFY = it + +RATIFY-total : ∀ {Γ s sig} → ∃[ s' ] Γ ⊢ s ⇀⦇ sig ,RATIFY⦈ s' +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 = computational⇒rightUnique it (RATIFY-total .proj₂) diff --git a/src/Ledger/Utxo/Properties.lagda b/src/Ledger/Utxo/Properties.lagda index d93058f07..3df2b7de1 100644 --- a/src/Ledger/Utxo/Properties.lagda +++ b/src/Ledger/Utxo/Properties.lagda @@ -20,7 +20,7 @@ open import Tactic.EquationalReasoning using (module ≡-Reasoning) open import Tactic.MonoidSolver using (solve-macro) open Tactic.EquationalReasoning.≡-Reasoning {A = ℕ} (solve-macro (quoteTerm +-0-monoid)) -open import Ledger.Prelude; open Properties; open Computational +open import Ledger.Prelude; open Properties; open Computational ⦃...⦄ open import Ledger.Abstract open import Ledger.Transaction @@ -309,17 +309,16 @@ module DepositHelpers ∎ \end{code} -Here, we state the fact that the UTxO relation is computable. This -just follows from our automation. +Here, we state the fact that the UTxO relation is computable. \begin{figure*}[h] \begin{code} UTXO-step : UTxOEnv → UTxOState → Tx → Maybe UTxOState -UTXO-step = compute Computational-UTXO +UTXO-step = compute UTXO-step-computes-UTXO : UTXO-step Γ utxoState tx ≡ just utxoState' ⇔ Γ ⊢ utxoState ⇀⦇ tx ,UTXO⦈ utxoState' -UTXO-step-computes-UTXO = ≡-just⇔STS Computational-UTXO +UTXO-step-computes-UTXO = ≡-just⇔STS \end{code} \caption{Computing the UTXO transition system} \end{figure*}