Library ToyIntProof

Require Import ucert.
Require Import mathlib.
Require Import ToyIntPure.
Require Import oscore_common.
Open Scope code_scope.

Lemma toyisr_proof:
  forall ir si p r,
    Some p = BuildintPre OSToyISR int_spec ir si I ->
    Some r = BuildintRet OSToyISR int_spec ir si I ->
    exists s,
      os_interrupt OSToyISR = Some s /\
      {| OSQ_spec , GetHPrio, I, retfalse, r|}|- {{p}}s {{Afalse}}.
  Require Import Coq.Logic.FunctionalExtensionality.