prototyped recursive verifier with CI running

Author: tonyfloatersu

recursion/mersenne31.go

@@ -5,6 +5,7 @@ import (
 	"ExpanderVerifierCircuit/modules/fields"
 
 	"github.com/PolyhedraZK/ExpanderCompilerCollection/ecgo"
+	ecgoTest "github.com/PolyhedraZK/ExpanderCompilerCollection/ecgo/test"
 	"github.com/spf13/cobra"
 )
 
@@ -48,10 +49,32 @@ func Mersenne31RecursionImpl() {
 		OriginalCircuit: *originalCircuit,
 		Proof:           *proof.PlaceHolder(),
 	}
-	_, err = ecgo.Compile(fields.ECCM31.FieldModulus(), &m31RecursionCircuit)
+	m31Compilation, err := ecgo.Compile(fields.ECCM31.FieldModulus(), &m31RecursionCircuit)
 	if err != nil {
 		panic(err.Error())
 	}
 
-	// TODO circuit input witness
+	// witness definition
+	originalCircuit, _, err = circuit.ReadCircuit(circuitRel)
+	if err != nil {
+		panic(err.Error())
+	}
+
+	assignment := VerifierCircuit{
+		MpiSize:         mpiSize,
+		FieldEnum:       fields.ECCM31,
+		OriginalCircuit: *originalCircuit,
+		Proof:           *proof,
+	}
+
+	println("Solving witness...")
+	inputSolver := m31Compilation.GetInputSolver()
+	witness, err := inputSolver.SolveInput(&assignment, 0)
+	if err != nil {
+		panic(err.Error())
+	}
+
+	println("Checking satisfiability...")
+	layeredCircuit := m31Compilation.GetLayeredCircuit()
+	println(ecgoTest.CheckCircuit(layeredCircuit, witness))
 }

recursion/modules/polycommit/generics.go

@@ -23,7 +23,11 @@ type PolynomialCommitment interface {
 	// Verify checks against commitment the opening point and eval
 	// TODO(HS) for now this matches with raw commitment,
 	// later we should add polynomial commitment opening to the interface
-	Verify(arithmeticEngine fields.ArithmeticEngine, r [][]frontend.Variable, y []frontend.Variable)
+	Verify(
+		api fields.ArithmeticEngine,
+		rs, rSIMD, rMPI [][]frontend.Variable,
+		y []frontend.Variable,
+	)
 }
 
 // NewCommitment is the general interface for verifier circuit to extract a

recursion/modules/polycommit/raw.go

@@ -41,8 +41,22 @@ func EvalMultilinear(
 }
 
 func (c *RawCommitment) Verify(
-	api fields.ArithmeticEngine, r [][]frontend.Variable, y []frontend.Variable) {
-	api.AssertEq(EvalMultilinear(api, c.Vals, r), y)
+	api fields.ArithmeticEngine,
+	rs, rSIMD, rMPI [][]frontend.Variable,
+	y []frontend.Variable,
+) {
+	totalNumVars := len(rs) + len(rSIMD) + len(rMPI)
+
+	if 1<<len(rSIMD) != api.SIMDPackSize() {
+		panic("Inconsistent SIMD length with randomness")
+	}
+
+	challengePoint := make([][]frontend.Variable, totalNumVars)
+	copy(challengePoint, rSIMD)
+	copy(challengePoint[len(rSIMD):], rs)
+	copy(challengePoint[len(rSIMD)+len(rs):], rMPI)
+
+	api.AssertEq(EvalMultilinear(api, c.Vals, challengePoint), y)
 }
 
 func NewRawPolyCommitment(

recursion/modules/transcript/generics.go

@@ -141,7 +141,27 @@ func (t *FieldHasherTranscript) ChallengeF() []frontend.Variable {
 	return sampledChallenge
 }
 
-// TODO(HS) hash to state / set state? need after poseidon m31
+func (t *FieldHasherTranscript) HashAndReturnState() []frontend.Variable {
+	if len(t.dataPool) != 0 {
+		var newCount uint = 0
+		t.hashState, newCount = t.hasher.HashToState(t.dataPool...)
+
+		t.count += newCount
+		t.dataPool = nil
+	} else {
+		var newCount uint = 0
+		t.hashState, newCount = t.hasher.HashToState(t.hashState...)
+
+		t.count += newCount
+	}
+
+	return t.hashState
+}
+
+func (t *FieldHasherTranscript) SetState(newHashState []frontend.Variable) {
+	t.nextUnconsumed = t.hasher.StateCapacity()
+	t.hashState = newHashState
+}
 
 func (t *FieldHasherTranscript) GetCount() uint {
 	return t.count

recursion/modules/verifier/verifier.go

@@ -264,14 +264,15 @@ func Verify(
 		fsTranscript,
 	)
 
-	// TODO(HS) MPI Fiat-Shamir sync randomness rewrite
-	// Trigger an additional hash
+	// NOTE: MPI Fiat-Shamir sync randomness
 	if mpiSize > 1 {
-		_ = fsTranscript.ChallengeF()
+		newState := fsTranscript.HashAndReturnState()
+		fsTranscript.SetState(newState)
 	}
 
-	// TODO(HS) fix inconsistency between MPI and single process settings
-	log.Println("#Hashes for input: ", fsTranscript.GetCount())
+	if mpiSize > 1 {
+		log.Println("#Hashes for input: ", fsTranscript.GetCount())
+	}
 	fsTranscript.ResetCount()
 
 	originalCircuit.FillRndCoef(fsTranscript)
@@ -292,12 +293,9 @@ func Verify(
 	log.Println("#Hashes for gkr challenge: ", fsTranscript.GetCount())
 	fsTranscript.ResetCount()
 
-	rx = append(rx, r_simd...)
-	rx = append(rx, r_mpi...)
+	polyCom.Verify(api, rx, r_simd, r_mpi, claimed_v0)
 
-	ry = append(ry, r_simd...)
-	ry = append(ry, r_mpi...)
-
-	polyCom.Verify(api, rx, claimed_v0)
-	polyCom.Verify(api, ry, claimed_v1)
+	if ry != nil {
+		polyCom.Verify(api, ry, r_simd, r_mpi, claimed_v1)
+	}
 }

scripts/test_recursion.py

@@ -185,8 +185,17 @@ def test_m31_gkr_to_gkr_recursion(
 
     @in_recursion_dir
     def test_m31_gkr_to_gkr_recursion_payload():
-        # TODO m31 dev TBD
-        pass
+        m31_gkr_cmd = ' '.join(f'''
+        go run . mersenne31
+        --circuit-file ../{proof_config.circuit}
+        --witness-files ../{proof_config.witness}
+        --gkr-proofs ../{proof_path}
+        --mpi-size {mpi_config.cpus()}
+        '''.strip().split())
+
+        print(m31_gkr_cmd)
+        if subprocess.run(m31_gkr_cmd, shell=True).returncode != 0:
+            raise Exception("recursion proof is not proving correctly")
 
     test_m31_gkr_to_gkr_recursion_payload()