NB: This Coq documentation contains a revised version of the Coq implementation of these papers [1], [2], [3], [4], and is also the support for ongoing research. A partial archive (14/01/2001) is available at here. Drop us a line if you are interested in a complete, up-to-date archive.

Library LSF_LWP_comparation

Require Import ZArith List EqNat Classical Omega Max.
Require Import ssreflect ssrbool.
Require Import bipl seplog integral_type.

Require Import expr_b_dp.
Import seplog_Z_m.assert_m.
Import seplog_Z_m.assert_m.expr_m.
Import seplog_Z_m.

Local Open Scope heap_scope.
Local Open Scope seplog_expr_scope.
Local Open Scope seplog_cmd_scope.
Local Open Scope seplog_assert_scope.
Local Open Scope seplog_hoare_scope.
Local Close Scope Z_scope.

Require Import frag_list_triple.
Require Import frag_list_entail.

Import Fresh.

Smallfoot like proof-system (pure forward) with arithmetic

Inductive LSF : assrt -> @while.cmd cmd0 expr_b -> assrt -> Prop :=
| LSF_precond_stre : forall L1 L1' L2 c,
  assrt_interp L1 ===> assrt_interp L1' ->
  LSF L1' c L2 ->
  LSF L1 c L2
  
| LSF_seq_assoc : forall P Q c1 c2 c3,
  LSF P (c1; (c2; c3)) Q ->
  LSF P ((c1; c2); c3) Q
  
| LSF_add_empty : forall P Q c,
  LSF P (c; skip) Q ->
  LSF P c Q
  
| LSF_empty: forall P Q,
  assrt_interp P ===> assrt_interp Q ->
  LSF P skip Q
  
