feat(coq): align Compilation.v i64 ops with real Rust codegen (v0.8.0 prerequisite)#150
Open
avrabe wants to merge 3 commits into
Open
feat(coq): align Compilation.v i64 ops with real Rust codegen (v0.8.0 prerequisite)#150avrabe wants to merge 3 commits into
avrabe wants to merge 3 commits into
Conversation
… prerequisite) The previous Compilation.v modeled every i64 op as operating on a single 32-bit register (`R0`, `R1`) and a single ARM instruction — e.g. `I64Add -> [ADD R0 R0 (Reg R1)]`. The real Rust compiler at `crates/synth-synthesis/src/instruction_selector.rs:1450` emits a proper 64-bit add via the C flag (`ADDS R0,R0,R2; ADC R1,R1,R3`), with the i64 result spanning the (R0,R1) pair and the second operand in (R2,R3). The v0.8.0 umbrella (issue #147) falsification statement says: "v0.8.0 would be wrong if … the theorem proves a different operation than the compiler emits." This PR (1a) closes that gap as the prerequisite for the v0.8.0 lift queue (PRs 2–5) which can then rebase and lift T2 -> T1 proofs against the aligned model. Changes: - Add `ADDS / ADC / SUBS / SBC` real ARM instructions to `ArmInstructions.v` + `ArmSemantics.v` (ADDS sets C, ADC reads C). - Add high-level i64 pseudo-ops mirroring `ArmOp::I64Mul / I64Shl / I64ShrU / I64ShrS / I64Rotl / I64Rotr / I64Clz / I64Ctz / I64Popcnt / I64SetCond / I64SetCondZ / I64DivS / I64DivU / I64RemS / I64RemU / I64Const / I64ExtendI32S / I64ExtendI32U / I32WrapI64 / I64Load / I64Store` with axiomatized result semantics (parallels VFP modeling). - Update every i64 clause in `Compilation.v` to emit the aligned sequence; cite `instruction_selector.rs` line numbers liberally. - Re-admit 4 T1 i64 div/rem proofs and the i64_const_correct T1 proof (each Admitted with explicit pointer to a v0.8.0 lift queue PR). - Update `STATUS.md` and `CorrectnessComplete.v` metrics: 233 Qed / 10 Admitted -> 228 Qed / 15 Admitted (honest accounting of the prior T1 proofs which were stated against the wrong codegen model). - Add `docs/analysis/I64_CODEGEN_SURVEY.md` documenting the per-op Rust codegen survey that drove the alignment. T2 (existence-only) i64 proofs survive untouched: every new pseudo-op returns `Some <something>` for valid inputs and `None` only on div/rem trap, matching the existing `solve_single_arm / solve_cmp_mov` tactics. Architectural surprise: the Rust compiler treats almost every i64 op as a single high-level `ArmOp::I64*` pseudo-opcode that the encoder expands to a multi-instruction sequence. Only Add/Sub (and the bitwise pair ops) are decomposed into real ARM instructions at the ArmOp level. The Coq model now reflects that architecture, with axiomatized pseudo-op semantics analogous to how VFP is modeled. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
…attern)
CI failure on this branch surfaced that rules_rocq_rust requires every
Coq file's `Require Import Synth.X.Y.` line to be matched by a
corresponding `:y` target in the rocq_library's `deps` — transitive
deps through intermediate targets are NOT propagated to the coqc -Q
paths.
This is the pattern pulseengine/loom's proofs/BUILD.bazel uses (e.g.
:constant_folding lists both :wasm_semantics AND :term_semantics
directly, even though one is an alias to the other). synth's
:arm_instructions and :arm_semantics worked on main only because the
file content happened to not exercise the missing -Q paths under
rules_rocq_rust's caching layer; the v0.8.0 alignment changes broke
the happy accident.
Adds :base and :common as direct deps of:
- :arm_state (imports Synth.Common.Base + Synth.Common.Integers)
- :arm_instructions (same)
- :arm_semantics (same plus the previously-listed :arm_instructions
and now-redundant :arm_state for clarity)
No Coq source changes. Transitive chains preserved.
…braries Same root cause as the prior commit: rules_rocq_rust requires every `Require Import Synth.X.Y.` to have a matching `:y` target in the rocq_library's deps list. Transitive deps don't propagate `-Q` paths. This commit: - adds :base + :common as explicit deps to :wasm_values, :wasm_instructions, :wasm_semantics (they all import Synth.Common.Base + Synth.Common.Integers) - expands :compilation deps to include every directly-imported Synth.* module - same for :tactics - introduces _CORRECTNESS_FULL_DEPS list and reuses it for both correctness rocq_libraries (Group A + Group B), so the dep set stays consistent
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
This is v0.8.0 PR 1a — the prerequisite alignment step for the v0.8.0 milestone (umbrella issue #147). It fixes the verification gap surfaced by clean-room audit of PR #149.
The previous
coq/Synth/Synth/Compilation.vmodeled every i64 op as operating on a single 32-bit register (R0, R1) and a single ARM instruction — e.g.I64Add → [ADD R0 R0 (Reg R1)]. The real Rust compiler atcrates/synth-synthesis/src/instruction_selector.rs:1450emits a proper 64-bit add via the C flag (ADDS R0, R0, R2; ADC R1, R1, R3), with the i64 result spanning the(R0, R1)pair and the second operand in(R2, R3).The v0.8.0 umbrella's falsification statement explicitly forbids this kind of mismatch:
This PR closes the gap so that subsequent v0.8.0 lift PRs (PRs 2–5 in the queue) can rebase against an honest model.
Why this PR is small-scoped
Per the PR brief:
Quoted falsification clause (from #147)
The PR honors this by re-admitting any T1 proof whose result claim no longer matches the aligned compilation — see status table below.
Codegen survey
The full per-op survey lives at
docs/analysis/I64_CODEGEN_SURVEY.md. Highlights:I64Add,I64Sub(ADDS/ADC + SUBS/SBC pairs);I64And,I64Or,I64Xor(two AND/ORR/EOR per op, one on each half).I64Mul(UMULL + MLA cross products).I64Shl / ShrU / ShrS / Rotl / Rotr.I64Clz / Ctz / Popcnt(32-bit count result).I64SetCond(with condition field) andI64SetCondZ(unaryi64.eqz).I64DivS / DivU / RemS / RemU(gale software-helper calls__aeabi_*ldivmod).I64Const,I64ExtendI32S,I64ExtendI32U,I32WrapI64.I64Load,I64Store(8-byte, bounds-checked).ArmSemantics extensions
These are the minimum required to model the dual-precision arithmetic pattern:
ADDS,ADC,SUBS,SBCinstruction semantics inArmSemantics.v:ADDSsets the C flag from unsigned overflow (reuses existingcompute_c_flag_add).ADCaddsrn + op2 + C(reads C from prior state, does not set flags).SUBSsets C flag from unsigned borrow (reuses existingcompute_c_flag_sub).SBCsubtractsrn - op2 - NOT(C)(reads C).Status table: every previously-Qed i64 proof
i64_add_correct(T2)solve_single_armworks on the new 2-instr sequencei64_sub_correct(T2)i64_mul_correct(T2)I64MulPseudoreturnsSomei64_divs_correct(T1)I32.divsagainst a single-SDIV model that no longer existsi64_divu_correct(T1)i64_rems_correct(T1)i64_remu_correct(T1)i64_and / or / xor_correct(T2)solve_single_armi64_shl / shru / shrs / rotl / rotr_correct(T2)Somei64_eqz / eq / ne / lts / ltu / gts / gtu / les / leu / ges / geu_correct(T2)I64SetCond[Z]pseudo-opi64_clz / ctz / popcnt_correct(T2)i64_const_correct(T1)R0 = I32.repr (I64.unsigned n mod I32.modulus)was an artifact of the stale single-MOVW codegeni32_wrap_i64_executes(T2)I32WrapI64Pseudo R0 R0returnsSomei64_extend_i32_s_executes(T2)I64ExtendI32SPseudo R0 R1 R0returnsSomei64_extend_i32_u_executes(T2)I64ExtendI32UPseudo R0 R1 R0returnsSomei64_load_executes(T2)I64LoadPseudo R0 R1 R0 ...returnsSomei64_store_executes(T2)I64StorePseudo R0 R1 R2 ...returnsSomeNet change: -5 Qed (4 i64 div/rem T1 + 1 i64_const_correct T1), +5 Admitted, all with explicit "pending v0.8.0 PR X" pointer comments. Total proof count: 233 Qed / 10 Admitted → 228 Qed / 15 Admitted.
What ArmSemantics extensions were needed (one-line summary)
ADDS / ADC / SUBS / SBC: real ARM instructions with C-flag set/read — needed to model the i64 Add/Sub pattern faithfully.i64_mul_lo_bits,i64_shl_lo_bits, …,i64_setcond_bits,i64_divs_pair,i64_const_lo,i64_load_lo, …): one axiom per (op, output) — parallels VFP axiomatization. These do not constrain values, only existence; lift queue (PRs 2–5) replaces them with concreteI64.*-based defs.Architectural surprise
Almost every i64 op in the Rust compiler is a single high-level
ArmOp::I64*pseudo-opcode that the encoder expands to a multi-instruction sequence at the encode step. OnlyAdd/Sub(and bitwise pair ops) decompose into real ARM instructions at the ArmOp level. The Coq model now reflects that — closer in spirit to CompCert's approach for runtime calls (oneBL helper) than to the previous "model every emit as a sequence of real ARM instructions".Test plan
bazel test //coq:verify_proofs— green (228 Qed across all .v files, 15 documented admits).cargo test --workspaceshould be affected (no Rust changes in this PR).docs/analysis/I64_CODEGEN_SURVEY.mdand confirms each Compilation.v clause cites the correctinstruction_selector.rsline range.Related: umbrella #147, falsification clause; PR #149 (will rebase on top of this).
🤖 Generated with Claude Code