diff --git a/symbolic-base/data/midnight_powers_of_tau_2e20 b/symbolic-base/data/midnight_powers_of_tau_2e20 new file mode 100644 index 000000000..2548bb608 Binary files /dev/null and b/symbolic-base/data/midnight_powers_of_tau_2e20 differ diff --git a/symbolic-base/src/ZkFold/Protocol/NonInteractiveProof/TrustedSetup.hs b/symbolic-base/src/ZkFold/Protocol/NonInteractiveProof/TrustedSetup.hs index cc67d46c6..135b2ddc4 100644 --- a/symbolic-base/src/ZkFold/Protocol/NonInteractiveProof/TrustedSetup.hs +++ b/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 diff --git a/symbolic-base/symbolic-base.cabal b/symbolic-base/symbolic-base.cabal index ea49ec1db..75309b0d0 100644 --- a/symbolic-base/symbolic-base.cabal +++ b/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 diff --git a/symbolic-base/test/SetupGenerator.hs b/symbolic-base/test/SetupGenerator.hs new file mode 100644 index 000000000..277efab00 --- /dev/null +++ b/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 -- +-- +-- 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 " + +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." diff --git a/symbolic-ledger/bench/CircuitBreakdown.hs b/symbolic-ledger/bench/CircuitBreakdown.hs index f68c4fd8e..fe0a1336e 100644 --- a/symbolic-ledger/bench/CircuitBreakdown.hs +++ b/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 diff --git a/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Circuit/Compile.hs b/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Circuit/Compile.hs index 2a6c1aa05..cf86a4308 100644 --- a/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Circuit/Compile.hs +++ b/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 diff --git a/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Examples/Five.hs b/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Examples/Five.hs new file mode 100644 index 000000000..94a314374 --- /dev/null +++ b/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 diff --git a/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Examples/One.hs b/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Examples/One.hs index 67ce1f3f6..0b0b184ec 100644 --- a/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Examples/One.hs +++ b/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Examples/One.hs @@ -30,6 +30,7 @@ module ZkFold.Symbolic.Ledger.Examples.One ( S, N, TxCount, + G, ) where import Control.Applicative (pure) @@ -37,6 +38,7 @@ 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)) diff --git a/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Examples/Three.hs b/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Examples/Three.hs index f35c47209..a5cb4b27b 100644 --- a/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Examples/Three.hs +++ b/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Examples/Three.hs @@ -32,6 +32,17 @@ module ZkFold.Symbolic.Ledger.Examples.Three ( S, N, TxCount, + G, + -- Helpers for parameterizing TxCount + emptyTree, + utxoPreimage, + nullTx, + nullSigEntry, + SigEntry, + sigEntries1, + sigEntries2, + makeBatch, + makeSigs, ) where import Control.Applicative (pure) @@ -48,7 +59,10 @@ import ZkFold.Symbolic.Data.FieldElement (FieldElement) import ZkFold.Symbolic.Data.Hash (hash) import ZkFold.Symbolic.Data.Hash qualified as Base import ZkFold.Symbolic.Data.MerkleTree qualified as SymMerkle -import Prelude (($)) +import Prelude (Int, length, replicate, ($), (++)) +import Prelude qualified as P +import GHC.TypeNats (type (^)) +import ZkFold.Algebra.Number (KnownNat, value) import ZkFold.Symbolic.Ledger.Offchain.State.Update (updateLedgerState) import ZkFold.Symbolic.Ledger.Types @@ -71,6 +85,8 @@ type N = 2 type TxCount = 2 +type G = 2 ^ 18 + emptyTree :: SymMerkle.MerkleTree Ud I emptyTree = SymMerkle.fromLeaves (pure (nullUTxOHash @A @I)) @@ -305,14 +321,44 @@ tx4 = -- "address" has 2.5 ADA and 12.5 asset2. -- "address2" has 2.5 ADA and 12.5 asset2. -batch :: TransactionBatch N A TxCount I -batch = TransactionBatch {tbTransactions = unsafeToVector' [tx1, tx2]} +-- | Null transaction for padding batches to the desired TxCount. +nullTx :: Transaction N A I +nullTx = + Transaction + { inputs = Comp1 (fromList [nullOutputRef, nullOutputRef]) + , outputs = Comp1 (fromList [nullOutput @A @I :*: false, nullOutput @A @I :*: false]) + } -batch2 :: TransactionBatch N A TxCount I -batch2 = TransactionBatch {tbTransactions = unsafeToVector' [tx3, tx4]} +type SigEntry = (Vector S :.: (PublicKey :*: EdDSAPoint :*: EdDSAScalarField)) I -sigs :: (Vector TxCount :.: (Vector S :.: (PublicKey :*: EdDSAPoint :*: EdDSAScalarField))) I -sigs = +-- | Dummy signature entry for padding sigs to the desired TxCount. +nullSigEntry :: SigEntry +nullSigEntry = + let rPoint :*: s = signTransaction nullTx privateKey + in Comp1 + ( unsafeToVector' + [ publicKey :*: rPoint :*: s + , publicKey :*: rPoint :*: s + ] + ) + +-- | Build a transaction batch, padding with 'nullTx' to reach @txCount@. +makeBatch :: forall txCount. KnownNat txCount => [Transaction N A I] -> TransactionBatch N A txCount I +makeBatch txs = TransactionBatch {tbTransactions = unsafeToVector' (txs ++ replicate padding nullTx)} + where + padding :: Int + padding = P.fromIntegral (value @txCount) P.- length txs + +-- | Build signatures, padding with 'nullSigEntry' to reach @txCount@. +makeSigs :: forall txCount. KnownNat txCount => [SigEntry] -> (Vector txCount :.: (Vector S :.: (PublicKey :*: EdDSAPoint :*: EdDSAScalarField))) I +makeSigs entries = Comp1 (unsafeToVector' (entries ++ replicate padding nullSigEntry)) + where + padding :: Int + padding = P.fromIntegral (value @txCount) P.- length entries + +-- | Signature entries for batch 1 (tx1, tx2). +sigEntries1 :: [SigEntry] +sigEntries1 = let dummyRPoint :*: dummyS = signTransaction tx1 privateKey dummyPublicKey = publicKey @@ -327,25 +373,23 @@ sigs = rPointTx22 :*: sTx22 = signTransaction tx2 privateKey publicKeyTx22 = publicKey in - Comp1 - ( unsafeToVector' - [ Comp1 - ( unsafeToVector' - [ publicKeyTx11 :*: rPointTx11 :*: sTx11 - , publicKeyTx12 :*: rPointTx12 :*: sTx12 - ] - ) - , Comp1 - ( unsafeToVector' - [ publicKeyTx21 :*: rPointTx21 :*: sTx21 - , publicKeyTx22 :*: rPointTx22 :*: sTx22 - ] - ) - ] - ) + [ Comp1 + ( unsafeToVector' + [ publicKeyTx11 :*: rPointTx11 :*: sTx11 + , publicKeyTx12 :*: rPointTx12 :*: sTx12 + ] + ) + , Comp1 + ( unsafeToVector' + [ publicKeyTx21 :*: rPointTx21 :*: sTx21 + , publicKeyTx22 :*: rPointTx22 :*: sTx22 + ] + ) + ] -sigs2 :: (Vector TxCount :.: (Vector S :.: (PublicKey :*: EdDSAPoint :*: EdDSAScalarField))) I -sigs2 = +-- | Signature entries for batch 2 (tx3, tx4). +sigEntries2 :: [SigEntry] +sigEntries2 = let dummyRPoint :*: dummyS = signTransaction tx4 privateKey dummyPublicKey = publicKey @@ -360,22 +404,31 @@ sigs2 = rPointTx22 :*: sTx22 = dummyRPoint :*: dummyS publicKeyTx22 = dummyPublicKey in - Comp1 - ( unsafeToVector' - [ Comp1 - ( unsafeToVector' - [ publicKeyTx11 :*: rPointTx11 :*: sTx11 - , publicKeyTx12 :*: rPointTx12 :*: sTx12 - ] - ) - , Comp1 - ( unsafeToVector' - [ publicKeyTx21 :*: rPointTx21 :*: sTx21 - , publicKeyTx22 :*: rPointTx22 :*: sTx22 - ] - ) - ] - ) + [ Comp1 + ( unsafeToVector' + [ publicKeyTx11 :*: rPointTx11 :*: sTx11 + , publicKeyTx12 :*: rPointTx12 :*: sTx12 + ] + ) + , Comp1 + ( unsafeToVector' + [ publicKeyTx21 :*: rPointTx21 :*: sTx21 + , publicKeyTx22 :*: rPointTx22 :*: sTx22 + ] + ) + ] + +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 diff --git a/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Examples/Two.hs b/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Examples/Two.hs index d85be8839..8c729d87b 100644 --- a/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Examples/Two.hs +++ b/symbolic-ledger/src/ZkFold/Symbolic/Ledger/Examples/Two.hs @@ -14,6 +14,7 @@ module ZkFold.Symbolic.Ledger.Examples.Two ( S, N, TxCount, + G, ) where import Control.Applicative (pure) @@ -21,6 +22,7 @@ import Data.Function ((&)) import GHC.Generics ((:*:) (..), (:.:) (..)) import GHC.Natural (Natural) import ZkFold.Algebra.Class +import GHC.TypeNats (type (^)) import ZkFold.Algebra.EllipticCurve.Class (CyclicGroup (..)) import ZkFold.Data.MerkleTree (Leaves) import ZkFold.Data.Vector (Vector) @@ -52,6 +54,8 @@ type N = 3 type TxCount = 3 +type G = 2 ^ 18 + emptyTree :: SymMerkle.MerkleTree Ud I emptyTree = SymMerkle.fromLeaves (pure (nullUTxOHash @A @I)) diff --git a/symbolic-ledger/symbolic-ledger.cabal b/symbolic-ledger/symbolic-ledger.cabal index 4fb3d89f2..25cce3be2 100644 --- a/symbolic-ledger/symbolic-ledger.cabal +++ b/symbolic-ledger/symbolic-ledger.cabal @@ -99,6 +99,7 @@ library ZkFold.Symbolic.Ledger.Examples.Four ZkFold.Symbolic.Ledger.Examples.One ZkFold.Symbolic.Ledger.Examples.Three + ZkFold.Symbolic.Ledger.Examples.Five ZkFold.Symbolic.Ledger.Examples.Two ZkFold.Symbolic.Ledger.Offchain.State.Update ZkFold.Symbolic.Ledger.Types @@ -140,6 +141,7 @@ test-suite symbolic-ledger-test Tests.Symbolic.Ledger.E2E.Compile Tests.Symbolic.Ledger.E2E.Compile.One Tests.Symbolic.Ledger.E2E.Compile.Three + Tests.Symbolic.Ledger.E2E.Compile.Five Tests.Symbolic.Ledger.E2E.Compile.Two Tests.Symbolic.Ledger.E2E.Four Tests.Symbolic.Ledger.E2E.One @@ -184,7 +186,5 @@ benchmark bench-circuit-breakdown ghc-options: -O3 build-depends: base, - bytestring, - vector, symbolic-base, symbolic-ledger, diff --git a/symbolic-ledger/test/Tests/Symbolic/Ledger/E2E/Compile/Five.hs b/symbolic-ledger/test/Tests/Symbolic/Ledger/E2E/Compile/Five.hs new file mode 100644 index 000000000..5d444ef99 --- /dev/null +++ b/symbolic-ledger/test/Tests/Symbolic/Ledger/E2E/Compile/Five.hs @@ -0,0 +1,112 @@ +module Tests.Symbolic.Ledger.E2E.Compile.Five (specE2ECompileFive) where + +import Control.Applicative (pure) +import Control.Exception (evaluate) +import Data.ByteString (ByteString) +import Data.Map.Strict qualified as M +import GHC.Generics (U1 (..), (:*:) (..)) +import GHC.TypeNats (type (+)) +import Test.Hspec (Spec, it, shouldBe) +import ZkFold.Algebra.Class +import ZkFold.ArithmeticCircuit (acContext, acSizeM, acSizeN) +import ZkFold.ArithmeticCircuit.Context (acSystem) +import ZkFold.Protocol.NonInteractiveProof ( + NonInteractiveProof (verify), + TrustedSetup (..), + powersOfTauSubset, + ) +import ZkFold.Protocol.Plonkup.Input (PlonkupInput (..)) +import ZkFold.Protocol.Plonkup.Prover.Secret (PlonkupProverSecret (..)) +import ZkFold.Protocol.Plonkup.Relation (PlonkupRelation (pubInput)) +import ZkFold.Protocol.Plonkup.Verifier.Setup (PlonkupVerifierSetup (..)) +import ZkFold.Symbolic.Data.Class (arithmetize, payload) +import ZkFold.Symbolic.Interpreter (runInterpreter) +import Prelude (Semigroup ((<>)), Show (..), ($), (.), (==)) +import Prelude qualified as Haskell + +import Tests.Symbolic.Ledger.E2E.Utils (time) +import ZkFold.Symbolic.Ledger.Circuit.Compile ( + LedgerContractCompiledInput, + LedgerContractInput (..), + PlonkupTs, + ledgerCircuit, + ledgerProof, + ledgerSetup, + ) +import ZkFold.Symbolic.Ledger.Examples.Five + +specE2ECompileFive :: Spec +specE2ECompileFive = + it "E2E ledger circuit, Five: prove and verify" $ do + ts :: TrustedSetup (G + 6) <- powersOfTauSubset + let lci :: LedgerContractInput Bi Bo Ud A S N TxCount I + lci = + LedgerContractInput + { lciPreviousState = prevState + , lciTransactionBatch = batch + , lciNewState = newState + , lciStateWitness = witness + } + lci2 = + LedgerContractInput + { lciPreviousState = newState + , lciTransactionBatch = batch2 + , lciNewState = newState2 + , lciStateWitness = witness2 + } + compiledCircuit <- time "ledgerCircuit" $ do + let c = ledgerCircuit @Bi @Bo @Ud @A @S @N @TxCount @I + _ <- evaluate $ acSizeN c + pure c + + let zeroCons = M.size . M.filter (== zero) . acSystem . acContext $ compiledCircuit + + Haskell.putStrLn $ + "constraints: " + <> show (acSizeN compiledCircuit) + <> ", zero constraints: " + <> show zeroCons + <> ", variables: " + <> show (acSizeM compiledCircuit) + + let proverSecret = PlonkupProverSecret (pure zero) + + zkLedgerSetup <- + time "zkLedgerSetup" $ + evaluate $ + ledgerSetup + @G + @ByteString + @Bi + @Bo + @Ud + @A + @S + @N + @TxCount + @I + ts + compiledCircuit + + zkLedgerProof <- time "zkLedgerProof" $ evaluate $ ledgerProof @G @ByteString ts proverSecret compiledCircuit lci + zkLedgerProof2 <- time "zkLedgerProof2" $ evaluate $ ledgerProof @G @ByteString ts proverSecret compiledCircuit lci2 + + let + witnessInputs = runInterpreter $ arithmetize lci + witnessInputs2 = runInterpreter $ arithmetize lci2 + compiledInput = (witnessInputs :*: U1) :*: (payload lci :*: U1) + compiledInput2 = (witnessInputs2 :*: U1) :*: (payload lci2 :*: U1) + PlonkupVerifierSetup {relation} = zkLedgerSetup + zkLedgerInput = PlonkupInput (pubInput relation compiledInput) + zkLedgerInput2 = PlonkupInput (pubInput relation compiledInput2) + Haskell.putStrLn $ "zkLedgerInput: " <> show zkLedgerInput + verify @(PlonkupTs Bi Bo A (LedgerContractCompiledInput Bi Bo Ud A S N TxCount) G ByteString) + zkLedgerSetup + zkLedgerInput + zkLedgerProof + `shouldBe` Haskell.True + verify @(PlonkupTs Bi Bo A (LedgerContractCompiledInput Bi Bo Ud A S N TxCount) G ByteString) + zkLedgerSetup + zkLedgerInput2 + zkLedgerProof2 + `shouldBe` Haskell.True diff --git a/symbolic-ledger/test/Tests/Symbolic/Ledger/E2E/Compile/One.hs b/symbolic-ledger/test/Tests/Symbolic/Ledger/E2E/Compile/One.hs index 78b5ce78b..f279ee91e 100644 --- a/symbolic-ledger/test/Tests/Symbolic/Ledger/E2E/Compile/One.hs +++ b/symbolic-ledger/test/Tests/Symbolic/Ledger/E2E/Compile/One.hs @@ -25,7 +25,6 @@ import Prelude qualified as Haskell import Tests.Symbolic.Ledger.E2E.One import Tests.Symbolic.Ledger.E2E.Utils (time) import ZkFold.Symbolic.Ledger.Circuit.Compile ( - LedgerCircuitGates, LedgerContractCompiledInput, LedgerContractInput (..), PlonkupTs, @@ -37,7 +36,7 @@ import ZkFold.Symbolic.Ledger.Circuit.Compile ( specE2ECompileOne :: Spec specE2ECompileOne = it "E2E ledger circuit, One: prove and verify" $ do - ts :: TrustedSetup (LedgerCircuitGates + 6) <- powersOfTauSubset + ts :: TrustedSetup (G + 6) <- powersOfTauSubset let lci :: LedgerContractInput Bi Bo Ud A S N TxCount I lci = LedgerContractInput @@ -63,6 +62,7 @@ specE2ECompileOne = time "zkLedgerSetup" $ evaluate $ ledgerSetup + @G @ByteString @Bi @Bo @@ -75,8 +75,8 @@ specE2ECompileOne = ts compiledCircuit - zkLedgerProof <- time "zkLedgerProof" $ evaluate $ ledgerProof @ByteString ts proverSecret compiledCircuit lci - zkLedgerProof2 <- time "zkLedgerProof2" $ evaluate $ ledgerProof @ByteString ts proverSecret compiledCircuit lci2 + zkLedgerProof <- time "zkLedgerProof" $ evaluate $ ledgerProof @G @ByteString ts proverSecret compiledCircuit lci + zkLedgerProof2 <- time "zkLedgerProof2" $ evaluate $ ledgerProof @G @ByteString ts proverSecret compiledCircuit lci2 let witnessInputs = runInterpreter $ arithmetize lci compiledInput = (witnessInputs :*: U1) :*: (payload lci :*: U1) witnessInputs2 = runInterpreter $ arithmetize lci2 @@ -86,12 +86,12 @@ specE2ECompileOne = zkLedgerInput2 = PlonkupInput (pubInput relation compiledInput2) Haskell.putStrLn $ "zkLedgerInput: " <> show zkLedgerInput Haskell.putStrLn $ "zkLedgerInput2: " <> show zkLedgerInput2 - verify @(PlonkupTs Bi Bo A (LedgerContractCompiledInput Bi Bo Ud A S N TxCount) LedgerCircuitGates ByteString) + verify @(PlonkupTs Bi Bo A (LedgerContractCompiledInput Bi Bo Ud A S N TxCount) G ByteString) zkLedgerSetup zkLedgerInput zkLedgerProof `shouldBe` Haskell.True - verify @(PlonkupTs Bi Bo A (LedgerContractCompiledInput Bi Bo Ud A S N TxCount) LedgerCircuitGates ByteString) + verify @(PlonkupTs Bi Bo A (LedgerContractCompiledInput Bi Bo Ud A S N TxCount) G ByteString) zkLedgerSetup zkLedgerInput2 zkLedgerProof2 diff --git a/symbolic-ledger/test/Tests/Symbolic/Ledger/E2E/Compile/Three.hs b/symbolic-ledger/test/Tests/Symbolic/Ledger/E2E/Compile/Three.hs index c022187f8..8e054bcc3 100644 --- a/symbolic-ledger/test/Tests/Symbolic/Ledger/E2E/Compile/Three.hs +++ b/symbolic-ledger/test/Tests/Symbolic/Ledger/E2E/Compile/Three.hs @@ -26,7 +26,6 @@ import Prelude qualified as Haskell import Tests.Symbolic.Ledger.E2E.Utils (time) import ZkFold.Symbolic.Ledger.Circuit.Compile ( - LedgerCircuitGates, LedgerContractCompiledInput, LedgerContractInput (..), PlonkupTs, @@ -39,7 +38,7 @@ import ZkFold.Symbolic.Ledger.Examples.Three specE2ECompileThree :: Spec specE2ECompileThree = it "E2E ledger circuit, Three: prove and verify" $ do - ts :: TrustedSetup (LedgerCircuitGates + 6) <- powersOfTauSubset + ts :: TrustedSetup (G + 6) <- powersOfTauSubset let lci :: LedgerContractInput Bi Bo Ud A S N TxCount I lci = LedgerContractInput @@ -76,6 +75,7 @@ specE2ECompileThree = time "zkLedgerSetup" $ evaluate $ ledgerSetup + @G @ByteString @Bi @Bo @@ -88,8 +88,8 @@ specE2ECompileThree = ts compiledCircuit - zkLedgerProof <- time "zkLedgerProof" $ evaluate $ ledgerProof @ByteString ts proverSecret compiledCircuit lci - zkLedgerProof2 <- time "zkLedgerProof2" $ evaluate $ ledgerProof @ByteString ts proverSecret compiledCircuit lci2 + zkLedgerProof <- time "zkLedgerProof" $ evaluate $ ledgerProof @G @ByteString ts proverSecret compiledCircuit lci + zkLedgerProof2 <- time "zkLedgerProof2" $ evaluate $ ledgerProof @G @ByteString ts proverSecret compiledCircuit lci2 let witnessInputs = runInterpreter $ arithmetize lci @@ -100,12 +100,12 @@ specE2ECompileThree = zkLedgerInput = PlonkupInput (pubInput relation compiledInput) zkLedgerInput2 = PlonkupInput (pubInput relation compiledInput2) Haskell.putStrLn $ "zkLedgerInput: " <> show zkLedgerInput - verify @(PlonkupTs Bi Bo A (LedgerContractCompiledInput Bi Bo Ud A S N TxCount) LedgerCircuitGates ByteString) + verify @(PlonkupTs Bi Bo A (LedgerContractCompiledInput Bi Bo Ud A S N TxCount) G ByteString) zkLedgerSetup zkLedgerInput zkLedgerProof `shouldBe` Haskell.True - verify @(PlonkupTs Bi Bo A (LedgerContractCompiledInput Bi Bo Ud A S N TxCount) LedgerCircuitGates ByteString) + verify @(PlonkupTs Bi Bo A (LedgerContractCompiledInput Bi Bo Ud A S N TxCount) G ByteString) zkLedgerSetup zkLedgerInput2 zkLedgerProof2 diff --git a/symbolic-ledger/test/Tests/Symbolic/Ledger/E2E/Compile/Two.hs b/symbolic-ledger/test/Tests/Symbolic/Ledger/E2E/Compile/Two.hs index fcdf12f05..452b7bbaf 100644 --- a/symbolic-ledger/test/Tests/Symbolic/Ledger/E2E/Compile/Two.hs +++ b/symbolic-ledger/test/Tests/Symbolic/Ledger/E2E/Compile/Two.hs @@ -3,7 +3,7 @@ module Tests.Symbolic.Ledger.E2E.Compile.Two (specE2ECompileTwo) where import Control.Applicative (pure) import Data.ByteString (ByteString) import GHC.Generics (U1 (..), (:*:) (..)) -import GHC.TypeNats (type (+)) +import GHC.TypeNats (type (+), type (^)) import Test.Hspec (Spec, it, shouldBe) import ZkFold.Algebra.Class import ZkFold.ArithmeticCircuit (acSizeM, acSizeN) @@ -23,7 +23,6 @@ import Prelude qualified as Haskell import Tests.Symbolic.Ledger.E2E.Two import ZkFold.Symbolic.Ledger.Circuit.Compile ( - LedgerCircuitGates, LedgerContractCompiledInput, LedgerContractInput (..), PlonkupTs, @@ -32,10 +31,11 @@ import ZkFold.Symbolic.Ledger.Circuit.Compile ( ledgerSetup, ) + specE2ECompileTwo :: Spec specE2ECompileTwo = it "E2E ledger circuit, Two: prove and verify" $ do - ts :: TrustedSetup (LedgerCircuitGates + 6) <- powersOfTauSubset + ts :: TrustedSetup (G + 6) <- powersOfTauSubset let lci :: LedgerContractInput Bi Bo Ud A S N TxCount I lci = LedgerContractInput @@ -51,6 +51,7 @@ specE2ECompileTwo = proverSecret = PlonkupProverSecret (pure zero) zkLedgerSetup = ledgerSetup + @G @ByteString @Bi @Bo @@ -62,13 +63,13 @@ specE2ECompileTwo = @I ts compiledCircuit - zkLedgerProof = ledgerProof @ByteString ts proverSecret compiledCircuit lci + zkLedgerProof = ledgerProof @G @ByteString ts proverSecret compiledCircuit lci witnessInputs = runInterpreter $ arithmetize lci compiledInput = (witnessInputs :*: U1) :*: (payload lci :*: U1) PlonkupVerifierSetup {relation} = zkLedgerSetup zkLedgerInput = PlonkupInput (pubInput relation compiledInput) Haskell.putStrLn $ "zkLedgerInput: " <> show zkLedgerInput - verify @(PlonkupTs Bi Bo A (LedgerContractCompiledInput Bi Bo Ud A S N TxCount) LedgerCircuitGates ByteString) + verify @(PlonkupTs Bi Bo A (LedgerContractCompiledInput Bi Bo Ud A S N TxCount) G ByteString) zkLedgerSetup zkLedgerInput zkLedgerProof diff --git a/symbolic-ledger/test/Tests/Symbolic/Ledger/E2E/One.hs b/symbolic-ledger/test/Tests/Symbolic/Ledger/E2E/One.hs index fa8eaaafe..95f13a100 100644 --- a/symbolic-ledger/test/Tests/Symbolic/Ledger/E2E/One.hs +++ b/symbolic-ledger/test/Tests/Symbolic/Ledger/E2E/One.hs @@ -18,6 +18,7 @@ module Tests.Symbolic.Ledger.E2E.One ( S, N, TxCount, + G, ) where import Control.Applicative (pure) diff --git a/symbolic-ledger/test/Tests/Symbolic/Ledger/E2E/Two.hs b/symbolic-ledger/test/Tests/Symbolic/Ledger/E2E/Two.hs index 6a2f09f53..2563b9347 100644 --- a/symbolic-ledger/test/Tests/Symbolic/Ledger/E2E/Two.hs +++ b/symbolic-ledger/test/Tests/Symbolic/Ledger/E2E/Two.hs @@ -12,6 +12,7 @@ module Tests.Symbolic.Ledger.E2E.Two ( S, N, TxCount, + G, ) where import Control.Applicative (pure)