Library mcertikos.objects.dev.ObjConsole

Require Import Coqlib.
Require Import DeviceStateDataType.
Require Import FlatMemory.
Require Import AbstractDataType.
Require Import Values.
Require Import Maps.
Require Import Constant.
Require Import OracleInstances.
Require Import List.
Import List.ListNotations.

Notation CONS_BUFFER_SIZE := 512.

Section OBJ_Console_Buf_Concrete.

  Function cons_buf_init_concrete_spec (abd: RData) : option RData :=
    match (ikern abd, ihost abd, init abd) with
      | (true, true, true) ⇒
        Some abd {console_concrete: (console_concrete abd) {rpos_concrete: 0} {wpos_concrete: 0}}
      | _ ⇒ None
    end.

  Function cons_buf_write_concrete_spec (c: Z) (abd: RData) : option RData :=
    match (ikern abd, ihost abd, init abd) with
    | (true, true, true) ⇒
      let buf := cons_buf_concrete (console_concrete abd) in
      let rpos := rpos_concrete (console_concrete abd) in
      let wpos := wpos_concrete (console_concrete abd) in
      if zeq ((wpos + 1) mod CONS_BUFFER_SIZE) rpos then
        Some (abd {console_concrete: ((console_concrete abd) {cons_buf_concrete: ZMap.set wpos (BufVal c) buf} {wpos_concrete: (wpos + 1) mod CONS_BUFFER_SIZE} {rpos_concrete: (rpos + 1) mod CONS_BUFFER_SIZE})})
      else
        Some (abd {console_concrete: ((console_concrete abd) {cons_buf_concrete: ZMap.set wpos (BufVal c) buf} {wpos_concrete: (wpos + 1) mod CONS_BUFFER_SIZE})})
    | _ ⇒ None
    end.

  Function cons_buf_read_concrete_spec (abd: RData): option (RData × Z) :=
    match (ikern abd, ihost abd, init abd) with
      | (true, true, true) ⇒
        let s := console_concrete abd in
        let buf := cons_buf_concrete s in
        let rpos := rpos_concrete s in
        let wpos := wpos_concrete s in
        if zeq rpos wpos then
          Some (abd, 0)
        else
          match ZMap.get rpos buf with
            | BufValUndef ⇒ None
            | BufVal c ⇒
              Some (abd {console_concrete: (s {rpos_concrete: ((rpos + 1) mod CONS_BUFFER_SIZE)})}, c)
          end
      | _ ⇒ None
    end.

  Function cons_buf_wpos_concrete_spec (abd: RData): option Z :=
    match (ikern abd, ihost abd, init abd) with
      | (true, true, true) ⇒
        Some (wpos_concrete (console_concrete abd))
      | _ ⇒ None
    end.

End OBJ_Console_Buf_Concrete.

