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 frag


Require Import Omega ZArith List.
Require Import ssreflect ssrbool.
Require Import Bool_ext EqNat_ext Max_ext.
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 seplog_expr_scope.
Local Open Scope seplog_cmd_scope.
Local Open Scope seplog_assert_scope.
Local Open Scope seplog_hoare_scope.

definition of syntactic constructs

Inductive Sigma : Type :=
| singl : expr -> expr -> Sigma
| cell : expr -> Sigma
| epsi : Sigma
| star : Sigma -> Sigma -> Sigma.

Fixpoint Sigma_interp (a : Sigma) : assert :=
  match a with
    | singl e1 e2 => e1 |~> e2
    | epsi => emp
    | star s1 s2 => Sigma_interp s1 ** Sigma_interp s2
    | cell e => fun s h => exists v, (e |~> cst_e v) s h
  end.

Definition assrt := (expr_b * Sigma)%type.

Definition assrt_interp (a : assrt) : assert :=
  match a with
    | (pi, sigm) => fun s h => [ pi ]b_ s /\ Sigma_interp sigm s h
  end.

A proof system for assrt entailment

Inductive ps1 : assrt -> assrt -> Prop :=
| ps1_incons : forall pi1 pi2 sig1 sig2,
  (forall s, [ pi1 ]b_ s -> False) ->
  ps1 (pi1, sig1) (pi2, sig2)
  
| ps1_tauto : forall pi1 pi2,
  (forall s, [ pi1 ]b_ s -> [ pi2 ]b_ s) ->
  ps1 (pi1, epsi) (pi2, epsi)
  
| ps1_coml : forall pi1 sig1 sig2 L,
  ps1 (pi1, star sig2 sig1) L -> ps1 (pi1, star sig1 sig2) L
  
| ps1_comr : forall pi1 sig1 sig2 L,
  ps1 L (pi1, star sig2 sig1) -> ps1 L (pi1, star sig1 sig2)
  
| ps1_assocl : forall pi1 sig1 sig2 sig3 L,
  ps1 (pi1, star (star sig1 sig2) sig3) L ->
  ps1 (pi1, star sig1 (star sig2 sig3)) L
  
| ps1_assocr : forall pi1 sig1 sig2 sig3 L,
  ps1 L (pi1, star (star sig1 sig2) sig3) ->
  ps1 L (pi1, star sig1 (star sig2 sig3))
  
| ps1_epseliml : forall pi1 sig1 L,
  ps1 (pi1, sig1) L ->
  ps1 (pi1, star sig1 epsi) L
  
| ps1_epselimr : forall pi1 sig1 L,
  ps1 L (pi1, sig1) ->
  ps1 L (pi1, star sig1 epsi)
  
| ps1_epsintrol : forall pi1 sig1 L,
  ps1 (pi1, star sig1 epsi) L ->
  ps1 (pi1, sig1) L
  
| ps1_epsintror : forall pi1 sig1 L,
  ps1 L (pi1, star sig1 epsi) ->
  ps1 L (pi1, sig1)
  
| ps1_star_elim : forall pi1 pi2 sig1 sig2 e1 e2 e3 e4,
  (forall s, eval_b pi1 s -> eval_b (e1 =e e3) s) ->
  (forall s , eval_b pi1 s -> eval_b (e2 =e e4) s) ->
  ps1 (pi1, sig1) (pi2, sig2) ->
  ps1 (pi1, star sig1 (singl e1 e2)) (pi2, star sig2 (singl e3 e4))
  
| ps1_star_elim' : forall pi1 pi2 sig1 sig2 e1 e2 e3,
  (forall s, eval_b pi1 s -> eval_b (e1 =e e3) s) ->
  ps1 (pi1, sig1) (pi2, sig2) ->
  ps1 (pi1, star sig1 (singl e1 e2)) (pi2, star sig2 (cell e3))
  
| ps1_star_elim'' : forall pi1 pi2 sig1 sig2 e1 e3,
  (forall s, eval_b pi1 s -> eval_b (e1 =e e3) s) ->
  ps1 (pi1, sig1) (pi2, sig2) ->
  ps1 (pi1, star sig1 (cell e1)) (pi2, star sig2 (cell e3)).

Soundness of the proof system

Lemma ps1_soundness : forall P Q, ps1 P Q -> assrt_interp P ===> assrt_interp Q.

Tactics to prove a ps1 goal

