egglog-r2il-probe: report the cold egglog phase in µs; coresearch map for D-DRMC

.claude/board/entries/2026-10-22-coresearch-drmc-stack.md

@@ -0,0 +1,101 @@
+# 2026-10-22 — /coresearch: the D-DRMC stack (#1700–#1704)
+
+**Status:** EXPLORATION MAP; the operator chose X1, X2, X3, X4, X15, X17,
+X20 (applied 2026-10-22, see "Applied" below). Scope: the
+five stacked PRs of D-DRMC (#1700 charter, #1701 typed DR64 binding, #1702
+finite-population evidence, #1703 law/recipe identity, #1704 ACT-R handoff + CI).
+
+## Question (after the premise gate)
+
+The premise audit split the original question ("is this staging right, and what
+does outside knowledge change?") into four, because the stack bundled concepts
+with different signatures:
+
+- **A. Frame identity:** which revisions identify the reference, who seals them,
+  and how that seal stays apart from focus selection and authorization scope.
+- **B. Finite-population evidence:** what makes a claim over one 64×64 focus
+  checkable; how validity, K3 and completeness are carried.
+- **C. Promotion:** under what typed step, if any, evidence may become a law
+  premise. Evidence never becomes a proof.
+- **D. Rebinding:** what a recipe keys on so it is binding-independent while each
+  execution stays binding-guarded.
+
+Verified by the main thread before the scouts ran: two different
+`BindingWitness` types exist (dr-math `lib.rs:73`, 5 fields; egglog-r2il-probe
+`catalogue.rs:39`, 3 fields), and the only shipped recipe falls back on any
+binding change (`catalogue.rs:257`), which contradicts the charter's "the same
+recipe rebinds to a fresh snapshot".
+
+## Measured (main thread, release, not by the PRs, which never ran cargo)
+
+| head | tests | clippy `-D warnings` | `cargo fmt --check` | CI |
+|---|---|---|---|---|
+| #1702 `34c43161` | 12/12 pass | clean | 17 diffs | no workflow |
+| #1704 `63d27f35` | 20/20 pass | clean | 32 diffs | new `isolated-probe` job red at Format (#1703 and #1704) |
+
+## Exploration map
+
+Grades and evidence for every row are in the crosswalk (scratchpad, banked).
+B/F/X = bridge / firewall / falsifier co-architect verdicts.
+
+| # | idea | relation | B | F | verdict |
+|---|---|---|---|---|---|
+| X4 | `universal_on_focus` checks `Unknown` before `Counterexamples` (`population.rs:27-38`), so a refuted focus reports `Unknown(n)` and hides the counterexample. Certain-answer semantics (incomplete FCA, Libkin) put refuted first. The one test with both FALSE and UNKNOWN never calls it. | NEW (defect) | OPP | PASS | **ADOPT-NOW** in #1702: order Vacuous → Counterexamples → Unknown; test gamma `0b111`, R `0b001`, validity `0b011` ⇒ `== Counterexamples(1)`, plus both twins |
+| X17 | gamma and R are bound to the same bits in `contract_handoff.rs:69-70` and `exact_complete_focus_passes_without_causal_claim`; recipe tests bind all-zero rows. "gamma ⊆ R" is then gamma ⊆ gamma and cannot fail. | NEW (test defect) | OPP | TRAP | **ADOPT-NOW**: distinct non-empty fixtures with anti-vacuity asserts; disable = read gamma in place of R |
+| X20/X13 | Workflow added by #1704 is red at Format; installs `stable` while the repo pins 1.99; 32 rustfmt diffs. | PARTIAL | OPP | CONFLICT | **ADOPT-NOW**: `cargo fmt`, mirror `egglog-r2il-probe.yml`'s toolchain step |
+| X15 | Stage 3 re-spells Stage B's law/proof/target identity. `ProofDisposition::CheckedByExternalAuthority` is caller-set; `offer_recipe` checks only a nonzero digest and checker revision, so a forged digest passes where `ReplayCapsule::recheck` refuses. Breaks the Stage B anchor (proofs checked by egglog's own checker) and "authorization is provenance". | PARTIAL / duplicate | OPP (partial replace) | **TRAP** | **ADOPT-NOW (remove)**: delete the caller-settable disposition; keep `LawShape` as the Boolean-DR64 domain key; take proof and target from Stage B (`ReplayCapsule::recheck`, `TargetAbi`). Probe X15 (forged-digest count `> 0` today) |
+| X1 | The 5-field witness merges reference identity (source/map/coordinates), focus (motion) and authorization scope (policy), against the 2026-10-03 frame-vs-motion ruling. `dir-rmap-probe` already separates `Witness` (prep.rs:61-100) and `Focus` (focus.rs:70-79). PROV-DM: entity bundle / activity / agent. | PARTIAL | OPP | PASS | **ADOPT-NOW** in the probe: three objects, three checks, no `From` between frame and focus |
+| X2 | A seal is store-issued identity (`Witness::of(store, version)`, `Weak<Snapshot>` by pointer), not caller equality. | ALREADY-HAVE elsewhere | OPP | PASS | **ADOPT-NOW** with X1: reuse dir-rmap's `Witness`; probe: two stores at version 0 must not alias |
+| X3 | Validity is a carrier of R (Arrow validity bitmap, Alive2 value/poison, Quack `BoundField.validity`, D-QSP-0 NULL contract). #1702 types it as a third `BoundDr64` with its own method; a separate UNKNOWN carrier was already rejected here (EXO-50 /027, /028). | ALREADY-HAVE (probe diverges) | OPP | PASS | **ADOPT-NOW**: bind validity with R, Quack shape; probe: a validity bound to a foreign method must refuse |
+| X6 | `validity: None` silently means all-known (`population.rs:81`), a closed world chosen by the caller's `Option`. Completeness is scoped, attested metadata on the data source (Razniewski & Nutt; Corman/Nutt/Savković). | NEW | OPP | CONFLICT | **PROBE**: `None` must refuse or report `Unattested`; any completeness record is local to the probe and store-issued with the frame, never in the contract |
+| X8 | Key the recipe on its semantics; guard the binding on each run (fold contract "a prepared plan is not a valid execution world", PostgreSQL replanning, CompCert per-run validation, Enumo per-domain re-validation). Stage B's `Entry` holds one binding and `insert` overwrites. | PARTIAL | OPP | CONFLICT (out of fold only) | **PROBE**, owner egglog-r2il-probe: two certified bindings for one key; today the first falls back. Lookup and rebinding stay out of fold |
+| X16 | `LawShape` keys on axis kinds only, so one law is reused for class 1 and class 22 without re-validation. Laws over sort variables need a parametric proof; Enumo kept 90–100 %, not all, across domains. | PARTIAL | OPP | CONFLICT | **PROBE**: class 22 with 2 counterexamples must not receive the law; shape lookup only nominates |
+| X18 | `contract_handoff` feeds `false_pairs == 0` into ACT-R eligibility, unwraps `universal_on_focus` (inherits X4), and ties `Snapshot.witness_version` to the binding only by a coincidental literal (9). | PARTIAL | WORTH | CONFLICT | **PROBE** after X4: a census may veto, never qualify; snapshot derived from the binding |
+| X7 | Evidence nominates, a separate validator admits (Ruler `is_valid`, Enumo `partition`, D-CMR §3.5, `causal_audit`). No conversion PopulationReport → premise exists, correctly, but only by absence. | PARTIAL | OPP (negative) | CONFLICT | **PROBE**: compile-fail test that no such conversion exists; a population-derived premise may only ever be a named, undischarged hypothesis that `promote` refuses |
+| X5 | R bit × validity bit gives four codes, one duplicate. | NEW | WORTH | CONFLICT | **PARK**: canonical-form check `R ∧ ¬valid = 0` is cheap; Belnap "Both" only if a store merge ever writes it |
+| X9 | One focus is an FCA formal context but not a support count; support needs counts under an explicit equivalence key over a window (2026-10-14 coverage DECISION). | PARTIAL | WORTH | CONFLICT | **PARK**: document `PopulationReport` as a per-focus census; support stays with population-law-crosscheck |
+| X10 | Typed relation algebra: sort checks exist; composition/converse typing does not. | PARTIAL | WORTH | CONFLICT | **PARK**: composition belongs to dir-rmap compose / relalg, not this probe |
+| X14 | A changed method *resolution* is its own invalidation input (PostgreSQL search_path hole); `MethodSignature` is caller-built. | NEW | WORTH | CONFLICT | **PARK** until a ClassView registry exposes a revision; then ask its owner |
+| X21 | G0–G9 gate matrix, "27 atoms", heritage example, amortization design (END_TO_END_GATES.md). | NEW (prose) | park | PASS | **PARK**: label each gate CLAIMED until it cites a test |
+| X11 | Bag is a different semiring; `BagNeedsMultiplicity` already refuses. | ALREADY-HAVE | DROP | PASS | **SKIP** (duplicate) |
+| X12 | Proof re-check independent of its producer: Stage B `recheck` + i128 oracle. | ALREADY-HAVE | DROP | PASS | **SKIP** (duplicate; it is what X15 should consume) |
+| X19 | `Capability` gate: a math offer never authorizes an effect. | ALREADY-HAVE | DROP | PASS | **SKIP**; tighten `is_err()` to `== EffectRequiresSeparateAuthorization` |
+
+Tension resolved: authorization scope is not frame identity; it is checked as its
+own guard at borrow time. The D-RMAP §7.4 cache key may still be the composite
+(frame, scope) without merging the two types.
+
+## Not searched
+
+Differential Dataflow, DuckDB prepared statements, Isabelle/Coq kernels, Green et
+al. PODS 2007 (read secondhand only), Necula proof-carrying code, Alive2's
+internals beyond its value encoding, Libkin ICDT 2015 in full (abstract only).
+The `sql_where` internals in Quack, the `set_rules` driver body and the
+egglog-r2il-probe tests were not read. "No conversion PopulationReport → premise"
+was checked in `population.rs` and `artifact.rs` in full, not across the whole
+tree.
+
+OPEN: who owns the frame seal for real sources (G1); whether `LawShape` laws can
+ever be proved sort-parametric; whether Stage B's catalogue should hold several
+bindings per key.
+
+## Applied (operator choice, 2026-10-22)
+
+`STATUS: fixed | OUTCOME:` fix commits on the stacked branches, merged upward:
+#1701 `ca05b1d1` (X1/X2/X3: `FrameStore`-issued `Frame` compared by issue
+identity, separate `Focus` and `Scope` guards, validity carried by R),
+#1702 `365b6c9d` (X4 refuted before unknown; X17 distinct fixtures),
+#1703 `ca88feaf` (X15, corrected: an opaque `RecipeCertificate` that only
+a certified-compiler boundary can issue; none exists for DR64, so admission ends
+in `NoCertifiedCompiler`. The first attempt, `55f88ef4`, made `ReplayCapsule`
+the proof authority; it is replay evidence for E1 only), #1704 `1f63a5b1` + the merge after `ca88feaf` (X17 handoff fixture, snapshot from the frame, X19
+tightening, X20 workflow on the pinned toolchain).
+Every new guard was disable-verified red. | `OPEN:` a certified-compiler
+boundary for DR64 needs a typed relational statement language, egglog laws
+over it with checked proofs, and a lowering check. Candidate first law:
+associativity of Boolean relation composition over compatible ClassView
+domains, which also gives a real choice of association order. Also open: a
+specialization-selection gate (GF(2) elimination, M4RI, Boolean relational
+algebra) with three benchmark arms on the same typed problem, all of them
+hypotheses until measured. Probes X6, X7, X8, X16 and X18 not run.
+

