diff --git a/.claude/board/STATUS_BOARD.md b/.claude/board/STATUS_BOARD.md index 63761e72f..e4b3ec1a0 100644 --- a/.claude/board/STATUS_BOARD.md +++ b/.claude/board/STATUS_BOARD.md @@ -1,11 +1,13 @@ ## D-RFT / D-QSP — ClassView × Quack semantic substrate (2026-10-21) -Plans in #1667 (`d-rft-relalg-thought-git-frontier-v1.md`, `d-qsp-classview-quack-postgresql-parity-v1.md`; docs, not yet on main). Only the rows below have a claim or evidence; the other D-RFT / D-QSP / D-LFA ids stay as #1667 lists them. +Plans in #1667 (`d-rft-relalg-thought-git-frontier-v1.md`, `d-qsp-classview-quack-postgresql-parity-v1.md`, `d-lfa-lance-graph-flow-rubicon-assimilation-v1.md`; merged). Only the rows below have a claim or evidence; the other D-RFT / D-QSP / D-LFA ids stay as #1667 lists them. | D-id | scope | status | gate / falsifier | |---|---|---|---| -| **D-RFT-0 / D-QSP-0** | K3 normalization safety: rewrites keep SQL three-valued TRUE rows | In PR (EXO-50 claim `session_01G22yT6htkcdyXsihxxXdrg/031`; `entries/2026-10-21-d-rft-0-kleene-normalization.md`): `normalize_kleene`; `SetNormalize` admits it under `ThreeValued`. MEASURED: PostgreSQL 16.14 = Kleene oracle = `normalize_kleene` on 2000/2000; the two-valued form is wrong on 474 | Kleene evaluator over random expressions + PostgreSQL differential; 5 disables red. Remainder open: NULL literals, `COALESCE`, nullable arithmetic, empty `SUM`, `COUNT(expr)` | +| **D-RFT-0 / D-QSP-0** | K3 normalization safety: rewrites keep SQL three-valued TRUE rows | Shipped (#1668; EXO-50 claim `session_01G22yT6htkcdyXsihxxXdrg/031`; `entries/2026-10-21-d-rft-0-kleene-normalization.md`): `normalize_kleene`; `SetNormalize` admits it under `ThreeValued`. MEASURED: PostgreSQL 16.14 = Kleene oracle = `normalize_kleene` on 2000/2000; the two-valued form is wrong on 474 | Kleene evaluator over random expressions + PostgreSQL differential; 5 disables red. Remainder open: NULL literals, `COALESCE`, nullable arithmetic, empty `SUM`, `COUNT(expr)` | | **D-RFT-1..5, D-LFA-0** | composition, substitution, recursion, frontier, replay; flow census | PROPOSAL (`entries/2026-10-21-d-rft-d-lfa-0-assessment.md`) | per-row falsifiers in the entry; unclaimed | +| **D-LFA-1 / D-LFA-2** (amended 2026-10-21) | guarded-control verification of a Rubicon flow; integration with the existing drivers | PROPOSAL (plan amendment, `d-lfa-…-v1.md` § Amendment 2026-10-21; map `entries/2026-10-21-coresearch-plans-mapping-foresight.md`) | GKAT equivalence + separate no-commit-without-revision-and-MUL trace check; 3 disables; `GoTo`/`GoBack` refused; unclaimed | +| **D-GKAT-0** | GKAT fixture probe: G1 factoring, G2 nondeterminism refusal, G5 declared atom bound | Queued, unclaimed (research only; no runtime, dependency or executor) | the three fixtures in the D-LFA plan amendment | ## D-RU — D-RELALG-UNIFIED: JC/R statistics and Datalog sharing work through the contract set IR (2026-10-20) diff --git a/.claude/board/entries/2026-10-21-coresearch-plans-mapping-foresight.md b/.claude/board/entries/2026-10-21-coresearch-plans-mapping-foresight.md index 95f59dd78..465351d51 100644 --- a/.claude/board/entries/2026-10-21-coresearch-plans-mapping-foresight.md +++ b/.claude/board/entries/2026-10-21-coresearch-plans-mapping-foresight.md @@ -70,6 +70,8 @@ All probes compare counts or scalar folds. | P-ABA-MODDEL | Modify on one side and delete on the other is a named refusal | It resolves silently | | P-REFUSAL-KIND | A RouteRefusal is retried on another route. A SemanticRefusal is never retried. | A semantic refusal is retried | | P-TLP-COUNT | The counts for P, NOT P and P IS NULL sum to the table's row count | The sum differs | +| D-GKAT-0 (added 2026-10-21, after #1670) | GKAT fixtures: G1 guarded factoring, G2 refusal of genuine nondeterminism, G5 a declared atom bound. No runtime, dependency or executor. | A G1 rewrite with a changed label or polarity is accepted; nondeterminism is encoded as an `if` | +| P-GKAT-RUBICON (D-LFA-1) | A Rubicon reference flow and its optimized variant are GKAT-equivalent. Separately, no `RequestCommit` trace exists without a valid revision and MUL authorization. Guards are projected WHERE-style `{T}`, never CHECK-style `{T,U}`. | Any disable stays green: reversed polarity, commit moved ahead of its guard, or unguarded choice. A `GoTo`/`GoBack` flow is translated instead of refused. | Bridge findings worth a probe: - `JoinExec::bag_count` sums `u64` without an overflow check (`mork-pathmap-probe/src/join.rs:653-659`). The contract should be exact below a stated row bound and refused above it. diff --git a/.claude/plans/d-lfa-lance-graph-flow-rubicon-assimilation-v1.md b/.claude/plans/d-lfa-lance-graph-flow-rubicon-assimilation-v1.md index 580a6df5d..7ac1ee516 100644 --- a/.claude/plans/d-lfa-lance-graph-flow-rubicon-assimilation-v1.md +++ b/.claude/plans/d-lfa-lance-graph-flow-rubicon-assimilation-v1.md @@ -48,6 +48,56 @@ The z8run adapter is a **host** of flow graphs; Quack remains the evaluator. No **Stop conditions:** new execution loop or SQL evaluator, checkpointer becoming authoritative storage, conflicting Kanban transition owner, workflow graph identity becoming row identity, missing generation refusal, non-equivalent replay, or requiring pre-existing data materialization in Context. Halt runtime assimilation rather than papering over with adapters. +## Amendment 2026-10-21: guarded-control verification (GKAT) + +**Status:** approved by the operator 2026-10-21. Docs and probes only; no implementation is claimed, no owner is assigned. Source: [.arxiv/1907.05920 GKAT excerpt](../../.arxiv/1907.05920_guarded_kleene_algebra_verified_control_flow_excerpt.md) (#1670); [co-research map](../board/entries/2026-10-21-coresearch-plans-mapping-foresight.md). + +This amendment replaces the D-LFA-1 and D-LFA-2 contracts above where they differ; D-LFA-0 and D-LFA-3 are unchanged. D-RFT-2 is unchanged. D-RFT-4 keeps versioned thought binding and frontier behaviour; it does not own guarded workflow verification. + +### Guard projection (applies to D-LFA-1 and D-LFA-2) + +GKAT tests are Boolean. A K3 predicate becomes a GKAT test only through a **declared projection** of its designated truth values: + +- WHERE-style: designated `{T}` (UNKNOWN and FALSE do not pass); +- CHECK-style: designated `{T, U}` (only FALSE fails). + +The two are never interchanged. **Commit authorization uses `{T}` and must never inherit CHECK semantics:** an UNKNOWN revision or authorization does not authorize. + +### D-LFA-1: one Rubicon reference flow and one optimized variant + +- **Flows.** One structured Rubicon reference flow, and one optimized variant of it. Both use only sequence, guarded choice (`if b then e else f`) and guarded iteration (`while b do e`). +- **Equivalence.** The two are GKAT-equivalent, checked by bisimulation of their guarded automata. Conditions: + - both use the same action alphabet; + - both use the same declared guards, each with its declared projection. +- **Safety, checked separately.** No trace of the reference flow contains `RequestCommit` unless both a valid revision and MUL authorization precede it. Equivalence alone does not establish this: it only says the variant behaves like the reference. +- **`RequestCommit` is an intent, not a Lance write.** It proposes; the existing supervisor and `cycle_driver` seal. No flow step moves a dataset version. +- **Disable runs.** Each must fail the check named: + 1. Reverse a guard's polarity: the equivalence check fails. + 2. Move `RequestCommit` ahead of its guard: the equivalence check and the safety check both fail. + 3. Introduce an unguarded nondeterministic choice: the flow is refused as outside GKAT; it is never encoded as an `if` under an invented predicate. +- **Unstructured jumps are refused.** A flow that uses `GoTo` or `GoBack` is refused, never translated into an unsupported GKAT fragment. +- **`WaitForInput`.** It is modelled as an observation of external state at resume, i.e. a test, not an autonomous state transition. +- **Runtime gate.** Snapshot and codebook generation validation stays an independent runtime gate: a stale source refuses at resume. GKAT does not model versions and is not that gate. + +### D-LFA-2: integration with existing drivers + +- **Scope.** Exercise the existing pieces together: + - the graph-flow driver; + - thought-git verbs; + - Kanban/Rubicon transitions (`kanban.rs` `next_phases`); + - authorized action proposals. +- **Oracle.** Compare deterministic replay results and receipts against the independent from-scratch oracle (`thought-git-probe::oracle::next_version`). The D-TGB-4 receipt is a prerequisite; it does not exist in code yet. +- **Nothing new beside the existing pieces.** There is no second scheduler, evaluator, state store or commit owner. + +### D-GKAT-0: independent fixture probe + +- **Status.** Independent and unclaimed; a research and fixture probe only. +- **Checks.** The numbering follows the #1670 excerpt: + - **G1:** guarded factoring and equivalence. The paper's example: `if b then {p; q} else {q}` ≡ `(if b then {p} else {skip}); q` for identical pure `q`. Changing one action label or guard polarity must be rejected. + - **G2:** genuine nondeterminism is rejected rather than encoded. + - **G5:** the Boolean atom set is explicitly bounded and declared. Beyond the bound the probe refuses; it never enumerates silently. +- **Exclusions.** No production runtime, no dependency and no executor. A DR64 or DR256 mask is a physical lane set, never a set of GKAT tests. + ## Coordination Main PR: [ClassView/Quack PostgreSQL parity plan](d-qsp-classview-quack-postgresql-parity-v1.md). Priority companion: [relalg × thought-git frontier](d-rft-relalg-thought-git-frontier-v1.md). Existing source: '.claude/plans/thought-git-basics-v1.md' and EXO-98; '.claude/plans/relalg-v1.md' and EXO-86; EXO-50 messages. Any code handoff needs an explicit owner/claim and separate implementation PR. This PR changes plans only.