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 CounterMeasures 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 canary_needed_getcanary : forall f,
    canary_needed f = true -> getcanary <> None.
Proof.
  intros * NEEDED GET.
  unfold canary_needed in NEEDED. rewrite GET in NEEDED. congruence.
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.

Definition check_insn insn :=
  match insn with
  | Ireturn _ | Itailcall _ _ _ => true
  | _ => false
  end.

Opaque CounterMeasures.transf_function.

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.

Global Hint Unfold transf_tailcall transf_return check_sequence : rtlcm.

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 sig_function_preserved:
  forall f, fn_sig (transf_function f) = fn_sig f.
Proof.
  intros. 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.

Lemma find_function_lessdef:
  forall ros rs rs' fd,
    find_function ge ros rs = Some fd ->
    (forall r, ros = inl r -> Val.lessdef rs#r rs'#r) ->
    find_function ge ros rs' = Some fd.
Proof.
  intros [] * FIND LESS; simpl in *; auto.
  specialize (LESS _ eq_refl).
  apply Genv.find_funct_inv in FIND as EQ. destruct EQ as (?&EQ); rewrite EQ in *.
  inv LESS. simpl in *.
  auto.
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_perm_alloc': forall f m1 m2 sp,
  Mem.alloc m1 0 (fn_stacksize f + extra_canary_size f) = (m2, sp) ->
  canary_perm m2 f sp.
Proof.
  intros * ALLOC.
  intros ofs RANGE.
  eapply Mem.perm_alloc_2; eauto.
  assert (fn_stacksize f < 0 \/ fn_stacksize f >= 0) as [|] by lia.
  - rewrite extra_canary_size_0_if_incorrect_size in RANGE by assumption.
    lia.
  - lia.
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 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.

Ltac take_step :=
  match goal with
  | H: _!?pc = Some (Inop _) |- step _ (State _ _ _ ?pc _ _) _ _ =>
      eapply exec_Inop; eauto
  | H: _!?pc = Some (Iop _ _ _ _) |- step _ (State _ _ _ ?pc _ _) _ _ =>
      eapply exec_Iop; eauto
  | H: _!?pc = Some (Iload _ _ _ _ _ _) |- step _ (State _ _ _ ?pc _ _) _ _ =>
      eapply exec_Iload; eauto
  | H: _!?pc = Some (Istore _ _ _ _ _) |- step _ (State _ _ _ ?pc _ _) _ _ =>
      eapply exec_Istore; eauto
  | H: _!?pc = Some (Icond _ _ _ _ _) |- step _ (State _ _ _ ?pc _ _) _ _ =>
      eapply exec_Icond; eauto
  | H: _!?pc = Some (Ijumptable _ _) |- step _ (State _ _ _ ?pc _ _) _ _ =>
      eapply exec_Ijumptable; eauto
  | H: _!?pc = Some (Icall _ _ _ _ _) |- step _ (State _ _ _ ?pc _ _) _ _ =>
      eapply exec_Icall with (fd:=transf_fundef _); eauto
  | H: _!?pc = Some (Itailcall _ _ _) |- step _ (State _ _ _ ?pc _ _) _ _ =>
      eapply exec_Itailcall with (fd:=transf_fundef _); eauto
  | H: _!?pc = Some (Ireturn _) |- step _ (State _ _ _ ?pc _ _) _ _ =>
      eapply exec_Ireturn; eauto
  | H: _!?pc = Some (Iassert _ _ _) |- step _ (State _ _ _ ?pc _ _) _ _ =>
      eapply exec_Iassert; eauto
  | |- step _ (Callstate _ _ _ _) _ _ => econstructor; eauto
  | |- step _ _ _ (Returnstate _ _ _) => econstructor; eauto
  end.

Ltac transf f :=
  assert (transf_function f = transf_function f) as TR by reflexivity;
  unfold transf_function in TR at 2;
  destruct (canary_needed f) eqn:CANARY;
  [destruct CounterMeasures.transf_function eqn:TR1;
   eapply transf_function_correct in TR1; eauto; simpl in *; inv_seq|].

Ltac one_step TR :=
  do 2 esplit;
  [apply plus_one; rewrite TR; try take_step|try rewrite <-TR].

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.

  Ltac subgoals :=
    simpl;
    match goal with
    | |- step _ _ _ _ => take_step; simpl; eauto; simpl
    | |- has_loaded _ _ _ _ _ _ _ _ _ => econstructor; simpl; [eauto; try reflexivity|simpl]
    | |- context [Ptrofs.add Ptrofs.zero _] => rewrite Ptrofs.add_zero_l
    | |- context [Ptrofs.unsigned (Ptrofs.repr (canary_offset _))] =>
        rewrite Ptrofs.unsigned_repr by (apply no_huge_stacksize; assumption)
    | |- find_function _ _ _ = Some (transf_fundef _) =>
        eapply find_function_translated, find_function_lessdef; eauto
    | MATCH: match_regs ?f _ _ |- forall r, _ -> _ =>
        intros; subst;
        assert (r <= max_reg_function f)%positive by repeat subgoals
    | |- (_ <= max_reg_function _)%positive =>
        eapply max_reg_function_use; eauto; simpl; auto
    | MATCH: match_regs _ _ _ |- Val.lessdef _ _ =>
        eapply MATCH; eauto
    | |- funsig (transf_fundef _) = funsig _ => apply sig_preserved
    | |- _ => rewrite eval_negate_condition
    | |- _ => rewrite cmp_canary_ok
    | |- _ => rewrite Int.eq_true
    | |- _ => rewrite Int64.eq_true
    | |- _ => rewrite Regmap.gso; [|extlia]
    | |- _ => rewrite Regmap.gss
    | |- match_states _ _ => econstructor; eauto
    | |- match_stacks _ _ _ _ _ =>
        eauto using match_stacks_free, match_stacks_advance, Ple_refl
    | MATCH: match_regs ?f _ _ |- Val.lessdef_list _ _ => apply match_regs_args with (f:=f)
    | ros: _ + _ |- _ => now (destruct ros; simpl; auto)
    | |- match_regs _ _ _ => apply match_regs_above; [|extlia]; auto
    | |- _ => now eauto
    end.

  (* Inop *)
  - transf f; one_step TR; econstructor; eauto.

  (* 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).
    transf f; one_step TR.
    1,3:rewrite eval_operation_preserved with (ge1 := ge) by apply symbols_preserved; eauto.
    1,2:econstructor; eauto.
    1,2:eapply match_regs_assign; eauto; eapply max_reg_function_def; eauto.

  (* 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).
      transf f; one_step TR.
      1,3:(eapply has_loaded_normal; eauto;
           rewrite eval_addressing_preserved with (ge1 := ge) by apply symbols_preserved; eauto).
      1,2:econstructor; eauto.
      1,2:eapply match_regs_assign; eauto; eapply max_reg_function_def; eauto.

    + 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'.
        1,2:transf f; one_step TR.
        1,3:eapply has_loaded_normal; eauto.
        3,5:eapply has_loaded_default; eauto; intros; congruence.
        1-4:econstructor; eauto.
        1-4:eapply match_regs_assign; eauto; eapply max_reg_function_def; eauto.

      * transf f; one_step TR.
        1,3:eapply has_loaded_default; eauto; intros; congruence.
        1,2:econstructor; eauto.
        1,2:eapply match_regs_assign; eauto; eapply max_reg_function_def; eauto.

  (* 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').
    transf f; one_step TR.
    all:try (rewrite eval_addressing_preserved with (ge1 := ge) by apply symbols_preserved; eauto).
    1,2:econstructor; eauto.
    1,6:eapply mem_storev_valid_block_1; eassumption.
    1,5:eapply canary_perm_storev; eassumption.
    1,4:eapply f_out_of_bounds_storev; eassumption.
    1,3:eapply canary_present_storev; [exact MEM|exact ADDR_LESSDEF| | | |]; eauto.
    1,2:eapply match_stacks_storev; [exact MEM|exact ADDR_LESSDEF| | |]; eauto.

  (* Icall *)
  - assert (ARGS_LESSDEF : Val.lessdef_list (rs ## args) (rs' ## args)).
    { apply match_regs_args with (f := f); auto.
      intros r IN. eapply max_reg_function_use; eauto.
      destruct ros; simpl; auto. }
    transf f; one_step TR.
    all:repeat subgoals.
    1,2:econstructor; eauto; eapply max_reg_function_def; eauto.

  (* 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. }
    assert ((stk <= Mem.nextblock m2)%positive) as LE.
    { erewrite Mem.nextblock_free by eassumption.
      unfold Mem.valid_block in *. extlia. }
    transf f.
    + (* with canary *)
      try now (exfalso; eapply canary_needed_getcanary in CANARY; eauto).
      all:(do 2 esplit; plus_step 3; try apply plus_one).
      all:try rewrite TR; simpl; eauto.
      all:repeat subgoals.
    + (* without canary *)
      one_step TR; repeat subgoals.

  (* 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).
    assert (canary_perm m2' f sp0) as PERM.
    { destruct UNCHANGED.
      unfold canary_perm in *.
      intros ofs RANGE.
      apply unchanged_on_perm; auto using CANARY_PERM.
      - apply OUT_OF_BOUNDS. lia.
      - erewrite <- Mem.valid_block_extends; eassumption. }
    assert (f_out_of_bounds m2 f sp0) as OUT.
    { 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; eauto. }
    assert (canary_present m2' f sp0) as PRESENT.
    { eapply canary_present_external_call with (m1:=m); eauto.
      erewrite <- Mem.valid_block_extends; eassumption. }
    assert (Mem.valid_block m2 sp0) as VALID.
    { pose proof (external_call_nextblock _ _ _ _ _ _ _ CALL).
      unfold Mem.valid_block in *. extlia. }
    assert (match_regs f (regmap_setres res vres rs) (regmap_setres res vres' rs')) as REGS'.
    { split; intros.
      - apply set_res_lessdef; auto.
      - pose proof (max_reg_function_def f pc _ r H) as REMAIN.
        destruct REGS as (REGS1 & REGS2).
        destruct res; cbn in *; auto.
        destruct (peq x r).
        + subst. specialize (REMAIN eq_refl). extlia.
        + rewrite Regmap.gso by congruence. auto. }

    transf f; one_step TR.
    1,3:eapply exec_Ibuiltin with (m':=m2'); eauto using sig_preserved.
    1,3:eapply eval_builtin_args_preserved with (ge1:=ge); eauto using symbols_preserved.
    1,2:eapply external_call_symbols_preserved with (ge1:=ge); eauto using senv_preserved.
    1,2:rewrite <-TR; econstructor; eauto using match_stacks_external_call.

  (* 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; eauto. }
    transf f; [|one_step TR].
    exists (State stk' (transf_function f) (Vptr sp0 Ptrofs.zero) (if b then ifso else ifnot) rs' m').
    split; [eapply plus_two; try rewrite TR; try take_step; simpl; eauto|].
    1,4:eapply eval_condition_lessdef; eauto.
    destruct b; take_step.
    1,2:econstructor; eauto.

  (* Ijumptable *)
  - transf f; (one_step TR; [|econstructor; eauto]).
    1,2:(assert (arg <= max_reg_function f)%positive as REG_OK
            by (eapply max_reg_function_use; eauto; constructor; auto);
         destruct REGS as (REGS1 & REGS2);
         pose proof (REGS1 arg REG_OK) as LESSDEF;
         rewrite H0 in LESSDEF;
         inv LESSDEF; auto).

  (* 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. }
    assert ((stk <= Mem.nextblock m2)%positive) as LE.
    { erewrite Mem.nextblock_free by eassumption.
      unfold Mem.valid_block in *. extlia. }
    transf f.
    + (* with canary *)
      try now (exfalso; eapply canary_needed_getcanary in CANARY; eauto).
      all:(do 2 esplit; plus_step 3; try apply plus_one).
      all:try rewrite TR; simpl; eauto.
      all:repeat subgoals.
      all:destruct or; [|now auto]; simpl.
      all:eapply max_reg_function_use in H as ?LE; simpl; eauto.
      all:repeat subgoals.
    + (* without canary *)
      one_step TR.
      econstructor; eauto.
      * eapply match_stacks_free, match_stacks_advance with (bound := stk) in STACKS; eauto using Ple_refl.
      * destruct or; auto. simpl.
        eapply REGS, max_reg_function_use; eauto. simpl; auto.

  (* Iassert *)
  - eapply eval_assert_args_preserved with (ge2:=tge),
        eval_assert_args_lessdef with (rs2:=rs') in H0 as (?&?&?); eauto using symbols_preserved.
    2:{ intros. eapply REGS. eapply max_reg_function_use; eauto. }
    transf f; one_step TR; eauto. 1,3:econstructor; eauto.
    eapply eval_condition_lessdef; eauto.

  (* internal call *)
  - rename m' into m2. rename m'0 into m'. rename stk' into s'.
    rename H0 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').

    assert (TR : transf_function f = transf_function f) by reflexivity.
    unfold transf_function in TR at 2; destruct (canary_needed f) eqn:CANARY.
    + destruct CounterMeasures.transf_function eqn:TR1.
      eapply transf_function_entry in TR1 as (?&SPEC); eauto. inv_seq.

      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 CANARY.
        unfold canary_offset in RANGE.
        pose proof (no_negative_stacksize _ CANARY).
        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).
      assert (OUT': f_out_of_bounds m2 f stk).
      { intros ?? PERM. eapply Mem.perm_alloc_3 in PERM; eauto. extlia. }
      assert (PRES': canary_present m2'' f stk).
      { intros ?. erewrite Mem.load_store_same, load_canary_ok; eauto. }
      assert (EXT': Mem.extends m2 m2'').
      { eapply Mem.store_outside_extends; eauto.
        intros ? PERM RANGE.
        eapply Mem.perm_alloc_3 in PERM; eauto.
        unfold canary_offset in RANGE.
        pose proof (f_padding_nonneg f).
        lia. }
      assert (STACKS': match_stacks stk m2 m2'' s s').
      { eapply match_stacks_create_frame; eauto using Ple_refl.
        rewrite (Mem.alloc_result _ _ _ _ _ ALLOC); auto. }
      assert (REGS': match_regs f (init_regs args (fn_params f)) (init_regs args' (fn_params (transf_function f)))).
      { split; intros.
        - apply init_regs_lessdef; assumption.
        - intros. apply init_regs_undef. intros r' IN.
          pose proof (max_reg_function_params f r' IN).
          mylia. }

      try now (exfalso; eapply canary_needed_getcanary in CANARY; eauto).
      all:(do 2 esplit; plus_step 3; try apply plus_one).
      all:rewrite ? TR; repeat subgoals; eauto.
      all: try (eapply Val.has_argtype_list_lessdef; eassumption).
      all:(setoid_rewrite <-TR; repeat subgoals;
           eauto using Mem.valid_new_block, canary_perm_store, canary_perm_alloc').
    + do 2 esplit; eauto.
      * apply plus_one. apply exec_function_internal.
        { eapply Val.has_argtype_list_lessdef; eassumption. }
        eassumption.
      * assert (fn_entrypoint (transf_function f) = fn_entrypoint f) as ENTRYPOINT.
        { unfold transf_function. rewrite CANARY. 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