Proof of correctness for individual instructions

Require Import Coqlib Errors Maps Zbits.
Require Import AST Integers Floats Values Memory Globalenvs Linking Compopts Events.
Require Import Op Locations Machblock Conventions Lia.
Require Import Asmblock Asmblockgen Asmblockgenproof0 Asmblockprops.
Require Import OptionMonad.
Require Import MemcpyTypes.

Module MB := Machblock.
Module AB := Asmblock.

Local Open Scope option_monad_scope.
Local Opaque PregEq.eq.

Lemma int_sub_eq_zero:
  forall i j, Int.eq (Int.sub i j) Int.zero = Int.eq i j.

Lemma preg_of_not_R13:
  forall r, preg_of r <> IR13.

Lemma ireg_of_not_R13:
  forall m r, ireg_of m = OK r -> r <> IR13.

Lemma ireg_of_not_R13':
  forall m r, ireg_of m = OK r -> DR (IR r) <> IR13.
Global Hint Resolve preg_of_not_R13 ireg_of_not_R13 ireg_of_not_R13': asmgen.

Lemma preg_of_not_R14:
  forall r, preg_of r <> IR14.

Lemma ireg_of_not_R14:
  forall m r, ireg_of m = OK r -> IR r <> IR IR14.

Lemma ireg_of_not_R14':
  forall m r, ireg_of m = OK r -> DR (IR r) <> IR14.
Global Hint Resolve preg_of_not_R14 ireg_of_not_R14 ireg_of_not_R14': asmgen.

Definition if_preg (r: preg) : bool :=
  match r with
  | IR _ => true
  | FR _ => true
  | CR _ => false
  | PC => false
  end.

Lemma data_if_preg: forall r, data_preg r = true -> if_preg r = true.

Lemma data_preg_not_R14: forall r, data_preg r = true -> r <> IR14.

Lemma if_preg_not_PC: forall r, if_preg r = true -> r <> PC.
Global Hint Resolve data_if_preg if_preg_not_PC: asmgen.

Lemma undef_flags_rs_eq: forall rs r,
  if_preg r = true -> undef_flags rs r = rs r.

Lemma undef_flags_rs_eq': forall rs (r: ireg),
  undef_flags rs r = rs r.


