diff --git a/src/Ledger/Foreign/HSLedger.agda b/src/Ledger/Foreign/HSLedger.agda index 36d669528..9a6ec626a 100644 --- a/src/Ledger/Foreign/HSLedger.agda +++ b/src/Ledger/Foreign/HSLedger.agda @@ -2,15 +2,15 @@ open import Agda.Primitive using () renaming (Set to Type) -module Ledger.Foreign.HSLedger (pid : Type) where +module Ledger.Foreign.HSLedger where open import Ledger.Prelude import Data.Maybe as M import Data.Rational as ℚ -open import Algebra using (CommutativeMonoid) -- Monoid) -open import Algebra.Morphism using (module MonoidMorphisms ) +open import Algebra using (CommutativeMonoid) +open import Algebra.Morphism using (module MonoidMorphisms) open import Data.Nat.Properties using (+-0-monoid) open import Data.Nat using (_≤_; _≤ᵇ_) open import Data.Nat.Properties using (+-*-semiring; <-isStrictTotalOrder) @@ -104,27 +104,28 @@ open import Data.Nat module _ where - open TA pid + open TA ℕ open TA.TokenAlgebra coinTokenAlgebra : TokenAlgebra - Value-CommutativeMonoid coinTokenAlgebra = +-0-commutativeMonoid - coin coinTokenAlgebra = id - inject coinTokenAlgebra = id - policies coinTokenAlgebra = λ _ → ∅ - size coinTokenAlgebra = λ x → 1 -- there is only ada in this token algebra - _≤ᵗ_ coinTokenAlgebra = _≤_ - AssetName coinTokenAlgebra = String - specialAsset coinTokenAlgebra = "Ada" - property coinTokenAlgebra = λ _ → refl - coinTokenAlgebra .coinIsMonoidHomomorphism = + Value-CommutativeMonoid coinTokenAlgebra = +-0-commutativeMonoid + coin coinTokenAlgebra = id + inject coinTokenAlgebra = id + policies coinTokenAlgebra = λ _ → ∅ + size coinTokenAlgebra = λ x → 1 -- there is only ada in this token algebra + _≤ᵗ_ coinTokenAlgebra = _≤_ + AssetName coinTokenAlgebra = String + specialAsset coinTokenAlgebra = "Ada" + property coinTokenAlgebra = λ _ → refl + coinTokenAlgebra .coinIsMonoidHomomorphism = record - { isMagmaHomomorphism = record { isRelHomomorphism = record { cong = id } ; homo = λ _ _ → refl } - ; ε-homo = refl + { isMagmaHomomorphism = record { isRelHomomorphism = record { cong = id } ; homo = λ _ _ → refl } + ; ε-homo = refl } - DecEq-Value coinTokenAlgebra = record { _≟_ = Data.Nat._≟_ } + DecEq-Value coinTokenAlgebra = record { _≟_ = Data.Nat._≟_ } module _ where open TransactionStructure + open PParamsDiff HSTransactionStructure : TransactionStructure HSTransactionStructure .Ix = ℕ @@ -132,18 +133,14 @@ module _ where HSTransactionStructure .epochStructure = HSEpochStructure HSTransactionStructure .globalConstants = HSGlobalConstants HSTransactionStructure .AuxiliaryData = ⊤ - HSTransactionStructure .PolicyId = pid - HSTransactionStructure .AssetName = String HSTransactionStructure .crypto = HSCrypto HSTransactionStructure .adHashingScheme = isHashableSet-⊤ HSTransactionStructure .ppHashingScheme = isHashableSelf PParams - HSTransactionStructure .ppUpd = record - { UpdateT = ⊤ - ; updateGroups = λ _ → ∅ - ; applyUpdate = λ p _ → p - ; ppdWellFormed = λ _ → true - ; ppdWellFormed⇒WF = λ _ _ x → x - } + HSTransactionStructure .ppUpd .UpdateT = ⊤ + HSTransactionStructure .ppUpd .updateGroups = λ _ → ∅ + HSTransactionStructure .ppUpd .applyUpdate = λ p _ → p + HSTransactionStructure .ppUpd .ppdWellFormed = λ _ → true + HSTransactionStructure .ppUpd .ppdWellFormed⇒WF = λ _ _ x → x HSTransactionStructure .txidBytes = id HSTransactionStructure .networkId = tt HSTransactionStructure .tokenAlgebra = coinTokenAlgebra diff --git a/src/Ledger/TokenAlgebra.lagda b/src/Ledger/TokenAlgebra.lagda index bd315c1f8..57bdee318 100644 --- a/src/Ledger/TokenAlgebra.lagda +++ b/src/Ledger/TokenAlgebra.lagda @@ -4,13 +4,10 @@ \begin{code}[hide] {-# OPTIONS --safe #-} -open import Agda.Primitive using() renaming (Set to Type) - -module Ledger.TokenAlgebra (PolicyId : Type) where +module Ledger.TokenAlgebra (PolicyId : Set) where open import Ledger.Prelude -open import Agda.Primitive using() renaming (Set to Type) open import Algebra using (CommutativeMonoid ; Monoid) open import Algebra.Morphism using (module MonoidMorphisms ) open import Data.Nat.Properties using (+-0-monoid) @@ -23,7 +20,7 @@ open import Relation.Unary using (Pred) record TokenAlgebra : Set₁ where field Value-CommutativeMonoid : CommutativeMonoid 0ℓ 0ℓ - MemoryEstimate : Type + MemoryEstimate : Set MemoryEstimate = ℕ \end{code} \begin{code}[hide] @@ -36,13 +33,13 @@ record TokenAlgebra : Set₁ where open MonoidMorphisms (rawMonoid) (Monoid.rawMonoid +-0-monoid) public \end{code} \begin{code} - field coin : Value → Coin - inject : Coin → Value - policies : Value → ℙ PolicyId - size : Value → MemoryEstimate - _≤ᵗ_ : Value → Value → Set - AssetName : Type - specialAsset : AssetName + field coin : Value → Coin + inject : Coin → Value + policies : Value → ℙ PolicyId + size : Value → MemoryEstimate + _≤ᵗ_ : Value → Value → Set + AssetName : Set + specialAsset : AssetName property : coin ∘ inject ≗ id coinIsMonoidHomomorphism : IsMonoidHomomorphism coin \end{code} diff --git a/src/Ledger/Transaction.lagda b/src/Ledger/Transaction.lagda index 8b802de0c..3b9b8c606 100644 --- a/src/Ledger/Transaction.lagda +++ b/src/Ledger/Transaction.lagda @@ -35,15 +35,11 @@ the transaction body are: \item The size and the hash of the serialized form of the transaction that was included in the block. \end{itemize} -Finally, $\fun{txid}$ computes the transaction id of a given transaction. -This function must produce a unique id for each unique transaction body. -\textbf{We assume that} $\fun{txid}$ \textbf{is injective.} - \begin{figure*}[h] \emph{Abstract types} \AgdaTarget{Ix, TxId, Epoch, AuxiliaryData, PolicyId} \begin{code} - Ix TxId AuxiliaryData PolicyId AssetName : Set + Ix TxId AuxiliaryData : Set \end{code} \begin{code}[hide] epochStructure : EpochStructure @@ -63,7 +59,7 @@ This function must produce a unique id for each unique transaction body. DecEq-UpdT : DecEq (Ledger.PParams.PParamsDiff.UpdateT ppUpd) open Crypto crypto public - open TA PolicyId + open TA ScriptHash open isHashableSet adHashingScheme renaming (THash to ADHash) public field ss : Ledger.Script.ScriptStructure KeyHash ScriptHash Slot @@ -100,19 +96,19 @@ This function must produce a unique id for each unique transaction body. record TxBody : Set where field txins : ℙ TxIn txouts : Ix ⇀ TxOut - txcerts : List DCert - mint : Value txfee : Coin + mint : Value txvldt : Maybe Slot × Maybe Slot + txcerts : List DCert txwdrls : Wdrl + txvote : List GovVote + txprop : List GovProposal + txdonation : ℕ txup : Maybe Update txADhash : Maybe ADHash netwrk : Maybe Network txsize : ℕ txid : TxId - txvote : List GovVote - txprop : List GovProposal - txdonation : ℕ record TxWitnesses : Set where field vkSigs : VKey ⇀ Sig diff --git a/src/Ledger/Utxo/Properties.lagda b/src/Ledger/Utxo/Properties.lagda index 6ac3b4528..2f1f4952f 100644 --- a/src/Ledger/Utxo/Properties.lagda +++ b/src/Ledger/Utxo/Properties.lagda @@ -29,7 +29,7 @@ open import Tactic.MonoidSolver open TransactionStructure txs open import Ledger.PParams epochStructure -open import Ledger.TokenAlgebra PolicyId -- using (TokenAlgebra) +open import Ledger.TokenAlgebra ScriptHash open import Ledger.Utxo txs renaming (Computational-UTXO to Computational-UTXO') open TxBody