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.lagda.md b/src/Ledger/Conway/Specification.lagda.md index a9502f5b7..01c3d1940 100644 --- a/src/Ledger/Conway/Specification.lagda.md +++ b/src/Ledger/Conway/Specification.lagda.md @@ -33,8 +33,6 @@ import Ledger.Conway.Specification.RewardUpdate import Ledger.Conway.Specification.RewardUpdate.Properties import Ledger.Conway.Specification.Script import Ledger.Conway.Specification.Script.Validation -import Ledger.Conway.Specification.Test.Examples -import Ledger.Conway.Specification.Test.StructuredContracts import Ledger.Conway.Specification.TokenAlgebra.Base import Ledger.Conway.Specification.TokenAlgebra.Coin import Ledger.Conway.Specification.TokenAlgebra.ValueSet @@ -45,4 +43,7 @@ import Ledger.Conway.Specification.Utxo import Ledger.Conway.Specification.Utxo.Properties import Ledger.Conway.Specification.Utxow import Ledger.Conway.Specification.Utxow.Properties + +import Test.Examples +import Test.StructuredContracts ``` diff --git a/src/Ledger/Conway/Specification/Abstract.lagda.md b/src/Ledger/Conway/Specification/Abstract.lagda.md index b89f9ba2d..a269725ac 100644 --- a/src/Ledger/Conway/Specification/Abstract.lagda.md +++ b/src/Ledger/Conway/Specification/Abstract.lagda.md @@ -13,6 +13,7 @@ module Ledger.Conway.Specification.Abstract (txs : TransactionStructure) where open TransactionStructure txs open import Ledger.Conway.Specification.Certs govStructure +open import Ledger.Conway.Specification.Script.ScriptPurpose txs record indexOf : Type where field @@ -29,4 +30,5 @@ 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/ScriptPurpose.lagda.md b/src/Ledger/Conway/Specification/Script/ScriptPurpose.lagda.md new file mode 100644 index 000000000..454d199a8 --- /dev/null +++ b/src/Ledger/Conway/Specification/Script/ScriptPurpose.lagda.md @@ -0,0 +1,42 @@ +--- +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 + 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/Script/Validation.lagda.md b/src/Ledger/Conway/Specification/Script/Validation.lagda.md index f465be2eb..6ed6b3c83 100644 --- a/src/Ledger/Conway/Specification/Script/Validation.lagda.md +++ b/src/Ledger/Conway/Specification/Script/Validation.lagda.md @@ -21,21 +21,10 @@ module Ledger.Conway.Specification.Script.Validation open import Ledger.Prelude open import Ledger.Conway.Specification.Certs govStructure -``` ---> -```agda -data ScriptPurpose : Type where - Cert : DCert → ScriptPurpose - Rwrd : RwdAddr → ScriptPurpose - Mint : ScriptHash → ScriptPurpose - Spend : TxIn → ScriptPurpose - Vote : GovVoter → ScriptPurpose - Propose : GovProposal → ScriptPurpose -``` +open import Ledger.Conway.Specification.Abstract txs +open import Ledger.Conway.Specification.Script.ScriptPurpose txs - - ```agda -record TxInfo : Type where - field realizedInputs : UTxO - txOuts : Ix ⇀ TxOut - fee : Value - mint : Value - txCerts : List DCert - txWithdrawals : Withdrawals - txVldt : Maybe Slot × Maybe Slot - vkKey : ℙ KeyHash - txdats : ℙ Datum - txId : TxId - txInfo : Language → PParams → UTxO → Tx @@ -100,14 +76,14 @@ credsNeeded utxo txb (fromList (map voter txGovVotes)) ∪ mapPartial (λ p → if p .policy then (λ {sh} → just (Propose p , ScriptObj sh)) else nothing) (fromList txGovProposals) -``` - - diff --git a/src/Ledger/Conway/Specification/Test/Examples.lagda.md b/src/Ledger/Conway/Specification/Test/Examples.lagda.md deleted file mode 100644 index 45e1c99ca..000000000 --- a/src/Ledger/Conway/Specification/Test/Examples.lagda.md +++ /dev/null @@ -1,12 +0,0 @@ ---- -source_branch: master -source_path: src/Ledger/Conway/Specification/Test/Examples.lagda.md ---- - -```agda -{-# OPTIONS --safe #-} -module Ledger.Conway.Specification.Test.Examples where - -import Ledger.Conway.Specification.Test.Examples.SucceedIfNumber -import Ledger.Conway.Specification.Test.Examples.HelloWorld -``` diff --git a/src/Ledger/Conway/Specification/Test/Prelude.lagda.md b/src/Ledger/Conway/Specification/Test/Prelude.lagda.md deleted file mode 100644 index 2b5dae9aa..000000000 --- a/src/Ledger/Conway/Specification/Test/Prelude.lagda.md +++ /dev/null @@ -1,18 +0,0 @@ ---- -source_branch: master -source_path: src/Ledger/Conway/Specification/Test/Prelude.lagda.md ---- - -```agda -{-# OPTIONS --safe #-} -open import Ledger.Prelude hiding (fromList; ε); open Computational - -module Ledger.Conway.Specification.Test.Prelude where - -record ScriptImplementation (T D : Type) : Type₁ where - field serialise : T → D - deserialise : D → Maybe T - toData' : ∀ {A : Type} → A → D -- fix this - ⦃ DecEq-Data ⦄ : DecEq D - ⦃ Show-Data ⦄ : Show D -``` diff --git a/src/Ledger/Conway/Specification/Utxow/Properties/Computational.lagda.md b/src/Ledger/Conway/Specification/Utxow/Properties/Computational.lagda.md index b98fa8db3..ec5d0f0a9 100644 --- a/src/Ledger/Conway/Specification/Utxow/Properties/Computational.lagda.md +++ b/src/Ledger/Conway/Specification/Utxow/Properties/Computational.lagda.md @@ -3,6 +3,7 @@ source_branch: master source_path: src/Ledger/Conway/Specification/Utxow/Properties/Computational.lagda.md --- + +```agda instance Computational-UTXOW : Computational _⊢_⇀⦇_,UTXOW⦈_ String Computational-UTXOW = record {Go} - where module Go Γ s tx (let H , ⁇ H? = UTXOW-inductive-premises {tx} {s}) where + where module Go Γ s tx (let H , ⁇ H? = UTXOW-inductive-premises {tx}{s}) where open Computational Computational-UTXO renaming (computeProof to computeProof'; completeness to completeness') @@ -61,3 +64,10 @@ instance ... | yes _ with computeProof' Γ s tx | completeness' _ _ _ _ h ... | success _ | refl = refl ``` + + +The first two examples, "SucceedIfNumber" and "HelloWorld" are very simple +scripts that allow their UTxO to be spent if the input is a number or +the string "Hello World", respectively. In each file are also defined +example transactions that are expected to succeed or fail, respectively. +These transactions are passed through the UTxO-step rule, which uses the +formal ledger specification to simulate an actual transaction on the +blockchain and tells us if said transaction succeeds or not. As part +of the UTxO rule, we also run the scripts locking any consumed outputs, +which in our case are the validator scripts. + +The other examples are more in-depth and are separated across +multiple modules. + +```agda +import Test.Examples.MultiSig.Datum +import Test.Examples.MultiSig.Validator +import Test.Examples.MultiSig.Test.Trace +``` + +The "MultiSig" example is based on the Multi-Signature wallet smart +contract proposed in the seminal EUTxO paper by Chakravarty et. al. +It aims to simulate a wallet that has a certain number of authorized +signatories, of which a certain subset must sign before a payment +can be approved. Payments can also be cancelled if a deadline passes +before enough signatories can be gathered. + +All examples after and including this one use the same structure: + +A "Datum" file that defines the types of the Input and Redeemer for +our validator script. The Datum stores most of the stateful information +in our smart contract. In the case of MultiSig, that would include +if a payment is trying to be made, who the payment is for, and +who has already signed off on said payment. The Inputs, on the other hand, +are the "actions" that the script is allowed to take. This would include +proposing a payment, signing on a payment, cancelling the payment after +the deadline is passed, etc. + +A "Validator" file where the actual script is defined, alongside any +helper functions needed. Generally, the validator script is a combination +of checks that depend on what the contract is trying to accomplish, such +as making sure we only allow authorized wallets to sign, or executing +payments only after enough signatories are gathered. The validators +use Symbolic Data in order to avoid cyclical definitions. The Symbolic +data is described in more detail in a separate module in this folder, +but translates almost directly into the same data types used by the +Formal Ledger Rules. + +An "OffChain" folder, which defines the "endpoints" used to interact with +our account. Essentially, this defines a way to easily create a transaction +where we are attempting to execute one of the actions our validator +might allow. This includes various aspects, such as making sure the transaction + +is signed by the right person, that the correct fees are paid, that payments +are sent to the correct recipients, that the smart contract self-perpetuates, etc. + +Finally, the "Trace" file in the "Test" folder contains some definitions that +allow us to systematically apply multiple transactions in sequence, as well +as a couple of example traces of such sequences being run. By making use +of the previously defined "OffChain" endpoints, we can create transactions +which can be similarly verified using the UTxO or UTxOw rules defined by +the ledger specification. To do this for a sequence of transactions, we +define an "evalTransactions" function which takes a list of transactions +and applies them sequentially, letting us know if they all succeed or +if there is an error along the way. Finally, we put together some example +traces by defining lists of transactions that are expected to either +succeed or fail, running our "evalTransactions" function on that list +and checking that we get the expected result. + +We have a trace that puts the smart contract on the simulated ledger, +proposes a payment, adds the two required signatures, and then executes +a payment. This trace succeeds and is tested with both the UTxO and UTxOw +rules. We also have a failing trace, where after the first payment, we try +to propose another payment of a larger amount than is contained in the wallet, +which naturally fails. + +```agda +import Test.Examples.AccountSim.Datum +import Test.Examples.AccountSim.Validator +import Test.Examples.AccountSim.Test.Trace +``` + +The "AccountSim" contract attempts to simulate an account-based system +on UTxO. It is a naive implementation which holds all accounts represented +as a list of pairs linking a Public Key Hash to its associated Value. + +It is meant to have the generic abilities required of such a simulation: +opening/closing an account, depositing/withdrawing value from/to your account, +transferring value to some other account, and a cleanup function when there +are no accounts left to remove the UTxO from the blockchain. + +The example traces attempt to test every individual endpoint at least once, +as well as a simple failing trace where we try to withdraw more than an +account has in it. + + +```agda +import Test.Examples.DEx.Datum +import Test.Examples.DEx.Validator +import Test.Examples.DEx.Test.Trace +``` + +The "DEx" contract is meant to implement a Limit Order Book +Distributed Exchange. It is primarily designed for exchanging +one currency for another at various rates, but the Token Algebra +for native tokens is currently incomplete. As such, the example +currently exchanges Ada for Ada. When multiple assets can be used, +the code can be easily modified to fulfill its full purpose. + + +```agda +import Test.Examples.MultiSigV2.Datum +import Test.Examples.MultiSigV2.Validator +import Test.Examples.MultiSigV2.Test.Trace +``` + +The second implementation of "MultiSig" is, at its core, the same +contract, but with some modifications made to aid the effort of +proving properties of the validator. Many of these changes were +primarily made in order to better integrate with the Thread Token +mechanism necessary for certain properties of UTxO-based smart +contracts. Due to similar problems to the distributed exchange, +tokens are not currently fully functional, so for now, it can +be viewed as an alternative implementation of the same specification. diff --git a/src/Test/Examples/AccountSim/Datum.agda b/src/Test/Examples/AccountSim/Datum.agda new file mode 100644 index 000000000..dde66212f --- /dev/null +++ b/src/Test/Examples/AccountSim/Datum.agda @@ -0,0 +1,30 @@ +{-# OPTIONS --safe #-} + +open import Ledger.Prelude hiding (fromList; ε); open Computational + +module Test.Examples.AccountSim.Datum where + +open import Tactic.Derive.DecEq +open import Data.Vec as Vec + hiding (fromList) +import stdlib.Data.Vec.Instances as Vec +import Data.Vec.Relation.Binary.Pointwise.Inductive as Vec + +data Label : Set where + Always : List (ℕ × ℕ) -> Label +instance + unquoteDecl DecEq-Label = derive-DecEq + ((quote Label , DecEq-Label) ∷ []) + +data Input : Set where + Open : ℕ -> Input + Close : ℕ -> Input + Withdraw : ℕ -> ℕ -> Input + Deposit : ℕ -> ℕ -> Input + Transfer : ℕ -> ℕ -> ℕ -> Input + Cleanup : Input +instance + unquoteDecl DecEq-Input = derive-DecEq + ((quote Input , DecEq-Input) ∷ []) + +AccountSimData = Label ⊎ Input diff --git a/src/Test/Examples/AccountSim/OffChain/Cleanup.agda b/src/Test/Examples/AccountSim/OffChain/Cleanup.agda new file mode 100644 index 000000000..f98e950ca --- /dev/null +++ b/src/Test/Examples/AccountSim/OffChain/Cleanup.agda @@ -0,0 +1,49 @@ +{-# OPTIONS --safe #-} + +module Test.Examples.AccountSim.OffChain.Cleanup where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction + +open import Test.Examples.AccountSim.Datum +open import Test.Examples.AccountSim.OffChain.Lib +open import Test.Examples.AccountSim.Validator +open import Test.Prelude AccountSimData +open import Test.SymbolicData AccountSimData +open import Test.LedgerImplementation SData SData +open import Test.AbstractImplementation valContext +open import Test.Lib valContext + +open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions + +open TransactionStructure SVTransactionStructure +open Implementation + +makeCleanupTx : (id : ℕ) → UTxOState → PlutusScript → (w : ℕ) → Maybe Tx +makeCleanupTx id state script@(sh , _) w = + let + wutxo = getWalletUTxO w (UTxOState.utxo state) + in + maybe (λ { (scIn , (fst , txValue , snd)) → + just ( + record { body = record defaultTxBody + { txIns = Ledger.Prelude.fromList ((scIn ∷ []) ++ (map proj₁ wutxo)) + ; txOuts = fromListIx (makeFeeUnPaymentTxOut wutxo txValue) + ; txId = id + ; collateralInputs = Ledger.Prelude.fromList (map proj₁ wutxo) + ; reqSignerHashes = Ledger.Prelude.fromList (w ∷ []) + } ; + wits = record { vkSigs = fromListᵐ ((w , (_+_ {{addNat}} (getTxId wutxo) w) ) ∷ []) ; + scripts = Ledger.Prelude.fromList ((inj₂ script) ∷ []) ; + txdats = ∅ ; + txrdmrs = fromListᵐ (((Spend , (proj₂ scIn)) , + inj₁ (inj₂ Cleanup) , + ((getTxId wutxo) , w)) ∷ []) } ; + txsize = 10 ; + isValid = true ; + txAD = nothing } + ) + }) + nothing + (getScriptUTxO sh (UTxOState.utxo state)) + diff --git a/src/Test/Examples/AccountSim/OffChain/Close.agda b/src/Test/Examples/AccountSim/OffChain/Close.agda new file mode 100644 index 000000000..cbeb54f53 --- /dev/null +++ b/src/Test/Examples/AccountSim/OffChain/Close.agda @@ -0,0 +1,55 @@ +{-# OPTIONS --safe #-} + +module Test.Examples.AccountSim.OffChain.Close where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction + +open import Test.Examples.AccountSim.Datum +open import Test.Examples.AccountSim.Validator +open import Test.Examples.AccountSim.OffChain.Lib +open import Test.Prelude AccountSimData +open import Test.SymbolicData AccountSimData +open import Test.LedgerImplementation SData SData +open import Test.AbstractImplementation valContext +open import Test.Lib valContext + +open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions + +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 + wutxo = getWalletUTxO w (UTxOState.utxo state) + in + maybe (λ { (scIn , scOut) → maybe (λ label → + just ( + record { body = record defaultTxBody + { txIns = Ledger.Prelude.fromList ((scIn ∷ []) ++ (map proj₁ wutxo)) + ; txOuts = fromListIx (makeFeeTxOut wutxo ++ makeCloseTxOut label (proj₂ scIn) w scOut ) + ; txId = id + ; collateralInputs = Ledger.Prelude.fromList (map proj₁ wutxo) + ; reqSignerHashes = Ledger.Prelude.fromList (w ∷ []) + } ; + wits = record { vkSigs = fromListᵐ ((w , (_+_ {{addNat}} (getTxId wutxo) w) ) ∷ []) ; + scripts = Ledger.Prelude.fromList ((inj₂ script) ∷ []) ; + txdats = ∅ ; + txrdmrs = fromListᵐ (((Spend , (proj₂ scIn)) , + inj₁ (inj₂ (Close w)) , + ((getTxId wutxo) , w)) ∷ []) } ; + txsize = 10 ; + isValid = true ; + txAD = nothing } + )) + nothing + (getLabel scOut)}) + nothing + (getScriptUTxO sh (UTxOState.utxo state)) + diff --git a/src/Test/Examples/AccountSim/OffChain/Deposit.agda b/src/Test/Examples/AccountSim/OffChain/Deposit.agda new file mode 100644 index 000000000..26d5057f6 --- /dev/null +++ b/src/Test/Examples/AccountSim/OffChain/Deposit.agda @@ -0,0 +1,63 @@ +{-# OPTIONS --safe #-} + +module Test.Examples.AccountSim.OffChain.Deposit where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction + +open import Test.Examples.AccountSim.Datum +open import Test.Examples.AccountSim.OffChain.Lib +open import Test.Examples.AccountSim.Validator +open import Test.Prelude AccountSimData +open import Test.SymbolicData AccountSimData +open import Test.LedgerImplementation SData SData +open import Test.AbstractImplementation valContext +open import Test.Lib valContext + +open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions + +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) + where + val = getVal (Always l) w + + + +makeDepositTxOut : Label → (scriptIx : ℕ) → TxOut → (w : ℕ) → (v : Value) → List (ℕ × TxOut) +makeDepositTxOut (Always l) ix txo w v = + (ix , scriptDTxOut (Always l) txo w v) + ∷ [] + + + +makeDepositTx : (id : ℕ) → UTxOState → PlutusScript → (w : ℕ) → (v : Value) → Maybe Tx +makeDepositTx id state script@(sh , _) w v = + let + wutxo = getWalletUTxO w (UTxOState.utxo state) + in + maybe (λ { (scIn , scOut) → maybe (λ label → + just ( + record { body = record defaultTxBody + { txIns = Ledger.Prelude.fromList ((scIn ∷ []) ++ (map proj₁ wutxo)) + ; txOuts = fromListIx (makeFeePaymentTxOut wutxo v ++ makeDepositTxOut label (proj₂ scIn) scOut w v ) + ; txId = id + ; collateralInputs = Ledger.Prelude.fromList (map proj₁ wutxo) + ; reqSignerHashes = Ledger.Prelude.fromList (w ∷ []) + } ; + wits = record { vkSigs = fromListᵐ ((w , (_+_ {{addNat}} (getTxId wutxo) w)) ∷ []) ; + scripts = Ledger.Prelude.fromList ((inj₂ script) ∷ []) ; + txdats = ∅ ; + txrdmrs = fromListᵐ (((Spend , (proj₂ scIn)) , + inj₁ (inj₂ (Deposit w v)) , + ((getTxId wutxo) , w)) ∷ []) } ; + txsize = 10 ; + isValid = true ; + txAD = nothing } + )) + nothing + (getLabel scOut)}) + nothing + (getScriptUTxO sh (UTxOState.utxo state)) diff --git a/src/Test/Examples/AccountSim/OffChain/Lib.agda b/src/Test/Examples/AccountSim/OffChain/Lib.agda new file mode 100644 index 000000000..cbf113248 --- /dev/null +++ b/src/Test/Examples/AccountSim/OffChain/Lib.agda @@ -0,0 +1,97 @@ +{-# OPTIONS --safe #-} + +module Test.Examples.AccountSim.OffChain.Lib where + +open import Data.List using (filter) + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction using (TransactionStructure) + +open import Test.Examples.AccountSim.Datum +open import Test.Examples.AccountSim.Validator +open import Test.Prelude AccountSimData +open import Test.SymbolicData AccountSimData +open import Test.LedgerImplementation SData SData + +open TransactionStructure SVTransactionStructure + +defaultTxBody : TxBody +defaultTxBody = record + { txIns = ∅ + ; refInputs = ∅ + ; collateralInputs = ∅ + ; txOuts = ∅ + ; txFee = 10000000000 + ; mint = 0 + ; txVldt = nothing , nothing + ; txCerts = [] + ; txWithdrawals = ∅ + ; txGovVotes = [] + ; txGovProposals = [] + ; txDonation = 0 + ; txADhash = nothing + ; txNetworkId = just 0 + ; currentTreasury = nothing + ; txId = 0 + ; reqSignerHashes = ∅ + ; scriptIntegrityHash = nothing + } + +matchScriptAddress : (scriptHash : ℕ) → Credential → Set +matchScriptAddress sh (KeyHashObj x) = ⊥ +matchScriptAddress sh (ScriptObj y) = True (sh ≟ y) + +matchScriptAddress? : (sh : ℕ) → (c : Credential) → Dec (matchScriptAddress sh c) +matchScriptAddress? sh (KeyHashObj x) = no (λ x₁ → x₁) +matchScriptAddress? sh (ScriptObj y) = T? ⌊ (sh ≟ y) ⌋ + +getScriptUTxO : (scriptHash : ℕ) → UTxO → Maybe (TxIn × TxOut) +getScriptUTxO sh (utxo , prf) = head $ filter (λ { (_ , addr , _) → matchScriptAddress? sh (payCred addr)}) (setToList utxo) + +matchWalletHash : (keyHash : ℕ) → Credential → Set +matchWalletHash kh (KeyHashObj x) = True (kh ≟ x) +matchWalletHash kh (ScriptObj y) = ⊥ + +matchWalletHash? : (sh : ℕ) → (c : Credential) → Dec (matchWalletHash sh c) +matchWalletHash? kh (KeyHashObj x) = T? ⌊ (kh ≟ x) ⌋ +matchWalletHash? kh (ScriptObj y) = no (λ x₁ → x₁) + +getWalletUTxO : (scriptHash : ℕ) → UTxO → List (TxIn × TxOut) +getWalletUTxO sh (utxo , prf) = filter (λ { (_ , addr , _) → matchWalletHash? sh (payCred addr)}) (setToList utxo) + + + +getLabel : TxOut → Maybe Label +getLabel (fst , fst₁ , just (inj₁ (inj₁ (inj₁ x))) , snd) = just x +getLabel (fst , fst₁ , just (inj₁ (inj₁ (inj₂ y))) , snd) = nothing +getLabel (fst , fst₁ , just (inj₁ (inj₂ y)) , snd) = nothing +getLabel (fst , fst₁ , just (inj₂ y) , snd) = nothing +getLabel (fst , fst₁ , nothing , snd) = nothing + + + +-- Assumes a list of filtered waller txins and subtracts a default fee from the head of the list +makeFeeTxOut : List (TxIn × TxOut) → List (ℕ × TxOut) +makeFeeTxOut [] = [] +makeFeeTxOut ((txin , (fst , txValue , snd)) ∷ utxos) = (proj₂ txin , fst , txValue - feeValue , snd) ∷ [] + +makeFeeUnPaymentTxOut : List (TxIn × TxOut) → Value → List (ℕ × TxOut) +makeFeeUnPaymentTxOut [] v = [] +makeFeeUnPaymentTxOut ((txin , (fst , txValue , snd)) ∷ utxos) v = (proj₂ txin , fst , _+_ {{addValue}} (txValue - feeValue) v , snd) ∷ [] + +makeFeePaymentTxOut : List (TxIn × TxOut) → Value → List (ℕ × TxOut) +makeFeePaymentTxOut [] v = [] +makeFeePaymentTxOut ((txin , (fst , txValue , snd)) ∷ utxos) v = (proj₂ txin , fst , (txValue - feeValue ) - v , snd) ∷ [] + +-- return id of 0 if no txins +getTxId : List (TxIn × TxOut) → ℕ +getTxId xs = maybe (λ x → proj₁ (proj₁ x)) 0 (head xs) + +getVal : Label -> ℕ -> Value +getVal (Always l) w with lookup' w l +...| nothing = emptyValue +...| just v = v + + + + diff --git a/src/Test/Examples/AccountSim/OffChain/OffChain.agda b/src/Test/Examples/AccountSim/OffChain/OffChain.agda new file mode 100644 index 000000000..26af09991 --- /dev/null +++ b/src/Test/Examples/AccountSim/OffChain/OffChain.agda @@ -0,0 +1,11 @@ +{-# OPTIONS --safe #-} + +module Test.Examples.AccountSim.OffChain.OffChain where + +open import Test.Examples.AccountSim.OffChain.Start public +open import Test.Examples.AccountSim.OffChain.Close public +open import Test.Examples.AccountSim.OffChain.Open public +open import Test.Examples.AccountSim.OffChain.Deposit public +open import Test.Examples.AccountSim.OffChain.Withdraw public +open import Test.Examples.AccountSim.OffChain.Transfer public +open import Test.Examples.AccountSim.OffChain.Cleanup public diff --git a/src/Test/Examples/AccountSim/OffChain/Open.agda b/src/Test/Examples/AccountSim/OffChain/Open.agda new file mode 100644 index 000000000..48fbf6e03 --- /dev/null +++ b/src/Test/Examples/AccountSim/OffChain/Open.agda @@ -0,0 +1,54 @@ +{-# OPTIONS --safe #-} + +module Test.Examples.AccountSim.OffChain.Open where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction + +open import Test.Examples.AccountSim.Datum +open import Test.Examples.AccountSim.OffChain.Lib +open import Test.Examples.AccountSim.Validator +open import Test.Prelude AccountSimData +open import Test.SymbolicData AccountSimData +open import Test.LedgerImplementation SData SData +open import Test.AbstractImplementation valContext +open import Test.Lib valContext + +open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions + +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 + wutxo = getWalletUTxO w (UTxOState.utxo state) + in + maybe (λ { (scIn , scOut) → maybe (λ label → + just ( + record { body = record defaultTxBody + { txIns = Ledger.Prelude.fromList ((scIn ∷ []) ++ (map proj₁ wutxo)) + ; txOuts = fromListIx (makeFeeTxOut wutxo ++ makeOpenTxOut label (proj₂ scIn) w scOut ) + ; txId = id + ; collateralInputs = Ledger.Prelude.fromList (map proj₁ wutxo) + ; reqSignerHashes = Ledger.Prelude.fromList (w ∷ []) + } ; + wits = record { vkSigs = fromListᵐ ((w , (_+_ {{addNat}} (getTxId wutxo) w)) ∷ []) ; + scripts = Ledger.Prelude.fromList ((inj₂ script) ∷ []) ; + txdats = ∅ ; + txrdmrs = fromListᵐ (((Spend , (proj₂ scIn)) , + inj₁ (inj₂ (Open w)) , --(Add w) + ((getTxId wutxo) , w)) ∷ []) } ; + txsize = 10 ; + isValid = true ; + txAD = nothing } + )) + nothing + (getLabel scOut)}) + nothing + (getScriptUTxO sh (UTxOState.utxo state)) + diff --git a/src/Test/Examples/AccountSim/OffChain/Start.agda b/src/Test/Examples/AccountSim/OffChain/Start.agda new file mode 100644 index 000000000..d54fac4d1 --- /dev/null +++ b/src/Test/Examples/AccountSim/OffChain/Start.agda @@ -0,0 +1,47 @@ +{-# OPTIONS --safe #-} + +module Test.Examples.AccountSim.OffChain.Start where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction using (TransactionStructure) + +open import Test.Examples.AccountSim.Datum +open import Test.Examples.AccountSim.OffChain.Lib +open import Test.Examples.AccountSim.Validator +open import Test.Prelude AccountSimData +open import Test.SymbolicData AccountSimData +open import Test.LedgerImplementation SData SData +open import Test.Lib valContext + +open TransactionStructure SVTransactionStructure +open Implementation + +startTxOut : Value → PlutusScript → TxOut +startTxOut v script = inj₁ (record { net = 0 ; + pay = ScriptObj (proj₁ script) ; + stake = just (ScriptObj (proj₁ script)) }) + , v + , just (inj₁ (inj₁ (inj₁ (Always [])))) , nothing + +-- txid, wallet, value at script, script index +startTx : (id w tw : ℕ) → (v : Value) → PlutusScript → Tx +startTx id w tw v script = record { body = record defaultTxBody + { txIns = Ledger.Prelude.fromList ((w , w) ∷ []) + ; txOuts = fromListIx ((tw , startTxOut v script) + ∷ (w + , ((inj₁ (record { net = 0 ; + pay = KeyHashObj w ; + stake = just (KeyHashObj w) })) + , ((startValue - feeValue) - v) , nothing , nothing)) + ∷ []) + ; txId = id + ; collateralInputs = Ledger.Prelude.fromList ((w , w) ∷ []) + } ; + wits = record { vkSigs = fromListᵐ ((w , (_+_ {{addNat}} w id)) ∷ []) ; + scripts = ∅ ; + txdats = ∅ ; + txrdmrs = ∅ } ; + + txsize = 10 ; + isValid = true ; + txAD = nothing } diff --git a/src/Test/Examples/AccountSim/OffChain/Transfer.agda b/src/Test/Examples/AccountSim/OffChain/Transfer.agda new file mode 100644 index 000000000..31c10a031 --- /dev/null +++ b/src/Test/Examples/AccountSim/OffChain/Transfer.agda @@ -0,0 +1,58 @@ +{-# OPTIONS --safe #-} + +module Test.Examples.AccountSim.OffChain.Transfer where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction + +open import Test.Examples.AccountSim.Datum +open import Test.Examples.AccountSim.OffChain.Lib +open import Test.Examples.AccountSim.Validator +open import Test.Prelude AccountSimData +open import Test.SymbolicData AccountSimData +open import Test.LedgerImplementation SData SData +open import Test.AbstractImplementation valContext +open import Test.Lib valContext + +open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions + +open TransactionStructure SVTransactionStructure +open Implementation + + +makeTransferTxOut : Label → (scriptIx from to : ℕ) → (v : Value) → TxOut → List (ℕ × TxOut) +makeTransferTxOut (Always l) ix from to v (fst , fst' , snd) = + (ix , (fst , fst' , just (inj₁ (inj₁ (inj₁ (Always (insert' from (vF - v) (insert' to (_+_ {{addValue}} vT v) l)))))) , nothing)) ∷ [] + where + vF = getVal (Always l) from + vT = getVal (Always l) to + +makeTransferTx : (id : ℕ) → UTxOState → PlutusScript → (from to : ℕ) → (v : Value) → Maybe Tx +makeTransferTx id state script@(sh , _) from to v = + let + wutxo = getWalletUTxO from (UTxOState.utxo state) + in + maybe (λ { (scIn , scOut) → maybe (λ label → + just ( + record { body = record defaultTxBody + { txIns = Ledger.Prelude.fromList ((scIn ∷ []) ++ (map proj₁ wutxo)) + ; txOuts = fromListIx (makeFeeTxOut wutxo ++ makeTransferTxOut label (proj₂ scIn) from to v scOut ) + ; txId = id + ; collateralInputs = Ledger.Prelude.fromList (map proj₁ wutxo) + ; reqSignerHashes = Ledger.Prelude.fromList (from ∷ []) + } ; + wits = record { vkSigs = fromListᵐ ((from , (_+_ {{addNat}} (getTxId wutxo) from)) ∷ []) ; + scripts = Ledger.Prelude.fromList ((inj₂ script) ∷ []) ; + txdats = ∅ ; + txrdmrs = fromListᵐ (((Spend , (proj₂ scIn)) , + inj₁ (inj₂ (Transfer from to v)) , --(Add w) + ((getTxId wutxo) , from)) ∷ []) } ; + txsize = 10 ; + isValid = true ; + txAD = nothing } + )) + nothing + (getLabel scOut)}) + nothing + (getScriptUTxO sh (UTxOState.utxo state)) + diff --git a/src/Test/Examples/AccountSim/OffChain/Withdraw.agda b/src/Test/Examples/AccountSim/OffChain/Withdraw.agda new file mode 100644 index 000000000..e39f5e4ef --- /dev/null +++ b/src/Test/Examples/AccountSim/OffChain/Withdraw.agda @@ -0,0 +1,61 @@ +{-# OPTIONS --safe #-} + +module Test.Examples.AccountSim.OffChain.Withdraw where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction + +open import Test.Examples.AccountSim.Datum +open import Test.Examples.AccountSim.OffChain.Lib +open import Test.Examples.AccountSim.Validator +open import Test.Prelude AccountSimData +open import Test.SymbolicData AccountSimData +open import Test.LedgerImplementation SData SData +open import Test.AbstractImplementation valContext +open import Test.Lib valContext + +open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions + +open TransactionStructure SVTransactionStructure +open Implementation + + +scriptTxOut : Label → TxOut → (w : ℕ) → (v : Value) → TxOut +scriptTxOut (Always l) (fst , txValue , snd) w v = (fst , txValue - v , (just (inj₁ (inj₁ (inj₁ (Always (insert' w (val - v) l)))))) , nothing) + where + val = getVal (Always l) w + + +makeWithdrawTxOut : Label → (scriptIx : ℕ) → TxOut → (w : ℕ) → (v : Value) → List (ℕ × TxOut) +makeWithdrawTxOut (Always l) ix txo w v = + (ix , scriptTxOut (Always l) txo w v) ∷ [] + + +makeWithdrawTx : (id : ℕ) → UTxOState → PlutusScript → (w : ℕ) → (v : Value) → Maybe Tx +makeWithdrawTx id state script@(sh , _) w v = + let + wutxo = getWalletUTxO w (UTxOState.utxo state) + in + maybe (λ { (scIn , scOut) → maybe (λ label → + just ( + record { body = record defaultTxBody + { txIns = Ledger.Prelude.fromList ((scIn ∷ []) ++ (map proj₁ wutxo)) + ; txOuts = fromListIx (makeFeeUnPaymentTxOut wutxo v ++ makeWithdrawTxOut label (proj₂ scIn) scOut w v ) + ; txId = id + ; collateralInputs = Ledger.Prelude.fromList (map proj₁ wutxo) + ; reqSignerHashes = Ledger.Prelude.fromList (w ∷ []) + } ; + wits = record { vkSigs = fromListᵐ ((w , (_+_ {{addNat}} (getTxId wutxo) w)) ∷ []) ; + scripts = Ledger.Prelude.fromList ((inj₂ script) ∷ []) ; + txdats = ∅ ; + txrdmrs = fromListᵐ (((Spend , (proj₂ scIn)) , + inj₁ (inj₂ (Withdraw w v)) , + ((getTxId wutxo) , w)) ∷ []) } ; + txsize = 10 ; + isValid = true ; + txAD = nothing } + )) + nothing + (getLabel scOut)}) + nothing + (getScriptUTxO sh (UTxOState.utxo state)) diff --git a/src/Test/Examples/AccountSim/Test/Trace.agda b/src/Test/Examples/AccountSim/Test/Trace.agda new file mode 100644 index 000000000..4c2326e0f --- /dev/null +++ b/src/Test/Examples/AccountSim/Test/Trace.agda @@ -0,0 +1,165 @@ +{-# OPTIONS --safe #-} + +module Test.Examples.AccountSim.Test.Trace where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction using (TransactionStructure) + +open import Test.Examples.AccountSim.Datum +open import Test.Examples.AccountSim.OffChain.OffChain +open import Test.Examples.AccountSim.Validator +open import Test.Prelude AccountSimData +open import Test.SymbolicData AccountSimData +open import Test.LedgerImplementation SData SData +open import Test.AbstractImplementation valContext +open import Test.Lib valContext + +open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions +open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions +open import Ledger.Conway.Specification.Utxo.Properties.Computational SVTransactionStructure SVAbstractFunctions +open import Ledger.Conway.Specification.Utxow.Properties.Computational SVTransactionStructure SVAbstractFunctions + +open TransactionStructure SVTransactionStructure +open Implementation + +multiSigScript : PlutusScript +multiSigScript = 777 , applyScriptWithContext (accSimValidator) + +initEnv : UTxOEnv +initEnv = createEnv 0 + +initTxOut : TxOut +initTxOut = inj₁ (record { net = 0 ; + pay = ScriptObj 777 ; + stake = just (ScriptObj 777) }) + , scriptValue , just (inj₂ (inj₁ (inj₁ (Always [])))) , nothing + +script : TxIn × TxOut +script = (6 , 6) , initTxOut + + + +initState' : UTxO +initState' = fromList' (createInitUtxoState 5 startValue) + +data Tx' : Set where + start : ℕ → Value → Tx' + openn : ℕ → Tx' + close : ℕ → Tx' + withdraw : ℕ → Value → Tx' + deposit : ℕ -> 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/Test/Examples/AccountSim/Validator.agda b/src/Test/Examples/AccountSim/Validator.agda new file mode 100644 index 000000000..28b3e84d6 --- /dev/null +++ b/src/Test/Examples/AccountSim/Validator.agda @@ -0,0 +1,211 @@ +{-# OPTIONS --safe #-} + +-- Validator Simulating Accounts on Cardano based on Agda2hs work + +module Test.Examples.AccountSim.Validator where + +open import Data.Bool.Base renaming (_∧_ to _&&_) hiding (if_then_else_) +open import Data.List using (filter) +open import Data.Maybe renaming (map to maybeMap) + +open import Ledger.Prelude +open import Test.Examples.AccountSim.Datum +open import Test.Prelude AccountSimData +open import Test.SymbolicData AccountSimData + +import Agda.Builtin.Nat as N + +PubKeyHash : Type +PubKeyHash = ℕ + +instance + ShowAccountSimData : Show AccountSimData + ShowAccountSimData = mkShow (λ x → "") + +open import Test.LedgerImplementation SData SData +open import Ledger.Conway.Specification.Transaction using (TransactionStructure) + +open TransactionStructure SVTransactionStructure + +emptyValue : Value +emptyValue = 0 + +feeValue : Value +feeValue = 10000000000 + +startValue : Value +startValue = 1000000000000 + +scriptValue : Value +scriptValue = 30000000000 + +adaValueOf : ℕ -> 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/Test/Examples/DEx/Datum.agda b/src/Test/Examples/DEx/Datum.agda new file mode 100644 index 000000000..5c266fa35 --- /dev/null +++ b/src/Test/Examples/DEx/Datum.agda @@ -0,0 +1,30 @@ +{-# OPTIONS --safe #-} + +open import Ledger.Prelude hiding (fromList; ε); open Computational + +module Test.Examples.DEx.Datum where + +open import Tactic.Derive.DecEq +open import Data.Vec as Vec + hiding (fromList) +import stdlib.Data.Vec.Instances as Vec +import Data.Vec.Relation.Binary.Pointwise.Inductive as Vec + +open import Data.Rational.Base + +data Label : Set where + -- Holding : Label + Always : ℚ -> ℕ -> 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/Test/Examples/DEx/OffChain/Close.agda b/src/Test/Examples/DEx/OffChain/Close.agda new file mode 100644 index 000000000..f541af964 --- /dev/null +++ b/src/Test/Examples/DEx/OffChain/Close.agda @@ -0,0 +1,49 @@ +{-# OPTIONS --safe #-} + +module Test.Examples.DEx.OffChain.Close where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction + +open import Test.Examples.DEx.Datum +open import Test.Examples.DEx.Validator +open import Test.Examples.DEx.OffChain.Lib +open import Test.Prelude DExData +open import Test.SymbolicData DExData +open import Test.LedgerImplementation SData SData +open import Test.AbstractImplementation valContext +open import Test.Lib valContext + +open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions + +open TransactionStructure SVTransactionStructure +open Implementation + +makeCloseTx : (id : ℕ) → UTxOState → PlutusScript → (w : ℕ) → Maybe Tx +makeCloseTx id state script@(sh , _) w = + let + wutxo = getWalletUTxO w (UTxOState.utxo state) + in + maybe (λ { (scIn , (fst , txValue , snd)) → + just ( + record { body = record defaultTxBody + { txIns = Ledger.Prelude.fromList ((scIn ∷ []) ++ (map proj₁ wutxo)) + ; txOuts = fromListIx (makeFeeUnPaymentTxOut wutxo txValue) + ; txId = id + ; collateralInputs = Ledger.Prelude.fromList (map proj₁ wutxo) + ; reqSignerHashes = Ledger.Prelude.fromList (w ∷ []) + } ; + wits = record { vkSigs = fromListᵐ ((w , (_+_ {{addNat}} (getTxId wutxo) w) ) ∷ []) ; + scripts = Ledger.Prelude.fromList ((inj₂ script) ∷ []) ; + txdats = ∅ ; + txrdmrs = fromListᵐ (((Spend , (proj₂ scIn)) , + inj₁ (inj₂ Close) , + ((getTxId wutxo) , w)) ∷ []) } ; + txsize = 10 ; + isValid = true ; + txAD = nothing } + ) + }) + nothing + (getScriptUTxO sh (UTxOState.utxo state)) + diff --git a/src/Test/Examples/DEx/OffChain/Exchange.agda b/src/Test/Examples/DEx/OffChain/Exchange.agda new file mode 100644 index 000000000..a1d1f54c7 --- /dev/null +++ b/src/Test/Examples/DEx/OffChain/Exchange.agda @@ -0,0 +1,63 @@ +{-# OPTIONS --safe #-} + +module Test.Examples.DEx.OffChain.Exchange where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction + +open import Test.Examples.DEx.Datum +open import Test.Examples.DEx.Validator +open import Test.Examples.DEx.OffChain.Lib +open import Test.Prelude DExData +open import Test.SymbolicData DExData +open import Test.LedgerImplementation SData SData +open import Test.AbstractImplementation valContext +open import Test.Lib valContext + +open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions + +open TransactionStructure SVTransactionStructure +open Implementation + +import Data.Rational.Base as Q + +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) + + +makeExchangeTxOut : Label → (scriptIx : ℕ) → TxOut → (w : ℕ) → (v : Value) → List (ℕ × TxOut) +makeExchangeTxOut (Always r o) ix txo w v = + (ix , scriptETxOut (Always r o) txo w v) ∷ + (2 , ((inj₁ (record { net = 0 ; pay = KeyHashObj o ; stake = just (KeyHashObj o) })) , + (ratioValue v r , nothing , nothing)))∷ [] + + + +makeExchangeTx : (id : ℕ) → UTxOState → PlutusScript → (w : ℕ) → (v : Value) → Maybe Tx +makeExchangeTx id state script@(sh , _) w v = + let + wutxo = getWalletUTxO w (UTxOState.utxo state) + in + maybe (λ { (scIn , scOut) → maybe (λ {(Always r o) → + just ( + record { body = record defaultTxBody + { txIns = Ledger.Prelude.fromList ((scIn ∷ []) ++ (map proj₁ wutxo)) + ; txOuts = fromListIx (makeFeeSwapTxOut wutxo v (ratioValue v r) ++ makeExchangeTxOut (Always r o) (proj₂ scIn) scOut w v ) + ; txId = id + ; collateralInputs = Ledger.Prelude.fromList (map proj₁ wutxo) + ; reqSignerHashes = Ledger.Prelude.fromList (w ∷ []) + } ; + wits = record { vkSigs = fromListᵐ ((w , (_+_ {{addNat}} (getTxId wutxo) w)) ∷ []) ; + scripts = Ledger.Prelude.fromList ((inj₂ script) ∷ []) ; + txdats = ∅ ; + txrdmrs = fromListᵐ (((Spend , (proj₂ scIn)) , + inj₁ (inj₂ (Exchange w v)) , + ((getTxId wutxo) , w)) ∷ []) } ; + txsize = 10 ; + isValid = true ; + txAD = nothing } + )}) + nothing + (getLabel scOut)}) + nothing + (getScriptUTxO sh (UTxOState.utxo state)) diff --git a/src/Test/Examples/DEx/OffChain/Lib.agda b/src/Test/Examples/DEx/OffChain/Lib.agda new file mode 100644 index 000000000..646453b99 --- /dev/null +++ b/src/Test/Examples/DEx/OffChain/Lib.agda @@ -0,0 +1,111 @@ +{-# OPTIONS --safe #-} + +module Test.Examples.DEx.OffChain.Lib where + +open import Data.List using (filter) + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction using (TransactionStructure) + +open import Test.Examples.DEx.Datum +open import Test.Examples.DEx.Validator +open import Test.Prelude DExData +open import Test.SymbolicData DExData +open import Test.LedgerImplementation SData SData + +open TransactionStructure SVTransactionStructure + +defaultTxBody : TxBody +defaultTxBody = record + { txIns = ∅ + ; refInputs = ∅ + ; collateralInputs = ∅ + ; txOuts = ∅ + ; txFee = 10000000000 + ; mint = 0 + ; txVldt = nothing , nothing + ; txCerts = [] + ; txWithdrawals = ∅ + ; txGovVotes = [] + ; txGovProposals = [] + ; txDonation = 0 + ; txADhash = nothing + ; txNetworkId = just 0 + ; currentTreasury = nothing + ; txId = 0 + ; reqSignerHashes = ∅ + ; scriptIntegrityHash = nothing + } + +matchScriptAddress : (scriptHash : ℕ) → Credential → Set +matchScriptAddress sh (KeyHashObj x) = ⊥ +matchScriptAddress sh (ScriptObj y) = True (sh ≟ y) + +matchScriptAddress? : (sh : ℕ) → (c : Credential) → Dec (matchScriptAddress sh c) +matchScriptAddress? sh (KeyHashObj x) = no (λ x₁ → x₁) +matchScriptAddress? sh (ScriptObj y) = T? ⌊ (sh ≟ y) ⌋ + +getScriptUTxO : (scriptHash : ℕ) → UTxO → Maybe (TxIn × TxOut) +getScriptUTxO sh (utxo , prf) = head $ filter (λ { (_ , addr , _) → matchScriptAddress? sh (payCred addr)}) (setToList utxo) + +matchWalletHash : (keyHash : ℕ) → Credential → Set +matchWalletHash kh (KeyHashObj x) = True (kh ≟ x) +matchWalletHash kh (ScriptObj y) = ⊥ + +matchWalletHash? : (sh : ℕ) → (c : Credential) → Dec (matchWalletHash sh c) +matchWalletHash? kh (KeyHashObj x) = T? ⌊ (kh ≟ x) ⌋ +matchWalletHash? kh (ScriptObj y) = no (λ x₁ → x₁) + +getWalletUTxO : (scriptHash : ℕ) → UTxO → List (TxIn × TxOut) +getWalletUTxO sh (utxo , prf) = filter (λ { (_ , addr , _) → matchWalletHash? sh (payCred addr)}) (setToList utxo) + +{- +succeedTxOut' : TxOut +succeedTxOut' = inj₁ (record { net = 0 ; + pay = ScriptObj 777 ; + stake = just (ScriptObj 777) }) + , {!!} , just (inj₁ (inj₁ (inj₁ (Always [])))) , nothing +-- 700000000000 -} + +getLabel : TxOut → Maybe Label +getLabel (fst , fst₁ , just (inj₁ (inj₁ (inj₁ x))) , snd) = just x +getLabel (fst , fst₁ , just (inj₁ (inj₁ (inj₂ y))) , snd) = nothing +getLabel (fst , fst₁ , just (inj₁ (inj₂ y)) , snd) = nothing +getLabel (fst , fst₁ , just (inj₂ y) , snd) = nothing +getLabel (fst , fst₁ , nothing , snd) = nothing + + + +-- Assumes a list of filtered waller txins and subtracts a default fee from the head of the list +makeFeeTxOut : List (TxIn × TxOut) → List (ℕ × TxOut) +makeFeeTxOut [] = [] +makeFeeTxOut ((txin , (fst , txValue , snd)) ∷ utxos) = (proj₂ txin , fst , txValue - feeValue , snd) ∷ [] +--10000000000 + +makeFeeUnPaymentTxOut : List (TxIn × TxOut) → Value → List (ℕ × TxOut) +makeFeeUnPaymentTxOut [] v = [] +makeFeeUnPaymentTxOut ((txin , (fst , txValue , snd)) ∷ utxos) v = (proj₂ txin , fst , _+_ {{addValue}} (txValue - feeValue) v , snd) ∷ [] +-- 10000000000 + +makeFeePaymentTxOut : List (TxIn × TxOut) → Value → List (ℕ × TxOut) +makeFeePaymentTxOut [] v = [] +makeFeePaymentTxOut ((txin , (fst , txValue , snd)) ∷ utxos) v = (proj₂ txin , fst , (txValue - feeValue ) - v , snd) ∷ [] +--10000000000 + +makeFeeSwapTxOut : List (TxIn × TxOut) → Value → Value → List (ℕ × TxOut) +makeFeeSwapTxOut [] v1 v2 = [] +makeFeeSwapTxOut ((txin , (fst , txValue , snd)) ∷ utxos) refund new = (proj₂ txin , fst , _+_ {{addValue}} ((txValue - feeValue ) - new) refund , snd) ∷ [] + +-- return id of 0 if no txins +getTxId : List (TxIn × TxOut) → ℕ +getTxId xs = maybe (λ x → proj₁ (proj₁ x)) 0 (head xs) + +{- +getVal : Label -> ℕ -> Value +getVal (Always l) w with lookup' w l +...| nothing = emptyValue +...| just v = v +-} + + + diff --git a/src/Test/Examples/DEx/OffChain/OffChain.agda b/src/Test/Examples/DEx/OffChain/OffChain.agda new file mode 100644 index 000000000..b49a20296 --- /dev/null +++ b/src/Test/Examples/DEx/OffChain/OffChain.agda @@ -0,0 +1,8 @@ +{-# OPTIONS --safe #-} + +module Test.Examples.DEx.OffChain.OffChain where + +open import Test.Examples.DEx.OffChain.Start public +open import Test.Examples.DEx.OffChain.Close public +open import Test.Examples.DEx.OffChain.Update public +open import Test.Examples.DEx.OffChain.Exchange public diff --git a/src/Test/Examples/DEx/OffChain/Start.agda b/src/Test/Examples/DEx/OffChain/Start.agda new file mode 100644 index 000000000..e04cbd9a1 --- /dev/null +++ b/src/Test/Examples/DEx/OffChain/Start.agda @@ -0,0 +1,48 @@ +{-# OPTIONS --safe #-} + +module Test.Examples.DEx.OffChain.Start where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction using (TransactionStructure) + +open import Test.Examples.DEx.Datum +open import Test.Examples.DEx.OffChain.Lib +open import Test.Examples.DEx.Validator +open import Test.Prelude DExData +open import Test.SymbolicData DExData +open import Test.LedgerImplementation SData SData +open import Test.Lib valContext + +open TransactionStructure SVTransactionStructure +open Implementation + +import Data.Rational.Base as Q + +startTxOut : Value → Q.ℚ → ℕ → PlutusScript → TxOut +startTxOut v r o script = inj₁ (record { net = 0 ; + pay = ScriptObj (proj₁ script) ; + stake = just (ScriptObj (proj₁ script)) }) + , v + , just (inj₁ (inj₁ (inj₁ (Always r o)))) , nothing + + +startTx : (id w tw : ℕ) → (v : Value) → Q.ℚ → PlutusScript → Tx +startTx id w tw v r script = record { body = record defaultTxBody + { txIns = Ledger.Prelude.fromList ((w , w) ∷ []) + ; txOuts = fromListIx ((tw , startTxOut v r w script) + ∷ (w + , ((inj₁ (record { net = 0 ; + pay = KeyHashObj w ; + stake = just (KeyHashObj w) })) + , ((startValue - feeValue) - v) , nothing , nothing)) + ∷ []) + ; txId = id + ; collateralInputs = Ledger.Prelude.fromList ((w , w) ∷ []) + } ; + wits = record { vkSigs = fromListᵐ ((w , (_+_ {{addNat}} w id)) ∷ []) ; + scripts = ∅ ; + txdats = ∅ ; + txrdmrs = ∅ } ; + txsize = 10 ; + isValid = true ; + txAD = nothing } diff --git a/src/Test/Examples/DEx/OffChain/Update.agda b/src/Test/Examples/DEx/OffChain/Update.agda new file mode 100644 index 000000000..5330ed17c --- /dev/null +++ b/src/Test/Examples/DEx/OffChain/Update.agda @@ -0,0 +1,58 @@ +{-# OPTIONS --safe #-} + +module Test.Examples.DEx.OffChain.Update where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction + +open import Test.Examples.DEx.Datum +open import Test.Examples.DEx.Validator +open import Test.Examples.DEx.OffChain.Lib +open import Test.Prelude DExData +open import Test.SymbolicData DExData +open import Test.LedgerImplementation SData SData +open import Test.AbstractImplementation valContext +open import Test.Lib valContext + +open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions + +open TransactionStructure SVTransactionStructure +open Implementation + +import Data.Rational.Base as Q + + + +makeUpdateTxOut : Label → (scriptIx w : ℕ) → Value → Q.ℚ → TxOut → List (ℕ × TxOut) +makeUpdateTxOut (Always q o) ix w v r (fst , txValue , snd) = + (ix , (fst , v , just (inj₁ (inj₁ (inj₁ (Always r o)))) , nothing)) ∷ [] + +makeUpdateTx : (id : ℕ) → UTxOState → PlutusScript → (w : ℕ) → Value → Q.ℚ → Maybe Tx +makeUpdateTx id state script@(sh , _) w v r = + let + wutxo = getWalletUTxO w (UTxOState.utxo state) + in + maybe (λ { (scIn , (fst , txValue , snd)) → maybe (λ label → + just ( + record { body = record defaultTxBody + { txIns = Ledger.Prelude.fromList ((scIn ∷ []) ++ (map proj₁ wutxo)) + ; txOuts = fromListIx (makeFeeSwapTxOut wutxo txValue v ++ makeUpdateTxOut label (proj₂ scIn) w v r (fst , txValue , snd) ) + ; txId = id + ; collateralInputs = Ledger.Prelude.fromList (map proj₁ wutxo) + ; reqSignerHashes = Ledger.Prelude.fromList (w ∷ []) + } ; + wits = record { vkSigs = fromListᵐ ((w , (_+_ {{addNat}} (getTxId wutxo) w)) ∷ []) ; + scripts = Ledger.Prelude.fromList ((inj₂ script) ∷ []) ; + txdats = ∅ ; + txrdmrs = fromListᵐ (((Spend , (proj₂ scIn)) , + inj₁ (inj₂ (Input.Update v r)) , + ((getTxId wutxo) , w)) ∷ []) } ; + txsize = 10 ; + isValid = true ; + txAD = nothing } + )) + nothing + (getLabel (fst , txValue , snd))}) + nothing + (getScriptUTxO sh (UTxOState.utxo state)) + diff --git a/src/Test/Examples/DEx/Test/Trace.agda b/src/Test/Examples/DEx/Test/Trace.agda new file mode 100644 index 000000000..fa30b807a --- /dev/null +++ b/src/Test/Examples/DEx/Test/Trace.agda @@ -0,0 +1,140 @@ +{-# OPTIONS --safe #-} + +module 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 Test.Examples.DEx.Datum +open import Test.Examples.DEx.Validator +open import Test.Prelude DExData +open import Test.SymbolicData DExData +open import Test.LedgerImplementation SData SData +open import Test.AbstractImplementation valContext +open import Test.Lib valContext +open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions +open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions +open import Ledger.Conway.Specification.Utxo.Properties.Computational SVTransactionStructure SVAbstractFunctions +open import Ledger.Conway.Specification.Utxow.Properties.Computational SVTransactionStructure SVAbstractFunctions + + +open import Test.Examples.DEx.OffChain.OffChain + +open TransactionStructure SVTransactionStructure +open Implementation + + +par : Params +par = record { sellC = 0 ; buyC = 0 } + +multiSigScript : PlutusScript +multiSigScript = 777 , applyScriptWithContext (dexValidator par) + +initEnv : UTxOEnv +initEnv = createEnv 0 + + +initState' : UTxO +initState' = fromList' (createInitUtxoState 5 startValue) + + +data Tx' : Set where + start : ℕ → Value → Q.ℚ → Tx' + close : ℕ → Tx' + updatetx : ℕ → Value → Q.ℚ → Tx' + exchange : ℕ → Value → Tx' + + +makeTx : UTxOState → PlutusScript → Tx' → (id : ℕ) → Maybe Tx +makeTx s script (start w v r) id = just (startTx id w 999 v r script) +makeTx s script (close w) id = makeCloseTx id s script w +makeTx s script (updatetx w v r) id = makeUpdateTx id s script w v r +makeTx s script (exchange w v) id = makeExchangeTx id s script w v + +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) + +pf : ∀ {d} -> (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) + ∷ [] + + + +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/Test/Examples/DEx/Validator.agda b/src/Test/Examples/DEx/Validator.agda new file mode 100644 index 000000000..ce5915d9a --- /dev/null +++ b/src/Test/Examples/DEx/Validator.agda @@ -0,0 +1,182 @@ +{-# OPTIONS --safe #-} + +-- Validator for the MultiSig contract from the EUTxO paper adapted from Agda2hs version + +module 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_) + +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 Test.Examples.DEx.Datum +open import Test.Prelude DExData +open import Test.SymbolicData DExData + +PubKeyHash : Type +PubKeyHash = ℕ + +--TODO: Implement show properly +instance + ShowAccountSimData : Show DExData + ShowAccountSimData = mkShow (λ x → "") + +open import Test.LedgerImplementation SData SData + +open TransactionStructure SVTransactionStructure + +emptyValue : Value +emptyValue = 0 + +feeValue : Value +feeValue = 10000000000 + +startValue : Value +startValue = 1000000000000 + +scriptValue : Value +scriptValue = 30000000000 + +minValue : Value +minValue = 3000000 + +adaValueOf : ℕ -> 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/HelloWorld.lagda.md b/src/Test/Examples/HelloWorld.lagda.md similarity index 90% rename from src/Ledger/Conway/Specification/Test/Examples/HelloWorld.lagda.md rename to src/Test/Examples/HelloWorld.lagda.md index 85d23ee6f..de747eb8d 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/HelloWorld.lagda.md +++ b/src/Test/Examples/HelloWorld.lagda.md @@ -1,31 +1,33 @@ --- source_branch: master -source_path: src/Ledger/Conway/Specification/Test/Examples/HelloWorld.lagda.md +source_path: src/Test/Examples/HelloWorld.lagda.md --- ```agda {-# OPTIONS --safe #-} +module Test.Examples.HelloWorld where + open import Ledger.Prelude hiding (fromList; ε); open Computational -open import Ledger.Conway.Specification.Test.Prelude -module Ledger.Conway.Specification.Test.Examples.HelloWorld where +open import Test.LedgerImplementation String String +open import Ledger.Conway.Specification.Script.ScriptPurpose SVTransactionStructure + +open import Ledger.Conway.Specification.Transaction +open TransactionStructure SVTransactionStructure using (Data) -scriptImp : ScriptImplementation String String -scriptImp = record { serialise = id ; - deserialise = λ x → just x ; - toData' = λ x → "dummy" } +valContext : TxInfo → ScriptPurpose → Data +valContext x x₁ = "" -open import Ledger.Conway.Specification.Test.LedgerImplementation String String scriptImp -open import Ledger.Conway.Specification.Test.Lib String String scriptImp +open import Test.AbstractImplementation valContext +open import Test.Lib valContext open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions + open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions -open import Ledger.Conway.Specification.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 -- true if redeemer is "Hello World" helloWorld' : Maybe String → Maybe String → Bool @@ -54,7 +56,6 @@ succeedTx : Tx succeedTx = record { body = record { txIns = Ledger.Prelude.fromList ((6 , 6) ∷ (5 , 5) ∷ []) ; refInputs = ∅ - ; collateralInputs = Ledger.Prelude.fromList ((5 , 5) ∷ []) ; txOuts = fromListIx ((6 , initTxOut) ∷ (5 , ((inj₁ (record { net = 0 ; @@ -74,6 +75,7 @@ succeedTx = record { body = record ; txNetworkId = just 0 ; currentTreasury = nothing ; txId = 7 + ; collateralInputs = Ledger.Prelude.fromList ((5 , 5) ∷ []) ; reqSignerHashes = ∅ ; scriptIntegrityHash = nothing } ; @@ -91,7 +93,6 @@ failTx : Tx failTx = record { body = record { txIns = Ledger.Prelude.fromList ((6 , 6) ∷ []) ; refInputs = ∅ - ; collateralInputs = ∅ ; txOuts = ∅ ; txFee = 10 ; mint = 0 @@ -105,6 +106,7 @@ failTx = record { body = record ; txNetworkId = just 0 ; currentTreasury = nothing ; txId = 7 + ; collateralInputs = ∅ ; reqSignerHashes = ∅ ; scriptIntegrityHash = nothing } ; diff --git a/src/Test/Examples/MultiSig/Datum.agda b/src/Test/Examples/MultiSig/Datum.agda new file mode 100644 index 000000000..662a57487 --- /dev/null +++ b/src/Test/Examples/MultiSig/Datum.agda @@ -0,0 +1,27 @@ +{-# OPTIONS --safe #-} + +open import Ledger.Prelude hiding (fromList; ε); open Computational + +module Test.Examples.MultiSig.Datum where + +open import Tactic.Derive.DecEq + +data Label : Set where + Holding : Label + Collecting : ℕ -> ℕ -> ℕ -> 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/Test/Examples/MultiSig/OffChain/AddSig.agda b/src/Test/Examples/MultiSig/OffChain/AddSig.agda new file mode 100644 index 000000000..5e70b92b4 --- /dev/null +++ b/src/Test/Examples/MultiSig/OffChain/AddSig.agda @@ -0,0 +1,61 @@ +{-# OPTIONS --safe #-} + +module Test.Examples.MultiSig.OffChain.AddSig where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction + +open import Test.Examples.MultiSig.Datum +open import Test.Examples.MultiSig.Validator +open import Test.Examples.MultiSig.OffChain.Lib +open import Test.Prelude MultiSigData +open import Test.SymbolicData MultiSigData +open import Test.LedgerImplementation SData SData +open import Test.AbstractImplementation valContext +open import Test.Lib valContext + +open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions + +open TransactionStructure SVTransactionStructure +open Implementation + +-- TODO: Invesitgate what is going on with vkSigs vs reqSigHash in terms of +-- transaction not failing vkSigs +-- txinfo only gets reqSigHash + +makeAddSigTxOut : Label → (scriptIx w : ℕ) → TxOut → List (ℕ × TxOut) +makeAddSigTxOut Holding ix w txo = [] +makeAddSigTxOut (Collecting vl pkh d sigs) ix w (fst , fst₁ , snd) = + (ix , (fst , fst₁ , just (inj₁ (inj₁ (inj₁ (Collecting vl pkh d (w ∷ sigs))))) , nothing)) ∷ [] + +makeAddSigTx : (id : ℕ) → UTxOState → PlutusScript → (w : ℕ) → Maybe Tx +makeAddSigTx id state script@(sh , _) w = + let + wutxo = getWalletUTxO w (UTxOState.utxo state) + in + maybe (λ { (scIn , scOut) → maybe (λ label → + just ( + record { body = record defaultTxBody + { txIns = Ledger.Prelude.fromList ((scIn ∷ []) ++ (map proj₁ wutxo)) + ; txOuts = fromListIx (makeFeeTxOut wutxo ++ makeAddSigTxOut label (proj₂ scIn) w scOut ) + ; txId = id + ; collateralInputs = Ledger.Prelude.fromList (map proj₁ wutxo) + ; reqSignerHashes = Ledger.Prelude.fromList (w ∷ []) + } ; + wits = record { vkSigs = fromListᵐ ((w , (_+_ {{addValue}} (getTxId wutxo) w)) ∷ []) ; + -- signature now is first number + txId ≡ second number + -- first number is needs to be the id for the script + scripts = Ledger.Prelude.fromList ((inj₂ script) ∷ []) ; + txdats = ∅ ; -- fromListᵐ ((inj₁ (inj₁ Holding) , inj₁ (inj₁ Holding)) ∷ []) ; + txrdmrs = fromListᵐ (((Spend , (proj₂ scIn)) , + inj₁ (inj₂ (Add w)) , + ((getTxId wutxo) , w)) ∷ []) } ; + txsize = 10 ; + isValid = true ; + txAD = nothing } + )) + nothing + (getLabel scOut)}) + nothing + (getScriptUTxO sh (UTxOState.utxo state)) + diff --git a/src/Test/Examples/MultiSig/OffChain/Lib.agda b/src/Test/Examples/MultiSig/OffChain/Lib.agda new file mode 100644 index 000000000..7173ecca8 --- /dev/null +++ b/src/Test/Examples/MultiSig/OffChain/Lib.agda @@ -0,0 +1,84 @@ +{-# OPTIONS --safe #-} + +module Test.Examples.MultiSig.OffChain.Lib where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction using (TransactionStructure) + +open import Test.Examples.MultiSig.Datum +open import Test.Examples.MultiSig.Validator +open import Test.Prelude MultiSigData +open import Test.SymbolicData MultiSigData +open import Test.LedgerImplementation SData SData + +open TransactionStructure SVTransactionStructure +open Implementation +open import Data.List using (filter) +open import Relation.Nullary + +defaultTxBody : TxBody +defaultTxBody = record + { txIns = ∅ + ; refInputs = ∅ + ; collateralInputs = ∅ + ; txOuts = ∅ + ; txFee = 10000000000 + ; mint = 0 + ; txVldt = nothing , nothing + ; txCerts = [] + ; txWithdrawals = ∅ + ; txGovVotes = [] + ; txGovProposals = [] + ; txDonation = 0 + ; txADhash = nothing + ; txNetworkId = just 0 + ; currentTreasury = nothing + ; txId = 0 + ; reqSignerHashes = ∅ + ; scriptIntegrityHash = nothing + } + +matchScriptAddress : (scriptHash : ℕ) → Credential → Set +matchScriptAddress sh (KeyHashObj x) = ⊥ +matchScriptAddress sh (ScriptObj y) = True (sh ≟ y) + +matchScriptAddress? : (sh : ℕ) → (c : Credential) → Dec (matchScriptAddress sh c) +matchScriptAddress? sh (KeyHashObj x) = no (λ x₁ → x₁) +matchScriptAddress? sh (ScriptObj y) = T? ⌊ (sh ≟ y) ⌋ + +getScriptUTxO : (scriptHash : ℕ) → UTxO → Maybe (TxIn × TxOut) +getScriptUTxO sh (utxo , prf) = head $ filter (λ { (_ , addr , _) → matchScriptAddress? sh (payCred addr)}) (setToList utxo) + +matchWalletHash : (keyHash : ℕ) → Credential → Set +matchWalletHash kh (KeyHashObj x) = True (kh ≟ x) +matchWalletHash kh (ScriptObj y) = ⊥ + +matchWalletHash? : (sh : ℕ) → (c : Credential) → Dec (matchWalletHash sh c) +matchWalletHash? kh (KeyHashObj x) = T? ⌊ (kh ≟ x) ⌋ +matchWalletHash? kh (ScriptObj y) = no (λ x₁ → x₁) + +getWalletUTxO : (scriptHash : ℕ) → UTxO → List (TxIn × TxOut) +getWalletUTxO sh (utxo , prf) = filter (λ { (_ , addr , _) → matchWalletHash? sh (payCred addr)}) (setToList utxo) + +succeedTxOut' : TxOut +succeedTxOut' = inj₁ (record { net = 0 ; + pay = ScriptObj 777 ; + stake = just (ScriptObj 777) }) + , 700000000000 , just (inj₁ (inj₁ (inj₁ Holding))) , nothing + +getLabel : TxOut → Maybe Label +getLabel (fst , fst₁ , just (inj₁ (inj₁ (inj₁ x))) , snd) = just x +getLabel (fst , fst₁ , just (inj₁ (inj₁ (inj₂ y))) , snd) = nothing +getLabel (fst , fst₁ , just (inj₁ (inj₂ y)) , snd) = nothing +getLabel (fst , fst₁ , just (inj₂ y) , snd) = nothing +getLabel (fst , fst₁ , nothing , snd) = nothing + +-- Assumes a list of filtered waller txins and subtracts a default fee from the head of the list +makeFeeTxOut : List (TxIn × TxOut) → List (ℕ × TxOut) +makeFeeTxOut [] = [] +makeFeeTxOut ((txin , (fst , txValue , snd)) ∷ utxos) = (proj₂ txin , fst , txValue - 10000000000 , snd) ∷ [] + +-- return id of 0 if no txins +getTxId : List (TxIn × TxOut) → ℕ +getTxId xs = maybe (λ x → proj₁ (proj₁ x)) 0 (head xs) + diff --git a/src/Test/Examples/MultiSig/OffChain/OffChain.agda b/src/Test/Examples/MultiSig/OffChain/OffChain.agda new file mode 100644 index 000000000..8bbca7f62 --- /dev/null +++ b/src/Test/Examples/MultiSig/OffChain/OffChain.agda @@ -0,0 +1,8 @@ +{-# OPTIONS --safe #-} + +module Test.Examples.MultiSig.OffChain.OffChain where + +open import Test.Examples.MultiSig.OffChain.Pay public +open import Test.Examples.MultiSig.OffChain.Propose public +open import Test.Examples.MultiSig.OffChain.Open public +open import Test.Examples.MultiSig.OffChain.AddSig public diff --git a/src/Test/Examples/MultiSig/OffChain/Open.agda b/src/Test/Examples/MultiSig/OffChain/Open.agda new file mode 100644 index 000000000..1285c1d29 --- /dev/null +++ b/src/Test/Examples/MultiSig/OffChain/Open.agda @@ -0,0 +1,53 @@ +{-# OPTIONS --safe #-} + +module Test.Examples.MultiSig.OffChain.Open where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction + +open import Test.Examples.MultiSig.Datum +open import Test.Examples.MultiSig.Validator +open import Test.Examples.MultiSig.OffChain.Lib +open import Test.Prelude MultiSigData +open import Test.SymbolicData MultiSigData +open import Test.LedgerImplementation SData SData +open import Test.Lib valContext + +open TransactionStructure SVTransactionStructure +open Implementation + +openTxOut : Value → PlutusScript → TxOut +openTxOut v script = inj₁ (record { net = 0 ; + pay = ScriptObj (proj₁ script) ; + stake = just (ScriptObj (proj₁ script)) }) + , v + , just (inj₁ (inj₁ (inj₁ Holding))) , nothing + +-- txid, wallet, value at script, script index +openTx : (id w v tw : ℕ) → PlutusScript → Tx +openTx id w v tw script = record { body = record defaultTxBody + { txIns = Ledger.Prelude.fromList ((w , w) ∷ []) + ; txOuts = fromListIx ((tw , openTxOut v script) + ∷ (w + , ((inj₁ (record { net = 0 ; + pay = KeyHashObj w ; + stake = just (KeyHashObj w) })) + -- , 10000000000 , nothing , nothing)) + , ((1000000000000 - 10000000000) - v) , nothing , nothing)) + ∷ []) + ; txId = id + ; collateralInputs = Ledger.Prelude.fromList ((w , w) ∷ []) + } ; + wits = record { vkSigs = fromListᵐ ((w , (_+_ {{addValue}} w id)) ∷ []) ; + -- signature now is first number + txId ≡ second number + -- first number is needs to be the id for the script + scripts = ∅ ; -- Ledger.Prelude.fromList ((inj₂ script) ∷ []) ; + txdats = ∅ ; -- fromListᵐ ((inj₁ (inj₁ Holding) , (inj₁ (inj₁ Holding))) ∷ []) ; + txrdmrs = ∅ } ; + {- + ; -- fromListᵐ (((Propose , (proj₁ script)) , + -- inj₁ (inj₂ Pay) , + -- (5 , w)) ∷ []) } ; -} + txsize = 10 ; + isValid = true ; + txAD = nothing } diff --git a/src/Test/Examples/MultiSig/OffChain/Pay.agda b/src/Test/Examples/MultiSig/OffChain/Pay.agda new file mode 100644 index 000000000..1ce5a941c --- /dev/null +++ b/src/Test/Examples/MultiSig/OffChain/Pay.agda @@ -0,0 +1,63 @@ +{-# OPTIONS --safe #-} + +module Test.Examples.MultiSig.OffChain.Pay where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction + +open import Test.Examples.MultiSig.Datum +open import Test.Examples.MultiSig.Validator +open import Test.Examples.MultiSig.OffChain.Lib +open import Test.Prelude MultiSigData +open import Test.SymbolicData MultiSigData +open import Test.LedgerImplementation SData SData +open import Test.AbstractImplementation valContext +open import Test.Lib valContext + +open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions + +open TransactionStructure SVTransactionStructure +open Implementation + +payScriptTxOut : TxOut → (value : ℕ) → TxOut +payScriptTxOut (fst , txValue , snd) v = fst , txValue - v , just (inj₁ (inj₁ (inj₁ Holding))) , nothing + +-- TODO: Throw error here +-- -- (Ix × TxOut) +makePayTxOut : Label → (scriptIx : ℕ) → TxOut → List (ℕ × TxOut) +makePayTxOut Holding ix txo = [] +makePayTxOut (Collecting vl pkh x₂ x₃) ix txo = + (ix , payScriptTxOut txo vl) + ∷ + (777 , ((inj₁ (record { net = 0 ; pay = KeyHashObj pkh ; stake = just (KeyHashObj pkh) })) , + (vl , nothing , nothing))) ∷ [] + +makePayTx : (id : ℕ) → UTxOState → PlutusScript → (w : ℕ) → Maybe Tx +makePayTx id state script@(sh , _) w = + let + wutxo = getWalletUTxO w (UTxOState.utxo state) + in + maybe (λ { (scIn , scOut) → maybe (λ label → + just ( + record { body = record defaultTxBody + { txIns = Ledger.Prelude.fromList ((scIn ∷ []) ++ (map proj₁ wutxo)) + ; txOuts = fromListIx (makeFeeTxOut wutxo ++ makePayTxOut label (proj₂ scIn) scOut) + ; txId = id + ; collateralInputs = Ledger.Prelude.fromList (map proj₁ wutxo) + } ; + wits = record { vkSigs = fromListᵐ ((w , (_+_ {{addValue}} (getTxId wutxo) w)) ∷ []) ; + -- signature now is first number + txId ≡ second number + -- first number is needs to be the id for the script + scripts = Ledger.Prelude.fromList ((inj₂ script) ∷ []) ; + txdats = ∅ ; -- fromListᵐ ((inj₁ (inj₁ Holding) , inj₁ (inj₁ Holding)) ∷ []) ; + txrdmrs = fromListᵐ (((Spend , proj₂ scIn) , + inj₁ (inj₂ Pay) , + ((getTxId wutxo) , w)) ∷ []) } ; + txsize = 10 ; + isValid = true ; + txAD = nothing } + )) + nothing + (getLabel scOut)}) + nothing + (getScriptUTxO sh (UTxOState.utxo state)) diff --git a/src/Test/Examples/MultiSig/OffChain/Propose.agda b/src/Test/Examples/MultiSig/OffChain/Propose.agda new file mode 100644 index 000000000..a8772ab67 --- /dev/null +++ b/src/Test/Examples/MultiSig/OffChain/Propose.agda @@ -0,0 +1,57 @@ +{-# OPTIONS --safe #-} + +module Test.Examples.MultiSig.OffChain.Propose where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction + +open import Test.Examples.MultiSig.Datum +open import Test.Examples.MultiSig.Validator +open import Test.Examples.MultiSig.OffChain.Lib +open import Test.Prelude MultiSigData +open import Test.SymbolicData MultiSigData +open import Test.LedgerImplementation SData SData +open import Test.AbstractImplementation valContext +open import Test.Lib valContext + +open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions + +open TransactionStructure SVTransactionStructure +open Implementation + +-- TODO: Add error handling +makeProposeTxOut : Label → (scriptIx : ℕ) → TxOut → (v tw d : ℕ) → List (ℕ × TxOut) +makeProposeTxOut Holding ix (fst , txValue , snd) v tw d = (ix , (fst , txValue , (just (inj₁ (inj₁ (inj₁ (Collecting v tw d []))))) , nothing)) ∷ [] +makeProposeTxOut _ _ _ _ _ _ = [] + +makeProposeTx : (id : ℕ) → UTxOState → PlutusScript → (w v tw d : ℕ) → Maybe Tx +makeProposeTx id state script@(sh , _) w v tw d = + let + wutxo = getWalletUTxO w (UTxOState.utxo state) + in + maybe (λ { (scIn , scOut) → maybe (λ label → + just ( + record { body = record defaultTxBody + { txIns = Ledger.Prelude.fromList ((scIn ∷ []) ++ (map proj₁ wutxo)) + ; txOuts = fromListIx (makeFeeTxOut wutxo ++ makeProposeTxOut label (proj₂ scIn) scOut v tw d ) + ; txId = id + ; collateralInputs = Ledger.Prelude.fromList (map proj₁ wutxo) + } ; + wits = record { vkSigs = fromListᵐ ((w , (_+_ {{addValue}} (getTxId wutxo) w)) ∷ []) ; + -- signature now is first number + txId ≡ second number + -- first number is needs to be the id for the script + scripts = Ledger.Prelude.fromList ((inj₂ script) ∷ []) ; + txdats = ∅ ; -- fromListᵐ ((inj₁ (inj₁ Holding) , inj₁ (inj₁ Holding)) ∷ []) ; + txrdmrs = fromListᵐ (((Spend , (proj₂ scIn)) , + inj₁ (inj₂ (Propose v -- amount + tw -- wallet pkh + d)) , -- End Slot + ((getTxId wutxo) , w)) ∷ []) } ; + txsize = 10 ; + isValid = true ; + txAD = nothing } + )) + nothing + (getLabel scOut)}) + nothing + (getScriptUTxO sh (UTxOState.utxo state)) diff --git a/src/Test/Examples/MultiSig/Test/Trace.agda b/src/Test/Examples/MultiSig/Test/Trace.agda new file mode 100644 index 000000000..ddbc29d79 --- /dev/null +++ b/src/Test/Examples/MultiSig/Test/Trace.agda @@ -0,0 +1,135 @@ +{-# OPTIONS --safe #-} + +module Test.Examples.MultiSig.Test.Trace where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction using (TransactionStructure) + +open import Test.Examples.MultiSig.Datum +open import Test.Examples.MultiSig.OffChain.OffChain +open import Test.Examples.MultiSig.Validator +open import Test.Prelude MultiSigData +open import Test.SymbolicData MultiSigData +open import Test.LedgerImplementation SData SData +open import Test.AbstractImplementation valContext +open import Test.Lib valContext + +open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions +open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions +open import Ledger.Conway.Specification.Utxo.Properties.Computational SVTransactionStructure SVAbstractFunctions +open import Ledger.Conway.Specification.Utxow.Properties.Computational SVTransactionStructure SVAbstractFunctions + +open TransactionStructure SVTransactionStructure +open Implementation + +impMultiSig : MultiSig +impMultiSig = record { signatories = 3 ∷ 2 ∷ 5 ∷ [] ; minNumSignatures = 2 } + +multiSigScript : PlutusScript +multiSigScript = 777 , applyScriptWithContext (multiSigValidator impMultiSig) + +initEnv : UTxOEnv +initEnv = createEnv 0 + +initTxOut : TxOut +initTxOut = inj₁ (record { net = 0 ; + pay = ScriptObj 777 ; + stake = just (ScriptObj 777) }) + , 800000000000 , just (inj₂ (inj₁ (inj₁ Holding))) , nothing + +script : TxIn × TxOut +script = (6 , 6) , initTxOut + +initState : UTxO +initState = fromList' (script ∷ (createInitUtxoState 5 1000000000000)) + +initState' : UTxO +initState' = fromList' (createInitUtxoState 5 1000000000000) + +-- Hack to have partial Transactions +data Tx' : Set where + openContract : ℕ → ℕ → ℕ → ℕ → Tx' + addSig : ℕ → ℕ → Tx' + pay : ℕ → ℕ → Tx' + propose : ℕ → ℕ → ℕ → ℕ → ℕ → Tx' + +makeTx : UTxOState → PlutusScript → Tx' → Maybe Tx +makeTx s script (openContract id w v tw) = just (openTx id w v tw script) +makeTx s script (addSig id w) = makeAddSigTx id s script w +makeTx s script (pay id w) = makePayTx id s script w +makeTx s script (propose id w v tw d) = makeProposeTx id s script w v tw d + +evalTransanctions : UTxOEnv → ComputationResult String UTxOState → List Tx' → ComputationResult String UTxOState +evalTransanctions env s [] = s +evalTransanctions env state@(failure s) (x ∷ xs) = state +evalTransanctions env (success s) (tx' ∷ txs') = + maybe + (λ tx → evalTransanctions + initEnv + (UTXO-step initEnv s tx) + txs') + (failure "failed to generate tx") + (makeTx s multiSigScript tx') + +evalTransanctionsW : UTxOEnv → ComputationResult String UTxOState → List Tx' → ComputationResult String UTxOState +evalTransanctionsW env s [] = s +evalTransanctionsW env state@(failure s) (x ∷ xs) = state +evalTransanctionsW env (success s) (tx' ∷ txs') = + maybe + (λ tx → evalTransanctions + initEnv + (UTXO-stepW initEnv s tx) + txs') + (failure "failed to generate tx") + (makeTx s multiSigScript tx') + +-- Add Sig trace +addSigTrace : List Tx' +addSigTrace = openContract 6 5 800000000000 6 + ∷ propose 7 5 100000000000 2 4 + ∷ addSig 8 5 + ∷ addSig 9 2 + ∷ pay 10 2 + ∷ [] + +failingTrace : List Tx' +failingTrace = + openContract 6 2 800000000000 5 + ∷ propose 7 1 500000000000 5 13 + ∷ addSig 8 2 + ∷ addSig 9 3 + ∷ pay 10 4 + ∷ propose 11 2 300000000001 5 13 + ∷ [] + +utxowTrace : List Tx' +utxowTrace = openContract 6 5 800000000000 6 + ∷ propose 7 5 100000000000 2 3 + ∷ addSig 8 5 + ∷ addSig 9 2 + ∷ pay 10 5 + ∷ [] + +opaque + unfolding collectP2ScriptsWithContext + unfolding setToList + unfolding Computational-UTXO + unfolding outs + + t0 : ComputationResult String UTxOState + t0 = evalTransanctions initEnv (success ⟦ initState' , 0 , ∅ , 0 ⟧ᵘ) addSigTrace + + _ : isSuccess t0 ≡ true + _ = refl + + t1 : ComputationResult String UTxOState + t1 = evalTransanctions initEnv (success ⟦ initState' , 0 , ∅ , 0 ⟧ᵘ) failingTrace + + _ : isSuccess t1 ≡ false + _ = refl + + t2 : ComputationResult String UTxOState + t2 = evalTransanctionsW initEnv (success ⟦ initState' , 0 , ∅ , 0 ⟧ᵘ) utxowTrace + + _ : isSuccess t2 ≡ true + _ = refl diff --git a/src/Test/Examples/MultiSig/Validator.agda b/src/Test/Examples/MultiSig/Validator.agda new file mode 100644 index 000000000..1c5e0dbfc --- /dev/null +++ b/src/Test/Examples/MultiSig/Validator.agda @@ -0,0 +1,195 @@ +{-# OPTIONS --safe #-} + +module Test.Examples.MultiSig.Validator where + +open import Ledger.Prelude + +open import Test.Examples.MultiSig.Datum +open import Test.Prelude MultiSigData +open import Ledger.Conway.Specification.Transaction +open import Test.SymbolicData MultiSigData + +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 + field + signatories : List PubKeyHash + minNumSignatures : ℕ + +--TODO: Implement show properly +instance + ShowMultiSigData : Show MultiSigData + ShowMultiSigData = mkShow (λ x → "") + +open import Test.LedgerImplementation SData SData +open TransactionStructure SVTransactionStructure +open Implementation + +-- Make this get all output datums +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 + +-- 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/Test/Examples/MultiSigV2/Datum.agda b/src/Test/Examples/MultiSigV2/Datum.agda new file mode 100644 index 000000000..734538a1d --- /dev/null +++ b/src/Test/Examples/MultiSigV2/Datum.agda @@ -0,0 +1,26 @@ +{-# OPTIONS --safe #-} + +open import Ledger.Prelude hiding (fromList; ε); open Computational + +module Test.Examples.MultiSigV2.Datum where + +open import Tactic.Derive.DecEq + +data Label : Set where + Holding : Label + Collecting : ℕ -> ℕ -> ℕ -> 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/Test/Examples/MultiSigV2/OffChain/AddSig.agda b/src/Test/Examples/MultiSigV2/OffChain/AddSig.agda new file mode 100644 index 000000000..eec818bd9 --- /dev/null +++ b/src/Test/Examples/MultiSigV2/OffChain/AddSig.agda @@ -0,0 +1,57 @@ +{-# OPTIONS --safe #-} + +module Test.Examples.MultiSigV2.OffChain.AddSig where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction + +open import Test.Examples.MultiSigV2.Datum +open import Test.Examples.MultiSigV2.OffChain.Lib +open import Test.Examples.MultiSigV2.Validator +open import Test.Prelude MultiSigData +open import Test.SymbolicData MultiSigData +open import Test.LedgerImplementation SData SData +open import Test.AbstractImplementation valContext +open import Test.Lib valContext + +open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions +open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions + +open TransactionStructure SVTransactionStructure +open Implementation + + +makeAddSigTxOut : Label → (scriptIx w : ℕ) → TxOut → List (ℕ × TxOut) +makeAddSigTxOut Holding ix w txo = [] +makeAddSigTxOut (Collecting vl pkh d sigs) ix w (fst , fst₁ , snd) = + (ix , (fst , fst₁ , just (inj₁ (inj₁ (inj₁ (Collecting vl pkh d (insert' w sigs))))) , nothing)) ∷ [] + +makeAddSigTx : (id : ℕ) → UTxOState → PlutusScript → (w : ℕ) → Maybe Tx +makeAddSigTx id state script@(sh , _) w = + let + wutxo = getWalletUTxO w (UTxOState.utxo state) + in + maybe (λ { (scIn , scOut) → maybe (λ label → + just ( + record { body = record defaultTxBody + { txIns = Ledger.Prelude.fromList ((scIn ∷ []) ++ (map proj₁ wutxo)) + ; txOuts = fromListIx (makeFeeTxOut wutxo ++ makeAddSigTxOut label (proj₂ scIn) w scOut ) + ; txId = id + ; collateralInputs = Ledger.Prelude.fromList (map proj₁ wutxo) + ; reqSignerHashes = Ledger.Prelude.fromList (w ∷ []) + } ; + wits = record { vkSigs = fromListᵐ ((w , (_+_ {{addValue}} (getTxId wutxo) w)) ∷ []) ; + scripts = Ledger.Prelude.fromList ((inj₂ script) ∷ []) ; + txdats = ∅ ; + txrdmrs = fromListᵐ (((Spend , (proj₂ scIn)) , + inj₁ (inj₂ (Add w)) , + ((getTxId wutxo) , w)) ∷ []) } ; + txsize = 10 ; + isValid = true ; + txAD = nothing } + )) + nothing + (getLabel scOut)}) + nothing + (getScriptUTxO sh (UTxOState.utxo state)) + diff --git a/src/Test/Examples/MultiSigV2/OffChain/Cancel.agda b/src/Test/Examples/MultiSigV2/OffChain/Cancel.agda new file mode 100644 index 000000000..fa686c155 --- /dev/null +++ b/src/Test/Examples/MultiSigV2/OffChain/Cancel.agda @@ -0,0 +1,57 @@ +{-# OPTIONS --safe #-} + +module Test.Examples.MultiSigV2.OffChain.Cancel where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction + +open import Test.Examples.MultiSigV2.Datum +open import Test.Examples.MultiSigV2.OffChain.Lib +open import Test.Examples.MultiSigV2.Validator +open import Test.Prelude MultiSigData +open import Test.SymbolicData MultiSigData +open import Test.LedgerImplementation SData SData +open import Test.AbstractImplementation valContext +open import Test.Lib valContext + +open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions +open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions + +open TransactionStructure SVTransactionStructure +open Implementation + +makeCancelTxOut : Label → (scriptIx w : ℕ) → TxOut → List (ℕ × TxOut) +makeCancelTxOut Holding ix w txo = [] +makeCancelTxOut (Collecting vl pkh d sigs) ix w (fst , fst₁ , snd) = + (ix , (fst , fst₁ , just (inj₁ (inj₁ (inj₁ Holding))) , nothing)) ∷ [] + +makeCancelTx : (id : ℕ) → UTxOState → PlutusScript → (w : ℕ) → Maybe Tx +makeCancelTx id state script@(sh , _) w = + let + wutxo = getWalletUTxO w (UTxOState.utxo state) + in + maybe (λ { (scIn , scOut) → maybe (λ label → + just ( + record { body = record defaultTxBody + { txIns = Ledger.Prelude.fromList ((scIn ∷ []) ++ (map proj₁ wutxo)) + ; txOuts = fromListIx (makeFeeTxOut wutxo ++ makeCancelTxOut label (proj₂ scIn) w scOut ) + ; txId = id + ; collateralInputs = Ledger.Prelude.fromList (map proj₁ wutxo) + ; reqSignerHashes = Ledger.Prelude.fromList (w ∷ []) + ; txVldt = just 0 , just 11 + } ; + wits = record { vkSigs = fromListᵐ ((w , (_+_ {{addValue}} (getTxId wutxo) w)) ∷ []) ; + scripts = Ledger.Prelude.fromList ((inj₂ script) ∷ []) ; + txdats = ∅ ; + txrdmrs = fromListᵐ (((Spend , (proj₂ scIn)) , + inj₁ (inj₂ Cancel) , + ((getTxId wutxo) , w)) ∷ []) } ; + txsize = 10 ; + isValid = true ; + txAD = nothing } + )) + nothing + (getLabel scOut)}) + nothing + (getScriptUTxO sh (UTxOState.utxo state)) + diff --git a/src/Test/Examples/MultiSigV2/OffChain/Cleanup.agda b/src/Test/Examples/MultiSigV2/OffChain/Cleanup.agda new file mode 100644 index 000000000..66dcc4f35 --- /dev/null +++ b/src/Test/Examples/MultiSigV2/OffChain/Cleanup.agda @@ -0,0 +1,50 @@ +{-# OPTIONS --safe #-} + +module Test.Examples.MultiSigV2.OffChain.Cleanup where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction + +open import Test.Examples.MultiSigV2.Datum +open import Test.Examples.MultiSigV2.OffChain.Lib +open import Test.Examples.MultiSigV2.Validator +open import Test.Prelude MultiSigData +open import Test.SymbolicData MultiSigData +open import Test.LedgerImplementation SData SData +open import Test.AbstractImplementation valContext +open import Test.Lib valContext + +open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions +open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions + +open TransactionStructure SVTransactionStructure +open Implementation + +makeCleanupTx : (id : ℕ) → UTxOState → PlutusScript → (w : ℕ) → Maybe Tx +makeCleanupTx id state script@(sh , _) w = + let + wutxo = getWalletUTxO w (UTxOState.utxo state) + in + maybe (λ { (scIn , (fst , txValue , snd)) → + just ( + record { body = record defaultTxBody + { txIns = Ledger.Prelude.fromList ((scIn ∷ []) ++ (map proj₁ wutxo)) + ; txOuts = fromListIx (makeFeeUnPaymentTxOut wutxo txValue) + ; txId = id + ; collateralInputs = Ledger.Prelude.fromList (map proj₁ wutxo) + ; reqSignerHashes = Ledger.Prelude.fromList (w ∷ []) + } ; + wits = record { vkSigs = fromListᵐ ((w , (_+_ {{addNat}} (getTxId wutxo) w) ) ∷ []) ; + scripts = Ledger.Prelude.fromList ((inj₂ script) ∷ []) ; + txdats = ∅ ; + txrdmrs = fromListᵐ (((Spend , (proj₂ scIn)) , + inj₁ (inj₂ Cleanup) , + ((getTxId wutxo) , w)) ∷ []) } ; + txsize = 10 ; + isValid = true ; + txAD = nothing } + ) + }) + nothing + (getScriptUTxO sh (UTxOState.utxo state)) + diff --git a/src/Test/Examples/MultiSigV2/OffChain/Lib.agda b/src/Test/Examples/MultiSigV2/OffChain/Lib.agda new file mode 100644 index 000000000..d4570d70e --- /dev/null +++ b/src/Test/Examples/MultiSigV2/OffChain/Lib.agda @@ -0,0 +1,97 @@ +{-# OPTIONS --safe #-} + +module Test.Examples.MultiSigV2.OffChain.Lib where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction using (TransactionStructure) + +open import Test.Examples.MultiSigV2.Datum +open import Test.Examples.MultiSigV2.Validator +open import Test.Prelude MultiSigData +open import Test.SymbolicData MultiSigData +open import Test.LedgerImplementation SData SData +open import Test.AbstractImplementation valContext +open import Test.Lib valContext + +open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions +open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions + +open TransactionStructure SVTransactionStructure +open Implementation + +open import Data.List using (filter) + +defaultTxBody : TxBody +defaultTxBody = record + { txIns = ∅ + ; refInputs = ∅ + ; collateralInputs = ∅ + ; txOuts = ∅ + ; txFee = 10000000000 + ; mint = 0 + ; txVldt = nothing , nothing + ; txCerts = [] + ; txWithdrawals = ∅ + ; txGovVotes = [] + ; txGovProposals = [] + ; txDonation = 0 + ; txADhash = nothing + ; txNetworkId = just 0 + ; currentTreasury = nothing + ; txId = 0 + ; reqSignerHashes = ∅ + ; scriptIntegrityHash = nothing + } + +matchScriptAddress : (scriptHash : ℕ) → Credential → Set +matchScriptAddress sh (KeyHashObj x) = ⊥ +matchScriptAddress sh (ScriptObj y) = True (sh ≟ y) + +matchScriptAddress? : (sh : ℕ) → (c : Credential) → Dec (matchScriptAddress sh c) +matchScriptAddress? sh (KeyHashObj x) = no (λ x₁ → x₁) +matchScriptAddress? sh (ScriptObj y) = T? ⌊ (sh ≟ y) ⌋ + +getScriptUTxO : (scriptHash : ℕ) → UTxO → Maybe (TxIn × TxOut) +getScriptUTxO sh (utxo , prf) = head $ filter (λ { (_ , addr , _) → matchScriptAddress? sh (payCred addr)}) (setToList utxo) + +matchWalletHash : (keyHash : ℕ) → Credential → Set +matchWalletHash kh (KeyHashObj x) = True (kh ≟ x) +matchWalletHash kh (ScriptObj y) = ⊥ + +matchWalletHash? : (sh : ℕ) → (c : Credential) → Dec (matchWalletHash sh c) +matchWalletHash? kh (KeyHashObj x) = T? ⌊ (kh ≟ x) ⌋ +matchWalletHash? kh (ScriptObj y) = no (λ x₁ → x₁) + +getWalletUTxO : (scriptHash : ℕ) → UTxO → List (TxIn × TxOut) +getWalletUTxO sh (utxo , prf) = filter (λ { (_ , addr , _) → matchWalletHash? sh (payCred addr)}) (setToList utxo) + +succeedTxOut' : TxOut +succeedTxOut' = inj₁ (record { net = 0 ; + pay = ScriptObj 777 ; + stake = just (ScriptObj 777) }) + , 700000000000 , just (inj₁ (inj₁ (inj₁ Holding))) , nothing + +getLabel : TxOut → Maybe Label +getLabel (fst , fst₁ , just (inj₁ (inj₁ (inj₁ x))) , snd) = just x +getLabel (fst , fst₁ , just (inj₁ (inj₁ (inj₂ y))) , snd) = nothing +getLabel (fst , fst₁ , just (inj₁ (inj₂ y)) , snd) = nothing +getLabel (fst , fst₁ , just (inj₂ y) , snd) = nothing +getLabel (fst , fst₁ , nothing , snd) = nothing + +-- Assumes a list of filtered waller txins and subtracts a default fee from the head of the list +makeFeeTxOut : List (TxIn × TxOut) → List (ℕ × TxOut) +makeFeeTxOut [] = [] +makeFeeTxOut ((txin , (fst , txValue , snd)) ∷ utxos) = (proj₂ txin , fst , txValue - 10000000000 , snd) ∷ [] + +makeFeeUnPaymentTxOut : List (TxIn × TxOut) → Value → List (ℕ × TxOut) +makeFeeUnPaymentTxOut [] v = [] +makeFeeUnPaymentTxOut ((txin , (fst , txValue , snd)) ∷ utxos) v = (proj₂ txin , fst , _+_ {{addValue}} (txValue - feeValue) v , snd) ∷ [] + +makeFeePaymentTxOut : List (TxIn × TxOut) → Value → List (ℕ × TxOut) +makeFeePaymentTxOut [] v = [] +makeFeePaymentTxOut ((txin , (fst , txValue , snd)) ∷ utxos) v = (proj₂ txin , fst , (txValue - feeValue ) - v , snd) ∷ [] + +-- return id of 0 if no txins +getTxId : List (TxIn × TxOut) → ℕ +getTxId xs = maybe (λ x → proj₁ (proj₁ x)) 0 (head xs) + diff --git a/src/Test/Examples/MultiSigV2/OffChain/OffChain.agda b/src/Test/Examples/MultiSigV2/OffChain/OffChain.agda new file mode 100644 index 000000000..6fda49201 --- /dev/null +++ b/src/Test/Examples/MultiSigV2/OffChain/OffChain.agda @@ -0,0 +1,10 @@ +{-# OPTIONS --safe #-} + +module Test.Examples.MultiSigV2.OffChain.OffChain where + +open import Test.Examples.MultiSigV2.OffChain.Pay public +open import Test.Examples.MultiSigV2.OffChain.Propose public +open import Test.Examples.MultiSigV2.OffChain.Open public +open import Test.Examples.MultiSigV2.OffChain.AddSig public +open import Test.Examples.MultiSigV2.OffChain.Cancel public +open import Test.Examples.MultiSigV2.OffChain.Cleanup public diff --git a/src/Test/Examples/MultiSigV2/OffChain/Open.agda b/src/Test/Examples/MultiSigV2/OffChain/Open.agda new file mode 100644 index 000000000..878d87ab3 --- /dev/null +++ b/src/Test/Examples/MultiSigV2/OffChain/Open.agda @@ -0,0 +1,51 @@ +{-# OPTIONS --safe #-} + +module Test.Examples.MultiSigV2.OffChain.Open where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction + +open import Test.Examples.MultiSigV2.Datum +open import Test.Examples.MultiSigV2.OffChain.Lib +open import Test.Examples.MultiSigV2.Validator +open import Test.Prelude MultiSigData +open import Test.SymbolicData MultiSigData +open import Test.LedgerImplementation SData SData +open import Test.AbstractImplementation valContext +open import Test.Lib valContext + +open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions +open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions + +open TransactionStructure SVTransactionStructure +open Implementation + +openTxOut : Value → PlutusScript → TxOut +openTxOut v script = inj₁ (record { net = 0 ; + pay = ScriptObj (proj₁ script) ; + stake = just (ScriptObj (proj₁ script)) }) + , v + , just (inj₁ (inj₁ (inj₁ Holding))) , nothing + +-- txid, wallet, value at script, script index +openTx : (id w v tw : ℕ) → PlutusScript → Tx +openTx id w v tw script = record { body = record defaultTxBody + { txIns = Ledger.Prelude.fromList ((w , w) ∷ []) + ; txOuts = fromListIx ((tw , openTxOut v script) + ∷ (w + , ((inj₁ (record { net = 0 ; + pay = KeyHashObj w ; + stake = just (KeyHashObj w) })) + , ((1000000000000 - 10000000000) - v) , nothing , nothing)) + ∷ []) + ; txId = id + ; collateralInputs = Ledger.Prelude.fromList ((w , w) ∷ []) + } ; + wits = record { vkSigs = fromListᵐ ((w , (_+_ {{addValue}} w id)) ∷ []) ; + scripts = ∅ ; + txdats = ∅ ; + txrdmrs = ∅ } ; + + txsize = 10 ; + isValid = true ; + txAD = nothing } diff --git a/src/Test/Examples/MultiSigV2/OffChain/Pay.agda b/src/Test/Examples/MultiSigV2/OffChain/Pay.agda new file mode 100644 index 000000000..1d4f05ea9 --- /dev/null +++ b/src/Test/Examples/MultiSigV2/OffChain/Pay.agda @@ -0,0 +1,62 @@ +{-# OPTIONS --safe #-} + +module Test.Examples.MultiSigV2.OffChain.Pay where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction + +open import Test.Examples.MultiSigV2.Datum +open import Test.Examples.MultiSigV2.OffChain.Lib +open import Test.Examples.MultiSigV2.Validator +open import Test.Prelude MultiSigData +open import Test.SymbolicData MultiSigData +open import Test.LedgerImplementation SData SData +open import Test.AbstractImplementation valContext +open import Test.Lib valContext + +open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions +open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions + +open TransactionStructure SVTransactionStructure +open Implementation + + +payScriptTxOut : TxOut → (value : ℕ) → TxOut +payScriptTxOut (fst , txValue , snd) v = fst , txValue - v , just (inj₁ (inj₁ (inj₁ Holding))) , nothing + + +makePayTxOut : Label → (scriptIx : ℕ) → TxOut → List (ℕ × TxOut) +makePayTxOut Holding ix txo = [] +makePayTxOut (Collecting vl pkh x₂ x₃) ix txo = + (ix , payScriptTxOut txo vl) + ∷ + (777 , ((inj₁ (record { net = 0 ; pay = KeyHashObj pkh ; stake = just (KeyHashObj pkh) })) , + (vl , nothing , nothing))) ∷ [] + +makePayTx : (id : ℕ) → UTxOState → PlutusScript → (w : ℕ) → Maybe Tx +makePayTx id state script@(sh , _) w = + let + wutxo = getWalletUTxO w (UTxOState.utxo state) + in + maybe (λ { (scIn , scOut) → maybe (λ label → + just ( + record { body = record defaultTxBody + { txIns = Ledger.Prelude.fromList ((scIn ∷ []) ++ (map proj₁ wutxo)) + ; txOuts = fromListIx (makeFeeTxOut wutxo ++ makePayTxOut label (proj₂ scIn) scOut) + ; txId = id + ; collateralInputs = Ledger.Prelude.fromList (map proj₁ wutxo) + } ; + wits = record { vkSigs = fromListᵐ ((w , (_+_ {{addValue}} (getTxId wutxo) w)) ∷ []) ; + scripts = Ledger.Prelude.fromList ((inj₂ script) ∷ []) ; + txdats = ∅ ; + txrdmrs = fromListᵐ (((Spend , proj₂ scIn) , + inj₁ (inj₂ Pay) , + ((getTxId wutxo) , w)) ∷ []) } ; + txsize = 10 ; + isValid = true ; + txAD = nothing } + )) + nothing + (getLabel scOut)}) + nothing + (getScriptUTxO sh (UTxOState.utxo state)) diff --git a/src/Test/Examples/MultiSigV2/OffChain/Propose.agda b/src/Test/Examples/MultiSigV2/OffChain/Propose.agda new file mode 100644 index 000000000..b0da9fd83 --- /dev/null +++ b/src/Test/Examples/MultiSigV2/OffChain/Propose.agda @@ -0,0 +1,58 @@ +{-# OPTIONS --safe #-} + +module Test.Examples.MultiSigV2.OffChain.Propose where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction + +open import Test.Examples.MultiSigV2.Datum +open import Test.Examples.MultiSigV2.OffChain.Lib +open import Test.Examples.MultiSigV2.Validator +open import Test.Prelude MultiSigData +open import Test.SymbolicData MultiSigData +open import Test.LedgerImplementation SData SData +open import Test.AbstractImplementation valContext +open import Test.Lib valContext + +open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions +open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions + +open TransactionStructure SVTransactionStructure +open Implementation + + +-- TODO: Add error handling +makeProposeTxOut : Label → (scriptIx : ℕ) → TxOut → (v tw d : ℕ) → List (ℕ × TxOut) +makeProposeTxOut Holding ix (fst , txValue , snd) v tw d = (ix , (fst , txValue , (just (inj₁ (inj₁ (inj₁ (Collecting v tw d []))))) , nothing)) ∷ [] +makeProposeTxOut _ _ _ _ _ _ = [] + +makeProposeTx : (id : ℕ) → UTxOState → PlutusScript → (w v tw d : ℕ) → Maybe Tx +makeProposeTx id state script@(sh , _) w v tw d = + let + wutxo = getWalletUTxO w (UTxOState.utxo state) + in + maybe (λ { (scIn , scOut) → maybe (λ label → + just ( + record { body = record defaultTxBody + { txIns = Ledger.Prelude.fromList ((scIn ∷ []) ++ (map proj₁ wutxo)) + ; txOuts = fromListIx (makeFeeTxOut wutxo ++ makeProposeTxOut label (proj₂ scIn) scOut v tw d ) + ; txId = id + ; collateralInputs = Ledger.Prelude.fromList (map proj₁ wutxo) + ; txVldt = just 0 , just 10 + } ; + wits = record { vkSigs = fromListᵐ ((w , (_+_ {{addValue}} (getTxId wutxo) w)) ∷ []) ; + scripts = Ledger.Prelude.fromList ((inj₂ script) ∷ []) ; + txdats = ∅ ; + txrdmrs = fromListᵐ (((Spend , (proj₂ scIn)) , + inj₁ (inj₂ (Propose v + tw + d)) , + ((getTxId wutxo) , w)) ∷ []) } ; + txsize = 10 ; + isValid = true ; + txAD = nothing } + )) + nothing + (getLabel scOut)}) + nothing + (getScriptUTxO sh (UTxOState.utxo state)) diff --git a/src/Test/Examples/MultiSigV2/Test/Trace.agda b/src/Test/Examples/MultiSigV2/Test/Trace.agda new file mode 100644 index 000000000..478c792d8 --- /dev/null +++ b/src/Test/Examples/MultiSigV2/Test/Trace.agda @@ -0,0 +1,180 @@ +{-# OPTIONS --safe #-} + +module Test.Examples.MultiSigV2.Test.Trace where + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction + +open import Test.Examples.MultiSigV2.Datum +open import Test.Examples.MultiSigV2.OffChain.Lib +open import Test.Examples.MultiSigV2.Validator +open import Test.Prelude MultiSigData +open import Test.SymbolicData MultiSigData +open import Test.LedgerImplementation SData SData +open import Test.AbstractImplementation valContext +open import Test.Lib valContext + +open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions +open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions +open import Ledger.Conway.Specification.Utxo.Properties.Computational SVTransactionStructure SVAbstractFunctions +open import Ledger.Conway.Specification.Utxow.Properties.Computational SVTransactionStructure SVAbstractFunctions + +open TransactionStructure SVTransactionStructure +open Implementation + + +open import Test.Examples.MultiSigV2.OffChain.OffChain + +impMultiSig : Params +impMultiSig = record { authSigs = 3 ∷ 2 ∷ 5 ∷ [] ; minNumSignatures = 2 ; maxWait = 10 } + +multiSigScript : PlutusScript +multiSigScript = 777 , applyScriptWithContext (multiSigValidator impMultiSig) + +initEnv : UTxOEnv +initEnv = createEnv 0 + +initTxOut : TxOut +initTxOut = inj₁ (record { net = 0 ; + pay = ScriptObj 777 ; + stake = just (ScriptObj 777) }) + , 800000000000 , just (inj₂ (inj₁ (inj₁ Holding))) , nothing + +script : TxIn × TxOut +script = (6 , 6) , initTxOut + +initState : UTxO +initState = fromList' (script ∷ (createInitUtxoState 5 1000000000000)) + +initState' : UTxO +initState' = fromList' (createInitUtxoState 5 1000000000000) + +-- Hack to have partial Transactions +data Tx' : Set where + openContract : ℕ → ℕ → ℕ → ℕ → Tx' + addSig : ℕ → ℕ → Tx' + pay : ℕ → ℕ → Tx' + propose : ℕ → ℕ → ℕ → ℕ → ℕ → Tx' + cancel : ℕ → ℕ → Tx' + cleanup : ℕ → ℕ → Tx' + +makeTx : UTxOState → PlutusScript → Tx' → Maybe Tx +makeTx s script (openContract id w v tw) = just (openTx id w v tw script) +makeTx s script (addSig id w) = makeAddSigTx id s script w +makeTx s script (pay id w) = makePayTx id s script w +makeTx s script (propose id w v tw d) = makeProposeTx id s script w v tw d +makeTx s script (cancel id w) = makeCancelTx id s script w +makeTx s script (cleanup id w) = makeCleanupTx id s script w + +evalTransanctions : UTxOEnv → ComputationResult String UTxOState → List Tx' → ComputationResult String UTxOState +evalTransanctions env s [] = s +evalTransanctions env state@(failure s) (x ∷ xs) = state +evalTransanctions env (success s) (tx' ∷ txs') = + maybe + (λ tx → evalTransanctions + initEnv + (UTXO-step initEnv s tx) + txs') + (failure "failed to generate tx") + (makeTx s multiSigScript tx') + +evalTransanctionsW : UTxOEnv → ComputationResult String UTxOState → List Tx' → ComputationResult String UTxOState +evalTransanctionsW env s [] = s +evalTransanctionsW env state@(failure s) (x ∷ xs) = state +evalTransanctionsW env (success s) (tx' ∷ txs') = + maybe + (λ tx → evalTransanctions + initEnv + (UTXO-stepW initEnv s tx) + txs') + (failure "failed to generate tx") + (makeTx s multiSigScript tx') + +-- Add Sig trace +addSigTrace : List Tx' +addSigTrace = openContract 6 5 800000000000 6 + ∷ propose 7 5 100000000000 2 4 + ∷ addSig 8 5 + ∷ addSig 9 2 + ∷ pay 10 4 + ∷ [] + +failingTrace : List Tx' +failingTrace = + openContract 6 2 800000000000 5 + ∷ propose 7 1 500000000000 5 13 + ∷ addSig 8 2 + ∷ addSig 9 3 + ∷ pay 10 4 + ∷ propose 11 2 300000000001 5 13 + ∷ [] + +utxowTrace : List Tx' +utxowTrace = openContract 6 5 800000000000 6 + ∷ propose 7 5 100000000000 2 3 + ∷ addSig 8 5 + ∷ addSig 9 2 + ∷ pay 10 5 + ∷ [] + +utxowTrace2 : List Tx' +utxowTrace2 = openContract 6 5 800000000000 6 + ∷ propose 7 5 100000000000 2 0 + ∷ addSig 8 5 + ∷ addSig 9 2 + ∷ addSig 10 5 + ∷ addSig 11 2 + ∷ addSig 12 5 + ∷ addSig 13 2 + ∷ addSig 14 5 + ∷ addSig 15 2 + ∷ cancel 16 1 + ∷ [] + + +utxowTrace3 : List Tx' +utxowTrace3 = openContract 6 5 800000000000 6 + ∷ propose 7 5 799999999900 2 5 + ∷ addSig 8 5 + ∷ addSig 9 2 + ∷ pay 10 5 + ∷ cleanup 11 1 + ∷ [] + +opaque + unfolding collectP2ScriptsWithContext + unfolding setToList + unfolding Computational-UTXO + unfolding outs + + t0 : ComputationResult String UTxOState + t0 = evalTransanctions initEnv (success ⟦ initState' , 0 , ∅ , 0 ⟧ᵘ) addSigTrace + + _ : isSuccess t0 ≡ true + _ = refl + + t1 : ComputationResult String UTxOState + t1 = evalTransanctions initEnv (success ⟦ initState' , 0 , ∅ , 0 ⟧ᵘ) failingTrace + + _ : isSuccess t1 ≡ false + _ = refl + + t2 : ComputationResult String UTxOState + t2 = evalTransanctionsW initEnv (success ⟦ initState' , 0 , ∅ , 0 ⟧ᵘ) utxowTrace + + _ : isSuccess t2 ≡ true + _ = refl + + t3 : ComputationResult String UTxOState + t3 = evalTransanctionsW initEnv (success ⟦ initState' , 0 , ∅ , 0 ⟧ᵘ) utxowTrace2 + + _ : isSuccess t3 ≡ true + _ = refl + + t4 : ComputationResult String UTxOState + t4 = evalTransanctionsW initEnv (success ⟦ initState' , 0 , ∅ , 0 ⟧ᵘ) utxowTrace3 + + _ : isSuccess t4 ≡ true + _ = refl + + diff --git a/src/Test/Examples/MultiSigV2/Validator.agda b/src/Test/Examples/MultiSigV2/Validator.agda new file mode 100644 index 000000000..f475402f0 --- /dev/null +++ b/src/Test/Examples/MultiSigV2/Validator.agda @@ -0,0 +1,216 @@ +{-# OPTIONS --safe #-} + +-- Version 2 of MultiSig contract adapted from updated Agda2hs code + +open import Ledger.Prelude hiding (fromList; ε); open Computational +open import Test.Examples.MultiSigV2.Datum +open import Relation.Binary using (REL; Decidable) +open import Level using (Level; _⊔_; suc) +open import Data.Maybe renaming (map to maybeMap) +open import Data.List using (filter) + +open import Data.Bool.Base renaming (_∧_ to _&&_) hiding (if_then_else_) +import Agda.Builtin.Nat as N +open import Test.Prelude MultiSigData + +module Test.Examples.MultiSigV2.Validator where + +PubKeyHash = ℕ + +record Params : Set where + field + authSigs : List PubKeyHash + minNumSignatures : ℕ + maxWait : ℕ +open Params + +open import Test.SymbolicData MultiSigData + + +instance + ShowMultiSigData : Show MultiSigData + ShowMultiSigData = mkShow (λ x → "") + +open import Test.LedgerImplementation SData SData +open import Ledger.Conway.Specification.Transaction using (TransactionStructure) +open TransactionStructure SVTransactionStructure +open import Test.AbstractImplementation valContext +open import Test.Lib valContext +open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions +open import Data.Empty +open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions +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 + +emptyValue : Value +emptyValue = 0 + +feeValue : Value +feeValue = 10000000000 + +startValue : Value +startValue = 1000000000000 + +scriptValue : Value +scriptValue = 30000000000 + +minValue : Value +minValue = 5000000 + +adaValueOf : ℕ -> 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/SucceedIfNumber.lagda.md b/src/Test/Examples/SucceedIfNumber.lagda.md similarity index 92% rename from src/Ledger/Conway/Specification/Test/Examples/SucceedIfNumber.lagda.md rename to src/Test/Examples/SucceedIfNumber.lagda.md index 20a7accc2..40340d5d0 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/SucceedIfNumber.lagda.md +++ b/src/Test/Examples/SucceedIfNumber.lagda.md @@ -1,32 +1,35 @@ --- source_branch: master -source_path: src/Ledger/Conway/Specification/Test/Examples/SucceedIfNumber.lagda.md +source_path: src/Test/Examples/SucceedIfNumber.lagda.md --- ```agda {-# OPTIONS --safe #-} +module 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 Test.LedgerImplementation ℕ ℕ +open import Ledger.Conway.Specification.Script.ScriptPurpose SVTransactionStructure -scriptImp : ScriptImplementation ℕ ℕ -scriptImp = record { serialise = id ; - deserialise = λ x → just x ; - toData' = λ x → 9999999 } +open import Ledger.Conway.Specification.Transaction +open TransactionStructure SVTransactionStructure using (Data) + +valContext : TxInfo → ScriptPurpose → Data +valContext x x₁ = 0 -open import Ledger.Conway.Specification.Test.LedgerImplementation ℕ ℕ scriptImp -open import Ledger.Conway.Specification.Test.Lib ℕ ℕ scriptImp +open import Test.AbstractImplementation valContext +open import Test.Lib valContext open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions + open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions -open import Ledger.Conway.Specification.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 +``` +--> +```agda -- succeed if the datum is 1 succeedIf1Datum' : Maybe ℕ → Maybe ℕ → Bool succeedIf1Datum' (just (suc zero)) _ = true @@ -76,7 +79,6 @@ succeedTx : Tx succeedTx = record { body = record { txIns = Ledger.Prelude.fromList ((6 , 6) ∷ (5 , 5) ∷ []) ; refInputs = ∅ - ; collateralInputs = Ledger.Prelude.fromList ((5 , 5) ∷ []) ; txOuts = fromListIx ((6 , initTxOut) ∷ (5 , ((inj₁ (record { net = 0 ; @@ -84,18 +86,19 @@ succeedTx = record { body = record stake = just (KeyHashObj 5) })) , (1000000000000 - 10000000000) , nothing , nothing)) ∷ []) - ; txId = 7 - ; txCerts = [] ; txFee = 10000000000 - ; txWithdrawals = ∅ + ; mint = 0 ; txVldt = nothing , nothing - ; txADhash = nothing - ; txDonation = 0 + ; txCerts = [] + ; txWithdrawals = ∅ ; txGovVotes = [] ; txGovProposals = [] + ; txDonation = 0 + ; txADhash = nothing ; txNetworkId = just 0 ; currentTreasury = nothing - ; mint = 0 + ; txId = 7 + ; collateralInputs = Ledger.Prelude.fromList ((5 , 5) ∷ []) ; reqSignerHashes = ∅ ; scriptIntegrityHash = nothing } ; @@ -117,20 +120,20 @@ failTx : Tx failTx = record { body = record { txIns = Ledger.Prelude.fromList ((6 , 6) ∷ []) ; refInputs = ∅ - ; collateralInputs = ∅ ; txOuts = ∅ - ; txId = 7 - ; txCerts = [] ; txFee = 10 - ; txWithdrawals = ∅ + ; mint = 0 ; txVldt = nothing , nothing - ; txADhash = nothing - ; txDonation = 0 + ; txCerts = [] + ; txWithdrawals = ∅ ; txGovVotes = [] ; txGovProposals = [] + ; txDonation = 0 + ; txADhash = nothing ; txNetworkId = just 0 ; currentTreasury = nothing - ; mint = 0 + ; txId = 7 + ; collateralInputs = ∅ ; reqSignerHashes = ∅ ; scriptIntegrityHash = nothing } ; @@ -148,7 +151,9 @@ evalScriptRedeemer = evalP2Scripts (collectP2ScriptsWithContext (UTxOEnv.pparams exampleDatum' : Maybe Datum exampleDatum' = getDatum failTx initStateRedeemer (Spend (6 , 6)) - +``` + diff --git a/src/Ledger/Conway/Specification/Test/LedgerImplementation.lagda.md b/src/Test/LedgerImplementation.lagda.md similarity index 72% rename from src/Ledger/Conway/Specification/Test/LedgerImplementation.lagda.md rename to src/Test/LedgerImplementation.lagda.md index ed5c8b11e..bbc6254b7 100644 --- a/src/Ledger/Conway/Specification/Test/LedgerImplementation.lagda.md +++ b/src/Test/LedgerImplementation.lagda.md @@ -1,18 +1,16 @@ --- source_branch: master -source_path: src/Ledger/Conway/Specification/Test/LedgerImplementation.lagda.md +source_path: src/Test/LedgerImplementation.lagda.md --- + +```agda module Implementation where Network = ℕ SlotsPerEpochᶜ = 100 - ActiveSlotCoeff = ℤ.1ℤ ℚ./ 20 + ActiveSlotCoeff = ℤ.1ℤ ℚ./ 20 StabilityWindowᶜ = 10 - RandomnessStabilisationWindowᶜ = 10 - MaxLovelaceSupplyᶜ = 1 + RandomnessStabilisationWindowᶜ = 2 + MaxLovelaceSupplyᶜ = 1000000000000000000 Quorum = 1 NetworkId = 0 @@ -57,9 +57,7 @@ module Implementation where sign = _+_ Data = D - Dataʰ = mkHashableSet Data - toData : ∀ {A : Type} → A → D - toData = toData' -- fix this + Dataʰ = mkHashableSet D PlutusScript = ℕ × (List Data → Bool) ScriptHash = ℕ @@ -86,13 +84,12 @@ module Implementation where where open import Ledger.Conway.Specification.TokenAlgebra.Coin ScriptHash using (Coin-TokenAlgebra) - SVGlobalConstants = GlobalConstants ∋ record {Implementation} SVEpochStructure = EpochStructure ∋ ℕEpochStructure SVGlobalConstants instance _ = SVEpochStructure -SVCryptoStructure : CryptoStructure -SVCryptoStructure = record +SVCrypto : CryptoStructure +SVCrypto = record { Implementation ; pkk = SVPKKScheme } @@ -101,16 +98,20 @@ SVCryptoStructure = record SVPKKScheme : PKKScheme SVPKKScheme = record { Implementation - ; isSigned = λ a b m → ⊤ - ; sign = λ _ _ → zero - ; isSigned-correct = λ where (sk , sk , refl) _ _ h → tt + ; isSigned = λ a b m → a + b ≡ m + ; sign = _+_ + ; isSigned-correct = λ where (sk , sk , refl) _ _ h → h } - -instance _ = SVCryptoStructure +``` + +```agda SVScriptStructure : ScriptStructure SVScriptStructure = record { p1s = P1ScriptStructure-HTL @@ -132,11 +133,15 @@ SVScriptStructure = record { Implementation ; validPlutusScript = λ _ _ _ _ → ⊤ } - +``` + +```agda SVGovParams : GovParams SVGovParams = record { Implementation @@ -152,7 +157,7 @@ SVGovStructure = record { Implementation ; epochStructure = SVEpochStructure ; govParams = SVGovParams - ; cryptoStructure = SVCryptoStructure + ; cryptoStructure = SVCrypto ; globalConstants = SVGlobalConstants } instance _ = SVGovStructure @@ -166,36 +171,23 @@ SVTransactionStructure = record ; epochStructure = SVEpochStructure ; globalConstants = SVGlobalConstants ; adHashingScheme = it - ; cryptoStructure = SVCryptoStructure + ; cryptoStructure = SVCrypto ; govParams = SVGovParams ; txidBytes = id ; scriptStructure = SVScriptStructure } +``` + +```agda indexOfTxInImp : TxIn → ℙ TxIn → Maybe Ix indexOfTxInImp x y = lookupᵐ? (fromListᵐ (setToList y)) (proj₁ x) - -SVAbstractFunctions : AbstractFunctions -SVAbstractFunctions = record - { Implementation - ; txscriptfee = λ tt y → 0 - ; serSize = λ v → 0 -- changed to 0 - ; indexOfImp = record - { indexOfDCert = λ _ _ → nothing - ; indexOfRwdAddr = λ _ _ → nothing - ; indexOfTxIn = indexOfTxInImp - ; indexOfPolicyId = λ _ _ → nothing - ; indexOfVote = λ _ _ → nothing - ; indexOfProposal = λ _ _ → nothing - } - ; runPLCScript = λ { x x₁ x₂ x₃ → proj₂ x₁ x₃ } - ; scriptSize = λ _ → 0 - } -instance _ = SVAbstractFunctions ``` diff --git a/src/Ledger/Conway/Specification/Test/Lib.lagda.md b/src/Test/Lib.lagda.md similarity index 83% rename from src/Ledger/Conway/Specification/Test/Lib.lagda.md rename to src/Test/Lib.lagda.md index 0853a1291..01d96abeb 100644 --- a/src/Ledger/Conway/Specification/Test/Lib.lagda.md +++ b/src/Test/Lib.lagda.md @@ -1,30 +1,31 @@ --- source_branch: master -source_path: src/Ledger/Conway/Specification/Test/Lib.lagda.md +source_path: src/Test/Lib.lagda.md --- ```agda {-# OPTIONS --safe #-} -open import Ledger.Prelude hiding (fromList; ε; _/_); open Computational -open import Ledger.Conway.Specification.Test.Prelude +open import Ledger.Prelude hiding (fromList; ε; _/_) +open import Test.LedgerImplementation using (SVTransactionStructure) +import Ledger.Conway.Specification.Script.ScriptPurpose as SP -module Ledger.Conway.Specification.Test.Lib (A D : Type) - (scriptImp : ScriptImplementation A D) (open ScriptImplementation scriptImp) +module Test.Lib + {T D : Set}{{DecEq-Data : DecEq D}}{{Show-Data : Show D}} + (open SP (SVTransactionStructure T D) using (TxInfo; ScriptPurpose)) + (valContext' : TxInfo → ScriptPurpose → D) where -open import Ledger.Conway.Specification.Test.LedgerImplementation A D scriptImp -open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions -open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions -open import Ledger.Conway.Specification.Transaction -open TransactionStructure SVTransactionStructure -open import Ledger.Core.Specification.Epoch +open import Test.AbstractImplementation valContext' +open import Test.LedgerImplementation T D + renaming (SVTransactionStructure to SVTransactionStructure') +open import Ledger.Conway.Specification.Utxo SVTransactionStructure' SVAbstractFunctions +open import Ledger.Conway.Specification.Transaction using (TransactionStructure) +open TransactionStructure SVTransactionStructure' 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 ; @@ -122,5 +123,11 @@ isSuccess : ComputationResult String UTxOState → Bool isSuccess (success x) = true isSuccess (failure x) = false +applyScriptWithContext : (Maybe D → Maybe D → List D → Bool) → List D → Bool +applyScriptWithContext f [] = f nothing nothing [] +applyScriptWithContext f (_ ∷ []) = f nothing nothing [] +applyScriptWithContext f (redeemer ∷ valcontext ∷ []) = f nothing (just redeemer) [] +applyScriptWithContext f (datum ∷ redeemer ∷ valcontext ∷ vs) = f (just datum) (just redeemer) (valcontext ∷ vs) + -- [1] https://github.com/IntersectMBO/cardano-ledger/blob/master/docs/adr/2024-08-14_009-refscripts-fee-change.md ``` diff --git a/src/Test/Prelude.lagda.md b/src/Test/Prelude.lagda.md new file mode 100644 index 000000000..a26521a97 --- /dev/null +++ b/src/Test/Prelude.lagda.md @@ -0,0 +1,99 @@ +--- +source_branch: master +source_path: src/Test/Prelude.lagda.md +--- + + +```agda +SDatum = D +SValue = ℕ -- × Vec ℕ 3 +STxId = ℕ +SIx = ℕ +STxIn = STxId × SIx +SNetwork = ℕ +SSlot = ℕ +SKeyHash = ℕ + +-- SCredential = ℕ ⊎ ℕ +data SCredential : Type where + KeyHashObj : ℕ → SCredential + ScriptObj : ℕ → SCredential +instance + unquoteDecl DecEq-SCredential = derive-DecEq + ((quote SCredential , DecEq-SCredential) ∷ []) + +record SBaseAddr : Set where + field net : SNetwork + pay : SCredential + stake : Maybe SCredential +instance + unquoteDecl DecEq-SBaseAddr = derive-DecEq + ((quote SBaseAddr , DecEq-SBaseAddr) ∷ []) + +record SBootstrapAddr : Set where + field net : SNetwork + pay : SCredential + attrsSize : ℕ +instance + unquoteDecl DecEq-SBootstrapAddr = derive-DecEq + ((quote SBootstrapAddr , DecEq-SBootstrapAddr) ∷ []) + +SAddr = SBaseAddr ⊎ SBootstrapAddr + +-- ScriptHash +STxOut = SAddr × SValue × Maybe (D ⊎ D) -- Assumes hash is identity for datums, dropping Maybe Script for now +SUTxO = List (STxIn × STxOut) + +record SRwdAddr : Set where + field net : SNetwork + stake : SCredential +instance + unquoteDecl DecEq-SRwdAddr = derive-DecEq + ((quote SRwdAddr , DecEq-SRwdAddr) ∷ []) + +data SScriptPurpose : Set where + -- network is tt so we can ignore it here + Rwrd : SRwdAddr → SScriptPurpose + Mint : SValue → SScriptPurpose + Spend : STxIn → SScriptPurpose + Empty : SScriptPurpose +instance + unquoteDecl DecEq-SScriptPurpose = derive-DecEq + ((quote SScriptPurpose , DecEq-SScriptPurpose) ∷ []) + + +record STxInfo : Set where + field realizedInputs : SUTxO + txouts : List (SIx × STxOut) + fee : SValue + mint : SValue + -- not adding txcerts as rarely used + txwdrls : List (SRwdAddr × Coin) + txvldt : Maybe SSlot × Maybe SSlot + vkey : ℙ SKeyHash + txdats : List D -- Hash is id for datums therfore List D can replicate: DataHash ⇀ Datum + txid : STxId +``` + diff --git a/src/Ledger/Conway/Specification/Test/StructuredContracts.lagda.md b/src/Test/StructuredContracts.lagda.md similarity index 96% rename from src/Ledger/Conway/Specification/Test/StructuredContracts.lagda.md rename to src/Test/StructuredContracts.lagda.md index 4eb8abf55..81f968eaf 100644 --- a/src/Ledger/Conway/Specification/Test/StructuredContracts.lagda.md +++ b/src/Test/StructuredContracts.lagda.md @@ -18,12 +18,14 @@ open import Ledger.Conway.Specification.Abstract open import Ledger.Conway.Specification.TokenAlgebra.Base open import Ledger.Conway.Specification.TokenAlgebra.ValueSet -module Ledger.Conway.Specification.Test.StructuredContracts + +module Test.StructuredContracts (txs : _) (open TransactionStructure txs) (abs : AbstractFunctions txs) (open AbstractFunctions abs) where open import Ledger.Conway.Specification.Ledger txs abs +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 ``` diff --git a/src/Test/SymbolicData.agda b/src/Test/SymbolicData.agda new file mode 100644 index 000000000..1c0687862 --- /dev/null +++ b/src/Test/SymbolicData.agda @@ -0,0 +1,84 @@ +{-# OPTIONS --safe #-} + +open import Ledger.Prelude + +module Test.SymbolicData + (SD : Set) {{DecEq-Data : DecEq SD}} {{Show-Data : Show SD}} where + +open import Test.Prelude SD + +ScriptContext : Type +ScriptContext = STxInfo × SScriptPurpose + +SData : Type +SData = SDatum ⊎ ScriptContext + +instance ShowSData : Show SData + ShowSData = mkShow (λ x → "") + +open import Test.LedgerImplementation SData SData +open import Ledger.Conway.Specification.Script.ScriptPurpose SVTransactionStructure + +open import Ledger.Conway.Specification.Transaction using (TransactionStructure) +open TransactionStructure SVTransactionStructure + +open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure + +TxInToSymbolic : TxIn → STxIn +TxInToSymbolic x = x + +credToSymbolic : Credential → SCredential +credToSymbolic (KeyHashObj x) = KeyHashObj x +credToSymbolic (ScriptObj x) = ScriptObj x + +AddrToSymbolic : Addr → SAddr +AddrToSymbolic (inj₁ record { net = net ; pay = pay ; stake = stake }) + = inj₁ (record { net = net ; pay = credToSymbolic pay ; stake = maybe (λ x → just (credToSymbolic x)) nothing stake }) +AddrToSymbolic (inj₂ record { net = net ; pay = pay ; attrsSize = attrsSize }) + = inj₂ (record { net = net ; pay = credToSymbolic pay ; attrsSize = attrsSize }) + +RwdAddrToSymbolic : RwdAddr → SRwdAddr +RwdAddrToSymbolic record { net = net ; stake = stake } = record { net = net ; stake = credToSymbolic stake } + +DatumToSymbolic : Datum → Maybe SDatum +DatumToSymbolic (inj₁ x) = just x +DatumToSymbolic (inj₂ y) = nothing + +DatumPairToSymbolic : Datum ⊎ DataHash → Maybe (SDatum ⊎ SDatum) +DatumPairToSymbolic (inj₁ (inj₁ x)) = just (inj₁ x) +DatumPairToSymbolic (inj₁ (inj₂ y)) = nothing +DatumPairToSymbolic (inj₂ (inj₁ x)) = just (inj₂ x) +DatumPairToSymbolic (inj₂ (inj₂ y)) = nothing + +TxOutToSymbolic : TxOut → STxOut +TxOutToSymbolic (a , v , d , s) = AddrToSymbolic a , v , maybe DatumPairToSymbolic nothing d + +UTxOToSymbolic : UTxO → SUTxO +UTxOToSymbolic x = map (\ x → (proj₁ x , TxOutToSymbolic (proj₂ x))) (setToList (x ˢ)) + +txInfoToSymbolic : TxInfo → STxInfo +txInfoToSymbolic txinfo = + let open TxInfo txinfo + in + record + { realizedInputs = UTxOToSymbolic realizedInputs + ; txouts = map (\ x → (proj₁ x , TxOutToSymbolic (proj₂ x))) (setToList (txOuts ˢ)) + ; fee = fee + ; mint = mint + ; txwdrls = map (\ x → (RwdAddrToSymbolic (proj₁ x) , proj₂ x)) (setToList (txWithdrawals ˢ)) + ; txvldt = txVldt + ; vkey = vkKey + ; txdats = mapMaybe DatumToSymbolic (setToList txdats) + ; txid = txId + } + +ScriptPurposeToSymbolic : ScriptPurpose → SScriptPurpose +ScriptPurposeToSymbolic (Cert x) = Empty +ScriptPurposeToSymbolic (Rwrd x) = Rwrd (RwdAddrToSymbolic x) +ScriptPurposeToSymbolic (Mint x) = Mint x +ScriptPurposeToSymbolic (Spend x) = Spend x +ScriptPurposeToSymbolic (Vote x) = Empty +ScriptPurposeToSymbolic (Propose x) = Empty + +valContext : TxInfo → ScriptPurpose → Data +valContext txinfo sp = inj₂ ((txInfoToSymbolic txinfo) , (ScriptPurposeToSymbolic sp))