Alasdair/multi sig v2

.gitignore

@@ -30,6 +30,7 @@ result*
 ## git-merge conflict resolution artifacts
 *.agda.orig
 *.lagda.orig
+*.agdai
 
 ## Python
 build-tools/scripts/md/__pycache__/

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

@@ -50,7 +50,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/Validation.agda

@@ -1,7 +1,7 @@
 {-# OPTIONS --safe #-}
 
 open import Ledger.Conway.Specification.Transaction
-open import Ledger.Conway.Specification.Abstract
+open import Ledger.Conway.Specification.Abstract using (AbstractFunctions; indexOf)
 
 module Ledger.Conway.Specification.Script.Validation
   (txs : _) (open TransactionStructure txs)
@@ -10,14 +10,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     : Voter        → ScriptPurpose
-  Propose  : GovProposal  → ScriptPurpose
+open import Ledger.Conway.Specification.Abstract txs
+open import Ledger.Conway.Specification.ScriptPurpose txs
 
 rdptr : TxBody → ScriptPurpose → Maybe RdmrPtr
 rdptr txb = λ where
@@ -45,18 +39,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
-        txwdrls : Wdrl
-        txvldt  : Maybe Slot × Maybe Slot
-        vkKey   : ℙ KeyHash
-        txdats  : ℙ Datum
-        txid    : TxId
-
 txInfo : Language → PParams
                   → UTxO
                   → Tx
@@ -85,8 +67,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/ScriptPurpose.agda

@@ -0,0 +1,29 @@
+{-# OPTIONS --safe #-}
+
+open import Ledger.Prelude
+open import Ledger.Conway.Specification.Transaction
+
+module Ledger.Conway.Specification.ScriptPurpose (txs : TransactionStructure) where
+
+open TransactionStructure txs
+open import Ledger.Conway.Specification.Certs govStructure
+
+data ScriptPurpose : Type where
+  Cert     : DCert        → ScriptPurpose
+  Rwrd     : RwdAddr      → ScriptPurpose
+  Mint     : ScriptHash   → ScriptPurpose
+  Spend    : TxIn         → ScriptPurpose
+  Vote     : Voter        → ScriptPurpose
+  Propose  : GovProposal  → ScriptPurpose
+
+record TxInfo : Type where
+  field realizedInputs : UTxO
+        txouts  : Ix ⇀ TxOut
+        fee     : Value
+        mint    : Value
+        txcerts : List DCert
+        txwdrls : Wdrl
+        txvldt  : Maybe Slot × Maybe Slot
+        vkKey   : ℙ KeyHash
+        txdats  : ℙ Datum
+        txid    : TxId

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

@@ -0,0 +1,36 @@
+{-# OPTIONS --safe #-}
+
+open import Ledger.Prelude hiding (fromList; ε); open Computational
+open import Ledger.Conway.Specification.Test.Prelude
+open import Ledger.Conway.Specification.Transaction using (TransactionStructure)
+open import Ledger.Conway.Specification.Test.LedgerImplementation using (SVTransactionStructure)
+open import Ledger.Conway.Specification.ScriptPurpose using ()
+
+module Ledger.Conway.Specification.Test.AbstractImplementation (T D : Set){{DecEq-Data : DecEq D}}{{Show-Data : Show D}}
+  (open TransactionStructure (SVTransactionStructure T D))
+  (open Ledger.Conway.Specification.ScriptPurpose (SVTransactionStructure T D))
+  (valContext' : TxInfo → ScriptPurpose → D)
+  where
+
+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,9 @@
 {-# 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

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

@@ -1,18 +1,22 @@
 {-# OPTIONS --safe #-}
 
 open import Ledger.Prelude hiding (fromList; ε); open Computational
-open import Ledger.Conway.Specification.Test.Prelude
 
+open import Ledger.Conway.Specification.Test.Prelude (String)
 module Ledger.Conway.Specification.Test.Examples.HelloWorld where
+open import Ledger.Conway.Specification.Test.LedgerImplementation String String
+open import Ledger.Conway.Specification.Transaction using (TransactionStructure)
+open TransactionStructure SVTransactionStructure using (Data)
+open import Ledger.Conway.Specification.ScriptPurpose SVTransactionStructure
 
-scriptImp : ScriptImplementation String String
-scriptImp = record { serialise = id ;
-                     deserialise = λ x → just x ;
-                     toData' = λ x → "dummy" }
 
-open import Ledger.Conway.Specification.Test.LedgerImplementation String String scriptImp
-open import Ledger.Conway.Specification.Test.Lib String String scriptImp
+valContext : TxInfo → ScriptPurpose → Data
+valContext x x₁ = ""
+
+open import Ledger.Conway.Specification.Test.AbstractImplementation String String valContext
+open import Ledger.Conway.Specification.Test.Lib String String valContext
 open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions
+open import Data.Empty
 open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions
 open import Ledger.Conway.Specification.Transaction
 open TransactionStructure SVTransactionStructure
@@ -21,6 +25,7 @@ open EpochStructure SVEpochStructure
 open Implementation
 open import Ledger.Conway.Specification.Utxo.Properties SVTransactionStructure SVAbstractFunctions
 
+
 -- true if redeemer is "Hello World"
 helloWorld' : Maybe String → Maybe String → Bool
 helloWorld' _ (just s) = ⌊ (s ≟ "Hello World") ⌋

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

@@ -0,0 +1,27 @@
+{-# OPTIONS --safe #-}
+
+open import Ledger.Prelude hiding (fromList; ε); open Computational
+
+module Ledger.Conway.Specification.Test.Examples.MultiSig.Datum where
+
+open import Tactic.Derive.DecEq
+
+data Label : Set where
+  Holding : Label
+  Collecting : ℕ -> ℕ -> ℕ -> List ℕ -> Label
+instance
+  unquoteDecl DecEq-Label = derive-DecEq
+    ((quote Label , DecEq-Label) ∷ [])
+
+data Input : Set where
+  -- Propose: Ada amount, Target Wallet, Slot Deadline
+  Propose : ℕ -> ℕ -> ℕ -> Input
+  --  Add: Wallet signature to add
+  Add     : ℕ -> Input
+  Pay     : Input
+  Cancel  : Input
+instance
+  unquoteDecl DecEq-Input = derive-DecEq
+    ((quote Input , DecEq-Input) ∷ [])
+
+MultiSigData = Label ⊎ Input

src/Ledger/Conway/Specification/Test/Examples/MultiSig/OffChain/AddSig.agda

@@ -0,0 +1,65 @@
+{-# OPTIONS --safe #-}
+
+open import Ledger.Prelude hiding (fromList; ε); open Computational
+open import Ledger.Conway.Specification.Test.Examples.MultiSig.Datum
+open import Ledger.Conway.Specification.Test.Examples.MultiSig.Validator
+open import Ledger.Conway.Specification.Test.Prelude MultiSigData
+open import Ledger.Conway.Specification.Test.SymbolicData MultiSigData
+open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData
+open import Ledger.Conway.Specification.Transaction using (TransactionStructure)
+open TransactionStructure SVTransactionStructure
+open import Ledger.Conway.Specification.Test.AbstractImplementation SData SData valContext
+open import Ledger.Conway.Specification.Test.Lib SData SData valContext
+open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions
+open import Data.Empty
+open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions
+open import Ledger.Conway.Specification.Transaction
+open import Ledger.Core.Specification.Epoch
+open EpochStructure SVEpochStructure
+open Implementation
+open import Ledger.Conway.Specification.Utxo.Properties SVTransactionStructure SVAbstractFunctions
+open import Data.List using (filter)
+open import Ledger.Conway.Specification.Test.Examples.MultiSig.OffChain.Lib
+
+module Ledger.Conway.Specification.Test.Examples.MultiSig.OffChain.AddSig where
+
+-- TODO: Invesitgate what is going on with vkSigs vs reqSigHash in terms of
+-- transaction not failing vkSigs
+-- txinfo only gets reqSigHash
+
+makeAddSigTxOut : Label → (scriptIx w : ℕ) → TxOut → List (ℕ × TxOut)
+makeAddSigTxOut Holding ix w txo = []
+makeAddSigTxOut (Collecting vl pkh d sigs) ix w (fst , fst₁ , snd) =
+  (ix , (fst , fst₁ ,  just (inj₁ (inj₁ (inj₁ (Collecting vl pkh d (w ∷ sigs))))) , nothing)) ∷ []
+
+makeAddSigTx : (id : ℕ) → UTxOState → PlutusScript → (w : ℕ) → Maybe Tx
+makeAddSigTx 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 ++ makeAddSigTxOut label (proj₂ scIn) w scOut )
+                         ; txid = id
+                         ; collateral = Ledger.Prelude.fromList (map proj₁ wutxo)
+                         ; reqSigHash = Ledger.Prelude.fromList (w ∷ []) 
+                         } ;
+                wits = record { vkSigs = fromListᵐ ((w , (_+_ {{addValue}} (getTxId wutxo) w)) ∷ []) ;
+                                -- signature now is first number + txId ≡ second number
+                                -- first number is needs to be the id for the script
+                                scripts = Ledger.Prelude.fromList ((inj₂ script) ∷ []) ;
+                                txdats = ∅ ; -- fromListᵐ ((inj₁ (inj₁ Holding) , inj₁ (inj₁ Holding)) ∷ []) ;
+                                txrdmrs = fromListᵐ (((Spend , (proj₂ scIn)) ,
+                                                      inj₁ (inj₂ (Add 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/MultiSig/OffChain/Lib.agda

@@ -0,0 +1,93 @@
+{-# OPTIONS --safe #-}
+
+open import Ledger.Prelude hiding (fromList; ε); open Computational
+open import Ledger.Conway.Specification.Test.Examples.MultiSig.Datum
+open import Ledger.Conway.Specification.Test.Examples.MultiSig.Validator
+open import Ledger.Conway.Specification.Test.Prelude MultiSigData
+open import Ledger.Conway.Specification.Test.SymbolicData MultiSigData
+open import Ledger.Conway.Specification.Test.LedgerImplementation SData SData
+open import Ledger.Conway.Specification.Transaction using (TransactionStructure)
+open TransactionStructure SVTransactionStructure
+open import Ledger.Conway.Specification.Test.AbstractImplementation SData SData valContext
+open import Ledger.Conway.Specification.Test.Lib SData SData valContext
+open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions
+open import Data.Empty
+open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions
+open import Ledger.Conway.Specification.Transaction
+open import Ledger.Core.Specification.Epoch
+open EpochStructure SVEpochStructure
+open Implementation
+open import Ledger.Conway.Specification.Utxo.Properties SVTransactionStructure SVAbstractFunctions
+open import Data.List using (filter)
+
+module Ledger.Conway.Specification.Test.Examples.MultiSig.OffChain.Lib where
+
+open import Relation.Nullary
+
+defaultTxBody : TxBody
+defaultTxBody = record
+                  { txins = ∅
+                  ; refInputs = ∅
+                  ; txouts =  ∅
+                  ; txfee = 10000000000
+                  ; mint = 0
+                  ; txvldt = nothing , nothing
+                  ; txcerts = []
+                  ; txwdrls = ∅
+                  ; txvote = []
+                  ; txprop = []
+                  ; txdonation = 0
+                  ; txup = nothing
+                  ; txADhash = nothing
+                  ; txNetworkId = just 0
+                  ; curTreasury = nothing
+                  ; txid = 0
+                  ; collateral = ∅
+                  ; reqSigHash = ∅
+                  ; scriptIntHash = nothing
+                  }
+
+matchScriptAddress : (scriptHash : ℕ) → Credential → Set
+matchScriptAddress sh (KeyHashObj x) = ⊥
+matchScriptAddress sh (ScriptObj y) = True (sh ≟ y)
+
+matchScriptAddress? : (sh : ℕ) → (c : Credential) → Dec (matchScriptAddress sh c)
+matchScriptAddress? sh (KeyHashObj x) = no (λ x₁ → x₁)
+matchScriptAddress? sh (ScriptObj y) = T? ⌊ (sh ≟ y) ⌋
+
+getScriptUTxO : (scriptHash : ℕ) → UTxO → Maybe (TxIn × TxOut)
+getScriptUTxO sh (utxo , prf) = head $ filter (λ { (_ , addr , _) → matchScriptAddress? sh (payCred addr)}) (setToList utxo)
+
+matchWalletHash : (keyHash : ℕ) → Credential → Set
+matchWalletHash kh (KeyHashObj x) = True (kh ≟ x)
+matchWalletHash kh (ScriptObj y) = ⊥
+
+matchWalletHash? : (sh : ℕ) → (c : Credential) → Dec (matchWalletHash sh c)
+matchWalletHash? kh (KeyHashObj x) = T? ⌊ (kh ≟ x) ⌋
+matchWalletHash? kh (ScriptObj y) = no (λ x₁ → x₁)
+
+getWalletUTxO : (scriptHash : ℕ) → UTxO → List (TxIn × TxOut)
+getWalletUTxO sh (utxo , prf) = filter (λ { (_ , addr , _) → matchWalletHash? sh (payCred addr)}) (setToList utxo)
+
+succeedTxOut' : TxOut
+succeedTxOut' = inj₁ (record { net = 0 ;
+                           pay = ScriptObj 777 ;
+                           stake = just (ScriptObj 777) })
+                           , 700000000000 , just (inj₁ (inj₁ (inj₁ Holding))) , nothing
+
+getLabel : TxOut → Maybe Label
+getLabel (fst , fst₁ , just (inj₁ (inj₁ (inj₁ x))) , snd) = just x
+getLabel (fst , fst₁ , just (inj₁ (inj₁ (inj₂ y))) , snd) = nothing
+getLabel (fst , fst₁ , just (inj₁ (inj₂ y)) , snd) = nothing
+getLabel (fst , fst₁ , just (inj₂ y) , snd) = nothing
+getLabel (fst , fst₁ , nothing , snd) = nothing
+
+-- Assumes a list of filtered waller txins and subtracts a default fee from the head of the list
+makeFeeTxOut : List (TxIn × TxOut) → List (ℕ × TxOut)
+makeFeeTxOut [] = []
+makeFeeTxOut ((txin , (fst , txValue , snd)) ∷ utxos) = (proj₂ txin , fst , txValue - 10000000000 , snd) ∷ []
+
+-- return id of 0 if no txins
+getTxId : List (TxIn × TxOut) → ℕ
+getTxId xs = maybe (λ x → proj₁ (proj₁ x)) 0 (head xs)
+