diff --git a/.gitignore b/.gitignore index 39aaf721c..194c4f1e0 100644 --- a/.gitignore +++ b/.gitignore @@ -30,6 +30,7 @@ result* ## git-merge conflict resolution artifacts *.agda.orig *.lagda.orig +*.agdai ## Python build-tools/scripts/md/__pycache__/ diff --git a/src/Ledger/Conway/Foreign/HSLedger/ExternalStructures.agda b/src/Ledger/Conway/Foreign/HSLedger/ExternalStructures.agda index 363a46197..e7b6ec3e8 100644 --- a/src/Ledger/Conway/Foreign/HSLedger/ExternalStructures.agda +++ b/src/Ledger/Conway/Foreign/HSLedger/ExternalStructures.agda @@ -127,6 +127,7 @@ instance ; scriptSize = λ where (inj₁ x) → HSTimelock.tlScriptSize x (inj₂ x) → HSPlutusScript.psScriptSize x + ; valContext = λ _ _ → zero } open import Ledger.Core.Specification.Address Network KeyHash ScriptHash using () public diff --git a/src/Ledger/Conway/Specification/Abstract.agda b/src/Ledger/Conway/Specification/Abstract.agda index 5e34c6b5f..904600c2f 100644 --- a/src/Ledger/Conway/Specification/Abstract.agda +++ b/src/Ledger/Conway/Specification/Abstract.agda @@ -7,6 +7,7 @@ module Ledger.Conway.Specification.Abstract (txs : TransactionStructure) where open TransactionStructure txs open import Ledger.Conway.Specification.Certs govStructure +open import Ledger.Conway.Specification.ScriptPurpose txs record indexOf : Type where field @@ -23,3 +24,4 @@ record AbstractFunctions : Type where indexOfImp : indexOf runPLCScript : CostModel → P2Script → ExUnits → List Data → Bool scriptSize : Script → ℕ + valContext : TxInfo → ScriptPurpose → Data diff --git a/src/Ledger/Conway/Specification/Script/Base.agda b/src/Ledger/Conway/Specification/Script/Base.agda index 939f61170..ecda520fb 100644 --- a/src/Ledger/Conway/Specification/Script/Base.agda +++ b/src/Ledger/Conway/Specification/Script/Base.agda @@ -50,7 +50,7 @@ record PlutusStructure : Type₁ where field validPlutusScript : CostModel → List Data → ExUnits → PlutusScript → Type ⦃ Dec-validPlutusScript ⦄ : ∀ {x} → (validPlutusScript x ⁇³) language : PlutusScript → Language - toData : ∀ {A : Type} → A → Data + -- toData : ∀ {A : Type} → A → Data record ScriptStructure : Type₁ where diff --git a/src/Ledger/Conway/Specification/Script/Validation.agda b/src/Ledger/Conway/Specification/Script/Validation.agda index 9666d1cf0..1b1023dcd 100644 --- a/src/Ledger/Conway/Specification/Script/Validation.agda +++ b/src/Ledger/Conway/Specification/Script/Validation.agda @@ -1,7 +1,7 @@ {-# OPTIONS --safe #-} open import Ledger.Conway.Specification.Transaction -open import Ledger.Conway.Specification.Abstract +open import Ledger.Conway.Specification.Abstract using (AbstractFunctions; indexOf) module Ledger.Conway.Specification.Script.Validation (txs : _) (open TransactionStructure txs) @@ -10,14 +10,8 @@ module Ledger.Conway.Specification.Script.Validation open import Ledger.Prelude open import Ledger.Conway.Specification.Certs govStructure - -data ScriptPurpose : Type where - Cert : DCert → ScriptPurpose - Rwrd : RwdAddr → ScriptPurpose - Mint : ScriptHash → ScriptPurpose - Spend : TxIn → ScriptPurpose - Vote : Voter → ScriptPurpose - Propose : GovProposal → ScriptPurpose +open import Ledger.Conway.Specification.Abstract txs +open import Ledger.Conway.Specification.ScriptPurpose txs rdptr : TxBody → ScriptPurpose → Maybe RdmrPtr rdptr txb = λ where @@ -45,18 +39,6 @@ getDatum tx utxo (Spend txin) = m = setToMap (mapˢ < hash , id > (TxWitnesses.txdats (Tx.wits tx))) getDatum tx utxo _ = nothing -record TxInfo : Type where - field realizedInputs : UTxO - txouts : Ix ⇀ TxOut - fee : Value - mint : Value - txcerts : List DCert - txwdrls : Wdrl - txvldt : Maybe Slot × Maybe Slot - vkKey : ℙ KeyHash - txdats : ℙ Datum - txid : TxId - txInfo : Language → PParams → UTxO → Tx @@ -85,8 +67,8 @@ credsNeeded utxo txb open RwdAddr open GovProposal -valContext : TxInfo → ScriptPurpose → Data -valContext txinfo sp = toData (txinfo , sp) +-- valContext : TxInfo → ScriptPurpose → Data +-- valContext txinfo sp = toData (txinfo , sp) txOutToDataHash : TxOut → Maybe DataHash txOutToDataHash (_ , _ , d , _) = d >>= isInj₂ diff --git a/src/Ledger/Conway/Specification/ScriptPurpose.agda b/src/Ledger/Conway/Specification/ScriptPurpose.agda new file mode 100644 index 000000000..29f8a2b2c --- /dev/null +++ b/src/Ledger/Conway/Specification/ScriptPurpose.agda @@ -0,0 +1,29 @@ +{-# OPTIONS --safe #-} + +open import Ledger.Prelude +open import Ledger.Conway.Specification.Transaction + +module Ledger.Conway.Specification.ScriptPurpose (txs : TransactionStructure) where + +open TransactionStructure txs +open import Ledger.Conway.Specification.Certs govStructure + +data ScriptPurpose : Type where + Cert : DCert → ScriptPurpose + Rwrd : RwdAddr → ScriptPurpose + Mint : ScriptHash → ScriptPurpose + Spend : TxIn → ScriptPurpose + Vote : Voter → ScriptPurpose + Propose : GovProposal → ScriptPurpose + +record TxInfo : Type where + field realizedInputs : UTxO + txouts : Ix ⇀ TxOut + fee : Value + mint : Value + txcerts : List DCert + txwdrls : Wdrl + txvldt : Maybe Slot × Maybe Slot + vkKey : ℙ KeyHash + txdats : ℙ Datum + txid : TxId diff --git a/src/Ledger/Conway/Specification/Test/AbstractImplementation.agda b/src/Ledger/Conway/Specification/Test/AbstractImplementation.agda new file mode 100644 index 000000000..a1f642ee3 --- /dev/null +++ b/src/Ledger/Conway/Specification/Test/AbstractImplementation.agda @@ -0,0 +1,36 @@ +{-# OPTIONS --safe #-} + +open import Ledger.Prelude hiding (fromList; ε); open Computational +open import Ledger.Conway.Specification.Test.Prelude +open import Ledger.Conway.Specification.Transaction using (TransactionStructure) +open import Ledger.Conway.Specification.Test.LedgerImplementation using (SVTransactionStructure) +open import Ledger.Conway.Specification.ScriptPurpose using () + +module Ledger.Conway.Specification.Test.AbstractImplementation (T D : Set){{DecEq-Data : DecEq D}}{{Show-Data : Show D}} + (open TransactionStructure (SVTransactionStructure T D)) + (open Ledger.Conway.Specification.ScriptPurpose (SVTransactionStructure T D)) + (valContext' : TxInfo → ScriptPurpose → D) + where + +open import Ledger.Conway.Specification.Test.LedgerImplementation T D renaming (SVTransactionStructure to SVTransactionStructure') +open import Ledger.Conway.Specification.Abstract SVTransactionStructure' + +open Implementation + +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 (sh , script) x₂ x₃ → script x₃ } + ; scriptSize = λ _ → 0 + ; valContext = valContext' + } diff --git a/src/Ledger/Conway/Specification/Test/Examples.agda b/src/Ledger/Conway/Specification/Test/Examples.agda index 836819f27..75d61cac4 100644 --- a/src/Ledger/Conway/Specification/Test/Examples.agda +++ b/src/Ledger/Conway/Specification/Test/Examples.agda @@ -1,5 +1,9 @@ {-# OPTIONS --safe #-} + module Ledger.Conway.Specification.Test.Examples where import Ledger.Conway.Specification.Test.Examples.SucceedIfNumber import Ledger.Conway.Specification.Test.Examples.HelloWorld +import Ledger.Conway.Specification.Test.Examples.MultiSig.Datum +import Ledger.Conway.Specification.Test.Examples.MultiSig.Validator +import Ledger.Conway.Specification.Test.Examples.MultiSig.Test.Trace diff --git a/src/Ledger/Conway/Specification/Test/Examples/HelloWorld.agda b/src/Ledger/Conway/Specification/Test/Examples/HelloWorld.agda index b615036fd..300c0412f 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/HelloWorld.agda +++ b/src/Ledger/Conway/Specification/Test/Examples/HelloWorld.agda @@ -1,18 +1,22 @@ {-# OPTIONS --safe #-} open import Ledger.Prelude hiding (fromList; ε); open Computational -open import Ledger.Conway.Specification.Test.Prelude +open import Ledger.Conway.Specification.Test.Prelude (String) module Ledger.Conway.Specification.Test.Examples.HelloWorld where +open import Ledger.Conway.Specification.Test.LedgerImplementation String String +open import Ledger.Conway.Specification.Transaction using (TransactionStructure) +open TransactionStructure SVTransactionStructure using (Data) +open import Ledger.Conway.Specification.ScriptPurpose SVTransactionStructure -scriptImp : ScriptImplementation String String -scriptImp = record { serialise = id ; - deserialise = λ x → just x ; - toData' = λ x → "dummy" } -open import Ledger.Conway.Specification.Test.LedgerImplementation String String scriptImp -open import Ledger.Conway.Specification.Test.Lib String String scriptImp +valContext : TxInfo → ScriptPurpose → Data +valContext x x₁ = "" + +open import Ledger.Conway.Specification.Test.AbstractImplementation String String valContext +open import Ledger.Conway.Specification.Test.Lib String String valContext open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions +open import Data.Empty open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions open import Ledger.Conway.Specification.Transaction open TransactionStructure SVTransactionStructure @@ -21,6 +25,7 @@ open EpochStructure SVEpochStructure open Implementation open import Ledger.Conway.Specification.Utxo.Properties SVTransactionStructure SVAbstractFunctions + -- true if redeemer is "Hello World" helloWorld' : Maybe String → Maybe String → Bool helloWorld' _ (just s) = ⌊ (s ≟ "Hello World") ⌋ diff --git a/src/Ledger/Conway/Specification/Test/Examples/MultiSig/Datum.agda b/src/Ledger/Conway/Specification/Test/Examples/MultiSig/Datum.agda new file mode 100644 index 000000000..65c10cdb5 --- /dev/null +++ b/src/Ledger/Conway/Specification/Test/Examples/MultiSig/Datum.agda @@ -0,0 +1,27 @@ +{-# OPTIONS --safe #-} + +open import Ledger.Prelude hiding (fromList; ε); open Computational + +module Ledger.Conway.Specification.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/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/AddSig.agda b/src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/AddSig.agda new file mode 100644 index 000000000..5f007f399 --- /dev/null +++ b/src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/AddSig.agda @@ -0,0 +1,65 @@ +{-# OPTIONS --safe #-} + +open import Ledger.Prelude hiding (fromList; ε); open Computational +open import Ledger.Conway.Specification.Test.Examples.MultiSig.Datum +open import Ledger.Conway.Specification.Test.Examples.MultiSig.Validator +open import Ledger.Conway.Specification.Test.Prelude MultiSigData +open import Ledger.Conway.Specification.Test.SymbolicData MultiSigData +open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData +open import Ledger.Conway.Specification.Transaction using (TransactionStructure) +open TransactionStructure SVTransactionStructure +open import Ledger.Conway.Specification.Test.AbstractImplementation SData SData valContext +open import Ledger.Conway.Specification.Test.Lib SData SData valContext +open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions +open import Data.Empty +open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions +open import Ledger.Conway.Specification.Transaction +open import Ledger.Core.Specification.Epoch +open EpochStructure SVEpochStructure +open Implementation +open import Ledger.Conway.Specification.Utxo.Properties SVTransactionStructure SVAbstractFunctions +open import Data.List using (filter) +open import Ledger.Conway.Specification.Test.Examples.MultiSig.OffChain.Lib + +module Ledger.Conway.Specification.Test.Examples.MultiSig.OffChain.AddSig where + +-- 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 + ; collateral = Ledger.Prelude.fromList (map proj₁ wutxo) + ; reqSigHash = 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/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/Lib.agda b/src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/Lib.agda new file mode 100644 index 000000000..e7a8c19cd --- /dev/null +++ b/src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/Lib.agda @@ -0,0 +1,93 @@ +{-# OPTIONS --safe #-} + +open import Ledger.Prelude hiding (fromList; ε); open Computational +open import Ledger.Conway.Specification.Test.Examples.MultiSig.Datum +open import Ledger.Conway.Specification.Test.Examples.MultiSig.Validator +open import Ledger.Conway.Specification.Test.Prelude MultiSigData +open import Ledger.Conway.Specification.Test.SymbolicData MultiSigData +open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData +open import Ledger.Conway.Specification.Transaction using (TransactionStructure) +open TransactionStructure SVTransactionStructure +open import Ledger.Conway.Specification.Test.AbstractImplementation SData SData valContext +open import Ledger.Conway.Specification.Test.Lib SData SData valContext +open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions +open import Data.Empty +open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions +open import Ledger.Conway.Specification.Transaction +open import Ledger.Core.Specification.Epoch +open EpochStructure SVEpochStructure +open Implementation +open import Ledger.Conway.Specification.Utxo.Properties SVTransactionStructure SVAbstractFunctions +open import Data.List using (filter) + +module Ledger.Conway.Specification.Test.Examples.MultiSig.OffChain.Lib where + +open import Relation.Nullary + +defaultTxBody : TxBody +defaultTxBody = record + { txins = ∅ + ; refInputs = ∅ + ; txouts = ∅ + ; txfee = 10000000000 + ; mint = 0 + ; txvldt = nothing , nothing + ; txcerts = [] + ; txwdrls = ∅ + ; txvote = [] + ; txprop = [] + ; txdonation = 0 + ; txup = nothing + ; txADhash = nothing + ; txNetworkId = just 0 + ; curTreasury = nothing + ; txid = 0 + ; collateral = ∅ + ; reqSigHash = ∅ + ; scriptIntHash = 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/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/OffChain.agda b/src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/OffChain.agda new file mode 100644 index 000000000..b5e63108a --- /dev/null +++ b/src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/OffChain.agda @@ -0,0 +1,8 @@ +{-# OPTIONS --safe #-} + +module Ledger.Conway.Specification.Test.Examples.MultiSig.OffChain.OffChain where + +open import Ledger.Conway.Specification.Test.Examples.MultiSig.OffChain.Pay public +open import Ledger.Conway.Specification.Test.Examples.MultiSig.OffChain.Propose public +open import Ledger.Conway.Specification.Test.Examples.MultiSig.OffChain.Open public +open import Ledger.Conway.Specification.Test.Examples.MultiSig.OffChain.AddSig public diff --git a/src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/Open.agda b/src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/Open.agda new file mode 100644 index 000000000..eeca501b6 --- /dev/null +++ b/src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/Open.agda @@ -0,0 +1,61 @@ +{-# OPTIONS --safe #-} + +open import Ledger.Prelude hiding (fromList; ε); open Computational +open import Ledger.Conway.Specification.Test.Examples.MultiSig.Datum +open import Ledger.Conway.Specification.Test.Examples.MultiSig.Validator +open import Ledger.Conway.Specification.Test.Prelude MultiSigData +open import Ledger.Conway.Specification.Test.SymbolicData MultiSigData +open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData +open import Ledger.Conway.Specification.Transaction using (TransactionStructure) +open TransactionStructure SVTransactionStructure +open import Ledger.Conway.Specification.Test.AbstractImplementation SData SData valContext +open import Ledger.Conway.Specification.Test.Lib SData SData valContext +open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions +open import Data.Empty +open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions +open import Ledger.Conway.Specification.Transaction +open import Ledger.Core.Specification.Epoch +open EpochStructure SVEpochStructure +open Implementation +open import Ledger.Conway.Specification.Utxo.Properties SVTransactionStructure SVAbstractFunctions +open import Data.List using (filter) +open import Ledger.Conway.Specification.Test.Examples.MultiSig.OffChain.Lib + +module Ledger.Conway.Specification.Test.Examples.MultiSig.OffChain.Open where + +openTxOut : Value → PlutusScript → TxOut +openTxOut v script = inj₁ (record { net = 0 ; + 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 + ; collateral = 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/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/Pay.agda b/src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/Pay.agda new file mode 100644 index 000000000..bada0d92a --- /dev/null +++ b/src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/Pay.agda @@ -0,0 +1,67 @@ +{-# OPTIONS --safe #-} + +open import Ledger.Prelude hiding (fromList; ε); open Computational +open import Ledger.Conway.Specification.Test.Examples.MultiSig.Datum +open import Ledger.Conway.Specification.Test.Examples.MultiSig.Validator +open import Ledger.Conway.Specification.Test.Prelude MultiSigData +open import Ledger.Conway.Specification.Test.SymbolicData MultiSigData +open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData +open import Ledger.Conway.Specification.Transaction using (TransactionStructure) +open TransactionStructure SVTransactionStructure +open import Ledger.Conway.Specification.Test.AbstractImplementation SData SData valContext +open import Ledger.Conway.Specification.Test.Lib SData SData valContext +open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions +open import Data.Empty +open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions +open import Ledger.Conway.Specification.Transaction +open import Ledger.Core.Specification.Epoch +open EpochStructure SVEpochStructure +open Implementation +open import Ledger.Conway.Specification.Utxo.Properties SVTransactionStructure SVAbstractFunctions +open import Data.List using (filter) +open import Ledger.Conway.Specification.Test.Examples.MultiSig.OffChain.Lib + +module Ledger.Conway.Specification.Test.Examples.MultiSig.OffChain.Pay where + +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) + ∷ + (2 , ((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 + ; collateral = 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/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/Propose.agda b/src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/Propose.agda new file mode 100644 index 000000000..f7dfd0bb1 --- /dev/null +++ b/src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/Propose.agda @@ -0,0 +1,61 @@ +{-# OPTIONS --safe #-} + +open import Ledger.Prelude hiding (fromList; ε); open Computational +open import Ledger.Conway.Specification.Test.Examples.MultiSig.Datum +open import Ledger.Conway.Specification.Test.Examples.MultiSig.Validator +open import Ledger.Conway.Specification.Test.Prelude MultiSigData +open import Ledger.Conway.Specification.Test.SymbolicData MultiSigData +open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData +open import Ledger.Conway.Specification.Transaction using (TransactionStructure) +open TransactionStructure SVTransactionStructure +open import Ledger.Conway.Specification.Test.AbstractImplementation SData SData valContext +open import Ledger.Conway.Specification.Test.Lib SData SData valContext +open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions +open import Data.Empty +open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions +open import Ledger.Conway.Specification.Transaction +open import Ledger.Core.Specification.Epoch +open EpochStructure SVEpochStructure +open Implementation +open import Ledger.Conway.Specification.Utxo.Properties SVTransactionStructure SVAbstractFunctions +open import Data.List using (filter) +open import Ledger.Conway.Specification.Test.Examples.MultiSig.OffChain.Lib + +module Ledger.Conway.Specification.Test.Examples.MultiSig.OffChain.Propose where + +-- 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 + ; collateral = 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/Ledger/Conway/Specification/Test/Examples/MultiSig/Test/Trace.agda b/src/Ledger/Conway/Specification/Test/Examples/MultiSig/Test/Trace.agda new file mode 100644 index 000000000..dfabab88c --- /dev/null +++ b/src/Ledger/Conway/Specification/Test/Examples/MultiSig/Test/Trace.agda @@ -0,0 +1,138 @@ +{-# OPTIONS --safe #-} + +open import Ledger.Prelude hiding (fromList; ε); open Computational +open import Ledger.Conway.Specification.Test.Examples.MultiSig.Datum +open import Ledger.Conway.Specification.Test.Examples.MultiSig.Validator +open import Ledger.Conway.Specification.Test.Prelude MultiSigData +open import Ledger.Conway.Specification.Test.SymbolicData MultiSigData +open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData +open import Ledger.Conway.Specification.Transaction using (TransactionStructure) +open TransactionStructure SVTransactionStructure +open import Ledger.Conway.Specification.Test.AbstractImplementation SData SData valContext +open import Ledger.Conway.Specification.Test.Lib SData SData valContext +open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions +open import Data.Empty +open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions +open import Ledger.Conway.Specification.Transaction +open import Ledger.Core.Specification.Epoch +open EpochStructure SVEpochStructure +open Implementation +open import Ledger.Conway.Specification.Utxo.Properties SVTransactionStructure SVAbstractFunctions +open import Ledger.Conway.Specification.Utxow.Properties SVTransactionStructure SVAbstractFunctions +open import Data.List using (filter) + +module Ledger.Conway.Specification.Test.Examples.MultiSig.Test.Trace where + +open import Ledger.Conway.Specification.Test.Examples.MultiSig.OffChain.OffChain + +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 5 + ∷ [] + +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/Ledger/Conway/Specification/Test/Examples/MultiSig/Validator.agda b/src/Ledger/Conway/Specification/Test/Examples/MultiSig/Validator.agda new file mode 100644 index 000000000..14540cf6c --- /dev/null +++ b/src/Ledger/Conway/Specification/Test/Examples/MultiSig/Validator.agda @@ -0,0 +1,187 @@ +{-# OPTIONS --safe #-} + +open import Ledger.Prelude hiding (fromList; ε); open Computational +open import Ledger.Conway.Specification.Test.Examples.MultiSig.Datum +open import Relation.Binary using (REL; Decidable) +open import Level using (Level; _⊔_; suc) +open import Data.Maybe renaming (map to maybeMap) +open import Data.List using (filter) + +open import Ledger.Conway.Specification.Test.Prelude MultiSigData + +module Ledger.Conway.Specification.Test.Examples.MultiSig.Validator where + +PubKeyHash = ℕ + +record MultiSig : Set where + field + signatories : List PubKeyHash + minNumSignatures : ℕ + +open import Ledger.Conway.Specification.Test.SymbolicData MultiSigData + +--TODO: Implement show properly +instance + ShowMultiSigData : Show MultiSigData + ShowMultiSigData = mkShow (λ x → "") + +open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData +open import Ledger.Conway.Specification.Transaction using (TransactionStructure) +open TransactionStructure SVTransactionStructure +open import Ledger.Conway.Specification.Test.AbstractImplementation SData SData valContext +open import Ledger.Conway.Specification.Test.Lib SData SData valContext +open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions +open import Data.Empty +open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions +open import Ledger.Conway.Specification.Transaction +open import Ledger.Core.Specification.Epoch +open EpochStructure SVEpochStructure +open Implementation +open import Ledger.Conway.Specification.Utxo.Properties SVTransactionStructure SVAbstractFunctions +open import Ledger.Conway.Specification.Utxow.Properties SVTransactionStructure SVAbstractFunctions + +-- 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 + +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) ⌋ + +expired : ℕ -> ScriptContext -> Bool +expired slot (txinfo , _) = maybe (λ deadline → ⌊ slot >? deadline ⌋) + false + (proj₂ (STxInfo.txvldt txinfo)) + +multiSigValidator' : MultiSig → Label → Input → ScriptContext → Bool + +multiSigValidator' param Holding (Propose v pkh slot) ctx = + (oldValue ctx == newValue ctx) ∧ + compareScriptValues _≟_ (oldValue ctx) (newValue ctx) + ∧ compareScriptValues _≥?_ (oldValue ctx) (just v) + ∧ ⌊ v ≥? 0 ⌋ + ∧ (case (newLabel ctx) of λ where + nothing → false + (just Holding) → false + (just (Collecting v' pkh' slot' sigs')) → + (v == v') + ∧ (pkh == pkh') + ∧ (slot == slot') + ∧ (sigs' == []) ) + +multiSigValidator' param Holding _ ctx = false + +multiSigValidator' param (Collecting _ _ _ _) (Propose _ _ _) ctx = false + +multiSigValidator' param (Collecting v pkh slot sigs) (Add sig) ctx = + compareScriptValues _≟_ (oldValue ctx) (newValue ctx) -- should this be equal or _≤_ + ∧ checkSigned sig ctx + ∧ query sig (MultiSig.signatories param) + ∧ (case (newLabel ctx) of λ where + nothing → false + (just Holding) → false + (just (Collecting v' pkh' slot' sigs')) → + (v == v') + ∧ (pkh == pkh') + ∧ (slot == slot') + ∧ (sigs' == sig ∷ sigs)) -- Make this an order agnostic comparison? + +multiSigValidator' param (Collecting v pkh slot sigs) Pay ctx = + ⌊ (length sigs) ≥? MultiSig.minNumSignatures param ⌋ + ∧ (case (newLabel ctx) of λ where + nothing → false + (just Holding) → checkPayment pkh v ctx + ∧ compareScriptValues _≟_ (oldValue ctx) (maybeMap (_+_ {{addValue}} v) (newValue ctx)) + + (just (Collecting _ _ _ _)) → false) + +multiSigValidator' param (Collecting v pkh slot sigs) Cancel ctx = + compareScriptValues _≟_ (oldValue ctx) (newValue ctx) + ∧ (case (newLabel ctx) of λ where + nothing → false + (just Holding) → expired slot ctx + (just (Collecting _ _ _ _)) → false) + + +multiSigValidator : MultiSig → Maybe SData → Maybe SData → List SData → Bool +multiSigValidator m (just (inj₁ (inj₁ x))) (just (inj₁ (inj₂ y))) (inj₂ y₁ ∷ []) = + multiSigValidator' m x y y₁ +multiSigValidator _ _ _ _ = false + + diff --git a/src/Ledger/Conway/Specification/Test/Examples/SucceedIfNumber.agda b/src/Ledger/Conway/Specification/Test/Examples/SucceedIfNumber.agda index 13cbcaa05..4ff42befb 100644 --- a/src/Ledger/Conway/Specification/Test/Examples/SucceedIfNumber.agda +++ b/src/Ledger/Conway/Specification/Test/Examples/SucceedIfNumber.agda @@ -4,14 +4,16 @@ open import Ledger.Prelude hiding (fromList; ε); open Computational open import Ledger.Conway.Specification.Test.Prelude module Ledger.Conway.Specification.Test.Examples.SucceedIfNumber where +open import Ledger.Conway.Specification.Test.LedgerImplementation ℕ ℕ +open import Ledger.Conway.Specification.Transaction using (TransactionStructure) +open TransactionStructure SVTransactionStructure using (Data) +open import Ledger.Conway.Specification.ScriptPurpose SVTransactionStructure -scriptImp : ScriptImplementation ℕ ℕ -scriptImp = record { serialise = id ; - deserialise = λ x → just x ; - toData' = λ x → 9999999 } +valContext : TxInfo → ScriptPurpose → Data +valContext x x₁ = 0 -open import Ledger.Conway.Specification.Test.LedgerImplementation ℕ ℕ scriptImp -open import Ledger.Conway.Specification.Test.Lib ℕ ℕ scriptImp +open import Ledger.Conway.Specification.Test.AbstractImplementation ℕ ℕ valContext +open import Ledger.Conway.Specification.Test.Lib ℕ ℕ valContext open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions open import Ledger.Conway.Specification.Transaction @@ -196,3 +198,4 @@ opaque _ : failExampleU ≡ false _ = refl + diff --git a/src/Ledger/Conway/Specification/Test/LedgerImplementation.agda b/src/Ledger/Conway/Specification/Test/LedgerImplementation.agda index bf775654b..ff603eb3f 100644 --- a/src/Ledger/Conway/Specification/Test/LedgerImplementation.agda +++ b/src/Ledger/Conway/Specification/Test/LedgerImplementation.agda @@ -1,12 +1,9 @@ {-# OPTIONS --safe #-} -open import Ledger.Conway.Specification.Test.Prelude -open import Prelude using (Type) +open import Ledger.Prelude hiding (fromList; ε); open Computational module Ledger.Conway.Specification.Test.LedgerImplementation - (T D : Type) - (scriptImp : ScriptImplementation T D) (open ScriptImplementation scriptImp) - where + (T D : Set) {{DecEq-Data : DecEq D}} {{Show-Data : Show D}} where open import Ledger.Prelude hiding (fromList; ε); open Computational import Data.Integer as ℤ @@ -21,7 +18,7 @@ open import Ledger.Conway.Specification.Transaction open import Ledger.Core.Specification.Epoch open import Ledger.Conway.Specification.Gov.Base -module _ {A : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : Show A ⦄ where instance +module _ {A : Set} ⦃ _ : DecEq A ⦄ ⦃ _ : Show A ⦄ where instance ∀Hashable : Hashable A A ∀Hashable = λ where .hash → id @@ -35,7 +32,7 @@ instance module Implementation where Network = ℕ SlotsPerEpochᶜ = 100 - ActiveSlotCoeff = ℤ.1ℤ ℚ./ 20 + ActiveSlotCoeff = ℤ.1ℤ ℚ./ 20 StabilityWindowᶜ = 10 Quorum = 1 NetworkId = 0 @@ -49,9 +46,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 = ℕ @@ -78,13 +73,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 } @@ -93,15 +87,15 @@ 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 +instance _ = SVCrypto open import Ledger.Conway.Specification.Script it it -open import Ledger.Conway.Conformance.Script it it +open import Ledger.Conway.Conformance.Script it it public using (P1ScriptStructure-HTL) SVScriptStructure : ScriptStructure SVScriptStructure = record @@ -144,7 +138,7 @@ SVGovStructure = record { Implementation ; epochStructure = SVEpochStructure ; govParams = SVGovParams - ; cryptoStructure = SVCryptoStructure + ; cryptoStructure = SVCrypto ; globalConstants = SVGlobalConstants } instance _ = SVGovStructure @@ -158,7 +152,7 @@ SVTransactionStructure = record ; epochStructure = SVEpochStructure ; globalConstants = SVGlobalConstants ; adHashingScheme = it - ; cryptoStructure = SVCryptoStructure + ; cryptoStructure = SVCrypto ; govParams = SVGovParams ; txidBytes = id ; scriptStructure = SVScriptStructure @@ -166,27 +160,9 @@ SVTransactionStructure = record instance _ = SVTransactionStructure open import Ledger.Conway.Specification.Abstract it -open import Ledger.Conway.Specification.Gov it +open import Ledger.Conway.Conformance.Gov it open TransactionStructure it 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.agda b/src/Ledger/Conway/Specification/Test/Lib.agda index 3a5c259c2..2cee8ce98 100644 --- a/src/Ledger/Conway/Specification/Test/Lib.agda +++ b/src/Ledger/Conway/Specification/Test/Lib.agda @@ -1,17 +1,24 @@ {-# OPTIONS --safe #-} -open import Ledger.Prelude hiding (fromList; ε; _/_); open Computational +open import Ledger.Prelude hiding (fromList; ε; _/_); open Computational open import Ledger.Conway.Specification.Test.Prelude +open import Ledger.Conway.Specification.Transaction using (TransactionStructure) +open import Ledger.Conway.Specification.Test.LedgerImplementation using (SVTransactionStructure) +open import Ledger.Conway.Specification.ScriptPurpose using () -module Ledger.Conway.Specification.Test.Lib (A D : Type) - (scriptImp : ScriptImplementation A D) (open ScriptImplementation scriptImp) +module Ledger.Conway.Specification.Test.Lib (T D : Set){{DecEq-Data : DecEq D}}{{Show-Data : Show D}} + -- (open TransactionStructure (SVTransactionStructure T D) using (TxInfo; ScriptPurpose)) + (open Ledger.Conway.Specification.ScriptPurpose (SVTransactionStructure T D) using (TxInfo; ScriptPurpose)) + (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.Test.AbstractImplementation T D valContext' +open import Ledger.Conway.Specification.Test.LedgerImplementation T D + renaming (SVTransactionStructure to SVTransactionStructure') +open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure' SVAbstractFunctions +open import Ledger.Conway.Specification.Utxo SVTransactionStructure' SVAbstractFunctions open import Ledger.Conway.Specification.Transaction -open TransactionStructure SVTransactionStructure +open TransactionStructure SVTransactionStructure' open import Ledger.Core.Specification.Epoch open import Ledger.Prelude.Numeric using (mkUnitInterval; mkℕ⁺) open EpochStructure SVEpochStructure @@ -116,4 +123,10 @@ 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/Ledger/Conway/Specification/Test/Prelude.agda b/src/Ledger/Conway/Specification/Test/Prelude.agda index 7a7eb1ea0..66e0b414f 100644 --- a/src/Ledger/Conway/Specification/Test/Prelude.agda +++ b/src/Ledger/Conway/Specification/Test/Prelude.agda @@ -1,11 +1,86 @@ {-# OPTIONS --safe #-} + open import Ledger.Prelude hiding (fromList; ε); open Computational -module Ledger.Conway.Specification.Test.Prelude where +module Ledger.Conway.Specification.Test.Prelude (D : Set) {{DecEq-Data : DecEq D}} where + +open import Tactic.Derive.DecEq +open import Data.Vec + +-- Only implementing Rwd, Mint and Spend +-- TODO: Implement Cert, Propose and Vote +-- All maps become lists of pairs to ensure decidable equality + +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 +instance + unquoteDecl DecEq-STxInfo = derive-DecEq + ((quote STxInfo , DecEq-STxInfo) ∷ []) -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 +-- open import ScriptVerification.LedgerImplementation SScriptPurpose SScriptPurpose diff --git a/src/Ledger/Conway/Specification/Test/StructuredContracts.lagda b/src/Ledger/Conway/Specification/Test/StructuredContracts.lagda index ac870fb44..092c925ad 100644 --- a/src/Ledger/Conway/Specification/Test/StructuredContracts.lagda +++ b/src/Ledger/Conway/Specification/Test/StructuredContracts.lagda @@ -19,6 +19,7 @@ module Ledger.Conway.Specification.Test.StructuredContracts where open import Ledger.Conway.Specification.Ledger txs abs +open import Ledger.Conway.Specification.ScriptPurpose txs open import Ledger.Conway.Specification.Script.Validation txs abs open import Ledger.Conway.Specification.Utxo txs abs \end{code} diff --git a/src/Ledger/Conway/Specification/Test/SymbolicData.agda b/src/Ledger/Conway/Specification/Test/SymbolicData.agda new file mode 100644 index 000000000..23b80225d --- /dev/null +++ b/src/Ledger/Conway/Specification/Test/SymbolicData.agda @@ -0,0 +1,78 @@ +{-# OPTIONS --safe #-} + +open import Ledger.Prelude hiding (fromList; ε); open Computational + +module Ledger.Conway.Specification.Test.SymbolicData (SD : Set) {{DecEq-Data : DecEq SD}} {{Show-Data : Show SD}} where + +open import Ledger.Conway.Specification.Test.Prelude SD + +ScriptContext = STxInfo × SScriptPurpose +SData = SDatum ⊎ ScriptContext + +instance ShowSData : Show SData + ShowSData = mkShow (λ x → "") + +open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData +open import Ledger.Conway.Specification.Transaction using (TransactionStructure) +open import Ledger.Conway.Specification.ScriptPurpose SVTransactionStructure +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 (txwdrls ˢ)) + ; 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)) diff --git a/src/Ledger/Conway/Specification/Utxow/Properties.agda b/src/Ledger/Conway/Specification/Utxow/Properties.agda index a47de2033..815ef3996 100644 --- a/src/Ledger/Conway/Specification/Utxow/Properties.agda +++ b/src/Ledger/Conway/Specification/Utxow/Properties.agda @@ -54,3 +54,8 @@ instance ... | no ¬p = ⊥-elim $ ¬p ((p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈)) ... | yes _ with computeProof' Γ s tx | completeness' _ _ _ _ h ... | success _ | refl = refl + +open Computational ⦃...⦄ + +UTXO-stepW : UTxOEnv → UTxOState → Tx → ComputationResult String UTxOState +UTXO-stepW = compute ⦃ Computational-UTXOW ⦄