token algebras are era independent

Author: williamdemeo

src/Ledger/Conway/Specification/Transaction.lagda.md

@@ -27,7 +27,7 @@ import Ledger.Conway.Specification.PParams
 import Ledger.Conway.Specification.Script.Base
 import Ledger.Conway.Specification.Gov.Actions
 import Ledger.Conway.Specification.Certs
-import Ledger.Conway.Specification.TokenAlgebra.Base
+import Ledger.Core.Specification.TokenAlgebra.Base
 import Ledger.Core.Specification.Address
 
 open import Relation.Nullary.Decidable using (⌊_⌋)
@@ -88,7 +88,7 @@ record TransactionStructure : Type₁ where
 
   field cryptoStructure : _
   open CryptoStructure cryptoStructure public
-  open Ledger.Conway.Specification.TokenAlgebra.Base ScriptHash public
+  open Ledger.Core.Specification.TokenAlgebra.Base ScriptHash public
   open Ledger.Core.Specification.Address Network KeyHash ScriptHash ⦃ it ⦄ ⦃ it ⦄ ⦃ it ⦄ public
 
   field epochStructure : _

src/Ledger/Conway/Specification/Utxo.lagda.md

@@ -137,7 +137,7 @@ instance
 ```
 -->
 
- *UTxO transitions*
+*UTxO transitions*
 
 ```agda
 data _⊢_⇀⦇_,UTXO⦈_ : UTxOEnv → UTxOState → Tx → UTxOState → Type

src/Ledger/Core/Specification/TokenAlgebra/Base.lagda.md

@@ -1,6 +1,6 @@
 ---
 source_branch: master
-source_path: src/Ledger/Conway/Specification/TokenAlgebra/Base.lagda
+source_path: src/Ledger/Core/Specification/TokenAlgebra/Base.lagda
 ---
 
 # Token Algebras {#sec:token-algebra}
@@ -11,7 +11,7 @@ Token algebras are used for multiple assets.
 ```agda
 {-# OPTIONS --safe #-}
 open import Prelude using (Type)
-module Ledger.Conway.Specification.TokenAlgebra.Base (
+module Ledger.Core.Specification.TokenAlgebra.Base (
 ```
 -->
  *Abstract types*

src/Ledger/Core/Specification/TokenAlgebra/Coin.lagda.md

@@ -1,18 +1,18 @@
 ---
 source_branch: master
-source_path: src/Ledger/Conway/Specification/TokenAlgebra/Coin.lagda.md
+source_path: src/Ledger/Core/Specification/TokenAlgebra/Coin.lagda.md
 ---
 
 ```agda
 {-# OPTIONS --safe #-}
 open import Ledger.Prelude
 
-module Ledger.Conway.Specification.TokenAlgebra.Coin (X : Type) where
+module Ledger.Core.Specification.TokenAlgebra.Coin (X : Type) where
 
 open import Algebra.Morphism.Construct.Identity
   using (isMonoidHomomorphism)
 
-open import Ledger.Conway.Specification.TokenAlgebra.Base X
+open import Ledger.Core.Specification.TokenAlgebra.Base X
 
 open TokenAlgebra
 

src/Ledger/Core/Specification/TokenAlgebra/ValueSet.lagda.md

@@ -1,6 +1,6 @@
 ---
 source_branch: master
-source_path: src/Ledger/Conway/Specification/TokenAlgebra/ValueSet.lagda.md
+source_path: src/Ledger/Core/Specification/TokenAlgebra/ValueSet.lagda.md
 ---
 
 ## Value Set {#sec:value-set}
@@ -12,11 +12,11 @@ source_path: src/Ledger/Conway/Specification/TokenAlgebra/ValueSet.lagda.md
 
 open import Prelude using (Type)
 
-module Ledger.Conway.Specification.TokenAlgebra.ValueSet (PolicyId AssetName : Type) where
+module Ledger.Core.Specification.TokenAlgebra.ValueSet (PolicyId AssetName : Type) where
 
 open import Ledger.Prelude                         hiding (lookup ; update ; isMagma ; isEquivalence) renaming (TotalMap to _⇒_)
 open _⇒_
-open import Ledger.Conway.Specification.TokenAlgebra.Base PolicyId using (TokenAlgebra)
+open import Ledger.Core.Specification.TokenAlgebra.Base PolicyId using (TokenAlgebra)
 
 open import Algebra                                using (Op₂ ; IsSemigroup ; IsMonoid ; IsMagma ; IsCommutativeMonoid)
 open import Algebra.Morphism                       using (IsMonoidHomomorphism ; IsMagmaHomomorphism)

src/Ledger/Core/Specification/TokenAlgebra/ValueVector.lagda.md

@@ -1,13 +1,13 @@
 ---
 source_branch: master
-source_path: src/Ledger/Conway/Specification/TokenAlgebra/ValueVector.lagda.md
+source_path: src/Ledger/Core/Specification/TokenAlgebra/ValueVector.lagda.md
 ---
 
 ```agda
 {-# OPTIONS --safe #-}
 open import Ledger.Prelude hiding (_∙_; ε)
 
-module Ledger.Conway.Specification.TokenAlgebra.ValueVector (PolicyId : Type) (n : ℕ) where
+module Ledger.Core.Specification.TokenAlgebra.ValueVector (PolicyId : Type) (n : ℕ) where
 
 import Algebra as Alg
 open import Algebra.Construct.DirectProduct
@@ -19,7 +19,7 @@ open import Data.Vec as Vec
 import stdlib.Data.Vec.Instances as Vec
 import Data.Vec.Relation.Binary.Pointwise.Inductive as Vec
 
-open import Ledger.Conway.Specification.TokenAlgebra.Base PolicyId
+open import Ledger.Core.Specification.TokenAlgebra.Base PolicyId
 
 Quantity = ℕ
 

src/Ledger/Dijkstra/Specification/TokenAlgebra/Base.lagda.md

@@ -7,5 +7,5 @@ source_path: src/Ledger/Dijkstra/Specification/TokenAlgebra/Base.lagda.md
 open import Prelude using (Type)
 module Ledger.Dijkstra.Specification.TokenAlgebra.Base (PolicyId : Type) where
 
-open import Ledger.Conway.Specification.TokenAlgebra.Base PolicyId public
+open import Ledger.Core.Specification.TokenAlgebra.Base PolicyId public
 ```

src/Ledger/Dijkstra/Specification/Transaction.lagda.md

@@ -191,7 +191,8 @@ The fields that depend on the transaction level use the auxiliary functions
       field
         txBody       : TxBody txLevel
         txWitnesses  : TxWitnesses txLevel
-        isValid      : InTopLevel txLevel Bool
+        txSize       : InSubLevel txLevel ℕ    -- only in sub-level tx
+        isValid      : InTopLevel txLevel Bool -- only in top-level tx
         txAuxData    : Maybe AuxiliaryData
 
     record TxBody (txLevel : TxLevel) : Type where
@@ -391,6 +392,10 @@ could be either of them.
   getTxScripts {TxLevelSub} = getSubTxScripts
   getTxScripts {TxLevelTop} =
     concatMapˢ getSubTxScripts ∘ fromList ∘ TxBody.txSubTransactions ∘ TxBodyOf
+
+  getTopLevelTxSize : TopLevelTx → ℕ
+  getTopLevelTxSize txTop = sum (map (λ subTx → subTx .txSize) (txTop .txBody .txSubTransactions))
+    where open Tx; open TxBody
 ```
 -->