Skip to content

Commit b095511

Browse files
jeswrclaude
andauthored
test(proof-methods): tamper checks for both Noir openings and a gate-count script (#6816)
* test(proof-methods): tamper checks for both Noir openings and a gate-count script tamper.py now takes the circuit to check. For the Noir circuits it changes outputs of unconstrained hints, sampled per hint function (the rotation and carry hints, the compiler's division and inverse hints), skipping an is-zero inverse whose input is zero, which the check leaves free by design. gates.sh prints each circuit's UltraHonk gate count as JSON lines. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015CB7XiW3NDsggNCuDcuJJo * docs(proof-methods): describe tamper.py as a smoke test; syntax-check gates.sh tamper.py changes one witness without re-solving its dependents, so a rejection does not show the hint's own constraints are complete. Say so in the script and README. bash -n parses only its first operand, so check run.sh and gates.sh separately. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015CB7XiW3NDsggNCuDcuJJo --------- Co-authored-by: Claude <noreply@anthropic.com>
1 parent 41f7fa5 commit b095511

4 files changed

Lines changed: 110 additions & 30 deletions

File tree

‎.github/workflows/proof-methods.yml‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -66,6 +66,7 @@ jobs:
6666
python3 -m unittest proof-methods/vole/test_acir_to_sieve.py
6767
python3 -m py_compile proof-methods/acir/blake3_leaf.py proof-methods/acir/tamper.py
6868
bash -n proof-methods/acir/run.sh
69+
bash -n proof-methods/acir/gates.sh
6970
python3 -m unittest proof-methods/acir/test_blake3_leaf.py
7071
7172
- name: Measurement example runs

‎proof-methods/acir/README.md‎

Lines changed: 13 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -42,16 +42,25 @@ is written, and from writing ACIR by hand. `circuits/baseline` calls `full_u64_c
4242
# nargo and bb at the versions CI pins for zk/compose
4343
NARGO=nargo BB=bb proof-methods/acir/run.sh 0 9 10 999999999999999999 \
4444
1000000000000000000 9999999999999999999 10000000000000000000 18446744073709551615
45-
bb gates -s ultra_honk -b proof-methods/acir/circuits/target/hand.json
46-
BB=bb python3 proof-methods/acir/tamper.py 30
45+
BB=bb proof-methods/acir/gates.sh
46+
for c in hand noir_var noir_tuned; do BB=bb python3 proof-methods/acir/tamper.py "$c" 15; done
4747
python3 -m unittest proof-methods/acir/test_blake3_leaf.py
4848
```
4949

5050
`run.sh` proves and verifies all four circuits for the given values, with
5151
bounds that do not reveal them. It does not pin tool versions or thread
5252
counts; compare timings only from one machine and one toolchain.
53-
`tamper.py` changes one witness of the hand-written circuit at a time and
54-
checks that the proof fails. Measurements are kept outside the repository.
53+
`gates.sh` prints each circuit's UltraHonk gate count. `tamper.py` changes
54+
one prover-chosen witness at a time (in the hand-written circuit, an appended
55+
witness; in the Noir circuits, a hint output, sampled per hint function) and
56+
checks that the proof fails. It is a smoke test for hint outputs the circuit
57+
leaves unconstrained, not evidence that the constraints are complete: it does
58+
not re-solve the witnesses that depend on the changed one, so a rejection can
59+
come from those stale values rather than from the hint's own constraints, and
60+
it samples rather than covering every call site. Completeness rests on review
61+
of the generator and the Noir source, and, for the hand-written additions, on
62+
the unit test that bounds every addition result. Measurements are kept
63+
outside the repository.
5564

5665
Research prototype, not externally audited. It covers the unsigned opening
5766
only; `full_i64_check` has the same structure.

‎proof-methods/acir/gates.sh‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
#!/usr/bin/env bash
2+
# Prints the UltraHonk gate count of each circuit run.sh built, one JSON
3+
# object per line. Run run.sh first; leaf::N sets the number of openings.
4+
set -euo pipefail
5+
cd "$(dirname "$0")/circuits"
6+
BB=${BB:-bb}
7+
n=$(sed -n 's/^pub global N: u32 = \([0-9]*\);/\1/p' leaf/src/lib.nr)
8+
for p in baseline noir_var noir_tuned spliced hand; do
9+
gates=$("$BB" gates -s ultra_honk -b "target/$p.json" 2>/dev/null \
10+
| python3 -c 'import json,sys; print(json.load(sys.stdin)["functions"][0]["circuit_size"])')
11+
printf '{"circuit": "%s", "openings": %s, "ultra_honk_gates": %s}\n' "$p" "$n" "$gates"
12+
done

‎proof-methods/acir/tamper.py‎

Lines changed: 84 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,27 @@
11
#!/usr/bin/env python3
2-
"""Soundness spot check for the hand-written opening, after run.sh.
2+
"""Smoke test for unconstrained hint outputs in the openings, after run.sh.
33
4-
Changes one witness of circuits/target/hand.gz at a time (adds 1) and checks
5-
that UltraHonk proving or verification fails. XOR outputs are skipped:
6-
Barretenberg recomputes them from the inputs, so changing one in the witness
7-
file changes nothing.
4+
Changes one prover-chosen witness of circuits/target/CIRCUIT.gz at a time
5+
(adds 1) and checks that UltraHonk proving or verification fails:
86
9-
Usage: tamper.py SAMPLES [SEED] (BB names the bb binary, default `bb`)
7+
- hand: any witness the generator appended (digits, selectors, rotation and
8+
carry splits, message words, digest bytes);
9+
- noir_var, noir_tuned: any output of an unconstrained (Brillig) hint,
10+
sampled per hint function, so the rotation (`split`) and carry
11+
(`carry_split`) hints of noir_tuned and the compiler's division and
12+
inverse hints are each exercised. An inverse hint whose input is zero is
13+
skipped: an is-zero check leaves it free by design.
14+
15+
This does not show that the constraints are complete. Witnesses that depend
16+
on the changed one are not re-solved, so a change can be rejected by an
17+
equation further on that sees a stale value, even if the hint's own range
18+
check were missing; and each group is sampled, not every call site.
19+
20+
XOR outputs are skipped: Barretenberg recomputes them from the inputs, so
21+
changing one in the witness file changes nothing.
22+
23+
Usage: tamper.py CIRCUIT SAMPLES [SEED] (SAMPLES per group; BB names the bb
24+
binary, default `bb`)
1025
"""
1126

1227
import base64
@@ -28,42 +43,85 @@ def load(path):
2843
return m.unpack(gzip.decompress(f.read()))
2944

3045

31-
def accepted(witness):
46+
def accepted(circuit, witness):
3247
path, out = os.path.join(T, "tamper.gz"), os.path.join(T, "tamper")
3348
with open(path, "wb") as f:
3449
f.write(gzip.compress(m.pack([[[0, witness]]])))
3550
os.makedirs(out, exist_ok=True)
36-
vk = os.path.join(T, "proof-hand", "vk")
51+
vk = os.path.join(T, f"proof-{circuit}", "vk")
3752

3853
def run(*args):
3954
return subprocess.run([BB, *args], capture_output=True, check=False).returncode == 0
4055

41-
return run("prove", "-s", "ultra_honk", "-b", os.path.join(T, "hand.json"), "-w", path,
56+
return run("prove", "-s", "ultra_honk", "-b", os.path.join(T, f"{circuit}.json"), "-w", path,
4257
"-k", vk, "-o", out) and \
4358
run("verify", "-s", "ultra_honk", "-p", os.path.join(out, "proof"), "-k", vk,
4459
"-i", os.path.join(out, "public_inputs"))
4560

4661

62+
def value(expr, witness):
63+
products, linear, const = expr
64+
v = int.from_bytes(const, "big")
65+
for q, a, b in products:
66+
v += int.from_bytes(q, "big") * int.from_bytes(witness[a], "big") * int.from_bytes(witness[b], "big")
67+
for q, a in linear:
68+
v += int.from_bytes(q, "big") * int.from_bytes(witness[a], "big")
69+
return v % m.P
70+
71+
72+
def hint_outputs(program, witness):
73+
"""Outputs of each unconstrained (Brillig) hint, grouped by function name.
74+
75+
The inverse hint of an is-zero check is free when its input is zero (any
76+
value satisfies the check, and nothing else reads it), so those are left
77+
out."""
78+
names = [f[0] for f in program[1]]
79+
groups = {}
80+
for op in program[0][0][2]:
81+
if "BrilligCall" in op:
82+
fid, inputs, outputs = op["BrilligCall"][:3]
83+
if names[fid] == "directive_invert" and value(inputs[0]["Single"], witness) == 0:
84+
continue
85+
out = groups.setdefault(names[fid], set())
86+
for item in outputs:
87+
if "Simple" in item:
88+
out.add(item["Simple"])
89+
else:
90+
out.update(item["Array"])
91+
return groups
92+
93+
4794
def main():
48-
samples = int(sys.argv[1])
49-
random.seed(int(sys.argv[2]) if len(sys.argv) > 2 else 1)
50-
with open(os.path.join(T, "hand.json"), encoding="utf-8") as f:
95+
circuit, samples = sys.argv[1], int(sys.argv[2])
96+
random.seed(int(sys.argv[3]) if len(sys.argv) > 3 else 1)
97+
with open(os.path.join(T, f"{circuit}.json"), encoding="utf-8") as f:
5198
artifact = json.load(f)
52-
opcodes = m.unpack(gzip.decompress(base64.b64decode(artifact["bytecode"])))[0][0][2]
53-
xor_out = {op["BlackBoxFuncCall"]["XOR"][3] for op in opcodes
99+
program = m.unpack(gzip.decompress(base64.b64decode(artifact["bytecode"])))
100+
xor_out = {op["BlackBoxFuncCall"]["XOR"][3] for op in program[0][0][2]
54101
if "XOR" in op.get("BlackBoxFuncCall", {})}
55-
first = max(load(os.path.join(T, "spliced.gz"))[0][0][1]) + 1
56-
witness = load(os.path.join(T, "hand.gz"))[0][0][1]
57-
assert accepted(witness), "the untampered witness must prove and verify"
58-
added = sorted(k for k in witness if k >= first and k not in xor_out)
59-
bad = []
60-
for k in random.sample(added, samples):
61-
w = dict(witness)
62-
w[k] = m.fb(int.from_bytes(w[k], "big") + 1)
63-
if accepted(w):
64-
bad.append(k)
65-
print(json.dumps({"tampered": samples, "accepted": bad}))
66-
sys.exit(1 if bad else 0)
102+
witness = load(os.path.join(T, f"{circuit}.gz"))[0][0][1]
103+
assert accepted(circuit, witness), "the untampered witness must prove and verify"
104+
if circuit == "hand":
105+
first = max(load(os.path.join(T, "spliced.gz"))[0][0][1]) + 1
106+
groups = {"appended": {k for k in witness if k >= first}}
107+
else:
108+
groups = hint_outputs(program, witness)
109+
report = {}
110+
failed = False
111+
# Up to SAMPLES changes per group, so every kind of hint is exercised.
112+
for name, chosen in sorted(groups.items()):
113+
candidates = sorted(chosen - xor_out)
114+
picked = random.sample(candidates, min(samples, len(candidates)))
115+
bad = []
116+
for k in picked:
117+
w = dict(witness)
118+
w[k] = m.fb(int.from_bytes(w[k], "big") + 1)
119+
if accepted(circuit, w):
120+
bad.append(k)
121+
report[name] = {"candidates": len(candidates), "tampered": len(picked), "accepted": bad}
122+
failed |= bool(bad)
123+
print(json.dumps({"circuit": circuit, "groups": report}))
124+
sys.exit(1 if failed else 0)
67125

68126

69127
if __name__ == "__main__":

0 commit comments

Comments
 (0)