Ltac ps1_turnl :=
  match goal with
    | |- ps1 (?Pi, cell ?e) ?L => apply ps1_epsintrol; apply ps1_coml; repeat apply ps1_assocl
    | |- ps1 (?Pi, singl ?e1 ?e2) ?L => apply ps1_epsintrol; apply ps1_coml; repeat apply ps1_assocl
    | |- ps1 (?Pi, star ?e1 ?e2) ?L => apply ps1_coml; repeat apply ps1_assocl
  end.

Ltac ps1_turnr :=
  match goal with
    | |- ps1 ?L (?Pi, cell ?e) => apply ps1_epsintror; apply ps1_comr; repeat apply ps1_assocr
    | |- ps1 ?L (?Pi, singl ?e1 ?e2) => apply ps1_epsintror; apply ps1_comr; repeat apply ps1_assocr
    | |- ps1 ?L (?Pi, star ?e1 ?e2) => apply ps1_comr; repeat apply ps1_assocr
  end.

Ltac ps1_resolve := repeat apply ps1_assocr; repeat apply ps1_assocl;
  match goal with
    | |- ps1 (?pi1, star ?sig1 epsi) ?L => ps1_turnl; idtac
    | |- ps1 ?L (?Pi, cell ?e) => ps1_turnr; idtac
    | |- ps1 ?L (?Pi, singl ?e1 ?e2) => ps1_turnr; idtac
    | |- ps1 (?Pi, cell ?e) ?L => ps1_turnl; idtac
    | |- ps1 (?Pi, singl ?e1 ?e2) ?L => ps1_turnl; idtac
      

    | |- ps1 (?pi1, epsi) (?pi2, epsi) => apply ps1_tauto; do 2 intro; omegab
    | |- ps1 (?pi1, epsi) (?pi2, epsi) => apply ps1_incons; do 2 intro; omegab
                                                             

    | |- ps1 (?pi1, star ?e epsi) ?L => apply ps1_epseliml; idtac
    | |- ps1 ?L (?pi2, star ?e epsi) => apply ps1_epselimr; idtac

    | |- ps1 (?pi1, star ?sig1 (singl ?e1 ?e2)) (?pi2, star ?sig2 (singl ?e3 ?e4)) =>
      (apply ps1_star_elim; [ (do 2 intro; omegab) |
        (do 2 intro; omegab) | idtac] || ps1_turnl; idtac)
      
    | |- ps1 (?pi1, star ?sig1 (singl ?e1 ?e2)) (?pi2, star ?sig2 (cell ?e3)) =>
      (apply ps1_star_elim'; [ (do 2 intro; omegab) | idtac] || ps1_turnl; idtac)
      
    | |- ps1 (?pi1, star ?sig1 (cell ?e1)) (?pi2, star ?sig2 (cell ?e3)) =>
      (apply ps1_star_elim''; [ (do 2 intro; omegab) | idtac] || ps1_turnl; idtac)
      
    | |- ps1 (?pi2, star ?sig2 (cell ?e3)) (?pi1, star ?sig1 (singl ?e1 ?e2)) => ps1_turnl
   end.

Ltac ps1_Resolve := repeat ps1_resolve.


Lemma ps1_ex1: forall vy vx,
  ps1
  (true_b, star (singl (var_e 4%nat) (cst_e vx)) (singl (var_e 3%nat) (cst_e vy)))
  (true_b, star (singl (var_e 3%nat) (cst_e vy)) (singl (var_e 4%nat) (cst_e vx))).

Lemma ps1_ex2: forall startp sizep,
  (startp > 0)%nat -> (sizep > 4)%nat ->
  ps1
  (true_b,
    star
    (star (cell ((nat_e startp +e nat_e sizep) .-e cst_e 1%Z))
      (star (singl (nat_e startp) (cst_e 1%Z))
        (singl (nat_e startp +e cst_e 1%Z)
          ((cst_e (Z_of_nat startp) +e cst_e (Z_of_nat sizep)) .-e
                 cst_e 2%Z))))
    (cell ((nat_e startp +e nat_e sizep) .-e cst_e 2%Z)))
  (true_b,
    star
    (star
      (star (cell ((nat_e startp +e nat_e sizep) .-e cst_e 2%Z))
        (cell ((nat_e startp +e nat_e sizep) .-e cst_e 1%Z)))
      (singl (nat_e startp) (cst_e 1%Z)))
    (singl (nat_e startp +e cst_e 1%Z)
      ((cst_e (Z_of_nat startp) +e cst_e (Z_of_nat sizep)) .-e cst_e 2%Z))).

frag_decision is a certified decision procedure for entailment of assrt


Fixpoint Sigma_clean_epsi (t : Sigma) : Sigma :=
  match t with
    | star t1 t2 =>
      match Sigma_clean_epsi t1 with
        | epsi => Sigma_clean_epsi t2
        | t1' => match Sigma_clean_epsi t2 with
                   | epsi => t1'
                   | t2' => star t1' t2'
                 end
      end
    | _ => t
  end.

Definition Sigma_elt_eq (e1 e2 : Sigma) (env : expr_b) : bool :=
  match (e1, e2) with
    | (epsi, epsi) => true
    | (singl x1 x2, singl x3 x4) => expr_b_dp (env =b> (x1 =e x3)) && expr_b_dp (env =b> (x2 =e x4))
    | (singl x1 x2, cell x3) => expr_b_dp (env =b> (x1 =e x3))
    | (cell x1, cell x3) => expr_b_dp (env =b> (x1 =e x3))
    | (_, _) => false
  end.

Fixpoint Sigma_elt_term_extract (e t : Sigma) (env : expr_b) {struct t} : option Sigma :=
  match t with
    | star t1 t2 =>
      match Sigma_elt_term_extract e t1 env with
        | None => match Sigma_elt_term_extract e t2 env with
                    | None => None
                    | Some t2' => Some (Sigma_clean_epsi (star t1 t2'))
                  end
        | Some t1' => Some (Sigma_clean_epsi (star t1' t2))
      end
    | _ => if Sigma_elt_eq e t env then Some epsi else None
  end.

