diff --git a/.claude/board/entries/2026-10-08-ce64-isa-register-contract.md b/.claude/board/entries/2026-10-08-ce64-isa-register-contract.md new file mode 100644 index 000000000..2a2ee7573 --- /dev/null +++ b/.claude/board/entries/2026-10-08-ce64-isa-register-contract.md @@ -0,0 +1,93 @@ +# 2026-10-08 — CE64 ISA: strict decoder, register methods, field contracts + +**Status:** TEST-PINNED. Reasoning chooses the operation; `CausalEdge64` +defines what that operation means. + +Code: `crates/causal-edge/src/isa.rs` (new), `edge.rs`, `syllogism.rs`, +`network.rs`. Tests: `crates/causal-edge/tests/ce64_isa_contract.rs`, +`ce64_isa_golden.rs` (+ `ce64_legacy_capture.txt`), `ce64_op_contract.rs`; +`crates/lance-graph-planner/tests/gadamer_isa_revision.rs`; the MooreNars16 +probe (#1406) now compares `Result`s and draws executable inference codes. + +## What changed + +- **Strict decoder.** Of the 16 inference codes, exactly `+1` Deduction, + `+2` Induction, `-1` Abduction, `+4` Revision, `+5` Synthesis execute + (`Opcode::decode`). The other 11 (`0`, `-8`, `-2`, `±3`, `-4`, `-5`, + `±6`, `±7`) return `IsaFault::Unsupported { mantissa }`. Before, `±6` and + `±7` ran the Synthesis mean and came back stamped `±6` and `7`; `0`, `-8`, + `-2`, `±3`, `-4`, `-5` ran another instruction and came back stamped with + that instruction's code. +- **`forward` only dispatches**: decode, then `execute(op, ..)`. It now + returns `Result`; so do `forward_chain`, `NarsEngine::forward_edge` and + `replay_step` (`ReplayError::Isa`). +- **Register methods**: `deduction`, `induction`, `abduction`, `synthesis` + take an explicit `Compose` (S/P/O payload algebra) and return `Self`; + `revision(rhs)` is truth-only (writes F, C; keeps every other field of + `self`; no `Compose`); `counterfactual` and `intervention` are partial and + always refuse. +- **One truth function per instruction** (`isa::truth`); `forward`, `learn` + and `syllogize` delegate. The three previous copies are gone. +- **Field contracts** (`isa::contracts`): reads / computes / passes / + constants, payload algebra, failure condition, measured by perturbation in + `ce64_isa_contract.rs`. + +## Field-liveness matrix + +| instruction | computes | passes through | constant | Compose | fails | +|---|---|---|---|---|---| +| forward / `execute` | S/P/O, F, C, Pearl (AND) | inference ← B, Direction ← B, Plasticity ← B | W = 0, Epi5 = 0 | yes | B's code has no implementation | +| `revision` | F, C | everything else ← A | — | no | never | +| `learn` | S/P/O, F, C, Plasticity | Pearl, Direction, inference, W, Epi5 ← A | — | no | never | +| `syllogize` | S/P/O, F, C, Pearl, inference | — | Direction 0, Plasticity 0b111, W 0, Epi5 0 | no | `None` without a figure | + +The W/Epi5 zeroing in `forward` and `syllogize` is legacy behaviour, now +DECLARED, not changed. + +## Golden vectors + +- Legacy capture: 126 raw-word vectors recorded from the pre-ISA code. 71 + reproduce bit for bit; the 55 whose weight carries an unsupported code + now refuse with that code. Nothing else moved. +- Normative: 23 forward vectors through the named methods, checked against + an independent f64 reference (±1 on F/C) and the declared contract. + +## The max-confidence revision defect (not normative) + +`revision(c=255, c=255)` returns `f = c = 0`, in `forward`, `revision` and +`learn`. Path: `c = 1.0 >= 0.999` → `evidence_weight = f32::MAX` for both → +`ws = MAX + MAX = +inf` → `f = inf/inf = NaN`, `c = NaN` → the float-to-u8 +cast saturates NaN to 0. Not a u8 overflow, LUT bin, or zero-denominator +fallback. Also: ONE operand at 255 is finite but dominates (its weight is +`f32::MAX`), where the capped reference gives a weighted mean. Both kept +out of the normative set and pinned. + +## Gadamer stays above + +`GadamerRevision` decides whether evidence is admitted; `revision` only +computes. Ten echo or closed-cycle encounters leave confidence unchanged +because the gate never calls the register; ten new roots raise it. The +register alone would inflate an echo (pinned). + +## Disable runs (anchor asserted, each red) + +CF decoded as Synthesis (6 tests) · forward ignores the decoded op (4) · +learn clears W (4) · revision clears Epi5 (1) · diverging revision formula +(4) · known-bad promoted to normative (2) · a policy type named in `isa.rs` +(1) · `counterfactual` computes (1) · Gadamer gate bypassed (2). + +## OPEN + +- `forward`'s revision step (+4) composes payload; `revision(rhs)` does + not. Whether a payload-composing revision step should exist is a + decision, not made here. +- The c = 255 saturation rule (collapse and dominance). Smallest fix: cap + `c` before `evidence_weight` as the f64 reference does. +- `forward` writes the executed code into the result's bits 46..49. The + transition-loop reading ("do not whisper the operation back into the + result edge") says it should not. Pre-existing; not changed here. +- `learn` mixes arithmetic (revision) with policy (archetype reassignment, + freeze thresholds 0.9 / 0.7). Named split, not done. +- `syllogize` chooses the rule from the figure (a choice) and computes it. +- Planner truth copies outside the CE64 register (`TruthValue`, + `nars_infer`, `NarsTables`) still differ; out of scope. diff --git a/.claude/board/entries/README.md b/.claude/board/entries/README.md index 5bf0f170a..d7fa07dc1 100644 --- a/.claude/board/entries/README.md +++ b/.claude/board/entries/README.md @@ -25,7 +25,7 @@ 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. -268 entries, 2026-08-06 .. 2026-10-08. +269 entries, 2026-08-06 .. 2026-10-08. | date | entry id | finding | file | |---|---|---|---| @@ -35,6 +35,7 @@ exactly one of them, never both. | 2026-10-08 | `moore-nars16-isa-visible-representation` | | [2026-10-08-moore-nars16-isa-visible-representation.md](2026-10-08-moore-nars16-isa-visible-representation.md) | | 2026-10-08 | `D-MOORE-NARS-0` | | [2026-10-08-moore-nars-0-recipe-learning-gomoku.md](2026-10-08-moore-nars-0-recipe-learning-gomoku.md) | | 2026-10-08 | `coresearch-ce64-moore-masking-wiring` | | [2026-10-08-coresearch-ce64-moore-masking-wiring.md](2026-10-08-coresearch-ce64-moore-masking-wiring.md) | +| 2026-10-08 | `ce64-isa-register-contract` | | [2026-10-08-ce64-isa-register-contract.md](2026-10-08-ce64-isa-register-contract.md) | | 2026-10-07 | `tinker-janus-fold-harvest` | TinkerPop bulk = K (GroupReduce), ONE_BULK = S, GValue pinning = bundle invalidation; JanusGraph slice = OrderedLaneWitness→Range (30–38×); no new V4 op | [2026-10-07-tinker-janus-fold-harvest.md](2026-10-07-tinker-janus-fold-harvest.md) | | 2026-10-07 | `selector-seq-aware-coverage` | | [2026-10-07-selector-seq-aware-coverage.md](2026-10-07-selector-seq-aware-coverage.md) | | 2026-10-07 | `D-PUZZLE-ATTN-0` | | [2026-10-07-puzzle-attn-0-entropy-attention-crosswords.md](2026-10-07-puzzle-attn-0-entropy-attention-crosswords.md) | diff --git a/crates/causal-edge/src/edge.rs b/crates/causal-edge/src/edge.rs index 9af601d3c..d6a3ef2e7 100644 --- a/crates/causal-edge/src/edge.rs +++ b/crates/causal-edge/src/edge.rs @@ -4,6 +4,7 @@ use super::pearl::CausalMask; use super::plasticity::PlasticityState; +use crate::isa::{Compose, IsaFault, Opcode}; /// NARS inference types encoded in 3 bits. #[derive(Debug, Clone, Copy, PartialEq, Eq)] @@ -62,7 +63,7 @@ impl InferenceType { /// 6=Intervention(+)/Counterfactual(-) [PR-LL-1 absorbed per L-9], /// 7=Extension(+)/Intension-negative(-) [future]. #[inline] - pub fn to_mantissa(self) -> i8 { + pub const fn to_mantissa(self) -> i8 { match self { // Forward-chain (positive mantissa) Self::Deduction => 1, @@ -350,12 +351,7 @@ impl CausalEdge64 { /// Evidence weight: c / (1 - c). Returns u16::MAX if c == 255. #[inline] pub fn evidence_weight(self) -> f32 { - let c = self.confidence(); - if c >= 0.999 { - f32::MAX - } else { - c / (1.0 - c) - } + crate::isa::truth::evidence_weight(self.confidence()) } /// Set frequency (u8). @@ -657,10 +653,17 @@ impl CausalEdge64 { // ─── Forward Pass (BNN-style) ─────────────────────────────────── - /// The forward pass: compose palettes + propagate truth + propagate causality. + /// The forward pass: decode `weight`'s inference code, then execute + /// exactly that instruction (`self.deduction(weight, ..)` and so on). + /// + /// Decoding is strict ([`Opcode::decode`]): a code with no implementation + /// (counterfactual, intervention, the reserved values) is an + /// [`IsaFault`], never executed as another instruction. The field + /// contract is [`contracts::FORWARD`](crate::isa::contracts::FORWARD). /// - /// This IS the "neural network inference" — but every intermediate is - /// a CausalEdge64 with full interpretability. + /// # Errors + /// + /// [`IsaFault::Unsupported`] when `weight` carries an unexecutable code. #[inline] pub fn forward( self, @@ -668,72 +671,133 @@ impl CausalEdge64 { compose_s: &[u8; 256 * 256], compose_p: &[u8; 256 * 256], compose_o: &[u8; 256 * 256], - ) -> Self { - // 1. Palette composition (the "multiply") - let s_out = compose_s[self.s_idx() as usize * 256 + weight.s_idx() as usize]; - let p_out = compose_p[self.p_idx() as usize * 256 + weight.p_idx() as usize]; - let o_out = compose_o[self.o_idx() as usize * 256 + weight.o_idx() as usize]; - - // 2. NARS truth propagation (the "activation function") - // Under v2: decode the 4-bit signed mantissa (bits 46-49) and route - // through the same InferenceType variants. Without this, v2 edges - // built via `with_inference_mantissa()` route as 3-bit unsigned - // (e.g. -1 = 0b1111 reads as Reserved7), bypassing Abduction/ - // Counterfactual semantics entirely. + ) -> Result { #[cfg(feature = "causal-edge-v2-layout")] - #[allow(deprecated)] - // weight.inference_type() is the v1 fallback below; v2 uses mantissa - let resolved_infer = InferenceType::from_mantissa(weight.inference_mantissa()); + let op = Opcode::decode(weight.inference_mantissa())?; #[cfg(not(feature = "causal-edge-v2-layout"))] - #[allow(deprecated)] - // v1 layout: 3-bit unsigned inference type is the canonical read - let resolved_infer = weight.inference_type(); - let (f_out, c_out) = match resolved_infer { - InferenceType::Deduction => { - let f = self.frequency() * weight.frequency(); - let c = f * self.confidence() * weight.confidence(); - (f, c) - } - InferenceType::Induction => { - let f = weight.frequency(); - let w = self.frequency() * self.confidence() * weight.confidence(); - (f, w / (w + 1.0)) - } - InferenceType::Abduction => { - let f = self.frequency(); - let w = weight.frequency() * self.confidence() * weight.confidence(); - (f, w / (w + 1.0)) - } - InferenceType::Revision => { - let w1 = self.evidence_weight(); - let w2 = weight.evidence_weight(); - let ws = w1 + w2; - if ws < f32::EPSILON { - (0.5, 0.0) - } else { - let f = (self.frequency() * w1 + weight.frequency() * w2) / ws; - let c = ws / (ws + 1.0); - (f, c) - } - } - InferenceType::Synthesis | _ => { - let f = (self.frequency() + weight.frequency()) / 2.0; - let c = (self.confidence() + weight.confidence()) / 2.0; - (f, c) - } - }; + #[allow(deprecated)] // v1 layout: the 3-bit code is the canonical read + let op = Opcode::decode_v1(weight.inference_type())?; + Ok(self.execute( + op, + weight, + Compose { + s: compose_s, + p: compose_p, + o: compose_o, + }, + )) + } + + /// Deduction with `rhs` as the second premise. See [`execute`](Self::execute). + #[inline] + #[must_use] + pub fn deduction(self, rhs: Self, compose: Compose<'_>) -> Self { + self.execute(Opcode::Deduction, rhs, compose) + } + + /// Induction with `rhs` as the second premise. See [`execute`](Self::execute). + #[inline] + #[must_use] + pub fn induction(self, rhs: Self, compose: Compose<'_>) -> Self { + self.execute(Opcode::Induction, rhs, compose) + } + + /// Abduction with `rhs` as the second premise. See [`execute`](Self::execute). + #[inline] + #[must_use] + pub fn abduction(self, rhs: Self, compose: Compose<'_>) -> Self { + self.execute(Opcode::Abduction, rhs, compose) + } + + /// NARS revision: pool the evidence of `self` and `rhs` for the same + /// statement. Truth arithmetic only: writes frequency and confidence, + /// keeps every other field of `self`, needs no payload algebra + /// ([`contracts::REVISION`](crate::isa::contracts::REVISION)). + /// + /// With no evidence on either side the result is unknown, `(0.5, 0.0)`. + /// Whether two edges are independent enough to pool is the caller's + /// decision (a reasoning policy, such as a Gadamer-style revision gate), + /// never this method's. + #[inline] + #[must_use] + pub fn revision(self, rhs: Self) -> Self { + let (f, c) = Opcode::Revision.truth( + self.frequency(), + self.confidence(), + rhs.frequency(), + rhs.confidence(), + ); + let mut out = self; + out.set_frequency(f); + out.set_confidence(c); + out + } + + /// Synthesis (component-wise mean) with `rhs`. See [`execute`](Self::execute). + #[inline] + #[must_use] + pub fn synthesis(self, rhs: Self, compose: Compose<'_>) -> Self { + self.execute(Opcode::Synthesis, rhs, compose) + } + + /// Counterfactual. Partial; no implementation exists yet, so it always + /// refuses. It never runs another instruction in its place. + /// + /// # Errors + /// + /// Always [`IsaFault::Unsupported`] with the counterfactual code in the + /// active layout (`-6` in v2, `6` in v1); see [`IsaFault::unsupported`]. + #[inline] + pub fn counterfactual(self, _rhs: Self, _compose: Compose<'_>) -> Result { + Err(IsaFault::unsupported(InferenceType::Counterfactual)) + } + + /// Intervention. Partial; no implementation exists yet, so it always + /// refuses. + /// + /// # Errors + /// + /// Always [`IsaFault::Unsupported`] with the intervention code in the + /// active layout (`+6` in v2, `5` in v1); see [`IsaFault::unsupported`]. + #[inline] + pub fn intervention(self, _rhs: Self, _compose: Compose<'_>) -> Result { + Err(IsaFault::unsupported(InferenceType::Intervention)) + } + + /// Execute one chain step under `op` on `(self, rhs)`: what `forward` + /// runs after decoding the weight's code. + /// + /// - S/P/O: composed per plane through `compose`; + /// - truth: `op`'s canonical truth function ([`Opcode::truth`]); + /// - Pearl mask: AND of both operands; + /// - inference field: `op`'s own encoding; + /// - direction and plasticity: passed through from `rhs`; + /// - witness and epistemic state: written 0. + /// + /// No policy: the caller has already chosen the operands and the + /// instruction. + #[inline] + #[must_use] + pub fn execute(self, op: Opcode, rhs: Self, compose: Compose<'_>) -> Self { + let s_out = compose.s[self.s_idx() as usize * 256 + rhs.s_idx() as usize]; + let p_out = compose.p[self.p_idx() as usize * 256 + rhs.p_idx() as usize]; + let o_out = compose.o[self.o_idx() as usize * 256 + rhs.o_idx() as usize]; + + let (f_out, c_out) = op.truth( + self.frequency(), + self.confidence(), + rhs.frequency(), + rhs.confidence(), + ); - // 3. Causal mask: AND (only planes active in BOTH survive) let mask_out = - CausalMask::from_bits((self.causal_mask() as u8) & (weight.causal_mask() as u8)); + CausalMask::from_bits((self.causal_mask() as u8) & (rhs.causal_mask() as u8)); - // 4. Temporal: latest of the two (v1 read; the pack() below drops it under v2) + // Temporal: latest of the two (v1; `pack` ignores it under v2). #[allow(deprecated)] - let t_out = self.temporal().max(weight.temporal()); + let t_out = self.temporal().max(rhs.temporal()); - // 5. Inherit plasticity from weight (the "learned" edge) - // and direction will be recomputed from composed palette entries - #[allow(deprecated)] // pack() v2 path drops temporal; resolved_infer carries v2 mantissa + #[allow(deprecated)] // v2 `pack` ignores temporal let result = Self::pack( s_out, p_out, @@ -741,17 +805,15 @@ impl CausalEdge64 { (f_out.clamp(0.0, 1.0) * 255.0).round() as u8, (c_out.clamp(0.0, 1.0) * 255.0).round() as u8, mask_out, - weight.direction(), // TODO: recompute from composed palette dim0 signs - resolved_infer, - weight.plasticity(), + rhs.direction(), // TODO: recompute from composed palette dim0 signs + op.inference_type(), + rhs.plasticity(), t_out, ); - // Under v2: re-stamp the signed mantissa onto the result. pack() only - // writes 3 bits (v1 enum discriminant) into bits 46-48; bit 49 (the - // sign bit) stays 0, so negative mantissas (Abduction, Counterfactual) - // would lose their sign. Override here with the resolved value. + // Under v2 the inference field holds the signed code; `pack` writes the + // 3-bit enum discriminant. #[cfg(feature = "causal-edge-v2-layout")] - let result = result.with_inference_mantissa(resolved_infer.to_mantissa()); + let result = result.with_inference_mantissa(op.encoding()); result } @@ -785,13 +847,13 @@ impl CausalEdge64 { } } - // NARS revision: merge evidence - let w1 = self.evidence_weight(); - let w2 = observation.evidence_weight(); - let ws = w1 + w2; - if ws > f32::EPSILON { - let f_new = (self.frequency() * w1 + observation.frequency() * w2) / ws; - let c_new = ws / (ws + 1.0); + // NARS revision: merge evidence (the canonical truth function). + if let Some((f_new, c_new)) = crate::isa::truth::revision( + self.frequency(), + self.confidence(), + observation.frequency(), + observation.confidence(), + ) { self.set_frequency(f_new); self.set_confidence(c_new); @@ -1433,7 +1495,9 @@ mod tests { // Dummy compose tables (identity for test) let compose = [0u8; 256 * 256]; - let result = input.forward(weight, &compose, &compose, &compose); + let result = input + .forward(weight, &compose, &compose, &compose) + .expect("deduction weight"); // Deduction: f_out = f_in * f_w ≈ 0.80 * 0.90 = 0.72 assert!( diff --git a/crates/causal-edge/src/isa.rs b/crates/causal-edge/src/isa.rs new file mode 100644 index 000000000..ff35b7f22 --- /dev/null +++ b/crates/causal-edge/src/isa.rs @@ -0,0 +1,507 @@ +//! The CE64 instruction set. +//! +//! `CausalEdge64` is the register; this module is the decoder and the +//! semantics. Three rules hold here and nowhere else: +//! +//! 1. **The decoder is strict.** The 4-bit inference field holds 16 values, +//! but only five of them name an instruction this crate implements +//! ([`Opcode::decode`]). Every other value is [`IsaFault::Unsupported`]: +//! it is never executed as some other instruction and re-stamped with its +//! own code afterwards. In particular Counterfactual (`-6`), +//! Intervention (`+6`) and the reserved `±7` fault until each has an +//! implementation of its own. +//! 2. **One truth function per instruction** ([`truth`]). `forward`, `learn` +//! and `syllogize` all call these; none carries its own formula. +//! 3. **Every instruction declares its field contract** ([`Contract`]): which +//! operand fields it reads, which output fields it computes, which it +//! passes through unchanged from an operand, and which it overwrites with a +//! constant. `tests/ce64_isa_contract.rs` measures each declaration. +//! +//! ## Total and partial instructions +//! +//! - **Total**: every valid operand pair has a defined result. The five +//! [`Opcode`]s are total; their register methods return `Self`. +//! `deduction`, `induction`, `abduction` and `synthesis` compose the payload +//! through a [`Compose`] algebra; `revision` is truth-only and needs none. +//! - **Partial**: the instruction has preconditions; a violation returns an +//! [`IsaFault`]. `CausalEdge64::counterfactual` and `::intervention` are +//! partial with a precondition no operand satisfies yet (no implementation), +//! so they always fault. They exist so the slot is visible and so a caller +//! that names them gets a refusal, never another instruction. +//! +//! ## Layers +//! +//! - **Instruction** (this module and the register methods): truth arithmetic +//! and field transitions. +//! - **[`Compose`]**: the payload algebra for S/P/O. It never selects an +//! opcode or sees any reasoning state. +//! - **Reasoning** (recipes, planner, revision policies such as Gadamer's): +//! chooses operands, instruction, order, admissibility and when to stop. +//! It lives above this crate. +//! +//! The register space is larger than the decoder on purpose. A value written +//! by a producer the ISA does not execute (a counterfactual tag, a lens +//! reading) stays representable; it just cannot be executed. + +use crate::edge::InferenceType; + +/// An executable CE64 instruction. +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] +pub enum Opcode { + /// `A->B, B->C ⊢ A->C`. + Deduction, + /// `A->B, A->C ⊢ B->C`. + Induction, + /// `A->B, C->B ⊢ A->C`. + Abduction, + /// Pool two bodies of evidence for the same statement. + Revision, + /// Arithmetic mean of frequency and of confidence. + Synthesis, +} + +/// The payload algebra an instruction composes S, P and O through: one +/// 256 x 256 table per plane, indexed `lhs * 256 + rhs`. +/// +/// The ISA does not interpret the payload bytes itself; the caller declares +/// what they mean by the tables it passes. +#[derive(Debug, Clone, Copy)] +pub struct Compose<'a> { + /// S-plane composition. + pub s: &'a [u8; 256 * 256], + /// P-plane composition. + pub p: &'a [u8; 256 * 256], + /// O-plane composition. + pub o: &'a [u8; 256 * 256], +} + +/// A register value the ISA does not execute. +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] +pub enum IsaFault { + /// The inference field holds a code with no implementation here. + Unsupported { + /// The signed 4-bit value as stored (v1 layout: the 3-bit code). + mantissa: i8, + }, +} + +impl IsaFault { + /// The fault for an inference code the ISA does not execute, carrying the + /// code as the active layout encodes it: the signed v2 mantissa + /// (Counterfactual `-6`, Intervention `+6`) or the unsigned v1 3-bit value + /// (Intervention `5`, Counterfactual `6`). `forward` and the direct + /// partial methods both build their faults here, so the same instruction + /// always reports the same code. + #[inline] + pub const fn unsupported(code: InferenceType) -> Self { + #[cfg(feature = "causal-edge-v2-layout")] + let mantissa = code.to_mantissa(); + #[cfg(not(feature = "causal-edge-v2-layout"))] + let mantissa = code as i8; + IsaFault::Unsupported { mantissa } + } +} + +impl core::fmt::Display for IsaFault { + fn fmt(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result { + match self { + IsaFault::Unsupported { mantissa } => { + write!( + f, + "CE64 ISA: inference code {mantissa} has no implementation" + ) + } + } + } +} + +impl std::error::Error for IsaFault {} + +impl Opcode { + /// Every executable instruction. + pub const ALL: [Opcode; 5] = [ + Opcode::Deduction, + Opcode::Induction, + Opcode::Abduction, + Opcode::Revision, + Opcode::Synthesis, + ]; + + /// The signed v2 inference code this instruction is stored as. + #[inline] + pub const fn encoding(self) -> i8 { + match self { + Opcode::Deduction => 1, + Opcode::Induction => 2, + Opcode::Abduction => -1, + Opcode::Revision => 4, + Opcode::Synthesis => 5, + } + } + + /// Strict v2 decode: exactly the five encodings above execute. + /// + /// `0` (neutral), `-8`, `-2` (contraposition), `±3` (exemplification / + /// negative analogy), `-4`, `-5` (decomposition), `±6` (intervention / + /// counterfactual) and `±7` have no implementation and fault. + /// [`InferenceType::from_mantissa`] still maps all 16 values to its + /// nearest variant; that is a reading for display, not a decoder. + #[inline] + pub const fn decode(mantissa: i8) -> Result { + match mantissa { + 1 => Ok(Opcode::Deduction), + 2 => Ok(Opcode::Induction), + -1 => Ok(Opcode::Abduction), + 4 => Ok(Opcode::Revision), + 5 => Ok(Opcode::Synthesis), + m => Err(IsaFault::Unsupported { mantissa: m }), + } + } + + /// Strict decode of the v1 3-bit code (Deduction..Synthesis are 0..4). + #[inline] + pub const fn decode_v1(code: InferenceType) -> Result { + match code { + InferenceType::Deduction => Ok(Opcode::Deduction), + InferenceType::Induction => Ok(Opcode::Induction), + InferenceType::Abduction => Ok(Opcode::Abduction), + InferenceType::Revision => Ok(Opcode::Revision), + InferenceType::Synthesis => Ok(Opcode::Synthesis), + other => Err(IsaFault::unsupported(other)), + } + } + + /// The `InferenceType` this instruction is. + #[inline] + pub const fn inference_type(self) -> InferenceType { + match self { + Opcode::Deduction => InferenceType::Deduction, + Opcode::Induction => InferenceType::Induction, + Opcode::Abduction => InferenceType::Abduction, + Opcode::Revision => InferenceType::Revision, + Opcode::Synthesis => InferenceType::Synthesis, + } + } + + /// The canonical truth function of this instruction, on `(f, c)` pairs. + /// + /// Revision with no evidence on either side returns `(0.5, 0.0)` + /// (unknown); [`truth::revision`] reports that case as `None` for callers + /// that must leave their state untouched instead. + #[inline] + pub fn truth(self, f1: f32, c1: f32, f2: f32, c2: f32) -> (f32, f32) { + match self { + Opcode::Deduction => truth::deduction(f1, c1, f2, c2), + Opcode::Induction => truth::induction(f1, c1, f2, c2), + Opcode::Abduction => truth::abduction(f1, c1, f2, c2), + Opcode::Revision => truth::revision(f1, c1, f2, c2).unwrap_or((0.5, 0.0)), + Opcode::Synthesis => truth::synthesis(f1, c1, f2, c2), + } + } +} + +/// The canonical NARS truth functions (evidence horizon `k = 1`). +/// +/// These are the only formulas in this crate. The arithmetic and its order +/// are exactly what `forward`, `learn` and `syllogize` computed inline before +/// they delegated here, so every packed result is bit-identical. +pub mod truth { + /// Evidence weight `w = c / (1 - c)`, saturating to `f32::MAX` at + /// `c >= 0.999`. + /// + /// Known defect, pinned in `tests/ce64_isa_golden.rs`: when BOTH operands + /// of a revision saturate, the pooled weight overflows to infinity and the + /// result is `NaN`, which packs as `f = c = 0`. + #[inline] + pub fn evidence_weight(c: f32) -> f32 { + if c >= 0.999 { + f32::MAX + } else { + c / (1.0 - c) + } + } + + /// Deduction: `f = f1·f2`, `c = f1·f2·c1·c2`. + #[inline] + pub fn deduction(f1: f32, c1: f32, f2: f32, c2: f32) -> (f32, f32) { + let f = f1 * f2; + (f, f * c1 * c2) + } + + /// Induction: `f = f2`, `c = w/(w+1)` with `w = f1·c1·c2`. + #[inline] + pub fn induction(f1: f32, c1: f32, f2: f32, c2: f32) -> (f32, f32) { + let w = f1 * c1 * c2; + (f2, w / (w + 1.0)) + } + + /// Abduction: `f = f1`, `c = w/(w+1)` with `w = f2·c1·c2`. + #[inline] + pub fn abduction(f1: f32, c1: f32, f2: f32, c2: f32) -> (f32, f32) { + let w = f2 * c1 * c2; + (f1, w / (w + 1.0)) + } + + /// Revision: pool the evidence weights. `None` when neither side carries + /// evidence. + /// + /// The threshold is `ws > f32::EPSILON`. For confidences decoded from a + /// `u8` the smallest non-zero weight is `(1/255)/(254/255) ≈ 0.0039`, so + /// `ws` is either exactly 0 or far above the threshold. + #[inline] + pub fn revision(f1: f32, c1: f32, f2: f32, c2: f32) -> Option<(f32, f32)> { + let w1 = evidence_weight(c1); + let w2 = evidence_weight(c2); + let ws = w1 + w2; + if ws > f32::EPSILON { + Some(((f1 * w1 + f2 * w2) / ws, ws / (ws + 1.0))) + } else { + None + } + } + + /// Synthesis: the mean of each component. Not a NARS rule. + #[inline] + pub fn synthesis(f1: f32, c1: f32, f2: f32, c2: f32) -> (f32, f32) { + ((f1 + f2) / 2.0, (c1 + c2) / 2.0) + } +} + +/// A CE64 field, v2 layout. +#[cfg(feature = "causal-edge-v2-layout")] +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] +pub enum Field { + /// Bits 0..23: the S, P, O payload. + Spo, + /// Bits 24..31. + Frequency, + /// Bits 32..39. + Confidence, + /// Bits 40..42. + Pearl, + /// Bits 43..45: the S/P/O sign triple. + Direction, + /// Bits 46..49: the inference code. + Inference, + /// Bits 50..52. + Plasticity, + /// Bits 53..58. + Witness, + /// Bits 59..63. + Epistemic, +} + +#[cfg(feature = "causal-edge-v2-layout")] +impl Field { + /// Every field, in bit order. Together they cover all 64 bits once. + pub const ALL: [Field; 9] = [ + Field::Spo, + Field::Frequency, + Field::Confidence, + Field::Pearl, + Field::Direction, + Field::Inference, + Field::Plasticity, + Field::Witness, + Field::Epistemic, + ]; + + /// `(shift, width)`. + pub const fn span(self) -> (u32, u32) { + match self { + Field::Spo => (0, 24), + Field::Frequency => (24, 8), + Field::Confidence => (32, 8), + Field::Pearl => (40, 3), + Field::Direction => (43, 3), + Field::Inference => (46, 4), + Field::Plasticity => (50, 3), + Field::Witness => (53, 6), + Field::Epistemic => (59, 5), + } + } + + /// The field's bits in place. + pub const fn mask(self) -> u64 { + let (s, w) = self.span(); + ((1u64 << w) - 1) << s + } + + /// The field's value. + pub const fn get(self, word: u64) -> u64 { + (word & self.mask()) >> self.span().0 + } +} + +/// Which operand a field comes from. +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] +pub enum Operand { + /// The receiver: `forward`'s running edge, `learn`'s self, `syllogize`'s + /// first premise. + A, + /// The argument: `forward`'s weight, `learn`'s observation, `syllogize`'s + /// second premise. + B, +} + +/// What one instruction does to each field. +/// +/// Every output field appears in exactly one of `computes`, `passes` and +/// `constants`. +#[cfg(feature = "causal-edge-v2-layout")] +#[derive(Debug, Clone, Copy)] +pub struct Contract { + /// The instruction. + pub name: &'static str, + /// Operand fields that influence an output other than by passing through. + pub reads: &'static [(Operand, Field)], + /// Output fields computed from the reads. + pub computes: &'static [Field], + /// Output fields copied unchanged from one operand. + pub passes: &'static [(Field, Operand)], + /// Output fields overwritten with a constant, whatever the operands hold. + pub constants: &'static [(Field, u64)], + /// Whether the instruction composes S/P/O through a [`Compose`] algebra. + pub needs_compose: bool, + /// When the instruction refuses. + pub fails: &'static str, +} + +#[cfg(feature = "causal-edge-v2-layout")] +pub mod contracts { + //! The declared contracts, one per instruction. + use super::{Contract, Field::*, Operand::*}; + + /// `a.forward(b)`. The instruction comes from `b`'s inference field; + /// `a`'s is ignored. The output's inference field is `b`'s, unchanged. + pub const FORWARD: Contract = Contract { + name: "forward", + reads: &[ + (A, Spo), + (A, Frequency), + (A, Confidence), + (A, Pearl), + (B, Spo), + (B, Frequency), + (B, Confidence), + (B, Pearl), + (B, Inference), + ], + computes: &[Spo, Frequency, Confidence, Pearl], + passes: &[(Inference, B), (Direction, B), (Plasticity, B)], + constants: &[(Witness, 0), (Epistemic, 0)], + needs_compose: true, + fails: "B's inference code has no implementation (Opcode::decode)", + }; + + /// `a.learn(b)`: revision of `a` by the observation `b`. + pub const LEARN: Contract = Contract { + name: "learn", + reads: &[ + (A, Spo), + (A, Frequency), + (A, Confidence), + (A, Plasticity), + (B, Spo), + (B, Frequency), + (B, Confidence), + ], + computes: &[Spo, Frequency, Confidence, Plasticity], + passes: &[ + (Pearl, A), + (Direction, A), + (Inference, A), + (Witness, A), + (Epistemic, A), + ], + constants: &[], + needs_compose: false, + fails: "never; no evidence on either side leaves A unchanged", + }; + + /// `a.syllogize(b)`: a fresh conclusion; the rule follows from the figure. + pub const SYLLOGIZE: Contract = Contract { + name: "syllogize", + reads: &[ + (A, Spo), + (A, Frequency), + (A, Confidence), + (A, Pearl), + (B, Spo), + (B, Frequency), + (B, Confidence), + (B, Pearl), + ], + computes: &[Spo, Frequency, Confidence, Pearl, Inference], + passes: &[], + constants: &[ + (Direction, 0), + (Plasticity, 0b111), + (Witness, 0), + (Epistemic, 0), + ], + needs_compose: false, + fails: "None (not an error) when the two edges share no term or are the same statement", + }; + + /// `a.revision(b)`: pure truth revision of the same statement. + pub const REVISION: Contract = Contract { + name: "revision", + reads: &[ + (A, Frequency), + (A, Confidence), + (B, Frequency), + (B, Confidence), + ], + computes: &[Frequency, Confidence], + passes: &[ + (Spo, A), + (Pearl, A), + (Direction, A), + (Inference, A), + (Plasticity, A), + (Witness, A), + (Epistemic, A), + ], + constants: &[], + needs_compose: false, + fails: "never; no evidence on either side gives (0.5, 0.0)", + }; + + /// All declared contracts. + pub const ALL: [Contract; 4] = [FORWARD, LEARN, SYLLOGIZE, REVISION]; +} + +#[cfg(test)] +mod layout_fault_tests { + use super::*; + use crate::edge::CausalEdge64; + + /// The direct partial methods and `forward` report the same fault code + /// for the same instruction, in whichever layout this build uses. + #[test] + fn partial_methods_and_forward_agree_in_the_active_layout() { + let t = vec![0u8; 256 * 256].into_boxed_slice(); + let t: Box<[u8; 256 * 256]> = t.try_into().expect("64 KiB"); + let c = Compose { + s: &t, + p: &t, + o: &t, + }; + let a = CausalEdge64(0x6ab8_2fff_ff03_0201); + for (it, direct) in [ + (InferenceType::Counterfactual, a.counterfactual(a, c)), + (InferenceType::Intervention, a.intervention(a, c)), + ] { + let mut w = CausalEdge64(0xb54c_13fe_0106_0504); + w.set_inference(it); + let via_forward = a.forward(w, &t, &t, &t).map(|e| e.0); + assert_eq!(direct.map(|e| e.0), via_forward, "{it:?}"); + #[cfg(feature = "causal-edge-v2-layout")] + let expect = it.to_mantissa(); + #[cfg(not(feature = "causal-edge-v2-layout"))] + let expect = it as i8; + assert_eq!(direct, Err(IsaFault::Unsupported { mantissa: expect })); + } + } +} diff --git a/crates/causal-edge/src/lib.rs b/crates/causal-edge/src/lib.rs index 0b72ba8ed..8a504d69f 100644 --- a/crates/causal-edge/src/lib.rs +++ b/crates/causal-edge/src/lib.rs @@ -53,6 +53,7 @@ pub mod edge; pub mod edge_v3; +pub mod isa; pub mod layout; pub mod network; pub mod pearl; @@ -65,6 +66,7 @@ mod v2_layout_tests; pub use edge::CausalEdge64; pub use edge_v3::CausalEdgeV3; +pub use isa::{Compose, IsaFault, Opcode}; pub use pearl::CausalMask; pub use plasticity::PlasticityState; pub use syllogism::{Figure, Syllogism}; diff --git a/crates/causal-edge/src/network.rs b/crates/causal-edge/src/network.rs index 056428ce5..288d596c7 100644 --- a/crates/causal-edge/src/network.rs +++ b/crates/causal-edge/src/network.rs @@ -7,6 +7,7 @@ //! and every Pearl level IS a 3-bit mask. use crate::edge::{CausalEdge64, InferenceType}; +use crate::isa::IsaFault; use crate::pearl::CausalMask; use crate::plasticity::PlasticityState; use crate::tables::NarsTables; @@ -58,23 +59,31 @@ impl CausalNetwork { /// /// Input edge is composed with each weight edge in sequence. /// Each intermediate IS a CausalEdge64 with full interpretability. - pub fn forward_chain(&self, input: CausalEdge64, path: &[usize]) -> CausalPath { + /// + /// # Errors + /// + /// The first [`IsaFault`] a hop raises; the chain stops there. + pub fn forward_chain( + &self, + input: CausalEdge64, + path: &[usize], + ) -> Result { let mut current = input; let mut hops = Vec::with_capacity(path.len() + 1); hops.push(current); for &edge_id in path { let weight = self.edges[edge_id]; - current = current.forward(weight, &self.compose_s, &self.compose_p, &self.compose_o); + current = current.forward(weight, &self.compose_s, &self.compose_p, &self.compose_o)?; hops.push(current); } let causal_level = current.causal_mask(); - CausalPath { + Ok(CausalPath { hops, conclusion: current, causal_level, - } + }) } /// Learn from observation: update all edges on the path with NARS revision. diff --git a/crates/causal-edge/src/syllogism.rs b/crates/causal-edge/src/syllogism.rs index cd7839e40..fb7ff33da 100644 --- a/crates/causal-edge/src/syllogism.rs +++ b/crates/causal-edge/src/syllogism.rs @@ -200,9 +200,9 @@ impl CausalEdge64 { let (f1, c1) = (self.frequency(), self.confidence()); let (f2, c2) = (other.frequency(), other.confidence()); let (f, c) = match figure { - Figure::Chain | Figure::ChainRev => deduction_truth(f1, c1, f2, c2), - Figure::SharedSubject => induction_truth(f1, c1, f2, c2), - Figure::SharedObject => abduction_truth(f1, c1, f2, c2), + Figure::Chain | Figure::ChainRev => crate::isa::truth::deduction(f1, c1, f2, c2), + Figure::SharedSubject => crate::isa::truth::induction(f1, c1, f2, c2), + Figure::SharedObject => crate::isa::truth::abduction(f1, c1, f2, c2), }; // Pearl mask: AND (only planes active in both survive) — as `forward`. @@ -233,33 +233,6 @@ impl CausalEdge64 { // ─── Truth-functions (mirror `ndarray::hpc::nars` + `CausalEdge64::forward`) ── // -// Kept private to this module. The formulas are byte-identical to the canonical -// `ndarray` hardware functions and to `forward`'s inline arms; the intentional -// mirror keeps `causal-edge` zero-dep (it cannot import `ndarray`). A later DRY -// pass may factor `forward`'s arms onto these. The hot-path u8→u8 table form -// lives in `tables.rs` (deduction shipped; induction/abduction tables follow). - -/// Deduction `A->B, B->C ⊢ A->C`: `f = f1·f2`, `c = f1·f2·c1·c2`. -#[inline] -fn deduction_truth(f1: f32, c1: f32, f2: f32, c2: f32) -> (f32, f32) { - let f = f1 * f2; - (f, f * c1 * c2) -} - -/// Induction `A->B, A->C ⊢ B->C`: `f = f2`, `c = w/(w+1)`, `w = f1·c1·c2`. -#[inline] -fn induction_truth(f1: f32, c1: f32, f2: f32, c2: f32) -> (f32, f32) { - let w = f1 * c1 * c2; - (f2, w / (w + 1.0)) -} - -/// Abduction `A->B, C->B ⊢ A->C`: `f = f1`, `c = w/(w+1)`, `w = f2·c1·c2`. -#[inline] -fn abduction_truth(f1: f32, c1: f32, f2: f32, c2: f32) -> (f32, f32) { - let w = f2 * c1 * c2; - (f1, w / (w + 1.0)) -} - #[cfg(test)] mod tests { use super::*; diff --git a/crates/causal-edge/tests/ce64_isa_contract.rs b/crates/causal-edge/tests/ce64_isa_contract.rs new file mode 100644 index 000000000..30d23cda1 --- /dev/null +++ b/crates/causal-edge/tests/ce64_isa_contract.rs @@ -0,0 +1,446 @@ +//! CE64 ISA contract: the decoder, the register methods, and each +//! instruction's declared field contract, measured. +//! +//! Reasoning chooses the operation. `CausalEdge64` defines what that operation +//! means. +#![cfg(feature = "causal-edge-v2-layout")] + +use causal_edge::isa::{contracts, truth, Contract, Field, IsaFault, Opcode, Operand}; +use causal_edge::{CausalEdge64, Compose}; + +fn tables() -> [Box<[u8; 65536]>; 3] { + let mk = |a: usize, b: usize| { + let mut t = vec![0u8; 65536].into_boxed_slice(); + for x in 0..256 { + for y in 0..256 { + t[x * 256 + y] = (x * a + y * b) as u8; + } + } + t.try_into().unwrap() + }; + [mk(31, 17), mk(7, 13), mk(11, 29)] +} + +fn compose(t: &[Box<[u8; 65536]>; 3]) -> Compose<'_> { + Compose { + s: &t[0], + p: &t[1], + o: &t[2], + } +} + +struct Rng(u64); +impl Rng { + fn next(&mut self) -> u64 { + self.0 = self.0.wrapping_add(0x9E37_79B9_7F4A_7C15); + let mut z = self.0; + z = (z ^ (z >> 30)).wrapping_mul(0xBF58_476D_1CE4_E5B9); + z = (z ^ (z >> 27)).wrapping_mul(0x94D0_49BB_1331_11EB); + z ^ (z >> 31) + } +} + +fn set(word: u64, f: Field, v: u64) -> u64 { + (word & !f.mask()) | ((v << f.span().0) & f.mask()) +} + +// ─── Decoder ──────────────────────────────────────────────────────────── + +/// Exactly five of the sixteen codes decode; every other code is refused +/// with that same code. +#[test] +fn the_decoder_accepts_exactly_the_implemented_codes() { + let mut accepted = Vec::new(); + for m in -8i8..=7 { + match Opcode::decode(m) { + Ok(op) => { + assert_eq!(op.encoding(), m, "decode is the inverse of encoding"); + accepted.push(m); + } + Err(IsaFault::Unsupported { mantissa }) => assert_eq!(mantissa, m), + } + } + accepted.sort_unstable(); + assert_eq!(accepted, vec![-1, 1, 2, 4, 5]); +} + +/// Counterfactual, intervention and reserved codes fault in `forward`; they +/// are never executed as another instruction and re-stamped. +#[test] +fn counterfactual_intervention_and_reserved_fault_in_forward() { + let t = tables(); + let running = CausalEdge64(0x6ab8_2fff_ff03_0201); + for m in [-6i8, 6, 7, -7] { + let weight = CausalEdge64(0xb54c_13fe_0106_0504).with_inference_mantissa(m); + assert_eq!( + running.forward(weight, &t[0], &t[1], &t[2]), + Err(IsaFault::Unsupported { mantissa: m }) + ); + } +} + +/// opcode = X executes exactly instruction X: `forward` on a weight carrying +/// X equals the named register method, bit for bit, and differs from every +/// other instruction on the same operands. +#[test] +fn forward_executes_exactly_the_decoded_instruction() { + let t = tables(); + let c = compose(&t); + let mut r = Rng(11); + let mut discriminated = 0; + for _ in 0..400 { + let running = CausalEdge64(r.next()); + let base = CausalEdge64(r.next()); + for op in Opcode::ALL { + let weight = base.with_inference_mantissa(op.encoding()); + let via_forward = running.forward(weight, c.s, c.p, c.o).unwrap(); + assert_eq!(via_forward, running.execute(op, weight, c)); + let named = match op { + Opcode::Deduction => running.deduction(weight, c), + Opcode::Induction => running.induction(weight, c), + Opcode::Abduction => running.abduction(weight, c), + Opcode::Revision => running.execute(Opcode::Revision, weight, c), + Opcode::Synthesis => running.synthesis(weight, c), + }; + assert_eq!(via_forward, named); + // The output carries the instruction that ran. + assert_eq!(via_forward.inference_mantissa(), op.encoding()); + let others_differ = Opcode::ALL.iter().filter(|&&o| o != op).all(|&o| { + let w = base.with_inference_mantissa(o.encoding()); + ( + running.execute(o, w, c).frequency_u8(), + running.execute(o, w, c).confidence_u8(), + ) != (via_forward.frequency_u8(), via_forward.confidence_u8()) + }); + discriminated += usize::from(others_differ); + } + } + // Anti-vacuity: on most operands every instruction is distinguishable. + assert!( + discriminated > 1500, + "only {discriminated}/2000 discriminated" + ); +} + +/// The register methods route through the one canonical truth function per +/// instruction: their F/C equal `Opcode::truth` packed, over a u8 grid. +#[test] +fn every_path_uses_the_canonical_truth_function() { + let t = tables(); + let c = compose(&t); + let pack = |x: f32| (x.clamp(0.0, 1.0) * 255.0).round() as u8; + for fa in (0..=255u8).step_by(17) { + for ca in (0..=254u8).step_by(23) { + for fb in (0..=255u8).step_by(19) { + for cb in (0..=254u8).step_by(29) { + let mut a = CausalEdge64(0); + a.set_frequency_u8(fa); + a.set_confidence_u8(ca); + let mut b = CausalEdge64(0); + b.set_frequency_u8(fb); + b.set_confidence_u8(cb); + let (f1, c1, f2, c2) = + (a.frequency(), a.confidence(), b.frequency(), b.confidence()); + for op in Opcode::ALL { + let (f, cc) = op.truth(f1, c1, f2, c2); + let out = a.execute(op, b, c); + assert_eq!( + (out.frequency_u8(), out.confidence_u8()), + (pack(f), pack(cc)) + ); + } + // learn's revision is the same function. + let mut l = a; + l.learn(b, 0); + match truth::revision(f1, c1, f2, c2) { + Some((f, cc)) => { + assert_eq!((l.frequency_u8(), l.confidence_u8()), (pack(f), pack(cc))) + } + None => assert_eq!((l.frequency_u8(), l.confidence_u8()), (fa, ca)), + } + } + } + } + } +} + +/// Partial instructions refuse with their own code; they never compute. +#[test] +fn counterfactual_and_intervention_methods_refuse() { + let t = tables(); + let c = compose(&t); + let (a, b) = ( + CausalEdge64(0x6ab8_2fff_ff03_0201), + CausalEdge64(0xb54c_13fe_0106_0504), + ); + #[cfg(feature = "causal-edge-v2-layout")] + { + assert_eq!( + a.counterfactual(b, c), + Err(IsaFault::Unsupported { mantissa: -6 }) + ); + assert_eq!( + a.intervention(b, c), + Err(IsaFault::Unsupported { mantissa: 6 }) + ); + } + #[cfg(not(feature = "causal-edge-v2-layout"))] + { + assert_eq!( + a.counterfactual(b, c), + Err(IsaFault::Unsupported { mantissa: 6 }) + ); + assert_eq!( + a.intervention(b, c), + Err(IsaFault::Unsupported { mantissa: 5 }) + ); + } +} + +/// The direct partial methods report the same fault `forward` reports for a +/// weight carrying the same instruction, in whichever layout is built. +#[test] +fn partial_methods_and_forward_report_the_same_code() { + use causal_edge::edge::InferenceType; + let t = tables(); + let c = compose(&t); + let a = CausalEdge64(0x6ab8_2fff_ff03_0201); + for (it, direct) in [ + (InferenceType::Counterfactual, a.counterfactual(a, c)), + (InferenceType::Intervention, a.intervention(a, c)), + ] { + let mut w = CausalEdge64(0xb54c_13fe_0106_0504); + w.set_inference(it); + let via_forward = a.forward(w, &t[0], &t[1], &t[2]).map(|e| e.0); + assert_eq!(direct.map(|e| e.0), via_forward, "{it:?}"); + assert!(direct.is_err()); + } +} + +/// `Compose` is operand algebra only: two different payload algebras change +/// S/P/O and nothing else. Every ISA-owned field is identical. +#[test] +fn compose_changes_only_the_payload() { + let t1 = tables(); + let mk = |a: usize, b: usize| -> Box<[u8; 65536]> { + let mut t = vec![0u8; 65536].into_boxed_slice(); + for x in 0..256 { + for y in 0..256 { + t[x * 256 + y] = (x * a ^ y * b) as u8; + } + } + t.try_into().unwrap() + }; + let t2 = [mk(3, 5), mk(9, 1), mk(13, 7)]; + let (c1, c2) = (compose(&t1), compose(&t2)); + let mut r = Rng(5); + let mut payload_differs = 0; + for _ in 0..500 { + let (a, b) = (CausalEdge64(r.next()), CausalEdge64(r.next())); + for op in Opcode::ALL { + let (x, y) = (a.execute(op, b, c1).0, a.execute(op, b, c2).0); + assert_eq!(x & !Field::Spo.mask(), y & !Field::Spo.mask(), "{op:?}"); + payload_differs += usize::from(x != y); + } + } + assert!( + payload_differs > 2000, + "the two algebras must actually differ" + ); +} + +// ─── Field contracts, measured ────────────────────────────────────────── + +#[derive(Clone, Copy, Debug)] +enum Instr { + Forward, + Learn, + Syllogize, + Revision, +} + +fn exec(i: Instr, a: u64, b: u64, c: Compose<'_>) -> Option { + let (a, b) = (CausalEdge64(a), CausalEdge64(b)); + match i { + Instr::Forward => a.forward(b, c.s, c.p, c.o).ok().map(|e| e.0), + Instr::Learn => { + let mut e = a; + e.learn(b, 0); + Some(e.0) + } + Instr::Syllogize => a.syllogize(b).map(|s| s.conclusion.0), + Instr::Revision => Some(a.revision(b).0), + } +} + +/// Operands valid for the instruction: forward needs an executable weight +/// code; syllogize needs a figure (chain: a.O == b.S). +fn operands(i: Instr, r: &mut Rng) -> (u64, u64) { + let (a, mut b) = (r.next(), r.next()); + match i { + Instr::Forward => { + let op = Opcode::ALL[(r.next() % 5) as usize]; + b = set(b, Field::Inference, u64::from(op.encoding() as u8 & 0xF)); + } + Instr::Syllogize => { + b = (b & !0xFF) | ((a >> 16) & 0xFF); + } + Instr::Learn | Instr::Revision => {} + } + (a, b) +} + +fn varied(i: Instr, word: u64, f: Field, r: &mut Rng) -> u64 { + let bits = (1u64 << f.span().1) - 1; + let mut v = (f.get(word) + 1 + r.next() % bits) & bits; + if matches!(i, Instr::Forward) && f == Field::Inference { + // Stay inside the decodable set: vary to another executable code. + let cur = f.get(word); + let ops: Vec = Opcode::ALL + .iter() + .map(|o| u64::from(o.encoding() as u8 & 0xF)) + .filter(|&e| e != cur) + .collect(); + v = ops[(r.next() % ops.len() as u64) as usize]; + } + set(word, f, v) +} + +fn check(contract: Contract, i: Instr) { + let t = tables(); + let c = compose(&t); + // Every output field is declared exactly once. + // A Spo output that is computed by composition needs an algebra. + assert_eq!( + contract.needs_compose, + matches!(i, Instr::Forward), + "{}: needs_compose", + contract.name + ); + for f in Field::ALL { + let n = usize::from(contract.computes.contains(&f)) + + contract.passes.iter().filter(|(g, _)| *g == f).count() + + contract.constants.iter().filter(|(g, _)| *g == f).count(); + assert_eq!(n, 1, "{}: {f:?} declared {n} times", contract.name); + } + let mut r = Rng(0xC0FFEE); + // passes / constants hold on every sample. + for _ in 0..2000 { + let (a, b) = operands(i, &mut r); + let out = exec(i, a, b, c).expect("valid operands"); + for &(f, side) in contract.passes { + let src = if side == Operand::A { a } else { b }; + assert_eq!(f.get(out), f.get(src), "{}: {f:?} passes", contract.name); + } + for &(f, v) in contract.constants { + assert_eq!(f.get(out), v, "{}: {f:?} constant", contract.name); + } + } + // reads: exactly the declared operand fields influence an output that is + // not their own pass-through. + let mut measured = Vec::new(); + for side in [Operand::A, Operand::B] { + for f in Field::ALL { + let mut hit = false; + for _ in 0..600 { + let (a, b) = operands(i, &mut r); + let (a2, b2) = if side == Operand::A { + (varied(i, a, f, &mut r), b) + } else { + (a, varied(i, b, f, &mut r)) + }; + // Keep the syllogism's chain figure intact under the variation. + let b2 = if matches!(i, Instr::Syllogize) { + (b2 & !0xFF) | ((a2 >> 16) & 0xFF) + } else { + b2 + }; + let (Some(o1), Some(o2)) = (exec(i, a, b, c), exec(i, a2, b2, c)) else { + continue; + }; + let passthrough = contract.passes.contains(&(f, side)); + let diff = Field::ALL + .iter() + .any(|&g| !(passthrough && g == f) && g.get(o1) != g.get(o2)); + if diff { + hit = true; + break; + } + } + if hit { + measured.push((side, f)); + } + } + } + let mut declared = contract.reads.to_vec(); + let key = |x: &(Operand, Field)| (x.0 as u8, x.1 as u8); + declared.sort_by_key(key); + measured.sort_by_key(key); + assert_eq!(measured, declared, "{}: reads", contract.name); +} + +#[test] +fn forward_contract_holds() { + check(contracts::FORWARD, Instr::Forward); +} + +#[test] +fn learn_contract_holds() { + check(contracts::LEARN, Instr::Learn); +} + +#[test] +fn revision_contract_holds() { + check(contracts::REVISION, Instr::Revision); +} + +#[test] +fn syllogize_contract_holds() { + check(contracts::SYLLOGIZE, Instr::Syllogize); +} + +/// No instruction zeroes a field without declaring it a constant: W and +/// Epi5 are either passed through or declared constant 0. +#[test] +fn witness_and_epistemic_are_never_cleared_undeclared() { + for k in contracts::ALL { + for f in [ + Field::Witness, + Field::Epistemic, + Field::Direction, + Field::Pearl, + ] { + let declared = k.computes.contains(&f) + || k.passes.iter().any(|(g, _)| *g == f) + || k.constants.iter().any(|(g, _)| *g == f); + assert!(declared, "{}: {f:?}", k.name); + } + } +} + +// ─── Layering ─────────────────────────────────────────────────────────── + +/// `isa.rs` defines arithmetic only. Reasoning-level policy (Gadamer +/// revision, horizons, grammar, codebooks, lenses, recipes) stays outside. +#[test] +fn isa_rs_names_no_reasoning_policy() { + let src = include_str!("../src/isa.rs"); + let code: String = src + .lines() + .filter(|l| !l.trim_start().starts_with("//")) + .collect::>() + .join("\n"); + for banned in [ + "lance_graph_contract", + "Gadamer", + "RevisionPolicy", + "Horizon", + "Grammar", + "Codebook", + "Lens", + "ThoughtCtx", + "Recipe", + ] { + assert!(!code.contains(banned), "isa.rs names {banned}"); + } +} diff --git a/crates/causal-edge/tests/ce64_isa_golden.rs b/crates/causal-edge/tests/ce64_isa_golden.rs new file mode 100644 index 000000000..746296184 --- /dev/null +++ b/crates/causal-edge/tests/ce64_isa_golden.rs @@ -0,0 +1,361 @@ +//! CE64 ISA golden vectors on raw `u64` words. +//! +//! Two sets, kept apart on purpose: +//! +//! - **Legacy capture** (`ce64_legacy_capture.txt`): what `forward`, `learn` +//! and `syllogize` returned BEFORE the ISA decoder, defects included, +//! recorded from that code. The ledger test says exactly which of them the +//! ISA changed (only the unsupported opcodes, which now refuse) and that +//! every other word is reproduced bit for bit. +//! - **Normative vectors**: the subset accepted as canonical, checked through +//! the register methods (`a.deduction(b, ..)` etc.) and, independently, +//! against an f64 reference of the NARS truth functions. The max-confidence +//! revision defect is NOT in this set; it is pinned as +//! [`KNOWN_BAD_REVISION_MAX_CONFIDENCE`]. +#![cfg(feature = "causal-edge-v2-layout")] + +use causal_edge::isa::{Field, IsaFault, Opcode}; +use causal_edge::{CausalEdge64, Compose}; + +const LEGACY: &str = include_str!("ce64_legacy_capture.txt"); + +/// `(a, b)` operands of the max-confidence revision defect: both edges at +/// confidence 255, weight opcode Revision. The legacy path, and the current +/// one, return frequency 0 and confidence 0. +const KNOWN_BAD_REVISION_MAX_CONFIDENCE: (u64, u64) = + (0x6ab8_2fff_ff03_0201, 0xb54d_13ff_ff06_0504); + +fn tables() -> [Box<[u8; 65536]>; 3] { + let mk = |a: usize, b: usize| { + let mut t = vec![0u8; 65536].into_boxed_slice(); + for x in 0..256 { + for y in 0..256 { + t[x * 256 + y] = (x * a + y * b) as u8; + } + } + t.try_into().unwrap() + }; + [mk(31, 17), mk(7, 13), mk(11, 29)] +} + +fn compose(t: &[Box<[u8; 65536]>; 3]) -> Compose<'_> { + Compose { + s: &t[0], + p: &t[1], + o: &t[2], + } +} + +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +enum Kind { + Forward(u8), + Learn, + Syllogize(u8), +} + +struct Vector { + kind: Kind, + a: u64, + b: u64, + expected: u64, +} + +fn legacy() -> Vec { + LEGACY + .lines() + .map(|l| { + let f: Vec<&str> = l.split_whitespace().collect(); + let hex = |s: &str| u64::from_str_radix(s.trim_start_matches("0x"), 16).unwrap(); + let kind = match f[0] { + "F" => Kind::Forward(f[1].parse().unwrap()), + "L" => Kind::Learn, + _ => Kind::Syllogize(f[1].parse().unwrap()), + }; + Vector { + kind, + a: hex(f[2]), + b: hex(f[3]), + expected: hex(f[4]), + } + }) + .collect() +} + +fn sign_extend(nibble: u8) -> i8 { + ((nibble << 4) as i8) >> 4 +} + +fn run(v: &Vector, c: Compose<'_>) -> Result { + let (a, b) = (CausalEdge64(v.a), CausalEdge64(v.b)); + Ok(match v.kind { + Kind::Forward(_) => a.forward(b, c.s, c.p, c.o)?.0, + Kind::Learn => { + let mut e = a; + e.learn(b, 0); + e.0 + } + Kind::Syllogize(_) => a.syllogize(b).unwrap().conclusion.0, + }) +} + +/// Revision with a c = 255 operand is outside the normative domain until the +/// saturation rule is decided: both operands at 255 collapse to (0, 0) +/// ([`KNOWN_BAD_REVISION_MAX_CONFIDENCE`]); one operand at 255 takes that +/// side's frequency outright (its weight saturates to `f32::MAX`), where the +/// capped f64 reference gives a weighted mean. +fn is_known_bad(v: &Vector) -> bool { + let revises = matches!(v.kind, Kind::Learn | Kind::Forward(4)); + revises && (Field::Confidence.get(v.a) == 255 || Field::Confidence.get(v.b) == 255) +} + +// ─── Legacy ledger ────────────────────────────────────────────────────── + +/// Every pre-ISA word is reproduced exactly, except the forward rows whose +/// weight carries an opcode with no implementation: those now refuse with +/// that exact code. Nothing else moved. +#[test] +fn the_isa_changed_exactly_the_unsupported_opcodes() { + let t = tables(); + let vectors = legacy(); + assert_eq!(vectors.len(), 126, "capture file"); + let (mut same, mut refused) = (0, 0); + for v in &vectors { + match (v.kind, run(v, compose(&t))) { + (_, Ok(w)) => { + assert_eq!(w, v.expected, "{:?} {:#018x} {:#018x}", v.kind, v.a, v.b); + same += 1; + } + (Kind::Forward(n), Err(IsaFault::Unsupported { mantissa })) => { + assert_eq!(mantissa, sign_extend(n)); + assert!(Opcode::decode(mantissa).is_err()); + refused += 1; + } + (k, Err(e)) => panic!("{k:?} faulted unexpectedly: {e}"), + } + } + // 16 nibbles, 5 supported: 11 x 5 forward rows refuse. + assert_eq!((same, refused), (126 - 55, 55)); +} + +// ─── Normative vectors through the register methods ───────────────────── + +fn opcode_of(nibble: u8) -> Option { + Opcode::decode(sign_extend(nibble)).ok() +} + +/// Every accepted forward vector, reproduced through the named register +/// method, not through `forward`'s decoder. +#[test] +fn normative_vectors_reproduce_through_register_methods() { + let t = tables(); + let c = compose(&t); + let mut n = 0; + for v in legacy() { + let Kind::Forward(nib) = v.kind else { continue }; + let Some(op) = opcode_of(nib) else { continue }; + if is_known_bad(&v) { + continue; + } + let (a, b) = (CausalEdge64(v.a), CausalEdge64(v.b)); + let out = match op { + Opcode::Deduction => a.deduction(b, c), + Opcode::Induction => a.induction(b, c), + Opcode::Abduction => a.abduction(b, c), + Opcode::Revision => a.execute(Opcode::Revision, b, c), + Opcode::Synthesis => a.synthesis(b, c), + }; + assert_eq!(out.0, v.expected, "{op:?}"); + n += 1; + } + // 25 executable rows, minus the 2 revision rows with a c = 255 operand. + assert_eq!(n, 23); +} + +/// f64 reference of the NARS truth functions (evidence horizon k = 1). +/// Confidence is capped at 0.9999 before revision, as the canonical upstream +/// (`ndarray::hpc::nars::NarsTruth::new`) does, so `c = 1` stays defined. +fn reference(op: Opcode, f1: f64, c1: f64, f2: f64, c2: f64) -> Option<(f64, f64)> { + Some(match op { + Opcode::Deduction => (f1 * f2, f1 * f2 * c1 * c2), + Opcode::Induction => { + let w = f1 * c1 * c2; + (f2, w / (w + 1.0)) + } + Opcode::Abduction => { + let w = f2 * c1 * c2; + (f1, w / (w + 1.0)) + } + Opcode::Revision => { + let (c1, c2) = (c1.min(0.9999), c2.min(0.9999)); + let (w1, w2) = (c1 / (1.0 - c1), c2 / (1.0 - c2)); + if w1 + w2 == 0.0 { + return None; + } + ((f1 * w1 + f2 * w2) / (w1 + w2), (w1 + w2) / (w1 + w2 + 1.0)) + } + Opcode::Synthesis => ((f1 + f2) / 2.0, (c1 + c2) / 2.0), + }) +} + +fn fc(word: u64) -> (u8, u8) { + ( + Field::Frequency.get(word) as u8, + Field::Confidence.get(word) as u8, + ) +} + +fn close(got: (u8, u8), want: (f64, f64)) -> bool { + let q = |x: f64| (x.clamp(0.0, 1.0) * 255.0).round() as i32; + (i32::from(got.0) - q(want.0)).abs() <= 1 && (i32::from(got.1) - q(want.1)).abs() <= 1 +} + +/// The normative vectors are not self-referential: their truth agrees with an +/// independent f64 reference, and every other field follows the declared +/// contract. +#[test] +fn normative_vectors_agree_with_an_independent_reference() { + for v in legacy() { + let Kind::Forward(nib) = v.kind else { continue }; + let Some(op) = opcode_of(nib) else { continue }; + if is_known_bad(&v) { + continue; + } + let u = |x: u64| x as f64 / 255.0; + let (fa, ca) = fc(v.a); + let (fb, cb) = fc(v.b); + let want = reference(op, u(fa.into()), u(ca.into()), u(fb.into()), u(cb.into())) + .unwrap_or((0.5, 0.0)); + assert!( + close(fc(v.expected), want), + "{op:?} {:?} vs {want:?}", + fc(v.expected) + ); + let e = v.expected; + assert_eq!( + Field::Pearl.get(e), + Field::Pearl.get(v.a) & Field::Pearl.get(v.b) + ); + assert_eq!(Field::Direction.get(e), Field::Direction.get(v.b)); + assert_eq!(Field::Plasticity.get(e), Field::Plasticity.get(v.b)); + assert_eq!(sign_extend(Field::Inference.get(e) as u8), op.encoding()); + assert_eq!((Field::Witness.get(e), Field::Epistemic.get(e)), (0, 0)); + } +} + +// ─── The max-confidence revision defect ───────────────────────────────── + +/// MEASURED DEFECT, NOT NORMATIVE. Revising two edges at confidence 255 +/// returns f = 0, c = 0, in `revision` and in `learn` alike. +/// +/// The path, step by step (each step asserted below): +/// 1. `c = 255/255 = 1.0 >= 0.999`, so `evidence_weight` returns `f32::MAX` +/// for both operands; +/// 2. `ws = MAX + MAX` overflows to `+inf`; +/// 3. `f = (f1·MAX + f2·MAX) / inf`: with `f1 = f2 = 1` the numerator is +/// also `inf`, so `f = inf/inf = NaN`; `c = inf / (inf + 1) = NaN`; +/// 4. packing: `NaN.clamp(0, 1)` is `NaN`, and the float-to-`u8` cast +/// saturates `NaN` to `0`. +/// +/// Not a u8 overflow, a table bin, or a zero-denominator fallback: the +/// confidence-to-weight transform saturates to a finite value whose SUM +/// overflows. The intended result (f64 reference, c capped at 0.9999) is the +/// mean frequency at confidence 255. +/// +/// FAILS IF: the defect is fixed. Then move this case into the normative set +/// with the reference result. +#[test] +fn known_bad_revision_max_confidence_collapses_to_zero() { + use causal_edge::isa::truth; + // 1-3, on the canonical truth function. + assert_eq!(truth::evidence_weight(1.0), f32::MAX); + assert_eq!(f32::MAX + f32::MAX, f32::INFINITY); + let (f, c) = truth::revision(1.0, 1.0, 1.0, 1.0).unwrap(); + assert!(f.is_nan() && c.is_nan()); + // 4. + assert_eq!((f.clamp(0.0, 1.0) * 255.0).round() as u8, 0); + + let t = tables(); + let (a, b) = KNOWN_BAD_REVISION_MAX_CONFIDENCE; + let out = CausalEdge64(a).revision(CausalEdge64(b)); + let step = CausalEdge64(a).execute(Opcode::Revision, CausalEdge64(b), compose(&t)); + assert_eq!(fc(step.0), (0, 0)); + assert_eq!(fc(out.0), (0, 0)); + let mut l = CausalEdge64(a); + l.learn(CausalEdge64(b), 0); + assert_eq!(fc(l.0), (0, 0)); + + // What it should be. + let want = reference(Opcode::Revision, 1.0, 1.0, 1.0, 1.0).unwrap(); + assert!(close((255, 255), want)); + assert!(!close(fc(out.0), want)); +} + +/// MEASURED, NOT NORMATIVE. With ONE operand at c = 255 the result is +/// finite, but that operand's weight saturates to `f32::MAX` and its +/// frequency wins outright. The capped reference gives a weighted mean. +/// Which of the two is canonical is the same open decision as the collapse. +#[test] +fn one_saturated_operand_dominates_revision() { + use causal_edge::isa::truth; + let (f, c) = truth::revision(1.0, 1.0, 1.0 / 255.0, 254.0 / 255.0).unwrap(); + assert!(f.is_finite() && c.is_finite()); + let got = ((f * 255.0).round() as u8, (c * 255.0).round() as u8); + assert_eq!(got, (255, 255)); + let want = reference(Opcode::Revision, 1.0, 1.0, 1.0 / 255.0, 254.0 / 255.0).unwrap(); + assert_eq!((want.0 * 255.0).round() as u8, 249); +} + +// ─── Revision boundary contract ───────────────────────────────────────── + +/// Numeric revision at the confidence boundaries, for identical, asymmetric +/// and contradictory frequencies, through both the register method and +/// `learn`. All agree with the f64 reference except the double-saturated +/// pair. (A single c = 255 operand against c = 0 agrees: the other side has +/// no weight to lose.) +#[test] +fn revision_boundaries_match_the_reference_except_the_known_defect() { + let confidences = [(0u8, 0u8), (0, 255), (1, 1), (254, 254), (255, 255)]; + let frequencies = [(200u8, 200u8), (230, 40), (255, 0)]; + let mut bad = Vec::new(); + for &(ca, cb) in &confidences { + for &(fa, fb) in &frequencies { + let a = CausalEdge64(0) + .with_inference_mantissa(1) + .with_w_slot(9) + .with_epistemic_raw5(5); + let mut a = a; + a.set_frequency_u8(fa); + a.set_confidence_u8(ca); + let mut b = CausalEdge64(0); + b.set_frequency_u8(fb); + b.set_confidence_u8(cb); + let u = |x: u8| f64::from(x) / 255.0; + let want = reference(Opcode::Revision, u(fa), u(ca), u(fb), u(cb)); + + let m = fc(a.revision(b).0); + let mut l = a; + l.learn(b, 0); + let learned = fc(l.0); + match want { + None => { + // No evidence on either side: the method reports + // "unknown", learn leaves the edge untouched. + assert_eq!(m, (128, 0)); + assert_eq!(learned, (fa, ca)); + } + Some(w) => { + if !close(m, w) || !close(learned, w) { + bad.push(((fa, ca), (fb, cb), m, learned)); + } + } + } + // learn's revision preserves the register's other state. + assert_eq!((l.w_slot(), l.epistemic_raw5()), (9, 5)); + } + } + // Only the double-saturated pair disagrees, for every frequency mix. + assert_eq!(bad.len(), 3, "{bad:?}"); + assert!(bad + .iter() + .all(|&((_, ca), (_, cb), _, _)| (ca, cb) == (255, 255))); +} diff --git a/crates/causal-edge/tests/ce64_legacy_capture.txt b/crates/causal-edge/tests/ce64_legacy_capture.txt new file mode 100644 index 000000000..3be2205f8 --- /dev/null +++ b/crates/causal-edge/tests/ce64_legacy_capture.txt @@ -0,0 +1,126 @@ +F 0 0x6ab82f0000030201 0xb54c134080060504 0x000c530000cf4f63 +F 0 0x6ab82fffff030201 0xb54c13fe01060504 0x000c530101cf4f63 +F 0 0x6ab82f4080030201 0xb54c1301fe060504 0x000c53007fcf4f63 +F 0 0x6ab82ffe01030201 0xb54c130000060504 0x000c530000cf4f63 +F 0 0x6ab82f01fe030201 0xb54c13ffff060504 0x000c5301fecf4f63 +F 1 0x6ab82f0000030201 0xb54c534080060504 0x000c530000cf4f63 +F 1 0x6ab82fffff030201 0xb54c53fe01060504 0x000c530101cf4f63 +F 1 0x6ab82f4080030201 0xb54c5301fe060504 0x000c53007fcf4f63 +F 1 0x6ab82ffe01030201 0xb54c530000060504 0x000c530000cf4f63 +F 1 0x6ab82f01fe030201 0xb54c53ffff060504 0x000c5301fecf4f63 +F 2 0x6ab82f0000030201 0xb54c934080060504 0x000c930080cf4f63 +F 2 0x6ab82fffff030201 0xb54c93fe01060504 0x000c937f01cf4f63 +F 2 0x6ab82f4080030201 0xb54c9301fe060504 0x000c9300fecf4f63 +F 2 0x6ab82ffe01030201 0xb54c930000060504 0x000c930000cf4f63 +F 2 0x6ab82f01fe030201 0xb54c93ffff060504 0x000c9301ffcf4f63 +F 3 0x6ab82f0000030201 0xb54cd34080060504 0x000d532040cf4f63 +F 3 0x6ab82fffff030201 0xb54cd3fe01060504 0x000d53ff80cf4f63 +F 3 0x6ab82f4080030201 0xb54cd301fe060504 0x000d5321bfcf4f63 +F 3 0x6ab82ffe01030201 0xb54cd30000060504 0x000d537f01cf4f63 +F 3 0x6ab82f01fe030201 0xb54cd3ffff060504 0x000d5380ffcf4f63 +F 4 0x6ab82f0000030201 0xb54d134080060504 0x000d134080cf4f63 +F 4 0x6ab82fffff030201 0xb54d13fe01060504 0x000d13ffffcf4f63 +F 4 0x6ab82f4080030201 0xb54d1301fe060504 0x000d134181cf4f63 +F 4 0x6ab82ffe01030201 0xb54d130000060504 0x000d13fe01cf4f63 +F 4 0x6ab82f01fe030201 0xb54d13ffff060504 0x000d13ffffcf4f63 +F 5 0x6ab82f0000030201 0xb54d534080060504 0x000d532040cf4f63 +F 5 0x6ab82fffff030201 0xb54d53fe01060504 0x000d53ff80cf4f63 +F 5 0x6ab82f4080030201 0xb54d5301fe060504 0x000d5321bfcf4f63 +F 5 0x6ab82ffe01030201 0xb54d530000060504 0x000d537f01cf4f63 +F 5 0x6ab82f01fe030201 0xb54d53ffff060504 0x000d5380ffcf4f63 +F 6 0x6ab82f0000030201 0xb54d934080060504 0x000d932040cf4f63 +F 6 0x6ab82fffff030201 0xb54d93fe01060504 0x000d93ff80cf4f63 +F 6 0x6ab82f4080030201 0xb54d9301fe060504 0x000d9321bfcf4f63 +F 6 0x6ab82ffe01030201 0xb54d930000060504 0x000d937f01cf4f63 +F 6 0x6ab82f01fe030201 0xb54d93ffff060504 0x000d9380ffcf4f63 +F 7 0x6ab82f0000030201 0xb54dd34080060504 0x000dd32040cf4f63 +F 7 0x6ab82fffff030201 0xb54dd3fe01060504 0x000dd3ff80cf4f63 +F 7 0x6ab82f4080030201 0xb54dd301fe060504 0x000dd321bfcf4f63 +F 7 0x6ab82ffe01030201 0xb54dd30000060504 0x000dd37f01cf4f63 +F 7 0x6ab82f01fe030201 0xb54dd3ffff060504 0x000dd380ffcf4f63 +F 8 0x6ab82f0000030201 0xb54e134080060504 0x000c530000cf4f63 +F 8 0x6ab82fffff030201 0xb54e13fe01060504 0x000c530101cf4f63 +F 8 0x6ab82f4080030201 0xb54e1301fe060504 0x000c53007fcf4f63 +F 8 0x6ab82ffe01030201 0xb54e130000060504 0x000c530000cf4f63 +F 8 0x6ab82f01fe030201 0xb54e13ffff060504 0x000c5301fecf4f63 +F 9 0x6ab82f0000030201 0xb54e534080060504 0x000dd32040cf4f63 +F 9 0x6ab82fffff030201 0xb54e53fe01060504 0x000dd3ff80cf4f63 +F 9 0x6ab82f4080030201 0xb54e5301fe060504 0x000dd321bfcf4f63 +F 9 0x6ab82ffe01030201 0xb54e530000060504 0x000dd37f01cf4f63 +F 9 0x6ab82f01fe030201 0xb54e53ffff060504 0x000dd380ffcf4f63 +F 10 0x6ab82f0000030201 0xb54e934080060504 0x000e932040cf4f63 +F 10 0x6ab82fffff030201 0xb54e93fe01060504 0x000e93ff80cf4f63 +F 10 0x6ab82f4080030201 0xb54e9301fe060504 0x000e9321bfcf4f63 +F 10 0x6ab82ffe01030201 0xb54e930000060504 0x000e937f01cf4f63 +F 10 0x6ab82f01fe030201 0xb54e93ffff060504 0x000e9380ffcf4f63 +F 11 0x6ab82f0000030201 0xb54ed34080060504 0x000d532040cf4f63 +F 11 0x6ab82fffff030201 0xb54ed3fe01060504 0x000d53ff80cf4f63 +F 11 0x6ab82f4080030201 0xb54ed301fe060504 0x000d5321bfcf4f63 +F 11 0x6ab82ffe01030201 0xb54ed30000060504 0x000d537f01cf4f63 +F 11 0x6ab82f01fe030201 0xb54ed3ffff060504 0x000d5380ffcf4f63 +F 12 0x6ab82f0000030201 0xb54f134080060504 0x000d134080cf4f63 +F 12 0x6ab82fffff030201 0xb54f13fe01060504 0x000d13ffffcf4f63 +F 12 0x6ab82f4080030201 0xb54f1301fe060504 0x000d134181cf4f63 +F 12 0x6ab82ffe01030201 0xb54f130000060504 0x000d13fe01cf4f63 +F 12 0x6ab82f01fe030201 0xb54f13ffff060504 0x000d13ffffcf4f63 +F 13 0x6ab82f0000030201 0xb54f534080060504 0x000fd30000cf4f63 +F 13 0x6ab82fffff030201 0xb54f53fe01060504 0x000fd301ffcf4f63 +F 13 0x6ab82f4080030201 0xb54f5301fe060504 0x000fd30080cf4f63 +F 13 0x6ab82ffe01030201 0xb54f530000060504 0x000fd30001cf4f63 +F 13 0x6ab82f01fe030201 0xb54f53ffff060504 0x000fd301fecf4f63 +F 14 0x6ab82f0000030201 0xb54f934080060504 0x000fd30000cf4f63 +F 14 0x6ab82fffff030201 0xb54f93fe01060504 0x000fd301ffcf4f63 +F 14 0x6ab82f4080030201 0xb54f9301fe060504 0x000fd30080cf4f63 +F 14 0x6ab82ffe01030201 0xb54f930000060504 0x000fd30001cf4f63 +F 14 0x6ab82f01fe030201 0xb54f93ffff060504 0x000fd301fecf4f63 +F 15 0x6ab82f0000030201 0xb54fd34080060504 0x000fd30000cf4f63 +F 15 0x6ab82fffff030201 0xb54fd3fe01060504 0x000fd301ffcf4f63 +F 15 0x6ab82f4080030201 0xb54fd301fe060504 0x000fd30080cf4f63 +F 15 0x6ab82ffe01030201 0xb54fd30000060504 0x000fd30001cf4f63 +F 15 0x6ab82f01fe030201 0xb54fd3ffff060504 0x000fd301fecf4f63 +F 4 0x6ab82fffff030201 0xb54d13ffff060504 0x000d130000cf4f63 +L - 0x6abc750000030201 0xb5410b0000090807 0x6abc750000030201 +L - 0x6abc750000030201 0xb5410bffff090807 0x6aa075ffff090807 +L - 0x6abc750000030201 0xb5410b4080090807 0x6abc754080090807 +L - 0x6abc750000030201 0xb5410bfe01090807 0x6aa075fe01090807 +L - 0x6abc750000030201 0xb5410b01fe090807 0x6abc7501fe090807 +L - 0x6abc75ffff030201 0xb5410b0000090807 0x6aa075ffff030201 +L - 0x6abc75ffff030201 0xb5410bffff090807 0x6abc750000030201 +L - 0x6abc75ffff030201 0xb5410b4080090807 0x6aa075ffff030201 +L - 0x6abc75ffff030201 0xb5410bfe01090807 0x6aa075ffff030201 +L - 0x6abc75ffff030201 0xb5410b01fe090807 0x6aa075ffff030201 +L - 0x6abc754080030201 0xb5410b0000090807 0x6abc754080030201 +L - 0x6abc754080030201 0xb5410bffff090807 0x6aa075ffff090807 +L - 0x6abc754080030201 0xb5410b4080090807 0x6abc756680030201 +L - 0x6abc754080030201 0xb5410bfe01090807 0x6aa075fe01090807 +L - 0x6abc754080030201 0xb5410b01fe090807 0x6abc754181030201 +L - 0x6abc75fe01030201 0xb5410b0000090807 0x6aa075fe01030201 +L - 0x6abc75fe01030201 0xb5410bffff090807 0x6aa075ffff090807 +L - 0x6abc75fe01030201 0xb5410b4080090807 0x6aa075fe01030201 +L - 0x6abc75fe01030201 0xb5410bfe01090807 0x6aa075fe01030201 +L - 0x6abc75fe01030201 0xb5410b01fe090807 0x6aa075fe01030201 +L - 0x6abc7501fe030201 0xb5410b0000090807 0x6abc7501fe030201 +L - 0x6abc7501fe030201 0xb5410bffff090807 0x6aa075ffff090807 +L - 0x6abc7501fe030201 0xb5410b4080090807 0x6abc754181090807 +L - 0x6abc7501fe030201 0xb5410bfe01090807 0x6aa075fe01090807 +L - 0x6abc7501fe030201 0xb5410b01fe090807 0x6abc7502fe030201 +S 0 0x6aa4af0000030201 0xb5495e0000050403 0x001c460000050201 +S 0 0x6aa4afffff030201 0xb5495effff050403 0x001c46ffff050201 +S 0 0x6aa4af4080030201 0xb5495e8040050403 0x001c460420050201 +S 0 0x6aa4affe01030201 0xb5495e01fe050403 0x001c460001050201 +S 0 0x6aa4af01fe030201 0xb5495efe01050403 0x001c460001050201 +S 1 0x6aa4af0000030201 0xb5495e0000010405 0x001c460000030405 +S 1 0x6aa4afffff030201 0xb5495effff010405 0x001c46ffff030405 +S 1 0x6aa4af4080030201 0xb5495e8040010405 0x001c460420030405 +S 1 0x6aa4affe01030201 0xb5495e01fe010405 0x001c460001030405 +S 1 0x6aa4af01fe030201 0xb5495efe01010405 0x001c460001030405 +S 2 0x6aa4af0000030201 0xb5495e0000050401 0x001c860000050203 +S 2 0x6aa4afffff030201 0xb5495effff050401 0x001c8680ff050203 +S 2 0x6aa4af4080030201 0xb5495e8040050401 0x001c860f40050203 +S 2 0x6aa4affe01030201 0xb5495e01fe050401 0x001c8600fe050203 +S 2 0x6aa4af01fe030201 0xb5495efe01050401 0x001c860101050203 +S 3 0x6aa4af0000030201 0xb5495e0000030405 0x001fc60000050201 +S 3 0x6aa4afffff030201 0xb5495effff030405 0x001fc680ff050201 +S 3 0x6aa4af4080030201 0xb5495e8040030405 0x001fc60880050201 +S 3 0x6aa4affe01030201 0xb5495e01fe030405 0x001fc60101050201 +S 3 0x6aa4af01fe030201 0xb5495efe01030405 0x001fc600fe050201 diff --git a/crates/causal-edge/tests/ce64_op_contract.rs b/crates/causal-edge/tests/ce64_op_contract.rs index bb2a46cb4..12a936dfb 100644 --- a/crates/causal-edge/tests/ce64_op_contract.rs +++ b/crates/causal-edge/tests/ce64_op_contract.rs @@ -5,8 +5,9 @@ //! has to flip an assertion on purpose rather than drift past it: //! //! 1. `forward` selects its NARS rule from the WEIGHT operand's mantissa -//! (bits 46..49). Counterfactual (−6) has no arm of its own, so it runs the -//! Synthesis average and is then re-stamped −6. +//! (bits 46..49). Counterfactual (−6) has no implementation. It used to run +//! the Synthesis average and be re-stamped −6; since the CE64 ISA decoder +//! (`isa.rs`) it faults instead. //! 2. Which operations keep the W slot (53..58) and `EpistemicState5` //! (59..63), and which silently zero them. //! @@ -46,7 +47,9 @@ fn edge(f: u8, c: u8, rule: InferenceType) -> CausalEdge64 { fn forward(running: CausalEdge64, weight: CausalEdge64) -> CausalEdge64 { let t = keep_left(); - running.forward(weight, &t, &t, &t) + running + .forward(weight, &t, &t, &t) + .expect("executable weight code") } fn fc(e: CausalEdge64) -> (u8, u8) { @@ -73,25 +76,23 @@ fn forward_dispatch_on_the_weight_mantissa_is_live() { assert_ne!(fc(forward(running, weight)), fc(forward(running, synth))); } -/// MEASURED DEFECT (pinned): a weight carrying Counterfactual (−6) computes -/// exactly the Synthesis average. The mantissa still reads −6 afterwards, so -/// the edge is labelled counterfactual but holds an average. +/// FLIPPED by the CE64 ISA decoder. A weight carrying Counterfactual (−6) used +/// to compute exactly the Synthesis average and be re-stamped −6. It now +/// faults: no counterfactual rule exists, so nothing runs. /// -/// FAILS IF: `forward` gains a Counterfactual rule (then flip this test and -/// record the rule) — or stops re-stamping −6. +/// FAILS IF: `forward` gains a Counterfactual rule (then pin the rule here) or +/// falls back to another instruction again. #[test] -fn a_counterfactual_weight_runs_the_synthesis_average() { +fn a_counterfactual_weight_faults_instead_of_running_synthesis() { + let t = keep_left(); let running = edge(255, 255, InferenceType::Deduction); let cf = edge(0, 0, InferenceType::Deduction) .with_inference_mantissa(InferenceType::Counterfactual.to_mantissa()); - let synth = edge(0, 0, InferenceType::Synthesis); assert_eq!(cf.inference_mantissa(), -6, "fixture must carry −6"); - - let out_cf = forward(running, cf); - let out_synth = forward(running, synth); - assert_eq!(fc(out_cf), fc(out_synth), "−6 runs the Synthesis arm"); - assert_eq!(fc(out_cf), (128, 128)); - assert_eq!(out_cf.inference_mantissa(), -6, "and is re-stamped −6"); + assert_eq!( + running.forward(cf, &t, &t, &t), + Err(causal_edge::IsaFault::Unsupported { mantissa: -6 }) + ); } /// Silent arm: the same weight twice gives the same answer. diff --git a/crates/lance-graph-planner/examples/dcr_w0_replay_budget.rs b/crates/lance-graph-planner/examples/dcr_w0_replay_budget.rs index 7268cde12..67598995a 100644 --- a/crates/lance-graph-planner/examples/dcr_w0_replay_budget.rs +++ b/crates/lance-graph-planner/examples/dcr_w0_replay_budget.rs @@ -123,7 +123,9 @@ fn promised_step( weight.confidence_u8(), ); // 2. the packed-edge half - let out = running.forward(weight, cs, cp, co); + let out = running + .forward(weight, cs, cp, co) + .expect("executable weight code"); // fold the lookup back in so neither half can be optimised away CausalEdge64(out.0 ^ ((unpack_f(revised) as u64) << 32) ^ (unpack_c(revised) as u64)) } diff --git a/crates/lance-graph-planner/src/cache/nars_engine.rs b/crates/lance-graph-planner/src/cache/nars_engine.rs index cf8200852..099564308 100644 --- a/crates/lance-graph-planner/src/cache/nars_engine.rs +++ b/crates/lance-graph-planner/src/cache/nars_engine.rs @@ -603,7 +603,7 @@ impl NarsEngine { compose_s: &[u8; 256 * 256], compose_p: &[u8; 256 * 256], compose_o: &[u8; 256 * 256], - ) -> CausalEdge64 { + ) -> Result { input.forward(weight, compose_s, compose_p, compose_o) } diff --git a/crates/lance-graph-planner/src/cache/stage26_v3_parity.rs b/crates/lance-graph-planner/src/cache/stage26_v3_parity.rs index 2eba01a41..65f24f816 100644 --- a/crates/lance-graph-planner/src/cache/stage26_v3_parity.rs +++ b/crates/lance-graph-planner/src/cache/stage26_v3_parity.rs @@ -60,7 +60,7 @@ use std::collections::BTreeMap; -use causal_edge::{CausalEdge64, CausalEdgeV3}; +use causal_edge::{CausalEdge64, CausalEdgeV3, IsaFault}; use super::nars_engine::{NarsEngine, SpoDistances, SpoHead}; @@ -90,15 +90,17 @@ struct Leg { case: String, /// Direct arm. direct_edge: CausalEdge64, - direct_fwd: CausalEdge64, + /// `Err` when the weight's inference code does not execute (the CE64 ISA + /// decoder); both arms must then refuse identically. + direct_fwd: Result, direct_head: SpoHead, - direct_fwd_head: SpoHead, + direct_fwd_head: Result, direct_syllogism: Option, /// V3 arm — same engine, same methods, edge routed through V3. v3_edge: CausalEdge64, - v3_fwd: CausalEdge64, + v3_fwd: Result, v3_head: SpoHead, - v3_fwd_head: SpoHead, + v3_fwd_head: Result, v3_syllogism: Option, } @@ -300,10 +302,10 @@ fn run_leg( Leg { case, direct_head: engine.from_causal_edge(direct_edge), - direct_fwd_head: engine.from_causal_edge(direct_fwd), + direct_fwd_head: direct_fwd.map(|e| engine.from_causal_edge(e)), direct_syllogism: syl(direct_edge, direct_w), v3_head: engine.from_causal_edge(v3_edge), - v3_fwd_head: engine.from_causal_edge(v3_fwd), + v3_fwd_head: v3_fwd.map(|e| engine.from_causal_edge(e)), v3_syllogism: syl(v3_edge, v3_w), direct_edge, direct_fwd, @@ -475,7 +477,7 @@ mod tests { // there, which is the property the non-identity tables exist to give. let moved = legs .iter() - .filter(|l| l.direct_fwd != l.direct_edge) + .filter(|l| l.direct_fwd.is_ok_and(|f| f != l.direct_edge)) .count(); assert!( moved > 0, @@ -483,7 +485,10 @@ mod tests { ); let spo_moved = legs .iter() - .filter(|l| spo_of(l.direct_fwd) != spo_of(l.direct_edge)) + .filter(|l| { + l.direct_fwd + .is_ok_and(|f| spo_of(f) != spo_of(l.direct_edge)) + }) .count(); assert!( spo_moved > 0, diff --git a/crates/lance-graph-planner/src/chain_replay.rs b/crates/lance-graph-planner/src/chain_replay.rs index 02f8f0c94..549d6104f 100644 --- a/crates/lance-graph-planner/src/chain_replay.rs +++ b/crates/lance-graph-planner/src/chain_replay.rs @@ -133,10 +133,13 @@ pub type ChainStep = (u8, CausalEdge64); /// A replay could not be performed as asked. /// -/// Deliberately small: replay has exactly one way to fail, and it is a -/// property of the ADDRESS SPACE the caller offered, never of the recorded -/// chain (see [`crate::chain_admission::validate_chain`] for why a chain's -/// content is not judged here). +/// Two ways to fail. [`SequenceExhausted`](Self::SequenceExhausted) is a +/// property of the ADDRESS SPACE the caller offered. [`Isa`](Self::Isa) is a +/// property of a recorded weight: its inference code is one the CE64 ISA +/// does not execute, so the step cannot be computed. Replay still does not +/// judge whether a chain is plausible +/// ([`crate::chain_admission::validate_chain`] owns that); it only refuses a +/// step it has no instruction for. #[derive(Debug, Clone, Copy, PartialEq, Eq)] #[non_exhaustive] pub enum ReplayError { @@ -154,6 +157,14 @@ pub enum ReplayError { /// How many steps the chain needed. steps: usize, }, + /// A step's weight carries an inference code the CE64 ISA does not + /// execute ([`causal_edge::isa::IsaFault`]). + Isa { + /// The step that faulted. + step: usize, + /// The fault. + fault: causal_edge::isa::IsaFault, + }, } impl fmt::Display for ReplayError { @@ -163,6 +174,7 @@ impl fmt::Display for ReplayError { f, "durable sequence exhausted: base {base_seq} cannot reserve {steps} steps" ), + Self::Isa { step, fault } => write!(f, "step {step}: {fault}"), } } } @@ -174,13 +186,12 @@ impl std::error::Error for ReplayError {} /// the table lookup (evidence fusion) then the packed forward (palette /// composition + truth propagation). #[inline] -#[must_use] pub fn replay_step( running: CausalEdge64, weight: CausalEdge64, tables: &NarsTables, compose: ComposeTables<'_>, -) -> CausalEdge64 { +) -> Result { // 1. fuse this step's evidence into the running truth (the lookup half) let revised = tables.revise( running.frequency_u8(), @@ -189,12 +200,12 @@ pub fn replay_step( weight.confidence_u8(), ); // 2. propagate palettes + causality (the packed half) - let mut out = running.forward(weight, compose.s, compose.p, compose.o); + let mut out = running.forward(weight, compose.s, compose.p, compose.o)?; // 3. the revised truth is the step's truth — written back into the packed // edge, not carried beside it (there is no second truth register). out.set_frequency_u8(unpack_f(revised)); out.set_confidence_u8(unpack_c(revised)); - out + Ok(out) } /// Replay a recorded chain against `seed`, emitting one trace row per step. @@ -228,6 +239,10 @@ pub fn replay_step( /// does not fit in `u64`. The reservation is checked ONCE, up front, so the /// loop cannot emit a partial trace and then discover it has no coordinate /// left — a half-written trace is worse than a refusal. +/// +/// [`ReplayError::Isa`] when a step's weight carries an inference code the +/// CE64 ISA does not execute (Counterfactual, Intervention, or a reserved +/// code). pub fn replay_chain( chain: &[ChainStep], seed: CausalEdge64, @@ -248,7 +263,8 @@ pub fn replay_chain( let mut running = seed; let mut trace = Vec::with_capacity(steps); for (i, &(predicate, weight)) in chain.iter().enumerate() { - running = replay_step(running, weight, tables, compose); + running = replay_step(running, weight, tables, compose) + .map_err(|fault| ReplayError::Isa { step: i, fault })?; trace.push(ReplayTraceRow { owner, cast_seq: base_seq + i as u64, diff --git a/crates/lance-graph-planner/tests/chain_confidence.rs b/crates/lance-graph-planner/tests/chain_confidence.rs index 620925b39..3d530cb19 100644 --- a/crates/lance-graph-planner/tests/chain_confidence.rs +++ b/crates/lance-graph-planner/tests/chain_confidence.rs @@ -57,7 +57,7 @@ fn trace(hops: usize, step: impl Fn(CausalEdge64, CausalEdge64) -> CausalEdge64) #[test] fn forward_deduction_lowers_confidence_along_the_chain() { let t = keep_left(); - let c = trace(5, |r, w| r.forward(w, &t, &t, &t)); + let c = trace(5, |r, w| r.forward(w, &t, &t, &t).unwrap()); assert!(c.windows(2).all(|p| p[1] < p[0]), "{c:?}"); } @@ -77,7 +77,7 @@ fn replay_step_raises_confidence_along_a_deduction_chain() { p: &t, o: &t, }; - let c = trace(5, |r, w| replay_step(r, w, &tables, compose)); + let c = trace(5, |r, w| replay_step(r, w, &tables, compose).unwrap()); assert_eq!(c, [200, 224, 237, 237, 237, 237]); } @@ -96,7 +96,7 @@ fn self_revision_raises_confidence_on_the_replay_path() { o: &t, }; let e = edge(200, 128); - let out = replay_step(e, e, &tables, compose); + let out = replay_step(e, e, &tables, compose).unwrap(); assert!( out.confidence_u8() > e.confidence_u8(), "{} -> {}", @@ -120,7 +120,7 @@ fn a_zero_confidence_weight_still_adds_confidence_on_the_replay_path() { o: &t, }; let e = edge(200, 128); - let out = replay_step(e, edge(200, 0), &tables, compose); + let out = replay_step(e, edge(200, 0), &tables, compose).unwrap(); assert_eq!((e.confidence_u8(), out.confidence_u8()), (128, 137)); } @@ -129,6 +129,6 @@ fn a_zero_confidence_weight_still_adds_confidence_on_the_replay_path() { #[test] fn forward_deduction_adds_nothing_for_a_zero_confidence_weight() { let t = keep_left(); - let out = edge(200, 128).forward(edge(200, 0), &t, &t, &t); + let out = edge(200, 128).forward(edge(200, 0), &t, &t, &t).unwrap(); assert_eq!(out.confidence_u8(), 0); } diff --git a/crates/lance-graph-planner/tests/gadamer_isa_revision.rs b/crates/lance-graph-planner/tests/gadamer_isa_revision.rs new file mode 100644 index 000000000..f24b3d2b6 --- /dev/null +++ b/crates/lance-graph-planner/tests/gadamer_isa_revision.rs @@ -0,0 +1,137 @@ +//! Gadamer decides whether revision is warranted; the CE64 register defines how +//! admitted evidence is numerically revised. +//! +//! `GadamerRevision` (lance-graph-contract) is a reasoning-level gate. +//! `CausalEdge64::revision` (causal-edge) is arithmetic. This probe is the +//! orchestration between them, kept here, above both: the register never sees +//! a horizon, and the gate never computes a truth value. +//! +//! The claim pinned: repeated echo or closed-cycle encounters cannot mint +//! confidence, because the gate never admits them to the register. The +//! register itself would happily pool the same evidence again; that is why +//! the gate has to sit above it. + +use causal_edge::CausalEdge64; +use lance_graph_contract::revision::{ + BasisView, CodebookId, EncounterEvidence, EvidentialEffect, GadamerRevision, GrammarId, + HorizonId, InterpretiveHorizon, LanguageId, LensId, QuestionId, RevisionKind, RevisionPolicy, +}; + +fn horizon(roots: u64) -> InterpretiveHorizon<(), u64> { + InterpretiveHorizon { + id: HorizonId(1), + awareness: (), + question: QuestionId(1), + language: LanguageId(1), + grammar: GrammarId(1), + codebook: CodebookId(1), + lens: LensId(1), + projected_claims: 0b1, + independent_roots: roots, + inherited_roots: 0, + unresolved_tension: 0, + revision_index: 0, + } +} + +fn encounter(roots: u64) -> EncounterEvidence { + EncounterEvidence { + proposed_claims: 0b1, // the same working whole + independent_roots: roots, + inherited_roots: 0, + resistance: 0, + contradictions: 0, + affected_parts: 0, + } +} + +fn edge(f: u8, c: u8) -> CausalEdge64 { + let mut e = CausalEdge64(0); + e.set_frequency_u8(f); + e.set_confidence_u8(c); + e +} + +/// The orchestration: revise only what the gate admits. +fn orchestrate( + belief: CausalEdge64, + evidence: CausalEdge64, + effect: EvidentialEffect, +) -> CausalEdge64 { + match effect { + EvidentialEffect::IncreaseEligible => belief.revision(evidence), + EvidentialEffect::NoIncrease | EvidentialEffect::Suspend => belief, + } +} + +/// Run `rounds` encounters through gate + register; the encounter for round +/// `k` contacts `roots_of(k)` and the ancestry already holds `known`. +fn run( + rounds: u32, + cycle: bool, + roots_of: impl Fn(u32) -> u64, +) -> (CausalEdge64, Vec) { + let mut belief = edge(200, 100); + let evidence = edge(200, 100); + let mut known = 0b1u64; + let mut kinds = Vec::new(); + for k in 0..rounds { + let roots = roots_of(k); + let ancestry = BasisView { + ancestry_independent_roots: known, + ancestry_derived_roots: 0, + ancestor_claims: 0b1, + closes_cycle: cycle, + }; + let delta = GadamerRevision.revise(&horizon(known), &encounter(roots), &ancestry); + kinds.push(delta.kind); + belief = orchestrate(belief, evidence, delta.evidential_effect); + known |= roots; + } + (belief, kinds) +} + +/// Echo: the same root re-read ten times. The gate never admits it, so the +/// register never runs and confidence does not move. +#[test] +fn echo_cannot_mint_confidence() { + let (belief, kinds) = run(10, false, |_| 0b1); + assert!(kinds.iter().all(|k| *k == RevisionKind::Echo), "{kinds:?}"); + assert_eq!(belief.confidence_u8(), 100); +} + +/// Closed cycle: the candidate depends on itself. +#[test] +fn a_closed_cycle_cannot_mint_confidence() { + let (belief, kinds) = run(10, true, |_| 0b1); + assert!( + kinds.iter().all(|k| *k == RevisionKind::ClosedCycle), + "{kinds:?}" + ); + assert_eq!(belief.confidence_u8(), 100); +} + +/// Can-fire arm: a genuinely new independent root each round is admitted and +/// revised, so confidence rises. +#[test] +fn new_independent_roots_are_revised() { + let (belief, kinds) = run(10, false, |k| 1u64 << (k + 1)); + assert!( + kinds + .iter() + .all(|k| *k == RevisionKind::IndependentConfirmation), + "{kinds:?}" + ); + assert!(belief.confidence_u8() > 200, "{}", belief.confidence_u8()); +} + +/// Why the gate must sit above the register: the arithmetic alone pools +/// whatever it is given, echo included. +#[test] +fn the_register_alone_would_inflate_an_echo() { + let mut belief = edge(200, 100); + for _ in 0..10 { + belief = belief.revision(edge(200, 100)); + } + assert!(belief.confidence_u8() > 200); +} diff --git a/crates/lance-graph-planner/tests/moore_nars16_probe.rs b/crates/lance-graph-planner/tests/moore_nars16_probe.rs index 20ca03317..37fc01a50 100644 --- a/crates/lance-graph-planner/tests/moore_nars16_probe.rs +++ b/crates/lance-graph-planner/tests/moore_nars16_probe.rs @@ -41,6 +41,7 @@ //! operation. use causal_edge::edge::CausalEdge64; +use causal_edge::isa::{IsaFault, Opcode}; use causal_edge::network::CausalNetwork; use causal_edge::tables::NarsTables; use lance_graph_contract::epistemic_state5::{Epi5Gen, EpistemicState5}; @@ -351,10 +352,17 @@ const OPS: [Op; 5] = [ Op::Syllogize, ]; -fn run(op: Op, x: CausalEdge64, y: CausalEdge64, t: &[Box<[u8; 256 * 256]>; 3]) -> CausalEdge64 { - match op { - Op::ForwardRunning => x.forward(y, &t[0], &t[1], &t[2]), - Op::ForwardWeight => y.forward(x, &t[0], &t[1], &t[2]), +/// `Err` when the weight carries an inference code the CE64 ISA does not +/// execute (`causal_edge::isa::Opcode::decode`). +fn run( + op: Op, + x: CausalEdge64, + y: CausalEdge64, + t: &[Box<[u8; 256 * 256]>; 3], +) -> Result { + Ok(match op { + Op::ForwardRunning => x.forward(y, &t[0], &t[1], &t[2])?, + Op::ForwardWeight => y.forward(x, &t[0], &t[1], &t[2])?, Op::LearnSelf => { let mut e = x; e.learn(y, 0); @@ -370,7 +378,7 @@ fn run(op: Op, x: CausalEdge64, y: CausalEdge64, t: &[Box<[u8; 256 * 256]>; 3]) .expect("fixture builds a chain figure") .conclusion } - } + }) } // ─── Fixtures ─────────────────────────────────────────────────────────── @@ -390,6 +398,9 @@ impl Rng { /// the given witness. Direction is a random sign triple. fn canonical(r: &mut Rng, witness: u8) -> CausalEdge64 { let e = CausalEdge64(r.next()); + // An executable inference code, so `forward` runs on either side. + let op = Opcode::ALL[(r.next() % 5) as usize]; + let e = Field::Energy.set(e, u64::from(op.encoding() as u8 & 0xF)); let e = Field::W.set(e, u64::from(witness)); Field::Epi5.set(e, r.next() % 24) } @@ -425,7 +436,7 @@ fn divergences(mutation: Mutation, rounds: usize) -> usize { for op in OPS { let a = run(op, edges[k], partners[k], &t); let b = run(op, moore, partners[k], &t); - if observable(a) != observable(b) { + if a.map(observable) != b.map(observable) { diff += 1; } } @@ -504,7 +515,7 @@ fn all_sixteen_energy_encodings_drive_forward_identically() { assert_eq!(Field::Energy.get(m), nibble); let a = run(Op::ForwardWeight, edges[k], partners[k], &t); let b = run(Op::ForwardWeight, m, partners[k], &t); - assert_eq!(observable(a), observable(b), "nibble {nibble}"); + assert_eq!(a.map(observable), b.map(observable), "nibble {nibble}"); } } } @@ -524,7 +535,9 @@ fn reads(field: Field) -> Vec<(String, Field)> { let (x, y) = (edges[0], partners[0]); let bits = (1u64 << field.span().1) - 1; let x2 = field.set(x, (field.get(x) + 1 + r.next() % bits) & bits); - let (a, b) = (run(op, x, y, &t), run(op, x2, y, &t)); + let (Ok(a), Ok(b)) = (run(op, x, y, &t), run(op, x2, y, &t)) else { + continue; + }; for f in FIELDS { if f != field && f.get(a) != f.get(b) { let key = (format!("{op:?}"), f); @@ -567,7 +580,10 @@ fn pearl_energy_and_plasticity_are_read() { let (edges, _, partners) = tenant_fixture(&mut r); let x = Field::Pearl.set(edges[0], 0b111); let y = Field::Pearl.set(partners[0], 0b101); - assert_eq!(Field::Pearl.get(run(Op::ForwardRunning, x, y, &t)), 0b101); + assert_eq!( + Field::Pearl.get(run(Op::ForwardRunning, x, y, &t).unwrap()), + 0b101 + ); } // ─── D: ISA observational equivalence ─────────────────────────────────── @@ -602,8 +618,8 @@ fn the_equivalence_is_observational_not_bitwise() { let (edges, polarity, partners) = tenant_fixture(&mut r); let tenant = MooreTenant::project(edges, polarity, Mutation::None).unwrap(); for k in 0..8 { - let a = run(Op::ForwardWeight, edges[k], partners[k], &t); - let b = run(Op::ForwardWeight, tenant.operand(k).edge, partners[k], &t); + let a = run(Op::ForwardWeight, edges[k], partners[k], &t).unwrap(); + let b = run(Op::ForwardWeight, tenant.operand(k).edge, partners[k], &t).unwrap(); assert_eq!(observable(a), observable(b)); raw_differs += usize::from(a.0 != b.0); } @@ -655,8 +671,12 @@ fn polarity_reverses_the_relation_and_leaves_plasticity_alone() { let b = MooreTenant::project(edges, polarity, Mutation::None).unwrap(); for k in 0..8 { assert_eq!( - run(Op::LearnSelf, a.operand(k).edge, partners[k], &t).0, - run(Op::LearnSelf, b.operand(k).edge, partners[k], &t).0 + run(Op::LearnSelf, a.operand(k).edge, partners[k], &t) + .unwrap() + .0, + run(Op::LearnSelf, b.operand(k).edge, partners[k], &t) + .unwrap() + .0 ); } } diff --git a/docs/architecture/ce64-semantic-upper-half.md b/docs/architecture/ce64-semantic-upper-half.md index 05f3ac83c..dba995d44 100644 --- a/docs/architecture/ce64-semantic-upper-half.md +++ b/docs/architecture/ce64-semantic-upper-half.md @@ -44,6 +44,22 @@ as current behaviour and the diagram's name as a proposed interpretation. - **SPO alignment.** The payload, frequency and confidence feed learning and calibration; certification is not derived from them. +## Encoding, reading, operation + +Three things are kept apart: + +- **Physical encoding**: which bits a field occupies (`layout.rs`). +- **Declared reading**: what those bits mean for a given tenant. The S/P/O + sign triad on bits 43..45 is the one reading implemented today. It does + not oblige every future tenant to read those bits the same way, and a + different reading (for example a Moore slot plus polarity, with the axis + fixed by the tenant's HHTL address) does not reconstruct the sign triad. + Readings are told apart by a versioned binding, never inferred. +- **ISA operation**: what an instruction computes on the declared reading + (`crates/causal-edge/src/isa.rs`). The decoder executes only the + implemented inference codes, and each instruction declares which fields + it reads, computes, passes through and overwrites. + ## Open - Whether bits 43..52 should be re-read as orientation, activation and