Prover: adds check-only mode (#3913)

* create an prover-checker that can be used for checking
* feat(check-only): adds a check-only mode in the config

prover/backend/execution/prove.go

@@ -170,6 +170,15 @@ func mustProveAndPass(
 			utils.Panic("The prover did not pass: %v", err)
 		}
 		return "", ""
+
+	case config.ProverModeCheckOnly:
+
+		fullZkEvm := zkevm.FullZkEVMCheckOnly(traces)
+		// this will panic to alert errors, so there is no need to handle or
+		// sanity-check anything.
+		_ = fullZkEvm.ProveInner(w.ZkEVM)
+		return "", ""
+
 	default:
 		panic("not implemented")
 	}

prover/config/config.go

@@ -198,7 +198,7 @@ type Execution struct {
 	WithRequestDir `mapstructure:",squash"`
 
 	// ProverMode stores the kind of prover to use.
-	ProverMode ProverMode `mapstructure:"prover_mode" validate:"required,oneof=dev partial full proofless bench"`
+	ProverMode ProverMode `mapstructure:"prover_mode" validate:"required,oneof=dev partial full proofless bench check-only"`
 
 	// CanRunFullLarge indicates whether the prover is running on a large machine (and can run full large traces).
 	CanRunFullLarge bool `mapstructure:"can_run_full_large"`

prover/config/types.go

@@ -25,4 +25,6 @@ const (
 	// ProverModeBench is used to only run the inner-proof. This is convenient
 	// in a context where it is simpler to not have to deal with the setup.
 	ProverModeBench ProverMode = "bench"
+	// ProverModeCheckOnly is used to test the constraints of the whole system
+	ProverModeCheckOnly ProverMode = "check-only"
 )

prover/protocol/compiler/dummy/dummy_prover_level.go

@@ -0,0 +1,143 @@
+package dummy
+
+import (
+	"fmt"
+	"sync"
+
+	"github.com/consensys/zkevm-monorepo/prover/protocol/column"
+	"github.com/consensys/zkevm-monorepo/prover/protocol/wizard"
+	"github.com/consensys/zkevm-monorepo/prover/utils"
+	"github.com/consensys/zkevm-monorepo/prover/utils/parallel"
+	"github.com/sirupsen/logrus"
+)
+
+// CompileAtProverLvl instantiate the oracle as the prover. Meaning that the
+// prover is responsible for checking all the queries and the verifier does not
+// see any compiled IOP.
+//
+// This is useful for quick "manual" testing and debugging. One perk is that
+// unlike [CompileAtVerifierLvl] the FS is not pressured as we don't push many
+// column in plain-text to the verifier. The drawback is that since it happens
+// at prover level, the "errors" result in panics. This makes it not very
+// suitable for established unit-tests where we want to analyze the errors.
+func CompileAtProverLvl(comp *wizard.CompiledIOP) {
+
+	comp.DummyCompiled = true
+
+	/*
+		Registers all declared commitments and query parameters
+		as messages in the same round. This steps is only relevant
+		for the compiledIOP. We elaborate on how to update the provers
+		and verifiers to account for this. Additionally, we take the queries
+		as we compile them from the `CompiledIOP`.
+	*/
+	numRounds := comp.NumRounds()
+
+	/*
+		The filter returns true, as long as the query has not been marked as
+		already compiled. This is to avoid them being compiled a second time.
+	*/
+	queriesParamsToCompile := comp.QueriesParams.AllUnignoredKeys()
+	queriesNoParamsToCompile := comp.QueriesNoParams.AllUnignoredKeys()
+
+	for i := 0; i < numRounds; i++ {
+		// Mark all the commitments as messages
+		coms := comp.Columns.AllKeysAt(i)
+		for _, com := range coms {
+			// Check the status of the commitment
+			status := comp.Columns.Status(com)
+
+			if status == column.Ignored {
+				// If the column is ignored, we can just skip it
+				continue
+			}
+
+			if status.IsPublic() {
+				// Nothing specific to do on the prover side
+				continue
+			}
+
+			// Mark them as "public" to the verifier
+			switch status {
+			case column.Precomputed:
+				// send it to the verifier directly as part of the verifying key
+				comp.Columns.SetStatus(com, column.VerifyingKey)
+			case column.Committed:
+				// send it to the verifier directly as part of the proof
+				comp.Columns.SetStatus(com, column.Proof)
+			default:
+				utils.Panic("Unknown status : %v", status.String())
+			}
+		}
+	}
+
+	/*
+		And mark the queries as already compiled
+	*/
+	for _, q := range queriesNoParamsToCompile {
+		comp.QueriesNoParams.MarkAsIgnored(q)
+	}
+
+	for _, q := range queriesParamsToCompile {
+		comp.QueriesParams.MarkAsIgnored(q)
+	}
+
+	/*
+		One step to be run at the end, by verifying every constraint
+		"a la mano"
+	*/
+	verifier := func(run *wizard.ProverRuntime) {
+
+		logrus.Infof("started to run the dummy verifier")
+
+		var finalErr error
+		lock := sync.Mutex{}
+
+		/*
+			Test all the query with parameters
+		*/
+		parallel.Execute(len(queriesParamsToCompile), func(start, stop int) {
+			for i := start; i < stop; i++ {
+				name := queriesParamsToCompile[i]
+				lock.Lock()
+				q := comp.QueriesParams.Data(name)
+				lock.Unlock()
+				if err := q.Check(run); err != nil {
+					lock.Lock()
+					finalErr = fmt.Errorf("%v\nfailed %v - %v", finalErr, name, err)
+					lock.Unlock()
+					logrus.Debugf("query %v failed\n", name)
+				} else {
+					logrus.Debugf("query %v passed\n", name)
+				}
+			}
+		})
+
+		/*
+			Test the queries without parameters
+		*/
+		parallel.Execute(len(queriesNoParamsToCompile), func(start, stop int) {
+			for i := start; i < stop; i++ {
+				name := queriesNoParamsToCompile[i]
+				lock.Lock()
+				q := comp.QueriesNoParams.Data(name)
+				lock.Unlock()
+				if err := q.Check(run); err != nil {
+					lock.Lock()
+					finalErr = fmt.Errorf("%v\nfailed %v - %v", finalErr, name, err)
+					lock.Unlock()
+				} else {
+					logrus.Debugf("query %v passed\n", name)
+				}
+			}
+		})
+
+		if finalErr != nil {
+			utils.Panic("dummy.Compile brought errors: %v", finalErr.Error())
+		}
+	}
+
+	logrus.Debugf("NB: The gnark circuit does not check the verifier of the dummy reduction\n")
+	comp.SubProvers.AppendToInner(numRounds-1, verifier)
+
+}

prover/zkevm/full.go

@@ -7,6 +7,7 @@ import (
 	"github.com/consensys/zkevm-monorepo/prover/crypto/ringsis"
 	"github.com/consensys/zkevm-monorepo/prover/protocol/compiler"
 	"github.com/consensys/zkevm-monorepo/prover/protocol/compiler/cleanup"
+	"github.com/consensys/zkevm-monorepo/prover/protocol/compiler/dummy"
 	"github.com/consensys/zkevm-monorepo/prover/protocol/compiler/mimc"
 	"github.com/consensys/zkevm-monorepo/prover/protocol/compiler/selfrecursion"
 	"github.com/consensys/zkevm-monorepo/prover/protocol/compiler/vortex"
@@ -34,8 +35,10 @@ const (
 )
 
 var (
-	fullZkEvm     *ZkEvm
-	onceFullZkEvm = sync.Once{}
+	fullZkEvm              *ZkEvm
+	fullZkEvmCheckOnly     *ZkEvm
+	onceFullZkEvm          = sync.Once{}
+	onceFullZkEvmCheckOnly = sync.Once{}
 
 	// This is the SIS instance, that has been found to minimize the overhead of
 	// recursion. It is changed w.r.t to the estimated because the estimated one
@@ -45,6 +48,8 @@ var (
 	// level target.
 	sisInstance = ringsis.Params{LogTwoBound: 16, LogTwoDegree: 6}
 
+	dummyCompilationSuite = compilationSuite{dummy.CompileAtProverLvl}
+
 	// This is the compilation suite in use for the full prover
 	fullCompilationSuite = compilationSuite{
 		// logdata.Log("initial-wizard"),
@@ -108,68 +113,81 @@ var (
 func FullZkEvm(tl *config.TracesLimits) *ZkEvm {
 
 	onceFullZkEvm.Do(func() {
-
-		// @Alex: only set mandatory parameters here. aka, the one that are not
-		// actually feature-gated.
-		settings := Settings{
-			Arithmetization: arithmetization.Settings{
-				Limits: tl,
-			},
-			Statemanager: statemanager.Settings{
-				AccSettings: accumulator.Settings{
-					MaxNumProofs:    merkleProofLimit,
-					Name:            "SM_ACCUMULATOR",
-					MerkleTreeDepth: 40,
-				},
-				MiMCCodeHashSize: tl.Rom,
-			},
-			// The compilation suite itself is hard-coded and reflects the
-			// actual full proof system.
-			CompilationSuite: fullCompilationSuite,
-			Metadata: wizard.VersionMetadata{
-				Title:   "linea/evm-execution/full",
-				Version: "beta-v1",
-			},
-			Keccak: keccak.Settings{
-				MaxNumKeccakf: keccakLimit,
-			},
-			Ecdsa: ecdsa.Settings{
-				MaxNbEcRecover:     tl.PrecompileEcrecoverEffectiveCalls,
-				MaxNbTx:            tl.BlockTransactions,
-				NbInputInstance:    4,
-				NbCircuitInstances: utils.DivCeil(tl.PrecompileEcrecoverEffectiveCalls+tl.BlockTransactions, 4),
-			},
-			Modexp: modexp.Settings{
-				MaxNbInstance256:  tl.PrecompileModexpEffectiveCalls,
-				MaxNbInstance4096: 1,
-			},
-			Ecadd: ecarith.Limits{
-				// 14 was found the right number to have just under 2^19 constraints
-				// per circuit.
-				NbInputInstances:   utils.DivCeil(tl.PrecompileEcaddEffectiveCalls, 28),
-				NbCircuitInstances: 28,
-			},
-			Ecmul: ecarith.Limits{
-				NbCircuitInstances: utils.DivCeil(tl.PrecompileEcmulEffectiveCalls, 6),
-				NbInputInstances:   6,
-			},
-			Ecpair: ecpair.Limits{
-				NbMillerLoopInputInstances:   1,
-				NbMillerLoopCircuits:         tl.PrecompileEcpairingMillerLoops,
-				NbFinalExpInputInstances:     1,
-				NbFinalExpCircuits:           tl.PrecompileEcpairingEffectiveCalls,
-				NbG2MembershipInputInstances: 6,
-				NbG2MembershipCircuits:       utils.DivCeil(tl.PrecompileEcpairingG2MembershipCalls, 6),
-			},
-			Sha2: sha2.Settings{
-				MaxNumSha2F: tl.PrecompileSha2Blocks,
-			},
-		}
-
 		// Initialize the Full zkEVM arithmetization
-		fullZkEvm = NewZkEVM(settings)
-
+		fullZkEvm = fullZKEVMWithSuite(tl, fullCompilationSuite)
 	})
 
 	return fullZkEvm
 }
+
+func FullZkEVMCheckOnly(tl *config.TracesLimits) *ZkEvm {
+
+	onceFullZkEvmCheckOnly.Do(func() {
+		// Initialize the Full zkEVM arithmetization
+		fullZkEvmCheckOnly = fullZKEVMWithSuite(tl, dummyCompilationSuite)
+	})
+
+	return fullZkEvmCheckOnly
+}
+
+func fullZKEVMWithSuite(tl *config.TracesLimits, suite compilationSuite) *ZkEvm {
+
+	// @Alex: only set mandatory parameters here. aka, the one that are not
+	// actually feature-gated.
+	settings := Settings{
+		CompilationSuite: suite,
+		Arithmetization: arithmetization.Settings{
+			Limits: tl,
+		},
+		Statemanager: statemanager.Settings{
+			AccSettings: accumulator.Settings{
+				MaxNumProofs:    merkleProofLimit,
+				Name:            "SM_ACCUMULATOR",
+				MerkleTreeDepth: 40,
+			},
+			MiMCCodeHashSize: tl.Rom,
+		},
+		Metadata: wizard.VersionMetadata{
+			Title:   "linea/evm-execution/full",
+			Version: "beta-v1",
+		},
+		Keccak: keccak.Settings{
+			MaxNumKeccakf: keccakLimit,
+		},
+		Ecdsa: ecdsa.Settings{
+			MaxNbEcRecover:     tl.PrecompileEcrecoverEffectiveCalls,
+			MaxNbTx:            tl.BlockTransactions,
+			NbInputInstance:    4,
+			NbCircuitInstances: utils.DivCeil(tl.PrecompileEcrecoverEffectiveCalls+tl.BlockTransactions, 4),
+		},
+		Modexp: modexp.Settings{
+			MaxNbInstance256:  tl.PrecompileModexpEffectiveCalls,
+			MaxNbInstance4096: 1,
+		},
+		Ecadd: ecarith.Limits{
+			// 14 was found the right number to have just under 2^19 constraints
+			// per circuit.
+			NbInputInstances:   utils.DivCeil(tl.PrecompileEcaddEffectiveCalls, 28),
+			NbCircuitInstances: 28,
+		},
+		Ecmul: ecarith.Limits{
+			NbCircuitInstances: utils.DivCeil(tl.PrecompileEcmulEffectiveCalls, 6),
+			NbInputInstances:   6,
+		},
+		Ecpair: ecpair.Limits{
+			NbMillerLoopInputInstances:   1,
+			NbMillerLoopCircuits:         tl.PrecompileEcpairingMillerLoops,
+			NbFinalExpInputInstances:     1,
+			NbFinalExpCircuits:           tl.PrecompileEcpairingEffectiveCalls,
+			NbG2MembershipInputInstances: 6,
+			NbG2MembershipCircuits:       utils.DivCeil(tl.PrecompileEcpairingG2MembershipCalls, 6),
+		},
+		Sha2: sha2.Settings{
+			MaxNumSha2F: tl.PrecompileSha2Blocks,
+		},
+	}
+
+	// Initialize the Full zkEVM arithmetization
+	fullZkEvm = NewZkEVM(settings)
+	return fullZkEvm
+}