Library mcertikos.objects.dev.ObjKeyboard

Require Import Coqlib.
Require Import Maps.
Require Import DeviceStateDataType.
Require Import AbstractDataType.
Require Import Integers.
Require Import Values.
Require Import Constant.
Require Import OracleInstances.

Section OBJ_KeyboardDevice.

  Open Scope Z_scope.

  Import ListNotations.

  Function keymap (a: KeyAction): list Z :=
    match a with
    | Press k ⇒ if zle_le KEY_ESC k KEY_F12 then [k + 1]
                else if zle_le KEY_PAD k KEY_APP then [SCODE_DAUL_KEY; k + 1]
                else if zeq k KEY_PRINT_SCREEN then [SCODE_DAUL_KEY; 42; SCODE_DAUL_KEY; 55]
                else if zeq k KEY_PAUSE then [225; 29; 69; 225; 157; 197]
                else [k]
    | Release k ⇒ if zle_le KEY_ESC k KEY_F12 then [k + 129]
                else if zle_le KEY_PAD k KEY_APP then [SCODE_DAUL_KEY; k + 129]
                else if zeq k KEY_PRINT_SCREEN then [SCODE_DAUL_KEY; 42; SCODE_DAUL_KEY; 170]
                else [k]
    end.

  Function keymap_all (s: list KeyAction) (zs: list Z): list Z :=
    match s with
    | nil ⇒ zs
    | h :: t ⇒ keymap_all t (zs ++ (keymap h))
    end.

  Function keyboard_trans_env (e: KeyboardEvent) (s: KeyboardState): KeyboardState :=
    match e with
    | Keys keys ⇒
      match keys with
      | nil ⇒ s
      | _ :: _ ⇒ s {KbdRxBuf: firstn KEYBOARD_HW_BUF_SIZE (KbdRxBuf s ++ keymap_all keys nil)}
                   {KbdIrq: true}
      end
    end.

  Notation KeyboardDataPort := 96%Z.
  Notation KeyboardCmdPort := 100%Z.

  Function keyboard_trans_cpu (op: DeviceOp) (s: KeyboardState): KeyboardState :=
    match op with
    | OpInput n ⇒
      if zeq n KeyboardDataPort then
        match (KbdRxBuf s) with
        | nil ⇒ s
        | _ :: rxbuf´ ⇒ s {KbdRxBuf: rxbuf´} {KbdIrq: false}
        end
      else
        s
    | OpOutput n v ⇒
      s
    end.


  Function keyboard_in_spec (port: Z) (abd: RData): option (RData × Z) :=
    let log := l1 (kbd abd) in
    let s := s (kbd abd) in
    let s´ := keyboard_trans_env (KeyboardEnv log) s in
    let s´´ := keyboard_trans_cpu (OpInput port) s´ in
    if zeq port KeyboardDataPort then
      Some (abd {kbd: ((kbd abd) {s: s´´} {l1: log + 1})}, hd 0 (KbdRxBuf s´))
    else if zeq port KeyboardCmdPort then
      Some (abd {kbd: ((kbd abd) {s: s´´} {l1: log + 1})}, match (KbdRxBuf s´) with | nil ⇒ 0 | _ ⇒ 1 end)
    else
      None.

End OBJ_KeyboardDevice.

Section OBJ_KeyboardDriver.

  Open Scope Z_scope.

  Function keyboard_scan_spec (abd: RData): option (RData × Z) :=
    match KbdRxBuf (s (kbd abd)) with
    | nil ⇒
      match (KeyboardEnv (l1 (kbd abd)), KeyboardEnv (l1 (kbd abd) + 1)) with
      | (Keys nil, _) ⇒ Some (abd {kbd: (kbd abd) {l1: (l1 (kbd abd) + 1)}}, 256)
      | (Keys s1, Keys nil) ⇒
        let ms1 := keymap_all s1 nil in
        Some (abd {kbd: (kbd abd)
                          {l1: (l1 (kbd abd) + 2)}
                          {s/KbdRxBuf: tl ms1}}, hd 0 ms1)
      | (Keys s1, Keys s2) ⇒
        let ms1 := keymap_all s1 nil in
        let ms2 := keymap_all s2 nil in
        Some (abd {kbd: (kbd abd)
                          {l1: l1 (kbd abd) + 2}
                          {s/KbdRxBuf: tl (firstn KEYBOARD_HW_BUF_SIZE (ms1 ++ ms2))}},
              hd 0 (ms1 ++ ms2))
      end
    | h :: t ⇒
      match (KeyboardEnv (l1 (kbd abd)), KeyboardEnv (l1 (kbd abd) + 1)) with
      | (Keys nil, Keys nil) ⇒
        Some (abd {kbd: (kbd abd)
                          {l1: l1 (kbd abd) + 2}
                          {s/KbdRxBuf: t}}, h)
      | (Keys nil, Keys s2) ⇒
        let ms2 := keymap_all s2 nil in
        Some (abd {kbd: (kbd abd)
                          {l1: l1 (kbd abd) + 2}
                          {s/KbdRxBuf: firstn KEYBOARD_HW_BUF_SIZE (t ++ ms2)}}, h)
      | (Keys s1, Keys nil) ⇒
        let ms1 := keymap_all s1 nil in
        Some (abd {kbd: (kbd abd)
                          {l1: l1 (kbd abd) + 2}
                          {s/KbdRxBuf: firstn KEYBOARD_HW_BUF_SIZE (t ++ ms1)}}, h)
      | (Keys s1, Keys s2) ⇒
        let ms1 := keymap_all s1 nil in
        let ms2 := keymap_all s2 nil in
        Some (abd {kbd: (kbd abd)
                          {l1: l1 (kbd abd) + 2}
                          {s/KbdRxBuf: firstn KEYBOARD_HW_BUF_SIZE (t ++ ms1 ++ ms2)}}, h)
      end
    end.

