Library mcertikos.dev.Oracle

***********************************************************************
*                                                                     *
*            The CertiKOS Certified Kit Operating System              *
*                                                                     *
*                   The FLINT Group, Yale University                  *
*                                                                     *
*  Copyright The FLINT Group, Yale University.  All rights reserved.  *
*  This file is distributed under the terms of the Yale University    *
*  Non-Commercial License Agreement.                                  *
*                                                                     *
***********************************************************************

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.