Fixpoint Sigma_elt_term_extract' (e t : Sigma) (env : expr_b) {struct t} : option Sigma :=
  match t with
    | star t1 t2 =>
      match Sigma_elt_term_extract' e t1 env with
        | None => match Sigma_elt_term_extract' e t2 env with
                    | None => None
                    | Some t2' => Some (Sigma_clean_epsi (star t1 t2'))
                  end
        | Some t1' => Some (Sigma_clean_epsi (star t1' t2))
      end
    | _ => if Sigma_elt_eq t e env then Some epsi else None
  end.

Fixpoint Sigma_term_term_eq (t1 t2 : Sigma) (env : expr_b) {struct t1} : option Sigma :=
  match t1 with
    | star t11 t12 =>
      match Sigma_term_term_eq t11 t2 env with
        | None => None
        | Some t2' => match Sigma_term_term_eq t12 t2' env with
                        | None => None
                        | Some t2'' => Some t2''
                      end
      end
    | _ => match Sigma_elt_term_extract t1 t2 env with
             | None => None
             | Some t2' => Some t2'
           end
  end.

Fixpoint Sigma_get_cell_val (e : expr) (sig : Sigma) (env : expr_b) {struct sig} : option expr :=
  match sig with
    | epsi => None
    | singl e1 e2 => if expr_b_dp (env =b> (e1 =e e)) then Some e2 else None
    | cell e1 => None
    | star s1 s2 =>
      match Sigma_get_cell_val e s1 env with
        | None => Sigma_get_cell_val e s2 env
        | Some e2 => Some e2
      end
  end.

Definition frag_decision (P Q : expr_b * Sigma) : bool :=
  let (pi1, sig1) := P in
  let (pi2, sig2) := Q in
    if expr_b_dp (pi1 =b> pi2) then
      match Sigma_term_term_eq sig1 sig2 pi1 with
        | Some epsi => true
        | _ => false
      end
      else
        false .

Lemma Sigma_clean_epsi_correct : forall t,
  Sigma_interp (Sigma_clean_epsi t) ===> Sigma_interp t.

Lemma Sigma_clean_epsi_correct' : forall t,
  Sigma_interp t ===> Sigma_interp (Sigma_clean_epsi t).

Lemma Sigma_elt_eq_correct : forall e1 e2 env, Sigma_elt_eq e1 e2 env ->
  forall s h, [ env ]b_s -> Sigma_interp e1 s h -> Sigma_interp e2 s h.

Opaque Sigma_clean_epsi.

Local Open Scope heap_scope.

