Library OSSchedProof

Require Import ucert.
Require Import mathlib.
Require Import oscore_common.

Open Scope code_scope.

Lemma OSSched_proof:
    forall vl p r logicl,
      Some p =
      BuildPreI os_internal OS_Sched
                  vl logicl OS_SchedPre->
      Some r =
      BuildRetI os_internal OS_Sched vl logicl OS_SchedPost->
      exists t d1 d2 s,
        os_internal OS_Sched = Some (t, d1, d2, s) /\
        {|OSQ_spec , GetHPrio, I, r, Afalse|}|- {{p}} s {{Afalse}}.