circom/R1CS front-end: scribe import-r1cs#19
Conversation
New crates/r1cs-front: parses the iden3 .r1cs binary format (magic/version/ sections; header prime, wire counts; sparse A/B/C linear combinations) and the companion .sym signal map, then expands each rank-1 row ⟨A,w⟩·⟨B,w⟩ = ⟨C,w⟩ exactly into gadget-ir's sum-of-products form: - wire 0 (constant 1) contributes to coefficients, never monomials; like monomials merge mod p; zero rows drop - coefficients canonicalize to signed form (p−1 → -1) so the emitted theorem stays generic over the field; circuits whose arithmetic only means something at the exact header prime (wide canonical coefficients, e.g. constant inverses) are REJECTED with guidance rather than mistranslated (v1 scope, --max-coeff-bits) - .sym names sanitize to Lean binders (main.in[0] → in_0), including the Lean keyword collision that bites in practice: circom's ubiquitous 'in' → 'in_' - build_r1cs_bytes is public so tests and fixtures need no circom install; examples/gen_fixtures.rs generates a correct Num2Bits(2) and the classic circomlib IsZero missing-constraint bug at the real BN254 prime scribe import-r1cs --r1cs f.r1cs --sym f.sym --spec '...' emits reviewable gadget TOML (constraints machine-derived; the spec stays the human trust root — R1CS carries constraints, never intent). The whole existing pipeline consumes it unchanged. Live proof of life: imported the buggy IsZero fixture and ran scribe judge — prove phase correctly exhausted, refuter found the kernel-checked textbook counterexample (in = 1, inv = 0, out = 1) at iteration 1 → UNSOUND, exit 2. The first R1CS-format circuit judged end-to-end. README: front-ends reframed (TOML = reviewable fixture format; circuits enter via r1cs-front or halva-bridge), import-r1cs section with the circom → import → judge flow. 8 new parser/conversion tests; workspace green; clippy clean.
![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: 31340c5c35
ℹ️ 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".
| // Collect the wires that actually occur (excluding wire 0). | ||
| let mut used: std::collections::BTreeSet<u32> = std::collections::BTreeSet::new(); | ||
| for c in &r1cs.constraints { | ||
| for (w, _) in c.a.iter().chain(c.b.iter()).chain(c.c.iter()) { | ||
| if *w != 0 { | ||
| used.insert(*w); | ||
| } | ||
| } | ||
| } |
There was a problem hiding this comment.
When an R1CS wire appears in the .sym map but not in any rank-1 row, this collection drops it from gadget.witnesses. That breaks exactly the dangling-output audit case this repo models in benchmark/suite/19-neg-swap-unconstrained-output.toml:1-8: a spec mentioning the unconstrained signal will later emit Lean with an unbound identifier, or users must omit the signal and cannot get a refutation. The importer should preserve nonzero .sym wires (at least public inputs/outputs, and ideally all named wires) even when they have no terms.
Useful? React with 👍 / 👎.
1 participant
The circom front-end — from a compiled circuit binary to a judged verdict, using the whole existing pipeline unchanged:
What's in it
crates/r1cs-front: parser for the iden3.r1csbinary format (header prime, sparse A/B/C rows) +.symsignal map, and an exact expansion of each rank-1 row⟨A,w⟩·⟨B,w⟩ = ⟨C,w⟩into gadget-ir's sum-of-products form. Wire 0 handled as the constant; like monomials merged mod p; coefficients canonicalized to signed form (p−1→-1).--max-coeff-bits). Bit-decomposition / boolean / mux circuits — most of circomlib's core — convert cleanly and stay generic overp.inbecomesin_(caught live: the first import produced an unparseable binder).build_r1cs_bytesis public;examples/gen_fixtures.rsgenerates a correct Num2Bits(2) and the classic circomlib IsZero missing-constraint bug at the real BN254 prime.soundness_specstays the human trust root (R1CS carries constraints, never intent — the file header says so).Proof of life
Imported the buggy IsZero (the canonical audit bug:
in·out = 0dropped) and ranscribe judge:in = 1, inv = 0, out = 1at iteration 1README reframed: TOML is the fixture format; real circuits enter via
r1cs-front(circom) orhalva-bridge(halo2). 8 new tests; workspace green; clippy clean.Next (separate PRs): real circom-compiled circomlib binaries as fixtures + a disclosure-bug reproduction table.