Module CFCproof

Require Import Coqlib List Maps Integers Errors.
Import ListNotations.
Require Import AST Linking Smallstep.
Require Import Globalenvs Values.
Require Import Op Registers Memory RTL.
Require Import CounterMeasures CFC.

Ltac monadInv := match goal with H: _ |- _ => Errors.monadInv H end.

Definition match_prog (prog tprog: program) :=
  match_program (fun cunit f tf => transf_fundef f = OK tf) eq prog tprog.

Lemma transf_program_match: forall p tp,
  transf_program p = OK tp ->
  match_prog p tp.

Proof.

intros. eapply match_transform_partial_program; eauto.
Qed.

Global Hint Unfold
  transf_join
  transf_nop transf_op
  transf_load transf_store
  transf_call transf_builtin
  transf_cond set_xor_gsr add_test
  transf_return : rtlcm.

Section compute_sigs.

  Lemma compute_sigs_correct f : forall sigs joins pc i,
      compute_sigs f = OK (sigs, joins) ->
      (fn_code f)!pc = Some i ->
      match i with
      | Inop pc1
      | Iop _ _ _ pc1
      | Iload _ _ _ _ _ pc1
      | Istore _ _ _ _ pc1
      | Icall _ _ _ _ pc1
      | Ibuiltin _ _ _ pc1
      | Iassert _ _ pc1 =>
          if is_join joins pc1 then True
          else sigs!pc1 = sigs!pc
      | Ijumptable _ pcs => False
      | Icond _ _ _ _ _ | Itailcall _ _ _ | Ireturn _ => True
      end.

Proof.

    intros * SIGS FIND. unfold compute_sigs, correct_sigs in *.
    destruct ext_compute_sigs. repeat monadInv. destruct x.
    revert EQ FIND.
    eapply PTree_Properties.fold_rec.
    - intros * EQ. rewrite EQ; auto.
    - intros * _ EMPTY.
      rewrite PTree.gempty in EMPTY. congruence.
    - intros * NONE FIND IND MON SET.
      repeat monadInv. destruct x; subst.
      rewrite PTree.gsspec in SET. destruct (peq _ _); [inv SET|].
      + destruct i; cases_eq; repeat monadInv; auto.
      + apply IND; auto.
  Qed.

End compute_sigs.

Section CFC.

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

Static properties

Lemma sig_preserved: forall f tf,
transf_fundef f = OK tf ->
funsig tf = funsig f.

Proof.

intros [] * TR; simpl in *; repeat monadInv; auto.
Qed.

Lemma symbols_preserved:
forall id,
Genv.find_symbol tge id = Genv.find_symbol ge id.

Proof.

apply (Genv.find_symbol_transf_partial TRANSL).
Qed.

Lemma senv_preserved:
Senv.equiv ge tge.

Proof.

apply (Genv.senv_transf_partial TRANSL).
Qed.

Lemma functions_translated:
  forall v f,
  Genv.find_funct ge v = Some f ->
  exists tf, Genv.find_funct tge v = Some tf /\ transf_fundef f = OK tf.

Proof.

apply (Genv.find_funct_transf_partial TRANSL).
Qed.

Lemma function_ptr_translated:
  forall v f,
  Genv.find_funct_ptr ge v = Some f ->
  exists tf, Genv.find_funct_ptr tge v = Some tf /\ transf_fundef f = OK tf.

Proof.

apply (Genv.find_funct_ptr_transf_partial TRANSL).
Qed.

Lemma find_function_translated:
  forall ros rs fd,
  find_function ge ros rs = Some fd ->
  exists tf, find_function tge ros rs = Some tf /\ transf_fundef fd = OK tf.

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 gsr f := Pos.succ (max_reg_function f).
Definition rts f := Pos.succ (Pos.succ (max_reg_function f)).

Ltac extlia := unfold gsr, rts in *; Coqlib.extlia.

Lemma transf_function_entry :
  forall f tf,
    do_protect f = true ->
    transf_function f = OK tf ->
    exists sigs joins,
      compute_sigs f = OK (sigs, joins)
      /\ (fn_code tf)!(fn_entrypoint tf) = Some (Iop (Ointconst (get_sig sigs (fn_entrypoint f))) [] (gsr f) (fn_entrypoint f)).

