Skip to content

Commit 0e20946

Browse files
chore: add circuit-flattening audit artifacts and generator scripts
Single-file flattened views of the protocol circuits for end-to-end auditing, plus the generator patch and regeneration scripts. Excludes noir-repo submodule changes (generator lives there as an uncommitted patch).
1 parent 64b0f16 commit 0e20946

24 files changed

Lines changed: 109786 additions & 0 deletions

circuit-flattening/README.md

Lines changed: 283 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,283 @@
1+
# Circuit flattening — single-file circuit artifacts for bug hunting
2+
3+
**This is an experiment.** The idea is to flatten each protocol circuit —
4+
normally spread across many files, libraries, and generic helpers in
5+
`noir-projects/noir-protocol-circuits/` — into a single self-contained file,
6+
on the theory that one concrete, fully-resolved file is easier for an AI to
7+
audit end-to-end than source code scattered across a dependency tree. It may
8+
turn out that none of these views beats reading the original source; that is
9+
part of what we are trying to find out. The originals are the source of truth
10+
and are never modified by this work.
11+
12+
## The three outputs
13+
14+
Two views per circuit, plus one file that chains several circuits together.
15+
None is compilable Noir — they are reading artifacts.
16+
17+
| Output | Scope | What it is | When to reach for it |
18+
|---|---|---|---|
19+
| `*.monomorphized-readable.nr` | one circuit | The compiler's monomorphized AST, printed with names restored. Every reachable function appears as its **own definition**; calls stay as calls. | Default starting point. Read one function at a time with its real name, then follow calls to other definitions in the same file. |
20+
| `*.monomorphized-inlined.nr` | one circuit | The **same** named view as `-readable.nr` but after an inlining pass collapses the constrained call tree into `main`, so the circuit reads top-to-bottom as one body. | When you want to trace data flow through a circuit without jumping between function definitions. |
21+
| `chain-example.inlined.nr` | a chain of circuits | The inlined `main` of each stage of one example kernel→rollup composition, concatenated in order with the hand-offs marked. | Cross-circuit reading: trace a value across folds and spot checks that fall *between* circuits. |
22+
23+
**`-readable` and `-inlined` are the same view, differing only by one pass**,
24+
and the author has no preference between them — both exist to find out which
25+
serves an auditor better. `-readable` is the monomorphized program as-is
26+
(`nargo compile --show-monomorphized`); `-inlined` is that same program after
27+
its constrained call tree is flattened into `main` (add `--inline-monomorphized`).
28+
Same names, same legend, same desugaring — `-inlined` just pastes most function
29+
bodies into their call sites. Both cover one entire circuit: every function
30+
reachable from `main`, with generics resolved to concrete sizes and globals to
31+
concrete values.
32+
33+
## `*.monomorphized-readable.nr`
34+
35+
The base view: the compiler's monomorphized AST for one circuit, names
36+
restored, every reachable function printed as its own definition with calls
37+
left as calls — you follow a call by jumping to its definition elsewhere in the
38+
file.
39+
40+
Reading guide:
41+
42+
- A **legend** at the top maps every source-level struct/enum/alias name to
43+
the structural tuple it monomorphized to. Function signatures use the
44+
source-level names; a type claimed by several distinct names (e.g. two
45+
single-`Field` wrapper structs) prints structurally instead, so a name in a
46+
signature is always trustworthy.
47+
- **Field accesses are named** (`self.vk_data.leaf_index`), recovered from the
48+
HIR at monomorphization time — not guessed.
49+
- **`unsafe { ... }` marks every call from constrained code into an
50+
unconstrained function.** Nothing inside the callee emits gates, so any
51+
value it returns is prover-supplied and must be re-checked by constrained
52+
code nearby — a prime place for bugs to hide. `unconstrained fn` definitions
53+
are also labeled.
54+
- This output is faithful by construction (it is the compiler's own IR), but
55+
it is **not compilable Noir** — structs are tuples, `match`es are
56+
desugared, and legend lines such as `type Foo<Bar, 64> = ...` are not valid
57+
syntax.
58+
59+
Caveats:
60+
61+
- Compiler-synthesized accesses (closure environments, function tuples) still
62+
print positionally (`.0`, `.1`).
63+
- A tuple-destructure `let (a, b) = e;` desugars to a temp plus field
64+
extractions, printed as `let _ = e; let a = _.0; let b = _.1;`. The `_` is
65+
the temp (the monomorphizer names the extraction idents by index; they are
66+
rendered as `_` so `_.0` does not read as the float `0.0` — Noir has no
67+
float literals).
68+
- `if (!is_unconstrained()) { ... }` guards and `should_validate_output()`
69+
come from the simulated/constrained code sharing; in the constrained
70+
circuit the guard body is live.
71+
72+
## `*.monomorphized-inlined.nr`
73+
74+
The `-readable` view after the inlining pass (see the at-a-glance note above
75+
for how the two relate). Each constrained call is replaced by the callee's
76+
body pasted in at the call site: where `-readable.nr` shows `main` calling
77+
`validate_x(...)` defined further down, `-inlined.nr` has `validate_x`'s body
78+
inline in `main`, so the circuit reads top-to-bottom as one body. Details of
79+
the inlined form:
80+
81+
- Each inlined call site appears as a scope block opening with a
82+
`// >>> inlined call: <function>` marker, then `let <param> = <arg>;`
83+
bindings, then the callee body. Where an argument expression mentions a
84+
name equal to a callee parameter name, arguments are first bound to
85+
`__arg_N` temporaries so the printed text cannot read as capturing the
86+
wrong variable.
87+
- **Not inlined, by design:** unconstrained functions (they remain
88+
`unsafe { ... }` calls — nothing in them is constrained),
89+
`#[fold]`/`#[no_predicates]` functions (separate compilation units), and
90+
functions called from several constrained call sites with large bodies
91+
(crypto primitives and generated `eq`-style helpers — inlining them would
92+
bury protocol logic under duplicated primitive bodies). Those remain as
93+
named functions after `main`.
94+
- Verification: the inlined AST is the program that actually compiles when
95+
the flag is set, so generation doubles as validation. For
96+
`private_kernel_inner`: full `nargo info` opcode/gate table is identical
97+
with and without the flag, and execution outputs match on test programs.
98+
(Bytecode bytes differ only in witness numbering order.)
99+
100+
## `chain-example.inlined.nr`
101+
102+
A **separate experiment**: a combined, **non-compilable** artifact for
103+
cross-circuit reading — tracing a value across folds to find a check that
104+
should span a hand-off but is owned by no single circuit. `build_chain.py`
105+
takes the `-inlined` `main` of each stage of one example composition, in order
106+
— `init → inner → reset → inner → reset-tail-to-public → hiding-to-public →
107+
rollup-tx-base-public` — renames each to `main__<stage>`, joins them with
108+
`// STAGE` / `// JOIN` markers, and appends one deduplicated set of the shared
109+
type legend, globals, and helper definitions. (It reads the `-inlined` files,
110+
so generate those first; `flatten-circuits.sh` does both.)
111+
112+
It does **not** fuse the stages into one circuit — they stay separate proofs.
113+
The hand-offs (`return_data` of one stage == `call_data` of the next) are
114+
enforced by barretenberg's CHONK databus + recursion, **not** by any Noir
115+
assert, hence the `// JOIN` markers; and the prover chooses the composition, so
116+
this is ONE legal instance, not the only shape. Verify any finding against the
117+
real per-circuit source. (The two `inner` stages are byte-identical.) The
118+
`-inlined` inputs are trimmed via `--no-inline-fns` so sha256, the AVM column
119+
map, and `Serialize` plumbing stay as single named definitions instead of being
120+
duplicated inline.
121+
122+
## Regenerating
123+
124+
All generated `.nr` files land in `output/`, alongside
125+
`circuits-source-commit.txt` — a small record of the repo commit the artifacts
126+
were generated from (the outer repo's `HEAD`, which fixes both the circuit
127+
source and the noir pin). `flatten-circuits.sh` uses it to tell you whether
128+
your checkout has moved since the artifacts were last generated.
129+
130+
Three scripts, deliberately separate:
131+
132+
- **`./apply-patch.sh`** — first-time setup. Applies the generator patch to the
133+
noir submodule working tree (where the generator lives but is not committed),
134+
so nargo can be built with the extra flags. Safe to re-run: it reports and
135+
exits if the patch is already applied, and stops with a pointer to the
136+
recovery instructions if the patch no longer fits.
137+
- **`./flatten-circuits.sh`** — the common path. Rebuilds nargo, regenerates
138+
both per-circuit variants (`-readable` and `-inlined`) for every circuit in
139+
its list, and reassembles `chain-example.inlined.nr` from the `-inlined`
140+
files — so a full run produces all three output types. Before doing the work
141+
it compares your current commit against the one recorded in
142+
`output/circuits-source-commit.txt`, tells you whether your checkout is newer,
143+
older, or diverged, and asks whether to bother regenerating (`--yes` skips the
144+
prompt; non-interactive runs proceed). A successful full run rewrites that
145+
record. Pass package names to limit it (e.g.
146+
`./flatten-circuits.sh private_kernel_inner`); a subset run skips the prompt
147+
and leaves the record unchanged. It never touches the patch.
148+
- **`./export-patch.sh`** — maintainer-only, the inverse of `apply-patch.sh`.
149+
Re-exports the generator from the submodule working tree into
150+
`noir-circuit-flattening.patch`. Run it after ANY edit to the submodule's
151+
monomorphization/driver code so the patch cannot drift. Two guards: it refuses
152+
to write an empty/tiny diff (so a clean submodule can't clobber the patch),
153+
and it asks for confirmation before overwriting. Pass `--yes` to skip the
154+
prompt in automation; run non-interactively without it and it refuses rather
155+
than guess.
156+
157+
So a fresh setup is just:
158+
159+
```bash
160+
cd circuit-flattening
161+
./apply-patch.sh
162+
./flatten-circuits.sh
163+
```
164+
165+
The patch is recorded against submodule commit
166+
`c57152f91260ecdb9faad4efc20abb14b6d2ece7`. The rest of this section shows the
167+
underlying per-package commands `flatten-circuits.sh` runs, for one-offs or
168+
debugging.
169+
170+
The **readable** variant is just `--show-monomorphized`:
171+
172+
```bash
173+
cd noir-projects/noir-protocol-circuits
174+
../../noir/noir-repo/target/release/nargo compile \
175+
--package private_kernel_inner --show-monomorphized --silence-warnings \
176+
> ../../circuit-flattening/output/private-kernel-inner.monomorphized-readable.nr
177+
```
178+
179+
For the **inlined** variant, add `--inline-monomorphized`. Also pass
180+
`--no-inline-fns` with the comma-separated keep-as-calls list — without it,
181+
crypto and serialization bodies (sha256, the AVM column map, `Serialize`
182+
plumbing) get duplicated inline at every call site and bury the protocol
183+
logic. Use the exact list from the `NO_INLINE` variable in
184+
`flatten-circuits.sh` so the output matches the committed file:
185+
186+
```bash
187+
cd noir-projects/noir-protocol-circuits
188+
../../noir/noir-repo/target/release/nargo compile \
189+
--package private_kernel_inner --inline-monomorphized \
190+
--no-inline-fns "sha256_var,sha256_compression,...<see NO_INLINE in flatten-circuits.sh>" \
191+
--show-monomorphized --silence-warnings \
192+
> ../../circuit-flattening/output/private-kernel-inner.monomorphized-inlined.nr
193+
```
194+
195+
Finally, assemble the chain artifact from the per-circuit `-inlined` files
196+
(this step is **not** needed if you ran `./flatten-circuits.sh`, which does it
197+
for you; run it by hand only when regenerating the inlined files manually):
198+
199+
```bash
200+
cd circuit-flattening
201+
python3 build_chain.py
202+
```
203+
204+
The patch changes (all in the noir submodule):
205+
206+
- `monomorphization/ast.rs`: `ExtractTupleField` and `LValue::MemberAccess`
207+
carry the original struct field name (`Option<String>`, printing only).
208+
- `monomorphization/mod.rs`: lowering populates those names; a thread-local
209+
recorder captures `type name -> structural type` for every converted
210+
struct/enum/alias plus the HIR signature names of every monomorphized
211+
function (enabled only for `--show-monomorphized`).
212+
- `monomorphization/printer.rs`: `show_field_names` + `readable_type_names`
213+
options, the legend, name substitution in signatures/globals, reliable
214+
`unsafe { }` marking of constrained->unconstrained calls, and a fix for
215+
doubled semicolons.
216+
- `monomorphization/inliner.rs`: the inlining pass behind
217+
`--inline-monomorphized` (runs before codegen, so compiling validates it).
218+
- `noirc_driver/src/lib.rs`: `--show-monomorphized` uses the readable printer;
219+
`--inline-monomorphized` runs the inliner on the program that compiles.
220+
221+
## If the patch no longer applies
222+
223+
The patch is a unified diff — a text record of "remove these lines, add those"
224+
at specific places in 17 noir files, each hunk anchored by a few lines of
225+
surrounding context. `git apply` replays those hunks onto the current files.
226+
When the noir submodule advances to a new commit and upstream edits land near
227+
the patched code, the recorded context stops matching and `git apply` rejects
228+
the affected hunks instead of guessing — the apply fails with messages like
229+
`error: patch failed: ... ` / `error: ... patch does not apply`. That is what
230+
"the patch is outdated" means: the diff is fine, it just no longer lines up
231+
with the new files. You then reconcile it, much like resolving a merge.
232+
233+
The patch was recorded against submodule commit
234+
`c57152f91260ecdb9faad4efc20abb14b6d2ece7` (see above). If a plain
235+
`git apply` fails after the submodule moves, recover in this order:
236+
237+
1. **3-way merge (try this first).** The patch carries blob hashes
238+
(`index <old>..<new>` lines), so git can merge it against the new files
239+
the same way it merges branches:
240+
241+
```bash
242+
cd noir/noir-repo
243+
git apply --3way ../../circuit-flattening/noir-circuit-flattening.patch
244+
```
245+
246+
Hunks that still fit apply silently. Where upstream changed the same
247+
region, git leaves ordinary `<<<<<<< / ======= / >>>>>>>` conflict markers
248+
in the file — open each one, keep both intents (the upstream change *and*
249+
the patch's change), and delete the markers. This needs the patch's base
250+
blobs in the object store; they are, since it's the same submodule history.
251+
252+
2. **Reject files (fallback if `--3way` can't merge).** Apply every hunk that
253+
still fits and write the failures out as `.rej` files:
254+
255+
```bash
256+
cd noir/noir-repo
257+
git apply --reject ../../circuit-flattening/noir-circuit-flattening.patch
258+
```
259+
260+
Each `<file>.rej` lists the hunks that did not apply; edit those changes
261+
into the corresponding file by hand, then delete the `.rej` files. The
262+
"patch changes" list above tells you the intent of each file's edits, so
263+
you know what the rejected hunk was trying to achieve.
264+
265+
3. **Re-validate and re-record.** Once the working tree compiles, re-export
266+
the patch from the now-reconciled working tree, then rebuild and regenerate
267+
the artifacts:
268+
269+
```bash
270+
cd circuit-flattening
271+
./export-patch.sh # patch now anchored to the new files
272+
./flatten-circuits.sh # rebuild nargo + regenerate all three outputs
273+
```
274+
275+
Then update the recorded base-commit hash in this README (the
276+
`c571...` value above) to the submodule commit you reconciled against, so
277+
the next person starts from an accurate anchor. Commit the refreshed
278+
`noir-circuit-flattening.patch` together with that README change.
279+
280+
If upstream has restructured the monomorphizer enough that a hunk no longer
281+
has a sensible home, treat the "patch changes" list as the spec and re-apply
282+
that *intent* to the new code rather than forcing the old text in — then
283+
re-export as above.

circuit-flattening/apply-patch.sh

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
#!/usr/bin/env bash
2+
# Apply the generator patch to the noir submodule working tree, so nargo can be
3+
# built with the --show-monomorphized / --inline-monomorphized flags. This is
4+
# the inverse of export-patch.sh, and the first step of a fresh setup:
5+
# ./apply-patch.sh
6+
# ./flatten-circuits.sh # builds nargo + generates the artifacts
7+
#
8+
# Safe to re-run: if the patch is already applied it reports that and exits 0.
9+
# If the patch no longer fits (the submodule has moved), it stops and points to
10+
# the recovery instructions instead of leaving a half-applied tree.
11+
set -euo pipefail
12+
13+
FLAT="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
14+
ROOT="$(cd "$FLAT/.." && pwd)"
15+
NOIR="$ROOT/noir/noir-repo"
16+
PATCH="$FLAT/noir-circuit-flattening.patch"
17+
18+
# If the patch can be reversed, it is already applied.
19+
if git -C "$NOIR" apply --reverse --check "$PATCH" 2>/dev/null; then
20+
echo "patch already applied to $NOIR — nothing to do."
21+
exit 0
22+
fi
23+
24+
if ! git -C "$NOIR" apply --check "$PATCH" 2>/dev/null; then
25+
echo "error: patch does not apply cleanly to $NOIR." >&2
26+
echo " The submodule has likely advanced since the patch was recorded." >&2
27+
echo " See \"If the patch no longer applies\" in README.md." >&2
28+
exit 1
29+
fi
30+
31+
git -C "$NOIR" apply "$PATCH"
32+
echo "applied patch to $NOIR. Next: ./flatten-circuits.sh"

0 commit comments

Comments
 (0)