Close real checkpoint proof trust gaps

Closes #188. Closes #189. Closes #190.\n\nImplements export-bound predictor weight commitments, calibrated real activation tables, bundle-carried float reference/tolerance, CLI faithfulness gating, parity tests, and updated trust-boundary docs.

Author: AbdelStark

.gitignore

@@ -24,3 +24,4 @@ lean/.lake/
 # Local demo/showcase scratch outputs (.artifacts/ already ignored above)
 /public-demo.html
 /demo.html
+uv.lock

AGENTS.md

@@ -31,9 +31,11 @@ non-reproducible attention. There is no proving circuit and no arithmetization.
   implemented and tested. P3 (full CEM planner) and P4 (pixel-to-plan, the ViT
   encoder inside the proof) are deferred. The image encoder is the trusted offline
   step today.
-- The proof attests the exact integer (quantized) relation, not float or PyTorch
-  equivalence. Per-tensor activation-scale calibration for float-faithful outputs
-  is a further refinement; activations stay int8 throughout the current scheme.
+- The proof attests the exact integer (quantized) relation, not the full PyTorch
+  program. Predictor bundles carry calibrated SiLU, GELU, inverse-sqrt, and
+  softmax-exp tables plus an offline float reference output and measured
+  tolerance; the CLI checks the verified integer `z_next` against that bound.
+  Activations stay int8 throughout the proved relation.
 - The argmin uniqueness check and the Freivalds probability bound are formally
   verified in Lean 4 (no `sorry`), under `lean/`.
 
@@ -71,7 +73,7 @@ cargo run -p pwm-testkit --bin pwm --release -- prove-predictor <bundle> # real
 cargo test --workspace                                                   # accept + reject suites
 ```
 
-The `pwm` CLI prints a four-stage pipeline (EXPORT, PROVE, VERIFY, TAMPER); it
+The `pwm` CLI prints a five-stage pipeline (LOAD, INFER, COMMIT, VERIFY, TAMPER); it
 honors `NO_COLOR` and `--json`.
 
 ## Conventions

CHANGELOG.md

@@ -13,6 +13,21 @@ entry.
 
 ## [Unreleased]
 
+### Security
+
+- **The predictor bundle is now commitment-chained to the export** (#188): the
+  Python export emits, in `lewm_predictor.json`, a predictor-scoped
+  `weights_root` computed over exactly the 30 proven block tensors in the Rust
+  prover's canonical `tensor_id` order (`pwm_export.export.predictor_weight_dicts`),
+  and the prover binds that *carried* value into the model commitment
+  (`prove_predictor_with_weights_root`), so `verify_predictor` rejects with
+  `CommitmentMismatch(Model)` unless the proven weights reproduce the export's
+  commitment bit-for-bit. The artifact alone now certifies which weight set was
+  proven (bundle ⇄ export bound; checkpoint ⇄ export remains trusted
+  preprocessing — documented in README and specs §13). The Python↔Rust
+  canonical-encoding parity gate is now two-way: the multi-leaf `weights_root`
+  vector and the full predictor weight scheme are pinned on both sides.
+
 ### Changed
 
 - **The `prove-predictor` demo path is now commitment-bound** (#187): the full

README.md

@@ -24,9 +24,12 @@ one honest hole CommitLLM leaves open: non-reproducible attention.
 
 ### What it does not claim
 
-It proves an exact arithmetic relation. It does not claim floating-point or PyTorch
-equivalence, the physical truth of the predictions, or zero knowledge. Public
-claims must be a subset of the proven statement.
+It proves an exact integer arithmetic relation. For predictor bundles, the export
+also carries a float reference output and a measured tolerance, and the demo CLI
+checks the verified integer output against that bound. The verifier still does
+not prove the full PyTorch program, the physical truth of the predictions, zero
+knowledge, or that the checkpoint bytes were exported honestly. Public claims
+must be a subset of the proven statement.
 
 ## Quickstart
 
@@ -64,11 +67,13 @@ ProvableWorldModel  commit-and-audit over the le-wm world model
   ├ witness  689,760 claimed op outputs (5.26 MiB)  trace_root 56bc38fc...
   └ bind     absorbed model + inputs + trace, then squeezed the Freivalds r (non-adaptive)
 
-[stage 4/5] VERIFY  no_std, float-free, never re-runs the model
+[stage 4/5] VERIFY  no_std, float-free, commitment-bound, never re-runs the model
+  ├ binding  recomputed model, quantization, planner, input + output commitments
   ├ challenge derived the Freivalds r for 30 linear projections
   ├ checks   Freivalds v·x == r·z  (soundness ≤ 1/p, p = 2⁶¹−1; union over the checks ~2⁻⁴⁴)
   │          exact recompute of attention, softmax, GELU, LayerNorm, residuals
-  └ verdict  ACCEPT  in 28.6 ms  (1.7x faster than proving; audits arithmetic only)
+  ├ faith    max |int - float| <= bundle tolerance  (offline reference from the export bundle)
+  └ verdict  ACCEPT  in 28.6 ms  (1.7x faster than proving; commitments + arithmetic audited)
 
 [stage 5/5] TAMPER  forge one matmul output
   └ forged matmul op 2 -> REJECT FreivaldsCheckFailed { op_id: 2 }  (caught)
@@ -131,6 +136,7 @@ ProvableWorldModel  export the real le-wm checkpoint into the prover
 [QUANTIZE]  34 matrices -> 11,705,856 int8 params   (float32 44.7 MiB -> int8 11.2 MiB, 4.0x smaller)
 [COMMIT]    model_commitment / quantization_commitment / graph_commitment  (Blake2s-256)
 [ENCODE]    real PushT expert episode (lerobot/pusht): 3 frames @ frameskip 5 -> ViT encoder; real 2D action
+[CALIBRATE] real SiLU/GELU/inverse-sqrt/softmax-exp tables + measured predictor tolerance
 ```
 
 The prover then runs the exact-integer inference on those real weights and audits it:
