Library OSEventRemoveProof

Require Import ucert.
Open Scope code_scope.
Require Import mathlib.
Require Import OSEventRemovePure.

Ltac hoare_change pos asrt :=
  hoare lift pos%nat pre; apply backward_1 with (P´:=asrt); sep pauto.


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