[REAL DoS] Reconcile foreign-expired source liens during resolved close

[aeyakovenko]

What changed

• Before the resolved source-domain phase chooses ReleaseLien, detect an account-local counterparty lien whose shared backing bucket was already moved to Impaired by another account.
• Accrue utilization fees only through the bucket expiry slot, then relabel exactly that account lien from live to impaired state.
• Keep the close step bounded to one source domain and leave the already-impaired aggregate bucket unchanged.
• Preserve mixed counterparty/insurance liens by moving only the proportional fee revenue associated with the impaired counterparty reserve.
• Add a public-operation engine regression and a symbolic exact-relabel/conservation proof.

Root cause and impact

Account A can create a legitimate source-credit initial-margin lien through ordinary trades while a shared backing bucket is Fresh. In Resolved mode, a lien-free account B can close first and expire that shared bucket, moving aggregate valid_liened_backing_num to impaired_liened_backing_num. Account A still records its account-local counterparty lien as live.

The old resolved phase selected ReleaseLien solely from A's nonzero account-local lien. It then tried to debit the aggregate live-lien counter, which was already zero, and returned CounterUnderflow. SVM rollback restores the same state, so every bounded CloseResolved retry fails. Resolved portfolios have no alternate trade, rebalance, withdraw, or auto-crank route, making this a persistent public terminal DoS.

The exact parent regression fails at that point with CounterUnderflow. The wrapper LiteSVM reproduction reaches the same state using four initialized portfolios, authenticated mark accrual, ordinary public trades, public resolution, and public CloseResolved calls; three retries all fail with wrapper custom error 0x19 and byte-identical rollback.

Scope and dependencies

• Stacked on [REAL DoS] Expire prospective loss backing before resolved settlement #151 (and its [REAL DoS] Expire prospective K/F sources before resolved settlement #150 dependency).
• The account-lien relabel helper intentionally matches the latest mixed-fee semantics in [REAL DoS] Reconcile expired source liens during live refresh #112. [REAL DoS] Reconcile expired source liens during live refresh #112 covers Live expiry; this PR covers the distinct Resolved ordering where a foreign account has already expired the aggregate bucket. When the stack is rebased after [REAL DoS] Reconcile expired source liens during live refresh #112, the shared helper/proof should deduplicate and only the terminal invocation/regression remain here.
• [REAL LoF] Keep terminal source payouts monotonic #145 is a separate known terminal payout issue. This PR removes the earlier foreign-expiry rank blocker; it does not claim to replace [REAL LoF] Keep terminal source payouts monotonic #145.

Validation

• Exact parent 68364eac72c47d73e07820608f08acb58e38b08f: new engine public-operation regression fails with CounterUnderflow.
• Fixed engine: cargo test --all-targets --features fuzz: 171 passed.
• Kani proof_v16_resolved_foreign_expiry_lien_impairment_is_exact_relabel: 245 checks passed, 3/3 covers satisfied.
• Fixed wrapper SBF: 5 unit + 578 LiteSVM/CU tests passed.
• Public fixed-path transaction stays below the 1,000,000-CU guardrail.

Wrapper public reproduction: aeyakovenko/percolator-prog#300