Skip to content

Commit

Permalink
make PolicyId a module parameter, not a record field
Browse files Browse the repository at this point in the history
  • Loading branch information
@williamdemeo
williamdemeo committed Jul 7, 2023
1 parent 4302f04 commit fdc7a8c
Show file tree
Hide file tree
Showing 4 changed files with 86 additions and 68 deletions.
100 changes: 55 additions & 45 deletions src/Ledger/Foreign/HSLedger.agda
View file
Original file line number Diff line number Diff line change
@@ -1,11 +1,17 @@
{-# OPTIONS --overlapping-instances #-}
module Ledger.Foreign.HSLedger where

open import Agda.Primitive using () renaming (Set to Type)

module Ledger.Foreign.HSLedger (pid : Type) 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 Data.Nat.Properties using (+-0-monoid)
open import Data.Nat using (_≤_; _≤ᵇ_)
open import Data.Nat.Properties using (+-*-semiring; <-isStrictTotalOrder)

Expand Down Expand Up @@ -91,57 +97,61 @@ HSP2ScriptStructure .validPlutusScript? = λ ()
HSScriptStructure : ScriptStructure ℕ ℕ ℕ
HSScriptStructure = record { p1s = HSP1ScriptStructure ; ps = HSP2ScriptStructure }

open import Data.Nat
open import Data.Nat.Properties using (+-0-commutativeMonoid; _≟_)
open import Ledger.TokenAlgebra
open import Ledger.Transaction
import Ledger.TokenAlgebra as TA
open import Data.Nat.Properties using (+-0-commutativeMonoid; _≟_)
open import Data.Nat

coinTokenAlgebra : TokenAlgebra
coinTokenAlgebra = record
{ PolicyId = ℕ
; Value-CommutativeMonoid = +-0-commutativeMonoid
; coin = id
; inject = id
; policies = λ x → ∅
; size = λ x → 1 -- there is only ada in this token algebra
; property = λ x → refl
; coinIsMonoidHomomorphism =
record
{ isMagmaHomomorphism = record { isRelHomomorphism = record { cong = id } ; homo = λ _ _ → refl }
; ε-homo = refl
}
; AssetName = String
; specialAsset = "Ada"
; _≤ᵗ_ = _≤_
; DecEq-Value = record { _≟_ = Data.Nat._≟_ }
}
module _ where

open TA pid
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 =
record
{ isMagmaHomomorphism = record { isRelHomomorphism = record { cong = id } ; homo = λ _ _ → refl }
; ε-homo = refl
}
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 .crypto = HSCrypto
HSTransactionStructure .adHashingScheme = isHashableSet-⊤
HSTransactionStructure .ppHashingScheme = isHashableSelf PParams
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
HSTransactionStructure .DecEq-TxId = DecEq-ℕ
HSTransactionStructure .DecEq-Ix = DecEq-ℕ
HSTransactionStructure .DecEq-Netw = DecEq-⊤
HSTransactionStructure .DecEq-UpdT = DecEq-⊤
HSTransactionStructure .ss = HSScriptStructure
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 .txidBytes = id
HSTransactionStructure .networkId = tt
HSTransactionStructure .tokenAlgebra = coinTokenAlgebra
HSTransactionStructure .DecEq-TxId = DecEq-ℕ
HSTransactionStructure .DecEq-Ix = DecEq-ℕ
HSTransactionStructure .DecEq-Netw = DecEq-⊤
HSTransactionStructure .DecEq-UpdT = DecEq-⊤
HSTransactionStructure .ss = HSScriptStructure

open import Ledger.Utxo HSTransactionStructure
open import Ledger.Utxo.Properties HSTransactionStructure
Expand Down
11 changes: 6 additions & 5 deletions src/Ledger/TokenAlgebra.lagda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,9 @@
\begin{code}[hide]
{-# OPTIONS --safe #-}

module Ledger.TokenAlgebra where
open import Agda.Primitive using() renaming (Set to Type)

module Ledger.TokenAlgebra (PolicyId : Type) where

open import Ledger.Prelude

Expand All @@ -19,20 +21,19 @@ open import Relation.Unary using (Pred)
\begin{figure*}
\begin{code}
record TokenAlgebra : Set₁ where
field PolicyId : Set
Value-CommutativeMonoid : CommutativeMonoid 0ℓ 0ℓ
field Value-CommutativeMonoid : CommutativeMonoid 0ℓ 0ℓ

MemoryEstimate : Type
MemoryEstimate = ℕ
\end{code}
\begin{code}[hide]
open CommutativeMonoid Value-CommutativeMonoid public
using ( _≈_ ; ε ; monoid )
using ( _≈_ ; ε ; monoid ; rawMonoid)
renaming ( Carrier to Value
; refl to reflᵛ
; _∙_ to _+ᵛ_
)
open MonoidMorphisms (Monoid.rawMonoid monoid) (Monoid.rawMonoid +-0-monoid)
open MonoidMorphisms (rawMonoid) (Monoid.rawMonoid +-0-monoid) public
\end{code}
\begin{code}
field coin : Value → Coin
Expand Down
28 changes: 17 additions & 11 deletions src/Ledger/Transaction.lagda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,10 +12,10 @@ open import Ledger.Prelude

open import Ledger.Crypto
open import Ledger.Epoch
open import Ledger.TokenAlgebra
import Ledger.PParams
import Ledger.Script
import Ledger.GovernanceActions
import Ledger.TokenAlgebra as TA

record TransactionStructure : Set₁ where
field
Expand All @@ -35,11 +35,15 @@ 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}
\AgdaTarget{Ix, TxId, Epoch, AuxiliaryData, PolicyId}
\begin{code}
Ix TxId AuxiliaryData : Set
Ix TxId AuxiliaryData PolicyId AssetName : Set
\end{code}
\begin{code}[hide]
epochStructure : EpochStructure
Expand All @@ -53,17 +57,19 @@ the transaction body are:
ppUpd : Ledger.PParams.PParamsDiff epochStructure
txidBytes : TxId → Crypto.Ser crypto
networkId : Network
tokenAlgebra : TokenAlgebra
instance DecEq-TxId : DecEq TxId
DecEq-Ix : DecEq Ix
DecEq-Netw : DecEq Network
DecEq-UpdT : DecEq (Ledger.PParams.PParamsDiff.UpdateT ppUpd)

open Crypto crypto public
open TokenAlgebra tokenAlgebra public
open TA PolicyId
open isHashableSet adHashingScheme renaming (THash to ADHash) public

field ss : Ledger.Script.ScriptStructure KeyHash ScriptHash Slot
field ss : Ledger.Script.ScriptStructure KeyHash ScriptHash Slot
tokenAlgebra : TokenAlgebra

open TokenAlgebra tokenAlgebra public

open Ledger.Script.ScriptStructure ss public

Expand Down Expand Up @@ -94,19 +100,19 @@ the transaction body are:
record TxBody : Set where
field txins : ℙ TxIn
txouts : Ix ⇀ TxOut
txfee : Coin
txcerts : List DCert
mint : Value
txfee : Coin
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
Expand Down
15 changes: 8 additions & 7 deletions src/Ledger/Utxo/Properties.lagda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@ open import Tactic.MonoidSolver
open TransactionStructure txs

open import Ledger.PParams epochStructure
open import Ledger.TokenAlgebra using (TokenAlgebra)
open import Ledger.TokenAlgebra PolicyId -- using (TokenAlgebra)
open import Ledger.Utxo txs renaming (Computational-UTXO to Computational-UTXO')

open TxBody
Expand Down Expand Up @@ -61,22 +61,23 @@ abstract
Computational-UTXO : Computational _⊢_⇀⦇_,UTXO⦈_
Computational-UTXO = Computational-UTXO'

⟦⟧-cong-Coin = IsMonoidHomomorphism.⟦⟧-cong coinIsMonoidHomomorphism
∙-homo-Coin = IsMagmaHomomorphism.homo (IsMonoidHomomorphism.isMagmaHomomorphism coinIsMonoidHomomorphism)

balance-cong : proj₁ utxo ≡ᵉ proj₁ utxo' → balance utxo ≈ balance utxo'
balance-cong {utxo} {utxo'} = indexedSumᵐ-cong {x = utxo ᶠᵐ} {utxo' ᶠᵐ}

balance-cong-coin : proj₁ utxo ≡ᵉ proj₁ utxo' → cbalance utxo ≡ cbalance utxo'
balance-cong-coin {utxo} {utxo'} x = ⟦⟧-cong-Coin (balance-cong {utxo} {utxo'} x)
balance-cong-coin {utxo} {utxo'} x = IsMonoidHomomorphism.⟦⟧-cong coinIsMonoidHomomorphism (balance-cong {utxo} {utxo'} x)

