Library mcertikos.objects.dev.Oracle

Require Import Coqlib.
Require Import List.
Require Import Bool.

Module Type Event.
  Parameter T: Type.
  Parameter d: T.
End Event.

Module Type Oracle.
  Parameter Time: Set.
  Parameter Entry: Type.
  Parameter Tape: Type.

  Parameter span: Time.
  Parameter tlt: Time → Time → Prop.
  Parameter tle: Time → Time → Prop.
  Parameter empty: Tape.
  Parameter default: Entry.

  Parameter get: Time → Tape → option Entry.
  Parameter valid: Tape → Prop.

  Axiom empty_def: ∀ t:Time,
      get t empty = None.

  Axiom order: ∀ a b: Time,
      {tlt a b} + {a = b} + {¬tle a b}.

  Axiom valid_range: ∀ (t: Time) (l: Tape),
      valid l →
      tlt t span →
      ∃ e,
        get t l = Some e.

End Oracle.