Library mcertikos.conlib.conmtlib.SingleOracleDef

Require Import Coqlib.
Require Import Maps.
Require Import ASTExtra.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import MemoryX.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Asm.
Require Import Conventions.
Require Import Machregs.
Require Import AuxLemma.

Require Import Values.
Require Import Maps.
Require Import Constant.
Require Import Maps.
Require Import ASTExtra.
Require Import Floats.
Require Import Values.
Require Import MemoryX.
Require Import Events.
Require Import Globalenvs.

Require Import liblayers.logic.PTreeModules.
Require Import liblayers.compcertx.MemWithData.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compat.CompatData.
Require Import liblayers.compat.CompatPrimSem.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatExternalCalls.
Require Import Decision.
Require Import LAsm.
Require Import GlobIdent.

Require Import FlatMemory.

Require Import AlgebraicMem.

Inductive lval:=
| Lint (n: int)
| Lptr (b: block) (ofs: int).

Section VAL2LVAL.

  Inductive val2Lval: val → lval → Prop:=
  | VAL2LVALINT:
      ∀ n,
        val2Lval (Vint n) (Lint n)
  | VAL2LVALPTR:
      ∀ n ofs,
        val2Lval (Vptr n ofs) (Lptr n ofs).

  Inductive val2Lval_list: (list val) → (list lval) → Prop:=
  | VAL2LVALNIL:
      val2Lval_list nil nil
  | VAL2LVALCON:
      ∀ v v´ l l´,
        val2Lval v v´ →
        val2Lval_list l l´ →
        val2Lval_list (v::l) (v´::l´).

  Lemma val2Lval_lessdef:
    ∀ v v´ gv,
      Val.lessdef v v´ →
      val2Lval v gv →
      val2Lval v´ gv.
  Proof.
    intros. inv H0; inv H; constructor.
  Qed.

  Lemma val2Lval_list_lessdef:
    ∀ v v´ gv,
      Val.lessdef_list v v´ →
      val2Lval_list v gv →
      val2Lval_list v´ gv.
  Proof.
    induction v; intros.
    - inv H; inv H0. constructor.
    - inv H. inv H0. constructor; eauto.
      eapply val2Lval_lessdef; eauto.
  Qed.

End VAL2LVAL.

Require Import SingleAbstractDataType.
Require Import DeviceStateDataType.
Require Import AuxStateDataType.

Record privDataSnap :=
  mk_privDataSnap {
      tiSnap: trapinfo;
      
      ikernSnap: bool;
      ihostSnap: bool;
      
      
      HPSnap: flatmem;
      
      ACSnap : Container;
      
      uctxtSnap : UContext;
      
      ppermSnap: PPermT;
      
      PTSnap: Z;
      ptpoolSnap: PMapPool;
      iptSnap: bool;
      
      syncchpoolSnap : SyncChanPool;
      bufferSnap: PageBufferPool;
      
      
      eptSnap: EPT;
      vmcsSnap: VMCS;
      vmxSnap: VMX;
      
      com1Snap: SerialData;
      drv_serialSnap: SerialDriver;
      console_concreteSnap: ConsoleDriverConcrete;
      consoleSnap: ConsoleDriver;
      
      
      ioapicSnap: IoApicData;
      lapicSnap: LApicData;
      tfSnap: TrapFrames;
      tf_regSnap: val;

      curr_intr_numSnap: Z;
      intr_flagSnap: bool;
      saved_intr_flagsSnap: list bool;
      
      in_intrSnap: bool;
      i_dev_serialSnap: bool
                      
    }.

Inductive LogEventUnit :=
| LogYield (n: positive)
| LogSleep (i: Z) (n: positive) (syncch : option AuxStateDataType.SyncChanPool)
| LogPrim (id: ident) (args: list lval) (choice : Z) (dprocSnap : privDataSnap)



| LogYieldBack.

Inductive LogEventType :=
| LogYieldTy
| LogOtherTy.

Inductive LogEvent :=
| LEvent : Z → LogEventUnit → LogEvent.


Function getLogEventUnitType (le : LogEventUnit) :=
  match le with
    | LogYield _ ⇒ LogYieldTy
    | LogSleep _ _ _ ⇒ LogYieldTy
    | _ ⇒ LogOtherTy
  end.

Function getLogEventType (le : LogEvent) :=
  match le with
    | LEvent _ t ⇒ getLogEventUnitType t
  end.

Function getLogEventUnitNB (le : LogEventUnit) :=
  match le with
    | LogYield n ⇒ Some n
    | LogSleep _ n _ ⇒ Some n
    | _ ⇒ None
  end.

Function getLogEventNB (le : LogEvent) :=
  match le with
    | LEvent _ t ⇒ getLogEventUnitNB t
  end.

Function getThrdID (le : LogEvent) :=
  match le with
    | LEvent cid _ ⇒ cid
  end.

Definition Log := list LogEvent.

Section Auxiliary.

  Set Implicit Arguments.

  Variable A : Type.

  Fixpoint last_op (l : list A) : option A :=
    match l with
      | nil ⇒ None
      | hd::_ ⇒ Some hd
    end.

  Definition remove_hd (l : list A) : list A :=
    match l with
    | nil ⇒ nil
    | ev::l´ ⇒ l´
    end.

  Lemma eq_lst_has_same_length:
    ∀ (l l´: list A),
      l = l´ → length l = length l´.
  Proof.
    induction l; intros; inv H; auto.
  Qed.

  Lemma all_lst_has_length:
    ∀ (l : list A), ∃ n, length l = n.
  Proof.
    induction l; intros; [∃ 0%nat |]; auto.
    destruct IHl; eauto.
  Qed.

  Lemma cons_lst_succ_length:
    ∀ (l: list A) (e: A) n, length l = n → length (e::l) = S n.
  Proof.
    destruct l; intros.
    - simpl; auto.
    - simpl; simpl in H; auto.
  Qed.

  Lemma cons_lst_eq_lst_contradiction:
    ∀ (l : list A) e, e::l = l → False.
  Proof.
    intros; generalize (all_lst_has_length l); intros.
    destruct H0 as (n, H0).
    generalize H0; intros.
    eapply eq_lst_has_same_length in H.
    eapply cons_lst_succ_length with (e := e) in H1.
    rewrite H1, H0 in H; generalize H; clear.
    intros; induction n.
    - inv H.
    - inversion H; clear H.
      apply IHn; auto.
  Qed.

  Unset Implicit Arguments.

End Auxiliary.

Function lastEvType (lg : Log) : option LogEventType :=
  match (last_op lg) with
  | Some ev ⇒ Some (getLogEventType ev)
    | None ⇒ None
  end.


Definition ThreadIDSet := list Z.