probes(D-TFLP 6.5): softmax fixture replay + certified preparation gate

.claude/probes/fisherz-softmax-v1/softmax_oracle.cc

@@ -0,0 +1,37 @@
+// Runs TFLite Micro's real int8 SOFTMAX (Register_SOFTMAX via KernelRunner).
+// stdin, one case per line: n scale_bits zero_point beta_bits c_0 .. c_{n-1}
+// stdout, one line per case: prepare_ok invoke_ok o_0 .. o_{n-1}
+// Output contract: int8, scale 1/256, zero point -128.
+#include <cstdint>
+#include <cstdio>
+#include <cstring>
+#include <vector>
+#include "tensorflow/lite/micro/builtin_op_data.h"
+#include "tensorflow/lite/micro/kernels/kernel_runner.h"
+#include "tensorflow/lite/micro/test_helpers.h"
+
+int main() {
+  int n; unsigned sb, bb; int zp;
+  while (std::scanf("%d %x %d %x", &n, &sb, &zp, &bb) == 4) {
+    float scale, beta;
+    std::memcpy(&scale, &sb, 4); std::memcpy(&beta, &bb, 4);
+    std::vector<int8_t> in(n), out(n);
+    for (int i = 0; i < n; ++i) { int v; std::scanf("%d", &v); in[i] = (int8_t)v; }
+    int dims_data[] = {2, 1, n};
+    TfLiteIntArray* dims = tflite::testing::IntArrayFromInts(dims_data);
+    TfLiteTensor tensors[2] = {
+        tflite::testing::CreateQuantizedTensor(in.data(), dims, scale, zp),
+        tflite::testing::CreateQuantizedTensor(out.data(), dims, 1.0f / 256.0f, -128)};
+    int ia[] = {1, 0}, oa[] = {1, 1};
+    TfLiteSoftmaxParams params = {beta};
+    const TFLMRegistration reg = tflite::Register_SOFTMAX();
+    tflite::micro::KernelRunner runner(reg, tensors, 2, tflite::testing::IntArrayFromInts(ia),
+                                       tflite::testing::IntArrayFromInts(oa), &params);
+    TfLiteStatus p = runner.InitAndPrepare();
+    TfLiteStatus v = p == kTfLiteOk ? runner.Invoke() : kTfLiteError;
+    std::printf("%d %d", p == kTfLiteOk, v == kTfLiteOk);
+    for (int i = 0; i < n; ++i) std::printf(" %d", out[i]);
+    std::printf("\n");
+  }
+  return 0;
+}

.claude/probes/pal256-admission-v1/replay/Cargo.toml

@@ -0,0 +1,16 @@
+[package]
+name = "replay"
+version = "0.0.0"
+edition = "2021"
+publish = false
+
+# D-TFLP Amendment 6.5 P2: replay of the committed softmax reciprocal fixtures without TFLM.
+# Lab only; not a workspace member.
+[dependencies]
+serde_json = "1"
+sha2 = "0.10"
+
+[profile.release]
+debug = 0
+
+[workspace]

.claude/probes/pal256-admission-v1/replay/README.md