.claude/board/entries/2026-10-22-math-compiler-stage-b-e1.md

@@ -41,8 +41,9 @@
 - "Independent proof check MISSING" overstated the gap. egglog already checks every proof it returns. What is missing is a check callable from outside egglog on a proof object. The i128 oracle covers answer correctness independently.
 - No egglog change was needed.
 
+**Cold cost (operator decision, 2026-10-22: report cold costs in microseconds, not gated):** egglog phase (setup + saturation + `prove-variants`) 21 084 / 26 875 / 28 793 µs over three runs, each a median of 5, release, Xeon @ 2.10 GHz, 4 vCPU, shared host. In the same runs encode was 3–4 µs and lower + execute 6–15 µs. `examples/e1_cold_cost.rs` now prints the egglog row. The cost line above is unchanged; it records the earlier state.
+
 OPEN:
-- the ruling on reporting cold-compile cost;
 - E2–E5 beyond what E1 exercises;
 - a lowering target for wrapping arithmetic (none exists; by design?);
 - `Measure::Scale` stays gated on a real population-measure consumer in a separate PR.

.claude/board/entries/README.md

@@ -25,13 +25,14 @@ 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.
 
-428 entries, 2026-08-06 .. 2026-10-22.
+429 entries, 2026-08-06 .. 2026-10-22.
 
 | date | entry id | finding | file |
 |---|---|---|---|
 | 2026-10-22 | `math-compiler-stage-b-e1` |  | [2026-10-22-math-compiler-stage-b-e1.md](2026-10-22-math-compiler-stage-b-e1.md) |
 | 2026-10-22 | `math-compiler-gap-matrix` |  | [2026-10-22-math-compiler-gap-matrix.md](2026-10-22-math-compiler-gap-matrix.md) |
 | 2026-10-22 | `D-MPS-9` |  | [2026-10-22-d-mps-9-mork-oracle.md](2026-10-22-d-mps-9-mork-oracle.md) |
