Library IntExitProof

Require Import ucert.
Require Import mathlib.
Require Import OSIntExitPure.
Require Import oscore_common.
Require Import lab.
Open Scope code_scope.
Lemma OSIntExit_proof:
    forall vl p r logicl,
      Some p =
      BuildPreI os_internal OSIntExit
                  vl logicl OSIntExitPre->
      Some r =
      BuildRetI os_internal OSIntExit vl logicl OSIntExitPost->
      exists t d1 d2 s,
        os_internal OSIntExit = Some (t, d1, d2, s) /\
        {|OSQ_spec, GetHPrio, I, r, Afalse|}|- {{p}} s {{Afalse}}.

Close Scope code_scope.