Library TimeIntProof

Require Import ucert.
Require Import OSTimeTickPure.
Require Import oscore_common.
Open Scope code_scope.

Lemma timetickisr_proof:
  forall ir si p r,
    Some p = BuildintPre OSTickISR int_spec ir si I ->
    Some r = BuildintRet OSTickISR int_spec ir si I ->
    exists s,
      os_interrupt OSTickISR = Some s /\
      {| OSQ_spec , GetHPrio, I, retfalse, r|}|- {{p}}s {{Afalse}}.
  Require Import common.