Skip to content

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

Merged
AdaWorldAPI merged 2 commits into
mainfrom
claude/d-tflp-softmax-evidence
Oct 26, 2026
Merged

AdaWorldAPI merged 2 commits into
mainfrom
claude/d-tflp-softmax-evidence

Conversation

@AdaWorldAPI

@AdaWorldAPI AdaWorldAPI commented Oct 26, 2026 •

Copy link
Copy Markdown
Owner

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 on main in two reviewable layers:

  1. a replay that runs under plain cargo test;
  2. the TFLM-backed gate that produced the evidence.

Scope (two commits; review the first on its own)

  1. 66b7431fc replay + fixtures: .claude/probes/pal256-admission-v1/replay/ and .claude/probes/source-behavior-v1/fixtures65/. Contents:

    • 14 prepared tables;
    • 529 witnesses, plus a 27-row reduced suite;
    • 7 equivalence rows and 10 unreachable candidates;
    • a SHA-256 manifest;
    • checked arithmetic and named refusals.

    It needs no TFLM. Landing-PR additions:

    • a witness must claim the calibration its table was prepared for;
    • the row maximum (code 127) is mandatory;
    • four new tamper tests.
  2. 26666aa0f certification 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:

    • the gate now verifies table ↔ calibration itself (Option B). It recomputes the prepared table from the claimed (scale, β) with the pinned TFLM primitives and refuses table_identity_mismatch;
    • it prints the numerical cache key (mult, shift) and the semantic receipt (scale, zp, β) on separate lines;
    • TFLM_DIR replaces a hard-coded path.

Landing pages: pal256-admission-v1/replay/README.md and source-behavior-v1/SOFTMAX65.md.

Evidence used

Research branch claude/bpe-tokenization-architecture-3xd4eh:

  • 4b657dd25 (P1 gate) and 3fbd44792 (P2 fixtures);
  • 7c8898274 (6.3 helpers) and 74804aab0 (oracle);
  • Amendment 6.5 in .claude/board/entries/2026-10-26-d-tflp-parity-audit.md.

The oracle is TFLM 5f64e4ad, source digest 0566576b…eb3c, built with g++ 13.3.0 on x86-64. The research branch is not rebased and not rewritten.

Tests run

  • replay: cargo test --release gives 11 passed. --full passes 529 + 27 + 7 + 10. --reciprocal exact --full gives 556 failures with the 7 equivalence rows still passing, as intended.
  • Disable runs: removing the new identity check fails wrong_calibration_identity_is_rejected; removing the max check fails missing_mandatory_maximum_is_rejected.
  • Gate: a full re-run of softcert65.py --mutations on all 22 calibrations takes 49 s.
    • Known: 601 / 529 / 72. Held-out: 514 / 446 / 68. All validated; calibration 9 is PROVED_OUTPUT_EQUIVALENT.
    • Decisions, witnesses and unreachable pairs are identical to the research run.
    • Fixtures regenerated from the new run are byte-identical.
  • Identity controls:
    • wrong calibration: 13/14 typed_refusal:table_identity_mismatch. The 14th pair has the identical table and is correctly accepted;
    • the same run with the gate check disabled: caught only by the driver's validation;
    • calibration 1's table under calibration 2's identity: accepted, equal numeric key, different receipt;
    • a different table: refused.
  • Mutations: 11 of 13 are effective, and every effect is refused or detected. e_minus1 and exclude_lower_endpoint are ineffective, and documented as such.

What this does not prove

  • It covers one TFLM revision, one compiler and x86-64.
  • No calibration other than 9 admits the exact reciprocal.
  • It says nothing about int16, other output quantizations or sums outside [2^19, 2^28).
  • No ONNX/TFLite model import.
  • A table digest is a numerical cache key, never semantic identity.

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

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
@coderabbitai

coderabbitai Bot commented Oct 26, 2026 •

Copy link
Copy Markdown

Important

  • 🔍 Trigger review

This repository does not receive automatic reviews because it has fewer than 10 stars.

Run configuration
  • Source mode: Auto
  • Repository: Unavailable
  • Branch: Unavailable
  • File: No configuration file from this repository applied
  • Commit: Unavailable
  • Layers: Organization UI
  • Review profile: CHILL
  • Plan: Advanced
  • Run ID: 9a02e424-f4e7-45b6-a561-5e8e28af2abc
  • Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

Warning

Billing warning: we have not been able to collect payment for this subscription for more than 72 hours. Please update the payment method or pay any pending invoices in Billing to avoid service interruption.

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

Comment @coderabbitai help to get the list of available commands.

AdaWorldAPI pushed a commit that referenced this pull request Oct 26, 2026
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01ArVbbq3DsToBM7r79zGeEf
@AdaWorldAPI
AdaWorldAPI marked this pull request as ready for review October 26, 2026 20:43
@chatgpt-codex-connector

chatgpt-codex-connector Bot commented Oct 26, 2026 •

Copy link
Copy Markdown

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review Status Commit Review trigger
📝 Code Review ✅ Completed 2026-10-26T20:45:29.928689Z 26666aa Draft marked ready
ℹ️ 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" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

@chatgpt-codex-connector chatgpt-codex-connector Bot left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 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".

Comment on lines +110 to +114
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

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P2 Badge 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 👍 / 👎.

@AdaWorldAPI
AdaWorldAPI merged commit 7d485dc into main Oct 26, 2026
1 check passed
AdaWorldAPI pushed a commit that referenced this pull request Oct 26, 2026
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
AdaWorldAPI added a commit that referenced this pull request Oct 26, 2026
board: #1800 is certified bit-exact against the original TFLite kernel
AdaWorldAPI pushed a commit that referenced this pull request Oct 28, 2026
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants