Library mcertikos.driver.CertiKOSAux

Require Import RealParams.
Require Import Maps.
Require Import CommonTactic.
Require Import AuxLemma.
Require Import Coqlib.
Require Import ErrorMonad.
Require Import LinkSourceTemplate.
Require Export LinkTactic. Require Export LinkTemplate.
Require Export LAsmModuleSemEvent.
Require Export CompCertiKOSproofImpl.
Require Import CertiKOS.
Require Import GlobalOracleProp.

Tactics used for global linking

For some reason, applying the Foo.make_program_exists theorem efficiently is a little bit tricky. We use these tactics to massage everything as needed.

First, we unfold the Foo_impl modules which are of the form link_impl Foo_module _, so that the corresponding theorem can unify without effort.

Ltac unfold_into_link_impl H :=
  lazymatch type of H with
    | ?Foo_impl = OK _ ⇒
      lazymatch eval red in Foo_impl with
        | link_impl ?module ?base_layer ⇒
          change Foo_impl with (link_impl module base_layer) in H
      end
  end.

Ltac unfold_all_into_link_impl :=
  repeat match goal with H: _ |- _ ⇒ unfold_into_link_impl H end.

With the assumption that our Foo_impl now match the generic make_program_exists_type, we can locate the appropiate hypothesis to solve the corresponding subgoal, without computing the hell out of it.

Ltac impl_ok_assumption :=
  lazymatch goal with
    | |- ?impl = OK _ ⇒
      lazymatch goal with
        | H: impl = OK _ |- _ ⇒
          apply H
      end
  end ||
  eassumption.

We also do something similar for make_program hypotheses.

Ltac make_program_ok_assumption :=
  match goal with
    | |- make_program _ _ ?L = OK _ ⇒
      match goal with
        | H: make_program _ _ L = OK _ |- _ ⇒
          exact H
      end
  end.

Now, it's easy to destruct a Foo.make_program_exists theorem efficiently by using impl_ok_assumption for the first subgoal.

Ltac destruct_mpe hyp :=
  let p := fresh "p" in
  let Hp := fresh "H" p in
  edestruct hyp as [p Hp];
    [ impl_ok_assumption ..
    | make_program_ok_assumption
    | ].

Similarly, this tactic is used to apply Foo.cl_backward_simulation.

Ltac last_backward_simulation thm :=
  eapply thm;
  [ assumption
  | impl_ok_assumption ..
  | make_program_ok_assumption
  | make_program_ok_assumption ].

Ltac compose_backward_simulation thm :=
  eapply compose_backward_simulation;
  [ assumption
  | last_backward_simulation thm
  | idtac ].

Lemmas used to establish the final theorem

Lemma option_rel_eq_antisymmetry {A}{x y : option A} :
  option_le eq x y → option_le eq y x → x = y.
Proof.
  intros x_le_y y_le_x.
  inversion x_le_y; inversion y_le_x; congruence.
Qed.

Lemma prog_defs_le_antisymmetry {F V} p1 p2 :
    @CompcertStructures.prog_defs_le F V p1 p2 →
    @CompcertStructures.prog_defs_le F V p2 p1 →
    p1 = p2.
Proof.
  intros le12 le21.
  induction le12; try reflexivity.
  inversion le21.
  subst.
  f_equal.
  - inversion H.
    inversion H3.
    rewrite (surjective_pairing x), (surjective_pairing y).
    unfold RelationPairs.RelCompFun in H0.
    rewrite (option_rel_eq_antisymmetry H1 H4).
    congruence.
  - apply IHle12; assumption.
Qed.

Lemma make_program_equiv {D}(s: stencil)(M1 M2: module) L prog :
  M1 ≡ M2 →
  make_program (D := D) s M1 L = OK prog →
  make_program s M2 L = OK prog.
Proof.
  intros Mequiv mk1.
  assert (M1_le_M2 : M1 ≤ M2) by apply Mequiv.
  assert (M2_le_M1 : M2 ≤ M1) by apply Mequiv.
  assert (L_le_L : L ≤ L) by reflexivity.
  assert (res1_le_2 := make_program_monotonic s _ _ M1_le_M2 _ _ L_le_L).
  assert (res2_le_1 := make_program_monotonic s _ _ M2_le_M1 _ _ L_le_L).
  rewrite mk1 in res1_le_2, res2_le_1.
  clear mk1 M1_le_M2 M2_le_M1 L_le_L.

  inversion res2_le_1 as [ prog2 ? prog2_le mk2 |]; subst.
  inversion res1_le_2 as [ ? prog1 prog1_le xeq mk1 |]; [ subst | congruence ].
  simpl; rewrite <- mk1.
  rewrite <- mk1 in mk2; injection mk2 as →.
  clear res1_le_2 res2_le_1 mk1 mk2.

  destruct prog1_le.
  f_equal; f_equal.
  inversion prog2_le.
  apply prog_defs_le_antisymmetry; assumption.
Qed.

Require Import AlgebraicMemImpl.
Require Import SingleOracle.
Require Import SingleConfiguration.
Require Import SingleOracleImpl.

Section CERTIKOSPLUSCONTEXT.

  Context `{multi_oracle_prop : MultiOracleProp}.
  Context `{s_oracle_ops : SingleOracleOps}.
  Context `{s_threads_ops: ThreadsConfigurationOps}.

  Context `{s_threads_prf: !ThreadsConfiguration (s_oracle := s_oracle_prf)}.
  Context `{s_oracle_basic_prop_prf: !SingleOracleBasicProp (single_oracle_prf := s_oracle_prf)
                                      (s_threads_ops := s_threads_ops)}.

  Existing Instance SingleOracleImpl.s_oracle_prf.
  Existing Instance SingleOracleImpl.s_oracle_prop_prf.
  Existing Instance SingleOracleImpl.s_config.

  Context `{multi_oracle_link: !MultiOracleLink}.

  Lemma per_cpu_CertiKOS_plus_context CTXT kernel:
    CertiKOS.per_cpu_certikos = OK kernel →
    ∃ combined,
      CertiKOS.per_cpu_certikos_plus_ctxt CTXT = OK combined ∧
      CTXT ⊕ kernel ≡ combined.
  Proof.
    unfold CertiKOS.per_cpu_certikos.
    unfold CertiKOS.per_cpu_certikos_plus_ctxt.
    unfold CertiKOS.add_loc.
    intros Hkernel.
    inv_monad´ Hkernel.
    repeat match goal with H: _ = ret _ |- _ ⇒ rewrite H end.
    clear.
    monad_norm.
    eexists.
    split.
    - reflexivity.
    - split; le_oplus.
  Qed.

  Lemma per_thread_CertiKOS_plus_context CTXT kernel:
    CertiKOS.per_thread_certikos = OK kernel →
    ∃ combined,
      CertiKOS.per_thread_certikos_plus_ctxt CTXT = OK combined ∧
      CTXT ⊕ kernel ≡ combined.
  Proof.
    unfold CertiKOS.per_thread_certikos.
    unfold CertiKOS.per_thread_certikos_plus_ctxt.
    unfold CertiKOS.add_loc.
    intros Hkernel.
    inv_monad´ Hkernel.
    repeat match goal with H: _ = ret _ |- _ ⇒ rewrite H end.
    clear.
    monad_norm.
    eexists.
    split.
    - reflexivity.
    - split; le_oplus.
  Qed.

  Lemma CertiKOS_plus_context CTXT kernel:
    CertiKOS.certikos = OK kernel →
    ∃ combined,
      CertiKOS.certikos_plus_ctxt CTXT = OK combined ∧
      CTXT ⊕ kernel ≡ combined.
  Proof.
    unfold CertiKOS.certikos.
    unfold CertiKOS.certikos_plus_ctxt.
    unfold CertiKOS.add_loc.
    intros Hkernel.
    inv_monad´ Hkernel.
    repeat match goal with H: _ = ret _ |- _ ⇒ rewrite H end.
    clear.
    monad_norm.
    eexists.
    split.
    - reflexivity.
    - split; le_oplus.
  Qed.

End CERTIKOSPLUSCONTEXT.