Section OBJ_Console.

  Section OBJ_Console_Buf.

    Function cons_buf_init_spec (abd: RData) : option RData :=
      match (ikern abd, ihost abd, init abd) with
        | (true, true, true) ⇒
          Some abd {console: console_init_d}
        | _ ⇒ None
      end.

    Function cons_buf_write_spec (c: Z) (abd: RData) : option RData :=
      match (ikern abd, ihost abd, init abd) with
        | (true, true, true) ⇒
          Some (abd {console: (handle_cons_buf_write (console abd) c)})
        | _ ⇒ None
      end.

    Function cons_buf_read_spec (abd: RData): option (RData × Z) :=
      match (ikern abd, ihost abd, init abd) with
        | (true, true, true) ⇒
          let s := console abd in
          let b := cons_buf s in
          let r := rpos s in
          match b with
            | nil ⇒ Some (abd, 0)
            | c :: tl ⇒
              Some (abd {console: (s {cons_buf: tl}{rpos: ((r + 1) mod CONS_BUFFER_SIZE)})}, c)
          end
        | _ ⇒ None
      end.

    Function cons_buf_wpos_spec (abd: RData): option Z :=
      match (ikern abd, ihost abd, init abd) with
        | (true, true, true) ⇒
          let s := console abd in
          let b := cons_buf s in
          let r := rpos s in
          Some ((r + (Z.of_nat (length b))) mod CONS_BUFFER_SIZE)
        | _ ⇒ None
      end.

  End OBJ_Console_Buf.

  Section OBJ_Console_Driver.

    Function cons_init_spec (abd: RData) : option RData :=
      match (ikern abd, init abd, ihost abd) with
      | (true, true, true) ⇒
        match com1 abd with
        | mkDevData
            (mkSerialState PortCom1Base true false _ nil nil _ _ _ _ _ _ _) lrx _ _ ⇒
          match SerialEnv lrx with
          | SerialRecv str ⇒
            Some (abd {console: console_init_d}
                      {com1 / s: ( mkSerialState
                                     PortCom1Base true false false nil (tl str)
                                     false 1 8 1 pNone 199 11)}
                      {com1 / l1: lrx + 1}
                      {drv_serial: (mkSerialDriver 1)}
                 )
          | _ ⇒
            Some (abd {console: console_init_d}
                      {com1 / s: ( mkSerialState
                                     PortCom1Base true false false nil nil
                                     false 1 8 1 pNone 199 11)}
                      {com1 / l1: lrx + 1}
                      {drv_serial: (mkSerialDriver 1)}
                 )
          end
        | _ ⇒ None
        end
      | _ ⇒ None
      end.

    Notation CONS_BUFFER_MAX_CHARS := (CONS_BUFFER_SIZE - 1).

    Require Import ObjInterruptDriver.

    Function cons_intr_aux (abd: RData): option RData :=
      match (ikern abd, ihost abd, init abd, in_intr abd) with
      | (true, true, true, true) ⇒
        if zeq 1 (serial_exists (drv_serial abd))
        then
          match com1 abd with
          | mkDevData
              (mkSerialState _ true true true nil rxbuf false _ _ _ _ _ _) lrx _ _ ⇒
            match SerialEnv (lrx - 1) with
            | SerialRecv str ⇒
              if list_eq_dec Z.eq_dec str rxbuf then
                if zle
                     (Zlength (abd.(console).(cons_buf) ++ rxbuf)) CONS_BUFFER_MAX_CHARS
                then Some (abd
                             {console / cons_buf: (cons_buf (console abd)) ++ rxbuf}
                             {com1 / l1: (lrx + Zlength rxbuf × 2 + 1)}
                             {com1 / s / RxBuf: nil}
                             {com1 / s / SerialIrq: false})
                else Some abd
                          {console / cons_buf: skipn
                                                 (Z.to_nat( Zlength ((cons_buf (console abd)) ++ rxbuf) - CONS_BUFFER_MAX_CHARS))
                                                 ((cons_buf (console abd)) ++ rxbuf)}
                          {console / rpos: ((rpos (console abd)) + Zlength(cons_buf (console abd) ++ rxbuf) + 1) mod CONSOLE_BUFFER_SIZE}
                          {com1 / l1: (lrx + Zlength rxbuf × 2 + 1)}
                          {com1 / s /RxBuf: nil}
                          {com1 / s /SerialIrq: false}
              else None
            | _ ⇒ None
            end
          | _ ⇒ None
          end
        else
          None
      | _ ⇒ None
      end.

    Function cons_intr_spec (abd1: RData): option RData :=
      match (ikern abd1, ihost abd1, init abd1, in_intr abd1) with
        | (true, true, true, true) ⇒
          match lapic_eoi_spec abd1 with
            | Some abd ⇒ cons_intr_aux abd
            | _ ⇒ None
          end
        | _ ⇒ None
      end.

    Lemma cons_intr_aux_subset:
      ∀ d d´ r,
        cons_intr_spec d = Some d´ →
        lapic_eoi_spec d = Some r →
        cons_intr_aux r = Some d´.
    Proof.
      intros.
      unfold cons_intr_spec in H.
      rewrite H0 in H.
      functional inversion H0; subst.
      inv H. rewrite H2, H3, H4, H5 in ×. reflexivity.
    Qed.

