Proof of correctness for individual instructions

Require Import Coqlib Errors Maps.
Require Import AST Integers Floats Values Memory Globalenvs.
Require Import Op Locations Machblock Conventions.
Require Import Asmblock Asmblockgen Asmblockgenproof0 Asmblockprops.
Require Import Chunks.
Require Import Lia.

Import PArithCoercions.


Lemma make_immed32_sound:
  forall n,
  match make_immed32 n with
  | Imm32_single imm => n = imm
  end.

Lemma make_immed64_sound:
  forall n,
  match make_immed64 n with
  | Imm64_single imm => n = imm
  end.



Lemma ireg_of_not_RTMP:
  forall m r, ireg_of m = OK r -> IR r <> IR RTMP.

Lemma ireg_of_not_RTMP':
  forall m r, ireg_of m = OK r -> r <> RTMP.

#[global] Hint Resolve ireg_of_not_RTMP ireg_of_not_RTMP': asmgen.



Ltac Simplif :=
  ((rewrite nextblock_inv by eauto with asmgen)
  || (rewrite nextblock_inv1 by eauto with asmgen)
  || (rewrite Pregmap.gss)
  || (rewrite nextblock_pc)
  || (rewrite Pregmap.gso by eauto with asmgen)
  ); auto with asmgen.

Ltac Simpl := repeat Simplif.

Correctness of RISC-V constructor functions

Section CONSTRUCTORS.

Variable ge: genv.
Variable fn: function.

Lemma loadimm32_correct:
  forall rd n k rs m,
  exists rs',
     exec_straight ge (loadimm32 rd n ::g k) rs m k rs' m
  /\ rs'#rd = Vint n
  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.

Lemma loadimm64_correct:
  forall rd n k rs m,
  exists rs',
     exec_straight ge (loadimm64 rd n ::g k) rs m k rs' m
  /\ rs'#rd = Vlong n
  /\ forall r, r <> PC -> r <> rd -> r <> RTMP -> rs'#r = rs#r.

