feat: bump constraint limit to 2^20

symbolic-base/src/ZkFold/Protocol/NonInteractiveProof/TrustedSetup.hs

@@ -1,3 +1,5 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeOperators #-}
 
 module ZkFold.Protocol.NonInteractiveProof.TrustedSetup (
@@ -41,10 +43,14 @@ data TrustedSetup (n :: Natural)
 powersOfTau2e18p6 :: IO (TrustedSetup (2 ^ 18 + 6))
 powersOfTau2e18p6 = powersOfTauSubset
 
--- | Read no more than 2^18 + 6 G1 points and both G2 points from the Midnight trusted setup.
+-- | Read no more than 2^20 + 6 G1 points and both G2 points from the Midnight trusted setup.
 powersOfTauSubset :: forall (n :: Natural). KnownNat n => IO (TrustedSetup n)
 powersOfTauSubset = do
-  fp <- getDataFileName "data/midnight_powers_of_tau_2e18"
+  let n = value @n
+  fp <-
+    if n P.<= 2 P.^ 18 P.+ 6
+      then getDataFileName "data/midnight_powers_of_tau_2e18"
+      else getDataFileName "data/midnight_powers_of_tau_2e20"
   Just ts <- readTrustedSetup fp True
   P.pure ts
 

symbolic-base/symbolic-base.cabal

@@ -14,6 +14,7 @@ build-type:         Custom
 Data-Files:
     test/data/shabittestvectors/*.rsp
     data/midnight_powers_of_tau_2e18
+    data/midnight_powers_of_tau_2e20
 extra-source-files:
   rust-wrapper/*.toml
   rust-wrapper/src/*.rs
@@ -469,6 +470,18 @@ benchmark bench-lagrange-basis
       tasty-bench,
       QuickCheck
 
+executable setup-generator
+    import: options-exe
+    main-is: SetupGenerator.hs
+    hs-source-dirs: test
+    ghc-options:
+      -O2
+      -threaded
+      "-with-rtsopts=-A128M -N"
+    build-depends:
+      base,
+      symbolic-base
+
 executable group-elements-generator
     import: options-exe
     main-is: Main.hs

symbolic-base/test/SetupGenerator.hs

@@ -0,0 +1,53 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeApplications #-}
+
+-- | Extract a subset of G1 points from the Midnight trusted setup ceremony file.
+--
+-- The original Midnight file (~3GB for 2^25) contains uncompressed BLS12-381 G1
+-- points (96 bytes each) followed by two uncompressed G2 points (192 bytes each).
+-- See https://github.com/midnightntwrk/midnight-trusted-setup
+--
+-- This tool reads the first N G1 points and both G2 points, validates them on the
+-- curve, and saves them with compressed G1 points (48 bytes each).
+--
+-- Usage:
+--
+-- > cabal run setup-generator -- <n-points> <input-midnight-file> <output-file>
+--
+-- Example (extract 2^20 + 6 = 1048582 points):
+--
+-- > cabal run setup-generator -- 1048582 ~/Downloads/midnight-powers-of-tau-2p25 data/midnight_powers_of_tau_2e20
+module Main where
+
+import GHC.TypeNats (SomeNat (..), someNatVal)
+import Data.Proxy (Proxy (..))
+import System.Environment (getArgs)
+import Prelude
+
+import ZkFold.Algebra.Number (value)
+import ZkFold.Protocol.NonInteractiveProof.TrustedSetup (readTrustedSetup, saveTrustedSetup)
+
+main :: IO ()
+main = do
+  args <- getArgs
+  case args of
+    [nStr, inputPath, outputPath] ->
+      case reads nStr of
+        [(n, "")] | n > 0 -> extractSetup n inputPath outputPath
+        _ -> putStrLn "ERROR: first argument must be a positive integer (number of G1 points)"
+    _ -> putStrLn "Usage: setup-generator <n-points> <input-midnight-file> <output-file>"
+
+extractSetup :: Integer -> FilePath -> FilePath -> IO ()
+extractSetup n inputPath outputPath =
+  case someNatVal (fromIntegral n) of
+    SomeNat (_ :: Proxy n) -> do
+      putStrLn $ "Extracting " ++ show n ++ " G1 points from: " ++ inputPath
+      -- The original Midnight file has uncompressed G1 points (96 bytes each)
+      result <- readTrustedSetup @n inputPath False
+      case result of
+        Nothing -> putStrLn "ERROR: Failed to read trusted setup (points not on curve?)"
+        Just ts -> do
+          putStrLn $ "Successfully read " ++ show (value @n) ++ " G1 points and 2 G2 points"
+          putStrLn $ "Saving compressed to: " ++ outputPath
+          saveTrustedSetup outputPath True ts
+          putStrLn "Done."

symbolic-ledger/bench/CircuitBreakdown.hs

@@ -26,7 +26,6 @@ import ZkFold.Prelude (foldl')
 import ZkFold.Symbolic.Algorithm.EdDSA (eddsaVerify)
 import ZkFold.Symbolic.Class (Symbolic (..))
 import ZkFold.Symbolic.Data.Bool (Bool, BoolType (..), false, true, (||))
-import ZkFold.Symbolic.Data.EllipticCurve.Jubjub (shamirDoubleScale)
 import ZkFold.Symbolic.Data.FieldElement (FieldElement (..))
 import ZkFold.Symbolic.Data.Hash (hash)
 import ZkFold.Symbolic.Data.Hash qualified as Base

symbolic-ledger/src/ZkFold/Symbolic/Ledger/Circuit/Compile.hs

@@ -28,7 +28,7 @@ import Data.Type.Equality (type (~))
 import Data.Word (Word8)
 import GHC.Generics (Generic, Generic1, Par1 (..), U1 (..), (:*:) (..), (:.:) (..))
 import GHC.Natural (Natural, naturalToInteger)
-import GHC.TypeNats (KnownNat, type (+), type (-), type (^))
+import GHC.TypeNats (KnownNat, type (*), type (+), type (-), type (^))
 import ZkFold.Algebra.Class
 import ZkFold.Algebra.EllipticCurve.BLS12_381 (
   BLS12_381_G1_CompressedPoint,
@@ -166,7 +166,7 @@ ledgerContract LedgerContractInput {..} =
     :*: swBridgeOut lciStateWitness
 
 -- TODO: Circuit gate count is likely not good enough, see https://github.com/zkFold/symbolic/issues/766.
-type LedgerCircuitGates = 2 ^ 18
+type LedgerCircuitGates = 2 ^ 20
 
 type LedgerContractInputLayout bi bo ud a s n t =
   Layout
@@ -224,30 +224,31 @@ type TranscriptConstraints ts =
   )
 
 ledgerSetup
-  :: forall tc bi bo ud a s n t c
-   . TranscriptConstraints tc
+  :: forall g tc bi bo ud a s n t c
+   . (KnownNat g, KnownNat (4 * g + 6))
+  => TranscriptConstraints tc
   => RollupBF ~ BaseField c
   => SignatureState bi bo ud a c
   => SignatureTransactionBatch ud s n a t c
-  => TrustedSetup (LedgerCircuitGates + 6)
+  => TrustedSetup (g + 6)
   -> LedgerCircuit bi bo ud a s n t
-  -> SetupVerify (PlonkupTs bi bo a (LedgerContractCompiledInput bi bo ud a s n t) LedgerCircuitGates tc)
+  -> SetupVerify (PlonkupTs bi bo a (LedgerContractCompiledInput bi bo ud a s n t) g tc)
 ledgerSetup TrustedSetup {..} circuit = setupV
  where
-  (omega, k1, k2) = getParams (Number.value @LedgerCircuitGates)
+  (omega, k1, k2) = getParams (Number.value @g)
   plonkup = Plonkup omega k1 k2 circuit g2_1 g1s
-  setupV = setupVerify @(PlonkupTs bi bo a (LedgerContractCompiledInput bi bo ud a s n t) LedgerCircuitGates tc) plonkup
+  setupV = setupVerify @(PlonkupTs bi bo a (LedgerContractCompiledInput bi bo ud a s n t) g tc) plonkup
 
 ledgerProof
-  :: forall tc bi bo ud a s n t c
-   . (TranscriptConstraints tc, c ~ Interpreter RollupBF)
+  :: forall g tc bi bo ud a s n t c
+   . (KnownNat g, KnownNat (4 * g + 6), TranscriptConstraints tc, c ~ Interpreter RollupBF)
   => SignatureState bi bo ud a c
   => SignatureTransactionBatch ud s n a t c
-  => TrustedSetup (LedgerCircuitGates + 6)
+  => TrustedSetup (g + 6)
   -> PlonkupProverSecret BLS12_381_G1_JacobianPoint
   -> LedgerCircuit bi bo ud a s n t
   -> LedgerContractInput bi bo ud a s n t c
-  -> Proof (PlonkupTs bi bo a (LedgerContractCompiledInput bi bo ud a s n t) LedgerCircuitGates tc)
+  -> Proof (PlonkupTs bi bo a (LedgerContractCompiledInput bi bo ud a s n t) g tc)
 ledgerProof TrustedSetup {..} ps circuit input = proof
  where
   witnessInputs :: (Layout (LedgerContractInput bi bo ud a s n t) (Order RollupBF)) RollupBF
@@ -256,11 +257,11 @@ ledgerProof TrustedSetup {..} ps circuit input = proof
   paddedWitnessInputs :: LedgerContractCompiledInput bi bo ud a s n t RollupBF
   paddedWitnessInputs = (witnessInputs :*: U1) :*: (payload input :*: U1)
 
-  (omega, k1, k2) = getParams (Number.value @LedgerCircuitGates)
+  (omega, k1, k2) = getParams (Number.value @g)
   plonkup =
     Plonkup omega k1 k2 circuit g2_1 g1s
-      :: PlonkupTs bi bo a (LedgerContractCompiledInput bi bo ud a s n t) LedgerCircuitGates tc
-  setupP = setupProve @(PlonkupTs bi bo a (LedgerContractCompiledInput bi bo ud a s n t) LedgerCircuitGates tc) plonkup
+      :: PlonkupTs bi bo a (LedgerContractCompiledInput bi bo ud a s n t) g tc
+  setupP = setupProve @(PlonkupTs bi bo a (LedgerContractCompiledInput bi bo ud a s n t) g tc) plonkup
   witness =
     ( PlonkupWitnessInput @(LedgerContractCompiledInput bi bo ud a s n t) @BLS12_381_G1_JacobianPoint paddedWitnessInputs
     , ps

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

@@ -0,0 +1,98 @@
+{-# OPTIONS_GHC -Wno-missing-signatures #-}
+
+module ZkFold.Symbolic.Ledger.Examples.Five (
+  prevState,
+  batch,
+  batch2,
+  witness,
+  newState,
+  utxoPreimage2,
+  asset2Policy,
+  asset2Name,
+  address,
+  address2,
+  tx1,
+  tx2,
+  tx3,
+  tx4,
+  sigs,
+  sigs2,
+  bridgeInOutput,
+  bridgedIn,
+  bridgeOutOutput,
+  bridgedIn2,
+  newState2,
+  witness2,
+  utxoPreimage3,
+  I,
+  Bi,
+  Bo,
+  Ud,
+  A,
+  S,
+  N,
+  TxCount,
+  G,
+) where
+
+import GHC.Generics ((:*:) (..), (:.:) (..))
+import GHC.TypeNats (type (^))
+import GHC.IsList (IsList (..))
+
+import ZkFold.Data.Vector (Vector)
+import ZkFold.Symbolic.Ledger.Offchain.State.Update (updateLedgerState)
+import ZkFold.Symbolic.Ledger.Types
+
+import ZkFold.Symbolic.Ledger.Examples.Three (
+  A,
+  Bi,
+  Bo,
+  I,
+  N,
+  S,
+  Ud,
+  address,
+  address2,
+  asset2Name,
+  asset2Policy,
+  bridgeInOutput,
+  bridgeOutOutput,
+  bridgedIn,
+  emptyTree,
+  makeBatch,
+  makeSigs,
+  sigEntries1,
+  sigEntries2,
+  tx1,
+  tx2,
+  tx3,
+  tx4,
+  utxoPreimage,
+ )
+import ZkFold.Symbolic.Ledger.Examples.Three qualified as Three (prevState)
+
+type TxCount = 4
+
+type G = 2 ^ 20
+
+prevState :: State Ud A I
+prevState = Three.prevState
+
+batch :: TransactionBatch N A TxCount I
+batch = makeBatch @TxCount [tx1, tx2]
+
+batch2 :: TransactionBatch N A TxCount I
+batch2 = makeBatch @TxCount [tx3, tx4]
+
+sigs :: (Vector TxCount :.: (Vector S :.: (PublicKey :*: EdDSAPoint :*: EdDSAScalarField))) I
+sigs = makeSigs @TxCount sigEntries1
+
+sigs2 :: (Vector TxCount :.: (Vector S :.: (PublicKey :*: EdDSAPoint :*: EdDSAScalarField))) I
+sigs2 = makeSigs @TxCount sigEntries2
+
+newState :*: witness :*: utxoTree2 :*: utxoPreimage2 = updateLedgerState @Bi @Bo prevState emptyTree utxoPreimage bridgedIn batch sigs
+
+bridgedIn2 :: (Vector Bi :.: Output A) I
+bridgedIn2 = Comp1 (fromList [nullOutput @A @I])
+
+newState2 :*: witness2 :*: _utxoTree3 :*: utxoPreimage3 = updateLedgerState @Bi @Bo newState utxoTree2 (unComp1 utxoPreimage2) bridgedIn2 batch2 sigs2

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

@@ -30,13 +30,15 @@ module ZkFold.Symbolic.Ledger.Examples.One (
   S,
   N,
   TxCount,
+  G,
 ) where
 
 import Control.Applicative (pure)
 import Data.Function ((&))
 import GHC.Generics ((:*:) (..), (:.:) (..))
 import GHC.IsList (IsList (..))
 import GHC.Natural (Natural)
+import GHC.TypeNats (type (^))
 import ZkFold.Algebra.Class
 import ZkFold.Algebra.EllipticCurve.Class (CyclicGroup (..))
 import ZkFold.Data.MerkleTree (Leaves)
@@ -69,6 +71,8 @@ type N = 1
 
 type TxCount = 1
 
+type G = 2 ^ 18
+
 emptyTree :: SymMerkle.MerkleTree Ud I
 emptyTree = SymMerkle.fromLeaves (pure (nullUTxOHash @A @I))