From 00969817fd08e01a8eb83c0701391dbd38e0aa9d Mon Sep 17 00:00:00 2001
From: "J. Kirby Ross" <james@flyingrobots.dev>
Date: Fri, 2 Jan 2026 19:19:48 -0800
Subject: [PATCH 1/2] M2.1: add DPO concurrency litmus (spec + tests)

---
 .../warp-core/tests/dpo_concurrency_litmus.rs | 309 ++++++++++++++++++
 docs/decision-log.md                          |   7 +
 docs/execution-plan.md                        |  39 ++-
 docs/spec-mwmr-concurrency.md                 |   2 +-
 .../SPEC-0003-dpo-concurrency-litmus-v0.md    |  74 +++++
 5 files changed, 416 insertions(+), 15 deletions(-)
 create mode 100644 crates/warp-core/tests/dpo_concurrency_litmus.rs
 create mode 100644 docs/spec/SPEC-0003-dpo-concurrency-litmus-v0.md

diff --git a/crates/warp-core/tests/dpo_concurrency_litmus.rs b/crates/warp-core/tests/dpo_concurrency_litmus.rs
new file mode 100644
index 00000000..a6569682
--- /dev/null
+++ b/crates/warp-core/tests/dpo_concurrency_litmus.rs
@@ -0,0 +1,309 @@
+// SPDX-License-Identifier: Apache-2.0
+// © James Ross Ω FLYING•ROBOTS <https://github.com/flyingrobots>
+
+//! DPO concurrency litmus tests for `warp-core`.
+//!
+//! These tests pin “order independence” at the engine boundary:
+//! enqueue order must not change the terminal digests for commuting cases, and
+//! overlap must yield deterministic rejection for conflicting cases.
+
+use warp_core::demo::ports::{port_rule, PORT_RULE_NAME};
+use warp_core::{
+    encode_motion_atom_payload, make_node_id, make_type_id, ApplyResult, AttachmentValue, Engine,
+    EngineError, Footprint, GraphStore, NodeId, NodeRecord, PatternGraph, RewriteRule,
+};
+
+const LITMUS_PORT_READ_0: &str = "litmus/port_read_0";
+const LITMUS_PORT_READ_1: &str = "litmus/port_read_1";
+
+fn litmus_rule_id(name: &'static str) -> warp_core::Hash {
+    let mut hasher = blake3::Hasher::new();
+    hasher.update(b"rule:");
+    hasher.update(name.as_bytes());
+    hasher.finalize().into()
+}
+
+fn litmus_port_read_matcher(store: &GraphStore, scope: &NodeId) -> bool {
+    store.node(scope).is_some()
+}
+
+fn litmus_port_read_executor(_store: &mut GraphStore, _scope: &NodeId) {}
+
+fn litmus_port_read_0_footprint(store: &GraphStore, scope: &NodeId) -> Footprint {
+    let mut fp = Footprint::default();
+    if store.node(scope).is_some() {
+        fp.n_read.insert_node(scope);
+        fp.b_in.insert(warp_core::pack_port_key(scope, 0, true));
+    }
+    fp
+}
+
+fn litmus_port_read_1_footprint(store: &GraphStore, scope: &NodeId) -> Footprint {
+    let mut fp = Footprint::default();
+    if store.node(scope).is_some() {
+        fp.n_read.insert_node(scope);
+        fp.b_in.insert(warp_core::pack_port_key(scope, 1, true));
+    }
+    fp
+}
+
+fn litmus_port_read_0_rule() -> RewriteRule {
+    RewriteRule {
+        id: litmus_rule_id(LITMUS_PORT_READ_0),
+        name: LITMUS_PORT_READ_0,
+        left: PatternGraph { nodes: Vec::new() },
+        matcher: litmus_port_read_matcher,
+        executor: litmus_port_read_executor,
+        compute_footprint: litmus_port_read_0_footprint,
+        factor_mask: 0,
+        conflict_policy: warp_core::ConflictPolicy::Abort,
+        join_fn: None,
+    }
+}
+
+fn litmus_port_read_1_rule() -> RewriteRule {
+    RewriteRule {
+        id: litmus_rule_id(LITMUS_PORT_READ_1),
+        name: LITMUS_PORT_READ_1,
+        left: PatternGraph { nodes: Vec::new() },
+        matcher: litmus_port_read_matcher,
+        executor: litmus_port_read_executor,
+        compute_footprint: litmus_port_read_1_footprint,
+        factor_mask: 0,
+        conflict_policy: warp_core::ConflictPolicy::Abort,
+        join_fn: None,
+    }
+}
+
+fn build_litmus_engine() -> Result<Engine, EngineError> {
+    let mut store = GraphStore::default();
+    let root = make_node_id("litmus-world-root");
+    store.insert_node(
+        root,
+        NodeRecord {
+            ty: make_type_id("world"),
+        },
+    );
+
+    let mut engine = Engine::new(store, root);
+    engine.register_rule(warp_core::motion_rule())?;
+    engine.register_rule(port_rule())?;
+    engine.register_rule(litmus_port_read_0_rule())?;
+    engine.register_rule(litmus_port_read_1_rule())?;
+    Ok(engine)
+}
+
+fn assert_terminal_digests_equal(a: &warp_core::Snapshot, b: &warp_core::Snapshot) {
+    assert_eq!(a.hash, b.hash, "commit hash must be order-independent");
+    assert_eq!(
+        a.plan_digest, b.plan_digest,
+        "plan digest must be order-independent"
+    );
+    assert_eq!(
+        a.rewrites_digest, b.rewrites_digest,
+        "rewrites digest must be order-independent"
+    );
+    assert_eq!(
+        a.decision_digest, b.decision_digest,
+        "decision (receipt) digest must be order-independent"
+    );
+    assert_eq!(
+        a.patch_digest, b.patch_digest,
+        "patch digest must be order-independent"
+    );
+    assert_eq!(a.policy_id, b.policy_id, "policy id must match");
+    assert_eq!(a.parents, b.parents, "parents must match in litmus setup");
+}
+
+#[test]
+fn dpo_litmus_commuting_independent_pair() -> Result<(), EngineError> {
+    // Two candidates are independent (disjoint footprints) and commute:
+    // enqueue order must not change the terminal digest.
+    fn setup() -> Result<(Engine, NodeId, NodeId), EngineError> {
+        let mut engine = build_litmus_engine()?;
+
+        let entity_motion = make_node_id("litmus-entity-motion");
+        engine.insert_node(
+            entity_motion,
+            NodeRecord {
+                ty: make_type_id("entity"),
+            },
+        )?;
+        let pos = [10.0, -2.0, 3.5];
+        let vel = [0.125, 2.0, -1.5];
+        engine.set_node_attachment(
+            entity_motion,
+            Some(AttachmentValue::Atom(encode_motion_atom_payload(pos, vel))),
+        )?;
+
+        let entity_port = make_node_id("litmus-entity-port");
+        engine.insert_node(
+            entity_port,
+            NodeRecord {
+                ty: make_type_id("entity"),
+            },
+        )?;
+
+        Ok((engine, entity_motion, entity_port))
+    }
+
+    let (mut a, entity_motion, entity_port) = setup()?;
+    let tx_a = a.begin();
+    assert!(matches!(
+        a.apply(tx_a, warp_core::MOTION_RULE_NAME, &entity_motion)?,
+        ApplyResult::Applied
+    ));
+    assert!(matches!(
+        a.apply(tx_a, PORT_RULE_NAME, &entity_port)?,
+        ApplyResult::Applied
+    ));
+    let (snap_a, receipt_a, _patch_a) = a.commit_with_receipt(tx_a)?;
+
+    let (mut b, entity_motion, entity_port) = setup()?;
+    let tx_b = b.begin();
+    assert!(matches!(
+        b.apply(tx_b, PORT_RULE_NAME, &entity_port)?,
+        ApplyResult::Applied
+    ));
+    assert!(matches!(
+        b.apply(tx_b, warp_core::MOTION_RULE_NAME, &entity_motion)?,
+        ApplyResult::Applied
+    ));
+    let (snap_b, receipt_b, _patch_b) = b.commit_with_receipt(tx_b)?;
+
+    assert_terminal_digests_equal(&snap_a, &snap_b);
+    assert_eq!(
+        receipt_a.digest(),
+        receipt_b.digest(),
+        "receipt digest must match across enqueue orders"
+    );
+    Ok(())
+}
+
+#[test]
+fn dpo_litmus_conflicting_pair_is_deterministically_rejected() -> Result<(), EngineError> {
+    // Two candidates overlap (critical-pair style): only one should be admitted,
+    // and the winner must be deterministic (enqueue-order independent).
+    fn setup() -> Result<(Engine, NodeId), EngineError> {
+        let mut engine = build_litmus_engine()?;
+
+        let entity = make_node_id("litmus-entity-conflict");
+        engine.insert_node(
+            entity,
+            NodeRecord {
+                ty: make_type_id("entity"),
+            },
+        )?;
+        let pos = [0.0, 0.0, 0.0];
+        let vel = [1.0, 0.0, 0.0];
+        engine.set_node_attachment(
+            entity,
+            Some(AttachmentValue::Atom(encode_motion_atom_payload(pos, vel))),
+        )?;
+
+        Ok((engine, entity))
+    }
+
+    let (mut a, entity) = setup()?;
+    let tx_a = a.begin();
+    assert!(matches!(
+        a.apply(tx_a, warp_core::MOTION_RULE_NAME, &entity)?,
+        ApplyResult::Applied
+    ));
+    assert!(matches!(
+        a.apply(tx_a, PORT_RULE_NAME, &entity)?,
+        ApplyResult::Applied
+    ));
+    let (snap_a, receipt_a, _patch_a) = a.commit_with_receipt(tx_a)?;
+
+    let (mut b, entity) = setup()?;
+    let tx_b = b.begin();
+    assert!(matches!(
+        b.apply(tx_b, PORT_RULE_NAME, &entity)?,
+        ApplyResult::Applied
+    ));
+    assert!(matches!(
+        b.apply(tx_b, warp_core::MOTION_RULE_NAME, &entity)?,
+        ApplyResult::Applied
+    ));
+    let (snap_b, receipt_b, _patch_b) = b.commit_with_receipt(tx_b)?;
+
+    assert_terminal_digests_equal(&snap_a, &snap_b);
+    assert_eq!(receipt_a.digest(), receipt_b.digest());
+
+    let a_entries = receipt_a.entries();
+    assert_eq!(a_entries.len(), 2, "fixture must produce two candidates");
+    let applied = a_entries
+        .iter()
+        .filter(|e| e.disposition == warp_core::TickReceiptDisposition::Applied)
+        .count();
+    let rejected = a_entries
+        .iter()
+        .filter(|e| {
+            e.disposition
+                == warp_core::TickReceiptDisposition::Rejected(
+                    warp_core::TickReceiptRejection::FootprintConflict,
+                )
+        })
+        .count();
+    assert_eq!(applied, 1, "exactly one candidate must be applied");
+    assert_eq!(rejected, 1, "exactly one candidate must be rejected");
+
+    Ok(())
+}
+
+#[test]
+fn dpo_litmus_overlapping_scope_disjoint_ports_are_composable() -> Result<(), EngineError> {
+    // Two candidates share the same scope node but reserve disjoint boundary ports.
+    // This is an “overlap but still composable” case: both should be admitted and
+    // the terminal digest must be enqueue-order independent.
+    fn setup() -> Result<(Engine, NodeId), EngineError> {
+        let mut engine = build_litmus_engine()?;
+        let entity = make_node_id("litmus-entity-ports");
+        engine.insert_node(
+            entity,
+            NodeRecord {
+                ty: make_type_id("entity"),
+            },
+        )?;
+        Ok((engine, entity))
+    }
+
+    let (mut a, entity) = setup()?;
+    let tx_a = a.begin();
+    assert!(matches!(
+        a.apply(tx_a, LITMUS_PORT_READ_0, &entity)?,
+        ApplyResult::Applied
+    ));
+    assert!(matches!(
+        a.apply(tx_a, LITMUS_PORT_READ_1, &entity)?,
+        ApplyResult::Applied
+    ));
+    let (snap_a, receipt_a, _patch_a) = a.commit_with_receipt(tx_a)?;
+
+    let (mut b, entity) = setup()?;
+    let tx_b = b.begin();
+    assert!(matches!(
+        b.apply(tx_b, LITMUS_PORT_READ_1, &entity)?,
+        ApplyResult::Applied
+    ));
+    assert!(matches!(
+        b.apply(tx_b, LITMUS_PORT_READ_0, &entity)?,
+        ApplyResult::Applied
+    ));
+    let (snap_b, receipt_b, _patch_b) = b.commit_with_receipt(tx_b)?;
+
+    assert_terminal_digests_equal(&snap_a, &snap_b);
+    assert_eq!(receipt_a.digest(), receipt_b.digest());
+
+    let entries = receipt_a.entries();
+    assert_eq!(entries.len(), 2);
+    assert!(
+        entries
+            .iter()
+            .all(|e| e.disposition == warp_core::TickReceiptDisposition::Applied),
+        "both disjoint-port candidates should be admitted"
+    );
+
+    Ok(())
+}
diff --git a/docs/decision-log.md b/docs/decision-log.md
index 78232e14..fe46615d 100644
--- a/docs/decision-log.md
+++ b/docs/decision-log.md
@@ -6,6 +6,7 @@
 
 | Date | Context | Decision | Rationale | Consequence |
 | ---- | ------- | -------- | --------- | ----------- |
