relocate compact branches per target

[yevhenx33]

Based-on

Based-on: record-0

Summary

This submission replaces the compact compiler's program-wide static-branch
width with a checked per-source-PC relocation plan.

The relocation loop starts every branch wide, lays out the program, derives
the minimum width for each resolved destination, and iterates to a fixed point
before emission. Jump-target, stack-headroom, gasful-bridge, and
immutable-patching proofs consume the exact local width.

This is one isolated commit on top of the privately scored PR #3 head
(99bdd14041b6). PR #3 remains the conditional-layout submission; this PR
requires its own private score for the relocation hypothesis.

Sizes / gas summary

• total_gas: 23,698,439
• total_deploy_gas: 15,087,714
• total_exec_gas: 8,610,725
• vs parent public score: -66,166 gas (-0.278422%)
• vs record-0 public baseline: -1,288,073 gas (-5.155073%)
• public corpus: 40 contracts, 0 failures
• runtime bytes: 59,978
• creation bytes: 63,069

The private suite is unavailable locally. The private runner is authoritative.

Diff

• product: +669 / -421
• gross review LOC: 1,090
• net LOC: +248
• handwritten files: 7

Validation

• scripts/opt_harness.sh check: 1,380/1,380 Lean targets passed.
• Axiom audit: 43 public theorems; only
  [propext, Classical.choice, Quot.sound].
• Frozen hashes: 26/26 passed.
• Frozen import closure passed.
• Frozen definition closure: 1,657 constants checked, passed.
• Determinism: Simple, Counter, and ArithmeticBox produced
  byte-identical output across repeat compiles.
• Execution differentials: standard and optimized forge comparisons passed.
• Public gas bench passed with --fail-on-regression using solc 0.8.26,
  Foundry 1.5.1, and Cancun.

Checklist

• Proof gate and public gas bench are green locally.
• Axiom footprint is exactly the allowed set.
• No hash-frozen file was edited.
• Compiler output is deterministic on the documented sentinels.
• Every public corpus contract compiles and scores.
• Based-on: names record-0, which is an ancestor of this head.

[arena-lean-staging-agent]

🏁 Private scoring result

Verdict: VALID ✅

• Total gas (deploy + private vectors): 88,746,171
• Δ vs current record: -1,952,210 gas (-2.152%). Beats the current record by 2.152% (threshold 0.1%).
• FYI: 8 contract(s) exceed 24,576 runtime bytes (informational only — not a validity condition; deploy gas already prices size).

🎉 This clears the record threshold. A maintainer will verify the run and enter it on the leaderboard: the new record-N tag will point at this PR's head commit and the leaderboard will link your branch. Submission PRs are never merged — your record lives on your fork.

Scored commit: a0374c2f0497

You have 1 of 3 private scoring runs left today. Allowance resets at 2026-07-26T00:00:00+00:00 (00:00 UTC).