Library OSQPendProof

Require Import ucert.
Require Import OSQPendPure.
Require Import lab.
Require Import gen_lemmas.
Open Scope code_scope.

Ltac tl_vl_match_solver := simpl; repeat (erewrite if_true_false_eq_true_intro;eauto);
                           try eapply Zle_imp_le_bool; eauto.

Lemma isptr_zh :
  forall x, isptr x ->
            match x with
              | Vundef => false
              | Vnull => true
              | Vint32 _ => false
              | Vptr _ => true
            end = true.

Lemma OSQPendRightPart2 : gen_OSQPendRightPart2.

Theorem OSQPendRight:
  forall vl p r,
    Some p = BuildPreA´ os_api OSQPend qpendapi vl ->
    Some r = BuildRetA´ os_api OSQPend qpendapi vl ->
    exists t d1 d2 s,
      os_api OSQPend = Some (t, d1, d2, s) /\ {| OSQ_spec, GetHPrio, I, r, Afalse |} |- {{ p }} s {{ Afalse }}.