probe(cg-5): def-use rows closed by egglog classify division sites

.claude/board/entries/2026-11-11-cg5-defuse-probe.md

@@ -0,0 +1,21 @@
+# 2026-11-11 — CG-5: def-use rows classify division sites; loop nesting does not
+
+**Status:** MEASURED (probe). `.claude/probes/2026-11-11-cg5-defuse/`, `crates/cg-defuse-probe`. Board: EXO-237.
+
+Def-use rows from Charon LLBC (783 rows, 16 `Div`/`Rem` sites in `foundry-parity-lab`) were closed
+three ways: egglog in proofs mode, a plain fixpoint, and a source-only scan. All three give the
+answer fixed beforehand on EXO-237: `method.rs:58` and `arm_b.rs:245` are scalar thresholds,
+`arm_a.rs:75` and `oracle.rs:62` are per-element quotients. egglog and the fixpoint agree on all 63
+sites of the four fixtures.
+
+**Finding:** loop nesting of the LLBC statement is wrong on `arm_b.rs:245` (Charon copies the tail
+of `cook_ops` into the loop's exit paths) and on mutant m3 (scalar division moved into the loop).
+Operand provenance is right on both.
+
+Mutants: division by the loop element flips the class; removing the division removes the site.
+24 disable runs, 24 red.
+
+Cost, reported and not a gate: egglog 1.65 to 2.10 s cold per crate with proofs; plain fixpoint
+about 1 ms. egglog adds the proof, not the answer.
+
+OPEN: def-use rows as a store row kind (CG-3 format decision, EXO-235); interprocedural provenance.

.claude/board/entries/README.md

@@ -25,12 +25,13 @@ index row, (3) no duplicate entry id. Checks 1 and 2 are deliberately
 opposite directions; the stranding this convention prevents shows up in
 exactly one of them, never both.
 
-599 entries, 2026-08-06 .. 2026-11-11.
+600 entries, 2026-08-06 .. 2026-11-11.
 
 | date | entry id | finding | file |
 |---|---|---|---|
 | 2026-11-11 | `codegraph-recon-2` |  | [2026-11-11-codegraph-recon-2.md](2026-11-11-codegraph-recon-2.md) |
 | 2026-11-11 | `codegraph-recon-1` |  | [2026-11-11-codegraph-recon-1.md](2026-11-11-codegraph-recon-1.md) |
+| 2026-11-11 | `cg5-defuse-probe` |  | [2026-11-11-cg5-defuse-probe.md](2026-11-11-cg5-defuse-probe.md) |
 | 2026-11-11 | `cg-beh-1` |  | [2026-11-11-cg-beh-1.md](2026-11-11-cg-beh-1.md) |
 | 2026-11-10 | `lab-resolve-borrow-all` |  | [2026-11-10-lab-resolve-borrow-all.md](2026-11-10-lab-resolve-borrow-all.md) |
 | 2026-11-10 | `int8-direct-packed-b` |  | [2026-11-10-int8-direct-packed-b.md](2026-11-10-int8-direct-packed-b.md) |

.claude/probes/2026-11-11-cg5-defuse/REPORT.md

@@ -0,0 +1,115 @@
+# CG-5 probe: def-use rows separate a scalar threshold from a per-element quotient
+
+Slice: CG-5 (Linear EXO-237), after CG-8 (EXO-241). Ruling: D-CODEGRAPH-BOARD-RULING-2 allowed one
+bounded, read-only probe on the ndarray PR 422 case. Status: MEASURED. Nothing here is a production
+path; no row format, opcode, lowering or rewrite is added.
+
+## Question
+
+`foundry-parity-lab` has four `/` sites. Two build one threshold before any row is read
+(`(q + per_staff - 1) / per_staff`); two divide once per recipe ingredient (`v / d`). The effects rows
+of CG-8 find all four and say nothing about which kind each is. 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:
+
+| site | expected |
+|---|---|
+| `src/method.rs:58` (`can_cook_guard`) | scalar threshold |
+| `src/arm_b.rs:245` (`cook_ops`) | scalar threshold |
+| `src/arm_a.rs:75` (`can_cook`) | per-element quotient |
+| `src/oracle.rs:62` (`can_cook`) | per-element quotient |
+
+## Method
+
+1. `charon cargo --no-dedup-serialized-ast -- --lib` on the crate (Charon 0.1.297).
+2. `extract_defuse.py` reads the LLBC and writes rows for every function holding a `Div` or `Rem`:
+   `ARG`, `DEF` (one per defining statement, with the locals it reads), `ELEM` (result of an iterator
+   `next` call inside a loop), `INDEX` (value read through an index projection), `SITE` (the operator,
+   its file, line, loop depth and two operands). The rows are flow-insensitive. 783 rows, 16 sites
+   (5 `Div` statements at 4 source lines, 11 `Rem`).
+3. `crates/cg-defuse-probe` answers each site three ways:
+   - **egglog** (`derive`): the rows as terms, eight rules, proofs mode, stepped to a fixpoint.
+     A class is reported only with the proof egglog checked.
+   - **plain fixpoint** (`fixpoint`): the same two closures as Rust loops. Shares the rows only.
+   - **source scan** (`source_class`): reads the source line and the open `for` headers. Shares
+     neither rows nor rules.
+   Loop nesting of the statement (`nesting_class`) is the cheap comparator.
+
+Rules, per function: a site is per-element when an operand depends on an element source through any
+chain of definitions. A local is scalar when it is an argument, or is not an element source, has
+exactly one definition, and that definition reads only scalar locals. A site is a scalar threshold
+when both operands are scalar or literals. Everything else is unknown.
+
+## Result
+
+All three arms give the expected table. From `cargo run --release --example report`:
+
+| site | egglog | plain fixpoint | source scan | loop nesting |
+|---|---|---|---|---|
+| `method.rs:58` | scalar | scalar | scalar | scalar |
+| `arm_b.rs:245` (two LLBC copies) | 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 |
+
+- Loop nesting is wrong on one of four real sites. `arm_b.rs:245` stands after the source loop, and
+  Charon copies the tail of `cook_ops` into the loop's exit paths, so the statement appears twice
+  inside a `Loop` node.
+- Of the 11 `Rem` sites in `fixture.rs`, 8 are scalar and 3 are unknown: their divisor is a global
+  place, which the rules do not classify. Unknown carries no proof.
+- egglog and the plain fixpoint agree on all 63 sites of the four fixtures.
+- The proof for `method.rs:58` is 62,654 bytes; for `arm_a.rs:75`, 2,838 bytes.
+
+## Mutation control
+
+`mutate.py` writes three variants of `src/method.rs`; each is run through Charon again.
+
+| mutant | change | egglog | source scan | loop nesting |
+|---|---|---|---|---|
+| m1 | division moved into the loop, divisor is the element `d` | per-element | per-element | per-element |
+| m2 | division removed | no site (16 → 15 sites) | no operator on the line | — |
+| m3 | division moved into the loop, operands unchanged | scalar | scalar | **per-element (wrong)** |
+
+m1 flips the class, m2 removes the row, and m3 shows the classes follow the operands and not the
+position of the statement.
+
+## Cost (reported, not a gate)
+
+One cold derivation over 783 rows, release build: egglog 1.65 to 2.10 s (1,654,062 to 2,101,388 µs,
+26 steps), including the proofs of all sites. The plain fixpoint over the same rows: 912 to 1,190 µs.
+The derivation runs once per program and never per query.
+
+## What this does and does not show
+
+- It shows that operand provenance from LLBC decides this case where loop nesting does not, and that
+  egglog can carry the closure with a checked proof per site.
+- The plain fixpoint gets the same classes about 1,800 times faster. What egglog adds is the proof,
+  not the answer. Whether a proof per site is worth two seconds per crate is open.
+- The source scan also gets all seven cases right. It is a line scan with `for` headers; it would
+  miss a divisor that reaches the line through a helper or a renamed binding. No such case is in the
+  crate, so that limit is not measured here.
+- "Per element" means per item of the loop the operand comes from. In this crate that loop is over
+  recipe ingredients, not store rows. Dependence on the row argument is a different question and
+  was not asked.
+- The rows are flow-insensitive and intraprocedural. A call result is scalar when its arguments are.
+  A value written through a `&mut` passed to a call counts as a second definition.
+- One crate, four division sites, three mutants.
+
+## Open
+
+- Should def-use rows become a store row kind? That is the format decision of CG-3 (EXO-235) and is
+  not made here; the rows live in this probe's fixtures only.
+- Interprocedural provenance (is the divisor `fixture.rs:105`'s `per_staff`?) needs field-level
+  def-use across the `recipe` call. Not attempted.
+
+## Reproduce
+
+```
+cd crates/cg-defuse-probe && cargo test --release                # 18 tests
+cargo run --release --example report -- tests/data/m0.defuse.tsv src/method.rs:58
+CHARON=<charon binary> .claude/probes/2026-11-11-cg5-defuse/regenerate.sh   # rewrites tests/data
+python3 .claude/probes/2026-11-11-cg5-defuse/disable_runs.py     # 24 guards, receipt: 24 red
+```
+
+`regenerate.sh` was run after the fixtures were committed and changed no byte. The crate has its own
+workspace root and no CI workflow.

.claude/probes/2026-11-11-cg5-defuse/disable_runs.py

@@ -0,0 +1,75 @@
+#!/usr/bin/env python3
+"""Disable runs for crates/cg-defuse-probe/src/lib.rs.
+
+Each guard is patched out (the anchor must occur exactly once, or the run is reported as
+ANCHOR-MISSING and counts as a failure), `cargo test --release` is run in the crate, and
+the file is restored. A guard is load-bearing when its run is RED.
+
+Run from the repository root on a clean tree:  python3 <this file>
+Exit 0 only when every guard is RED. Writes the receipt next to this file.
+"""
+import re, subprocess, sys
+from pathlib import Path
+
+CRATE = Path(__file__).resolve().parents[3] / "crates/cg-defuse-probe"
+P = CRATE / "src/lib.rs"
+RECEIPT = Path(__file__).with_name("disable_runs.receipt.tsv")
+G = [
+ ("egglog-flow-rule", "(rule ((= f (Flow a b)) (= (Elem a) (T)))\n      ((union (Elem b) (T))) :ruleset defuse)\n", ""),
+ ("egglog-site-elem-lhs", "(rule ((= s (Site f n a b)) (= (Elem a) (T)))\n      ((union (ClassOf f n) (PerElement))) :ruleset defuse)\n", ""),
+ ("egglog-site-elem-rhs", "(rule ((= s (Site f n a b)) (= (Elem b) (T)))\n      ((union (ClassOf f n) (PerElement))) :ruleset defuse)\n", ""),
+ ("egglog-site-scalar-both", "(rule ((= s (Site f n a b)) (= (Scalar a) (T)) (= (Scalar b) (T)))", "(rule ((= s (Site f n a b)) (= (Scalar a) (T)))"),
+ ("egglog-all-scalar-head", "(rule ((= l (Cons v r)) (= (Scalar v) (T)) (= (AllScalar r) (T)))", "(rule ((= l (Cons v r)) (= (AllScalar r) (T)))"),
+ ("egglog-all-scalar-tail", "(rule ((= l (Cons v r)) (= (Scalar v) (T)) (= (AllScalar r) (T)))", "(rule ((= l (Cons v r)) (= (Scalar v) (T)))"),
+ ("egglog-const-scalar", "(union (Scalar (K)) (T))\n", ""),
+ ("encode-sole-def", "        if defs.len() == 1\n            && !facts.args.contains(&(f.clone(), *l))", "        if !defs.is_empty()\n            && !facts.args.contains(&(f.clone(), *l))"),
+ ("encode-elem-not-scalar", "            && !facts.elems.contains(&(f.clone(), *l))\n            && let Some(d)", "            && let Some(d)"),
+ ("encode-global-operand", "        Operand::Global => None,\n    }\n}\n\n/// The rows as egglog facts.", "        Operand::Global => Some(\"(K)\".to_string()),\n    }\n}\n\n/// The rows as egglog facts."),
+ ("derive-conflict", "    if prove(&mut egraph, \"(= (PerElement) (ScalarThreshold))\").is_some() {", "    if false {"),
+ ("derive-fuel", "        if iterations == fuel {", "        if false {"),
+ ("fixpoint-flow", ".any(|d| d.2.iter().any(|s| elem.contains(&(func.clone(), *s))))", ".any(|d| d.2.iter().any(|s| false && elem.contains(&(func.clone(), *s))))"),
+ ("fixpoint-sole-def", "                && defs.len() == 1\n                && defs\n                    .iter()\n                    .all(", "                && defs\n                    .iter()\n                    .all("),
+ ("fixpoint-global", "        Operand::Global => false,", "        Operand::Global => true,"),
+ ("parse-version", "        Some((_, \"#version 1\")) => {}\n        _ => return Err(FactsRefusal::Version),", "        Some(_) => {}\n        _ => return Err(FactsRefusal::Version),"),
+ ("parse-unknown-kind", "            _ => return Err(FactsRefusal::Row(n)),", "            _ => {}"),
+ ("parse-short-site", "                need(9)?;\n", ""),
+ ("parse-index-is-elem", "            \"ELEM\" | \"INDEX\" => {", "            \"ELEM\" => {\n                facts.elems.insert((func, num(f[2], n)?));\n            }\n            \"INDEX\" if false => {"),
+ ("source-bound-names", "used.iter().any(|w| bound.contains(w))", "used.iter().any(|w| false && bound.contains(w))"),
+ ("source-loop-close", "                    if open.last().is_some_and(|(d, _)| *d == depth) {\n                        open.pop();\n                    }\n", ""),
+ ("source-index", "    if target.contains('[') || ", "    if "),
+ ("source-comment", "    let code = |l: &str| l.split(\"//\").next().unwrap_or(\"\").to_string();", "    let code = |l: &str| l.to_string();"),
+ ("source-no-operator", "    if !target.contains('/') && !target.contains('%') {\n        return None;\n    }\n", ""),
+]
+
+def main():
+    if subprocess.run(["git", "diff", "--quiet", "--", str(P)]).returncode != 0:
+        sys.exit(f"{P} has local changes; commit first (the restore would not be exact)")
+    orig = P.read_text()
+    bad = 0
+    lines = ["guard\tresult\tfailing tests"]
+    try:
+        for name, old, new in G:
+            if orig.count(old) != 1:
+                lines.append(f"{name}\tANCHOR-MISSING({orig.count(old)})\t")
+                bad += 1
+                continue
+            P.write_text(orig.replace(old, new))
+            out = subprocess.run(["cargo", "test", "--release"], cwd=CRATE,
+                                 capture_output=True, text=True)
+            text = out.stdout + out.stderr
+            failed = sorted(set(re.findall(r"^test (\S+) \.\.\. FAILED", text, re.M)))
+            if out.returncode == 0:
+                res = "GREEN"; bad += 1
+            elif failed:
+                res = "RED"
+            else:
+                res = "RED(build)" if "error" in text else "RED(?)"
+                bad += 1
+            lines.append(f"{name}\t{res}\t{','.join(failed)}")
+            print(lines[-1], flush=True)
+    finally:
+        P.write_text(orig)
+    RECEIPT.write_text("\n".join(lines) + f"\n# {len(G)} guards, {bad} not red\n")
+    sys.exit(1 if bad else 0)
+
+main()

.claude/probes/2026-11-11-cg5-defuse/disable_runs.receipt.tsv

@@ -0,0 +1,26 @@
+guard	result	failing tests
+egglog-flow-rule	RED	a_division_by_the_loop_element_flips_to_per_element_in_every_arm,a_scalar_division_inside_the_loop_stays_scalar_where_nesting_gets_it_wrong,dependence_on_an_element_is_followed_through_a_chain,egglog_and_the_plain_fixpoint_agree_on_every_site_of_every_fixture,every_classified_site_carries_a_proof_and_unknown_carries_none,removing_the_division_removes_the_site,the_derivation_gives_the_preregistered_answer
+egglog-site-elem-lhs	RED	a_site_that_would_be_both_is_refused,a_value_read_through_an_index_is_an_element_source
+egglog-site-elem-rhs	RED	dependence_on_an_element_is_followed_through_a_chain
+egglog-site-scalar-both	RED	dependence_on_an_element_is_followed_through_a_chain,egglog_and_the_plain_fixpoint_agree_on_every_site_of_every_fixture,every_classified_site_carries_a_proof_and_unknown_carries_none
+egglog-all-scalar-head	RED	a_division_by_the_loop_element_flips_to_per_element_in_every_arm,a_scalar_division_inside_the_loop_stays_scalar_where_nesting_gets_it_wrong,dependence_on_an_element_is_followed_through_a_chain,egglog_and_the_plain_fixpoint_agree_on_every_site_of_every_fixture,every_classified_site_carries_a_proof_and_unknown_carries_none,one_non_scalar_source_anywhere_in_a_definition_blocks_scalar,removing_the_division_removes_the_site,the_derivation_gives_the_preregistered_answer
+egglog-all-scalar-tail	RED	one_non_scalar_source_anywhere_in_a_definition_blocks_scalar
+egglog-const-scalar	RED	a_site_that_would_be_both_is_refused,a_statement_copied_by_charon_is_one_definition,egglog_and_the_plain_fixpoint_agree_on_every_site_of_every_fixture,every_classified_site_carries_a_proof_and_unknown_carries_none
+encode-sole-def	RED	a_local_with_two_different_definitions_is_not_scalar,one_non_scalar_source_anywhere_in_a_definition_blocks_scalar
+encode-elem-not-scalar	RED	a_value_read_through_an_index_is_an_element_source,dependence_on_an_element_is_followed_through_a_chain
+encode-global-operand	RED	egglog_and_the_plain_fixpoint_agree_on_every_site_of_every_fixture,every_classified_site_carries_a_proof_and_unknown_carries_none
+derive-conflict	RED	a_site_that_would_be_both_is_refused
+derive-fuel	RED	running_out_of_fuel_is_a_refusal_not_a_partial_answer
+fixpoint-flow	RED	dependence_on_an_element_is_followed_through_a_chain,egglog_and_the_plain_fixpoint_agree_on_every_site_of_every_fixture
+fixpoint-sole-def	RED	a_local_with_two_different_definitions_is_not_scalar,one_non_scalar_source_anywhere_in_a_definition_blocks_scalar
+fixpoint-global	RED	egglog_and_the_plain_fixpoint_agree_on_every_site_of_every_fixture
+parse-version	RED	malformed_rows_are_refused
+parse-unknown-kind	RED	malformed_rows_are_refused
+parse-short-site	RED	malformed_rows_are_refused
+parse-index-is-elem	RED	a_value_read_through_an_index_is_an_element_source
+source-bound-names	RED	a_division_by_the_loop_element_flips_to_per_element_in_every_arm,the_source_scan_agrees_on_the_four_sites_without_reading_any_row,the_source_scan_ignores_a_loop_that_has_closed
+source-loop-close	RED	the_source_scan_ignores_a_loop_that_has_closed
+source-index	RED	the_source_scan_treats_an_indexed_read_as_per_element
+source-comment	RED	the_source_scan_treats_an_indexed_read_as_per_element
+source-no-operator	RED	removing_the_division_removes_the_site
+# 24 guards, 0 not red