effect changes requested by @WhatisRT

IntersectMBO · Jul 12, 2023 · 0b16e3d · 0b16e3d
1 parent fdc7a8c
commit 0b16e3d
Show file tree

Hide file tree

Showing 4 changed files with 40 additions and 50 deletions.
diff --git 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,46 +104,43 @@ 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              = ℕ
   HSTransactionStructure .TxId            = ℕ
   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
@@ -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
@@ -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
@@ -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