@@ -148,8 +154,9 @@ The prover then runs the exact-integer inference on those real weights and audit
   ├ latency  forward pass in 49.0 ms  (49.7 Kop/s, 661 MMAC/s)
   └ z_next   [11, 55, 32, -73, -57, 13]  (predicted next-latent head, from the real forward pass)
 
-[stage 4/5] VERIFY  no_std, float-free, never re-runs the model
-  └ verdict  ACCEPT  in 28.6 ms  (1.7x faster than proving; audits arithmetic only)
+[stage 4/5] VERIFY  no_std, float-free, commitment-bound, never re-runs the model
+  ├ faith    max |int - float| <= bundle tolerance  (offline reference from the export bundle)
+  └ verdict  ACCEPT  in 28.6 ms  (1.7x faster than proving; commitments + arithmetic audited)
 
 [stage 5/5] TAMPER  forge one matmul output
   └ forged matmul op 2 -> REJECT FreivaldsCheckFailed { op_id: 2 }  (caught)
@@ -161,7 +168,14 @@ A real expert episode (consistent observation and action) goes through the
 checkpoint's own encoders to produce the latent history and action embedding the
 predictor consumes. The encode is the trusted offline step (the image encoder is
 P4-deferred for proving), and the predictor step is what the no_std verifier
-audits. The action is the real 2D expert control plus the agent state; the full
+audits. The bundle also carries the export-computed `weights_root` over the 30
+proven block tensors; the prover binds that carried value into the model
+commitment, so the verifier rejects unless the proven weights reproduce the
+export's commitment bit-for-bit (bundle ⇄ export bound; checkpoint ⇄ export
+trusted). The same bundle carries the calibrated SiLU, GELU, inverse-sqrt, and
+softmax-exp tables plus the float predictor output on the same encoded input; the
+CLI checks the verified integer `z_next` against the bundle's measured tolerance.
+The action is the real 2D expert control plus the agent state; the full
 le-wm 10-dim action layout lives in the 13 GB lewm-pusht dataset.
 
 The predictor is built as the real le-wm architecture over the named-buffer block
@@ -208,7 +222,7 @@ and exactly recomputes the attention, softmax, GELU, LayerNorm, and residuals.
 +============================+===============================================+
 |                            v        VERIFIER  (no_std / float-free)        |
 |  +------------------------------------------------------------+            |