| LSF_assign: forall pi sig Q c x e x',
  fresh_assrt x' (pi, sig) ->
  fresh_assrt x' Q ->
  fresh_cmd x' c ->
  fresh_e x' e ->
  fresh_e x' (var_e x) ->
  LSF (((subst_b pi (var_e x) (var_e x')) &e ((var_e x) =e (subst_e e (var_e x) (var_e x')))), subst_Sigma sig x (var_e x')) c Q ->
  LSF (pi, sig) (x <- e ; c) Q
  
| LSF_lookup: forall pi sig e1 e2 e x Q c x',
  (forall s, eval_b pi s -> eval_b (e1 =e e) s ) ->
  fresh_assrt x' (pi, star sig (singl e1 e2)) ->
  fresh_assrt x' Q ->
  fresh_cmd x' c ->
  fresh_e x' e ->
  fresh_e x' (var_e x) ->
  LSF (((subst_b pi (var_e x) (var_e x')) &e ((var_e x) =e (subst_e e2 (var_e x) (var_e x')))), subst_Sigma (star sig (singl e1 e2)) x (var_e x')) c Q ->
  LSF (pi,star sig (singl e1 e2)) (x <-* e; c) Q
  
| LSF_mutation: forall pi1 sig1 e1 e2 e3 e4 Q c,
  (forall s, eval_b pi1 s -> eval_b (e1 =e e3) s ) ->
  LSF (pi1,star sig1 (singl e1 e4)) c Q ->
  LSF (pi1,star sig1 (singl e1 e2)) (e3 *<- e4 ; c) Q
  
| LSF_mutation': forall pi1 sig1 e1 e3 e4 Q c,
  (forall s, eval_b pi1 s -> eval_b (e1 =e e3) s ) ->
  LSF (pi1,star sig1 (singl e1 e4)) c Q ->
  LSF (pi1,star sig1 (cell e1)) (e3 *<- e4 ; c) Q
  
| LSF_cond: forall b c1 c2 c Q pi sig,
  LSF (pi &e b, sig) (c1; c) Q ->
  LSF (pi &e (~e b), sig) (c2 ; c) Q ->
  LSF (pi, sig) (ifte b thendo c1 elsedo c2; c) Q
  
| LSF_unroll_lst_lookup: forall pi sig e1 e2 e x Q c x',
  (forall s, eval_b pi s -> eval_b (e1 =e e) s ) ->
  fresh_assrt x' (pi, star sig (lst e1 e2)) ->
  fresh_assrt x' Q ->
  fresh_cmd x' c ->
  fresh_e x' e ->
  fresh_e x' (var_e x) ->
  (forall s, [ pi =b> (e1 <>e e2) ]b_s) ->
  LSF ((pi &e ((var_e x') =e e2) ,star sig (star (star (singl e1 (var_e x')) (cell (e1 +e (nat_e 1)))) (lst (var_e x') e2)))) (x <-* e; c) Q ->
  LSF ((pi &e ((var_e x') <>e e2) ,star sig (star (star (singl e1 (var_e x')) (cell (e1 +e (nat_e 1)))) (lst (var_e x') e2)))) (x <-* e; c) Q ->
  LSF (pi,star sig (lst e1 e2)) (x <-* e; c) Q.

Axiom LSF_sound: forall P c Q,
  LSF P c Q ->
  {{assrt_interp P}} c {{assrt_interp Q}}.

Axiom LSF_lookup': forall pi sig e1 e2 e x Q c x',
  (forall s, eval_b pi s -> eval_b (e1 =e e) s ) ->
  x' = (max (var_max_cmd c) (max (var_max_assrt (pi,star sig (singl e1 e2))) (max (var_max_assrt Q) (max x (Max_ext.max_lst (vars e)))))) + 1 ->
  LSF (((subst_b pi (var_e x) (var_e x')) &e ((var_e x) =e (subst_e e2 (var_e x) (var_e x')))), subst_Sigma (star sig (singl e1 e2)) x (var_e x')) c Q ->
  LSF (pi,star sig (singl e1 e2)) (x <-* e; c) Q.

Axiom LSF_assign': forall pi sig Q c x e x',
  x' = (max (var_max_cmd c) (max (var_max_assrt (pi,sig)) (max (var_max_assrt Q) (max x (Max_ext.max_lst (vars e)))))) + 1 ->
  LSF (((subst_b pi (var_e x) (var_e x')) &e ((var_e x) =e (subst_e e (var_e x) (var_e x')))), subst_Sigma sig x (var_e x')) c Q ->
  LSF (pi, sig) (x <- e ; c) Q.

Axiom LSF_unroll_lst_lookup': forall pi sig e1 e2 e x Q c x',
  (forall s, eval_b pi s -> eval_b (e1 =e e) s ) ->
  x' = (max (var_max_cmd c) (max (var_max_assrt (pi,star sig (lst e1 e2))) (max (var_max_assrt Q) (max x (Max_ext.max_lst (vars e)))))) + 1 ->
  (forall s, [ pi =b> (e1 <>e e2) ]b_s) ->
  LSF ((pi &e (var_e x' =e e2), star sig (star (star (singl e1 (var_e x')) (cell (e1 +e (nat_e 1)))) (lst (var_e x') e2)))) (x <-* e; c) Q ->
  LSF ((pi &e (var_e x' <>e e2), star sig (star (star (singl e1 (var_e x')) (cell (e1 +e (nat_e 1)))) (lst (var_e x') e2)))) (x <-* e; c) Q ->
  LSF (pi, star sig (lst e1 e2)) (x <-* e; c) Q.



Local Open Scope frag_list_scope.

Goal
  {{{ ((var_e 1 <>e var_e 2) &e (var_e 1 <>e cst_e 0%Z), lst (var_e 1) (var_e 2)) }}}
  0 <-* (var_e 1)
  {{{ (true_b, lst (var_e 1) (var_e 2)) }}}.

Goal
  {{ assrt_interp ((var_e 1 <>e var_e 2) &e (var_e 1 <>e cst_e 0%Z), lst (var_e 1) (var_e 2))}}
  0 <-* (var_e 1)
  {{ assrt_interp (true_b, lst (var_e 1) (var_e 2))}}.


Goal
  {{ assrt_interp (true_b, emp)}}
  ifte ((var_e 1) >>= (var_e 2)) thendo
    ifte ((var_e 1) >>= (var_e 3)) thendo
      (0 <- (var_e 1))
    elsedo
      (0 <- (var_e 3))
  elsedo
    ifte ((var_e 2) >>= (var_e 3)) thendo
      (0 <- (var_e 2))
    elsedo
      (0 <- (var_e 3))
  {{ assrt_interp (((var_e 0) =e (var_e 1)) |e ((var_e 0) =e (var_e 2)) |e ((var_e 0) =e (var_e 3)), emp)}}.


Goal
  {{{ (true_b, emp) }}}
  ifte (var_e 1 >>= var_e 2) thendo
    ifte (var_e 1 >>= var_e 3) thendo
      (0 <- var_e 1)
    elsedo
      (0 <- var_e 3)
  elsedo
    ifte (var_e 2 >>= var_e 3) thendo
      (0 <- var_e 2)
    elsedo
      (0 <- var_e 3)
  {{{ ((var_e 0 =e var_e 1) |e (var_e 0 =e var_e 2) |e (var_e 0 =e var_e 3),emp) }}}.

Ltac Rotate_LSF_sig_lhs :=
  match goal with
    | |- LSF (?pi,?sig) ?c ?Q =>
      eapply LSF_precond_stre with (
        (pi, remove_empty_heap pi (star_assoc_left (star_com sig) emp))
      ); [apply entail_soundness; simpl; Entail| simpl]
  end.

Section swap.


Definition i : var.v := 1.
Definition j : var.v := 2.
Definition x : var.v := 4.
Definition y : var.v := 3.
Definition vx : var.v := 5.
Definition vy : var.v := 6.

Definition swap (x y:var.v) : @while.cmd cmd0 expr_b :=
    i <-* var_e x;
    j <-* var_e y;
    var_e x *<- var_e j;
    var_e y *<- var_e i.

Definition swap_precond (x y:var.v) (vx vy : nat) : assrt :=
  (true_b, star (singl (var_e x) (var_e vx)) (singl (var_e y) (var_e vy))).

Definition swap_postcond (x y:var.v) (vx vy : nat) : assrt :=
  (true_b, star (singl (var_e x) (var_e vy)) (singl (var_e y) (var_e vx))).


Lemma swap_verif:
  {{assrt_interp (swap_precond x y vx vy)}}
  swap x y
  {{assrt_interp ((swap_postcond x y vx vy))}}.


Lemma swap_verif':
    {{assrt_interp (swap_precond x y vx vy)}}
    swap x y
    {{Assrt_interp ((swap_postcond x y vx vy)::nil)}}.

End swap.


Definition ptr : var.v := 1.
Definition startl : var.v := 2.
Definition size: var.v := 3.
Definition idx: var.v := 4.
Definition init_val: var.v := 5.

Fixpoint init_body (n: nat) {struct n}: @while.cmd cmd0 expr_b :=
  match n with
    0 => skip
    | S n' =>
      ((var_e ptr) +e (var_e idx)) *<- var_e init_val;
       ptr <- (var_e ptr) +e (var_e size);
       init_body n'
   end.

Definition init (n: nat) : @while.cmd cmd0 expr_b :=
    ptr <- var_e startl;
    init_body n.

Fixpoint init_precond_sigma (n: nat) {struct n} : Sigma :=
  match n with
    0 => emp
    | S n' => star
        (cell (((var_e startl) +e (var_e idx)) +e ((var_e size) *e (cst_e (Z_of_nat n'))) ))
        (init_precond_sigma n')
end.

Definition init_precond (n: nat) : assrt :=
  (var_e startl >> cst_e 0%Z, init_precond_sigma n).

Fixpoint init_postcond_sigma (n: nat) {struct n}: Sigma :=
  match n with
    0 => emp
    | S n' => star
        (singl (((var_e startl) +e (var_e idx)) +e ((var_e size) *e (cst_e (Z_of_nat n'))) ) (var_e init_val))
        (init_postcond_sigma n')
end.

Definition init_postcond (n: nat) : assrt :=
  (var_e startl >> cst_e 0%Z, init_postcond_sigma n).


Lemma init_verif_bigtoe_5: forall n, n = 5 ->
  {{{ init_precond n }}} init n {{{ init_postcond n }}}.

Lemma init_verif_bigtoe_10: forall n, n = 10 ->
  {{{ init_precond n }}} init n {{{ init_postcond n }}}.

Lemma init_verif_bigtoe_12: forall n, n = 12 ->
  {{{ init_precond n }}} init n {{{ init_postcond n }}}.


Require Import ssreflect ssrbool.
Import ZIT.

tactics for cleaning hypothesis

Ltac Decompose_hyp := eval_b2Prop_hyps;
  match goal with
    | id: ex ?P |- _ => inversion_clear id; Decompose_hyp
    | id: ?P1 /\ ?P2 |- _ => decompose [and] id; clear id; Decompose_hyp
    | id: eval ?e ?s = ?v |- _ => simpl in id
    | |- _ => idtac
  end.

Lemma init_verif_smallfoot_5: forall n, n = 5 ->
  {{ assrt_interp (init_precond n)}} (init n) {{ assrt_interp (init_postcond n)}}.
Ltac local_omega :=
  Decompose_hyp; omegab.

Lemma init_verif_smallfoot_10: forall n, n = 10 ->
  {{ assrt_interp (init_precond n)}} init n {{ assrt_interp (init_postcond n)}}.

Lemma init_verif_smallfoot_12: forall n, n = 12 ->
  {{ assrt_interp (init_precond n)}} (init n) {{ assrt_interp (init_postcond n)}}.