Proof.

  intros * FIND NOTCOND; simpl. unfold transf_function in *. repeat pMonadInv.
  rewrite FIND in MON. Errors.monadInv MON.
  do 3 esplit; eauto.
  destruct (CounterMeasures.transf_function) eqn:TR; simpl.
  eapply transf_function_entry in TR; eauto; inv_seq; eauto.
Qed.

Lemma transf_code_correct:
  forall f tf pc i,
    do_protect f = true ->
    f.(fn_code)!pc = Some i ->
    transf_function f = OK tf ->
    exists abort sigs joins e seq cont,
      compute_sigs f = OK (sigs, joins)
      /\ transf_instr
          (transf_nop sigs joins (gsr f)) (transf_op sigs joins (gsr f))
          (transf_load sigs joins (gsr f)) (transf_store sigs joins (gsr f))
          (transf_call sigs joins (gsr f)) transf_tailcall_default (transf_builtin sigs joins (gsr f))
          (transf_cond sigs (gsr f) (rts f))
          transf_jumptable_default (transf_return sigs (gsr f))
          pc i = existT _ e (seq, cont)
      /\ spec_seq abort (fn_code tf) pc seq cont.

Proof.

  intros * FIND TR NOTCOND. repeat monadInv.
  rewrite FIND in EQ; repeat monadInv.
  destruct CounterMeasures.transf_function eqn:?TR; simpl.
  eapply transf_function_correct in TR; eauto; simpl in TR; destruct_conjs; eauto.
  destruct transf_instr as (?&?&?) eqn:?TR. destruct TR as (?&?&?).
  repeat (esplit; eauto).
Qed.

Simulation invariant

