Library sep_pure

Require Import Coq.Bool.IfProp.
Require Import Coq.Logic.Classical_Prop.
Require Import Recdef.
Require Import Coq.Init.Wf.
Require Import Coq.Arith.Wf_nat.
Require Import Coq.Logic.FunctionalExtensionality.
Require Import inferules.
Require Import seplog_lemmas.
Require Import seplog_tactics.
Require Import memdata.
Require Import memory.
Require Import language.
Require Import opsem.
Require Import assertion.
Require Import hoare_conseq.
Require Import Integers.
Require Import baseTac.
Require Import LibTactics.
Require Import val.
Require Import derivedrules.
Require Import BaseAsrtDef.
Require Import simulation.
Require Import aux_for_hoare_lemmas.
Require Import symbolic_execution.
Require Import hoare_assign.
Require Import BaseAsrtDef.
Require Import inv_prop.
Require Import InternalFunSpec.
Require Import IntLib.
Require Import List.
Require Import can_change_aop_proof.
Require Import type_val_match.
Require Import init_spec.
Require Import os_code_notations.
Require Import os_code_defs.
Require Import os_ucos_h.
Require Import os_time.
Require Import mathsolver.
Set Implicit Arguments.

Open Scope code_scope.

Lemma isptr2_bool_not_vundef : forall v1 v2,
   isptr v1 ->
        isptr v2 ->
        val_inj
          (bool_and (val_inj (notint (val_inj (val_eq v1 Vnull))))
             (val_inj (notint (val_inj (val_eq v2 Vnull))))) <> Vundef.

Lemma isptr2_bool_and : forall v1 v2 ,
        isptr v1 ->
        isptr v2 ->
        val_inj
          (bool_and (val_inj (notint (val_inj (val_eq v1 Vnull))))
             (val_inj (notint (val_inj (val_eq v2 Vnull))))) <>
        Vint32 Int.zero ->
             exists x y, v1 = Vptr x /\ v2 = Vptr y.

Lemma isptr_neq_vundef : forall v, isptr v ->
                                val_inj (val_eq v Vnull) <> Vundef.

Lemma isptr_neq_notint_vundef : forall v, isptr v ->
                                val_inj (notint (val_inj (val_eq v Vnull))) <> Vundef.

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

Lemma ptr_neq_null : forall x, isptr x ->
                                val_inj (val_eq x Vnull) <> Vint32 Int.zero
                                -> x = Vnull.

Lemma isptr_pointer_intro : forall x , isptr x ->
                              ((val_inj (val_eq x Vnull) = Vint32 Int.zero \/
                                val_inj (val_eq x Vnull) = Vnull)) -> exists v, x = Vptr v.

Lemma int32_inj_neq_Vundef: forall x y, val_inj (val_eq (V$x) (V$y)) <> Vundef.

Lemma vptr_inj_neq_Vundef: forall x y, isptr x ->
                                        isptr y ->
                                        val_inj (val_eq x y ) <> Vundef.

Lemma ltu_zero_false_imp_eq_zero :
  forall i,
    Int.ltu Int.zero i = false ->
    i = Int.zero.

Lemma shru_3_lt_8 :
  forall i,
    Int.unsigned i < 64 ->
    Int.unsigned (Int.shru i ($ 3)) < 8.

Lemma GAarray_imp_length :
  forall s x t n vl,
    s |= GAarray x (Tarray t n) vl -> length vl = n.

Lemma LAarray_imp_length :
  forall s x t n vl,
    s |= LAarray x (Tarray t n) vl -> length vl = n.

Lemma GAarray_imp_length_P :
  forall s x t n vl P,
    s |= GAarray x (Tarray t n) vl**P -> length vl = n.

Lemma LAarray_imp_length_P :
  forall s x t n vl,
    s |= LAarray x (Tarray t n) vl -> length vl = n.

Lemma val_inj_not_Vundef_1 :
  forall x,
    type_val_match OS_EVENT ∗ x = true ->
    val_inj (val_eq x Vnull) <> Vundef.

Lemma val_inj_impl_eq :
  forall x y,
    val_inj (val_eq x y) <> Vint32 Int.zero /\
    val_inj (val_eq x y) <> Vnull /\
    val_inj (val_eq x y) <> Vundef ->
    x = y.

Lemma val_inj_impl_Vnull :
  forall x,
    val_inj (val_eq x Vnull) <> Vint32 Int.zero /\
    val_inj (val_eq x Vnull) <> Vnull /\
    val_inj (val_eq x Vnull) <> Vundef ->
    x = Vnull.

