From c72d6066b2731f13ee3db2c50ec6a67b73bcce19 Mon Sep 17 00:00:00 2001 From: Tudor Ferariu Date: Fri, 17 Oct 2025 13:16:55 +0100 Subject: [PATCH 1/5] Reimplemented Alasdair's Example Traces and added 3 more example contracts --- .../Foreign/HSLedger/ExternalStructures.agda | 1 + src/Ledger/Conway/Specification/Abstract.agda | 2 + .../Conway/Specification/Script/Base.lagda.md | 2 +- .../Specification/Script/Validation.lagda.md | 25 +- .../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 .../Conway/Specification/Test/Examples.agda | 13 + .../Test/Examples.agda:Zone.Identifier | Bin 0 -> 25 bytes .../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 .../Test/Examples/HelloWorld.agda | 23 +- .../Examples/HelloWorld.agda:Zone.Identifier | Bin 0 -> 25 bytes .../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 .../Test/Examples/SucceedIfNumber.agda | 43 ++-- .../SucceedIfNumber.agda:Zone.Identifier | Bin 0 -> 25 bytes .../Test/LedgerImplementation.agda | 58 ++--- .../LedgerImplementation.agda:Zone.Identifier | Bin 0 -> 25 bytes src/Ledger/Conway/Specification/Test/Lib.agda | 27 ++- .../Test/Lib.agda:Zone.Identifier | Bin 0 -> 25 bytes .../Conway/Specification/Test/Prelude.agda | 89 ++++++- .../Test/Prelude.agda:Zone.Identifier | Bin 0 -> 25 bytes .../Test/StructuredContracts.lagda | 17 +- .../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.agda | 6 + 107 files changed, 3650 insertions(+), 114 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.agda b/src/Ledger/Conway/Specification/Abstract.agda index 14fd2b2ff..d70149f95 100644 --- a/src/Ledger/Conway/Specification/Abstract.agda +++ b/src/Ledger/Conway/Specification/Abstract.agda @@ -7,6 +7,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 @@ -23,3 +24,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 02e9dd5d1..eb3476811 100644 --- a/src/Ledger/Conway/Specification/Script/Validation.lagda.md +++ b/src/Ledger/Conway/Specification/Script/Validation.lagda.md @@ -17,13 +17,8 @@ module Ledger.Conway.Specification.Script.Validation open import Ledger.Prelude 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 +open import Ledger.Conway.Specification.Abstract txs +open import Ledger.Conway.Specification.ScriptPurpose txs rdptr : TxBody → ScriptPurpose → Maybe RdmrPtr rdptr txb = λ where @@ -51,18 +46,6 @@ getDatum tx utxo (Spend txin) = m = setToMap (mapˢ < hash , id > (TxWitnesses.txdats (Tx.wits tx))) getDatum tx utxo _ = nothing -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 @@ -92,8 +75,8 @@ credsNeeded utxo txb 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₂ 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 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@K2xdl#JyUFr831@K2xdl#JyUFr831@K2x Date: Fri, 17 Oct 2025 13:46:26 +0100 Subject: [PATCH 2/5] 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 3/5] 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 bfe047bbb73b875c64779284fda2a19119d79474 Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Wed, 22 Oct 2025 22:22:01 -0600 Subject: [PATCH 4/5] 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 13666bd9316f7fa46eaa29ac9319ce3856935aa3 Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Thu, 23 Oct 2025 01:53:08 -0600 Subject: [PATCH 5/5] Refactor: reorganize files and clean up imports (for PR #955) --- src/Ledger/Conway/Specification/Abstract.agda | 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.agda | 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.agda | 22 ++++++------ src/Ledger/Conway/Specification/Test/Lib.agda | 22 +++++------- .../Test/StructuredContracts.lagda | 2 +- .../Specification/Test/SymbolicData.agda | 14 +++++--- 42 files changed, 411 insertions(+), 577 deletions(-) rename src/Ledger/Conway/Specification/{ScriptPurpose.agda => Script/ScriptPurpose.lagda.md} (76%) diff --git a/src/Ledger/Conway/Specification/Abstract.agda b/src/Ledger/Conway/Specification/Abstract.agda index d70149f95..9b798221b 100644 --- a/src/Ledger/Conway/Specification/Abstract.agda +++ b/src/Ledger/Conway/Specification/Abstract.agda @@ -7,7 +7,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 eb3476811..6b6e6a6e1 100644 --- a/src/Ledger/Conway/Specification/Script/Validation.lagda.md +++ b/src/Ledger/Conway/Specification/Script/Validation.lagda.md @@ -18,7 +18,7 @@ open import Ledger.Prelude 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.agda b/src/Ledger/Conway/Specification/Test/Examples/HelloWorld.agda index bba15ea1a..cd357690b 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/HelloWorld.agda +++ b/src/Ledger/Conway/Specification/Test/Examples/HelloWorld.agda @@ -1,30 +1,27 @@ {-# 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.agda b/src/Ledger/Conway/Specification/Test/Examples/SucceedIfNumber.agda index 447947f1b..a5dfc72a3 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/SucceedIfNumber.agda +++ b/src/Ledger/Conway/Specification/Test/Examples/SucceedIfNumber.agda @@ -1,27 +1,27 @@ {-# OPTIONS --safe #-} +module Ledger.Conway.Specification.Test.Examples.SucceedIfNumber where + 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 import Ledger.Conway.Specification.Test.LedgerImplementation ℕ ℕ +open import Ledger.Conway.Specification.Script.ScriptPurpose SVTransactionStructure + +open import Ledger.Conway.Specification.Transaction open TransactionStructure SVTransactionStructure using (Data) -open import Ledger.Conway.Specification.ScriptPurpose SVTransactionStructure valContext : TxInfo → ScriptPurpose → Data valContext x x₁ = 0 -open import Ledger.Conway.Specification.Test.AbstractImplementation ℕ ℕ valContext -open import Ledger.Conway.Specification.Test.Lib ℕ ℕ 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 Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions -open import Ledger.Conway.Specification.Transaction +open import Ledger.Conway.Specification.Utxo.Properties.Computational SVTransactionStructure SVAbstractFunctions + open TransactionStructure SVTransactionStructure -open import Ledger.Core.Specification.Epoch -open EpochStructure SVEpochStructure open Implementation -open import Ledger.Conway.Specification.Utxo.Properties.Computational SVTransactionStructure SVAbstractFunctions -- succeed if the datum is 1 succeedIf1Datum' : Maybe ℕ → Maybe ℕ → Bool diff --git a/src/Ledger/Conway/Specification/Test/Lib.agda b/src/Ledger/Conway/Specification/Test/Lib.agda index 2cee8ce98..42564a2e6 100644 --- a/src/Ledger/Conway/Specification/Test/Lib.agda +++ b/src/Ledger/Conway/Specification/Test/Lib.agda @@ -1,31 +1,25 @@ {-# 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 b/src/Ledger/Conway/Specification/Test/StructuredContracts.lagda index 092c925ad..602cdeb00 100644 --- a/src/Ledger/Conway/Specification/Test/StructuredContracts.lagda +++ b/src/Ledger/Conway/Specification/Test/StructuredContracts.lagda @@ -19,7 +19,7 @@ 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.ScriptPurpose txs open import Ledger.Conway.Specification.Script.Validation txs abs open import Ledger.Conway.Specification.Utxo txs abs \end{code} 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