Repository navigation
probes(D-TFLP 6.5): softmax fixture replay + certified preparation gate - #1800
Conversation
Committed int8 SOFTMAX fixtures (14 prepared tables, 529 witnesses, a 27-row reduced suite, 7 calibration-9 equivalence rows, 10 unreachable candidates; SHA-256 manifest) and a lab crate that replays them under plain `cargo test` with checked arithmetic and named refusals. Imported from the research branch claude/bpe-tokenization-architecture-3xd4eh (3fbd447, P2), with two additions made while landing: - the runner now rejects a witness whose claimed calibration identity is not the one its table was prepared for, and a row without the mandatory maximum (code 127), each before the sum is recomputed; - four tamper tests: wrong calibration identity, witness pointing at another table, missing maximum, incorrect stored sum. Fixture files are byte-identical to the research branch; regenerating them with the hardened gate reproduces them byte for byte. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01ArVbbq3DsToBM7r79zGeEf
…ntity check A source-global certificate for the TFLM int8 SOFTMAX reciprocal and a per-calibration gate (PROVED_OUTPUT_EQUIVALENT / REQUIRES_SOURCE_RECIPROCAL / REFUSE_UNKNOWN), validated independently on 14 known and 8 held-out calibrations (601/529/72 and 514/446/68; calibration 9 equivalent), with 13 mutation controls and the P3 cost measurements. Imported from claude/bpe-tokenization-architecture-3xd4eh (4b657dd P1, 3fbd447 P2 generator, 6.3 helpers 7c88982, softmax_oracle.cc 74804aa). Changes made while landing: - the gate recomputes the prepared table from the claimed (scale, beta) with the pinned TFLM primitives and refuses table_identity_mismatch; it prints the numerical cache key (mult, shift) and the semantic receipt (scale, zp, beta) as separate lines; - controls: wrong calibration refused 13/14 (the 14th pair has the identical table), the same run with the check disabled is caught only by the driver, calibration 1's table under calibration 2's identity is accepted with equal key and different receipt, a different table is refused; - TFLM_DIR replaces a hard-coded checkout path; - softcert65_run.json regenerated; decisions, witnesses and unreachable pairs are identical to the research run, and fixtures regenerated from it are byte-identical. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01ArVbbq3DsToBM7r79zGeEf
|
Important
This repository does not receive automatic reviews because it has fewer than 10 stars.
|
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01ArVbbq3DsToBM7r79zGeEf
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 26666aa0f1
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| r = subprocess.run([ORACLE], input=text, capture_output=True, text=True) | ||
| out = [] | ||
| for l in r.stdout.splitlines(): | ||
| t = l.split(); out.append(list(map(int, t[2:])) if t[:2] == ["1", "1"] else None) | ||
| return out |
There was a problem hiding this comment.
Reject failed or incomplete oracle batches
If the TFLM oracle aborts or produces fewer output lines than requested, this function ignores its exit status and returns the partial results. The subsequent zip(wcands, ko) silently skips unreturned witnesses, and verdict() still reports valid because it checks only witness_bad, not whether every witness was confirmed. Using /bin/false as the oracle reproduces this with calibration 0: all 20 witnesses remain unconfirmed, yet the verdict is valid. The equivalence check likewise accepts zero checked rows. Require a successful oracle exit, exactly one result per requested row, and successful preparation/invocation before accepting validation.
Useful? React with 👍 / 👎.
PR_ARC_INVENTORY: the #1800 Confidence line said only "MEASURED (lab)". It now records the certification: every fixture row confirmed by the real TFLM int8 SOFTMAX kernel (5f64e4ad), the TFLM-free Rust replay reproducing those bytes on all 529 + 27 + 7 rows, the exact-reciprocal negative control failing all 556 witness rows, and the scope stated in the probe's own README. A dated correction line notes that the replay crate landed with #1800, not #1801; #1801's Confidence line now names its admit/ contract and points to #1800 for the certification. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VncKoyG6JkpsoqhqTGTv3f
board: #1800 is certified bit-exact against the original TFLite kernel
Brings the research branch up to main eeaaafb (136 commits) without rewriting its history: the audit and ledger cite this branch's hashes. Conflicts were all files that landed on main in hardened form through #1800/#1801/#1803 (table-identity check, compact data, pinned-codec-set claim); main's versions were taken. The research-only run record softcert65_run.json stays here as evidence. The audit entry heading now reads D-TFLP-AUDIT so its index id no longer collides with main's D-TFLP 6.5 landing entry; the entries index is regenerated. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01ArVbbq3DsToBM7r79zGeEf
Why
D-TFLP Amendment 6.5 showed that for int8 SOFTMAX, the correctly rounded reciprocal changes output bytes against TFLM's
GetReciprocal. This happens on 13 of 14 known calibrations; calibration 9 is the only one where it can be swapped in. That evidence currently lives only on a research branch. This PR lands it onmainin two reviewable layers:cargo test;Scope (two commits; review the first on its own)
66b7431fcreplay + fixtures:.claude/probes/pal256-admission-v1/replay/and.claude/probes/source-behavior-v1/fixtures65/. Contents:It needs no TFLM. Landing-PR additions:
26666aa0fcertification gate:softcert65.{cc,py}, the source-global certificate, held-out calibrations, the fixture generator,perf65, and the 6.3 helpers it needs (trace63,recipall63,softmax63.py,softmax_oracle.cc). Landing-PR additions:table_identity_mismatch;(mult, shift)and the semantic receipt(scale, zp, β)on separate lines;TFLM_DIRreplaces a hard-coded path.Landing pages:
pal256-admission-v1/replay/README.mdandsource-behavior-v1/SOFTMAX65.md.Evidence used
Research branch
claude/bpe-tokenization-architecture-3xd4eh:4b657dd25(P1 gate) and3fbd44792(P2 fixtures);7c8898274(6.3 helpers) and74804aab0(oracle);.claude/board/entries/2026-10-26-d-tflp-parity-audit.md.The oracle is TFLM
5f64e4ad, source digest0566576b…eb3c, built with g++ 13.3.0 on x86-64. The research branch is not rebased and not rewritten.Tests run
replay:cargo test --releasegives 11 passed.--fullpasses 529 + 27 + 7 + 10.--reciprocal exact --fullgives 556 failures with the 7 equivalence rows still passing, as intended.wrong_calibration_identity_is_rejected; removing the max check failsmissing_mandatory_maximum_is_rejected.softcert65.py --mutationson all 22 calibrations takes 49 s.PROVED_OUTPUT_EQUIVALENT.typed_refusal:table_identity_mismatch. The 14th pair has the identical table and is correctly accepted;e_minus1andexclude_lower_endpointare ineffective, and documented as such.What this does not prove
[2^19, 2^28).Production impact
None. Lab files under
.claude/probes/only: no crate, workspace member, ABI or kernel changes. The accumulator-wrapping proposal (int8-semantics-v1/accum_wrapping65.diff) is deliberately not included. It needs an owner decision on overflow semantics.Dependencies / rollback
No dependency on other open PRs. Rollback is a revert of either commit; the replay commit stands alone.
Links
🤖 Generated with Claude Code
https://claude.ai/code/session_01ArVbbq3DsToBM7r79zGeEf