ensure constraints in Circom circuits are generated correctly

[yushihang]

While studying Zeto’s open-source code, I have learned a lot from it, and I want to thank you for sharing the codes and youtube videos.

I have a question regarding the template CheckSum():

zeto/zkp/circuits/lib/check-sum.circom

Lines 31 to 45 in aa3c1fd

	template CheckSum(numInputs, numOutputs) {
	signal input inputValues[numInputs];
	signal input outputValues[numOutputs];
	// check that the sum of input values equals the sum of output values
	var sumInputs = 0;
	for (var i = 0; i < numInputs; i++) {
	sumInputs = sumInputs + inputValues[i];
	}
	var sumOutputs = 0;
	for (var i = 0; i < numOutputs; i++) {
	sumOutputs = sumOutputs + outputValues[i];
	}
	assert(sumInputs == sumOutputs);
	}

From the circom code, it seems that the checksum() does not add any constraints to the input signals, but instead uses assert() for validation.

In the Circom documentation (https://docs.circom.io/circom-language/code-quality/code-assertion/), it mentions that assert is effective during the compilation and witness generation stages, but it does not explicitly state whether assert() applies during the verification stage.

In my understanding, during the verification phase, the verifier has access to the QAP and the associated proof information. If assertions are not converted into r1cs, would they not be effective during the verification phase?

Therefore, I am a bit unsure if this approach is sufficiently secure.

Once again, thank you for your help.

[Chengxuan]

Thanks for catching this @yushihang you are correct, assert does not generate constraints and should only be used to catch compilation errors and quick checks for dev purposes.

[Chengxuan]

Recording the steps to reproduce the problem:

1. follow the normal workflow to validate proof generation for validate inputs should pass verifier check. Example commands:

circom ./lib/check-sum.circom --r1cs --sym --wasm
snarkjs groth16 setup check-sum.r1cs $PTAU_DOWNLOAD_PATH/powersOfTau28_hez_final_09.ptau check-sum.zkey
snarkjs zkey export verificationkey check-sum.zkey check-sum.json
snarkjs groth16 fullprove input.json check-sum_js/check-sum.wasm check-sum.zkey proof.json public.json
snarkjs groth16 verify check-sum.json public.json proof.json
# verification should return success result
snarkjs groth16 fullprove hack_input.json check-sum_js/check-sum.wasm check-sum.zkey proof.json public.json
# proof generation should fail due to assertion error

input.json:

{ "inputValues": ["1", "2"], "outputValues": ["1", "2"] }

hack_input.json:

{ "inputValues": ["1", "2"], "outputValues": ["11", "22"] }

2. remove the sum check assertion from check-sum.circom, compile the circuit again and generate the proof using hack_input.json should now be successful and pass the proof verification 🐞 :

circom ./lib/check-sum.circom --r1cs --sym --wasm
snarkjs groth16 fullprove hack_input.json check-sum_js/check-sum.wasm check-sum.zkey proof.json public.json
snarkjs groth16 verify check-sum.json public.json proof.json
# verification should return success result, which proves the prover manage to bypass the assertion with a modified version of circuit. as the checks done by assertions do not generate constraints

Appendix:

check-sum.circom:

template CheckSum(numInputs, numOutputs) { signal input inputValues[numInputs]; signal input outputValues[numOutputs];

signal output b;

// check that the sum of input values equals the sum of output values
var sumInputs = 0;
for (var i = 0; i < numInputs; i++) {
sumInputs = sumInputs + inputValues[i];
}
var sumOutputs = 0;
for (var i = 0; i < numOutputs; i++) {
sumOutputs = sumOutputs + outputValues[i];
}
// assert(sumInputs == sumOutputs);

b <== inputValues[0] * inputValues[1];
}

component main = CheckSum(2,2);