diff --git a/docs/agda-spec/src/Axiom/Set.agda b/docs/agda-spec/src/Axiom/Set.agda index 0342cf8936..83486f9b82 100644 --- a/docs/agda-spec/src/Axiom/Set.agda +++ b/docs/agda-spec/src/Axiom/Set.agda @@ -97,6 +97,9 @@ record Theory {ℓ} : Type (sucˡ ℓ) where finite : Set A → Type ℓ finite X = ∃[ l ] ∀ {a} → a ∈ X ⇔ a ∈ˡ l + Show-finite : ⦃ Show A ⦄ → Show (Σ (Set A) finite) + Show.show Show-finite (X , (l , _)) = Show-List .show l + weakly-finite : Set A → Type ℓ weakly-finite X = ∃[ l ] ∀ {a} → a ∈ X → a ∈ˡ l @@ -291,6 +294,11 @@ record Theoryᶠ : Type₁ where lengthˢ : ⦃ DecEq A ⦄ → Set A → ℕ lengthˢ X = card (X , DecEq⇒strongly-finite X) + module _ {A : Type} ⦃ _ : Show A ⦄ where + instance + Show-Set : Show (Set A) + Show-Set .show = λ x → Show-finite .show (x , (finiteness x)) + -- set theories with an infinite set (containing all natural numbers) record Theoryⁱ : Type₁ where field theory : Theory @@ -307,30 +315,32 @@ record Theoryᵈ : Type₁ where field ∈-sp : ⦃ DecEq A ⦄ → spec-∈ A _∈?_ : ⦃ DecEq A ⦄ → Decidable² (_∈_ {A = A}) - all? : ⦃ DecEq A ⦄ → {P : A → Type} (P? : Decidable¹ P) {X : Set A} → Dec (All P X) - any? : ⦃ DecEq A ⦄ → {P : A → Type} (P? : Decidable¹ P) (X : Set A) → Dec (Any P X) - - module _ {A : Type} ⦃ _ : DecEq A ⦄ where + all? : {P : A → Type} (P? : Decidable¹ P) {X : Set A} → Dec (All P X) + any? : {P : A → Type} (P? : Decidable¹ P) (X : Set A) → Dec (Any P X) - _∈ᵇ_ : A → Set A → Bool - a ∈ᵇ X = ⌊ a ∈? X ⌋ - - instance - Dec-∈ : _∈_ {A = A} ⁇² - Dec-∈ = ⁇² _∈?_ - module _ {P : A → Type} ⦃ _ : P ⁇¹ ⦄ where instance + module _ {A : Type} {P : A → Type} where + module _ ⦃ _ : P ⁇¹ ⦄ where instance Dec-Allˢ : All P ⁇¹ Dec-Allˢ = ⁇¹ λ x → all? dec¹ {x} Dec-Anyˢ : Any P ⁇¹ Dec-Anyˢ = ⁇¹ any? dec¹ - module _ {P : A → Type} (P? : Decidable¹ P) where + module _ (P? : Decidable¹ P) where allᵇ anyᵇ : (X : Set A) → Bool allᵇ X = ⌊ all? P? {X} ⌋ anyᵇ X = ⌊ any? P? X ⌋ + module _ {A : Type} ⦃ _ : DecEq A ⦄ where + + _∈ᵇ_ : A → Set A → Bool + a ∈ᵇ X = ⌊ a ∈? X ⌋ + + instance + Dec-∈ : _∈_ {A = A} ⁇² + Dec-∈ = ⁇² _∈?_ + _ = _∈_ {A = A} ⁇² ∋ it _ = _⊆_ {A = A} ⁇² ∋ it _ = _≡ᵉ_ {A = A} ⁇² ∋ it diff --git a/docs/agda-spec/src/Axiom/Set/Map.agda b/docs/agda-spec/src/Axiom/Set/Map.agda index fb46f2b244..3d12497c22 100644 --- a/docs/agda-spec/src/Axiom/Set/Map.agda +++ b/docs/agda-spec/src/Axiom/Set/Map.agda @@ -289,6 +289,9 @@ mapPartial-uniq {f = f} prop {a} {b} {b'} p q = mapMaybeWithKeyᵐ : (A → B → Maybe B') → Map A B → Map A B' mapMaybeWithKeyᵐ f (rel , prop) = mapMaybeWithKey f rel , mapPartial-uniq {f = f} prop +mapFromPartialFun : (A → Maybe B) → Set A → Map A B +mapFromPartialFun f s = mapMaybeWithKeyᵐ (λ _ → f) (idMap s) + module Restrictionᵐ (sp-∈ : spec-∈ A) where private module R = Restriction sp-∈ open Unionᵐ sp-∈ diff --git a/docs/agda-spec/src/Interface/ComputationalRelation.agda b/docs/agda-spec/src/Interface/ComputationalRelation.agda index ac1c6fef4f..879995ded2 100644 --- a/docs/agda-spec/src/Interface/ComputationalRelation.agda +++ b/docs/agda-spec/src/Interface/ComputationalRelation.agda @@ -161,13 +161,14 @@ module _ {STS : C → S → Sig → S → Type} (comp comp' : Computational STS compute-ext≡ = ExtendedRel-rightUnique comp (ExtendedRel-compute comp) (ExtendedRel-compute comp') -Computational⇒Dec' : - ⦃ _ : DecEq S ⦄ {STS : C → S → Sig → S → Type} ⦃ comp : Computational STS Err ⦄ - → Dec (STS c s sig s') -Computational⇒Dec' ⦃ comp = comp ⦄ = Computational⇒Dec comp - open Computational ⦃...⦄ +Computational⇒Dec' : + {STS : C → S → Sig → S → Type} ⦃ comp : Computational STS Err ⦄ → Dec (∃[ s' ] STS c s sig s') +Computational⇒Dec' with computeProof _ _ _ in eq +... | success x = yes x +... | failure x = no λ (_ , h) → failure⇒∀¬STS (-, cong (map proj₁) eq) _ h + record InjectError Err₁ Err₂ : Type where field injectError : Err₁ → Err₂ diff --git a/docs/agda-spec/src/Interface/HasAdd/Instance.agda b/docs/agda-spec/src/Interface/HasAdd/Instance.agda index 79327d8f9e..10fcd6cfe0 100644 --- a/docs/agda-spec/src/Interface/HasAdd/Instance.agda +++ b/docs/agda-spec/src/Interface/HasAdd/Instance.agda @@ -4,6 +4,7 @@ module Interface.HasAdd.Instance where open import Interface.HasAdd open import Data.Integer as ℤ using (ℤ) open import Data.Nat as ℕ using (ℕ) +open import Data.String as Str instance addInt : HasAdd ℤ @@ -11,3 +12,6 @@ instance addNat : HasAdd ℕ addNat ._+_ = ℕ._+_ + + addString : HasAdd String + addString ._+_ = Str._++_ diff --git a/docs/agda-spec/src/Interface/HasOrder.agda b/docs/agda-spec/src/Interface/HasOrder.agda index ec7b562578..da89ef0f0e 100644 --- a/docs/agda-spec/src/Interface/HasOrder.agda +++ b/docs/agda-spec/src/Interface/HasOrder.agda @@ -64,7 +64,7 @@ module _ {a} {A : Set a} where <-asymmetric : Asymmetric _<_ <-asymmetric = ≤-antisym⇒<-asym ≤-antisym - open IsEquivalence ≈-isEquivalence renaming (sym to ≈-sym) + open IsEquivalence ≈-isEquivalence using () renaming (sym to ≈-sym) public <-trans : Transitive _<_ <-trans i⊎≈ x⊎≈ x⊎≈ x 0 +paramsWF-elim pp pwf (suc n) x = z0 : (pp : PParams) → paramsWellFormed pp → (PParams.refScriptCostStride pp) > 0 +refScriptCostStride>0 pp pwf = paramsWF-elim pp pwf (PParams.refScriptCostStride pp) (there (there (there (there (here refl))))) +\end{code} +\end{AgdaMultiCode} +\caption{Protocol parameter well-formedness} +\label{fig:protocol-parameter-well-formedness} +\end{figure*} +\begin{code}[hide] instance + Show-ℚ = Show _ ∋ record {M} + where import Data.Rational.Show as M unquoteDecl DecEq-DrepThresholds = derive-DecEq ((quote DrepThresholds , DecEq-DrepThresholds) ∷ []) unquoteDecl DecEq-PoolThresholds = derive-DecEq @@ -141,6 +194,12 @@ instance ((quote PParams , DecEq-PParams) ∷ []) unquoteDecl DecEq-PParamGroup = derive-DecEq ((quote PParamGroup , DecEq-PParamGroup) ∷ []) + unquoteDecl Show-DrepThresholds = derive-Show + ((quote DrepThresholds , Show-DrepThresholds) ∷ []) + unquoteDecl Show-PoolThresholds = derive-Show + ((quote PoolThresholds , Show-PoolThresholds) ∷ []) + unquoteDecl Show-PParams = derive-Show + ((quote PParams , Show-PParams) ∷ []) module PParamsUpdate where record PParamsUpdate : Type where @@ -154,8 +213,12 @@ module PParamsUpdate where keyDeposit : Maybe Coin poolDeposit : Maybe Coin coinsPerUTxOByte : Maybe Coin - minFeeRefScriptCoinsPerByte : Maybe ℚ prices : Maybe Prices + minFeeRefScriptCoinsPerByte : Maybe ℚ + maxRefScriptSizePerTx : Maybe ℕ + maxRefScriptSizePerBlock : Maybe ℕ + refScriptCostStride : Maybe ℕ + refScriptCostMultiplier : Maybe ℚ minUTxOValue : Maybe Coin -- retired, keep for now a0 : Maybe ℚ Emax : Maybe Epoch @@ -172,7 +235,7 @@ module PParamsUpdate where paramsUpdateWellFormed : PParamsUpdate → Type paramsUpdateWellFormed ppu = just 0 ∉ fromList ( maxBlockSize ∷ maxTxSize ∷ maxHeaderSize ∷ maxValSize - ∷ minUTxOValue ∷ poolDeposit ∷ collateralPercentage ∷ ccMaxTermLength + ∷ coinsPerUTxOByte ∷ poolDeposit ∷ collateralPercentage ∷ ccMaxTermLength ∷ govActionLifetime ∷ govActionDeposit ∷ drepDeposit ∷ [] ) where open PParamsUpdate ppu @@ -201,6 +264,10 @@ module PParamsUpdate where ∷ is-just poolDeposit ∷ is-just coinsPerUTxOByte ∷ is-just minFeeRefScriptCoinsPerByte + ∷ is-just maxRefScriptSizePerTx + ∷ is-just maxRefScriptSizePerBlock + ∷ is-just refScriptCostStride + ∷ is-just refScriptCostMultiplier ∷ is-just prices ∷ is-just minUTxOValue ∷ []) @@ -271,6 +338,10 @@ module PParamsUpdate where ; poolDeposit = U.poolDeposit ?↗ P.poolDeposit ; coinsPerUTxOByte = U.coinsPerUTxOByte ?↗ P.coinsPerUTxOByte ; minFeeRefScriptCoinsPerByte = U.minFeeRefScriptCoinsPerByte ?↗ P.minFeeRefScriptCoinsPerByte + ; maxRefScriptSizePerTx = U.maxRefScriptSizePerTx ?↗ P.maxRefScriptSizePerTx + ; maxRefScriptSizePerBlock = U.maxRefScriptSizePerBlock ?↗ P.maxRefScriptSizePerBlock + ; refScriptCostStride = U.refScriptCostStride ?↗ P.refScriptCostStride + ; refScriptCostMultiplier = U.refScriptCostMultiplier ?↗ P.refScriptCostMultiplier ; prices = U.prices ?↗ P.prices ; minUTxOValue = U.minUTxOValue ?↗ P.minUTxOValue ; a0 = U.a0 ?↗ P.a0 @@ -294,12 +365,7 @@ module PParamsUpdate where instance unquoteDecl DecEq-PParamsUpdate = derive-DecEq ((quote PParamsUpdate , DecEq-PParamsUpdate) ∷ []) - \end{code} -\end{AgdaMultiCode} -\caption{Protocol parameter declarations} -\label{fig:protocol-parameter-declarations} -\end{figure*} % Retiring ProtVer's documentation since ProtVer is retired. % \ProtVer represents the protocol version used in the Cardano ledger. % It is a pair of natural numbers, representing the major and minor version, @@ -365,7 +431,7 @@ can be applied and it has a set of groups associated with it. An update is well formed if it has at least one group (i.e. if it updates something) and if it preserves well-formedness. -\begin{figure*}[h!] +\begin{figure*}[ht] \begin{AgdaMultiCode} \begin{code}[hide] record PParamsDiff : Type₁ where @@ -399,4 +465,5 @@ record GovParams : Type₁ where field ppHashingScheme : isHashableSet PParams open isHashableSet ppHashingScheme renaming (THash to PPHash) public field ⦃ DecEq-UpdT ⦄ : DecEq PParamsUpdate +-- ⦃ Show-UpdT ⦄ : Show PParamsUpdate \end{code} diff --git a/docs/agda-spec/src/Ledger/Script.lagda b/docs/agda-spec/src/Ledger/Script.lagda index 7d29da9f3a..b82be2f127 100644 --- a/docs/agda-spec/src/Ledger/Script.lagda +++ b/docs/agda-spec/src/Ledger/Script.lagda @@ -32,17 +32,19 @@ record P1ScriptStructure : Type₁ where record PlutusStructure : Type₁ where field Dataʰ : HashableSet Language PlutusScript CostModel Prices LangDepView ExUnits : Type + PlutusV1 PlutusV2 PlutusV3 : Language ⦃ ExUnit-CommutativeMonoid ⦄ : IsCommutativeMonoid' 0ℓ 0ℓ ExUnits ⦃ Hashable-PlutusScript ⦄ : Hashable PlutusScript ScriptHash + ⦃ DecEq-Language ⦄ : DecEq Language ⦃ DecEq-CostModel ⦄ : DecEq CostModel ⦃ DecEq-LangDepView ⦄ : DecEq LangDepView + ⦃ Show-CostModel ⦄ : Show CostModel field _≥ᵉ_ : ExUnits → ExUnits → Type ⦃ DecEq-ExUnits ⦄ : DecEq ExUnits ⦃ DecEQ-Prices ⦄ : DecEq Prices - -- GetPair : ExUnits → Type × Type - -- coinIsMonoidMorphism : GetPair Is ExUnit-CommutativeMonoid - -- -CommutativeMonoid⟶ +-0-commutativeMonoid + ⦃ Show-ExUnits ⦄ : Show ExUnits + ⦃ Show-Prices ⦄ : Show Prices open HashableSet Dataʰ renaming (T to Data; THash to DataHash) public diff --git a/docs/agda-spec/src/Ledger/Set/Theory.agda b/docs/agda-spec/src/Ledger/Set/Theory.agda index 7b6992843d..ca65a1f6c5 100644 --- a/docs/agda-spec/src/Ledger/Set/Theory.agda +++ b/docs/agda-spec/src/Ledger/Set/Theory.agda @@ -54,8 +54,13 @@ opaque DecEq-ℙ : ⦃ _ : DecEq A ⦄ → DecEq (ℙ A) DecEq-ℙ = L.Decˡ.DecEq-Set -open import Axiom.Set.Rel th public - hiding (_∣'_; _∣^'_; dom; range) + Show-ℙ : ⦃ _ : Show A ⦄ → Show (ℙ A) + Show-ℙ .show = λ x → Show-finite .show (x , (finiteness x)) + +import Axiom.Set.Rel +module Rel = Axiom.Set.Rel th + +open Rel public hiding (_∣'_; _∣^'_; dom; range) open import Axiom.Set.Map th public renaming ( Map to infixr 1 _⇀_ @@ -76,7 +81,7 @@ module _ ⦃ _ : DecEq A ⦄ where renaming (_∣_ to _∣ʳ_; _∣_ᶜ to _∣ʳ_ᶜ) open Corestriction {A} ∈-sp public - hiding (_∣^_; _∣^_ᶜ) public + renaming (_∣^_ to _∣^ʳ_; _∣^_ᶜ to _∣^ʳ_ᶜ) public open Restrictionᵐ {A} ∈-sp public open Corestrictionᵐ {A} ∈-sp public @@ -132,3 +137,7 @@ opaque singleton-≢-∅ : ∀ {a} {x : a} → ⦃ DecEq a ⦄ → singleton x ≢ ∅ singleton-≢-∅ {x = x} () + +aggregateBy : ⦃ DecEq A ⦄ → ⦃ DecEq B ⦄ → ⦃ DecEq C ⦄ → ⦃ IsCommutativeMonoid' 0ℓ 0ℓ C ⦄ + → Rel A B → A ⇀ C → B ⇀ C +aggregateBy R m = mapFromFun (λ b → ∑[ x ← m ∣ Rel.dom (R ∣^ʳ ❴ b ❵) ] x) (Rel.range R) diff --git a/docs/agda-spec/src/Ledger/Types/Epoch.agda b/docs/agda-spec/src/Ledger/Types/Epoch.agda index 2765f173b1..a306e1c1ce 100644 --- a/docs/agda-spec/src/Ledger/Types/Epoch.agda +++ b/docs/agda-spec/src/Ledger/Types/Epoch.agda @@ -11,14 +11,18 @@ open import Data.Nat.Properties using (+-*-semiring) open import Data.Rational using (ℚ) open import Data.Rational.Ext using (PosUnitInterval) +additionVia : ∀{A : Set} → (A → A) → ℕ → A → A +additionVia sucFun zero r = r +additionVia sucFun (suc l) r = sucFun (additionVia sucFun l r) + record EpochStructure : Type₁ where field Slotʳ : Semiring 0ℓ 0ℓ - Epoch : Type; ⦃ DecEq-Epoch ⦄ : DecEq Epoch - KESPeriod : Type; ⦃ DecEq-KESPeriod ⦄ : DecEq KESPeriod; ⦃ HasPreorder-KESPeriod ⦄ : HasPreorder≡ {A = KESPeriod} + Epoch : Type; ⦃ DecEq-Epoch ⦄ : DecEq Epoch; ⦃ Show-Epoch ⦄ : Show Epoch + KESPeriod : Type; ⦃ DecEq-KESPeriod ⦄ : DecEq KESPeriod; ⦃ DecTo-KESPeriod ⦄ : HasDecTotalOrder≡ {A = KESPeriod} Slot = Semiring.Carrier Slotʳ - field ⦃ DecPo-Slot ⦄ : HasDecPartialOrder≡ {A = Slot} + field ⦃ DecTo-Slot ⦄ : HasDecTotalOrder≡ {A = Slot} ⦃ DecEq-Slot ⦄ : DecEq Slot epoch : Slot → Epoch @@ -34,6 +38,12 @@ record EpochStructure : Type₁ where ActiveSlotCoeff : PosUnitInterval MaxMajorPV : ℕ + _+ᵉ_ = additionVia sucᵉ + + field + _+ᵉ'_ : ℕ → Epoch → Epoch + +ᵉ≡+ᵉ' : ∀ {a b} → a +ᵉ b ≡ a +ᵉ' b + -- preorders and partial orders instance @@ -59,10 +69,6 @@ record EpochStructure : Type₁ where ℕtoEpoch zero = epoch 0# ℕtoEpoch (suc n) = sucᵉ (ℕtoEpoch n) - _+ᵉ_ : ℕ → Epoch → Epoch - zero +ᵉ e = e - suc n +ᵉ e = sucᵉ (n +ᵉ e) - instance addSlot : HasAdd Slot addSlot ._+_ = _+ˢ_ @@ -75,7 +81,7 @@ record EpochStructure : Type₁ where Number-Epoch .Number.fromNat x = ℕtoEpoch x record GlobalConstants : Type₁ where - field Network : Type; ⦃ DecEq-Netw ⦄ : DecEq Network + field Network : Type; ⦃ DecEq-Netw ⦄ : DecEq Network; ⦃ Show-Network ⦄ : Show Network SlotsPerEpochᶜ : ℕ; ⦃ NonZero-SlotsPerEpochᶜ ⦄ : NonZero SlotsPerEpochᶜ StabilityWindowᶜ : ℕ RandomnessStabilisationWindowᶜ : ℕ @@ -86,6 +92,10 @@ record GlobalConstants : Type₁ where ActiveSlotCoeffᶜ : PosUnitInterval MaxMajorPVᶜ : ℕ + ℕ+ᵉ≡+ᵉ' : ∀ {a b} → additionVia suc a b ≡ a + b + ℕ+ᵉ≡+ᵉ' {zero} {b} = refl + ℕ+ᵉ≡+ᵉ' {suc a} {b} = cong suc (ℕ+ᵉ≡+ᵉ' {a} {b}) + ℕEpochStructure : EpochStructure ℕEpochStructure = λ where .Slotʳ → +-*-semiring @@ -96,12 +106,14 @@ record GlobalConstants : Type₁ where .StabilityWindow → StabilityWindowᶜ .RandomnessStabilisationWindow → RandomnessStabilisationWindowᶜ .sucᵉ → suc + ._+ᵉ'_ → _+_ .kesPeriod slot → slot / SlotsPerKESPeriodᶜ ._+ᵏ_ → _+_ ._-ᵏ_ → _-_ .MaxKESEvo → MaxKESEvoᶜ .ActiveSlotCoeff → ActiveSlotCoeffᶜ .MaxMajorPV → MaxMajorPVᶜ + .+ᵉ≡+ᵉ' {a} {b} → ℕ+ᵉ≡+ᵉ' {a} {b} where open EpochStructure diff --git a/docs/agda-spec/src/Makefile b/docs/agda-spec/src/Makefile index d1fc7287b7..2de9935429 100644 --- a/docs/agda-spec/src/Makefile +++ b/docs/agda-spec/src/Makefile @@ -39,3 +39,7 @@ clean: $(LATEX_DIR)/$(PDF_NAME).*\ $(LATEX_DIR)/*.aux\ $(OUT_DIR)/ + +wipe: clean + rm -rf $(LATEX_DIR)/Spec\ + $(OUT_DIR)/ diff --git a/docs/agda-spec/src/Spec/BlockDefinitions.lagda b/docs/agda-spec/src/Spec/BlockDefinitions.lagda index 4acbc13d27..0a728a4830 100644 --- a/docs/agda-spec/src/Spec/BlockDefinitions.lagda +++ b/docs/agda-spec/src/Spec/BlockDefinitions.lagda @@ -31,6 +31,9 @@ record BlockStructure : Type₁ where HashBBody : Type -- hash of a block body VRFRes : Type -- VRF result value \end{code} +\begin{code}[hide] + ⦃ DecEq-HashHeader ⦄ : DecEq HashHeader +\end{code} \emph{Concrete types} \begin{code} BlockNo = ℕ -- block number diff --git a/docs/agda-spec/src/Spec/ChainHead/Properties.agda b/docs/agda-spec/src/Spec/ChainHead/Properties.agda new file mode 100644 index 0000000000..af6b1d58cb --- /dev/null +++ b/docs/agda-spec/src/Spec/ChainHead/Properties.agda @@ -0,0 +1,111 @@ +{-# OPTIONS --safe #-} + +open import InterfaceLibrary.Ledger +open import Spec.BaseTypes using (Nonces) +open import Spec.BlockDefinitions +open import Ledger.Crypto +open import Ledger.Script +open import Ledger.Types.Epoch +open import Data.Rational.Ext + +module Spec.ChainHead.Properties + (crypto : _) (open Crypto crypto) + (nonces : Nonces crypto) (open Nonces nonces) + (es : _) (open EpochStructure es) + (ss : ScriptStructure crypto es) (open ScriptStructure ss) + (bs : BlockStructure crypto nonces es ss) (open BlockStructure bs) + (af : _) (open AbstractFunctions af) + (li : LedgerInterface crypto es ss) (let open LedgerInterface li) + (rs : _) (open RationalExtStructure rs) + where + +open import Tactic.GenError +open import Ledger.Prelude +open import Ledger.PParams crypto es ss using (PParams; ProtVer) +open import Spec.TickForecast crypto es ss li +open import Spec.TickForecast.Properties crypto es ss li +open import Spec.TickNonce crypto es nonces +open import Spec.TickNonce.Properties crypto es nonces +open import Spec.Protocol crypto nonces es ss bs af rs +open import Spec.Protocol.Properties crypto nonces es ss bs af rs +open import Spec.ChainHead crypto nonces es ss bs af li rs + +instance + + prtlSeqChecks⁇ : prtlSeqChecks ⁇² + prtlSeqChecks⁇ {nothing} {_} .dec = yes tt + prtlSeqChecks⁇ {lab@(just ⟦ bℓ , sℓ , _ ⟧ℓ)} {bh} .dec = + sℓ computeProof) ≡ success s′ + completeness ⟦ cs′ , η₀′ , ηv′ , ηc′ , ηh′ , lab′ ⟧ᶜˢ (Chain-Head (psc , tickfStep , cc , ticknStep , prtclStep)) + with ¿ prtlSeqChecks ¿² lab bh + ... | no ¬psc = contradiction psc ¬psc + ... | yes _ + with computeTICKF _ nes slot | complete _ nes _ _ tickfStep + ... | success (forecast , _) | refl + with + (let pp = getPParams forecast; open PParams + in chainChecks? MaxMajorPV (pp .maxHeaderSize , pp .maxBlockSize , pp .pv) bh) + ... | no ¬cc = contradiction cc ¬cc + ... | yes _ + with + (let e₂ = getEpoch forecast; ne = (e₁ ≠ e₂) + in computeTICKN ticknΓ ticknSt ne) | complete ticknΓ ticknSt _ _ ticknStep + ... | success (⟦ η₀′ , _ ⟧ᵗˢ , _) | refl + with computePRTCL ⟦ getPoolDistr forecast , η₀′ ⟧ᵖᵉ prtclSt bh | complete ⟦ getPoolDistr forecast , η₀′ ⟧ᵖᵉ prtclSt _ _ prtclStep + ... | success _ | refl = refl diff --git a/docs/agda-spec/src/Spec/OperationalCertificate.lagda b/docs/agda-spec/src/Spec/OperationalCertificate.lagda index bfcca9e743..ea8f02ece7 100644 --- a/docs/agda-spec/src/Spec/OperationalCertificate.lagda +++ b/docs/agda-spec/src/Spec/OperationalCertificate.lagda @@ -112,7 +112,7 @@ data _⊢_⇀⦇_,OCERT⦈_ where in ∙ c₀ ≤ kp ∙ kp < c₀ +ᵏ MaxKESEvo - ∙ ∃[ m ] just m ≡ currentIssueNo stpools cs hk × (n ≡ m ⊎ n ≡ suc m) + ∙ ∃[ m ] (just m ≡ currentIssueNo stpools cs hk × (n ≡ m ⊎ n ≡ suc m)) ∙ isSignedˢ issuerVk (encode (vkₕ , n , c₀)) τ ∙ isSignedᵏ vkₕ t (encode bhb) σ ──────────────────────────────── diff --git a/docs/agda-spec/src/Spec/OperationalCertificate/Properties.agda b/docs/agda-spec/src/Spec/OperationalCertificate/Properties.agda new file mode 100644 index 0000000000..53cce7cd4e --- /dev/null +++ b/docs/agda-spec/src/Spec/OperationalCertificate/Properties.agda @@ -0,0 +1,55 @@ +{-# OPTIONS --safe #-} + +open import Ledger.Crypto +open import Ledger.Script +open import Ledger.Types.Epoch +open import Spec.BaseTypes using (Nonces) +open import Spec.BlockDefinitions + +module Spec.OperationalCertificate.Properties + (crypto : _) (open Crypto crypto) + (nonces : Nonces crypto) (open Nonces nonces) + (es : _) (open EpochStructure es) + (ss : ScriptStructure crypto es) (open ScriptStructure ss) + (bs : BlockStructure crypto nonces es ss) (open BlockStructure bs) + (af : _) (open AbstractFunctions af) + where + +open import Ledger.Prelude +open import Data.Maybe.Relation.Unary.Any as M +open import Spec.OperationalCertificate crypto nonces es ss bs af + +instance + + Computational-OCERT : Computational _⊢_⇀⦇_,OCERT⦈_ String + Computational-OCERT = record {Go} where + module Go (stpools : OCertEnv) (cs : OCertState) (bh : BHeader) where + bhb = bh .proj₁; open BHBody bhb + σ = bh .proj₂ + open OCert oc renaming (σ to τ) + hk = hash issuerVk + kp = kesPeriod slot + t = kp -ᵏ c₀ + + hyps = ¿ c₀ ≤ kp + × kp < c₀ +ᵏ MaxKESEvo + × M.Any (λ m → n ≡ m ⊎ n ≡ suc m) (currentIssueNo stpools cs hk) + × isSignedˢ issuerVk (encode (vkₕ , n , c₀)) τ + × isSignedᵏ vkₕ t (encode bhb) σ ¿ + + computeProof : ComputationResult String (∃[ cs′ ] stpools ⊢ cs ⇀⦇ bh ,OCERT⦈ cs′) + computeProof with hyps + ... | no ¬p = failure "Failed in OCERT" + ... | yes (p₁ , p₂ , p₃ , p₄ , p₅) = success (-, Update-OCert (p₁ , p₂ , satisfied× p₃ , p₄ , p₅)) + where + satisfied× : ∀ {a p} {A : Set a} {y : Maybe A} {P : Pred A p} → M.Any P y → ∃[ x ] just x ≡ y × P x + satisfied× (just Px) = (-, refl , Px) + + completeness : ∀ cs′ → stpools ⊢ cs ⇀⦇ bh ,OCERT⦈ cs′ → (proj₁ <$> computeProof) ≡ success cs′ + completeness _ (Update-OCert (p₁ , p₂ , (_ , p , q) , p₄ , p₅)) + with hyps + ... | yes prf rewrite dec-yes hyps prf .proj₂ = refl + ... | no ¬prf = contradiction (p₁ , p₂ , AnyP×≡→AnyP (Equivalence.to M.just-equivalence q) p , p₄ , p₅) ¬prf + where + AnyP×≡→AnyP : ∀ {a p} {A : Set a} {x : A} {y : Maybe A} {P : Pred A p} → M.Any P (just x) → just x ≡ y → M.Any P y + AnyP×≡→AnyP {P = P} prf eq = subst (M.Any P) eq prf diff --git a/docs/agda-spec/src/Spec/PDF.lagda b/docs/agda-spec/src/Spec/PDF.lagda index e124c72cef..4da375f713 100644 --- a/docs/agda-spec/src/Spec/PDF.lagda +++ b/docs/agda-spec/src/Spec/PDF.lagda @@ -110,3 +110,14 @@ module Spec.PDF where \bibliography{references} \end{document} + +\begin{code}[hide] + +import Spec.TickNonce.Properties +import Spec.UpdateNonce.Properties +import Spec.OperationalCertificate.Properties +import Spec.Protocol.Properties +import Spec.TickForecast.Properties +import Spec.ChainHead.Properties + +\end{code} diff --git a/docs/agda-spec/src/Spec/Protocol.lagda b/docs/agda-spec/src/Spec/Protocol.lagda index 71e0971d22..c145fbaf2d 100644 --- a/docs/agda-spec/src/Spec/Protocol.lagda +++ b/docs/agda-spec/src/Spec/Protocol.lagda @@ -128,7 +128,7 @@ checkLeaderVal (certℕ , certℕprf) (f , posf , f≤1) σ = \begin{code} c = ln (1ℚ ℚ.- f) in - ℚ.1/ q < exp ((ℚ.- σ) ℚ.* c) + ℚ.1/ q ℚ.< exp ((ℚ.- σ) ℚ.* c) \end{code} \end{AgdaAlign} diff --git a/docs/agda-spec/src/Spec/Protocol/Properties.agda b/docs/agda-spec/src/Spec/Protocol/Properties.agda new file mode 100644 index 0000000000..b682a7f83d --- /dev/null +++ b/docs/agda-spec/src/Spec/Protocol/Properties.agda @@ -0,0 +1,102 @@ +{-# OPTIONS --safe #-} + +open import Spec.BaseTypes using (Nonces) +open import Spec.BlockDefinitions +open import Ledger.Crypto +open import Ledger.Script +open import Ledger.Types.Epoch +open import Data.Rational.Ext + +module Spec.Protocol.Properties + (crypto : _) (open Crypto crypto) + (nonces : Nonces crypto) (open Nonces nonces) + (es : _) (open EpochStructure es) + (ss : ScriptStructure crypto es) (open ScriptStructure ss) + (bs : BlockStructure crypto nonces es ss) (open BlockStructure bs) + (af : _) (open AbstractFunctions af) + (rs : _) (open RationalExtStructure rs) + where + +open import Data.Rational as ℚ using (1ℚ) +open import Ledger.Prelude +open import Tactic.GenError +open import Spec.Protocol crypto nonces es ss bs af rs +open import Spec.BaseTypes crypto using (OCertCounters) +open import Spec.UpdateNonce crypto nonces es +open import Spec.UpdateNonce.Properties crypto nonces es +open import Spec.OperationalCertificate crypto nonces es ss bs af +open import Spec.OperationalCertificate.Properties crypto nonces es ss bs af +open import InterfaceLibrary.Common.BaseTypes crypto using (PoolDistr; lookupPoolDistr) + +private + + checkLeaderVal? : ∀ cert int σ → Dec (checkLeaderVal cert int σ) + checkLeaderVal? (certℕ , certℕprf) (f , posf , f≤1) σ + with f ≟ 1ℚ + ... | yes _ = yes _ + ... | no f≢1ℚ = + let + p = ℤ.pos certℕ ℚ./ (2 ^ 512) + q = 1ℚ ℚ.- p + p≢1ℚ = ↥p<↧p⇒p≢1 {p} (n0 = ℚ.positive (≤∧≢⇒< 1-f≥0 $ ≢-sym 1-f≢0) + c = ln (1ℚ ℚ.- f) + in + ℚ.1/ q ℚ. computeProof) ≡ success s′ + completeness _ (Evolve-Prtcl (updnStep , ocertStep , p)) + with hyps + ... | no ¬p = contradiction p ¬p + ... | yes _ + with computeUPDN updnΓ updnSt slot | complete updnΓ updnSt _ _ updnStep + ... | success _ | refl + with computeOCERT ocertΓ cs bh | complete _ _ _ _ ocertStep + ... | success _ | refl = refl diff --git a/docs/agda-spec/src/Spec/TickForecast/Properties.agda b/docs/agda-spec/src/Spec/TickForecast/Properties.agda new file mode 100644 index 0000000000..8eea212058 --- /dev/null +++ b/docs/agda-spec/src/Spec/TickForecast/Properties.agda @@ -0,0 +1,40 @@ +{-# OPTIONS --safe #-} + +open import Ledger.Crypto +open import Ledger.Script +open import Ledger.Types.Epoch +open import InterfaceLibrary.Ledger + +module Spec.TickForecast.Properties + (crypto : Crypto) + (es : _) (open EpochStructure es) + (ss : ScriptStructure crypto es) (open ScriptStructure ss) + (li : LedgerInterface crypto es ss) (let open LedgerInterface li) + where + +open import Ledger.Prelude +open import Spec.TickForecast crypto es ss li + +instance + + _ = Monad-ComputationResult + + Computational-TICKF : Computational _⊢_⇀⦇_,TICKF⦈_ String + Computational-TICKF = record {Go} where + open Computational ⦃...⦄ renaming (computeProof to comp; completeness to complete) + computeNEWEPOCH = comp {STS = _⊢_⇀⦇_,NEWEPOCH⦈_} + module Go + (Γ : ⊤) + (nes : NewEpochState) + (s : Slot) + where + + computeProof : ComputationResult String (∃[ nes′ ] Γ ⊢ nes ⇀⦇ s ,TICKF⦈ nes′) + computeProof = do + (_ , newEpochStep) ← computeNEWEPOCH Γ nes (epoch s) + success (-, Tick-Forecast newEpochStep) + + completeness : ∀ nes′ → Γ ⊢ nes ⇀⦇ s ,TICKF⦈ nes′ → (proj₁ <$> computeProof) ≡ success nes′ + completeness forecast (Tick-Forecast newEpochStep) + with computeNEWEPOCH Γ nes (epoch s) | complete Γ nes _ _ newEpochStep + ... | success _ | refl = refl diff --git a/docs/agda-spec/src/Spec/TickNonce/Properties.agda b/docs/agda-spec/src/Spec/TickNonce/Properties.agda new file mode 100644 index 0000000000..52d49cbcaf --- /dev/null +++ b/docs/agda-spec/src/Spec/TickNonce/Properties.agda @@ -0,0 +1,23 @@ +{-# OPTIONS --safe #-} + +open import Ledger.Crypto +open import Ledger.Script +open import Ledger.Types.Epoch +open import Spec.BaseTypes using (Nonces) + +module Spec.TickNonce.Properties + (crypto : _) (open Crypto crypto) + (es : _) (open EpochStructure es) + (nonces : Nonces crypto) (open Nonces nonces) + where + +open import Ledger.Prelude +open Computational ⦃...⦄ +open import Spec.TickNonce crypto es nonces + +instance + Computational-TICKN : Computational _⊢_⇀⦇_,TICKN⦈_ String + Computational-TICKN .computeProof _ _ false = success (-, Not-New-Epoch) + Computational-TICKN .computeProof _ _ true = success (-, New-Epoch) + Computational-TICKN .completeness _ _ false _ Not-New-Epoch = refl + Computational-TICKN .completeness _ _ true _ New-Epoch = refl diff --git a/docs/agda-spec/src/Spec/UpdateNonce/Properties.agda b/docs/agda-spec/src/Spec/UpdateNonce/Properties.agda new file mode 100644 index 0000000000..cd35a29155 --- /dev/null +++ b/docs/agda-spec/src/Spec/UpdateNonce/Properties.agda @@ -0,0 +1,28 @@ +{-# OPTIONS --safe #-} + +open import Ledger.Crypto +open import Ledger.Types.Epoch using (EpochStructure) +open import Spec.BaseTypes using (Nonces) + +module Spec.UpdateNonce.Properties + (crypto : _) (open Crypto crypto) + (nonces : Nonces crypto) (open Nonces nonces) + (es : _) (open EpochStructure es) + where + +open import Ledger.Prelude +open Computational ⦃...⦄ +open import Spec.UpdateNonce crypto nonces es + +instance + Computational-UPDN : Computational _⊢_⇀⦇_,UPDN⦈_ String + Computational-UPDN .computeProof _ _ s = + case ¿ s + RandomnessStabilisationWindow < firstSlot (sucᵉ (epoch s)) ¿ of λ where + (yes p) → success (-, Update-Both p) + (no ¬p) → success (-, Only-Evolve (≮⇒≥ {A = Slot} _≟_ ¬p)) + Computational-UPDN .completeness _ _ s _ (Update-Both p) + rewrite dec-yes ¿ s + RandomnessStabilisationWindow < firstSlot (sucᵉ (epoch s)) ¿ p .proj₂ = + refl + Computational-UPDN .completeness _ _ s _ (Only-Evolve p) + rewrite dec-no ¿ s + RandomnessStabilisationWindow < firstSlot (sucᵉ (epoch s)) ¿ $ ≥⇒≮ {A = Slot} p = + refl diff --git a/docs/agda-spec/src/latex/iohk.sty b/docs/agda-spec/src/latex/iohk.sty index 71a1dc5b1f..5bbb60e9b8 100644 --- a/docs/agda-spec/src/latex/iohk.sty +++ b/docs/agda-spec/src/latex/iohk.sty @@ -1,11 +1,12 @@ \NeedsTeXFormat{LaTeX2e} \ProvidesPackage{iohk}[2018/10/18] -\RequirePackage{amssymb} +% \RequirePackage{amssymb} \RequirePackage{extarrows} \RequirePackage{slashed} \RequirePackage[tikz]{bclogo} \RequirePackage{stmaryrd} +\usepackage{fontspec} \DeclareMathOperator{\dom}{dom} \DeclareMathOperator{\range}{range} @@ -33,6 +34,13 @@ \newcommand{\varUpdate}[1]{\boldsymbol{\color{Violet}#1}} +% Make the ⇀ symbol a bit larger +\usepackage{scalerel} +\usepackage{newunicodechar} +\newcommand{\largerightharpoonup}{\ensuremath{\mathrel{\scaleto{\rightharpoonup}{1.2ex}}}} + +\newunicodechar{⇀}{\largerightharpoonup} + \newenvironment{question} {\begin{bclogo}[logo=\bcquestion, couleur=orange!10, arrondi=0.2]{ QUESTION}} {\end{bclogo}}