+| 2026-10-22 | `D-DRMC` |  | [2026-10-22-coresearch-drmc-stack.md](2026-10-22-coresearch-drmc-stack.md) |
 | 2026-10-21 | `zero-copy-join-index-map` |  | [2026-10-21-zero-copy-join-index-map.md](2026-10-21-zero-copy-join-index-map.md) |
 | 2026-10-21 | `D-RU-4` |  | [2026-10-21-u4-coaddressed-join.md](2026-10-21-u4-coaddressed-join.md) |
 | 2026-10-21 | `D-RU-3` |  | [2026-10-21-u3-cross-rule-cse.md](2026-10-21-u3-cross-rule-cse.md) |

CLAUDE.md

@@ -80,6 +80,16 @@ benchmarks and PR bodies alike.
   - This holds for tests and oracles too: answers are compared by folds
     through the template, never by expanding them into rows.
 - REVISIT WHEN: never on cost grounds.
+- **SCOPED EXCEPTION — cold, out-of-fold compile and oracle costs** (DECISION,
+  operator, 2026-10-22: *"Report the cold costs in microseconds, not gated"*).
+  A cold compile outside the fold (egglog saturation + proof in
+  `egglog-r2il-probe`) or a differential-oracle reference arm (MORK in
+  `crepe-plan-probe/examples/mork_split.rs`) may be reported, always in µs
+  and always labelled "reported, not gates". It never licenses a ms-scale
+  in-fold path: encode, lower, execute and every query terminal stay under
+  the rule above. BASIS: these phases run once per program or only as an
+  oracle, never per query. REVISIT WHEN: a cold phase moves onto a per-query
+  path.
 
 ## P0 — AdaWorldAPI forks ONLY, NEVER crates.io upstream
 

