Feat/autocompute nbkeccakf (#176)

* feat estimate maxNbKeccakF * feat actual estimation * docs todo * fix extra room for padding --------- Co-authored-by: Arya Tabaie <15056835+Tabaie@users.noreply.github.com> Co-authored-by: Leo Jeong <dreamerty@postech.ac.kr>
2026-01-09 15:38:06 -05:00 · 2024-10-14 07:12:36 -05:00
parent 482b31ecb7
commit 368e40424b
9 changed files with 20 additions and 19 deletions
--- a/prover/circuits/pi-interconnection/bench/main.go
+++ b/prover/circuits/pi-interconnection/bench/main.go
@@ -26,7 +26,6 @@ func main() {
 	c, err := pi_interconnection.Compile(config.PublicInput{
 		MaxNbDecompression: 400,
 		MaxNbExecution:     400,
-		MaxNbKeccakF:       10000,
 		ExecutionMaxNbMsg:  16,
 		L2MsgMerkleDepth:   5,
 		L2MsgMaxNbMerkle:   10,
--- a/prover/circuits/pi-interconnection/circuit.go
+++ b/prover/circuits/pi-interconnection/circuit.go
@@ -229,7 +229,7 @@ func Compile(c config.PublicInput, wizardCompilationOpts ...func(iop *wizard.Com
 		c.L2MsgMaxNbMerkle = (c.MaxNbExecution*c.ExecutionMaxNbMsg + merkleNbLeaves - 1) / merkleNbLeaves
 	}

-	sh := newKeccakCompiler(c).Compile(c.MaxNbKeccakF, wizardCompilationOpts...)
+	sh := newKeccakCompiler(c).Compile(wizardCompilationOpts...)
 	shc, err := sh.GetCircuit()
 	if err != nil {
 		return nil, err
@@ -261,7 +261,6 @@ func (c *Compiled) getConfig() (config.PublicInput, error) {
 	return config.PublicInput{
 		MaxNbDecompression: len(c.Circuit.DecompressionFPIQ),
 		MaxNbExecution:     len(c.Circuit.ExecutionFPIQ),
-		MaxNbKeccakF:       c.Keccak.MaxNbKeccakF(),
 		ExecutionMaxNbMsg:  executionNbMsg,
 		L2MsgMerkleDepth:   c.Circuit.L2MessageMerkleDepth,
 		L2MsgMaxNbMerkle:   c.Circuit.L2MessageMaxNbMerkle,
--- a/prover/circuits/pi-interconnection/circuit_test.go
+++ b/prover/circuits/pi-interconnection/circuit_test.go
@@ -118,7 +118,6 @@ func TestMaxNbCircuitsSum(t *testing.T) {
 				MaxNbDecompression: maxNbDecompression,
 				MaxNbExecution:     maxNbExecution,
 				MaxNbCircuits:      20,
-				MaxNbKeccakF:       200,
 				ExecutionMaxNbMsg:  2,
 				L2MsgMerkleDepth:   5,
 				L2MsgMaxNbMerkle:   2,
--- a/prover/circuits/pi-interconnection/compile/test_compile.go
+++ b/prover/circuits/pi-interconnection/compile/test_compile.go
@@ -21,7 +21,6 @@ func main() {
 	c, err := pi_interconnection.Compile(config.PublicInput{
 		MaxNbDecompression: 400,
 		MaxNbExecution:     400,
-		MaxNbKeccakF:       10000,
 		ExecutionMaxNbMsg:  16,
 		L2MsgMerkleDepth:   5,
 		L2MsgMaxNbMerkle:   10,
--- a/prover/circuits/pi-interconnection/e2e_test.go
+++ b/prover/circuits/pi-interconnection/e2e_test.go
@@ -30,7 +30,7 @@ import (

 // some of the execution data are faked
 func TestSingleBlockBlob(t *testing.T) {
-	testPI(t, 103, pitesting.AssignSingleBlockBlob(t), withSlack(0, 1, 2))
+	testPI(t, pitesting.AssignSingleBlockBlob(t), withSlack(0, 1, 2))
 }

 func TestSingleBlobBlobE2E(t *testing.T) {
@@ -38,7 +38,6 @@ func TestSingleBlobBlobE2E(t *testing.T) {
 	cfg := config.PublicInput{
 		MaxNbDecompression: len(req.Decompressions),
 		MaxNbExecution:     len(req.Executions),
-		MaxNbKeccakF:       100,
 		ExecutionMaxNbMsg:  1,
 		L2MsgMerkleDepth:   5,
 		L2MsgMaxNbMerkle:   1,
@@ -124,7 +123,7 @@ func TestTinyTwoBatchBlob(t *testing.T) {
 		},
 	}

-	testPI(t, 100, req, withSlack(0, 1, 2))
+	testPI(t, req, withSlack(0, 1, 2))
 }

 func TestTwoTwoBatchBlobs(t *testing.T) {
@@ -205,13 +204,13 @@ func TestTwoTwoBatchBlobs(t *testing.T) {
 		},
 	}

-	testPI(t, 101, req, withSlack(0, 1, 2))
+	testPI(t, req, withSlack(0, 1, 2))
 }

 func TestEmpty(t *testing.T) {
 	const hexZeroBlock = "0x0000000000000000000000000000000000000000000000000000000000000000"

-	testPI(t, 50, pi_interconnection.Request{
+	testPI(t, pi_interconnection.Request{
 		Aggregation: public_input.Aggregation{
 			FinalShnarf:                             hexZeroBlock,
 			ParentAggregationFinalShnarf:            hexZeroBlock,
@@ -242,7 +241,7 @@ func withSlack(slack ...int) testPIOption {
 	}
 }

-func testPI(t *testing.T, maxNbKeccakF int, req pi_interconnection.Request, options ...testPIOption) {
+func testPI(t *testing.T, req pi_interconnection.Request, options ...testPIOption) {
 	var cfg testPIConfig
 	for _, o := range options {
 		o(&cfg)
@@ -267,7 +266,6 @@ func testPI(t *testing.T, maxNbKeccakF int, req pi_interconnection.Request, opti
 		cfg := config.PublicInput{
 			MaxNbDecompression: len(req.Decompressions) + slack[0],
 			MaxNbExecution:     len(req.Executions) + slack[1],
-			MaxNbKeccakF:       maxNbKeccakF,
 			ExecutionMaxNbMsg:  1 + slack[2],
 			L2MsgMerkleDepth:   5,
 			L2MsgMaxNbMerkle:   1 + slack[3],
--- a/prover/circuits/pi-interconnection/keccak/assign.go
+++ b/prover/circuits/pi-interconnection/keccak/assign.go
@@ -29,7 +29,7 @@ import (
 // Finally, the gnark sub-circuit can produce a SNARK hasher to be used inside the circuit.Define function.

 // TODO Perhaps a permutation argument would help usability
-// i.e. compute \prod (r+ inLen + in_0 s + in_1 s^2 + ... + in_{maxInLen-1} s^{maxInLen} + out_0 s^{maxInLen+1} + ... + out_31 s^{maxInLen+32)
+// i.e. compute ∏ (r+ inLen + in₀ s + in₁ s² + ... + in_{maxInLen-1} sᵐᵃˣᴵⁿᴸᵉⁿ + out_0 sᵐᵃˣᴵⁿᴸᵉⁿ⁺¹ + ... + out₃₁ sᵐᵃˣᴵⁿᴸᵉⁿ⁺³²
 // on both sides and assert their equality
 // (can pack the in-outs first to reduce constraints slightly)

@@ -79,13 +79,20 @@ func (h *StrictHasherCompiler) WithHashLengths(l ...int) *StrictHasherCompiler {
 	return h
 }

-func (h *StrictHasherCompiler) Compile(maxNbKeccakF int, wizardCompilationOpts ...func(iop *wizard.CompiledIOP)) CompiledStrictHasher { // TODO compute maxNbKeccakF instead of taking as param
-	wc := NewWizardVerifierSubCircuit(maxNbKeccakF, wizardCompilationOpts...)
+func (h *StrictHasherCompiler) Compile(wizardCompilationOpts ...func(iop *wizard.CompiledIOP)) CompiledStrictHasher {
+	nbKeccakF := 0 // Since the output size is smaller than the block size the squeezing phase is trivial TODO @Tabaie check with @azam.soleimanian that this is correct
+
+	const blockNbBytesIn = lanesPerBlock * 8
+	for _, l := range *h {
+		nbKeccakF += l/blockNbBytesIn + 1 // extra room for padding
+	}
+
+	wc := NewWizardVerifierSubCircuit(nbKeccakF, wizardCompilationOpts...)

 	return CompiledStrictHasher{
 		wc:           *wc,
 		lengths:      *h,
-		maxNbKeccakF: maxNbKeccakF,
+		maxNbKeccakF: nbKeccakF,
 	}
 }

--- a/prover/circuits/pi-interconnection/keccak/assign_test.go
+++ b/prover/circuits/pi-interconnection/keccak/assign_test.go
@@ -15,7 +15,7 @@ import (
 func TestAssign(t *testing.T) {

 	compiler := NewStrictHasherCompiler(1)
-	compiled := compiler.WithHashLengths(32).Compile(10, dummy.Compile)
+	compiled := compiler.WithHashLengths(32).Compile(dummy.Compile)

 	var zero [32]byte

--- a/prover/circuits/pi-interconnection/keccak/snark.go
+++ b/prover/circuits/pi-interconnection/keccak/snark.go
@@ -28,7 +28,8 @@ type BlockHasher interface {
 	Sum(nbIn frontend.Variable, bytess ...[32]frontend.Variable) [32]frontend.Variable
 }

-// Hasher is stateless from the user's perspective, but in the background it prepares columns for the Vortex prover
+// Hasher prepares the input columns for the Vortex verifier in a SNARK circuit.
+// It is stateless from the user's perspective, but it does its works as it is being fed input.
 type Hasher struct {
 	api         frontend.API
 	nbLanes     int
--- a/prover/config/config.go
+++ b/prover/config/config.go
@@ -255,7 +255,6 @@ type PublicInput struct {
 	MaxNbDecompression int  `mapstructure:"max_nb_decompression" validate:"gte=0"`
 	MaxNbExecution     int  `mapstructure:"max_nb_execution" validate:"gte=0"`
 	MaxNbCircuits      int  `mapstructure:"max_nb_circuits" validate:"gte=0"` // if not set, will be set to MaxNbDecompression + MaxNbExecution
-	MaxNbKeccakF       int  `mapstructure:"max_nb_keccakf" validate:"gte=0"`
 	ExecutionMaxNbMsg  int  `mapstructure:"execution_max_nb_msg" validate:"gte=0"`
 	L2MsgMerkleDepth   int  `mapstructure:"l2_msg_merkle_depth" validate:"gte=0"`
 	L2MsgMaxNbMerkle   int  `mapstructure:"l2_msg_max_nb_merkle" validate:"gte=0"` // if not explicitly provided (i.e. non-positive) it will be set to maximum