There is a possible soundness concern where the implementation deviates from the Nova paper. Any feedback would be appreciated.
The Nova on-chain decider splits the check NIFS.V(r, U_n, u_n, T̄) = U_{n+1} into an in-circuit
half (step 6.1, the field elements u and x) and a native half (step 6.2, the commitments).
Neither half is joined to the other:
- The fold challenge
r is unconstrained. DeciderNovaGadget::fold_field_elements_gadget
receives it as _randomness and ignores it, and proof.r is not among the Groth16 public
inputs. The circuit derives its own Fiat-Shamir challenge and uses it for the field elements;
the verifier folds the commitments with whatever r the prover sent.
- The commitments folded natively are unauthenticated.
Decider::verify receives
running_commitments and incoming_commitments from the caller (in the Solidity verifier,
straight from calldata) and folds them, but nothing — in-circuit or natively — ties them to the
U_i / u_i that the circuit's hash check (step 3) binds to the IVC chain. Both are private
witnesses in the circuit.
Because the relaxed-R1CS check (step 1) uses a private, unconstrained error vector W_{i+1}.E,
gap 2 alone makes the entire statement forgeable: a prover picks any W, solves step 1 for
E := Az∘Bz − u'·Cz, commits to both with the public KZG SRS, and submits those commitments as the
"running instance" commitments. Every remaining check then passes honestly.
As a result Decider::verify accepts a proof for an arbitrary (i, z_0, z_i), using only public
artifacts — no witness, no IVC step, no interaction. Verified end-to-end (see PoC below).
There is a possible soundness concern where the implementation deviates from the Nova paper. Any feedback would be appreciated.
The Nova on-chain decider splits the check
NIFS.V(r, U_n, u_n, T̄) = U_{n+1}into an in-circuithalf (step 6.1, the field elements
uandx) and a native half (step 6.2, the commitments).Neither half is joined to the other:
ris unconstrained.DeciderNovaGadget::fold_field_elements_gadgetreceives it as
_randomnessand ignores it, andproof.ris not among the Groth16 publicinputs. The circuit derives its own Fiat-Shamir challenge and uses it for the field elements;
the verifier folds the commitments with whatever
rthe prover sent.Decider::verifyreceivesrunning_commitmentsandincoming_commitmentsfrom the caller (in the Solidity verifier,straight from calldata) and folds them, but nothing — in-circuit or natively — ties them to the
U_i/u_ithat the circuit's hash check (step 3) binds to the IVC chain. Both are privatewitnesses in the circuit.
Because the relaxed-R1CS check (step 1) uses a private, unconstrained error vector
W_{i+1}.E,gap 2 alone makes the entire statement forgeable: a prover picks any
W, solves step 1 forE := Az∘Bz − u'·Cz, commits to both with the public KZG SRS, and submits those commitments as the"running instance" commitments. Every remaining check then passes honestly.
As a result
Decider::verifyaccepts a proof for an arbitrary(i, z_0, z_i), using only publicartifacts — no witness, no IVC step, no interaction. Verified end-to-end (see PoC below).