Adding Example Smart Contracts and Traces.

src/Ledger/Conway/Foreign/HSLedger/ExternalStructures.agda

@@ -127,6 +127,7 @@ instance
     ; scriptSize = λ where 
         (inj₁ x) → HSTimelock.tlScriptSize x
         (inj₂ x) → HSPlutusScript.psScriptSize x
+    ; valContext = λ _ _ → zero
     }
 
 open import Ledger.Core.Specification.Address Network KeyHash ScriptHash using () public

src/Ledger/Conway/Specification/Abstract.agda

@@ -7,6 +7,7 @@ module Ledger.Conway.Specification.Abstract (txs : TransactionStructure) where
 
 open TransactionStructure txs
 open import Ledger.Conway.Specification.Certs govStructure
+open import Ledger.Conway.Specification.Script.ScriptPurpose txs
 
 record indexOf : Type where
   field
@@ -23,3 +24,4 @@ record AbstractFunctions : Type where
         indexOfImp   : indexOf
         runPLCScript : CostModel → P2Script → ExUnits → List Data → Bool
         scriptSize   : Script → ℕ
+        valContext   : TxInfo → ScriptPurpose → Data

src/Ledger/Conway/Specification/Script/Base.lagda.md

@@ -56,7 +56,7 @@ record PlutusStructure : Type₁ where
   field validPlutusScript : CostModel → List Data → ExUnits → PlutusScript → Type
         ⦃ Dec-validPlutusScript ⦄ : ∀ {x} → (validPlutusScript x ⁇³)
         language : PlutusScript → Language
-        toData : ∀ {A : Type} → A → Data
+       -- toData : ∀ {A : Type} → A → Data
 
 record ScriptStructure : Type₁ where
 

src/Ledger/Conway/Specification/Script/ScriptPurpose.lagda.md

@@ -0,0 +1,42 @@
+---
+source_branch: master
+source_path: src/Ledger/Conway/Specification/Script/ScriptPurpose.lagda.md
+---
+
+# Script Purpose {#sec:script-purpose}
+
+<!--
+```agda
+{-# OPTIONS --safe #-}
+
+open import Ledger.Conway.Specification.Transaction
+
+module Ledger.Conway.Specification.Script.ScriptPurpose (txs : TransactionStructure) where
+
+open import Ledger.Prelude
+open TransactionStructure txs
+open import Ledger.Conway.Specification.Certs govStructure
+```
+-->
+
+```agda
+data ScriptPurpose : Type where
+  Cert     : DCert        → ScriptPurpose
+  Rwrd     : RwdAddr      → ScriptPurpose
+  Mint     : ScriptHash   → ScriptPurpose
+  Spend    : TxIn         → ScriptPurpose
+  Vote     : GovVoter     → ScriptPurpose
+  Propose  : GovProposal  → ScriptPurpose
+
+record TxInfo : Type where
+  field realizedInputs : UTxO
+        txOuts         : Ix ⇀ TxOut
+        fee            : Value
+        mint           : Value
+        txCerts        : List DCert
+        txWithdrawals  : Withdrawals
+        txVldt         : Maybe Slot × Maybe Slot
+        vkKey          : ℙ KeyHash
+        txdats         : ℙ Datum
+        txId           : TxId
+```

src/Ledger/Conway/Specification/Script/Validation.lagda.md

@@ -17,13 +17,8 @@ module Ledger.Conway.Specification.Script.Validation
 open import Ledger.Prelude
 open import Ledger.Conway.Specification.Certs govStructure
 
-data ScriptPurpose : Type where
-  Cert     : DCert        → ScriptPurpose
-  Rwrd     : RwdAddr      → ScriptPurpose
-  Mint     : ScriptHash   → ScriptPurpose
-  Spend    : TxIn         → ScriptPurpose
-  Vote     : GovVoter     → ScriptPurpose
-  Propose  : GovProposal  → ScriptPurpose
+open import Ledger.Conway.Specification.Abstract txs
+open import Ledger.Conway.Specification.Script.ScriptPurpose txs
 
 rdptr : TxBody → ScriptPurpose → Maybe RdmrPtr
 rdptr txb = λ where
@@ -51,18 +46,6 @@ getDatum tx utxo (Spend txin) =
        m = setToMap (mapˢ < hash , id > (TxWitnesses.txdats (Tx.wits tx)))
 getDatum tx utxo _ = nothing
 