Ltac Simplif :=
  ((rewrite undef_flags_rs_eq by eauto with asmgen)
  || (rewrite undef_flags_rs_eq' by eauto with asmgen)
  || (rewrite Pregmap.gss)
  || (rewrite Pregmap.gso by eauto with asmgen)); auto with asmgen.

Ltac Simpl := repeat Simplif.

Correctness of ARM constructor functions

Section CONSTRUCTORS.

Variable ge: genv.

Local Transparent Archi.ptr64.

Lemma iterate_op_correct:
  forall op1 op2 (f: val -> int -> val) (rs: regset) (r: ireg) m v0 is_addsub n k,
  (forall (rs:regset) n,
    exec_basic ge (op2 (SOimm n)) rs m =
    Next (undef_flags rs#r <- (f (rs#r) n)) m) ->
  (forall n,
    exec_basic ge (op1 (SOimm n)) rs m =
    Next (undef_flags rs#r <- (f v0 n)) m) ->
  exists rs',
     exec_straight ge (iterate_op op1 op2 (decompose_int is_addsub n) k) rs m k rs' m
  /\ rs'#r = List.fold_left f (decompose_int is_addsub n) v0
  /\ forall r': preg, r' <> r -> if_preg r' = true -> rs'#r' = rs#r'.


Lemma loadimm_correct:
  forall r n k rs m,
  exists rs',
     exec_straight ge (loadimm r n k) rs m k rs' m
  /\ rs'#r = Vint n
  /\ forall r': preg, r' <> r -> if_preg r' = true -> rs'#r' = rs#r'.


Lemma addimm_correct:
  forall r1 r2 n k rs m,
  exists rs',
     exec_straight ge (addimm r1 r2 n k) rs m k rs' m
  /\ rs'#r1 = Val.add rs#r2 (Vint n)
  /\ forall r': preg, r' <> r1 -> if_preg r' = true -> rs'#r' = rs#r'.


Lemma andimm_correct:
  forall r1 r2 n k rs m,
  exists rs',
     exec_straight ge (andimm r1 r2 n k) rs m k rs' m
  /\ rs'#r1 = Val.and rs#r2 (Vint n)
  /\ forall r': preg, r' <> r1 -> if_preg r' = true -> rs'#r' = rs#r'.


Lemma rsubimm_correct:
  forall r1 r2 n k rs m,
  exists rs',
     exec_straight ge (rsubimm r1 r2 n k) rs m k rs' m
  /\ rs'#r1 = Val.sub (Vint n) rs#r2
  /\ forall r': preg, r' <> r1 -> if_preg r' = true -> rs'#r' = rs#r'.


Lemma orimm_correct:
  forall r1 r2 n k rs m,
  exists rs',
     exec_straight ge (orimm r1 r2 n k) rs m k rs' m
  /\ rs'#r1 = Val.or rs#r2 (Vint n)
  /\ forall r': preg, r' <> r1 -> if_preg r' = true -> rs'#r' = rs#r'.


Lemma xorimm_correct:
  forall r1 r2 n k rs m,
  exists rs',
     exec_straight ge (xorimm r1 r2 n k) rs m k rs' m
  /\ rs'#r1 = Val.xor rs#r2 (Vint n)
  /\ forall r': preg, r' <> r1 -> if_preg r' = true -> rs'#r' = rs#r'.


Lemma indexed_memory_access_correct:
  forall (P: regset -> Prop) (mk_instr: ireg -> int -> basic)
         (mk_immed: int -> int) (base: ireg) n k (rs: regset) m m',
  (forall (r1: ireg) (rs1: regset) n1 k,
    Val.add rs1#r1 (Vint n1) = Val.add rs#base (Vint n) ->
    (forall (r: preg), if_preg r = true -> r <> IR14 -> rs1 r = rs r) ->
    exists rs',
    exec_straight ge (mk_instr r1 n1 :: k) rs1 m k rs' m' /\ P rs') ->
  exists rs',
     exec_straight ge
        (indexed_memory_access mk_instr mk_immed base n k) rs m
        k rs' m'
  /\ P rs'.

Lemma loadind_int_correct:
  forall (base: ireg) ofs dst (rs: regset) m v k,
  Mem.loadv Mint32 m (Val.offset_ptr rs#base ofs) = Some v ->
  exists rs',
     exec_straight ge (loadind_int base ofs dst k) rs m k rs' m
  /\ rs'#dst = v
  /\ forall r, if_preg r = true -> r <> IR14 -> r <> dst -> 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 c rs m k rs' m
  /\ rs'#(preg_of dst) = v
  /\ forall r, if_preg r = true -> r <> IR14 -> 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 c rs m k rs' m'
  /\ forall r, if_preg r = true -> r <> IR14 -> rs'#r = rs#r.


Lemma save_lr_correct:
  forall ofs k (rs: regset) m m',
  Mem.storev Mint32 m (Val.offset_ptr rs#IR13 ofs) (rs#IR14) = Some m' ->
  exists rs',
     exec_straight ge (save_lr ofs k) rs m k rs' m'
  /\ (forall r, if_preg r = true -> r <> IR12 -> rs'#r = rs#r)
  /\ (save_lr_preserves_R12 ofs = true -> rs'#IR12 = rs#IR12).


Lemma transl_shift_correct:
  forall s (r: ireg) (rs: regset),
  eval_shift_op (transl_shift s r) rs = eval_shift s (rs#r).


Lemma compare_int_spec:
  forall rs v1 v2 m,
  let rs1 := compare_int rs v1 v2 m in
     rs1#CN = Val.negative (Val.sub v1 v2)
  /\ rs1#CZ = Val.cmpu (Mem.valid_pointer m) Ceq v1 v2
  /\ rs1#CC = Val.cmpu (Mem.valid_pointer m) Cge v1 v2
  /\ rs1#CV = Val.sub_overflow v1 v2.

Lemma compare_int_inv:
  forall rs v1 v2 m,
  let rs1 := compare_int rs v1 v2 m in
  forall r', data_preg r' = true -> rs1#r' = rs#r'.

Lemma compare_int_test_spec:
  forall rs v1 v2,
  let rs1 := compare_int_test rs v1 v2 in
     rs1#CN = Val.negative (Val.and v1 v2)
  /\ rs1#CZ = Val.cmp Ceq (Val.and v1 v2) (Vint Int.zero)
  /\ rs1#CC = Vundef
  /\ rs1#CV = Vundef.

Lemma compare_int_test_inv:
  forall rs v1 v2,
  let rs1 := compare_int_test rs v1 v2 in
  forall r', data_preg r' = true -> rs1#r' = rs#r'.

Lemma cond_for_maskzero_correct:
  forall n v rs b,
  Val.cmp_bool Ceq (Val.and v (Vint n)) (Vint Int.zero) = Some b ->
  eval_testcond TCeq (compare_int_test rs v (Vint n)) = Some b.

Lemma cond_for_masknotzero_correct:
  forall n v rs b,
  Val.cmp_bool Cne (Val.and v (Vint n)) (Vint Int.zero) = Some b ->
  eval_testcond TCne (compare_int_test rs v (Vint n)) = Some b.

Lemma int_signed_eq:
  forall x y, Int.eq x y = zeq (Int.signed x) (Int.signed y).

Lemma int_not_lt:
  forall x y, negb (Int.lt y x) = (Int.lt x y || Int.eq x y).

Lemma int_lt_not:
  forall x y, Int.lt y x = negb (Int.lt x y) && negb (Int.eq x y).

Lemma int_not_ltu:
  forall x y, negb (Int.ltu y x) = (Int.ltu x y || Int.eq x y).

Lemma int_ltu_not:
  forall x y, Int.ltu y x = negb (Int.ltu x y) && negb (Int.eq x y).

Lemma cond_for_signed_cmp_correct:
  forall c v1 v2 rs m b,
  Val.cmp_bool c v1 v2 = Some b ->
  eval_testcond (cond_for_signed_cmp c)
                (compare_int rs v1 v2 m) = Some b.

Lemma cond_for_unsigned_cmp_correct:
  forall c v1 v2 rs m b,
  Val.cmpu_bool (Mem.valid_pointer m) c v1 v2 = Some b ->
  eval_testcond (cond_for_unsigned_cmp c)
                (compare_int rs v1 v2 m) = Some b.

Lemma compare_float_spec:
  forall rs f1 f2,
  let rs1 := compare_float rs (Vfloat f1) (Vfloat f2) in
     rs1#CN = Val.of_bool (Float.cmp Clt f1 f2)
  /\ rs1#CZ = Val.of_bool (Float.cmp Ceq f1 f2)
  /\ rs1#CC = Val.of_bool (negb (Float.cmp Clt f1 f2))
  /\ rs1#CV = Val.of_bool (negb (Float.cmp Ceq f1 f2 || Float.cmp Clt f1 f2 || Float.cmp Cgt f1 f2)).

Lemma compare_float_inv:
  forall rs v1 v2,
  let rs1 := compare_float rs v1 v2 in
  forall r', data_preg r' = true -> rs1#r' = rs#r'.

Lemma cond_for_float_cmp_correct: forall c v1 v2 b rs,
  Val.cmpf_bool c v1 v2 = Some b ->
  eval_testcond (cond_for_float_cmp c) (compare_float rs v1 v2) = Some b.

Lemma cond_for_float_not_cmp_correct: forall c v1 v2 b rs,
  option_map negb (Val.cmpf_bool c v1 v2) = Some b ->
  eval_testcond (cond_for_float_not_cmp c) (compare_float rs v1 v2) = Some b.

Lemma compare_float32_spec:
  forall rs f1 f2,
  let rs1 := compare_float32 rs (Vsingle f1) (Vsingle f2) in
     rs1#CN = Val.of_bool (Float32.cmp Clt f1 f2)
  /\ rs1#CZ = Val.of_bool (Float32.cmp Ceq f1 f2)
  /\ rs1#CC = Val.of_bool (negb (Float32.cmp Clt f1 f2))
  /\ rs1#CV = Val.of_bool (negb (Float32.cmp Ceq f1 f2 || Float32.cmp Clt f1 f2 || Float32.cmp Cgt f1 f2)).

Lemma compare_float32_inv:
  forall rs v1 v2,
  let rs1 := compare_float32 rs v1 v2 in
  forall r', data_preg r' = true -> rs1#r' = rs#r'.

Lemma cond_for_float32_cmp_correct: forall c v1 v2 b rs,
  Val.cmpfs_bool c v1 v2 = Some b ->
  eval_testcond (cond_for_float_cmp c) (compare_float32 rs v1 v2) = Some b.

Lemma cond_for_float32_not_cmp_correct: forall c v1 v2 b rs,
  option_map negb (Val.cmpfs_bool c v1 v2) = Some b ->
  eval_testcond (cond_for_float_not_cmp c) (compare_float32 rs v1 v2) = Some b.

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
  | [ H: match _ with true => _ | false => assertion_failed end = OK _ |- _ ] => monadInv H
  end);
  subst;
  repeat (match goal with
  | [ H: ireg_of ?x = OK ?y |- _ ] => simpl in *; rewrite (ireg_of_eq _ _ H) in *
  | [ H: freg_of ?x = OK ?y |- _ ] => simpl in *; rewrite (freg_of_eq _ _ H) in *
  end).



Lemma cmp_sbcs_signed_correct:
  forall hi1 lo1 hi2 lo2,
  let c1 := if Int.ltu lo1 lo2 then Int.zero else Int.one in
  let bin := Int.sub Int.one c1 in
  Int.xor (Int.sub_overflow hi1 hi2 bin)
          (Int.negative (Int.sub (Int.sub hi1 hi2) bin)) =
    (if Int64.lt (Int64.ofwords hi1 lo1) (Int64.ofwords hi2 lo2)
     then Int.one else Int.zero).

Lemma cmp_sbcs_carry_correct:
  forall hi1 lo1 hi2 lo2,
  let c1 := if Int.ltu lo1 lo2 then Int.zero else Int.one in
  Int.add_carry hi1 (Int.not hi2) c1 =
    (if Int64.ltu (Int64.ofwords hi1 lo1) (Int64.ofwords hi2 lo2)
     then Int.zero else Int.one).

Lemma transl_cond_correct:
  forall cond args k c rs m,
  transl_cond cond args k = OK c ->
  exists rs',
     exec_straight ge c rs m k rs' m
  /\ (forall b,
      eval_condition cond (map rs (map preg_of args)) m = Some b ->
      eval_testcond (cond_for_cond cond) rs' = Some b)
  /\ forall r, data_preg r = true -> rs'#r = rs#r.

Lemma transl_cond_correct':
  forall cond args k c tbb rs m,
  transl_cond cond args k = OK c ->
  exists rs',
     exec_straight ge c rs m k rs' m
  /\ (forall b,
      eval_condition cond (map rs (map preg_of args)) m = Some b ->
      eval_testcond (cond_for_cond cond) (incrPC (Ptrofs.repr (size tbb)) rs') = Some b)
  /\ forall r, data_preg r = true -> rs'#r = rs#r.

Lemma transl_cbranch_pbc:
  forall cond args lbl near_labels bdy,
  transl_cbranch cond args lbl near_labels = OK (bdy, PCtlFlow (Pbc (cond_for_cond cond) lbl)) ->
  transl_cond cond args nil = OK bdy.

Definition outcome_undef_flags (o: outcome) : outcome :=
  match o with Next rs m => Next (undef_flags rs) m | Stuck => Stuck end.

Lemma transl_cbranch_correct_gen:
  forall f cond args lbl near_labels b m rs tbb bdy ctl,
  transl_cbranch cond args lbl near_labels = OK (bdy, ctl) ->
  eval_condition cond (map rs (map preg_of args)) m = Some b ->
  exists rs' cfi (wrap: outcome -> outcome),
     ctl = PCtlFlow cfi
  /\ exec_straight_opt ge bdy rs m nil rs' m
  /\ exec_cfi ge f cfi (incrPC (Ptrofs.repr (size tbb)) rs') m =
        wrap (if b then goto_label f lbl (incrPC (Ptrofs.repr (size tbb)) rs') m else
        Next (incrPC (Ptrofs.repr (size tbb)) rs') m)
  /\ (wrap Stuck = Stuck)
  /\ (forall rs0 m0, exists rs1, wrap (Next rs0 m0) = Next rs1 m0
        /\ (forall r, data_preg r = true -> rs1 r = rs0 r)
        /\ rs1 PC = rs0 PC
        /\ rs1 IR14 = rs0 IR14)
  /\ forall r, data_preg r = true -> rs'#r = rs#r.

Lemma transl_cbranch_correct:
  forall fm f cond args lbl near_labels b m rs tbb bdy,
  transl_control fm (MBcond cond args lbl) near_labels = OK (bdy, PCtlFlow (Pbc (cond_for_cond cond) lbl)) ->
  eval_condition cond (map rs (map preg_of args)) m = Some b ->
  exists rs',
     exec_straight_opt ge bdy rs m nil rs' m
  /\ exec_cfi ge f (Pbc (cond_for_cond cond) lbl) (incrPC (Ptrofs.repr (size tbb)) rs') m =
        (if b then goto_label f lbl (incrPC (Ptrofs.repr (size tbb)) rs') m else
        Next (incrPC (Ptrofs.repr (size tbb)) rs') m)
  /\ forall r, data_preg r = true -> rs'#r = rs#r.


Ltac TranslOpSimpl :=
  econstructor; split;
  [ apply exec_straight_one; simpl; unfold arith_uf_fn; simpl; eauto
  | split; [try rewrite transl_shift_correct; repeat Simpl | intros; repeat Simpl] ].

Lemma transl_op_cmp_default_correct:
  forall cmp args r k bc (rs: regset) m,
  transl_op_cmp_default cmp args r k = OK bc ->
  exists rs',
    exec_straight ge bc rs m k rs' m
    /\ Val.lessdef
        (Val.of_optbool (eval_condition cmp (map rs (map preg_of args)) m))
        (rs' r)
    /\ forall r0, data_preg r0 = true -> r0 <> r -> rs' r0 = rs r0.

Lemma transl_op_cmp_cne_correct:
  forall cmp args r k bc (rs: regset) m,
  transl_op_cmp_cne cmp args r k = Some (OK bc) ->
  exists rs',
    exec_straight ge bc rs m k rs' m
    /\ Val.lessdef
        (Val.of_optbool (eval_condition cmp (map rs (map preg_of args)) m))
        (rs' r)
    /\ forall r0, data_preg r0 = true -> r0 <> r -> rs' r0 = rs r0.

Lemma transl_op_cmp_ceq_clz_correct:
  forall cmp args r k bc (rs: regset) m,
  transl_op_cmp_ceq_clz cmp args r k = Some (OK bc) ->
  exists rs',
    exec_straight ge bc rs m k rs' m
    /\ Val.lessdef
        (Val.of_optbool (eval_condition cmp (map rs (map preg_of args)) m))
        (rs' r)
    /\ forall r0, data_preg r0 = true -> r0 <> r -> rs' r0 = rs r0.

Lemma transl_op_cmp_correct:
  forall cmp args r k bc (rs: regset) m,
  transl_op_cmp cmp args r k = OK bc ->
  exists rs',
    exec_straight ge bc rs m k rs' m
    /\ Val.lessdef
        (Val.of_optbool (eval_condition cmp (map rs (map preg_of args)) m))
        (rs' r)
    /\ forall r0, data_preg r0 = true -> r0 <> r -> rs' r0 = rs r0.


Lemma transl_op_correct_same:
  forall op args res k c (rs: regset) m v,
  transl_op op args res k = OK c ->
  eval_operation ge rs#IR13 op (map rs (map preg_of args)) m = Some v ->
  match op with
  | Ocopy | Ocopyimm _ | Ocmp _ | Osel _ | Oselimm _ _ | Oselimm2 _ _ _
  | Ocmpcarryu _ | Ocmpcarry _ | Oaddrstack _ => False
  | _ => True end ->
  exists rs',
     exec_straight ge c rs m k rs' m
  /\ rs'#(preg_of res) = v
  /\ forall r, data_preg r = true -> r <> preg_of res -> preg_notin r (destroyed_by_op op) -> rs'#r = rs#r.

Lemma transl_op_correct:
  forall op args res k c (rs: regset) m v,
  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 c rs m 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 transl_memory_access_correct:
  forall (P: regset -> Prop) (mk_instr_imm: ireg -> int -> basic)
         (mk_instr_gen: option (ireg -> shift_op -> basic))
         (mk_immed: int -> int)
         addr args k c (rs: regset) a m m',
  transl_memory_access mk_instr_imm mk_instr_gen mk_immed addr args k = OK c ->
  eval_addressing ge (rs#SP) addr (map rs (map preg_of args)) = Some a ->
  match a with Vptr _ _ => True | _ => False end ->
  (forall (r1: ireg) (rs1: regset) n k,
    Val.add rs1#r1 (Vint n) = a ->
    (forall (r: preg), if_preg r = true -> r <> IR14 -> rs1 r = rs r) ->
    exists rs',
    exec_straight ge (mk_instr_imm r1 n :: k) rs1 m k rs' m' /\ P rs') ->
  match mk_instr_gen with
  | None => True
  | Some mk =>
      (forall (r1: ireg) (sa: shift_op) k,
      Val.add rs#r1 (eval_shift_op sa rs) = a ->
       exists rs',
      exec_straight ge (mk r1 sa :: k) rs m k rs' m' /\ P rs')
  end ->
  exists rs',
    exec_straight ge c rs m k rs' m' /\ P rs'.

Lemma transl_load_int_correct:
  forall mk_instr is_immed dst addr args k c (rs: regset) a chunk m v,
  transl_memory_access_int mk_instr is_immed dst addr args k = OK c ->
  eval_addressing ge (rs#SP) addr (map rs (map preg_of args)) = Some a ->
  Mem.loadv chunk m a = Some v ->
  (forall (r1 r2: ireg) (sa: shift_op) (rs1: regset),
    exec_basic ge (mk_instr r1 r2 sa) rs1 m =
    exec_load_aux chunk (Val.add rs1#r2 (eval_shift_op sa rs1)) r1 rs1 m) ->
  exists rs',
      exec_straight ge c rs m k rs' m
   /\ rs'#(preg_of dst) = v
   /\ forall r, data_preg r = true -> r <> preg_of dst -> rs'#r = rs#r.

Lemma transl_load_float_correct:
  forall mk_instr is_immed dst addr args k c (rs: regset) a chunk m v,
  transl_memory_access_float mk_instr is_immed dst addr args k = OK c ->
  eval_addressing ge (rs#SP) addr (map rs (map preg_of args)) = Some a ->
  Mem.loadv chunk m a = Some v ->
  (forall (r1: freg) (r2: ireg) (n: int) (rs1: regset),
    exec_basic ge (mk_instr r1 r2 n) rs1 m =
    exec_load_aux chunk (Val.add rs1#r2 (Vint n)) r1 rs1 m) ->
  exists rs',
      exec_straight ge c rs m k rs' m
   /\ rs'#(preg_of dst) = v
   /\ forall r, data_preg r = true -> r <> preg_of dst -> rs'#r = rs#r.

Lemma transl_store_int_correct:
  forall mr mk_instr is_immed src addr args k c (rs: regset) a chunk m m',
  transl_memory_access_int mk_instr is_immed src addr args 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' ->
  (forall (r1 r2: ireg) (sa: shift_op) (rs1: regset),
    exec_basic ge (mk_instr r1 r2 sa) rs1 m =
    exec_store_aux chunk (Val.add rs1#r2 (eval_shift_op sa rs1)) r1 rs1 m) ->
  exists rs',
      exec_straight ge c rs m k rs' m'
   /\ forall r, data_preg r = true -> preg_notin r mr -> rs'#r = rs#r.

Lemma transl_store_float_correct:
  forall mr mk_instr is_immed src addr args k c (rs: regset) a chunk m m',
  transl_memory_access_float mk_instr is_immed src addr args 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' ->
  (forall (r1: freg) (r2: ireg) (n: int) (rs1: regset),
    exec_basic ge (mk_instr r1 r2 n) rs1 m =
    exec_store_aux chunk (Val.add rs1#r2 (Vint n)) r1 rs1 m) ->
  exists rs',
      exec_straight ge c rs m k rs' m'
   /\ forall r, data_preg r = true -> preg_notin r mr -> rs'#r = rs#r.

Lemma transl_load_correct:
  forall trap chunk addr args dst k c (rs: regset) a m 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 c rs m k rs' m
   /\ rs'#(preg_of dst) = v
   /\ forall r, data_preg r = true -> r <> preg_of dst -> rs'#r = rs#r.

Lemma transl_store_correct:
  forall chunk addr args src k c (rs: regset) a m 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 c rs m k rs' m'
   /\ forall r, data_preg r = true -> preg_notin r (destroyed_by_store chunk addr) -> rs'#r = rs#r.

Lemma extract_memcpy_builtin_arg_correct:
  forall ba r i rs m b ofs,
  evalopt_builtin_arg ge (fun r: dreg => rs r) (rs#SP) m (map_builtin_arg dreg_of ba) = Some (Vptr b i) ->
  extract_memcpy_builtin_arg ba = OK (r, ofs) ->
  Val.add (rs#r) (Vint ofs) = Vptr b i.

Lemma extract_memcpy_builtin_arg_data:
  forall ba x ofs,
  extract_memcpy_builtin_arg ba = OK (x, ofs) ->
  data_preg x = true.

Lemma indexed_memcpy_access_correct:
  forall (mk_instr: ireg -> ireg -> int -> int -> basic)
         (mk_immed: int -> int) (ras rad: ireg) ofss ofsd k (rs: regset) m m' l,
  data_preg ras = true -> data_preg rad = true ->
  (forall (r1 r2: ireg) (rs1: regset) n1 n2 k,
    data_preg r1 = true -> data_preg r2 = true ->
    r1 = ras \/ r1 = IR2 \/ r1 = IR3 -> r2 = rad \/ r2 = IR2 \/ r2 = IR3 ->
    Val.add rs1#r1 (Vint n1) = Val.add rs#ras (Vint ofss) ->
    Val.add rs1#r2 (Vint n2) = Val.add rs#rad (Vint ofsd) ->
    (forall r: preg,
      data_preg r = true -> preg_notin r (R2 :: R3 :: l) -> rs1 r = rs r) ->
    exists rs',
      exec_straight ge (mk_instr r1 r2 n1 n2 :: k) rs1 m k rs' m'
    /\
      (forall r: preg,
        data_preg r = true -> preg_notin r (R2 :: R3 :: l) -> rs r = rs' r)) ->
  exists rs',
    exec_straight ge
      (indexed_memcpy_access mk_instr mk_immed ras rad ofss ofsd k)
      rs m k rs' m'
  /\
    (forall r: preg,
      data_preg r = true -> preg_notin r (R2 :: R3 :: l) -> rs r = rs' r).

Lemma exec_memcpy_aux_general:
  forall (rs rs1: regset) (r1 r2 r1' r2': ireg) i1 i2 i1' i2' sz m m' va1 va2 vargs b1 b2 l
  (HVARGS: va2 :: va1 :: nil = vargs)
  (VA1: evalopt_builtin_arg ge (fun r : dreg => rs r) (rs IR13) m (map_builtin_arg dreg_of b1) = Some va1)
  (VA2: evalopt_builtin_arg ge (fun r : dreg => rs r) (rs IR13) m (map_builtin_arg dreg_of b2) = Some va2)
  (HRS: extract_memcpy_builtin_arg b1 = OK (r1, i1))
  (HRD: extract_memcpy_builtin_arg b2 = OK (r2, i2))
  (VD1: Val.add (rs1 r1') (Vint i1') = Val.add (rs r1) (Vint i1))
  (VD2: Val.add (rs1 r2') (Vint i2') = Val.add (rs r2) (Vint i2))
  (HMEM: memcpy_run (atomic sz) vargs m = Some m')
  (HL: forall r: preg, In r (map DR l) -> (DR r2) <> r),
  exec_memcpy_aux l r1' r2' (Ofs i1') (Ofs i2') (Zpos sz) rs1 m =
  Next (undef_regs (map DR l) rs1) m'.

Lemma transl_memcpy_correct:
  forall sz sz' args vargs vargs' m k c (rs: regset) m',
  Val.lessdef_list vargs vargs' ->
  Z_to_memcpy_typ (Zpos sz) = Some sz' ->
  transl_memcpy sz' args k = OK c ->
  evalopt_builtin_args ge (fun r: dreg => rs r) (rs SP) m (map (map_builtin_arg dreg_of) args) = Some vargs' ->
  memcpy_run (atomic sz) vargs' m = Some m' ->
  exists rs',
    exec_straight ge c rs m k rs' m'
    /\ forall r, data_preg r = true -> preg_notin r (destroyed_by_memcpy sz') -> rs#r = rs'#r.

Lemma make_epilogue_correct:
  forall tge f m stk soff cs m' ms rs tm,
  Mach.load_stack m (Vptr stk soff) Tptr (fn_link_ofs f) = Some (parent_sp cs) ->
  Mach.load_stack m (Vptr stk soff) Tptr (fn_retaddr_ofs f) =
    Some (PAC.pointer_auth_encode (fn_retaddr_pac f) (parent_ra cs) (parent_sp cs)) ->
  Mem.free m stk 0 (fn_stacksize f) = Some m' ->
  agree ms (Vptr stk soff) rs ->
  Mem.extends m tm ->
  match_stack tge cs ->
  (function_preserves_IR14 f = true -> rs#RA = parent_ra cs) ->
  exists rs' tm',
       exec_straight ge (make_epilogue f) rs tm nil rs' tm'
    /\ agree ms (parent_sp cs) rs'
    /\ Mem.extends m' tm'
    /\ rs'#SP = parent_sp cs
    /\ rs'#RA = parent_ra cs
    /\ (forall r, if_preg r = true -> r <> SP -> r <> RA -> rs'#r = rs#r).

Correctness of preserves_IR14

Lemma undef_flags_IR14:
  forall rs, undef_flags rs IR14 = rs IR14.

Lemma compare_int_IR14:
  forall rs v1 v2 m,
  compare_int rs v1 v2 m IR14 = rs IR14.

Lemma compare_int_add_IR14:
  forall rs v1 v2 m,
  compare_int_add rs v1 v2 m IR14 = rs IR14.

Lemma compare_int_test_IR14:
  forall rs v1 v2,
  compare_int_test rs v1 v2 IR14 = rs IR14.

Lemma compare_float_IR14:
  forall rs v1 v2,
  compare_float rs v1 v2 IR14 = rs IR14.

Lemma compare_float32_IR14:
  forall rs v1 v2,
  compare_float32 rs v1 v2 IR14 = rs IR14.

Remark indexed_memory_access_eq:
  forall mk_instr mk_immed base n k,
  Int.eq n (mk_immed n) = true ->
  indexed_memory_access mk_instr mk_immed base n k = mk_instr base n :: k.

Lemma exec_load_aux_IR14:
  forall chunk addr (rd: ireg) rs m rs' m',
  exec_load_aux chunk addr rd rs m = Next rs' m' ->
  IR rd <> IR IR14 ->
  rs' IR14 = rs IR14.

Lemma exec_store_aux_IR14:
  forall chunk addr (rf: preg) rs m rs' m',
  exec_store_aux chunk addr rf rs m = Next rs' m' ->
  rs' IR14 = rs IR14.

Lemma exec_straight_length:
  forall c rs m c' rs' m',
  exec_straight ge c rs m c' rs' m' ->
  (length c > length c')%nat.

Lemma exec_straight_singleton:
  forall i k rs m rs' m',
  exec_straight ge (i :: k) rs m k rs' m' ->
  exec_basic ge i rs m = Next rs' m'.

Lemma exec_straight_singleton_bi:
  forall (i: basic) k rs m rs' m',
  exec_straight ge (i ::bi k) rs m k rs' m' ->
  exec_basic ge i rs m = Next rs' m'.

Lemma exec_straight_IR14:
  forall c rs m k rs' m',
  exec_straight ge c rs m k rs' m' ->
  (forall i rs1 m1 rs2 m2,
     In i c -> exec_basic ge i rs1 m1 = Next rs2 m2 -> rs2 IR14 = rs1 IR14) ->
  rs' IR14 = rs IR14.

Lemma exec_straight_determ:
  forall c rs m c' rs1 m1 rs2 m2,
  exec_straight ge c rs m c' rs1 m1 ->
  exec_straight ge c rs m c' rs2 m2 ->
  rs1 = rs2 /\ m1 = m2.

Remark compare_int_IR14':
  forall rs v1 v2 m r,
  arith_comparison_ro_compare r rs v1 v2 m IR14 = rs IR14.

Remark compare_float_IR14':
  forall rs v1 v2 r,
  arith_comparison_ff_compare r rs v1 v2 IR14 = rs IR14.

Remark compare_float_zero_IR14:
  forall r rs v1 v2,
  arith_comparison_f_compare r rs v1 v2 IR14 = rs IR14.

Lemma compare_int_if_preg:
  forall rs v1 v2 m r, if_preg r = true -> compare_int rs v1 v2 m r = rs r.

Lemma compare_int_test_if_preg:
  forall rs v1 v2 r, if_preg r = true -> compare_int_test rs v1 v2 r = rs r.

Lemma compare_float_if_preg:
  forall rs v1 v2 r, if_preg r = true -> compare_float rs v1 v2 r = rs r.

Lemma compare_float32_if_preg:
  forall rs v1 v2 r, if_preg r = true -> compare_float32 rs v1 v2 r = rs r.

Lemma transl_cond_correct_strong:
  forall cond args k c rs m,
  transl_cond cond args k = OK c ->
  cond_preserves_IR14 cond = true ->
  exists rs',
     exec_straight ge c rs m k rs' m
  /\ forall r, if_preg r = true -> rs'#r = rs#r.

Lemma transl_cond_preserves_IR14:
  forall cond args k c rs m,
  transl_cond cond args k = OK c ->
  cond_preserves_IR14 cond = true ->
  forall rs' m',
  exec_straight ge c rs m k rs' m' ->
  rs' IR14 = rs IR14.

Lemma exec_straight_pnop_IR14:
  forall rs m rs' m',
  exec_straight ge (Pnop false :: nil) rs m nil rs' m' ->
  rs' IR14 = rs IR14.

Lemma transl_cbranch_preserves_IR14:
  forall cond args lbl near_labels bdy ctl rs m,
  transl_cbranch cond args lbl near_labels = OK (bdy, ctl) ->
  cond_preserves_IR14 cond = true ->
  forall rs' m',
  exec_straight_opt ge bdy rs m nil rs' m' ->
  rs' IR14 = rs IR14.

IR14 preservation for transl_op

Local Hint Extern 1 (FR _ <> IR _) => discriminate : asmgen.
Local Hint Extern 1 (IR _ <> FR _) => discriminate : asmgen.
Local Hint Extern 1 (_ <> _) => apply not_eq_sym : asmgen.

Lemma exec_straight_two_IR14:
  forall i1 i2 k0 rs0 m0 rs0' m0',
  exec_straight ge (i1 :: i2 :: k0) rs0 m0 k0 rs0' m0' ->
  (forall rs1 m1 rs2 m2, exec_basic ge i1 rs1 m1 = Next rs2 m2 -> rs2 IR14 = rs1 IR14) ->
  (forall rs1 m1 rs2 m2, exec_basic ge i2 rs1 m1 = Next rs2 m2 -> rs2 IR14 = rs1 IR14) ->
  rs0' IR14 = rs0 IR14.

Lemma exec_straight_three_IR14:
  forall i1 i2 i3 k0 rs0 m0 rs0' m0',
  exec_straight ge (i1 :: i2 :: i3 :: k0) rs0 m0 k0 rs0' m0' ->
  (forall rs1 m1 rs2 m2, exec_basic ge i1 rs1 m1 = Next rs2 m2 -> rs2 IR14 = rs1 IR14) ->
  (forall rs1 m1 rs2 m2, exec_basic ge i2 rs1 m1 = Next rs2 m2 -> rs2 IR14 = rs1 IR14) ->
  (forall rs1 m1 rs2 m2, exec_basic ge i3 rs1 m1 = Next rs2 m2 -> rs2 IR14 = rs1 IR14) ->
  rs0' IR14 = rs0 IR14.

Lemma transl_op_cmp_default_preserves_IR14:
  forall cmp args res r k bc (rs: regset) m,
  ireg_of res = OK r ->
  transl_op_cmp_default cmp args r k = OK bc ->
  cond_preserves_IR14 cmp = true ->
  forall rs' m',
  exec_straight ge bc rs m k rs' m' ->
  rs' IR14 = rs IR14.

Lemma transl_op_cmp_cne_preserves_IR14:
  forall cmp args res r k bc (rs: regset) m,
  ireg_of res = OK r ->
  transl_op_cmp_cne cmp args r k = Some (OK bc) ->
  forall rs' m',
  exec_straight ge bc rs m k rs' m' ->
  rs' IR14 = rs IR14.

Lemma transl_op_cmp_ceq_clz_preserves_IR14:
  forall cmp args res r k bc (rs: regset) m,
  ireg_of res = OK r ->
  transl_op_cmp_ceq_clz cmp args r k = Some (OK bc) ->
  forall rs' m',
  exec_straight ge bc rs m k rs' m' ->
  rs' IR14 = rs IR14.

Lemma transl_op_cmp_preserves_IR14:
  forall cmp args res r k bc (rs: regset) m,
  ireg_of res = OK r ->
  transl_op_cmp cmp args r k = OK bc ->
  cond_preserves_IR14 cmp = true ->
  forall rs' m',
  exec_straight ge bc rs m k rs' m' ->
  rs' IR14 = rs IR14.

Lemma transl_op_preserves_IR14:
  forall op args res k c (rs: regset) m,
  transl_op op args res k = OK c ->
  preserves_IR14 (MBop op args res) = true ->
  forall rs' m',
  exec_straight ge c rs m k rs' m' ->
  rs' IR14 = rs IR14.

Lemma undef_regs_pres:
  forall rl (rs: regset) r,
  ~ In r rl ->
  undef_regs rl rs r = rs r.

Lemma exec_memcpy_aux_Ofs_IR14:
  forall dregs ras rad ofs1 ofs2 sz (rs: regset) m rs' m',
  exec_memcpy_aux dregs ras rad (Ofs ofs1) (Ofs ofs2) sz rs m = Next rs' m' ->
  ~ In (IR IR14 : dreg) dregs ->
  rs' IR14 = rs IR14.

Lemma addimm_preserves_IR14:
  forall r1 r2 n k (rs: regset) m rs' m',
  exec_straight ge (addimm r1 r2 n k) rs m k rs' m' ->
  r1 <> IR14 ->
  rs' IR14 = rs IR14.

Lemma exec_straight_suffix:
  forall c rs m c2 rs2 m2 c3 rs3 m3,
  exec_straight ge c rs m c3 rs3 m3 ->
  exec_straight ge c rs m c2 rs2 m2 ->
  (length c2 > length c3)%nat ->
  exec_straight ge c2 rs2 m2 c3 rs3 m3.

Lemma indexed_memcpy_access_preserves_IR14:
  forall mk_instr mk_immed ras rad n1 n2 k (rs: regset) m rs' m',
  exec_straight ge (indexed_memcpy_access mk_instr mk_immed ras rad n1 n2 k) rs m k rs' m' ->
  (forall ras' rad' n1' n2' rs0 m0 rs0' m0',
     exec_basic ge (mk_instr ras' rad' n1' n2') rs0 m0 = Next rs0' m0' -> rs0' IR14 = rs0 IR14) ->
  rs' IR14 = rs IR14.

Lemma transl_memcpy_preserves_IR14:
  forall sz bargs k c (rs: regset) m,
  transl_memcpy sz bargs k = OK c ->
  preserves_IR14 (MBmemcpy sz bargs) = true ->
  forall rs' m',
  exec_straight ge c rs m k rs' m' ->
  rs' IR14 = rs IR14.

Lemma transl_instr_basic_preserves_IR14:
  forall f i r12 k c (rs: regset) m,
  transl_instr_basic f i r12 k = OK c ->
  preserves_IR14 i = true ->
  forall rs' m',
  exec_straight ge c rs m k rs' m' ->
  rs' IR14 = rs IR14.

End CONSTRUCTORS.