crates/egglog-r2il-probe/examples/e1_cold_cost.rs

@@ -1,11 +1,10 @@
-//! In-fold cost of E1 (encode, and lowering + execution on R2IL), release
-//! build, median of 5.
+//! Cost of E1, release build, median of 5, in microseconds: encode, the egglog
+//! phase (setup, saturation, `prove-variants`) and lowering + execution on
+//! R2IL.
 //!
-//! The egglog phase is timed in `Compiled::timings.egglog` but NOT printed:
-//! it is a cold, out-of-fold compile whose cost is above the workspace's
-//! microsecond budget, and whether cold-compile costs may be reported at all
-//! is an open operator decision (lance-graph `CLAUDE.md`, "no millisecond
-//! results"). Until it is ruled, this example does not publish that number.
+//! The egglog phase is a cold, out-of-fold compile. Per the operator decision
+//! of 2026-10-22 it is reported in microseconds and is not a gate; the
+//! in-fold rows (encode, lower + execute) stay under the workspace budget.
 //!
 //!   cargo run --release --example e1_cold_cost
 //!
@@ -43,23 +42,29 @@ fn main() {
     );
 
     let mut encode = Vec::with_capacity(RUNS);
+    let mut egglog = Vec::with_capacity(RUNS);
     let mut lower = Vec::with_capacity(RUNS);
     for _ in 0..RUNS {
         let c = compile(&p, Arith::Exact, 8);
         assert!(c.error.is_none(), "egglog error: {:?}", c.error);
         encode.push(c.timings.encode);
+        egglog.push(c.timings.egglog);
         let t = Instant::now();
         let v = lower_and_run(&c, &[("c", C)]).expect("lowers and runs");
         lower.push(t.elapsed());
         assert_eq!(i128::from(v), want);
     }
 
-    println!("in-fold costs; reported, not gates (egglog phase withheld, see module doc)");
+    println!("cold compile costs; reported, not gates");
     println!("E1 under Exact, fuel 8, c = {C}, median of {RUNS}, microseconds:");
     println!(
         "  encode                              {:>10}",
         micros(median(encode))
     );
+    println!(
+        "  egglog (setup + saturate + prove)   {:>10}",
+        micros(median(egglog))
+    );
     println!(
         "  lower + execute                     {:>10}",
         micros(median(lower))