From 6d4366138e0be77f8833bf44085b2a3deff726c1 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 22 Oct 2026 14:50:23 +0000 Subject: [PATCH 1/5] =?UTF-8?q?egglog-r2il-probe:=20report=20the=20cold=20?= =?UTF-8?q?egglog=20phase=20in=20=C2=B5s,=20not=20gated?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Operator decision 2026-10-22: cold, out-of-fold costs are reported in microseconds and are not gates. e1_cold_cost now prints the egglog phase (setup + saturation + prove-variants): 21 084 / 26 875 / 28 793 µs over three runs, each a median of 5, release, shared 4-vCPU host. Encode (3-4 µs) and lower + execute (6-15 µs) are unchanged. CLAUDE.md records the scoped exception under the "no millisecond results" P0: cold compile and differential-oracle reference arms only, always µs, always labelled not-gated; in-fold paths stay under the rule. The Stage B board entry gains the numbers and drops the open ruling. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01G22yT6htkcdyXsihxxXdrg --- .../2026-10-22-math-compiler-stage-b-e1.md | 3 ++- CLAUDE.md | 10 +++++++++ .../examples/e1_cold_cost.rs | 21 ++++++++++++------- 3 files changed, 25 insertions(+), 9 deletions(-) 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.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)) From 441865dd82e8487ae4df5644a7e77cd4fb4be4c3 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 22 Oct 2026 15:04:36 +0000 Subject: [PATCH 2/5] board: /coresearch exploration map for the D-DRMC stack (#1700-#1704) Premise gate split the question into frame identity, finite-population evidence, promotion and rebinding. Five scouts, a 21-row crosswalk and three co-architect passes. Measured on the PR heads: 12/12 and 20/20 tests pass, clippy clean, 17 and 32 rustfmt diffs, new probe workflow red at Format. ADOPT-NOW candidates: the Unknown-before-Counterexamples ordering defect, tautological fixtures, caller-set proof disposition, frame/focus/ scope split, validity as a carrier of R, CI fix. Nothing adopted. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01G22yT6htkcdyXsihxxXdrg --- .../2026-10-22-coresearch-drmc-stack.md | 79 +++++++++++++++++++ .claude/board/entries/README.md | 3 +- 2 files changed, 81 insertions(+), 1 deletion(-) create mode 100644 .claude/board/entries/2026-10-22-coresearch-drmc-stack.md 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..f3e11f8fa --- /dev/null +++ b/.claude/board/entries/2026-10-22-coresearch-drmc-stack.md @@ -0,0 +1,79 @@ +# 2026-10-22 — /coresearch: the D-DRMC stack (#1700–#1704) + +**Status:** EXPLORATION MAP. Nothing adopted; the operator chooses. 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. 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) | From a55eb711e54688774c82b50709a2572603036d70 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 22 Oct 2026 15:25:21 +0000 Subject: [PATCH 3/5] board: record the D-DRMC fixes applied from the coresearch map Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01G22yT6htkcdyXsihxxXdrg --- .../2026-10-22-coresearch-drmc-stack.md | 20 ++++++++++++++++++- 1 file changed, 19 insertions(+), 1 deletion(-) diff --git a/.claude/board/entries/2026-10-22-coresearch-drmc-stack.md b/.claude/board/entries/2026-10-22-coresearch-drmc-stack.md index f3e11f8fa..36027f018 100644 --- a/.claude/board/entries/2026-10-22-coresearch-drmc-stack.md +++ b/.claude/board/entries/2026-10-22-coresearch-drmc-stack.md @@ -1,6 +1,7 @@ # 2026-10-22 — /coresearch: the D-DRMC stack (#1700–#1704) -**Status:** EXPLORATION MAP. Nothing adopted; the operator chooses. Scope: the +**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). @@ -77,3 +78,20 @@ 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 `55f88ef4` + `b14dc037` (X15: `ProofReference` only via +`ReplayCapsule::recheck` on the law's `SemanticKey`, `TargetAbi` target), +#1704 `1f63a5b1` (X17 handoff fixture, snapshot from the frame, X19 +tightening, X20 workflow on the pinned toolchain with the ndarray sibling). +Every new guard was disable-verified red, except the `recheck` call, which +cannot fire while capsules only come from `certify` in-process (stated in +`RECIPE_ADMISSION.md`). | `OPEN:` Stage B checks integer substitution only, so +no Boolean-DR64 law has a checker; the recipe tests use E1's statement for the +plumbing. X6, X7, X8, X16, X18 probes not run. + From 0d2830b8e74af01c38b64a21a13cfc7a4b813c54 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 22 Oct 2026 15:29:13 +0000 Subject: [PATCH 4/5] board: D-DRMC X15 corrected; record the relational-law and specialization directions as open Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01G22yT6htkcdyXsihxxXdrg --- .../2026-10-22-coresearch-drmc-stack.md | 20 +++++++++++-------- 1 file changed, 12 insertions(+), 8 deletions(-) diff --git a/.claude/board/entries/2026-10-22-coresearch-drmc-stack.md b/.claude/board/entries/2026-10-22-coresearch-drmc-stack.md index 36027f018..2b4dcb909 100644 --- a/.claude/board/entries/2026-10-22-coresearch-drmc-stack.md +++ b/.claude/board/entries/2026-10-22-coresearch-drmc-stack.md @@ -85,13 +85,17 @@ bindings per key. #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 `55f88ef4` + `b14dc037` (X15: `ProofReference` only via -`ReplayCapsule::recheck` on the law's `SemanticKey`, `TargetAbi` target), -#1704 `1f63a5b1` (X17 handoff fixture, snapshot from the frame, X19 +#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 with the ndarray sibling). -Every new guard was disable-verified red, except the `recheck` call, which -cannot fire while capsules only come from `certify` in-process (stated in -`RECIPE_ADMISSION.md`). | `OPEN:` Stage B checks integer substitution only, so -no Boolean-DR64 law has a checker; the recipe tests use E1's statement for the -plumbing. X6, X7, X8, X16, X18 probes not run. +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. From 8faa9f0c6d2d8804003a1268a48d8e81de45978e Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 22 Oct 2026 15:29:29 +0000 Subject: [PATCH 5/5] board: drop a stale workflow detail from the D-DRMC entry Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01G22yT6htkcdyXsihxxXdrg --- .claude/board/entries/2026-10-22-coresearch-drmc-stack.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.claude/board/entries/2026-10-22-coresearch-drmc-stack.md b/.claude/board/entries/2026-10-22-coresearch-drmc-stack.md index 2b4dcb909..655cce54e 100644 --- a/.claude/board/entries/2026-10-22-coresearch-drmc-stack.md +++ b/.claude/board/entries/2026-10-22-coresearch-drmc-stack.md @@ -89,7 +89,7 @@ identity, separate `Focus` and `Scope` guards, validity carried by R), 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 with the ndarray sibling). +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: