SucceedIfNumber

{-# OPTIONS --safe #-}

open import Ledger.Prelude hiding (fromList; ε); open Computational
open import Ledger.Conway.Test.Prelude

module Ledger.Conway.Test.Examples.SucceedIfNumber where

scriptImp : ScriptImplementation ℕ ℕ
scriptImp = record { serialise = id ;
                     deserialise = λ x → just x ;
                     toData' = λ x →  }

open import Ledger.Conway.Test.LedgerImplementation ℕ ℕ scriptImp
open import Ledger.Conway.Test.Lib ℕ ℕ scriptImp
open import Ledger.Conway.Script.Validation SVTransactionStructure SVAbstractFunctions
open import Ledger.Conway.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.Utxo.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
                         ; txid = 
                         ; collateral = Ledger.Prelude.fromList (( , ) ∷ [])
                         ; reqSigHash = ∅
                         ; scriptIntHash = nothing
                         } ;
                wits = record { vkSigs = fromListᵐ (( , ) ∷ []) ;
                                scripts = Ledger.Prelude.fromList ((inj₂ succeedIf1Datum) ∷ []) ;
                                txdats = Ledger.Prelude.fromList ( ∷ []) ;
                                txrdmrs = fromListᵐ (((Spend , ) ,  , ( , )) ∷ []) } ;
                txsize =  ;
                isValid = true ;
                txAD = nothing }

evalScriptDatum : Bool
evalScriptDatum = evalP2Scripts (collectP2ScriptsWithContext (UTxOEnv.pparams initEnv) succeedTx initStateDatum)

exampleDatum : Maybe 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
                         ; txid = 
                         ; collateral = ∅
                         ; reqSigHash = ∅
                         ; scriptIntHash = nothing
                         } ;
                wits = record { vkSigs = ∅ ;
                                scripts = Ledger.Prelude.fromList ((inj₂ succeedIf1Redeemer) ∷ []) ;
                                txdats = ∅ ;
                                txrdmrs = fromListᵐ (((Spend , ) ,  , ( , )) ∷ []) } ;
                txsize =  ;
                isValid = true ;
                txAD = nothing }


evalScriptRedeemer : Bool
evalScriptRedeemer = evalP2Scripts (collectP2ScriptsWithContext (UTxOEnv.pparams initEnv) failTx initStateRedeemer)

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

opaque
  unfolding Computational-UTXO
  unfolding collectP2ScriptsWithContext
  unfolding setToList
  unfolding outs

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

  _ : exampleDatum ≡ just 
  _ = refl

  _ : exampleDatum' ≡ nothing
  _ = 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 $\begin{pmatrix} \,\href{Ledger.Conway.Test.Examples.SucceedIfNumber.html#2105}{\htmlId{6555}{\htmlClass{Function}{\text{initStateDatum}}}}\, \\ \,\htmlId{6572}{\htmlClass{Number}{\text{0}}}\, \\ \,\href{Class.HasEmptySet.html#287}{\htmlId{6576}{\htmlClass{Field}{\text{∅}}}}\, \\ \,\htmlId{6580}{\htmlClass{Number}{\text{0}}}\, \end{pmatrix}$  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 $\begin{pmatrix} \,\href{Ledger.Conway.Test.Examples.SucceedIfNumber.html#2209}{\htmlId{6810}{\htmlClass{Function}{\text{initStateRedeemer}}}}\, \\ \,\htmlId{6830}{\htmlClass{Number}{\text{0}}}\, \\ \,\href{Class.HasEmptySet.html#287}{\htmlId{6834}{\htmlClass{Field}{\text{∅}}}}\, \\ \,\htmlId{6838}{\htmlClass{Number}{\text{0}}}\, \end{pmatrix}$  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 $\begin{pmatrix} \,\href{Ledger.Conway.Test.Examples.SucceedIfNumber.html#2209}{\htmlId{7051}{\htmlClass{Function}{\text{initStateRedeemer}}}}\, \\ \,\htmlId{7071}{\htmlClass{Number}{\text{0}}}\, \\ \,\href{Class.HasEmptySet.html#287}{\htmlId{7075}{\htmlClass{Field}{\text{∅}}}}\, \\ \,\htmlId{7079}{\htmlClass{Number}{\text{0}}}\, \end{pmatrix}$ failTx of λ where
    (success x) → true
    (failure x) → false

  _ : failExampleS ≡ true
  _ = refl

  failExampleU : Bool
  failExampleU = case compute Computational-UTXO initEnv $\begin{pmatrix} \,\href{Ledger.Conway.Test.Examples.SucceedIfNumber.html#2209}{\htmlId{7268}{\htmlClass{Function}{\text{initStateRedeemer}}}}\, \\ \,\htmlId{7288}{\htmlClass{Number}{\text{0}}}\, \\ \,\href{Class.HasEmptySet.html#287}{\htmlId{7292}{\htmlClass{Field}{\text{∅}}}}\, \\ \,\htmlId{7296}{\htmlClass{Number}{\text{0}}}\, \end{pmatrix}$ failTx of λ where
    (success x) → true
    (failure x) → false

  _ : failExampleU ≡ false
  _ = refl