End OBJ_KeyboardDriver.

Section OBJ_Keyboard_Buf_Concrete.

  Function kbd_buf_init_concrete_spec (abd: RData) : option RData :=
    match (ikern abd, ihost abd, init abd) with
      | (true, true, true) ⇒
        Some (abd {kbd_drv / kbd_rpos_concrete: 0}
                  {kbd_drv / kbd_wpos_concrete: 0})
      | _ ⇒ None
    end.

  Function kbd_buf_write_concrete_spec (c: Z) (abd: RData) : option RData :=
    match (ikern abd, ihost abd, init abd) with
    | (true, true, true) ⇒
      let buf := kbd_buf_concrete (kbd_drv abd) in
      let rpos := kbd_rpos_concrete (kbd_drv abd) in
      let wpos := kbd_wpos_concrete (kbd_drv abd) in
      if zeq ((wpos + 1) mod KEYBOARD_SW_BUF_SIZE) rpos then
        Some (abd {kbd_drv / kbd_buf_concrete: ZMap.set wpos (BufVal c) buf}
                  {kbd_drv / kbd_wpos_concrete: (wpos + 1) mod KEYBOARD_SW_BUF_SIZE}
                  {kbd_drv / kbd_rpos_concrete: (rpos + 1) mod KEYBOARD_SW_BUF_SIZE})
      else
        Some (abd {kbd_drv / kbd_buf_concrete: ZMap.set wpos (BufVal c) buf}
                  {kbd_drv / kbd_wpos_concrete: (wpos + 1) mod KEYBOARD_SW_BUF_SIZE})
    | _ ⇒ None
    end.

  Function kbd_buf_read_concrete_spec (abd: RData): option (RData × Z) :=
    match (ikern abd, ihost abd, init abd) with
    | (true, true, true) ⇒
      let buf := kbd_buf_concrete (kbd_drv abd) in
      let rpos := kbd_rpos_concrete (kbd_drv abd) in
      let wpos := kbd_wpos_concrete (kbd_drv abd) in
      if zeq rpos wpos then
        Some (abd, 0)
      else
        match ZMap.get rpos buf with
        | BufValUndef ⇒ None
        | BufVal c ⇒
          Some (abd {kbd_drv / kbd_rpos_concrete: ((rpos + 1) mod KEYBOARD_SW_BUF_SIZE)}, c)
        end
    | _ ⇒ None
    end.

  Function kbd_buf_wpos_concrete_spec (abd: RData): option Z :=
    match (ikern abd, ihost abd, init abd) with
      | (true, true, true) ⇒
        Some (kbd_wpos_concrete (kbd_drv abd))
      | _ ⇒ None
    end.

End OBJ_Keyboard_Buf_Concrete.

Section OBJ_Keyboard_Buf.

  Function kbd_buf_init_spec (abd: RData) : option RData :=
    match (ikern abd, ihost abd, init abd) with
    | (true, true, true) ⇒
      Some (abd {kbd_drv / shift_toggle: 0}
                {kbd_drv / kbd_buf: nil})
    | _ ⇒ None
    end.

  Import ListNotations.
  Function handle_kbd_buf_write (s: KeyboardDriver) (c: Z) : KeyboardDriver :=
    let b := kbd_buf s in
    if zlt (Zlength b) (KEYBOARD_SW_BUF_SIZE - 1)
    then
      s {kbd_buf: (b ++ [c])}
    else
      s {kbd_buf: skipn 1 (b ++ [c])}.

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

  Function kbd_buf_read_spec (abd: RData): option (RData × Z) :=
    match (ikern abd, ihost abd, init abd) with
    | (true, true, true) ⇒
      match kbd_buf (kbd_drv abd) with
      | nil ⇒ Some (abd, 0)
      | c :: tl ⇒
        Some (abd {kbd_drv / kbd_buf: tl}, c)
      end
    | _ ⇒ None
    end.

End OBJ_Keyboard_Buf.

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

    Context {re1: relate_impl_iflags}.
    Context {re2: relate_impl_kbd}.

    Lemma keyboard_in_exist:
      ∀ s habd habd´ labd port i f,
        keyboard_in_spec port habd = Some (habd´, i)
        → relate_AbData s f habd labd
        → ∃ labd´, keyboard_in_spec port labd = Some (labd´, i)
                         ∧ relate_AbData s f habd´ labd´.
    Proof.
      unfold keyboard_in_spec; intros.
      exploit relate_impl_iflags_eq; eauto; inversion 1.
      exploit relate_impl_kbd_eq; eauto; inversion 1.
      revert H. subrewrite.
      subdestruct;
      inv HQ; refine_split´; trivial; subst;
      repeat (
      try apply relate_impl_kbd_update; eauto).
    Qed.

    Context {mt1: match_impl_com1}.
    Context {mt2: match_impl_kbd}.

    Lemma keyboard_in_match:
      ∀ s d d´ m i f port,
        keyboard_in_spec port d = Some (d´, i)
        → match_AbData s d m f
        → match_AbData s d´ m f.
    Proof.
      unfold keyboard_in_spec; intros. subdestruct; inv H; trivial;
      repeat(
      try eapply match_impl_kbd_update);
      assumption.
    Qed.

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

    Lemma keyboard_in_sim :
      ∀ id,
        sim (crel RData RData) (id ↦ gensem keyboard_in_spec)
            (id ↦ gensem keyboard_in_spec).
    Proof.
      intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
      exploit keyboard_in_exist; eauto 1; intros (labd´ & HP & HM).
      match_external_states_simpl.
      eapply keyboard_in_match; eauto.
    Qed.

  End KEYBOARD_IN_SIM.

End OBJ_SIM.