Simplification substitution json format
The file contains a dictionary where the entries are the numbers of the simplified signals as a string and the values are the linear expression that has replaced the signal.
{
"sig_num_1": lin_expr_1,
...
"sig_num_n": lin_expr_n,
}
where the linear expression is represented by a dictionary with the signal numbers as strings occurring in the linear expression (with non-zero coefficient) as entries and their coefficients (as string) as values:
{ "sig_num_l1": "coef_1", ... , "sig_num_lm": "coef_m"}
All signals occurring in the linear expression are signals that are not removed. Hence, if you also include the --sym
flag, in the generated sym file all these signals are associated to a position in the witness list. On the other hand, al signals sig_num_1 ... sig_num_n that appear as entries in the substitution dictionary are associated to -1.
Let us consider the following simple circuit in 'simplify.circom':
pragma circom 2.0.0;
template Internal() {
signal input in[2];
signal output out;
out <== in[0]*in[1];
}
template Main() {
signal input in[2];
signal output out;
component c = Internal ();
c.in[0] <== in[0];
c.in[1] <== in[1]+2*in[0]+1;
c.out ==> out;
}
if we run
circom simplify.circom --r1cs --wasm --simplification_substitution
a file 'simplify_substitutions.json' is generated that contains
{
"5" : {"2":"1"},
"4" : {"1":"1"}
}
where we can see that two signals have been substituted (since the --O1
simplification is the default).
Instead, if we run
circom simplify.circom --r1cs --wasm --simplification_substitution --O0
to indicate that we do not want to apply any simplification, the generated file 'simplify_substitutions.json' contains
{
}
Finally, if we run
circom simplify.circom --r1cs --wasm --simplification_substitution --O2
to indicate that we want to apply the full form of simplification, the generated file 'simplify_substitutions.json' contains:
{
"5" : {"2":"1"},
"4" : {"1":"1"},
"6" : {"0":"1","2":"2","3":"1"}
}