Open
{-# OPTIONS --safe #-}
module Test.Examples.MultiSigV2.OffChain.Open where
open import Ledger.Prelude
open import Ledger.Conway.Specification.Transaction
open import Test.Examples.MultiSigV2.Datum
open import Test.Examples.MultiSigV2.OffChain.Lib
open import Test.Examples.MultiSigV2.Validator
open import Test.Prelude MultiSigData
open import Test.SymbolicData MultiSigData
open import Test.LedgerImplementation SData SData
open import Test.AbstractImplementation valContext
open import Test.Lib valContext
open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions
open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions
open TransactionStructure SVTransactionStructure
open Implementation
openTxOut : Value → PlutusScript → TxOut
openTxOut v script = inj₁ (record { net = 0 ;
pay = ScriptObj (proj₁ script) ;
stake = just (ScriptObj (proj₁ script)) })
, v
, just (inj₁ (inj₁ (inj₁ Holding))) , nothing
openTx : (id w v tw : ℕ) → PlutusScript → Tx
openTx id w v tw script = record { body = record defaultTxBody
{ txIns = Ledger.Prelude.fromList ((w , w) ∷ [])
; txOuts = fromListIx ((tw , openTxOut v script)
∷ (w
, ((inj₁ (record { net = 0 ;
pay = KeyHashObj w ;
stake = just (KeyHashObj w) }))
, ((1000000000000 - 10000000000) - v) , nothing , nothing))
∷ [])
; txId = id
; collateralInputs = Ledger.Prelude.fromList ((w , w) ∷ [])
} ;
wits = record { vkSigs = fromListᵐ ((w , (_+_ {{addValue}} w id)) ∷ []) ;
scripts = ∅ ;
txdats = ∅ ;
txrdmrs = ∅ } ;
txsize = 10 ;
isValid = true ;
txAD = nothing }