Library OSEventWaitListInitProof

Require Import ucert.
Require Import mathlib.

Open Scope code_scope.

Ltac forwardwith H :=
  rewrite Int.mul_one in *; unfold Int.one; rewrite H in *;
  hoare forward;
  [int auto | rewrite Zdiv_1_r;
     eauto;
     int auto | simpl ; int auto ..];try int auto.

Lemma OSEventWaitListInit_proof:
    forall vl p r ll,
      Some p =
      BuildPreI os_internal OS_EventWaitListInit
                  vl ll OS_EventWaitListInitPre ->
      Some r =
      BuildRetI os_internal OS_EventWaitListInit vl ll OS_EventWaitListInitPost ->
      exists t d1 d2 s,
        os_internal OS_EventWaitListInit = Some (t, d1, d2, s) /\
        {|OSQ_spec , GetHPrio, I, r, Afalse|}|- {{p}} s {{Afalse}}.