v0.8.0: i64 T1 result-correspondence parity (verification depth)

[avrabe]

v0.8.0 milestone — Verification depth on i64 (T1 result-correspondence parity)

Per PulseEngine defense-in-depth methodology, v0.8.0 promotes the i64 integer-op proofs from T2 existence-only to T1 result-correspondence, bringing i64 to the same verification tier i32 already enjoys. This closes the largest gap in the current proof matrix:

Tier	i32 today	i64 today	i64 after v0.8.0
T1 (result)	35	4 (div only)	33 (4 + 29 new)
T2 (existence)	n/a	29	0
T3 (admitted)	10	0	0

Scope (30 theorems to promote, +1 foundation PR)

PR breakdown (queue order):

1. Foundation — Tactics + flag-correspondence lemmas
   • Add synth_binop_proof_i64 and synth_cmp_binop_proof_i64 tactic variants to coq/Synth/Synth/Tactics.v (currently i32-only — see synth#TBD report)
   • Add 11 i64 flag-correspondence lemmas to coq/Synth/ARM/ArmFlagLemmas.v (parallel to the existing 20 i32 lemmas)
   • Verify bazel test //coq:verify_proofs stays green
2. i64 arithmetic + bitwise (12 theorems): I64Add/Sub/Mul + I64And/Or/Xor in CorrectnessI64.v
3. i64 shifts + rotates (10 theorems): I64Shl/ShrS/ShrU + I64Rotl/Rotr
4. i64 comparisons (11 theorems): I64Eq/Ne/LtS/LtU/LeS/LeU/GtS/GtU/GeS/GeU/Eqz in CorrectnessI64Comparisons.v
5. i64 bit-manip (3 theorems): I64Clz/Ctz/Popcnt — already have 6 supporting axioms per STATUS.md

Optional additive PRs (not required for the theme but sized to bundle):

6. F64↔I64 conversions (~150 lines): close the deferred F64ConvertI64S/U, I64TruncF64S/U from v0.7.0's CHANGELOG
7. F32DemoteF64 (~80 lines): close the deferred F32DemoteF64 from v0.7.0's CHANGELOG

Falsification statement

v0.8.0 would be wrong if:

• Any i64 op covered by a newly-added T1 theorem is observed to miscompile against the WASM reference (the theorem's premises would be violated in practice, OR the theorem proves a different operation than the compiler emits).
• The bazel test //coq:verify_proofs job goes red on a clean v0.8.0 checkout.
• The new tactics (synth_binop_proof_i64, synth_cmp_binop_proof_i64) succeed on a malformed proof obligation, indicating the tactic is unsound rather than reusable.

Optional (if items 6+7 ship):

• Any covered f64↔i64 conversion or F32DemoteF64 op miscompiles on a Cortex-M7DP target.

Why this is a single release

Per the planning research (synth#TBD subagent reports):

• i64 T1 parity alone is MEDIUM risk, 2–3 weeks of proof work. The existing T2 proofs already establish that the compiled ARM code executes — promoting them to T1 is per-theorem manual proof effort using the existing i32 patterns as templates.
• RV32 T1 parity was considered but is out of scope: there is no coq/RISCV/RiscvSemantics.v yet. Building the RISC-V semantic substrate is its own multi-release effort. Tracked separately.
• P3 async (synth#80) is blocked by upstream: meld#94 (P3 lowering), kiln#230 (P3 runtime), and synth#77 (platform abstraction). Doing it now would mean rework when those land.

Closes / unblocks

This milestone advances coq/STATUS.md from "35 T1 Qed / 142 T2 / 10 admitted" to projected "64 T1 Qed / 113 T2 / 10 admitted" — a ~83% increase in result-correspondence coverage. The 10 admitted proofs (i32 division trap-guard sequences) are unchanged; that's a separate exec_program model extension tracked elsewhere.

[avrabe]

Scope amendment — adding PR 1a prerequisite.

Clean-room check of PR #149 surfaced a verification gap explicitly forbidden by this milestone's own falsification statement: Compilation.v models i64 ops as 32-bit single-instruction (e.g., I64Add → [ADD R0 R0 R1], with the comment "Simplified: just add low 32 bits"), while the real Rust compiler at crates/synth-synthesis/src/instruction_selector.rs:1450 emits proper register-pair sequences (ADDS R0, R0, R2; ADC R1, R1, R3). PR #149 proves the simplified model — not what the compiler emits.

#149 has been moved to draft. The PR queue is updated:

1. PR 1a (new prerequisite) — Align coq/Synth/Synth/Compilation.v's i64 op clauses (and ArmState.v / supporting infra if needed) with the real Rust codegen. Specifically: I64Add/Sub/Mul, I64And/Or/Xor, I64Shl/ShrS/ShrU, I64Rotl/Rotr, I64Eq/Ne/... must emit the actual register-pair / multi-instruction sequences the Rust compiler emits. This may require expanding exec_program / ArmState to model dual-register results. Expect this PR to invalidate existing T1 proofs that were Qed against the simplified model — those break and get re-proved in the lift PRs.
2. PR 1b (rebased from feat(coq): i64 tactics + flag-correspondence lemmas (v0.8.0 foundation) #149) — Tactics + 11 flag lemmas + 14 helpers, against the aligned model.
3. PRs 2–5: i64 arithmetic + bitwise, shifts + rotates, comparisons, bit-manip (as before, but discharging the aligned obligations).

This is a real scope expansion. PR 1a is intricate (it might surface other simplified-model corners we hadn't accounted for). The honest framing is: v0.8.0 is now "i64 T1 parity against the aligned compiler model" — the proofs claim what the compiler actually does, not a simplification of it.

The falsification statement stands. The "OR the theorem proves a different operation than the compiler emits" clause was put there exactly for this kind of finding, and it caught it.

PR #148 (f64↔i64 docs deferral) merged independently — that one was orthogonal.