diff --git a/.claude/board/entries/2026-10-22-coresearch-drmc-stack.md b/.claude/board/entries/2026-10-22-coresearch-drmc-stack.md new file mode 100644 index 000000000..655cce54e --- /dev/null +++ b/.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` 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. + diff --git a/.claude/board/entries/2026-10-22-math-compiler-stage-b-e1.md b/.claude/board/entries/2026-10-22-math-compiler-stage-b-e1.md index 935e7e483..d54f9866f 100644 --- a/.claude/board/entries/2026-10-22-math-compiler-stage-b-e1.md +++ b/.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. diff --git a/.claude/board/entries/README.md b/.claude/board/entries/README.md index 1f634299c..dd6231c6a 100644 --- a/.claude/board/entries/README.md +++ b/.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) | diff --git a/CLAUDE.md b/CLAUDE.md index 25b16121b..5cc93055f 100644 --- a/CLAUDE.md +++ b/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 diff --git a/crates/egglog-r2il-probe/examples/e1_cold_cost.rs b/crates/egglog-r2il-probe/examples/e1_cold_cost.rs index ad6dba4f4..619da71f6 100644 --- a/crates/egglog-r2il-probe/examples/e1_cold_cost.rs +++ b/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))