diff --git a/.claude/board/STATUS_BOARD.md b/.claude/board/STATUS_BOARD.md index 64841a178..c84644480 100644 --- a/.claude/board/STATUS_BOARD.md +++ b/.claude/board/STATUS_BOARD.md @@ -93,7 +93,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 | In progress (oracle + shape measured: integer-valued `f64` exact on all 2³² rows of the four laws, the table shape off on 10–18 %; kernel and terminal not built; entry `2026-10-13-d-nalp-4-truth-law-shape.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 | @@ -101,6 +101,7 @@ Plan: `.claude/plans/nal-polyfill-v1.md`. Template: D-SQLP. No opcode, tenant or | **D-NALP-9** | `narsese!{}` declared mode via the D-SQLP-4 generator | Blocked (D-SQLP-4) | generated = interpreted; ≤ 1.05× hand-built; no dispatch in hot loop | | **D-NALP-10** | Benchmark, D-SQLP-3 protocol | Queued | answers equal before timing; interpreted ≤ 1.05× hand-built | | **D-NALP-11** | One spelling: quack / cypher-quack / Java route through the procedures | Queued | byte-identical `Program`s; Java `ApiSurfaceTest` green | +| **D-NALP-12** | OGAR Loco → lance-graph R2IL method composition: resolve one OGAR method declaration through a stable method identity and an existing Loco inventory, bind it to a shipped NAL operation (W3 `Revision`), compile through `FoldDialect` into mask-risc, run it over a witnessed belief population | Queued (requested 2026-10-13; starts once W4/W5 have moved far enough). Constraints: `lance-graph-contract` stays dependency-free; no second evaluator, NARS engine or workflow runner; `lance-graph-loco` / `lance-graph-ona` only if each earns its keep | same answer through the typed API as through the OGAR method; missing identity or body, wrong schema/classid/generation, an inventory-local `FnAddr` used as identity, stale scratch across folds, repeated evidence: each refused; OGAR opcode/arity tests and r2sleigh behaviour unchanged; no contract → OGAR edge | ## D-HL — CE64 hypothesis layers over an immutable address (2026-10-12) diff --git a/.claude/board/entries/2026-10-13-d-nalp-4-truth-law-shape.md b/.claude/board/entries/2026-10-13-d-nalp-4-truth-law-shape.md new file mode 100644 index 000000000..759d9b33c --- /dev/null +++ b/.claude/board/entries/2026-10-13-d-nalp-4-truth-law-shape.md @@ -0,0 +1,37 @@ +# 2026-10-13 — D-NALP-4: which realization of the per-row truth laws is exact (W4) + +**Status:** MEASURED (shape exactness); the lane-producing kernel and terminal are OPEN. + +**MEASURED:** `cargo run --release --manifest-path crates/lance-graph-nal/Cargo.toml --example w4_truth_law_probe` +on an AVX-512 host (the probe prints the tier; it is a scalar probe, so it +measures exactness, not speed). Every input, `(f1, c1, f2, c2)` ∈ 256⁴ = 2³² +rows per law, against the exact integer law rounded once, half up +(`crates/lance-graph-nal/tests/common/truth_law.rs`): + +| law | table (256² `u8` laws) | `f32`, codes decoded to `x/255` (`isa::truth`) | `f32`, integer-valued | `f64`, integer-valued | +|---|---|---|---|---| +| deduction | 419,227,709 rows off | 2,413 | 1,368 | **0** | +| analogy | 521,640,704 | 512 | 0 | **0** | +| induction | 775,161,856 | 4,352 | 7,680 | **0** | +| abduction | 775,161,856 | 4,352 | 7,680 | **0** | + +Every miss is one code on the confidence; the frequency never differs. + +**What follows:** +- The table shape (plan §4 C candidate 1, `MapPairU8`) rounds at every stage + and misses 10–18 % of all rows. Rejected. +- `f32` misses a few thousand rows per law, on either encoding. +- Integer-valued `f64` (products of codes, one division, one rounding) is + exact on all 2³² rows of all four laws. It is also the shape that covers + the variable division of `w / (w + k)`, which a multiply-high by a constant + (§4 C candidate 2) cannot. + +**OPEN:** +- Speed: no SIMD kernel exists yet; `F64x8` has `floor` and `mul_add` but no + lane conversion from the `I32` truth lanes. Cost per element is measured on + the kernel, not on this scalar probe. +- The plan's gate "one shape serves SQL nullable arithmetic too" is not met by + this measurement: `f64` is exact for `i32` sums and differences, not for + every `i32` product (past 2⁵³). +- Which premise is "1" in induction/abduction is W5's join (ONA swaps the + arguments of its `Truth_Induction`); the laws here are two-input laws. diff --git a/.claude/board/entries/README.md b/.claude/board/entries/README.md index 77bb272d1..dc16c2cc6 100644 --- a/.claude/board/entries/README.md +++ b/.claude/board/entries/README.md @@ -25,11 +25,12 @@ 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-13. | date | entry id | finding | file | |---|---|---|---| | 2026-10-13 | `D-PROD-V4` | | [2026-10-13-production-targets-v4.md](2026-10-13-production-targets-v4.md) | +| 2026-10-13 | `D-NALP-4` | | [2026-10-13-d-nalp-4-truth-law-shape.md](2026-10-13-d-nalp-4-truth-law-shape.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) | | 2026-10-12 | `D-SAG-5-0` | Post-#1509 SAG self-querying, provenance and limited attention with NARS/Hyperon/PLN comparisons; research prompt and high-signal falsifiers | [2026-10-12-sag-reflexive-cognition-research.md](2026-10-12-sag-reflexive-cognition-research.md) | diff --git a/.claude/plans/nal-polyfill-v1.md b/.claude/plans/nal-polyfill-v1.md index a6b37e890..766e34652 100644 --- a/.claude/plans/nal-polyfill-v1.md +++ b/.claude/plans/nal-polyfill-v1.md @@ -158,6 +158,13 @@ candidate shapes, chosen by W4's measurement, not here: lanes. Fewer table bytes, no per-stage table rounding, and it needs an ndarray multiply-high word. +**MEASURED (2026-10-13, W4 probe):** neither candidate as written. Over all +2³² inputs per law, the table shape misses 10–18 % of rows by one code and +`f32` misses a few thousand; integer-valued `f64` (products of codes, one +division, one rounding) is exact on every row of deduction, analogy, +induction and abduction, and handles the variable division of `w / (w + k)`. +Entry `2026-10-13-d-nalp-4-truth-law-shape.md`. + Whichever wins, it is solved once for both NAL and SQL nullable arithmetic, never twice. The path is: ndarray primitive with parity on every realization row → mask-risc terminal with parity → `FoldDialect` wiring → one `ogar-nal` diff --git a/crates/lance-graph-nal/Cargo.toml b/crates/lance-graph-nal/Cargo.toml index 6719d505c..80eb79ccc 100644 --- a/crates/lance-graph-nal/Cargo.toml +++ b/crates/lance-graph-nal/Cargo.toml @@ -20,6 +20,10 @@ lance-graph-r2il = { path = "../lance-graph-r2il" } # By git `main`, the coordinate `lance-graph-r2il` uses (one `ogar-loco`). ogar-loco = { git = "https://github.com/AdaWorldAPI/OGAR", branch = "main" } +[dev-dependencies] +# The in-tree scalar NARS truth formulas (zero dependencies), the W4 parity reference. +causal-edge = { path = "../causal-edge" } + [patch."https://github.com/AdaWorldAPI/lance-graph"] lance-graph-contract = { path = "../lance-graph-contract" } diff --git a/crates/lance-graph-nal/examples/w4_truth_law_probe.rs b/crates/lance-graph-nal/examples/w4_truth_law_probe.rs new file mode 100644 index 000000000..1aaeb7424 --- /dev/null +++ b/crates/lance-graph-nal/examples/w4_truth_law_probe.rs @@ -0,0 +1,189 @@ +//! W4 (D-NALP-4) measurement: how exactly each candidate realization of the +//! per-row truth laws reproduces the exact law, over EVERY input +//! (`(f1, c1, f2, c2)` ∈ 256⁴ = 2³² rows per law). +//! +//! Shapes measured against `tests/common/truth_law.rs` (exact integers, one +//! half-up rounding): +//! - `table`: 256×256 `u8` laws composed, rounding at every stage +//! (`mul[a][b] = round(a·b/255)`, `w2c[x] = round(255·x/(x+255))`); +//! - `f32-dec`: `causal_edge::isa::truth`'s arithmetic, codes decoded to +//! `x/255` in `f32`, packed with `(v·255).round()`; +//! - `f32-int`: the exact integer formula evaluated in `f32` (products of +//! codes, one division by the constant, one rounding); +//! - `f64-int`: the same in `f64`. +//! +//! Run: `cargo run --release --example w4_truth_law_probe`. + +#[path = "../tests/common/truth_law.rs"] +mod truth_law; + +use std::thread; + +type Shape = fn(&str, u8, u8, u8, u8) -> (u8, u8); + +fn mul_table() -> Vec { + let mut t = vec![0u8; 256 * 256]; + for a in 0..256u64 { + for b in 0..256u64 { + t[(a * 256 + b) as usize] = truth_law::round_div(a * b, 255); + } + } + t +} + +fn w2c_table() -> Vec { + (0..256u64) + .map(|x| truth_law::round_div(255 * x, x + 255)) + .collect() +} + +thread_local! { + static MUL: Vec = mul_table(); + static W2C: Vec = w2c_table(); +} + +fn table(name: &str, f1: u8, c1: u8, f2: u8, c2: u8) -> (u8, u8) { + MUL.with(|m| { + W2C.with(|w| { + let mul = |a: u8, b: u8| m[usize::from(a) * 256 + usize::from(b)]; + match name { + "deduction" => { + let f = mul(f1, f2); + (f, mul(f, mul(c1, c2))) + } + "analogy" => (mul(f1, f2), mul(mul(c1, c2), f2)), + "induction" => (f2, w[usize::from(mul(mul(f1, c1), c2))]), + "abduction" => (f1, w[usize::from(mul(mul(f2, c1), c2))]), + _ => unreachable!(), + } + }) + }) +} + +fn pack(v: f32) -> u8 { + (v.clamp(0.0, 1.0) * 255.0).round() as u8 +} + +fn f32_dec(name: &str, f1: u8, c1: u8, f2: u8, c2: u8) -> (u8, u8) { + use causal_edge::isa::truth; + let d = |x: u8| f32::from(x) / 255.0; + let (f, c) = match name { + "deduction" => truth::deduction(d(f1), d(c1), d(f2), d(c2)), + "induction" => truth::induction(d(f1), d(c1), d(f2), d(c2)), + "abduction" => truth::abduction(d(f1), d(c1), d(f2), d(c2)), + "analogy" => (d(f1) * d(f2), d(c1) * d(c2) * d(f2)), + _ => unreachable!(), + }; + (pack(f), pack(c)) +} + +macro_rules! int_shape { + ($fname:ident, $t:ty) => { + fn $fname(name: &str, f1: u8, c1: u8, f2: u8, c2: u8) -> (u8, u8) { + let x = |v: u8| <$t>::from(v); + let r = |p: $t, q: $t| (p / q + 0.5).floor() as u8; + let (k1, k2, k3): ($t, $t, $t) = (255.0, 65025.0, 16581375.0); + match name { + "deduction" => { + let ff = x(f1) * x(f2); + (r(ff, k1), r(ff * x(c1) * x(c2), k3)) + } + "analogy" => (r(x(f1) * x(f2), k1), r(x(c1) * x(c2) * x(f2), k2)), + "induction" => { + let w = x(f1) * x(c1) * x(c2); + (f2, r(255.0 * w, w + k3)) + } + "abduction" => { + let w = x(f2) * x(c1) * x(c2); + (f1, r(255.0 * w, w + k3)) + } + _ => unreachable!(), + } + } + }; +} +int_shape!(f32_int, f32); +int_shape!(f64_int, f64); + +const SHAPES: [(&str, Shape); 4] = [ + ("table", table), + ("f32-dec", f32_dec), + ("f32-int", f32_int), + ("f64-int", f64_int), +]; + +#[derive(Default, Clone, Copy)] +struct Tally { + rows_off: u64, + max_df: u8, + max_dc: u8, +} + +fn measure(name: &'static str, law: truth_law::Law) -> [Tally; 4] { + let threads = 4u16; + let parts: Vec<[Tally; 4]> = thread::scope(|s| { + (0..threads) + .map(|t| { + s.spawn(move || { + let mut tally = [Tally::default(); 4]; + 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 (ef, ec) = law(f1b, c1, f2, c2); + for (i, (_, shape)) in SHAPES.iter().enumerate() { + let (sf, sc) = shape(name, f1b, c1, f2, c2); + let df = ef.abs_diff(sf); + let dc = ec.abs_diff(sc); + let tl = &mut tally[i]; + tl.rows_off += u64::from(df != 0 || dc != 0); + tl.max_df = tl.max_df.max(df); + tl.max_dc = tl.max_dc.max(dc); + } + } + } + } + f1 += threads; + } + tally + }) + }) + .collect::>() + .into_iter() + .map(|h| h.join().expect("worker")) + .collect() + }); + let mut out = [Tally::default(); 4]; + for p in parts { + for i in 0..4 { + out[i].rows_off += p[i].rows_off; + out[i].max_df = out[i].max_df.max(p[i].max_df); + out[i].max_dc = out[i].max_dc.max(p[i].max_dc); + } + } + out +} + +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} {:<8} {:>14} {:>8} {:>8}", + "law", "shape", "rows off", "max df", "max dc" + ); + for (name, law) in truth_law::LAWS { + let t = measure(name, law); + for (i, (shape, _)) in SHAPES.iter().enumerate() { + println!( + "{:<10} {:<8} {:>14} {:>8} {:>8}", + name, shape, t[i].rows_off, t[i].max_df, t[i].max_dc + ); + } + } +} diff --git a/crates/lance-graph-nal/tests/common/mod.rs b/crates/lance-graph-nal/tests/common/mod.rs new file mode 100644 index 000000000..6ae1697bc --- /dev/null +++ b/crates/lance-graph-nal/tests/common/mod.rs @@ -0,0 +1,3 @@ +//! Test oracles shared by the integration tests and the W4 probe. + +pub mod truth_law; diff --git a/crates/lance-graph-nal/tests/common/truth_law.rs b/crates/lance-graph-nal/tests/common/truth_law.rs new file mode 100644 index 000000000..d3eca0b4f --- /dev/null +++ b/crates/lance-graph-nal/tests/common/truth_law.rs @@ -0,0 +1,72 @@ +//! The exact per-row NAL truth laws over `u8` codes (W4 oracle). +//! +//! A code `x` stands for the value `x / 255`. Each law is computed in exact +//! integer arithmetic and rounded ONCE, half up, back into a code — the one +//! rounding `causal_edge::isa::truth` performs when it packs (`(v * +//! 255).round()`), without its intermediate `f32` rounding. This is the +//! contract a lane-producing realization must meet; it is test code, never a +//! production path (the production law runs in mask-risc). +//! +//! Formulas (horizon `k = 1`, `causal_edge::isa::truth` and the planner's +//! `TruthValue`): +//! - deduction: `f = f1·f2`, `c = f1·f2·c1·c2`; +//! - analogy: `f = f1·f2`, `c = c1·c2·f2`; +//! - induction: `f = f2`, `c = w / (w + 1)`, `w = f1·c1·c2`; +//! - abduction: `f = f1`, `c = w / (w + 1)`, `w = f2·c1·c2`. +//! +//! Which premise is "1" and which is "2" is the syllogism's business (W5); +//! these are two-input laws. + +#![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 K2: u64 = 255 * 255; +const K3: u64 = 255 * 255 * 255; + +fn w2c(w_num: u64) -> u8 { + // w = w_num / 255³, c = w / (w + 1) = w_num / (w_num + 255³), code = 255·c. + 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 analogy. +pub fn analogy(f1: u8, c1: u8, f2: u8, c2: u8) -> (u8, u8) { + let ff = u64::from(f1) * u64::from(f2); + let c = u64::from(c1) * u64::from(c2) * u64::from(f2); + (round_div(ff, K1), round_div(c, K2)) +} + +/// `(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 rule, for iteration. +pub type Law = fn(u8, u8, u8, u8) -> (u8, u8); + +/// The four NAL-1 laws by name. +pub const LAWS: [(&str, Law); 4] = [ + ("deduction", deduction), + ("analogy", analogy), + ("induction", induction), + ("abduction", abduction), +]; diff --git a/crates/lance-graph-nal/tests/w4.rs b/crates/lance-graph-nal/tests/w4.rs new file mode 100644 index 000000000..0bbe63aa2 --- /dev/null +++ b/crates/lance-graph-nal/tests/w4.rs @@ -0,0 +1,131 @@ +//! W4 (D-NALP-4): the per-row truth laws a lane-producing terminal must meet. +//! +//! The oracle (`common/truth_law.rs`) computes each law exactly in integers +//! and rounds once. These tests pin it against values computed by hand, the +//! OpenNARS outputs recorded in `.claude/knowledge/nal-recipe-audit/oracles.md` +//! (pinned `4d1bdb0`), and `causal_edge::isa::truth`, the in-tree scalar +//! formulas it must agree with up to `f32` rounding. + +mod common; + +use common::truth_law::{abduction, analogy, deduction, induction, LAWS}; + +fn decode(code: u8) -> f64 { + f64::from(code) / 255.0 +} + +/// Hand-computed: f = 128·128/255 = 64.25 → 64; c = 128⁴/255³ = 16.19 → 16. +#[test] +fn deduction_matches_hand_computed_codes() { + assert_eq!(deduction(128, 128, 128, 128), (64, 16)); + // f = 255·200/255 = 200; c = 255·200·255·100/255³ = 78.43 → 78. + assert_eq!(deduction(255, 255, 200, 100), (200, 78)); +} + +/// Analogy: f = f1·f2, c = c1·c2·f2. With f2 = 0 the conclusion carries no +/// confidence, while deduction with the same premises also has none: the two +/// differ where f1 = 0 instead (analogy keeps c, deduction drops it). +#[test] +fn analogy_and_deduction_differ_on_the_first_frequency() { + assert_eq!(analogy(0, 200, 255, 200), (0, 157)); + assert_eq!(deduction(0, 200, 255, 200), (0, 0)); +} + +/// Induction and abduction take the conclusion's frequency from opposite +/// premises and weigh the other one. Swapping premises must change the +/// answer, or a direction bug would pass unseen (the W5 hazard, ledger R1). +#[test] +fn induction_and_abduction_are_mirror_images() { + let (f1, c1, f2, c2) = (255, 230, 51, 200); + assert_eq!(induction(f1, c1, f2, c2), abduction(f2, c1, f1, c2)); + assert_ne!(induction(f1, c1, f2, c2), abduction(f1, c1, f2, c2)); +} + +/// The round-once rule is half up. All-ones evidence gives w = 1, so +/// c = 1/2 = 127.5 codes, which rounds to 128; rounding down gives 127. That +/// tie cannot reject ties-to-even (128 is even), so a second tie 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!(induction(255, 255, 255, 255), (255, 128)); + assert_eq!(abduction(255, 255, 255, 255), (255, 128)); + assert_eq!(induction(195, 255, 255, 255), (255, 111)); + assert_eq!(abduction(255, 255, 195, 255), (255, 111)); +} + +/// Zero evidence yields zero confidence for every law. +#[test] +fn no_evidence_no_confidence() { + for (name, law) in LAWS { + assert_eq!(law(255, 0, 255, 255).1, 0, "{name}"); + assert_eq!(law(255, 255, 255, 0).1, 0, "{name}"); + } +} + +/// OpenNARS at `4d1bdb0`, nal1.1: ` animal>. %1.00;0.90%` and +/// ` bird>. %1.00;0.90%` give ` animal>. %1.00;0.81%` +/// (deduction) and ` robin>. %1.00;0.45%` (the weak reverse). The +/// printout has two decimals; 0.9 is code 230. +#[test] +fn matches_opennars_nal1_1() { + let (f, c) = deduction(255, 230, 255, 230); + assert_eq!( + (format!("{:.2}", decode(f)), format!("{:.2}", decode(c))), + ("1.00".into(), "0.81".into()) + ); + let (f, c) = induction(255, 230, 255, 230); + assert_eq!( + (format!("{:.2}", decode(f)), format!("{:.2}", decode(c))), + ("1.00".into(), "0.45".into()) + ); +} + +/// Pack the way `CausalEdge64` does: `(v.clamp(0, 1) · 255).round()`. +fn pack(v: f32) -> u8 { + (v.clamp(0.0, 1.0) * 255.0).round() as u8 +} + +fn isa(name: &str, f1: u8, c1: u8, f2: u8, c2: u8) -> (u8, u8) { + use causal_edge::isa::truth; + let d = |x: u8| f32::from(x) / 255.0; + let (f, c) = match name { + "deduction" => truth::deduction(d(f1), d(c1), d(f2), d(c2)), + "induction" => truth::induction(d(f1), d(c1), d(f2), d(c2)), + "abduction" => truth::abduction(d(f1), d(c1), d(f2), d(c2)), + // `isa::truth` has no analogy; the planner's `TruthValue::analogy` + // formula, in the same f32 arithmetic. + "analogy" => (d(f1) * d(f2), d(c1) * d(c2) * d(f2)), + _ => unreachable!(), + }; + (pack(f), pack(c)) +} + +/// The exact law and the in-tree `f32` formulas agree within one code on a +/// stratified grid (every 5th code, ≈7.3M rows per law). One code is the most +/// a single `f32` rounding near a half can move. +#[test] +fn agrees_with_isa_truth_within_one_code() { + let grid: Vec = (0..=255u16).step_by(5).map(|x| x as u8).collect(); + for (name, law) in LAWS { + let mut differ = 0u64; + for &f1 in &grid { + for &c1 in &grid { + for &f2 in &grid { + for &c2 in &grid { + let (ef, ec) = law(f1, c1, f2, c2); + let (sf, sc) = isa(name, f1, c1, f2, c2); + let df = (i16::from(ef) - i16::from(sf)).abs(); + let dc = (i16::from(ec) - i16::from(sc)).abs(); + assert!( + df <= 1 && dc <= 1, + "{name}({f1},{c1},{f2},{c2}): exact ({ef},{ec}) isa ({sf},{sc})" + ); + differ += u64::from(df + dc > 0); + } + } + } + } + eprintln!("{name}: {differ} grid rows differ by one code"); + } +}