+| 2026-01-03 | Planning hygiene + M2.1 kickoff | Refresh `docs/execution-plan.md` to reflect current GitHub state and begin issue #206 (DPO concurrency litmus: spec note + tests). | The execution plan had drifted (closed issues and PR-queue work still marked as active), which wastes triage time. Issue #206 is a leverage point: it turns DPO concurrency claims into pinned, executable cases. | The active frontier is now issue-driven again, and #206 work proceeds as a single-purpose branch with deterministic litmus tests + a small spec note. |
 | 2026-01-02 | Docs tooling: VitePress upgrade | Upgrade the pinned docs site generator from `vitepress@0.1.1` to a modern stable VitePress release, and keep VitePress pages “plain Markdown” (avoid YAML frontmatter) because SPDX HTML comment headers must be first in-file. | The current VitePress pin is too old to run on modern Node (e.g., Node 25 breaks old `fs.rmdir({ recursive: true })` usage). VitePress frontmatter parsing requires `---` at the start of the file, but repo policy requires SPDX headers first. | `pnpm docs:build` and `pnpm docs:dev` become reliable for contributors on current Node toolchains; angle-bracket / generic-type syntax is no longer misinterpreted as HTML; dead-link checks catch broken internal references; docs pages don’t leak frontmatter into rendered output. |
 | 2026-01-02 | Docs: scheduler benchmarks drift | Consolidate the implemented `warp-core` scheduler benchmarks into a canonical performance doc (`docs/scheduler-performance-warp-core.md`), keep planned system-scheduler benchmark scenarios in `docs/spec-scheduler.md`, and turn `docs/scheduler-benchmarks.md` into a lightweight redirect. | Bench docs tend to rot when they mix “planned” and “implemented” benchmarks. A canonical, implementation-focused doc keeps links to real bench files accurate and reviewable. | Contributors have a single place to find and run warp-core scheduler benchmarks, while older links remain stable and planned scenarios remain discoverable. |
 | 2026-01-02 | Docs: scheduler confusion | Introduce a scheduler landing doc (`docs/scheduler.md`) that distinguishes the implemented `warp-core` rewrite scheduler (`reserve()`/drain) from the planned Echo ECS/system scheduler, and consolidate `reserve()` evidence into a single canonical doc (`docs/scheduler-warp-core.md`) with redirects for older links. | Multiple docs used “scheduler” to mean different mechanisms (rewrite scheduling vs ECS/system ordering), which causes onboarding and review confusion. Consolidating `reserve()` documentation reduces drift and keeps evidence/claims reviewable in one place. | Contributors can quickly pick the correct scheduler document; future changes to either scheduler have canonical entrypoints for documentation updates, and older links remain stable. |
