From 210ed31a4c1cac9f118253c1b3d519fe5a42e850 Mon Sep 17 00:00:00 2001 From: Alasdair Hill Date: Wed, 13 Mar 2024 12:24:07 +0000 Subject: [PATCH] Modifying ledger and adding working script examples --- src/Everything.agda | 3 + src/Interface/Hashable.agda | 2 +- src/Ledger/Foreign/HSLedger.agda | 4 +- src/Ledger/Script.lagda | 3 +- src/Ledger/ScriptValidation.agda | 5 +- src/Ledger/Set/HashMap.agda | 7 +- src/Ledger/Utxo.lagda | 12 +- src/MidnightExample/HSLedger.agda | 3 +- src/MidnightExample/Ledger.lagda | 2 - src/ScriptVerification/Examples.agda | 115 +-------- src/ScriptVerification/HelloWorld.agda | 128 ++++++++++ .../LedgerImplementation.agda | 52 ++-- src/ScriptVerification/LedgerTypes.agda | 0 src/ScriptVerification/Lib.agda | 54 +--- src/ScriptVerification/Prelude.agda | 8 +- src/ScriptVerification/SimpleScript.agda | 3 - src/ScriptVerification/SucceedIfNumber.agda | 232 ++++++++++++++++++ 17 files changed, 433 insertions(+), 200 deletions(-) create mode 100644 src/ScriptVerification/HelloWorld.agda delete mode 100644 src/ScriptVerification/LedgerTypes.agda delete mode 100644 src/ScriptVerification/SimpleScript.agda create mode 100644 src/ScriptVerification/SucceedIfNumber.agda diff --git a/src/Everything.agda b/src/Everything.agda index d92b5eb9..41674e02 100644 --- a/src/Everything.agda +++ b/src/Everything.agda @@ -14,3 +14,6 @@ import MidnightExample.HSLedger -- ** not currently used import Tactic.DeriveComp import Foreign.Convertible.DerivingTest + +-- ** Verifying Script Examples +import ScriptVerification.Examples diff --git a/src/Interface/Hashable.agda b/src/Interface/Hashable.agda index ab9ae53e..4d13379a 100644 --- a/src/Interface/Hashable.agda +++ b/src/Interface/Hashable.agda @@ -6,7 +6,7 @@ open import Function.Definitions using (Injective) record Hashable (T THash : Set) : Set where field hash : T → THash - hashInj : Injective _≡_ _≡_ hash + -- hashInj : Injective _≡_ _≡_ hash open Hashable ⦃...⦄ public diff --git a/src/Ledger/Foreign/HSLedger.agda b/src/Ledger/Foreign/HSLedger.agda index fc5f422d..7cc5fe54 100644 --- a/src/Ledger/Foreign/HSLedger.agda +++ b/src/Ledger/Foreign/HSLedger.agda @@ -24,14 +24,14 @@ open import Interface.HasOrder.Instance module _ {A : Set} ⦃ _ : DecEq A ⦄ where instance ∀Hashable : Hashable A A - ∀Hashable = λ where .hash → id; .hashInj refl → refl + ∀Hashable = λ where .hash → id ∀isHashableSet : isHashableSet A ∀isHashableSet = mkIsHashableSet A instance Hashable-⊤ : Hashable ⊤ ℕ - Hashable-⊤ = λ where .hash tt → 0; .hashInj _ → refl + Hashable-⊤ = λ where .hash tt → 0 module Implementation where Network = ⊤ diff --git a/src/Ledger/Script.lagda b/src/Ledger/Script.lagda index 60306c78..dd856006 100644 --- a/src/Ledger/Script.lagda +++ b/src/Ledger/Script.lagda @@ -34,7 +34,7 @@ record PlutusStructure : Set₁ where Language PlutusScript CostModel Prices LangDepView ExUnits : Set ⦃ ExUnit-CommutativeMonoid ⦄ : IsCommutativeMonoid' 0ℓ 0ℓ ExUnits ⦃ Hashable-PlutusScript ⦄ : Hashable PlutusScript ScriptHash - ⦃ DecEq-PlutusScript ⦄ : DecEq PlutusScript + -- ⦃ DecEq-PlutusScript ⦄ : DecEq PlutusScript ⦃ DecEq-CostModel ⦄ : DecEq CostModel ⦃ DecEq-LangDepView ⦄ : DecEq LangDepView @@ -173,6 +173,7 @@ record ScriptStructure : Set₁ where Script = P1Script ⊎ P2Script + open import Data.Empty open import Agda.Builtin.Equality open import Relation.Binary.PropositionalEquality diff --git a/src/Ledger/ScriptValidation.agda b/src/Ledger/ScriptValidation.agda index b34bf1fb..89fb2a6c 100644 --- a/src/Ledger/ScriptValidation.agda +++ b/src/Ledger/ScriptValidation.agda @@ -10,7 +10,6 @@ open import Ledger.Transaction open import Ledger.Abstract open import Ledger.Crypto - module Ledger.ScriptValidation (txs : _) (open TransactionStructure txs) (abs : AbstractFunctions txs) (open AbstractFunctions abs) (open indexOf indexOfImp) @@ -51,7 +50,6 @@ getDatum tx utxo (Spend txin) = let open Tx tx; open TxWitnesses wits in (lookupᵐ? utxo txin) getDatum tx utxo _ = [] - record TxInfo : Set where field realizedInputs : UTxO txouts : Ix ⇀ TxOut @@ -148,7 +146,8 @@ valContext txinfo sp = toData (txinfo , sp) -- need to update costmodels to add the language map in order to check -- (Language ↦ CostModel) ∈ costmdls ↦ (Language ↦ CostModel) -abstract + +opaque collectPhaseTwoScriptInputs' : PParams → Tx → UTxO → (ScriptPurpose × ScriptHash) → Maybe (Script × List Data × ExUnits × CostModel) diff --git a/src/Ledger/Set/HashMap.agda b/src/Ledger/Set/HashMap.agda index b172e118..5e3cf572 100644 --- a/src/Ledger/Set/HashMap.agda +++ b/src/Ledger/Set/HashMap.agda @@ -5,11 +5,16 @@ open import Data.Product.Ext open import Interface.Hashable open import Ledger.Set.Theory -module Ledger.Set.HashMap {A B : Set} ⦃ _ : Hashable A B ⦄ (X : ℙ A) where +module Ledger.Set.HashMap {A B : Set} ⦃ _ : Hashable A B ⦄ ⦃ _ : DecEq B ⦄ (X : ℙ A) where setToHashRel : ℙ (B × A) setToHashRel = mapˡ hash (mapˢ ×-dup X) +setToHashMap : B ⇀ A +setToHashMap = fromListᵐ (setToList setToHashRel) + +{- setToHashMap : B ⇀ A setToHashMap = setToHashRel ᵐ where instance _ = record { isLeftUnique = mapˡ∘map⦅×-dup⦆-uniq {inj = hashInj} } +-} diff --git a/src/Ledger/Utxo.lagda b/src/Ledger/Utxo.lagda index 427bf1ab..ec0a060f 100644 --- a/src/Ledger/Utxo.lagda +++ b/src/Ledger/Utxo.lagda @@ -124,12 +124,14 @@ module _ (let open Tx; open TxBody; open TxWitnesses) where opaque \end{code} \end{NoConway} \begin{code} - minfee : PParams → UTxO → Tx → Coin - minfee pp utxo tx = pp .a * tx .body .txsize + pp .b - + txscriptfee (pp .prices) (totExUnits tx) - + pp .minFeeRefScriptCoinsPerByte - *↓ ∑ˢ[ x ← refScripts tx utxo ] scriptSize x + open import Axiom.Set.Sum + minfee : PParams → UTxO → Tx → Coin + minfee pp utxo tx = + pp .a * tx .body .txsize + pp .b + + txscriptfee (pp .prices) (totExUnits tx) + + pp .minFeeRefScriptCoinsPerByte + *↓ ∑[ x ← (mapValues scriptSize $ setToHashMap (refScripts tx utxo)) ] x \end{code} \begin{code}[hide] module _ where diff --git a/src/MidnightExample/HSLedger.agda b/src/MidnightExample/HSLedger.agda index 197144be..d66d72ed 100644 --- a/src/MidnightExample/HSLedger.agda +++ b/src/MidnightExample/HSLedger.agda @@ -14,11 +14,10 @@ open F using (Hash) private variable A B : Set instance _ : Hashable String Hash - _ = λ where .hash → F.hash; .hashInj → F.hash-inj + _ = λ where .hash → F.hash private Show⇒Hashable : ⦃ Show A ⦄ → Hashable A Hash Show⇒Hashable .hash = hash ∘ show - Show⇒Hashable .hashInj = hash-inj where postulate hash-inj : _ instance Show-List : ⦃ Hashable A Hash ⦄ → Show (List A) Show-List .show = foldr (λ a acc → show (hash a) ++ "," ++ acc) "" diff --git a/src/MidnightExample/Ledger.lagda b/src/MidnightExample/Ledger.lagda index afd97237..189dc858 100644 --- a/src/MidnightExample/Ledger.lagda +++ b/src/MidnightExample/Ledger.lagda @@ -23,7 +23,6 @@ instance Hashable-ℕ : Hashable ℕ Hash Hashable-ℕ .hash n = hash (+ n) - Hashable-ℕ .hashInj = ℤ.+-injective ∘ hashInj _<ᵇ_ : Maybe ℕ → Maybe ℕ → Bool just a <ᵇ just b = a Prelude.<ᵇ b @@ -89,7 +88,6 @@ txDelta-injective {dec} {dec} refl = refl instance Hashable-Tx : Hashable Tx Hash Hashable-Tx .hash = hash ∘ txDelta - Hashable-Tx .hashInj = txDelta-injective ∘ hashInj \end{code} \caption{Transactions} \end{figure*} diff --git a/src/ScriptVerification/Examples.agda b/src/ScriptVerification/Examples.agda index 040433c1..a2071f55 100644 --- a/src/ScriptVerification/Examples.agda +++ b/src/ScriptVerification/Examples.agda @@ -1,113 +1,4 @@ -open import Ledger.Prelude hiding (fromList; ε); open Computational -open import ScriptVerification.Prelude +module ScriptVerification.Examples where -module ScriptVerification.Examples - (scriptImp : ScriptImplementation ℕ) (open ScriptImplementation scriptImp) - where - -open import ScriptVerification.LedgerImplementation ℕ scriptImp -open import ScriptVerification.Lib ℕ scriptImp - -open Implementation - -open import Ledger.ScriptValidation SVTransactionStructure SVAbstractFunctions -open import Data.Empty --- open import Ledger.UTxo SVTransactionStructure SVAbstractFunctions -open import Ledger.Utxo SVTransactionStructure SVAbstractFunctions -open import Ledger.Transaction -open TransactionStructure SVTransactionStructure -open import Ledger.Types.Epoch -open EpochStructure SVEpochStructure - -open import Data.Rational - -succeedIf1 : PlutusScript -succeedIf1 zero _ = false -succeedIf1 (suc zero) _ = true -succeedIf1 (suc (suc x)) _ = false - -succeedIf1' : ℕ → ℕ → Bool -succeedIf1' zero _ = false -succeedIf1' (suc zero) _ = true -succeedIf1' (suc (suc x)) _ = false - -test : PlutusScript -test x y with deserialise x -... | just x₁ = succeedIf1' x₁ y -... | nothing = false - -initEnv : UTxOEnv -initEnv = createEnv 0 - -initState : UTxO -initState = fromList' (createInitUtxoState 5 10) - -initTxOut : TxOut -initTxOut = inj₁ (record { net = tt ; - pay = inj₂ succeedIf1 ; - stake = inj₂ succeedIf1 }) - , 10 , nothing - -exTx : Tx -exTx = record { body = record - { txins = ∅ - ; txouts = fromListIx ((6 , initTxOut) ∷ []) - ; txfee = 10 - ; mint = 0 - ; txvldt = nothing , nothing - ; txcerts = [] - ; txwdrls = ∅ - ; txvote = [] - ; txprop = [] - ; txdonation = 0 - ; txup = nothing - ; txADhash = nothing - ; netwrk = just tt - ; txsize = 10 - ; txid = 6 - ; collateral = ∅ - ; reqSigHash = ∅ -- maybe need this - ; scriptIntHash = nothing -- not sure - } ; - wits = record { vkSigs = ∅ ; - scripts = ∅ ; - txdats = ∅ ; - txrdmrs = ∅ } ; - isValid = false ; - txAD = nothing } - - -example : Bool -example = evalScripts exTx (collectPhaseTwoScriptInputs (UTxOEnv.pparams initEnv) exTx initState) - -example2 : Bool -example2 = not true - - --- scriptsNoTest : {!!} --- scriptsNoTest = Scripts-No {!!} - - -{- -initList : List (TxIn × TxOut) -initList = ((1 , 1) , inj₂ (record { net = tt ; pay = inj₁ 1 ; attrsSize = 1 }) , (1 , nothing)) ∷ [] - -initUTxO : UTxO -initUTxO = fromListᵐ initList - -exTx : Tx -exTx = {!!} - -example : Bool -example = evalScripts exTx (collectPhaseTwoScriptInputs (UTxOEnv.pparams initEnv) exTx initUTxO) --} - - -{- -initState : UTxOState -initState = ? - -transaction : Tx -transaction = ? --} --- _⊢_⇀⦇_,UTXOS⦈_ : UTxOEnv → UTxOState → Tx → UTxOState → Set +import ScriptVerification.SucceedIfNumber +import ScriptVerification.HelloWorld diff --git a/src/ScriptVerification/HelloWorld.agda b/src/ScriptVerification/HelloWorld.agda new file mode 100644 index 00000000..740f70aa --- /dev/null +++ b/src/ScriptVerification/HelloWorld.agda @@ -0,0 +1,128 @@ +open import Ledger.Prelude hiding (fromList; ε); open Computational +open import ScriptVerification.Prelude + +module ScriptVerification.HelloWorld where + +scriptImp : ScriptImplementation String String +scriptImp = record { serialise = id ; + deserialise = λ x → just x ; + toData' = λ x → "dummy" } + +open import ScriptVerification.LedgerImplementation String String scriptImp +open import ScriptVerification.Lib String String scriptImp +open import Ledger.ScriptValidation SVTransactionStructure SVAbstractFunctions +open import Data.Empty +open import Ledger.Utxo SVTransactionStructure SVAbstractFunctions +open import Ledger.Transaction +open TransactionStructure SVTransactionStructure +open import Ledger.Types.Epoch +open EpochStructure SVEpochStructure +open Implementation + +-- true if redeemer is "Hello World" +helloWorld' : Maybe String → Maybe String → Bool +helloWorld' _ (just s) = ⌊ (s ≟ "Hello World") ⌋ +helloWorld' _ _ = false + +helloWorld : PlutusScript +helloWorld = 777 , applyScript helloWorld' + +initEnv : UTxOEnv +initEnv = createEnv 0 + +initTxOut : TxOut +initTxOut = inj₁ (record { net = tt ; + pay = inj₂ 777 ; + stake = inj₂ 777 }) + , 10 , nothing + +script : TxIn × TxOut +script = (6 , 6) , initTxOut + +initState : UTxO +initState = fromList' (script ∷ (createInitUtxoState 5 10)) + +succeedTx : Tx +succeedTx = record { body = record + { txins = Ledger.Prelude.fromList ((6 , 6) ∷ []) + ; txouts = ∅ -- fromListIx ((6 , initTxOut) ∷ []) + ; txfee = 10 + ; mint = 0 + ; txvldt = nothing , nothing + ; txcerts = [] + ; txwdrls = ∅ + ; txvote = [] + ; txprop = [] + ; txdonation = 0 + ; txup = nothing + ; txADhash = nothing + ; netwrk = just tt + ; txsize = 10 + ; txid = 7 + ; collateral = ∅ + ; reqSigHash = ∅ -- maybe need this + ; scriptIntHash = nothing -- not sure + } ; + wits = record { vkSigs = ∅ ; + scripts = Ledger.Prelude.fromList ((inj₂ helloWorld) ∷ []) ; + txdats = ∅ ; + txrdmrs = fromListᵐ (((Spend , 6) , "Hello World" , (5 , 5)) ∷ []) } ; + isValid = true ; + txAD = nothing } + +failTx : Tx +failTx = record { body = record + { txins = Ledger.Prelude.fromList ((6 , 6) ∷ []) + ; txouts = ∅ -- fromListIx ((6 , initTxOut) ∷ []) + ; txfee = 10 + ; mint = 0 + ; txvldt = nothing , nothing + ; txcerts = [] + ; txwdrls = ∅ + ; txvote = [] + ; txprop = [] + ; txdonation = 0 + ; txup = nothing + ; txADhash = nothing + ; netwrk = just tt + ; txsize = 10 + ; txid = 7 + ; collateral = ∅ + ; reqSigHash = ∅ -- maybe need this + ; scriptIntHash = nothing -- not sure + } ; + wits = record { vkSigs = ∅ ; + scripts = Ledger.Prelude.fromList ((inj₂ helloWorld) ∷ []) ; + txdats = ∅ ; + txrdmrs = fromListᵐ (((Spend , 6) , "Hello World!" , (5 , 5)) ∷ []) } ; + isValid = true ; + txAD = nothing } + +succeedState : List (Script × List Implementation.Data × Implementation.ExUnits × Implementation.CostModel) +succeedState = (collectPhaseTwoScriptInputs (UTxOEnv.pparams initEnv) succeedTx initState) + +succeedExample : Bool +succeedExample = evalScripts succeedTx succeedState + +failState : List (Script × List Implementation.Data × Implementation.ExUnits × Implementation.CostModel) +failState = (collectPhaseTwoScriptInputs (UTxOEnv.pparams initEnv) failTx initState) + +failExample : Bool +failExample = evalScripts failTx failState + +opaque + unfolding collectPhaseTwoScriptInputs + unfolding setToList + + -- need to check that the state is non-empty otherwise evalScripts will always return true + _ : notEmpty succeedState ≡ ⊤ + _ = refl + + _ : succeedExample ≡ true + _ = refl + + _ : notEmpty failState ≡ ⊤ + _ = refl + + _ : failExample ≡ false + _ = refl diff --git a/src/ScriptVerification/LedgerImplementation.agda b/src/ScriptVerification/LedgerImplementation.agda index 0b0fcbbc..ed7518a9 100644 --- a/src/ScriptVerification/LedgerImplementation.agda +++ b/src/ScriptVerification/LedgerImplementation.agda @@ -1,41 +1,35 @@ open import ScriptVerification.Prelude module ScriptVerification.LedgerImplementation - (D : Set) - (scriptImp : ScriptImplementation D) (open ScriptImplementation scriptImp) + (T D : Set) + (scriptImp : ScriptImplementation T D) (open ScriptImplementation scriptImp) where open import Ledger.Prelude hiding (fromList; ε); open Computational - open import Data.Rational using (0ℚ; ½) - open import Algebra using (CommutativeMonoid) open import Algebra.Morphism using (module MonoidMorphisms) open import Data.Nat.Properties using (+-0-commutativeMonoid; +-0-isCommutativeMonoid) open import Relation.Binary.Morphism.Structures - open import Foreign.Convertible - import Foreign.Haskell as F import Ledger.Foreign.LedgerTypes as F - open import Ledger.Crypto open import Ledger.Transaction open import Ledger.Types.Epoch open import Ledger.Types.GovStructure - open import Interface.HasOrder.Instance module _ {A : Set} ⦃ _ : DecEq A ⦄ where instance ∀Hashable : Hashable A A - ∀Hashable = λ where .hash → id; .hashInj refl → refl + ∀Hashable = λ where .hash → id ∀isHashableSet : isHashableSet A ∀isHashableSet = mkIsHashableSet A instance Hashable-⊤ : Hashable ⊤ ℕ - Hashable-⊤ = λ where .hash tt → 0; .hashInj _ → refl + Hashable-⊤ = λ where .hash tt → 0 module Implementation where Network = ⊤ @@ -55,10 +49,10 @@ module Implementation where Data = D Dataʰ = mkHashableSet Data toData : ∀ {A : Set} → A → D - toData = serialise + toData = toData' -- fix this - PlutusScript = Data → Data → Bool - ScriptHash = Data → Data → Bool + PlutusScript = ℕ × (List Data → Bool) + ScriptHash = ℕ ExUnits = ℕ × ℕ ExUnit-CommutativeMonoid = IsCommutativeMonoid' 0ℓ 0ℓ ExUnits ∋ (toCommMonoid' record @@ -74,7 +68,7 @@ module Implementation where Language = ⊤ LangDepView = ⊤ Prices = ⊤ - open import Ledger.TokenAlgebra (Data → Data → Bool) + open import Ledger.TokenAlgebra ℕ coinTokenAlgebra : TokenAlgebra coinTokenAlgebra = λ where .Value → ℕ @@ -124,23 +118,30 @@ instance _ = SVCrypto open import Ledger.Script it it + + SVScriptStructure : ScriptStructure SVScriptStructure = record { hashRespectsUnion = hashRespectsUnion ; ps = SVP2ScriptStructure } where - postulate - instance Hashable-Timelock : Hashable Timelock (Implementation.Data → Implementation.Data → Bool) -- ℕ + + instance Hashable-Timelock : Hashable Timelock ℕ + Hashable-Timelock = record { hash = λ x → 0 } + + instance Hashable-PlutusScript : Hashable Implementation.PlutusScript ℕ + Hashable-PlutusScript = record { hash = λ x → proj₁ x } hashRespectsUnion : ∀ {A B ℍ} → Hashable A ℍ → Hashable B ℍ → Hashable (A ⊎ B) ℍ + hashRespectsUnion ha hb = record { hash = λ { (inj₁ x) → Hashable.hash ha x ; (inj₂ y) → Hashable.hash hb y }} - SVP2ScriptStructure : PlutusStructure - SVP2ScriptStructure = record - { Implementation - ; validPlutusScript = λ _ _ _ _ → ⊤ - } + SVP2ScriptStructure : PlutusStructure + SVP2ScriptStructure = record + { Implementation + ; validPlutusScript = λ _ _ _ _ → ⊤ + } instance _ = SVScriptStructure @@ -187,6 +188,11 @@ instance _ = SVTransactionStructure open import Ledger.Abstract it open import Ledger.Gov it +open TransactionStructure it + +indexOfTxInImp : TxIn → ℙ TxIn → Maybe Ix +indexOfTxInImp x y = lookupᵐ? (fromListᵐ (setToList y)) (proj₁ x) + SVAbstractFunctions : AbstractFunctions SVAbstractFunctions = record { Implementation @@ -195,12 +201,12 @@ SVAbstractFunctions = record ; indexOfImp = record { indexOfDCert = λ _ _ → nothing ; indexOfRwdAddr = λ _ _ → nothing - ; indexOfTxIn = λ _ _ → nothing + ; indexOfTxIn = indexOfTxInImp ; indexOfPolicyId = λ _ _ → nothing ; indexOfVote = λ _ _ → nothing ; indexOfProposal = λ _ _ → nothing } - ; runPLCScript = λ _ _ _ _ → false + ; runPLCScript = λ { x x₁ x₂ x₃ → proj₂ x₁ x₃ } ; scriptSize = λ _ → 0 } instance _ = SVAbstractFunctions diff --git a/src/ScriptVerification/LedgerTypes.agda b/src/ScriptVerification/LedgerTypes.agda deleted file mode 100644 index e69de29b..00000000 diff --git a/src/ScriptVerification/Lib.agda b/src/ScriptVerification/Lib.agda index df4fd050..c5d806ed 100644 --- a/src/ScriptVerification/Lib.agda +++ b/src/ScriptVerification/Lib.agda @@ -1,14 +1,11 @@ open import Ledger.Prelude hiding (fromList; ε); open Computational open import ScriptVerification.Prelude -module ScriptVerification.Lib (D : Set) - (scriptImp : ScriptImplementation D) (open ScriptImplementation scriptImp) +module ScriptVerification.Lib (A D : Set) + (scriptImp : ScriptImplementation A D) (open ScriptImplementation scriptImp) where -open import ScriptVerification.LedgerImplementation D scriptImp - -open Implementation - +open import ScriptVerification.LedgerImplementation A D scriptImp open import Ledger.ScriptValidation SVTransactionStructure SVAbstractFunctions open import Data.Empty open import Ledger.Utxo SVTransactionStructure SVAbstractFunctions @@ -16,9 +13,9 @@ open import Ledger.Transaction open TransactionStructure SVTransactionStructure open import Ledger.Types.Epoch open EpochStructure SVEpochStructure - open import Data.Rational open import Ledger.Set.Theory +open Implementation createEnv : ℕ → UTxOEnv createEnv s = record { slot = s ; @@ -91,37 +88,12 @@ fromList' = fromListᵐ fromListIx : List (Implementation.Ix × TxOut) → Implementation.Ix ⇀ TxOut fromListIx = fromListᵐ -{- -createTx : ℙ TxIn - → List TxOut - → D - → D - → List PlutusScript - → Tx -createTx a b c d e = record { body = record - { txins = {!!} - ; txouts = {!!} - ; txfee = {!!} - ; mint = {!!} - ; txvldt = {!!} - ; txcerts = {!!} - ; txwdrls = {!!} - ; txvote = {!!} - ; txprop = {!!} - ; txdonation = {!!} - ; txup = {!!} - ; txADhash = {!!} - ; netwrk = {!!} - ; txsize = {!!} - ; txid = {!!} - ; collateral = {!!} - ; reqSigHash = {!!} - ; scriptIntHash = {!!} - } - ; wits = record { vkSigs = {!!} - ; scripts = {!!} - ; txdats = {!!} - ; txrdmrs = {!!} } - ; isValid = {!!} - ; txAD = {!!} } --} +applyScript : (Maybe D → Maybe D → Bool) → List D → Bool +applyScript f [] = f nothing nothing +applyScript f (_ ∷ []) = f nothing nothing +applyScript f (redeemer ∷ valcontext ∷ []) = f nothing (just redeemer) +applyScript f (datum ∷ redeemer ∷ valcontext ∷ _) = f (just datum) (just redeemer) + +notEmpty : ∀ {A : Set} → List A → Set +notEmpty [] = ⊥ +notEmpty (x ∷ xs) = ⊤ diff --git a/src/ScriptVerification/Prelude.agda b/src/ScriptVerification/Prelude.agda index f468c9fb..bd428599 100644 --- a/src/ScriptVerification/Prelude.agda +++ b/src/ScriptVerification/Prelude.agda @@ -2,8 +2,8 @@ open import Ledger.Prelude hiding (fromList; ε); open Computational module ScriptVerification.Prelude where -record ScriptImplementation (D : Set) : Set₁ where - field serialise : ∀ {A : Set} → A → D - deserialise : ∀ {A : Set} → D → Maybe A +record ScriptImplementation (T D : Set) : Set₁ where + field serialise : T → D + deserialise : D → Maybe T + toData' : ∀ {A : Set} → A → D -- fix this ⦃ DecEq-Data ⦄ : DecEq D - ⦃ DecEq-Script ⦄ : DecEq (D → D → Bool) diff --git a/src/ScriptVerification/SimpleScript.agda b/src/ScriptVerification/SimpleScript.agda deleted file mode 100644 index 482038b8..00000000 --- a/src/ScriptVerification/SimpleScript.agda +++ /dev/null @@ -1,3 +0,0 @@ -{-# OPTIONS --safe #-} - -module ScriptVerification.SimpleScript where diff --git a/src/ScriptVerification/SucceedIfNumber.agda b/src/ScriptVerification/SucceedIfNumber.agda new file mode 100644 index 00000000..97eaeada --- /dev/null +++ b/src/ScriptVerification/SucceedIfNumber.agda @@ -0,0 +1,232 @@ +open import Ledger.Prelude hiding (fromList; ε); open Computational +open import ScriptVerification.Prelude + +module ScriptVerification.SucceedIfNumber where + +scriptImp : ScriptImplementation ℕ ℕ +scriptImp = record { serialise = id ; + deserialise = λ x → just x ; + toData' = λ x → 9999999 } + +open import ScriptVerification.LedgerImplementation ℕ ℕ scriptImp +open import ScriptVerification.Lib ℕ ℕ scriptImp +open import Ledger.ScriptValidation SVTransactionStructure SVAbstractFunctions +open import Data.Empty +open import Ledger.Utxo SVTransactionStructure SVAbstractFunctions +open import Ledger.Transaction +open TransactionStructure SVTransactionStructure +open import Ledger.Types.Epoch +open EpochStructure SVEpochStructure +open Implementation + +-- succeed if the datum is 1 +succeedIf1' : Maybe ℕ → Maybe ℕ → Bool +succeedIf1' (just (suc zero)) _ = true +succeedIf1' _ _ = false + +succeedIf1 : PlutusScript +succeedIf1 = 777 , applyScript succeedIf1' + +--succeed if the redeemer is 1 +succeedIf1Redeemer' : Maybe ℕ → Maybe ℕ → Bool +succeedIf1Redeemer' _ (just (suc zero)) = true +succeedIf1Redeemer' _ _ = false + +succeedIf1Redeemer : PlutusScript +succeedIf1Redeemer = 888 , applyScript succeedIf1Redeemer' + +{- +test : PlutusScript +test x y with deserialise x +... | just x₁ = succeedIf1' x₁ y +... | nothing = false +-} + +initEnv : UTxOEnv +initEnv = createEnv 0 + +initState : UTxO +initState = fromList' (createInitUtxoState 5 10) + +-- initTxOut for script with datum reference +initTxOut : TxOut +initTxOut = inj₁ (record { net = tt ; + pay = inj₂ 777 ; + stake = inj₂ 777 }) + , 10 , just 99 + +-- initTxOut for script without datum reference +initTxOut' : TxOut +initTxOut' = inj₁ (record { net = tt ; + pay = inj₂ 888 ; + stake = inj₂ 888 }) + , 10 , nothing + +script : TxIn × TxOut +script = (6 , 6) , initTxOut + +script' : TxIn × TxOut +script' = (6 , 6) , initTxOut' + +initState' : UTxO +initState' = fromList' (script ∷ (createInitUtxoState 5 10)) + +initState'' : UTxO +initState'' = fromList' (script' ∷ (createInitUtxoState 5 10)) + +exTx : Tx +exTx = record { body = record + { txins = ∅ + ; txouts = fromListIx ((6 , initTxOut) ∷ []) + ; txfee = 10 + ; mint = 0 + ; txvldt = nothing , nothing + ; txcerts = [] + ; txwdrls = ∅ + ; txvote = [] + ; txprop = [] + ; txdonation = 0 + ; txup = nothing + ; txADhash = nothing + ; netwrk = just tt + ; txsize = 10 + ; txid = 6 + ; collateral = ∅ + ; reqSigHash = ∅ + ; scriptIntHash = nothing + } ; + wits = record { vkSigs = ∅ ; + scripts = ∅ ; + txdats = ∅ ; + txrdmrs = ∅ } ; + isValid = false ; + txAD = nothing } + + +getState : List (Script × List Implementation.Data × Implementation.ExUnits × Implementation.CostModel) +getState = (collectPhaseTwoScriptInputs (UTxOEnv.pparams initEnv) exTx initState) + +example : Bool +example = evalScripts exTx (collectPhaseTwoScriptInputs (UTxOEnv.pparams initEnv) exTx initState) + +exTx' : Tx +exTx' = record { body = record + { txins = Ledger.Prelude.fromList ((6 , 6) ∷ []) + ; txouts = ∅ -- fromListIx ((6 , initTxOut) ∷ []) + ; txfee = 10 + ; mint = 0 + ; txvldt = nothing , nothing + ; txcerts = [] + ; txwdrls = ∅ + ; txvote = [] + ; txprop = [] + ; txdonation = 0 + ; txup = nothing + ; txADhash = nothing + ; netwrk = just tt + ; txsize = 10 + ; txid = 7 + ; collateral = ∅ + ; reqSigHash = ∅ -- maybe need this + ; scriptIntHash = nothing -- not sure + } ; + wits = record { vkSigs = ∅ ; + scripts = Ledger.Prelude.fromList ((inj₂ succeedIf1) ∷ []) ; + txdats = fromListᵐ ((99 , 1) ∷ []) ; + txrdmrs = fromListᵐ (((Spend , 6) , 5 , (5 , 5)) ∷ []) } ; + isValid = true ; + txAD = nothing } + +getState' : List (Script × List Implementation.Data × Implementation.ExUnits × Implementation.CostModel) +getState' = (collectPhaseTwoScriptInputs (UTxOEnv.pparams initEnv) exTx' initState') + +helpMe : Maybe (Script × List Implementation.Data × Implementation.ExUnits × Implementation.CostModel) → Bool +helpMe (just x) = true +helpMe nothing = false + +example2 : Bool +example2 = evalScripts exTx' (collectPhaseTwoScriptInputs (UTxOEnv.pparams initEnv) exTx' initState') + +exampleDatum : List Datum +exampleDatum = getDatum exTx' initState' (Spend (6 , 6)) + +exTx'' : Tx +exTx'' = record { body = record + { txins = Ledger.Prelude.fromList ((6 , 6) ∷ []) + ; txouts = ∅ -- fromListIx ((6 , initTxOut) ∷ []) + ; txfee = 10 + ; mint = 0 + ; txvldt = nothing , nothing + ; txcerts = [] + ; txwdrls = ∅ + ; txvote = [] + ; txprop = [] + ; txdonation = 0 + ; txup = nothing + ; txADhash = nothing + ; netwrk = just tt + ; txsize = 10 + ; txid = 7 + ; collateral = ∅ + ; reqSigHash = ∅ + ; scriptIntHash = nothing + } ; + wits = record { vkSigs = ∅ ; + scripts = Ledger.Prelude.fromList ((inj₂ succeedIf1Redeemer) ∷ []) ; + txdats = ∅ ; + txrdmrs = fromListᵐ (((Spend , 6) , 1 , (5 , 5)) ∷ []) } ; + isValid = true ; + txAD = nothing } + + +example3 : Bool +example3 = evalScripts exTx'' (collectPhaseTwoScriptInputs (UTxOEnv.pparams initEnv) exTx'' initState'') + +open import Ledger.Utxo.Properties SVTransactionStructure SVAbstractFunctions + +initUtxoState : UTxOState +initUtxoState = ⟦ initState'' , 0 , fromListᵐ [] , 0 ⟧ᵘ + +testThis : ComputationResult String UTxOState +testThis = UTXO-step initEnv initUtxoState exTx'' + +isSuccess : ComputationResult String UTxOState → Bool +isSuccess (success x) = true +isSuccess (failure x) = false + +exampleDatum' : List Datum +exampleDatum' = getDatum exTx'' initState'' (Spend (6 , 6)) + +opaque + unfolding collectPhaseTwoScriptInputs + unfolding setToList + + _ : getState ≡ [] + _ = refl + + _ : example ≡ true + _ = refl + + test2 : lookupScriptHash 777 exTx' ≡ just (inj₂ succeedIf1) + test2 = refl + + _ : exampleDatum ≡ 1 ∷ [] + _ = refl + + -- _ : getState' ≡ [] + -- _ = {!refl!} + + _ : exampleDatum' ≡ [] + _ = refl + + _ : example2 ≡ true + _ = refl + + _ : example3 ≡ true + _ = refl + +exampleRunScript' : Bool +exampleRunScript' = ⟦ succeedIf1 ⟧, tt , ( 1000 , 1000 ) , (1 ∷ 0 ∷ []) + + +-- UTXO-step : UTxOEnv → UTxOState → Tx → ComputationResult String UTxOState