rocq/backend/RegsProof.v
# Soundness proofs for Regs.v
Machine-checked invariants of the Gallina register allocator, validator, parallel-move compiler and 3-address selection in Regs.v (M7 of docs/gallina-backend.md):
1. **Interval and call-point tests** (hreg_eqb_spec,
[ivals_disjoint_sound], [ivals_hit_points_sound]): disjoint interval lists share no program point, and an interval list that misses the sorted call points contains none of them.
2. **Allocation validator simulation** (check_rinst_step_sound,
[check_rinsts_rev_sound], [poll_edge_clobber_sound], [callee_saves_restore_sound], [lower_key_never_hreg]): any register map accepted by [check_rinsts_rev] and [check_succs_polls] preserves temporary values across instructions, simultaneous definitions, caller-saved register clobbers (`%r10`, `%r11`) at calls and poll edges, restores all five callee-saved registers (`%rbx`, `%r12`–`%r15`) on exit, and keeps capability lowers in stack root slots.
3. **Parallel moves** (ready_pmove_step_sound,
[cycle_break_step_sound]): peeling an unread destination or saving a cycle head into `%rcx` preserves the simultaneous assignment of all non-scratch locations.
4. **3-address lea and immediate selection**
([imm32_add_mod_sound], [imm32_sub_lea_w_sound], [imm32_sub_lea_l_sound]): signed 32-bit immediates and negated `lea` displacements compute the exact modular sum and difference at both 32-bit (`w`, including `-2^31`) and 64-bit (`l`) widths.
From Stdlib Require Import String ZArith List Bool Arith Lia
From Nanofil Require Import Term Syntax Maps
From Backend Require Import Plan Layout Emit Regs
Import ListNotations
Open Scope Z_scope
Open Scope list_scope
1. Hardware register equality and interval disjointness
Proof 1 step Qed
destruct r ; reflexivity
Proof 5 steps Qed
intros a b
split ; intro H
–destruct a , b ; simpl in H ; try discriminate ; reflexivity
–subst b
apply hreg_eqb_refl
Proof 3 steps Qed
Proof 3 steps Qed
Proof 3 steps Qed
Whether point p lies in some closed interval [lo, hi] of ivs.
match ivs with
[ ]
⇒
False
Strictly ordered interval list: each interval ends before the next begins, and every interval satisfies lo ≤ hi.
match ivs with
[ ]
⇒
True
Proof 7 steps Qed
induction ivs as | lo hi ivs′ IH ; intros bound p Hwf Hin ; simpl in *
–contradiction
Proof 3 steps Qed
destruct ivs as | lo hi ivs′ ; intros b1 b2 Hle Hwf ; simpl in * ; exact I |
destruct Hwf as H1 H2
split ; lia | exact H2
∀ fuel xs ys bx by0 p
False
Proof 34 steps Qed
induction fuel as | fuel′ IH ; intros xs ys bx by0 p Hwx Hwy Hdisj Hx Hy
–destruct xs as | a1 b1 xs′ ; simpl in Hx ; exact Hx |
destruct ys as | a2 b2 ys′ ; simpl in Hy ; exact Hy |
simpl in Hdisj
discriminate
–destruct xs as | a1 b1 xs′ ; simpl in Hx ; exact Hx |
destruct ys as | a2 b2 ys′ ; simpl in Hy ; exact Hy |
simpl in Hdisj
destruct Hwx as Hbx Hab1 Hwx′
destruct Hwy as Hby Hab2 Hwy′
destruct nat_ltbb1 a2 eqn: E1
+apply nat_ltb_spec in E1
simpl in Hx
destruct Hx as Hpa1 Hpb1 | Hx′
∗assert Hpge : a2 ≤ p%nat
{apply in_ivals_ge_bounda2, b2 :: ys' a2 p ; | exact Hy
simpl
split ; lia | split ; exact Hab2 | exact Hwy'
lia
∗eapply IH ; exact Hwx' | | exact Hdisj | exact Hx' | exact Hy
simpl
split ; exact Hby | split ; exact Hab2 | exact Hwy'
+destruct nat_ltbb2 a1 eqn: E2 ; | discriminate
apply nat_ltb_spec in E2
simpl in Hy
destruct Hy as Hpa2 Hpb2 | Hy′
∗assert Hpge : a1 ≤ p%nat
{apply in_ivals_ge_bounda1, b1 :: xs' a1 p ; | exact Hx
simpl
split ; lia | split ; exact Hab1 | exact Hwx'
lia
∗eapply IH ; | exact Hwy' | exact Hdisj | exact Hx | exact Hy'
simpl
split ; exact Hbx | split ; exact Hab1 | exact Hwx'
Disjoint well-formed interval lists share no program point.
Proof 3 steps Qed
intros xs ys p Hwx Hwy Hdisj Hx Hy
unfold ivals_disjoint in Hdisj
eapply ivals_disjoint_fuel_sound ; exact Hwx | exact Hwy | exact Hdisj | exact Hx | exact Hy
match pts with
[ ]
⇒
True
Proof 7 steps Qed
∀ fuel ivs pts bi bp p
False
Proof 34 steps Qed
induction fuel as | fuel′ IH ; intros ivs pts bi bp p Hwi Hwp Hhit Hin Hpt
simpl in Hhit
discriminate
simpl in Hhit
destruct Hwi as Hbi Hab Hwi′
destruct Hwp as Hbp Hwp′
+destruct nat_ltbq a eqn: E2 ; | discriminate
apply nat_ltb_spec in E2
simpl in Hpt
destruct Hpt as ← | Hpt′
∗assert Hale : a ≤ q%nat
{apply in_ivals_ge_bounda, b :: ivs' a q ; | exact Hin
simpl
split ; lia | split ; exact Hab | exact Hwi'
lia
∗eapply IH ; | exact Hwp' | exact Hhit | exact Hin | exact Hpt'
simpl
split ; exact Hbi | split ; exact Hab | exact Hwi'
When ivals_hit_points returns false, no call point in pts falls inside ivs.
Proof 3 steps Qed
intros ivs pts p Hwi Hwp Hhit Hin Hpt
unfold ivals_hit_points in Hhit
eapply ivals_hit_points_fuel_sound ; exact Hwi | exact Hwp | exact Hhit | exact Hin | exact Hpt
2. Validator soundness and forward simulation
Concrete register+slot state for a function body.
match ds, vs with
_, _
⇒
ms
match ds, vs with
_, _
⇒
tenv
A call clobbers caller-saved registers (%r10, %r11) with arbitrary values arb while preserving callee-saved registers and stack slots.
λ r ⇒
else
arbr
ms_slotms
State agreement on all temporaries in live (for mapped temporaries under dom = Somekm, and unconditionally on unmapped temporaries).
∀t, zmap_find_natt rm = None → ms_slotms t = tenvt ∧ ∀t, Int live → read_machrm ms t = tenvt
∀ r rs
hreg_in_listr rs = true ↔ Inr rs
Proof 9 steps Qed
intros r rs
induction rs as | r′ rs′ IH ; simpl
–split ; intro H ; discriminate | contradiction
–destruct hreg_eqbr r' eqn: E
+rewrite IH
split ; right ; exact H | intros Heq | Hin ; subst ; rewrite hreg_eqb_refl in E ; discriminate | exact Hin
Proof 16 steps Qed
intros rm ts
induction ts as | t ts′ IH ; intros seen t1 r Hnd Hin Hseen Hrm ; simpl in *
–contradiction
–destruct zmap_find_natt rm as rt | eqn: Ert
+destruct hreg_in_listrt seen eqn: Ein ; discriminate |
destruct Hin as ← | Hin′
∗rewrite Hrm in Ert
injection Ert as ←
pose proof proj2hreg_in_list_specr seen Hseen as Ht
rewrite Ht in Ein
discriminate
∗eapply IH ; exact Hnd | exact Hin' | right ; exact Hseen | exact Hrm
When no_dup_hregs holds on a duplicate-free list ts, distinct elements in ts never map to the same hreg.
∀ rm ts t1 t2 r
NoDupts
no_dup_hregsrm ts = true
Int1 ts
Int2 ts
t1 ≠ t2
zmap_find_natt1 rm = Somer
zmap_find_natt2 rm = Somer
False
Proof 21 steps Qed
unfold no_dup_hregs
intros rm ts Hndup
assert Hgen : ∀seen, no_dup_hregs_accrm ts seen = true → ∀t1 t2 r, Int1 ts → Int2 ts → t1 ≠ t2 → zmap_find_natt1 rm = Somer → zmap_find_natt2 rm = Somer → False
{induction Hndup as | t ts′ Hnotin Hndup′ IH ; intros seen Hacc t1 t2 r Hin1 Hin2 Hneq Hr1 Hr2 ; simpl in *
–contradiction
–destruct zmap_find_natt rm as rt | eqn: Ert
+destruct hreg_in_listrt seen eqn: Ein ; discriminate |
destruct Hin1 as ← | Hin1′ ; destruct Hin2 as ← | Hin2′
∗congruence
∗rewrite Hr1 in Ert
injection Ert as ←
eapply no_dup_hregs_acc_disjoint ; exact Hacc | exact Hin2' | left ; reflexivity | exact Hr2
∗rewrite Hr2 in Ert
injection Ert as ←
eapply no_dup_hregs_acc_disjoint ; exact Hacc | exact Hin1' | left ; reflexivity | exact Hr1
∗eapply IH ; exact Hacc | exact Hin1' | exact Hin2' | exact Hneq | exact Hr1 | exact Hr2
+destruct Hin1 as ← | Hin1′ ; rewrite Hr1 in Ert ; discriminate |
destruct Hin2 as ← | Hin2′ ; rewrite Hr2 in Ert ; discriminate |
eapply IH ; exact Hacc | exact Hin1' | exact Hin2' | exact Hneq | exact Hr1 | exact Hr2
intros Hacc
eapply Hgen ; exact Hacc
Proof 10 steps Qed
intros rm ts
induction ts as | x ts′ IH ; intros t r Hall Hin Hrm ; simpl in *
–contradiction
–destruct Hin as ← | Hin′
+rewrite Hrm in Hall
destruct hreg_callee_savedr ; reflexivity | discriminate
+destruct zmap_find_natx rm as rx |
∗destruct hreg_callee_savedrx ; | discriminate
eapply IH ; eauto
∗eapply IH ; eauto
Clobbering caller-saved registers preserves state_agrees on any set ts accepted by all_callee_saved.
∀ rm ts tenv ms arb
all_callee_savedrm ts = true
state_agreesrm ts tenv ms
state_agreesrm ts tenv clobber_callarb ms
Proof 13 steps Qed
intros rm ts tenv ms arb Hcs Hslot Hlive
split
–intros t Hnone
simpl
apply Hslot
exact Hnone
–intros t Hin
unfold read_mach in *
specialize Hlivet Hin
destruct zmap_find_natt rm as r | eqn: Er ; simpl
+rewrite all_callee_saved_specrm ts t r Hcs Hin Er
exact Hlive
+exact Hlive
Corollary for poll edges: when check_succs_polls accepts a Poll edge to block si, filc_pollcheck_slow clobbering caller-saved registers preserves every live-in and phi-defined temporary of si.
∀ rm header_live tenv ms arb
all_callee_savedrm header_live = true
state_agreesrm header_live tenv ms
state_agreesrm header_live tenv clobber_callarb ms
Proof 2 steps Qed
intros
apply clobber_preserves_agrees ; assumption
∀r t, Int live → t ≠ d → zmap_find_natd rm = Somer → zmap_find_natt rm = Somer → False
∀ rm live tenv ms d v
dest_no_collisionrm d live
state_agreesrm filterλt ⇒ negbNat.eqbt d live tenv ms
state_agreesrm live
λ t ⇒
else
tenvt
write_machrm ms d v
Proof 40 steps Qed
intros rm live tenv ms d v Hdisj Hslot Hlive
split
–intros t Hnone
unfold write_mach
destruct zmap_find_natd rm as rd | eqn: Erd ; simpl
∗apply Nat.eqb_eq in Etd
subst t
rewrite Hnone in Erd
discriminate
∗apply Hslot
exact Hnone
–intros t Hin
unfold read_mach , write_mach
+apply Nat.eqb_eq in Etd
subst t
destruct zmap_find_natd rm as rd | eqn: Erd ; simpl
∗rewrite hreg_eqb_refl
reflexivity
∗rewrite Nat.eqb_refl
reflexivity
{apply filter_In
split ; exact Hin | rewrite Etd ; reflexivity
specialize Hlivet Hin_filt
unfold read_mach in Hlive
destruct zmap_find_natd rm as rd | eqn: Erd ; destruct zmap_find_natt rm as rt | eqn: Ert ; simpl
∗destruct hreg_eqbrt rd eqn: Er
--apply hreg_eqb_spec in Er
subst rt
exfalso
apply Nat.eqb_neq in Etd
eapply Hdisj ; exact Hin | exact Etd | exact Erd | exact Ert
--exact Hlive
∗exact Hlive
∗exact Hlive
∗rewrite Etd
exact Hlive
Helper predicates and state steps for check_rinst_step_sound, stated at top level so the theorem renders as an inference rule without nested let or match blocks.
match call with
_
⇒
True
match call with
_
⇒
True
match call with
_
⇒
ms
match call with
Complete one-instruction simulation theorem: reading inputs uses, clobbering caller-saved registers according to call, and writing destination d preserves state_agrees whenever no_dup_hregs and all_callee_saved hold as checked by check_rinsts_rev.
∀ rm live_after d uses call f arb1 arb2 tenv ms
dest_no_collisionrm d live_after
call_mid_okrm call live_withoutd live_after
call_pre_okrm call uses ++ live_withoutd live_after
state_agreesrm uses ++ live_withoutd live_after tenv ms
mapread_machrm pre_call_statecall arb1 ms uses = maptenv uses ∧ state_agreesrm live_after tenv_settenv d fmaptenv uses write_machrm post_call_statecall arb2 pre_call_statecall arb1 ms d fmapread_machrm pre_call_statecall arb1 ms uses
Proof 43 steps Qed
intros rm live_after d uses call f arb1 arb2 tenv ms Hnodup Hca Hcd Hagree
set live_mid := live_withoutd live_after in *
set live_before := uses ++ live_mid in *
set ms_pre := pre_call_statecall arb1 ms
assert Hagree_pre : state_agreesrm live_before tenv ms_pre
{unfold ms_pre , pre_call_state
destruct call ; try exact Hagree
apply clobber_preserves_agrees ; exact Hcd | exact Hagree
assert Hargs : mapread_machrm ms_pre uses = maptenv uses
{apply map_ext_in
intros u Hu
destruct Hagree_pre as _ Hlb
apply Hlb
unfold live_before
apply in_or_app
left
exact Hu
split ; exact Hargs |
rewrite Hargs
unfold tenv_set
apply write_mach_step_sound ; exact Hnodup |
assert Hagree_mid : state_agreesrm live_mid tenv ms_pre
{destruct Hagree_pre as Hs Hlb
split ; exact Hs |
intros t Ht
apply Hlb
unfold live_before
apply in_or_app
right
exact Ht
unfold post_call_state
destruct call
–exact Hagree_mid
–apply clobber_preserves_agrees ; exact Hca | exact Hagree_mid
–apply clobber_preserves_agrees
+simpl in Hcd
clear - Hcd
unfold live_before in Hcd
induction uses as | u uses′ IH ; simpl in * ; exact Hcd |
destruct zmap_find_natu rm as ru |
∗destruct hreg_callee_savedru ; exact IHHcd | discriminate
∗exact IHHcd
+exact Hagree_mid
Callee-saved save and restore invariant: every callee-saved register r is restored to its caller entry value entry_regsr, whether r was saved and restored from its dedicated save slot (because rm used r) or untouched throughout the body (because rm never assigned r and every call preserves callee-saved registers).
λ r ⇒
else
save_memr
λ r ⇒
else
body_regsr
hreg_callee_savedr = true
hreg_in_listr used = false → body_regsr = entry_regsr
exec_restoresused exec_savesused entry_regs save_mem0 body_regs r = entry_regsr
Proof 6 steps Qed
intros used entry_regs body_regs save_mem0 r _ Huntouched
unfold exec_restores , exec_saves
destruct hreg_in_listr used eqn: Ein
–reflexivity
–apply Huntouched
reflexivity
∀ rc k r
key_pm_locrc KLowerk ≠ SomePmRegr
3. Parallel-move soundness
Abstract valuation of parallel-move locations.
λ l ⇒
else
envl
∀ l
pm_loc_eqbl l = true
Proof 4 steps Qed
∀ a b
pm_loc_eqba b = true ↔ a = b
Proof 7 steps Qed
intros a b
destruct a as r1 | o1 | , b as r2 | o2 | ; simpl ; try split ; intro H ; discriminate | congruence
–rewrite hreg_eqb_spec
split ; congruence
–rewrite Z.eqb_eq
split ; congruence
–split ; reflexivity
∀ env m m′
loc_read_in_pmovespmv_dstm m′ = false
eval_pm_srcexec_pmove_absenv m pmv_halfm′ pmv_srcm′ = eval_pm_srcenv pmv_halfm′ pmv_srcm′
Proof 10 steps Qed
intros env m m′ Hnr
simpl in Hnr
unfold eval_pm_src , exec_pmove_abs
destruct pm_loc_eqbl' pmv_dstm eqn: E
–reflexivity
∀ env m rest
loc_read_in_pmovespmv_dstm rest = false
exec_pmove_absenv m pmv_dstm = eval_pm_srcenv pmv_halfm pmv_srcm ∧ ∀m′, Inm′ rest → eval_pm_srcexec_pmove_absenv m pmv_halfm′ pmv_srcm′ = eval_pm_srcenv pmv_halfm′ pmv_srcm′ ∧ ∀l, l ≠ pmv_dstm → exec_pmove_absenv m l = envl
Proof 20 steps Qed
intros env m rest Hnr
split ; | split
–intros m′ Hin
induction rest as | r0 rs IH ; simpl in *
+contradiction
–intros l Hneq
unfold exec_pmove_abs
destruct pm_loc_eqbl pmv_dstm eqn: E ; | reflexivity
apply pm_loc_eqb_spec in E
contradiction
Cycle-breaking step: saving old into PmCycleTmp (%rcx) and rewriting reads of old to PmCycleTmp preserves the target value of every move (provided PmCycleTmp was not previously read) and eliminates all reads of old, making old immediately ready on the next step.
λ l ⇒
else
envl
let src′ ≔
s
⇒
s
in
_
⇒
True
∀ env old m
old ≠ PmCycleTmp
eval_pm_srcsave_cycle_absenv old pmv_halfsubst_one_pmoveold m pmv_srcsubst_one_pmoveold m = eval_pm_srcenv pmv_halfm pmv_srcm ∧ loc_read_in_pmovesold subst_one_pmoveold m = false
Proof 26 steps Qed
intros env old m Hnot_tmp Hno_tmp
unfold no_cycle_tmp_src in Hno_tmp
unfold save_cycle_abs , subst_one_pmove , eval_pm_src
simpl
–destruct pm_loc_eqbl old eqn: Elo
+apply pm_loc_eqb_spec in Elo
subst l
simpl
split ; reflexivity |
destruct pm_loc_eqbold PmCycleTmp eqn: Ebad ; | reflexivity
apply pm_loc_eqb_spec in Ebad
contradiction
+simpl
destruct pm_loc_eqbl PmCycleTmp eqn: Elt
∗split ; reflexivity |
destruct pm_loc_eqbold l eqn: Eol ; | reflexivity
apply pm_loc_eqb_spec in Eol
subst l
rewrite pm_loc_eqb_refl in Elo
discriminate
–split ; reflexivity
–split ; reflexivity
4. Soundness of 3-address lea and immediate selection
integer_immediate produces a value congruent to n modulo 2 ^ 32 (half = true) or 2 ^ 64 (half = false).
Proof 16 steps Qed
intros | n iv H ; unfold integer_immediate in H
–injection H as ←
rewrite Zminus_mod_idemp_l
replace n + 2147483648 − 2147483648 with n by lia
reflexivity
Immediate add and lea disp(%rx) compute x + n mod M at both 32-bit and 64-bit widths.
∀ half x n iv
integer_immediatehalf n = Someiv
Proof 8 steps Qed
intros half x n iv H
pose proof imm32_congruenthalf n iv H as Hc
rewrite H1 , H2 by exact Hm
rewrite Hc
reflexivity
Proof 4 steps Qed
Proof 4 steps Qed
intros x n iv H
rewrite mod_two64_mod_two32
replace x − n with x + −n by lia
exact imm32_add_mod_soundtrue x −n iv H
64-bit Sub via leaq (-n)(%rx), %dst computes x − n mod 2 ^ 64.
Proof 3 steps Qed
5. Executable rejection examples for valid_alloc
zmap_add_nat0%nat L zmap_add_nat1%nat L zmap_add_nat2%nat Double ZMap.emptyclass
zmap_add_natt r ZMap.emptyhreg
Two live parameters mapped to the same register HRbx are rejected.
720Example ex_rejects_collision: valid_allocex_cmap2 0%nat; 1%nat ex_rb_collision ex_rm_collision = false
Proof 1 step Qed
reflexivity
mkRBlock0%nat [ ] [ ] mkRInst[ ] [ ] RCallAfterReads 0%nat
A caller-saved register HR10 live across RCallAfterReads is rejected, while callee-saved HRbx is accepted.
729Example ex_rejects_r10_call: valid_allocex_cmap2 0%nat ex_rb_after_call ex_rm10%nat HR10 = false ∧ valid_allocex_cmap2 0%nat ex_rb_after_call ex_rm10%nat HRbx = true
Proof 1 step Qed
split ; reflexivity
mkRBlock0%nat [ ] [ ] mkRInst0%nat [ ] RCallDuringReads [ ]
Input of RCallDuringReads (AStorePointer / ADispatch) in HR11 is rejected even when dead after the instruction.
739Example ex_rejects_r11_read_call: valid_allocex_cmap2 0%nat ex_rb_during_call ex_rm10%nat HR11 = false ∧ valid_allocex_cmap2 0%nat ex_rb_during_call ex_rm10%nat HR12 = true
Proof 1 step Qed
split ; reflexivity
mkRBlock1%nat 1%nat, true 1%nat, 0%nat, Some0%nat; 1%nat, Some1%nat [ ] 1%nat
752Example ex_rejects_r10_poll: valid_allocex_cmap2 0%nat ex_rb_poll0; ex_rb_poll1 ex_rm11%nat HR10 = false ∧ valid_allocex_cmap2 0%nat ex_rb_poll0; ex_rb_poll1 ex_rm11%nat HR13 = true
Proof 1 step Qed
split ; reflexivity
Assigning a float temporary (Double) to a general register is rejected.
Proof 1 step Qed
reflexivity