open MonoidMorphisms.IsMonoidHomomorphism
private
∙-homo-Coin = IsMagmaHomomorphism.homo (isMagmaHomomorphism coinIsMonoidHomomorphism)

balance-∪ : disjoint (dom (utxo ˢ)) (dom (utxo' ˢ))
→ cbalance (utxo ∪ᵐˡ utxo') ≡ cbalance utxo + cbalance utxo'
balance-∪ {utxo} {utxo'} h = begin
cbalance (utxo ∪ᵐˡ utxo')
≡⟨ ⟦⟧-cong-Coin (indexedSumᵐ-cong {x = (utxo ∪ᵐˡ utxo') ᶠᵐ} {(utxo ᶠᵐ) ∪ᵐˡᶠ (utxo' ᶠᵐ)} (id , id)) ⟩
≡⟨ ⟦⟧-cong coinIsMonoidHomomorphism (indexedSumᵐ-cong {x = (utxo ∪ᵐˡ utxo') ᶠᵐ} {(utxo ᶠᵐ) ∪ᵐˡᶠ (utxo' ᶠᵐ)} (id , id)) ⟩
coin (indexedSumᵐ _ ((utxo ᶠᵐ) ∪ᵐˡᶠ (utxo' ᶠᵐ)))
≡⟨ ⟦⟧-cong-Coin (indexedSumᵐ-∪ {X = utxo ᶠᵐ} {utxo' ᶠᵐ} h) ⟩
≡⟨ ⟦⟧-cong coinIsMonoidHomomorphism (indexedSumᵐ-∪ {X = utxo ᶠᵐ} {utxo' ᶠᵐ} h) ⟩
coin (balance utxo +ᵛ balance utxo')
≡⟨ ∙-homo-Coin _ _ ⟩
cbalance utxo + cbalance utxo' ∎
Expand Down

0 comments on commit fdc7a8c

Please sign in to comment.