From 040c81e6d392c11364728228dfae706a4381a7c8 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 14 Oct 2026 05:31:58 +0000 Subject: [PATCH 1/4] causal-edge: exact truth codes for deduction, induction, abduction A register holds f and c as u8 codes. execute (forward and the named register methods) and syllogize decoded them to f32, applied the law with rounding at every step, and packed with (v * 255).round(). That is off by one code on 2,413 of 2^32 inputs for deduction and 4,352 each for induction and abduction. isa::truth::code computes each law in integers and rounds once, half up; Opcode::truth_code routes the three rules there (revision and synthesis keep the f32 path, unchanged). The f32 functions stay for real-valued callers. The oracle and the probe are harvested from #1544 (D-NALP-4): an independent integer oracle in tests/common/truth_law.rs, hand-computed codes, two half-up ties, the OpenNARS nal1.1 outputs, and register tests on exactly the inputs where the f32 path was off. The exhaustive probe (examples/truth_exact_probe.rs) finds 0 differences from the oracle over 2^32 inputs per law. The legacy golden capture is unchanged. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_011BMJnDBAfzcuQh5HeT39Rh --- .../causal-edge/examples/truth_exact_probe.rs | 86 +++++++ crates/causal-edge/src/edge.rs | 16 +- crates/causal-edge/src/isa.rs | 74 ++++++ crates/causal-edge/src/syllogism.rs | 14 +- crates/causal-edge/tests/ce64_truth_exact.rs | 234 ++++++++++++++++++ crates/causal-edge/tests/common/mod.rs | 1 + crates/causal-edge/tests/common/truth_law.rs | 47 ++++ 7 files changed, 457 insertions(+), 15 deletions(-) create mode 100644 crates/causal-edge/examples/truth_exact_probe.rs create mode 100644 crates/causal-edge/tests/ce64_truth_exact.rs create mode 100644 crates/causal-edge/tests/common/mod.rs create mode 100644 crates/causal-edge/tests/common/truth_law.rs diff --git a/crates/causal-edge/examples/truth_exact_probe.rs b/crates/causal-edge/examples/truth_exact_probe.rs new file mode 100644 index 000000000..4a9588560 --- /dev/null +++ b/crates/causal-edge/examples/truth_exact_probe.rs @@ -0,0 +1,86 @@ +//! Exhaustive check of the exact truth codes, over every input +//! (`(f1, c1, f2, c2)` ∈ 256⁴ = 2³² rows per law). +//! +//! For deduction, induction and abduction it counts the rows where +//! - `truth::code` (what the register paths pack) differs from the +//! independent oracle in `tests/common/truth_law.rs` (must be 0), and +//! - the `f32` functions, packed with `(v · 255).round()`, differ from it +//! (the error the exact codes remove). +//! +//! Run: `cargo run --release -p causal-edge --example truth_exact_probe`. + +#[path = "../tests/common/truth_law.rs"] +mod truth_law; + +use causal_edge::isa::{truth, Opcode}; +use std::thread; + +type Law = truth_law::Law; + +const LAWS: [(&str, Opcode, Law, Law); 3] = [ + ( + "deduction", + Opcode::Deduction, + truth::code::deduction, + truth_law::deduction, + ), + ( + "induction", + Opcode::Induction, + truth::code::induction, + truth_law::induction, + ), + ( + "abduction", + Opcode::Abduction, + truth::code::abduction, + truth_law::abduction, + ), +]; + +fn f32_path(op: Opcode, f1: u8, c1: u8, f2: u8, c2: u8) -> (u8, u8) { + let d = |x: u8| f32::from(x) / 255.0; + let (f, c) = op.truth(d(f1), d(c1), d(f2), d(c2)); + (truth::pack(f), truth::pack(c)) +} + +fn main() { + println!( + "tier: avx512f={} avx2={} (scalar probe; exactness, not speed)", + cfg!(target_feature = "avx512f"), + cfg!(target_feature = "avx2") + ); + println!("rows per law: 2^32 = {}", 1u64 << 32); + println!("{:<10} {:>14} {:>14}", "law", "code != law", "f32 != law"); + for (name, op, code, oracle) in LAWS { + let threads = 8u16; + let (code_off, f32_off) = thread::scope(|s| { + let hs: Vec<_> = (0..threads) + .map(|t| { + s.spawn(move || { + let (mut a, mut b) = (0u64, 0u64); + let mut f1 = t; + while f1 < 256 { + let f1b = f1 as u8; + for c1 in 0..=255u8 { + for f2 in 0..=255u8 { + for c2 in 0..=255u8 { + let want = oracle(f1b, c1, f2, c2); + a += u64::from(code(f1b, c1, f2, c2) != want); + b += u64::from(f32_path(op, f1b, c1, f2, c2) != want); + } + } + } + f1 += threads; + } + (a, b) + }) + }) + .collect(); + hs.into_iter() + .map(|h| h.join().expect("worker")) + .fold((0, 0), |x, y| (x.0 + y.0, x.1 + y.1)) + }); + println!("{name:<10} {code_off:>14} {f32_off:>14}"); + } +} diff --git a/crates/causal-edge/src/edge.rs b/crates/causal-edge/src/edge.rs index d6a3ef2e7..fee1b1cf4 100644 --- a/crates/causal-edge/src/edge.rs +++ b/crates/causal-edge/src/edge.rs @@ -768,7 +768,7 @@ impl CausalEdge64 { /// runs after decoding the weight's code. /// /// - S/P/O: composed per plane through `compose`; - /// - truth: `op`'s canonical truth function ([`Opcode::truth`]); + /// - truth: `op`'s truth codes ([`Opcode::truth_code`]); /// - Pearl mask: AND of both operands; /// - inference field: `op`'s own encoding; /// - direction and plasticity: passed through from `rhs`; @@ -783,11 +783,11 @@ impl CausalEdge64 { 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(), + let (f_out, c_out) = op.truth_code( + self.frequency_u8(), + self.confidence_u8(), + rhs.frequency_u8(), + rhs.confidence_u8(), ); let mask_out = @@ -802,8 +802,8 @@ impl CausalEdge64 { s_out, p_out, o_out, - (f_out.clamp(0.0, 1.0) * 255.0).round() as u8, - (c_out.clamp(0.0, 1.0) * 255.0).round() as u8, + f_out, + c_out, mask_out, rhs.direction(), // TODO: recompute from composed palette dim0 signs op.inference_type(), diff --git a/crates/causal-edge/src/isa.rs b/crates/causal-edge/src/isa.rs index ff35b7f22..a7098eb92 100644 --- a/crates/causal-edge/src/isa.rs +++ b/crates/causal-edge/src/isa.rs @@ -198,6 +198,26 @@ impl Opcode { Opcode::Synthesis => truth::synthesis(f1, c1, f2, c2), } } + + /// The truth codes a register gets: `f` and `c` as `u8` codes (`x / 255`) + /// in and out. This is what `execute`, `forward` and `syllogize` pack. + /// + /// Deduction, induction and abduction are exact ([`truth::code`]): the + /// law's value rounded once, half up. Revision and synthesis still go + /// through the `f32` functions and are packed with `(v · 255).round()`. + #[inline] + pub fn truth_code(self, f1: u8, c1: u8, f2: u8, c2: u8) -> (u8, u8) { + match self { + Opcode::Deduction => truth::code::deduction(f1, c1, f2, c2), + Opcode::Induction => truth::code::induction(f1, c1, f2, c2), + Opcode::Abduction => truth::code::abduction(f1, c1, f2, c2), + Opcode::Revision | Opcode::Synthesis => { + let d = |x: u8| f32::from(x) / 255.0; + let (f, c) = self.truth(d(f1), d(c1), d(f2), d(c2)); + (truth::pack(f), truth::pack(c)) + } + } + } } /// The canonical NARS truth functions (evidence horizon `k = 1`). @@ -265,6 +285,60 @@ pub mod truth { pub fn synthesis(f1: f32, c1: f32, f2: f32, c2: f32) -> (f32, f32) { ((f1 + f2) / 2.0, (c1 + c2) / 2.0) } + + /// A value in `[0, 1]` as a `u8` code: `(v.clamp(0, 1) · 255).round()`. + /// `NaN` packs as 0. + #[inline] + pub fn pack(v: f32) -> u8 { + (v.clamp(0.0, 1.0) * 255.0).round() as u8 + } + + /// The same laws on `u8` codes (`x` stands for `x / 255`), exact. + /// + /// Each value is computed in integers and rounded once, half up, into a + /// code. The `f32` functions above round at every step, so packing their + /// result is off by one code on some inputs: measured over all 2³² + /// inputs, 2,413 rows for deduction and 4,352 each for induction and + /// abduction (`examples/truth_exact_probe.rs`). These functions are what + /// the register paths pack. + pub mod code { + const K1: u64 = 255; + const K3: u64 = 255 * 255 * 255; + + /// `round(p / q)`, half up, for `p ≤ q · 255` and `q > 0`. + #[inline] + fn round_div(p: u64, q: u64) -> u8 { + ((2 * p + q) / (2 * q)) as u8 + } + + /// `c = w / (w + 1)` with `w = w_num / 255³`, as a code. + #[inline] + fn w2c(w_num: u64) -> u8 { + round_div(K1 * w_num, w_num + K3) + } + + /// Deduction: `f = f1·f2`, `c = f1·f2·c1·c2`. + #[inline] + pub fn deduction(f1: u8, c1: u8, f2: u8, c2: u8) -> (u8, u8) { + let ff = u64::from(f1) * u64::from(f2); + ( + round_div(ff, K1), + round_div(ff * u64::from(c1) * u64::from(c2), K3), + ) + } + + /// Induction: `f = f2`, `c = w/(w+1)` with `w = f1·c1·c2`. + #[inline] + pub fn induction(f1: u8, c1: u8, f2: u8, c2: u8) -> (u8, u8) { + (f2, w2c(u64::from(f1) * u64::from(c1) * u64::from(c2))) + } + + /// Abduction: `f = f1`, `c = w/(w+1)` with `w = f2·c1·c2`. + #[inline] + pub fn abduction(f1: u8, c1: u8, f2: u8, c2: u8) -> (u8, u8) { + (f1, w2c(u64::from(f2) * u64::from(c1) * u64::from(c2))) + } + } } /// A CE64 field, v2 layout. diff --git a/crates/causal-edge/src/syllogism.rs b/crates/causal-edge/src/syllogism.rs index fb7ff33da..6dcf39392 100644 --- a/crates/causal-edge/src/syllogism.rs +++ b/crates/causal-edge/src/syllogism.rs @@ -197,12 +197,12 @@ impl CausalEdge64 { // Conclusion truth — canonical NARS rule for the figure (premise order // self, other). Mirrors `ndarray::hpc::nars` and `forward`. - let (f1, c1) = (self.frequency(), self.confidence()); - let (f2, c2) = (other.frequency(), other.confidence()); + let (f1, c1) = (self.frequency_u8(), self.confidence_u8()); + let (f2, c2) = (other.frequency_u8(), other.confidence_u8()); let (f, c) = match figure { - 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), + Figure::Chain | Figure::ChainRev => crate::isa::truth::code::deduction(f1, c1, f2, c2), + Figure::SharedSubject => crate::isa::truth::code::induction(f1, c1, f2, c2), + Figure::SharedObject => crate::isa::truth::code::abduction(f1, c1, f2, c2), }; // Pearl mask: AND (only planes active in both survive) — as `forward`. @@ -218,8 +218,8 @@ impl CausalEdge64 { cs, cp, co, - (f.clamp(0.0, 1.0) * 255.0).round() as u8, - (c.clamp(0.0, 1.0) * 255.0).round() as u8, + f, + c, mask, 0, // direction: neutral; recomputed from composed palette downstream figure.rule(), diff --git a/crates/causal-edge/tests/ce64_truth_exact.rs b/crates/causal-edge/tests/ce64_truth_exact.rs new file mode 100644 index 000000000..bed166de4 --- /dev/null +++ b/crates/causal-edge/tests/ce64_truth_exact.rs @@ -0,0 +1,234 @@ +//! The exact truth codes of deduction, induction and abduction. +//! +//! A register holds `f` and `c` as `u8` codes (`x / 255`). The conclusion is +//! the law's exact value rounded once, half up, into a code. These tests pin +//! the crate against an oracle written independently of it +//! (`common/truth_law.rs`), against hand-computed values, and against the +//! OpenNARS output for nal1.1; and they check that the register paths +//! (`execute`, `forward`, `syllogize`) pack exactly those codes. + +mod common; + +use causal_edge::isa::{truth, Opcode}; +use causal_edge::{CausalEdge64, Compose}; +use common::truth_law::{self as law, Law}; + +const LAWS: [(Opcode, Law); 3] = [ + (Opcode::Deduction, law::deduction), + (Opcode::Induction, law::induction), + (Opcode::Abduction, law::abduction), +]; + +fn code_fn(op: Opcode) -> Law { + match op { + Opcode::Deduction => truth::code::deduction, + Opcode::Induction => truth::code::induction, + Opcode::Abduction => truth::code::abduction, + _ => unreachable!(), + } +} + +/// Hand-computed: f = 128·128/255 = 64.25 → 64; c = 128⁴/255³ = 16.19 → 16. +/// f = 255·200/255 = 200; c = 255·200·255·100/255³ = 78.43 → 78. +#[test] +fn deduction_matches_hand_computed_codes() { + assert_eq!(truth::code::deduction(128, 128, 128, 128), (64, 16)); + assert_eq!(truth::code::deduction(255, 255, 200, 100), (200, 78)); +} + +/// The rounding is half up. All-ones evidence gives w = 1, c = 127.5 codes, +/// 128 half up (127 rounding down). That tie cannot reject ties-to-even, so +/// a second one has an even lower integer: f1 = 195 gives c = 255·195/450 = +/// 110.5 codes, 111 half up and 110 ties-to-even. +#[test] +fn a_tie_rounds_up() { + assert_eq!(truth::code::induction(255, 255, 255, 255), (255, 128)); + assert_eq!(truth::code::abduction(255, 255, 255, 255), (255, 128)); + assert_eq!(truth::code::induction(195, 255, 255, 255), (255, 111)); + assert_eq!(truth::code::abduction(255, 255, 195, 255), (255, 111)); +} + +/// Induction and abduction take the frequency from opposite premises; a +/// premise swap must change the answer. +#[test] +fn induction_and_abduction_are_mirror_images() { + let (f1, c1, f2, c2) = (255, 230, 51, 200); + assert_eq!( + truth::code::induction(f1, c1, f2, c2), + truth::code::abduction(f2, c1, f1, c2) + ); + assert_ne!( + truth::code::induction(f1, c1, f2, c2), + truth::code::abduction(f1, c1, f2, c2) + ); +} + +#[test] +fn no_evidence_no_confidence() { + for (op, _) in LAWS { + let f = code_fn(op); + assert_eq!(f(255, 0, 255, 255).1, 0, "{op:?}"); + assert_eq!(f(255, 255, 255, 0).1, 0, "{op:?}"); + } +} + +/// OpenNARS at `4d1bdb0`, nal1.1: `%1.00;0.90%` premises give `%1.00;0.81%` +/// by deduction and `%1.00;0.45%` by induction. The printout has two +/// decimals; 0.9 is code 230. +#[test] +fn matches_opennars_nal1_1() { + let two = |x: u8| format!("{:.2}", f64::from(x) / 255.0); + let (f, c) = truth::code::deduction(255, 230, 255, 230); + assert_eq!((two(f), two(c)), ("1.00".into(), "0.81".into())); + let (f, c) = truth::code::induction(255, 230, 255, 230); + assert_eq!((two(f), two(c)), ("1.00".into(), "0.45".into())); +} + +fn grid() -> Vec { + (0..=255u16).step_by(5).map(|x| x as u8).collect() +} + +/// The crate's codes equal the independent oracle on a stratified grid +/// (every 5th code, 52⁴ ≈ 7.3M rows per law). The exhaustive 2³² check is +/// `examples/truth_exact_probe.rs`. +#[test] +fn codes_equal_the_oracle_on_a_grid() { + let g = grid(); + for (op, oracle) in LAWS { + let mine = code_fn(op); + for &f1 in &g { + for &c1 in &g { + for &f2 in &g { + for &c2 in &g { + assert_eq!( + mine(f1, c1, f2, c2), + oracle(f1, c1, f2, c2), + "{op:?}({f1},{c1},{f2},{c2})" + ); + } + } + } + } + } +} + +/// The `f32` arithmetic the register paths used before: decode `x / 255`, +/// apply the law, pack with `(v · 255).round()`. +fn f32_path(op: Opcode, f1: u8, c1: u8, f2: u8, c2: u8) -> (u8, u8) { + let d = |x: u8| f32::from(x) / 255.0; + let (f, c) = op.truth(d(f1), d(c1), d(f2), d(c2)); + let p = |v: f32| (v.clamp(0.0, 1.0) * 255.0).round() as u8; + (p(f), p(c)) +} + +/// Rows where the old `f32` path and the exact law disagree. These are the +/// rows the register tests must cover; without them a register path still on +/// `f32` would pass. +/// +/// Deduction: the every-5th grid (it disagrees on 12 of its rows). +/// Induction and abduction disagree on no grid row, so their search is +/// exhaustive over the three codes their confidence depends on, with the +/// passed-through frequency fixed at 200. +fn disagreeing_rows(op: Opcode, oracle: Law) -> Vec<[u8; 4]> { + let mut rows = Vec::new(); + let mut check = |r: [u8; 4]| { + let [f1, c1, f2, c2] = r; + if f32_path(op, f1, c1, f2, c2) != oracle(f1, c1, f2, c2) { + rows.push(r); + } + }; + match op { + Opcode::Deduction => { + let g = grid(); + for &f1 in &g { + for &c1 in &g { + for &f2 in &g { + for &c2 in &g { + check([f1, c1, f2, c2]); + } + } + } + } + } + Opcode::Induction | Opcode::Abduction => { + for a in 0..=255u8 { + for c1 in 0..=255u8 { + for c2 in 0..=255u8 { + // Induction weighs f1, abduction f2. + check(if op == Opcode::Induction { + [a, c1, 200, c2] + } else { + [200, c1, a, c2] + }); + } + } + } + } + _ => unreachable!(), + } + rows +} + +fn edge(s: u8, o: u8, f: u8, c: u8) -> CausalEdge64 { + let mut e = CausalEdge64(0); + e.set_s_idx(s); + e.set_p_idx(7); + e.set_o_idx(o); + e.set_frequency_u8(f); + e.set_confidence_u8(c); + e +} + +fn fc(e: CausalEdge64) -> (u8, u8) { + (e.frequency_u8(), e.confidence_u8()) +} + +/// `execute` (what `forward` and the named register methods run) packs the +/// exact codes, on every grid row where the `f32` path was off by one. +#[test] +fn register_methods_pack_the_exact_codes() { + let t: Box<[u8; 65536]> = vec![0u8; 65536].into_boxed_slice().try_into().unwrap(); + let c = Compose { + s: &t, + p: &t, + o: &t, + }; + for (op, oracle) in LAWS { + let rows = disagreeing_rows(op, oracle); + // Anti-vacuity: the f32 path really is off on these inputs. + assert!(!rows.is_empty(), "{op:?}: no disagreeing row"); + eprintln!("{op:?}: {} rows where f32 was off", rows.len()); + for [f1, c1, f2, c2] in rows { + let (a, b) = (edge(1, 2, f1, c1), edge(2, 3, f2, c2)); + assert_eq!( + fc(a.execute(op, b, c)), + oracle(f1, c1, f2, c2), + "{op:?}({f1},{c1},{f2},{c2})" + ); + } + } +} + +/// `syllogize` packs the exact codes for each figure's rule, premise order +/// (self, other), on the same rows. +#[test] +fn syllogize_packs_the_exact_codes() { + for (op, oracle) in LAWS { + for [f1, c1, f2, c2] in disagreeing_rows(op, oracle) { + // Chain (o1 == s2) → deduction; shared subject → induction; + // shared object → abduction. + let (a, b) = match op { + Opcode::Deduction => (edge(1, 2, f1, c1), edge(2, 3, f2, c2)), + Opcode::Induction => (edge(1, 2, f1, c1), edge(1, 3, f2, c2)), + Opcode::Abduction => (edge(1, 3, f1, c1), edge(2, 3, f2, c2)), + _ => unreachable!(), + }; + let s = a.syllogize(b).expect("a figure"); + assert_eq!( + fc(s.conclusion), + oracle(f1, c1, f2, c2), + "{op:?}({f1},{c1},{f2},{c2})" + ); + } + } +} diff --git a/crates/causal-edge/tests/common/mod.rs b/crates/causal-edge/tests/common/mod.rs new file mode 100644 index 000000000..1e5803438 --- /dev/null +++ b/crates/causal-edge/tests/common/mod.rs @@ -0,0 +1 @@ +pub mod truth_law; diff --git a/crates/causal-edge/tests/common/truth_law.rs b/crates/causal-edge/tests/common/truth_law.rs new file mode 100644 index 000000000..d383b0258 --- /dev/null +++ b/crates/causal-edge/tests/common/truth_law.rs @@ -0,0 +1,47 @@ +//! The exact NAL truth laws over `u8` codes, written independently of the +//! crate (harvested from lance-graph #1544, D-NALP-4). +//! +//! A code `x` stands for `x / 255`. Each law is computed in exact integer +//! arithmetic and rounded once, half up, back into a code. Formulas (horizon +//! `k = 1`): +//! - deduction: `f = f1·f2`, `c = f1·f2·c1·c2`; +//! - induction: `f = f2`, `c = w / (w + 1)`, `w = f1·c1·c2`; +//! - abduction: `f = f1`, `c = w / (w + 1)`, `w = f2·c1·c2`. + +#![allow(dead_code)] + +/// `round(p / q)`, half up, for `p ≥ 0`, `q > 0`. +pub fn round_div(p: u64, q: u64) -> u8 { + let r = (2 * p + q) / (2 * q); + u8::try_from(r).expect("a law value lies in [0, 1]") +} + +const K1: u64 = 255; +const K3: u64 = 255 * 255 * 255; + +/// `w = w_num / 255³`, `c = w / (w + 1) = w_num / (w_num + 255³)`. +fn w2c(w_num: u64) -> u8 { + round_div(255 * w_num, w_num + K3) +} + +/// `(f, c)` codes of deduction. +pub fn deduction(f1: u8, c1: u8, f2: u8, c2: u8) -> (u8, u8) { + let ff = u64::from(f1) * u64::from(f2); + ( + round_div(ff, K1), + round_div(ff * u64::from(c1) * u64::from(c2), K3), + ) +} + +/// `(f, c)` codes of induction. +pub fn induction(f1: u8, c1: u8, f2: u8, c2: u8) -> (u8, u8) { + (f2, w2c(u64::from(f1) * u64::from(c1) * u64::from(c2))) +} + +/// `(f, c)` codes of abduction. +pub fn abduction(f1: u8, c1: u8, f2: u8, c2: u8) -> (u8, u8) { + (f1, w2c(u64::from(f2) * u64::from(c1) * u64::from(c2))) +} + +/// A two-premise law, for iteration. +pub type Law = fn(u8, u8, u8, u8) -> (u8, u8); From b0b3fb75e12462673258d960625457f5d35e4490 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 14 Oct 2026 05:35:07 +0000 Subject: [PATCH 2/4] board: D-NALP-4 exact truth codes in isa::truth (measured, open items) Entry 2026-10-14-isa-truth-exact-codes.md with the exhaustive measurement and the open items (revision/synthesis not exact; whether a lane terminal is still needed). STATUS_BOARD D-NALP-4 -> partial, in PR. Plan 4 C gets a MEASURED note; the rescope of 4 B/C stays open. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_011BMJnDBAfzcuQh5HeT39Rh --- .claude/board/STATUS_BOARD.md | 2 +- .../2026-10-14-isa-truth-exact-codes.md | 50 +++++++++++++++++++ .claude/board/entries/README.md | 3 +- .claude/plans/nal-polyfill-v1.md | 8 +++ 4 files changed, 61 insertions(+), 2 deletions(-) create mode 100644 .claude/board/entries/2026-10-14-isa-truth-exact-codes.md diff --git a/.claude/board/STATUS_BOARD.md b/.claude/board/STATUS_BOARD.md index 56d26dc97..5be1a1b64 100644 --- a/.claude/board/STATUS_BOARD.md +++ b/.claude/board/STATUS_BOARD.md @@ -104,7 +104,7 @@ Plan: `.claude/plans/nal-polyfill-v1.md`. Template: D-SQLP. No opcode, tenant or | **D-NALP-1** | Statement layout + declared ClassView reading; additive `WideFieldMask` projection path on `ClassView`; binder's mask; term width decision | Partial: #1525 merged `08635ed` (NodeGuid reading `nal-statement-v1`, term width u16, aperture selection); ClassView wide projection and binder mask Queued | only the mask's lanes are read; undeclared reading and masked-out field refuse; Small = Wide answers | | **D-NALP-2** | Query procedures: select, truth threshold, choice by confidence, support count | Shipped #1525 `08635ed` (`crates/lance-graph-nal`: NodeGuid key, byte apertures; 7 oracle tests, 7 disable runs red; 19–248 ns at 1,048,576 rows); support count and argmax not built | equal to a row-at-a-time oracle; one-pattern threshold disable red; no new opcode | | **D-NALP-3** | Revision as `GroupCrossPowerSumsI32` over stored `w`/`f` | Shipped #1538 `4ceaab3` (`nal::Revision`, key = evidence class from the stamps; refuses overlap and missing provenance; 11 tests, 7 disable runs red; ONA's mid-fold saturation is a documented divergence, the fold keeps the exact sum) | equal to exact integer revision; OpenNARS revision points; duplicate evidence counts once | -| **D-NALP-4** | Per-row truth law into a lane: `MapPairU8` vs fixed-point multiply-high | Queued | insufficiency proof; per-row parity with `isa::truth`, error in codes; one shape also serves SQL nullable arithmetic | +| **D-NALP-4** | Per-row truth law into a lane: `MapPairU8` vs fixed-point multiply-high | Partial, in PR: the exact scalar law for deduction / induction / abduction is `causal_edge::isa::truth::code`, packed by `execute` and `syllogize` (0 of 2³² rows off the oracle; harvested from draft #1544); whether a lane terminal is still needed is open (entry `2026-10-14-isa-truth-exact-codes.md`) | insufficiency proof; per-row parity with `isa::truth`, error in codes; one shape also serves SQL nullable arithmetic | | **D-NALP-5** | Deduction / induction / abduction / analogy over populations | Queued (after D-NALP-4) | equals pairwise scalar rule; abduction direction test red for the reversed statement | | **D-NALP-6** | `lance-graph-nal`: typed `nal::{Operation}` surface (`NalOp`), parser (tokens only), binder over the reverse label index, `NAL::narsese()`, typed refusals | Queued | text and typed calls give byte-identical `Program`s; no string in the plan, rows or wire; ambiguous / unknown label refuses; lowers from the bound plan; no fallback; no `Program` outside procedures | | **D-NALP-7** | Oracle parity on NAL-1/2 fixtures vs pinned OpenNARS, `jc::reliability` | Queued | within D-HL-4 tolerance per rule | diff --git a/.claude/board/entries/2026-10-14-isa-truth-exact-codes.md b/.claude/board/entries/2026-10-14-isa-truth-exact-codes.md new file mode 100644 index 000000000..f030e360a --- /dev/null +++ b/.claude/board/entries/2026-10-14-isa-truth-exact-codes.md @@ -0,0 +1,50 @@ +# 2026-10-14 — Exact truth codes in `causal_edge::isa::truth` (D-NALP-4 harvest) + +**Status:** IN PR (branch `ccr-9f3b8075-74u47l-truth-exact`). Harvested from +the draft #1544, which stays open as a reminder and is not merged. + +**DECISION:** the exact per-row truth law lives where NARS truth already +lives, in `causal_edge::isa::truth`, not in a second substrate (a lane +terminal plus `nal::Deduction` in `lance-graph-nal`). + +**SCOPE:** deduction, induction, abduction. `truth::code::{deduction, +induction, abduction}` take and return `u8` codes (`x / 255`), compute in +integers and round once, half up. `Opcode::truth_code` routes the three +rules there; `execute` (so `forward` and the named register methods) and +`syllogize` pack its result. Revision and synthesis keep the `f32` path, +unchanged. The `f32` functions stay for real-valued callers. + +**MEASURED** (`cargo run --release -p causal-edge --example +truth_exact_probe`, all 2³² inputs per law, 8 threads, 37.7 s): + +| law | `truth::code` ≠ oracle | old `f32` path ≠ oracle | +|---|---:|---:| +| deduction | 0 | 2,413 | +| induction | 0 | 4,352 | +| abduction | 0 | 4,352 | + +Every old miss is one confidence code. The oracle +(`crates/causal-edge/tests/common/truth_law.rs`) is written independently of +the crate. + +**TEST-PINNED** (`tests/ce64_truth_exact.rs`, 8 tests): hand-computed codes; +two half-up ties (127.5 → 128, 110.5 → 111, the second rejects +ties-to-even); the induction/abduction mirror; zero evidence; OpenNARS nal1.1 +at `4d1bdb0` (0.81 deduction, 0.45 induction); the codes equal the oracle on +the every-5th grid; `execute` and `syllogize` pack the oracle's codes on +exactly the inputs where the `f32` path was off (12 deduction rows of the +grid, 17 induction and 17 abduction rows of an exhaustive three-code scan; +the grid alone holds none for induction or abduction). Disable runs, each +red: `truth_code` back to `f32` (register test), `syllogize` deduction back +to `f32` (syllogize test), round down, ties-to-even. The legacy golden +capture (`ce64_isa_golden.rs`, 126 words) is unchanged: none of its inputs +is one the `f32` path got wrong. + +**OPEN:** +- Revision and synthesis are not exact. Exact revision has to settle the + both-operands-at-255 case first (today it packs `(0, 0)`, pinned as a known + defect in `ce64_isa_golden.rs`). +- Whether D-NALP-4/5 still need a lane terminal at all, or whether + populations of CE64 registers carry the law (plan §4 B/C). Not decided. +- `cargo clippy -D warnings` on `causal-edge` fails on six lints in code this + change does not touch; CI runs only `cargo test` for the crate. diff --git a/.claude/board/entries/README.md b/.claude/board/entries/README.md index 77bb272d1..6d4ee920e 100644 --- a/.claude/board/entries/README.md +++ b/.claude/board/entries/README.md @@ -25,10 +25,11 @@ index row, (3) no duplicate entry id. Checks 1 and 2 are deliberately opposite directions; the stranding this convention prevents shows up in exactly one of them, never both. -326 entries, 2026-08-06 .. 2026-10-13. +327 entries, 2026-08-06 .. 2026-10-14. | date | entry id | finding | file | |---|---|---|---| +| 2026-10-14 | `D-NALP-4` | | [2026-10-14-isa-truth-exact-codes.md](2026-10-14-isa-truth-exact-codes.md) | | 2026-10-13 | `D-PROD-V4` | | [2026-10-13-production-targets-v4.md](2026-10-13-production-targets-v4.md) | | 2026-10-12 | `D-SAG-1` | | [2026-10-12-software-awareness-graph.md](2026-10-12-software-awareness-graph.md) | | 2026-10-12 | `D-CMR-RESET` | method layer was a second algebra beside the folds and slower than a row loop (430–480 µs vs 283 µs); moved to backup, rebuild as bindings over existing folds | [2026-10-12-session-reset-inventory.md](2026-10-12-session-reset-inventory.md) | diff --git a/.claude/plans/nal-polyfill-v1.md b/.claude/plans/nal-polyfill-v1.md index a6b37e890..985806b95 100644 --- a/.claude/plans/nal-polyfill-v1.md +++ b/.claude/plans/nal-polyfill-v1.md @@ -163,6 +163,14 @@ never twice. The path is: ndarray primitive with parity on every realization row → mask-risc terminal with parity → `FoldDialect` wiring → one `ogar-nal` byte → procedure. +MEASURED 2026-10-14: the exact law is now `causal_edge::isa::truth::code` +(deduction, induction, abduction), integers with one half-up rounding, and +the CE64 register paths pack it; 0 of 2³² inputs per law differ from the +independent oracle, where the old `f32` path differed on 2,413 / 4,352 / +4,352. Whether this section's lane terminal is still needed, or whether +populations of CE64 registers carry the law, is OPEN (entry +`2026-10-14-isa-truth-exact-codes.md`). + ### D. Binding goes through the ClassView, never through hard-coded offsets - A Narsese statement population is a class. Its reading of the bytes From b6518398f0e186bb160375dd1d07799e207219d9 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 14 Oct 2026 05:57:37 +0000 Subject: [PATCH 3/4] board: Gadamer revision invariants G1-G7, Rubikon goal revision R1-R4 DECISION (approved, points 1-4): the Gadamer gate's invariants are frozen, each cited to the test that pins it; the revision layers (gate, CE64 register, folded evidence, Rubikon phases) are kept apart; goal revision runs only in Planning and Evaluation, agreement on a goal is a HorizonFusion with the other party's statement as the new root, and a goal is never revised by counting. Tests for R1-R4 are open. Also records the differential against main for the exact truth codes: 5 of 16,000,000 register results differ, only in the confidence field, by one code; bits 50..52 and 59..63 never change. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_011BMJnDBAfzcuQh5HeT39Rh --- .../2026-10-14-isa-truth-exact-codes.md | 7 +++ .../2026-10-14-revision-layer-invariants.md | 60 +++++++++++++++++++ .claude/board/entries/README.md | 3 +- 3 files changed, 69 insertions(+), 1 deletion(-) create mode 100644 .claude/board/entries/2026-10-14-revision-layer-invariants.md diff --git a/.claude/board/entries/2026-10-14-isa-truth-exact-codes.md b/.claude/board/entries/2026-10-14-isa-truth-exact-codes.md index f030e360a..8bf67facb 100644 --- a/.claude/board/entries/2026-10-14-isa-truth-exact-codes.md +++ b/.claude/board/entries/2026-10-14-isa-truth-exact-codes.md @@ -40,6 +40,13 @@ to `f32` (syllogize test), round down, ties-to-even. The legacy golden capture (`ce64_isa_golden.rs`, 126 words) is unchanged: none of its inputs is one the `f32` path got wrong. +**MEASURED, differential against `main`** (2,000,000 random register-word +pairs, all bits random including 50..52 and 59..63; every path: the five +`execute` opcodes, `syllogize`, `learn`, `revision`; 16,000,000 results): 5 +words differ (3 induction, 1 deduction, 1 abduction), each only in the +confidence field (bits 32..39), by exactly one code. No other bit changed; +`learn`, `revision` and synthesis are bit-identical. + **OPEN:** - Revision and synthesis are not exact. Exact revision has to settle the both-operands-at-255 case first (today it packs `(0, 0)`, pinned as a known diff --git a/.claude/board/entries/2026-10-14-revision-layer-invariants.md b/.claude/board/entries/2026-10-14-revision-layer-invariants.md new file mode 100644 index 000000000..21af818aa --- /dev/null +++ b/.claude/board/entries/2026-10-14-revision-layer-invariants.md @@ -0,0 +1,60 @@ +# 2026-10-14 — Revision layers: Gadamer gate invariants, Rubikon goal revision + +**Status:** DECISION (approved 2026-10-14, points 1–4). The invariants are +TEST-PINNED; points 2–4 are specifications whose tests are OPEN. + +## 1. Gadamer revision: invariants that must never be touched + +`lance_graph_contract::revision::GadamerRevision` decides **whether** and +**in which sense** an encounter revises an interpretive horizon. It is set +algebra over masks (union, intersection, difference, subset over claims, +roots, resistance and contradictions); it never counts. + +| # | invariant | pinned by | +|---|---|---| +| G1 | An echo or a closed cycle earns zero evidential weight (`Echo`, `ClosedCycle` → `NoIncrease`). | `revision.rs`: `repeated_derived_claim_is_an_echo_and_adds_no_weight`, `self_supporting_ancestry_is_a_closed_cycle`; `planner/tests/gadamer_isa_revision.rs`: `echo_cannot_mint_confidence`, `a_closed_cycle_cannot_mint_confidence` | +| G2 | A synthesis must be earned: `HorizonFusion` needs a new independent root; the same contradiction without one is `ContradictionPreserved` → `Suspend`. No `IncreaseEligible` kind is reachable without a new root. | `contradiction_without_a_new_root_suspends_instead_of_synthesising`, `no_increase_eligible_outcome_is_reachable_without_a_new_root`, the `debug_assert` in `revise` | +| G3 | Gadamer, not Hegel: `unresolved_tension` grows by union and is never cleared. | `fusion_accumulates_tension_and_never_clears_prior_tension` | +| G4 | The evidential effect is categorical (`IncreaseEligible` / `NoIncrease` / `Suspend`), deliberately coarser than a confidence. It is never replaced by a number. | the type `EvidentialEffect` | +| G5 | The gate sits above the register: the register never sees a horizon, the gate never computes a truth value. The register alone would inflate an echo. | `gadamer_isa_revision.rs`: `the_register_alone_would_inflate_an_echo`, `new_independent_roots_are_revised` | +| G6 | Eligibility is not acceptance: commit needs `IncreaseEligible` AND a counterfactual verdict `Necessary`; revision outputs stop before any world mutation. | `RevisionVerdict::is_acceptable`, `revision_verdict_alone_cannot_reach_commit` | +| G7 | Revision is relative to a question: the horizon carries `question`, `language`, `grammar`, `codebook`, `lens` and `projected_claims` (the anticipated whole the parts are read against). | the type `InterpretiveHorizon` | + +## 2. The layers, kept apart + +| layer | question | operands | algebra | output | +|---|---|---|---|---| +| Gadamer gate | has understanding moved, and was it earned? | claim / root / resistance / contradiction masks | set algebra | `RevisionKind` + effect | +| CE64 register (`isa::truth`) | how much evidence is pooled? | `(f, c)` codes | arithmetic (exact codes for deduction / induction / abduction, #1548) | a number | +| folded evidence | how often is it observed? | extension masks | AND + popcount at the terminal | a number from counts | +| Rubikon (kanban phases) | committed, and did the action meet the intention? | the intention's phase | phase transitions on a gate | a phase | + +Counting layers answer "how much"; the Gadamer gate answers "whether". A +counting layer runs only after the gate admits the encounter (G5). + +## 3. Specifications (approved, tests OPEN) + +- **R1 — goal revision only outside `CognitiveWork`.** A goal's horizon is + revised in `Planning` (pre-Rubicon, including the veto) and in + `Evaluation` (postactional); never in `CognitiveWork`, where the + intention is shielded (Heckhausen). Matches `alpha-channel-rung-overlay-v1` + §3f ("revision runs in the pre-act window"). OPEN: a test that a goal + revision attempted in `CognitiveWork` is refused, and that + `Evaluation → Plan` reopens the goal. +- **R2 — agreement on a goal is a `HorizonFusion`** between two horizons, + where the other party's statement supplies the new independent root. + Without it: `ContradictionPreserved` → `Suspend`, the disagreement kept. + No new type. OPEN: what counts as an independent root for a person (an + utterance, a signed decision) — a modelling decision. +- **R3 — a goal is never revised by counting.** Evidence may inform + feasibility before the Rubicon; it never decides what the goal is. +- **R4 — evidence-layer folding** (popcount of intersections) runs only under + the Gadamer gate and only for observational statements, never for goals. + +## OPEN (found while checking, pre-existing) + +`execute` writes witness (53..58) and epistemic state (59..63) as 0, and +`syllogize` writes plasticity (50..52) as `0b111` and epistemic state as 0 +(`isa::contracts::{FORWARD, SYLLOGIZE}`). A derived conclusion therefore does +not carry the hydration-set direct/indirect, known/unknown or CARE bits of its +premises. Whether 0 is the right state for a derived edge is not decided. diff --git a/.claude/board/entries/README.md b/.claude/board/entries/README.md index 6d4ee920e..1b55917e6 100644 --- a/.claude/board/entries/README.md +++ b/.claude/board/entries/README.md @@ -25,10 +25,11 @@ index row, (3) no duplicate entry id. Checks 1 and 2 are deliberately opposite directions; the stranding this convention prevents shows up in exactly one of them, never both. -327 entries, 2026-08-06 .. 2026-10-14. +328 entries, 2026-08-06 .. 2026-10-14. | date | entry id | finding | file | |---|---|---|---| +| 2026-10-14 | `revision-layer-invariants` | | [2026-10-14-revision-layer-invariants.md](2026-10-14-revision-layer-invariants.md) | | 2026-10-14 | `D-NALP-4` | | [2026-10-14-isa-truth-exact-codes.md](2026-10-14-isa-truth-exact-codes.md) | | 2026-10-13 | `D-PROD-V4` | | [2026-10-13-production-targets-v4.md](2026-10-13-production-targets-v4.md) | | 2026-10-12 | `D-SAG-1` | | [2026-10-12-software-awareness-graph.md](2026-10-12-software-awareness-graph.md) | From 0e15cff73689c859f56b926bb098995f8b7439bc Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 14 Oct 2026 05:57:52 +0000 Subject: [PATCH 4/4] board: name the file of the G6 test (kanban.rs) Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_011BMJnDBAfzcuQh5HeT39Rh --- .claude/board/entries/2026-10-14-revision-layer-invariants.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.claude/board/entries/2026-10-14-revision-layer-invariants.md b/.claude/board/entries/2026-10-14-revision-layer-invariants.md index 21af818aa..c5e6e72bc 100644 --- a/.claude/board/entries/2026-10-14-revision-layer-invariants.md +++ b/.claude/board/entries/2026-10-14-revision-layer-invariants.md @@ -17,7 +17,7 @@ roots, resistance and contradictions); it never counts. | G3 | Gadamer, not Hegel: `unresolved_tension` grows by union and is never cleared. | `fusion_accumulates_tension_and_never_clears_prior_tension` | | G4 | The evidential effect is categorical (`IncreaseEligible` / `NoIncrease` / `Suspend`), deliberately coarser than a confidence. It is never replaced by a number. | the type `EvidentialEffect` | | G5 | The gate sits above the register: the register never sees a horizon, the gate never computes a truth value. The register alone would inflate an echo. | `gadamer_isa_revision.rs`: `the_register_alone_would_inflate_an_echo`, `new_independent_roots_are_revised` | -| G6 | Eligibility is not acceptance: commit needs `IncreaseEligible` AND a counterfactual verdict `Necessary`; revision outputs stop before any world mutation. | `RevisionVerdict::is_acceptable`, `revision_verdict_alone_cannot_reach_commit` | +| G6 | Eligibility is not acceptance: commit needs `IncreaseEligible` AND a counterfactual verdict `Necessary`; revision outputs stop before any world mutation. | `RevisionVerdict::is_acceptable`; `contract/src/kanban.rs`: `revision_verdict_alone_cannot_reach_commit` | | G7 | Revision is relative to a question: the horizon carries `question`, `language`, `grammar`, `codebook`, `lens` and `projected_claims` (the anticipated whole the parts are read against). | the type `InterpretiveHorizon` | ## 2. The layers, kept apart