proof: partition byte forgeries by returned component coverage

[Nicola-Ceornea]

The EasyCrypt byte-game forgery residual now separates new top/bottom WOTS component messages, a private FORS value at an unreturned ordinary coordinate, and coverage assembled from earlier signing responses. Every logged output retains its widths. Covered ordinary values match the actual private coordinate and returned value; the thirteenth root-as-secret is handled separately. The signer, client, oracle calls, game and existing probability charges are unchanged.

An existing XmssmtCC_All arithmetic step failed the mandatory interactive replay. It now explicitly derives a product's nonnegativity from its factors, with the original theorem statement and assumptions preserved. The failed replay is retained in the receipt; both whole-file drivers, a fresh frozen review, and the corrected full replay cover this repair.

The three Rust source bindings now match current master’s signing-progress callbacks. Four transcript checks and two progress-correspondence checks pass; the EasyCrypt proof/control bytes remain unchanged. Callback side effects and timing remain outside the manual functional correspondence.

General information exposure and numerical private/chain/encoding charges remain open under #100/#295. Unreturned coordinates do not imply unknown values. The probability hop retains successful forgery; this is not a closed numerical EUF bound.

Validation: 438 direct targets, 438 default-CLI targets and 411 controls pass in the full cold replay with unchanged input 06793da6caf1b7efe0ff7b7691927981. Eight modules passed 16 source-matched whole-file checks; 25 new controls, eleven checker regression groups, static contract and 402-input source binding pass. Old statements/assumptions remain unchanged; no new project axiom/admit/clone assumption. The controls include ten positive consumers/examples, eight scope probes and seven exact-statement mismatches. Conditional examples and diagnostic rejections are not semantic counterexamples or complete-game nonvacuity evidence.

Opus returned GO; Astra reported GAP solely for the then-pending combined-source full cold replay. Both found no source-level blocker across all seven focus areas, including the three refreshed Rust bindings. The coordinator resolved the exact pending-replay gap with the matching completed green replay; raw reviewer verdicts are preserved. Source d03db3d99bf1eb34b6e27ed32fa60c43bed66fed; receipt head 74c394b01c5f9b7422c64870e79ef7eb151a81f6. Evidence. Standing owner substitutions: Astra replaces SOL; Kimi omitted.

Hosted CI status and any baseline failures are recorded separately in the receipt. No overall green-CI, Rust-extraction, concrete SHA-256, QROM, numerical security-level or production claim. #509 remains deferred.