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.Conway.ScriptValidation SVTransactionStructure SVAbstractFunctions
open import Data.Empty
open import stdlib-classes.Class.HasCast
open import Ledger.Conway.Conformance.Utxo SVTransactionStructure SVAbstractFunctions
open import Ledger.Conway.Transaction
open TransactionStructure SVTransactionStructure
open import Ledger.Conway.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