zkvm: the same witness rule at the precompile's door

The 0x80 precompile takes both the verifying key and the public-input count from
its caller's calldata, so a caller picks both and they have to agree. Its comment
said so — "numInputs must match vk.K length minus 1" — while the code checked
only that there were not too many. Too few leaves the trailing K points out of
the linear combination and judges the proof against a smaller statement than the
key describes, which is the same hole just closed in the VM's own verifier and
reachable here by anyone who can call the precompile.

The comment described the rule; now the code does.

Co-authored-by: Hanzo Dev <[email protected]>

zkvm/precompiles/zk_verifiers.go

@@ -122,9 +122,14 @@ func (v *Groth16Verifier) Run(input []byte) ([]byte, error) {
 		return resultInvalid, errInputTooShort
 	}
 
-	// Bound check: numInputs must match vk.K length minus 1 (K[0] is the constant term)
-	if int(numInputs)+1 > len(vk.K) {
-		return resultInvalid, errors.New("too many public inputs for verifying key")
+	// K holds one point per public input plus the constant term K[0], so the key
+	// states how many inputs its circuit takes. The caller supplies both the key
+	// and the count, and they have to agree: too many reads past the end of K,
+	// and too few leaves the trailing K points out of the linear combination
+	// below, judging the proof against a smaller statement than the key
+	// describes.
+	if want := len(vk.K) - 1; int(numInputs) != want {
+		return resultInvalid, fmt.Errorf("public inputs: %d supplied, the verifying key's circuit takes %d", numInputs, want)
 	}
 
 	witness := make([]fr.Element, numInputs)

zkvm/precompiles/zk_verifiers_test.go

@@ -621,3 +621,51 @@ func serializeGroth16Input(vk *groth16VK, proof *groth16Proof, witness []fr.Elem
 	}
 	return buf
 }
+
+// TestPublicInputCountMustMatchTheKeysCircuit. This precompile takes both the
+// verifying key and the public-input count from its caller's calldata, so a
+// caller picks both and they have to agree. K holds one point per public input
+// plus a constant term, so the key states how many its circuit takes. Too many
+// reads past the end of K; too few leaves the trailing K points out of the
+// linear combination, judging the proof against a smaller statement than the
+// key describes. Only the first was checked.
+func TestPublicInputCountMustMatchTheKeysCircuit(t *testing.T) {
+	_, _, g1, g2 := bn254.Generators()
+
+	// Three K points is a circuit taking two public inputs.
+	vk := &groth16VK{Alpha: g1, Beta: g2, Gamma: g2, Delta: g2,
+		K: []bn254.G1Affine{g1, g1, g1}}
+
+	var r fr.Element
+	r.SetRandom()
+	var rBI big.Int
+	var randG1 bn254.G1Affine
+	randG1.ScalarMultiplication(&g1, r.BigInt(&rBI))
+	proof := &groth16Proof{Ar: randG1, Bs: g2, Krs: g1}
+
+	witness := func(n int) []fr.Element {
+		out := make([]fr.Element, n)
+		for i := range out {
+			out[i].SetUint64(uint64(i + 1))
+		}
+		return out
+	}
+
+	v := &Groth16Verifier{}
+	for _, n := range []int{0, 1, 3, 7} {
+		if _, err := v.Run(serializeGroth16Input(vk, proof, witness(n))); err == nil {
+			t.Fatalf("%d public inputs judged against a circuit taking 2", n)
+		}
+	}
+
+	// The count the key states reaches the arithmetic and is answered on its
+	// merits — without this control the refusals above would prove only that
+	// this rejects everything.
+	result, err := v.Run(serializeGroth16Input(vk, proof, witness(2)))
+	if err != nil {
+		t.Fatalf("the count the key states must reach the pairing, got: %v", err)
+	}
+	if len(result) != 1 || result[0] != 0x00 {
+		t.Fatalf("a proof satisfying no statement must be rejected, got %x", result)
+	}
+}