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 Class.To
open import Ledger.Conway.Conformance.Utxo SVTransactionStructure SVAbstractFunctions
open import Ledger.Transaction
open TransactionStructure SVTransactionStructure
open import Ledger.Types.Epoch
open EpochStructure SVEpochStructure
open Implementation
open import Ledger.Conway.Conformance.Utxo.Properties SVTransactionStructure SVAbstractFunctions
open import Ledger.Conway.Conformance.Utxow.Properties SVTransactionStructure SVAbstractFunctions

-- true if redeemer is "Hello World"
helloWorld' : Maybe String → Maybe String → Bool
helloWorld' _ (just s) = ⌊ (s ≟ "Hello World") ⌋
helloWorld' _ _ = false

helloWorld : PlutusScript
helloWorld =  , applyScript helloWorld'

initEnv : UTxOEnv
initEnv = createEnv 

initTxOut : TxOut
initTxOut = inj₁ (record { net =  ;
                           pay = ScriptObj  ;
                           stake = just (ScriptObj ) })
                           ,  , nothing , nothing

script : TxIn × TxOut
script = ( , ) , initTxOut

initState : UTxO
initState = fromList' (script ∷ (createInitUtxoState  ))

succeedTx : Tx
succeedTx = record { body = record
                         { txins = Ledger.Prelude.fromList (( , ) ∷ ( , ) ∷ [])
                         ; refInputs = ∅
                         ; txouts = fromListIx (( , initTxOut)
                                               ∷ (
                                                 , ((inj₁ (record { net =  ;
                                                                    pay = KeyHashObj  ;
                                                                    stake = just (KeyHashObj ) }))
                                                 , ( - ) , nothing , nothing))
                                               ∷ [])
                         ; txfee = 
                         ; mint = 
                         ; txvldt = nothing , nothing
                         ; txcerts = []
                         ; txwdrls = ∅
                         ; txvote = []
                         ; txprop = []
                         ; txdonation = 
                         ; txup = nothing
                         ; txADhash = nothing
                         ; txNetworkId = just 
                         ; curTreasury = nothing
                         ; txsize = 
                         ; txid = 
                         ; collateral = Ledger.Prelude.fromList (( , ) ∷ [])
                         ; reqSigHash = ∅
                         ; scriptIntHash = nothing
                         } ;
                wits = record { vkSigs = fromListᵐ (( , ) ∷ []) ;
                                -- signature now is first number + txId ≡ second number
                                -- first number is needs to be the id for the script
                                scripts = Ledger.Prelude.fromList ((inj₂ helloWorld) ∷ []) ;
                                txdats = ∅ ;
                                txrdmrs = fromListᵐ (((Spend , ) , "Hello World" , ( , )) ∷ []) } ;
                isValid = true ;
                txAD = nothing }

failTx : Tx
failTx = record { body = record
                         { txins = Ledger.Prelude.fromList (( , ) ∷ [])
                         ; refInputs = ∅
                         ; txouts = ∅
                         ; txfee = 
                         ; mint = 
                         ; txvldt = nothing , nothing
                         ; txcerts = []
                         ; txwdrls = ∅
                         ; txvote = []
                         ; txprop = []
                         ; txdonation = 
                         ; txup = nothing
                         ; txADhash = nothing
                         ; txNetworkId = just 
                         ; curTreasury = nothing
                         ; txsize = 
                         ; txid = 
                         ; collateral = ∅
                         ; reqSigHash = ∅
                         ; scriptIntHash = nothing
                         } ;
                wits = record { vkSigs = ∅ ;
                                scripts = Ledger.Prelude.fromList ((inj₂ helloWorld) ∷ []) ;
                                txdats = ∅ ;
                                txrdmrs = fromListᵐ (((Spend , ) , "Hello World!" , ( , )) ∷ []) } ;
                isValid = true ;
                txAD = nothing }

succeedState : List (Script × List Implementation.Data × Implementation.ExUnits × Implementation.CostModel)
succeedState = (collectPhaseTwoScriptInputs (UTxOEnv.pparams initEnv) succeedTx initState)

evalSucceedScript : Bool
evalSucceedScript = evalScripts succeedTx succeedState

failState : List (Script × List Implementation.Data × Implementation.ExUnits × Implementation.CostModel)
failState = (collectPhaseTwoScriptInputs (UTxOEnv.pparams initEnv) failTx initState)

evalFailScript : Bool
evalFailScript = evalScripts failTx failState

opaque
  unfolding collectPhaseTwoScriptInputs
  unfolding setToList
  unfolding outs

  _ : notEmpty succeedState ≡ ⊤
  _ = refl

  -- need to check that the state is non-empty otherwise evalScripts will always return true
  _ : notEmpty succeedState ≡ ⊤
  _ = refl

  _ : evalSucceedScript ≡ true
  _ = refl

  _ : notEmpty failState ≡ ⊤
  _ = refl

  _ : evalFailScript ≡ false
  _ = refl

  -- Compute the result of running the UTXO rules on the succeedTx transaction
  succeedExample : ComputationResult String UTxOState
  succeedExample = UTXO-step initEnv ⟦ initState ,  , ∅ ,  ⟧  succeedTx

  _ : isSuccess succeedExample ≡ true
  _  = refl

  -- Compute the result of running the UTXO rules on the failTx transaction
  failExample : ComputationResult String UTxOState
  failExample = UTXO-step initEnv ⟦ initState ,  , ∅ ,  ⟧  failTx

  _ : isFailure failExample
  _ = _ , refl