Lemma val_inj_impl_Vptr :
  forall x,
    val_inj (val_eq x Vnull) = Vint32 Int.zero \/
    val_inj (val_eq x Vnull) = Vnull ->
    exists a, x = Vptr a.

Lemma bool_type_val_match :
  forall v,
    Some v = Some (V$ 1) \/ Some v = Some (V$ 0) ->
    type_val_match Tint8 v = true.

Lemma val_inj_not_Vundef_2 :
  forall v,
    Some v = Some (V$ 1) \/ Some v = Some (V$ 0) ->
    val_inj (val_eq v (V$ 0)) <> Vundef.

Lemma Int_i2_i_1 :
  forall i2 i,
    (Int.unsigned i2 <=? 65535) = true ->
    true = Int.ltu ($ 0) i2 ->
    (Int.unsigned i <=? 255) = true ->
    (Int.unsigned (i2 -ᵢ $ 1) <=? 65535) = true.

Lemma Int_i2_i_1_iftrue:
  forall i2 i,
    (Int.unsigned i2 <=? 65535) = true ->
    true = Int.ltu ($ 0) i2 ->
    (Int.unsigned i <=? 255) = true ->
    (if Int.unsigned (i2-ᵢ$ 1) <=? Int16.max_unsigned then true else false) =
    true.

Lemma isptr_val_inj_neqvundef : forall x b ofs,
  isptr x -> val_inj
     match x with
     | Vundef => None
     | Vnull => Some (Vint32 Int.zero)
     | Vint32 _ => None
     | Vptr (b2, ofs2) =>
         if peq b b2
         then
          if Int.eq ofs ofs2
          then Some (Vint32 Int.one)
          else Some (Vint32 Int.zero)
         else Some (Vint32 Int.zero)
     end <> Vundef.

Hint Resolve isptr2_bool_and: pauto_lemmas.
Hint Resolve isptr2_bool_not_vundef : pauto_lemmas.
Hint Resolve isptr_val_inj_neqvundef: pauto_lemmas.
Hint Resolve Int_i2_i_1 Int_i2_i_1_iftrue : pauto_lemmas.
Hint Resolve isptr_neq_vundef : pauto_lemmas.
Hint Resolve isptr_neq_notint_vundef : pauto_lemmas.
Hint Resolve isptr_match_eq_true : pauto_lemmas.
Hint Resolve ptr_neq_null : pauto_lemmas.
Hint Resolve isptr_pointer_intro : pauto_lemmas.
Hint Resolve int32_inj_neq_Vundef : pauto_lemmas.
Hint Resolve vptr_inj_neq_Vundef : pauto_lemmas.
Hint Resolve ltu_zero_false_imp_eq_zero : pauto_lemmas.
Hint Resolve shru_3_lt_8 : pauto_lemmas.
Hint Resolve val_inj_impl_eq : pauto_lemmas.
Hint Resolve bool_type_val_match : pauto_lemmas.
Hint Resolve val_inj_not_Vundef_2 : pauto_lemmas.
Hint Resolve val_inj_impl_Vptr : pauto_lemmas.
Hint Resolve val_inj_not_Vundef_1 : pauto_lemmas.
Hint Resolve val_inj_impl_Vnull : pauto_lemmas.
Hint Resolve val_inj_impl_eq : pauto_lemmas.


Lemma good_frm_star : forall p q, GoodFrm p -> GoodFrm q ->
                                  GoodFrm (p ** q).

Lemma good_frm_ex : forall (t:Type) (p : t -> asrt),
                      (forall x, GoodFrm (p x)) -> GoodFrm (EX x, p x).

Lemma good_frm_aemp : GoodFrm ( Aemp).

Lemma good_frm_lenv : forall x , GoodFrm ( A_dom_lenv x).

Lemma good_frm_astruct´: forall l dls vl, GoodFrm (Astruct´ l dls vl).

Lemma good_frm_astruct : forall l t vl , GoodFrm (Astruct l t vl ).

Lemma good_frm_sllseg : forall vl head tail t next,
                          GoodFrm (sllseg head tail vl t next).

Lemma good_frm_sll : forall head vl t next, GoodFrm (sll head vl t next).

Lemma good_frm_dllseg : forall vl head hp tail tn t next pre,
                          GoodFrm (dllseg head hp tail tn vl t next pre).

Lemma good_frm_tcbdllseg : forall vl head hp tail tn ,
                             GoodFrm(tcbdllseg head hp tail tn vl).

Lemma good_frm_array´ : forall x n t vl, GoodFrm (Aarray´ x n t vl).

Lemma good_frm_array : forall x t vl, GoodFrm (Aarray x t vl).

Lemma good_frm_garray: forall l t n vl,
                         GoodFrm (GAarray l (Tarray t n) vl).

Lemma good_frm_pure: forall (p:Prop), GoodFrm (Apure p).

Lemma good_frm_absop : forall a b, GoodFrm (Aabsdata a b).

Lemma good_frm_gvar: forall x t v, GoodFrm (GV x @ t |-> v).

Hint Resolve good_frm_gvar : good_frm_lemmas.

Lemma good_frm_lvar: forall x t v, GoodFrm (LV x @ t |-> v).

Hint Resolve good_frm_lvar : good_frm_lemmas.

Lemma good_frm_ptr : forall x t v, GoodFrm (PV x@t |-> v).
Hint Resolve good_frm_aemp : good_frm_lemmas.
Hint Resolve good_frm_ptr : good_frm_lemmas.
Hint Resolve good_frm_astruct´ : good_frm_lemmas.
Hint Resolve good_frm_astruct : good_frm_lemmas.
Hint Resolve good_frm_sllseg : good_frm_lemmas.
Hint Resolve good_frm_sll : good_frm_lemmas.
Hint Resolve good_frm_dllseg : good_frm_lemmas.
Hint Resolve good_frm_tcbdllseg : good_frm_lemmas.
Hint Resolve good_frm_dllseg : good_frm_lemmas.
Hint Resolve good_frm_tcbdllseg : good_frm_lemmas.
Hint Resolve good_frm_array : good_frm_lemmas.
Hint Resolve good_frm_garray: good_frm_lemmas.
Hint Resolve good_frm_pure : good_frm_lemmas.
Hint Resolve good_frm_absop : good_frm_lemmas.
Hint Resolve good_frm_array´ : good_frm_lemmas.
Hint Resolve good_frm_array : good_frm_lemmas.
Hint Resolve good_frm_garray : good_frm_lemmas.
Hint Resolve good_frm_lenv : good_frm_lemmas.

Ltac good_frm_sovler :=
  match goal with
   | |- GoodFrm ?p =>
     match p with
         | Aexists _ => apply good_frm_ex; intros; good_frm_sovler
         | ?p1 ** ?p2 => apply good_frm_star; good_frm_sovler
         | _ => first [auto with good_frm_lemmas | simpl; auto]
     end
   | _ => idtac
end.

Lemma good_frm_AOSEventTbl : forall x0 v0, GoodFrm (AOSEventTbl x0 v0).

Hint Resolve good_frm_AOSEventTbl : good_frm_lemmas.

Lemma good_frm_node : forall v vl t , GoodFrm (node v vl t).

Hint Resolve good_frm_node : good_frm_lemmas.

Lemma good_frm_AOSEvent : forall a0 v x, GoodFrm
                                                    (AOSEvent a0 v x).

Hint Resolve good_frm_AOSEvent : good_frm_lemmas.

Lemma good_frm_AOSQBlk : forall x1 v2 x2, GoodFrm (AOSQBlk x1 v2 x2).

Hint Resolve good_frm_AOSQBlk : good_frm_lemmas.

Lemma good_frm_AOSQCtr : forall x1 v2, GoodFrm (AOSQCtr x1 v2).

Hint Resolve good_frm_AOSQCtr : good_frm_lemmas.

Lemma good_frm_AMsgData : forall x v1 x1 x2, GoodFrm ( AMsgData x v1 x1 x2).

Hint Resolve good_frm_AMsgData : good_frm_lemmas.

Lemma good_frm_amsgnode : forall p a b v1 v2 v3 l,
                            GoodFrm (AEventNode p a b (DMsgQ l v1 v2 v3)).

Hint Resolve good_frm_amsgnode : good_frm_lemmas.

Lemma good_frm_mqsllseg : forall p n l msgqls, GoodFrm (evsllseg p n l msgqls).

Hint Resolve good_frm_mqsllseg : good_frm_lemmas.

Lemma good_frm_ecbfslleg : forall ls x y ,
                               GoodFrm (ecbf_sllseg x y ls OS_EVENT V_OSEventListPtr).

Hint Resolve good_frm_ecbfslleg : good_frm_lemmas.

Lemma good_frm_ecbfsll: forall ls x ,
                               GoodFrm (ecbf_sll x ls OS_EVENT V_OSEventListPtr).

Hint Resolve good_frm_ecbfsll : good_frm_lemmas.

Lemma good_frm_AOSEventFreeList: forall x ,
                                   GoodFrm (AOSEventFreeList x).

Hint Resolve good_frm_AOSEventFreeList : good_frm_lemmas.

Lemma good_frm_qblkf_sllseg : forall x y qblkl, GoodFrm (qblkf_sllseg x y qblkl OS_Q_FREEBLK V_nextblk).

Hint Resolve good_frm_qblkf_sllseg : good_frm_lemmas.

Lemma good_frm_qblkf_sll : forall x qblkl, GoodFrm (qblkf_sll x qblkl OS_Q_FREEBLK V_nextblk).

Hint Resolve good_frm_qblkf_sll : good_frm_lemmas.

Lemma good_frm_AOSQFreeList: forall x ,
                               GoodFrm (AOSQFreeList x ).

Hint Resolve good_frm_AOSQFreeList : good_frm_lemmas.

Lemma good_frm_AOSQFreeBlk : forall qblkl, GoodFrm (AOSQFreeBlk qblkl).

Hint Resolve good_frm_AOSQFreeBlk : good_frm_lemmas.


Lemma good_frm_EventList´ : forall qptrl msgql,
                               GoodFrm ((EX p : val,
       GV OSEventList @ OS_EVENT∗ |-> p ** evsllseg p Vnull qptrl msgql)).

Hint Resolve good_frm_EventList´ : good_frm_lemmas.

Lemma good_frm_AMsgQList : forall qptrl msgql mqls tcbls,
                             GoodFrm (AECBList qptrl msgql mqls tcbls ).

Hint Resolve good_frm_AMsgQList : good_frm_lemmas.

Lemma good_frm_AOSMapTbl : GoodFrm AOSMapTbl.

Hint Resolve good_frm_AOSMapTbl : good_frm_lemmas.

Lemma good_frm_AOSUnMapTbl : GoodFrm AOSUnMapTbl.

Hint Resolve good_frm_AOSUnMapTbl : good_frm_lemmas.

Lemma good_frm_AOSTCBPrioTbl: forall ptbl rtbl tcbls vhold,
                                GoodFrm (AOSTCBPrioTbl ptbl rtbl tcbls vhold).

Hint Resolve good_frm_AOSTCBPrioTbl : good_frm_lemmas.

Lemma good_frm_AOSIntNesting : GoodFrm AOSIntNesting.

Hint Resolve good_frm_AOSIntNesting : good_frm_lemmas.

Lemma good_frm_AOSTime : forall t,GoodFrm (AOSTime t).

Hint Resolve good_frm_AOSTime : good_frm_lemmas.

Lemma good_frm_AGVars : GoodFrm AGVars.

Hint Resolve good_frm_AGVars : good_frm_lemmas.

Lemma good_frm_AOSTCBList: forall x1 x2 x3 x4 x5 x6 x7,
                             GoodFrm (AOSTCBList x1 x2 x3 x4 x5 x6 x7).

Hint Resolve good_frm_AOSTCBList : good_frm_lemmas.

Lemma good_frm_AOSTCBFreeList: forall x1 x2,
                             GoodFrm (AOSTCBFreeList x1 x2).

Hint Resolve good_frm_AOSTCBFreeList : good_frm_lemmas.

Lemma good_frm_AOSRdyTbl : forall vl,
                               GoodFrm (AOSRdyTbl vl).

Hint Resolve good_frm_AOSRdyTbl : good_frm_lemmas.

Lemma good_frm_AOSRdyGrp : forall vl,
                               GoodFrm (AOSRdyGrp vl).

Hint Resolve good_frm_AOSRdyGrp : good_frm_lemmas.

Lemma good_frm_AOSRdyTblGrp : forall rtbl rgrp,
                               GoodFrm (AOSRdyTblGrp rtbl rgrp).

Hint Resolve good_frm_AOSRdyTblGrp : good_frm_lemmas.

