[REAL LoF / DoS] Credit post-snapshot expired backing to payouts

[aeyakovenko]

What changed

• Credit residual released by a backing-bucket expiry after payout-snapshot capture into both persisted payout snapshots.
• Recompute the common resolved-payout rate immediately through a small production accounting kernel.
• Prove exact snapshot conservation and rate behavior for haircut-improvement and haircut-to-full cases.

Root cause

Fresh source backing is excluded from junior residual while it remains a senior provider claim. If that backing expired after the resolved payout snapshot was captured, it became junior residual but the frozen payout ledger was not increased. Close order could therefore leave real vault atoms outside every claimant's entitlement.

The public LiteSVM reproduction on the exact parent creates two independent winner/loser pairs and captures a 40/80 payout snapshot before the second 40-atom counterparty backing bucket expires. Both losers receive 960 and both winners receive only 1,020 from four 1,000-atom deposits, while 40 atoms remain in the vault as the winners' unpaid claims.

Impact

Each independent winner loses 20 atoms and the terminal market retains 40 undistributable atoms after all positions are closed. This is both loss of funds and terminal market denial of service through ordinary public trade, crank, resolve, and close routes.

Verification

• cargo test --all-targets (50 unit, 10 backing fuzz, 2 insolvent payout fuzz, 75 v16 spec tests)
• cargo kani --tests --features fuzz --exact --harness proof_v16_post_snapshot_backing_expiry_credits_junior_pool (99 checks, 2/2 covers)
• Exact-parent public LiteSVM RED and fixed-head GREEN are carried by the stacked wrapper PR.

[aeyakovenko]

Proof-strengthening follow-up pushed in a7f0a404.

Added/generalized obligations:

• Full-width payout conservation across symbolic released backing, junior residual, mixed receipted/unreceipted claims, snapshot metadata, and both haircut branches.
• Two production zero-copy route bindings: partial haircut improvement and restoration to full payout rate.
• Exhaustive expiry eligibility over all bucket statuses plus not-yet-expired Fresh state.
• Production replay frame proving a second expiry is Stale and cannot mutate backing, source aggregates, risk epoch, payout snapshots, vault, capital, or insurance.
• Separate pre-snapshot under-backed and fully-backed liveness routes proving expiry removes realizable source support without initializing terminal accounting.

Non-vacuity/mutation checks:

• All four symbolic payout covers are satisfiable.
• Disabling the post-snapshot credit call fails the production route theorem.
• Weakening the expiry eligibility gate fails both the status theorem and the replay frame.

Verification:

• All added Kani harnesses complete within 71s individually.
• cargo test --all-targets --features fuzz --quiet: 166 passed.
• cargo fmt --all -- --check: passed.
• Production source is unchanged by this follow-up.