-record TxInfo : Type where
-  field realizedInputs : UTxO
-        txOuts         : Ix ⇀ TxOut
-        fee            : Value
-        mint           : Value
-        txCerts        : List DCert
-        txWithdrawals  : Withdrawals
-        txVldt         : Maybe Slot × Maybe Slot
-        vkKey          : ℙ KeyHash
-        txdats         : ℙ Datum
-        txId           : TxId
-
 txInfo : Language → PParams
                   → UTxO
                   → Tx
@@ -92,8 +75,8 @@ credsNeeded utxo txb
     open RwdAddr
     open GovProposal
 
-valContext : TxInfo → ScriptPurpose → Data
-valContext txinfo sp = toData (txinfo , sp)
+-- valContext : TxInfo → ScriptPurpose → Data
+-- valContext txinfo sp = toData (txinfo , sp)
 
 txOutToDataHash : TxOut → Maybe DataHash
 txOutToDataHash (_ , _ , d , _) = d >>= isInj₂

src/Ledger/Conway/Specification/Test/AbstractImplementation.agda

@@ -0,0 +1,37 @@
+{-# OPTIONS --safe #-}
+
+open import Ledger.Prelude using (DecEq; Show)
+import Ledger.Conway.Specification.Script.ScriptPurpose as SP
+open import Ledger.Conway.Specification.Test.LedgerImplementation using (SVTransactionStructure)
+
+module Ledger.Conway.Specification.Test.AbstractImplementation
+  {T D : Set} {{DecEq-Data : DecEq D}} {{Show-Data : Show D}}
+  (open SP (SVTransactionStructure T D) using (TxInfo; ScriptPurpose))
+  (valContext' : TxInfo → ScriptPurpose → D)
+  where
+
+open import Ledger.Prelude using (nothing; _,_)
+
+open import Ledger.Conway.Specification.Test.LedgerImplementation T D
+  renaming (SVTransactionStructure to SVTransactionStructure')
+open import Ledger.Conway.Specification.Abstract SVTransactionStructure'
+
+open Implementation
+
+SVAbstractFunctions : AbstractFunctions
+SVAbstractFunctions = record
+  { Implementation
+  ; txscriptfee = λ tt y → 0
+  ; serSize     = λ v → 0 -- changed to 0
+  ; indexOfImp  = record
+    { indexOfDCert    = λ _ _ → nothing
+    ; indexOfRwdAddr  = λ _ _ → nothing
+    ; indexOfTxIn     = indexOfTxInImp
+    ; indexOfPolicyId = λ _ _ → nothing
+    ; indexOfVote     = λ _ _ → nothing
+    ; indexOfProposal = λ _ _ → nothing
+    }
+  ; runPLCScript = λ { x (sh , script) x₂ x₃ → script x₃ }
+  ; scriptSize = λ _ → 0
+  ; valContext = valContext'
+  }

src/Ledger/Conway/Specification/Test/Examples.agda

@@ -1,5 +1,18 @@
 {-# OPTIONS --safe #-}
+
 module Ledger.Conway.Specification.Test.Examples where
 
 import Ledger.Conway.Specification.Test.Examples.SucceedIfNumber
 import Ledger.Conway.Specification.Test.Examples.HelloWorld
+import Ledger.Conway.Specification.Test.Examples.MultiSig.Datum
+import Ledger.Conway.Specification.Test.Examples.MultiSig.Validator
+import Ledger.Conway.Specification.Test.Examples.MultiSig.Test.Trace
+import Ledger.Conway.Specification.Test.Examples.AccountSim.Datum
+import Ledger.Conway.Specification.Test.Examples.AccountSim.Validator
+import Ledger.Conway.Specification.Test.Examples.AccountSim.Test.Trace
+import Ledger.Conway.Specification.Test.Examples.DEx.Datum
+import Ledger.Conway.Specification.Test.Examples.DEx.Validator
+import Ledger.Conway.Specification.Test.Examples.DEx.Test.Trace
+import Ledger.Conway.Specification.Test.Examples.MultiSigV2.Datum
+import Ledger.Conway.Specification.Test.Examples.MultiSigV2.Validator
+import Ledger.Conway.Specification.Test.Examples.MultiSigV2.Test.Trace

src/Ledger/Conway/Specification/Test/Examples/AccountSim/Datum.agda

@@ -0,0 +1,30 @@
+{-# OPTIONS --safe #-}
+
+open import Ledger.Prelude hiding (fromList; ε); open Computational
+
+module Ledger.Conway.Specification.Test.Examples.AccountSim.Datum where
+
+open import Tactic.Derive.DecEq
+open import Data.Vec as Vec
+  hiding (fromList)
+import stdlib.Data.Vec.Instances as Vec
+import Data.Vec.Relation.Binary.Pointwise.Inductive as Vec
+
+data Label : Set where
+  Always : List (ℕ × ℕ) -> Label 
+instance
+  unquoteDecl DecEq-Label = derive-DecEq
+    ((quote Label , DecEq-Label) ∷ [])
+
+data Input : Set where
+  Open     : ℕ -> Input
+  Close    : ℕ -> Input
+  Withdraw : ℕ -> ℕ -> Input
+  Deposit  : ℕ -> ℕ -> Input
+  Transfer : ℕ -> ℕ -> ℕ -> Input
+  Cleanup  : Input
+instance
+  unquoteDecl DecEq-Input = derive-DecEq
+    ((quote Input , DecEq-Input) ∷ [])
+
+AccountSimData = Label ⊎ Input

src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Cleanup.agda

@@ -0,0 +1,49 @@
+{-# OPTIONS --safe #-}
+
+module Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.Cleanup where
+
+open import Ledger.Prelude
+open import Ledger.Conway.Specification.Transaction
+
+open import Ledger.Conway.Specification.Test.Examples.AccountSim.Datum
+open import Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.Lib
+open import Ledger.Conway.Specification.Test.Examples.AccountSim.Validator
+open import Ledger.Conway.Specification.Test.Prelude AccountSimData
+open import Ledger.Conway.Specification.Test.SymbolicData AccountSimData
+open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData
+open import Ledger.Conway.Specification.Test.AbstractImplementation valContext
+open import Ledger.Conway.Specification.Test.Lib valContext
+
+open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions
+
+open TransactionStructure SVTransactionStructure
+open Implementation
+
+makeCleanupTx : (id : ℕ) → UTxOState → PlutusScript → (w : ℕ) → Maybe Tx
+makeCleanupTx id state script@(sh , _) w = 
+  let
+    wutxo = getWalletUTxO w (UTxOState.utxo state)
+  in
+    maybe (λ { (scIn , (fst , txValue , snd)) →
+    just (
+          record { body = record defaultTxBody
+                         { txIns = Ledger.Prelude.fromList ((scIn ∷ []) ++ (map proj₁ wutxo))
+                         ; txOuts = fromListIx (makeFeeUnPaymentTxOut wutxo txValue)
+                         ; txId = id
+                         ; collateralInputs = Ledger.Prelude.fromList (map proj₁ wutxo)
+                         ; reqSignerHashes = Ledger.Prelude.fromList (w ∷ [])
+                         } ;
+                wits = record { vkSigs = fromListᵐ ((w , (_+_ {{addNat}} (getTxId wutxo) w) ) ∷ []) ;
+                                scripts = Ledger.Prelude.fromList ((inj₂ script) ∷ []) ;
+                                txdats = ∅ ; 
+                                txrdmrs = fromListᵐ (((Spend , (proj₂ scIn)) ,
+                                                      inj₁ (inj₂ Cleanup) ,
+                                                      ((getTxId wutxo) , w)) ∷ []) } ;
+                txsize = 10 ;
+                isValid = true ;
+                txAD = nothing }
+                )
+            })
+          nothing
+          (getScriptUTxO sh (UTxOState.utxo state))
+

src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Close.agda

@@ -0,0 +1,55 @@
+{-# OPTIONS --safe #-}
+
+module Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.Close where
+
+open import Ledger.Prelude
+open import Ledger.Conway.Specification.Transaction
+
+open import Ledger.Conway.Specification.Test.Examples.AccountSim.Datum
+open import Ledger.Conway.Specification.Test.Examples.AccountSim.Validator
+open import Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.Lib
+open import Ledger.Conway.Specification.Test.Prelude AccountSimData
+open import Ledger.Conway.Specification.Test.SymbolicData AccountSimData
+open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData
+open import Ledger.Conway.Specification.Test.AbstractImplementation valContext
+open import Ledger.Conway.Specification.Test.Lib valContext
+
+open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions
+
+open TransactionStructure SVTransactionStructure
+open Implementation
+
+
+makeCloseTxOut : Label → (scriptIx w : ℕ) → TxOut → List (ℕ × TxOut)
+makeCloseTxOut (Always l) ix w (fst , fst' , snd) =
+  (ix , (fst , fst' ,  just (inj₁ (inj₁ (inj₁ (Always (delete' w l))))) , nothing)) ∷ []
+
+makeCloseTx : (id : ℕ) → UTxOState → PlutusScript → (w : ℕ) → Maybe Tx
+makeCloseTx id state script@(sh , _) w =
+  let
+    wutxo = getWalletUTxO w (UTxOState.utxo state)
+  in
+    maybe (λ { (scIn , scOut) → maybe (λ label →
+    just (
+          record { body = record defaultTxBody
+                         { txIns = Ledger.Prelude.fromList ((scIn ∷ []) ++ (map proj₁ wutxo))
+                         ; txOuts = fromListIx (makeFeeTxOut wutxo ++ makeCloseTxOut label (proj₂ scIn) w scOut )
+                         ; txId = id
+                         ; collateralInputs = Ledger.Prelude.fromList (map proj₁ wutxo)
+                         ; reqSignerHashes = Ledger.Prelude.fromList (w ∷ [])
+                         } ;
+                wits = record { vkSigs = fromListᵐ ((w , (_+_ {{addNat}} (getTxId wutxo) w) ) ∷ []) ;
+                                scripts = Ledger.Prelude.fromList ((inj₂ script) ∷ []) ;
+                                txdats = ∅ ;
+                                txrdmrs = fromListᵐ (((Spend , (proj₂ scIn)) ,
+                                                      inj₁ (inj₂ (Close w)) ,
+                                                      ((getTxId wutxo) , w)) ∷ []) } ;
+                txsize = 10 ;
+                isValid = true ;
+                txAD = nothing }
+                ))
+            nothing
+            (getLabel scOut)})
+          nothing
+          (getScriptUTxO sh (UTxOState.utxo state))
+

src/Ledger/Conway/Specification/Test/Examples/AccountSim/OffChain/Deposit.agda

@@ -0,0 +1,63 @@
+{-# OPTIONS --safe #-}
+
+module Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.Deposit where
+
+open import Ledger.Prelude
+open import Ledger.Conway.Specification.Transaction
+
+open import Ledger.Conway.Specification.Test.Examples.AccountSim.Datum
+open import Ledger.Conway.Specification.Test.Examples.AccountSim.OffChain.Lib
+open import Ledger.Conway.Specification.Test.Examples.AccountSim.Validator
+open import Ledger.Conway.Specification.Test.Prelude AccountSimData
+open import Ledger.Conway.Specification.Test.SymbolicData AccountSimData
+open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData
+open import Ledger.Conway.Specification.Test.AbstractImplementation valContext
+open import Ledger.Conway.Specification.Test.Lib valContext
+
+open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions
+
+open TransactionStructure SVTransactionStructure
+open Implementation
+
+scriptDTxOut : Label → TxOut → (w : ℕ) → (v : Value) → TxOut
+scriptDTxOut (Always l) (fst , txValue , snd) w v = (fst , (_+_ {{addValue}} txValue v) , (just (inj₁ (inj₁ (inj₁ (Always (insert' w (_+_ {{addValue}} val v) l)))))) , nothing)
+  where
+    val = getVal (Always l) w
+
+
+
+makeDepositTxOut : Label → (scriptIx : ℕ) → TxOut → (w : ℕ) → (v : Value) → List (ℕ × TxOut)
+makeDepositTxOut (Always l) ix txo w v =
+            (ix , scriptDTxOut (Always l) txo w v)
+            ∷ []
+
+
+
+makeDepositTx : (id : ℕ) → UTxOState → PlutusScript → (w : ℕ) → (v : Value) → Maybe Tx
+makeDepositTx id state script@(sh , _) w v =
+  let
+    wutxo = getWalletUTxO w (UTxOState.utxo state)
+  in
+    maybe (λ { (scIn , scOut) → maybe (λ label →
+    just (
+          record { body = record defaultTxBody
+                         { txIns = Ledger.Prelude.fromList ((scIn ∷ []) ++ (map proj₁ wutxo))
+                         ; txOuts = fromListIx (makeFeePaymentTxOut wutxo v ++ makeDepositTxOut label (proj₂ scIn) scOut w v )
+                         ; txId = id
+                         ; collateralInputs = Ledger.Prelude.fromList (map proj₁ wutxo)
+                         ; reqSignerHashes = Ledger.Prelude.fromList (w ∷ [])
+                         } ;
+                wits = record { vkSigs = fromListᵐ ((w , (_+_ {{addNat}} (getTxId wutxo) w)) ∷ []) ;
+                                scripts = Ledger.Prelude.fromList ((inj₂ script) ∷ []) ;
+                                txdats = ∅ ;
+                                txrdmrs = fromListᵐ (((Spend , (proj₂ scIn)) ,
+                                                      inj₁ (inj₂ (Deposit w v)) ,
+                                                      ((getTxId wutxo) , w)) ∷ []) } ;
+                txsize = 10 ;
+                isValid = true ;
+                txAD = nothing }
+                ))
+            nothing
+            (getLabel scOut)})
+          nothing
+          (getScriptUTxO sh (UTxOState.utxo state))