-
Notifications
You must be signed in to change notification settings - Fork 12
/
Examples.agda
113 lines (88 loc) · 3.23 KB
/
Examples.agda
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
open import Ledger.Prelude hiding (fromList; ε); open Computational
open import ScriptVerification.Prelude
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