Library OSEventTaskRdy

Require Import ucert.
Require Import mathlib.
Require Import OSEventTaskRdyPure.
Require Import lab.
Require Import oscore_common.
Open Scope code_scope.

Ltac rtmatch_solve:=
  apply true_if_else_true;
  apply Zle_is_le_bool;
  try rewrite byte_max_unsigned_val; try rewrite max_unsigned_val;
  try omega.

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

Close Scope code_scope.