From d406853c4ef78b446a6eb76272d52a0e8b2b17ad Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Fri, 22 Nov 2024 05:35:46 -0700 Subject: [PATCH] CERTS should do the base case first (#604) * CERTS should do the base case first This closes issue #545. * progress * implement Ulf's idea to split off base case * progress * task complete * cleanup: remove unused code; clean up some pdf figures * attempt at more abstract implementation of "base case first" mod * proof of computationality and completeness * cleanup --- src/Interface/ComputationalRelation.agda | 35 +++++++++++++++++------ src/Interface/STS.agda | 30 ++++++++++++------- src/Ledger/Certs.lagda | 32 ++++++++++----------- src/Ledger/Certs/Properties.agda | 19 +++++++----- src/Ledger/Conway/Conformance/Certs.agda | 2 +- src/Ledger/Conway/Conformance/Gov.agda | 2 +- src/Ledger/Conway/Conformance/Ledger.agda | 2 +- src/Ledger/Gov.lagda | 2 +- src/Ledger/Ledger.lagda | 2 +- src/Ledger/Ledger/Properties.agda | 2 +- src/Ledger/Ratify.lagda | 2 +- 11 files changed, 82 insertions(+), 48 deletions(-) diff --git a/src/Interface/ComputationalRelation.agda b/src/Interface/ComputationalRelation.agda index 879995ded..d6eb89371 100644 --- a/src/Interface/ComputationalRelation.agda +++ b/src/Interface/ComputationalRelation.agda @@ -40,7 +40,7 @@ instance Bifunctor-ComputationResult : ∀ {a : Level} → Bifunctor {_} {a} ComputationResult Bifunctor-ComputationResult .bimap _ f (success x) = success $ f x Bifunctor-ComputationResult .bimap f _ (failure x) = failure $ f x - + Functor-ComputationResult : ∀ {E : Type} → Functor (ComputationResult E) Functor-ComputationResult ._<$>_ f (success x) = success $ f x Functor-ComputationResult ._<$>_ _ (failure x) = failure x @@ -135,7 +135,7 @@ module _ {STS : C → S → Sig → S → Type} (comp : Computational STS Err) w ExtendedRel-rightUnique {s' = success x} {success x'} h h' with trans (sym $ Equivalence.from ≡-success⇔STS h) (Equivalence.from ≡-success⇔STS h') ... | refl = refl - + ExtendedRel-rightUnique {s' = success x} {failure _} h h' = ⊥-elim $ h' x h ExtendedRel-rightUnique {s' = failure _} {success x'} h h' = ⊥-elim $ h x' h' ExtendedRel-rightUnique {s' = failure a} {failure b} h h' = refl @@ -190,9 +190,9 @@ instance module _ {BSTS : C → S → ⊤ → S → Type} ⦃ _ : Computational BSTS Err₁ ⦄ where module _ {STS : C → S → Sig → S → Type} ⦃ _ : Computational STS Err₂ ⦄ ⦃ _ : InjectError Err₁ Err ⦄ ⦃ _ : InjectError Err₂ Err ⦄ where instance - Computational-ReflexiveTransitiveClosureᵇ : Computational (ReflexiveTransitiveClosureᵇ BSTS STS) (Err) + Computational-ReflexiveTransitiveClosureᵇ : Computational (ReflexiveTransitiveClosureᵇ {_⊢_⇀⟦_⟧ᵇ_ = BSTS}{STS}) (Err) Computational-ReflexiveTransitiveClosureᵇ .computeProof c s [] = bimap (injectError it) (map₂′ BS-base) (computeProof c s tt) - Computational-ReflexiveTransitiveClosureᵇ .computeProof c s (sig ∷ sigs) with computeProof c s sig + Computational-ReflexiveTransitiveClosureᵇ .computeProof c s (sig ∷ sigs) with computeProof c s sig ... | success (s₁ , h) with computeProof c s₁ sigs ... | success (s₂ , hs) = success (s₂ , BS-ind h hs) ... | failure a = failure (injectError it a) @@ -209,7 +209,7 @@ module _ {BSTS : C → S → ⊤ → S → Type} ⦃ _ : Computational BSTS Err module _ {STS : C × ℕ → S → Sig → S → Type} ⦃ Computational-STS : Computational STS Err₂ ⦄ ⦃ InjectError-Err₁ : InjectError Err₁ Err ⦄ ⦃ InjectError-Err₂ : InjectError Err₂ Err ⦄ where instance - Computational-ReflexiveTransitiveClosureᵢᵇ' : Computational (_⊢_⇀⟦_⟧ᵢ*'_ BSTS STS) Err + Computational-ReflexiveTransitiveClosureᵢᵇ' : Computational (_⊢_⇀⟦_⟧ᵢ*'_ {_⊢_⇀⟦_⟧ᵇ_ = BSTS}{STS}) Err Computational-ReflexiveTransitiveClosureᵢᵇ' .computeProof c s [] = bimap (injectError it) (map₂′ BS-base) (computeProof (proj₁ c) s tt) Computational-ReflexiveTransitiveClosureᵢᵇ' .computeProof c s (sig ∷ sigs) with computeProof c s sig @@ -226,16 +226,35 @@ module _ {BSTS : C → S → ⊤ → S → Type} ⦃ _ : Computational BSTS Err with computeProof (proj₁ c , suc (proj₂ c)) s₁ sigs | completeness _ _ _ _ hs ... | success (s₂ , _) | p = p - Computational-ReflexiveTransitiveClosureᵢᵇ : Computational (ReflexiveTransitiveClosureᵢᵇ BSTS STS) Err + Computational-ReflexiveTransitiveClosureᵢᵇ : Computational (ReflexiveTransitiveClosureᵢᵇ {_⊢_⇀⟦_⟧ᵇ_ = BSTS}{STS}) Err Computational-ReflexiveTransitiveClosureᵢᵇ .computeProof c = Computational-ReflexiveTransitiveClosureᵢᵇ' .computeProof (c , 0) Computational-ReflexiveTransitiveClosureᵢᵇ .completeness c = Computational-ReflexiveTransitiveClosureᵢᵇ' .completeness (c , 0) +module _ {BSTS : C → S → ⊤ → S → Type} ⦃ _ : Computational BSTS Err₁ ⦄ where + module _ {STS : C → S → Sig → S → Type} ⦃ _ : Computational STS Err₂ ⦄ + ⦃ _ : InjectError Err₁ Err ⦄ ⦃ _ : InjectError Err₂ Err ⦄ where instance + Computational-ReflexiveTransitiveClosureᵇ' : Computational (ReflexiveTransitiveClosureᵇ' {_⊢_⇀⟦_⟧ᵇ_ = BSTS} {STS}) (Err) + Computational-ReflexiveTransitiveClosureᵇ' .computeProof c s sigs with (computeProof{STS = BSTS} c s tt) + ... | failure a = failure (injectError it a) + ... | success (s' , h) with (computeProof{STS = ReflexiveTransitiveClosureᵇ {_⊢_⇀⟦_⟧ᵇ_ = IdSTS} {STS}} c s' sigs) + ... | failure a = failure a + ... | success (s' , hs) = success (s' , (RTC (h , hs))) + + Computational-ReflexiveTransitiveClosureᵇ' .completeness c s sigs s'' (RTC (bsts , sts)) + with (computeProof {STS = BSTS} c s tt) | completeness _ _ _ _ bsts + ... | success (s₁ , h) | refl + with computeProof {STS = ReflexiveTransitiveClosureᵇ {_⊢_⇀⟦_⟧ᵇ_ = IdSTS} {STS}}{Err} c s₁ sigs + | completeness {Err = Err} _ _ _ _ sts + ... | success (s₂ , _) | p = p + + Computational-ReflexiveTransitiveClosure : {STS : C → S → Sig → S → Type} → ⦃ Computational STS Err ⦄ - → Computational (ReflexiveTransitiveClosure STS) Err + → Computational (ReflexiveTransitiveClosure {sts = STS}) Err Computational-ReflexiveTransitiveClosure = it Computational-ReflexiveTransitiveClosureᵢ : {STS : C × ℕ → S → Sig → S → Type} → ⦃ Computational STS Err ⦄ - → Computational (ReflexiveTransitiveClosureᵢ STS) Err + → Computational (ReflexiveTransitiveClosureᵢ {sts = STS}) Err Computational-ReflexiveTransitiveClosureᵢ = it + diff --git a/src/Interface/STS.agda b/src/Interface/STS.agda index cbe268b17..515aed50b 100644 --- a/src/Interface/STS.agda +++ b/src/Interface/STS.agda @@ -39,7 +39,7 @@ private -- small-step to big-step transformer -module _ (_⊢_⇀⟦_⟧ᵇ_ : C → S → ⊤ → S → Type) (_⊢_⇀⟦_⟧_ : C → S → Sig → S → Type) where +module _ {_⊢_⇀⟦_⟧ᵇ_ : C → S → ⊤ → S → Type} {_⊢_⇀⟦_⟧_ : C → S → Sig → S → Type} where data _⊢_⇀⟦_⟧*_ : C → S → List Sig → S → Type where BS-base : @@ -53,7 +53,7 @@ module _ (_⊢_⇀⟦_⟧ᵇ_ : C → S → ⊤ → S → Type) (_⊢_⇀⟦_⟧ ─────────────────────────────────────── Γ ⊢ s ⇀⟦ sig ∷ sigs ⟧* s'' -module _ (_⊢_⇀⟦_⟧ᵇ_ : C → S → ⊤ → S → Type) (_⊢_⇀⟦_⟧_ : C × ℕ → S → Sig → S → Type) where +module _ {_⊢_⇀⟦_⟧ᵇ_ : C → S → ⊤ → S → Type} {_⊢_⇀⟦_⟧_ : C × ℕ → S → Sig → S → Type} where data _⊢_⇀⟦_⟧ᵢ*'_ : C × ℕ → S → List Sig → S → Type where BS-base : @@ -73,29 +73,38 @@ module _ (_⊢_⇀⟦_⟧ᵇ_ : C → S → ⊤ → S → Type) (_⊢_⇀⟦_⟧ data IdSTS {C S} : C → S → ⊤ → S → Type where Id-nop : IdSTS Γ s _ s +module _ {_⊢_⇀⟦_⟧ᵇ_ : C → S → ⊤ → S → Type} {_⊢_⇀⟦_⟧_ : C → S → Sig → S → Type} where + data _⊢_⇀⟦_⟧*'_ : C → S → List Sig → S → Type where + RTC : + ∙ Γ ⊢ s ⇀⟦ _ ⟧ᵇ s' + ∙ _⊢_⇀⟦_⟧*_ {_⊢_⇀⟦_⟧ᵇ_ = IdSTS}{_⊢_⇀⟦_⟧_} Γ s' sigs s'' + ─────────────────────────────────────── + Γ ⊢ s ⇀⟦ sigs ⟧*' s'' + + -- with a trivial base case -ReflexiveTransitiveClosure : (C → S → Sig → S → Type) → C → S → List Sig → S → Type -ReflexiveTransitiveClosure = _⊢_⇀⟦_⟧*_ IdSTS +ReflexiveTransitiveClosure : {sts : C → S → Sig → S → Type} → C → S → List Sig → S → Type +ReflexiveTransitiveClosure {sts = sts} = _⊢_⇀⟦_⟧*_ {_⊢_⇀⟦_⟧ᵇ_ = IdSTS}{sts} STS-total : (C → S → Sig → S → Type) → Type STS-total _⊢_⇀⟦_⟧_ = ∀ {Γ s sig} → ∃[ s' ] Γ ⊢ s ⇀⟦ sig ⟧ s' ReflexiveTransitiveClosure-total : {_⊢_⇀⟦_⟧_ : C → S → Sig → S → Type} - → STS-total _⊢_⇀⟦_⟧_ → STS-total (ReflexiveTransitiveClosure _⊢_⇀⟦_⟧_) + → STS-total _⊢_⇀⟦_⟧_ → STS-total (ReflexiveTransitiveClosure {sts = _⊢_⇀⟦_⟧_}) ReflexiveTransitiveClosure-total SS-total {Γ} {s} {[]} = s , BS-base Id-nop ReflexiveTransitiveClosure-total SS-total {Γ} {s} {x ∷ sig} = case SS-total of λ where (s' , Ps') → map₂′ (BS-ind Ps') $ ReflexiveTransitiveClosure-total SS-total -ReflexiveTransitiveClosureᵢ : (C × ℕ → S → Sig → S → Type) → C → S → List Sig → S → Type -ReflexiveTransitiveClosureᵢ = _⊢_⇀⟦_⟧ᵢ*_ IdSTS +ReflexiveTransitiveClosureᵢ : {sts : C × ℕ → S → Sig → S → Type} → C → S → List Sig → S → Type +ReflexiveTransitiveClosureᵢ {sts = sts} = _⊢_⇀⟦_⟧ᵢ*_ {_⊢_⇀⟦_⟧ᵇ_ = IdSTS}{sts} ReflexiveTransitiveClosureᵢ-total : {_⊢_⇀⟦_⟧_ : C × ℕ → S → Sig → S → Type} - → STS-total _⊢_⇀⟦_⟧_ → STS-total (ReflexiveTransitiveClosureᵢ _⊢_⇀⟦_⟧_) + → STS-total _⊢_⇀⟦_⟧_ → STS-total (ReflexiveTransitiveClosureᵢ {sts = _⊢_⇀⟦_⟧_}) ReflexiveTransitiveClosureᵢ-total SS-total = helper SS-total where helper : {_⊢_⇀⟦_⟧_ : C × ℕ → S → Sig → S → Type} - → STS-total _⊢_⇀⟦_⟧_ → STS-total (_⊢_⇀⟦_⟧ᵢ*'_ IdSTS _⊢_⇀⟦_⟧_) + → STS-total _⊢_⇀⟦_⟧_ → STS-total (_⊢_⇀⟦_⟧ᵢ*'_ {_⊢_⇀⟦_⟧ᵇ_ = IdSTS}{_⊢_⇀⟦_⟧_}) helper SS-total {s = s} {[]} = s , BS-base Id-nop helper SS-total {s = s} {x ∷ sig} = case SS-total of λ where @@ -104,11 +113,12 @@ ReflexiveTransitiveClosureᵢ-total SS-total = helper SS-total -- with a given base case ReflexiveTransitiveClosureᵢᵇ = _⊢_⇀⟦_⟧ᵢ*_ ReflexiveTransitiveClosureᵇ = _⊢_⇀⟦_⟧*_ +ReflexiveTransitiveClosureᵇ' = _⊢_⇀⟦_⟧*'_ LedgerInvariant : (C → S → Sig → S → Type) → (S → Type) → Type LedgerInvariant STS P = ∀ {c s sig s'} → STS c s sig s' → P s → P s' RTC-preserves-inv : ∀ {STS : C → S → Sig → S → Type} {P} - → LedgerInvariant STS P → LedgerInvariant (ReflexiveTransitiveClosure STS) P + → LedgerInvariant STS P → LedgerInvariant (ReflexiveTransitiveClosure {sts = STS}) P RTC-preserves-inv inv (BS-base Id-nop) = id RTC-preserves-inv inv (BS-ind p₁ p₂) = RTC-preserves-inv inv p₂ ∘ inv p₁ diff --git a/src/Ledger/Certs.lagda b/src/Ledger/Certs.lagda index dca153797..91820df67 100644 --- a/src/Ledger/Certs.lagda +++ b/src/Ledger/Certs.lagda @@ -264,42 +264,41 @@ constitutional committee. \end{itemize} \begin{figure*}[h] -\begin{AgdaSuppressSpace} +\begin{AgdaMultiCode} \begin{code}[hide] data \end{code} \begin{code} - _⊢_⇀⦇_,DELEG⦈_ : DelegEnv → DState → DCert → DState → Type + _⊢_⇀⦇_,DELEG⦈_ : DelegEnv → DState → DCert → DState → Type \end{code} \begin{code}[hide] data \end{code} \begin{code} - _⊢_⇀⦇_,POOL⦈_ : PoolEnv → PState → DCert → PState → Type + _⊢_⇀⦇_,POOL⦈_ : PoolEnv → PState → DCert → PState → Type \end{code} \begin{code}[hide] data \end{code} \begin{code} - _⊢_⇀⦇_,GOVCERT⦈_ : GovCertEnv → GState → DCert → GState → Type + _⊢_⇀⦇_,GOVCERT⦈_ : GovCertEnv → GState → DCert → GState → Type \end{code} \begin{code}[hide] data \end{code} \begin{code} - _⊢_⇀⦇_,CERT⦈_ : CertEnv → CertState → DCert → CertState → Type + _⊢_⇀⦇_,CERT⦈_ : CertEnv → CertState → DCert → CertState → Type \end{code} \begin{code}[hide] data \end{code} \begin{code} - _⊢_⇀⦇_,CERTBASE⦈_ : CertEnv → CertState → ⊤ → CertState → Type -\end{code} -\begin{code} -_⊢_⇀⦇_,CERTS⦈_ : CertEnv → CertState → List DCert → CertState → Type -_⊢_⇀⦇_,CERTS⦈_ = ReflexiveTransitiveClosureᵇ _⊢_⇀⦇_,CERTBASE⦈_ _⊢_⇀⦇_,CERT⦈_ + _⊢_⇀⦇_,CERTBASE⦈_ : CertEnv → CertState → ⊤ → CertState → Type + +_⊢_⇀⦇_,CERTS⦈_ : CertEnv → CertState → List DCert → CertState → Type +_⊢_⇀⦇_,CERTS⦈_ = ReflexiveTransitiveClosureᵇ' {_⊢_⇀⟦_⟧ᵇ_ = _⊢_⇀⦇_,CERTBASE⦈_} {_⊢_⇀⦇_,CERT⦈_} \end{code} -\end{AgdaSuppressSpace} +\end{AgdaMultiCode} \caption{Types for the transition systems relating to certificates} \label{fig:sts:certs-types} \end{figure*} @@ -318,15 +317,15 @@ data _⊢_⇀⦇_,DELEG⦈_ where fromList ( nothing ∷ just abstainRep ∷ just noConfidenceRep ∷ [] ) ∙ mkh ∈ mapˢ just (dom pools) ∪ ❴ nothing ❵ ──────────────────────────────── - ⟦ pp , pools , delegatees ⟧ᵈᵉ ⊢ - ⟦ vDelegs , sDelegs , rwds ⟧ᵈ ⇀⦇ delegate c mv mkh d ,DELEG⦈ + ⟦ pp , pools , delegatees ⟧ᵈᵉ ⊢ ⟦ vDelegs , sDelegs , rwds ⟧ᵈ + ⇀⦇ delegate c mv mkh d ,DELEG⦈ ⟦ insertIfJust c mv vDelegs , insertIfJust c mkh sDelegs , rwds ∪ˡ ❴ c , 0 ❵ ⟧ᵈ DELEG-dereg : ∙ (c , 0) ∈ rwds ──────────────────────────────── - ⟦ pp , pools , delegatees ⟧ᵈᵉ ⊢ ⟦ vDelegs , sDelegs , rwds ⟧ᵈ ⇀⦇ dereg c d ,DELEG⦈ - ⟦ vDelegs ∣ ❴ c ❵ ᶜ , sDelegs ∣ ❴ c ❵ ᶜ , rwds ∣ ❴ c ❵ ᶜ ⟧ᵈ + ⟦ pp , pools , delegatees ⟧ᵈᵉ ⊢ ⟦ vDelegs , sDelegs , rwds ⟧ᵈ ⇀⦇ dereg c d ,DELEG⦈ + ⟦ vDelegs ∣ ❴ c ❵ ᶜ , sDelegs ∣ ❴ c ❵ ᶜ , rwds ∣ ❴ c ❵ ᶜ ⟧ᵈ \end{code} \end{AgdaSuppressSpace} \caption{Auxiliary DELEG transition system} @@ -430,7 +429,8 @@ data _⊢_⇀⦇_,CERTBASE⦈_ where refresh = mapPartial getDRepVote (fromList vs) refreshedDReps = mapValueRestricted (const (e + drepActivity)) dReps refresh wdrlCreds = mapˢ stake (dom wdrls) - validVoteDelegs = voteDelegs ∣^ (mapˢ (credVoter DRep) (dom dReps) ∪ fromList (noConfidenceRep ∷ abstainRep ∷ [])) + validVoteDelegs = voteDelegs ∣^ ( mapˢ (credVoter DRep) (dom dReps) + ∪ fromList (noConfidenceRep ∷ abstainRep ∷ []) ) in ∙ filter isKeyHash wdrlCreds ⊆ dom voteDelegs ∙ mapˢ (map₁ stake) (wdrls ˢ) ⊆ rewards ˢ diff --git a/src/Ledger/Certs/Properties.agda b/src/Ledger/Certs/Properties.agda index d15a00351..c38d1fb61 100644 --- a/src/Ledger/Certs/Properties.agda +++ b/src/Ledger/Certs/Properties.agda @@ -145,7 +145,6 @@ Computational-CERTS = it private variable dCert : DCert - Γ : CertEnv l : List DCert A A' B : Type instance @@ -158,7 +157,8 @@ getCoin-singleton = indexedSum-singleton' {M = Coin} (finiteness _) → a ∈ dom m → getCoin (m ∪ˡ ❴ (a , c) ❵ᵐ) ≡ getCoin m ∪ˡsingleton∈dom m {(a , c)} a∈dom = ≡ᵉ-getCoin (m ∪ˡ ❴ (a , c) ❵) m (singleton-∈-∪ˡ {m = m} a∈dom) -module _ ( indexedSumᵛ'-∪ : {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ Coin) +module _ {Γ : CertEnv} + ( indexedSumᵛ'-∪ : {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ Coin) → disjoint (dom m) (dom m') → getCoin (m ∪ˡ m') ≡ getCoin m + getCoin m' ) where @@ -281,11 +281,16 @@ module _ ( indexedSumᵛ'-∪ : {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ C getCoin (zeroMap ∪ˡ rewards) + getCoin wdrls ∎ - CERTS-pov : {stᵈ stᵈ' : DState} {stᵖ stᵖ' : PState} {stᵍ stᵍ' : GState} - → Γ ⊢ ⟦ stᵈ , stᵖ , stᵍ ⟧ᶜˢ ⇀⦇ l ,CERTS⦈ ⟦ stᵈ' , stᵖ' , stᵍ' ⟧ᶜˢ - → getCoin ⟦ stᵈ , stᵖ , stᵍ ⟧ᶜˢ ≡ getCoin ⟦ stᵈ' , stᵖ' , stᵍ' ⟧ᶜˢ + getCoin (CertEnv.wdrls Γ) - CERTS-pov (BS-base x) = CERTBASE-pov x - CERTS-pov (BS-ind x xs) = trans (CERT-pov x) (CERTS-pov xs) + sts-pov : {s₁ sₙ : CertState} → ReflexiveTransitiveClosure {sts = _⊢_⇀⦇_,CERT⦈_} Γ s₁ l sₙ + → getCoin s₁ ≡ getCoin sₙ + sts-pov (BS-base Id-nop) = refl + sts-pov (BS-ind x xs) = trans (CERT-pov x) (sts-pov xs) + + CERTS-pov : {s₁ sₙ : CertState} → Γ ⊢ s₁ ⇀⦇ l ,CERTS⦈ sₙ → getCoin s₁ ≡ getCoin sₙ + getCoin (CertEnv.wdrls Γ) + CERTS-pov (RTC {s' = s'} {s'' = sₙ} (bsts , BS-base Id-nop)) = CERTBASE-pov bsts + CERTS-pov (RTC (bsts , BS-ind x sts)) = trans (CERTBASE-pov bsts) + (cong (_+ getCoin (CertEnv.wdrls Γ)) + (trans (CERT-pov x) (sts-pov sts))) -- TODO: Prove the following property. -- range vDelegs ⊆ map (credVoter DRep) (dom DReps) diff --git a/src/Ledger/Conway/Conformance/Certs.agda b/src/Ledger/Conway/Conformance/Certs.agda index 38d502316..64f940086 100644 --- a/src/Ledger/Conway/Conformance/Certs.agda +++ b/src/Ledger/Conway/Conformance/Certs.agda @@ -200,4 +200,4 @@ data _⊢_⇀⦇_,CERTBASE⦈_ : CertEnv → CertState → ⊤ → CertState → ⟧ᶜˢ _⊢_⇀⦇_,CERTS⦈_ : CertEnv → CertState → List DCert → CertState → Type -_⊢_⇀⦇_,CERTS⦈_ = ReflexiveTransitiveClosureᵇ _⊢_⇀⦇_,CERTBASE⦈_ _⊢_⇀⦇_,CERT⦈_ +_⊢_⇀⦇_,CERTS⦈_ = ReflexiveTransitiveClosureᵇ' {_⊢_⇀⟦_⟧ᵇ_ = _⊢_⇀⦇_,CERTBASE⦈_}{_⊢_⇀⦇_,CERT⦈_} diff --git a/src/Ledger/Conway/Conformance/Gov.agda b/src/Ledger/Conway/Conformance/Gov.agda index 93fc0994c..4a10bfd27 100644 --- a/src/Ledger/Conway/Conformance/Gov.agda +++ b/src/Ledger/Conway/Conformance/Gov.agda @@ -268,4 +268,4 @@ data _⊢_⇀⦇_,GOV'⦈_ where ─────────────────────────────────────── (Γ , k) ⊢ s ⇀⦇ inj₂ prop ,GOV'⦈ s' -_⊢_⇀⦇_,GOV⦈_ = ReflexiveTransitiveClosureᵢ _⊢_⇀⦇_,GOV'⦈_ +_⊢_⇀⦇_,GOV⦈_ = ReflexiveTransitiveClosureᵢ {sts = _⊢_⇀⦇_,GOV'⦈_} diff --git a/src/Ledger/Conway/Conformance/Ledger.agda b/src/Ledger/Conway/Conformance/Ledger.agda index f7ccdd78c..f2a9f3e47 100644 --- a/src/Ledger/Conway/Conformance/Ledger.agda +++ b/src/Ledger/Conway/Conformance/Ledger.agda @@ -90,4 +90,4 @@ pattern LEDGER-V⋯ w x y z = LEDGER-V (w , x , y , z) pattern LEDGER-I⋯ y z = LEDGER-I (y , z) _⊢_⇀⦇_,LEDGERS⦈_ : LEnv → LState → List Tx → LState → Type -_⊢_⇀⦇_,LEDGERS⦈_ = ReflexiveTransitiveClosure _⊢_⇀⦇_,LEDGER⦈_ +_⊢_⇀⦇_,LEDGERS⦈_ = ReflexiveTransitiveClosure {sts = _⊢_⇀⦇_,LEDGER⦈_} diff --git a/src/Ledger/Gov.lagda b/src/Ledger/Gov.lagda index 232f69a43..f3fb5802d 100644 --- a/src/Ledger/Gov.lagda +++ b/src/Ledger/Gov.lagda @@ -354,7 +354,7 @@ data _⊢_⇀⦇_,GOV'⦈_ where ─────────────────────────────────────── (Γ , k) ⊢ s ⇀⦇ inj₂ prop ,GOV'⦈ s' -_⊢_⇀⦇_,GOV⦈_ = ReflexiveTransitiveClosureᵢ _⊢_⇀⦇_,GOV'⦈_ +_⊢_⇀⦇_,GOV⦈_ = ReflexiveTransitiveClosureᵢ {sts = _⊢_⇀⦇_,GOV'⦈_} \end{code} \caption{Rules for the GOV transition system} \label{defs:gov-rules} diff --git a/src/Ledger/Ledger.lagda b/src/Ledger/Ledger.lagda index 886a9ddf0..fec1e45a2 100644 --- a/src/Ledger/Ledger.lagda +++ b/src/Ledger/Ledger.lagda @@ -137,7 +137,7 @@ pattern LEDGER-I⋯ y z = LEDGER-I (y , z) \begin{figure*}[h] \begin{code} _⊢_⇀⦇_,LEDGERS⦈_ : LEnv → LState → List Tx → LState → Type -_⊢_⇀⦇_,LEDGERS⦈_ = ReflexiveTransitiveClosure _⊢_⇀⦇_,LEDGER⦈_ +_⊢_⇀⦇_,LEDGERS⦈_ = ReflexiveTransitiveClosure {sts = _⊢_⇀⦇_,LEDGER⦈_} \end{code} \caption{LEDGERS transition system} \end{figure*} diff --git a/src/Ledger/Ledger/Properties.agda b/src/Ledger/Ledger/Properties.agda index a8d707207..afeaeb49a 100644 --- a/src/Ledger/Ledger/Properties.agda +++ b/src/Ledger/Ledger/Properties.agda @@ -237,7 +237,7 @@ module LEDGER-PROPS (tx : Tx) (Γ : LEnv) (s : LState) where STS→GovSt≡ (LEDGER-V x) refl = STS→updateGovSt≡ (txgov txb) 0 (proj₂ (proj₂ (proj₂ x))) where STS→updateGovSt≡ : (vps : List (GovVote ⊎ GovProposal)) (k : ℕ) {certSt : CertState} {govSt govSt' : GovState} - → (_⊢_⇀⟦_⟧ᵢ*'_ IdSTS _⊢_⇀⦇_,GOV'⦈_ (⟦ txid , epoch slot , pp , ppolicy , enactState , certSt ⟧ᵍ , k) govSt vps govSt') + → (_⊢_⇀⟦_⟧ᵢ*'_ {_⊢_⇀⟦_⟧ᵇ_ = IdSTS}{_⊢_⇀⦇_,GOV'⦈_} (⟦ txid , epoch slot , pp , ppolicy , enactState , certSt ⟧ᵍ , k) govSt vps govSt') → govSt' ≡ updateGovStates vps k govSt STS→updateGovSt≡ [] _ (BS-base Id-nop) = refl STS→updateGovSt≡ (inj₁ v ∷ vps) k (BS-ind (GOV-Vote x) h) diff --git a/src/Ledger/Ratify.lagda b/src/Ledger/Ratify.lagda index 875afec90..d260d6e3d 100644 --- a/src/Ledger/Ratify.lagda +++ b/src/Ledger/Ratify.lagda @@ -578,7 +578,7 @@ data _⊢_⇀⦇_,RATIFY'⦈_ : RatifyEnv → RatifyState → GovActionID × Gov _⊢_⇀⦇_,RATIFY⦈_ : RatifyEnv → RatifyState → List (GovActionID × GovActionState) → RatifyState → Type -_⊢_⇀⦇_,RATIFY⦈_ = ReflexiveTransitiveClosure _⊢_⇀⦇_,RATIFY'⦈_ +_⊢_⇀⦇_,RATIFY⦈_ = ReflexiveTransitiveClosure {sts = _⊢_⇀⦇_,RATIFY'⦈_} \end{code} \end{AgdaSuppressSpace} \caption{The RATIFY transition system}