Library mcertikos.objects.dev.OracleInstances

Require Import Coqlib.
Require Import Integers.
Require Export FlatMemory.
Require Export Asm.
Require Import DeviceStateDataType.
Require Import Values.
Require Import Constant.
Require Import LOracle.
Require Import AbstractDataType.
Require Import AuxStateDataType.
Require Import Maps.
Require Import ListLemma.

Open Scope Z_scope.

Parameter LEnv : ∀ ET: Type, Z → ET.

Section DeviceEvent.

  Inductive SerialEvent :=
  | NullEvent
  
  | SerialRecv (s: list Z)
  | SerialSendComplete
  | SerialPlugin
  .

  Inductive KeyboardEvent :=
  | Keys (keys: list KeyAction)
  .

End DeviceEvent.

Definition KeyboardModel (a: KeyAction) :=
  match a with
  | Press k ⇒ 0 ≤ k ≤ 101
  | Release k ⇒ 0 ≤ k ≤ 101
  end.

Module SerialEventT <: Event.
Definition T := SerialEvent.
Definition d := NullEvent.
End SerialEventT.

Module KeyboardEventT <: Event.
Definition T := KeyboardEvent.
Definition d := (Keys nil).
End KeyboardEventT.

Module SerialOracle := LOracle SerialEventT.
Module KeyboardOracle := LOracle KeyboardEventT.

Definition SerialEnv := LEnv SerialEvent.
Definition KeyboardEnv := LEnv KeyboardEvent.

Function is_relate_tx (e: SerialEvent) : bool :=
  match e with
  | NullEvent ⇒ false
  | SerialRecv _ ⇒ false
  | SerialSendComplete ⇒ true
  | SerialPlugin ⇒ false
  end.

Function is_relate_rx (e: SerialEvent) : bool :=
  match e with
  | NullEvent ⇒ false
  | SerialRecv _ ⇒ true
  | SerialSendComplete ⇒ false
  | SerialPlugin ⇒ false
  end.

Module OracleInvariants.
  Parameter serial_send_complete_bound:
    ∀ d,
      d.(com1).(s).(TxBuf) ≠ nil →
      ∃ t,
        0 ≤ t < 12800 ∧
        (∀ n, 0 ≤ n < t → SerialEnv ((l2 (com1 d)) + n) = NullEvent) ∧
        SerialEnv ((l2 (com1 d)) + t) = SerialSendComplete.

  Parameter serial_recv_limit:
    ∀ t str,
      SerialEnv t = SerialRecv str →
      (str ≠ nil ∧
       0 < Zlength str ≤ 12 ∧
       Forall isChar str ∧
       ∀ n, n ≤ (Zlength str) × 2 + 5 →
            SerialEnv (t + n) = NullEvent).

  Parameter serial_active_on_boot:
    ∃ t, t < 0 ∧ SerialEnv t = SerialPlugin.

  Parameter keyboard_recv_limit :
    ∀ t s,
      KeyboardEnv t = Keys s →
      s ≠ nil →
      (0 < Zlength s ≤ 6 ∧
       Forall KeyboardModel s ∧
       ∀ n, n ≤ (Zlength s) × 2 + 5 →
            KeyboardEnv (t + n) = Keys nil).

End OracleInvariants.