Module Canaryproof


Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
Require Import AST Linking.
Require Import Memory Registers Op RTL Maps.

Require Import Globalenvs Values.
Require Import Linking Values Memory Globalenvs Events Smallstep.
Require Import Registers Op RTL.
Require Import Canary.

Lemma cmp_canary_ok: forall m,
  eval_condition canary_cmp ((canary_val tt) :: (canary_val tt) :: nil) m = Some true.
Proof.
  intro. unfold canary_cmp.
  match goal with
  | |- context [Archi.canary64] => unfold canary_val ; destruct Archi.canary64
  | |- _ => idtac
  end.
  all : cbn; try rewrite Int64.eq_true; try rewrite Int.eq_true; reflexivity.
Qed.

Lemma load_canary_ok:
  Val.load_result canary_chunk (canary_val tt) = (canary_val tt).
Proof.
  unfold canary_chunk, canary_val.
  destruct Archi.canary64; reflexivity.
Qed.
                                            
Lemma padding_correct : forall ofs al, (al | ofs + padding ofs al).
Proof.
  intros. unfold padding.
  pose proof (Z_div_mod_eq_full ofs al) as EQ.
  destruct zeq.
  - rewrite e in EQ. rewrite Z.add_0_r in EQ.
    rewrite Z.add_0_r.
    exists (ofs / al). rewrite Z.mul_comm. assumption.
  - replace (ofs + (al - ofs mod al)) with
      (al * ((ofs / al) + 1)); cycle 1.
    { rewrite EQ at 2. ring. }
    exists (ofs / al + 1). ring.
Qed.
               
Lemma canary_offset_correct: forall f,
    ( align_chunk canary_chunk | canary_offset f).
Proof.
  unfold canary_offset. intros.
  apply padding_correct.
Qed.

Lemma padding_nonneg: forall x al (POS : al > 0), 0 <= padding x al.
Proof.
  unfold padding. intros.
  destruct zeq. lia.
  assert (0 < al) as POS' by lia.
  pose proof (Z.mod_pos_bound x al POS'). lia.
Qed.

Definition f_padding_nonneg f := padding_nonneg (fn_stacksize f) _ (align_chunk_pos canary_chunk).

Lemma no_negative_stacksize : forall f,
    canary_needed f = true -> 0 <= f.(fn_stacksize).
Proof.
  unfold canary_needed. intros.
  destruct getcanary. 2: discriminate.
  destruct zle. 2: discriminate.
  assumption.
Qed.
  
Lemma no_huge_stacksize : forall f,
    canary_needed f = true -> 0 <= (canary_offset f) <= Ptrofs.max_unsigned.
Proof.
  unfold canary_needed. intros.
  destruct getcanary. 2: discriminate.
  destruct zle. 2: discriminate.
  destruct zle. 2: discriminate.
  split. 2: assumption.
  unfold canary_offset.
  pose proof (f_padding_nonneg f).
  lia.
Qed.
  
Lemma eval_getcanary: forall canary_op
    (GET : getcanary = Some canary_op)
    (F V: Type) (genv: Genv.t F V) sp m,
    eval_operation genv sp canary_op nil m = Some (canary_val tt).
Proof.
  intros.
  unfold getcanary in *; inv GET; reflexivity.
Qed.

Lemma eval_clearcanary: forall
  (F V: Type) (genv: Genv.t F V) sp m,
    exists v,
    eval_operation genv sp clearcanary nil m = Some v.
Proof.
  intros. unfold clearcanary.
  destruct Archi.canary64; cbn; eexists; reflexivity.
Qed.

Ltac mylia := unfold Mem.valid_block, node, Ple, Plt in *; cbn in *; lia.

Lemma code_append_remain: forall pc' (st : code * node) fop (LT: Plt pc' (snd st)),
    (fst (code_append st fop)) ! pc' = (fst st) ! pc'.
Proof.
  unfold code_append, Plt. intros.
  destruct st as (co, pc). cbn in *.
  apply PTree.gso. lia.
Qed.

Lemma code_append_incr: forall (st : code * node) fop,
    (snd (code_append st fop)) = Pos.succ (snd st).
Proof.
  unfold code_append. intros.
  destruct st as (co, pc). reflexivity.
Qed.

Lemma code_append_set: forall st fop pc (EQ : pc = (snd st)),
    (fst (code_append st fop)) ! pc = Some (fop pc).
Proof.
  unfold code_append. intros. cbn.
  destruct st. cbn in *. subst. apply PTree.gss.
Qed.

Ltac rew_code_append_remain := rewrite code_append_remain by (repeat rewrite code_append_incr ; unfold Plt in *; cbn; unfold node in *; lia).

Lemma entry_sequence_remain: forall pc' entrypoint offset tmpreg st
  (LT: Plt pc' (snd st)),
    (fst (entry_sequence entrypoint offset tmpreg st)) ! pc' = (fst st) ! pc'.
Proof.
  intros. unfold entry_sequence.
  destruct getcanary. 2: reflexivity.
  repeat rew_code_append_remain.
  reflexivity.
Qed.

Lemma entry_sequence_incr: forall entrypoint offset tmpreg (st: code*node),
    Ple (snd st) (snd (entry_sequence entrypoint offset tmpreg st)).
Proof.
  intros. unfold entry_sequence.
  destruct getcanary. 2: apply Ple_refl.
  repeat rewrite code_append_incr.
  mylia.
Qed.

Lemma entry_sequence_incr2: forall entrypoint offset tmpreg st,
    getcanary <> None ->
    Ple ((snd st)+3)%positive (snd (entry_sequence entrypoint offset tmpreg st)).
Proof.
  intros. unfold entry_sequence.
  destruct getcanary. 2: contradiction.
  repeat rewrite code_append_incr.
  mylia.
Qed.

Lemma crash_sequence_remain: forall pc' st (LT: Plt pc' (snd st)),
    (fst (crash_sequence st)) ! pc' = (fst st) ! pc'.
Proof.
  intros. unfold crash_sequence.
  repeat rew_code_append_remain. reflexivity.
Qed.

Lemma crash_sequence_incr: forall st,
    Plt (snd st) (snd (crash_sequence st)).
Proof.
  unfold crash_sequence. intros.
  repeat rewrite code_append_incr. mylia.
Qed.

Lemma check_sequence_incr:
  forall crash_pc offset tmpreg code insn,
    Ple (snd code) (snd (check_sequence crash_pc offset tmpreg insn code)).
Proof.
  intros. unfold check_sequence.
  destruct getcanary as [canary_op | ]. 2: apply Ple_refl.
  repeat rewrite code_append_incr. mylia.
Qed.

Lemma check_sequence_remain:
  forall crash_pc offset tmpreg code insn pc (LT : Plt pc (snd code)),
    (fst (check_sequence crash_pc offset tmpreg insn code)) ! pc =
      (fst code) ! pc.
Proof.
  intros. unfold check_sequence.
  destruct getcanary. 2: reflexivity.
  repeat rewrite code_append_remain. reflexivity.
  all: repeat rewrite code_append_incr; mylia.
Qed.

Lemma apply_check_incr:
  forall crash_pc offset tmpreg code at_pc insn,
    Ple (snd code) (snd (apply_check crash_pc offset tmpreg code at_pc insn)).
Proof.
  intros. unfold apply_check.
  destruct (check_insn insn). 2: apply Ple_refl.
  Local Opaque check_sequence. cbn.
  apply check_sequence_incr.
Qed.

Lemma apply_check_remain1:
  forall crash_pc offset tmpreg code at_pc insn pc
    (NOT_INSN: check_insn insn = false),
    (fst (apply_check crash_pc offset tmpreg code at_pc insn)) ! pc =
      (fst code) ! pc.
Proof.
  intros. unfold apply_check. rewrite NOT_INSN. reflexivity.
Qed.

Lemma apply_check_remain2:
  forall crash_pc offset tmpreg code at_pc insn pc
    (LT: Plt pc (snd code)) (NEQ: pc <> at_pc),
    (fst (apply_check crash_pc offset tmpreg code at_pc insn)) ! pc =
      (fst code) ! pc.
Proof.
  intros. unfold apply_check. destruct (check_insn insn); cbn.
  - rewrite PTree.gso by congruence.
    apply check_sequence_remain. assumption.
  - reflexivity.
Qed.
  
Lemma apply_checks_list_incr:
  forall l crash_pc offset tmpreg code,
  Ple (snd code)
    (snd
       (fold_left
          (fun (a : RTL.code * node) (p : positive * instruction) =>
           apply_check crash_pc offset tmpreg a (fst p) (snd p))
          l code)).
Proof.
  induction l; intros; cbn. apply Ple_refl.
  eapply Ple_trans.
  - apply apply_check_incr.
  - apply IHl.
Qed.
  
Lemma apply_checks_list_remain:
  forall l crash_pc offset tmpreg code pc
    (LT: Plt pc (snd code))
    (NOT_INSN: forall insn, In (pc, insn) l -> check_insn insn = false),
    (fst
       (fold_left
          (fun (a : RTL.code * node) (p : positive * instruction) =>
           apply_check crash_pc offset tmpreg a (fst p) (snd p))
          l code)) ! pc = (fst code) ! pc.
Proof.
  induction l; intros; cbn. reflexivity.
  rewrite IHl; cycle 1.
  { pose proof (apply_check_incr crash_pc offset tmpreg code (fst a) (snd a)).
    mylia. }
  { intros. apply NOT_INSN. right. assumption. }
  destruct (peq pc (fst a)).
  { subst.
    apply apply_check_remain1.
    apply NOT_INSN. left. destruct a. reflexivity. }
  apply apply_check_remain2; assumption.
Qed.

Lemma apply_checks_incr:
  forall crash_pc offset tmpreg original_code code,
    Ple (snd code) (snd (apply_checks crash_pc offset tmpreg original_code code)).
Proof.
  intros. unfold apply_checks. rewrite PTree.fold_spec.
  apply apply_checks_list_incr.