-|  | VERIFY  (NEVER re-runs the model; audits arithmetic only)  |            |
+|  | VERIFY  (NEVER re-runs the model; audits bindings + trace) |            |
 |  | replay transcript; Freivalds-check every fixed matmul:     |            |
 |  | v.x == r.z  because  rT(W x) = (rT W) x                    |            |
 |  | soundness err <= 1/p, p = 2^61-1;                          |            |
@@ -227,7 +241,8 @@ and exactly recomputes the attention, softmax, GELU, LayerNorm, and residuals.
 +============================================================================+
 
 exact integer fixed point makes attention reproducible: the one hole
-CommitLLM leaves open is closed here. The verifier audits arithmetic only.
+CommitLLM leaves open is closed here. The verifier audits the committed
+statement and the exact arithmetic trace.
 ```
 
 The prover runs the model normally and commits to its execution trace. The
@@ -278,9 +293,10 @@ and reject tests. The exporter ingests the real `quentinll/lewm-pusht` checkpoin
 and quantizes the full 192-dim V0 subgraph, and the Rust prover proves and
 verifies the full 6-block, 16-head, 192-dim predictor with the real quantized
 weights (`pwm prove-predictor`), plus the `pred_proj` head on its own
-(`pwm prove-lewm`). The proof attests the exact integer (quantized) relation;
-per-tensor activation-scale calibration for float-faithful outputs is a further
-refinement. For P2, all `S` candidate costs must be proven, not only the winner:
+(`pwm prove-lewm`). The proof attests the exact integer (quantized) relation, and
+predictor bundles now include calibrated activation tables plus an offline
+float-reference tolerance that the CLI enforces after verification. For P2, all
+`S` candidate costs must be proven, not only the winner:
 proving only the selected candidate would be unsound.
 
 Binding status, precisely: both the P0 feed-forward statement (`AuditArtifact`) and
@@ -295,6 +311,19 @@ claimed accumulator) before any challenge is squeezed, so the challenge is
 statement-bound and non-adaptive. A bare `verify_block` still exists for standalone
 arithmetic audits; the committed relation is the one to use for a real statement.
 
+The trust boundary, exactly: **bundle ⇄ export is cryptographically bound;
+checkpoint ⇄ export is trusted preprocessing.** The export computes a
+predictor-scoped `weights_root` over exactly the proven block tensors (in the
+prover's canonical `tensor_id` order) and carries it in the bundle; the prover
+binds that carried value, not a recomputed one, into the model commitment, so
+`verify_predictor` accepts only if the proven weights reproduce the export's
+commitment bit-for-bit (`CommitmentMismatch(Model)` otherwise). The artifact alone
+therefore certifies *which* weight set was proven, with no out-of-band weights.
+What remains trusted is the export step itself: that the quantized tensors
+faithfully derive from the `quentinll/lewm-pusht` checkpoint bytes (download,
+float-to-int8 quantization, and input encoding are offline preprocessing, outside
+the proven relation).
+
 ## Architecture
 
 Five small crates, one trust anchor. The verifier depends on neither the exporter

crates/pwm-core/tests/commit.rs

@@ -178,6 +178,36 @@ fn weights_root_changes_with_a_leaf_and_handles_edges() {
     assert_ne!(single, base);
 }
 
+#[test]
+fn weights_root_multi_leaf_parity_vector_is_pinned() {
+    // The cross-language parity vector: predictor-style tensors (ids 1000..,
+    // scale_id 0, int8 bounds; three leaves exercise the odd-level node
+    // duplication). The Python exporter pins the same hex in
+    // crates/pwm-export/python/tests/test_canonical_parity.py
+    // (test_predictor_weights_root_matches_rust), so the gate is two-way: a
+    // change to either side's encoding breaks its own pin.
+    let shaped = |id: u32, shape: &[u32], vals: &[i64]| {
+        let data = vals
+            .iter()
+            .map(|&v| BoundedInt::new(v, -128, 127).unwrap())
+            .collect();
+        Tensor::new(id, shape.to_vec(), 0, data).unwrap()
+    };
+    let w = [
+        shaped(1000, &[1, 2], &[1, -2]),
+        shaped(1001, &[2, 1], &[3, 4]),
+        shaped(1002, &[2, 2], &[-5, 6, -7, 8]),
+    ];
+    let hex: String = weights_root(&w)
+        .iter()
+        .map(|b| format!("{b:02x}"))
+        .collect();
+    assert_eq!(
+        hex,
+        "c666f637a30f38d653f7c6a3280e87b705777df25bae4644148b534992b03120"
+    );
+}
+
 #[test]
 fn output_commitment_binds_outputs() {
     let o1 = tensor(0, &[1, 2]);

crates/pwm-export/python/pwm_export/export.py

@@ -13,11 +13,9 @@
 """
 from __future__ import annotations
 
-import numpy as np
+from typing import Any
 
 from . import canonical as c
-from .fold import fold_linear_bn
-from .quantize import mac_fits_int32, quantize_array
 
 
 def tensor_dict(tensor_id: int, scale_id: int, q_list: list[int], shape: list[int]) -> dict:
@@ -30,15 +28,50 @@ def tensor_dict(tensor_id: int, scale_id: int, q_list: list[int], shape: list[in
     }
 
 
+def predictor_weight_dicts(
+    blocks: list[dict], d: int, heads: int, dim_head: int, mlp: int
+) -> list[dict]:
+    """The predictor-bundle weight tensors in the Rust prover's canonical scheme.
+
+    Mirrors `lewm_predictor.rs` exactly: per block `i` the tensor ids are
+    `1000 + 5*i ..` in registration order `adaln, qkv, out, fc1, fc2`.
+    Weight tensor `k` uses `scale_id = 10 + k`, matching the Rust builder and
+    binding the per-tensor `log2` interpretation into the quantization
+    commitment. `weights_root` over this list is the commitment the bundle
+    carries and the prover must reproduce bit-for-bit (pinned cross-language in
+    the canonical-parity tests).
+    """
+    inner = heads * dim_head
+    out = []
+    for i, bk in enumerate(blocks):
+        base = 1000 + 5 * i
+        for off, (key, shape) in enumerate((
+            ("adaln", [6 * d, d]),
+            ("qkv", [3 * inner, d]),
+            ("out", [d, inner]),
+            ("fc1", [mlp, d]),
+            ("fc2", [d, mlp]),
+        )):
+            k = 5 * i + off
+            out.append(tensor_dict(base + off, 10 + k, bk[key], shape))
+    return out
+
+
 def quantize_torch(w, qmax: int = 127) -> tuple[list[int], int]:
     """Torch entry point for E-202: convert a tensor to an array and quantize."""
+    import numpy as np
+
+    from .quantize import quantize_array
+
     return quantize_array(np.asarray(w.detach().cpu().numpy()), qmax)
 
 
 def fold_torch(weight, bias, bn):
     """Torch entry point for E-203: pull frozen BN stats and fold (NumPy core)."""
     import torch
 
+    from .fold import fold_linear_bn
+
     affine = getattr(bn, "affine", False)
     gamma = bn.weight if affine else torch.ones_like(bn.running_mean)
     beta = bn.bias if affine else torch.zeros_like(bn.running_mean)
@@ -58,6 +91,10 @@ def quantize_linear(tensor_id: int, scale_id: int, weight) -> tuple[dict, dict]:
 
     Asserts the int8 MAC for this layer fits the int32 accumulator (spec §3).
     """
+    import numpy as np
+
+    from .quantize import mac_fits_int32, quantize_array
+
     weight = np.asarray(weight, dtype=np.float64)
     out, inner = weight.shape
     if not mac_fits_int32(inner):
@@ -78,12 +115,14 @@ def build_manifest(ops: list[dict], weights: list[dict], tables: list[dict], sca
     }
 
 
-def export_graph(named_weights: list[tuple[int, str, np.ndarray]], tables: list[dict]) -> dict:
+def export_graph(named_weights: list[tuple[int, str, Any]], tables: list[dict]) -> dict:
     """Quantize a list of `(op_id, name, weight)` Linears into a committed manifest.
 
     Returns `{"manifest", "weights", "ops", "scales"}` — the manifest carries the
     same commitments the Rust prover/verifier reproduce (E-205/E-207).
     """
+    import numpy as np
+
     ops: list[dict] = []
     weights: list[dict] = []
     scales: list[dict] = []