Library absop_rules

Require Import include.
Require Import memory.
Require Import memdata.
Require Import assertion.
Require Import absop.
Require Import simulation.
Require Import language.
Require Import opsem.
Require Import os_program.
Require Import os_spec.
Require Import inferules.
Require Import os_code_notations.
Require Import os_code_defs.
Require Import os_ucos_h.
Require Import os_time.
Require Import baseTac.
Require Import auxdef.
Require Import seplog_lemmas.
Require Import seplog_tactics.
Require Import derivedrules.
Require Import hoare_conseq.
Require Import symbolic_execution.
Require Import hoare_assign.
Require Import hoare_lemmas.
Require Import BaseAsrtDef.
Require Import inv_prop.
Require Import InternalFunSpec.
Require Import IntLib.
Require Import List.
Require Import can_change_aop_proof.
Require Import cancel_absdata.
Require Import sep_pure.
Require Import type_val_match.
Require Import hoare_tactics.

Lemma eqdom_same:forall O, eqdomO O O.

Lemma eqtid_same : forall O, tidsame O O.

Definition eqtls i x y :=
  match i with
    | abtcblsid => match x,y with
                     | abstcblist tls, abstcblist tls´ => eqdomtls tls tls´
                     | _ , _ => False
                   end
    | _ => True
  end.

Lemma tls_get_set_indom:
  forall tcbls ct x y,
    TcbMod.get tcbls ct = Some x ->
    eqdomtls tcbls (TcbMod.set tcbls ct y).

Lemma abst_get_set_eqdom:
  forall O x y z,
    OSAbstMod.get O x = Some y ->
    eqtls x y z ->
    eqdomO O (OSAbstMod.set O x z).

Lemma tidsame_set:
  forall O x y,
    x <> curtid ->
    tidsame O (OSAbstMod.set O x y).

Lemma specstep_merge_emp:
  forall r O r´ O´,
    spec_step r (OSAbstMod.merge O empabst) r´ (OSAbstMod.merge O´ empabst) ->
    spec_step r O r´ O´.

Lemma hmstep_merge_emp:
  forall r O r´ O´,
    hmstep r (OSAbstMod.merge O empabst) r´ (OSAbstMod.merge O´ empabst) ->
    hmstep r O r´ O´.

Hint Resolve eqdom_same eqtid_same OSAbstMod.disj_emp_r OSAbstMod.disj_emp_l.

Open Scope code_scope.

Lemma OSTimeGet_high_level_step :
  forall P mqls tcbls t ct ,
    can_change_aop P ->
    absinfer (<|| tmgetcode nil ||> ** HECBList mqls ** HTCBList tcbls ** HTime t ** HCurTCB ct ** P)
           (<|| END (Some (Vint32 t)) ||> ** HECBList mqls ** HTCBList tcbls ** HTime t ** HCurTCB ct ** P).


Lemma OSTimeDly_high_level_step_1 :
  forall i P,
    i = Int.zero ->
    can_change_aop P ->
    absinfer (<||tmdlycode (Vint32 i :: nil)||> ** P )
           ( <|| END None ||> ** P).

Lemma OSTimeDly_high_level_step_2 :
  forall i P ecbls tcbls t ct pri msg,
    TcbMod.get tcbls ct = Some (pri, rdy, msg) ->
    Int.ltu Int.zero i = true ->
    can_change_aop P ->
    absinfer (<||tmdlycode (Vint32 i :: nil)||> ** HECBList ecbls ** HTCBList tcbls ** HTime t ** HCurTCB ct ** P)
             ( <|| isched;; END None ||> ** HECBList ecbls ** HTCBList (TcbMod.set tcbls ct (pri, wait os_stat_time i, msg)) ** HTime t ** HCurTCB ct ** P).


Lemma OSTimeDly_high_level_step_4 :
  forall i P ecbls tcbls t ct st msg,
    TcbMod.get tcbls ct = Some (Int.repr OS_IDLE_PRIO, st, msg) ->
    can_change_aop P ->
    absinfer (<||tmdlycode (Vint32 i :: nil)||> ** HECBList ecbls ** HTCBList tcbls ** HTime t ** HCurTCB ct ** P)
             (<|| END None ||> ** HECBList ecbls ** HTCBList tcbls ** HTime t ** HCurTCB ct ** P).

Lemma OSTimeDly_high_level_step_3 :
  forall i P ecbls tcbls t ct pri st msg,
    TcbMod.get tcbls ct = Some (pri, st, msg) ->
    ~ (st =rdy) ->
    Int.ltu Int.zero i = true ->
    can_change_aop P ->
    absinfer (<||tmdlycode (Vint32 i :: nil)||> ** HECBList ecbls ** HTCBList tcbls ** HTime t ** HCurTCB ct ** P)
             (<|| END None ||> ** HECBList ecbls ** HTCBList tcbls ** HTime t ** HCurTCB ct ** P).

Ltac hoare_forward_abscsq step:=
  hoare_abscsq;[ eapply step;[can_change_aop_solver | simpl;pauto] | ].

Close Scope code_scope.