@@ -112,6 +113,12 @@
 ## Recent Decisions (2025-10-28 onward)
 
 The following entries use a heading + bullets format for richer context.
+
+## 2026-01-03 — Planning hygiene + #206 kickoff (DPO concurrency litmus)
+
+- Decision: treat the execution plan as a live artifact again (update “Today’s Intent” + “Next Up”), then start issue #206 with a minimal spec note + deterministic litmus tests in `warp-core`.
+- Rationale: plan drift causes duplicate triage, and concurrency/determinism claims need executable, reviewable evidence (commuting vs conflicting vs overlapping-but-safe cases).
+- Next: land a small DPO concurrency note and a new litmus test file that compares terminal digests across enqueue orders and pins conflict outcomes.
 | 2025-12-01 | `docs/guides/how-do-echo-work` PDF build | Escaped bare `&` tokens, fixed TikZ bidirectional arrows, added a minimal Rust listing language, and made the LaTeX Makefile run in non-interactive `-halt-on-error` mode (three passes). | Prevents TikZ parse failures and listings errors, avoids TeX prompting in CI/automation, and keeps code samples readable. | `make` in `docs/guides/how-do-echo-work` now produces `main.pdf` without interaction; remaining output is cosmetic overfull hbox warnings. |
 | 2025-12-01 | `docs/guides/how-do-echo-work` accuracy + visuals | Synced guide content to current code: clarified scheduler kinds (Radix/Legacy), footprint conflicts, sandbox determinism helper, and `F32Scalar` behavior (canonical zero only; NaNs passthrough for now). Added timeline tree TikZ, resized hex diagram, refreshed comparison table, and Rust listings. Removed layout warnings. | Keep the guide truthful to warp-core as implemented; improves reader clarity and CI reliability. | `main.pdf` builds non-interactively; visuals/tables reflect actual APIs and invariants; remaining determinism work (LUT sin/cos, NaN canonicalization) is called out as future work. |
 | 2025-12-01 | SPDX appendix + CI check | Added `legal-appendix.tex` with dual-license explainer and included it in the guide. Introduced `spdx-header-check.yml` workflow that runs `scripts/check_spdx.sh --check --all` to enforce SPDX headers. | Ensures licensing terms are visible in the book and keeps automated enforcement in CI. | New appendix renders in PDF; workflow will fail PRs missing SPDX headers. |
