LF+ WE gate: enforce statement binding via Ajtai exposed-prefix (SP1 digest) + fail-closed checks #2
Conversation
- Add explicit check that `setchk::Out.r` matches the transcript-derived sumcheck point. - Propagate `Dcom`/set-check failures instead of panicking, and plumb errors through `CmProof::verify_with_mlen`. - In WE arith, expose `dcom.out.r` vars for CM and glue them to the setchk-derived `r`.
This reverts commit 9500c7a.
This reverts commit 8167cdb.
This reverts commit bca2f2f.
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 9a73d43d7e
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| for lp in &proof.lproof { | ||
| lp.verify(&mut self.transcript); | ||
| } |
There was a problem hiding this comment.
When public inputs are non-empty, the prover now absorbs them into the transcript before any Fiat–Shamir challenges are sampled, but PlusVerifier::verify starts verifying lproof immediately on the current transcript. This means a typical verifier created with a fresh transcript will derive different challenges and reject an otherwise valid proof unless the caller manually pre-absorbs the same public inputs. To avoid this regression, the verifier should either accept public_inputs and absorb them before lproof, or document/enforce that callers must do so.
Useful? React with 👍 / 👎.
When public inputs are non-empty, the prover now absorbs them into the transcript before any Fiat–Shamir challenges are sampled, but PlusVerifier::verify starts verifying lproof immediately on the current transcript. This means a typical verifier created with a fresh transcript will derive different challenges and reject an otherwise valid proof unless the caller manually pre-absorbs the same public inputs. To avoid this regression, the verifier should either accept public_inputs and absorb them before lproof, or document/enforce that callers must do so.
|
@codex review |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 84bbf1e30e
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| const EXPOSE_MAX: usize = 8; | ||
| let expose_rows = EXPOSE_MAX.min(kappa); | ||
| if expose_rows > 0 { |
There was a problem hiding this comment.
The Dcom-prefix binding in the WE-gate hard-codes EXPOSE_MAX = 8 and uses min(kappa, 8) to decide how many cm_f coordinates to equate with public_inputs. This ignores the actual expose_rows configured in AjtaiCommitmentScheme::seeded_with_exposed_prefix. If a proof is built with a different exposure size (e.g., expose_rows = 4 with kappa = 16, or expose_rows = 0 for a non-binding configuration), the WE-gate will still require 8 public inputs and enforce equality on cm_f[0..8), causing otherwise valid proofs to fail verification or to enforce the wrong binding. The binding length should come from the Ajtai exposure configuration (or be passed in via params) instead of being fixed at 8.
Useful? React with 👍 / 👎.
This PR makes statement binding verifier-enforced end-to-end for the LF+ → WE/DPP path by tying the SP1 statement digest (public inputs) to the committed witness via Ajtai prefix exposure, and ensuring the full PlusProof WE gate actually enforces the same binding constraints as native verification.
Key changes
latticefoldcommitment scheme so selectedcm_fcoordinates expose fixed witness slots for cheap equality checks.crates/latticefold/src/commitment/commitment_scheme.rsDcom/Cmverification supports anexpected_prefixand checkscm_f[0..E)matches it (constant-coeff), preventing “same witness, different statement”.crates/latticefold-plus/src/rgchk.rs,crates/latticefold-plus/src/cm.rspublic_inputsinto the Dcom gadget and glues them, so the in-circuit constraints includecm_f[0..E) == public_inputs[0..E)instead of silently skipping.crates/latticefold-plus/src/we_gate_arith.rspublic_inputsare missing/too short orL != 1in the SP1 streamed/WE setting.crates/latticefold-plus/src/we_gate_arith.rs,crates/latticefold-plus/src/rgchk.rsLFP_WE_GATE_DIGEST_V1is no longer[0;32](now a stable nonzero label).crates/latticefold-plus/src/we_statement.rsSecurity impact
Test plan
latticefold-plusWE gate tests; specifically the “flip public input” negative test now becomes UNSAT in the full WE gate.FLIP_PUBLIC_INPUT0=1and (optionally)LFP_SKIP_PREFIX_BINDING_CHECK=1to confirm native can be skipped for debugging but WE still fails.Oneproof output log: