Library OSSemPostProof

Require Import sem_common.
Require Import sempend_pure.
Require Import sempost_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.

Lemma sempost_part_1: gen_sempost_part_1.

Lemma sempost_part_2: gen_sempost_part_2.

Lemma sempost_part_3: gen_sempost_part_3.

Lemma sempost_part_4: gen_sempost_part_4.

Lemma sempost_part_5: gen_sempost_part_5.

Lemma sempost_part_6: gen_sempost_part_6.

Lemma sempost_part_0: gen_sempost_part_0.
Lemma OSSemPostProof:
  forall vl p r,
    Some p =
    BuildPreA´ os_api OSSemPost
               sem_postapi vl ->
    Some r =
    BuildRetA´ os_api OSSemPost
               sem_postapi vl ->
    exists t d1 d2 s,
      os_api OSSemPost = Some (t, d1, d2, s) /\
      {|OSQ_spec, GetHPrio, I, r, Afalse|} |- {{p}} s {{Afalse}}.