diff --git a/docs/execution-plan.md b/docs/execution-plan.md
index e20afa01..682aac70 100644
--- a/docs/execution-plan.md
+++ b/docs/execution-plan.md
@@ -35,16 +35,27 @@ This is Codex’s working map for building Echo. Update it relentlessly—each s
 
 ## Today’s Intent
 
-> 2026-01-03 — Merge-train: oldest open PRs (#220 → #227 → #242) (IN PROGRESS)
+> 2026-01-03 — Planning hygiene + start #206 (DPO concurrency litmus) (DONE)
 
-- Goal: land the remaining open PRs in oldest-first order using a deterministic merge workflow (no rebases).
-- Scope (repeat per PR):
-  - Checkout the PR branch.
-  - Merge `origin/main` into it and resolve conflicts.
-  - Pull PR comments/review threads and extract actionable items (including human reviewer notes).
-  - Fix remaining issues (or perform a strict self-review if no actionables remain), then push.
-  - If clean: merge the branch into `origin/main` via merge commit and verify PR state.
-- Exit criteria: each PR is either merged to `main` or has a pushed fix commit + explicit next-step notes.
+- Goal: refresh the execution plan so it matches current GitHub state, then begin issue #206 with a minimal “DPO concurrency litmus” suite (spec note + tests).
+- Scope:
+  - Planning hygiene:
+    - Update this document’s *Today’s Intent* and “Next Up” queue to reflect the current work frontier.
+    - Record the pivot in `docs/decision-log.md` so the next session doesn’t re-triage already-closed threads.
+  - #206:
+    - Add a spec note documenting which parts of the DPO concurrency story Echo relies on (and what we enforce mechanically via footprints + scheduler independence checks).
+    - Add litmus tests that pin commuting/overlapping/conflicting rule-pair outcomes deterministically.
+- Outcome:
+  - Planning hygiene: execution-plan “Today’s Intent” + “Next Up” refreshed to match GitHub state.
+  - #206 started with a minimal spec note + litmus tests (commuting vs conflicting vs overlapping-but-safe).
+- Evidence:
+  - `docs/spec/SPEC-0003-dpo-concurrency-litmus-v0.md`
+  - `crates/warp-core/tests/dpo_concurrency_litmus.rs`
+
+> 2026-01-03 — Merge-train: oldest open PRs (#220 → #227 → #242) (DONE)
+
+- Outcome: no open PRs remained by the end of the merge-train; the last merges landed on `main` (see merge commit `8082bbb`).
+- Next: treat subsequent work as issue-driven (one branch per issue), starting with #206.
 
 > 2026-01-03 — PR #213: merge `origin/main` + resolve review feedback (DONE)
 
@@ -1042,11 +1053,11 @@ This is Codex’s working map for building Echo. Update it relentlessly—each s
 
 ## Next Up Queue
 
-1. WARP View Protocol demo path (`docs/tasks.md`)
-2. ECS storage implementation plan
-3. Branch tree BlockStore abstraction design
-4. Temporal Bridge implementation plan
-5. Confluence + serialization protocol review
+1. M2.1: DPO concurrency theorem coverage (issue #206)
+2. Demo 2: Splash Guy docs course modules (issue #226)
+3. Demo 3: Tumble Tower Stage 1 physics (issue #232)
+4. TT1 follow-ons: dt policy / retention / merge semantics / capabilities (issues #243–#246)
+5. ECS storage implementation plan
 
 Populate with concrete tasks in priority order. When you start one, move it to “Today’s Intent.”
 
diff --git a/docs/spec-mwmr-concurrency.md b/docs/spec-mwmr-concurrency.md
index 9ad5438c..2f024725 100644
--- a/docs/spec-mwmr-concurrency.md
+++ b/docs/spec-mwmr-concurrency.md
@@ -114,4 +114,4 @@ Phase 2 (Optimization)
 Phase 3 (Real demo)
 - Multiplayer confluence demo (zero desync), time‑travel fork/merge, inspector visualization of footprints/conflicts
 
-References: confluence skeleton v5, WARP math confluence, offset-graph arena notes
+References: confluence skeleton v5, WARP math confluence, offset-graph arena notes, SPEC-0003 (DPO concurrency litmus)
diff --git a/docs/spec/SPEC-0003-dpo-concurrency-litmus-v0.md b/docs/spec/SPEC-0003-dpo-concurrency-litmus-v0.md
new file mode 100644
index 00000000..41b684bf
--- /dev/null
+++ b/docs/spec/SPEC-0003-dpo-concurrency-litmus-v0.md
@@ -0,0 +1,74 @@
+<!-- SPDX-License-Identifier: Apache-2.0 OR MIND-UCAL-1.0 -->
+<!-- © James Ross Ω FLYING•ROBOTS <https://github.com/flyingrobots> -->
+# SPEC-0003: DPO Concurrency Litmus (v0)
+
+Status: Draft • Date: 2026-01-03 • Owner: warp-core
+
+This spec note is a bridge between the **DPO/DPOI concurrency story** (critical pairs, commuting squares, and order-independence) and what `warp-core` enforces **today**:
+
+- a deterministic scheduler order,
+- conservative **footprint-based independence checks**, and
+- receipts that commit to “accepted vs rejected” outcomes deterministically.
+
+It is intentionally “low ceremony”: the goal is to pin *executable evidence* (litmus tests) that match the theory-shaped intent without claiming we have implemented full categorical DPO.
+
+## What we are (and are not) proving in code
+
+`warp-core` does **not** implement categorical DPO/DPOI rewriting directly yet; rules are matcher/executor functions plus explicit read/write `Footprint`s. The concurrency claim we can actually test right now is:
+
+> Given a fixed starting state and a fixed set of candidate rewrites for a tick, the engine produces a unique deterministic outcome (same terminal digest) independent of the order in which candidates were enqueued.
+
+In other words: we test *order independence under the engine’s admissibility rules*, not the full “unique up to iso” statement from adhesive-category DPO.
+
+## Ambient assumptions (pragmatic “adhesive enough”)
+
+The intended north-star semantics are typed open-graph DPOI in an adhesive (or quasi-adhesive) setting. The implementation relies on a pragmatic subset of those assumptions:
+
+- **Typed graph discipline**: rules and payloads are domain-separated by `TypeId` and stable ids; “same bytes, different meaning” is prevented at the deterministic boundary.
+- **No hidden edges**: attachment bytes are opaque; any causal dependency that matters to matching/scheduling must be expressed as explicit skeleton structure (nodes/edges/ports) or explicit attachment-slot reads (Stage B1 descent-chain reads).
+- **Gluing/dangling conditions become mechanical invariants**:
+  - “Dangling edge” and “delete-under-descent” hazards are prevented by rule design + validation (where present) and, critically, by conservative footprints that force serialization when overlap is possible.
+- **Deterministic resolution policy for overlaps**: overlapping candidates do not race; they are either:
+  - jointly admitted when independent, or
+  - deterministically rejected/serialized when not independent.
+
+## Mapping: DPO concurrency vocabulary → `warp-core` mechanisms
+
+This table is a translation layer for the parts we actually enforce mechanically.
+
+| DPO/DPOI concept | `warp-core` mechanism (today) |
+| --- | --- |
+| “Independent” parallel rewrites commute | `Footprint` sets are disjoint under the scheduler’s conflict rules; both candidates reserve and commit; result is order-independent. |
+| Critical pair (overlapping matches) | Overlap shows up as footprint intersection (node/edge/attachment/port); later candidate is rejected with `FootprintConflict`. |
+| Concurrency theorem gives uniqueness of result | Engine drains candidates in a canonical order and applies an admissible subset; receipts + digests pin the outcome deterministically. |
+| Gluing condition / dangling prevention | Enforced conservatively via explicit footprint reads/writes, “no hidden edges”, and (where implemented) validation checks. |
+
+## Litmus suite (executable taxonomy)
+
+The litmus suite exists to keep the “DPO concurrency” claim honest by pinning three case families:
+
+1. **Commuting / independent pair**
+   - Two candidates are independent (disjoint footprints).
+   - Enqueue order varies, but the terminal digest is identical.
+2. **Conflicting / critical-pair-style overlap**
+   - Two candidates overlap (footprint intersection).
+   - Outcome is deterministic: exactly one is admitted (canonical winner), and the other is rejected with `FootprintConflict` in the receipt.
+3. **Overlapping scope but still composable**
+   - Candidates share a high-level scope notion (e.g., both target the same node),
+     but their *resource footprints* remain disjoint (e.g., disjoint boundary ports, read-only overlaps).
+   - Both are admitted and the terminal digest is order-independent.
+
+## What “terminal digest” means here
+
+For litmus tests that compare different enqueue orders within the **same tick**, “terminal digest” is the full `Snapshot.hash` produced by `Engine::commit()`. This commits to:
+
+- `state_root` (reachable-only canonical hashing),
+- `patch_digest` (delta ops + slot sets),
+- parent list (empty for the first commit in the litmus setup), and
+- policy id (part of the deterministic boundary).
+
+## References
+
+- `docs/spec-mwmr-concurrency.md` (footprints, ports, and independence model)
+- `docs/warp-math-claims.md` (theory framing: DPO/DPOI + determinism claims)
+- Litmus tests: `crates/warp-core/tests/dpo_concurrency_litmus.rs`

From 8a7667f9d0b3f47bfe4b197686ba443443a94350 Mon Sep 17 00:00:00 2001
From: "J. Kirby Ross" <james@flyingrobots.dev>
Date: Fri, 2 Jan 2026 21:41:49 -0800
Subject: [PATCH 2/2] tests: strengthen DPO litmus receipt assertions

---
 .../warp-core/tests/dpo_concurrency_litmus.rs | 37 +++++++++++++++++++
 1 file changed, 37 insertions(+)

diff --git a/crates/warp-core/tests/dpo_concurrency_litmus.rs b/crates/warp-core/tests/dpo_concurrency_litmus.rs
index a6569682..25bb45cd 100644
--- a/crates/warp-core/tests/dpo_concurrency_litmus.rs
+++ b/crates/warp-core/tests/dpo_concurrency_litmus.rs
@@ -177,6 +177,25 @@ fn dpo_litmus_commuting_independent_pair() -> Result<(), EngineError> {
         receipt_b.digest(),
         "receipt digest must match across enqueue orders"
     );
+
+    // Verify both candidates were actually applied (not just that digests match).
+    let a_entries = receipt_a.entries();
+    assert_eq!(a_entries.len(), 2, "fixture must produce two candidates");
+    assert!(
+        a_entries
+            .iter()
+            .all(|e| e.disposition == warp_core::TickReceiptDisposition::Applied),
+        "independent candidates must both be applied"
+    );
+
+    let b_entries = receipt_b.entries();
+    assert_eq!(b_entries.len(), 2, "fixture must produce two candidates");
+    assert!(
+        b_entries
+            .iter()
+            .all(|e| e.disposition == warp_core::TickReceiptDisposition::Applied),
+        "independent candidates must both be applied (order B)"
+    );
     Ok(())
 }
 
@@ -184,6 +203,10 @@ fn dpo_litmus_commuting_independent_pair() -> Result<(), EngineError> {
 fn dpo_litmus_conflicting_pair_is_deterministically_rejected() -> Result<(), EngineError> {
     // Two candidates overlap (critical-pair style): only one should be admitted,
     // and the winner must be deterministic (enqueue-order independent).
+    //
+    // Conflict surface: both `motion/update` and `demo/port_nop` write the same
+    // α-plane node attachment slot (the motion payload), so their `a_write`
+    // footprints intersect when scoped to the same node.
     fn setup() -> Result<(Engine, NodeId), EngineError> {
         let mut engine = build_litmus_engine()?;
 
@@ -249,6 +272,13 @@ fn dpo_litmus_conflicting_pair_is_deterministically_rejected() -> Result<(), Eng
     assert_eq!(applied, 1, "exactly one candidate must be applied");
     assert_eq!(rejected, 1, "exactly one candidate must be rejected");
 
+    let b_entries = receipt_b.entries();
+    assert_eq!(b_entries.len(), 2, "fixture must produce two candidates");
+    assert_eq!(
+        a_entries, b_entries,
+        "receipt structure must be order-independent (not just digest)"
+    );
+
     Ok(())
 }
 
@@ -305,5 +335,12 @@ fn dpo_litmus_overlapping_scope_disjoint_ports_are_composable() -> Result<(), En
         "both disjoint-port candidates should be admitted"
     );
 
+    let b_entries = receipt_b.entries();
+    assert_eq!(b_entries.len(), 2);
+    assert_eq!(
+        entries, b_entries,
+        "receipt structure must be order-independent (not just digest)"
+    );
+
     Ok(())
 }
