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 →  }

open import ScriptVerification.LedgerImplementation ℕ ℕ scriptImp
open import ScriptVerification.Lib ℕ ℕ 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

-- succeed if the datum is 1
succeedIf1Datum' : Maybe ℕ → Maybe ℕ → Bool
succeedIf1Datum' (just (suc zero)) _ = true
succeedIf1Datum' _ _ = false

succeedIf1Datum : PlutusScript
succeedIf1Datum =  , applyScript succeedIf1Datum'

--succeed if the redeemer is 1
succeedIf1Redeemer' : Maybe ℕ → Maybe ℕ → Bool
succeedIf1Redeemer' _ (just (suc zero)) = true
succeedIf1Redeemer' _ _ = false

succeedIf1Redeemer : PlutusScript
succeedIf1Redeemer =  , applyScript succeedIf1Redeemer'

initEnv : UTxOEnv
initEnv = createEnv 

-- initTxOut for script with datum reference
initTxOut : TxOut
initTxOut = inj₁ (record { net =  ;
                           pay = ScriptObj  ;
                           stake = just (ScriptObj ) })
                           ,  , just (inj₂ ) , nothing

-- initTxOut for script without datum reference
initTxOut' : TxOut
initTxOut' = inj₁ (record { net =  ;
                           pay = ScriptObj  ;
                           stake = just (ScriptObj ) })
                           ,  , nothing , nothing

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

scriptRedeemer : TxIn × TxOut
scriptRedeemer = ( , ) , initTxOut'

initStateDatum : UTxO
initStateDatum = fromList' (scriptDatum ∷ (createInitUtxoState  ))

initStateRedeemer : UTxO
initStateRedeemer = fromList' (scriptRedeemer ∷ (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ᵐ (( , ) ∷ []) ;
                                scripts = Ledger.Prelude.fromList ((inj₂ succeedIf1Datum) ∷ []) ;
                                txdats = fromListᵐ (( , ) ∷ []) ;
                                txrdmrs = fromListᵐ (((Spend , ) ,  , ( , )) ∷ []) } ;
                isValid = true ;
                txAD = nothing }

evalScriptDatum : Bool
evalScriptDatum = evalScripts succeedTx (collectPhaseTwoScriptInputs (UTxOEnv.pparams initEnv) succeedTx initStateDatum)

exampleDatum : List Datum
exampleDatum = getDatum succeedTx initStateDatum (Spend ( , ))

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₂ succeedIf1Redeemer) ∷ []) ;
                                txdats = ∅ ;
                                txrdmrs = fromListᵐ (((Spend , ) ,  , ( , )) ∷ []) } ;
                isValid = true ;
                txAD = nothing }


evalScriptRedeemer : Bool
evalScriptRedeemer = evalScripts failTx (collectPhaseTwoScriptInputs (UTxOEnv.pparams initEnv) failTx initStateRedeemer)

exampleDatum' : List Datum
exampleDatum' = getDatum failTx initStateRedeemer (Spend ( , ))

opaque
  unfolding collectPhaseTwoScriptInputs
  unfolding setToList
  unfolding outs

  gotScript : lookupScriptHash  succeedTx initStateDatum ≡ just (inj₂ succeedIf1Datum)
  gotScript = refl

  _ : exampleDatum ≡  ∷ []
  _ = refl

  _ : exampleDatum' ≡ []
  _ = refl

  _ : evalScriptDatum ≡ true
  _ = refl

  _ : evalScriptRedeemer ≡ true
  _ = refl

  -- Compute the result of running the UTXO rules on the succeedTx transaction
  succeedExample : ComputationResult String UTxOState
  succeedExample = UTXO-step initEnv ⟦ initStateDatum ,  , ∅ ,  ⟧  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 ⟦ initStateRedeemer ,  , ∅ ,  ⟧  failTx

  _ : isFailure failExample
  _ = _ , refl

  -- Note that the UTXOS rule succeeds but the UTXO rule fails for failTx
  failExampleS : Bool
  failExampleS = case compute Computational-UTXOS initEnv ⟦ initStateRedeemer ,  , ∅ ,  ⟧ failTx of λ where
    (success x) → true
    (failure x) → false

  _ : failExampleS ≡ true
  _ = refl

  failExampleU : Bool
  failExampleU = case compute Computational-UTXO initEnv ⟦ initStateRedeemer ,  , ∅ ,  ⟧ failTx of λ where
    (success x) → true
    (failure x) → false

  _ : failExampleU ≡ false
  _ = refl