@@ -0,0 +1,92 @@
+# Softmax reciprocal fixture replay (D-TFLP 6.5, lab)
+
+This crate replays committed int8 SOFTMAX fixtures without TensorFlow Lite Micro.
+It shows that the fixtures, and the integer recipe they were recorded against, still agree.
+It runs under plain `cargo test`. It is not a workspace member and has no production consumer.
+
+## What is tested
+
+The fixtures live in `../../source-behavior-v1/fixtures65/`. A SHA-256 manifest
+(`manifest65.json`) covers every file.
+
+| file | rows | content |
+|---|---|---|
+| `softmax_tables65.json` | 14 tables | prepared source weights per calibration: admitted flag, `A = exp_on_negative_values`, `B = Rescale<12>`, each with its SHA-256 |
+| `witness65_full.jsonl` | 529 | every kernel-confirmed witness row. In each, the TFLM reciprocal and the correctly rounded one give different output bytes |
+| `witness65_reduced.jsonl` | 27 | the regression subset (selection rule in each row's `why`) |
+| `equivalence65.jsonl` | 7 | calibration 9 rows where both reciprocals give the kernel's bytes |
+| `unreachable65.jsonl` | 10 | arithmetic candidates proved not to occur in any admitted row |
+
+The runner works through three stages, in this order:
+1. manifest integrity: any mismatch exits with code 2;
+2. each table's digest;
+3. every fixture row.
+
+For each witness row it checks the following:
+- the claimed calibration identity is the one the table was prepared for;
+- the row maximum is code 127;
+- every code is admitted and every count is positive;
+- the recomputed sum equals the stored `S`;
+- `S` lies in the supported domain;
+- the source-reciprocal byte equals the stored kernel byte;
+- the exact-reciprocal byte equals the stored alternative byte, which differs from the source byte.
+
+All arithmetic is checked: an overflow the source would leave undefined becomes a named `Refusal`.
+
+## Where the oracle came from
+
+TFLM revision `5f64e4ad` (its `tensorflow/` tree is identical to `8f6596d`), reference int8 SOFTMAX
+(`kernels/internal/reference/softmax.h`), built with g++ 13.3.0 on x86-64.
+The source digest is sha256(`common.h` + `fixedpoint.h` + `reference/softmax.h`), equal to
+`0566576b4fb0be4df914ce36e369de295d22e227d661c13a0cec17f5d7f2eb3c`.
+
+The rows were produced by the certification gate (`../../source-behavior-v1/softcert65.cc`) and
+confirmed by the real TFLM kernel (`softmax_oracle.cc`) before `fixtures65.py` wrote them.
+Regenerating them with the current gate gives byte-identical files.
+
+## Admitted domain
+
+- int8 input, output scale 1/256, zero point −128;
+- `x_integer_digits = 12`;
+- row sums `S ∈ [2^19, 2^28)`.
+
+The 14 calibrations are the known set of `softmax63.py`.
+
+## How to run
+
+```sh
+cargo test --release                                                 # 11 tests, < 1 s
+cargo run --release -- ../../source-behavior-v1/fixtures65 --full    # all 529 + 27 + 7 + 10
+cargo run --release -- ../../source-behavior-v1/fixtures65 --reciprocal exact --full
+```
+
+The last command is the negative control. It must fail all 556 witness rows (529 full and 27 reduced) while
+the 7 equivalence rows still pass. Measured: about 90 ms for the full tier.
+
+## What PASS proves
+
+- The committed fixture bytes are the ones the manifest names.
+- On these 14 calibrations and these rows, the integer recipe in `src/lib.rs` reproduces the bytes the TFLM kernel produced.
+- The correctly rounded reciprocal is *not* a drop-in replacement on the 13 calibrations that have witnesses.
+- The tamper cases below are rejected, each for its own reason.
+
+## What PASS does not prove
+
+- It says nothing about calibrations outside the 14, rows outside the fixtures, other TFLM revisions, other compilers or other backends.
+- It does not re-run TFLM. Kernel agreement was established when the fixtures were made; the replay checks the recorded result.
+- It is not a softmax implementation, a Codec8 consumer or a production path.
+
+## Tamper detection (`tests/tamper.rs`)
+
+| tamper | expected result |
+|---|---|
+| changed byte, manifest not re-stamped | exit 2, `REFUSE integrity` |
+| changed source byte, re-stamped | `source byte … != stored` |
+| changed table weight, re-stamped | `table digest` |
+| witness claims another calibration (scale) | `calibration identity` |
+| witness points at another calibration's table | `table_sha256` |
+| row without its maximum (code 127) | `no mandatory maximum` |
+| stored `S` off by one | `!= stored S` |
+| a count of −1 | `NonPositiveMultiplicity` |
+| 600 maxima (`S > 2^28`) | `UnsupportedDomain` |
+| exact reciprocal | 556 failures, 7 equivalence rows still pass |

.claude/probes/pal256-admission-v1/replay/src/bin/replay.rs

@@ -0,0 +1,170 @@
+//! Replay the D-TFLP 6.5 softmax fixtures. Usage: replay FIXTURE_DIR [--reciprocal source|exact] [--full]
+//!
+//! Order: manifest digests (integrity) → each table's digest → each fixture. The reduced suite runs by
+//! default; `--full` adds the complete 529-witness tier. Exit status 0 only if every check passes.
+//! `--reciprocal exact` is the negative control: the witnesses must then fail and the
+//! calibration-9 equivalence rows must still pass.
+use replay::*;
+use serde_json::Value;
+use sha2::{Digest, Sha256};
+use std::{collections::BTreeMap, fs, path::Path, process::ExitCode};
+
+fn hex(b: &[u8]) -> String {
+    b.iter().map(|x| format!("{x:02x}")).collect()
+}
+
+fn table(v: &Value) -> Table {
+    let arr = |k: &str| v[k].as_array().unwrap().iter().map(|x| x.as_i64().unwrap()).collect::<Vec<_>>();
+    let (adm, a, b) = (arr("admitted"), arr("A"), arr("B"));
+    let mut t = Table { admitted: [false; 256], a: [0; 256], b: [0; 256] };
+    for i in 0..256 {
+        t.admitted[i] = adm[i] == 1;
+        t.a[i] = a[i] as i32;
+        t.b[i] = b[i] as i32;
+    }
+    t
+}
+
+fn row_pairs(v: &Value) -> Vec<(i32, i32)> {
+    match v {
+        Value::Object(m) => m.iter().map(|(k, n)| (k.parse().unwrap(), n.as_i64().unwrap() as i32)).collect(),
+        Value::Array(a) => {
+            let mut c: BTreeMap<i32, i32> = BTreeMap::new();
+            for x in a {
+                *c.entry(x.as_i64().unwrap() as i32).or_default() += 1;
+            }
+            c.into_iter().collect()
+        }
+        _ => panic!("row"),
+    }
+}
+
+fn main() -> ExitCode {
+    let args: Vec<String> = std::env::args().collect();
+    let dir = Path::new(&args[1]);
+    let recip = if args.iter().any(|a| a == "exact") { Recip::Exact } else { Recip::Source };
+    let full = args.iter().any(|a| a == "--full");
+    let mut fails: Vec<String> = Vec::new();
+    let t0 = std::time::Instant::now();
+    // 1. integrity
+    let man: Value = serde_json::from_str(&fs::read_to_string(dir.join("manifest65.json")).unwrap()).unwrap();
+    for (name, want) in man["sha256"].as_object().unwrap() {
+        let got = hex(&Sha256::digest(fs::read(dir.join(name)).unwrap()));
+        if &got != want.as_str().unwrap() {
+            fails.push(format!("integrity {name}"));
+        }
+    }
+    if !fails.is_empty() {
+        println!("REFUSE integrity: {fails:?}");
+        return ExitCode::from(2);
+    }
+    let t_integrity = t0.elapsed();
+    // 2. tables
+    let tj: Value = serde_json::from_str(&fs::read_to_string(dir.join("softmax_tables65.json")).unwrap()).unwrap();
+    let mut tables: BTreeMap<String, Table> = BTreeMap::new();
+    for (key, t) in tj["tables"].as_object().unwrap() {
+        let d = hex(&Sha256::digest(serde_json::to_string(t).unwrap()));
+        if d != tj["sha256"][key].as_str().unwrap() {
+            fails.push(format!("table digest {key}"));
+        }
+        tables.insert(key.clone(), table(t));
+    }
+    let t_tables = t0.elapsed() - t_integrity;
+    // 3. fixtures
+    let lines = |f: &str| fs::read_to_string(dir.join(f)).unwrap().lines().map(|l| serde_json::from_str::<Value>(l).unwrap()).collect::<Vec<_>>();
+    let mut ok = BTreeMap::<&str, u32>::new();
+    let mut check_w = |name: &'static str, ws: &[Value], fails: &mut Vec<String>| {
+        for w in ws {
+            let id = w["id"].as_str().unwrap();
+            let key = w["table"].as_str().unwrap();
+            if tj["sha256"][key] != w["table_sha256"] {
+                fails.push(format!("{name} {id}: table_sha256"));
+                continue;
+            }
+            // the calibration identity the witness claims must be the one its table was prepared for
+            let claimed = format!("{}:{}", w["scale_bits"].as_str().unwrap_or(""), w["beta_bits"].as_str().unwrap_or(""));
+            if claimed != key || tj["tables"][key]["scale_bits"].as_str() != w["scale_bits"].as_str() {
+                fails.push(format!("{name} {id}: calibration identity {claimed} != table {key}"));
+                continue;
+            }
+            let t = &tables[key];
+            let row = row_pairs(&w["row"]);
+            let d = w["d"].as_i64().unwrap() as i32;
+            let r = (|| -> Result<(), String> {
+                // differences are relative to code 127: the row maximum is mandatory
+                if row.iter().map(|&(c, _)| c).max() != Some(127) {
+                    return Err("no mandatory maximum (code 127)".into());
+                }
+                let s = row_sum(t, &row).map_err(|e| e.to_string())?;
+                if s != w["S"].as_i64().unwrap() {
+                    return Err(format!("sum {s} != stored S"));
+                }
+                if !row.iter().any(|&(c, _)| c == 127 + d) {
+                    return Err("no element at d".into());
+                }
+                let bs = byte_of(t, &row, 127 + d, recip).map_err(|e| e.to_string())?;
+                let bx = byte_of(t, &row, 127 + d, Recip::Exact).map_err(|e| e.to_string())?;
+                if i64::from(bs) != w["byte_source"].as_i64().unwrap() || i64::from(bs) != w["kernel_byte"].as_i64().unwrap() {
+                    return Err(format!("source byte {bs} != stored"));
+                }
+                if i64::from(bx) != w["byte_exact"].as_i64().unwrap() || bs == bx {
+                    return Err(format!("exact byte {bx}"));
+                }
+                Ok(())
+            })();
+            match r {
+                Ok(()) => *ok.entry(name).or_default() += 1,
+                Err(e) => fails.push(format!("{name} {id}: {e}")),
+            }
+        }
+    };
+    check_w("reduced", &lines("witness65_reduced.jsonl"), &mut fails);
+    if full {
+        check_w("full", &lines("witness65_full.jsonl"), &mut fails);
+    }
+    for e in lines("equivalence65.jsonl") {
+        let t = &tables[e["table"].as_str().unwrap()];
+        let codes: Vec<i32> = e["row"].as_array().unwrap().iter().map(|x| x.as_i64().unwrap() as i32).collect();
+        let row = row_pairs(&e["row"]);
+        let want: Vec<i64> = e["kernel_bytes"].as_array().unwrap().iter().map(|x| x.as_i64().unwrap()).collect();
+        let got: Result<Vec<i64>, Refusal> = codes.iter().map(|&c| byte_of(t, &row, c, recip).map(i64::from)).collect();
+        let got_x: Result<Vec<i64>, Refusal> = codes.iter().map(|&c| byte_of(t, &row, c, Recip::Exact).map(i64::from)).collect();
+        if got.as_ref() == Ok(&want) && got_x.as_ref() == Ok(&want) {
+            *ok.entry("equivalence").or_default() += 1;
+        } else {
+            fails.push(format!("equivalence {}", e["id"]));
+        }
+    }
+    for u in lines("unreachable65.jsonl") {
+        let t = &tables[u["table"].as_str().unwrap()];
+        let (s, d) = (u["S"].as_i64().unwrap(), u["d"].as_i64().unwrap() as i32);
+        let r = s - i64::from(t.b[255]) - if d != 0 { i64::from(t.b[(d + 255) as usize]) } else { 0 };
+        let proved = match u["status"].as_str().unwrap() {
+            "unreachable_negative" => r < 0,
+            _ => r >= 0 && r <= 4_000_000 && !representable(t, r as usize),
+        };
+        if proved {
+            *ok.entry("unreachable").or_default() += 1;
+        } else {
+            fails.push(format!("unreachable S={s} d={d}"));
+        }
+    }
+    let t_total = t0.elapsed();
+    eprintln!("timing_us integrity={} tables={} fixtures={} total={}", t_integrity.as_micros(), t_tables.as_micros(), (t_total - t_integrity - t_tables).as_micros(), t_total.as_micros());
+    println!("recip={recip:?} passed={ok:?} failures={}", fails.len());
+    for f in fails.iter().take(10) {
+        println!("  {f}");
+    }
+    if fails.is_empty() { ExitCode::SUCCESS } else { ExitCode::from(1) }
+}
+
+/// Plain unbounded-coin DP over the admitted weights: is r a non-negative combination?
+fn representable(t: &Table, r: usize) -> bool {
+    let coins: Vec<usize> = (0..256).filter(|&i| t.admitted[i] && t.b[i] > 0).map(|i| t.b[i] as usize).collect();
+    let mut rep = vec![false; r + 1];
+    rep[0] = true;
+    for x in 1..=r {
+        rep[x] = coins.iter().any(|&c| c <= x && rep[x - c]);
+    }
+    rep[r]
+}