Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Modifying ledger and adding working script examples
- Loading branch information
Showing
17 changed files
with
433 additions
and
200 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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 |
Oops, something went wrong.