Lemma opimm64_correct:
  forall (op: arith_name_rrr)
         (opi: arith_name_rri64)
         (sem: val -> val -> val) m,
  (forall d s1 s2 rs,
   exec_basic_instr ge (op d s1 s2) rs m = Next ((rs#d <- (sem rs#s1 rs#s2))) m) ->
  (forall d s n rs,
   exec_basic_instr ge (opi d s n) rs m = Next ((rs#d <- (sem rs#s (Vlong n)))) m) ->
  forall rd r1 n k rs,
  r1 <> RTMP ->
  exists rs',
     exec_straight ge (opimm64 op opi rd r1 n ::g k) rs m k rs' m
  /\ rs'#rd = sem rs#r1 (Vlong n)
  /\ forall r, r <> PC -> r <> rd -> r <> RTMP -> rs'#r = rs#r.


Lemma addptrofs_correct:
  forall rd r1 n k rs m,
  r1 <> RTMP ->
  exists rs',
     exec_straight ge (addptrofs rd r1 n ::g k) rs m k rs' m
  /\ Val.lessdef (Val.offset_ptr rs#r1 n) rs'#rd
  /\ forall r, r <> PC -> r <> rd -> r <> RTMP -> rs'#r = rs#r.

Ltac ArgsInv :=
  repeat (match goal with
  | [ H: Error _ = OK _ |- _ ] => discriminate
  | [ H: match ?args with nil => _ | _ :: _ => _ end = OK _ |- _ ] => destruct args
  | [ H: bind _ _ = OK _ |- _ ] => monadInv H
  | [ H: match _ with left _ => _ | right _ => assertion_failed end = OK _ |- _ ] => monadInv H; ArgsInv
  | [ H: match _ with true => _ | false => assertion_failed end = OK _ |- _ ] => monadInv H; ArgsInv
  end);
  subst;
  repeat (match goal with
  | [ H: ireg_of _ = OK _ |- _ ] => simpl in *; rewrite (ireg_of_eq _ _ H) in *
  | [ H: freg_of _ = OK _ |- _ ] => simpl in *; rewrite (freg_of_eq _ _ H) in *
  end).

Inductive exec_straight_opt: list instruction -> regset -> mem -> list instruction -> regset -> mem -> Prop :=
  | exec_straight_opt_refl: forall c rs m,
      exec_straight_opt c rs m c rs m
  | exec_straight_opt_intro: forall c1 rs1 m1 c2 rs2 m2,
      exec_straight ge c1 rs1 m1 c2 rs2 m2 ->
      exec_straight_opt c1 rs1 m1 c2 rs2 m2.

Remark exec_straight_opt_right:
  forall c3 rs3 m3 c1 rs1 m1 c2 rs2 m2,
  exec_straight_opt c1 rs1 m1 c2 rs2 m2 ->
  exec_straight ge c2 rs2 m2 c3 rs3 m3 ->
  exec_straight ge c1 rs1 m1 c3 rs3 m3.

Lemma transl_comp_correct:
  forall cmp r1 r2 lbl k rs m tbb b,
  exists rs',
     exec_straight ge (transl_comp cmp Signed r1 r2 lbl k) rs m (Pcb BTwnez RTMP lbl ::g k) rs' m
  /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)
  /\ ( Val.cmp_bool cmp rs#r1 rs#r2 = Some b ->
       exec_control ge fn (Some (PCtlFlow (Pcb BTwnez RTMP lbl))) (nextblock tbb rs') m
        = eval_branch fn lbl (nextblock tbb rs') m (Some b))
  .

Lemma transl_compi_correct:
  forall cmp r1 n lbl k rs m tbb b,
  exists rs',
     exec_straight ge (transl_compi cmp Signed r1 n lbl k) rs m (Pcb BTwnez RTMP lbl ::g k) rs' m
  /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)
  /\ ( Val.cmp_bool cmp rs#r1 (Vint n) = Some b ->
       exec_control ge fn (Some (PCtlFlow (Pcb BTwnez RTMP lbl))) (nextblock tbb rs') m
        = eval_branch fn lbl (nextblock tbb rs') m (Some b))
  .

Lemma transl_compu_correct:
  forall cmp r1 r2 lbl k rs m tbb b,
  exists rs',
     exec_straight ge (transl_comp cmp Unsigned r1 r2 lbl k) rs m (Pcb BTwnez RTMP lbl ::g k) rs' m
  /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)
  /\ (Val.mxcmpu_bool cmp rs#r1 rs#r2 = Some b ->
       exec_control ge fn (Some (PCtlFlow ((Pcb BTwnez RTMP lbl)))) (nextblock tbb rs') m
        = eval_branch fn lbl (nextblock tbb rs') m (Some b))
  .

Lemma transl_compui_correct:
  forall cmp r1 n lbl k rs m tbb b,
  exists rs',
     exec_straight ge (transl_compi cmp Unsigned r1 n lbl k) rs m (Pcb BTwnez RTMP lbl ::g k) rs' m
  /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)
  /\ (Val.mxcmpu_bool cmp rs#r1 (Vint n) = Some b ->
       exec_control ge fn (Some (PCtlFlow ((Pcb BTwnez RTMP lbl)))) (nextblock tbb rs') m
        = eval_branch fn lbl (nextblock tbb rs') m (Some b))
  .

Lemma transl_compl_correct:
  forall cmp r1 r2 lbl k rs m tbb b,
  exists rs',
     exec_straight ge (transl_compl cmp Signed r1 r2 lbl k) rs m (Pcb BTwnez RTMP lbl ::g k) rs' m
  /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)
  /\ ( Val.cmpl_bool cmp rs#r1 rs#r2 = Some b ->
       exec_control ge fn (Some (PCtlFlow (Pcb BTwnez RTMP lbl))) (nextblock tbb rs') m
        = eval_branch fn lbl (nextblock tbb rs') m (Some b))
  .

Lemma transl_compil_correct:
  forall cmp r1 n lbl k rs m tbb b,
  exists rs',
     exec_straight ge (transl_compil cmp Signed r1 n lbl k) rs m (Pcb BTwnez RTMP lbl ::g k) rs' m
  /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)
  /\ ( Val.cmpl_bool cmp rs#r1 (Vlong n) = Some b ->
       exec_control ge fn (Some (PCtlFlow (Pcb BTwnez RTMP lbl))) (nextblock tbb rs') m
        = eval_branch fn lbl (nextblock tbb rs') m (Some b))
  .

Lemma swap_comparison_cmpf_eq:
  forall v1 v2 cmp,
  (Val.cmpf cmp v1 v2) = (Val.cmpf (swap_comparison cmp) v2 v1).

Lemma swap_comparison_cmpf_bool:
  forall cmp ft v1 v2,
  ftest_for_cmp cmp = Reversed ft ->
  Val.cmpf_bool cmp v1 v2 = Val.cmpf_bool (swap_comparison cmp) v2 v1.

Lemma transl_compf_correct:
  forall cmp r1 r2 lbl k rs m tbb b,
  exists rs',
     exec_straight ge (transl_comp_float64 cmp r1 r2 lbl k) rs m (Pcb BTwnez RTMP lbl ::g k) rs' m
  /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)
  /\ ( Val.cmpf_bool cmp rs#r1 rs#r2 = Some b ->
       exec_control ge fn (Some (PCtlFlow (Pcb BTwnez RTMP lbl))) (nextblock tbb rs') m
        = eval_branch fn lbl (nextblock tbb rs') m (Some b))
  .

Lemma cmpf_bool_ne_eq:
  forall v1 v2,
  Val.cmpf_bool Cne v1 v2 = option_map negb (Val.cmpf_bool Ceq v1 v2).

Lemma cmpf_bool_ne_eq_rev:
  forall v1 v2,
  Val.cmpf_bool Ceq v1 v2 = option_map negb (Val.cmpf_bool Cne v1 v2).

Lemma option_map_negb_negb:
  forall v,
  option_map negb (option_map negb v) = v.

Lemma notbool_option_map_negb:
  forall v, Val.notbool (Val.of_optbool v) = Val.of_optbool (option_map negb v).

Lemma swap_comparison_cmpf_bool_notftest:
  forall cmp ft v1 v2,
  notftest_for_cmp cmp = Reversed ft ->
  Val.cmpf_bool cmp v1 v2 = Val.cmpf_bool (swap_comparison cmp) v2 v1.

Lemma transl_compnotf_correct:
  forall cmp r1 r2 lbl k rs m tbb b,
  exists rs',
     exec_straight ge (transl_comp_notfloat64 cmp r1 r2 lbl k) rs m (Pcb BTwnez RTMP lbl ::g k) rs' m
  /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)
  /\ (option_map negb (Val.cmpf_bool cmp rs#r1 rs#r2) = Some b ->
       exec_control ge fn (Some (PCtlFlow (Pcb BTwnez RTMP lbl))) (nextblock tbb rs') m
        = eval_branch fn lbl (nextblock tbb rs') m (Some b))
  .

Lemma swap_comparison_cmpfs_bool:
  forall cmp ft v1 v2,
  ftest_for_cmp cmp = Reversed ft ->
  Val.cmpfs_bool cmp v1 v2 = Val.cmpfs_bool (swap_comparison cmp) v2 v1.

Lemma transl_compfs_correct:
  forall cmp r1 r2 lbl k rs m tbb b,
  exists rs',
     exec_straight ge (transl_comp_float32 cmp r1 r2 lbl k) rs m (Pcb BTwnez RTMP lbl ::g k) rs' m
  /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)
  /\ ( Val.cmpfs_bool cmp rs#r1 rs#r2 = Some b ->
       exec_control ge fn (Some (PCtlFlow (Pcb BTwnez RTMP lbl))) (nextblock tbb rs') m
        = eval_branch fn lbl (nextblock tbb rs') m (Some b))
  .

Lemma swap_comparison_cmpfs_bool_notftest:
  forall cmp ft v1 v2,
  notftest_for_cmp cmp = Reversed ft ->
  Val.cmpfs_bool cmp v1 v2 = Val.cmpfs_bool (swap_comparison cmp) v2 v1.

Lemma cmpfs_bool_ne_eq:
  forall v1 v2,
  Val.cmpfs_bool Cne v1 v2 = option_map negb (Val.cmpfs_bool Ceq v1 v2).

Lemma cmpfs_bool_ne_eq_rev:
  forall v1 v2,
  Val.cmpfs_bool Ceq v1 v2 = option_map negb (Val.cmpfs_bool Cne v1 v2).

Lemma transl_compnotfs_correct:
  forall cmp r1 r2 lbl k rs m tbb b,
  exists rs',
     exec_straight ge (transl_comp_notfloat32 cmp r1 r2 lbl k) rs m (Pcb BTwnez RTMP lbl ::g k) rs' m
  /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)
  /\ (option_map negb (Val.cmpfs_bool cmp rs#r1 rs#r2) = Some b ->
       exec_control ge fn (Some (PCtlFlow (Pcb BTwnez RTMP lbl))) (nextblock tbb rs') m
        = eval_branch fn lbl (nextblock tbb rs') m (Some b))
  .

Lemma transl_complu_correct:
  forall cmp r1 r2 lbl k rs m tbb b,
  exists rs',
     exec_straight ge (transl_compl cmp Unsigned r1 r2 lbl k) rs m (Pcb BTwnez RTMP lbl ::g k) rs' m
  /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)
  /\ ( Val.mxcmplu_bool cmp rs#r1 rs#r2 = Some b ->
       exec_control ge fn (Some (PCtlFlow (Pcb BTwnez RTMP lbl))) (nextblock tbb rs') m
        = eval_branch fn lbl (nextblock tbb rs') m (Some b))
  .

Lemma transl_compilu_correct:
  forall cmp r1 n lbl k rs m tbb b,
  exists rs',
     exec_straight ge (transl_compil cmp Unsigned r1 n lbl k) rs m (Pcb BTwnez RTMP lbl ::g k) rs' m
  /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)
  /\ ( Val.mxcmplu_bool cmp rs#r1 (Vlong n) = Some b ->
       exec_control ge fn (Some (PCtlFlow (Pcb BTwnez RTMP lbl))) (nextblock tbb rs') m
        = eval_branch fn lbl (nextblock tbb rs') m (Some b))
  .

Lemma transl_opt_compuimm_correct:
  forall n cmp r1 lbl k rs m b tbb c,
  select_comp n cmp = Some c ->
  exists rs', exists insn,
     exec_straight_opt (transl_opt_compuimm n cmp r1 lbl k) rs m ((PControl insn) ::g k) rs' m
  /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)
  /\ ( Val.mxcmpu_bool cmp rs#r1 (Vint n) = Some b ->
       exec_control ge fn (Some insn) (nextblock tbb rs') m = eval_branch fn lbl (nextblock tbb rs') m (Some b))
  .

Lemma transl_opt_compluimm_correct:
  forall n cmp r1 lbl k rs m b tbb c,
  select_compl n cmp = Some c ->
  exists rs', exists insn,
     exec_straight_opt (transl_opt_compluimm n cmp r1 lbl k) rs m ((PControl insn) ::g k) rs' m
  /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)
  /\ ( Val.mxcmplu_bool cmp rs#r1 (Vlong n) = Some b ->
       exec_control ge fn (Some insn) (nextblock tbb rs') m = eval_branch fn lbl (nextblock tbb rs') m (Some b))
  .

Local Hint Resolve Val.mxcmpu_bool_correct Val.mxcmplu_bool_correct: core.

Lemma transl_cbranch_correct_1:
  forall cond args lbl k c m ms b sp rs m' tbb,
  transl_cbranch cond args lbl k = OK c ->
  eval_condition cond (List.map ms args) m = Some b ->
  agree ms sp rs ->
  Mem.extends m m' ->
  exists rs', exists insn,
     exec_straight_opt c rs m' ((PControl insn) ::g k) rs' m'
  /\ exec_control ge fn (Some insn) (nextblock tbb rs') m' = eval_branch fn lbl (nextblock tbb rs') m' (Some b)
  /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r.

Lemma transl_cbranch_correct_true:
  forall cond args lbl k c m ms sp rs m' tbb,
  transl_cbranch cond args lbl k = OK c ->
  eval_condition cond (List.map ms args) m = Some true ->
  agree ms sp rs ->
  Mem.extends m m' ->
  exists rs', exists insn,
     exec_straight_opt c rs m' ((PControl insn) ::g k) rs' m'
  /\ exec_control ge fn (Some insn) (nextblock tbb rs') m' = goto_label fn lbl (nextblock tbb rs') m'
  /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r.

Lemma transl_cbranch_correct_false:
  forall cond args lbl k c m ms sp rs tbb m',
  transl_cbranch cond args lbl k = OK c ->
  eval_condition cond (List.map ms args) m = Some false ->
  agree ms sp rs ->
  Mem.extends m m' ->
  exists rs', exists insn,
     exec_straight_opt c rs m' ((PControl insn) ::g k) rs' m'
  /\ exec_control ge fn (Some insn) (nextblock tbb rs') m' = Next (nextblock tbb rs') m'
  /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r.


Lemma transl_cond_int32s_correct:
  forall cmp rd r1 r2 k rs m,
  exists rs',
     exec_straight ge (basics_to_code (transl_cond_int32s cmp rd r1 r2 k)) rs m (basics_to_code k) rs' m
  /\ Val.lessdef (Val.cmp cmp rs#r1 rs#r2) rs'#rd
  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.


Lemma transl_cond_int32u_correct:
  forall cmp rd r1 r2 k rs m,
  exists rs',
     exec_straight ge (basics_to_code (transl_cond_int32u cmp rd r1 r2 k)) rs m (basics_to_code k) rs' m
  /\ rs'#rd = Val.mxcmpu cmp rs#r1 rs#r2
  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.

Lemma transl_cond_int64s_correct:
  forall cmp rd r1 r2 k rs m,
  exists rs',
     exec_straight ge (basics_to_code (transl_cond_int64s cmp rd r1 r2 k)) rs m (basics_to_code k) rs' m
  /\ Val.lessdef (Val.maketotal (Val.cmpl cmp rs#r1 rs#r2)) rs'#rd
  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.

Lemma transl_cond_int64u_correct:
  forall cmp rd r1 r2 k rs m,
  exists rs',
     exec_straight ge (basics_to_code (transl_cond_int64u cmp rd r1 r2 k)) rs m (basics_to_code k) rs' m
  /\ rs'#rd = Val.mxcmplu cmp rs#r1 rs#r2
  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.

Lemma transl_condimm_int32s_correct:
  forall cmp rd r1 n k rs m,
  r1 <> RTMP ->
  exists rs',
     exec_straight ge (basics_to_code (transl_condimm_int32s cmp rd r1 n k)) rs m (basics_to_code k) rs' m
  /\ Val.lessdef (Val.cmp cmp rs#r1 (Vint n)) rs'#rd
  /\ forall r, r <> PC -> r <> rd -> r <> RTMP -> rs'#r = rs#r.

Local Hint Resolve Val.mxcmpu_correct Val.mxcmplu_correct: core.

Lemma transl_condimm_int32u_correct:
  forall cmp rd r1 n k rs m,
  r1 <> RTMP ->
  exists rs',
     exec_straight ge (basics_to_code (transl_condimm_int32u cmp rd r1 n k)) rs m (basics_to_code k) rs' m
  /\ Val.lessdef (Val.cmpu (Mem.valid_pointer m) cmp rs#r1 (Vint n)) rs'#rd
  /\ forall r, r <> PC -> r <> rd -> r <> RTMP -> rs'#r = rs#r.

Lemma transl_condimm_int64s_correct:
  forall cmp rd r1 n k rs m,
  r1 <> RTMP ->
  exists rs',
     exec_straight ge (basics_to_code (transl_condimm_int64s cmp rd r1 n k)) rs m (basics_to_code k) rs' m
  /\ Val.lessdef (Val.maketotal (Val.cmpl cmp rs#r1 (Vlong n))) rs'#rd
  /\ forall r, r <> PC -> r <> rd -> r <> RTMP -> rs'#r = rs#r.

Lemma transl_condimm_int64u_correct:
  forall cmp rd r1 n k rs m,
  r1 <> RTMP ->
  exists rs',
     exec_straight ge (basics_to_code (transl_condimm_int64u cmp rd r1 n k)) rs m (basics_to_code k) rs' m
  /\ Val.lessdef (Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp rs#r1 (Vlong n))) rs'#rd
  /\ forall r, r <> PC -> r <> rd -> r <> RTMP -> rs'#r = rs#r.

Lemma swap_comparison_cmpfs:
  forall v1 v2 cmp,
  Val.lessdef (Val.cmpfs cmp v1 v2) (Val.cmpfs (swap_comparison cmp) v2 v1).

Lemma transl_cond_float32_correct:
  forall cmp rd r1 r2 k rs m,
  exists rs',
     exec_straight ge (basics_to_code (transl_cond_float32 cmp rd r1 r2 k)) rs m (basics_to_code k) rs' m
  /\ Val.lessdef (Val.cmpfs cmp rs#r1 rs#r2) rs'#rd
  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.

Lemma transl_cond_nofloat32_correct:
  forall cmp rd r1 r2 k rs m,
  exists rs',
     exec_straight ge (basics_to_code (transl_cond_notfloat32 cmp rd r1 r2 k)) rs m (basics_to_code k) rs' m
  /\ Val.lessdef (Val.of_optbool (option_map negb (Val.cmpfs_bool cmp (rs r1) (rs r2)))) rs'#rd
  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.

Lemma swap_comparison_cmpf:
  forall v1 v2 cmp,
  Val.lessdef (Val.cmpf cmp v1 v2) (Val.cmpf (swap_comparison cmp) v2 v1).

Lemma transl_cond_float64_correct:
  forall cmp rd r1 r2 k rs m,
  exists rs',
     exec_straight ge (basics_to_code (transl_cond_float64 cmp rd r1 r2 k)) rs m (basics_to_code k) rs' m
  /\ Val.lessdef (Val.cmpf cmp rs#r1 rs#r2) rs'#rd
  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.

Lemma transl_cond_nofloat64_correct:
  forall cmp rd r1 r2 k rs m,
  exists rs',
     exec_straight ge (basics_to_code (transl_cond_notfloat64 cmp rd r1 r2 k)) rs m (basics_to_code k) rs' m
  /\ Val.lessdef (Val.of_optbool (option_map negb (Val.cmpf_bool cmp (rs r1) (rs r2)))) rs'#rd
  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.

Lemma transl_cond_op_correct:
  forall cond rd args k c rs m,
  transl_cond_op cond rd args k = OK c ->
  exists rs',
     exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m
  /\ Val.lessdef (Val.of_optbool (eval_condition cond (map rs (map preg_of args)) m)) rs'#rd
  /\ forall r, r <> PC -> r <> rd -> r <> RTMP -> rs'#r = rs#r.


Ltac SimplEval H :=
  match type of H with
  | Some _ = None _ => discriminate
  | Some _ = Some _ => inv H
  | ?a = Some ?b => let A := fresh in assert (A: Val.maketotal a = b) by (rewrite H; reflexivity)
end.

Ltac TranslOpSimpl :=
  econstructor; split;
  [ apply exec_straight_one; reflexivity
  | split; [ apply Val.lessdef_same; simpl; Simpl; fail | intros; simpl; Simpl; fail ] ].

Lemma int_eq_comm:
  forall (x y: int),
  (Int.eq x y) = (Int.eq y x).

Lemma int64_eq_comm:
  forall (x y: int64),
  (Int64.eq x y) = (Int64.eq y x).

Lemma select_same_lessdef:
  forall c v,
    Val.lessdef (Val.select c v v) v.

Lemma if_neg : forall X,
    forall a,
    forall b c : X,
    (if (negb a) then b else c) = (if a then c else b).

Lemma int_ltu_to_neq:
  forall x,
    Int.ltu Int.zero x = negb (Int.eq x Int.zero).

Lemma int64_ltu_to_neq:
  forall x,
    Int64.ltu Int64.zero x = negb (Int64.eq x Int64.zero).

Ltac splitall := repeat match goal with |- _ /\ _ => split end.

Lemma transl_op_correct:
  forall op args res k (rs: regset) m v c,
  transl_op op args res k = OK c ->
  eval_operation ge (rs#SP) op (map rs (map preg_of args)) m = Some v ->
  exists rs',
     exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m
  /\ Val.lessdef v rs'#(preg_of res)
  /\ forall r, data_preg r = true -> r <> preg_of res -> preg_notin r (destroyed_by_op op) -> rs' r = rs r.


Lemma indexed_memory_access_correct:
  forall mk_instr base ofs k rs m,
  exists base' ofs' rs' ptr',
     exec_straight_opt (indexed_memory_access mk_instr base ofs ::g k) rs m
                       (mk_instr base' ofs' ::g k) rs' m
  /\ eval_offset ofs' = OK ptr'
  /\ Val.offset_ptr rs'#base' ptr' = Val.offset_ptr rs#base ofs
  /\ forall r, r <> PC -> rs'#r = rs#r.


Lemma indexed_load_access_correct:
  forall trap chunk (mk_instr: ireg -> offset -> basic) rd m,
  (forall base ofs rs,
     exec_basic_instr ge (mk_instr base ofs) rs m = exec_load_offset trap chunk rs m rd base ofs) ->
  forall (base: ireg) ofs k (rs: regset) v,
  Mem.loadv chunk m (Val.offset_ptr rs#base ofs) = Some v ->
  exists rs',
     exec_straight ge (indexed_memory_access mk_instr base ofs ::g k) rs m k rs' m
  /\ rs'#rd = v
  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r.

Lemma indexed_store_access_correct:
  forall chunk (mk_instr: ireg -> offset -> basic) r1 m,
  (forall base ofs rs,
     exec_basic_instr ge (mk_instr base ofs) rs m = exec_store_offset chunk rs m r1 base ofs) ->
  forall (base: ireg) ofs k (rs: regset) m',
  Mem.storev chunk m (Val.offset_ptr rs#base ofs) (rs#r1) = Some m' ->
  exists rs',
     exec_straight ge (indexed_memory_access mk_instr base ofs ::g k) rs m k rs' m'
  /\ forall r, r <> PC -> rs'#r = rs#r.

Lemma loadind_correct:
  forall (base: ireg) ofs ty dst k c (rs: regset) m v,
  loadind base ofs ty dst k = OK c ->
  Mem.loadv (chunk_of_type ty) m (Val.offset_ptr rs#base ofs) = Some v ->
  exists rs',
     exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m
  /\ rs'#(preg_of dst) = v
  /\ forall r, r <> PC -> r <> preg_of dst -> rs'#r = rs#r.

Lemma storeind_correct:
  forall (base: ireg) ofs ty src k c (rs: regset) m m',
  storeind src base ofs ty k = OK c ->
  Mem.storev (chunk_of_type ty) m (Val.offset_ptr rs#base ofs) rs#(preg_of src) = Some m' ->
  exists rs',
     exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m'
  /\ forall r, r <> PC -> rs'#r = rs#r.

Ltac bsimpl := unfold exec_bblock; simpl.

Lemma Pget_correct:
  forall (dst: gpreg) (src: preg) k (rs: regset) m,
  src = RA ->
  exists rs',
     exec_straight ge (Pget dst src ::g k) rs m k rs' m
  /\ rs'#dst = rs#src
  /\ forall r, r <> PC -> r <> dst -> rs'#r = rs#r.

Lemma Pset_correct:
  forall (dst: preg) (src: gpreg) k (rs: regset) m,
  dst = RA ->
  exists rs',
     exec_straight ge (Pset dst src ::g k) rs m k rs' m
  /\ rs'#dst = rs#src
  /\ forall r, r <> PC -> r <> dst -> rs'#r = rs#r.

Lemma loadind_ptr_correct:
  forall (base: ireg) ofs (dst: ireg) k (rs: regset) m v,
  Mem.loadv Mptr m (Val.offset_ptr rs#base ofs) = Some v ->
  exists rs',
     exec_straight ge (loadind_ptr base ofs dst ::g k) rs m k rs' m
  /\ rs'#dst = v
  /\ forall r, r <> PC -> r <> dst -> rs'#r = rs#r.

Lemma storeind_ptr_correct:
  forall (base: ireg) ofs (src: ireg) k (rs: regset) m m',
  Mem.storev Mptr m (Val.offset_ptr rs#base ofs) rs#src = Some m' ->
  exists rs',
     exec_straight ge (storeind_ptr src base ofs ::g k) rs m k rs' m'
  /\ forall r, r <> PC -> rs'#r = rs#r.

Lemma transl_memory_access_correct:
  forall mk_instr addr args k c (rs: regset) m v,
  transl_memory_access mk_instr addr args k = OK c ->
  eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some v ->
  exists base ofs rs' ptr,
     exec_straight_opt (basics_to_code c) rs m (mk_instr base ofs ::g (basics_to_code k)) rs' m
  /\ eval_offset ofs = OK ptr
  /\ Val.offset_ptr rs'#base ptr = v
  /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r.

Lemma transl_memory_access2_correct:
  forall mk_instr addr args k c (rs: regset) m v,
  transl_memory_access2 mk_instr addr args k = OK c ->
  eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some v ->
  exists base ro mro mr1 rs',
     args = mr1 :: mro :: nil
  /\ ireg_of mro = OK ro
  /\ exec_straight_opt (basics_to_code c) rs m (mk_instr base ro ::g (basics_to_code k)) rs' m
  /\ Val.addl rs'#base rs'#ro = v
  /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r.

Lemma transl_memory_access2XS_correct:
  forall chunk mk_instr (scale : Z) args k c (rs: regset) m v,
  transl_memory_access2XS chunk mk_instr scale args k = OK c ->
  eval_addressing ge rs#SP (Aindexed2XS scale) (map rs (map preg_of args)) = Some v ->
  exists base ro mro mr1 rs',
     args = mr1 :: mro :: nil
  /\ ireg_of mro = OK ro
  /\ exec_straight_opt (basics_to_code c) rs m (mk_instr base ro ::g (basics_to_code k)) rs' m
  /\ Val.addl rs'#base (Val.shll rs'#ro (Vint (Int.repr scale))) = v
  /\ (forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r)
  /\ scale = (zscale_of_chunk chunk).

Lemma transl_load_access2_correct:
  forall trap chunk (mk_instr: ireg -> ireg -> basic) addr args k c rd (rs: regset) m v mro mr1 ro v',
  args = mr1 :: mro :: nil ->
  ireg_of mro = OK ro ->
  (forall base rs,
     exec_basic_instr ge (mk_instr base ro) rs m = exec_load_reg trap chunk rs m rd base ro) ->
  transl_memory_access2 mk_instr addr args k = OK c ->
  eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some v ->
  Mem.loadv chunk m v = Some v' ->
  exists rs',
     exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m
  /\ rs'#rd = v'
  /\ forall r, r <> PC -> r <> RTMP -> r <> rd -> rs'#r = rs#r.

Lemma transl_load_access2_correct_notrap2:
  forall chunk (mk_instr: ireg -> ireg -> basic) addr args k c rd (rs: regset) m v mro mr1 ro,
  args = mr1 :: mro :: nil ->
  ireg_of mro = OK ro ->
  (forall base rs,
     exec_basic_instr ge (mk_instr base ro) rs m = exec_load_reg NOTRAP chunk rs m rd base ro) ->
  transl_memory_access2 mk_instr addr args k = OK c ->
  eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some v ->
  Mem.loadv chunk m v = None ->
  exists rs',
     exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m
  /\ rs'#rd = Vundef
  /\ forall r, r <> PC -> r <> RTMP -> r <> rd -> rs'#r = rs#r.

Lemma transl_load_access2XS_correct:
  forall trap chunk (mk_instr: ireg -> ireg -> basic) (scale : Z) args k c rd (rs: regset) m v mro mr1 ro v',
  args = mr1 :: mro :: nil ->
  ireg_of mro = OK ro ->
  (forall base rs,
     exec_basic_instr ge (mk_instr base ro) rs m = exec_load_regxs trap chunk rs m rd base ro) ->
  transl_memory_access2XS chunk mk_instr scale args k = OK c ->
  eval_addressing ge rs#SP (Aindexed2XS scale) (map rs (map preg_of args)) = Some v ->
  Mem.loadv chunk m v = Some v' ->
  exists rs',
     exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m
  /\ rs'#rd = v'
  /\ forall r, r <> PC -> r <> RTMP -> r <> rd -> rs'#r = rs#r.

Lemma transl_load_access2XS_correct_notrap2:
  forall chunk (mk_instr: ireg -> ireg -> basic) (scale : Z) args k c rd (rs: regset) m v mro mr1 ro,
  args = mr1 :: mro :: nil ->
  ireg_of mro = OK ro ->
  (forall base rs,
     exec_basic_instr ge (mk_instr base ro) rs m = exec_load_regxs NOTRAP chunk rs m rd base ro) ->
  transl_memory_access2XS chunk mk_instr scale args k = OK c ->
  eval_addressing ge rs#SP (Aindexed2XS scale) (map rs (map preg_of args)) = Some v ->
  Mem.loadv chunk m v = None ->
  exists rs',
     exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m
  /\ rs'#rd = Vundef
  /\ forall r, r <> PC -> r <> RTMP -> r <> rd -> rs'#r = rs#r.

Lemma transl_load_access_correct:
  forall trap chunk (mk_instr: ireg -> offset -> basic) addr args k c rd (rs: regset) m v v',
  (forall base ofs rs,
     exec_basic_instr ge (mk_instr base ofs) rs m = exec_load_offset trap chunk rs m rd base ofs) ->
  transl_memory_access mk_instr addr args k = OK c ->
  eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some v ->
  Mem.loadv chunk m v = Some v' ->
  exists rs',
     exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m
  /\ rs'#rd = v'
  /\ forall r, r <> PC -> r <> RTMP -> r <> rd -> rs'#r = rs#r.

Lemma transl_load_access_correct_notrap2:
  forall chunk (mk_instr: ireg -> offset -> basic) addr args k c rd (rs: regset) m v,
  (forall base ofs rs,
     exec_basic_instr ge (mk_instr base ofs) rs m = exec_load_offset NOTRAP chunk rs m rd base ofs) ->
  transl_memory_access mk_instr addr args k = OK c ->
  eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some v ->
  Mem.loadv chunk m v = None ->
  exists rs',
     exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m
  /\ rs'#rd = Vundef
  /\ forall r, r <> PC -> r <> RTMP -> r <> rd -> rs'#r = rs#r.

Lemma transl_load_memory_access_ok:
  forall addr trap chunk args dst k c rs a v m,
  (match addr with Aindexed2XS _ | Aindexed2 => False | _ => True end) ->
  transl_load trap chunk addr args dst k = OK c ->
  eval_addressing ge (rs (IR SP)) addr (map rs (map preg_of args)) = Some a ->
  Mem.loadv chunk m a = Some v ->
  exists mk_instr rd,
     preg_of dst = IR rd
  /\ transl_memory_access mk_instr addr args k = OK c
  /\ forall base ofs rs,
        exec_basic_instr ge (mk_instr base ofs) rs m = exec_load_offset trap chunk rs m rd base ofs.

Lemma transl_load_memory_access_ok_notrap2:
  forall addr chunk args dst k c rs a m,
  (match addr with Aindexed2XS _ | Aindexed2 => False | _ => True end) ->
  transl_load NOTRAP chunk addr args dst k = OK c ->
  eval_addressing ge (rs (IR SP)) addr (map rs (map preg_of args)) = Some a ->
  Mem.loadv chunk m a = None ->
  exists mk_instr rd,
     preg_of dst = IR rd
  /\ transl_memory_access mk_instr addr args k = OK c
  /\ forall base ofs rs,
        exec_basic_instr ge (mk_instr base ofs) rs m = exec_load_offset NOTRAP chunk rs m rd base ofs.

Lemma transl_load_memory_access2_ok:
  forall trap chunk args dst k c rs a v m,
  transl_load trap chunk Aindexed2 args dst k = OK c ->
  eval_addressing ge (rs (IR SP)) Aindexed2 (map rs (map preg_of args)) = Some a ->
  Mem.loadv chunk m a = Some v ->
  exists mk_instr mr0 mro rd ro,
      args = mr0 :: mro :: nil
   /\ preg_of dst = IR rd
   /\ preg_of mro = IR ro
   /\ transl_memory_access2 mk_instr Aindexed2 args k = OK c
   /\ forall base rs,
      exec_basic_instr ge (mk_instr base ro) rs m = exec_load_reg trap chunk rs m rd base ro.


Lemma transl_load_memory_access2_ok_notrap2:
  forall chunk args dst k c rs a m,
  transl_load NOTRAP chunk Aindexed2 args dst k = OK c ->
  eval_addressing ge (rs (IR SP)) Aindexed2 (map rs (map preg_of args)) = Some a ->
  Mem.loadv chunk m a = None ->
  exists mk_instr mr0 mro rd ro,
      args = mr0 :: mro :: nil
   /\ preg_of dst = IR rd
   /\ preg_of mro = IR ro
   /\ transl_memory_access2 mk_instr Aindexed2 args k = OK c
   /\ forall base rs,
      exec_basic_instr ge (mk_instr base ro) rs m = exec_load_reg NOTRAP chunk rs m rd base ro.

Lemma transl_load_memory_access2XS_ok:
  forall scale trap chunk args dst k c rs a v m,
  transl_load trap chunk (Aindexed2XS scale) args dst k = OK c ->
  eval_addressing ge (rs (IR SP)) (Aindexed2XS scale) (map rs (map preg_of args)) = Some a ->
  Mem.loadv chunk m a = Some v ->
  exists mk_instr mr0 mro rd ro,
      args = mr0 :: mro :: nil
   /\ preg_of dst = IR rd
   /\ preg_of mro = IR ro
   /\ transl_memory_access2XS chunk mk_instr scale args k = OK c
   /\ forall base rs,
      exec_basic_instr ge (mk_instr base ro) rs m = exec_load_regxs trap chunk rs m rd base ro.


Lemma transl_load_memory_access2XS_ok_notrap2:
  forall scale chunk args dst k c rs a m,
  transl_load NOTRAP chunk (Aindexed2XS scale) args dst k = OK c ->
  eval_addressing ge (rs (IR SP)) (Aindexed2XS scale) (map rs (map preg_of args)) = Some a ->
  Mem.loadv chunk m a = None ->
  exists mk_instr mr0 mro rd ro,
      args = mr0 :: mro :: nil
   /\ preg_of dst = IR rd
   /\ preg_of mro = IR ro
   /\ transl_memory_access2XS chunk mk_instr scale args k = OK c
   /\ forall base rs,
      exec_basic_instr ge (mk_instr base ro) rs m = exec_load_regxs NOTRAP chunk rs m rd base ro.

Lemma transl_load_correct:
  forall trap chunk addr args dst k c (rs: regset) m a v,
  transl_load trap chunk addr args dst k = OK c ->
  eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some a ->
  Mem.loadv chunk m a = Some v ->
  exists rs',
     exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m
  /\ rs'#(preg_of dst) = v
  /\ forall r, r <> PC -> r <> RTMP -> r <> preg_of dst -> rs'#r = rs#r.

Lemma transl_load_correct_notrap2:
  forall chunk addr args dst k c (rs: regset) m a,
  transl_load NOTRAP chunk addr args dst k = OK c ->
  eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some a ->
  Mem.loadv chunk m a = None ->
  exists rs',
     exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m
  /\ rs'#(preg_of dst) = Vundef
  /\ forall r, r <> PC -> r <> RTMP -> r <> preg_of dst -> rs'#r = rs#r.

Lemma transl_store_access2_correct:
  forall chunk (mk_instr: ireg -> ireg -> basic) addr args k c r1 (rs: regset) m v mr1 mro ro m',
  args = mr1 :: mro :: nil ->
  ireg_of mro = OK ro ->
  (forall base rs,
     exec_basic_instr ge (mk_instr base ro) rs m = exec_store_reg chunk rs m r1 base ro) ->
  transl_memory_access2 mk_instr addr args k = OK c ->
  eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some v ->
  Mem.storev chunk m v rs#r1 = Some m' ->
  r1 <> RTMP ->
  exists rs',
     exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m'
  /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r.

Lemma transl_store_access2XS_correct:
  forall chunk (mk_instr: ireg -> ireg -> basic) scale args k c r1 (rs: regset) m v mr1 mro ro m',
  args = mr1 :: mro :: nil ->
  ireg_of mro = OK ro ->
  (forall base rs,
     exec_basic_instr ge (mk_instr base ro) rs m = exec_store_regxs chunk rs m r1 base ro) ->
  transl_memory_access2XS chunk mk_instr scale args k = OK c ->
  eval_addressing ge rs#SP (Aindexed2XS scale) (map rs (map preg_of args)) = Some v ->
  Mem.storev chunk m v rs#r1 = Some m' ->
  r1 <> RTMP ->
  exists rs',
     exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m'
  /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r.

Lemma transl_store_access_correct:
  forall chunk (mk_instr: ireg -> offset -> basic) addr args k c r1 (rs: regset) m v m',
  (forall base ofs rs,
     exec_basic_instr ge (mk_instr base ofs) rs m = exec_store_offset chunk rs m r1 base ofs) ->
  transl_memory_access mk_instr addr args k = OK c ->
  eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some v ->
  Mem.storev chunk m v rs#r1 = Some m' ->
  r1 <> RTMP ->
  exists rs',
     exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m'
  /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r.


Remark exec_store_offset_8_sign rs m x base ofs:
  exec_store_offset Mint8unsigned rs m x base ofs = exec_store_offset Mint8signed rs m x base ofs.

Remark exec_store_offset_16_sign rs m x base ofs:
  exec_store_offset Mint16unsigned rs m x base ofs = exec_store_offset Mint16signed rs m x base ofs.

Lemma transl_store_memory_access_ok:
  forall addr chunk args src k c rs a m m',
  (match addr with Aindexed2XS _ | Aindexed2 => False | _ => True end) ->
  transl_store chunk addr args src k = OK c ->
  eval_addressing ge (rs (IR SP)) addr (map rs (map preg_of args)) = Some a ->
  Mem.storev chunk m a (rs (preg_of src)) = Some m' ->
  exists mk_instr chunk' rr,
     preg_of src = IR rr
  /\ transl_memory_access mk_instr addr args k = OK c
  /\ (forall base ofs rs,
       exec_basic_instr ge (mk_instr base ofs) rs m = exec_store_offset chunk' rs m rr base ofs)
  /\ Mem.storev chunk m a rs#(preg_of src) = Mem.storev chunk' m a rs#(preg_of src).

Remark exec_store_reg_8_sign rs m x base ofs:
  exec_store_reg Mint8unsigned rs m x base ofs = exec_store_reg Mint8signed rs m x base ofs.

Remark exec_store_reg_16_sign rs m x base ofs:
  exec_store_reg Mint16unsigned rs m x base ofs = exec_store_reg Mint16signed rs m x base ofs.

Remark exec_store_regxs_8_sign rs m x base ofs:
  exec_store_regxs Mint8unsigned rs m x base ofs = exec_store_regxs Mint8signed rs m x base ofs.

Remark exec_store_regxs_16_sign rs m x base ofs:
  exec_store_regxs Mint16unsigned rs m x base ofs = exec_store_regxs Mint16signed rs m x base ofs.

Lemma transl_store_memory_access2_ok:
  forall addr chunk args src k c rs a m m',
  addr = Aindexed2 ->
  transl_store chunk addr args src k = OK c ->
  eval_addressing ge (rs (IR SP)) addr (map rs (map preg_of args)) = Some a ->
  Mem.storev chunk m a (rs (preg_of src)) = Some m' ->
  exists mk_instr chunk' rr mr0 mro ro,
     args = mr0 :: mro :: nil
  /\ preg_of mro = IR ro
  /\ preg_of src = IR rr
  /\ transl_memory_access2 mk_instr addr args k = OK c
  /\ (forall base rs,
       exec_basic_instr ge (mk_instr base ro) rs m = exec_store_reg chunk' rs m rr base ro)
  /\ Mem.storev chunk m a rs#(preg_of src) = Mem.storev chunk' m a rs#(preg_of src).

Lemma transl_store_memory_access2XS_ok:
  forall scale chunk args src k c rs a m m',
  transl_store chunk (Aindexed2XS scale) args src k = OK c ->
  eval_addressing ge (rs (IR SP)) (Aindexed2XS scale) (map rs (map preg_of args)) = Some a ->
  Mem.storev chunk m a (rs (preg_of src)) = Some m' ->
  exists mk_instr chunk' rr mr0 mro ro,
     args = mr0 :: mro :: nil
  /\ preg_of mro = IR ro
  /\ preg_of src = IR rr
  /\ transl_memory_access2XS chunk' mk_instr scale args k = OK c
  /\ (forall base rs,
       exec_basic_instr ge (mk_instr base ro) rs m = exec_store_regxs chunk' rs m rr base ro)
  /\ Mem.storev chunk m a rs#(preg_of src) = Mem.storev chunk' m a rs#(preg_of src).

Lemma transl_store_correct:
  forall chunk addr args src k c (rs: regset) m a m',
  transl_store chunk addr args src k = OK c ->
  eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some a ->
  Mem.storev chunk m a rs#(preg_of src) = Some m' ->
  exists rs',
     exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m'
  /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r.

Lemma make_epilogue_correct:
  forall ge0 f m stk soff cs m' ms rs k tm,
  Mach.load_stack m (Vptr stk soff) Tptr f.(fn_link_ofs) = Some (parent_sp cs) ->
  Mach.load_stack m (Vptr stk soff) Tptr f.(fn_retaddr_ofs) = Some (parent_ra cs) ->
  Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
  agree ms (Vptr stk soff) rs ->
  Mem.extends m tm ->
  match_stack ge0 cs ->
  exists rs', exists tm',
     exec_straight ge (make_epilogue f k) rs tm k rs' tm'
  /\ agree ms (parent_sp cs) rs'
  /\ Mem.extends m' tm'
  /\ rs'#RA = parent_ra cs
  /\ rs'#SP = parent_sp cs
  /\ (forall r, r <> PC -> r <> RA -> r <> SP -> r <> RTMP -> r <> GPRA -> rs'#r = rs#r).

End CONSTRUCTORS.