Merge pull request #807 from zkFold/allow-null-txs

feat: allow for null transactions

Author: vlasin

symbolic-ledger/bench/CircuitSize.hs

@@ -49,4 +49,5 @@ main =
       [ goldenCircuit "Ledger.1.1.2.1.1.1.1" (ledgerCircuit @1 @1 @2 @1 @1 @1 @1 @RollupBFInterpreter)
       , goldenCircuit "Ledger.1.1.2.1.1.1.2" (ledgerCircuit @1 @1 @2 @1 @1 @1 @2 @RollupBFInterpreter)
       , goldenCircuit "Ledger.1.1.4.1.1.1.2" (ledgerCircuit @1 @1 @4 @1 @1 @1 @2 @RollupBFInterpreter)
+      , goldenCircuit "Ledger.1.1.2.2.2.2.2" (ledgerCircuit @1 @1 @2 @2 @2 @2 @2 @RollupBFInterpreter)
       ]

symbolic-ledger/src/ZkFold/Symbolic/Ledger/Examples/Four.hs

@@ -0,0 +1,81 @@
+{-# OPTIONS_GHC -Wno-missing-signatures #-}
+
+-- | Example demonstrating that null transactions can be used as batch padding.
+-- A "null transaction" has all null inputs and all null outputs. It is a pure
+-- no-op on the UTxO state and passes validation.
+module ZkFold.Symbolic.Ledger.Examples.Four (
+  prevState,
+  batch,
+  witness,
+  newState,
+  utxoPreimage2,
+  tx1,
+  nullTx,
+  sigs,
+  bridgedIn,
+  I,
+  Bi,
+  Bo,
+  Ud,
+  A,
+  Ixs,
+  Oxs,
+  TxCount,
+) where
+
+import Control.Applicative (pure)
+import GHC.Generics ((:*:) (..), (:.:) (..))
+import GHC.IsList (IsList (..))
+import ZkFold.Symbolic.Data.Bool (false)
+
+import ZkFold.Symbolic.Ledger.Examples.One (
+  A,
+  Bi,
+  Bo,
+  I,
+  Ixs,
+  Oxs,
+  Ud,
+  bridgedIn,
+  prevState,
+  privateKey,
+  publicKey,
+  tx,
+ )
+import ZkFold.Symbolic.Ledger.Offchain.State.Update (updateLedgerState)
+import ZkFold.Symbolic.Ledger.Types
+import ZkFold.Symbolic.Ledger.Utils (unsafeToVector')
+
+-- | Batch of 2: one real transaction followed by one null transaction used as padding.
+type TxCount = 2
+
+-- | The real transaction (same as 'tx' from Examples.One).
+tx1 :: Transaction Ixs Oxs A I
+tx1 = tx
+
+-- | A null transaction: all null inputs and all null outputs.
+-- Intended as a padding transaction to fill a fixed-size batch.
+nullTx :: Transaction Ixs Oxs A I
+nullTx =
+  Transaction
+    { inputs = Comp1 (fromList [nullOutputRef])
+    , outputs = Comp1 (fromList [nullOutput @A @I :*: false])
+    }
+
+batch :: TransactionBatch Ixs Oxs A TxCount I
+batch = TransactionBatch {tbTransactions = unsafeToVector' [tx1, nullTx]}
+
+sigs =
+  let rPoint :*: s = signTransaction tx1 privateKey
+      -- Any signature works for the null transaction since its null inputs
+      -- skip signature verification (isNullUTxO = true).
+      dummyRPoint :*: dummyS = rPoint :*: s
+   in Comp1
+        ( unsafeToVector'
+            [ Comp1 (fromList [rPoint :*: s :*: publicKey])
+            , Comp1 (fromList [dummyRPoint :*: dummyS :*: publicKey])
+            ]
+        )
+
+newState :*: witness :*: utxoPreimage2 =
+  updateLedgerState prevState (pure (nullUTxO @A @I)) bridgedIn batch sigs

symbolic-ledger/src/ZkFold/Symbolic/Ledger/Examples/One.hs

@@ -17,6 +17,8 @@ module ZkFold.Symbolic.Ledger.Examples.One (
   tx2,
   sigs2,
   bridgedIn2,
+  privateKey,
+  publicKey,
   I,
   Bi,
   Bo,

symbolic-ledger/src/ZkFold/Symbolic/Ledger/Validation/State.hs

@@ -44,7 +44,7 @@ For validating transactions, we should check:
 \* Bridged out outputs are checked to be same as in bridge out list.
 \* Outputs (bridged out or not) must have at least one ada and all assets are non-negative.
 \* Transaction is balanced.
-\* Transaction must have at least one input.
+\* Transaction must have at least one input OR the entire transaction is null (no inputs & no outputs)
 \* Bridged out output is not a null output.
 
 For validating batch, we simply apply transaction validation check iteratively.

symbolic-ledger/src/ZkFold/Symbolic/Ledger/Validation/Transaction.hs

@@ -26,7 +26,7 @@ import ZkFold.Algebra.Class (
 import ZkFold.Control.Conditional (ifThenElse)
 import ZkFold.Data.Eq
 import ZkFold.Data.HFunctor.Classes (HShow)
-import ZkFold.Data.Ord ((>=))
+import ZkFold.Data.Ord ((>), (>=))
 import ZkFold.Data.Vector (Vector, Zip (..))
 import ZkFold.Data.Vector qualified as Vector
 import ZkFold.Prelude (foldl')
@@ -251,9 +251,9 @@ validateTransaction utxoTree bridgedOutOutputs tx txw =
           true
           outputsAssets
     inputsWithWitness = zipWith (:*:) (unComp1 tx.inputs) (unComp1 txw.twInputs)
-    (isInsValid :*: consumedAtleastOneInput :*: updatedUTxOTreeForInputs) =
+    (isInsValid :*: updatedUTxOTreeForInputs) =
       foldl'
-        ( \(isInsValidAcc :*: consumedAtleastOneAcc :*: acc) (inputRef :*: (merkleEntry :*: utxo :*: rPoint :*: s :*: publicKey)) ->
+        ( \(isInsValidAcc :*: acc) (inputRef :*: (merkleEntry :*: utxo :*: rPoint :*: s :*: publicKey)) ->
             let
               nullUTxOHash' = nullUTxOHash @a @context
               utxoHash :: HashSimple context = hash utxo & Base.hHash
@@ -280,12 +280,9 @@ validateTransaction utxoTree bridgedOutOutputs tx txw =
                           (rPoint :*: s)
                     )
              in
-              ( isValid'
-                  :*: (consumedAtleastOneAcc || not isNullUTxO)
-                  :*: updatedTree
-              )
+              (isValid' :*: updatedTree)
         )
-        ((true :: Bool context) :*: (false :: Bool context) :*: utxoTree)
+        ((true :: Bool context) :*: utxoTree)
         inputsWithWitness
     outputsWithWitness = zipWith (:*:) (unComp1 tx.outputs) (unComp1 txw.twOutputs)
     (bouts :*: _ :*: outsValid :*: updatedUTxOTreeForOutputs) =
@@ -332,13 +329,13 @@ validateTransaction utxoTree bridgedOutOutputs tx txw =
         outputsWithWitness
    in
     ( bouts
-        :*: (outsValid && isInsValid && consumedAtleastOneInput && isBalanced)
+        :*: (outsValid && isInsValid && isBalanced) -- Note that we don't need to check if transaction consumes at least one input or is null entirely as our transaction currently only has two fields, namely, inputs & outputs and if thus inputs are null, outputs are null too.
         :*: updatedUTxOTreeForOutputs
     )
 
 -- | Check if output has sane value.
 --
--- We check if the output has at least one ada and all assets are non-negative.
+-- We check if the output has at least one ada and all non-null assets have strictly positive quantity.
 outputHasValueSanity
   :: forall a context
    . (KnownRegistersAssetQuantity context, Symbolic context)
@@ -357,7 +354,7 @@ outputHasValueSanity output =
                          >= fromConstant @Haskell.Integer 1_000_000
                      )
               )
-                :*: (allNonNegAcc && (asset.assetQuantity >= zero))
+                :*: (allNonNegAcc && (asset.assetQuantity > zero || (asset.assetPolicy == zero && asset.assetName == zero)))
           )
           (false :*: true)
           (unComp1 (oAssets output))

symbolic-ledger/stats/Ledger.1.1.2.1.1.1.1

@@ -1,5 +1,5 @@
 Ledger.1.1.2.1.1.1.1
-Number of polynomial constraints: 48735
-Number of variables: 50041
+Number of polynomial constraints: 48740
+Number of variables: 50050
 Number of lookup constraints: 1271
 Number of lookup tables: 9

symbolic-ledger/stats/Ledger.1.1.2.1.1.1.2

@@ -1,5 +1,5 @@
 Ledger.1.1.2.1.1.1.2
-Number of polynomial constraints: 81497
-Number of variables: 84064
+Number of polynomial constraints: 81504
+Number of variables: 84077
 Number of lookup constraints: 2500
 Number of lookup tables: 9

symbolic-ledger/stats/Ledger.1.1.2.2.2.2.2

@@ -0,0 +1,5 @@
+Ledger.1.1.2.2.2.2.2
+Number of polynomial constraints: 190858
+Number of variables: 196576
+Number of lookup constraints: 5736
+Number of lookup tables: 9

symbolic-ledger/stats/Ledger.1.1.4.1.1.1.2

@@ -1,5 +1,5 @@
 Ledger.1.1.4.1.1.1.2
-Number of polynomial constraints: 125747
-Number of variables: 128392
+Number of polynomial constraints: 125754
+Number of variables: 128405
 Number of lookup constraints: 2500
 Number of lookup tables: 9

symbolic-ledger/symbolic-ledger.cabal

@@ -96,6 +96,7 @@ library
   import: options
   exposed-modules:
     ZkFold.Symbolic.Ledger.Circuit.Compile
+    ZkFold.Symbolic.Ledger.Examples.Four
     ZkFold.Symbolic.Ledger.Examples.One
     ZkFold.Symbolic.Ledger.Examples.Three
     ZkFold.Symbolic.Ledger.Examples.Two
@@ -140,6 +141,7 @@ test-suite symbolic-ledger-test
     Tests.Symbolic.Ledger.E2E.Compile.One
     Tests.Symbolic.Ledger.E2E.Compile.Three
     Tests.Symbolic.Ledger.E2E.Compile.Two
+    Tests.Symbolic.Ledger.E2E.Four
     Tests.Symbolic.Ledger.E2E.One
     Tests.Symbolic.Ledger.E2E.Three
     Tests.Symbolic.Ledger.E2E.Two