Ltac pauto´ :=
  match goal with

  | H : _ |- {| _ , _ , _ , _, _ |}|- {{ _ }} _ {{ _ }} => idtac
  | H : _ |- _ |= _ => idtac
  | H : false = (Int.unsigned _ <=? 65535) |- _ =>
    erewrite Int_i2_i_1 in H; eauto; inverts H
  | H : (Int.unsigned _ <=? 65535) = false |- _ =>
    erewrite Int_i2_i_1 in H; eauto; inverts H
  | H: _ |- ?x = ?x => reflexivity
  | H:?x <= ?y |- _ => apply Zle_imp_le_bool in H; pauto´
  | H: context [Byte.max_unsigned] |- _ =>
    rewrite byte_max_unsigned_val in H; pauto´
  | H:_ |- context [Byte.max_unsigned] =>
    rewrite byte_max_unsigned_val; pauto´
  | H: context [Int16.max_unsigned] |- _ =>
    rewrite int16_max_unsigned_val in H; pauto´
  | H:_ |- context [Int16.max_unsigned] =>
    rewrite int16_max_unsigned_val; pauto´
  | H: context [Int.max_unsigned] |- _ =>
    rewrite max_unsigned_val in H; pauto´
  | H:_ |- context [Int.max_unsigned] =>
    rewrite max_unsigned_val ; pauto´
  | H: context [if ?x then _ else _] |- _ =>
    let Hr := fresh in remember x as Hr; destruct Hr; pauto´
  | H:_ |- _ /\ _ => splits; pauto´
  | H:_ |- struct_type_vallist_match _ _ => simpl;splits;pauto´
  | H:_ |- rule_type_val_match _ _ = true => simpl rule_type_val_match; pauto´

  | |- can_change_aop _ => can_change_aop_solver || auto
  | |- GoodFrm _ => good_frm_sovler || auto
  | H:_ |- context [if ?x then _ else _] =>
           let Hr := fresh in
            remember x as Hr; destruct Hr ; pauto´
  
  | H: _ |- ?t (_ :: _) = Some _ => try unfold t; simpl ; auto
  | H: _ |- _ => auto || eauto || auto with pauto_lemmas
                 || eauto with pauto_lemmas || intuition eauto
 

 end.

Ltac unfold_field_fun´ :=
  try unfold V_OSQPtr in *;
  try unfold V_OSEventListPtr in *;
  try unfold V_OSTCBNext in *;
  try unfold V_OSTCBPrev in *;
  try unfold V_OSTCBEventPtr in *;
  try unfold V_OSTCBMsg in *;
  try unfold V_OSTCBDly in *;
  try unfold V_OSTCBStat in *;
  try unfold V_OSTCBPrio in *;
  try unfold V_OSTCBX in *;
  try unfold V_OSTCBY in *;
  try unfold V_OSTCBBitX in *;
  try unfold V_OSTCBBitY in *;
  try unfold V_OSEventType in *;
  try unfold V_OSEventGrp in *;
  try unfold V_OSEventCnt in *;
  try unfold V_OSEventPtr in *;
  try unfold V_OSQStart in *;
  try unfold V_OSQEnd in *;
  try unfold V_OSQIn in *;
  try unfold V_OSQOut in *;
  try unfold V_OSQSize in *;
  try unfold V_OSQEntries in *;
  try unfold V_qfreeblk in *;
  try unfold V_nextblk in *;
  try unfold V_next in *;
  try unfold V_qeventptr in *.

Ltac pauto :=
 unfold_field_fun´; simpl nth_val in *;
  repeat match goal with
           | H : Some _ = Some _ |- _ => inverts H
           | H : Vptr _ = Vptr _ |- _ => inverts H
           | H : Vint32 _ = Vint32 _ |- _ => inverts H
           | _ => idtac
         end;
  try solve [auto || eauto || auto
             with pauto_lemmas
                    || eauto with pauto_lemmas || pauto´].

Ltac cauto :=
  match goal with
  | H : context [ GAarray ?id (Tarray ?t ?n) ?vl ] |- context [ length ?vl ] =>
    let H100 := fresh in
    assert (length vl = n) as H100
        by (sep destroy H;
            match goal with
            | H0 : _ |= GAarray id (Tarray t n) vl |- _ => apply GAarray_imp_length in H0; exact H0
            end); rewrite H100; clear H100; simpl; cauto
  | H : context [ LAarray ?id (Tarray ?t ?n) ?vl ] |- context [ length ?vl ] =>
    let H100 := fresh in
    assert (length vl = n) as H100
        by (sep destroy H;
            match goal with
            | H0 : _ |= GAarray id (Tarray t n) vl |- _ => apply LAarray_imp_length in H0; exact H0
            end); rewrite H100; clear H100; simpl; cauto
  | H : Int.ltu Int.zero ?i = false |- ?i = Int.zero => apply ltu_zero_false_imp_eq_zero in H; auto
  | |- Int.unsigned (Int.shru _ ($ 3)) < 8 => apply shru_3_lt_8; try omega
  | |- (Z.to_nat _ < _)%nat =>
    apply Nat2Z.inj_lt; rewrite Z2Nat.id; [ cauto | clear; int auto ]
  | _ => idtac
  end.

Close Scope code_scope.