Library OSSemPendProof

Require Import sem_common.
Require Import sempend_pure.
Require Import lab.
Require Import gen_lemmas.
Open Scope code_scope.

Ltac lzh_find_ret_stmt stmts :=
  match stmts with
    | sseq ?s ?rs =>
      match s with
        | srete _ => constr:(some 1%nat)
        | _ => lzh_find_ret_stmt rs
      end
    | srete _ => constr:(some 1%nat)
    | _ => constr:(none 1%nat)
  end.

Ltac lzh_hoare_if :=
  lzh_hoare_unfold;
  hoare forward;
  match goal with
    | |- {|_, _, _, _, _|} |- {{?p ** [|?v <> Vint32 Int.zero /\
                                       ?v <> Vnull /\
                                       ?v <> Vundef|]}} ?stmts {{_}} =>
      
      let x := lzh_find_ret_stmt stmts in
        match x with
          | some _ => instantiate (1:=Afalse)
          | none _ => idtac
        end;
      hoare_split_pure_all;
      lzh_val_inj_simpl; tryfalse

    | |- {|_, _, _, _, _|} |- {{_}} _ {{_}} =>
      
      hoare forward;
      hoare_split_pure_all;
      lzh_val_inj_simpl; tryfalse
      
    | _ => pauto
  end.

Hint Resolve CltEnvMod.beq_refl: brel .

Lemma sempend_part1:gen_sempend_part1.

Lemma OSSemPendProof:
    forall vl p r,
      Some p =
      BuildPreA´ os_api OSSemPend
                 sem_pendapi vl ->
      Some r =
      BuildRetA´ os_api OSSemPend
                 sem_pendapi vl ->
      exists t d1 d2 s,
        os_api OSSemPend = Some (t, d1, d2, s) /\
        {|OSQ_spec, GetHPrio, I, r, Afalse|}|- {{p}}s {{Afalse}}.
    Ltac lzh_val_inj_simpl_tmp :=
      repeat match goal with
        | |- ?x = ?x /\ ?y = ?y => auto
        | H: context [val_inj] |- _ =>
            simpl in H;
            try unfold Int.notbool in H;
            try rewrite Int.eq_true in H;
            try rewrite Int.eq_false in H;
            simpl in H;
            try rewrite sempend_ltu_ass1 in H;
            try rewrite sempend_ltu_ass2 in H;
            simpl in H
        | H: Vint32 Int.one = Vint32 Int.zero \/ _ |- _=>
            destruct H; tryfalse
        | |- Int.zero <> Int.one =>
            int auto
        | |- Int.one <> Int.zero =>
            int auto
             end.
  Require Import semacc_pure.