Library C_seplog

Require Import ssreflect ssrbool.
Require Import ZArith_ext Lists_ext.
Require Import machine_int.
Import MachineInt.
Require Import C_types C_expr C_bipl C_cmd.

Local Open Scope heap_scope.
Local Open Scope minC_expr_scope.
Local Open Scope minC_cmd_scope.
Local Open Scope minC_assert_scope.
Local Open Scope minC_types.

Definition wp_assign (t : typ) (x : var) (e : exp) (P : assert) : assert :=
  fun s h => exists v, [ e ]_ s = Some v /\
    typof s (var_e x) =ot _ctxt s ot= t /\
    typof s e =ot _ctxt s ot= t /\
    P (store_upd x v s) h.

Definition wp_lookup tx (x : var) (e : exp) (P : assert) : assert := fun s h =>
  wf_tstore (_tstore s) /\
  typof s (var_e x) =ot _ctxt s ot= tx /\
  typof s e =ot _ctxt s ot= ptyp tx /\
  exists p, [ e ]_s = Some (pval p) /\
    exists v, heap_get (Zabs_nat (u2Z p)) tx h = Some v /\
      P (store_upd x v s) h.

Definition wp_mutation (e e' : exp) (P : assert) : assert := fun s h =>
  wf_tstore (_tstore s) /\
  exists p, [ e ]_ s = Some (pval p) /\
    exists t, typof s e =ot _ctxt s ot= ptyp t /\
      exists v, heap_get (Zabs_nat (u2Z p)) t h = Some v /\
        exists v', [ e' ]_ s = Some v' /\
          typof s e' =ot (_ctxt s) ot= t /\
          P s (heap_upd (Zabs_nat (u2Z p)) v' t h).

Definition wp_malloc t (x : var) (wft_t : wft t) (e : exp) (P : assert) : assert :=
  fun s h =>
    typof s (var_e x) =ot _ctxt s ot= ptyp t /\
    cover (_ctxt s) t /\
    complete (_ctxt s) /\
    forall a (lst : list exp) v,
      h # ctrl a ->
      seq_ext.dis (hp.dom h) (seq_ext.ran a (Zabs_nat (u2Z v) * sizeof t)) ->
      seq_ext.dis (seq_ext.ran a (Zabs_nat (u2Z v) * sizeof t)) (hp.dom (ctrl a)) ->
      [ e ]_ s = Some (bval32 v) ->
      List.length lst = Zabs_nat (u2Z v) ->
      block_len _ (ctrl a) (refl_equal _) = (List.length lst * sizeof t)%nat ->
      (((fun _ h => h = ctrl a) **
        cst_pe wft_t (Z2u ptr_len (Z_of_nat a)) |% t %> lst) -*
      wp_assign (ptyp t) x (cst_pe wft_t (Z2u ptr_len (Z_of_nat a))) P) s h.

Definition wp_free (e : exp) (P : assert) := fun s h => exists p,
    [ e ]_s = Some (pval p) /\
    ctrl (Zabs_nat (u2Z p)) [<=m] h /\
    incl (seq (Zabs_nat (u2Z p)) (Block_len (ctrl (Zabs_nat (u2Z p))))) (seq_ext.s2l (hp.dom h)) /\
    P s (h [\m]
      seq_ext.l2s (List.seq (Zabs_nat (u2Z p)) (Block_len (ctrl (Zabs_nat (u2Z p))))) [\m]
      hp.dom (ctrl (Zabs_nat (u2Z p)))).

Inductive hoare0 : assert -> cmd0 -> assert -> Prop :=
| hoare0_skip: forall P, hoare0 P skip P
| hoare0_assign : forall P t x e, hoare0 (wp_assign t x e P) (x <- e) P
| hoare0_lookup : forall P tx x e, hoare0 (wp_lookup tx x e P) (x <-* e) P
| hoare0_mutation : forall P e e', hoare0 (wp_mutation e e' P) (e *<- e') P
| hoare0_malloc : forall P tx (x : var) e (H : wft (tx)),
  hoare0 (wp_malloc tx x H e P) (x <-malloc e) P
| hoare0_free : forall P (e : exp), hoare0 (wp_free e P) (free e) P.

Notation "'hoare_semantics'" :=
  (@while.hoare_semantics store hp.t _ exec0 _ (fun eb s => [ eb ]b_ (fst s))) : minC_hoare_scope.

Local Open Scope minC_hoare_scope.

Require Import eqtype.

Lemma soundness0 : forall (P Q : assert) c,
  hoare0 P c Q -> hoare_semantics P c Q.

Notation "'wp_semantics'" := (@while.wp_semantics store hp.t _ exec0 _ (fun eb s => [ eb ]b_ (fst s)))
  : temp_minC_hoare_scope.

Notation "{{ P }} c {{ Q }}" := (while.hoare store hp.t
  cmd0 _ (fun eb s => [ eb ]b_ (fst s)) (hoare0) P c Q) (at level 82, no associativity) : temp_minC_hoare_scope.

Axiom wp0 : cmd0 -> assert -> assert.

Axiom wp0_no_err : forall s h c P, wp0 c P s h -> ~ (Some (s, h) -- c ----> None).

Local Open Scope temp_minC_hoare_scope.

Axiom wp_semantics_sound0 : forall (c:cmd0) P, {{ wp_semantics c P }} c {{ P }}.


Module MINC_Hoare <: while.WHILE_HOARE.

Include MINC_Semop.

Definition assert := store -> heap -> Prop.

Definition wp0 : cmd0 -> assert -> assert := wp0.
Definition wp0_no_err : forall s h c P, wp0 c P s h -> ~ (Some (s,h) -- c ----> None) := wp0_no_err.

Definition hoare0 : assert -> cmd0 -> assert -> Prop := hoare0.

Definition hoare : assert -> cmd -> assert -> Prop := @while.hoare store heap
  cmd0 expr_b eval_b hoare0.

Definition soundness0 : forall P Q c, hoare0 P c Q -> hoare_semantics P c Q := soundness0.

Definition wp_semantics_sound0 : forall (c:cmd0) P, {{ wp_semantics c P }} c {{ P }} :=
  fun c => wp_semantics_sound0 c.

End MINC_Hoare.


Local Close Scope temp_minC_hoare_scope.

Notation "{{ P }} c {{ Q }}" := (@while.hoare store hp.t
  cmd0 bexp (fun eb s => [ eb ]b_ (fst s)) (hoare0) P c Q) (at level 82, no associativity) : minC_hoare_scope.

Module minc_hoare_prop_m := while.While_Hoare_Prop MINC_Hoare.

Lemma hoare_assign' : forall t (Q P : assert) x e,
  P ===> wp_assign t x e Q -> {{ P }} x <- e {{ Q }}.

Lemma hoare_assign : forall t R P Q x e c, P ===> wp_assign t x e R ->
  {{ R }} c {{ Q }} -> {{ P }} x <- e ; c {{ Q }}.

Lemma hoare_lookup' : forall t (Q P : assert) x e,
  P ===> (wp_lookup t x e Q) -> {{ P }} x <-* e {{ Q }}.

Lemma hoare_lookup_back : forall t x e P,
  {{ fun s h => wf_tstore (_tstore s) /\
    typof s (var_e x) =ot _ctxt s ot= t /\
    typof s e =ot _ctxt s ot= ptyp t /\
    exists p, [ e ]_s = Some (pval p) /\
      exists e0, (e |~ t ~> e0 **
        (e |~ t ~> e0 -* wp_assign t x e0 P)) s h }}
  x <-* e
  {{ P }}.

Lemma hoare_lookup_back'' : forall t P Q R x e c,
  P ===> (fun s h =>
    wf_tstore (_tstore s) /\
    typof s (var_e x) =ot _ctxt s ot= t /\
    typof s e =ot _ctxt s ot= ptyp t /\
    exists p, [ e ]_s = Some (pval p) /\
    exists e0, (e |~ t ~> e0 **
      (e |~ t ~> e0 -* wp_assign t x e0 R)) s h) ->
  {{ R }} c {{ Q }} -> {{ P }} x <-* e; c {{ Q }}.

Lemma hoare_false: forall c P, {{ FF }} c {{ P }}.

Local Open Scope minC_cmd_scope.

Fixpoint modified_vars (c : @while.cmd _ bexp) {struct c} : list var :=
  match c with
    | skip => nil
    | x <- e => x :: nil
    | x <-* e => x :: nil
    | e *<- f => nil
    | x <-malloc e => x :: nil
    | free e => nil
    | while.seq c1 c2 => modified_vars c1 ++ modified_vars c2
    | while.ifte a c1 c2 => modified_vars c1 ++ modified_vars c2
    | while.while a c1 => modified_vars c1
   end.

Definition inde (l : list var) (P : assert) := forall s h,
  (forall x v, In x l -> (P s h <-> P (store_upd x v s) h)).

Lemma inde_seq : forall R c d, inde (modified_vars (c ; d)) R ->
  inde (modified_vars c) R /\ inde (modified_vars d) R.

Lemma inde_ifte : forall R b c d, inde (modified_vars (while.ifte b c d)) R ->
  inde (modified_vars c) R /\ inde (modified_vars d) R.

Lemma inde_upd_tstore : forall (P : assert) x z s h,
  inde (x :: List.nil) P -> P s h -> P (store_upd x z s) h.
Require Import String_ext.
Require Import nodup.

Lemma frame_rule0 : forall P c Q, hoare0 P c Q ->
  forall R, inde (modified_vars c) R -> {{ P ** R }} c {{ Q ** R }}.

Lemma frame_rule : forall P c Q, {{ P }} c {{ Q }} ->
  forall R, inde (modified_vars c) R -> {{ P ** R }} c {{ Q ** R }}.

Local Open Scope minC_assert_scope.

Lemma hoare_mutation_global : forall P t e e',
  {{ (fun s' h' =>
    wf_tstore (_tstore s') /\
    typof s' e' = Some t /\
    exists e'', (e |~ t ~> e'') s' h') ** P }}
  e *<- e'
  {{ (fun s h => (e |~ t ~> e') s h) **
    P}}.

Lemma hoare_mutation_backwards : forall P t e e',
  {{ fun s h => wf_tstore (_tstore s) /\
    typof s e' = Some t /\
    exists e'', (e |~ t ~> e'' **
    (e |~ t ~> e' -* P)) s h }}
  e *<- e'
  {{ P }}.

Lemma hoare_mutation_backwards' : forall Q P t e1 e2,
  P ===> (fun s h => wf_tstore (_tstore s) /\
    typof s e2 = Some t /\
    exists e'', (e1 |~ t ~> e'' ** (e1 |~ t ~> e2 -* Q)) s h) ->
  {{ P }} e1 *<- e2 {{ Q }}.

Lemma hoare_mutation_backwards'' : forall Q P R e1 t e2 c,
  P ===> (fun s h =>
   wf_tstore (_tstore s) /\
    typof s e2 = Some t /\
    exists e'', (e1 |~ t ~> e'' **
      (e1 |~ t ~> e2 -* R)) s h) ->
  {{ R }} c {{ Q }} -> {{ P }} e1 *<- e2 ; c {{ Q }}.