Library OSTimeTickProof

Require Import ucert.
Require Import mathlib.
Require Import OSTimeTickPure.
Require Import OSTimeDlyPure.
Require Import common.
Require Import oscore_common.

Open Scope code_scope.

Lemma OSTimeTick_proof:
    forall vl p r logicl,
      Some p =
      BuildPreI os_internal OSTimeTick
                  vl logicl OSTimeTickPre ->
      Some r =
      BuildRetI os_internal OSTimeTick vl logicl OSTimeTickPost ->
      exists t d1 d2 s,
        os_internal OSTimeTick = Some (t, d1, d2, s) /\
        {|OSQ_spec , GetHPrio, I, r, Afalse|}|- {{p}} s {{Afalse}}.
  Ltac init_spec´ :=
  intros; init_retspec; init_prespec; eapply backward_rule1;
   [ apply Aop_Aop´_eq´ | idtac ];
   (let H := fresh in
    eapply r_conseq_rule;
     [ intros ? ? H; apply Aop_Aop´_eq; exact H
     | intros ? H; exact H
     | idtac ]; type_val_match_elim).