Qed.

Lemma apply_checks_remain:
  forall crash_pc offset tmpreg original_code code pc
    (LT: Plt pc (snd code))
    (NOT_INSN: forall insn, original_code ! pc = Some insn ->
                            check_insn insn = false),
    (fst (apply_checks crash_pc offset tmpreg original_code code)) ! pc =
      (fst code) ! pc.
Proof.
  intros. unfold apply_checks. rewrite PTree.fold_spec.
  apply apply_checks_list_remain. assumption.
  intros. apply NOT_INSN.
  apply PTree.elements_complete. assumption.
Qed.

Local Opaque canary_needed entry_sequence crash_sequence.

Ltac use_entry_sequence_incr :=
  match goal with | |- context [ entry_sequence ?a ?b ?c ?d ] =>
                        pose proof (entry_sequence_incr a b c d) end.

Ltac use_crash_sequence_incr :=
  match goal with | |- context [ crash_sequence ?a ] =>
                        pose proof (crash_sequence_incr a) end.

Local Transparent canary_needed.
Lemma canary_exists_if_needed: forall f, canary_needed f = true -> (getcanary <> None).
Proof.
  unfold canary_needed. intros. destruct getcanary; discriminate.
Qed.

Ltac use_entry_sequence_incr2 :=
  match goal with | NEEDED: canary_needed ?f = true
               |- context [ entry_sequence ?a ?b ?c ?d ] =>
                        pose proof (entry_sequence_incr2 a b c d (canary_exists_if_needed _ NEEDED)) as ENTRY_INCR end.

Lemma transf_code:
  forall f pc i,
  f.(fn_code)!pc = Some i -> ((check_insn i) && (canary_needed f) = false) ->
  (transf_function f).(fn_code)!pc = Some i.
Proof.
  intros.
  assert (Ple pc (max_pc_function f)) as LE.
  { eapply max_pc_function_sound; eassumption. }
  unfold transf_function.
  destruct canary_needed; cbn. 2: assumption.
  rewrite apply_checks_remain.
  - rewrite crash_sequence_remain.
    + rewrite entry_sequence_remain; cbn. assumption. mylia.
    + use_entry_sequence_incr. mylia.
  - use_crash_sequence_incr. use_entry_sequence_incr. mylia.
  - intros.
    replace i with insn in H0 by congruence.
    rewrite andb_true_r in H0. assumption.
Qed.

