[sysuTobo]

Why

The use contract can already require a candidate implementation to reproduce the reference, but the training-inference gap — the learner and the engine scoring the same rollout tokens — was only a diagnostic summary in a history report. #79 turns it into a declared, replayable claim: a contract can now require that the two sides agree on those exact paths, either bit for bit, per token, or as a whole-path log ratio.

What

• New Invar.Paths module. A path observation carries the token path and prompt split, the distribution rule (temperature, logprobs, truncation), the forward-weight identity (frozen base + trainable adapter), the implementation identity, the FP32 words and their provenance. Comparisons are exact, on Rational words; zero support is represented explicitly.
• Comparability by forward weights only. A pair is compared when the token path and rule agree and either the forward weights are equal or a declared correspondence relates them. Adapter and learner-state digests remain provenance; assemblies may differ; different weights are a policy difference, not an implementation difference.
• Three contract relations. training-path-words, training-path-token-log-gap and training-path-log-ratio, each naming the learner side. use prepare predicts the path-execution-report-authenticity and path-behavior-measurement premises, plus an optional forward-weight-correspondence.
• One comparison for history and use. History admission derives observations from each generation's samples and probability artifact; History.paths exposes them per sample. use inspect and use admit attach them through the --history-* options (including --history-run), so the report and the decision run the same measure/judge.
• Probability artifacts v6. Each optimizer step records the adapter identity it actually used, so current words are bound to the forward weights that produced them. The first step must use the update's starting policy.
• Missing evidence stays undetermined. A path requirement without attached path observations gets an explicit missing-evidence claim and an unknown finding instead of an accidental admission.

Validation

• cabal test: all suites pass, including 11 new tests in test/Paths.hs (exact comparison, cancellation, incomparability, zero support, correspondence, scoped claims, admitted-update observations, per-step adapter identity).
• HF worker suite: 224 tests OK, 2 skipped; shared worker suite: 20 tests OK.
• test/types.sh ghc exit 0; confidence checker: 122 bounds checked, 14 invalid inputs refused.
• fourmolu --mode check, hlint src test app, cabal check: clean.
• End-to-end against a real HF training run: invar use admit --history-run returned admitted_under_declared_reliance with a contract whose generated pair and training paths use the initial checkpoint.

Refs #79.

The documented limits stay: a pair with unbound different forward weights is unknown until #84 declares the conversion/correspondence; the correspondence itself is recorded, not authenticated.

[sysuTobo]

• Added e7e102a after the code review.
• Fixed History.paths role/sample pairing and switched the cohort to the request’s behavior version; per-step current observations are no longer claimed because their weights differ from the behavior policy after the first step.
• Path implementation checks now ignore the adapter digest (policy content) and honor declared transfers; reference observations use the reference adapter on both sides.
• The probability artifact’s per-step policy is now required to equal the applied step’s before digest in both runtime and history admission.
• The path contract E2E now runs two optimizer steps with learner-scored references.
• Re-ran: cabal test PASS; HF suite 224 tests OK (2 skipped); shared suite 20 OK; types.sh, fourmolu, hlint, cabal check clean.