Definition match_regs (fn : function) pc (rs rs' : regset) :=
    (forall r, (r <= RTL.max_reg_function fn)%positive -> rs'#r = rs#r)
  /\ (do_protect fn = true ->
     exists sigs joins, compute_sigs fn = OK (sigs, joins)
                   /\ rs'#(gsr fn) = Vint (get_sig sigs pc)).

Inductive match_stacks: list RTL.stackframe -> list RTL.stackframe -> Prop :=
| match_frames_nil: match_stacks nil nil
| match_frames_cons: forall tail tail' res f tf sp pc0 pc pc' rs rs'
    (REG_OK : (res <= max_reg_function f)%positive)
    (TR: transf_function f = OK tf)
    (PC1: do_protect f = false -> pc' = pc)
    (REGS: match_regs f pc0 rs rs')
    (PC2: do_protect f = true ->
          exists joins sigs,
            compute_sigs f = OK (sigs, joins)
            /\ (if is_join joins pc
               then (fn_code tf)!pc' = Some (Iop (Oxorimm (Int.xor (get_sig sigs pc0) (get_sig sigs pc))) [gsr f] (gsr f) pc)
               else pc' = pc /\ sigs!pc0 = sigs!pc))
    (TAIL: match_stacks tail tail'),
  match_stacks
    ((Stackframe res f sp pc rs) :: tail)
    ((Stackframe res tf sp pc' rs') :: tail').

Inductive match_states: RTL.state -> RTL.state -> Prop :=
| match_regular_states: forall stk stk' f tf sp pc rs rs' m
        (STACKS: match_stacks stk stk')
        (TF: transf_function f = OK tf)
        (REGS : match_regs f pc rs rs'),
      match_states (State stk f sp pc rs m)
                   (State stk' tf sp pc rs' m)
  | match_callstates: forall stk stk' f tf args m
      (STACKS: match_stacks stk stk')
      (TF: transf_fundef f = OK tf),
      match_states (Callstate stk f args m)
                   (Callstate stk' tf args m)
  | match_returnstates: forall stk stk' v m
    (STACKS: match_stacks stk stk'),
      match_states (Returnstate stk v m)
                   (Returnstate stk' v m).

Initial state

Lemma transf_initial_states:
forall st1, initial_state prog st1 -> exists st2, initial_state tprog st2 /\ match_states st1 st2.

Proof.

  intros. inv H.
  edestruct function_ptr_translated as (?&FIND'&TR); eauto.
  econstructor; split.
  - econstructor; eauto.
    + eapply (Genv.init_mem_transf_partial TRANSL); eauto.
    + rewrite symbols_preserved. setoid_rewrite (match_program_main TRANSL). eauto.
    + erewrite sig_preserved; eauto.
  - repeat (econstructor; eauto).
Qed.

Final state

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.
constructor.
Qed.

Step simulation

Lemma match_regs_update_pc1 :
  forall f pc pc' rs rs',
    do_protect f = false ->
    match_regs f pc rs rs' ->
    match_regs f pc' rs rs'.

Proof.

intros * EQ (?&M2).
split; auto. intros HARD. congruence.
Qed.

Lemma match_regs_update_pc2 :
  forall f sigs joins pc pc' rs rs',
    compute_sigs f = OK (sigs, joins) ->
    sigs!pc' = sigs!pc ->
    match_regs f pc rs rs' ->
    match_regs f pc' rs rs'.

Proof.

  intros * SIGS EQ (?&M2).
  split; auto. intros HARD.
  destruct M2 as (?&?&SIGS'&?); auto.
  rewrite SIGS in SIGS'; inv SIGS'.
  repeat (esplit; eauto). unfold get_sig. now rewrite EQ.
Qed.

Lemma match_regs_assign1 :
  forall f pc rs rs' res v,
    do_protect f = false ->
    match_regs f pc rs rs' ->
    match_regs f pc (rs # res <- v) (rs' # res <- v).

Proof.

  unfold match_regs. intros * ? (REGS1 & REGS2).
  split; intros; [|congruence].
  destruct (peq r res).
  - subst r. repeat rewrite Regmap.gss. reflexivity.
  - repeat rewrite Regmap.gso by congruence.
    auto.
Qed.

Lemma match_regs_assign2 :
  forall f pc rs rs' res v
         (RES_OK : (res <= max_reg_function f)%positive)
         (MATCH_REGS : match_regs f pc rs rs'),
    match_regs f pc (rs # res <- v) (rs' # res <- v).

Proof.

  unfold match_regs. intros * ? (REGS1 & REGS2).
  split; intros.
  - destruct (peq r res).
    { subst r. repeat rewrite Regmap.gss. reflexivity. }
    repeat rewrite Regmap.gso by congruence.
    auto.
  - unfold gsr. rewrite Regmap.gso by lia. auto.
Qed.

Lemma match_regs_assign_gsr : forall f sigs joins pc pc' rs rs',
    compute_sigs f = OK (sigs, joins) ->
    match_regs f pc rs rs' ->
    match_regs f pc' rs
      rs' # (gsr f) <- (Val.xor rs' # (gsr f) (Vint (Int.xor (get_sig sigs pc) (get_sig sigs pc')))).

Proof.

  intros * SIGS (REGS1&REGS2). split.
  - intros. rewrite Regmap.gso; eauto.
    unfold gsr. lia.
  - intros HARD. edestruct REGS2 as (?&?&SIGS'&GSR); eauto.
    rewrite SIGS' in SIGS; inv SIGS.
    repeat (esplit; eauto).
    rewrite Regmap.gss, GSR. simpl.
    now rewrite <-Int.xor_assoc, Int.xor_idem, Int.xor_zero_l.
Qed.

Lemma eval_builtin_arg_match : forall rs rs' sp m a v,
    (forall r, In r (params_of_builtin_arg a) -> rs' # r = rs # r) ->
    Events.eval_builtin_arg ge (fun r => rs # r) sp m a v ->
    Events.eval_builtin_arg ge (fun r => rs' # r) sp m a v.

Proof.

  induction a; intros * INCL EVAL; inv EVAL; try econstructor; eauto.
  1:{ replace (rs # x) with (rs' # x); [econstructor|].
      apply INCL; simpl; auto. }
  all:try eapply IHa1; try eapply IHa2; eauto.
  all:intros; apply INCL; simpl; auto with datatypes.
Qed.

Fact eval_builtin_args_BA : forall ge rs sp m args,
Events.eval_builtin_args ge (fun x => rs # x) sp m
(map (@BA _) args) (rs ## args).

Proof.

induction args; repeat constructor; auto.
Qed.

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 MS.
  assert (TF':=TF).
  unfold transf_function in TF'; repeat pMonadInv.
  destruct (do_protect f) eqn:PROT; simpl in *; repeat monadInv.

  Local Ltac imply :=
    match goal with
    | H:match_regs _ _ _ _ |- _ => destruct H as (?REGS1&?REGS2)
    | |- eval_operation tge _ _ _ _ = _ =>
        erewrite eval_operation_preserved; [|now eauto using symbols_preserved]
    | |- eval_addressing tge _ _ _ = _ =>
        erewrite eval_addressing_preserved; [|now eauto using symbols_preserved]
    | |- _ = _ => apply map_ext_in; intros
    | H: forall a, _ -> _ # a = _ # a |- _ # _ = _ # _ => rewrite H; [reflexivity|]
    | |- _ <= max_reg_function _ => eapply max_reg_function_use; [now eauto|simpl; eauto]
    | H: context [?rs1 # ?arg] |- context [?rs2 # _] =>
        replace (rs2 # arg) with (rs1 # arg); [now eauto|auto]
    | H: context [?rs1 ## ?args] |- context [?rs2 ## _] =>
        replace (rs2 ## args) with (rs1 ## args); [now eauto|auto]
    end.

    Local Ltac one_step CONS :=
      do 2 esplit;
      [eapply plus_one, CONS; eauto
      |econstructor; eauto using match_regs_update_pc1, match_regs_assign1].

    Local Ltac two_step CONS1 CONS2 :=
      do 2 esplit;
      [eapply plus_two; eauto; try rewrite Events.E0_right; eauto;
       [eapply CONS1|eapply CONS2]; eauto; simpl; eauto
      |econstructor; eauto].

  -{ (* regular state in protected function *)
      destruct CounterMeasures.transf_function eqn:TR; clear TR.
      inv STEP.
      all:(eapply transf_code_correct in TF as TR; eauto; simpl in *; inv_seq).
      all:(rewrite EQ in H; inv H).
      all:(eapply compute_sigs_correct in EQ as SIGS; eauto; simpl in SIGS).

      - (* Inop *)
        destruct is_join; inv_seq.
        + two_step exec_Inop exec_Iop; simpl; eauto.
          eapply match_regs_assign_gsr; eauto.
        + one_step exec_Inop.
          eapply match_regs_update_pc2; eauto.

      - (* Iop *)
        assert (eval_operation tge sp op rs' ## args m = Some v) as OP by repeat imply.
        destruct is_join; inv_seq.
        + two_step exec_Iop exec_Iop.
          eapply match_regs_assign_gsr, match_regs_assign2; eauto.
          eapply max_reg_function_def; eauto.
        + one_step exec_Iop.
          eapply match_regs_update_pc2, match_regs_assign2; eauto.
          eapply max_reg_function_def; eauto.

      - (* Iload *)
        assert (eval_addressing tge sp addr rs' ## args = eval_addressing ge sp addr rs ## args) as ADDR.
        { repeat imply.
          replace (rs' ## args) with (rs ## args); eauto.
          repeat imply. }
        assert (has_loaded tge sp rs' m chunk addr args v trap) as LOADED.
        { inv H8; [eapply has_loaded_normal|eapply has_loaded_default]; eauto; intros.
          - congruence.
          - eapply LOAD. congruence. }

       destruct is_join; inv_seq.
        + two_step exec_Iload exec_Iop.
          eapply match_regs_assign_gsr, match_regs_assign2; eauto.
          eapply max_reg_function_def; eauto.
        + one_step exec_Iload.
          eapply match_regs_update_pc2, match_regs_assign2; eauto.
          eapply max_reg_function_def; eauto.

      - (* Istore *)
       destruct is_join; inv_seq.
        + two_step exec_Istore exec_Iop. 1,2:repeat imply.
          eapply match_regs_assign_gsr; eauto.
        + one_step exec_Istore. 1,2:repeat imply.
          eapply match_regs_update_pc2; eauto.

      - (* Icall *)
        edestruct find_function_translated as (tfd&?&?); eauto.
        destruct is_join eqn:J; inv_seq.
        1,2:do 2 esplit; [eapply plus_one, exec_Icall with (fd:=tfd); eauto|].
        1,4:destruct ros; simpl in *; auto; repeat imply.
        1,3:erewrite sig_preserved; eauto.
        1,2:replace (rs' ## args) with (rs ## args) by (repeat imply; destruct ros; simpl; auto).
        1,2:do 2 (econstructor; eauto).
        1,4:eapply max_reg_function_def; eauto.
        1:intros; congruence.
        1,2:intros; repeat (esplit; eauto); rewrite J; eauto.

      - (* Itailcall *)
        edestruct find_function_translated as (tfd&?&?); eauto.
        do 2 esplit; [eapply plus_one, exec_Itailcall with (fd:=tfd); eauto|].
        + destruct ros; simpl in *; auto. repeat imply.
        + erewrite sig_preserved; eauto.
        + replace (rs' ## args) with (rs ## args).
          2:{ repeat imply. destruct ros; simpl; auto. }
          do 2 (econstructor; eauto using match_regs_update_pc1).

      - (* Ibuiltin *)
        assert (Events.eval_builtin_args tge (fun r : positive => rs' # r) sp m args vargs) as ARGS.
        { eapply Events.eval_builtin_args_preserved; eauto using symbols_preserved.
          eapply list_forall2_imply; eauto; intros.
          eapply eval_builtin_arg_match; [|eauto]. intros.
          repeat imply. eauto using params_of_builtin_args_In. }
        assert (Events.external_call ef tge vargs m t vres m') as EXTCALL.
        { eapply Events.external_call_symbols_preserved; eauto using senv_preserved. }
        assert (match_regs f pc (regmap_setres res vres rs) (regmap_setres res vres rs')) as MATCH.
        { eapply match_regs_update_pc2 with (pc:=pc); eauto.
          destruct res; simpl; auto.
          eapply match_regs_assign2; auto. eapply max_reg_function_def; eauto. }
        destruct is_join; inv_seq.
        + two_step exec_Ibuiltin exec_Iop.
          eapply match_regs_assign_gsr; eauto.
        + one_step exec_Ibuiltin.
          eapply match_regs_update_pc2; eauto.

      - (* Icond *)
        assert (forall r, In r args -> r <> rts f) as NORTS.
        { intros.
          eapply max_reg_function_use in H7; eauto.
          extlia. }
        assert (rs' ## args = rs ## args) as EQARGS by repeat imply.
        destruct REGS as (REGS1 & REGS2). specialize (REGS2 PROT) as (?&?&SIGS'&GSR).
        rewrite EQ in SIGS'; inv SIGS'.

        do 2 esplit.
        + plus_step 7; try apply plus_one.
          * (* Assertion *)
            eapply exec_Iassert; eauto.
            -- repeat (econstructor; eauto).
            -- simpl. rewrite GSR. simpl. now rewrite Int.eq_true.
          * (* Duplicated condition *)
            eapply exec_Icond; eauto.
            rewrite EQARGS; eauto.
          * (* Set rts *)
            instantiate (1:=State _ _ _ _ (if b then _ else _) _).
            destruct b; eapply exec_Iop; eauto; simpl; eauto.
          * (* Observe condition *)
            eapply exec_Ibuiltin; eauto; [|constructor].
            eapply eval_builtin_args_BA.
          * (* Actual condition *)
            simpl. instantiate (1:=if b then _ else _).
            destruct b; eapply exec_Icond; eauto.
            1,2:rewrite regs_gsso, EQARGS; eauto.
            1,2:intros IN; specialize (NORTS _ IN); congruence.
          * (* Set gsr *)
            instantiate (1:=if b then _ else _).
            destruct b; eapply exec_Iop; eauto; simpl.
            1,2:rewrite ? MATCHR, ? Regmap.gss, Regmap.gso; try extlia; rewrite GSR; simpl.
            1,2:rewrite <-Int.xor_assoc, Int.xor_idem, Int.xor_zero_l; eauto.
          * (* Test *)
            instantiate (1:=if b then _ else _).
            destruct b; eapply exec_Icond; eauto; simpl.
            1,2:rewrite Regmap.gss; simpl.
            1,2:rewrite Int.eq_true; reflexivity.
          * (* Observe gsr *)
            instantiate (1:=if b then _ else _).
            destruct b; (eapply exec_Ibuiltin; eauto; repeat econstructor).
        + simpl. destruct b; econstructor; eauto.
          1,2:split; eauto.
          1,3:intros * Lt; rewrite ? Regmap.gso, ? MATCHR, ? Regmap.gso; eauto; try extlia.
          1,2:intros; repeat (esplit; eauto); rewrite Regmap.gss; auto.

      - (* Ijumptable *) inv SIGS.

      - (* Ireturn *)
        replace (regmap_optget or Vundef rs) with (regmap_optget or Vundef rs').
         2:{ destruct or; simpl; auto.
             destruct REGS as (REGS1&_). rewrite REGS1; auto.
             eapply max_reg_function_use; eauto; simpl; auto. }
        destruct Compopts.intra_cfc_return; inv_seq.
        + destruct REGS as (_&(?&?&SIGS'&GSR)); auto.
          rewrite EQ in SIGS'; inv SIGS'.
          do 2 esplit; [eapply plus_three|econstructor; eauto].
          * eapply exec_Iassert; eauto; simpl.
            -- repeat constructor.
            -- rewrite GSR. simpl. now rewrite Int.eq_true.
          * eapply exec_Icond with (b:=false); eauto. simpl.
            rewrite GSR. simpl. now rewrite Int.eq_true.
          * eapply exec_Ireturn; eauto.
          * reflexivity.
        + do 2 esplit; [|econstructor; eauto].
          eapply plus_one, exec_Ireturn; auto.

      - (* Iassert *)
        destruct is_join; inv_seq.
        + two_step exec_Inop exec_Iop; simpl; eauto.
          eapply match_regs_assign_gsr; eauto.
        + one_step exec_Inop.
          eapply match_regs_update_pc2; eauto.
    }

  - (* regular state in unprotected function *)
    inv STEP.
    + one_step exec_Inop.
    + one_step exec_Iop; repeat imply.
    + one_step exec_Iload; repeat imply.
      assert (eval_addressing tge sp addr rs' ## args = eval_addressing ge sp addr rs ## args) as ADDR.
      { repeat imply.
        replace (rs' ## args) with (rs ## args); eauto.
        repeat imply. }
      inv H8.
      * eapply has_loaded_normal; eauto. congruence.
      * eapply has_loaded_default; eauto. now rewrite ADDR.
    + one_step exec_Istore; repeat imply.
    + edestruct find_function_translated as (tfd&?&?); eauto.
      do 2 esplit; [eapply plus_one, exec_Icall with (fd:=tfd); eauto|].
      * destruct ros; simpl in *; auto. repeat imply.
      * erewrite sig_preserved; eauto.
      * replace (rs' ## args) with (rs ## args).
        2:{ repeat imply. destruct ros; simpl; auto. }
        do 2 (econstructor; eauto using match_regs_update_pc1).
        -- eapply max_reg_function_def; eauto; simpl; auto.
        -- intros. congruence.
    + edestruct find_function_translated as (tfd&?&?); eauto.
      do 2 esplit; [eapply plus_one, exec_Itailcall with (fd:=tfd); eauto|].
      * destruct ros; simpl in *; auto. repeat imply.
      * erewrite sig_preserved; eauto.
      * replace (rs' ## args) with (rs ## args).
        2:{ repeat imply. destruct ros; simpl; auto. }
        do 2 (econstructor; eauto using match_regs_update_pc1).
    + one_step exec_Ibuiltin; repeat imply.
      * eapply Events.eval_builtin_args_preserved; eauto using symbols_preserved.
        eapply list_forall2_imply; eauto; intros.
        eapply eval_builtin_arg_match; [|eauto]. intros.
        repeat imply. eauto using params_of_builtin_args_In.
      * eapply Events.external_call_symbols_preserved; eauto using senv_preserved.
      * eapply match_regs_update_pc1 with (pc:=pc); eauto.
        destruct res; simpl; auto. 2,3:split; auto.
        eapply match_regs_assign1; auto. split; auto.
    + one_step exec_Icond; repeat imply.
    + one_step exec_Ijumptable; repeat imply.
    + do 2 esplit; [eapply plus_one, exec_Ireturn; eauto|].
      destruct or; simpl; [|constructor; auto].
      replace (rs' # r) with (rs # r); [constructor; auto|].
      repeat imply.
    + eapply eval_assert_args_preserved, eval_assert_args_lessdef with (rs2:=rs') in H8 as (?&?&?);
        eauto using symbols_preserved, Mem.extends_refl.
      2:{ intros. replace (rs # x) with (rs' # x); eauto using Val.lessdef_refl.
          eapply REGS, max_reg_function_use; eauto. }
      one_step exec_Iassert; eauto.
      eapply eval_condition_lessdef; eauto using Mem.extends_refl.

  - (* Callstate *)
    inv STEP; monadInv.
    + (* internal *)
      assert (fn_stacksize x = fn_stacksize f0) as STACKSIZE by now repeat monadInv.
      assert (fn_params x = fn_params f0) as PARAMS by now repeat monadInv.
      assert (fn_sig x = fn_sig f0) as SIG by now repeat monadInv.

      assert (forall r, (max_reg_function f0 < r)%positive -> (init_regs args (fn_params f0)) # r = Vundef) as UNDEF.
      { intros * Lt.
        assert (~In r (fn_params f0)) as NIN.
        { intros IN. apply max_reg_function_params in IN. unfold Ple in *. lia. }
        clear - NIN. revert args.
        induction (fn_params f0); intros; simpl; auto using Regmap.gi.
        destruct args; auto using Regmap.gi.
        apply not_in_cons in NIN as (NEQ&NIN).
        rewrite Regmap.gso; auto.
      }

    destruct (do_protect f0) eqn:PROT.
    (* change of entrypoint *)
    *{ eapply transf_function_entry in PROT as (?&?&?&ENTRY); eauto.
       eexists. split; [eapply plus_two|econstructor]; eauto using Events.Eapp_E0.
       - apply exec_function_internal; eauto.
         + now rewrite SIG.
         + rewrite STACKSIZE; eauto.
      - eapply exec_Iop; eauto.
        simpl; eauto.
      - split; auto.
        + intros * Le. rewrite Regmap.gso, PARAMS; eauto.
          unfold gsr. lia.
        + rewrite Regmap.gss; eauto.
     }

    (* no change *)
    *{ eexists. split; [|econstructor; eauto].
       - apply plus_one.
         replace (fn_entrypoint f0) with (fn_entrypoint x).
         2:{ repeat monadInv. rewrite PROT in EQ0. inv EQ0. auto. }
         apply exec_function_internal; auto.
         + now rewrite SIG.
         + now rewrite STACKSIZE.
       - split; auto.
         + intros. now rewrite PARAMS.
         + intros; congruence. }
    + (* external *)
    eexists. split; [|econstructor; eauto].
    apply plus_one, exec_function_external.
    eapply Events.external_call_symbols_preserved; eauto using senv_preserved.

  - (* Returnstate *)
    inv STACKS; inv STEP.
    destruct (do_protect f) eqn:PROT.
    + (* protected *)
      destruct PC2 as (?&?&SIGS&PC'); auto.
      destruct is_join.
      * two_step exec_return exec_Iop.
        eapply match_regs_assign_gsr; eauto.
        apply match_regs_assign2; auto.
      * destruct PC' as (?&EQ); subst. symmetry in EQ.
        one_step exec_return.
        apply match_regs_assign2; auto.
        eapply match_regs_update_pc2 with (pc:=pc0); eauto.
    + (* unprotected *)
      specialize (PC1 eq_refl); subst.
      eexists. split; [eapply plus_one, exec_return|].
      econstructor; eauto.
      apply match_regs_assign2; auto.
      split; [apply REGS|intros; congruence].
Qed.

Correctness theorem

Theorem transf_program_correct:
forward_simulation (semantics prog) (semantics tprog).

Proof.

  eapply forward_simulation_plus.
  - apply senv_preserved.
  - apply transf_initial_states.
  - apply transf_final_states.
  - apply step_simulation.
Qed.

Extra: backward simulation

Theorem transf_program_backward:
backward_simulation (semantics prog) (semantics tprog).

Proof.

  apply forward_to_backward_simulation.
  - apply transf_program_correct.
  - apply semantics_receptive.
  - apply semantics_determinate.
Qed.

End CFC.