End OBJ_Console_Driver.

End OBJ_Console.

Require Import liblayers.compat.CompatGenSem.
Require Import liblayers.compat.CompatLayers.
Require Import CommonTactic.
Require Import RefinementTactic.
Require Import PrimSemantics.
Require Import AuxLemma.
Require Import GlobIdent.
Require Import LAsmModuleSemAux.

Section OBJ_SIM.

  Context `{data : CompatData RData}.
  Context `{data0 : CompatData RData}.

  Context `{Hstencil: Stencil}.
  Context `{Hmem: Mem.MemoryModel}.
  Context `{Hmwd: UseMemWithData mem}.

  Notation HDATAOps := (cdata (cdata_prf := data) RData).
  Notation LDATAOps := (cdata (cdata_prf := data0) RData).

  Context `{rel_prf: CompatRel _ (memory_model_ops:= memory_model_ops) _
                               (stencil_ops:= stencil_ops) HDATAOps LDATAOps}.

  Local Open Scope Z_scope.

  Section CONS_BUF_INIT_SIM.

    Context {re1: relate_impl_iflags}.
    Context {re2: relate_impl_console}.
    Context {re3: relate_impl_init}.

    Lemma cons_buf_init_exist:
      ∀ s habd habd´ labd f,
        cons_buf_init_spec habd = Some habd´
        → relate_AbData s f habd labd
        → ∃ labd´, cons_buf_init_spec labd = Some labd´
                         ∧ relate_AbData s f habd´ labd´.
    Proof.
      unfold cons_buf_init_spec; intros.
      exploit relate_impl_iflags_eq; eauto; inversion 1.
      exploit relate_impl_console_eq; eauto; inversion 1.
      exploit relate_impl_init_eq; eauto; inversion 1.
      revert H. subrewrite.
      subdestruct. inv HQ; refine_split´; trivial.
      apply relate_impl_console_update; eauto.
    Qed.

    Context {mt1: match_impl_console}.

    Lemma cons_buf_init_match:
      ∀ s d d´ m f,
        cons_buf_init_spec d = Some d´
        → match_AbData s d m f
        → match_AbData s d´ m f.
    Proof.
      unfold cons_buf_init_spec; intros. subdestruct; inv H; trivial.
      eapply match_impl_console_update. assumption.
    Qed.

    Context {inv: PreservesInvariants (HD:= data) cons_buf_init_spec}.
    Context {inv0: PreservesInvariants (HD:= data0) cons_buf_init_spec}.

    Lemma cons_buf_init_sim :
      ∀ id,
        sim (crel RData RData) (id ↦ gensem cons_buf_init_spec)
            (id ↦ gensem cons_buf_init_spec).
    Proof.
      intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
      exploit cons_buf_init_exist; eauto 1; intros (labd´ & HP & HM).
      match_external_states_simpl.
      eapply cons_buf_init_match; eauto.
    Qed.

  End CONS_BUF_INIT_SIM.

  Section CONS_BUF_WRITE_SIM.

    Context {re1: relate_impl_iflags}.
    Context {re2: relate_impl_console}.
    Context {re3: relate_impl_init}.

    Lemma cons_buf_write_exist:
      ∀ s habd habd´ c labd f,
        cons_buf_write_spec c habd = Some habd´
        → relate_AbData s f habd labd
        → ∃ labd´, cons_buf_write_spec c labd = Some labd´
                         ∧ relate_AbData s f habd´ labd´.
    Proof.
      unfold cons_buf_write_spec; intros.
      exploit relate_impl_iflags_eq; eauto; inversion 1.
      exploit relate_impl_console_eq; eauto; inversion 1.
      exploit relate_impl_init_eq; eauto; inversion 1.
      revert H. subrewrite.
      subdestruct. inv HQ; refine_split´; trivial.
      apply relate_impl_console_update; eauto.
    Qed.

    Context {mt1: match_impl_console}.

    Lemma cons_buf_write_match:
      ∀ s d d´ c m f,
        cons_buf_write_spec c d = Some d´
        → match_AbData s d m f
        → match_AbData s d´ m f.
    Proof.
      unfold cons_buf_write_spec; intros. subdestruct; inv H; trivial.
      eapply match_impl_console_update. assumption.
    Qed.

    Context {inv: PreservesInvariants (HD:= data) cons_buf_write_spec}.
    Context {inv0: PreservesInvariants (HD:= data0) cons_buf_write_spec}.

    Lemma cons_buf_write_sim :
      ∀ id,
        sim (crel RData RData) (id ↦ gensem cons_buf_write_spec)
            (id ↦ gensem cons_buf_write_spec).
    Proof.
      intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
      exploit cons_buf_write_exist; eauto 1; intros (labd´ & HP & HM).
      match_external_states_simpl.
      eapply cons_buf_write_match; eauto.
    Qed.

  End CONS_BUF_WRITE_SIM.

  Section CONS_BUF_READ_SIM.

    Context {re1: relate_impl_iflags}.
    Context {re2: relate_impl_console}.
    Context {re3: relate_impl_init}.

    Lemma cons_buf_read_exist:
      ∀ s habd habd´ c labd f,
        cons_buf_read_spec habd = Some (habd´, c)
        → relate_AbData s f habd labd
        → ∃ labd´, cons_buf_read_spec labd = Some (labd´, c)
                         ∧ relate_AbData s f habd´ labd´.
    Proof.
      unfold cons_buf_read_spec; intros.
      exploit relate_impl_iflags_eq; eauto; inversion 1.
      exploit relate_impl_console_eq; eauto; inversion 1.
      exploit relate_impl_init_eq; eauto; inversion 1.
      revert H. subrewrite.
      subdestruct. inv HQ; refine_split´; trivial.
      subdestruct. inv HQ; refine_split´; trivial.
      apply relate_impl_console_update; eauto.
    Qed.

    Context {mt1: match_impl_console}.

    Lemma cons_buf_read_match:
      ∀ s d d´ c m f,
        cons_buf_read_spec d = Some (d´, c)
        → match_AbData s d m f
        → match_AbData s d´ m f.
    Proof.
      unfold cons_buf_read_spec; intros. subdestruct; inv H; trivial.
      eapply match_impl_console_update. assumption.
    Qed.

    Context {inv: PreservesInvariants (HD:= data) cons_buf_read_spec}.
    Context {inv0: PreservesInvariants (HD:= data0) cons_buf_read_spec}.

    Lemma cons_buf_read_sim :
      ∀ id,
        sim (crel RData RData) (id ↦ gensem cons_buf_read_spec)
            (id ↦ gensem cons_buf_read_spec).
    Proof.
      intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
      exploit cons_buf_read_exist; eauto 1; intros (labd´ & HP & HM).
      match_external_states_simpl.
      eapply cons_buf_read_match; eauto.
    Qed.

  End CONS_BUF_READ_SIM.

  Section CONS_BUF_WPOS_SIM.

    Context {re1: relate_impl_iflags}.
    Context {re2: relate_impl_console}.
    Context {re3: relate_impl_init}.

    Lemma cons_buf_wpos_exist:
      ∀ s habd labd z f,
        cons_buf_wpos_spec habd = Some z
        → relate_AbData s f habd labd
        → cons_buf_wpos_spec labd = Some z.
    Proof.
      unfold cons_buf_wpos_spec; intros.
      exploit relate_impl_iflags_eq; eauto; inversion 1.
      exploit relate_impl_console_eq; eauto; inversion 1.
      exploit relate_impl_init_eq; eauto; inversion 1.
      revert H; subrewrite.
    Qed.

    Lemma cons_buf_wpos_sim :
      ∀ id,
        sim (crel RData RData) (id ↦ gensem cons_buf_wpos_spec)
            (id ↦ gensem cons_buf_wpos_spec).
    Proof.
      intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
      match_external_states_simpl.
      erewrite cons_buf_wpos_exist; eauto. reflexivity.
    Qed.

  End CONS_BUF_WPOS_SIM.

  Section CONS_INIT_SIM.

    Context {re1: relate_impl_iflags}.
    Context {re2: relate_impl_drv_serial}.
    Context {re3: relate_impl_com1}.
    Context {re4: relate_impl_console}.
    Context {re5: relate_impl_init}.

    Lemma cons_init_exist:
      ∀ s habd habd´ labd f,
        cons_init_spec habd = Some habd´
        → relate_AbData s f habd labd
        → ∃ labd´, cons_init_spec labd = Some labd´
                         ∧ relate_AbData s f habd´ labd´.
    Proof.
      unfold cons_init_spec; intros.
      exploit relate_impl_iflags_eq; eauto; inversion 1.
      exploit relate_impl_com1_eq; eauto; inversion 1.
      exploit relate_impl_console_eq; eauto; inversion 1.
      exploit relate_impl_init_eq; eauto; inversion 1.
      revert H. subrewrite.
      subdestruct;
      inv HQ; refine_split´; trivial;
      repeat (try apply relate_impl_drv_serial_update; eauto;
      try rewrite H4;
      try apply relate_impl_com1_update; eauto;
      try apply relate_impl_com1_update; eauto;
      try apply relate_impl_console_update; eauto).
    Qed.

    Context {mt1: match_impl_console}.
    Context {mt2: match_impl_com1}.
    Context {mt3: match_impl_drv_serial}.

    Lemma cons_init_match:
      ∀ s d d´ m f,
        cons_init_spec d = Some d´
        → match_AbData s d m f
        → match_AbData s d´ m f.
    Proof.
      unfold cons_init_spec; intros. subdestruct; inv H; trivial;
      eapply match_impl_drv_serial_update;
      eapply match_impl_com1_update;
      eapply match_impl_com1_update;
      eapply match_impl_console_update;
      assumption.
    Qed.

    Context {inv: PreservesInvariants (HD:= data) cons_init_spec}.
    Context {inv0: PreservesInvariants (HD:= data0) cons_init_spec}.

    Lemma cons_init_sim :
      ∀ id,
        sim (crel RData RData) (id ↦ gensem cons_init_spec)
            (id ↦ gensem cons_init_spec).
    Proof.
      intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
      exploit cons_init_exist; eauto 1; intros (labd´ & HP & HM).
      match_external_states_simpl.
      eapply cons_init_match; eauto.
    Qed.

  End CONS_INIT_SIM.

  Section CONS_INTR_SIM.

    Context {re1: relate_impl_iflags}.
    Context {re2: relate_impl_drv_serial}.
    Context {re3: relate_impl_com1}.
    Context {re4: relate_impl_console}.
    Context {re5: relate_impl_lapic}.
    Context {re6: relate_impl_ioapic}.
    Context {re7: relate_impl_in_intr}.
    Context {re8: relate_impl_init}.

    Lemma cons_intr_aux_exist:
      ∀ s habd habd´ labd f,
        cons_intr_aux habd = Some habd´
        → relate_AbData s f habd labd
        → ∃ labd´, cons_intr_aux labd = Some labd´
                         ∧ relate_AbData s f habd´ labd´.
    Proof.
      unfold cons_intr_aux.
      intros.
      exploit relate_impl_iflags_eq; eauto; inversion 1.
      exploit relate_impl_com1_eq; eauto; inversion 1.
      exploit relate_impl_drv_serial_eq; eauto; inversion 1.
      exploit relate_impl_console_eq; eauto; inversion 1.
      exploit relate_impl_init_eq; eauto; inversion 1.
      exploit relate_impl_in_intr_eq; eauto; inversion 1.
      revert H.
      subrewrite.
      subdestruct;
      inv HQ; refine_split´; trivial;
      exploit relate_impl_iflags_eq; eauto; inversion 1;
      exploit relate_impl_com1_eq; eauto; inversion 1;
      exploit relate_impl_drv_serial_eq; eauto; inversion 1;
      exploit relate_impl_console_eq; eauto; inversion 1;
      exploit relate_impl_init_eq; eauto; inversion 1;
      exploit relate_impl_in_intr_eq; eauto; inversion 1;
      unfold_DeviceData;
      destruct (com1 habd); simpl in *;
      inv H4;
      repeat (
      try apply relate_impl_in_intr_update; eauto;
      try apply relate_impl_com1_update; eauto;
      try apply relate_impl_drv_serial_update; eauto;
      try apply relate_impl_console_update; eauto;
      try apply relate_impl_init_update; eauto); eauto.
    Qed.

    Lemma cons_intr_exist:
      ∀ s habd habd´ labd f,
        cons_intr_spec habd = Some habd´
        → relate_AbData s f habd labd
        → ∃ labd´, cons_intr_spec labd = Some labd´
                         ∧ relate_AbData s f habd´ labd´.
    Proof.
      unfold cons_intr_spec; intros.
      exploit relate_impl_iflags_eq; eauto; inversion 1.
      exploit relate_impl_com1_eq; eauto; inversion 1.
      exploit relate_impl_console_eq; eauto; inversion 1.
      exploit relate_impl_drv_serial_eq; eauto; inversion 1.
      exploit relate_impl_lapic_eq; eauto; inversion 1.
      exploit relate_impl_ioapic_eq; eauto; inversion 1.
      exploit relate_impl_in_intr_eq; eauto; inversion 1.
      exploit relate_impl_init_eq; eauto; inversion 1.
      revert H. subrewrite.
      subdestruct.
      exploit lapic_eoi_exist; eauto; inversion 1.
      destruct H15.
      rewrite H15.
      eapply cons_intr_aux_exist; eauto.
    Qed.

    Context {mt1: match_impl_console}.
    Context {mt2: match_impl_com1}.
    Context {mt3: match_impl_drv_serial}.
    Context {mt4: match_impl_lapic}.
    Context {mt5: match_impl_ioapic}.

    Lemma cons_intr_aux_match:
      ∀ s d d´ m f,
        cons_intr_aux d = Some d´
        → match_AbData s d m f
        → match_AbData s d´ m f.
    Proof.
      intros.
      functional inversion H; subst;
      repeat (try apply match_impl_com1_update; eauto;
      try apply match_impl_console_update; eauto).
    Qed.

    Lemma cons_intr_match:
      ∀ s d d´ m f,
        cons_intr_spec d = Some d´
        → match_AbData s d m f
        → match_AbData s d´ m f.
    Proof.
      unfold cons_intr_spec; intros.
      subdestruct; inv H; trivial.
      eapply cons_intr_aux_match; eauto.
      eapply lapic_eoi_match; eauto.
    Qed.

    Context {inv: PreservesInvariants (HD:= data) cons_intr_spec}.
    Context {inv0: PreservesInvariants (HD:= data0) cons_intr_spec}.

    Lemma cons_intr_sim :
      ∀ id,
        sim (crel RData RData) (id ↦ gensem cons_intr_spec)
            (id ↦ gensem cons_intr_spec).
    Proof.
      intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
      exploit cons_intr_exist; eauto 1; intros (labd´ & HP & HM).
      match_external_states_simpl.
      eapply cons_intr_match; eauto.
    Qed.

  End CONS_INTR_SIM.

End OBJ_SIM.