diff --git a/.claude/board/INTEGRATION_PLANS.md b/.claude/board/INTEGRATION_PLANS.md index 560ef3cb5..c4a1a52fc 100644 --- a/.claude/board/INTEGRATION_PLANS.md +++ b/.claude/board/INTEGRATION_PLANS.md @@ -1,3 +1,8 @@ +## 2026-10-30 — D-DRCA-3: DR #4 method routing falsifier (lab) → `.claude/plans/d-drca-3-dr4-method-routing-v1.md` + +**Status:** lab probe in `dr-math-binding-probe` (`src/dr4.rs`, `tests/dr4_method_routing.rs`); first DR #4 falsifier of D-DRDT §5. **Board:** [entry](entries/2026-10-30-d-drca-3-dr4-method-routing.md), [STATUS_BOARD](STATUS_BOARD.md) D-DRCA-3. DT-owned method key, guard witness and effect order are carried opaque; the effect-order oracle is ndarray #395's order law. No DT resolver (D-CMH-1), no MethodKey mint, no contract change. +**Confidence:** 12 tests, 7 disable runs red; lab only. + ## 2026-10-28 — D-DRDT: DR = HHTL16 Cartesian direct routing, DT = ClassId binding store → `.claude/plans/d-drdt-dr-dt-ownership-amendment-v1.md` **Status:** PROPOSED, docs only; amends D-DT64-6 §1 (per-cell WHEN×ON×DO, DR#3) and supersedes the DT64 "tensor register" noun of Bardioc-rs #9. **Board:** [entry](entries/2026-10-28-d-drdt-dr-dt-ownership-amendment.md), [STATUS_BOARD](STATUS_BOARD.md) D-DRDT. Records the DR/DT contract, reads the DR64/DR256 overview against existing pieces, gives the reuse/gap table for Cartesian and relational fold operators (proof: #1834, D-DRCA-1) and hands off DT method identity / guard / effect order and the DR #4 interface. diff --git a/.claude/board/STATUS_BOARD.md b/.claude/board/STATUS_BOARD.md index 81e013c18..c6f17c9d6 100644 --- a/.claude/board/STATUS_BOARD.md +++ b/.claude/board/STATUS_BOARD.md @@ -5,9 +5,9 @@ | D-id | Deliverable | Status | Gate | |---|---|---|---| | D-DRDT-0 | amendment: DR/DT ownership, reuse/gap analysis, DT and DR #4 handoff (docs) | In PR | docs review | -| D-DRCA-1 | HHTL16 Cartesian projection proof in `dr-math-binding-probe` (12 tests, 6 disable runs, stage costs) | In PR (#1834) | review; lab only | -| D-DRCA-2 | DR256::WHERE × DR#3 and the stay / rebind / masked-read choice | Queued | D-DRCA-1 merged | -| D-DRCA-3 | DR #4 falsifier: two methods, same read/write sets, different effect order, stay distinct; dropped guard refuses | Queued | DT MethodId contract (D-DRDT §4) | +| D-DRCA-1 | HHTL16 Cartesian projection proof in `dr-math-binding-probe` (12 tests, 6 disable runs, stage costs) | Shipped (#1834) | review; lab only | +| D-DRCA-2 | DR256::WHERE × DR#3 and the stay / rebind / masked-read choice | Shipped (#1836) | lab only | +| D-DRCA-3 | DR #4 falsifier: two methods, same read/write sets, different effect order, stay distinct; dropped guard refuses | In PR (lab: `dr4.rs`, 12 tests, 7 disable runs; [entry](entries/2026-10-30-d-drca-3-dr4-method-routing.md)) | lab uses a test-minted method key; the real key and the DT resolver stay with D-CMH (MethodKey mint, D-CMH-1) | ## D-DT64-6 — DR64 routing, DT64 bind store, per-cell WHEN×ON×DO, OGIT reference predicates (2026-10-28) diff --git a/.claude/board/entries/2026-10-30-d-drca-3-dr4-method-routing.md b/.claude/board/entries/2026-10-30-d-drca-3-dr4-method-routing.md new file mode 100644 index 000000000..835d744e6 --- /dev/null +++ b/.claude/board/entries/2026-10-30-d-drca-3-dr4-method-routing.md @@ -0,0 +1,18 @@ +# D-DRCA-3: DR #4 method routing falsifier + +**Status:** TEST-PINNED, lab only. Code: `crates/dr-math-binding-probe/src/dr4.rs`, test `tests/dr4_method_routing.rs`; plan `.claude/plans/d-drca-3-dr4-method-routing-v1.md`. Contract: D-DRDT §5 (#1835). + +## Result + +- Two methods on one cell with equal read/write sets and effects `[Set(1), Add(1)]` vs `[Add(1), Set(1)]` (oracle 2 vs 1; `check_reorder` refuses the swap) stay two routed entries, each with its own effect-order reference. Two methods whose effects commute also stay two entries: merging is not DR's decision. +- A declared guard with no witness refuses (`GuardDropped`), a different witness refuses (`GuardMismatch`), the right witness is carried; an unguarded method needs none. +- Refused, each with its own variant: stale register frame, resolution under another frame issue (including another store at equal numbers), foreign class, duplicate key, coordinates outside 64 × 64, numeric fold, presence over a three-valued register. +- Cell, row and column values equal a scalar loop; K3 value is masked by validity (the fixture has UNKNOWN cells with a 1 payload). +- DT-owned values (method key, guard witness, effect-order reference) are opaque to DR. The effect-order law is ndarray #395's, ported verbatim into the test as the oracle. +- 12 tests; 7 disable runs, each red on its named test. + +## Open + +- The method key is test-minted; the real one is DT's (D-CMH §2.1, decision ledger item 2). The DT resolver is D-CMH-1's `PreparedClass`, not built here. +- DT gaps of D-DRDT §4 stay with the contract owner: no MethodId independent of name (`ActionDef.predicate`), single `field == value` guard, no effect order, no single lookup. +- DR #4 over a `LocalSelection` or a `Chain` composition is untested. diff --git a/.claude/board/entries/README.md b/.claude/board/entries/README.md index 56f735fd6..5aa3b5cea 100644 --- a/.claude/board/entries/README.md +++ b/.claude/board/entries/README.md @@ -25,10 +25,11 @@ 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. -502 entries, 2026-08-06 .. 2026-10-29. +503 entries, 2026-08-06 .. 2026-10-30. | date | entry id | finding | file | |---|---|---|---| +| 2026-10-30 | `D-DRCA-3` | | [2026-10-30-d-drca-3-dr4-method-routing.md](2026-10-30-d-drca-3-dr4-method-routing.md) | | 2026-10-29 | `palette512-turbovec9-nsl-worksteal` | | [2026-10-29-palette512-turbovec9-nsl-worksteal.md](2026-10-29-palette512-turbovec9-nsl-worksteal.md) | | 2026-10-28 | `thought-layers-nan-skip` | | [2026-10-28-thought-layers-nan-skip.md](2026-10-28-thought-layers-nan-skip.md) | | 2026-10-28 | `lane-layout-from-classview` | | [2026-10-28-lane-layout-from-classview.md](2026-10-28-lane-layout-from-classview.md) | diff --git a/.claude/plans/d-drca-3-dr4-method-routing-v1.md b/.claude/plans/d-drca-3-dr4-method-routing-v1.md new file mode 100644 index 000000000..1dde8874d --- /dev/null +++ b/.claude/plans/d-drca-3-dr4-method-routing-v1.md @@ -0,0 +1,85 @@ +# D-DRCA-3: DR #4 method routing falsifier (lab) + +**Date:** 2026-10-30. **Status:** PROPOSED → implemented as a lab probe in +`crates/dr-math-binding-probe` (`src/dr4.rs`, `tests/dr4_method_routing.rs`). +**Parent:** D-DRDT (`d-drdt-dr-dt-ownership-amendment-v1.md`, #1835) §5 "Handoff: +DR #4", first falsifier. **Not:** a DT resolver, a MethodKey mint, an ABI, a +contract change, or method execution. + +## Overview + +#1835 §5 defines DR #4 as the route from a mapped coordinate set to a method +operation, and fixes what it must preserve and refuse. Its first falsifier: +*two methods on one cell with the same read/write sets and different effect +order must stay distinct through routing, and a dropped guard must refuse.* + +DR stores neither a method's meaning nor its effects (#1835 §1). So the lab +treats every DT-owned value as **opaque**: the method key, the signature +revision, the guard witness and the effect-order reference are carried, never +interpreted. The meaning lives in the test's DT stub, which is also the +oracle that proves two routed methods really are different. + +### Ownership boundaries kept + +- **Method identity is DT's, and is not minted here.** D-CMH + (`class-method-schema-hotplug-v1.md` §2.1, decision ledger item 2) leaves the + 16-byte `MethodKey` to the OGAR owner. The lab uses a test-minted + `[u8; 16]`, named as such. +- **The DT resolver is D-CMH-1's `PreparedClass`, not this probe.** No second + resolver, no contract type. `Resolution` here is a lab stand-in for DT's + answer, constructed only by the test. +- **The effect-order law is #395's** (ndarray `examples/pof_antennas/order_law.rs`: + `Effect`, `run_effects`, `commutes`, `check_reorder`), ported verbatim into + the test as the oracle. DR does not decide commutation. + +## Checklist + +- [x] Read the parent contract (#1835 §4–§5), D-CMH (§2.1, §7), the #395 order law, + and the existing lab API (`lib.rs`, `where_dr3.rs`, `hhtl16.rs`). +- [x] Tests first (`tests/dr4_method_routing.rs`), confirmed red before the module exists. +- [x] `src/dr4.rs`: `route` over one admitted `BoundDr64` and one `Resolution`. +- [x] Disable runs, each red on a named test. +- [x] README section, board entry, STATUS_BOARD row, entries index. + +## Contract under test + +`route(store, register, resolution, op, observed_guards) -> Result` + +**Preserves** (one output entry per input method, in input order): method key, +signature revision, read and write field sets, guard witness, effect-order +reference, and the register's frame. + +**Refuses**, in this order: + +| refusal | when | +|---|---| +| `Frame(Refusal)` | the register's frame is not its store's current seal | +| `ResolvedUnderOtherFrame` | DT resolved the methods under another frame issue (another revision, a reseal or another store, even at equal numbers) | +| `ForeignClass` | the resolution or a method belongs to another class than the register | +| `DuplicateMethod` | one method key appears twice (two keys with equal sets are fine) | +| `OutOfRegister` | the operation's coordinates are outside 64 × 64 | +| `UnsupportedAlgebra` | the method declares an algebra DR does not have (a numeric fold) | +| `NotBoolean` | a presence method over a three-valued register | +| `GuardDropped` / `GuardMismatch` | a declared guard has no witness, or another one | + +## Falsifiers + +1. Two methods, equal read/write sets, effects `[Set(1), Add(1)]` vs + `[Add(1), Set(1)]`: the oracle gives 2 vs 1 and `check_reorder` refuses the + swap; routing returns two entries with their own effect references. +2. Commuting effects (`[Add(2), Add(3)]` vs reversed): the oracle gives equal + results and the swap is legal; routing **still** returns two entries. + Merging is not DR's decision. +3. A required guard with no witness refuses; a different witness refuses; the + right witness is carried into the output. An unguarded method needs none. +4. Stale register frame, stale resolution, foreign store at equal numbers, + foreign class, duplicate key, out-of-register, numeric algebra, presence over + three-valued: each refuses with its own variant. +5. Values equal an independent scalar loop for cell, row and column, two- and + three-valued (K3 value masked by validity). + +## Not done + +DT resolver (D-CMH-1); MethodKey mint; guard evaluation (DR only carries +witnesses); effect execution; DR #4 over a `LocalSelection` (D-DRCA-2) or a +`Chain` composition; production placement. diff --git a/crates/dr-math-binding-probe/README.md b/crates/dr-math-binding-probe/README.md index b5fddf871..bdb59a4ad 100644 --- a/crates/dr-math-binding-probe/README.md +++ b/crates/dr-math-binding-probe/README.md @@ -135,3 +135,18 @@ One WHERE halves the fresh read. Warm reuse breaks even at N = 1 and pays from N - A negated selection costs its own WHERE, which is the price of `NOT UNKNOWN` staying UNKNOWN. - One 64-slot frame per table; no larger focus, no DR256 resident register, no reuse of a scattered (`ScatterOrU32`) mask. - `project` is 64 scalar probes (~1 µs); admission (~76–82 ns) is not broken down. + +## D-DRCA-3: DR #4 method routing (`dr4`) + +The first DR #4 falsifier of D-DRDT §5 (#1835): two methods on one cell with the same read/write sets and a different effect order must stay distinct through routing, and a dropped guard must refuse. Module `src/dr4.rs`, test `tests/dr4_method_routing.rs`, plan `.claude/plans/d-drca-3-dr4-method-routing-v1.md`. + +- **DR carries DT's values opaque.** `MethodKey`, `GuardWitness` and `EffectOrderRef` are 16-byte references that `route` compares for equality and never interprets. The method key is DT's to mint (D-CMH §2.1); the test mints its own, named as such. `Resolution` (class, frame, methods) is DT's answer handed in by the caller; this crate has no DT resolver (that is D-CMH-1's `PreparedClass`). +- **One entry per input method, in input order.** Key, signature revision, read and write field sets, guard witness and effect-order reference pass through unchanged, with the register's frame on the result. Nothing is merged: two methods whose effects commute are still two entries, because merging is the law owner's decision. +- **Refusals, in order:** a stale register frame (`Frame(..)`); a resolution made under another frame issue, including another store at equal numbers (`ResolvedUnderOtherFrame`); the resolution or a method for another class (`ForeignClass`); a duplicate key (`DuplicateMethod`; equal read/write sets are not a duplicate); coordinates outside 64 × 64 (`OutOfRegister`); a numeric fold (`UnsupportedAlgebra`); a presence read over a three-valued register (`NotBoolean`); a declared guard with no witness (`GuardDropped`) or another one (`GuardMismatch`). DR checks witnesses; it evaluates no guard. +- **Values** come from the existing register reads: cell, row and column presence, and K3 value + validity with the value masked by validity. + +Oracle: the DT stub in the test holds each method's real effects and guard. The effect-order law is ndarray #395's `Effect` / `run_effects` / `commutes` / `check_reorder` (`examples/pof_antennas/order_law.rs`), ported verbatim. In the core fixture `[Set(1), Add(1)]` and `[Add(1), Set(1)]` give 2 and 1 and the swap is refused, so the two references DR keeps apart are provably different methods; the commuting control `[Add(2), Add(3)]` and its reverse give equal results and the swap is legal, and routing still keeps both. Values are compared against plain scalar loops over the register words. + +Twelve tests; seven disable runs, each restored from the commit and each turning its named test red: entries collapsed by equal read/write sets (3 tests red), a dropped guard accepted, a mismatched witness accepted, the resolution frame not checked, a method's class not checked, a duplicate key accepted, the K3 value not masked by validity. + +**Not done.** The DT resolver (D-CMH-1), a minted `MethodKey`, guard evaluation, effect execution, DR #4 over a `LocalSelection` (D-DRCA-2) or a `Chain` composition, production placement. diff --git a/crates/dr-math-binding-probe/src/dr4.rs b/crates/dr-math-binding-probe/src/dr4.rs new file mode 100644 index 000000000..167d40db7 --- /dev/null +++ b/crates/dr-math-binding-probe/src/dr4.rs @@ -0,0 +1,275 @@ +//! D-DRCA-3: DR #4, method routing over one admitted register (lab only). +//! +//! DR #4 is the route from a mapped coordinate set to a method operation +//! (D-DRDT §5, lance-graph #1835). DR owns the coordinates and the fold; DT +//! owns what a method means. So every DT-owned value here is **opaque**: +//! +//! - [`MethodKey`]: the method's identity. Minted by the DT owner (D-CMH +//! §2.1); this lab never mints one and never derives one from a name. +//! - [`GuardWitness`]: evidence that DT's guard was evaluated. DR compares it +//! for equality and never evaluates a guard. +//! - [`EffectOrderRef`]: DT's reference to the method's ordered effects. DR +//! never runs, reorders or compares effects by meaning. +//! +//! # What routing preserves +//! +//! One [`RoutedMethod`] per input method, in input order: the key, the +//! signature revision, the read and write field sets, the guard witness and +//! the effect-order reference. Two methods with equal read/write sets and a +//! different effect order are two entries. So are two methods whose effects +//! commute: whether they may be merged is decided by the law owner, not by +//! routing. +//! +//! # What routing refuses +//! +//! In order: a stale register frame, a resolution made under another frame +//! issue, a foreign class, a duplicate key, coordinates outside 64 × 64, an +//! algebra DR does not have, a presence read over a three-valued register, +//! and a guard that was declared but not witnessed (or witnessed differently). +//! See [`Dr4Refusal`]. +//! +//! # What this module does not do +//! +//! It is not a DT resolver (that is D-CMH-1's `PreparedClass`), it stores +//! nothing, and it executes no effect. [`Resolution`] is DT's answer, handed +//! in by the caller. + +use lance_graph_contract::class_view::ClassId; + +use crate::hhtl16; +use crate::{BoundDr64, Frame, FrameStore, Population, Refusal, Truth}; + +/// A method's identity, minted by the DT owner. Opaque to DR. +#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)] +pub struct MethodKey(pub [u8; 16]); + +/// Evidence that a method's guard was evaluated. Opaque to DR. +#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)] +pub struct GuardWitness(pub [u8; 16]); + +/// DT's reference to a method's ordered effects. Opaque to DR. +#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)] +pub struct EffectOrderRef(pub [u8; 16]); + +/// The algebra a method declares for its operation over the register. +#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)] +pub enum Algebra { + /// Boolean presence over a two-valued, distinct register. + Presence, + /// Value and validity, three-valued; a two-valued register is known + /// everywhere. + PresenceK3, + /// A numeric fold. DR has no admitted numeric fold over DR64, so this + /// refuses. + NumericFold, +} + +/// Whether DT declared a guard for the method, and which. +#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)] +pub enum GuardDecl { + Unguarded, + Required(GuardWitness), +} + +/// One method as DT resolved it, as DR receives it. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub struct MethodRef { + pub class: ClassId, + pub key: MethodKey, + pub signature_rev: u32, + /// Field positions read and written (a `FieldMask`-width lab view). + pub reads: u64, + pub writes: u64, + pub guard: GuardDecl, + pub effects: EffectOrderRef, + pub algebra: Algebra, +} + +/// DT's answer for one class, and the frame it was resolved under. +#[derive(Clone, Debug)] +pub struct Resolution { + pub class: ClassId, + pub under: Frame, + pub methods: Vec, +} + +/// The operation routed over the register's coordinates. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum Op { + Cell { x: u8, y: u8 }, + Row { x: u8 }, + Column { y: u8 }, +} + +/// What one method's algebra produced at the routed coordinates. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum Value { + Bool(bool), + Mask(u64), + /// `value` is masked by `known`: an UNKNOWN cell never reads TRUE. + K3 { + value: u64, + known: u64, + }, +} + +/// One routed method: its DT references, unchanged, and its value. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub struct RoutedMethod { + pub key: MethodKey, + pub signature_rev: u32, + pub reads: u64, + pub writes: u64, + /// The witness the guard was checked against; `None` when unguarded. + pub guard: Option, + pub effects: EffectOrderRef, + pub value: Value, +} + +/// The routing result. No public constructor. +#[derive(Clone, Debug)] +pub struct Routed { + frame: Frame, + op: Op, + entries: Vec, +} + +impl Routed { + /// The frame the result was computed under. + pub fn frame(&self) -> &Frame { + &self.frame + } + pub fn op(&self) -> Op { + self.op + } + /// One entry per input method, in input order. + pub fn entries(&self) -> &[RoutedMethod] { + &self.entries + } +} + +/// Why a route was refused. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum Dr4Refusal { + /// The register's frame is not its store's current seal. + Frame(Refusal), + /// DT resolved the methods under another frame issue. + ResolvedUnderOtherFrame, + /// The resolution, or one of its methods, is for another class. + ForeignClass, + /// One method key appears twice. + DuplicateMethod, + /// Coordinates outside 64 × 64. + OutOfRegister, + /// The method declares an algebra DR does not have. + UnsupportedAlgebra, + /// A presence read over a three-valued or bag register. + NotBoolean, + /// A declared guard has no witness. + GuardDropped, + /// A declared guard was witnessed with another value. + GuardMismatch, +} + +/// Route DT's methods for one class over one admitted register. +/// +/// `observed` holds the guard witnesses the caller obtained, keyed by method. +pub fn route( + store: &FrameStore, + register: &BoundDr64<'_>, + resolution: &Resolution, + op: Op, + observed: &[(MethodKey, GuardWitness)], +) -> Result { + store.check(®ister.frame).map_err(Dr4Refusal::Frame)?; + if !resolution.under.same_issue(®ister.frame) { + return Err(Dr4Refusal::ResolvedUnderOtherFrame); + } + let class = register.method.owner_class; + if resolution.class != class || resolution.methods.iter().any(|m| m.class != class) { + return Err(Dr4Refusal::ForeignClass); + } + for (i, m) in resolution.methods.iter().enumerate() { + if resolution.methods[..i].iter().any(|p| p.key == m.key) { + return Err(Dr4Refusal::DuplicateMethod); + } + } + let in_range = match op { + Op::Cell { x, y } => x < 64 && y < 64, + Op::Row { x } => x < 64, + Op::Column { y } => y < 64, + }; + if !in_range { + return Err(Dr4Refusal::OutOfRegister); + } + let boolean = register.method.truth == Truth::TwoValued + && register.method.population == Population::Distinct; + + let mut entries = Vec::with_capacity(resolution.methods.len()); + for m in &resolution.methods { + let value = match m.algebra { + Algebra::NumericFold => return Err(Dr4Refusal::UnsupportedAlgebra), + Algebra::Presence if !boolean => return Err(Dr4Refusal::NotBoolean), + Algebra::Presence => presence(register, op), + Algebra::PresenceK3 => presence_k3(register, op), + }; + let guard = match m.guard { + GuardDecl::Unguarded => None, + GuardDecl::Required(want) => { + let got = observed + .iter() + .find(|(k, _)| *k == m.key) + .map(|(_, w)| *w) + .ok_or(Dr4Refusal::GuardDropped)?; + if got != want { + return Err(Dr4Refusal::GuardMismatch); + } + Some(got) + } + }; + entries.push(RoutedMethod { + key: m.key, + signature_rev: m.signature_rev, + reads: m.reads, + writes: m.writes, + guard, + effects: m.effects, + value, + }); + } + Ok(Routed { + frame: register.frame.clone(), + op, + entries, + }) +} + +/// Boolean read; coordinates are already in range. +fn presence(r: &BoundDr64<'_>, op: Op) -> Value { + match op { + Op::Cell { x, y } => Value::Bool((r.rows[x as usize] >> y) & 1 == 1), + Op::Row { x } => Value::Mask(r.rows[x as usize]), + Op::Column { y } => Value::Mask(hhtl16::column(r.rows, y).unwrap_or(0)), + } +} + +/// Value and validity; a two-valued register is known everywhere. +fn presence_k3(r: &BoundDr64<'_>, op: Op) -> Value { + let all = [u64::MAX; 64]; + let validity = r.validity.unwrap_or(&all); + let (value, known) = match op { + Op::Cell { x, y } => { + let k = (validity[x as usize] >> y) & 1; + ((r.rows[x as usize] >> y) & k, k) + } + Op::Row { x } => (r.rows[x as usize], validity[x as usize]), + Op::Column { y } => ( + hhtl16::column(r.rows, y).unwrap_or(0), + hhtl16::column(validity, y).unwrap_or(0), + ), + }; + Value::K3 { + value: value & known, + known, + } +} diff --git a/crates/dr-math-binding-probe/src/lib.rs b/crates/dr-math-binding-probe/src/lib.rs index b1cb70372..fd7100549 100644 --- a/crates/dr-math-binding-probe/src/lib.rs +++ b/crates/dr-math-binding-probe/src/lib.rs @@ -290,3 +290,7 @@ pub mod relcomp; /// projected into one table's 64-slot frame and read over DR#3, with every /// reuse re-admitted against its guards. pub mod where_dr3; + +/// D-DRCA-3: DR #4 method routing over one admitted register. DT-owned +/// method key, guard witness and effect order are carried opaque. +pub mod dr4; diff --git a/crates/dr-math-binding-probe/tests/dr4_method_routing.rs b/crates/dr-math-binding-probe/tests/dr4_method_routing.rs new file mode 100644 index 000000000..7abe11ffb --- /dev/null +++ b/crates/dr-math-binding-probe/tests/dr4_method_routing.rs @@ -0,0 +1,513 @@ +//! D-DRCA-3: the DR #4 falsifier (D-DRDT §5, lance-graph #1835). +//! +//! Two methods on one cell with the same read/write sets and a different effect +//! order must stay distinct through routing, and a dropped guard must refuse. +//! +//! DR carries method references as opaque values. Their meaning lives in the +//! DT stub below, which is also the oracle: it shows that two references DR +//! keeps apart really are different methods. The effect-order law is ndarray +//! #395's (`examples/pof_antennas/order_law.rs`), ported verbatim. + +use dr_math_binding_probe::dr4::{ + Algebra, Dr4Refusal, EffectOrderRef, GuardDecl, GuardWitness, MethodKey, MethodRef, Op, + Resolution, Value, route, +}; +use dr_math_binding_probe::{ + Axis, AxisKind, BoundDr64, Focus, FrameRevisions, FrameStore, Guards, MethodSignature, Operand, + Refusal, Scope, Truth, bind_dr64, +}; +use lance_graph_contract::class_view::ClassId; +use sha2::{Digest, Sha256}; + +// ── #395 order law, verbatim (ndarray examples/pof_antennas/order_law.rs) ── + +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +enum Effect { + Set(i64), + Add(i64), + Mul(i64), +} + +impl Effect { + fn apply(&self, cell: i64) -> Option { + match *self { + Effect::Set(v) => Some(v), + Effect::Add(v) => cell.checked_add(v), + Effect::Mul(v) => cell.checked_mul(v), + } + } +} + +fn run_effects(init: i64, effs: &[Effect]) -> Option { + effs.iter().try_fold(init, |cell, e| e.apply(cell)) +} + +fn commutes(a: &Effect, b: &Effect) -> bool { + match (*a, *b) { + (Effect::Add(x), Effect::Add(y)) => !((x < 0 && y > 0) || (x > 0 && y < 0)), + (Effect::Mul(x), Effect::Mul(y)) => { + x == y || x == 1 || y == 1 || (x.unsigned_abs() >= 2 && y.unsigned_abs() >= 2) + } + (Effect::Set(x), Effect::Set(y)) => x == y, + _ => false, + } +} + +#[derive(Debug, PartialEq, Eq)] +struct OrderRefusal { + first: usize, + second: usize, +} + +fn check_reorder(effs: &[Effect], order: &[usize]) -> Result<(), OrderRefusal> { + let n = effs.len(); + assert_eq!(order.len(), n); + let mut pos = vec![usize::MAX; n]; + for (k, &orig) in order.iter().enumerate() { + assert_eq!(pos[orig], usize::MAX, "not a permutation"); + pos[orig] = k; + } + for i in 0..n { + for j in (i + 1)..n { + if !commutes(&effs[i], &effs[j]) && pos[i] > pos[j] { + return Err(OrderRefusal { + first: i, + second: j, + }); + } + } + } + Ok(()) +} + +// ── DT stub: the meaning DR never sees ── + +const CLASS: ClassId = 7; +const OTHER_CLASS: ClassId = 8; + +/// One method as DT would hold it. DR receives only `to_ref()`. +struct DtMethod { + key: [u8; 16], + reads: u64, + writes: u64, + guard: Option<&'static str>, + effects: Vec, + algebra: Algebra, +} + +fn digest16(bytes: &[u8]) -> [u8; 16] { + let h = Sha256::digest(bytes); + let mut out = [0u8; 16]; + out.copy_from_slice(&h[..16]); + out +} + +fn effect_ref(effs: &[Effect]) -> EffectOrderRef { + let mut enc = Vec::new(); + for e in effs { + let (tag, v) = match *e { + Effect::Set(v) => (0u8, v), + Effect::Add(v) => (1u8, v), + Effect::Mul(v) => (2u8, v), + }; + enc.push(tag); + enc.extend_from_slice(&v.to_le_bytes()); + } + EffectOrderRef(digest16(&enc)) +} + +fn guard_witness(guard: &str) -> GuardWitness { + GuardWitness(digest16(guard.as_bytes())) +} + +impl DtMethod { + fn to_ref(&self, class: ClassId) -> MethodRef { + MethodRef { + class, + key: MethodKey(self.key), + signature_rev: 1, + reads: self.reads, + writes: self.writes, + guard: match self.guard { + Some(g) => GuardDecl::Required(guard_witness(g)), + None => GuardDecl::Unguarded, + }, + effects: effect_ref(&self.effects), + algebra: self.algebra, + } + } +} + +fn method(key: u8, effects: Vec, guard: Option<&'static str>) -> DtMethod { + DtMethod { + key: [key; 16], + reads: 0b0110, + writes: 0b1000, + guard, + effects, + algebra: Algebra::Presence, + } +} + +// ── register fixture ── + +fn revisions(n: u64) -> FrameRevisions { + FrameRevisions { + source: n, + relation_map: 10, + coordinates: 20, + } +} + +fn signature(truth: Truth) -> MethodSignature { + let id = Axis { + class: CLASS, + kind: AxisKind::Identity, + }; + let prop = Axis { + class: CLASS, + kind: AxisKind::Property, + }; + let mut s = MethodSignature::presence(CLASS, 3, id, prop); + s.truth = truth; + s +} + +fn rows_fixture() -> [u64; 64] { + core::array::from_fn(|x| (x as u64).wrapping_mul(0x9E37_79B9_7F4A_7C15) ^ (1 << (x % 64))) +} + +fn validity_fixture() -> [u64; 64] { + core::array::from_fn(|x| !((x as u64).wrapping_mul(0xD6E8_FEB8_6659_FD93)) | 1) +} + +const FOCUS: Focus = Focus { revision: 1 }; +const SCOPE: Scope = Scope { id: 2 }; + +fn bind<'a>( + store: &FrameStore, + truth: Truth, + rows: &'a [u64; 64], + validity: Option<&'a [u64; 64]>, +) -> BoundDr64<'a> { + let sig = signature(truth); + let guards = Guards { + frame: store.seal(), + focus: FOCUS, + scope: SCOPE, + }; + bind_dr64( + store, + sig, + sig, + &guards, + (FOCUS, SCOPE), + Operand { rows, validity }, + ) + .unwrap() +} + +fn resolution(store: &FrameStore, methods: &[&DtMethod]) -> Resolution { + Resolution { + class: CLASS, + under: store.seal(), + methods: methods.iter().map(|m| m.to_ref(CLASS)).collect(), + } +} + +/// The witnesses a caller observed, one per guarded method. +fn witnesses(methods: &[&DtMethod]) -> Vec<(MethodKey, GuardWitness)> { + methods + .iter() + .filter_map(|m| m.guard.map(|g| (MethodKey(m.key), guard_witness(g)))) + .collect() +} + +// ── 1. the falsifier ── + +#[test] +fn same_read_write_sets_different_effect_order_stay_distinct() { + let a = method(1, vec![Effect::Set(1), Effect::Add(1)], None); + let b = method(2, vec![Effect::Add(1), Effect::Set(1)], None); + // Anti-vacuity: the two methods are different by the oracle and look + // identical by everything DR could compare except their opaque refs. + assert_eq!((a.reads, a.writes), (b.reads, b.writes)); + assert_ne!(run_effects(0, &a.effects), run_effects(0, &b.effects)); + assert_eq!( + check_reorder(&a.effects, &[1, 0]), + Err(OrderRefusal { + first: 0, + second: 1 + }) + ); + + let store = FrameStore::new(revisions(1)); + let rows = rows_fixture(); + let reg = bind(&store, Truth::TwoValued, &rows, None); + let res = resolution(&store, &[&a, &b]); + let routed = route(&store, ®, &res, Op::Cell { x: 5, y: 9 }, &[]).unwrap(); + + assert_eq!(routed.entries().len(), 2); + let (ea, eb) = (&routed.entries()[0], &routed.entries()[1]); + assert_eq!(ea.key, MethodKey(a.key)); + assert_eq!(eb.key, MethodKey(b.key)); + assert_eq!(ea.effects, effect_ref(&a.effects)); + assert_eq!(eb.effects, effect_ref(&b.effects)); + assert_ne!(ea.effects, eb.effects); + assert_eq!((ea.reads, ea.writes), (eb.reads, eb.writes)); + // Same algebra over the same cell: same value, still two entries. + assert_eq!(ea.value, eb.value); + assert!(routed.frame().same_issue(®.frame)); +} + +#[test] +fn commuting_effects_are_still_not_merged() { + let a = method(1, vec![Effect::Add(2), Effect::Add(3)], None); + let b = method(2, vec![Effect::Add(3), Effect::Add(2)], None); + assert_eq!(run_effects(0, &a.effects), run_effects(0, &b.effects)); + assert_eq!(check_reorder(&a.effects, &[1, 0]), Ok(())); + // The ported law, both ways: equal-magnitude-class products commute, + // a product across a sum does not. + assert!(commutes(&Effect::Mul(2), &Effect::Mul(3))); + assert!(!commutes(&Effect::Mul(2), &Effect::Add(1))); + assert_ne!( + run_effects(1, &[Effect::Mul(2), Effect::Add(1)]), + run_effects(1, &[Effect::Add(1), Effect::Mul(2)]) + ); + + let store = FrameStore::new(revisions(1)); + let rows = rows_fixture(); + let reg = bind(&store, Truth::TwoValued, &rows, None); + let res = resolution(&store, &[&a, &b]); + let routed = route(&store, ®, &res, Op::Column { y: 3 }, &[]).unwrap(); + assert_eq!(routed.entries().len(), 2); + assert_ne!(routed.entries()[0].effects, routed.entries()[1].effects); +} + +// ── 2. guards ── + +#[test] +fn a_dropped_guard_refuses() { + let a = method(1, vec![Effect::Set(1)], Some("state == draft")); + let store = FrameStore::new(revisions(1)); + let rows = rows_fixture(); + let reg = bind(&store, Truth::TwoValued, &rows, None); + let res = resolution(&store, &[&a]); + assert_eq!( + route(&store, ®, &res, Op::Cell { x: 0, y: 0 }, &[]).err(), + Some(Dr4Refusal::GuardDropped) + ); +} + +#[test] +fn a_different_guard_witness_refuses() { + let a = method(1, vec![Effect::Set(1)], Some("state == draft")); + let store = FrameStore::new(revisions(1)); + let rows = rows_fixture(); + let reg = bind(&store, Truth::TwoValued, &rows, None); + let res = resolution(&store, &[&a]); + let wrong = [(MethodKey(a.key), guard_witness("state == posted"))]; + assert_eq!( + route(&store, ®, &res, Op::Cell { x: 0, y: 0 }, &wrong).err(), + Some(Dr4Refusal::GuardMismatch) + ); +} + +#[test] +fn the_right_guard_witness_is_carried_and_unguarded_needs_none() { + let a = method(1, vec![Effect::Set(1)], Some("state == draft")); + let b = method(2, vec![Effect::Add(1)], None); + let store = FrameStore::new(revisions(1)); + let rows = rows_fixture(); + let reg = bind(&store, Truth::TwoValued, &rows, None); + let res = resolution(&store, &[&a, &b]); + let routed = route( + &store, + ®, + &res, + Op::Cell { x: 0, y: 0 }, + &witnesses(&[&a, &b]), + ) + .unwrap(); + assert_eq!( + routed.entries()[0].guard, + Some(guard_witness("state == draft")) + ); + assert_eq!(routed.entries()[1].guard, None); +} + +// ── 3. frame, class, identity ── + +#[test] +fn a_stale_register_frame_refuses() { + let a = method(1, vec![Effect::Set(1)], None); + let mut store = FrameStore::new(revisions(1)); + let rows = rows_fixture(); + let reg = bind(&store, Truth::TwoValued, &rows, None); + let res = resolution(&store, &[&a]); + store.advance(revisions(2)); + assert_eq!( + route(&store, ®, &res, Op::Cell { x: 0, y: 0 }, &[]).err(), + Some(Dr4Refusal::Frame(Refusal::SourceChanged)) + ); +} + +#[test] +fn a_resolution_under_another_frame_refuses() { + let a = method(1, vec![Effect::Set(1)], None); + let mut store = FrameStore::new(revisions(1)); + let old = resolution(&store, &[&a]); + store.advance(revisions(2)); + let rows = rows_fixture(); + let reg = bind(&store, Truth::TwoValued, &rows, None); + assert_eq!( + route(&store, ®, &old, Op::Cell { x: 0, y: 0 }, &[]).err(), + Some(Dr4Refusal::ResolvedUnderOtherFrame) + ); + // Equal numbers in another store are another frame. + let other = FrameStore::new(revisions(2)); + let foreign = resolution(&other, &[&a]); + assert_eq!( + route(&store, ®, &foreign, Op::Cell { x: 0, y: 0 }, &[]).err(), + Some(Dr4Refusal::ResolvedUnderOtherFrame) + ); +} + +#[test] +fn a_foreign_class_refuses() { + let a = method(1, vec![Effect::Set(1)], None); + let store = FrameStore::new(revisions(1)); + let rows = rows_fixture(); + let reg = bind(&store, Truth::TwoValued, &rows, None); + let mut res = resolution(&store, &[&a]); + res.class = OTHER_CLASS; + assert_eq!( + route(&store, ®, &res, Op::Cell { x: 0, y: 0 }, &[]).err(), + Some(Dr4Refusal::ForeignClass) + ); + let mut res = resolution(&store, &[&a]); + res.methods[0].class = OTHER_CLASS; + assert_eq!( + route(&store, ®, &res, Op::Cell { x: 0, y: 0 }, &[]).err(), + Some(Dr4Refusal::ForeignClass) + ); +} + +#[test] +fn a_duplicate_key_refuses_but_equal_sets_do_not() { + let a = method(1, vec![Effect::Set(1)], None); + let a2 = method(1, vec![Effect::Add(1)], None); + let store = FrameStore::new(revisions(1)); + let rows = rows_fixture(); + let reg = bind(&store, Truth::TwoValued, &rows, None); + let res = resolution(&store, &[&a, &a2]); + assert_eq!( + route(&store, ®, &res, Op::Cell { x: 0, y: 0 }, &[]).err(), + Some(Dr4Refusal::DuplicateMethod) + ); +} + +#[test] +fn out_of_register_and_unsupported_algebra_refuse() { + let mut a = method(1, vec![Effect::Set(1)], None); + let store = FrameStore::new(revisions(1)); + let rows = rows_fixture(); + let reg = bind(&store, Truth::TwoValued, &rows, None); + let res = resolution(&store, &[&a]); + assert_eq!( + route(&store, ®, &res, Op::Cell { x: 64, y: 0 }, &[]).err(), + Some(Dr4Refusal::OutOfRegister) + ); + assert_eq!( + route(&store, ®, &res, Op::Column { y: 64 }, &[]).err(), + Some(Dr4Refusal::OutOfRegister) + ); + a.algebra = Algebra::NumericFold; + let res = resolution(&store, &[&a]); + assert_eq!( + route(&store, ®, &res, Op::Cell { x: 0, y: 0 }, &[]).err(), + Some(Dr4Refusal::UnsupportedAlgebra) + ); +} + +// ── 4. values against an independent scalar loop ── + +fn bit(rows: &[u64; 64], x: usize, y: usize) -> bool { + (rows[x] >> y) & 1 == 1 +} + +#[test] +fn boolean_values_match_the_scalar_oracle() { + let a = method(1, vec![Effect::Set(1)], None); + let store = FrameStore::new(revisions(1)); + let rows = rows_fixture(); + let reg = bind(&store, Truth::TwoValued, &rows, None); + let res = resolution(&store, &[&a]); + let mut seen = (false, false); + for x in 0..64u8 { + for y in [0u8, 1, 31, 63] { + let v = route(&store, ®, &res, Op::Cell { x, y }, &[]).unwrap(); + let want = bit(&rows, x as usize, y as usize); + assert_eq!(v.entries()[0].value, Value::Bool(want), "cell {x},{y}"); + if want { + seen.0 = true; + } else { + seen.1 = true; + } + } + let r = route(&store, ®, &res, Op::Row { x }, &[]).unwrap(); + assert_eq!(r.entries()[0].value, Value::Mask(rows[x as usize])); + } + assert!(seen.0 && seen.1, "fixture has no TRUE or no FALSE cell"); + for y in 0..64u8 { + let want = (0..64).fold(0u64, |m, x| m | (u64::from(bit(&rows, x, y as usize)) << x)); + let c = route(&store, ®, &res, Op::Column { y }, &[]).unwrap(); + assert_eq!(c.entries()[0].value, Value::Mask(want), "column {y}"); + } +} + +#[test] +fn presence_over_three_valued_refuses_and_k3_masks_by_validity() { + let mut a = method(1, vec![Effect::Set(1)], None); + let store = FrameStore::new(revisions(1)); + let rows = rows_fixture(); + let validity = validity_fixture(); + let reg = bind(&store, Truth::ThreeValued, &rows, Some(&validity)); + let res = resolution(&store, &[&a]); + assert_eq!( + route(&store, ®, &res, Op::Column { y: 2 }, &[]).err(), + Some(Dr4Refusal::NotBoolean) + ); + a.algebra = Algebra::PresenceK3; + let res = resolution(&store, &[&a]); + let mut unknown_true_payload = false; + for y in 0..64u8 { + let (mut value, mut known) = (0u64, 0u64); + for x in 0..64 { + let k = bit(&validity, x, y as usize); + let v = bit(&rows, x, y as usize); + known |= u64::from(k) << x; + value |= u64::from(k && v) << x; + unknown_true_payload |= !k && v; + } + let c = route(&store, ®, &res, Op::Column { y }, &[]).unwrap(); + assert_eq!( + c.entries()[0].value, + Value::K3 { value, known }, + "column {y}" + ); + } + // Anti-vacuity: some UNKNOWN cell carries a 1 payload bit that must not + // read as TRUE. + assert!(unknown_true_payload); + // A two-valued register under K3 is known everywhere. + let reg2 = bind(&store, Truth::TwoValued, &rows, None); + let c = route(&store, ®2, &res, Op::Row { x: 4 }, &[]).unwrap(); + assert_eq!( + c.entries()[0].value, + Value::K3 { + value: rows[4], + known: u64::MAX + } + ); +}