Lemma Sigma_elt_term_extract_correct : forall e2 e1 env e2',
  Sigma_elt_term_extract e1 e2 env = Some e2' ->
  forall s h, [ env ]b_s ->
    Sigma_interp (star e1 e2') s h -> Sigma_interp e2 s h.

Lemma Sigma_elt_term_extract'_correct : forall e2 e1 env e2',
  Sigma_elt_term_extract' e1 e2 env = Some e2' ->
  forall s h, [ env ]b_s ->
    Sigma_interp e2 s h -> Sigma_interp (star e1 e2') s h.

Lemma Sigma_term_term_eq_correct : forall t1 t2 env t1',
  Sigma_term_term_eq t1 t2 env = Some t1' ->
  forall s h, [ env ]b_s ->
    Sigma_interp (star t1 t1') s h -> Sigma_interp t2 s h.

Lemma Sigma_get_cell_val_correct : forall sig e env e',
  Sigma_get_cell_val e sig env = Some e' ->
  forall s h, [ env ]b_s ->
    Sigma_interp sig s h -> (Sigma_interp (singl e e') ** TT) s h.

Lemma frag_decision_correct : forall P Q,
  frag_decision P Q -> assrt_interp P ===> assrt_interp Q.

Transparent Sigma_clean_epsi.

proof system for hoare triple using the fragment

Inductive wpAssrt : Type :=
| wpElt : assrt -> wpAssrt
| wpSubst : list (var.v * expr) -> wpAssrt -> wpAssrt
| wpLookup : var.v -> expr -> wpAssrt -> wpAssrt
| wpMutation : expr -> expr -> wpAssrt -> wpAssrt
| wpIf : expr_b -> wpAssrt -> wpAssrt -> wpAssrt.

Fixpoint wpAssrt_interp (a : wpAssrt) : assert :=
  match a with
    | wpElt a1 => assrt_interp a1
    | wpSubst l L => wp_assigns l (wpAssrt_interp L)
    | wpLookup x e L =>
      fun s h => exists e0, (e |~> e0 ** (e |~> e0 -* (wp_assign x e0 (wpAssrt_interp L)))) s h
    | wpMutation e1 e2 L =>
      fun s h => exists e0, (e1 |~> e0 ** (e1 |~> e2 -* (wpAssrt_interp L))) s h
    | wpIf b L1 L2 =>
      fun s h => ([ b ]b_ s -> wpAssrt_interp L1 s h) /\ (~~ [ b ]b_ s -> wpAssrt_interp L2 s h)
  end.

Fixpoint subst_Sigma (a : Sigma) (x : var.v) (e : expr) {struct a} : Sigma :=
  match a with
    | singl e1 e2 => singl (subst_e e1 (var_e x) e) (subst_e e2 (var_e x) e)
    | epsi => epsi
    | star s1 s2 => star (subst_Sigma s1 x e) (subst_Sigma s2 x e)
    | cell e1 => cell (subst_e e1 (var_e x) e)
  end.

Definition subst_assrt (a : assrt) (x : var.v) (e : expr) : assrt :=
  match a with
    | (pi, sigm) => (subst_b pi (var_e x) e, subst_Sigma sigm x e)
  end.

Fixpoint subst_assrt_lst (l : list (var.v * expr)) (a : assrt) {struct l} : assrt :=
  match l with
    | nil => a
    | (x, e) :: tl => subst_assrt_lst tl (subst_assrt a x e)
  end.

properties of substitution functions

Lemma subst_Sigma2store_update : forall sigm s h x v,
  Sigma_interp (subst_Sigma sigm x v) s h ->
  Sigma_interp sigm (store.upd x ([ v ]e_ s) s) h.

Lemma subst_Sigma2store_update' : forall sigm s h x v,
  Sigma_interp sigm (store.upd x ([ v ]e_ s) s) h ->
  Sigma_interp (subst_Sigma sigm x v) s h.

Lemma wp_assigns_assrt_interp : forall l s h pi sigm,
  assrt_interp (subst_assrt_lst l (pi, sigm)) s h ->
  wp_assigns l (assrt_interp (pi, sigm)) s h.

a module for fresh variables (w.r.t. syntactic constructs)

Module Type FRESH.

Parameter fresh_Sigma : var.v -> Sigma -> Prop.

Parameter fresh_assrt : var.v -> assrt -> Prop.

Parameter fresh_wpAssrt : var.v -> wpAssrt -> Prop.

Parameter fresh_wpAssrt_inde: forall L x , fresh_wpAssrt x L ->
  inde (x :: nil) (wpAssrt_interp L).

End FRESH.

Require Import Max.

Module Fresh <: FRESH.

Fixpoint var_max_Sigma (s : Sigma) : var.v :=
  match s with
    | singl e1 e2 => max (max_lst (vars e1)) (max_lst (vars e2))
    | epsi => O
    | star s1 s2 => max (var_max_Sigma s1) (var_max_Sigma s2)
    | cell e1 => max_lst (vars e1)
  end.

Definition var_max_assrt (a : assrt) : var.v :=
  match a with
    | (pi, sigm) => max (max_lst (vars_b pi)) (var_max_Sigma sigm)
  end.

Fixpoint var_max_wpAssrt (a : wpAssrt) : var.v :=
  match a with
    | wpElt a1 => var_max_assrt a1
    | wpSubst l L => max (var_max_lst l) (var_max_wpAssrt L)
    | wpLookup x e L=> max (max x (max_lst (vars e))) (var_max_wpAssrt L)
    | wpMutation e1 e2 L => max (max (max_lst (vars e1)) (max_lst (vars e2))) (var_max_wpAssrt L)
    | wpIf b L1 L2 => max (max (var_max_wpAssrt L1) (var_max_wpAssrt L2)) (max_lst (vars_b b))
  end.

Local Close Scope Z_scope.

Definition fresh_Sigma x s := (var_max_Sigma s < x)%nat.

Definition fresh_assrt x a := (var_max_assrt a < x)%nat.

Definition fresh_wpAssrt x L := (var_max_wpAssrt L < x)%nat.

Ltac open_fresh_frag :=
  open_fresh_frag_hypo; open_fresh_frag_goal
with
  open_fresh_frag_hypo := match goal with
    | H: fresh_e _ _ |- _ => unfold fresh_e in H; simpl in H; open_fresh_frag_hypo
    | H: fresh_b _ _ |- _ => unfold fresh_b in H; simpl in H; open_fresh_frag_hypo
    | H: fresh_Sigma _ _ |- _ => unfold fresh_Sigma in H; simpl in H; open_fresh_frag_hypo
    | H: fresh_assrt _ _ |- _ => unfold fresh_assrt in H; simpl in H; open_fresh_frag_hypo
    | H: fresh_lst _ _ |- _ => unfold fresh_lst in H; simpl in H; open_fresh_frag_hypo
    | H: fresh_wpAssrt _ _ |- _ => unfold fresh_wpAssrt in H; simpl in H; open_fresh_frag_hypo
    | H: context [ var_max_assrt _ ] |- _ => unfold var_max_assrt in H; simpl in H; open_fresh_frag_hypo
    | |- _ => idtac
  end
with
  open_fresh_frag_goal := match goal with
    | |- fresh_e _ _ => rewrite /fresh_e /=; open_fresh_frag_goal
    | |- fresh_b _ _ => rewrite /fresh_b /=; open_fresh_frag_goal
    | |- fresh_Sigma _ _ => rewrite /fresh_Sigma /=; open_fresh_frag_goal
    | |- fresh_assrt _ _ => rewrite /fresh_assrt /=; open_fresh_frag_goal
    | |- fresh_lst _ _ => rewrite /fresh_lst /=; open_fresh_frag_goal
    | |- fresh_wpAssrt _ _ => rewrite /fresh_wpAssrt /=; open_fresh_frag_goal
    | |- context [var_max_assrt _ ] => rewrite /var_max_assrt /=; open_fresh_frag_goal
    | |- _ => idtac
  end.

Ltac Max_inf_resolve := open_fresh_frag; Resolve_lt_max.

relations between freshness predicates and the independence predicate ("inde")

Lemma var_max_Sigma_inde : forall sigm x, fresh_Sigma x sigm ->
  inde (x :: nil) (Sigma_interp sigm).

Lemma fresh_assrt_inde : forall a x, fresh_assrt x a ->
  inde (x :: nil) (assrt_interp a).

Lemma fresh_wpAssrt_inde : forall L x, fresh_wpAssrt x L ->
  inde (x :: nil) (wpAssrt_interp L).

End Fresh.

Import Fresh.

definition of LWP and its soundness

Inductive LWP : assrt -> wpAssrt -> Prop :=
| LWP_entail : forall pi1 pi2 sig1 sig2,
  assrt_interp (pi1, sig1) ===> assrt_interp (pi2, sig2) ->
  LWP (pi1, sig1) (wpElt (pi2, sig2))
  
| LWP_precond_stre : forall L1 L1' L2,
  assrt_interp L1 ===> assrt_interp L1' ->
  LWP L1' L2 ->
  LWP L1 L2
  
| LWP_if : forall pi1 sig1 L1 L2 b,
  LWP (pi1 &e b, sig1) L1 ->
  LWP (pi1 &e (~e b), sig1) L2 ->
  LWP (pi1, sig1) (wpIf b L1 L2)
  
| LWP_mutation : forall pi1 sig1 e1 e2 e3 e4 L,
  (forall s, [ pi1 ]b_s -> [ e1 =e e3 ]b_s) ->
  LWP (pi1, star sig1 (singl e1 e4)) L ->
  LWP (pi1, star sig1 (singl e1 e2)) (wpMutation e3 e4 L)
  
| LWP_mutation' : forall pi1 sig1 e1 e3 e4 L,
  (forall s, [ pi1 ]b_s -> [ e1 =e e3 ]b_s) ->
  LWP (pi1, star sig1 (singl e1 e4)) L ->
  LWP (pi1, star sig1 (cell e1)) (wpMutation e3 e4 L)
  
| LWP_lookup : forall pi1 sig1 e1 e2 e x L,
  (forall s, [ pi1 ]b_s -> [ e1 =e e ]b_s) ->
  LWP (pi1, star sig1 (singl e1 e2)) (wpSubst ((x, e2) :: nil) L) ->
  LWP (pi1, star sig1 (singl e1 e2)) (wpLookup x e L)
  
| LWP_subst_elt : forall pi1 pi2 sig1 sig2 l,
  LWP (pi1, sig1) (wpElt (subst_assrt_lst l (pi2, sig2))) ->
  LWP (pi1, sig1) (wpSubst l (wpElt (pi2, sig2)))
  
| LWP_subst_subst : forall pi1 sig1 l1 l2 L,
  LWP (pi1, sig1) (wpSubst (l2 ++ l1) L) ->
  LWP (pi1, sig1) (wpSubst l1 (wpSubst l2 L))
  
| LWP_subst_lookup : forall pi1 sig1 e1 e2 e x x' l L,
  (forall s, [ pi1 ]b_s -> [ e1 =e subst_e_lst l e ]b_ s) ->
  fresh_lst x' l ->
  fresh_wpAssrt x' L ->
  fresh_e x' (var_e x) ->
  LWP (pi1, star sig1 (singl e1 e2)) (wpSubst ((x, (var_e x')) :: l ++ ((x', e2) :: nil)) L) ->
  LWP (pi1, star sig1 (singl e1 e2)) (wpSubst l (wpLookup x e L))
  
| LWP_subst_mutation : forall pi1 sig1 e1 e2 l L,
  LWP (pi1, sig1) (wpMutation (subst_e_lst l e1) (subst_e_lst l e2) (wpSubst l L)) ->
  LWP (pi1, sig1) (wpSubst l (wpMutation e1 e2 L))
    
| LWP_subst_if : forall pi1 sig1 l b L1 L2,
  LWP (pi1, sig1) (wpIf (subst_b_lst l b) (wpSubst l L1) (wpSubst l L2)) ->
  LWP (pi1, sig1) (wpSubst l (wpIf b L1 L2)).

replace a substitution (e/x) by two substitutions (x/x')(e/x') with x' fresh
Lemma intro_fresh_var : forall l x x' e s h L,
  fresh_lst x' l -> fresh_wpAssrt x' L -> fresh_e x' (var_e x) ->
  wp_assigns l (fun s' h' => wpAssrt_interp L (store.upd x ([ var_e x' ]e_ s') s') h')
    (store.upd x' ([ e ]e_ s) s) h ->
  wp_assigns l (fun s' h' => wpAssrt_interp L (store.upd x ([ e ]e_ s) s') h')
    s h.

Import ZIT.

Lemma LWP_soundness: forall P Q, LWP P Q -> assrt_interp P ===> wpAssrt_interp Q.

weakest pre-condition generator and its soudness

Fixpoint wp_frag (Q : option wpAssrt) (c : @while.cmd cmd0 expr_b) {struct c} : option wpAssrt :=
  match c with
    | skip => match Q with
              | None => None
              | Some Q' => Some Q'
              end
    | assign v e => match Q with
                      | None => None
                      | Some Q' => Some (wpSubst ((v, e) :: nil) Q')
                    end
    | lookup v e => match Q with
                      | None => None
                      | Some Q' => Some (wpLookup v e Q')
                    end
    | mutation e1 e2 => match Q with
                          | None => None
                          | Some Q' => Some (wpMutation e1 e2 Q')
                        end
    | while.seq c1 c2 => wp_frag (wp_frag Q c2) c1
    | ifte b thendo c1 elsedo c2 => match wp_frag Q c1 with
                                      | None => None
                                      | Some Q1 => match wp_frag Q c2 with
                                                     | None => None
                                                     | Some Q2 => Some (wpIf b Q1 Q2)
                                                   end
                                    end
    | while.while a c => None
    | malloc v e => None
    | free e => None
  end.

Lemma wp_frag_None_is_None : forall c, wp_frag None c = None.

Lemma wp_frag_soudness : forall c Q Q',
  wp_frag (Some Q) c = Some Q' -> {{ wpAssrt_interp Q' }} c {{ wpAssrt_interp Q }}.

Resolution tactic

Lemma LWP_use : forall c P Q R,
  wp_frag (Some (wpElt Q)) c = Some R ->
  LWP P R ->
  {{ assrt_interp P }} c {{ assrt_interp Q }}.

Local Close Scope Z_scope.

Lemma LWP_subst_lookup' : forall pi1 sig1 e1 e2 e x x' l L,
  (forall s, [ pi1 ]b_ s -> [ e1 =e (subst_e_lst l e) ]b_ s) ->
  x' = (max (max (var_max_lst l) (var_max_wpAssrt L)) x) + 1 ->
  LWP (pi1, star sig1 (singl e1 e2)) (wpSubst ((x, (var_e x')) :: l ++ ((x', e2) :: nil)) L) ->
  LWP (pi1, star sig1 (singl e1 e2)) (wpSubst l (wpLookup x e L)).

Tactics to resolve LWP goals

Fixpoint Sigma_assoc_left (t t' : Sigma) {struct t} : Sigma :=
  match t with
    | star sig1 sig2 => Sigma_assoc_left (sig2) (star t' sig1)
    | _ => match t' with
             | epsi => t
             | _ => star t' t
           end
 end.

Definition Sigma_com (t : Sigma) : Sigma :=
  match t with
    | star sig1 sig2 => star sig2 sig1
    | _ => t
  end.

Ltac Rotate_LWP_sig_lhs :=
  match goal with
    | |- LWP (?pi, ?sig) ?L' =>
      apply LWP_precond_stre with ((pi, Sigma_clean_epsi (Sigma_assoc_left (Sigma_com sig) epsi)));
        [apply ps1_soundness; simpl; ps1_Resolve| simpl]
  end.

Ltac LWP_resolve :=
  match goal with
    | |- LWP (?pi1, ?sig1) (wpElt (?pi2, ?sig2)) => apply LWP_entail; [eapply ps1_soundness; ps1_Resolve]
      
    | |- LWP (?pi1, star ?sig1 (singl ?e1 ?e2)) (wpMutation ?e3 ?e4 ?L') =>
      apply LWP_mutation; [(do 2 intro; omegab) | LWP_resolve] || Rotate_LWP_sig_lhs; idtac
      
    | |- LWP (?pi1, star ?sig1 (cell ?e1)) (wpMutation ?e3 ?e4 ?L') =>
      apply LWP_mutation'; [(do 2 intro; omegab) | LWP_resolve] || Rotate_LWP_sig_lhs; idtac
      
    | |- LWP (?pi1, star ?sig1 (singl ?e1 ?e2)) (wpLookup ?x ?e ?L') =>
      apply LWP_lookup; [(do 2 intro; omegab) | LWP_resolve] || Rotate_LWP_sig_lhs; idtac
      
    | |- LWP ?L (wpSubst ?l (wpElt ?L')) => eapply LWP_subst_elt; simpl; idtac
    | |- LWP ?L (wpSubst ?l (wpSubst ?l' ?L')) => eapply LWP_subst_subst; simpl; idtac
      
    | |- LWP ?L (wpSubst ?l (wpLookup ?x ?e ?L')) =>
      eapply LWP_subst_lookup'; [(do 2 intro; omegab) | simpl; intuition | LWP_resolve] || Rotate_LWP_sig_lhs; idtac
      
    | |- LWP ?L (wpSubst ?l (wpMutation ?e1 ?e2 ?L')) => apply LWP_subst_mutation; simpl; idtac
    | |- LWP ?L (wpSubst ?l (wpIf ?b ?L1 ?L2)) => eapply LWP_subst_if; simpl; idtac
    | |- LWP ?L (wpIf ?b ?L1 ?L2) => eapply LWP_if; simpl; idtac
   end.

Ltac LWP_Resolve := Rotate_LWP_sig_lhs; repeat LWP_resolve.

Definition LWP_step (pi : expr_b) (sig : Sigma) (A : wpAssrt) : option (list ((expr_b * Sigma) * wpAssrt)) :=
  match A with
    | wpElt L => if frag_decision (pi, sig) L then Some nil else None
    | wpSubst l L =>
      match L with
        | wpElt L' => Some (((pi, sig), wpElt (subst_assrt_lst l L')) :: nil)
        | wpSubst l' L' => Some (((pi, sig), wpSubst (l'++ l) L') :: nil)
        | wpLookup x e L' =>
          match Sigma_get_cell_val (subst_e_lst l e) sig pi with
            | None => None
            | Some e' =>
              let x' := (max (max (var_max_lst l) (var_max_wpAssrt L')) x) + 1 in
                Some (((pi, sig), wpSubst ((x, var_e x')::l ++ ((x', e')::nil)) L')::nil)
          end
        | wpMutation e1 e2 L' =>
          Some (((pi, sig), wpMutation (subst_e_lst l e1) (subst_e_lst l e2) (wpSubst l L')) :: nil)
        | wpIf b L1 L2 =>
          Some (((pi, sig), wpIf (subst_b_lst l b) (wpSubst l L1) (wpSubst l L2)) :: nil)
      end
    | wpLookup x e L =>
      match Sigma_get_cell_val e sig pi with
        | None => None
        | Some e' => Some (((pi, sig), wpSubst ((x, e') :: nil) L) :: nil)
      end
    | wpMutation e1 e2 L =>
      match Sigma_elt_term_extract' (cell e1) sig pi with
        | None => None
        | Some sig' => Some (((pi, star (singl e1 e2) sig'), L) :: nil)
      end
    | wpIf b L1 L2 =>
      Some (((pi &e b, sig), L1) :: ((pi &e (~e b), sig), L2) :: nil)
  end.

Fixpoint wpAssrt_size (A : wpAssrt) : nat :=
  match A with
    | wpElt P => 2
    | wpSubst l P => 2 + wpAssrt_size P
    | wpLookup x e P => 2 + wpAssrt_size P
    | wpMutation e1 e2 P => 2 + wpAssrt_size P
    | wpIf b L1 L2 => 2 + wpAssrt_size L1 + wpAssrt_size L2
  end.

Fixpoint LWP_list (l : list ((expr_b * Sigma) * wpAssrt)) : option (list ((expr_b * Sigma) * wpAssrt)) :=
  match l with
    | nil => Some nil
    | ((pi, sig), A) :: tl =>
      match LWP_step pi sig A with
        | None => None
        | Some l' =>
          match LWP_list tl with
            | None => None
            | Some l'' => Some (l' ++ l'')
          end
      end
  end.

Fixpoint LWP_list_rec (l : list ((expr_b * Sigma) * wpAssrt)) (size : nat) {struct size} : option (list ((expr_b * Sigma) * wpAssrt)) :=
  match size with
    | 0 => Some l
    | S size' =>
      match LWP_list l with
        | None => None
        | Some l' => LWP_list_rec l' size'
      end
  end.

Definition frag_hoare (P Q : expr_b * Sigma) (c : @while.cmd cmd0 expr_b) : bool :=
  match wp_frag (Some (wpElt Q)) c with
    | None => false
    | Some L =>
      let (p, s) := P in
        match LWP_list_rec (((p, s), L) :: nil) (wpAssrt_size L) with
          | Some nil => true
          | _ => false
        end
  end.

Opaque frag_decision.

Lemma LWP_step_correct : forall pi sig A l,
  LWP_step pi sig A = Some l ->
  (forall pi' sig' A', In ((pi', sig'), A') l -> assrt_interp (pi',sig') ===> wpAssrt_interp A') ->
  assrt_interp (pi, sig) ===> wpAssrt_interp A.

Transparent frag_decision.

Lemma LWP_list_correct: forall l l', LWP_list l = Some l' ->
  (forall pi sig A, In ((pi, sig), A) l' ->
    assrt_interp (pi, sig) ===> wpAssrt_interp A) ->
  forall pi sig A, In ((pi, sig), A) l -> assrt_interp (pi, sig) ===> wpAssrt_interp A.

Lemma LWP_list_rec_correct : forall a l l',
  LWP_list_rec l a = Some l' ->
  (forall pi sig A, In ((pi, sig), A) l' -> assrt_interp (pi, sig) ===> wpAssrt_interp A) ->
  forall pi sig A, In ((pi, sig), A) l -> assrt_interp (pi, sig) ===> wpAssrt_interp A.

Lemma frag_hoare_correct : forall P Q c,
  frag_hoare P Q c -> {{ assrt_interp P }} c {{ assrt_interp Q }}.