Module ExpandObserveproof

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 ExpandObserve.

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

Lemma transf_program_match: forall p,
match_prog p (transf_program p).

Proof.

intros. eapply match_transform_program; eauto.
Qed.

Section Expand.

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,
funsig (transf_fundef f) = funsig f.

Proof.

intros []; simpl; auto.
Qed.

Lemma fn_sig_preserved: forall f,
fn_sig (transf_function f) = fn_sig f.

Proof.

intros []; simpl; auto.
Qed.

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

Proof.

reflexivity. Qed.

Lemma stacksize_preserved: forall f,
fn_stacksize (transf_function f) = fn_stacksize f.

Proof.

reflexivity. Qed.

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

Proof.

apply (Genv.find_symbol_transf TRANSL).
Qed.

Lemma senv_preserved:
Senv.equiv ge tge.

Proof.

apply (Genv.senv_transf TRANSL).
Qed.

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

Proof.

apply (Genv.find_funct_transf TRANSL).
Qed.

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.

apply (Genv.find_funct_ptr_transf TRANSL).
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.

Opaque CounterMeasures.transf_function.

Lemma transf_function_entry:
forall f,
(fn_code (transf_function f))!(fn_entrypoint (transf_function f)) = Some (Inop (fn_entrypoint f)).

Proof.

  intros *.
  unfold transf_function in *.
  destruct CounterMeasures.transf_function eqn:?TR; simpl.
  eapply transf_function_entry in TR; eauto; simpl in TR; destruct_conjs; eauto.
  repeat inv_transf_function.
Qed.

Lemma transf_function_correct:
  forall f pc i,
    f.(fn_code)!pc = Some i ->
    exists abort e seq cont,
      transf_instr
        transf_nop_default transf_op_default
        transf_load_default transf_store_default
        transf_call_default transf_tailcall_default
        transf_builtin
        transf_cond_default
        transf_jumptable_default transf_return_default
        pc i = existT _ e (seq, cont)
      /\ spec_seq abort (fn_code (transf_function f)) pc seq cont.

Proof.

  intros * FIND.
  unfold transf_function in *.
  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 (rs rs' : regset) :=
    forall r, rs'#r = rs#r.

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 sp pc rs rs'
    (REG_OK : (res <= max_reg_function f)%positive)
    (REGS: forall v, match_regs (rs # res <- v) (rs' # res <- v))
    (TAIL: match_stacks tail tail'),
  match_stacks
    ((Stackframe res f sp pc rs) :: tail)
    ((Stackframe res (transf_function f) sp pc rs') :: tail').

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

Lemma match_regs_assign :
  forall rs rs' res v,
    match_regs rs rs' ->
    match_regs (rs # res <- v) (rs' # res <- v).

Proof.

intros * MATCH ?.
now rewrite ? Regmap.gsspec, MATCH.
Qed.

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.
  econstructor; split.
  - econstructor; eauto using function_ptr_translated.
    + eapply (Genv.init_mem_transf 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 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.

Lemma step_opaque_copies abort stk tf sp m :
  forall args pc sig pc' cseq rs rs1',
    concretized pc (opaque_copies sig args) (COneExit pc') cseq ->
    spec_cseq abort (fun _ => True) NoPred (fn_code tf) cseq ->
    match_regs rs rs1' ->
    exists rs2',
      plus step tge (State stk tf sp pc rs1' m) Events.E0 (State stk tf sp pc' rs2' m)
      /\ match_regs rs rs2'.

Proof.

  induction args as [|?]; intros * CONC SPEC REGS; simpl in *.
  1,2:repeat inv_transf_function.
  - do 2 esplit; [eapply plus_one|eauto].
    + eapply exec_Inop; eauto.
  - edestruct IHargs with (rs:=rs) (rs1':=rs1' # a <- (rs1' # a)) as (rs'&PLUS&MATCHR); eauto.
    + intros ?. rewrite Regmap.gsident. auto.
    + do 2 esplit; [eapply plus_left'; eauto|auto].
      * eapply exec_Iop; eauto.
      * now rewrite <- Events.Eapp_E0.
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.

  - (* regular state *)
    Local Ltac imply :=
      match goal with
      | H:match_regs _ _ |- _ => now rewrite H
      | |- 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
      | |- match_regs (_ # _ <- _) (_ # _ <- _) =>
          eapply match_regs_assign; 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].

    inv STEP.
    all:edestruct transf_function_correct as (?&?); [eauto|]; simpl in *.
    all:inv_transf_function.
    + 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.
    + do 2 esplit; [eapply plus_one, exec_Icall with (fd:=transf_fundef fd); eauto|].
      * eapply find_function_translated.
        destruct ros; simpl in *; auto. repeat imply.
      * erewrite sig_preserved; eauto.
      * replace (rs' ## args) with (rs ## args) by repeat imply.
        do 2 (econstructor; eauto).
        -- eapply max_reg_function_def; eauto; simpl; auto.
        -- intros. repeat imply.
    + do 2 esplit; [eapply plus_one, exec_Itailcall with (fd:=transf_fundef fd); eauto|].
      * eapply find_function_translated.
        destruct ros; simpl in *; auto. repeat imply.
      * erewrite sig_preserved; eauto.
      * replace (rs' ## args) with (rs ## args).
        2:{ repeat imply. }
        repeat (econstructor; eauto).
    + unfold transf_builtin in *.
      destruct (is_observe ef res) eqn:OBS; inv_transf_function.
      * destruct ef, res; simpl in *; inv OBS. inv H9.
        destruct Compopts.opaque_copies.
        -- eapply step_opaque_copies in H as (?&PLUS&MATCHR); eauto using match_states.
        -- inv_transf_function.
           do 2 esplit; [eapply plus_one, exec_Inop|]; eauto using match_states.
      * one_step exec_Ibuiltin.
        -- 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.
        -- eapply Events.external_call_symbols_preserved; eauto using senv_preserved.
        -- destruct res; simpl; auto. repeat imply.
    + do 2 esplit; [eapply plus_two|econstructor; eauto].
      * eapply exec_Icond with (b:=b); eauto.
        repeat imply.
      * destruct b; eapply exec_Inop; eauto.
      * now rewrite <- Events.Eapp_E0.
    + 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.
    + one_step exec_Inop.

  - (* Callstate *)
    inv STEP; simpl in *; repeat pMonadInv.
    + (* internal *)
      do 2 esplit; [eapply plus_two|].
      * eapply exec_function_internal.
        { rewrite fn_sig_preserved. assumption. }
        erewrite stacksize_preserved; eauto.
      * eapply exec_Inop; eauto using transf_function_entry.
      * now rewrite <- Events.Eapp_E0.
      * econstructor; eauto.
        erewrite params_preserved; eauto.
        intros ?. reflexivity.
    + (* external *)
      do 2 esplit; [eapply plus_one|].
      * eapply exec_function_external.
        eapply Events.external_call_symbols_preserved; eauto using senv_preserved.
      * econstructor; eauto.

  - (* Returnstate *)
    inv STEP; inv STACKS.
    do 2 esplit; [eapply plus_one|].
    + eapply exec_return.
    + econstructor; eauto.
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.

End Expand.