From f3361a364e927d10f76fd79a98fab65b0f842697 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Javier=20D=C3=ADaz?= Date: Thu, 12 Dec 2024 18:56:35 +0000 Subject: [PATCH] Remove unnecessary parameters from `PParams` MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Signed-off-by: Javier Díaz --- .../src/InterfaceLibrary/Ledger.lagda | 4 +- docs/agda-spec/src/Ledger/PParams.lagda | 381 +----------------- docs/agda-spec/src/Ledger/Script.lagda | 184 --------- .../agda-spec/src/Spec/BlockDefinitions.lagda | 4 +- docs/agda-spec/src/Spec/ChainHead.lagda | 12 +- .../src/Spec/ChainHead/Properties.agda | 18 +- .../src/Spec/OperationalCertificate.lagda | 4 +- .../OperationalCertificate/Properties.agda | 6 +- docs/agda-spec/src/Spec/Protocol.lagda | 6 +- .../src/Spec/Protocol/Properties.agda | 10 +- docs/agda-spec/src/Spec/TickForecast.lagda | 4 +- .../src/Spec/TickForecast/Properties.agda | 6 +- docs/agda-spec/src/Spec/TickNonce.lagda | 1 - .../src/Spec/TickNonce/Properties.agda | 1 - 14 files changed, 42 insertions(+), 599 deletions(-) delete mode 100644 docs/agda-spec/src/Ledger/Script.lagda diff --git a/docs/agda-spec/src/InterfaceLibrary/Ledger.lagda b/docs/agda-spec/src/InterfaceLibrary/Ledger.lagda index d3cdb1b358..4b8622f60e 100644 --- a/docs/agda-spec/src/InterfaceLibrary/Ledger.lagda +++ b/docs/agda-spec/src/InterfaceLibrary/Ledger.lagda @@ -4,16 +4,14 @@ -- TODO: The following should be likely located in Common. open import Ledger.Prelude open import Ledger.Crypto -open import Ledger.Script open import Ledger.Types.Epoch module InterfaceLibrary.Ledger (crypto : Crypto) (es : _) (open EpochStructure es) - (ss : ScriptStructure crypto es) (open ScriptStructure ss) where -open import Ledger.PParams crypto es ss using (PParams) +open import Ledger.PParams using (PParams) open import InterfaceLibrary.Common.BaseTypes crypto using (PoolDistr) \end{code} diff --git a/docs/agda-spec/src/Ledger/PParams.lagda b/docs/agda-spec/src/Ledger/PParams.lagda index 0667fb3b83..39cd3acd6b 100644 --- a/docs/agda-spec/src/Ledger/PParams.lagda +++ b/docs/agda-spec/src/Ledger/PParams.lagda @@ -1,59 +1,37 @@ \section{Protocol Parameters} \label{sec:protocol-parameters} -This section defines the adjustable protocol parameters of the Cardano ledger. -These parameters are used in block validation and can affect various features of the system, -such as minimum fees, maximum and minimum sizes of certain components, and more. +This section defines the adjustable protocol parameters of the Cardano consensus. +These parameters are used in block header validation and can affect various features +of the system, such as maximum and minimum sizes of certain components, and more. \begin{code}[hide] {-# OPTIONS --safe #-} open import Data.Product.Properties open import Data.Nat.Properties using (m+1+n≢m) -open import Data.Rational using (ℚ) -open import Relation.Nullary.Decidable -open import Data.List.Relation.Unary.Any using (Any; here; there) open import Tactic.Derive.DecEq open import Tactic.Derive.Show open import Ledger.Prelude -open import Ledger.Crypto -open import Ledger.Script -open import Ledger.Types.Epoch -module Ledger.PParams - (crypto : Crypto ) - (es : _) (open EpochStructure es) - (ss : ScriptStructure crypto es) (open ScriptStructure ss) - where +module Ledger.PParams where private variable m n : ℕ \end{code} -\begin{NoConway} -The \AgdaRecord{Acnt} record has two fields, \AgdaField{treasury} and \AgdaField{reserves}, so -the \AgdaBound{acnt} field in \AgdaRecord{NewEpochState} keeps track of the total assets that -remain in treasury and reserves. - \begin{figure*}[ht] \begin{AgdaMultiCode} \begin{code} -record Acnt : Type where -\end{code} -\begin{code}[hide] - constructor ⟦_,_⟧ᵃ - field -\end{code} -\begin{code} - treasury reserves : Coin - ProtVer : Type ProtVer = ℕ × ℕ - +\end{code} +\begin{code}[hide] instance Show-ProtVer : Show ProtVer Show-ProtVer = Show-× - +\end{code} +\begin{code} data pvCanFollow : ProtVer → ProtVer → Type where canFollowMajor : pvCanFollow (m , n) (m + 1 , 0) canFollowMinor : pvCanFollow (m , n) (m , n + 1) @@ -62,34 +40,12 @@ data pvCanFollow : ProtVer → ProtVer → Type where \caption{Definitions related to protocol parameters} \label{fig:protocol-parameter-defs} \end{figure*} -\end{NoConway} \begin{figure*}[ht] \begin{AgdaMultiCode} \begin{code} data PParamGroup : Type where - NetworkGroup : PParamGroup - EconomicGroup : PParamGroup - TechnicalGroup : PParamGroup - GovernanceGroup : PParamGroup - SecurityGroup : PParamGroup - -record DrepThresholds : Type where -\end{code} -\begin{code}[hide] - field -\end{code} -\begin{code} - P1 P2a P2b P3 P4 P5a P5b P5c P5d P6 : ℚ - -record PoolThresholds : Type where -\end{code} -\begin{code}[hide] - field -\end{code} -\begin{code} - Q1 Q2a Q2b Q4 Q5e : ℚ - + NetworkGroup : PParamGroup record PParams : Type where \end{code} \begin{code}[hide] @@ -97,57 +53,9 @@ record PParams : Type where \end{code} \emph{Network group} \begin{code} - maxBlockSize : ℕ - maxTxSize : ℕ - maxHeaderSize : ℕ - maxTxExUnits : ExUnits - maxBlockExUnits : ExUnits - maxValSize : ℕ - maxCollateralInputs : ℕ -\end{code} -\begin{code}[hide] - pv : ProtVer -- retired, keep for now -\end{code} -\emph{Economic group} -\begin{code} - a : ℕ - b : ℕ - keyDeposit : Coin - poolDeposit : Coin - coinsPerUTxOByte : Coin - prices : Prices - minFeeRefScriptCoinsPerByte : ℚ - maxRefScriptSizePerTx : ℕ - maxRefScriptSizePerBlock : ℕ - refScriptCostStride : ℕ - refScriptCostMultiplier : ℚ -\end{code} -\begin{code}[hide] - minUTxOValue : Coin -- retired, keep for now -\end{code} -\emph{Technical group} -\begin{code} - Emax : Epoch - nopt : ℕ - a0 : ℚ - collateralPercentage : ℕ -\end{code} -\begin{code}[hide] - -- costmdls : Language →/⇀ CostModel (Does not work with DecEq) -\end{code} -\begin{code} - costmdls : CostModel -\end{code} -\emph{Governance group} -\begin{code} - poolThresholds : PoolThresholds - drepThresholds : DrepThresholds - ccMinSize : ℕ - ccMaxTermLength : ℕ - govActionLifetime : ℕ - govActionDeposit : Coin - drepDeposit : Coin - drepActivity : Epoch + maxHeaderSize : ℕ + maxBlockSize : ℕ + pv : ProtVer \end{code} \end{AgdaMultiCode} \caption{Protocol parameter definitions} @@ -157,9 +65,7 @@ record PParams : Type where \begin{AgdaMultiCode} \begin{code} positivePParams : PParams → List ℕ -positivePParams pp = ( maxBlockSize ∷ maxTxSize ∷ maxHeaderSize ∷ maxValSize ∷ refScriptCostStride - ∷ coinsPerUTxOByte ∷ poolDeposit ∷ collateralPercentage ∷ ccMaxTermLength - ∷ govActionLifetime ∷ govActionDeposit ∷ drepDeposit ∷ [] ) +positivePParams pp = maxHeaderSize ∷ maxBlockSize ∷ [] \end{code} \begin{code}[hide] where open PParams pp @@ -174,9 +80,6 @@ paramsWF-elim : (pp : PParams) → paramsWellFormed pp → (n : ℕ) → n ∈ˡ 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} @@ -186,229 +89,17 @@ refScriptCostStride>0 pp pwf = paramsWF-elim pp pwf (PParams.refScriptCostStride 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 - ((quote PoolThresholds , DecEq-PoolThresholds) ∷ []) unquoteDecl DecEq-PParams = derive-DecEq ((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 - field - maxBlockSize maxTxSize : Maybe ℕ - maxHeaderSize maxValSize : Maybe ℕ - maxCollateralInputs : Maybe ℕ - maxTxExUnits maxBlockExUnits : Maybe ExUnits - pv : Maybe ProtVer -- retired, keep for now - a b : Maybe ℕ - keyDeposit : Maybe Coin - poolDeposit : Maybe Coin - coinsPerUTxOByte : Maybe Coin - 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 - nopt : Maybe ℕ - collateralPercentage : Maybe ℕ - costmdls : Maybe CostModel - drepThresholds : Maybe DrepThresholds - poolThresholds : Maybe PoolThresholds - govActionLifetime : Maybe ℕ - govActionDeposit drepDeposit : Maybe Coin - drepActivity : Maybe Epoch - ccMinSize ccMaxTermLength : Maybe ℕ - - paramsUpdateWellFormed : PParamsUpdate → Type - paramsUpdateWellFormed ppu = - just 0 ∉ fromList ( maxBlockSize ∷ maxTxSize ∷ maxHeaderSize ∷ maxValSize - ∷ coinsPerUTxOByte ∷ poolDeposit ∷ collateralPercentage ∷ ccMaxTermLength - ∷ govActionLifetime ∷ govActionDeposit ∷ drepDeposit ∷ [] ) - where open PParamsUpdate ppu - - paramsUpdateWellFormed? : ( u : PParamsUpdate ) → Dec (paramsUpdateWellFormed u) - paramsUpdateWellFormed? u = ¿ paramsUpdateWellFormed u ¿ - - modifiesNetworkGroup : PParamsUpdate → Bool - modifiesNetworkGroup ppu = let open PParamsUpdate ppu in - or - ( is-just maxBlockSize - ∷ is-just maxTxSize - ∷ is-just maxHeaderSize - ∷ is-just maxValSize - ∷ is-just maxCollateralInputs - ∷ is-just maxTxExUnits - ∷ is-just maxBlockExUnits - ∷ is-just pv - ∷ []) - - modifiesEconomicGroup : PParamsUpdate → Bool - modifiesEconomicGroup ppu = let open PParamsUpdate ppu in - or - ( is-just a - ∷ is-just b - ∷ is-just keyDeposit - ∷ 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 - ∷ []) - - modifiesTechnicalGroup : PParamsUpdate → Bool - modifiesTechnicalGroup ppu = let open PParamsUpdate ppu in - or - ( is-just a0 - ∷ is-just Emax - ∷ is-just nopt - ∷ is-just collateralPercentage - ∷ is-just costmdls - ∷ []) - - modifiesGovernanceGroup : PParamsUpdate → Bool - modifiesGovernanceGroup ppu = let open PParamsUpdate ppu in - or - ( is-just drepThresholds - ∷ is-just poolThresholds - ∷ is-just govActionLifetime - ∷ is-just govActionDeposit - ∷ is-just drepDeposit - ∷ is-just drepActivity - ∷ is-just ccMinSize - ∷ is-just ccMaxTermLength - ∷ []) - - modifiedUpdateGroups : PParamsUpdate → ℙ PParamGroup - modifiedUpdateGroups ppu = - ( modifiesNetworkGroup ?═⇒ NetworkGroup - ∪ modifiesEconomicGroup ?═⇒ EconomicGroup - ∪ modifiesTechnicalGroup ?═⇒ TechnicalGroup - ∪ modifiesGovernanceGroup ?═⇒ GovernanceGroup - ) - where - _?═⇒_ : (PParamsUpdate → Bool) → PParamGroup → ℙ PParamGroup - pred ?═⇒ grp = if pred ppu then ❴ grp ❵ else ∅ - - _?↗_ : ∀ {A : Type} → Maybe A → A → A - just x ?↗ _ = x - nothing ?↗ x = x - - ≡-update : ∀ {A : Type} {u : Maybe A} {p : A} {x : A} → u ?↗ p ≡ x ⇔ (u ≡ just x ⊎ (p ≡ x × u ≡ nothing)) - ≡-update {u} {p} {x} = mk⇔ to from - where - to : ∀ {A} {u : Maybe A} {p : A} {x : A} → u ?↗ p ≡ x → (u ≡ just x ⊎ (p ≡ x × u ≡ nothing)) - to {u = just x} refl = inj₁ refl - to {u = nothing} refl = inj₂ (refl , refl) - - from : ∀ {A} {u : Maybe A} {p : A} {x : A} → u ≡ just x ⊎ (p ≡ x × u ≡ nothing) → u ?↗ p ≡ x - from (inj₁ refl) = refl - from (inj₂ (refl , refl)) = refl - - applyPParamsUpdate : PParams → PParamsUpdate → PParams - applyPParamsUpdate pp ppu = - record - { maxBlockSize = U.maxBlockSize ?↗ P.maxBlockSize - ; maxTxSize = U.maxTxSize ?↗ P.maxTxSize - ; maxHeaderSize = U.maxHeaderSize ?↗ P.maxHeaderSize - ; maxValSize = U.maxValSize ?↗ P.maxValSize - ; maxCollateralInputs = U.maxCollateralInputs ?↗ P.maxCollateralInputs - ; maxTxExUnits = U.maxTxExUnits ?↗ P.maxTxExUnits - ; maxBlockExUnits = U.maxBlockExUnits ?↗ P.maxBlockExUnits - ; pv = U.pv ?↗ P.pv - ; a = U.a ?↗ P.a - ; b = U.b ?↗ P.b - ; keyDeposit = U.keyDeposit ?↗ P.keyDeposit - ; 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 - ; Emax = U.Emax ?↗ P.Emax - ; nopt = U.nopt ?↗ P.nopt - ; collateralPercentage = U.collateralPercentage ?↗ P.collateralPercentage - ; costmdls = U.costmdls ?↗ P.costmdls - ; drepThresholds = U.drepThresholds ?↗ P.drepThresholds - ; poolThresholds = U.poolThresholds ?↗ P.poolThresholds - ; govActionLifetime = U.govActionLifetime ?↗ P.govActionLifetime - ; govActionDeposit = U.govActionDeposit ?↗ P.govActionDeposit - ; drepDeposit = U.drepDeposit ?↗ P.drepDeposit - ; drepActivity = U.drepActivity ?↗ P.drepActivity - ; ccMinSize = U.ccMinSize ?↗ P.ccMinSize - ; ccMaxTermLength = U.ccMaxTermLength ?↗ P.ccMaxTermLength - } - where - open module P = PParams pp - open module U = PParamsUpdate ppu - - instance - unquoteDecl DecEq-PParamsUpdate = derive-DecEq - ((quote PParamsUpdate , DecEq-PParamsUpdate) ∷ []) \end{code} -% 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, -% respectively. -\PParams contains parameters used in the Cardano ledger, which we group according +\PParams contains parameters used in the Cardano consensus, which we group according to the general purpose that each parameter serves. -\begin{itemize} - \item \NetworkGroup: parameters related to the network settings; - \item \EconomicGroup: parameters related to the economic aspects of the ledger; - \item \TechnicalGroup: parameters related to technical settings; - \item \GovernanceGroup: parameters related to governance settings; - \item \SecurityGroup: parameters that can impact the security of the system. -\end{itemize} - -The first four groups have the property that every protocol parameter -is associated to precisely one of these groups. The \SecurityGroup is -special: a protocol parameter may or may not be in the -\SecurityGroup. So, each protocol parameter belongs to at least one -and at most two groups. Note that in \cite{cip1694} there is no -\SecurityGroup, but there is the concept of security-relevant protocol -parameters. The difference between these notions is only social, so we -implement security-relevant protocol parameters as a group. - -The purpose of the groups is to determine voting thresholds for -proposals aiming to change parameters. The thresholds depend on the -groups of the parameters contained in such a proposal. - -These new parameters are declared in -Figure~\ref{fig:protocol-parameter-declarations} and denote the -following concepts. \begin{itemize} - \item \drepThresholds: governance thresholds for \DReps; these are rational numbers - named \Pone, \Ptwoa, \Ptwob, \Pthree, \Pfour, \Pfivea, \Pfiveb, \Pfivec, \Pfived, and \Psix; - \item \poolThresholds: pool-related governance thresholds; these are rational numbers named \Qone, \Qtwoa, \Qtwob, \Qfour and \Qfivee; - \item \ccMinSize: minimum constitutional committee size; - \item \ccMaxTermLength: maximum term limit (in epochs) of constitutional committee members; - \item \govActionLifetime: governance action expiration; - \item \govActionDeposit: governance action deposit; - \item \drepDeposit: \DRep deposit amount; - \item \drepActivity: \DRep activity period; - \item \minimumAVS: the minimum active voting threshold. + \item \NetworkGroup: parameters related to the network settings; \end{itemize} Figure~\ref{fig:protocol-parameter-declarations} also defines the @@ -425,45 +116,3 @@ instance ... | yes refl | no ¬p = yes canFollowMajor ... | yes refl | yes p = ⊥-elim $ m+1+n≢m m $ ×-≡,≡←≡ p .proj₁ \end{code} - -Finally, to update parameters we introduce an abstract type. An update -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*}[ht] -\begin{AgdaMultiCode} -\begin{code}[hide] -record PParamsDiff : Type₁ where - field -\end{code} -\emph{Abstract types \& functions} -\begin{code} - UpdateT : Type - applyUpdate : PParams → UpdateT → PParams - updateGroups : UpdateT → ℙ PParamGroup - -\end{code} -\begin{code}[hide] - ⦃ ppWF? ⦄ : ∀ {u} → (∀ pp → paramsWellFormed pp → paramsWellFormed (applyUpdate pp u)) ⁇ -\end{code} -\emph{Well-formedness condition} -\begin{code} - - ppdWellFormed : UpdateT → Type - ppdWellFormed u = updateGroups u ≢ ∅ - × ∀ pp → paramsWellFormed pp → paramsWellFormed (applyUpdate pp u) -\end{code} -\end{AgdaMultiCode} -\caption{Abstract type for parameter updates} -\label{fig:pp-update-type} -\end{figure*} -\begin{code}[hide] -record GovParams : Type₁ where - field ppUpd : PParamsDiff - open PParamsDiff ppUpd renaming (UpdateT to PParamsUpdate) public - 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 deleted file mode 100644 index b82be2f127..0000000000 --- a/docs/agda-spec/src/Ledger/Script.lagda +++ /dev/null @@ -1,184 +0,0 @@ -\section{Scripts} -\begin{code}[hide] -{-# OPTIONS --safe #-} - -open import Algebra using (CommutativeMonoid) -open import Algebra.Morphism -open import Data.List.Relation.Unary.All using (All; []; _∷_; all?; uncons) -open import Data.List.Relation.Unary.Any -open import Data.Nat.Properties using (+-0-commutativeMonoid; suc-injective) - -open import Data.List.Relation.Unary.MOf - -open import Tactic.Derive.DecEq -open import Tactic.Inline - -open import Ledger.Prelude hiding (All; Any; all?; any?; _∷ʳ_; uncons; _⊆_) -open import Ledger.Crypto -open import Ledger.Types.Epoch - -module Ledger.Script - (crypto : _) (open Crypto crypto) - (es : _) (open EpochStructure es) - where - -record P1ScriptStructure : Type₁ where - field P1Script : Type - validP1Script : ℙ KeyHashˢ → Maybe Slot × Maybe Slot → P1Script → Type - ⦃ Dec-validP1Script ⦄ : validP1Script ⁇³ - ⦃ Hashable-P1Script ⦄ : Hashable P1Script ScriptHash - ⦃ DecEq-P1Script ⦄ : DecEq P1Script - -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 - ⦃ Show-ExUnits ⦄ : Show ExUnits - ⦃ Show-Prices ⦄ : Show Prices - - open HashableSet Dataʰ renaming (T to Data; THash to DataHash) public - - -- Type aliases for Data - Datum = Data - Redeemer = Data - - field validPlutusScript : CostModel → List Data → ExUnits → PlutusScript → Type - ⦃ Dec-validPlutusScript ⦄ : ∀ {x} → (validPlutusScript x ⁇³) - language : PlutusScript → Language - toData : ∀ {A : Type} → A → Data -\end{code} -We define \Timelock scripts here. They can verify the presence of keys and whether a transaction happens in a certain slot interval. These scripts are executed as part of the regular witnessing. -\begin{figure*}[h] -\begin{code} -data Timelock : Type where - RequireAllOf : List Timelock → Timelock - RequireAnyOf : List Timelock → Timelock - RequireMOf : ℕ → List Timelock → Timelock - RequireSig : KeyHashˢ → Timelock - RequireTimeStart : Slot → Timelock - RequireTimeExpire : Slot → Timelock -\end{code} -\begin{code}[hide] -unquoteDecl DecEq-Timelock = derive-DecEq ((quote Timelock , DecEq-Timelock) ∷ []) - -private variable - s : Timelock - ss ss' : List Timelock - m : ℕ - x : KeyHashˢ - a l r : Slot - -open import Data.List.Relation.Binary.Sublist.Ext -open import Data.List.Relation.Binary.Sublist.Propositional as S -import Data.Maybe.Relation.Unary.Any as M -\end{code} -\begin{code}[hide] -data -\end{code} -\begin{code} - evalTimelock (khs : ℙ KeyHashˢ) (I : Maybe Slot × Maybe Slot) : Timelock → Type where - evalAll : All (evalTimelock khs I) ss - → (evalTimelock khs I) (RequireAllOf ss) - evalAny : Any (evalTimelock khs I) ss - → (evalTimelock khs I) (RequireAnyOf ss) - evalMOf : MOf m (evalTimelock khs I) ss - → (evalTimelock khs I) (RequireMOf m ss) - evalSig : x ∈ khs - → (evalTimelock khs I) (RequireSig x) - evalTSt : M.Any (a ≤_) (I .proj₁) - → (evalTimelock khs I) (RequireTimeStart a) - evalTEx : M.Any (_≤ a) (I .proj₂) - → (evalTimelock khs I) (RequireTimeExpire a) -\end{code} -\caption{Timelock scripts and their evaluation} -\label{fig:defs:timelock} -\end{figure*} - -\begin{code}[hide] -instance - Dec-evalTimelock : evalTimelock ⁇³ - Dec-evalTimelock {khs} {I} {tl} .dec = go? tl - where mutual - go = evalTimelock khs I - - -- ** inversion principles for `evalTimelock` - evalAll˘ : ∀ {ss} → go (RequireAllOf ss) → All go ss - evalAll˘ (evalAll p) = p - - evalAny˘ : ∀ {ss} → go (RequireAnyOf ss) → Any go ss - evalAny˘ (evalAny p) = p - - evalTSt˘ : go (RequireTimeStart a) → M.Any (a ≤_) (I .proj₁) - evalTSt˘ (evalTSt p) = p - - evalTEx˘ : go (RequireTimeExpire a) → M.Any (_≤ a) (I .proj₂) - evalTEx˘ (evalTEx p) = p - - evalSig˘ : go (RequireSig x) → x ∈ khs - evalSig˘ (evalSig p) = p - - evalMOf˘ : ∀ {m xs} - → go (RequireMOf m xs) - → MOf m go xs - evalMOf˘ (evalMOf p) = p - - -- ** inlining recursive decision procedures to please the termination checker - MOf-go? : ∀ m xs → Dec (MOf m go xs) - unquoteDef MOf-go? = inline MOf-go? (quoteTerm (MOf? go?)) - - all-go? : Decidable¹ (All go) - unquoteDef all-go? = inline all-go? (quoteTerm (all? go?)) - - any-go? : Decidable¹ (Any go) - unquoteDef any-go? = inline any-go? (quoteTerm (any? go?)) - - -- ** the actual decision procedure - go? : Decidable¹ go - go? = λ where - (RequireAllOf ss) → mapDec evalAll evalAll˘ (all-go? ss) - (RequireAnyOf ss) → mapDec evalAny evalAny˘ (any-go? ss) - (RequireSig x) → mapDec evalSig evalSig˘ dec - (RequireTimeStart a) → mapDec evalTSt evalTSt˘ dec - (RequireTimeExpire a) → mapDec evalTEx evalTEx˘ dec - (RequireMOf m xs) → mapDec evalMOf evalMOf˘ (MOf-go? m xs) - -P1ScriptStructure-TL : ⦃ Hashable Timelock ScriptHash ⦄ → P1ScriptStructure -P1ScriptStructure-TL = record - { P1Script = Timelock - ; validP1Script = evalTimelock } - -record ScriptStructure : Type₁ where - field hashRespectsUnion : - {A B Hash : Type} → Hashable A Hash → Hashable B Hash → Hashable (A ⊎ B) Hash - ⦃ Hash-Timelock ⦄ : Hashable Timelock ScriptHash - - p1s : P1ScriptStructure - p1s = P1ScriptStructure-TL - open P1ScriptStructure p1s public - - field ps : PlutusStructure - open PlutusStructure ps public - renaming ( PlutusScript to P2Script - ; validPlutusScript to validP2Script - ) - - Script = P1Script ⊎ P2Script - - open import Data.Empty - open import Agda.Builtin.Equality - open import Relation.Binary.PropositionalEquality - - instance - Hashable-Script : Hashable Script ScriptHash - Hashable-Script = hashRespectsUnion Hashable-P1Script Hashable-PlutusScript -\end{code} diff --git a/docs/agda-spec/src/Spec/BlockDefinitions.lagda b/docs/agda-spec/src/Spec/BlockDefinitions.lagda index 0a728a4830..b94acc3a0b 100644 --- a/docs/agda-spec/src/Spec/BlockDefinitions.lagda +++ b/docs/agda-spec/src/Spec/BlockDefinitions.lagda @@ -7,17 +7,15 @@ open import Spec.BaseTypes using (Nonces) open import Ledger.Prelude open import Ledger.Crypto -open import Ledger.Script open import Ledger.Types.Epoch module Spec.BlockDefinitions (crypto : _) (open Crypto crypto) (nonces : Nonces crypto) (open Nonces nonces) (es : _) (open EpochStructure es) - (ss : ScriptStructure crypto es) (open ScriptStructure ss) where -open import Ledger.PParams crypto es ss using (ProtVer) +open import Ledger.PParams using (ProtVer) record BlockStructure : Type₁ where field diff --git a/docs/agda-spec/src/Spec/ChainHead.lagda b/docs/agda-spec/src/Spec/ChainHead.lagda index f1adba653a..18c8d18887 100644 --- a/docs/agda-spec/src/Spec/ChainHead.lagda +++ b/docs/agda-spec/src/Spec/ChainHead.lagda @@ -27,7 +27,6 @@ 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 @@ -35,18 +34,17 @@ module Spec.ChainHead (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) + (bs : BlockStructure crypto nonces es) (open BlockStructure bs) (af : _) (open AbstractFunctions af) - (li : LedgerInterface crypto es ss) (let open LedgerInterface li) + (li : LedgerInterface crypto es) (let open LedgerInterface li) (rs : _) (open RationalExtStructure rs) where open import Spec.BaseTypes crypto using (OCertCounters) -open import Spec.TickForecast crypto es ss li +open import Spec.TickForecast crypto es li open import Spec.TickNonce crypto es nonces -open import Spec.Protocol crypto nonces es ss bs af rs -open import Ledger.PParams crypto es ss using (PParams; ProtVer) +open import Spec.Protocol crypto nonces es bs af rs +open import Ledger.PParams using (PParams; ProtVer) open import Ledger.Prelude \end{code} diff --git a/docs/agda-spec/src/Spec/ChainHead/Properties.agda b/docs/agda-spec/src/Spec/ChainHead/Properties.agda index af6b1d58cb..13fe48fad7 100644 --- a/docs/agda-spec/src/Spec/ChainHead/Properties.agda +++ b/docs/agda-spec/src/Spec/ChainHead/Properties.agda @@ -4,7 +4,6 @@ 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 @@ -12,23 +11,22 @@ 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) + (bs : BlockStructure crypto nonces es) (open BlockStructure bs) (af : _) (open AbstractFunctions af) - (li : LedgerInterface crypto es ss) (let open LedgerInterface li) + (li : LedgerInterface crypto es) (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 Ledger.PParams using (PParams; ProtVer) +open import Spec.TickForecast crypto es li +open import Spec.TickForecast.Properties crypto es 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 +open import Spec.Protocol crypto nonces es bs af rs +open import Spec.Protocol.Properties crypto nonces es bs af rs +open import Spec.ChainHead crypto nonces es bs af li rs instance diff --git a/docs/agda-spec/src/Spec/OperationalCertificate.lagda b/docs/agda-spec/src/Spec/OperationalCertificate.lagda index ea8f02ece7..c1a4661ffa 100644 --- a/docs/agda-spec/src/Spec/OperationalCertificate.lagda +++ b/docs/agda-spec/src/Spec/OperationalCertificate.lagda @@ -10,7 +10,6 @@ and consists of the mapping of operation certificate issue numbers. Its signal i \begin{code}[hide] {-# 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 @@ -19,8 +18,7 @@ module Spec.OperationalCertificate (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) + (bs : BlockStructure crypto nonces es) (open BlockStructure bs) (af : _) (open AbstractFunctions af) where diff --git a/docs/agda-spec/src/Spec/OperationalCertificate/Properties.agda b/docs/agda-spec/src/Spec/OperationalCertificate/Properties.agda index 53cce7cd4e..5373f3b03d 100644 --- a/docs/agda-spec/src/Spec/OperationalCertificate/Properties.agda +++ b/docs/agda-spec/src/Spec/OperationalCertificate/Properties.agda @@ -1,7 +1,6 @@ {-# 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 @@ -10,14 +9,13 @@ 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) + (bs : BlockStructure crypto nonces es) (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 +open import Spec.OperationalCertificate crypto nonces es bs af instance diff --git a/docs/agda-spec/src/Spec/Protocol.lagda b/docs/agda-spec/src/Spec/Protocol.lagda index c145fbaf2d..e472fef9bd 100644 --- a/docs/agda-spec/src/Spec/Protocol.lagda +++ b/docs/agda-spec/src/Spec/Protocol.lagda @@ -23,7 +23,6 @@ Its state is shown in Figure~\ref{fig:ts-types:prtcl} and consists of 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 @@ -31,14 +30,13 @@ module Spec.Protocol (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) + (bs : BlockStructure crypto nonces es) (open BlockStructure bs) (af : _) (open AbstractFunctions af) (rs : _) (open RationalExtStructure rs) where open import InterfaceLibrary.Common.BaseTypes crypto using (PoolDistr; lookupPoolDistr) -open import Spec.OperationalCertificate crypto nonces es ss bs af +open import Spec.OperationalCertificate crypto nonces es bs af open import Spec.UpdateNonce crypto nonces es open import Spec.BaseTypes crypto using (OCertCounters) open import Data.Rational as ℚ using (ℚ; 0ℚ; 1ℚ) diff --git a/docs/agda-spec/src/Spec/Protocol/Properties.agda b/docs/agda-spec/src/Spec/Protocol/Properties.agda index b682a7f83d..624bc64424 100644 --- a/docs/agda-spec/src/Spec/Protocol/Properties.agda +++ b/docs/agda-spec/src/Spec/Protocol/Properties.agda @@ -3,7 +3,6 @@ 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 @@ -11,8 +10,7 @@ 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) + (bs : BlockStructure crypto nonces es) (open BlockStructure bs) (af : _) (open AbstractFunctions af) (rs : _) (open RationalExtStructure rs) where @@ -20,12 +18,12 @@ module Spec.Protocol.Properties 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.Protocol crypto nonces es 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 Spec.OperationalCertificate crypto nonces es bs af +open import Spec.OperationalCertificate.Properties crypto nonces es bs af open import InterfaceLibrary.Common.BaseTypes crypto using (PoolDistr; lookupPoolDistr) private diff --git a/docs/agda-spec/src/Spec/TickForecast.lagda b/docs/agda-spec/src/Spec/TickForecast.lagda index 53c648e112..c4350e4bca 100644 --- a/docs/agda-spec/src/Spec/TickForecast.lagda +++ b/docs/agda-spec/src/Spec/TickForecast.lagda @@ -9,15 +9,13 @@ and its signal is the current slot. {-# OPTIONS --safe #-} open import Ledger.Crypto -open import Ledger.Script open import Ledger.Types.Epoch open import InterfaceLibrary.Ledger module Spec.TickForecast (crypto : Crypto) (es : _) (open EpochStructure es) - (ss : ScriptStructure crypto es) (open ScriptStructure ss) - (li : LedgerInterface crypto es ss) (let open LedgerInterface li) + (li : LedgerInterface crypto es) (let open LedgerInterface li) where open import Ledger.Prelude diff --git a/docs/agda-spec/src/Spec/TickForecast/Properties.agda b/docs/agda-spec/src/Spec/TickForecast/Properties.agda index 8eea212058..7e890d1055 100644 --- a/docs/agda-spec/src/Spec/TickForecast/Properties.agda +++ b/docs/agda-spec/src/Spec/TickForecast/Properties.agda @@ -1,19 +1,17 @@ {-# 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) + (li : LedgerInterface crypto es) (let open LedgerInterface li) where open import Ledger.Prelude -open import Spec.TickForecast crypto es ss li +open import Spec.TickForecast crypto es li instance diff --git a/docs/agda-spec/src/Spec/TickNonce.lagda b/docs/agda-spec/src/Spec/TickNonce.lagda index 663a09e12b..c3da798baf 100644 --- a/docs/agda-spec/src/Spec/TickNonce.lagda +++ b/docs/agda-spec/src/Spec/TickNonce.lagda @@ -11,7 +11,6 @@ Its state consists of the epoch nonce \afld{η₀} and the previous epoch's last {-# OPTIONS --safe #-} open import Ledger.Crypto -open import Ledger.Script open import Ledger.Types.Epoch open import Spec.BaseTypes using (Nonces) diff --git a/docs/agda-spec/src/Spec/TickNonce/Properties.agda b/docs/agda-spec/src/Spec/TickNonce/Properties.agda index 52d49cbcaf..46ccfc7edb 100644 --- a/docs/agda-spec/src/Spec/TickNonce/Properties.agda +++ b/docs/agda-spec/src/Spec/TickNonce/Properties.agda @@ -1,7 +1,6 @@ {-# OPTIONS --safe #-} open import Ledger.Crypto -open import Ledger.Script open import Ledger.Types.Epoch open import Spec.BaseTypes using (Nonces)