Record has_check_sequence f pc code' (chk_pc' : node) : Prop :=
  { chk_crash_pc : node;
     chk_tmpreg : positive;
     chk_canary_op : operation;
     tmp_reg_ok : Plt (max_reg_function f) chk_tmpreg;
     chk_canary_op_ok : getcanary = Some chk_canary_op;
     chk_jump: code' ! pc = Some (Inop chk_pc');
     chk_load: code' ! chk_pc' =
        Some (Iload TRAP canary_chunk (Ainstack (Ptrofs.repr (canary_offset f)))
          nil chk_tmpreg (Pos.succ chk_pc'));
     chk_canary: code' ! (Pos.succ chk_pc') =
        Some (Iop chk_canary_op nil (Pos.succ chk_tmpreg) (chk_pc' + 2)%positive);
     chk_cond: code' ! (chk_pc' + 2)%positive =
        Some (Icond (negate_condition canary_cmp)
                       (chk_tmpreg :: (Pos.succ chk_tmpreg) :: nil)
                      chk_crash_pc (chk_pc' + 3)%positive (Some false)) ;
     chk_insn: code' ! (chk_pc' + 3)%positive =
                 f.(fn_code) ! pc
  }.

Ltac use_apply_check_incr :=
  match goal with
  | |- context[apply_check ?a ?b ?c ?d ?e ?f] =>
      pose proof (apply_check_incr a b c d e f)
  end.
         
Lemma apply_check_has:
  forall f crash_pc tmpreg code at_pc insn canary_op
    (AT_CODE: f.(fn_code) ! at_pc = Some insn)
    (AT_PC: Plt at_pc (snd code))
    (TMPREG: Plt (max_reg_function f) tmpreg)
    (CANARY_OP : getcanary = Some canary_op)
    (CHECK_INSN: check_insn insn = true),
    has_check_sequence f at_pc
      (fst (apply_check crash_pc (canary_offset f) tmpreg code at_pc insn))
      (snd code).
Proof.
  intros.
  unfold apply_check. rewrite CHECK_INSN.
  Local Transparent check_sequence.
  unfold check_sequence. rewrite CANARY_OP.

  apply Build_has_check_sequence with (chk_pc' := (snd code))
        (chk_crash_pc := crash_pc) (chk_tmpreg := tmpreg)
        (chk_canary_op := canary_op); trivial; cbn.
  { apply PTree.gss. }
  all: rewrite PTree.gso by mylia.
  - rewrite code_append_remain.
    rewrite code_append_remain.
    rewrite code_append_remain.
    { rewrite code_append_set; reflexivity. }
    all: repeat rewrite code_append_incr; mylia.
  - rewrite code_append_remain.
    rewrite code_append_remain.
    { rewrite code_append_set.
      - repeat f_equal. lia.
      - rewrite code_append_incr. reflexivity. }
    all: repeat rewrite code_append_incr; mylia.
  - rewrite code_append_remain.
    { rewrite code_append_set.
      - repeat f_equal. lia.
      - repeat rewrite code_append_incr. mylia. }
    all: repeat rewrite code_append_incr; mylia.
  - rewrite code_append_set. congruence.
    repeat rewrite code_append_incr; mylia.
Qed.

Lemma norepet_noway:
  forall {A B : Type} a b (l : list (A*B))
    (NOREPET: list_norepet (map fst ((a,b)::l)))
      (P: Prop) b'
      (IN : In (a, b') l), P.
Proof.
  intros. exfalso. inv NOREPET. apply H1.
  change a with (fst (a, b')).
  apply in_map. assumption.
Qed.

Lemma correct_positions: forall {B : Type} a c (l: list (positive*B))
  (AT_PC : Plt c a)
  (ALL : Forall (fun x => Ple x c) (map fst l))
  (P: Prop) b
  (IN : In (a,b) l), P.
Proof.
  induction l; intros; exfalso. exact IN.
  inv ALL.
  destruct IN as [FIRST | OTHER].
  { subst a0. mylia. }
  eapply IHl; eassumption.
Qed.

Local Opaque getcanary.

Lemma apply_checks_has_list:
  forall l f crash_pc tmpreg code at_pc insn canary_op
         (IN_LIST: In (at_pc, insn) l)
         (NOREPET: list_norepet (map fst l))
         (LOW: Forall (fun pc => Ple pc (max_pc_function f)) (map fst l))
    (AT_CODE: f.(fn_code) ! at_pc = Some insn)
    (AT_PC: Plt (max_pc_function f) (snd code))
    (TMPREG: Plt (max_reg_function f) tmpreg)
    (CANARY_OP : getcanary = Some canary_op)
    (CHECK_INSN: check_insn insn = true),
    exists pc',
    has_check_sequence f at_pc
      (fst
       (fold_left
          (fun (a : RTL.code * node) (p : positive * instruction) =>
           apply_check crash_pc (canary_offset f) tmpreg a (fst p) (snd p))
          l code)) pc'.
Proof.
  induction l; cbn; intros. exfalso. assumption.
  destruct IN_LIST.
  - subst a. cbn.
    assert (AT_PC' : Plt at_pc (snd code)).
    { pose proof (max_pc_function_sound _ _ _ AT_CODE). mylia. }
    destruct (apply_check_has f crash_pc tmpreg code at_pc insn canary_op AT_CODE AT_PC' TMPREG CANARY_OP CHECK_INSN).
    exists (snd code).
    eapply (Build_has_check_sequence f at_pc); try eassumption.
    + rewrite apply_checks_list_remain.
      * eassumption.
      * use_apply_check_incr. mylia.
      * intros. eapply norepet_noway; eassumption.
    + rewrite apply_checks_list_remain.
      * eassumption.
      * unfold apply_check. rewrite CHECK_INSN. cbn.
        unfold check_sequence. rewrite CANARY_OP. cbn.
        repeat rewrite code_append_incr. mylia.
      * inv LOW. intros.
        eapply correct_positions. 2: exact H2. all: eassumption.
    + rewrite apply_checks_list_remain.
      * eassumption.
      * unfold apply_check. rewrite CHECK_INSN. cbn.
        unfold check_sequence. rewrite CANARY_OP. cbn.
        repeat rewrite code_append_incr. mylia.
      * inv LOW. intros.
        eapply correct_positions. 2: exact H2. 2: eassumption.
        mylia.
    + rewrite apply_checks_list_remain.
      * eassumption.
      * unfold apply_check. rewrite CHECK_INSN. cbn.
        unfold check_sequence. rewrite CANARY_OP. cbn.
        repeat rewrite code_append_incr. mylia.
      * inv LOW. intros.
        eapply correct_positions. 2: exact H2. 2: eassumption.
        mylia.
    + rewrite apply_checks_list_remain.
      * eassumption.
      * unfold apply_check. rewrite CHECK_INSN. cbn.
        unfold check_sequence. rewrite CANARY_OP. cbn.
        repeat rewrite code_append_incr. mylia.
      * inv LOW. intros.
        eapply correct_positions. 2: exact H2. 2: eassumption.
        mylia.
        
  - apply IHl with (canary_op := canary_op) (insn := insn); trivial.
    { inv NOREPET. assumption. }
    { inv LOW. assumption. }
    use_apply_check_incr. mylia.
Qed.

Lemma apply_checks_has:
  forall f crash_pc tmpreg code at_pc insn canary_op
    (AT_CODE: f.(fn_code) ! at_pc = Some insn)
    (AT_PC: Plt (max_pc_function f) (snd code))
    (TMPREG: Plt (max_reg_function f) tmpreg)
    (CANARY_OP : getcanary = Some canary_op)
    (CHECK_INSN: check_insn insn = true),
    exists pc',
    has_check_sequence f at_pc
                       (fst (apply_checks crash_pc (canary_offset f) tmpreg f.(fn_code) code)) pc'.
Proof.
  intros. unfold apply_checks. rewrite PTree.fold_spec.
  apply apply_checks_has_list with (insn:=insn) (canary_op:=canary_op); trivial.
  - apply PTree.elements_correct. assumption.
  - apply PTree.elements_keys_norepet.
  - rewrite Forall_forall. intros.
    destruct (list_in_map_inv _ _ _ H) as ((x0,y0) & FST & IN).
    apply max_pc_function_sound with (i := y0).
    apply PTree.elements_complete. subst. exact IN.
Qed.
 
Lemma transf_code_chk:
  forall f pc insn
         (AT_CODE : f.(fn_code)!pc = Some insn)
         (INSERTED: ((check_insn insn) && (canary_needed f) = true)),
    exists pc',
  has_check_sequence f pc (transf_function f).(fn_code) pc'.
Proof.
  intros.
  pose proof (max_pc_function_sound _ _ _ AT_CODE).
  rewrite andb_true_iff in INSERTED.
  destruct INSERTED as (CHECK & NEEDED).
  unfold transf_function.
  rewrite NEEDED. cbn.
  unfold canary_needed in *.
  destruct getcanary as [canary_op | ] eqn:CANARY_OP. 2: discriminate.
  apply apply_checks_has with (insn:=insn) (canary_op:=canary_op); trivial.
  - use_crash_sequence_incr.
    use_entry_sequence_incr. mylia.
  - mylia.
Qed.

Local Transparent canary_needed getcanary.
Lemma extra_canary_size_0_if_incorrect_size: forall f,
    f.(fn_stacksize) < 0 -> extra_canary_size f = 0.
Proof.
  unfold extra_canary_size, canary_needed. intros.
  destruct (zle 0 f.(fn_stacksize)); cbn; lia.
Qed.

Definition match_prog (p tp: RTL.program) :=
  match_program (fun ctx f tf => tf = transf_fundef f) eq p tp.

Lemma transf_program_match:
  forall p, match_prog p (transf_program p).
Proof.
  intros. eapply match_transform_program; eauto.
Qed.

Section PRESERVATION.

Variables prog tprog: program.
Hypothesis TRANSL: match_prog prog tprog.
Let ge := Genv.globalenv prog.
Let tge := Genv.globalenv tprog.

Lemma functions_translated:
  forall v f,
  Genv.find_funct ge v = Some f ->
  Genv.find_funct tge v = Some (transf_fundef f).
Proof (Genv.find_funct_transf TRANSL).

Lemma function_ptr_translated:
  forall v f,
  Genv.find_funct_ptr ge v = Some f ->
  Genv.find_funct_ptr tge v = Some (transf_fundef f).
Proof (Genv.find_funct_ptr_transf TRANSL).

Lemma symbols_preserved:
  forall id,
  Genv.find_symbol tge id = Genv.find_symbol ge id.
Proof (Genv.find_symbol_transf TRANSL).

Lemma senv_preserved:
  Senv.equiv ge tge.
Proof (Genv.senv_transf TRANSL).

Lemma sig_preserved:
  forall f, funsig (transf_fundef f) = funsig f.
Proof.
  destruct f; reflexivity.
Qed.

Lemma find_function_translated:
  forall ros rs fd,
  find_function ge ros rs = Some fd ->
  find_function tge ros rs = Some (transf_fundef fd).
Proof.
  unfold find_function; intros. destruct ros as [r|id].
  eapply functions_translated; eauto.
  rewrite symbols_preserved. destruct (Genv.find_symbol ge id); try congruence.
  eapply function_ptr_translated; eauto.
Qed.

Definition match_regs (fn : function) (rs rs' : regset) :=
  (forall r, (r <= RTL.max_reg_function fn)%positive -> Val.lessdef (rs#r) (rs'#r) ) /\(
  forall r, (RTL.max_reg_function fn < r)%positive -> rs#r = Vundef).

Lemma match_regs_params:
  forall f params args args'
         (LESSDEF : Val.lessdef_list args args')
         (ALL : List.Forall (fun x => (x <= max_reg_function f)%positive) params),
         match_regs f (init_regs args params)
                    (init_regs args' params).
Proof.
  induction params; intros.
  { split. constructor. intros. constructor. }
  cbn. inv LESSDEF; unfold match_regs in *; intros.
  { split. constructor. intros. apply Regmap.gi. }
  inv ALL.
  destruct (IHparams _ _ H0 H4) as (IHparams1 & IHparams2).
  split; intros.
  - destruct (peq a r).
    { subst a. repeat rewrite Regmap.gss. assumption.
    }
    repeat rewrite Regmap.gso by congruence.
    apply IHparams1; trivial.
  - rewrite Regmap.gso by lia.
    apply IHparams2; trivial.
Qed.

Definition canary_perm m f sp :=
  Mem.range_perm m sp (f.(fn_stacksize)) (f.(fn_stacksize) + (extra_canary_size f))
                 Cur Freeable.

Definition f_out_of_bounds m f sp :=
  forall ofs (BEYOND : f.(fn_stacksize) <= ofs),
    loc_out_of_bounds m sp ofs.

Definition canary_present m f sp :=
  canary_needed f = true -> Mem.load canary_chunk m sp (canary_offset f) = Some (canary_val tt).

Lemma canary_present_store:
  forall f sp chunk m m' b i v v' m2 m2'
    (EXTENDS: Mem.extends m m')
    (STORE: Mem.store chunk m b i v = Some m2)
    (STORE': Mem.store chunk m' b i v' = Some m2')
    (OUT_OF_BOUNDS : f_out_of_bounds m f sp)
    (PRESENT: canary_present m' f sp),
    canary_present m2' f sp.
Proof.
  intros.
  unfold canary_present, f_out_of_bounds, loc_out_of_bounds in *.
  destruct canary_needed. 2: discriminate.
  intro TRUE. cbn in *.
  pose proof (PRESENT TRUE) as CANARY.
  clear PRESENT TRUE.
  erewrite Mem.load_store_other.
  exact CANARY.
  exact STORE'.
  destruct (peq b sp).
  2: left; congruence.
  right.
  subst b.
  unfold not in OUT_OF_BOUNDS.
  destruct (Mem.store_valid_access_3 _ _ _ _ _ _ STORE) as (RANGE_PERM & ALIGNED).
  assert(i <= (i + size_chunk chunk - 1) <
           (i + size_chunk chunk)) as RANGE by (pose proof (size_chunk_pos chunk); lia).
  pose proof (RANGE_PERM _ RANGE) as PERM.
  destruct (Z.lt_ge_cases (i + size_chunk chunk - 1)
                          f.(fn_stacksize)) as [LT | GE]; cycle 1.
  { exfalso.
    apply (OUT_OF_BOUNDS _ GE). apply Mem.perm_cur_max.
    eapply Mem.perm_implies. eassumption. constructor. }
  right.
  unfold canary_offset.
  pose proof (f_padding_nonneg f). lia.
Qed.

Local Opaque canary_present.

Lemma canary_present_storev:
  forall f sp chunk m m' a a' v v' m2 m2'
    (EXTENDS: Mem.extends m m')
    (LESSDEF: Val.lessdef a a')
    (STORE: Mem.storev chunk m a v = Some m2)
    (STORE': Mem.storev chunk m' a' v' = Some m2')
    (OUT_OF_BOUNDS : f_out_of_bounds m f sp)
    (PRESENT: canary_present m' f sp),
    canary_present m2' f sp.
Proof.
  destruct a; intros; try discriminate; inv LESSDEF.
  eapply canary_present_store; eassumption.
Qed.

Inductive match_stacks: block -> mem -> mem -> list RTL.stackframe -> list RTL.stackframe -> Prop :=
| match_frames_nil: forall bound m m', match_stacks bound m m' nil nil
| match_frames_cons: forall bound m m' tail tail'
           res f sp pc rs rs' (REGS : match_regs f rs rs')
           (REG_OK : (res <= max_reg_function f)%positive)
           (VALID_SP: Plt sp bound)
           (CANARY_PERM : canary_perm m' f sp)
           (OUT_OF_BOUNDS : f_out_of_bounds m f sp)
           (CANARY_PRESENT: canary_present m' f sp)
           (TAIL: match_stacks sp m m' tail tail'),
  match_stacks bound m m'
    ((Stackframe res f (Vptr sp Ptrofs.zero) pc rs) :: tail)
    ((Stackframe res (transf_function f) (Vptr sp Ptrofs.zero) pc rs') :: tail').

Lemma canary_perm_store: forall m1 m2 f sp0 chunk b0 ofs0 v
  (CANARY_PERM : canary_perm m1 f sp0)
  (STORE : Mem.store chunk m1 b0 ofs0 v = Some m2),
    canary_perm m2 f sp0.
Proof.
  unfold canary_perm. intros.
  intros ofs RANGE.
  eapply Mem.perm_store_1. eassumption.
  apply CANARY_PERM. assumption.
Qed.

Lemma canary_perm_storev: forall m1 m2 f sp0 chunk a v
  (CANARY_PERM : canary_perm m1 f sp0)
  (STORE : Mem.storev chunk m1 a v = Some m2),
    canary_perm m2 f sp0.
Proof.
  unfold Mem.storev. intros.
  destruct a; try discriminate.
  eapply canary_perm_store; eassumption.
Qed.

Lemma f_out_of_bounds_store: forall m1 m2 f sp0 chunk b ofs0 v
  (CANARY_PERM : f_out_of_bounds m1 f sp0)
  (STORE : Mem.store chunk m1 b ofs0 v = Some m2),
    f_out_of_bounds m2 f sp0.
Proof.
  unfold f_out_of_bounds. intros.
  unfold loc_out_of_bounds in *. intro PERM.
  apply Mem.perm_store_2 with (m1:=m1) (chunk:=chunk) (b:=b) (ofs:=ofs0) (v := v) in PERM.
  pose proof (CANARY_PERM ofs BEYOND).
  contradiction.
  assumption.
Qed.

Lemma f_out_of_bounds_storev: forall m1 m2 f sp0 chunk a v
  (CANARY_PERM : f_out_of_bounds m1 f sp0)
  (STORE : Mem.storev chunk m1 a v = Some m2),
    f_out_of_bounds m2 f sp0.
Proof.
  unfold Mem.storev.
  destruct a; try discriminate.
  apply f_out_of_bounds_store.
Qed.

Lemma f_out_of_bounds_free: forall m1 m2 f sp0 b lo hi
  (CANARY_PERM : f_out_of_bounds m1 f sp0)
  (FREE : Mem.free m1 b lo hi = Some m2),
    f_out_of_bounds m2 f sp0.
Proof.
  intros. unfold f_out_of_bounds, loc_out_of_bounds in *.
  intros ofs RANGE.
  pose proof (CANARY_PERM ofs RANGE) as PERM.
  intro PERM2. apply PERM.
  exact (Mem.perm_free_3 _ _ _ _ _ FREE _ _ _ _ PERM2).
Qed.
  
Lemma canary_perm_free: forall m1 m2 f sp0 b lo hi
  (NEQ: sp0 <> b)
  (CANARY_PERM : canary_perm m1 f sp0)
  (FREE : Mem.free m1 b lo hi = Some m2),
    canary_perm m2 f sp0.
Proof.
  intros. unfold canary_perm in *.
  intros ofs RANGE.
  eapply Mem.perm_free_1.
  - eassumption.
  - left. assumption.
  - apply CANARY_PERM; lia.
Qed.

Local Transparent canary_present.
Lemma canary_present_free: forall m1 m2 f sp0 b lo hi
  (NEQ: sp0 <> b)
  (CANARY_PERM : canary_present m1 f sp0)
  (FREE : Mem.free m1 b lo hi = Some m2),
    canary_present m2 f sp0.
Proof.
  intros. unfold canary_present in *.
  destruct canary_needed. 2: discriminate.
  intro TRUE. pose proof (CANARY_PERM TRUE) as LOAD.
  clear CANARY_PERM TRUE.
  erewrite Mem.load_free; try eassumption.
  left. assumption.
Qed.

Lemma f_out_of_bounds_alloc: forall m1 m2 f sp0 b lo hi
  (VALID : Mem.valid_block m1 sp0)
  (OUT_OF_BOUNDS : f_out_of_bounds m1 f sp0)
  (ALLOC : Mem.alloc m1 lo hi = (m2, b)),
    f_out_of_bounds m2 f sp0.
Proof.
  unfold Mem.valid_block, f_out_of_bounds, loc_out_of_bounds, Plt in *. intros.
  intro PERM2.
  apply (OUT_OF_BOUNDS ofs BEYOND).
  eapply Mem.perm_alloc_4; try eassumption.
  erewrite <- Mem.alloc_result in VALID by eassumption.
  lia.
Qed.
  
Lemma canary_perm_alloc: forall m1 m2 f sp0 b lo hi
  (CANARY_PERM : canary_perm m1 f sp0)
  (ALLOC : Mem.alloc m1 lo hi = (m2, b)),
    canary_perm m2 f sp0.
Proof.
  unfold canary_perm in *. intros.
  intros ofs RANGE.
  eapply Mem.perm_alloc_1. eassumption.
  apply CANARY_PERM. assumption.
Qed.
  
Lemma canary_present_alloc: forall m1 m2 f sp0 b lo hi
  (CANARY_PERM : canary_present m1 f sp0)
  (ALLOC : Mem.alloc m1 lo hi = (m2, b)),
    canary_present m2 f sp0.
Proof.
  intros.
  unfold canary_present in *.
  intro TRUE.
  pose proof (CANARY_PERM TRUE) as LOAD.
  clear CANARY_PERM TRUE.
  erewrite Mem.load_alloc_other; try eassumption.
  reflexivity.
Qed.

Lemma f_out_of_bounds_external_call:
  forall ef ge vargs t vres m1 m2 f sp
         (VALID_SP: Mem.valid_block m1 sp)
         (OUT_OF_BOUNDS: f_out_of_bounds m1 f sp)
         (EXTCALL: external_call ef ge vargs m1 t vres m2),
    f_out_of_bounds m2 f sp.
Proof.
  intros. unfold f_out_of_bounds, loc_out_of_bounds in *.
  intros ofs RANGE. pose proof (OUT_OF_BOUNDS ofs RANGE) as OOB.
  intro PERM2. apply OOB.
  eapply external_call_max_perm; eassumption.
Qed.

Lemma canary_perm_external_call:
  forall ef ge vargs vargs' t vres vres' m1 m1' m2 m2' f sp
         (CANARY_PERM : canary_perm m1' f sp)
         (VALID_SP : Mem.valid_block m1' sp)
         (OUT_OF_BOUNDS: f_out_of_bounds m1 f sp)
         (EXTCALL: external_call ef ge vargs m1 t vres m2)
         (EXTCALL': external_call ef ge vargs' m1' t vres' m2')
         (UNCHANGED: Mem.unchanged_on (loc_out_of_bounds m1) m1' m2'),
    canary_perm m2' f sp.
Proof.
  intros.
  destruct UNCHANGED.
  unfold canary_perm in *.
  intros ofs RANGE.
  rewrite <- unchanged_on_perm.
  3: assumption.
  { apply CANARY_PERM. assumption. }
  unfold f_out_of_bounds in *.
  apply OUT_OF_BOUNDS. lia.
Qed.

Lemma canary_present_external_call:
  forall ef ge vargs vargs' t vres vres' m1 m1' m2 m2' f sp
         (CANARY_PRESENT : canary_present m1' f sp)
         (VALID_SP : Mem.valid_block m1' sp)
         (OUT_OF_BOUNDS: f_out_of_bounds m1 f sp)
         (EXTCALL: external_call ef ge vargs m1 t vres m2)
         (EXTCALL': external_call ef ge vargs' m1' t vres' m2')
         (UNCHANGED: Mem.unchanged_on (loc_out_of_bounds m1) m1' m2'),
    canary_present m2' f sp.
Proof.
  intros. unfold canary_present in *.
  intro TRUE. pose proof (CANARY_PRESENT TRUE) as LOAD.
  clear CANARY_PRESENT.
  erewrite Mem.load_unchanged_on_1; try eassumption.
  unfold f_out_of_bounds, loc_out_of_bounds in *.
  intros. apply OUT_OF_BOUNDS.
  unfold canary_offset in *.
  pose proof (f_padding_nonneg f). lia.
Qed.

Lemma match_stacks_advance:
  forall bound bound2 (LE: Ple bound bound2) m m' stk stk'
         (STACKS : match_stacks bound m m' stk stk'),
    match_stacks bound2 m m' stk stk'.
Proof.
  induction stk; intros; inv STACKS.
  { constructor. }
  constructor; trivial.
  unfold Ple, Plt in *. lia.
Qed.

Lemma match_stacks_storev:
  forall stk stk' bound m m' m2 m2' chunk a a' v v'
         (EXTENDS: Mem.extends m m')
         (LESSDEF: Val.lessdef a a')
         (STORE: Mem.storev chunk m a v = Some m2)
         (STORE': Mem.storev chunk m' a' v' = Some m2')
         (STACKS: match_stacks bound m m' stk stk'),
    match_stacks bound m2 m2' stk stk'.
Proof.
  induction stk; intros; inv STACKS.
  { constructor. }
  constructor; trivial.
  - eapply canary_perm_storev; eassumption.
  - eapply f_out_of_bounds_storev; eassumption.
  - eapply canary_present_storev; eassumption.
  - eapply IHstk; eassumption.
Qed.

Lemma match_stacks_free:
  forall stk stk' bound m m' b lo lo' hi hi' m2 m2'
         (STORE: Mem.free m b lo hi = Some m2)
         (STORE': Mem.free m' b lo' hi' = Some m2')
         (STACKS: match_stacks bound m m' stk stk')
         (LE: Ple bound b),
    match_stacks bound m2 m2' stk stk'.
Proof.
  induction stk; intros; inv STACKS.
  { constructor. }
  constructor; trivial.
  - eapply canary_perm_free. 2,3: eassumption.
    mylia.
  - eapply f_out_of_bounds_free; eassumption.
  - eapply canary_present_free. 2,3: eassumption.
    mylia.
  - eapply IHstk; try eassumption.
    unfold Ple, Plt in *. lia.
Qed.

Lemma match_stacks_alloc:
  forall stk stk' bound m m' lo lo' hi hi' m2 m2' b b'
         (VALID : Ple bound (Mem.nextblock m))
         (STORE: Mem.alloc m lo hi = (m2, b))
         (STORE': Mem.alloc m' lo' hi' = (m2', b'))
         (STACKS: match_stacks bound m m' stk stk'),
    match_stacks bound m2 m2' stk stk'.
Proof.
  induction stk; intros; inv STACKS.
  { constructor. }
  constructor; trivial.
  - eapply canary_perm_alloc; eassumption.
  - eapply f_out_of_bounds_alloc with (m1 := m). 2, 3: eassumption.
    mylia.
  - eapply canary_present_alloc; eassumption.
  - eapply IHstk. 2,3,4: eassumption. mylia.
Qed.

Lemma match_stacks_external_call:
  forall stk stk' ef ge vargs vargs' t vres vres' m1 m1' m2 m2' f sp
         (MEM: Mem.extends m1 m1')
         (VALID_SP : Mem.valid_block m1 sp)
         (OUT_OF_BOUNDS: f_out_of_bounds m1 f sp)
         (EXTCALL: external_call ef ge vargs m1 t vres m2)
         (EXTCALL': external_call ef ge vargs' m1' t vres' m2')
         (UNCHANGED: Mem.unchanged_on (loc_out_of_bounds m1) m1' m2')
         (STACKS: match_stacks sp m1 m1' stk stk'),
    match_stacks sp m2 m2' stk stk'.
Proof.
  induction stk; intros; inv STACKS.
  { constructor. }
  constructor; trivial.
  - eapply canary_perm_external_call; try eassumption.
    rewrite <- Mem.valid_block_extends by eassumption. mylia.
  - eapply f_out_of_bounds_external_call; try eassumption. mylia.
  - eapply canary_present_external_call; try eassumption.
    rewrite <- Mem.valid_block_extends by eassumption. mylia.
  - eapply IHstk; try eassumption. mylia.
Qed.

Inductive match_states: RTL.state -> RTL.state -> Prop :=
| match_regular_states: forall stk stk' f sp pc rs rs' m m'
        (VALID_SP: Mem.valid_block m sp)
        (CANARY_PERM : canary_perm m' f sp)
        (OUT_OF_BOUNDS : f_out_of_bounds m f sp)
        (CANARY_PRESENT: canary_present m' f sp)
        (REGS : match_regs f rs rs')
        (MEM: Mem.extends m m')
        (STACKS: match_stacks sp m m' stk stk'),
      match_states (State stk f (Vptr sp Ptrofs.zero) pc rs m)
                   (State stk' (transf_function f) (Vptr sp Ptrofs.zero) pc rs' m')
  | match_callstates: forall stk stk' f args args' m m'
        (MEM: Mem.extends m m')
        (STACKS: match_stacks (Mem.nextblock m) m m' stk stk')
        (ARGS : Val.lessdef_list args args'),
      match_states (Callstate stk f args m)
                   (Callstate stk' (transf_fundef f) args' m')
  | match_returnstates: forall stk stk' v v' m m'
        (MEM: Mem.extends m m')
        (STACKS: match_stacks (Mem.nextblock m) m m' stk stk')
        (RES: Val.lessdef v v'),
      match_states (Returnstate stk v m)
                   (Returnstate stk' v' m').

Lemma match_regs_args : forall args f rs rs'
    (MATCH_REGS : match_regs f rs rs')
    (ARGS_OK : forall r, In r args -> (r <= (max_reg_function f))%positive),
    Val.lessdef_list (rs ## args) (rs' ## args).
Proof.
  unfold match_regs. induction args; intros; cbn; constructor.
  - apply MATCH_REGS. apply ARGS_OK. left. reflexivity.
  - apply IHargs with (f:=f). apply MATCH_REGS.
    intros. apply ARGS_OK. right. assumption.
Qed.
      
Lemma match_regs_assign :
  forall f rs rs' res v v'
         (RES_OK : (res <= (max_reg_function f))%positive)
         (MATCH_REGS : match_regs f rs rs')
         (INJECT : Val.lessdef v v'),
    match_regs f (rs # res <- v) (rs' # res <- v').
Proof.
  unfold match_regs. intros.
  destruct MATCH_REGS as (REGS1 & REGS2).
  split; intros.
  - destruct (peq r res).
    { subst r. repeat rewrite Regmap.gss. assumption. }
    repeat rewrite Regmap.gso by congruence.
    auto.
  - rewrite Regmap.gso by lia. auto.
Qed.

Lemma extra_canary_size_nonneg: forall f, 0 <= extra_canary_size f.
Proof.
  unfold extra_canary_size. intros.
  destruct canary_needed. 2: lia.
  pose proof (f_padding_nonneg f).
  unfold canary_size.
  destruct Archi.canary64; lia.
Qed.

Lemma mem_storev_valid_block_1:
  forall m m2 chunk a v sp,
    Mem.valid_block m sp ->
    Mem.storev chunk m a v = Some m2 ->
    Mem.valid_block m2 sp.
Proof.
  intros.
  destruct a; cbn in *; try discriminate.
  eapply Mem.store_valid_block_1; eassumption.
Qed.

Lemma free_with_canary:
  forall m m' m2 stk f
         (FREE : Mem.free m stk 0 (fn_stacksize f) = Some m2)
         (MEM : Mem.extends m m')
         (OUT_OF_BOUNDS : f_out_of_bounds m f stk)
         (CANARY_PERM : canary_perm m' f stk),
    exists m2',
      Mem.free m' stk 0 (fn_stacksize (transf_function f)) = Some m2' /\
        (Mem.extends m2 m2').
Proof.
  intros.
  assert(RANGE_PERM' : Mem.range_perm m' stk 0 (fn_stacksize (transf_function f)) Cur Freeable).
  { pose proof (Mem.free_range_perm _ _ _ _ _ FREE) as RANGE_PERM.
    intros ofs RANGE.
    assert (ofs < fn_stacksize f \/ ofs >= fn_stacksize f) as ZZ by lia.
    destruct ZZ.
    - apply Mem.perm_extends with (m1 := m). assumption.
      apply RANGE_PERM. lia.
    - unfold canary_perm in CANARY_PERM.
      apply CANARY_PERM. cbn in RANGE. lia.
  }
  destruct (Mem.range_perm_free _ _ _ _ RANGE_PERM') as (m2' & FREE').
  exists m2'. split. assumption.
  eapply Mem.free_right_extends. 2: eassumption.
  { eapply Mem.extends_extends_compose. 2: eassumption.
    eapply Mem.free_left_extends.
    apply Mem.extends_refl. eassumption. }
  intros.
  assert (ofs < fn_stacksize f \/ fn_stacksize f <= ofs) as ZZ by lia.
  destruct ZZ as [BELOW | ABOVE].
  - assert (0 <= ofs < fn_stacksize f) as RANGE by lia.
    apply (Mem.perm_free_2 _ _ _ _ _ FREE _ k p RANGE). assumption.
  - unfold f_out_of_bounds in *.
    pose proof (OUT_OF_BOUNDS ofs ABOVE) as OOB.
    unfold loc_out_of_bounds in OOB. apply OOB.
    pose proof (Mem.perm_free_3 _ _ _ _ _ FREE _ _ _ _ H).
    apply Mem.perm_max with (k:=k).
    apply Mem.perm_implies with (p1:=p). assumption.
    constructor.
Qed.

Lemma entry_sequence0: forall f
    (NEEDED: canary_needed f = true),
    exists canary_op, getcanary = Some canary_op /\
    (transf_function f).(fn_code) ! ((transf_function f).(fn_entrypoint)) = Some
               (Iop canary_op nil (Pos.succ (max_reg_function f))
                          ((max_pc_function f) + 2)%positive).
Proof.
  intros. unfold transf_function. rewrite NEEDED. cbn.
  pose proof (canary_exists_if_needed f NEEDED) as CANARY.
  destruct getcanary as [canary_op | ] eqn:CANARY_OP. 2: contradiction.
  clear CANARY.
  exists canary_op. split. reflexivity.
  rewrite apply_checks_remain.
  - rewrite crash_sequence_remain.
    + Local Transparent entry_sequence.
      unfold entry_sequence. rewrite CANARY_OP.
      rewrite code_append_remain. rewrite code_append_remain.
      { rewrite code_append_set. repeat f_equal. lia. reflexivity. }
      all: repeat rewrite code_append_incr; mylia.
    + use_entry_sequence_incr. mylia.
  - use_entry_sequence_incr. use_crash_sequence_incr. mylia.
  - intros insn ABSURD. exfalso.
    pose proof (max_pc_function_sound _ _ _ ABSURD). mylia.
Qed.

Local Transparent canary_needed.
Local Opaque code_append entry_sequence.

Lemma entry_sequence1: forall f
    (NEEDED: canary_needed f = true),
    (transf_function f).(fn_code) ! (max_pc_function f + 2)%positive = Some
      (Istore canary_chunk (Ainstack (Ptrofs.repr (canary_offset f))) nil
         (Pos.succ (max_reg_function f)) ((max_pc_function f) + 3)%positive).
Proof.
  intros. unfold transf_function. rewrite NEEDED. cbn.
  pose proof (canary_exists_if_needed f NEEDED) as CANARY.
  destruct getcanary as [canary_op | ] eqn:CANARY_OP. 2: contradiction.
  clear CANARY.
  Local Transparent entry_sequence.
  unfold entry_sequence. rewrite CANARY_OP.
  rewrite apply_checks_remain.
  - rewrite crash_sequence_remain.
    + rewrite code_append_remain.
      { rewrite code_append_set. repeat f_equal. lia.
        rewrite code_append_incr. cbn. lia. }
      repeat rewrite code_append_incr. mylia.
    + repeat rewrite code_append_incr. mylia.
  - repeat rewrite code_append_incr.
    use_crash_sequence_incr.
    repeat rewrite code_append_incr in H. mylia.
  - intros insn ABSURD. exfalso.
    pose proof (max_pc_function_sound _ _ _ ABSURD). mylia.
Qed.

Local Transparent canary_needed.
Local Opaque code_append entry_sequence clearcanary.

Lemma entry_sequence2: forall f
    (NEEDED: canary_needed f = true),
    (transf_function f).(fn_code) ! (max_pc_function f + 3)%positive = Some
               (Iop clearcanary nil (Pos.succ (max_reg_function f))
                          (f.(fn_entrypoint))).
Proof.
  intros. unfold transf_function. rewrite NEEDED. cbn.
  pose proof (canary_exists_if_needed f NEEDED) as CANARY.
  destruct getcanary as [canary_op | ] eqn:CANARY_OP. 2: contradiction.
  clear CANARY.
  Local Transparent entry_sequence.
  unfold entry_sequence. rewrite CANARY_OP.
  rewrite apply_checks_remain.
  - rewrite crash_sequence_remain.
    { rewrite code_append_set. reflexivity.
      repeat rewrite code_append_incr. cbn. lia. }
    repeat rewrite code_append_incr. mylia.
  - repeat rewrite code_append_incr.
    use_crash_sequence_incr.
    repeat rewrite code_append_incr in H. mylia.
  - intros insn ABSURD. exfalso.
    pose proof (max_pc_function_sound _ _ _ ABSURD). mylia.
Qed.

Lemma params_preserved: forall f,
    (fn_params (transf_function f)) = fn_params f.
Proof.
  reflexivity.
Qed.

Lemma init_regs_lessdef: forall params args args' (LESSDEF : Val.lessdef_list args args') r,
    Val.lessdef (init_regs args params) # r
                (init_regs args' params) # r.
Proof.
  induction params; intros; cbn.
  { constructor. }
  destruct args as [ | hargs targs]; inv LESSDEF.
  { constructor. }
  destruct (peq a r).
  { subst. repeat rewrite Regmap.gss.
    assumption. }
  repeat rewrite Regmap.gso by congruence.
  apply IHparams. assumption.
Qed.

Lemma canary_encode_size :
  (Z.of_nat (Datatypes.length (encode_val canary_chunk (canary_val tt)))) =
                                       canary_size.
Proof.
  unfold canary_val, canary_chunk, canary_size. intros.
  rewrite encode_val_length.
  destruct Archi.canary64 ; reflexivity.
Qed.

Lemma init_regs_undef:
  forall params args r,
  (forall r', In r' params -> Plt r' r) ->
  (init_regs args params) # r = Vundef.
Proof.
  induction params; intros. reflexivity.
  destruct args. reflexivity. cbn.
  destruct (peq a r).
  { subst.
    assert (Plt r r).
    { apply H. left. reflexivity. }
    mylia.
  }
  rewrite Regmap.gso by congruence.
  apply IHparams.
  intros r' IN.
  apply H. right. assumption.
Qed.

Lemma match_stacks_create_frame: forall
    s s' stk sp m m' m2 m2' m2'' sz extra ofs
  (PLE: Ple sp stk)
  (STACKS: match_stacks sp m m' s s')
  (ALLOC: Mem.alloc m 0 sz = (m2, stk))
  (ALLOC': Mem.alloc m' 0 (sz + extra) = (m2', stk))
  (EXTENDS : Mem.extends m m')
  (EXTENDS2 : Mem.extends m2 m2')
  (STORE' : Mem.store canary_chunk m2' stk ofs (canary_val tt) =
           Some m2''),
    match_stacks sp m2 m2'' s s'.
Proof.
  induction s; intros; inv STACKS. { constructor. }
  constructor; trivial.
  - eapply canary_perm_store. 2: eassumption.
    eapply canary_perm_alloc. 2: eassumption.
    assumption.
  - unfold f_out_of_bounds, loc_out_of_bounds in *. intros.
    intro PERM2.
    assert (sp0 <> stk) as NEQ by mylia.
    pose proof (Mem.perm_alloc_4 _ _ _ _ _ ALLOC _ _ _ _ PERM2 NEQ) as PERM.
    pose proof (OUT_OF_BOUNDS ofs0 BEYOND).
    contradiction.
  - unfold canary_present in *. intro TRUE.
    pose proof (CANARY_PRESENT TRUE) as LOAD.
    clear CANARY_PRESENT.
    erewrite Mem.load_store_other. 2: eassumption.
    2: left; mylia.
    erewrite Mem.load_alloc_unchanged; try eassumption.
    rewrite <- Mem.valid_block_extends; try eassumption.
    pose proof (Mem.alloc_result _ _ _ _ _ ALLOC).
    mylia.
  - eapply IHs; try eassumption. mylia.
Qed.

Local Opaque canary_needed.

Definition check_sequence_passthrough
           stk' f sp pc rs rs' m' :=
  exists pc' rs2',
    star step tge (State stk' (transf_function f) sp pc rs' m') E0
                  (State stk' (transf_function f) sp pc' rs2' m') /\
    match_regs f rs rs2' /\
    (transf_function f).(fn_code) ! pc' = f.(fn_code) ! pc.

Lemma match_regs_above: forall f rs rs'
  (REGS: match_regs f rs rs') r v (ABOVE: Plt (max_reg_function f) r),
    (match_regs f rs (rs' # r <- v)).
Proof.
  intros. destruct REGS as (REGS1 & REGS2). constructor; intros.
  - rewrite Regmap.gso by mylia. apply REGS1. assumption.
  - apply REGS2. assumption.
Qed.

Local Opaque canary_cmp.
Lemma has_check_sequence_exec:
  forall stk stk' f sp pc rs rs' m m'
         (insn : instruction)
         (AT_PC: f.(fn_code) ! pc = Some insn)
         (MATCH: match_states (State stk f sp pc rs m)
                              (State stk' (transf_function f) sp pc rs' m')),
    check_sequence_passthrough stk' f sp pc rs rs' m'.
Proof.
  intros.
  pose proof (transf_code f pc insn AT_PC) as TRANSF.
  pose proof (transf_code_chk f pc insn AT_PC) as TRANSF_CHK.
  inv MATCH.
  destruct (check_insn insn && canary_needed f) eqn:TRIG; cycle 1.
  { pose proof (TRANSF eq_refl) as TRANSF'.
    exists pc. exists rs'. split. apply star_refl.
    split. assumption. congruence.
  }
  rewrite andb_true_iff in TRIG.
  destruct TRIG as (CHECK_INSN & NEEDED).
  destruct (TRANSF_CHK eq_refl) as (pc' & HAS_CHECK).
  destruct HAS_CHECK.
  unfold check_sequence_passthrough.
  eexists. eexists. split. apply plus_star.
  eapply plus_left' with (t1:=E0) (t2:=E0). 3: reflexivity.
  { apply exec_Inop. eassumption. }
  eapply plus_left' with (t1:=E0) (t2:=E0). 3: reflexivity.
  { eapply exec_Iload with (v:=canary_val tt). eassumption.
    eapply has_loaded_normal.
    { reflexivity. }
    cbn. rewrite Ptrofs.add_zero_l.
    rewrite Ptrofs.unsigned_repr by (apply no_huge_stacksize; assumption).
    exact (CANARY_PRESENT NEEDED).
  }
  eapply plus_left' with (t1:=E0) (t2:=E0). 3: reflexivity.
  { eapply exec_Iop with (v:=canary_val tt). eassumption.
    apply eval_getcanary. assumption. }
  eapply plus_one.
  { eapply exec_Icond. eassumption.
    {
      rewrite eval_negate_condition. cbn.
      rewrite Regmap.gso by lia. rewrite Regmap.gss.
      rewrite Regmap.gss.
      rewrite cmp_canary_ok. reflexivity.
    }
    reflexivity.
  }
  split.
  { apply match_regs_above. 2: mylia.
    apply match_regs_above. 2: mylia.
    assumption. }
  assumption.
Qed.

Ltac TRANSF := apply transf_code; (eassumption || reflexivity).

Lemma step_simulation:
  forall s1 t s2 (STEP : step ge s1 t s2)
  s1' (MS: match_states s1 s1'),
  exists s2', plus step tge s1' t s2' /\ match_states s2 s2'.
Proof.
  intros. inv STEP; inv MS.

  (* Inop *)
  - eexists. split.
    + apply plus_one. apply exec_Inop.
      TRANSF.
    + constructor; auto.
      
  (* Iop *)
  - assert (ARGS_LESSDEF : Val.lessdef_list (rs ## args) (rs' ## args)).
    { apply match_regs_args with (f := f). assumption.
      intros r IN. eapply max_reg_function_use. eassumption. exact IN. }
    destruct (eval_operation_lessdef _ _ _ ARGS_LESSDEF MEM H0) as
      (v' & EVAL' & RES_LESSDEF).
    eexists. split.
    + apply plus_one.
      apply exec_Iop with (op := op) (args := args).
      TRANSF.
      rewrite eval_operation_preserved with (ge1 := ge) by apply symbols_preserved.
      exact EVAL'.
    + constructor; trivial.
      apply match_regs_assign; trivial.
      eapply max_reg_function_def. eassumption. reflexivity.

  (* Iload *)
  - rename stk' into s'.
    assert (ARGS_LESSDEF : Val.lessdef_list (rs ## args) (rs' ## args)).
    { apply match_regs_args with (f := f). assumption.
      intros r IN. eapply max_reg_function_use. eassumption. exact IN. }
    inv H0.
    + destruct (eval_addressing_lessdef _ _ _ ARGS_LESSDEF EVAL) as
        (a' & EVAL' & ADDR_LESSDEF).
      destruct (Mem.loadv_extends _ _ _ _ _ _ MEM LOAD ADDR_LESSDEF)
             as (v' & LOAD' & LOAD_LESSDEF).
      eexists. split.
      * apply plus_one.
        apply exec_Iload with (trap:=trap) (chunk:=chunk) (addr:=addr) (args:=args).
        TRANSF.
        eapply has_loaded_normal.
        -- rewrite eval_addressing_preserved with (ge1 := ge) by apply symbols_preserved.
           eassumption.
        -- eassumption.
      * constructor; trivial.
        apply match_regs_assign; trivial.
        eapply max_reg_function_def. eassumption. reflexivity.
        
    + destruct (eval_addressing tge (Vptr sp0 Ptrofs.zero) addr rs' ## args) as [a' | ] eqn:ADDR'.
      * destruct (Mem.loadv chunk m' a') as [v' | ] eqn:LOAD'.
        -- eexists. split.
           ++ apply plus_one.
              apply exec_Iload with (trap:=NOTRAP) (chunk:=chunk) (addr:=addr) (args:=args).
              TRANSF.
              apply has_loaded_normal with (a:=a'). assumption.
              eassumption.
           ++ constructor; trivial.
              apply match_regs_assign; trivial.
              eapply max_reg_function_def. eassumption. reflexivity.
        -- eexists. split.
           ++ apply plus_one.
              apply exec_Iload with (trap:=NOTRAP) (chunk:=chunk) (addr:=addr) (args:=args).
              TRANSF.
              apply has_loaded_default.
              ** intros a'2 ADDR'2. congruence.
              ** reflexivity.
           ++ constructor; trivial.
              apply match_regs_assign; trivial.
              eapply max_reg_function_def. eassumption. reflexivity.
              
      * eexists. split.
        -- apply plus_one.
           apply exec_Iload with (trap:=NOTRAP) (chunk:=chunk) (addr:=addr) (args:=args).
           TRANSF.
           apply has_loaded_default.
           { intros a' ADDR'2. congruence. }
           reflexivity.
        -- constructor; trivial.
           apply match_regs_assign; trivial.
           eapply max_reg_function_def. eassumption. reflexivity.
           
  (* Istore *)
  - rename H0 into ADDR.
    rename H1 into STORE.
    rename m' into m2.
    rename m'0 into m'.
    assert (ARGS_LESSDEF : Val.lessdef_list (rs ## args) (rs' ## args)).
    { apply match_regs_args with (f := f). assumption.
      intros r IN. eapply max_reg_function_use. eassumption.
      cbn. right. assumption. }
    destruct (eval_addressing_lessdef _ _ _ ARGS_LESSDEF ADDR) as
      (a' & ADDR' & ADDR_LESSDEF).
    assert (SRC_LESSDEF : Val.lessdef rs # src rs' # src).
    { apply REGS.
      eapply max_reg_function_use. eassumption.
      left. reflexivity. }
    destruct (Mem.storev_extends _ _ _ _ _ _ _ _ MEM STORE ADDR_LESSDEF SRC_LESSDEF) as (m2' & STORE' & EXTENDS').
    eexists. split.
    + apply plus_one.
      apply exec_Istore with (chunk:=chunk) (addr:=addr) (args:=args) (src:=src) (a:=a').
      TRANSF.
      rewrite eval_addressing_preserved with (ge1 := ge) by apply symbols_preserved.
      assumption. eassumption.
    + constructor; trivial.
      * eapply mem_storev_valid_block_1; eassumption.
      * eapply canary_perm_storev; eassumption.
      * eapply f_out_of_bounds_storev; eassumption.
      * eapply canary_present_storev. exact MEM. exact ADDR_LESSDEF.
        all: eassumption.
      * eapply match_stacks_storev. exact MEM. exact ADDR_LESSDEF.
        all: eassumption.
        
  (* Icall *)
  - assert (ARGS_LESSDEF : Val.lessdef_list (rs ## args) (rs' ## args)).
    { apply match_regs_args with (f := f). assumption.
      intros r IN. eapply max_reg_function_use. eassumption.
      cbn. destruct ros ; [right ; assumption | assumption]. }
    eexists. split.
    + apply plus_one.
      apply exec_Icall with (sig:=(funsig fd)) (ros:=ros).
      3: apply sig_preserved.
      TRANSF.
      destruct ros; cbn in *.
      * apply functions_translated.
        assert (REG_OK : (r <= max_reg_function f)%positive).
        { eapply max_reg_function_use. eassumption. cbn.
          left. reflexivity. }
        destruct (Genv.find_funct_inv _ _ H0) as (b & PTR).
        destruct REGS as (REGS1 & REGS2).
        pose proof (REGS1 r REG_OK) as LESSDEF.
        rewrite PTR in LESSDEF. rewrite PTR in H0.
        inv LESSDEF. assumption.
      * rewrite symbols_preserved.
        destruct (Genv.find_symbol ge i). 2: discriminate.
        apply function_ptr_translated. exact H0.
    + apply match_callstates; trivial.
      constructor; trivial.
      eapply max_reg_function_def. eassumption. reflexivity.
        
  (* Itailcall *)
  - rename m' into m2. rename m'0 into m'. rename stk' into s'.
    rename H2 into FREE.
    destruct (free_with_canary _ _ _ _ _ FREE MEM OUT_OF_BOUNDS CANARY_PERM) as (m2' & FREE' & EXTENDS2).
    assert (match_states (State s f (Vptr stk Ptrofs.zero) pc rs m)
                         (State s' (transf_function f) (Vptr stk Ptrofs.zero) pc rs' m')) as MS.
    { constructor; assumption. }
    destruct (has_check_sequence_exec s s' f _ pc rs rs' m m' _ H MS) as (pc' & rs2' & STAR & REGS' & CODE).
    assert (ARGS_LESSDEF : Val.lessdef_list (rs ## args) (rs2' ## args)).
    { apply match_regs_args with (f := f). assumption.
      intros r IN. eapply max_reg_function_use. eassumption.
      cbn. destruct ros ; [right ; assumption | assumption]. }
    eexists. split.
    + eapply plus_right with (t1:=E0) (t2:=E0). 3: reflexivity.
      exact STAR.
      apply exec_Itailcall with (sig:=(funsig fd)) (ros:=ros) (args:=args).
      3: apply sig_preserved.
      * congruence.
      * destruct ros; cbn in *.
        -- apply functions_translated.
           assert (REG_OK : (r <= max_reg_function f)%positive).
           { eapply max_reg_function_use. eassumption. cbn.
             left. reflexivity. }
           destruct (Genv.find_funct_inv _ _ H0) as (b & PTR).
           destruct REGS' as (REGS1 & REGS2).
           pose proof (REGS1 r REG_OK) as LESSDEF.
           rewrite PTR in LESSDEF. rewrite PTR in H0.
           inv LESSDEF. assumption.
        -- rewrite symbols_preserved.
           destruct (Genv.find_symbol ge i). 2: discriminate.
           apply function_ptr_translated. exact H0.
      * eassumption.
    + constructor; trivial.
      apply match_stacks_advance with (bound := stk).
      { erewrite Mem.nextblock_free by eassumption.
        unfold Mem.valid_block, Ple, Plt in *. lia. }
      eapply match_stacks_free; try eassumption.
      apply Ple_refl.
        
  (* Ibuiltin *)
  - rename m' into m2. rename m'0 into m'.
    rename H0 into ARGS. rename H1 into CALL.
    assert (forall r, Val.lessdef rs#r rs'#r) as LESSDEF_REGS.
    { destruct REGS as (REGS1 & REGS2). intro r.
      assert (r <= max_reg_function f \/ max_reg_function f < r)%positive as ZZ by lia.
      destruct ZZ as [BELOW | ABOVE].
      - apply REGS1. trivial.
      - rewrite REGS2 by trivial. constructor. }
    destruct (eval_builtin_args_lessdef _ LESSDEF_REGS MEM ARGS)
             as (vargs' & ARGS' & LESSDEF_ARGS).
    destruct (external_call_mem_extends ef _ _ _ _ CALL MEM LESSDEF_ARGS) as
      (vres' & m2' & CALL' & LESSDEF_RES & EXTENDS2 & UNCHANGED).
    eexists. split.
    + apply plus_one.
      apply exec_Ibuiltin with (ef:=ef) (args:=args) (vargs:=vargs').
      * TRANSF.
      * apply eval_builtin_args_preserved with (ge1:=ge).
        -- apply symbols_preserved.
        -- assumption.
      * apply external_call_symbols_preserved with (ge1:=ge).
        { apply senv_preserved. }
        eassumption.
    + constructor; trivial.
      * pose proof (external_call_nextblock _ _ _ _ _ _ _ CALL).
        unfold Mem.valid_block, Ple, Plt in *. lia.
      * destruct UNCHANGED.
        unfold canary_perm in *.
        intros ofs RANGE.
        apply unchanged_on_perm.
        -- apply OUT_OF_BOUNDS. lia.
        -- erewrite <- Mem.valid_block_extends; eassumption.
        -- apply CANARY_PERM ; assumption.
      * unfold f_out_of_bounds in *.
        intros ofs RANGE.
        unfold loc_out_of_bounds in *.
        intro PERM2. apply (OUT_OF_BOUNDS ofs RANGE).
        eapply external_call_max_perm. exact CALL.
        assumption. assumption.
      * eapply canary_present_external_call; try eassumption.
        erewrite <- Mem.valid_block_extends; eassumption.
      * (* regmap_setres *)
        split; intros.
        -- apply set_res_lessdef. assumption.
           exact LESSDEF_REGS.
        -- pose proof (max_reg_function_def f pc _ r H) as REMAIN.
           destruct REGS as (REGS1 & REGS2).
           destruct res; cbn in *.
           { destruct (peq x r).
              - subst. unfold Ple in *.
                pose proof (REMAIN (eq_refl (Some r))). lia.
              - rewrite Regmap.gso by congruence.
                apply REGS2; assumption.
           }
           all: apply REGS2; assumption.

      * eapply match_stacks_external_call with (m1:=m) (m1':=m'); eassumption.
        
  (* Icond *)
  - rename H0 into COND.
    assert (ARGS_LESSDEF : Val.lessdef_list (rs ## args) (rs' ## args)).
    { apply match_regs_args with (f := f). assumption.
      intros r IN. eapply max_reg_function_use. eassumption.
      cbn. assumption. }
    exists (State stk' (transf_function f) (Vptr sp0 Ptrofs.zero) (if b then ifso else ifnot) rs' m'). split.
    + apply plus_one.
      apply exec_Icond with (cond:=cond) (args:=args) (ifso:=ifso) (ifnot:=ifnot) (predb:=predb) (b:=b).
      TRANSF.
      apply (eval_condition_lessdef _ ARGS_LESSDEF MEM COND).
      reflexivity.
    + constructor; trivial.
      
  (* Ijumptable *)
  - eexists. split.
    + apply plus_one.
      apply exec_Ijumptable with (arg:=arg) (tbl:=tbl) (n:=n).
      TRANSF.
      assert (arg <= max_reg_function f)%positive as REG_OK.
      { eapply max_reg_function_use. eassumption. constructor. reflexivity. }
      destruct REGS as (REGS1 & REGS2).
      pose proof (REGS1 arg REG_OK) as LESSDEF.
      rewrite H0 in LESSDEF.
      inv LESSDEF. reflexivity.
      eassumption.
    + constructor; trivial.

  (* Ireturn *)
  - rename m' into m2. rename m'0 into m'. rename stk' into s'.
    rename H0 into FREE.
    destruct (free_with_canary _ _ _ _ _ FREE MEM OUT_OF_BOUNDS CANARY_PERM) as (m2' & FREE' & EXTENDS2).
    assert (match_states (State s f (Vptr stk Ptrofs.zero) pc rs m)
                         (State s' (transf_function f) (Vptr stk Ptrofs.zero) pc rs' m')) as MS.
    { constructor; assumption. }
    destruct (has_check_sequence_exec s s' f _ pc rs rs' m m' _ H MS) as (pc' & rs2' & STAR & REGS' & CODE).
    eexists. split.
    + eapply plus_right with (t1:=E0) (t2:=E0). 3: reflexivity.
      exact STAR.
      apply exec_Ireturn with (or := or).
      congruence.
      eassumption.
    + constructor; trivial.
      * apply match_stacks_advance with (bound := stk).
        { erewrite Mem.nextblock_free by eassumption.
          unfold Mem.valid_block, Ple, Plt in *. lia. }
        eapply match_stacks_free; try eassumption.
        apply Ple_refl.
      * destruct or; cbn. 2: constructor.
        destruct REGS' as (REGS1 & REGS2).
        apply (REGS1 r).
        eapply max_reg_function_use. eassumption. constructor. reflexivity.
        
  (* internal call *)
  - rename m' into m2. rename m'0 into m'. rename stk' into s'.
    rename H into ALLOC.
    assert (LO : 0 <= 0) by lia.
    assert (HI: fn_stacksize f <= fn_stacksize (transf_function f)).
    { cbn. pose proof (extra_canary_size_nonneg f). lia. }
    destruct (Mem.alloc_extends _ _ _ _ _ _ _ _ MEM ALLOC LO HI) as (m2' & ALLOC' & EXTENDS').
    destruct (canary_needed f) eqn:NEEDED.
    + destruct (entry_sequence0 _ NEEDED) as (canary_op & CANARY_OP & OP0).
      assert (Mem.range_perm m2' stk (canary_offset f)
        (canary_offset f +
            Z.of_nat (Datatypes.length (encode_val canary_chunk (canary_val tt))))
         Cur Writable) as RANGE_PERM.
      { rewrite canary_encode_size.
        intros ofs RANGE.
        unfold transf_function in ALLOC'.
        cbn in ALLOC'.
        apply Mem.perm_implies with (p1 := Freeable). 2: constructor.
        eapply Mem.perm_alloc_2. eassumption.
        unfold extra_canary_size. rewrite NEEDED.
        unfold canary_offset in RANGE.
        pose proof (no_negative_stacksize _ NEEDED).
        pose proof (f_padding_nonneg f).
        lia.
      }
      destruct (Mem.range_perm_storebytes m2' stk (canary_offset f) (encode_val canary_chunk (canary_val tt)) RANGE_PERM) as (m2'' & STOREBYTES).
      assert (STORE' : Mem.store canary_chunk m2' stk (canary_offset f) (canary_val tt) = Some m2'').
      { apply Mem.storebytes_store. assumption.
        apply canary_offset_correct.
      }
      destruct (eval_clearcanary _ _ tge (Vptr stk Ptrofs.zero) m2'') as (v' & CLEAR).
      eexists. split.
      * eapply plus_left with (t1:=E0) (t2:=E0). 3: reflexivity.
        { constructor. eassumption. }
        eapply star_left with (t1:=E0) (t2:=E0). 3: reflexivity.
        { eapply exec_Iop.
          exact OP0.
          apply eval_getcanary. assumption.
        }
        eapply star_left with (t1:=E0) (t2:=E0). 3: reflexivity.
        { eapply exec_Istore.
          { apply entry_sequence1. assumption. }
          reflexivity. cbn.
          rewrite Ptrofs.add_zero_l.
          rewrite Ptrofs.unsigned_repr by (apply no_huge_stacksize; assumption).
          rewrite Regmap.gss. exact STORE'.
        }
        eapply star_one.
        eapply exec_Iop.
        { apply entry_sequence2. assumption. } cbn.
        exact CLEAR.
      * constructor.
        -- eapply Mem.valid_new_block. exact ALLOC.
        -- eapply canary_perm_store. 2: exact STORE'.
           intros ofs RANGE.
           cbn in ALLOC'.
           eapply Mem.perm_alloc_2. exact ALLOC'.
           assert (fn_stacksize f < 0 \/ fn_stacksize f >= 0) as ZZ by lia.
           destruct ZZ.
           { rewrite extra_canary_size_0_if_incorrect_size in RANGE by assumption.
             lia. }
           lia.
        -- intros ofs RANGE. unfold loc_out_of_bounds.
           intro PERM.
           pose proof (Mem.perm_alloc_3 _ _ _ _ _ ALLOC _ _ _ PERM).
           lia.
        -- unfold canary_present. intro TRUE.
           erewrite Mem.load_store_same. 2: exact STORE'.
           f_equal; apply load_canary_ok.
        -- unfold match_regs. split.
           ++ intros.
              repeat rewrite Regmap.gso by lia.
              rewrite params_preserved.
              apply init_regs_lessdef; assumption.
           ++ intros. apply init_regs_undef. intros r' IN.
              pose proof (max_reg_function_params f r' IN).
              mylia.
        -- eapply Mem.store_outside_extends. exact EXTENDS'.
           exact STORE'.
           intros ofs PERM RANGE.
           pose proof (Mem.perm_alloc_3 _ _ _ _ _ ALLOC _ _ _ PERM).
           unfold canary_offset in RANGE.
           pose proof (f_padding_nonneg f).
           lia.
        -- eapply match_stacks_create_frame.
           apply Ple_refl.
           { rewrite (Mem.alloc_result _ _ _ _ _ ALLOC).
             exact STACKS.
           }
           exact ALLOC.
           exact ALLOC'.
           exact MEM.
           exact EXTENDS'.
           exact STORE'.
    + eexists. split.
      * apply plus_one. apply exec_function_internal. eassumption.
      * assert (fn_entrypoint (transf_function f) = fn_entrypoint f) as ENTRYPOINT.
        { unfold transf_function. rewrite NEEDED. reflexivity. }
        rewrite ENTRYPOINT.
        apply match_regular_states; trivial.
        -- eapply Mem.valid_new_block; eassumption.
        -- unfold canary_perm. intros ofs RANGE.
           eapply Mem.perm_alloc_2. exact ALLOC'.
           cbn.
           assert (f.(fn_stacksize) < 0 \/ f.(fn_stacksize) >= 0) as ZZ by lia.
           destruct ZZ.
           { rewrite extra_canary_size_0_if_incorrect_size in RANGE by assumption.
             lia. }
           lia.
        -- unfold f_out_of_bounds. intros ofs RANGE.
           unfold loc_out_of_bounds. intro PERM.
           pose proof (Mem.perm_alloc_3 _ _ _ _ _ ALLOC _ _ _ PERM).
           lia.
        -- unfold canary_present. intro TRUE. congruence.
        -- apply match_regs_params. assumption.
           apply Forall_forall. intros.
           apply max_reg_function_params. assumption.
        -- assert (stk = Mem.nextblock m).
           { eapply Mem.alloc_result; eassumption. }
           subst stk.
           eapply match_stacks_alloc. 2,3,4: eassumption.
           apply Ple_refl.
    
  (* external call *)
  - rename m' into m2. rename m'0 into m'. rename s into stk.
    destruct (external_call_mem_extends _ _ _ _ _ H MEM ARGS) as (v' & m2' & CALL' & LESSDEF2 & EXTENDS2 & UNCHANGED).
    eexists. split.
    + apply plus_one. apply exec_function_external.
      apply external_call_symbols_preserved with (ge1:=ge).
      apply senv_preserved.
      exact CALL'.
    + constructor; trivial.
      destruct stk; inv STACKS.
      { constructor. }
      pose proof (external_call_nextblock _ _ _ _ _ _ _ H) as NEXTBLOCK.
      constructor; trivial.
      * unfold Ple, Plt in *. lia.
      * eapply canary_perm_external_call. eassumption.
        erewrite <- Mem.valid_block_extends by eassumption.
        exact VALID_SP.
        all: eassumption.
      * eapply f_out_of_bounds_external_call; eassumption.
      * eapply canary_present_external_call. eassumption.
        erewrite <- Mem.valid_block_extends by eassumption.
        exact VALID_SP.
        all: eassumption.
      * eapply match_stacks_external_call with (m1:=m) (m1':=m'); eassumption.

  (* return *)
  - inv STACKS. eexists. split.
    + apply plus_one. constructor.
    + constructor; trivial.
      apply match_regs_assign; trivial.
Qed.

Lemma transf_initial_states:
  forall st1, initial_state prog st1 -> exists st2, initial_state tprog st2 /\ match_states st1 st2.
Proof.
  intros. inv H. econstructor; split.
  - econstructor.
    + eapply (Genv.init_mem_transf TRANSL); eauto.
    + rewrite symbols_preserved. rewrite (match_program_main TRANSL). eauto.
    + eapply function_ptr_translated; eauto.
    + rewrite <- H3; apply sig_preserved.
  - constructor.
    + apply Mem.extends_refl.
    + constructor.
    + constructor.
Qed.
  
Lemma transf_final_states:
  forall st1 st2 r
         (MATCH : match_states st1 st2)
         (FINAL : final_state st1 r),
    final_state st2 r.
Proof.
  intros. inv FINAL. inv MATCH. inv STACKS. inv RES.
  constructor.
Qed.

Theorem transf_program_correct:
  forward_simulation (RTL.semantics prog) (RTL.semantics tprog).
Proof.
  eapply forward_simulation_plus.
  apply senv_preserved.
  eexact transf_initial_states.
  eexact transf_final_states.
  exact step_simulation.
Qed.

End PRESERVATION.
Generated by coq2html