[AdaWorldAPI]

CG-5 (Linear EXO-237), the bounded read-only probe allowed by D-CODEGRAPH-BOARD-RULING-2. Lab only: no row format, opcode, lowering, rewrite or per-query path. Independent of #2004 and #2006; based on main.

Question

foundry-parity-lab has four / sites (the ndarray PR 422 case). Two build one threshold before any row is read; two divide once per recipe ingredient. The effects rows of CG-8 find all four and cannot tell the kinds apart. Does a def-use derivation tell them apart, with a proof, and does it move when the code moves?

The expected answer was posted on EXO-237 before any derivation existed.

What is added

• crates/cg-defuse-probe (own workspace root, like egglog-r2il-probe): rows parser, egglog arm in proofs mode, plain fixpoint arm, source-only scan, 18 tests, a report example.
• .claude/probes/2026-11-11-cg5-defuse/: extract_defuse.py (LLBC to def-use rows), mutate.py, regenerate.sh, disable_runs.py with its receipt, REPORT.md.
• One board entry and the regenerated entries index.

Result

site	egglog (with proof)	plain fixpoint	source scan	loop nesting
method.rs:58	scalar	scalar	scalar	scalar
arm_b.rs:245	scalar	scalar	scalar	per-element (wrong)
arm_a.rs:75	per-element	per-element	per-element	per-element
oracle.rs:62	per-element	per-element	per-element	per-element

All three arms match the pre-registered table. Loop nesting is wrong on arm_b.rs:245, because Charon copies the tail of cook_ops into the loop's exit paths.

Mutants of method.rs, each run through Charon again:

mutant	egglog	loop nesting
m1: division by the loop element	flips to per-element	per-element
m2: division removed	site gone (16 to 15)	—
m3: same division moved into the loop	stays scalar	per-element (wrong)

• egglog and the plain fixpoint agree on all 63 sites of the four fixtures.
• 3 of the 11 Rem sites are unknown (divisor is a global place) and carry no proof.
• Disable runs: 24 guards, 24 red (disable_runs.receipt.tsv). Two guards were found without a test on the first run; one got a test, one was inert in the plain fixpoint and was removed.
• regenerate.sh was run after the fixtures were committed and changed no byte.

Cost (reported, not a gate)

One cold derivation with proofs: 1.65 to 2.10 s per crate (783 rows, 26 steps). The plain fixpoint over the same rows: about 1 ms. egglog adds the checked proof, not the answer.

Limits

• One crate, four division sites, three mutants.
• Rows are flow-insensitive and intraprocedural.
• "Per element" means per item of the loop the operand comes from (here: recipe ingredients), not per store row.
• The source scan also gets every case right here; it would miss a divisor that arrives through a helper or a renamed binding, and the crate has no such case.
• Def-use rows are not a store row kind. That is the CG-3 format decision (EXO-235).
• The crate has no CI workflow. Run cd crates/cg-defuse-probe && cargo test --release.

---

Generated by Claude Code

[coderabbitai]

Important

Draft PR not reviewed

Draft PRs are not automatically reviewed by default.

• Trigger a manual review

To automatically review draft PRs, update your CodeRabbit configuration:

reviews:
  auto_review:
    drafts: true

• Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

Share

• X
• Mastodon
• Reddit
• LinkedIn