From 13feb8375829c2f6b1d9ad4c3a8da2dd9867d869 Mon Sep 17 00:00:00 2001 From: Tudor Ferariu Date: Fri, 17 Oct 2025 13:16:55 +0100 Subject: [PATCH 01/11] Reimplemented Alasdair's Example Traces and added 3 more example contracts --- .../Foreign/HSLedger/ExternalStructures.agda | 1 + .../Conway/Specification/Abstract.lagda.md | 3 +- .../Conway/Specification/Script/Base.lagda.md | 2 +- .../Specification/Script/Validation.lagda.md | 34 +-- .../Conway/Specification/ScriptPurpose.agda | 30 +++ .../ScriptPurpose.agda:Zone.Identifier | Bin 0 -> 25 bytes .../Test/AbstractImplementation.agda | 36 +++ ...bstractImplementation.agda:Zone.Identifier | Bin 0 -> 25 bytes .../Test/Examples.agda:Zone.Identifier | Bin 0 -> 25 bytes .../Specification/Test/Examples.lagda.md | 17 +- .../Test/Examples/AccountSim/Datum.agda | 30 +++ .../AccountSim/Datum.agda:Zone.Identifier | Bin 0 -> 25 bytes .../Examples/AccountSim/OffChain/Cleanup.agda | 54 +++++ .../OffChain/Cleanup.agda:Zone.Identifier | Bin 0 -> 25 bytes .../Examples/AccountSim/OffChain/Close.agda | 59 +++++ .../OffChain/Close.agda:Zone.Identifier | Bin 0 -> 25 bytes .../Examples/AccountSim/OffChain/Deposit.agda | 70 ++++++ .../OffChain/Deposit.agda:Zone.Identifier | Bin 0 -> 25 bytes .../Examples/AccountSim/OffChain/Lib.agda | 108 +++++++++ .../OffChain/Lib.agda:Zone.Identifier | Bin 0 -> 25 bytes .../AccountSim/OffChain/OffChain.agda | 11 + .../OffChain/OffChain.agda:Zone.Identifier | Bin 0 -> 25 bytes .../Examples/AccountSim/OffChain/Open.agda | 60 +++++ .../OffChain/Open.agda:Zone.Identifier | Bin 0 -> 25 bytes .../Examples/AccountSim/OffChain/Start.agda | 54 +++++ .../OffChain/Start.agda:Zone.Identifier | Bin 0 -> 25 bytes .../AccountSim/OffChain/Transfer.agda | 64 +++++ .../OffChain/Transfer.agda:Zone.Identifier | Bin 0 -> 25 bytes .../AccountSim/OffChain/Withdraw.agda | 66 +++++ .../OffChain/Withdraw.agda:Zone.Identifier | Bin 0 -> 25 bytes .../Test/Examples/AccountSim/Test/Trace.agda | 169 +++++++++++++ .../Test/Trace.agda:Zone.Identifier | Bin 0 -> 25 bytes .../Test/Examples/AccountSim/Validator.agda | 225 ++++++++++++++++++ .../AccountSim/Validator.agda:Zone.Identifier | Bin 0 -> 25 bytes .../Test/Examples/DEx/Datum.agda | 30 +++ .../Examples/DEx/Datum.agda:Zone.Identifier | Bin 0 -> 25 bytes .../Test/Examples/DEx/OffChain/Close.agda | 54 +++++ .../DEx/OffChain/Close.agda:Zone.Identifier | Bin 0 -> 25 bytes .../Test/Examples/DEx/OffChain/Exchange.agda | 69 ++++++ .../OffChain/Exchange.agda:Zone.Identifier | Bin 0 -> 25 bytes .../Test/Examples/DEx/OffChain/Lib.agda | 121 ++++++++++ .../DEx/OffChain/Lib.agda:Zone.Identifier | Bin 0 -> 25 bytes .../Test/Examples/DEx/OffChain/OffChain.agda | 8 + .../OffChain/OffChain.agda:Zone.Identifier | Bin 0 -> 25 bytes .../Test/Examples/DEx/OffChain/Start.agda | 55 +++++ .../DEx/OffChain/Start.agda:Zone.Identifier | Bin 0 -> 25 bytes .../Test/Examples/DEx/OffChain/Update.agda | 61 +++++ .../DEx/OffChain/Update.agda:Zone.Identifier | Bin 0 -> 25 bytes .../Test/Examples/DEx/Test/Trace.agda | 140 +++++++++++ .../DEx/Test/Trace.agda:Zone.Identifier | Bin 0 -> 25 bytes .../Test/Examples/DEx/Validator.agda | 196 +++++++++++++++ .../DEx/Validator.agda:Zone.Identifier | Bin 0 -> 25 bytes .../Examples/HelloWorld.agda:Zone.Identifier | Bin 0 -> 25 bytes .../Test/Examples/HelloWorld.lagda.md | 23 +- .../Test/Examples/MultiSig/Datum.agda | 27 +++ .../MultiSig/Datum.agda:Zone.Identifier | Bin 0 -> 25 bytes .../Examples/MultiSig/OffChain/AddSig.agda | 65 +++++ .../OffChain/AddSig.agda:Zone.Identifier | Bin 0 -> 25 bytes .../Test/Examples/MultiSig/OffChain/Lib.agda | 93 ++++++++ .../OffChain/Lib.agda:Zone.Identifier | Bin 0 -> 25 bytes .../Examples/MultiSig/OffChain/OffChain.agda | 8 + .../OffChain/OffChain.agda:Zone.Identifier | Bin 0 -> 25 bytes .../Test/Examples/MultiSig/OffChain/Open.agda | 61 +++++ .../OffChain/Open.agda:Zone.Identifier | Bin 0 -> 25 bytes .../Test/Examples/MultiSig/OffChain/Pay.agda | 67 ++++++ .../OffChain/Pay.agda:Zone.Identifier | Bin 0 -> 25 bytes .../Examples/MultiSig/OffChain/Propose.agda | 61 +++++ .../OffChain/Propose.agda:Zone.Identifier | Bin 0 -> 25 bytes .../Test/Examples/MultiSig/Test/Trace.agda | 138 +++++++++++ .../MultiSig/Test/Trace.agda:Zone.Identifier | Bin 0 -> 25 bytes .../Test/Examples/MultiSig/Validator.agda | 205 ++++++++++++++++ .../MultiSig/Validator.agda:Zone.Identifier | Bin 0 -> 25 bytes .../Test/Examples/MultiSigV2/Datum.agda | 26 ++ .../MultiSigV2/Datum.agda:Zone.Identifier | Bin 0 -> 25 bytes .../Examples/MultiSigV2/OffChain/AddSig.agda | 59 +++++ .../OffChain/AddSig.agda:Zone.Identifier | Bin 0 -> 25 bytes .../Examples/MultiSigV2/OffChain/Cancel.agda | 61 +++++ .../OffChain/Cancel.agda:Zone.Identifier | Bin 0 -> 25 bytes .../Examples/MultiSigV2/OffChain/Cleanup.agda | 54 +++++ .../OffChain/Cleanup.agda:Zone.Identifier | Bin 0 -> 25 bytes .../Examples/MultiSigV2/OffChain/Lib.agda | 100 ++++++++ .../OffChain/Lib.agda:Zone.Identifier | Bin 0 -> 25 bytes .../MultiSigV2/OffChain/OffChain.agda | 10 + .../OffChain/OffChain.agda:Zone.Identifier | Bin 0 -> 25 bytes .../Examples/MultiSigV2/OffChain/Open.agda | 55 +++++ .../OffChain/Open.agda:Zone.Identifier | Bin 0 -> 25 bytes .../Examples/MultiSigV2/OffChain/Pay.agda | 64 +++++ .../OffChain/Pay.agda:Zone.Identifier | Bin 0 -> 25 bytes .../Examples/MultiSigV2/OffChain/Propose.agda | 60 +++++ .../OffChain/Propose.agda:Zone.Identifier | Bin 0 -> 25 bytes .../Test/Examples/MultiSigV2/Test/Trace.agda | 180 ++++++++++++++ .../Test/Trace.agda:Zone.Identifier | Bin 0 -> 25 bytes .../Test/Examples/MultiSigV2/Validator.agda | 216 +++++++++++++++++ .../MultiSigV2/Validator.agda:Zone.Identifier | Bin 0 -> 25 bytes .../SucceedIfNumber.agda:Zone.Identifier | Bin 0 -> 25 bytes .../Test/Examples/SucceedIfNumber.lagda.md | 2 +- .../LedgerImplementation.agda:Zone.Identifier | Bin 0 -> 25 bytes .../Test/LedgerImplementation.lagda.md | 1 - .../Test/Lib.agda:Zone.Identifier | Bin 0 -> 25 bytes .../Conway/Specification/Test/Lib.lagda.md | 27 ++- .../Test/Prelude.agda:Zone.Identifier | Bin 0 -> 25 bytes .../Specification/Test/Prelude.lagda.md | 1 - .../Test/StructuredContracts.lagda.md | 61 ++--- .../StructuredContracts.lagda:Zone.Identifier | Bin 0 -> 25 bytes .../Specification/Test/SymbolicData.agda | 78 ++++++ .../Test/SymbolicData.agda:Zone.Identifier | Bin 0 -> 25 bytes .../Utxow/Properties/Computational.lagda.md | 3 +- 107 files changed, 3544 insertions(+), 89 deletions(-) create mode 100644 src/Ledger/Conway/Specification/ScriptPurpose.agda create mode 100644 src/Ledger/Conway/Specification/ScriptPurpose.agda:Zone.Identifier create mode 100644 src/Ledger/Conway/Specification/Test/AbstractImplementation.agda create mode 100644 src/Ledger/Conway/Specification/Test/AbstractImplementation.agda:Zone.Identifier create mode 100644 src/Ledger/Conway/Specification/Test/Examples.agda:Zone.Identifier create mode 100644 src/Ledger/Conway/Specification/Test/Examples/AccountSim/Datum.agda create mode 100644 src/Ledger/Conway/Specification/Test/Examples/AccountSim/Datum.agda:Zone.Identifier create mode 100644 src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Cleanup.agda create mode 100644 src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Cleanup.agda:Zone.Identifier create mode 100644 src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Close.agda create mode 100644 src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Close.agda:Zone.Identifier create mode 100644 src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Deposit.agda create mode 100644 src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Deposit.agda:Zone.Identifier create mode 100644 src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Lib.agda create mode 100644 src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Lib.agda:Zone.Identifier create mode 100644 src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/OffChain.agda create mode 100644 src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/OffChain.agda:Zone.Identifier create mode 100644 src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Open.agda create mode 100644 src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Open.agda:Zone.Identifier create mode 100644 src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Start.agda create mode 100644 src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Start.agda:Zone.Identifier create mode 100644 src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Transfer.agda create mode 100644 src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Transfer.agda:Zone.Identifier create mode 100644 src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Withdraw.agda create mode 100644 src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Withdraw.agda:Zone.Identifier create mode 100644 src/Ledger/Conway/Specification/Test/Examples/AccountSim/Test/Trace.agda create mode 100644 src/Ledger/Conway/Specification/Test/Examples/AccountSim/Test/Trace.agda:Zone.Identifier create mode 100644 src/Ledger/Conway/Specification/Test/Examples/AccountSim/Validator.agda create mode 100644 src/Ledger/Conway/Specification/Test/Examples/AccountSim/Validator.agda:Zone.Identifier create mode 100644 src/Ledger/Conway/Specification/Test/Examples/DEx/Datum.agda create mode 100644 src/Ledger/Conway/Specification/Test/Examples/DEx/Datum.agda:Zone.Identifier create mode 100644 src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/Close.agda create mode 100644 src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/Close.agda:Zone.Identifier create mode 100644 src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/Exchange.agda create mode 100644 src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/Exchange.agda:Zone.Identifier create mode 100644 src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/Lib.agda create mode 100644 src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/Lib.agda:Zone.Identifier create mode 100644 src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/OffChain.agda create mode 100644 src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/OffChain.agda:Zone.Identifier create mode 100644 src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/Start.agda create mode 100644 src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/Start.agda:Zone.Identifier create mode 100644 src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/Update.agda create mode 100644 src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/Update.agda:Zone.Identifier create mode 100644 src/Ledger/Conway/Specification/Test/Examples/DEx/Test/Trace.agda create mode 100644 src/Ledger/Conway/Specification/Test/Examples/DEx/Test/Trace.agda:Zone.Identifier create mode 100644 src/Ledger/Conway/Specification/Test/Examples/DEx/Validator.agda create mode 100644 src/Ledger/Conway/Specification/Test/Examples/DEx/Validator.agda:Zone.Identifier create mode 100644 src/Ledger/Conway/Specification/Test/Examples/HelloWorld.agda:Zone.Identifier create mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSig/Datum.agda create mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSig/Datum.agda:Zone.Identifier create mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/AddSig.agda create mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/AddSig.agda:Zone.Identifier create mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/Lib.agda create mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/Lib.agda:Zone.Identifier create mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/OffChain.agda create mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/OffChain.agda:Zone.Identifier create mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/Open.agda create mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/Open.agda:Zone.Identifier create mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/Pay.agda create mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/Pay.agda:Zone.Identifier create mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/Propose.agda create mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/Propose.agda:Zone.Identifier create mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSig/Test/Trace.agda create mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSig/Test/Trace.agda:Zone.Identifier create mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSig/Validator.agda create mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSig/Validator.agda:Zone.Identifier create mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/Datum.agda create mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/Datum.agda:Zone.Identifier create mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/AddSig.agda create mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/AddSig.agda:Zone.Identifier create mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Cancel.agda create mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Cancel.agda:Zone.Identifier create mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Cleanup.agda create mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Cleanup.agda:Zone.Identifier create mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Lib.agda create mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Lib.agda:Zone.Identifier create mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/OffChain.agda create mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/OffChain.agda:Zone.Identifier create mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Open.agda create mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Open.agda:Zone.Identifier create mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Pay.agda create mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Pay.agda:Zone.Identifier create mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Propose.agda create mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Propose.agda:Zone.Identifier create mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/Test/Trace.agda create mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/Test/Trace.agda:Zone.Identifier create mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/Validator.agda create mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/Validator.agda:Zone.Identifier create mode 100644 src/Ledger/Conway/Specification/Test/Examples/SucceedIfNumber.agda:Zone.Identifier create mode 100644 src/Ledger/Conway/Specification/Test/LedgerImplementation.agda:Zone.Identifier create mode 100644 src/Ledger/Conway/Specification/Test/Lib.agda:Zone.Identifier create mode 100644 src/Ledger/Conway/Specification/Test/Prelude.agda:Zone.Identifier create mode 100644 src/Ledger/Conway/Specification/Test/StructuredContracts.lagda:Zone.Identifier create mode 100644 src/Ledger/Conway/Specification/Test/SymbolicData.agda create mode 100644 src/Ledger/Conway/Specification/Test/SymbolicData.agda:Zone.Identifier diff --git a/src/Ledger/Conway/Foreign/HSLedger/ExternalStructures.agda b/src/Ledger/Conway/Foreign/HSLedger/ExternalStructures.agda index 363a46197..e7b6ec3e8 100644 --- a/src/Ledger/Conway/Foreign/HSLedger/ExternalStructures.agda +++ b/src/Ledger/Conway/Foreign/HSLedger/ExternalStructures.agda @@ -127,6 +127,7 @@ instance ; scriptSize = λ where (inj₁ x) → HSTimelock.tlScriptSize x (inj₂ x) → HSPlutusScript.psScriptSize x + ; valContext = λ _ _ → zero } open import Ledger.Core.Specification.Address Network KeyHash ScriptHash using () public diff --git a/src/Ledger/Conway/Specification/Abstract.lagda.md b/src/Ledger/Conway/Specification/Abstract.lagda.md index b89f9ba2d..90e6618ee 100644 --- a/src/Ledger/Conway/Specification/Abstract.lagda.md +++ b/src/Ledger/Conway/Specification/Abstract.lagda.md @@ -13,6 +13,7 @@ module Ledger.Conway.Specification.Abstract (txs : TransactionStructure) where open TransactionStructure txs open import Ledger.Conway.Specification.Certs govStructure +open import Ledger.Conway.Specification.ScriptPurpose txs record indexOf : Type where field @@ -29,4 +30,4 @@ record AbstractFunctions : Type where indexOfImp : indexOf runPLCScript : CostModel → P2Script → ExUnits → List Data → Bool scriptSize : Script → ℕ -``` + valContext : TxInfo → ScriptPurpose → Data diff --git a/src/Ledger/Conway/Specification/Script/Base.lagda.md b/src/Ledger/Conway/Specification/Script/Base.lagda.md index 4af35ccc4..85fbb6519 100644 --- a/src/Ledger/Conway/Specification/Script/Base.lagda.md +++ b/src/Ledger/Conway/Specification/Script/Base.lagda.md @@ -56,7 +56,7 @@ record PlutusStructure : Type₁ where field validPlutusScript : CostModel → List Data → ExUnits → PlutusScript → Type ⦃ Dec-validPlutusScript ⦄ : ∀ {x} → (validPlutusScript x ⁇³) language : PlutusScript → Language - toData : ∀ {A : Type} → A → Data + -- toData : ∀ {A : Type} → A → Data record ScriptStructure : Type₁ where diff --git a/src/Ledger/Conway/Specification/Script/Validation.lagda.md b/src/Ledger/Conway/Specification/Script/Validation.lagda.md index f465be2eb..3da7dbc42 100644 --- a/src/Ledger/Conway/Specification/Script/Validation.lagda.md +++ b/src/Ledger/Conway/Specification/Script/Validation.lagda.md @@ -21,21 +21,11 @@ module Ledger.Conway.Specification.Script.Validation open import Ledger.Prelude open import Ledger.Conway.Specification.Certs govStructure -``` ---> -```agda -data ScriptPurpose : Type where - Cert : DCert → ScriptPurpose - Rwrd : RwdAddr → ScriptPurpose - Mint : ScriptHash → ScriptPurpose - Spend : TxIn → ScriptPurpose - Vote : GovVoter → ScriptPurpose - Propose : GovProposal → ScriptPurpose -``` - - ```agda -record TxInfo : Type where - field realizedInputs : UTxO - txOuts : Ix ⇀ TxOut - fee : Value - mint : Value - txCerts : List DCert - txWithdrawals : Withdrawals - txVldt : Maybe Slot × Maybe Slot - vkKey : ℙ KeyHash - txdats : ℙ Datum - txId : TxId - txInfo : Language → PParams → UTxO → Tx @@ -106,8 +83,8 @@ credsNeeded utxo txb ```agda where open TxBody txb; open GovVote; open RwdAddr; open GovProposal -valContext : TxInfo → ScriptPurpose → Data -valContext txinfo sp = toData (txinfo , sp) +-- valContext : TxInfo → ScriptPurpose → Data +-- valContext txinfo sp = toData (txinfo , sp) txOutToDataHash : TxOut → Maybe DataHash txOutToDataHash (_ , _ , d , _) = d >>= isInj₂ @@ -145,4 +122,3 @@ opaque evalP2Scripts : List (P2Script × List Data × ExUnits × CostModel) → Bool evalP2Scripts = all (λ (s , d , eu , cm) → runPLCScript cm s eu d) ``` ---> diff --git a/src/Ledger/Conway/Specification/ScriptPurpose.agda b/src/Ledger/Conway/Specification/ScriptPurpose.agda new file mode 100644 index 000000000..7f1697570 --- /dev/null +++ b/src/Ledger/Conway/Specification/ScriptPurpose.agda @@ -0,0 +1,30 @@ +{-# OPTIONS --safe #-} + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction + +module Ledger.Conway.Specification.ScriptPurpose (txs : TransactionStructure) where + +open TransactionStructure txs +open import Ledger.Conway.Specification.Certs govStructure + +data ScriptPurpose : Type where + Cert : DCert → ScriptPurpose + Rwrd : RwdAddr → ScriptPurpose + Mint : ScriptHash → ScriptPurpose + Spend : TxIn → ScriptPurpose + Vote : GovVoter → ScriptPurpose + Propose : GovProposal → ScriptPurpose + +record TxInfo : Type where + field realizedInputs : UTxO + txOuts : Ix ⇀ TxOut + fee : Value + mint : Value + txCerts : List DCert + txWithdrawals : Withdrawals + txVldt : Maybe Slot × Maybe Slot + vkKey : ℙ KeyHash + txdats : ℙ Datum + txId : TxId + diff --git a/src/Ledger/Conway/Specification/ScriptPurpose.agda:Zone.Identifier b/src/Ledger/Conway/Specification/ScriptPurpose.agda:Zone.Identifier new file mode 100644 index 0000000000000000000000000000000000000000..d6c1ec682968c796b9f5e9e080cc6f674b57c766 GIT binary patch literal 25 dcma!!%Fjy;DN4*MPD?F{<>dl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2x +```agda import Ledger.Conway.Specification.Test.Examples.SucceedIfNumber import Ledger.Conway.Specification.Test.Examples.HelloWorld +import Ledger.Conway.Specification.Test.Examples.MultiSig.Datum +import Ledger.Conway.Specification.Test.Examples.MultiSig.Validator +import Ledger.Conway.Specification.Test.Examples.MultiSig.Test.Trace +import Ledger.Conway.Specification.Test.Examples.AccountSim.Datum +import Ledger.Conway.Specification.Test.Examples.AccountSim.Validator +import Ledger.Conway.Specification.Test.Examples.AccountSim.Test.Trace +import Ledger.Conway.Specification.Test.Examples.DEx.Datum +import Ledger.Conway.Specification.Test.Examples.DEx.Validator +import Ledger.Conway.Specification.Test.Examples.DEx.Test.Trace +import Ledger.Conway.Specification.Test.Examples.MultiSigV2.Datum +import Ledger.Conway.Specification.Test.Examples.MultiSigV2.Validator +import Ledger.Conway.Specification.Test.Examples.MultiSigV2.Test.Trace ``` diff --git a/src/Ledger/Conway/Specification/Test/Examples/AccountSim/Datum.agda b/src/Ledger/Conway/Specification/Test/Examples/AccountSim/Datum.agda new file mode 100644 index 000000000..3c91bb622 --- /dev/null +++ b/src/Ledger/Conway/Specification/Test/Examples/AccountSim/Datum.agda @@ -0,0 +1,30 @@ +{-# OPTIONS --safe #-} + +open import Ledger.Prelude hiding (fromList; ε); open Computational + +module Ledger.Conway.Specification.Test.Examples.AccountSim.Datum where + +open import Tactic.Derive.DecEq +open import Data.Vec as Vec + hiding (fromList) +import stdlib.Data.Vec.Instances as Vec +import Data.Vec.Relation.Binary.Pointwise.Inductive as Vec + +data Label : Set where + Always : List (ℕ × ℕ) -> Label +instance + unquoteDecl DecEq-Label = derive-DecEq + ((quote Label , DecEq-Label) ∷ []) + +data Input : Set where + Open : ℕ -> Input + Close : ℕ -> Input + Withdraw : ℕ -> ℕ -> Input + Deposit : ℕ -> ℕ -> Input + Transfer : ℕ -> ℕ -> ℕ -> Input + Cleanup : Input +instance + unquoteDecl DecEq-Input = derive-DecEq + ((quote Input , DecEq-Input) ∷ []) + +AccountSimData = Label ⊎ Input diff --git a/src/Ledger/Conway/Specification/Test/Examples/AccountSim/Datum.agda:Zone.Identifier b/src/Ledger/Conway/Specification/Test/Examples/AccountSim/Datum.agda:Zone.Identifier new file mode 100644 index 0000000000000000000000000000000000000000..d6c1ec682968c796b9f5e9e080cc6f674b57c766 GIT binary patch literal 25 dcma!!%Fjy;DN4*MPD?F{<>dl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2x ℕ -> Value +getVal (Always l) w with lookup' w l +...| nothing = emptyValue +...| just v = v + + + + diff --git a/src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Lib.agda:Zone.Identifier b/src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Lib.agda:Zone.Identifier new file mode 100644 index 0000000000000000000000000000000000000000..d6c1ec682968c796b9f5e9e080cc6f674b57c766 GIT binary patch literal 25 dcma!!%Fjy;DN4*MPD?F{<>dl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2x Value -> Tx' + transfer : ℕ -> ℕ -> Value -> Tx' + cleanup : ℕ -> Tx' + + +makeTx : UTxOState → PlutusScript → Tx' → (id : ℕ) → Maybe Tx +makeTx s script (start w v) id = just (startTx id w 999 v script) +makeTx s script (openn w) id = makeOpenTx id s script w +makeTx s script (close w) id = makeCloseTx id s script w +makeTx s script (withdraw w v) id = makeWithdrawTx id s script w v +makeTx s script (deposit w v) id = makeDepositTx id s script w v +makeTx s script (transfer from to v) id = makeTransferTx id s script from to v +makeTx s script (cleanup w) id = makeCleanupTx id s script w + + +evalTransanctions : UTxOEnv → ComputationResult String UTxOState → List Tx' → ℕ → ComputationResult String UTxOState +evalTransanctions env s [] id = s +evalTransanctions env state@(failure s) (x ∷ xs) id = state +evalTransanctions env (success s) (tx' ∷ txs') id = + maybe + (λ tx → evalTransanctions + initEnv + (UTXO-step initEnv s tx) + txs' + (suc id)) + (failure "failed to generate tx") + (makeTx s multiSigScript tx' id) + +evalTransanctionsW : UTxOEnv → ComputationResult String UTxOState → List Tx' → ℕ → ComputationResult String UTxOState +evalTransanctionsW env s [] id = s +evalTransanctionsW env state@(failure s) (x ∷ xs) id = state +evalTransanctionsW env (success s) (tx' ∷ txs') id = + maybe + (λ tx → evalTransanctions + initEnv + (UTXO-stepW initEnv s tx) + txs' + (suc id)) + (failure "failed to generate tx") + (makeTx s multiSigScript tx' id) + +validTrace : List Tx' +validTrace = start 5 (adaValueOf 80000000) + ∷ openn 1 + ∷ openn 2 + ∷ close 2 + ∷ deposit 1 (adaValueOf 2000000000) + ∷ withdraw 1 (adaValueOf 1000000000) + ∷ deposit 1 (adaValueOf 10000000) + ∷ openn 3 + ∷ deposit 3 (adaValueOf 30000000) + ∷ transfer 3 1 (adaValueOf 5000000) + ∷ [] + + +validTrace2 : List Tx' +validTrace2 = start 5 (adaValueOf 8000000000) + ∷ openn 1 + ∷ openn 2 + ∷ close 2 + ∷ deposit 1 (adaValueOf 20000000000) + ∷ withdraw 1 (adaValueOf 10000000000) + ∷ deposit 1 (adaValueOf 10000000) + ∷ deposit 1 (adaValueOf 10000000) + ∷ openn 3 + ∷ deposit 3 (adaValueOf 30000000) + ∷ transfer 1 3 (adaValueOf 5000000) + ∷ [] + + +validTrace3 : List Tx' +validTrace3 = start 5 (adaValueOf 8000000000) + ∷ openn 2 + ∷ close 2 + ∷ cleanup 5 + ∷ [] + + + +failingTrace : List Tx' +failingTrace = start 5 (adaValueOf 8000000000) + ∷ openn 1 + ∷ openn 2 + ∷ deposit 1 (adaValueOf 20000000) + ∷ withdraw 2 (adaValueOf 10000000) + ∷ [] + +opaque + unfolding collectP2ScriptsWithContext + unfolding setToList + unfolding Computational-UTXO + unfolding outs + + evalValidTrace : ComputationResult String UTxOState + evalValidTrace = evalTransanctions initEnv (success ⟦ initState' , 0 , ∅ , 0 ⟧ᵘ) validTrace 6 + + evalValidTrace2 : ComputationResult String UTxOState + evalValidTrace2 = evalTransanctionsW initEnv (success ⟦ initState' , 0 , ∅ , 0 ⟧ᵘ) validTrace2 6 + + evalValidTrace3 : ComputationResult String UTxOState + evalValidTrace3 = evalTransanctionsW initEnv (success ⟦ initState' , 0 , ∅ , 0 ⟧ᵘ) validTrace3 6 + + evalFailingTrace : ComputationResult String UTxOState + evalFailingTrace = evalTransanctionsW initEnv (success ⟦ initState' , 0 , ∅ , 0 ⟧ᵘ) failingTrace 6 + + _ : isSuccess evalValidTrace ≡ true + _ = refl + + _ : isSuccess evalValidTrace2 ≡ true + _ = refl + + _ : isSuccess evalValidTrace3 ≡ true + _ = refl + + _ : isSuccess evalFailingTrace ≡ false + _ = refl diff --git a/src/Ledger/Conway/Specification/Test/Examples/AccountSim/Test/Trace.agda:Zone.Identifier b/src/Ledger/Conway/Specification/Test/Examples/AccountSim/Test/Trace.agda:Zone.Identifier new file mode 100644 index 0000000000000000000000000000000000000000..d6c1ec682968c796b9f5e9e080cc6f674b57c766 GIT binary patch literal 25 dcma!!%Fjy;DN4*MPD?F{<>dl#JyUFr831@K2x Value +adaValueOf n = n + + +geq : Value -> Value -> Bool +geq v1 v2 = ⌊ v1 ≥? v2 ⌋ + +subVal : Value -> Value -> Value +subVal v1 v2 = v1 - v2 + +instance ValueSub : HasSubtract Value Value + ValueSub = record { _-_ = λ x y → subVal x y } --subVal + + +getInlineOutputDatum : STxOut → List AccountSimData → Maybe Datum +getInlineOutputDatum (a , b , just (inj₁ (inj₁ x))) dats = just (inj₁ (inj₁ x)) +getInlineOutputDatum (a , b , just (inj₁ (inj₂ y))) dats = nothing +getInlineOutputDatum (a , b , just (inj₂ y)) dats = nothing +getInlineOutputDatum (a , b , nothing) dats = nothing + +newLabel : ScriptContext -> Maybe Label +newLabel (record { realizedInputs = realizedInputs ; txouts = txouts ; fee = fee ; mint = mint ; txwdrls = txwdrls ; txvldt = txvldt ; vkey = vkey ; txdats = txdats ; txid = txid } , snd) with + mapMaybe (λ x → getInlineOutputDatum x txdats) (map proj₂ txouts) +... | [] = nothing +... | inj₁ (inj₁ x) ∷ [] = just x +... | _ = nothing + +continuing : ScriptContext -> Bool +continuing (record { realizedInputs = realizedInputs ; txouts = txouts ; fee = fee ; mint = mint ; txwdrls = txwdrls ; txvldt = txvldt ; vkey = vkey ; txdats = txdats ; txid = txid } , snd) with + mapMaybe (λ x → getInlineOutputDatum x txdats) (map proj₂ txouts) +... | [] = false +... | _ = true + + +getPaymentCredential : STxOut → ℕ +getPaymentCredential (inj₁ record { net = net ; pay = (KeyHashObj x) ; stake = stake } , snd) = x +getPaymentCredential (inj₁ record { net = net ; pay = (ScriptObj x) ; stake = stake } , snd) = x +getPaymentCredential (inj₂ record { net = net ; pay = (KeyHashObj x) ; attrsSize = attrsSize } , snd) = x +getPaymentCredential (inj₂ record { net = net ; pay = (ScriptObj x) ; attrsSize = attrsSize } , snd) = x + + +getScriptCredential' : ℕ → SUTxO → Maybe ℕ +getScriptCredential' ix [] = nothing +getScriptCredential' ix (((txid' , ix') , txout) ∷ utxos) with ix ≟ ix' +... | no ¬a = getScriptCredential' ix utxos +... | yes a = just (getPaymentCredential txout) + + +getScriptCredential : ScriptContext → Maybe ℕ +getScriptCredential (fst , Rwrd x) = nothing +getScriptCredential (fst , Mint x) = nothing +getScriptCredential (txinfo , Spend (txid , ix)) = getScriptCredential' ix (STxInfo.realizedInputs txinfo) +getScriptCredential (fst , Empty) = nothing + +balanceSTxOut : List STxOut → Value +balanceSTxOut txout = foldr (_+_ {{addValue}}) emptyValue (map (λ {(_ , v , _) → v}) txout) + +matchIx : ℕ → SAddr → Set +matchIx n (inj₁ record { net = net ; pay = (KeyHashObj x) ; stake = stake }) = n ≡ x +matchIx n (inj₁ record { net = net ; pay = (ScriptObj y) ; stake = stake }) = n ≡ y +matchIx n (inj₂ record { net = net ; pay = (KeyHashObj x) ; attrsSize = attrsSize }) = n ≡ x +matchIx n (inj₂ record { net = net ; pay = (ScriptObj y) ; attrsSize = attrsSize }) = n ≡ y + +matchIx? : (n : ℕ) → (a : SAddr) → Dec (matchIx n a) +matchIx? n (inj₁ record { net = net ; pay = (KeyHashObj x) ; stake = stake }) = n ≟ x +matchIx? n (inj₁ record { net = net ; pay = (ScriptObj y) ; stake = stake }) = n ≟ y +matchIx? n (inj₂ record { net = net ; pay = (KeyHashObj x) ; attrsSize = attrsSize }) = n ≟ x +matchIx? n (inj₂ record { net = net ; pay = (ScriptObj y) ; attrsSize = attrsSize }) = n ≟ y + + +totalOuts : ScriptContext → PubKeyHash → Value +totalOuts (txinfo , _) ph = balanceSTxOut (filter (λ { (fst , snd) → matchIx? ph fst}) (map proj₂ (STxInfo.txouts txinfo))) + +totalIns : ScriptContext → PubKeyHash → Value +totalIns (txinfo , _) ph = balanceSTxOut (filter (λ { (fst , snd) → matchIx? ph fst}) (map proj₂ (STxInfo.realizedInputs txinfo))) + +-- Get the value of txouts for own script +newValue : ScriptContext → Maybe Value +newValue sc@(txinfo , sp) with getScriptCredential sc +... | nothing = nothing +... | just sh = just (totalOuts sc sh) + +oldValue : ScriptContext → Maybe Value +oldValue sc@(txinfo , sp) with getScriptCredential sc +... | nothing = nothing +... | just sh = just (totalIns sc sh) + + +open import Relation.Nullary.Decidable + +checkSigned : PubKeyHash → ScriptContext → Bool +checkSigned ph (txinfo , _) = ⌊ (ph ∈? (STxInfo.vkey txinfo)) ⌋ + +query : PubKeyHash → List PubKeyHash → Bool +query ph xs = any (λ k → ⌊ ph ≟ k ⌋) xs + +checkPayment : PubKeyHash -> Value -> ScriptContext -> Bool +checkPayment pkh v ctx = ⌊ totalOuts ctx pkh ≟ (_+_ {{addValue}} (totalIns ctx pkh) v) ⌋ + +expired : ℕ -> ScriptContext -> Bool +expired slot (txinfo , _) = maybe (λ deadline → ⌊ slot >? deadline ⌋) + false + (proj₂ (STxInfo.txvldt txinfo)) + + + +checkMembership : Maybe Value -> Bool +checkMembership (just x) = true +checkMembership nothing = false + +checkEmpty : Maybe Value -> Bool +checkEmpty (just x) = x == emptyValue +checkEmpty nothing = false + +insert' : PubKeyHash -> Value -> List (ℕ × Value) -> List (ℕ × Value) +insert' pkh val [] = ((pkh , val) ∷ []) +insert' pkh val ((x , y) ∷ xs) = if (pkh == x) then ((pkh , val) ∷ xs) else ((x , y) ∷ (insert' pkh val xs)) + +delete' : PubKeyHash -> List (ℕ × Value) -> List (ℕ × Value) +delete' pkh [] = [] +delete' pkh ((x , y) ∷ xs) = if (pkh == x) + then xs + else ((x , y) ∷ (delete' pkh xs)) + +lookup' : ℕ → List (ℕ × Value) → Maybe Value +lookup' x [] = nothing +lookup' x ((x₁ , y) ∷ xs) = if x == x₁ then just y else lookup' x xs + + + +checkWithdraw : Maybe Value -> ℕ -> Value -> Label -> ScriptContext -> Bool +checkWithdraw nothing _ _ _ _ = false +checkWithdraw (just v) pkh val (Always lab) ctx = geq val emptyValue && geq v val && (newLabel ctx == just (Always (insert' pkh (v - val) lab))) + +checkDeposit : Maybe Value -> ℕ -> Value -> Label -> ScriptContext -> Bool +checkDeposit nothing _ _ _ _ = false +checkDeposit (just v) pkh val (Always lab) ctx = geq val emptyValue && (newLabel ctx == just ( Always (insert' pkh (_+_ {{addValue}} v val) lab))) + +checkTransfer : Maybe Value -> Maybe Value -> ℕ -> ℕ -> Value -> Label -> ScriptContext -> Bool +checkTransfer nothing _ _ _ _ _ _ = false +checkTransfer (just vF) nothing _ _ _ _ _ = false +checkTransfer (just vF) (just vT) from to val (Always lab) ctx = geq val emptyValue && geq vF val && (from ≠ to) && (newLabel ctx == just (Always (insert' from (vF - val) (insert' to (_+_ {{addValue}} vT val) lab)))) + +agdaValidator : Label -> Input -> ScriptContext -> Bool +agdaValidator (Always lab) inp ctx = case inp of λ where + + (Open pkh) -> continuing ctx && (checkSigned pkh ctx) && (not (checkMembership (lookup' pkh lab))) && + (newLabel ctx == just (Always (insert' pkh emptyValue lab))) && (newValue ctx == oldValue ctx) + + (Close pkh) -> continuing ctx && (checkSigned pkh ctx) && (checkEmpty (lookup' pkh lab)) && + (newLabel ctx == just (Always (delete' pkh lab))) && (newValue ctx == oldValue ctx) + + (Withdraw pkh val) -> continuing ctx && (checkSigned pkh ctx) && (checkWithdraw (lookup' pkh lab) pkh val (Always lab) ctx) && + ((maybeMap (_+_ {{addValue}} val) (newValue ctx)) == oldValue ctx ) + + (Deposit pkh val) -> continuing ctx && checkSigned pkh ctx && checkDeposit (lookup' pkh lab) pkh val (Always lab) ctx && + (newValue ctx == (maybeMap (_+_ {{addValue}} val) (oldValue ctx))) + + (Transfer from to val) -> continuing ctx && checkSigned from ctx && + checkTransfer (lookup' from lab) (lookup' to lab) from to val (Always lab) ctx && + (newValue ctx == oldValue ctx) + + Cleanup -> not (continuing ctx) && (lab == []) + + +accSimValidator : Maybe SData → Maybe SData → List SData → Bool +accSimValidator (just (inj₁ (inj₁ x))) (just (inj₁ (inj₂ y))) (inj₂ y₁ ∷ []) = + agdaValidator x y y₁ +accSimValidator _ _ _ = false + diff --git a/src/Ledger/Conway/Specification/Test/Examples/AccountSim/Validator.agda:Zone.Identifier b/src/Ledger/Conway/Specification/Test/Examples/AccountSim/Validator.agda:Zone.Identifier new file mode 100644 index 0000000000000000000000000000000000000000..d6c1ec682968c796b9f5e9e080cc6f674b57c766 GIT binary patch literal 25 dcma!!%Fjy;DN4*MPD?F{<>dl#JyUFr831@K2x ℕ -> Label +instance + unquoteDecl DecEq-Label = derive-DecEq + ((quote Label , DecEq-Label) ∷ []) + +data Input : Set where + Update : ℕ -> ℚ -> Input + Exchange : ℕ -> ℕ -> Input + Close : Input +instance + unquoteDecl DecEq-Input = derive-DecEq + ((quote Input , DecEq-Input) ∷ []) + +DExData = Label ⊎ Input diff --git a/src/Ledger/Conway/Specification/Test/Examples/DEx/Datum.agda:Zone.Identifier b/src/Ledger/Conway/Specification/Test/Examples/DEx/Datum.agda:Zone.Identifier new file mode 100644 index 0000000000000000000000000000000000000000..d6c1ec682968c796b9f5e9e080cc6f674b57c766 GIT binary patch literal 25 dcma!!%Fjy;DN4*MPD?F{<>dl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2x ℕ -> Value +getVal (Always l) w with lookup' w l +...| nothing = emptyValue +...| just v = v +-} + + + diff --git a/src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/Lib.agda:Zone.Identifier b/src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/Lib.agda:Zone.Identifier new file mode 100644 index 0000000000000000000000000000000000000000..d6c1ec682968c796b9f5e9e080cc6f674b57c766 GIT binary patch literal 25 dcma!!%Fjy;DN4*MPD?F{<>dl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2x (d Data.Nat.Divisibility.Core.∣ 1) -> d ≡ 1 +pf {zero} (divides quotient equality) rewrite *-comm quotient zero = sym equality +pf {suc d} (divides (suc zero) eq) rewrite +-comm d 0 = sym eq +pf {suc zero} (divides (2+ q) ()) +pf {2+ d} (divides (2+ q) ()) + +rate : Q.ℚ +rate = (Q.mkℚ (ℤ.pos (suc zero)) zero (λ { (fst , snd) → pf fst }) ) + +rate2 : Q.ℚ +rate2 = (Q.mkℚ (ℤ.pos (suc zero)) (suc zero) (λ { (fst , snd) → pf fst }) ) + +rate3 : Q.ℚ +rate3 = (Q.mkℚ (ℤ.pos (suc (suc (suc zero)))) (zero) (λ { (fst , snd) → pf snd }) ) + +validTrace : List Tx' +validTrace = start 5 (adaValueOf 80000000) rate + ∷ updatetx 5 (adaValueOf 70000000) rate + ∷ close 5 + ∷ [] + + +validTrace2 : List Tx' +validTrace2 = start 5 (adaValueOf 8000000000) rate + ∷ exchange 1 (adaValueOf 70000000) --FIX + ∷ [] + + + +failingTrace : List Tx' +failingTrace = start 5 (adaValueOf 8000000000) rate + ∷ updatetx 1 (adaValueOf 40000000) rate3 + ∷ [] + +opaque + unfolding collectP2ScriptsWithContext + unfolding setToList + unfolding Computational-UTXO + unfolding outs + + evalValidTrace : ComputationResult String UTxOState + evalValidTrace = evalTransanctionsW initEnv (success ⟦ initState' , 0 , ∅ , 0 ⟧ᵘ) validTrace 6 + + evalValidTrace2 : ComputationResult String UTxOState + evalValidTrace2 = evalTransanctionsW initEnv (success ⟦ initState' , 0 , ∅ , 0 ⟧ᵘ) validTrace2 6 + + evalFailingTrace : ComputationResult String UTxOState + evalFailingTrace = evalTransanctionsW initEnv (success ⟦ initState' , 0 , ∅ , 0 ⟧ᵘ) failingTrace 6 + + _ : isSuccess evalValidTrace ≡ true + _ = refl + + _ : isSuccess evalValidTrace2 ≡ true + _ = refl + + _ : isSuccess evalFailingTrace ≡ false + _ = refl diff --git a/src/Ledger/Conway/Specification/Test/Examples/DEx/Test/Trace.agda:Zone.Identifier b/src/Ledger/Conway/Specification/Test/Examples/DEx/Test/Trace.agda:Zone.Identifier new file mode 100644 index 0000000000000000000000000000000000000000..d6c1ec682968c796b9f5e9e080cc6f674b57c766 GIT binary patch literal 25 dcma!!%Fjy;DN4*MPD?F{<>dl#JyUFr831@K2x Value +adaValueOf n = n + + +geq : Value -> Value -> Bool +geq v1 v2 = ⌊ v1 ≥? v2 ⌋ + +subVal : Value -> Value -> Value +subVal v1 v2 = v1 - v2 + +instance ValueSub : HasSubtract Value Value + ValueSub = record { _-_ = λ x y → subVal x y } --subVal + + + +record Params : Set where + field + sellC : ℕ + buyC : ℕ + + +getInlineOutputDatum : STxOut → List DExData → Maybe Datum +getInlineOutputDatum (a , b , just (inj₁ (inj₁ x))) dats = just (inj₁ (inj₁ x)) +getInlineOutputDatum (a , b , just (inj₁ (inj₂ y))) dats = nothing +getInlineOutputDatum (a , b , just (inj₂ y)) dats = nothing +getInlineOutputDatum (a , b , nothing) dats = nothing + +newLabel : ScriptContext -> Maybe Label +newLabel (record { realizedInputs = realizedInputs ; txouts = txouts ; fee = fee ; mint = mint ; txwdrls = txwdrls ; txvldt = txvldt ; vkey = vkey ; txdats = txdats ; txid = txid } , snd) with + mapMaybe (λ x → getInlineOutputDatum x txdats) (map proj₂ txouts) +... | [] = nothing +... | inj₁ (inj₁ x) ∷ [] = just x +... | _ = nothing + +continuing : ScriptContext -> Bool +continuing (record { realizedInputs = realizedInputs ; txouts = txouts ; fee = fee ; mint = mint ; txwdrls = txwdrls ; txvldt = txvldt ; vkey = vkey ; txdats = txdats ; txid = txid } , snd) with + mapMaybe (λ x → getInlineOutputDatum x txdats) (map proj₂ txouts) +... | [] = false +... | _ = true + +getPaymentCredential : STxOut → ℕ +getPaymentCredential (inj₁ record { net = net ; pay = (KeyHashObj x) ; stake = stake } , snd) = x +getPaymentCredential (inj₁ record { net = net ; pay = (ScriptObj x) ; stake = stake } , snd) = x +getPaymentCredential (inj₂ record { net = net ; pay = (KeyHashObj x) ; attrsSize = attrsSize } , snd) = x +getPaymentCredential (inj₂ record { net = net ; pay = (ScriptObj x) ; attrsSize = attrsSize } , snd) = x + +getScriptCredential' : ℕ → SUTxO → Maybe ℕ +getScriptCredential' ix [] = nothing +getScriptCredential' ix (((txid' , ix') , txout) ∷ utxos) with ix ≟ ix' +... | no ¬a = getScriptCredential' ix utxos +... | yes a = just (getPaymentCredential txout) + +getScriptCredential : ScriptContext → Maybe ℕ +getScriptCredential (fst , Rwrd x) = nothing +getScriptCredential (fst , Mint x) = nothing +getScriptCredential (txinfo , Spend (txid , ix)) = getScriptCredential' ix (STxInfo.realizedInputs txinfo) +getScriptCredential (fst , Empty) = nothing + +balanceSTxOut : List STxOut → Value +balanceSTxOut txout = foldr (_+_ {{addValue}}) emptyValue (map (λ {(_ , v , _) → v}) txout) + +matchIx : ℕ → SAddr → Set +matchIx n (inj₁ record { net = net ; pay = (KeyHashObj x) ; stake = stake }) = n ≡ x +matchIx n (inj₁ record { net = net ; pay = (ScriptObj y) ; stake = stake }) = n ≡ y +matchIx n (inj₂ record { net = net ; pay = (KeyHashObj x) ; attrsSize = attrsSize }) = n ≡ x +matchIx n (inj₂ record { net = net ; pay = (ScriptObj y) ; attrsSize = attrsSize }) = n ≡ y + +matchIx? : (n : ℕ) → (a : SAddr) → Dec (matchIx n a) +matchIx? n (inj₁ record { net = net ; pay = (KeyHashObj x) ; stake = stake }) = n ≟ x +matchIx? n (inj₁ record { net = net ; pay = (ScriptObj y) ; stake = stake }) = n ≟ y +matchIx? n (inj₂ record { net = net ; pay = (KeyHashObj x) ; attrsSize = attrsSize }) = n ≟ x +matchIx? n (inj₂ record { net = net ; pay = (ScriptObj y) ; attrsSize = attrsSize }) = n ≟ y + + +totalOuts : ScriptContext → PubKeyHash → Value +totalOuts (txinfo , _) ph = balanceSTxOut (filter (λ { (fst , snd) → matchIx? ph fst}) (map proj₂ (STxInfo.txouts txinfo))) + +totalIns : ScriptContext → PubKeyHash → Value +totalIns (txinfo , _) ph = balanceSTxOut (filter (λ { (fst , snd) → matchIx? ph fst}) (map proj₂ (STxInfo.realizedInputs txinfo))) + +newValue : ScriptContext → Maybe Value +newValue sc@(txinfo , sp) with getScriptCredential sc +... | nothing = nothing +... | just sh = just (totalOuts sc sh) + +oldValue : ScriptContext → Maybe Value +oldValue sc@(txinfo , sp) with getScriptCredential sc +... | nothing = nothing +... | just sh = just (totalIns sc sh) + + +open import Relation.Nullary.Decidable + +checkSigned : PubKeyHash → ScriptContext → Bool +checkSigned ph (txinfo , _) = ⌊ (ph ∈? (STxInfo.vkey txinfo)) ⌋ + + +checkRational : Q.ℚ -> Bool +checkRational (Q.mkℚ (ℤ.pos n) denominator-1 isCoprime) = ⌊ n ≥? 0 ⌋ +checkRational (Q.mkℚ (ℤ.negsuc n) denominator-1 isCoprime) = false + + +checkMinValue : Value -> Bool +checkMinValue v = geq v minValue + + +ratioValue : Value -> Q.ℚ -> Value +ratioValue v (Q.mkℚ (ℤ.pos n) denominator-1 isCoprime) = N.suc ((v * n) / (N.suc denominator-1)) +ratioValue v (Q.mkℚ (ℤ.negsuc n) denominator-1 isCoprime) = N.suc ((v * n) / (N.suc denominator-1)) + +checkBuyerPayment : PubKeyHash -> Value -> Q.ℚ -> ScriptContext -> Bool +checkBuyerPayment pkh v r ctx = ⌊ totalOuts ctx pkh ≟ (_+_ {{addValue}} (((totalIns ctx pkh) - feeValue) - ratioValue v r) v) ⌋ + +checkOwnerPayment : PubKeyHash -> Value -> Q.ℚ -> ScriptContext -> Bool +checkOwnerPayment pkh v (Q.mkℚ (ℤ.pos n) denominator-1 isCoprime) ctx = + ⌊ totalOuts ctx pkh ≥? (_+_ {{addValue}} (totalIns ctx pkh) ((v * n) / (N.suc denominator-1))) ⌋ +checkOwnerPayment pkh v (Q.mkℚ (ℤ.negsuc n) denominator-1 isCoprime) ctx = false + +agdaValidator : Params -> Label -> Input -> ScriptContext -> Bool +agdaValidator par (Always q o) inp ctx = (case inp of λ where + (Update v r) -> checkSigned o ctx && checkRational r && + checkMinValue v && (newValue ctx == just v) && + (newLabel ctx == just (Always r o)) && continuing ctx + (Exchange pkh amt) -> ((oldValue ctx) == (maybeMap (_+_ {{addValue}} amt) (newValue ctx))) && + (newLabel ctx == just (Always q o)) && + checkOwnerPayment o amt q ctx && checkBuyerPayment pkh amt q ctx && + checkMinValue amt && continuing ctx + Close -> checkSigned o ctx && not (continuing ctx) ) + + +dexValidator : Params → Maybe SData → Maybe SData → List SData → Bool +dexValidator par (just (inj₁ (inj₁ x))) (just (inj₁ (inj₂ y))) (inj₂ y₁ ∷ []) = + agdaValidator par x y y₁ +dexValidator _ _ _ _ = false + diff --git a/src/Ledger/Conway/Specification/Test/Examples/DEx/Validator.agda:Zone.Identifier b/src/Ledger/Conway/Specification/Test/Examples/DEx/Validator.agda:Zone.Identifier new file mode 100644 index 0000000000000000000000000000000000000000..d6c1ec682968c796b9f5e9e080cc6f674b57c766 GIT binary patch literal 25 dcma!!%Fjy;DN4*MPD?F{<>dl#JyUFr831@K2xdl#JyUFr831@K2x ℕ -> ℕ -> List ℕ -> Label +instance + unquoteDecl DecEq-Label = derive-DecEq + ((quote Label , DecEq-Label) ∷ []) + +data Input : Set where + -- Propose: Ada amount, Target Wallet, Slot Deadline + Propose : ℕ -> ℕ -> ℕ -> Input + -- Add: Wallet signature to add + Add : ℕ -> Input + Pay : Input + Cancel : Input +instance + unquoteDecl DecEq-Input = derive-DecEq + ((quote Input , DecEq-Input) ∷ []) + +MultiSigData = Label ⊎ Input diff --git a/src/Ledger/Conway/Specification/Test/Examples/MultiSig/Datum.agda:Zone.Identifier b/src/Ledger/Conway/Specification/Test/Examples/MultiSig/Datum.agda:Zone.Identifier new file mode 100644 index 0000000000000000000000000000000000000000..d6c1ec682968c796b9f5e9e080cc6f674b57c766 GIT binary patch literal 25 dcma!!%Fjy;DN4*MPD?F{<>dl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2x Maybe Label +newLabel (record { realizedInputs = realizedInputs ; txouts = txouts ; fee = fee ; mint = mint ; txwdrls = txwdrls ; txvldt = txvldt ; vkey = vkey ; txdats = txdats ; txid = txid } , snd) with + mapMaybe (λ x → getInlineOutputDatum x txdats) (map proj₂ txouts) +... | [] = nothing +... | inj₁ (inj₁ x) ∷ [] = just x +... | _ = nothing + +-- TODO: Look into this +getPaymentCredential : STxOut → ℕ +getPaymentCredential (inj₁ record { net = net ; pay = (KeyHashObj x) ; stake = stake } , snd) = x +getPaymentCredential (inj₁ record { net = net ; pay = (ScriptObj x) ; stake = stake } , snd) = x +getPaymentCredential (inj₂ record { net = net ; pay = (KeyHashObj x) ; attrsSize = attrsSize } , snd) = x +getPaymentCredential (inj₂ record { net = net ; pay = (ScriptObj x) ; attrsSize = attrsSize } , snd) = x + +-- TODO: look into Ledger.address version of getscripthash +getScriptCredential' : ℕ → SUTxO → Maybe ℕ +getScriptCredential' ix [] = nothing +getScriptCredential' ix (((txid' , ix') , txout) ∷ utxos) with ix ≟ ix' +... | no ¬a = getScriptCredential' ix utxos +... | yes a = just (getPaymentCredential txout) + +--TODO: Handle cases other than spend +getScriptCredential : ScriptContext → Maybe ℕ +getScriptCredential (fst , Rwrd x) = nothing +getScriptCredential (fst , Mint x) = nothing +getScriptCredential (txinfo , Spend (txid , ix)) = getScriptCredential' ix (STxInfo.realizedInputs txinfo) +getScriptCredential (fst , Empty) = nothing + +balanceSTxOut : List STxOut → Value +balanceSTxOut txout = foldr (_+_ {{addValue}}) 0 (map (λ {(_ , v , _) → v}) txout) + +matchIx : ℕ → SAddr → Set +matchIx n (inj₁ record { net = net ; pay = (KeyHashObj x) ; stake = stake }) = n ≡ x +matchIx n (inj₁ record { net = net ; pay = (ScriptObj y) ; stake = stake }) = n ≡ y +matchIx n (inj₂ record { net = net ; pay = (KeyHashObj x) ; attrsSize = attrsSize }) = n ≡ x +matchIx n (inj₂ record { net = net ; pay = (ScriptObj y) ; attrsSize = attrsSize }) = n ≡ y + +matchIx? : (n : ℕ) → (a : SAddr) → Dec (matchIx n a) +matchIx? n (inj₁ record { net = net ; pay = (KeyHashObj x) ; stake = stake }) = n ≟ x +matchIx? n (inj₁ record { net = net ; pay = (ScriptObj y) ; stake = stake }) = n ≟ y +matchIx? n (inj₂ record { net = net ; pay = (KeyHashObj x) ; attrsSize = attrsSize }) = n ≟ x +matchIx? n (inj₂ record { net = net ; pay = (ScriptObj y) ; attrsSize = attrsSize }) = n ≟ y + +totalOuts : ScriptContext → PubKeyHash → Value +totalOuts (txinfo , _) ph = balanceSTxOut (filter (λ { (fst , snd) → matchIx? ph fst}) (map proj₂ (STxInfo.txouts txinfo))) + +totalIns : ScriptContext → PubKeyHash → Value +totalIns (txinfo , _) ph = balanceSTxOut (filter (λ { (fst , snd) → matchIx? ph fst}) (map proj₂ (STxInfo.realizedInputs txinfo))) + +-- Get the value of txouts for own script +newValue : ScriptContext → Maybe Value +newValue sc@(txinfo , sp) with getScriptCredential sc +... | nothing = nothing +... | just sh = just (totalOuts sc sh) + +oldValue : ScriptContext → Maybe Value +oldValue sc@(txinfo , sp) with getScriptCredential sc +... | nothing = nothing +... | just sh = just (totalIns sc sh) + +compareScriptValues : {ℓ : Level}{r : REL ℕ ℕ ℓ} → Decidable r → Maybe Value → Maybe Value → Bool +compareScriptValues r (just ov) (just nv) = ⌊ r ov nv ⌋ +compareScriptValues r _ _ = false + + +checkPayment : PubKeyHash -> Value -> ScriptContext -> Bool +checkPayment pkh v (txinfo , _) = any (λ { (fst , val , snd) → v == val}) ((filter (λ { (fst , snd) → matchIx? pkh fst}) (map proj₂ (STxInfo.txouts txinfo)))) + + +open import Relation.Nullary.Decidable + +-- I think the signatories should just contain the signature +-- The agda implementation has sig == signature ctx +checkSigned : PubKeyHash → ScriptContext → Bool +checkSigned ph (txinfo , _) = ⌊ (ph ∈? (STxInfo.vkey txinfo)) ⌋ + +query : PubKeyHash → List PubKeyHash → Bool +query ph xs = any (λ k → ⌊ ph ≟ k ⌋) xs + +--checkPayment : PubKeyHash -> Value -> ScriptContext -> Bool +--checkPayment pkh v ctx = ⌊ totalOuts ctx pkh ≟ (_+_ {{addValue}} ((totalIns ctx pkh)) v) ⌋ + + +{- +balanceSTxOut : List STxOut → Value +balanceSTxOut txout = foldr (_+_ {{addValue}}) 0 (map (λ {(_ , v , _) → v}) txout) +totalOuts : ScriptContext → PubKeyHash → Value +totalOuts (txinfo , _) ph = balanceSTxOut (filter (λ { (fst , snd) → matchIx? ph fst}) (map proj₂ (STxInfo.txouts txinfo))) + +checkPayment :: PaymentPubKeyHash -> Value -> ScriptContext -> Bool +checkPayment pkh v ctx = case filter + (\i -> (txOutAddress i == (pubKeyHashAddress (unPaymentPubKeyHash pkh)))) + (txInfoOutputs (scriptContextTxInfo ctx)) of + os -> any (\o -> txOutValue o == v) os +-} +expired : ℕ -> ScriptContext -> Bool +expired slot (txinfo , _) = maybe (λ deadline → ⌊ slot >? deadline ⌋) + false + (proj₂ (STxInfo.txvldt txinfo)) + +multiSigValidator' : MultiSig → Label → Input → ScriptContext → Bool + +multiSigValidator' param Holding (Propose v pkh slot) ctx = + (oldValue ctx == newValue ctx) ∧ + compareScriptValues _≟_ (oldValue ctx) (newValue ctx) + ∧ compareScriptValues _≥?_ (oldValue ctx) (just v) + ∧ ⌊ v ≥? 0 ⌋ + ∧ (case (newLabel ctx) of λ where + nothing → false + (just Holding) → false + (just (Collecting v' pkh' slot' sigs')) → + (v == v') + ∧ (pkh == pkh') + ∧ (slot == slot') + ∧ (sigs' == []) ) + +multiSigValidator' param Holding _ ctx = false + +multiSigValidator' param (Collecting _ _ _ _) (Propose _ _ _) ctx = false + +multiSigValidator' param (Collecting v pkh slot sigs) (Add sig) ctx = + compareScriptValues _≟_ (oldValue ctx) (newValue ctx) -- should this be equal or _≤_ + ∧ checkSigned sig ctx + ∧ query sig (MultiSig.signatories param) + ∧ (case (newLabel ctx) of λ where + nothing → false + (just Holding) → false + (just (Collecting v' pkh' slot' sigs')) → + (v == v') + ∧ (pkh == pkh') + ∧ (slot == slot') + ∧ (sigs' == sig ∷ sigs)) -- Make this an order agnostic comparison? + +multiSigValidator' param (Collecting v pkh slot sigs) Pay ctx = + ⌊ (length sigs) ≥? MultiSig.minNumSignatures param ⌋ + ∧ (case (newLabel ctx) of λ where + nothing → false + (just Holding) → checkPayment pkh v ctx + ∧ compareScriptValues _≟_ (oldValue ctx) (maybeMap (_+_ {{addValue}} v) (newValue ctx)) + + (just (Collecting _ _ _ _)) → false) + +multiSigValidator' param (Collecting v pkh slot sigs) Cancel ctx = + compareScriptValues _≟_ (oldValue ctx) (newValue ctx) + ∧ (case (newLabel ctx) of λ where + nothing → false + (just Holding) → expired slot ctx + (just (Collecting _ _ _ _)) → false) + + +multiSigValidator : MultiSig → Maybe SData → Maybe SData → List SData → Bool +multiSigValidator m (just (inj₁ (inj₁ x))) (just (inj₁ (inj₂ y))) (inj₂ y₁ ∷ []) = + multiSigValidator' m x y y₁ +multiSigValidator _ _ _ _ = false + + diff --git a/src/Ledger/Conway/Specification/Test/Examples/MultiSig/Validator.agda:Zone.Identifier b/src/Ledger/Conway/Specification/Test/Examples/MultiSig/Validator.agda:Zone.Identifier new file mode 100644 index 0000000000000000000000000000000000000000..d6c1ec682968c796b9f5e9e080cc6f674b57c766 GIT binary patch literal 25 dcma!!%Fjy;DN4*MPD?F{<>dl#JyUFr831@K2x ℕ -> ℕ -> List ℕ -> Label +instance + unquoteDecl DecEq-Label = derive-DecEq + ((quote Label , DecEq-Label) ∷ []) + +data Input : Set where + Propose : ℕ -> ℕ -> ℕ -> Input + Add : ℕ -> Input + Pay : Input + Cancel : Input + Cleanup : Input +instance + unquoteDecl DecEq-Input = derive-DecEq + ((quote Input , DecEq-Input) ∷ []) + +MultiSigData = Label ⊎ Input diff --git a/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/Datum.agda:Zone.Identifier b/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/Datum.agda:Zone.Identifier new file mode 100644 index 0000000000000000000000000000000000000000..d6c1ec682968c796b9f5e9e080cc6f674b57c766 GIT binary patch literal 25 dcma!!%Fjy;DN4*MPD?F{<>dl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2x Value +adaValueOf n = n + + +geq : Value -> Value -> Bool +geq v1 v2 = ⌊ v1 ≥? v2 ⌋ + +gt : Value -> Value -> Bool +gt v1 v2 = ⌊ v1 >? v2 ⌋ + +subVal : Value -> Value -> Value +subVal v1 v2 = v1 - v2 + +instance ValueSub : HasSubtract Value Value + ValueSub = record { _-_ = λ x y → subVal x y } + + +getInlineOutputDatum : STxOut → List MultiSigData → Maybe Datum +getInlineOutputDatum (a , b , just (inj₁ (inj₁ x))) dats = just (inj₁ (inj₁ x)) +getInlineOutputDatum (a , b , just (inj₁ (inj₂ y))) dats = nothing +getInlineOutputDatum (a , b , just (inj₂ y)) dats = nothing +getInlineOutputDatum (a , b , nothing) dats = nothing + +newLabel : ScriptContext -> Maybe Label +newLabel (record { realizedInputs = realizedInputs ; txouts = txouts ; fee = fee ; mint = mint ; txwdrls = txwdrls ; txvldt = txvldt ; vkey = vkey ; txdats = txdats ; txid = txid } , snd) with + mapMaybe (λ x → getInlineOutputDatum x txdats) (map proj₂ txouts) +... | [] = nothing +... | inj₁ (inj₁ x) ∷ [] = just x +... | _ = nothing + +continuing : ScriptContext -> Bool +continuing (record { realizedInputs = realizedInputs ; txouts = txouts ; fee = fee ; mint = mint ; txwdrls = txwdrls ; txvldt = txvldt ; vkey = vkey ; txdats = txdats ; txid = txid } , snd) with + mapMaybe (λ x → getInlineOutputDatum x txdats) (map proj₂ txouts) +... | [] = false +... | _ = true + + +getPaymentCredential : STxOut → ℕ +getPaymentCredential (inj₁ record { net = net ; pay = (KeyHashObj x) ; stake = stake } , snd) = x +getPaymentCredential (inj₁ record { net = net ; pay = (ScriptObj x) ; stake = stake } , snd) = x +getPaymentCredential (inj₂ record { net = net ; pay = (KeyHashObj x) ; attrsSize = attrsSize } , snd) = x +getPaymentCredential (inj₂ record { net = net ; pay = (ScriptObj x) ; attrsSize = attrsSize } , snd) = x + +getScriptCredential' : ℕ → SUTxO → Maybe ℕ +getScriptCredential' ix [] = nothing +getScriptCredential' ix (((txid' , ix') , txout) ∷ utxos) with ix ≟ ix' +... | no ¬a = getScriptCredential' ix utxos +... | yes a = just (getPaymentCredential txout) + +getScriptCredential : ScriptContext → Maybe ℕ +getScriptCredential (fst , Rwrd x) = nothing +getScriptCredential (fst , Mint x) = nothing +getScriptCredential (txinfo , Spend (txid , ix)) = getScriptCredential' ix (STxInfo.realizedInputs txinfo) +getScriptCredential (fst , Empty) = nothing + +balanceSTxOut : List STxOut → Value +balanceSTxOut txout = foldr (_+_ {{addValue}}) emptyValue (map (λ {(_ , v , _) → v}) txout) + +matchIx : ℕ → SAddr → Set +matchIx n (inj₁ record { net = net ; pay = (KeyHashObj x) ; stake = stake }) = n ≡ x +matchIx n (inj₁ record { net = net ; pay = (ScriptObj y) ; stake = stake }) = n ≡ y +matchIx n (inj₂ record { net = net ; pay = (KeyHashObj x) ; attrsSize = attrsSize }) = n ≡ x +matchIx n (inj₂ record { net = net ; pay = (ScriptObj y) ; attrsSize = attrsSize }) = n ≡ y + +matchIx? : (n : ℕ) → (a : SAddr) → Dec (matchIx n a) +matchIx? n (inj₁ record { net = net ; pay = (KeyHashObj x) ; stake = stake }) = n ≟ x +matchIx? n (inj₁ record { net = net ; pay = (ScriptObj y) ; stake = stake }) = n ≟ y +matchIx? n (inj₂ record { net = net ; pay = (KeyHashObj x) ; attrsSize = attrsSize }) = n ≟ x +matchIx? n (inj₂ record { net = net ; pay = (ScriptObj y) ; attrsSize = attrsSize }) = n ≟ y + + +totalOuts : ScriptContext → PubKeyHash → Value +totalOuts (txinfo , _) ph = balanceSTxOut (filter (λ { (fst , snd) → matchIx? ph fst}) (map proj₂ (STxInfo.txouts txinfo))) + +totalIns : ScriptContext → PubKeyHash → Value +totalIns (txinfo , _) ph = balanceSTxOut (filter (λ { (fst , snd) → matchIx? ph fst}) (map proj₂ (STxInfo.realizedInputs txinfo))) + + +newValue : ScriptContext → Maybe Value +newValue sc@(txinfo , sp) with getScriptCredential sc +... | nothing = nothing +... | just sh = just (totalOuts sc sh) + +oldValue : ScriptContext → Maybe Value +oldValue sc@(txinfo , sp) with getScriptCredential sc +... | nothing = nothing +... | just sh = just (totalIns sc sh) + +insert' : PubKeyHash -> List PubKeyHash -> List PubKeyHash +insert' pkh [] = (pkh ∷ []) +insert' pkh (x ∷ l') = if (pkh == x) + then (x ∷ l') + else (x ∷ (insert' pkh l')) + +open import Relation.Nullary.Decidable + +checkSigned : PubKeyHash → ScriptContext → Bool +checkSigned ph (txinfo , _) = ⌊ (ph ∈? (STxInfo.vkey txinfo)) ⌋ + +query : PubKeyHash → List PubKeyHash → Bool +query ph xs = any (λ k → ⌊ ph ≟ k ⌋) xs + +checkPayment : PubKeyHash -> Value -> ScriptContext -> Bool +checkPayment pkh v ctx = if checkSigned pkh ctx + then ⌊ totalOuts ctx pkh ≟ ((_+_ {{addValue}} (totalIns ctx pkh) v) - feeValue) ⌋ + else ⌊ totalOuts ctx pkh ≟ (_+_ {{addValue}} (totalIns ctx pkh) v) ⌋ + + +expired : ℕ -> ScriptContext -> Bool +expired deadline (txinfo , _) = maybe (λ slot → ⌊ slot ≥? deadline ⌋) + false + (proj₁ (STxInfo.txvldt txinfo)) + + +notTooLate : Params -> ℕ -> ScriptContext -> Bool +notTooLate par deadline (txinfo , _) = maybe (λ now → ⌊ (_+_ {{addNat}} now (maxWait par)) >? deadline ⌋) + false + (proj₂ (STxInfo.txvldt txinfo)) + + + +agdaValidator : Params -> Label -> Input -> ScriptContext -> Bool +agdaValidator param lab red ctx = case (lab , red) of λ where + (Holding , (Propose v pkh d)) -> + (newValue ctx == oldValue ctx) && geq (fromMaybe 0 (oldValue ctx)) v && + geq v minValue && notTooLate param d ctx && continuing ctx && + (case (newLabel ctx) of λ where + (just (Collecting v' pkh' d' sigs')) -> (v == v') && (pkh == pkh') && (d == d') && (sigs' == []) + _ -> false ) + ((Collecting v pkh d sigs) , (Add sig)) -> + (newValue ctx == oldValue ctx) && checkSigned sig ctx && query sig (authSigs param) && + continuing ctx && (case (newLabel ctx) of λ where + (just (Collecting v' pkh' d' sigs')) -> (v == v') && (pkh == pkh') && (d == d') && (sigs' == insert' sig sigs) + _ -> false) + ((Collecting v pkh d sigs) , Pay) -> + geq (length sigs) (minNumSignatures param) && continuing ctx && (case (newLabel ctx) of λ where + (just Holding) -> (checkPayment pkh v ctx) && (oldValue ctx == (maybeMap (_+_ {{addValue}} v) (newValue ctx))) + _ -> false) + ((Collecting v pkh d sigs) , Cancel) -> + (newValue ctx == oldValue ctx) && continuing ctx && + (case (newLabel ctx) of λ where + (just Holding) -> expired d ctx + _ -> false) + (Holding , Cleanup) -> gt minValue (fromMaybe 0 (oldValue ctx)) && not (continuing ctx) + _ -> false + + +multiSigValidator : Params → Maybe SData → Maybe SData → List SData → Bool +multiSigValidator m (just (inj₁ (inj₁ x))) (just (inj₁ (inj₂ y))) (inj₂ y₁ ∷ []) = + agdaValidator m x y y₁ +multiSigValidator _ _ _ _ = false + + diff --git a/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/Validator.agda:Zone.Identifier b/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/Validator.agda:Zone.Identifier new file mode 100644 index 0000000000000000000000000000000000000000..d6c1ec682968c796b9f5e9e080cc6f674b57c766 GIT binary patch literal 25 dcma!!%Fjy;DN4*MPD?F{<>dl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2x - -We define an instance of the `StrucSimulation`{.AgdaRecord} record type by -implementing a stateful program on (the Agda specification of) the Cardano ledger. -The following must be specified when defining such an instance. - -1. `State`{.AgdaDatatype}: the program state type. - -2. `Input`{.AgdaDatatype}: the program input type. - -3. `STRUC`{.AgdaDatatype}: the program's small-step semantics. - -4. `πˢ`{.AgdaField}: the projection function of program state from a given - ledger state. - -5. `πⁱ`{.AgdaField}: the projection function of program input from a given - `TxInfo`{.AgdaRecord}. - -6. `simulates`{.AgdaField}: the proof obligation required for demonstrating - that data in items 1--5 are such that the state of the program as it appears - on the ledger can only be updated according to its small-step - `STRUC`{.AgdaDatatype} specification. - -```agda +\end{code} + +Defining an instance of the $\type{StrucSimulation}$ record constitutes implementing a +stateful program on (the Agda specification of) the Cardano ledger. The following +must be specified when defining such an instance: + +\begin{itemize} +\item[(i)] $\type{S}$ - the program state type +\item[(ii)] $\type{S}$ - the program input type +\item[(iii)] $\type{STRUC}$ - the program's small-step semantics +\item[(iv)] $\type{\pi^{s}}$ - projection function of program state from a given ledger state +\item[(v)] $\type{\pi^{i}}$ - projection function of program input from a given $\type{TxInfo}$ +\item[(vi)] $\type{simulates}$ - proof obligation required for demonstrating that data in (i)-(v) +is such that state of the program as it appears on the ledger can only be updated according to its +small-step $\type{STRUC}$ specification +\end{itemize} + +\begin{code} SSRel : Type → Type → Type → Type₁ SSRel Env State Input = Env → State → Input → State → Type @@ -58,17 +49,15 @@ record StrucSimulation S I (_⊢_⇀⦇_,STRUC⦈_ : SSRel ⊤ S I) : Type₁ wh field πˢ : LState → Maybe S πⁱ : TxInfo → I - -- here, add optional extra assumptions about ledger state, env, and - -- transaction that may be too difficult to prove without reasoning about - -- complete ledger traces; e.g., - -- * transaction does not re-add a UTxO entry it spends; - -- * current Slot is after the validity interval of some previous transaction + -- here, add optional extra assumptions about ledger state, env, and transaction that may be too difficult to prove without reasoning about complete ledger traces + -- e.g. transaction does not re-add a UTxO entry it spends + -- e.g. current Slot is after the validity interval of some previous transaction extraAssmp : LEnv → LState → Tx → Type _~ˢ_ : LState → S → Type -- R u ~ˢ s = πˢ u ≡ just s - -- only for PlutusV3 + -- only for PlutusV3 _~ᵉ_ : LEnv × Tx × LState → ⊤ × I → Type _~ᵉ_ = λ (le , tx , u) (tt , i) → πⁱ (txInfo PlutusV3 (PParamsOf le) (UTxOOf u) tx) ≡ i @@ -80,4 +69,4 @@ record StrucSimulation S I (_⊢_⇀⦇_,STRUC⦈_ : SSRel ⊤ S I) : Type₁ wh ──────────────────────────────── ∃[ s′ ] u′ ~ˢ s′ × tt ⊢ s ⇀⦇ i′ ,STRUC⦈ s′ -``` +\end{code} diff --git a/src/Ledger/Conway/Specification/Test/StructuredContracts.lagda:Zone.Identifier b/src/Ledger/Conway/Specification/Test/StructuredContracts.lagda:Zone.Identifier new file mode 100644 index 0000000000000000000000000000000000000000..d6c1ec682968c796b9f5e9e080cc6f674b57c766 GIT binary patch literal 25 dcma!!%Fjy;DN4*MPD?F{<>dl#JyUFr831@K2xdl#JyUFr831@K2x Date: Fri, 17 Oct 2025 13:46:26 +0100 Subject: [PATCH 02/11] Removed useless WSL Zone.Identifier artifacts --- .../ScriptPurpose.agda:Zone.Identifier | Bin 25 -> 0 bytes .../AbstractImplementation.agda:Zone.Identifier | Bin 25 -> 0 bytes .../Test/Examples.agda:Zone.Identifier | Bin 25 -> 0 bytes .../Examples/AccountSim/Datum.agda:Zone.Identifier | Bin 25 -> 0 bytes .../OffChain/Cleanup.agda:Zone.Identifier | Bin 25 -> 0 bytes .../AccountSim/OffChain/Close.agda:Zone.Identifier | Bin 25 -> 0 bytes .../OffChain/Deposit.agda:Zone.Identifier | Bin 25 -> 0 bytes .../AccountSim/OffChain/Lib.agda:Zone.Identifier | Bin 25 -> 0 bytes .../OffChain/OffChain.agda:Zone.Identifier | Bin 25 -> 0 bytes .../AccountSim/OffChain/Open.agda:Zone.Identifier | Bin 25 -> 0 bytes .../AccountSim/OffChain/Start.agda:Zone.Identifier | Bin 25 -> 0 bytes .../OffChain/Transfer.agda:Zone.Identifier | Bin 25 -> 0 bytes .../OffChain/Withdraw.agda:Zone.Identifier | Bin 25 -> 0 bytes .../AccountSim/Test/Trace.agda:Zone.Identifier | Bin 25 -> 0 bytes .../AccountSim/Validator.agda:Zone.Identifier | Bin 25 -> 0 bytes .../Test/Examples/DEx/Datum.agda:Zone.Identifier | Bin 25 -> 0 bytes .../DEx/OffChain/Close.agda:Zone.Identifier | Bin 25 -> 0 bytes .../DEx/OffChain/Exchange.agda:Zone.Identifier | Bin 25 -> 0 bytes .../Examples/DEx/OffChain/Lib.agda:Zone.Identifier | Bin 25 -> 0 bytes .../DEx/OffChain/OffChain.agda:Zone.Identifier | Bin 25 -> 0 bytes .../DEx/OffChain/Start.agda:Zone.Identifier | Bin 25 -> 0 bytes .../DEx/OffChain/Update.agda:Zone.Identifier | Bin 25 -> 0 bytes .../Examples/DEx/Test/Trace.agda:Zone.Identifier | Bin 25 -> 0 bytes .../Examples/DEx/Validator.agda:Zone.Identifier | Bin 25 -> 0 bytes .../Test/Examples/HelloWorld.agda:Zone.Identifier | Bin 25 -> 0 bytes .../Examples/MultiSig/Datum.agda:Zone.Identifier | Bin 25 -> 0 bytes .../MultiSig/OffChain/AddSig.agda:Zone.Identifier | Bin 25 -> 0 bytes .../MultiSig/OffChain/Lib.agda:Zone.Identifier | Bin 25 -> 0 bytes .../OffChain/OffChain.agda:Zone.Identifier | Bin 25 -> 0 bytes .../MultiSig/OffChain/Open.agda:Zone.Identifier | Bin 25 -> 0 bytes .../MultiSig/OffChain/Pay.agda:Zone.Identifier | Bin 25 -> 0 bytes .../MultiSig/OffChain/Propose.agda:Zone.Identifier | Bin 25 -> 0 bytes .../MultiSig/Test/Trace.agda:Zone.Identifier | Bin 25 -> 0 bytes .../MultiSig/Validator.agda:Zone.Identifier | Bin 25 -> 0 bytes .../Examples/MultiSigV2/Datum.agda:Zone.Identifier | Bin 25 -> 0 bytes .../OffChain/AddSig.agda:Zone.Identifier | Bin 25 -> 0 bytes .../OffChain/Cancel.agda:Zone.Identifier | Bin 25 -> 0 bytes .../OffChain/Cleanup.agda:Zone.Identifier | Bin 25 -> 0 bytes .../MultiSigV2/OffChain/Lib.agda:Zone.Identifier | Bin 25 -> 0 bytes .../OffChain/OffChain.agda:Zone.Identifier | Bin 25 -> 0 bytes .../MultiSigV2/OffChain/Open.agda:Zone.Identifier | Bin 25 -> 0 bytes .../MultiSigV2/OffChain/Pay.agda:Zone.Identifier | Bin 25 -> 0 bytes .../OffChain/Propose.agda:Zone.Identifier | Bin 25 -> 0 bytes .../MultiSigV2/Test/Trace.agda:Zone.Identifier | Bin 25 -> 0 bytes .../MultiSigV2/Validator.agda:Zone.Identifier | Bin 25 -> 0 bytes .../Examples/SucceedIfNumber.agda:Zone.Identifier | Bin 25 -> 0 bytes .../Test/LedgerImplementation.agda:Zone.Identifier | Bin 25 -> 0 bytes .../Specification/Test/Lib.agda:Zone.Identifier | Bin 25 -> 0 bytes .../Test/Prelude.agda:Zone.Identifier | Bin 25 -> 0 bytes .../Test/StructuredContracts.lagda:Zone.Identifier | Bin 25 -> 0 bytes .../Test/SymbolicData.agda:Zone.Identifier | Bin 25 -> 0 bytes 51 files changed, 0 insertions(+), 0 deletions(-) delete mode 100644 src/Ledger/Conway/Specification/ScriptPurpose.agda:Zone.Identifier delete mode 100644 src/Ledger/Conway/Specification/Test/AbstractImplementation.agda:Zone.Identifier delete mode 100644 src/Ledger/Conway/Specification/Test/Examples.agda:Zone.Identifier delete mode 100644 src/Ledger/Conway/Specification/Test/Examples/AccountSim/Datum.agda:Zone.Identifier delete mode 100644 src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Cleanup.agda:Zone.Identifier delete mode 100644 src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Close.agda:Zone.Identifier delete mode 100644 src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Deposit.agda:Zone.Identifier delete mode 100644 src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Lib.agda:Zone.Identifier delete mode 100644 src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/OffChain.agda:Zone.Identifier delete mode 100644 src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Open.agda:Zone.Identifier delete mode 100644 src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Start.agda:Zone.Identifier delete mode 100644 src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Transfer.agda:Zone.Identifier delete mode 100644 src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Withdraw.agda:Zone.Identifier delete mode 100644 src/Ledger/Conway/Specification/Test/Examples/AccountSim/Test/Trace.agda:Zone.Identifier delete mode 100644 src/Ledger/Conway/Specification/Test/Examples/AccountSim/Validator.agda:Zone.Identifier delete mode 100644 src/Ledger/Conway/Specification/Test/Examples/DEx/Datum.agda:Zone.Identifier delete mode 100644 src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/Close.agda:Zone.Identifier delete mode 100644 src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/Exchange.agda:Zone.Identifier delete mode 100644 src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/Lib.agda:Zone.Identifier delete mode 100644 src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/OffChain.agda:Zone.Identifier delete mode 100644 src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/Start.agda:Zone.Identifier delete mode 100644 src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/Update.agda:Zone.Identifier delete mode 100644 src/Ledger/Conway/Specification/Test/Examples/DEx/Test/Trace.agda:Zone.Identifier delete mode 100644 src/Ledger/Conway/Specification/Test/Examples/DEx/Validator.agda:Zone.Identifier delete mode 100644 src/Ledger/Conway/Specification/Test/Examples/HelloWorld.agda:Zone.Identifier delete mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSig/Datum.agda:Zone.Identifier delete mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/AddSig.agda:Zone.Identifier delete mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/Lib.agda:Zone.Identifier delete mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/OffChain.agda:Zone.Identifier delete mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/Open.agda:Zone.Identifier delete mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/Pay.agda:Zone.Identifier delete mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/Propose.agda:Zone.Identifier delete mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSig/Test/Trace.agda:Zone.Identifier delete mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSig/Validator.agda:Zone.Identifier delete mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/Datum.agda:Zone.Identifier delete mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/AddSig.agda:Zone.Identifier delete mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Cancel.agda:Zone.Identifier delete mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Cleanup.agda:Zone.Identifier delete mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Lib.agda:Zone.Identifier delete mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/OffChain.agda:Zone.Identifier delete mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Open.agda:Zone.Identifier delete mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Pay.agda:Zone.Identifier delete mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Propose.agda:Zone.Identifier delete mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/Test/Trace.agda:Zone.Identifier delete mode 100644 src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/Validator.agda:Zone.Identifier delete mode 100644 src/Ledger/Conway/Specification/Test/Examples/SucceedIfNumber.agda:Zone.Identifier delete mode 100644 src/Ledger/Conway/Specification/Test/LedgerImplementation.agda:Zone.Identifier delete mode 100644 src/Ledger/Conway/Specification/Test/Lib.agda:Zone.Identifier delete mode 100644 src/Ledger/Conway/Specification/Test/Prelude.agda:Zone.Identifier delete mode 100644 src/Ledger/Conway/Specification/Test/StructuredContracts.lagda:Zone.Identifier delete mode 100644 src/Ledger/Conway/Specification/Test/SymbolicData.agda:Zone.Identifier diff --git a/src/Ledger/Conway/Specification/ScriptPurpose.agda:Zone.Identifier b/src/Ledger/Conway/Specification/ScriptPurpose.agda:Zone.Identifier deleted file mode 100644 index d6c1ec682968c796b9f5e9e080cc6f674b57c766..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 25 dcma!!%Fjy;DN4*MPD?F{<>dl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2xdl#JyUFr831@K2x Date: Fri, 17 Oct 2025 15:52:38 +0100 Subject: [PATCH 03/11] Fixing the Djikstra CI error --- outputs | 1 + src/Ledger/Dijkstra/Specification/Script/Validation.lagda.md | 4 ++-- 2 files changed, 3 insertions(+), 2 deletions(-) create mode 120000 outputs diff --git a/outputs b/outputs new file mode 120000 index 000000000..4838095c3 --- /dev/null +++ b/outputs @@ -0,0 +1 @@ +/nix/store/5gvfvar49jfdpmaivpss8dyidzp27c0z-formal-ledger-0.1 \ No newline at end of file diff --git a/src/Ledger/Dijkstra/Specification/Script/Validation.lagda.md b/src/Ledger/Dijkstra/Specification/Script/Validation.lagda.md index 4c09154b6..43bdc0ace 100644 --- a/src/Ledger/Dijkstra/Specification/Script/Validation.lagda.md +++ b/src/Ledger/Dijkstra/Specification/Script/Validation.lagda.md @@ -129,8 +129,8 @@ credsNeeded TxLevelSub utxo txb = credsNeededMinusCollateral txb ∪ mapˢ (λ (i , o) → (Spend i , payCred (proj₁ o))) ((utxo ∣ txIns) ˢ) where open TxBody txb -valContext : TxInfo → ScriptPurpose → Data -valContext txinfo sp = toData (txinfo , sp) +--valContext : TxInfo → ScriptPurpose → Data +--valContext txinfo sp = toData (txinfo , sp) txOutToDataHash : TxOut → Maybe DataHash txOutToDataHash (_ , _ , d , _) = d >>= isInj₂ From a969ff7b76fd1d4f5870054b14e340e6edaded1d Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Wed, 22 Oct 2025 22:22:01 -0600 Subject: [PATCH 04/11] remove accidentally added file --- outputs | 1 - 1 file changed, 1 deletion(-) delete mode 120000 outputs diff --git a/outputs b/outputs deleted file mode 120000 index 4838095c3..000000000 --- a/outputs +++ /dev/null @@ -1 +0,0 @@ -/nix/store/5gvfvar49jfdpmaivpss8dyidzp27c0z-formal-ledger-0.1 \ No newline at end of file From ea5b6ef6af18621df34807a4f15becf4c2c26d06 Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Thu, 23 Oct 2025 01:53:08 -0600 Subject: [PATCH 05/11] Refactor: reorganize files and clean up imports (for PR #955) --- .../Conway/Specification/Abstract.lagda.md | 2 +- .../ScriptPurpose.lagda.md} | 18 ++++++-- .../Specification/Script/Validation.lagda.md | 2 +- .../Test/AbstractImplementation.agda | 17 ++++---- .../Examples/AccountSim/OffChain/Cleanup.agda | 27 +++++------- .../Examples/AccountSim/OffChain/Close.agda | 34 +++++++-------- .../Examples/AccountSim/OffChain/Deposit.agda | 29 +++++-------- .../Examples/AccountSim/OffChain/Lib.agda | 27 ++++-------- .../Examples/AccountSim/OffChain/Open.agda | 36 +++++++--------- .../Examples/AccountSim/OffChain/Start.agda | 27 +++++------- .../AccountSim/OffChain/Transfer.agda | 28 +++++------- .../AccountSim/OffChain/Withdraw.agda | 27 +++++------- .../Test/Examples/AccountSim/Test/Trace.agda | 26 +++++------ .../Test/Examples/AccountSim/Validator.agda | 32 ++++---------- .../Test/Examples/DEx/OffChain/Close.agda | 27 +++++------- .../Test/Examples/DEx/OffChain/Exchange.agda | 28 +++++------- .../Test/Examples/DEx/OffChain/Lib.agda | 26 ++++------- .../Test/Examples/DEx/OffChain/Start.agda | 23 ++++------ .../Test/Examples/DEx/OffChain/Update.agda | 25 +++++------ .../Test/Examples/DEx/Test/Trace.agda | 30 ++++++------- .../Test/Examples/DEx/Validator.agda | 32 ++++---------- .../Test/Examples/HelloWorld.lagda.md | 23 +++++----- .../Examples/MultiSig/OffChain/AddSig.agda | 26 +++++------ .../Test/Examples/MultiSig/OffChain/Lib.agda | 21 +++------ .../Test/Examples/MultiSig/OffChain/Open.agda | 26 ++++------- .../Test/Examples/MultiSig/OffChain/Pay.agda | 26 +++++------ .../Examples/MultiSig/OffChain/Propose.agda | 26 +++++------ .../Test/Examples/MultiSig/Test/Trace.agda | 25 +++++------ .../Test/Examples/MultiSig/Validator.agda | 30 +++++-------- .../Examples/MultiSigV2/OffChain/AddSig.agda | 24 +++++------ .../Examples/MultiSigV2/OffChain/Cancel.agda | 26 +++++------ .../Examples/MultiSigV2/OffChain/Cleanup.agda | 26 +++++------ .../Examples/MultiSigV2/OffChain/Lib.agda | 25 +++++------ .../Examples/MultiSigV2/OffChain/Open.agda | 25 +++++------ .../Examples/MultiSigV2/OffChain/Pay.agda | 24 +++++------ .../Examples/MultiSigV2/OffChain/Propose.agda | 24 +++++------ .../Test/Examples/MultiSigV2/Test/Trace.agda | 24 +++++------ .../Test/Examples/MultiSigV2/Validator.agda | 4 +- .../Test/Examples/SucceedIfNumber.lagda.md | 43 ++++++++++--------- .../Conway/Specification/Test/Lib.lagda.md | 22 ++++------ .../Test/StructuredContracts.lagda.md | 17 ++++---- .../Specification/Test/SymbolicData.agda | 14 ++++-- 42 files changed, 431 insertions(+), 593 deletions(-) rename src/Ledger/Conway/Specification/{ScriptPurpose.agda => Script/ScriptPurpose.lagda.md} (76%) diff --git a/src/Ledger/Conway/Specification/Abstract.lagda.md b/src/Ledger/Conway/Specification/Abstract.lagda.md index 90e6618ee..ea971e5bf 100644 --- a/src/Ledger/Conway/Specification/Abstract.lagda.md +++ b/src/Ledger/Conway/Specification/Abstract.lagda.md @@ -13,7 +13,7 @@ module Ledger.Conway.Specification.Abstract (txs : TransactionStructure) where open TransactionStructure txs open import Ledger.Conway.Specification.Certs govStructure -open import Ledger.Conway.Specification.ScriptPurpose txs +open import Ledger.Conway.Specification.Script.ScriptPurpose txs record indexOf : Type where field diff --git a/src/Ledger/Conway/Specification/ScriptPurpose.agda b/src/Ledger/Conway/Specification/Script/ScriptPurpose.lagda.md similarity index 76% rename from src/Ledger/Conway/Specification/ScriptPurpose.agda rename to src/Ledger/Conway/Specification/Script/ScriptPurpose.lagda.md index 7f1697570..454d199a8 100644 --- a/src/Ledger/Conway/Specification/ScriptPurpose.agda +++ b/src/Ledger/Conway/Specification/Script/ScriptPurpose.lagda.md @@ -1,13 +1,25 @@ +--- +source_branch: master +source_path: src/Ledger/Conway/Specification/Script/ScriptPurpose.lagda.md +--- + +# Script Purpose {#sec:script-purpose} + + +```agda data ScriptPurpose : Type where Cert : DCert → ScriptPurpose Rwrd : RwdAddr → ScriptPurpose @@ -27,4 +39,4 @@ record TxInfo : Type where vkKey : ℙ KeyHash txdats : ℙ Datum txId : TxId - +``` diff --git a/src/Ledger/Conway/Specification/Script/Validation.lagda.md b/src/Ledger/Conway/Specification/Script/Validation.lagda.md index 3da7dbc42..d66512f48 100644 --- a/src/Ledger/Conway/Specification/Script/Validation.lagda.md +++ b/src/Ledger/Conway/Specification/Script/Validation.lagda.md @@ -24,7 +24,7 @@ open import Ledger.Conway.Specification.Certs govStructure open import Ledger.Conway.Specification.Abstract txs -open import Ledger.Conway.Specification.ScriptPurpose txs +open import Ledger.Conway.Specification.Script.ScriptPurpose txs rdptr : TxBody → ScriptPurpose → Maybe RdmrPtr rdptr txb = λ where diff --git a/src/Ledger/Conway/Specification/Test/AbstractImplementation.agda b/src/Ledger/Conway/Specification/Test/AbstractImplementation.agda index a1f642ee3..d0987c6b7 100644 --- a/src/Ledger/Conway/Specification/Test/AbstractImplementation.agda +++ b/src/Ledger/Conway/Specification/Test/AbstractImplementation.agda @@ -1,18 +1,19 @@ {-# OPTIONS --safe #-} -open import Ledger.Prelude hiding (fromList; ε); open Computational -open import Ledger.Conway.Specification.Test.Prelude -open import Ledger.Conway.Specification.Transaction using (TransactionStructure) +open import Ledger.Prelude using (DecEq; Show) +import Ledger.Conway.Specification.Script.ScriptPurpose as SP open import Ledger.Conway.Specification.Test.LedgerImplementation using (SVTransactionStructure) -open import Ledger.Conway.Specification.ScriptPurpose using () -module Ledger.Conway.Specification.Test.AbstractImplementation (T D : Set){{DecEq-Data : DecEq D}}{{Show-Data : Show D}} - (open TransactionStructure (SVTransactionStructure T D)) - (open Ledger.Conway.Specification.ScriptPurpose (SVTransactionStructure T D)) +module Ledger.Conway.Specification.Test.AbstractImplementation + {T D : Set} {{DecEq-Data : DecEq D}} {{Show-Data : Show D}} + (open SP (SVTransactionStructure T D) using (TxInfo; ScriptPurpose)) (valContext' : TxInfo → ScriptPurpose → D) where -open import Ledger.Conway.Specification.Test.LedgerImplementation T D renaming (SVTransactionStructure to SVTransactionStructure') +open import Ledger.Prelude using (nothing; _,_) + +open import Ledger.Conway.Specification.Test.LedgerImplementation T D + renaming (SVTransactionStructure to SVTransactionStructure') open import Ledger.Conway.Specification.Abstract SVTransactionStructure' open Implementation diff --git a/src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Cleanup.agda b/src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Cleanup.agda index 50e3e840d..3cc1e5512 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Cleanup.agda +++ b/src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Cleanup.agda @@ -1,28 +1,23 @@ {-# OPTIONS --safe #-} -open import Ledger.Prelude hiding (fromList; ε); open Computational +module Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.Cleanup where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction + open import Ledger.Conway.Specification.Test.Examples.AccountSim.Datum +open import Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.Lib open import Ledger.Conway.Specification.Test.Examples.AccountSim.Validator open import Ledger.Conway.Specification.Test.Prelude AccountSimData open import Ledger.Conway.Specification.Test.SymbolicData AccountSimData open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Transaction using (TransactionStructure) -open TransactionStructure SVTransactionStructure -open import Ledger.Conway.Specification.Test.AbstractImplementation SData SData valContext -open import Ledger.Conway.Specification.Test.Lib SData SData valContext -open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions -open import Data.Empty -open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions -open import Ledger.Conway.Specification.Transaction -open import Ledger.Core.Specification.Epoch -open EpochStructure SVEpochStructure -open Implementation -open import Ledger.Conway.Specification.Utxo.Properties.Computational SVTransactionStructure SVAbstractFunctions -open import Data.List using (filter) -open import Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.Lib +open import Ledger.Conway.Specification.Test.AbstractImplementation valContext +open import Ledger.Conway.Specification.Test.Lib valContext -module Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.Cleanup where +open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions +open TransactionStructure SVTransactionStructure +open Implementation makeCleanupTx : (id : ℕ) → UTxOState → PlutusScript → (w : ℕ) → Maybe Tx makeCleanupTx id state script@(sh , _) w = diff --git a/src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Close.agda b/src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Close.agda index 64f327a4a..628f3f3a9 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Close.agda +++ b/src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Close.agda @@ -1,33 +1,29 @@ {-# OPTIONS --safe #-} -open import Ledger.Prelude hiding (fromList; ε); open Computational +module Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.Close where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction + open import Ledger.Conway.Specification.Test.Examples.AccountSim.Datum open import Ledger.Conway.Specification.Test.Examples.AccountSim.Validator +open import Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.Lib open import Ledger.Conway.Specification.Test.Prelude AccountSimData open import Ledger.Conway.Specification.Test.SymbolicData AccountSimData open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Transaction using (TransactionStructure) -open TransactionStructure SVTransactionStructure -open import Ledger.Conway.Specification.Test.AbstractImplementation SData SData valContext -open import Ledger.Conway.Specification.Test.Lib SData SData valContext -open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions -open import Data.Empty +open import Ledger.Conway.Specification.Test.AbstractImplementation valContext +open import Ledger.Conway.Specification.Test.Lib valContext + open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions -open import Ledger.Conway.Specification.Transaction -open import Ledger.Core.Specification.Epoch -open EpochStructure SVEpochStructure -open Implementation -open import Ledger.Conway.Specification.Utxo.Properties.Computational SVTransactionStructure SVAbstractFunctions -open import Data.List using (filter) -open import Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.Lib -module Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.Close where +open TransactionStructure SVTransactionStructure +open Implementation makeCloseTxOut : Label → (scriptIx w : ℕ) → TxOut → List (ℕ × TxOut) makeCloseTxOut (Always l) ix w (fst , fst' , snd) = (ix , (fst , fst' , just (inj₁ (inj₁ (inj₁ (Always (delete' w l))))) , nothing)) ∷ [] - + makeCloseTx : (id : ℕ) → UTxOState → PlutusScript → (w : ℕ) → Maybe Tx makeCloseTx id state script@(sh , _) w = let @@ -40,13 +36,13 @@ makeCloseTx id state script@(sh , _) w = ; txOuts = fromListIx (makeFeeTxOut wutxo ++ makeCloseTxOut label (proj₂ scIn) w scOut ) ; txId = id ; collateralInputs = Ledger.Prelude.fromList (map proj₁ wutxo) - ; reqSignerHashes = Ledger.Prelude.fromList (w ∷ []) + ; reqSignerHashes = Ledger.Prelude.fromList (w ∷ []) } ; wits = record { vkSigs = fromListᵐ ((w , (_+_ {{addNat}} (getTxId wutxo) w) ) ∷ []) ; scripts = Ledger.Prelude.fromList ((inj₂ script) ∷ []) ; - txdats = ∅ ; + txdats = ∅ ; txrdmrs = fromListᵐ (((Spend , (proj₂ scIn)) , - inj₁ (inj₂ (Close w)) , + inj₁ (inj₂ (Close w)) , ((getTxId wutxo) , w)) ∷ []) } ; txsize = 10 ; isValid = true ; diff --git a/src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Deposit.agda b/src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Deposit.agda index 827170ab8..2f73aaae6 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Deposit.agda +++ b/src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Deposit.agda @@ -1,30 +1,23 @@ {-# OPTIONS --safe #-} -open import Ledger.Prelude hiding (fromList; ε); open Computational +module Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.Deposit where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction + open import Ledger.Conway.Specification.Test.Examples.AccountSim.Datum +open import Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.Lib open import Ledger.Conway.Specification.Test.Examples.AccountSim.Validator open import Ledger.Conway.Specification.Test.Prelude AccountSimData open import Ledger.Conway.Specification.Test.SymbolicData AccountSimData open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Transaction using (TransactionStructure) -open TransactionStructure SVTransactionStructure -open import Ledger.Conway.Specification.Test.AbstractImplementation SData SData valContext -open import Ledger.Conway.Specification.Test.Lib SData SData valContext -open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions -open import Data.Empty -open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions -open import Ledger.Conway.Specification.Transaction -open import Ledger.Core.Specification.Epoch -open EpochStructure SVEpochStructure -open Implementation -open import Ledger.Conway.Specification.Utxo.Properties.Computational SVTransactionStructure SVAbstractFunctions -open import Data.List using (filter) -open import Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.Lib +open import Ledger.Conway.Specification.Test.AbstractImplementation valContext +open import Ledger.Conway.Specification.Test.Lib valContext -import Agda.Builtin.Nat renaming (_+_ to _plus_) - -module Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.Deposit where +open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions +open TransactionStructure SVTransactionStructure +open Implementation scriptDTxOut : Label → TxOut → (w : ℕ) → (v : Value) → TxOut scriptDTxOut (Always l) (fst , txValue , snd) w v = (fst , (_+_ {{addValue}} txValue v) , (just (inj₁ (inj₁ (inj₁ (Always (insert' w (_+_ {{addValue}} val v) l)))))) , nothing) diff --git a/src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Lib.agda b/src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Lib.agda index ac8d8e9f5..9ca347d0f 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Lib.agda +++ b/src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Lib.agda @@ -1,30 +1,19 @@ {-# OPTIONS --safe #-} -open import Ledger.Prelude hiding (fromList; ε); open Computational +module Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.Lib where + +open import Data.List using (filter) + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction using (TransactionStructure) + open import Ledger.Conway.Specification.Test.Examples.AccountSim.Datum open import Ledger.Conway.Specification.Test.Examples.AccountSim.Validator open import Ledger.Conway.Specification.Test.Prelude AccountSimData open import Ledger.Conway.Specification.Test.SymbolicData AccountSimData open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Transaction using (TransactionStructure) -open TransactionStructure SVTransactionStructure -open import Ledger.Conway.Specification.Test.AbstractImplementation SData SData valContext -open import Ledger.Conway.Specification.Test.Lib SData SData valContext -open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions -open import Data.Empty -open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions -open import Ledger.Conway.Specification.Transaction -open import Ledger.Core.Specification.Epoch -open EpochStructure SVEpochStructure -open Implementation -open import Ledger.Conway.Specification.Utxo.Properties.Computational SVTransactionStructure SVAbstractFunctions -open import Data.List using (filter) -import Agda.Builtin.Nat as Nat - -module Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.Lib where - -open import Relation.Nullary +open TransactionStructure SVTransactionStructure defaultTxBody : TxBody defaultTxBody = record diff --git a/src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Open.agda b/src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Open.agda index d5ceb3b4d..383ab9708 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Open.agda +++ b/src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Open.agda @@ -1,34 +1,28 @@ {-# OPTIONS --safe #-} -open import Ledger.Prelude hiding (fromList; ε); open Computational +module Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.Open where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction + open import Ledger.Conway.Specification.Test.Examples.AccountSim.Datum +open import Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.Lib open import Ledger.Conway.Specification.Test.Examples.AccountSim.Validator open import Ledger.Conway.Specification.Test.Prelude AccountSimData open import Ledger.Conway.Specification.Test.SymbolicData AccountSimData open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Transaction using (TransactionStructure) -open TransactionStructure SVTransactionStructure -open import Ledger.Conway.Specification.Test.AbstractImplementation SData SData valContext -open import Ledger.Conway.Specification.Test.Lib SData SData valContext -open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions -open import Data.Empty -open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions -open import Ledger.Conway.Specification.Transaction -open import Ledger.Core.Specification.Epoch -open EpochStructure SVEpochStructure -open Implementation -open import Ledger.Conway.Specification.Utxo.Properties.Computational SVTransactionStructure SVAbstractFunctions -open import Data.List using (filter) -open import Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.Lib - -module Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.Open where +open import Ledger.Conway.Specification.Test.AbstractImplementation valContext +open import Ledger.Conway.Specification.Test.Lib valContext +open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions +open TransactionStructure SVTransactionStructure +open Implementation makeOpenTxOut : Label → (scriptIx w : ℕ) → TxOut → List (ℕ × TxOut) makeOpenTxOut (Always l) ix w (fst , fst' , snd) = (ix , (fst , fst' , just (inj₁ (inj₁ (inj₁ (Always (insert' w emptyValue l))))) , nothing)) ∷ [] - + makeOpenTx : (id : ℕ) → UTxOState → PlutusScript → (w : ℕ) → Maybe Tx makeOpenTx id state script@(sh , _) w = let @@ -41,13 +35,13 @@ makeOpenTx id state script@(sh , _) w = ; txOuts = fromListIx (makeFeeTxOut wutxo ++ makeOpenTxOut label (proj₂ scIn) w scOut ) ; txId = id ; collateralInputs = Ledger.Prelude.fromList (map proj₁ wutxo) - ; reqSignerHashes = Ledger.Prelude.fromList (w ∷ []) + ; reqSignerHashes = Ledger.Prelude.fromList (w ∷ []) } ; wits = record { vkSigs = fromListᵐ ((w , (_+_ {{addNat}} (getTxId wutxo) w)) ∷ []) ; scripts = Ledger.Prelude.fromList ((inj₂ script) ∷ []) ; - txdats = ∅ ; + txdats = ∅ ; txrdmrs = fromListᵐ (((Spend , (proj₂ scIn)) , - inj₁ (inj₂ (Open w)) , --(Add w) + inj₁ (inj₂ (Open w)) , --(Add w) ((getTxId wutxo) , w)) ∷ []) } ; txsize = 10 ; isValid = true ; diff --git a/src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Start.agda b/src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Start.agda index ae207490c..fc3e3065f 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Start.agda +++ b/src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Start.agda @@ -1,27 +1,20 @@ {-# OPTIONS --safe #-} -open import Ledger.Prelude hiding (fromList; ε); open Computational +module Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.Start where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction using (TransactionStructure) + open import Ledger.Conway.Specification.Test.Examples.AccountSim.Datum +open import Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.Lib open import Ledger.Conway.Specification.Test.Examples.AccountSim.Validator open import Ledger.Conway.Specification.Test.Prelude AccountSimData open import Ledger.Conway.Specification.Test.SymbolicData AccountSimData open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Transaction using (TransactionStructure) +open import Ledger.Conway.Specification.Test.Lib valContext + open TransactionStructure SVTransactionStructure -open import Ledger.Conway.Specification.Test.AbstractImplementation SData SData valContext -open import Ledger.Conway.Specification.Test.Lib SData SData valContext -open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions -open import Data.Empty -open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions -open import Ledger.Conway.Specification.Transaction -open import Ledger.Core.Specification.Epoch -open EpochStructure SVEpochStructure open Implementation -open import Ledger.Conway.Specification.Utxo.Properties.Computational SVTransactionStructure SVAbstractFunctions -open import Data.List using (filter) -open import Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.Lib - -module Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.Start where startTxOut : Value → PlutusScript → TxOut startTxOut v script = inj₁ (record { net = 0 ; @@ -46,9 +39,9 @@ startTx id w tw v script = record { body = record defaultTxBody } ; wits = record { vkSigs = fromListᵐ ((w , (_+_ {{addNat}} w id)) ∷ []) ; scripts = ∅ ; - txdats = ∅ ; + txdats = ∅ ; txrdmrs = ∅ } ; - + txsize = 10 ; isValid = true ; txAD = nothing } diff --git a/src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Transfer.agda b/src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Transfer.agda index fe121522c..9c4e8ffd7 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Transfer.agda +++ b/src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Transfer.agda @@ -1,29 +1,23 @@ {-# OPTIONS --safe #-} -open import Ledger.Prelude hiding (fromList; ε); open Computational +module Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.Transfer where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction + open import Ledger.Conway.Specification.Test.Examples.AccountSim.Datum +open import Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.Lib open import Ledger.Conway.Specification.Test.Examples.AccountSim.Validator open import Ledger.Conway.Specification.Test.Prelude AccountSimData open import Ledger.Conway.Specification.Test.SymbolicData AccountSimData open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Transaction using (TransactionStructure) -open TransactionStructure SVTransactionStructure -open import Ledger.Conway.Specification.Test.AbstractImplementation SData SData valContext -open import Ledger.Conway.Specification.Test.Lib SData SData valContext -open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions -open import Data.Empty -open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions -open import Ledger.Conway.Specification.Transaction -open import Ledger.Core.Specification.Epoch -open EpochStructure SVEpochStructure -open Implementation -open import Ledger.Conway.Specification.Utxo.Properties.Computational SVTransactionStructure SVAbstractFunctions -open import Data.List using (filter) -open import Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.Lib +open import Ledger.Conway.Specification.Test.AbstractImplementation valContext +open import Ledger.Conway.Specification.Test.Lib valContext -import Agda.Builtin.Nat renaming (_+_ to _plus_) +open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions -module Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.Transfer where +open TransactionStructure SVTransactionStructure +open Implementation makeTransferTxOut : Label → (scriptIx from to : ℕ) → (v : Value) → TxOut → List (ℕ × TxOut) diff --git a/src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Withdraw.agda b/src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Withdraw.agda index 3ede12af3..797ce5069 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Withdraw.agda +++ b/src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Withdraw.agda @@ -1,28 +1,23 @@ {-# OPTIONS --safe #-} -open import Ledger.Prelude hiding (fromList; ε); open Computational +module Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.Withdraw where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction + open import Ledger.Conway.Specification.Test.Examples.AccountSim.Datum +open import Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.Lib open import Ledger.Conway.Specification.Test.Examples.AccountSim.Validator open import Ledger.Conway.Specification.Test.Prelude AccountSimData open import Ledger.Conway.Specification.Test.SymbolicData AccountSimData open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Transaction using (TransactionStructure) -open TransactionStructure SVTransactionStructure -open import Ledger.Conway.Specification.Test.AbstractImplementation SData SData valContext -open import Ledger.Conway.Specification.Test.Lib SData SData valContext -open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions -open import Data.Empty -open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions -open import Ledger.Conway.Specification.Transaction -open import Ledger.Core.Specification.Epoch -open EpochStructure SVEpochStructure -open Implementation -open import Ledger.Conway.Specification.Utxo.Properties.Computational SVTransactionStructure SVAbstractFunctions -open import Data.List using (filter) -open import Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.Lib +open import Ledger.Conway.Specification.Test.AbstractImplementation valContext +open import Ledger.Conway.Specification.Test.Lib valContext +open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions -module Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.Withdraw where +open TransactionStructure SVTransactionStructure +open Implementation scriptTxOut : Label → TxOut → (w : ℕ) → (v : Value) → TxOut diff --git a/src/Ledger/Conway/Specification/Test/Examples/AccountSim/Test/Trace.agda b/src/Ledger/Conway/Specification/Test/Examples/AccountSim/Test/Trace.agda index 8b6fbbb1f..46b669c9d 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/AccountSim/Test/Trace.agda +++ b/src/Ledger/Conway/Specification/Test/Examples/AccountSim/Test/Trace.agda @@ -1,30 +1,26 @@ {-# OPTIONS --safe #-} -open import Ledger.Prelude hiding (fromList; ε); open Computational +module Ledger.Conway.Specification.Test.Examples.AccountSim.Test.Trace where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction using (TransactionStructure) + open import Ledger.Conway.Specification.Test.Examples.AccountSim.Datum +open import Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.OffChain open import Ledger.Conway.Specification.Test.Examples.AccountSim.Validator open import Ledger.Conway.Specification.Test.Prelude AccountSimData open import Ledger.Conway.Specification.Test.SymbolicData AccountSimData open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Transaction using (TransactionStructure) -open TransactionStructure SVTransactionStructure -open import Ledger.Conway.Specification.Test.AbstractImplementation SData SData valContext -open import Ledger.Conway.Specification.Test.Lib SData SData valContext +open import Ledger.Conway.Specification.Test.AbstractImplementation valContext +open import Ledger.Conway.Specification.Test.Lib valContext + open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions -open import Data.Empty open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions -open import Ledger.Conway.Specification.Transaction -open import Ledger.Core.Specification.Epoch -open EpochStructure SVEpochStructure -open Implementation open import Ledger.Conway.Specification.Utxo.Properties.Computational SVTransactionStructure SVAbstractFunctions open import Ledger.Conway.Specification.Utxow.Properties.Computational SVTransactionStructure SVAbstractFunctions -open import Data.List using (filter) - -module Ledger.Conway.Specification.Test.Examples.AccountSim.Test.Trace where - -open import Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.OffChain +open TransactionStructure SVTransactionStructure +open Implementation multiSigScript : PlutusScript multiSigScript = 777 , applyScriptWithContext (accSimValidator) diff --git a/src/Ledger/Conway/Specification/Test/Examples/AccountSim/Validator.agda b/src/Ledger/Conway/Specification/Test/Examples/AccountSim/Validator.agda index 3aa6ba064..858ef6eed 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/AccountSim/Validator.agda +++ b/src/Ledger/Conway/Specification/Test/Examples/AccountSim/Validator.agda @@ -2,44 +2,30 @@ -- Validator Simulating Accounts on Cardano based on Agda2hs work -open import Ledger.Prelude hiding (fromList; ε); open Computational -open import Ledger.Conway.Specification.Test.Examples.AccountSim.Datum -open import Relation.Binary using (REL; Decidable) -open import Level using (Level; _⊔_; suc) -open import Data.Maybe renaming (map to maybeMap) -open import Data.List using (filter) +module Ledger.Conway.Specification.Test.Examples.AccountSim.Validator where open import Data.Bool.Base renaming (_∧_ to _&&_) hiding (if_then_else_) -import Agda.Builtin.Nat as N +open import Data.List using (filter) +open import Data.Maybe renaming (map to maybeMap) +open import Ledger.Prelude +open import Ledger.Conway.Specification.Test.Examples.AccountSim.Datum open import Ledger.Conway.Specification.Test.Prelude AccountSimData +open import Ledger.Conway.Specification.Test.SymbolicData AccountSimData -module Ledger.Conway.Specification.Test.Examples.AccountSim.Validator where +import Agda.Builtin.Nat as N +PubKeyHash : Type PubKeyHash = ℕ -open import Ledger.Conway.Specification.Test.SymbolicData AccountSimData - - instance ShowAccountSimData : Show AccountSimData ShowAccountSimData = mkShow (λ x → "") open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData open import Ledger.Conway.Specification.Transaction using (TransactionStructure) -open TransactionStructure SVTransactionStructure -open import Ledger.Conway.Specification.Test.AbstractImplementation SData SData valContext -open import Ledger.Conway.Specification.Test.Lib SData SData valContext -open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions -open import Data.Empty -open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions -open import Ledger.Conway.Specification.Transaction -open import Ledger.Core.Specification.Epoch -open EpochStructure SVEpochStructure -open Implementation -open import Ledger.Conway.Specification.Utxo.Properties.Computational SVTransactionStructure SVAbstractFunctions -open import Ledger.Conway.Specification.Utxow.Properties.Computational SVTransactionStructure SVAbstractFunctions +open TransactionStructure SVTransactionStructure emptyValue : Value emptyValue = 0 diff --git a/src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/Close.agda b/src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/Close.agda index d26790ff1..9b07b0424 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/Close.agda +++ b/src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/Close.agda @@ -1,28 +1,23 @@ {-# OPTIONS --safe #-} -open import Ledger.Prelude hiding (fromList; ε); open Computational +module Ledger.Conway.Specification.Test.Examples.DEx.OffChain.Close where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction + open import Ledger.Conway.Specification.Test.Examples.DEx.Datum open import Ledger.Conway.Specification.Test.Examples.DEx.Validator +open import Ledger.Conway.Specification.Test.Examples.DEx.OffChain.Lib open import Ledger.Conway.Specification.Test.Prelude DExData open import Ledger.Conway.Specification.Test.SymbolicData DExData open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Transaction using (TransactionStructure) -open TransactionStructure SVTransactionStructure -open import Ledger.Conway.Specification.Test.AbstractImplementation SData SData valContext -open import Ledger.Conway.Specification.Test.Lib SData SData valContext -open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions -open import Data.Empty -open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions -open import Ledger.Conway.Specification.Transaction -open import Ledger.Core.Specification.Epoch -open EpochStructure SVEpochStructure -open Implementation -open import Ledger.Conway.Specification.Utxo.Properties.Computational SVTransactionStructure SVAbstractFunctions -open import Data.List using (filter) -open import Ledger.Conway.Specification.Test.Examples.DEx.OffChain.Lib +open import Ledger.Conway.Specification.Test.AbstractImplementation valContext +open import Ledger.Conway.Specification.Test.Lib valContext -module Ledger.Conway.Specification.Test.Examples.DEx.OffChain.Close where +open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions +open TransactionStructure SVTransactionStructure +open Implementation makeCloseTx : (id : ℕ) → UTxOState → PlutusScript → (w : ℕ) → Maybe Tx makeCloseTx id state script@(sh , _) w = diff --git a/src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/Exchange.agda b/src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/Exchange.agda index 72b3a3c03..bb556f299 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/Exchange.agda +++ b/src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/Exchange.agda @@ -1,32 +1,26 @@ {-# OPTIONS --safe #-} -open import Ledger.Prelude hiding (fromList; ε); open Computational +module Ledger.Conway.Specification.Test.Examples.DEx.OffChain.Exchange where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction + open import Ledger.Conway.Specification.Test.Examples.DEx.Datum open import Ledger.Conway.Specification.Test.Examples.DEx.Validator +open import Ledger.Conway.Specification.Test.Examples.DEx.OffChain.Lib open import Ledger.Conway.Specification.Test.Prelude DExData open import Ledger.Conway.Specification.Test.SymbolicData DExData open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Transaction using (TransactionStructure) -open TransactionStructure SVTransactionStructure -open import Ledger.Conway.Specification.Test.AbstractImplementation SData SData valContext -open import Ledger.Conway.Specification.Test.Lib SData SData valContext -open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions -open import Data.Empty +open import Ledger.Conway.Specification.Test.AbstractImplementation valContext +open import Ledger.Conway.Specification.Test.Lib valContext + open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions -open import Ledger.Conway.Specification.Transaction -open import Ledger.Core.Specification.Epoch -open EpochStructure SVEpochStructure + +open TransactionStructure SVTransactionStructure open Implementation -open import Ledger.Conway.Specification.Utxo.Properties.Computational SVTransactionStructure SVAbstractFunctions -open import Data.List using (filter) -open import Ledger.Conway.Specification.Test.Examples.DEx.OffChain.Lib -import Agda.Builtin.Nat renaming (_+_ to _plus_) import Data.Rational.Base as Q -module Ledger.Conway.Specification.Test.Examples.DEx.OffChain.Exchange where - - scriptETxOut : Label → TxOut → (w : ℕ) → (v : Value) → TxOut scriptETxOut (Always q o) (fst , txValue , snd) w v = (fst , (txValue - v) , (just (inj₁ (inj₁ (inj₁ (Always q o))))) , nothing) diff --git a/src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/Lib.agda b/src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/Lib.agda index eda931fbc..199969383 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/Lib.agda +++ b/src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/Lib.agda @@ -1,29 +1,19 @@ {-# OPTIONS --safe #-} -open import Ledger.Prelude hiding (fromList; ε); open Computational +module Ledger.Conway.Specification.Test.Examples.DEx.OffChain.Lib where + +open import Data.List using (filter) + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction using (TransactionStructure) + open import Ledger.Conway.Specification.Test.Examples.DEx.Datum open import Ledger.Conway.Specification.Test.Examples.DEx.Validator open import Ledger.Conway.Specification.Test.Prelude DExData open import Ledger.Conway.Specification.Test.SymbolicData DExData open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Transaction using (TransactionStructure) -open TransactionStructure SVTransactionStructure -open import Ledger.Conway.Specification.Test.AbstractImplementation SData SData valContext -open import Ledger.Conway.Specification.Test.Lib SData SData valContext -open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions -open import Data.Empty -open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions -open import Ledger.Conway.Specification.Transaction -open import Ledger.Core.Specification.Epoch -open EpochStructure SVEpochStructure -open Implementation -open import Ledger.Conway.Specification.Utxo.Properties.Computational SVTransactionStructure SVAbstractFunctions -open import Data.List using (filter) -import Agda.Builtin.Nat as Nat -module Ledger.Conway.Specification.Test.Examples.DEx.OffChain.Lib where - -open import Relation.Nullary +open TransactionStructure SVTransactionStructure defaultTxBody : TxBody defaultTxBody = record diff --git a/src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/Start.agda b/src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/Start.agda index d1452732d..88d768564 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/Start.agda +++ b/src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/Start.agda @@ -1,30 +1,23 @@ {-# OPTIONS --safe #-} -open import Ledger.Prelude hiding (fromList; ε); open Computational +module Ledger.Conway.Specification.Test.Examples.DEx.OffChain.Start where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction using (TransactionStructure) + open import Ledger.Conway.Specification.Test.Examples.DEx.Datum +open import Ledger.Conway.Specification.Test.Examples.DEx.OffChain.Lib open import Ledger.Conway.Specification.Test.Examples.DEx.Validator open import Ledger.Conway.Specification.Test.Prelude DExData open import Ledger.Conway.Specification.Test.SymbolicData DExData open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Transaction using (TransactionStructure) +open import Ledger.Conway.Specification.Test.Lib valContext + open TransactionStructure SVTransactionStructure -open import Ledger.Conway.Specification.Test.AbstractImplementation SData SData valContext -open import Ledger.Conway.Specification.Test.Lib SData SData valContext -open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions -open import Data.Empty -open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions -open import Ledger.Conway.Specification.Transaction -open import Ledger.Core.Specification.Epoch -open EpochStructure SVEpochStructure open Implementation -open import Ledger.Conway.Specification.Utxo.Properties.Computational SVTransactionStructure SVAbstractFunctions -open import Data.List using (filter) -open import Ledger.Conway.Specification.Test.Examples.DEx.OffChain.Lib import Data.Rational.Base as Q -module Ledger.Conway.Specification.Test.Examples.DEx.OffChain.Start where - startTxOut : Value → Q.ℚ → ℕ → PlutusScript → TxOut startTxOut v r o script = inj₁ (record { net = 0 ; pay = ScriptObj (proj₁ script) ; diff --git a/src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/Update.agda b/src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/Update.agda index 4144c8511..09802394f 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/Update.agda +++ b/src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/Update.agda @@ -1,29 +1,26 @@ {-# OPTIONS --safe #-} -open import Ledger.Prelude hiding (fromList; ε); open Computational +module Ledger.Conway.Specification.Test.Examples.DEx.OffChain.Update where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction + open import Ledger.Conway.Specification.Test.Examples.DEx.Datum open import Ledger.Conway.Specification.Test.Examples.DEx.Validator +open import Ledger.Conway.Specification.Test.Examples.DEx.OffChain.Lib open import Ledger.Conway.Specification.Test.Prelude DExData open import Ledger.Conway.Specification.Test.SymbolicData DExData open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Transaction using (TransactionStructure) -open TransactionStructure SVTransactionStructure -open import Ledger.Conway.Specification.Test.AbstractImplementation SData SData valContext -open import Ledger.Conway.Specification.Test.Lib SData SData valContext -open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions -open import Data.Empty +open import Ledger.Conway.Specification.Test.AbstractImplementation valContext +open import Ledger.Conway.Specification.Test.Lib valContext + open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions -open import Ledger.Conway.Specification.Transaction -open import Ledger.Core.Specification.Epoch -open EpochStructure SVEpochStructure + +open TransactionStructure SVTransactionStructure open Implementation -open import Ledger.Conway.Specification.Utxo.Properties.Computational SVTransactionStructure SVAbstractFunctions -open import Data.List using (filter) -open import Ledger.Conway.Specification.Test.Examples.DEx.OffChain.Lib import Data.Rational.Base as Q -module Ledger.Conway.Specification.Test.Examples.DEx.OffChain.Update where makeUpdateTxOut : Label → (scriptIx w : ℕ) → Value → Q.ℚ → TxOut → List (ℕ × TxOut) diff --git a/src/Ledger/Conway/Specification/Test/Examples/DEx/Test/Trace.agda b/src/Ledger/Conway/Specification/Test/Examples/DEx/Test/Trace.agda index c99fc941b..7269c75a6 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/DEx/Test/Trace.agda +++ b/src/Ledger/Conway/Specification/Test/Examples/DEx/Test/Trace.agda @@ -1,33 +1,33 @@ {-# OPTIONS --safe #-} -open import Ledger.Prelude hiding (fromList; ε); open Computational +module Ledger.Conway.Specification.Test.Examples.DEx.Test.Trace where + +import Data.Rational.Base as Q +open import Data.Nat.Divisibility.Core +open import Data.Nat.Properties + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction using (TransactionStructure) + open import Ledger.Conway.Specification.Test.Examples.DEx.Datum open import Ledger.Conway.Specification.Test.Examples.DEx.Validator open import Ledger.Conway.Specification.Test.Prelude DExData open import Ledger.Conway.Specification.Test.SymbolicData DExData open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Transaction using (TransactionStructure) -open TransactionStructure SVTransactionStructure -open import Ledger.Conway.Specification.Test.AbstractImplementation SData SData valContext -open import Ledger.Conway.Specification.Test.Lib SData SData valContext +open import Ledger.Conway.Specification.Test.AbstractImplementation valContext +open import Ledger.Conway.Specification.Test.Lib valContext open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions -open import Data.Empty open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions -open import Ledger.Conway.Specification.Transaction -open import Ledger.Core.Specification.Epoch -open EpochStructure SVEpochStructure -open Implementation open import Ledger.Conway.Specification.Utxo.Properties.Computational SVTransactionStructure SVAbstractFunctions open import Ledger.Conway.Specification.Utxow.Properties.Computational SVTransactionStructure SVAbstractFunctions -open import Data.List using (filter) -import Data.Rational.Base as Q -open import Data.Nat.Divisibility.Core -open import Data.Nat.Properties -module Ledger.Conway.Specification.Test.Examples.DEx.Test.Trace where open import Ledger.Conway.Specification.Test.Examples.DEx.OffChain.OffChain +open TransactionStructure SVTransactionStructure +open Implementation + + par : Params par = record { sellC = 0 ; buyC = 0 } diff --git a/src/Ledger/Conway/Specification/Test/Examples/DEx/Validator.agda b/src/Ledger/Conway/Specification/Test/Examples/DEx/Validator.agda index e08e2e404..c62abb17b 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/DEx/Validator.agda +++ b/src/Ledger/Conway/Specification/Test/Examples/DEx/Validator.agda @@ -2,47 +2,33 @@ -- Validator for the MultiSig contract from the EUTxO paper adapted from Agda2hs version -open import Ledger.Prelude hiding (fromList; ε); open Computational -open import Ledger.Conway.Specification.Test.Examples.DEx.Datum -open import Relation.Binary using (REL; Decidable) -open import Level using (Level; _⊔_; suc) +module Ledger.Conway.Specification.Test.Examples.DEx.Validator where + open import Data.Maybe renaming (map to maybeMap) open import Data.List using (filter) - open import Data.Bool.Base renaming (_∧_ to _&&_) hiding (if_then_else_) ---open import Interface.ToBool + import Agda.Builtin.Nat as N import Data.Rational.Base as Q +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction using (TransactionStructure) +open import Ledger.Conway.Specification.Test.Examples.DEx.Datum open import Ledger.Conway.Specification.Test.Prelude DExData +open import Ledger.Conway.Specification.Test.SymbolicData DExData -module Ledger.Conway.Specification.Test.Examples.DEx.Validator where - +PubKeyHash : Type PubKeyHash = ℕ -open import Ledger.Conway.Specification.Test.SymbolicData DExData - --TODO: Implement show properly instance ShowAccountSimData : Show DExData ShowAccountSimData = mkShow (λ x → "") open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Transaction using (TransactionStructure) -open TransactionStructure SVTransactionStructure -open import Ledger.Conway.Specification.Test.AbstractImplementation SData SData valContext -open import Ledger.Conway.Specification.Test.Lib SData SData valContext -open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions -open import Data.Empty -open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions -open import Ledger.Conway.Specification.Transaction -open import Ledger.Core.Specification.Epoch -open EpochStructure SVEpochStructure -open Implementation -open import Ledger.Conway.Specification.Utxo.Properties.Computational SVTransactionStructure SVAbstractFunctions -open import Ledger.Conway.Specification.Utxow.Properties.Computational SVTransactionStructure SVAbstractFunctions +open TransactionStructure SVTransactionStructure emptyValue : Value emptyValue = 0 diff --git a/src/Ledger/Conway/Specification/Test/Examples/HelloWorld.lagda.md b/src/Ledger/Conway/Specification/Test/Examples/HelloWorld.lagda.md index 822367a16..d96e6c4c3 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/HelloWorld.lagda.md +++ b/src/Ledger/Conway/Specification/Test/Examples/HelloWorld.lagda.md @@ -6,31 +6,28 @@ source_path: src/Ledger/Conway/Specification/Test/Examples/HelloWorld.lagda.md ```agda {-# OPTIONS --safe #-} +module Ledger.Conway.Specification.Test.Examples.HelloWorld where + open import Ledger.Prelude hiding (fromList; ε); open Computational -open import Ledger.Conway.Specification.Test.Prelude (String) -module Ledger.Conway.Specification.Test.Examples.HelloWorld where open import Ledger.Conway.Specification.Test.LedgerImplementation String String -open import Ledger.Conway.Specification.Transaction using (TransactionStructure) -open TransactionStructure SVTransactionStructure using (Data) -open import Ledger.Conway.Specification.ScriptPurpose SVTransactionStructure +open import Ledger.Conway.Specification.Script.ScriptPurpose SVTransactionStructure +open import Ledger.Conway.Specification.Transaction +open TransactionStructure SVTransactionStructure using (Data) valContext : TxInfo → ScriptPurpose → Data valContext x x₁ = "" -open import Ledger.Conway.Specification.Test.AbstractImplementation String String valContext -open import Ledger.Conway.Specification.Test.Lib String String valContext +open import Ledger.Conway.Specification.Test.AbstractImplementation valContext +open import Ledger.Conway.Specification.Test.Lib valContext open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions -open import Data.Empty + open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions -open import Ledger.Conway.Specification.Transaction -open TransactionStructure SVTransactionStructure -open import Ledger.Core.Specification.Epoch -open EpochStructure SVEpochStructure -open Implementation open import Ledger.Conway.Specification.Utxo.Properties.Computational SVTransactionStructure SVAbstractFunctions +open TransactionStructure SVTransactionStructure +open Implementation -- true if redeemer is "Hello World" helloWorld' : Maybe String → Maybe String → Bool diff --git a/src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/AddSig.agda b/src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/AddSig.agda index 3b6d4fc5d..7627f343a 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/AddSig.agda +++ b/src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/AddSig.agda @@ -1,27 +1,23 @@ {-# OPTIONS --safe #-} -open import Ledger.Prelude hiding (fromList; ε); open Computational +module Ledger.Conway.Specification.Test.Examples.MultiSig.OffChain.AddSig where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction + open import Ledger.Conway.Specification.Test.Examples.MultiSig.Datum open import Ledger.Conway.Specification.Test.Examples.MultiSig.Validator +open import Ledger.Conway.Specification.Test.Examples.MultiSig.OffChain.Lib open import Ledger.Conway.Specification.Test.Prelude MultiSigData open import Ledger.Conway.Specification.Test.SymbolicData MultiSigData open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Transaction using (TransactionStructure) -open TransactionStructure SVTransactionStructure -open import Ledger.Conway.Specification.Test.AbstractImplementation SData SData valContext -open import Ledger.Conway.Specification.Test.Lib SData SData valContext -open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions -open import Data.Empty +open import Ledger.Conway.Specification.Test.AbstractImplementation valContext +open import Ledger.Conway.Specification.Test.Lib valContext + open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions -open import Ledger.Conway.Specification.Transaction -open import Ledger.Core.Specification.Epoch -open EpochStructure SVEpochStructure -open Implementation -open import Ledger.Conway.Specification.Utxo.Properties.Computational SVTransactionStructure SVAbstractFunctions -open import Data.List using (filter) -open import Ledger.Conway.Specification.Test.Examples.MultiSig.OffChain.Lib -module Ledger.Conway.Specification.Test.Examples.MultiSig.OffChain.AddSig where +open TransactionStructure SVTransactionStructure +open Implementation -- TODO: Invesitgate what is going on with vkSigs vs reqSigHash in terms of -- transaction not failing vkSigs diff --git a/src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/Lib.agda b/src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/Lib.agda index 3a83dc37b..e37f0b28d 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/Lib.agda +++ b/src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/Lib.agda @@ -1,30 +1,21 @@ {-# OPTIONS --safe #-} -open import Ledger.Prelude hiding (fromList; ε); open Computational +module Ledger.Conway.Specification.Test.Examples.MultiSig.OffChain.Lib where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction using (TransactionStructure) + open import Ledger.Conway.Specification.Test.Examples.MultiSig.Datum open import Ledger.Conway.Specification.Test.Examples.MultiSig.Validator open import Ledger.Conway.Specification.Test.Prelude MultiSigData open import Ledger.Conway.Specification.Test.SymbolicData MultiSigData open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Transaction using (TransactionStructure) + open TransactionStructure SVTransactionStructure -open import Ledger.Conway.Specification.Test.AbstractImplementation SData SData valContext -open import Ledger.Conway.Specification.Test.Lib SData SData valContext -open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions -open import Data.Empty -open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions -open import Ledger.Conway.Specification.Transaction -open import Ledger.Core.Specification.Epoch -open EpochStructure SVEpochStructure open Implementation -open import Ledger.Conway.Specification.Utxo.Properties.Computational SVTransactionStructure SVAbstractFunctions open import Data.List using (filter) - -module Ledger.Conway.Specification.Test.Examples.MultiSig.OffChain.Lib where - open import Relation.Nullary - defaultTxBody : TxBody defaultTxBody = record { txIns = ∅ diff --git a/src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/Open.agda b/src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/Open.agda index cc391ff29..f7bbd0940 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/Open.agda +++ b/src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/Open.agda @@ -1,27 +1,20 @@ {-# OPTIONS --safe #-} -open import Ledger.Prelude hiding (fromList; ε); open Computational +module Ledger.Conway.Specification.Test.Examples.MultiSig.OffChain.Open where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction + open import Ledger.Conway.Specification.Test.Examples.MultiSig.Datum open import Ledger.Conway.Specification.Test.Examples.MultiSig.Validator +open import Ledger.Conway.Specification.Test.Examples.MultiSig.OffChain.Lib open import Ledger.Conway.Specification.Test.Prelude MultiSigData open import Ledger.Conway.Specification.Test.SymbolicData MultiSigData open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Transaction using (TransactionStructure) +open import Ledger.Conway.Specification.Test.Lib valContext + open TransactionStructure SVTransactionStructure -open import Ledger.Conway.Specification.Test.AbstractImplementation SData SData valContext -open import Ledger.Conway.Specification.Test.Lib SData SData valContext -open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions -open import Data.Empty -open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions -open import Ledger.Conway.Specification.Transaction -open import Ledger.Core.Specification.Epoch -open EpochStructure SVEpochStructure open Implementation -open import Ledger.Conway.Specification.Utxo.Properties.Computational SVTransactionStructure SVAbstractFunctions -open import Data.List using (filter) -open import Ledger.Conway.Specification.Test.Examples.MultiSig.OffChain.Lib - -module Ledger.Conway.Specification.Test.Examples.MultiSig.OffChain.Open where openTxOut : Value → PlutusScript → TxOut openTxOut v script = inj₁ (record { net = 0 ; @@ -55,7 +48,6 @@ openTx id w v tw script = record { body = record defaultTxBody ; -- fromListᵐ (((Propose , (proj₁ script)) , -- inj₁ (inj₂ Pay) , -- (5 , w)) ∷ []) } ; -} - txsize = 10 ; + txsize = 10 ; isValid = true ; txAD = nothing } - diff --git a/src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/Pay.agda b/src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/Pay.agda index a2d886c33..282403d8b 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/Pay.agda +++ b/src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/Pay.agda @@ -1,27 +1,23 @@ {-# OPTIONS --safe #-} -open import Ledger.Prelude hiding (fromList; ε); open Computational +module Ledger.Conway.Specification.Test.Examples.MultiSig.OffChain.Pay where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction + open import Ledger.Conway.Specification.Test.Examples.MultiSig.Datum open import Ledger.Conway.Specification.Test.Examples.MultiSig.Validator +open import Ledger.Conway.Specification.Test.Examples.MultiSig.OffChain.Lib open import Ledger.Conway.Specification.Test.Prelude MultiSigData open import Ledger.Conway.Specification.Test.SymbolicData MultiSigData open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Transaction using (TransactionStructure) -open TransactionStructure SVTransactionStructure -open import Ledger.Conway.Specification.Test.AbstractImplementation SData SData valContext -open import Ledger.Conway.Specification.Test.Lib SData SData valContext -open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions -open import Data.Empty +open import Ledger.Conway.Specification.Test.AbstractImplementation valContext +open import Ledger.Conway.Specification.Test.Lib valContext + open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions -open import Ledger.Conway.Specification.Transaction -open import Ledger.Core.Specification.Epoch -open EpochStructure SVEpochStructure -open Implementation -open import Ledger.Conway.Specification.Utxo.Properties.Computational SVTransactionStructure SVAbstractFunctions -open import Data.List using (filter) -open import Ledger.Conway.Specification.Test.Examples.MultiSig.OffChain.Lib -module Ledger.Conway.Specification.Test.Examples.MultiSig.OffChain.Pay where +open TransactionStructure SVTransactionStructure +open Implementation payScriptTxOut : TxOut → (value : ℕ) → TxOut payScriptTxOut (fst , txValue , snd) v = fst , txValue - v , just (inj₁ (inj₁ (inj₁ Holding))) , nothing diff --git a/src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/Propose.agda b/src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/Propose.agda index bff93af91..3d2bcff8c 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/Propose.agda +++ b/src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/Propose.agda @@ -1,27 +1,23 @@ {-# OPTIONS --safe #-} -open import Ledger.Prelude hiding (fromList; ε); open Computational +module Ledger.Conway.Specification.Test.Examples.MultiSig.OffChain.Propose where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction + open import Ledger.Conway.Specification.Test.Examples.MultiSig.Datum open import Ledger.Conway.Specification.Test.Examples.MultiSig.Validator +open import Ledger.Conway.Specification.Test.Examples.MultiSig.OffChain.Lib open import Ledger.Conway.Specification.Test.Prelude MultiSigData open import Ledger.Conway.Specification.Test.SymbolicData MultiSigData open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Transaction using (TransactionStructure) -open TransactionStructure SVTransactionStructure -open import Ledger.Conway.Specification.Test.AbstractImplementation SData SData valContext -open import Ledger.Conway.Specification.Test.Lib SData SData valContext -open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions -open import Data.Empty +open import Ledger.Conway.Specification.Test.AbstractImplementation valContext +open import Ledger.Conway.Specification.Test.Lib valContext + open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions -open import Ledger.Conway.Specification.Transaction -open import Ledger.Core.Specification.Epoch -open EpochStructure SVEpochStructure -open Implementation -open import Ledger.Conway.Specification.Utxo.Properties.Computational SVTransactionStructure SVAbstractFunctions -open import Data.List using (filter) -open import Ledger.Conway.Specification.Test.Examples.MultiSig.OffChain.Lib -module Ledger.Conway.Specification.Test.Examples.MultiSig.OffChain.Propose where +open TransactionStructure SVTransactionStructure +open Implementation -- TODO: Add error handling makeProposeTxOut : Label → (scriptIx : ℕ) → TxOut → (v tw d : ℕ) → List (ℕ × TxOut) diff --git a/src/Ledger/Conway/Specification/Test/Examples/MultiSig/Test/Trace.agda b/src/Ledger/Conway/Specification/Test/Examples/MultiSig/Test/Trace.agda index 1730a8b24..f9e0a360f 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/MultiSig/Test/Trace.agda +++ b/src/Ledger/Conway/Specification/Test/Examples/MultiSig/Test/Trace.agda @@ -1,29 +1,26 @@ {-# OPTIONS --safe #-} -open import Ledger.Prelude hiding (fromList; ε); open Computational +module Ledger.Conway.Specification.Test.Examples.MultiSig.Test.Trace where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction using (TransactionStructure) + open import Ledger.Conway.Specification.Test.Examples.MultiSig.Datum +open import Ledger.Conway.Specification.Test.Examples.MultiSig.OffChain.OffChain open import Ledger.Conway.Specification.Test.Examples.MultiSig.Validator open import Ledger.Conway.Specification.Test.Prelude MultiSigData open import Ledger.Conway.Specification.Test.SymbolicData MultiSigData open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Transaction using (TransactionStructure) -open TransactionStructure SVTransactionStructure -open import Ledger.Conway.Specification.Test.AbstractImplementation SData SData valContext -open import Ledger.Conway.Specification.Test.Lib SData SData valContext +open import Ledger.Conway.Specification.Test.AbstractImplementation valContext +open import Ledger.Conway.Specification.Test.Lib valContext + open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions -open import Data.Empty open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions -open import Ledger.Conway.Specification.Transaction -open import Ledger.Core.Specification.Epoch -open EpochStructure SVEpochStructure -open Implementation open import Ledger.Conway.Specification.Utxo.Properties.Computational SVTransactionStructure SVAbstractFunctions open import Ledger.Conway.Specification.Utxow.Properties.Computational SVTransactionStructure SVAbstractFunctions -open import Data.List using (filter) - -module Ledger.Conway.Specification.Test.Examples.MultiSig.Test.Trace where -open import Ledger.Conway.Specification.Test.Examples.MultiSig.OffChain.OffChain +open TransactionStructure SVTransactionStructure +open Implementation impMultiSig : MultiSig impMultiSig = record { signatories = 3 ∷ 2 ∷ 5 ∷ [] ; minNumSignatures = 2 } diff --git a/src/Ledger/Conway/Specification/Test/Examples/MultiSig/Validator.agda b/src/Ledger/Conway/Specification/Test/Examples/MultiSig/Validator.agda index 20fb72924..a30a63af7 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/MultiSig/Validator.agda +++ b/src/Ledger/Conway/Specification/Test/Examples/MultiSig/Validator.agda @@ -1,16 +1,19 @@ {-# OPTIONS --safe #-} -open import Ledger.Prelude hiding (fromList; ε); open Computational -open import Ledger.Conway.Specification.Test.Examples.MultiSig.Datum -open import Relation.Binary using (REL; Decidable) -open import Level using (Level; _⊔_; suc) -open import Data.Maybe renaming (map to maybeMap) -open import Data.List using (filter) +module Ledger.Conway.Specification.Test.Examples.MultiSig.Validator where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Test.Examples.MultiSig.Datum open import Ledger.Conway.Specification.Test.Prelude MultiSigData +open import Ledger.Conway.Specification.Transaction +open import Ledger.Conway.Specification.Test.SymbolicData MultiSigData -module Ledger.Conway.Specification.Test.Examples.MultiSig.Validator where +open import Data.List using (filter) +open import Data.Maybe renaming (map to maybeMap) +open import Relation.Binary using (REL; Decidable) +PubKeyHash : Type PubKeyHash = ℕ record MultiSig : Set where @@ -18,27 +21,14 @@ record MultiSig : Set where signatories : List PubKeyHash minNumSignatures : ℕ -open import Ledger.Conway.Specification.Test.SymbolicData MultiSigData - --TODO: Implement show properly instance ShowMultiSigData : Show MultiSigData ShowMultiSigData = mkShow (λ x → "") open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Transaction using (TransactionStructure) open TransactionStructure SVTransactionStructure -open import Ledger.Conway.Specification.Test.AbstractImplementation SData SData valContext -open import Ledger.Conway.Specification.Test.Lib SData SData valContext -open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions -open import Data.Empty -open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions -open import Ledger.Conway.Specification.Transaction -open import Ledger.Core.Specification.Epoch -open EpochStructure SVEpochStructure open Implementation -open import Ledger.Conway.Specification.Utxo.Properties.Computational SVTransactionStructure SVAbstractFunctions -open import Ledger.Conway.Specification.Utxow.Properties.Computational SVTransactionStructure SVAbstractFunctions -- Make this get all output datums getInlineOutputDatum : STxOut → List MultiSigData → Maybe Datum diff --git a/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/AddSig.agda b/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/AddSig.agda index 74eb86365..6cbbe30a3 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/AddSig.agda +++ b/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/AddSig.agda @@ -1,27 +1,25 @@ {-# OPTIONS --safe #-} -open import Ledger.Prelude hiding (fromList; ε); open Computational +module Ledger.Conway.Specification.Test.Examples.MultiSigV2.OffChain.AddSig where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction + open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.Datum +open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.OffChain.Lib open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.Validator open import Ledger.Conway.Specification.Test.Prelude MultiSigData open import Ledger.Conway.Specification.Test.SymbolicData MultiSigData open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Transaction using (TransactionStructure) -open TransactionStructure SVTransactionStructure -open import Ledger.Conway.Specification.Test.AbstractImplementation SData SData valContext -open import Ledger.Conway.Specification.Test.Lib SData SData valContext +open import Ledger.Conway.Specification.Test.AbstractImplementation valContext +open import Ledger.Conway.Specification.Test.Lib valContext + open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions -open import Data.Empty open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions -open import Ledger.Conway.Specification.Transaction -open import Ledger.Core.Specification.Epoch -open EpochStructure SVEpochStructure + +open TransactionStructure SVTransactionStructure open Implementation -open import Ledger.Conway.Specification.Utxo.Properties.Computational SVTransactionStructure SVAbstractFunctions -open import Data.List using (filter) -open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.OffChain.Lib -module Ledger.Conway.Specification.Test.Examples.MultiSigV2.OffChain.AddSig where makeAddSigTxOut : Label → (scriptIx w : ℕ) → TxOut → List (ℕ × TxOut) makeAddSigTxOut Holding ix w txo = [] diff --git a/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Cancel.agda b/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Cancel.agda index 104c489f2..e1040fa18 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Cancel.agda +++ b/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Cancel.agda @@ -1,28 +1,24 @@ {-# OPTIONS --safe #-} -open import Ledger.Prelude hiding (fromList; ε); open Computational +module Ledger.Conway.Specification.Test.Examples.MultiSigV2.OffChain.Cancel where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction + open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.Datum +open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.OffChain.Lib open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.Validator open import Ledger.Conway.Specification.Test.Prelude MultiSigData open import Ledger.Conway.Specification.Test.SymbolicData MultiSigData open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Transaction using (TransactionStructure) -open TransactionStructure SVTransactionStructure -open import Ledger.Conway.Specification.Test.AbstractImplementation SData SData valContext -open import Ledger.Conway.Specification.Test.Lib SData SData valContext +open import Ledger.Conway.Specification.Test.AbstractImplementation valContext +open import Ledger.Conway.Specification.Test.Lib valContext + open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions -open import Data.Empty open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions -open import Ledger.Conway.Specification.Transaction -open import Ledger.Core.Specification.Epoch -open EpochStructure SVEpochStructure -open Implementation -open import Ledger.Conway.Specification.Utxo.Properties.Computational SVTransactionStructure SVAbstractFunctions -open import Data.List using (filter) -open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.OffChain.Lib - -module Ledger.Conway.Specification.Test.Examples.MultiSigV2.OffChain.Cancel where +open TransactionStructure SVTransactionStructure +open Implementation makeCancelTxOut : Label → (scriptIx w : ℕ) → TxOut → List (ℕ × TxOut) makeCancelTxOut Holding ix w txo = [] diff --git a/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Cleanup.agda b/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Cleanup.agda index 6cc9388ee..9f3680934 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Cleanup.agda +++ b/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Cleanup.agda @@ -1,28 +1,24 @@ {-# OPTIONS --safe #-} -open import Ledger.Prelude hiding (fromList; ε); open Computational +module Ledger.Conway.Specification.Test.Examples.MultiSigV2.OffChain.Cleanup where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction + open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.Datum +open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.OffChain.Lib open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.Validator open import Ledger.Conway.Specification.Test.Prelude MultiSigData open import Ledger.Conway.Specification.Test.SymbolicData MultiSigData open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Transaction using (TransactionStructure) -open TransactionStructure SVTransactionStructure -open import Ledger.Conway.Specification.Test.AbstractImplementation SData SData valContext -open import Ledger.Conway.Specification.Test.Lib SData SData valContext +open import Ledger.Conway.Specification.Test.AbstractImplementation valContext +open import Ledger.Conway.Specification.Test.Lib valContext + open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions -open import Data.Empty open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions -open import Ledger.Conway.Specification.Transaction -open import Ledger.Core.Specification.Epoch -open EpochStructure SVEpochStructure -open Implementation -open import Ledger.Conway.Specification.Utxo.Properties.Computational SVTransactionStructure SVAbstractFunctions -open import Data.List using (filter) -open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.OffChain.Lib - -module Ledger.Conway.Specification.Test.Examples.MultiSigV2.OffChain.Cleanup where +open TransactionStructure SVTransactionStructure +open Implementation makeCleanupTx : (id : ℕ) → UTxOState → PlutusScript → (w : ℕ) → Maybe Tx makeCleanupTx id state script@(sh , _) w = diff --git a/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Lib.agda b/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Lib.agda index aa81b93a4..8bd92207f 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Lib.agda +++ b/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Lib.agda @@ -1,28 +1,25 @@ {-# OPTIONS --safe #-} -open import Ledger.Prelude hiding (fromList; ε); open Computational +module Ledger.Conway.Specification.Test.Examples.MultiSigV2.OffChain.Lib where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction using (TransactionStructure) + open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.Datum open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.Validator open import Ledger.Conway.Specification.Test.Prelude MultiSigData open import Ledger.Conway.Specification.Test.SymbolicData MultiSigData open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Transaction using (TransactionStructure) -open TransactionStructure SVTransactionStructure -open import Ledger.Conway.Specification.Test.AbstractImplementation SData SData valContext -open import Ledger.Conway.Specification.Test.Lib SData SData valContext +open import Ledger.Conway.Specification.Test.AbstractImplementation valContext +open import Ledger.Conway.Specification.Test.Lib valContext + open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions -open import Data.Empty open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions -open import Ledger.Conway.Specification.Transaction -open import Ledger.Core.Specification.Epoch -open EpochStructure SVEpochStructure -open Implementation -open import Ledger.Conway.Specification.Utxo.Properties.Computational SVTransactionStructure SVAbstractFunctions -open import Data.List using (filter) -module Ledger.Conway.Specification.Test.Examples.MultiSigV2.OffChain.Lib where +open TransactionStructure SVTransactionStructure +open Implementation -open import Relation.Nullary +open import Data.List using (filter) defaultTxBody : TxBody defaultTxBody = record diff --git a/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Open.agda b/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Open.agda index 2ababa140..32a9d1e4a 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Open.agda +++ b/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Open.agda @@ -1,27 +1,24 @@ {-# OPTIONS --safe #-} -open import Ledger.Prelude hiding (fromList; ε); open Computational +module Ledger.Conway.Specification.Test.Examples.MultiSigV2.OffChain.Open where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction + open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.Datum +open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.OffChain.Lib open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.Validator open import Ledger.Conway.Specification.Test.Prelude MultiSigData open import Ledger.Conway.Specification.Test.SymbolicData MultiSigData open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Transaction using (TransactionStructure) -open TransactionStructure SVTransactionStructure -open import Ledger.Conway.Specification.Test.AbstractImplementation SData SData valContext -open import Ledger.Conway.Specification.Test.Lib SData SData valContext +open import Ledger.Conway.Specification.Test.AbstractImplementation valContext +open import Ledger.Conway.Specification.Test.Lib valContext + open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions -open import Data.Empty open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions -open import Ledger.Conway.Specification.Transaction -open import Ledger.Core.Specification.Epoch -open EpochStructure SVEpochStructure -open Implementation -open import Ledger.Conway.Specification.Utxo.Properties.Computational SVTransactionStructure SVAbstractFunctions -open import Data.List using (filter) -open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.OffChain.Lib -module Ledger.Conway.Specification.Test.Examples.MultiSigV2.OffChain.Open where +open TransactionStructure SVTransactionStructure +open Implementation openTxOut : Value → PlutusScript → TxOut openTxOut v script = inj₁ (record { net = 0 ; diff --git a/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Pay.agda b/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Pay.agda index 59b506cf3..444796561 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Pay.agda +++ b/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Pay.agda @@ -1,27 +1,25 @@ {-# OPTIONS --safe #-} -open import Ledger.Prelude hiding (fromList; ε); open Computational +module Ledger.Conway.Specification.Test.Examples.MultiSigV2.OffChain.Pay where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction + open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.Datum +open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.OffChain.Lib open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.Validator open import Ledger.Conway.Specification.Test.Prelude MultiSigData open import Ledger.Conway.Specification.Test.SymbolicData MultiSigData open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Transaction using (TransactionStructure) -open TransactionStructure SVTransactionStructure -open import Ledger.Conway.Specification.Test.AbstractImplementation SData SData valContext -open import Ledger.Conway.Specification.Test.Lib SData SData valContext +open import Ledger.Conway.Specification.Test.AbstractImplementation valContext +open import Ledger.Conway.Specification.Test.Lib valContext + open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions -open import Data.Empty open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions -open import Ledger.Conway.Specification.Transaction -open import Ledger.Core.Specification.Epoch -open EpochStructure SVEpochStructure + +open TransactionStructure SVTransactionStructure open Implementation -open import Ledger.Conway.Specification.Utxo.Properties.Computational SVTransactionStructure SVAbstractFunctions -open import Data.List using (filter) -open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.OffChain.Lib -module Ledger.Conway.Specification.Test.Examples.MultiSigV2.OffChain.Pay where payScriptTxOut : TxOut → (value : ℕ) → TxOut payScriptTxOut (fst , txValue , snd) v = fst , txValue - v , just (inj₁ (inj₁ (inj₁ Holding))) , nothing diff --git a/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Propose.agda b/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Propose.agda index e9cf61efb..972911fa5 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Propose.agda +++ b/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Propose.agda @@ -1,27 +1,25 @@ {-# OPTIONS --safe #-} -open import Ledger.Prelude hiding (fromList; ε); open Computational +module Ledger.Conway.Specification.Test.Examples.MultiSigV2.OffChain.Propose where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction + open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.Datum +open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.OffChain.Lib open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.Validator open import Ledger.Conway.Specification.Test.Prelude MultiSigData open import Ledger.Conway.Specification.Test.SymbolicData MultiSigData open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Transaction using (TransactionStructure) -open TransactionStructure SVTransactionStructure -open import Ledger.Conway.Specification.Test.AbstractImplementation SData SData valContext -open import Ledger.Conway.Specification.Test.Lib SData SData valContext +open import Ledger.Conway.Specification.Test.AbstractImplementation valContext +open import Ledger.Conway.Specification.Test.Lib valContext + open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions -open import Data.Empty open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions -open import Ledger.Conway.Specification.Transaction -open import Ledger.Core.Specification.Epoch -open EpochStructure SVEpochStructure + +open TransactionStructure SVTransactionStructure open Implementation -open import Ledger.Conway.Specification.Utxo.Properties.Computational SVTransactionStructure SVAbstractFunctions -open import Data.List using (filter) -open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.OffChain.Lib -module Ledger.Conway.Specification.Test.Examples.MultiSigV2.OffChain.Propose where -- TODO: Add error handling makeProposeTxOut : Label → (scriptIx : ℕ) → TxOut → (v tw d : ℕ) → List (ℕ × TxOut) diff --git a/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/Test/Trace.agda b/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/Test/Trace.agda index ab9760e2a..8c64ffb69 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/Test/Trace.agda +++ b/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/Test/Trace.agda @@ -1,27 +1,27 @@ {-# OPTIONS --safe #-} -open import Ledger.Prelude hiding (fromList; ε); open Computational +module Ledger.Conway.Specification.Test.Examples.MultiSigV2.Test.Trace where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction + open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.Datum +open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.OffChain.Lib open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.Validator open import Ledger.Conway.Specification.Test.Prelude MultiSigData open import Ledger.Conway.Specification.Test.SymbolicData MultiSigData open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Transaction using (TransactionStructure) -open TransactionStructure SVTransactionStructure -open import Ledger.Conway.Specification.Test.AbstractImplementation SData SData valContext -open import Ledger.Conway.Specification.Test.Lib SData SData valContext +open import Ledger.Conway.Specification.Test.AbstractImplementation valContext +open import Ledger.Conway.Specification.Test.Lib valContext + open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions -open import Data.Empty open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions -open import Ledger.Conway.Specification.Transaction -open import Ledger.Core.Specification.Epoch -open EpochStructure SVEpochStructure -open Implementation open import Ledger.Conway.Specification.Utxo.Properties.Computational SVTransactionStructure SVAbstractFunctions open import Ledger.Conway.Specification.Utxow.Properties.Computational SVTransactionStructure SVAbstractFunctions -open import Data.List using (filter) -module Ledger.Conway.Specification.Test.Examples.MultiSigV2.Test.Trace where +open TransactionStructure SVTransactionStructure +open Implementation + open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.OffChain.OffChain diff --git a/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/Validator.agda b/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/Validator.agda index e15573dfc..c5c1a166b 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/Validator.agda +++ b/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/Validator.agda @@ -34,8 +34,8 @@ instance open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData open import Ledger.Conway.Specification.Transaction using (TransactionStructure) open TransactionStructure SVTransactionStructure -open import Ledger.Conway.Specification.Test.AbstractImplementation SData SData valContext -open import Ledger.Conway.Specification.Test.Lib SData SData valContext +open import Ledger.Conway.Specification.Test.AbstractImplementation valContext +open import Ledger.Conway.Specification.Test.Lib valContext open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions open import Data.Empty open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions diff --git a/src/Ledger/Conway/Specification/Test/Examples/SucceedIfNumber.lagda.md b/src/Ledger/Conway/Specification/Test/Examples/SucceedIfNumber.lagda.md index fd2ade0a0..bcffc91cf 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/SucceedIfNumber.lagda.md +++ b/src/Ledger/Conway/Specification/Test/Examples/SucceedIfNumber.lagda.md @@ -11,14 +11,16 @@ open import Ledger.Prelude hiding (fromList; ε); open Computational open import Ledger.Conway.Specification.Test.Prelude module Ledger.Conway.Specification.Test.Examples.SucceedIfNumber where +open import Ledger.Conway.Specification.Test.LedgerImplementation ℕ ℕ +open import Ledger.Conway.Specification.Transaction using (TransactionStructure) +open TransactionStructure SVTransactionStructure using (Data) +open import Ledger.Conway.Specification.ScriptPurpose SVTransactionStructure -scriptImp : ScriptImplementation ℕ ℕ -scriptImp = record { serialise = id ; - deserialise = λ x → just x ; - toData' = λ x → 9999999 } +valContext : TxInfo → ScriptPurpose → Data +valContext x x₁ = 0 -open import Ledger.Conway.Specification.Test.LedgerImplementation ℕ ℕ scriptImp -open import Ledger.Conway.Specification.Test.Lib ℕ ℕ scriptImp +open import Ledger.Conway.Specification.Test.AbstractImplementation ℕ ℕ valContext +open import Ledger.Conway.Specification.Test.Lib ℕ ℕ valContext open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions open import Ledger.Conway.Specification.Transaction @@ -77,7 +79,6 @@ succeedTx : Tx succeedTx = record { body = record { txIns = Ledger.Prelude.fromList ((6 , 6) ∷ (5 , 5) ∷ []) ; refInputs = ∅ - ; collateralInputs = Ledger.Prelude.fromList ((5 , 5) ∷ []) ; txOuts = fromListIx ((6 , initTxOut) ∷ (5 , ((inj₁ (record { net = 0 ; @@ -85,18 +86,19 @@ succeedTx = record { body = record stake = just (KeyHashObj 5) })) , (1000000000000 - 10000000000) , nothing , nothing)) ∷ []) - ; txId = 7 - ; txCerts = [] ; txFee = 10000000000 - ; txWithdrawals = ∅ + ; mint = 0 ; txVldt = nothing , nothing - ; txADhash = nothing - ; txDonation = 0 + ; txCerts = [] + ; txWithdrawals = ∅ ; txGovVotes = [] ; txGovProposals = [] + ; txDonation = 0 + ; txADhash = nothing ; txNetworkId = just 0 ; currentTreasury = nothing - ; mint = 0 + ; txId = 7 + ; collateralInputs = Ledger.Prelude.fromList ((5 , 5) ∷ []) ; reqSignerHashes = ∅ ; scriptIntegrityHash = nothing } ; @@ -118,20 +120,20 @@ failTx : Tx failTx = record { body = record { txIns = Ledger.Prelude.fromList ((6 , 6) ∷ []) ; refInputs = ∅ - ; collateralInputs = ∅ ; txOuts = ∅ - ; txId = 7 - ; txCerts = [] ; txFee = 10 - ; txWithdrawals = ∅ + ; mint = 0 ; txVldt = nothing , nothing - ; txADhash = nothing - ; txDonation = 0 + ; txCerts = [] + ; txWithdrawals = ∅ ; txGovVotes = [] ; txGovProposals = [] + ; txDonation = 0 + ; txADhash = nothing ; txNetworkId = just 0 ; currentTreasury = nothing - ; mint = 0 + ; txId = 7 + ; collateralInputs = ∅ ; reqSignerHashes = ∅ ; scriptIntegrityHash = nothing } ; @@ -201,3 +203,4 @@ opaque _ : failExampleU ≡ false _ = refl + diff --git a/src/Ledger/Conway/Specification/Test/Lib.lagda.md b/src/Ledger/Conway/Specification/Test/Lib.lagda.md index 8db65644b..3f35964d6 100644 --- a/src/Ledger/Conway/Specification/Test/Lib.lagda.md +++ b/src/Ledger/Conway/Specification/Test/Lib.lagda.md @@ -6,32 +6,26 @@ source_path: src/Ledger/Conway/Specification/Test/Lib.lagda.md ```agda {-# OPTIONS --safe #-} -open import Ledger.Prelude hiding (fromList; ε; _/_); open Computational -open import Ledger.Conway.Specification.Test.Prelude -open import Ledger.Conway.Specification.Transaction using (TransactionStructure) +open import Ledger.Prelude hiding (fromList; ε; _/_) open import Ledger.Conway.Specification.Test.LedgerImplementation using (SVTransactionStructure) -open import Ledger.Conway.Specification.ScriptPurpose using () +import Ledger.Conway.Specification.Script.ScriptPurpose as SP -module Ledger.Conway.Specification.Test.Lib (T D : Set){{DecEq-Data : DecEq D}}{{Show-Data : Show D}} - -- (open TransactionStructure (SVTransactionStructure T D) using (TxInfo; ScriptPurpose)) - (open Ledger.Conway.Specification.ScriptPurpose (SVTransactionStructure T D) using (TxInfo; ScriptPurpose)) +module Ledger.Conway.Specification.Test.Lib + {T D : Set}{{DecEq-Data : DecEq D}}{{Show-Data : Show D}} + (open SP (SVTransactionStructure T D) using (TxInfo; ScriptPurpose)) (valContext' : TxInfo → ScriptPurpose → D) where -open import Ledger.Conway.Specification.Test.AbstractImplementation T D valContext' -open import Ledger.Conway.Specification.Test.LedgerImplementation T D +open import Ledger.Conway.Specification.Test.AbstractImplementation valContext' +open import Ledger.Conway.Specification.Test.LedgerImplementation T D renaming (SVTransactionStructure to SVTransactionStructure') -open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure' SVAbstractFunctions open import Ledger.Conway.Specification.Utxo SVTransactionStructure' SVAbstractFunctions -open import Ledger.Conway.Specification.Transaction +open import Ledger.Conway.Specification.Transaction using (TransactionStructure) open TransactionStructure SVTransactionStructure' -open import Ledger.Core.Specification.Epoch open import Ledger.Prelude.Numeric using (mkUnitInterval; mkℕ⁺) -open EpochStructure SVEpochStructure open import Data.Integer using (ℤ; +_) open import Data.Rational using (½; 1ℚ ; mkℚ+ ; _/_) open import Data.Nat.Coprimality using (Coprime; gcd≡1⇒coprime) -open Implementation createEnv : ℕ → UTxOEnv createEnv s = record { slot = s ; treasury = 0 ; diff --git a/src/Ledger/Conway/Specification/Test/StructuredContracts.lagda.md b/src/Ledger/Conway/Specification/Test/StructuredContracts.lagda.md index 7474069c5..064bf6df0 100644 --- a/src/Ledger/Conway/Specification/Test/StructuredContracts.lagda.md +++ b/src/Ledger/Conway/Specification/Test/StructuredContracts.lagda.md @@ -22,22 +22,23 @@ module Ledger.Conway.Specification.Test.StructuredContracts where open import Ledger.Conway.Specification.Ledger txs abs +open import Ledger.Conway.Specification.ScriptPurpose txs open import Ledger.Conway.Specification.Script.Validation txs abs open import Ledger.Conway.Specification.Utxo txs abs \end{code} -Defining an instance of the $\type{StrucSimulation}$ record constitutes implementing a -stateful program on (the Agda specification of) the Cardano ledger. The following +Defining an instance of the $\type{StrucSimulation}$ record constitutes implementing a +stateful program on (the Agda specification of) the Cardano ledger. The following must be specified when defining such an instance: \begin{itemize} -\item[(i)] $\type{S}$ - the program state type -\item[(ii)] $\type{S}$ - the program input type +\item[(i)] $\type{S}$ - the program state type +\item[(ii)] $\type{S}$ - the program input type \item[(iii)] $\type{STRUC}$ - the program's small-step semantics -\item[(iv)] $\type{\pi^{s}}$ - projection function of program state from a given ledger state -\item[(v)] $\type{\pi^{i}}$ - projection function of program input from a given $\type{TxInfo}$ +\item[(iv)] $\type{\pi^{s}}$ - projection function of program state from a given ledger state +\item[(v)] $\type{\pi^{i}}$ - projection function of program input from a given $\type{TxInfo}$ \item[(vi)] $\type{simulates}$ - proof obligation required for demonstrating that data in (i)-(v) -is such that state of the program as it appears on the ledger can only be updated according to its +is such that state of the program as it appears on the ledger can only be updated according to its small-step $\type{STRUC}$ specification \end{itemize} @@ -52,7 +53,7 @@ record StrucSimulation S I (_⊢_⇀⦇_,STRUC⦈_ : SSRel ⊤ S I) : Type₁ wh -- here, add optional extra assumptions about ledger state, env, and transaction that may be too difficult to prove without reasoning about complete ledger traces -- e.g. transaction does not re-add a UTxO entry it spends -- e.g. current Slot is after the validity interval of some previous transaction - extraAssmp : LEnv → LState → Tx → Type + extraAssmp : LEnv → LState → Tx → Type _~ˢ_ : LState → S → Type -- R u ~ˢ s = πˢ u ≡ just s diff --git a/src/Ledger/Conway/Specification/Test/SymbolicData.agda b/src/Ledger/Conway/Specification/Test/SymbolicData.agda index f17c07959..5a9473c2e 100644 --- a/src/Ledger/Conway/Specification/Test/SymbolicData.agda +++ b/src/Ledger/Conway/Specification/Test/SymbolicData.agda @@ -1,21 +1,27 @@ {-# OPTIONS --safe #-} -open import Ledger.Prelude hiding (fromList; ε); open Computational +open import Ledger.Prelude -module Ledger.Conway.Specification.Test.SymbolicData (SD : Set) {{DecEq-Data : DecEq SD}} {{Show-Data : Show SD}} where +module Ledger.Conway.Specification.Test.SymbolicData + (SD : Set) {{DecEq-Data : DecEq SD}} {{Show-Data : Show SD}} where open import Ledger.Conway.Specification.Test.Prelude SD +ScriptContext : Type ScriptContext = STxInfo × SScriptPurpose + +SData : Type SData = SDatum ⊎ ScriptContext instance ShowSData : Show SData ShowSData = mkShow (λ x → "") open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData +open import Ledger.Conway.Specification.Script.ScriptPurpose SVTransactionStructure + open import Ledger.Conway.Specification.Transaction using (TransactionStructure) -open import Ledger.Conway.Specification.ScriptPurpose SVTransactionStructure -open TransactionStructure SVTransactionStructure +open TransactionStructure SVTransactionStructure + open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure TxInToSymbolic : TxIn → STxIn From 5798e9ec813c54bf5e404b40e5bdeefd8ab1868d Mon Sep 17 00:00:00 2001 From: tferariu Date: Mon, 27 Oct 2025 17:00:51 +0000 Subject: [PATCH 06/11] Changed Example.agda to a markdown file with added descriptions --- .../Specification/Test/Examples.lagda.md | 127 ++++++++++++++++++ .../Test/Examples/DEx/Test/Trace.agda | 2 +- 2 files changed, 128 insertions(+), 1 deletion(-) diff --git a/src/Ledger/Conway/Specification/Test/Examples.lagda.md b/src/Ledger/Conway/Specification/Test/Examples.lagda.md index e68772ef4..af2656c04 100644 --- a/src/Ledger/Conway/Specification/Test/Examples.lagda.md +++ b/src/Ledger/Conway/Specification/Test/Examples.lagda.md @@ -3,6 +3,12 @@ source_branch: master source_path: src/Ledger/Conway/Specification/Test/Examples.lagda.md --- +The "Examples" module aims to add a couple of example smart contract +validators written as part of the Cardano Formal Ledger Specification. +These validator scripts are functions that examine a transaction and decide +if the UTxO locked by their script can be spent as part of the current +transaction. + -```agda -import Ledger.Conway.Specification.Test.Examples.SucceedIfNumber -import Ledger.Conway.Specification.Test.Examples.HelloWorld +module Test.Examples where +import Test.Examples.SucceedIfNumber +import Test.Examples.HelloWorld ``` +--> The first two examples, "SucceedIfNumber" and "HelloWorld" are very simple scripts that allow their UTxO to be spent if the input is a number or @@ -35,11 +33,9 @@ The other examples are more in-depth and are separated across multiple modules. ```agda - -import Ledger.Conway.Specification.Test.Examples.MultiSig.Datum -import Ledger.Conway.Specification.Test.Examples.MultiSig.Validator -import Ledger.Conway.Specification.Test.Examples.MultiSig.Test.Trace - +import Test.Examples.MultiSig.Datum +import Test.Examples.MultiSig.Validator +import Test.Examples.MultiSig.Test.Trace ``` The "MultiSig" example is based on the Multi-Signature wallet smart @@ -99,13 +95,11 @@ to propose another payment of a larger amount than is contained in the wallet, which naturally fails. ```agda - - -import Ledger.Conway.Specification.Test.Examples.AccountSim.Datum -import Ledger.Conway.Specification.Test.Examples.AccountSim.Validator -import Ledger.Conway.Specification.Test.Examples.AccountSim.Test.Trace - +import Test.Examples.AccountSim.Datum +import Test.Examples.AccountSim.Validator +import Test.Examples.AccountSim.Test.Trace ``` + The "AccountSim" contract attempts to simulate an account-based system on UTxO. It is a naive implementation which holds all accounts represented as a list of pairs linking a Public Key Hash to its associated Value. @@ -121,11 +115,9 @@ account has in it. ```agda - -import Ledger.Conway.Specification.Test.Examples.DEx.Datum -import Ledger.Conway.Specification.Test.Examples.DEx.Validator -import Ledger.Conway.Specification.Test.Examples.DEx.Test.Trace - +import Test.Examples.DEx.Datum +import Test.Examples.DEx.Validator +import Test.Examples.DEx.Test.Trace ``` The "DEx" contract is meant to implement a Limit Order Book @@ -137,11 +129,9 @@ the code can be easily modified to fulfill its full purpose. ```agda - -import Ledger.Conway.Specification.Test.Examples.MultiSigV2.Datum -import Ledger.Conway.Specification.Test.Examples.MultiSigV2.Validator -import Ledger.Conway.Specification.Test.Examples.MultiSigV2.Test.Trace - +import Test.Examples.MultiSigV2.Datum +import Test.Examples.MultiSigV2.Validator +import Test.Examples.MultiSigV2.Test.Trace ``` The second implementation of "MultiSig" is, at its core, the same diff --git a/src/Ledger/Conway/Specification/Test/Examples/AccountSim/Datum.agda b/src/Test/Examples/AccountSim/Datum.agda similarity index 86% rename from src/Ledger/Conway/Specification/Test/Examples/AccountSim/Datum.agda rename to src/Test/Examples/AccountSim/Datum.agda index 3c91bb622..dde66212f 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/AccountSim/Datum.agda +++ b/src/Test/Examples/AccountSim/Datum.agda @@ -2,7 +2,7 @@ open import Ledger.Prelude hiding (fromList; ε); open Computational -module Ledger.Conway.Specification.Test.Examples.AccountSim.Datum where +module Test.Examples.AccountSim.Datum where open import Tactic.Derive.DecEq open import Data.Vec as Vec @@ -11,7 +11,7 @@ import stdlib.Data.Vec.Instances as Vec import Data.Vec.Relation.Binary.Pointwise.Inductive as Vec data Label : Set where - Always : List (ℕ × ℕ) -> Label + Always : List (ℕ × ℕ) -> Label instance unquoteDecl DecEq-Label = derive-DecEq ((quote Label , DecEq-Label) ∷ []) diff --git a/src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Cleanup.agda b/src/Test/Examples/AccountSim/OffChain/Cleanup.agda similarity index 71% rename from src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Cleanup.agda rename to src/Test/Examples/AccountSim/OffChain/Cleanup.agda index 3cc1e5512..f98e950ca 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Cleanup.agda +++ b/src/Test/Examples/AccountSim/OffChain/Cleanup.agda @@ -1,18 +1,18 @@ {-# OPTIONS --safe #-} -module Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.Cleanup where +module Test.Examples.AccountSim.OffChain.Cleanup where open import Ledger.Prelude open import Ledger.Conway.Specification.Transaction -open import Ledger.Conway.Specification.Test.Examples.AccountSim.Datum -open import Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.Lib -open import Ledger.Conway.Specification.Test.Examples.AccountSim.Validator -open import Ledger.Conway.Specification.Test.Prelude AccountSimData -open import Ledger.Conway.Specification.Test.SymbolicData AccountSimData -open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Test.AbstractImplementation valContext -open import Ledger.Conway.Specification.Test.Lib valContext +open import Test.Examples.AccountSim.Datum +open import Test.Examples.AccountSim.OffChain.Lib +open import Test.Examples.AccountSim.Validator +open import Test.Prelude AccountSimData +open import Test.SymbolicData AccountSimData +open import Test.LedgerImplementation SData SData +open import Test.AbstractImplementation valContext +open import Test.Lib valContext open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions diff --git a/src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Close.agda b/src/Test/Examples/AccountSim/OffChain/Close.agda similarity index 74% rename from src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Close.agda rename to src/Test/Examples/AccountSim/OffChain/Close.agda index 628f3f3a9..cbeb54f53 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Close.agda +++ b/src/Test/Examples/AccountSim/OffChain/Close.agda @@ -1,18 +1,18 @@ {-# OPTIONS --safe #-} -module Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.Close where +module Test.Examples.AccountSim.OffChain.Close where open import Ledger.Prelude open import Ledger.Conway.Specification.Transaction -open import Ledger.Conway.Specification.Test.Examples.AccountSim.Datum -open import Ledger.Conway.Specification.Test.Examples.AccountSim.Validator -open import Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.Lib -open import Ledger.Conway.Specification.Test.Prelude AccountSimData -open import Ledger.Conway.Specification.Test.SymbolicData AccountSimData -open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Test.AbstractImplementation valContext -open import Ledger.Conway.Specification.Test.Lib valContext +open import Test.Examples.AccountSim.Datum +open import Test.Examples.AccountSim.Validator +open import Test.Examples.AccountSim.OffChain.Lib +open import Test.Prelude AccountSimData +open import Test.SymbolicData AccountSimData +open import Test.LedgerImplementation SData SData +open import Test.AbstractImplementation valContext +open import Test.Lib valContext open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions diff --git a/src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Deposit.agda b/src/Test/Examples/AccountSim/OffChain/Deposit.agda similarity index 77% rename from src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Deposit.agda rename to src/Test/Examples/AccountSim/OffChain/Deposit.agda index 2f73aaae6..26d5057f6 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Deposit.agda +++ b/src/Test/Examples/AccountSim/OffChain/Deposit.agda @@ -1,18 +1,18 @@ {-# OPTIONS --safe #-} -module Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.Deposit where +module Test.Examples.AccountSim.OffChain.Deposit where open import Ledger.Prelude open import Ledger.Conway.Specification.Transaction -open import Ledger.Conway.Specification.Test.Examples.AccountSim.Datum -open import Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.Lib -open import Ledger.Conway.Specification.Test.Examples.AccountSim.Validator -open import Ledger.Conway.Specification.Test.Prelude AccountSimData -open import Ledger.Conway.Specification.Test.SymbolicData AccountSimData -open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Test.AbstractImplementation valContext -open import Ledger.Conway.Specification.Test.Lib valContext +open import Test.Examples.AccountSim.Datum +open import Test.Examples.AccountSim.OffChain.Lib +open import Test.Examples.AccountSim.Validator +open import Test.Prelude AccountSimData +open import Test.SymbolicData AccountSimData +open import Test.LedgerImplementation SData SData +open import Test.AbstractImplementation valContext +open import Test.Lib valContext open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions diff --git a/src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Lib.agda b/src/Test/Examples/AccountSim/OffChain/Lib.agda similarity index 88% rename from src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Lib.agda rename to src/Test/Examples/AccountSim/OffChain/Lib.agda index 9ca347d0f..cbf113248 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Lib.agda +++ b/src/Test/Examples/AccountSim/OffChain/Lib.agda @@ -1,17 +1,17 @@ {-# OPTIONS --safe #-} -module Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.Lib where +module Test.Examples.AccountSim.OffChain.Lib where open import Data.List using (filter) open import Ledger.Prelude open import Ledger.Conway.Specification.Transaction using (TransactionStructure) -open import Ledger.Conway.Specification.Test.Examples.AccountSim.Datum -open import Ledger.Conway.Specification.Test.Examples.AccountSim.Validator -open import Ledger.Conway.Specification.Test.Prelude AccountSimData -open import Ledger.Conway.Specification.Test.SymbolicData AccountSimData -open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData +open import Test.Examples.AccountSim.Datum +open import Test.Examples.AccountSim.Validator +open import Test.Prelude AccountSimData +open import Test.SymbolicData AccountSimData +open import Test.LedgerImplementation SData SData open TransactionStructure SVTransactionStructure diff --git a/src/Test/Examples/AccountSim/OffChain/OffChain.agda b/src/Test/Examples/AccountSim/OffChain/OffChain.agda new file mode 100644 index 000000000..26af09991 --- /dev/null +++ b/src/Test/Examples/AccountSim/OffChain/OffChain.agda @@ -0,0 +1,11 @@ +{-# OPTIONS --safe #-} + +module Test.Examples.AccountSim.OffChain.OffChain where + +open import Test.Examples.AccountSim.OffChain.Start public +open import Test.Examples.AccountSim.OffChain.Close public +open import Test.Examples.AccountSim.OffChain.Open public +open import Test.Examples.AccountSim.OffChain.Deposit public +open import Test.Examples.AccountSim.OffChain.Withdraw public +open import Test.Examples.AccountSim.OffChain.Transfer public +open import Test.Examples.AccountSim.OffChain.Cleanup public diff --git a/src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Open.agda b/src/Test/Examples/AccountSim/OffChain/Open.agda similarity index 75% rename from src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Open.agda rename to src/Test/Examples/AccountSim/OffChain/Open.agda index 383ab9708..48fbf6e03 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Open.agda +++ b/src/Test/Examples/AccountSim/OffChain/Open.agda @@ -1,18 +1,18 @@ {-# OPTIONS --safe #-} -module Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.Open where +module Test.Examples.AccountSim.OffChain.Open where open import Ledger.Prelude open import Ledger.Conway.Specification.Transaction -open import Ledger.Conway.Specification.Test.Examples.AccountSim.Datum -open import Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.Lib -open import Ledger.Conway.Specification.Test.Examples.AccountSim.Validator -open import Ledger.Conway.Specification.Test.Prelude AccountSimData -open import Ledger.Conway.Specification.Test.SymbolicData AccountSimData -open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Test.AbstractImplementation valContext -open import Ledger.Conway.Specification.Test.Lib valContext +open import Test.Examples.AccountSim.Datum +open import Test.Examples.AccountSim.OffChain.Lib +open import Test.Examples.AccountSim.Validator +open import Test.Prelude AccountSimData +open import Test.SymbolicData AccountSimData +open import Test.LedgerImplementation SData SData +open import Test.AbstractImplementation valContext +open import Test.Lib valContext open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions diff --git a/src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Start.agda b/src/Test/Examples/AccountSim/OffChain/Start.agda similarity index 75% rename from src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Start.agda rename to src/Test/Examples/AccountSim/OffChain/Start.agda index fc3e3065f..d54fac4d1 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Start.agda +++ b/src/Test/Examples/AccountSim/OffChain/Start.agda @@ -1,17 +1,17 @@ {-# OPTIONS --safe #-} -module Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.Start where +module Test.Examples.AccountSim.OffChain.Start where open import Ledger.Prelude open import Ledger.Conway.Specification.Transaction using (TransactionStructure) -open import Ledger.Conway.Specification.Test.Examples.AccountSim.Datum -open import Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.Lib -open import Ledger.Conway.Specification.Test.Examples.AccountSim.Validator -open import Ledger.Conway.Specification.Test.Prelude AccountSimData -open import Ledger.Conway.Specification.Test.SymbolicData AccountSimData -open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Test.Lib valContext +open import Test.Examples.AccountSim.Datum +open import Test.Examples.AccountSim.OffChain.Lib +open import Test.Examples.AccountSim.Validator +open import Test.Prelude AccountSimData +open import Test.SymbolicData AccountSimData +open import Test.LedgerImplementation SData SData +open import Test.Lib valContext open TransactionStructure SVTransactionStructure open Implementation diff --git a/src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Transfer.agda b/src/Test/Examples/AccountSim/OffChain/Transfer.agda similarity index 76% rename from src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Transfer.agda rename to src/Test/Examples/AccountSim/OffChain/Transfer.agda index 9c4e8ffd7..31c10a031 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Transfer.agda +++ b/src/Test/Examples/AccountSim/OffChain/Transfer.agda @@ -1,18 +1,18 @@ {-# OPTIONS --safe #-} -module Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.Transfer where +module Test.Examples.AccountSim.OffChain.Transfer where open import Ledger.Prelude open import Ledger.Conway.Specification.Transaction -open import Ledger.Conway.Specification.Test.Examples.AccountSim.Datum -open import Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.Lib -open import Ledger.Conway.Specification.Test.Examples.AccountSim.Validator -open import Ledger.Conway.Specification.Test.Prelude AccountSimData -open import Ledger.Conway.Specification.Test.SymbolicData AccountSimData -open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Test.AbstractImplementation valContext -open import Ledger.Conway.Specification.Test.Lib valContext +open import Test.Examples.AccountSim.Datum +open import Test.Examples.AccountSim.OffChain.Lib +open import Test.Examples.AccountSim.Validator +open import Test.Prelude AccountSimData +open import Test.SymbolicData AccountSimData +open import Test.LedgerImplementation SData SData +open import Test.AbstractImplementation valContext +open import Test.Lib valContext open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions diff --git a/src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Withdraw.agda b/src/Test/Examples/AccountSim/OffChain/Withdraw.agda similarity index 77% rename from src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Withdraw.agda rename to src/Test/Examples/AccountSim/OffChain/Withdraw.agda index 797ce5069..e39f5e4ef 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Withdraw.agda +++ b/src/Test/Examples/AccountSim/OffChain/Withdraw.agda @@ -1,18 +1,18 @@ {-# OPTIONS --safe #-} -module Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.Withdraw where +module Test.Examples.AccountSim.OffChain.Withdraw where open import Ledger.Prelude open import Ledger.Conway.Specification.Transaction -open import Ledger.Conway.Specification.Test.Examples.AccountSim.Datum -open import Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.Lib -open import Ledger.Conway.Specification.Test.Examples.AccountSim.Validator -open import Ledger.Conway.Specification.Test.Prelude AccountSimData -open import Ledger.Conway.Specification.Test.SymbolicData AccountSimData -open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Test.AbstractImplementation valContext -open import Ledger.Conway.Specification.Test.Lib valContext +open import Test.Examples.AccountSim.Datum +open import Test.Examples.AccountSim.OffChain.Lib +open import Test.Examples.AccountSim.Validator +open import Test.Prelude AccountSimData +open import Test.SymbolicData AccountSimData +open import Test.LedgerImplementation SData SData +open import Test.AbstractImplementation valContext +open import Test.Lib valContext open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions diff --git a/src/Ledger/Conway/Specification/Test/Examples/AccountSim/Test/Trace.agda b/src/Test/Examples/AccountSim/Test/Trace.agda similarity index 88% rename from src/Ledger/Conway/Specification/Test/Examples/AccountSim/Test/Trace.agda rename to src/Test/Examples/AccountSim/Test/Trace.agda index 46b669c9d..4c2326e0f 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/AccountSim/Test/Trace.agda +++ b/src/Test/Examples/AccountSim/Test/Trace.agda @@ -1,18 +1,18 @@ {-# OPTIONS --safe #-} -module Ledger.Conway.Specification.Test.Examples.AccountSim.Test.Trace where +module Test.Examples.AccountSim.Test.Trace where open import Ledger.Prelude open import Ledger.Conway.Specification.Transaction using (TransactionStructure) -open import Ledger.Conway.Specification.Test.Examples.AccountSim.Datum -open import Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.OffChain -open import Ledger.Conway.Specification.Test.Examples.AccountSim.Validator -open import Ledger.Conway.Specification.Test.Prelude AccountSimData -open import Ledger.Conway.Specification.Test.SymbolicData AccountSimData -open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Test.AbstractImplementation valContext -open import Ledger.Conway.Specification.Test.Lib valContext +open import Test.Examples.AccountSim.Datum +open import Test.Examples.AccountSim.OffChain.OffChain +open import Test.Examples.AccountSim.Validator +open import Test.Prelude AccountSimData +open import Test.SymbolicData AccountSimData +open import Test.LedgerImplementation SData SData +open import Test.AbstractImplementation valContext +open import Test.Lib valContext open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions diff --git a/src/Ledger/Conway/Specification/Test/Examples/AccountSim/Validator.agda b/src/Test/Examples/AccountSim/Validator.agda similarity index 95% rename from src/Ledger/Conway/Specification/Test/Examples/AccountSim/Validator.agda rename to src/Test/Examples/AccountSim/Validator.agda index 858ef6eed..28b3e84d6 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/AccountSim/Validator.agda +++ b/src/Test/Examples/AccountSim/Validator.agda @@ -2,16 +2,16 @@ -- Validator Simulating Accounts on Cardano based on Agda2hs work -module Ledger.Conway.Specification.Test.Examples.AccountSim.Validator where +module Test.Examples.AccountSim.Validator where open import Data.Bool.Base renaming (_∧_ to _&&_) hiding (if_then_else_) open import Data.List using (filter) open import Data.Maybe renaming (map to maybeMap) open import Ledger.Prelude -open import Ledger.Conway.Specification.Test.Examples.AccountSim.Datum -open import Ledger.Conway.Specification.Test.Prelude AccountSimData -open import Ledger.Conway.Specification.Test.SymbolicData AccountSimData +open import Test.Examples.AccountSim.Datum +open import Test.Prelude AccountSimData +open import Test.SymbolicData AccountSimData import Agda.Builtin.Nat as N @@ -22,7 +22,7 @@ instance ShowAccountSimData : Show AccountSimData ShowAccountSimData = mkShow (λ x → "") -open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData +open import Test.LedgerImplementation SData SData open import Ledger.Conway.Specification.Transaction using (TransactionStructure) open TransactionStructure SVTransactionStructure @@ -40,7 +40,7 @@ scriptValue : Value scriptValue = 30000000000 adaValueOf : ℕ -> Value -adaValueOf n = n +adaValueOf n = n geq : Value -> Value -> Bool diff --git a/src/Ledger/Conway/Specification/Test/Examples/DEx/Datum.agda b/src/Test/Examples/DEx/Datum.agda similarity index 91% rename from src/Ledger/Conway/Specification/Test/Examples/DEx/Datum.agda rename to src/Test/Examples/DEx/Datum.agda index 93f4411b9..5c266fa35 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/DEx/Datum.agda +++ b/src/Test/Examples/DEx/Datum.agda @@ -2,7 +2,7 @@ open import Ledger.Prelude hiding (fromList; ε); open Computational -module Ledger.Conway.Specification.Test.Examples.DEx.Datum where +module Test.Examples.DEx.Datum where open import Tactic.Derive.DecEq open import Data.Vec as Vec diff --git a/src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/Close.agda b/src/Test/Examples/DEx/OffChain/Close.agda similarity index 72% rename from src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/Close.agda rename to src/Test/Examples/DEx/OffChain/Close.agda index 9b07b0424..f541af964 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/Close.agda +++ b/src/Test/Examples/DEx/OffChain/Close.agda @@ -1,18 +1,18 @@ {-# OPTIONS --safe #-} -module Ledger.Conway.Specification.Test.Examples.DEx.OffChain.Close where +module Test.Examples.DEx.OffChain.Close where open import Ledger.Prelude open import Ledger.Conway.Specification.Transaction -open import Ledger.Conway.Specification.Test.Examples.DEx.Datum -open import Ledger.Conway.Specification.Test.Examples.DEx.Validator -open import Ledger.Conway.Specification.Test.Examples.DEx.OffChain.Lib -open import Ledger.Conway.Specification.Test.Prelude DExData -open import Ledger.Conway.Specification.Test.SymbolicData DExData -open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Test.AbstractImplementation valContext -open import Ledger.Conway.Specification.Test.Lib valContext +open import Test.Examples.DEx.Datum +open import Test.Examples.DEx.Validator +open import Test.Examples.DEx.OffChain.Lib +open import Test.Prelude DExData +open import Test.SymbolicData DExData +open import Test.LedgerImplementation SData SData +open import Test.AbstractImplementation valContext +open import Test.Lib valContext open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions diff --git a/src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/Exchange.agda b/src/Test/Examples/DEx/OffChain/Exchange.agda similarity index 79% rename from src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/Exchange.agda rename to src/Test/Examples/DEx/OffChain/Exchange.agda index bb556f299..a1d1f54c7 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/Exchange.agda +++ b/src/Test/Examples/DEx/OffChain/Exchange.agda @@ -1,18 +1,18 @@ {-# OPTIONS --safe #-} -module Ledger.Conway.Specification.Test.Examples.DEx.OffChain.Exchange where +module Test.Examples.DEx.OffChain.Exchange where open import Ledger.Prelude open import Ledger.Conway.Specification.Transaction -open import Ledger.Conway.Specification.Test.Examples.DEx.Datum -open import Ledger.Conway.Specification.Test.Examples.DEx.Validator -open import Ledger.Conway.Specification.Test.Examples.DEx.OffChain.Lib -open import Ledger.Conway.Specification.Test.Prelude DExData -open import Ledger.Conway.Specification.Test.SymbolicData DExData -open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Test.AbstractImplementation valContext -open import Ledger.Conway.Specification.Test.Lib valContext +open import Test.Examples.DEx.Datum +open import Test.Examples.DEx.Validator +open import Test.Examples.DEx.OffChain.Lib +open import Test.Prelude DExData +open import Test.SymbolicData DExData +open import Test.LedgerImplementation SData SData +open import Test.AbstractImplementation valContext +open import Test.Lib valContext open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions diff --git a/src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/Lib.agda b/src/Test/Examples/DEx/OffChain/Lib.agda similarity index 90% rename from src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/Lib.agda rename to src/Test/Examples/DEx/OffChain/Lib.agda index 199969383..646453b99 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/Lib.agda +++ b/src/Test/Examples/DEx/OffChain/Lib.agda @@ -1,17 +1,17 @@ {-# OPTIONS --safe #-} -module Ledger.Conway.Specification.Test.Examples.DEx.OffChain.Lib where +module Test.Examples.DEx.OffChain.Lib where open import Data.List using (filter) open import Ledger.Prelude open import Ledger.Conway.Specification.Transaction using (TransactionStructure) -open import Ledger.Conway.Specification.Test.Examples.DEx.Datum -open import Ledger.Conway.Specification.Test.Examples.DEx.Validator -open import Ledger.Conway.Specification.Test.Prelude DExData -open import Ledger.Conway.Specification.Test.SymbolicData DExData -open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData +open import Test.Examples.DEx.Datum +open import Test.Examples.DEx.Validator +open import Test.Prelude DExData +open import Test.SymbolicData DExData +open import Test.LedgerImplementation SData SData open TransactionStructure SVTransactionStructure diff --git a/src/Test/Examples/DEx/OffChain/OffChain.agda b/src/Test/Examples/DEx/OffChain/OffChain.agda new file mode 100644 index 000000000..b49a20296 --- /dev/null +++ b/src/Test/Examples/DEx/OffChain/OffChain.agda @@ -0,0 +1,8 @@ +{-# OPTIONS --safe #-} + +module Test.Examples.DEx.OffChain.OffChain where + +open import Test.Examples.DEx.OffChain.Start public +open import Test.Examples.DEx.OffChain.Close public +open import Test.Examples.DEx.OffChain.Update public +open import Test.Examples.DEx.OffChain.Exchange public diff --git a/src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/Start.agda b/src/Test/Examples/DEx/OffChain/Start.agda similarity index 77% rename from src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/Start.agda rename to src/Test/Examples/DEx/OffChain/Start.agda index 88d768564..e04cbd9a1 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/Start.agda +++ b/src/Test/Examples/DEx/OffChain/Start.agda @@ -1,17 +1,17 @@ {-# OPTIONS --safe #-} -module Ledger.Conway.Specification.Test.Examples.DEx.OffChain.Start where +module Test.Examples.DEx.OffChain.Start where open import Ledger.Prelude open import Ledger.Conway.Specification.Transaction using (TransactionStructure) -open import Ledger.Conway.Specification.Test.Examples.DEx.Datum -open import Ledger.Conway.Specification.Test.Examples.DEx.OffChain.Lib -open import Ledger.Conway.Specification.Test.Examples.DEx.Validator -open import Ledger.Conway.Specification.Test.Prelude DExData -open import Ledger.Conway.Specification.Test.SymbolicData DExData -open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Test.Lib valContext +open import Test.Examples.DEx.Datum +open import Test.Examples.DEx.OffChain.Lib +open import Test.Examples.DEx.Validator +open import Test.Prelude DExData +open import Test.SymbolicData DExData +open import Test.LedgerImplementation SData SData +open import Test.Lib valContext open TransactionStructure SVTransactionStructure open Implementation diff --git a/src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/Update.agda b/src/Test/Examples/DEx/OffChain/Update.agda similarity index 77% rename from src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/Update.agda rename to src/Test/Examples/DEx/OffChain/Update.agda index 09802394f..5330ed17c 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/DEx/OffChain/Update.agda +++ b/src/Test/Examples/DEx/OffChain/Update.agda @@ -1,18 +1,18 @@ {-# OPTIONS --safe #-} -module Ledger.Conway.Specification.Test.Examples.DEx.OffChain.Update where +module Test.Examples.DEx.OffChain.Update where open import Ledger.Prelude open import Ledger.Conway.Specification.Transaction -open import Ledger.Conway.Specification.Test.Examples.DEx.Datum -open import Ledger.Conway.Specification.Test.Examples.DEx.Validator -open import Ledger.Conway.Specification.Test.Examples.DEx.OffChain.Lib -open import Ledger.Conway.Specification.Test.Prelude DExData -open import Ledger.Conway.Specification.Test.SymbolicData DExData -open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Test.AbstractImplementation valContext -open import Ledger.Conway.Specification.Test.Lib valContext +open import Test.Examples.DEx.Datum +open import Test.Examples.DEx.Validator +open import Test.Examples.DEx.OffChain.Lib +open import Test.Prelude DExData +open import Test.SymbolicData DExData +open import Test.LedgerImplementation SData SData +open import Test.AbstractImplementation valContext +open import Test.Lib valContext open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions diff --git a/src/Ledger/Conway/Specification/Test/Examples/DEx/Test/Trace.agda b/src/Test/Examples/DEx/Test/Trace.agda similarity index 87% rename from src/Ledger/Conway/Specification/Test/Examples/DEx/Test/Trace.agda rename to src/Test/Examples/DEx/Test/Trace.agda index 14bf65c2a..fa30b807a 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/DEx/Test/Trace.agda +++ b/src/Test/Examples/DEx/Test/Trace.agda @@ -1,6 +1,6 @@ {-# OPTIONS --safe #-} -module Ledger.Conway.Specification.Test.Examples.DEx.Test.Trace where +module Test.Examples.DEx.Test.Trace where import Data.Rational.Base as Q open import Data.Nat.Divisibility.Core @@ -9,20 +9,20 @@ open import Data.Nat.Properties open import Ledger.Prelude open import Ledger.Conway.Specification.Transaction using (TransactionStructure) -open import Ledger.Conway.Specification.Test.Examples.DEx.Datum -open import Ledger.Conway.Specification.Test.Examples.DEx.Validator -open import Ledger.Conway.Specification.Test.Prelude DExData -open import Ledger.Conway.Specification.Test.SymbolicData DExData -open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Test.AbstractImplementation valContext -open import Ledger.Conway.Specification.Test.Lib valContext +open import Test.Examples.DEx.Datum +open import Test.Examples.DEx.Validator +open import Test.Prelude DExData +open import Test.SymbolicData DExData +open import Test.LedgerImplementation SData SData +open import Test.AbstractImplementation valContext +open import Test.Lib valContext open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions open import Ledger.Conway.Specification.Utxo.Properties.Computational SVTransactionStructure SVAbstractFunctions open import Ledger.Conway.Specification.Utxow.Properties.Computational SVTransactionStructure SVAbstractFunctions -open import Ledger.Conway.Specification.Test.Examples.DEx.OffChain.OffChain +open import Test.Examples.DEx.OffChain.OffChain open TransactionStructure SVTransactionStructure open Implementation diff --git a/src/Ledger/Conway/Specification/Test/Examples/DEx/Validator.agda b/src/Test/Examples/DEx/Validator.agda similarity index 95% rename from src/Ledger/Conway/Specification/Test/Examples/DEx/Validator.agda rename to src/Test/Examples/DEx/Validator.agda index c62abb17b..ce5915d9a 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/DEx/Validator.agda +++ b/src/Test/Examples/DEx/Validator.agda @@ -2,7 +2,7 @@ -- Validator for the MultiSig contract from the EUTxO paper adapted from Agda2hs version -module Ledger.Conway.Specification.Test.Examples.DEx.Validator where +module Test.Examples.DEx.Validator where open import Data.Maybe renaming (map to maybeMap) open import Data.List using (filter) @@ -14,9 +14,9 @@ import Data.Rational.Base as Q open import Ledger.Prelude open import Ledger.Conway.Specification.Transaction using (TransactionStructure) -open import Ledger.Conway.Specification.Test.Examples.DEx.Datum -open import Ledger.Conway.Specification.Test.Prelude DExData -open import Ledger.Conway.Specification.Test.SymbolicData DExData +open import Test.Examples.DEx.Datum +open import Test.Prelude DExData +open import Test.SymbolicData DExData PubKeyHash : Type PubKeyHash = ℕ @@ -26,7 +26,7 @@ instance ShowAccountSimData : Show DExData ShowAccountSimData = mkShow (λ x → "") -open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData +open import Test.LedgerImplementation SData SData open TransactionStructure SVTransactionStructure diff --git a/src/Ledger/Conway/Specification/Test/Examples/HelloWorld.lagda.md b/src/Test/Examples/HelloWorld.lagda.md similarity index 94% rename from src/Ledger/Conway/Specification/Test/Examples/HelloWorld.lagda.md rename to src/Test/Examples/HelloWorld.lagda.md index d96e6c4c3..de747eb8d 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/HelloWorld.lagda.md +++ b/src/Test/Examples/HelloWorld.lagda.md @@ -1,16 +1,16 @@ --- source_branch: master -source_path: src/Ledger/Conway/Specification/Test/Examples/HelloWorld.lagda.md +source_path: src/Test/Examples/HelloWorld.lagda.md --- ```agda {-# OPTIONS --safe #-} -module Ledger.Conway.Specification.Test.Examples.HelloWorld where +module Test.Examples.HelloWorld where open import Ledger.Prelude hiding (fromList; ε); open Computational -open import Ledger.Conway.Specification.Test.LedgerImplementation String String +open import Test.LedgerImplementation String String open import Ledger.Conway.Specification.Script.ScriptPurpose SVTransactionStructure open import Ledger.Conway.Specification.Transaction @@ -19,8 +19,8 @@ open TransactionStructure SVTransactionStructure using (Data) valContext : TxInfo → ScriptPurpose → Data valContext x x₁ = "" -open import Ledger.Conway.Specification.Test.AbstractImplementation valContext -open import Ledger.Conway.Specification.Test.Lib valContext +open import Test.AbstractImplementation valContext +open import Test.Lib valContext open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions diff --git a/src/Ledger/Conway/Specification/Test/Examples/MultiSig/Datum.agda b/src/Test/Examples/MultiSig/Datum.agda similarity index 90% rename from src/Ledger/Conway/Specification/Test/Examples/MultiSig/Datum.agda rename to src/Test/Examples/MultiSig/Datum.agda index 65c10cdb5..662a57487 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/MultiSig/Datum.agda +++ b/src/Test/Examples/MultiSig/Datum.agda @@ -2,7 +2,7 @@ open import Ledger.Prelude hiding (fromList; ε); open Computational -module Ledger.Conway.Specification.Test.Examples.MultiSig.Datum where +module Test.Examples.MultiSig.Datum where open import Tactic.Derive.DecEq diff --git a/src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/AddSig.agda b/src/Test/Examples/MultiSig/OffChain/AddSig.agda similarity index 78% rename from src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/AddSig.agda rename to src/Test/Examples/MultiSig/OffChain/AddSig.agda index 7627f343a..5e70b92b4 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/AddSig.agda +++ b/src/Test/Examples/MultiSig/OffChain/AddSig.agda @@ -1,18 +1,18 @@ {-# OPTIONS --safe #-} -module Ledger.Conway.Specification.Test.Examples.MultiSig.OffChain.AddSig where +module Test.Examples.MultiSig.OffChain.AddSig where open import Ledger.Prelude open import Ledger.Conway.Specification.Transaction -open import Ledger.Conway.Specification.Test.Examples.MultiSig.Datum -open import Ledger.Conway.Specification.Test.Examples.MultiSig.Validator -open import Ledger.Conway.Specification.Test.Examples.MultiSig.OffChain.Lib -open import Ledger.Conway.Specification.Test.Prelude MultiSigData -open import Ledger.Conway.Specification.Test.SymbolicData MultiSigData -open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Test.AbstractImplementation valContext -open import Ledger.Conway.Specification.Test.Lib valContext +open import Test.Examples.MultiSig.Datum +open import Test.Examples.MultiSig.Validator +open import Test.Examples.MultiSig.OffChain.Lib +open import Test.Prelude MultiSigData +open import Test.SymbolicData MultiSigData +open import Test.LedgerImplementation SData SData +open import Test.AbstractImplementation valContext +open import Test.Lib valContext open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions diff --git a/src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/Lib.agda b/src/Test/Examples/MultiSig/OffChain/Lib.agda similarity index 88% rename from src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/Lib.agda rename to src/Test/Examples/MultiSig/OffChain/Lib.agda index e37f0b28d..7173ecca8 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/Lib.agda +++ b/src/Test/Examples/MultiSig/OffChain/Lib.agda @@ -1,15 +1,15 @@ {-# OPTIONS --safe #-} -module Ledger.Conway.Specification.Test.Examples.MultiSig.OffChain.Lib where +module Test.Examples.MultiSig.OffChain.Lib where open import Ledger.Prelude open import Ledger.Conway.Specification.Transaction using (TransactionStructure) -open import Ledger.Conway.Specification.Test.Examples.MultiSig.Datum -open import Ledger.Conway.Specification.Test.Examples.MultiSig.Validator -open import Ledger.Conway.Specification.Test.Prelude MultiSigData -open import Ledger.Conway.Specification.Test.SymbolicData MultiSigData -open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData +open import Test.Examples.MultiSig.Datum +open import Test.Examples.MultiSig.Validator +open import Test.Prelude MultiSigData +open import Test.SymbolicData MultiSigData +open import Test.LedgerImplementation SData SData open TransactionStructure SVTransactionStructure open Implementation diff --git a/src/Test/Examples/MultiSig/OffChain/OffChain.agda b/src/Test/Examples/MultiSig/OffChain/OffChain.agda new file mode 100644 index 000000000..8bbca7f62 --- /dev/null +++ b/src/Test/Examples/MultiSig/OffChain/OffChain.agda @@ -0,0 +1,8 @@ +{-# OPTIONS --safe #-} + +module Test.Examples.MultiSig.OffChain.OffChain where + +open import Test.Examples.MultiSig.OffChain.Pay public +open import Test.Examples.MultiSig.OffChain.Propose public +open import Test.Examples.MultiSig.OffChain.Open public +open import Test.Examples.MultiSig.OffChain.AddSig public diff --git a/src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/Open.agda b/src/Test/Examples/MultiSig/OffChain/Open.agda similarity index 81% rename from src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/Open.agda rename to src/Test/Examples/MultiSig/OffChain/Open.agda index f7bbd0940..1285c1d29 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/Open.agda +++ b/src/Test/Examples/MultiSig/OffChain/Open.agda @@ -1,17 +1,17 @@ {-# OPTIONS --safe #-} -module Ledger.Conway.Specification.Test.Examples.MultiSig.OffChain.Open where +module Test.Examples.MultiSig.OffChain.Open where open import Ledger.Prelude open import Ledger.Conway.Specification.Transaction -open import Ledger.Conway.Specification.Test.Examples.MultiSig.Datum -open import Ledger.Conway.Specification.Test.Examples.MultiSig.Validator -open import Ledger.Conway.Specification.Test.Examples.MultiSig.OffChain.Lib -open import Ledger.Conway.Specification.Test.Prelude MultiSigData -open import Ledger.Conway.Specification.Test.SymbolicData MultiSigData -open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Test.Lib valContext +open import Test.Examples.MultiSig.Datum +open import Test.Examples.MultiSig.Validator +open import Test.Examples.MultiSig.OffChain.Lib +open import Test.Prelude MultiSigData +open import Test.SymbolicData MultiSigData +open import Test.LedgerImplementation SData SData +open import Test.Lib valContext open TransactionStructure SVTransactionStructure open Implementation diff --git a/src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/Pay.agda b/src/Test/Examples/MultiSig/OffChain/Pay.agda similarity index 80% rename from src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/Pay.agda rename to src/Test/Examples/MultiSig/OffChain/Pay.agda index 282403d8b..1ce5a941c 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/Pay.agda +++ b/src/Test/Examples/MultiSig/OffChain/Pay.agda @@ -1,18 +1,18 @@ {-# OPTIONS --safe #-} -module Ledger.Conway.Specification.Test.Examples.MultiSig.OffChain.Pay where +module Test.Examples.MultiSig.OffChain.Pay where open import Ledger.Prelude open import Ledger.Conway.Specification.Transaction -open import Ledger.Conway.Specification.Test.Examples.MultiSig.Datum -open import Ledger.Conway.Specification.Test.Examples.MultiSig.Validator -open import Ledger.Conway.Specification.Test.Examples.MultiSig.OffChain.Lib -open import Ledger.Conway.Specification.Test.Prelude MultiSigData -open import Ledger.Conway.Specification.Test.SymbolicData MultiSigData -open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Test.AbstractImplementation valContext -open import Ledger.Conway.Specification.Test.Lib valContext +open import Test.Examples.MultiSig.Datum +open import Test.Examples.MultiSig.Validator +open import Test.Examples.MultiSig.OffChain.Lib +open import Test.Prelude MultiSigData +open import Test.SymbolicData MultiSigData +open import Test.LedgerImplementation SData SData +open import Test.AbstractImplementation valContext +open import Test.Lib valContext open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions diff --git a/src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/Propose.agda b/src/Test/Examples/MultiSig/OffChain/Propose.agda similarity index 79% rename from src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/Propose.agda rename to src/Test/Examples/MultiSig/OffChain/Propose.agda index 3d2bcff8c..a8772ab67 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/Propose.agda +++ b/src/Test/Examples/MultiSig/OffChain/Propose.agda @@ -1,18 +1,18 @@ {-# OPTIONS --safe #-} -module Ledger.Conway.Specification.Test.Examples.MultiSig.OffChain.Propose where +module Test.Examples.MultiSig.OffChain.Propose where open import Ledger.Prelude open import Ledger.Conway.Specification.Transaction -open import Ledger.Conway.Specification.Test.Examples.MultiSig.Datum -open import Ledger.Conway.Specification.Test.Examples.MultiSig.Validator -open import Ledger.Conway.Specification.Test.Examples.MultiSig.OffChain.Lib -open import Ledger.Conway.Specification.Test.Prelude MultiSigData -open import Ledger.Conway.Specification.Test.SymbolicData MultiSigData -open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Test.AbstractImplementation valContext -open import Ledger.Conway.Specification.Test.Lib valContext +open import Test.Examples.MultiSig.Datum +open import Test.Examples.MultiSig.Validator +open import Test.Examples.MultiSig.OffChain.Lib +open import Test.Prelude MultiSigData +open import Test.SymbolicData MultiSigData +open import Test.LedgerImplementation SData SData +open import Test.AbstractImplementation valContext +open import Test.Lib valContext open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions diff --git a/src/Ledger/Conway/Specification/Test/Examples/MultiSig/Test/Trace.agda b/src/Test/Examples/MultiSig/Test/Trace.agda similarity index 86% rename from src/Ledger/Conway/Specification/Test/Examples/MultiSig/Test/Trace.agda rename to src/Test/Examples/MultiSig/Test/Trace.agda index f9e0a360f..ddbc29d79 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/MultiSig/Test/Trace.agda +++ b/src/Test/Examples/MultiSig/Test/Trace.agda @@ -1,18 +1,18 @@ {-# OPTIONS --safe #-} -module Ledger.Conway.Specification.Test.Examples.MultiSig.Test.Trace where +module Test.Examples.MultiSig.Test.Trace where open import Ledger.Prelude open import Ledger.Conway.Specification.Transaction using (TransactionStructure) -open import Ledger.Conway.Specification.Test.Examples.MultiSig.Datum -open import Ledger.Conway.Specification.Test.Examples.MultiSig.OffChain.OffChain -open import Ledger.Conway.Specification.Test.Examples.MultiSig.Validator -open import Ledger.Conway.Specification.Test.Prelude MultiSigData -open import Ledger.Conway.Specification.Test.SymbolicData MultiSigData -open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Test.AbstractImplementation valContext -open import Ledger.Conway.Specification.Test.Lib valContext +open import Test.Examples.MultiSig.Datum +open import Test.Examples.MultiSig.OffChain.OffChain +open import Test.Examples.MultiSig.Validator +open import Test.Prelude MultiSigData +open import Test.SymbolicData MultiSigData +open import Test.LedgerImplementation SData SData +open import Test.AbstractImplementation valContext +open import Test.Lib valContext open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions diff --git a/src/Ledger/Conway/Specification/Test/Examples/MultiSig/Validator.agda b/src/Test/Examples/MultiSig/Validator.agda similarity index 95% rename from src/Ledger/Conway/Specification/Test/Examples/MultiSig/Validator.agda rename to src/Test/Examples/MultiSig/Validator.agda index a30a63af7..1c5e0dbfc 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/MultiSig/Validator.agda +++ b/src/Test/Examples/MultiSig/Validator.agda @@ -1,13 +1,13 @@ {-# OPTIONS --safe #-} -module Ledger.Conway.Specification.Test.Examples.MultiSig.Validator where +module Test.Examples.MultiSig.Validator where open import Ledger.Prelude -open import Ledger.Conway.Specification.Test.Examples.MultiSig.Datum -open import Ledger.Conway.Specification.Test.Prelude MultiSigData +open import Test.Examples.MultiSig.Datum +open import Test.Prelude MultiSigData open import Ledger.Conway.Specification.Transaction -open import Ledger.Conway.Specification.Test.SymbolicData MultiSigData +open import Test.SymbolicData MultiSigData open import Data.List using (filter) open import Data.Maybe renaming (map to maybeMap) @@ -26,7 +26,7 @@ instance ShowMultiSigData : Show MultiSigData ShowMultiSigData = mkShow (λ x → "") -open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData +open import Test.LedgerImplementation SData SData open TransactionStructure SVTransactionStructure open Implementation diff --git a/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/Datum.agda b/src/Test/Examples/MultiSigV2/Datum.agda similarity index 88% rename from src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/Datum.agda rename to src/Test/Examples/MultiSigV2/Datum.agda index e5cbeb04b..734538a1d 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/Datum.agda +++ b/src/Test/Examples/MultiSigV2/Datum.agda @@ -2,7 +2,7 @@ open import Ledger.Prelude hiding (fromList; ε); open Computational -module Ledger.Conway.Specification.Test.Examples.MultiSigV2.Datum where +module Test.Examples.MultiSigV2.Datum where open import Tactic.Derive.DecEq diff --git a/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/AddSig.agda b/src/Test/Examples/MultiSigV2/OffChain/AddSig.agda similarity index 76% rename from src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/AddSig.agda rename to src/Test/Examples/MultiSigV2/OffChain/AddSig.agda index 6cbbe30a3..eec818bd9 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/AddSig.agda +++ b/src/Test/Examples/MultiSigV2/OffChain/AddSig.agda @@ -1,18 +1,18 @@ {-# OPTIONS --safe #-} -module Ledger.Conway.Specification.Test.Examples.MultiSigV2.OffChain.AddSig where +module Test.Examples.MultiSigV2.OffChain.AddSig where open import Ledger.Prelude open import Ledger.Conway.Specification.Transaction -open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.Datum -open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.OffChain.Lib -open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.Validator -open import Ledger.Conway.Specification.Test.Prelude MultiSigData -open import Ledger.Conway.Specification.Test.SymbolicData MultiSigData -open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Test.AbstractImplementation valContext -open import Ledger.Conway.Specification.Test.Lib valContext +open import Test.Examples.MultiSigV2.Datum +open import Test.Examples.MultiSigV2.OffChain.Lib +open import Test.Examples.MultiSigV2.Validator +open import Test.Prelude MultiSigData +open import Test.SymbolicData MultiSigData +open import Test.LedgerImplementation SData SData +open import Test.AbstractImplementation valContext +open import Test.Lib valContext open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions diff --git a/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Cancel.agda b/src/Test/Examples/MultiSigV2/OffChain/Cancel.agda similarity index 76% rename from src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Cancel.agda rename to src/Test/Examples/MultiSigV2/OffChain/Cancel.agda index e1040fa18..fa686c155 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Cancel.agda +++ b/src/Test/Examples/MultiSigV2/OffChain/Cancel.agda @@ -1,18 +1,18 @@ {-# OPTIONS --safe #-} -module Ledger.Conway.Specification.Test.Examples.MultiSigV2.OffChain.Cancel where +module Test.Examples.MultiSigV2.OffChain.Cancel where open import Ledger.Prelude open import Ledger.Conway.Specification.Transaction -open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.Datum -open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.OffChain.Lib -open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.Validator -open import Ledger.Conway.Specification.Test.Prelude MultiSigData -open import Ledger.Conway.Specification.Test.SymbolicData MultiSigData -open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Test.AbstractImplementation valContext -open import Ledger.Conway.Specification.Test.Lib valContext +open import Test.Examples.MultiSigV2.Datum +open import Test.Examples.MultiSigV2.OffChain.Lib +open import Test.Examples.MultiSigV2.Validator +open import Test.Prelude MultiSigData +open import Test.SymbolicData MultiSigData +open import Test.LedgerImplementation SData SData +open import Test.AbstractImplementation valContext +open import Test.Lib valContext open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions diff --git a/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Cleanup.agda b/src/Test/Examples/MultiSigV2/OffChain/Cleanup.agda similarity index 72% rename from src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Cleanup.agda rename to src/Test/Examples/MultiSigV2/OffChain/Cleanup.agda index 9f3680934..66dcc4f35 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Cleanup.agda +++ b/src/Test/Examples/MultiSigV2/OffChain/Cleanup.agda @@ -1,18 +1,18 @@ {-# OPTIONS --safe #-} -module Ledger.Conway.Specification.Test.Examples.MultiSigV2.OffChain.Cleanup where +module Test.Examples.MultiSigV2.OffChain.Cleanup where open import Ledger.Prelude open import Ledger.Conway.Specification.Transaction -open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.Datum -open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.OffChain.Lib -open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.Validator -open import Ledger.Conway.Specification.Test.Prelude MultiSigData -open import Ledger.Conway.Specification.Test.SymbolicData MultiSigData -open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Test.AbstractImplementation valContext -open import Ledger.Conway.Specification.Test.Lib valContext +open import Test.Examples.MultiSigV2.Datum +open import Test.Examples.MultiSigV2.OffChain.Lib +open import Test.Examples.MultiSigV2.Validator +open import Test.Prelude MultiSigData +open import Test.SymbolicData MultiSigData +open import Test.LedgerImplementation SData SData +open import Test.AbstractImplementation valContext +open import Test.Lib valContext open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions diff --git a/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Lib.agda b/src/Test/Examples/MultiSigV2/OffChain/Lib.agda similarity index 86% rename from src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Lib.agda rename to src/Test/Examples/MultiSigV2/OffChain/Lib.agda index 8bd92207f..d4570d70e 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Lib.agda +++ b/src/Test/Examples/MultiSigV2/OffChain/Lib.agda @@ -1,17 +1,17 @@ {-# OPTIONS --safe #-} -module Ledger.Conway.Specification.Test.Examples.MultiSigV2.OffChain.Lib where +module Test.Examples.MultiSigV2.OffChain.Lib where open import Ledger.Prelude open import Ledger.Conway.Specification.Transaction using (TransactionStructure) -open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.Datum -open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.Validator -open import Ledger.Conway.Specification.Test.Prelude MultiSigData -open import Ledger.Conway.Specification.Test.SymbolicData MultiSigData -open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Test.AbstractImplementation valContext -open import Ledger.Conway.Specification.Test.Lib valContext +open import Test.Examples.MultiSigV2.Datum +open import Test.Examples.MultiSigV2.Validator +open import Test.Prelude MultiSigData +open import Test.SymbolicData MultiSigData +open import Test.LedgerImplementation SData SData +open import Test.AbstractImplementation valContext +open import Test.Lib valContext open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions diff --git a/src/Test/Examples/MultiSigV2/OffChain/OffChain.agda b/src/Test/Examples/MultiSigV2/OffChain/OffChain.agda new file mode 100644 index 000000000..6fda49201 --- /dev/null +++ b/src/Test/Examples/MultiSigV2/OffChain/OffChain.agda @@ -0,0 +1,10 @@ +{-# OPTIONS --safe #-} + +module Test.Examples.MultiSigV2.OffChain.OffChain where + +open import Test.Examples.MultiSigV2.OffChain.Pay public +open import Test.Examples.MultiSigV2.OffChain.Propose public +open import Test.Examples.MultiSigV2.OffChain.Open public +open import Test.Examples.MultiSigV2.OffChain.AddSig public +open import Test.Examples.MultiSigV2.OffChain.Cancel public +open import Test.Examples.MultiSigV2.OffChain.Cleanup public diff --git a/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Open.agda b/src/Test/Examples/MultiSigV2/OffChain/Open.agda similarity index 70% rename from src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Open.agda rename to src/Test/Examples/MultiSigV2/OffChain/Open.agda index 32a9d1e4a..878d87ab3 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Open.agda +++ b/src/Test/Examples/MultiSigV2/OffChain/Open.agda @@ -1,18 +1,18 @@ {-# OPTIONS --safe #-} -module Ledger.Conway.Specification.Test.Examples.MultiSigV2.OffChain.Open where +module Test.Examples.MultiSigV2.OffChain.Open where open import Ledger.Prelude open import Ledger.Conway.Specification.Transaction -open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.Datum -open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.OffChain.Lib -open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.Validator -open import Ledger.Conway.Specification.Test.Prelude MultiSigData -open import Ledger.Conway.Specification.Test.SymbolicData MultiSigData -open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Test.AbstractImplementation valContext -open import Ledger.Conway.Specification.Test.Lib valContext +open import Test.Examples.MultiSigV2.Datum +open import Test.Examples.MultiSigV2.OffChain.Lib +open import Test.Examples.MultiSigV2.Validator +open import Test.Prelude MultiSigData +open import Test.SymbolicData MultiSigData +open import Test.LedgerImplementation SData SData +open import Test.AbstractImplementation valContext +open import Test.Lib valContext open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions @@ -42,11 +42,10 @@ openTx id w v tw script = record { body = record defaultTxBody ; collateralInputs = Ledger.Prelude.fromList ((w , w) ∷ []) } ; wits = record { vkSigs = fromListᵐ ((w , (_+_ {{addValue}} w id)) ∷ []) ; - scripts = ∅ ; + scripts = ∅ ; txdats = ∅ ; txrdmrs = ∅ } ; - - txsize = 10 ; + + txsize = 10 ; isValid = true ; txAD = nothing } - diff --git a/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Pay.agda b/src/Test/Examples/MultiSigV2/OffChain/Pay.agda similarity index 78% rename from src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Pay.agda rename to src/Test/Examples/MultiSigV2/OffChain/Pay.agda index 444796561..1d4f05ea9 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Pay.agda +++ b/src/Test/Examples/MultiSigV2/OffChain/Pay.agda @@ -1,18 +1,18 @@ {-# OPTIONS --safe #-} -module Ledger.Conway.Specification.Test.Examples.MultiSigV2.OffChain.Pay where +module Test.Examples.MultiSigV2.OffChain.Pay where open import Ledger.Prelude open import Ledger.Conway.Specification.Transaction -open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.Datum -open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.OffChain.Lib -open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.Validator -open import Ledger.Conway.Specification.Test.Prelude MultiSigData -open import Ledger.Conway.Specification.Test.SymbolicData MultiSigData -open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Test.AbstractImplementation valContext -open import Ledger.Conway.Specification.Test.Lib valContext +open import Test.Examples.MultiSigV2.Datum +open import Test.Examples.MultiSigV2.OffChain.Lib +open import Test.Examples.MultiSigV2.Validator +open import Test.Prelude MultiSigData +open import Test.SymbolicData MultiSigData +open import Test.LedgerImplementation SData SData +open import Test.AbstractImplementation valContext +open import Test.Lib valContext open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions diff --git a/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Propose.agda b/src/Test/Examples/MultiSigV2/OffChain/Propose.agda similarity index 77% rename from src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Propose.agda rename to src/Test/Examples/MultiSigV2/OffChain/Propose.agda index 972911fa5..b0da9fd83 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/OffChain/Propose.agda +++ b/src/Test/Examples/MultiSigV2/OffChain/Propose.agda @@ -1,18 +1,18 @@ {-# OPTIONS --safe #-} -module Ledger.Conway.Specification.Test.Examples.MultiSigV2.OffChain.Propose where +module Test.Examples.MultiSigV2.OffChain.Propose where open import Ledger.Prelude open import Ledger.Conway.Specification.Transaction -open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.Datum -open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.OffChain.Lib -open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.Validator -open import Ledger.Conway.Specification.Test.Prelude MultiSigData -open import Ledger.Conway.Specification.Test.SymbolicData MultiSigData -open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Test.AbstractImplementation valContext -open import Ledger.Conway.Specification.Test.Lib valContext +open import Test.Examples.MultiSigV2.Datum +open import Test.Examples.MultiSigV2.OffChain.Lib +open import Test.Examples.MultiSigV2.Validator +open import Test.Prelude MultiSigData +open import Test.SymbolicData MultiSigData +open import Test.LedgerImplementation SData SData +open import Test.AbstractImplementation valContext +open import Test.Lib valContext open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions diff --git a/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/Test/Trace.agda b/src/Test/Examples/MultiSigV2/Test/Trace.agda similarity index 88% rename from src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/Test/Trace.agda rename to src/Test/Examples/MultiSigV2/Test/Trace.agda index 8c64ffb69..478c792d8 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/Test/Trace.agda +++ b/src/Test/Examples/MultiSigV2/Test/Trace.agda @@ -1,18 +1,18 @@ {-# OPTIONS --safe #-} -module Ledger.Conway.Specification.Test.Examples.MultiSigV2.Test.Trace where +module Test.Examples.MultiSigV2.Test.Trace where open import Ledger.Prelude open import Ledger.Conway.Specification.Transaction -open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.Datum -open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.OffChain.Lib -open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.Validator -open import Ledger.Conway.Specification.Test.Prelude MultiSigData -open import Ledger.Conway.Specification.Test.SymbolicData MultiSigData -open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData -open import Ledger.Conway.Specification.Test.AbstractImplementation valContext -open import Ledger.Conway.Specification.Test.Lib valContext +open import Test.Examples.MultiSigV2.Datum +open import Test.Examples.MultiSigV2.OffChain.Lib +open import Test.Examples.MultiSigV2.Validator +open import Test.Prelude MultiSigData +open import Test.SymbolicData MultiSigData +open import Test.LedgerImplementation SData SData +open import Test.AbstractImplementation valContext +open import Test.Lib valContext open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions @@ -23,7 +23,7 @@ open TransactionStructure SVTransactionStructure open Implementation -open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.OffChain.OffChain +open import Test.Examples.MultiSigV2.OffChain.OffChain impMultiSig : Params impMultiSig = record { authSigs = 3 ∷ 2 ∷ 5 ∷ [] ; minNumSignatures = 2 ; maxWait = 10 } diff --git a/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/Validator.agda b/src/Test/Examples/MultiSigV2/Validator.agda similarity index 94% rename from src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/Validator.agda rename to src/Test/Examples/MultiSigV2/Validator.agda index c5c1a166b..f475402f0 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/MultiSigV2/Validator.agda +++ b/src/Test/Examples/MultiSigV2/Validator.agda @@ -3,7 +3,7 @@ -- Version 2 of MultiSig contract adapted from updated Agda2hs code open import Ledger.Prelude hiding (fromList; ε); open Computational -open import Ledger.Conway.Specification.Test.Examples.MultiSigV2.Datum +open import Test.Examples.MultiSigV2.Datum open import Relation.Binary using (REL; Decidable) open import Level using (Level; _⊔_; suc) open import Data.Maybe renaming (map to maybeMap) @@ -11,9 +11,9 @@ open import Data.List using (filter) open import Data.Bool.Base renaming (_∧_ to _&&_) hiding (if_then_else_) import Agda.Builtin.Nat as N -open import Ledger.Conway.Specification.Test.Prelude MultiSigData +open import Test.Prelude MultiSigData -module Ledger.Conway.Specification.Test.Examples.MultiSigV2.Validator where +module Test.Examples.MultiSigV2.Validator where PubKeyHash = ℕ @@ -24,18 +24,18 @@ record Params : Set where maxWait : ℕ open Params -open import Ledger.Conway.Specification.Test.SymbolicData MultiSigData +open import Test.SymbolicData MultiSigData instance ShowMultiSigData : Show MultiSigData ShowMultiSigData = mkShow (λ x → "") -open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData +open import Test.LedgerImplementation SData SData open import Ledger.Conway.Specification.Transaction using (TransactionStructure) open TransactionStructure SVTransactionStructure -open import Ledger.Conway.Specification.Test.AbstractImplementation valContext -open import Ledger.Conway.Specification.Test.Lib valContext +open import Test.AbstractImplementation valContext +open import Test.Lib valContext open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions open import Data.Empty open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions diff --git a/src/Ledger/Conway/Specification/Test/Examples/SucceedIfNumber.lagda.md b/src/Test/Examples/SucceedIfNumber.lagda.md similarity index 91% rename from src/Ledger/Conway/Specification/Test/Examples/SucceedIfNumber.lagda.md rename to src/Test/Examples/SucceedIfNumber.lagda.md index bcffc91cf..40340d5d0 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/SucceedIfNumber.lagda.md +++ b/src/Test/Examples/SucceedIfNumber.lagda.md @@ -1,35 +1,35 @@ --- source_branch: master -source_path: src/Ledger/Conway/Specification/Test/Examples/SucceedIfNumber.lagda.md +source_path: src/Test/Examples/SucceedIfNumber.lagda.md --- - +```agda -- succeed if the datum is 1 succeedIf1Datum' : Maybe ℕ → Maybe ℕ → Bool succeedIf1Datum' (just (suc zero)) _ = true @@ -151,7 +151,9 @@ evalScriptRedeemer = evalP2Scripts (collectP2ScriptsWithContext (UTxOEnv.pparams exampleDatum' : Maybe Datum exampleDatum' = getDatum failTx initStateRedeemer (Spend (6 , 6)) - +``` + diff --git a/src/Ledger/Conway/Specification/Test/LedgerImplementation.lagda.md b/src/Test/LedgerImplementation.lagda.md similarity index 72% rename from src/Ledger/Conway/Specification/Test/LedgerImplementation.lagda.md rename to src/Test/LedgerImplementation.lagda.md index d37502ff2..bbc6254b7 100644 --- a/src/Ledger/Conway/Specification/Test/LedgerImplementation.lagda.md +++ b/src/Test/LedgerImplementation.lagda.md @@ -1,18 +1,16 @@ --- source_branch: master -source_path: src/Ledger/Conway/Specification/Test/LedgerImplementation.lagda.md +source_path: src/Test/LedgerImplementation.lagda.md --- + +```agda module Implementation where Network = ℕ SlotsPerEpochᶜ = 100 - ActiveSlotCoeff = ℤ.1ℤ ℚ./ 20 + ActiveSlotCoeff = ℤ.1ℤ ℚ./ 20 StabilityWindowᶜ = 10 - RandomnessStabilisationWindowᶜ = 10 - MaxLovelaceSupplyᶜ = 1 + RandomnessStabilisationWindowᶜ = 2 + MaxLovelaceSupplyᶜ = 1000000000000000000 Quorum = 1 NetworkId = 0 @@ -57,9 +57,7 @@ module Implementation where sign = _+_ Data = D - Dataʰ = mkHashableSet Data - toData : ∀ {A : Type} → A → D - toData = toData' -- fix this + Dataʰ = mkHashableSet D PlutusScript = ℕ × (List Data → Bool) ScriptHash = ℕ @@ -86,13 +84,12 @@ module Implementation where where open import Ledger.Conway.Specification.TokenAlgebra.Coin ScriptHash using (Coin-TokenAlgebra) - SVGlobalConstants = GlobalConstants ∋ record {Implementation} SVEpochStructure = EpochStructure ∋ ℕEpochStructure SVGlobalConstants instance _ = SVEpochStructure -SVCryptoStructure : CryptoStructure -SVCryptoStructure = record +SVCrypto : CryptoStructure +SVCrypto = record { Implementation ; pkk = SVPKKScheme } @@ -101,16 +98,20 @@ SVCryptoStructure = record SVPKKScheme : PKKScheme SVPKKScheme = record { Implementation - ; isSigned = λ a b m → ⊤ - ; sign = λ _ _ → zero - ; isSigned-correct = λ where (sk , sk , refl) _ _ h → tt + ; isSigned = λ a b m → a + b ≡ m + ; sign = _+_ + ; isSigned-correct = λ where (sk , sk , refl) _ _ h → h } - -instance _ = SVCryptoStructure +``` + +```agda SVScriptStructure : ScriptStructure SVScriptStructure = record { p1s = P1ScriptStructure-HTL @@ -132,11 +133,15 @@ SVScriptStructure = record { Implementation ; validPlutusScript = λ _ _ _ _ → ⊤ } - +``` + +```agda SVGovParams : GovParams SVGovParams = record { Implementation @@ -152,7 +157,7 @@ SVGovStructure = record { Implementation ; epochStructure = SVEpochStructure ; govParams = SVGovParams - ; cryptoStructure = SVCryptoStructure + ; cryptoStructure = SVCrypto ; globalConstants = SVGlobalConstants } instance _ = SVGovStructure @@ -166,35 +171,23 @@ SVTransactionStructure = record ; epochStructure = SVEpochStructure ; globalConstants = SVGlobalConstants ; adHashingScheme = it - ; cryptoStructure = SVCryptoStructure + ; cryptoStructure = SVCrypto ; govParams = SVGovParams ; txidBytes = id ; scriptStructure = SVScriptStructure } +``` + +```agda indexOfTxInImp : TxIn → ℙ TxIn → Maybe Ix indexOfTxInImp x y = lookupᵐ? (fromListᵐ (setToList y)) (proj₁ x) - -SVAbstractFunctions : AbstractFunctions -SVAbstractFunctions = record - { Implementation - ; txscriptfee = λ tt y → 0 - ; serSize = λ v → 0 -- changed to 0 - ; indexOfImp = record - { indexOfDCert = λ _ _ → nothing - ; indexOfRwdAddr = λ _ _ → nothing - ; indexOfTxIn = indexOfTxInImp - ; indexOfPolicyId = λ _ _ → nothing - ; indexOfVote = λ _ _ → nothing - ; indexOfProposal = λ _ _ → nothing - } - ; runPLCScript = λ { x x₁ x₂ x₃ → proj₂ x₁ x₃ } - ; scriptSize = λ _ → 0 - } -instance _ = SVAbstractFunctions +``` diff --git a/src/Ledger/Conway/Specification/Test/Lib.lagda.md b/src/Test/Lib.lagda.md similarity index 94% rename from src/Ledger/Conway/Specification/Test/Lib.lagda.md rename to src/Test/Lib.lagda.md index 3f35964d6..01d96abeb 100644 --- a/src/Ledger/Conway/Specification/Test/Lib.lagda.md +++ b/src/Test/Lib.lagda.md @@ -1,23 +1,23 @@ --- source_branch: master -source_path: src/Ledger/Conway/Specification/Test/Lib.lagda.md +source_path: src/Test/Lib.lagda.md --- ```agda {-# OPTIONS --safe #-} open import Ledger.Prelude hiding (fromList; ε; _/_) -open import Ledger.Conway.Specification.Test.LedgerImplementation using (SVTransactionStructure) +open import Test.LedgerImplementation using (SVTransactionStructure) import Ledger.Conway.Specification.Script.ScriptPurpose as SP -module Ledger.Conway.Specification.Test.Lib +module Test.Lib {T D : Set}{{DecEq-Data : DecEq D}}{{Show-Data : Show D}} (open SP (SVTransactionStructure T D) using (TxInfo; ScriptPurpose)) (valContext' : TxInfo → ScriptPurpose → D) where -open import Ledger.Conway.Specification.Test.AbstractImplementation valContext' -open import Ledger.Conway.Specification.Test.LedgerImplementation T D +open import Test.AbstractImplementation valContext' +open import Test.LedgerImplementation T D renaming (SVTransactionStructure to SVTransactionStructure') open import Ledger.Conway.Specification.Utxo SVTransactionStructure' SVAbstractFunctions open import Ledger.Conway.Specification.Transaction using (TransactionStructure) diff --git a/src/Test/Prelude.lagda.md b/src/Test/Prelude.lagda.md new file mode 100644 index 000000000..a26521a97 --- /dev/null +++ b/src/Test/Prelude.lagda.md @@ -0,0 +1,99 @@ +--- +source_branch: master +source_path: src/Test/Prelude.lagda.md +--- + + +```agda +SDatum = D +SValue = ℕ -- × Vec ℕ 3 +STxId = ℕ +SIx = ℕ +STxIn = STxId × SIx +SNetwork = ℕ +SSlot = ℕ +SKeyHash = ℕ + +-- SCredential = ℕ ⊎ ℕ +data SCredential : Type where + KeyHashObj : ℕ → SCredential + ScriptObj : ℕ → SCredential +instance + unquoteDecl DecEq-SCredential = derive-DecEq + ((quote SCredential , DecEq-SCredential) ∷ []) + +record SBaseAddr : Set where + field net : SNetwork + pay : SCredential + stake : Maybe SCredential +instance + unquoteDecl DecEq-SBaseAddr = derive-DecEq + ((quote SBaseAddr , DecEq-SBaseAddr) ∷ []) + +record SBootstrapAddr : Set where + field net : SNetwork + pay : SCredential + attrsSize : ℕ +instance + unquoteDecl DecEq-SBootstrapAddr = derive-DecEq + ((quote SBootstrapAddr , DecEq-SBootstrapAddr) ∷ []) + +SAddr = SBaseAddr ⊎ SBootstrapAddr + +-- ScriptHash +STxOut = SAddr × SValue × Maybe (D ⊎ D) -- Assumes hash is identity for datums, dropping Maybe Script for now +SUTxO = List (STxIn × STxOut) + +record SRwdAddr : Set where + field net : SNetwork + stake : SCredential +instance + unquoteDecl DecEq-SRwdAddr = derive-DecEq + ((quote SRwdAddr , DecEq-SRwdAddr) ∷ []) + +data SScriptPurpose : Set where + -- network is tt so we can ignore it here + Rwrd : SRwdAddr → SScriptPurpose + Mint : SValue → SScriptPurpose + Spend : STxIn → SScriptPurpose + Empty : SScriptPurpose +instance + unquoteDecl DecEq-SScriptPurpose = derive-DecEq + ((quote SScriptPurpose , DecEq-SScriptPurpose) ∷ []) + + +record STxInfo : Set where + field realizedInputs : SUTxO + txouts : List (SIx × STxOut) + fee : SValue + mint : SValue + -- not adding txcerts as rarely used + txwdrls : List (SRwdAddr × Coin) + txvldt : Maybe SSlot × Maybe SSlot + vkey : ℙ SKeyHash + txdats : List D -- Hash is id for datums therfore List D can replicate: DataHash ⇀ Datum + txid : STxId +``` + diff --git a/src/Ledger/Conway/Specification/Test/StructuredContracts.lagda.md b/src/Test/StructuredContracts.lagda.md similarity index 98% rename from src/Ledger/Conway/Specification/Test/StructuredContracts.lagda.md rename to src/Test/StructuredContracts.lagda.md index 064bf6df0..79e045727 100644 --- a/src/Ledger/Conway/Specification/Test/StructuredContracts.lagda.md +++ b/src/Test/StructuredContracts.lagda.md @@ -16,7 +16,7 @@ open import Ledger.Conway.Specification.TokenAlgebra.Base open import Ledger.Conway.Specification.TokenAlgebra.ValueSet -module Ledger.Conway.Specification.Test.StructuredContracts +module Test.StructuredContracts (txs : _) (open TransactionStructure txs) (abs : AbstractFunctions txs) (open AbstractFunctions abs) where diff --git a/src/Ledger/Conway/Specification/Test/SymbolicData.agda b/src/Test/SymbolicData.agda similarity index 94% rename from src/Ledger/Conway/Specification/Test/SymbolicData.agda rename to src/Test/SymbolicData.agda index 5a9473c2e..1c0687862 100644 --- a/src/Ledger/Conway/Specification/Test/SymbolicData.agda +++ b/src/Test/SymbolicData.agda @@ -2,10 +2,10 @@ open import Ledger.Prelude -module Ledger.Conway.Specification.Test.SymbolicData +module Test.SymbolicData (SD : Set) {{DecEq-Data : DecEq SD}} {{Show-Data : Show SD}} where -open import Ledger.Conway.Specification.Test.Prelude SD +open import Test.Prelude SD ScriptContext : Type ScriptContext = STxInfo × SScriptPurpose @@ -16,7 +16,7 @@ SData = SDatum ⊎ ScriptContext instance ShowSData : Show SData ShowSData = mkShow (λ x → "") -open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData +open import Test.LedgerImplementation SData SData open import Ledger.Conway.Specification.Script.ScriptPurpose SVTransactionStructure open import Ledger.Conway.Specification.Transaction using (TransactionStructure) From edba388a3a1f6262170d2bce4e60be8cab5c88b1 Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Thu, 6 Nov 2025 09:24:36 -0700 Subject: [PATCH 09/11] fix problem created during merge --- src/Ledger/Conway/Specification.lagda.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Ledger/Conway/Specification.lagda.md b/src/Ledger/Conway/Specification.lagda.md index a00f440ed..da4181794 100644 --- a/src/Ledger/Conway/Specification.lagda.md +++ b/src/Ledger/Conway/Specification.lagda.md @@ -127,8 +127,8 @@ import Ledger.Conway.Specification.Script.Validation ## Tests and Examples ```agda -import Ledger.Conway.Specification.Test.Examples -import Ledger.Conway.Specification.Test.StructuredContracts +import Test.Examples +import Test.StructuredContracts ``` ## Token Algebras From 32638968aef353c475385a8f24629ebe7726911a Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Thu, 6 Nov 2025 10:39:48 -0700 Subject: [PATCH 10/11] post-merge fixes and improvements --- src/Ledger.lagda.md | 2 ++ src/Ledger/Conway/Specification.lagda.md | 7 ------- src/Test/Examples.lagda.md | 9 ++++----- src/Test/Examples/AccountSim/Test/Trace.agda | 8 ++++---- src/Test/Examples/DEx/Test/Trace.agda | 14 +++++++------- src/Test/Examples/MultiSig/Test/Trace.agda | 2 +- src/Test/Examples/MultiSigV2/Test/Trace.agda | 2 +- 7 files changed, 19 insertions(+), 25 deletions(-) diff --git a/src/Ledger.lagda.md b/src/Ledger.lagda.md index 625792738..d04d63a95 100644 --- a/src/Ledger.lagda.md +++ b/src/Ledger.lagda.md @@ -12,5 +12,7 @@ import Ledger.Core import Ledger.Conway import Ledger.Dijkstra +import Test.Examples + import EssentialAgda ``` diff --git a/src/Ledger/Conway/Specification.lagda.md b/src/Ledger/Conway/Specification.lagda.md index da4181794..366492148 100644 --- a/src/Ledger/Conway/Specification.lagda.md +++ b/src/Ledger/Conway/Specification.lagda.md @@ -124,13 +124,6 @@ import Ledger.Conway.Specification.Script import Ledger.Conway.Specification.Script.Validation ``` -## Tests and Examples - -```agda -import Test.Examples -import Test.StructuredContracts -``` - ## Token Algebras ```agda diff --git a/src/Test/Examples.lagda.md b/src/Test/Examples.lagda.md index 4ffa48e15..7076446c8 100644 --- a/src/Test/Examples.lagda.md +++ b/src/Test/Examples.lagda.md @@ -7,7 +7,7 @@ The "Examples" module aims to add a couple of example smart contract validators written as part of the Cardano Formal Ledger Specification. These validator scripts are functions that examine a transaction and decide if the UTxO locked by their script can be spent as part of the current -transaction. +transaction. + +We define an instance of the `StrucSimulation`{.AgdaRecord} record type by +implementing a stateful program on (the Agda specification of) the Cardano ledger. +The following must be specified when defining such an instance. + +1. `State`{.AgdaDatatype}: the program state type. + +2. `Input`{.AgdaDatatype}: the program input type. + +3. `STRUC`{.AgdaDatatype}: the program's small-step semantics. + +4. `πˢ`{.AgdaField}: the projection function of program state from a given + ledger state. + +5. `πⁱ`{.AgdaField}: the projection function of program input from a given + `TxInfo`{.AgdaRecord}. + +6. `simulates`{.AgdaField}: the proof obligation required for demonstrating + that data in items 1--5 are such that the state of the program as it appears + on the ledger can only be updated according to its small-step + `STRUC`{.AgdaDatatype} specification. + +```agda SSRel : Type → Type → Type → Type₁ SSRel Env State Input = Env → State → Input → State → Type @@ -50,15 +60,17 @@ record StrucSimulation S I (_⊢_⇀⦇_,STRUC⦈_ : SSRel ⊤ S I) : Type₁ wh field πˢ : LState → Maybe S πⁱ : TxInfo → I - -- here, add optional extra assumptions about ledger state, env, and transaction that may be too difficult to prove without reasoning about complete ledger traces - -- e.g. transaction does not re-add a UTxO entry it spends - -- e.g. current Slot is after the validity interval of some previous transaction - extraAssmp : LEnv → LState → Tx → Type + -- here, add optional extra assumptions about ledger state, env, and + -- transaction that may be too difficult to prove without reasoning about + -- complete ledger traces; e.g., + -- * transaction does not re-add a UTxO entry it spends; + -- * current Slot is after the validity interval of some previous transaction + extraAssmp : LEnv → LState → Tx → Type _~ˢ_ : LState → S → Type -- R u ~ˢ s = πˢ u ≡ just s - -- only for PlutusV3 + -- only for PlutusV3 _~ᵉ_ : LEnv × Tx × LState → ⊤ × I → Type _~ᵉ_ = λ (le , tx , u) (tt , i) → πⁱ (txInfo PlutusV3 (PParamsOf le) (UTxOOf u) tx) ≡ i @@ -70,4 +82,4 @@ record StrucSimulation S I (_⊢_⇀⦇_,STRUC⦈_ : SSRel ⊤ S I) : Type₁ wh ──────────────────────────────── ∃[ s′ ] u′ ~ˢ s′ × tt ⊢ s ⇀⦇ i′ ,STRUC⦈ s′ -\end{code} +```