Module CFCsecurity

Require Import Coqlib List Maps Integers Errors.
Import ListNotations.
Require Import AST Linking Smallstep Events.
Require Import Globalenvs Values Kildall.
Require Import Op Registers Memory RTL.
Require Import CounterMeasures CFC CFCproof.
Require Import RTLtyping RTLpast RTLfault.


Section compute_sigs.

  Lemma compute_sigs_robust f : forall sigs joins pc c rs pc1 pc2 pred,
      compute_sigs f = OK (sigs, joins) ->
      (fn_code f)!pc = Some (Icond c rs pc1 pc2 pred) ->
      pc1 <> pc2 ->
      get_sig sigs pc1 <> get_sig sigs pc2.

End compute_sigs.


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

Ltac destruct_disjs :=
  repeat match goal with H: _ \/ _ |- _ => destruct H end.

Lemma transf_code_cond_inv f tf env : forall pc c rs pc1 pc2 pred,
    wt_function f env ->
    transf_function f = OK tf ->
    do_protect f = true ->
    let code := fn_code tf in
    code!pc = Some (Icond c rs pc1 pc2 pred) ->
    (exists sigs joins abort pcf c' rs' pc1' pc2' pred',
        (fn_code f)!pcf = Some (Icond c' rs' pc1' pc2' pred')
        /\ compute_sigs f = OK (sigs, joins)
        /\ spec_seq_inv (fun pc => pc <> fn_entrypoint tf) abort code
            pc (Icond c rs pc1 pc2 pred)
            pcf (transf_cond sigs (gsr f) (rts f) pcf c' rs' pc1' pc2' pred') (CTwoExits pc1' pc2')
        /\ code!abort = Some (Ibuiltin EF_cm_catch [] BR_none abort))
    \/ (exists sigs joins abort pcf r,
          (fn_code f)!pcf = Some (Ireturn r)
          /\ compute_sigs f = OK (sigs, joins)
          /\ spec_seq_inv (fun pc => pc <> fn_entrypoint tf) abort code
              pc (Icond c rs pc1 pc2 pred) pcf (transf_return sigs (gsr f) pcf r) CNoExit
          /\ code!abort = Some (Ibuiltin EF_cm_catch [] BR_none abort)
      ).

Lemma transf_function_protect : forall f tf,
    transf_function f = OK tf ->
    do_protect tf = do_protect f.

Section CFC.

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

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

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

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

Hypothesis WT: wt_program prog.

Ltac external_call_nofault :=
  exfalso;
  repeat
    match goal with
    | H:external_call _ _ _ _ [_] _ _ |- _ =>
        eapply external_call_nofault in H; inv H
    | H:forall f, _ <> _ |- False => eapply H; eauto
    end.

Ltac simplify_xors :=
  match goal with
  | EQ: ?x = Vint _ |- context [?x] => rewrite EQ; simpl
  | EQ: ?x = Vint _, H: context [?x] |- _ => rewrite EQ in H; simpl in H
  | |- context [Int.xor ?x (Int.xor ?x _)] =>
      rewrite <- Int.xor_assoc, Int.xor_idem, Int.xor_zero_l; simpl
  | H:context [Int.xor ?x (Int.xor ?x _)] |- _ =>
      rewrite <- Int.xor_assoc, Int.xor_idem, Int.xor_zero_l in H; simpl in H
  end.

Ltac simplify_tests :=
  match goal with
  | |- context [Int.eq ?x ?x] => rewrite Int.eq_true; simpl
  | |- context [Int.eq _ _] => rewrite Int.eq_false by (intros ?; eauto); simpl
  end.

Ltac imply_condition :=
  match goal with
  | H: eval_condition _ ?rs _ = Some _ |- eval_condition _ ?rs' _ = Some _ =>
      replace rs' with rs; eauto;
      apply map_ext_in; intros * IN; rewrite Regmap.gso; auto
  | H1: eval_condition _ ?rs _ = Some _, H2: eval_condition _ ?rs' _ = Some _ |- _ =>
      replace rs' with rs in H2;
      [rewrite H1 in H2; inv H2|apply map_ext_in; intros * IN; rewrite Regmap.gso; auto]
  end.

Ltac do_step :=
  match goal with
  | H: _ ! ?pc = Some (Inop _) |- step _ (RTL.State _ _ _ ?pc _ _) _ _ =>
      eapply RTL.exec_Inop; [eauto]; simpl; eauto
  | H: _ ! ?pc = Some (Iop _ _ _ _) |- step _ (RTL.State _ _ _ ?pc _ _) _ _ =>
      eapply RTL.exec_Iop; [now eauto|]; simpl; eauto
  | H: _ ! ?pc = Some (Ibuiltin _ _ _ _) |- step _ (RTL.State _ _ _ ?pc _ _) _ _ =>
      eapply RTL.exec_Ibuiltin; eauto; [|constructor]; repeat econstructor
  | H: _ ! ?pc = Some (Icond _ _ _ _ _) |- step _ (RTL.State _ _ _ ?pc _ _) _ _ =>
      eapply RTL.exec_Icond; eauto; simpl; try imply_condition; simpl
  | |- fstep _ _ _ (Valid _) =>
      instantiate (1:=RTL.State _ _ _ _ _ _); simpl
  | H: _ ! ?pc = Some (Inop _) |- fstep _ (Valid (State _ _ _ ?pc _ _)) _ _ =>
      constructor
  | H: _ ! ?pc = Some (Iop _ _ _ _) |- fstep _ (Valid (State _ _ _ ?pc _ _)) _ _ =>
      constructor
  | H: _ ! ?pc = Some (Ibuiltin _ _ _ _) |- fstep _ (Valid (RTL.State _ _ _ ?pc _ _)) _ _ =>
      constructor
  | H: _ ! ?pc = Some (Icond _ _ _ _ _) |- fstep _ (Valid (State _ _ _ ?pc _ _)) _ _ =>
      constructor
  | H: _ ! ?pc = Some (Ibuiltin EF_cm_catch _ _ _) |- fstep _ (Valid (State _ _ _ ?pc _ _)) _ _ =>
      eapply exec_IbuiltinCatch; eauto
  end.

Tactic Notation "star_step" int_or_var(n) :=
  do n (try (eapply star_left; eauto using Eapp_E0)); try apply star_refl.

Ltac simplify_regs :=
  match goal with
  | |- context [(_ # ?x <- _) # ?x] => rewrite Regmap.gss
  | |- context [(_ # _ <- _) # _] => rewrite Regmap.gso by auto
  | H: context [(_ # ?x <- _) # ?x] |- _ => rewrite Regmap.gss in H
  | H: context [(_ # _ <- _) # _] |- _ => rewrite Regmap.gso in H by auto
  end.

Ltac simplify_ctx :=
  simpl in *;
  match goal with
  | H:Some _ = Some _ |- _ => inv H
  | H:Vint _ = Vint _ |- _ => inv H
  | _ => (simplify_regs||simplify_xors||simplify_tests)
  end.

Opaque transf_function.


Ltac inv_equalities :=
  match goal with
  | H1: ?x = Some _, H2: ?x = Some _ |- _ => rewrite H2 in H1; inv H1
  | H1: ?x = OK _, H2: ?x = OK _ |- _ => rewrite H2 in H1; inv H1
  end.

Ltac inv_gsr :=
  simpl in *;
  repeat
    match goal with
    | H: eval_assert_args _ _ _ _ [_] _ |- _ =>
        inversion H as [|???? ?EVAL ?NIL]; subst; clear H; inv NIL; inv EVAL
    | H: Val.cmp_bool Ceq ?rs # (gsr ?f) _ = Some true |- _ =>
        simpl in H; destruct (rs # (gsr f)) eqn:GSR; inversion H as [EQ];
        apply Int.same_if_eq in EQ; subst; auto
    end.

Lemma fault_step: forall st0 t0 st1 (attacked: function) st2,
    do_protect attacked = true ->
    RTL.initial_state tprog st0 ->
    star step tge st0 t0 st1 ->
    fstep tge (Valid st1) [Event_fault (Fault_invertcond attacked)] st2 ->
    gets_caught tprog st2
    \/ (exists (st' : RTL.state) (t' : trace),
          star fstep tge st2 t' (Valid st') /\ nofault t' /\ star step tge st1 t' st').

Theorem transf_program_secure: forall (attacked: function),
    do_protect attacked = true ->
    secure_against tprog (Fault_invertcond attacked).

End CFC.