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.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

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