Commit ae5eed3c authored by charguer's avatar charguer

wp_seq_encoded

parent 1553cd8e
......@@ -23,7 +23,6 @@ Open Scope string_scope.
(* ---------------------------------------------------------------------- *)
(** Representation of variables and locations *)
Definition tag := nat.
Definition var := string.
Definition loc := nat.
Definition null : loc := 0%nat.
......@@ -34,6 +33,15 @@ Definition eq_var_dec := String.string_dec.
Global Opaque field var loc.
(* ---------------------------------------------------------------------- *)
(** Tags for encoded language constructs *)
Inductive tag : Type :=
| tag_seq : tag
| tag_for : tag
| tag_while : tag.
(* ---------------------------------------------------------------------- *)
(** Syntax of the source language *)
......@@ -66,8 +74,8 @@ with trm : Type :=
| trm_app : trm -> trm -> trm
| trm_while : trm -> trm -> trm
| trm_for : var -> trm -> trm -> trm -> trm
| trm_tag : tag -> trm -> trm
| trm_protect : var -> trm -> trm.
| trm_protect : var -> trm -> trm
| trm_tag : tag -> trm -> trm.
(** The type of values is inhabited *)
......@@ -100,8 +108,6 @@ Definition is_reserved_var (x:var) : bool :=
(** Encoding of sequences *)
Definition tag_seq : tag := 1%nat.
Definition trm_seq (t1:trm) (t2:trm) : trm :=
trm_tag tag_seq (trm_let "$_" t1 (trm_protect "$_" t2)).
......@@ -126,8 +132,8 @@ Fixpoint subst (y:var) (w:val) (t:trm) : trm :=
| trm_app t1 t2 => trm_app (aux t1) (aux t2)
| trm_while t1 t2 => trm_while (aux t1) (aux t2)
| trm_for x t1 t2 t3 => trm_for x (aux t1) (aux t2) (aux_no_capture x t3)
| trm_tag g t1 => trm_tag g (aux t1)
| trm_protect x t1 => if eq_var_dec x y then t else trm_protect x (aux t1)
| trm_tag g t1 => trm_tag g (aux t1)
end.
......@@ -148,12 +154,12 @@ Implicit Types b : bool.
Implicit Types n : int.
Inductive red : state -> trm -> state -> val -> Prop :=
| red_tag : forall g t1 m1 m2 v,
red m1 t1 m2 v ->
red m1 (trm_tag g t1) m2 v
| red_protect : forall x t1 m1 m2 v,
red m1 t1 m2 v ->
red m1 (trm_protect x t1) m2 v
| red_tag : forall g t1 m1 m2 v,
red m1 t1 m2 v ->
red m1 (trm_tag g t1) m2 v
| red_val : forall m v,
red m v m v
| red_fun : forall m x t1,
......
......@@ -17,6 +17,17 @@ Implicit Types v w : val.
Implicit Types t : trm.
(* todo: move *)
Lemma red_seq' : forall m1 m2 m3 t1 t2 r1 r,
red m1 t1 m2 r1 ->
red m2 t2 m3 r ->
red m1 (trm_seq t1 t2) m3 r.
Proof using.
introv M1 M2. applys red_tag. applys* red_let.
simpl. applys* red_protect.
Qed.
(* ********************************************************************** *)
(* * WP generator *)
......@@ -181,6 +192,9 @@ Definition wp_val (v:val) : formula := local (fun Q =>
Definition wp_seq (F1 F2:formula) : formula := local (fun Q =>
F1 (fun r => \[r = val_unit] \* F2 Q)).
Definition wp_seq' (F1 F2:formula) : formula := local (fun Q =>
F1 (fun r => F2 Q)).
Definition wp_let (F1:formula) (F2of:val->formula) : formula := local (fun Q =>
F1 (fun X => F2of X Q)).
......@@ -231,17 +245,17 @@ Fixpoint wp (E:ctx) (t:trm) : formula :=
| trm_app t1 t2 => local (weakestpre (triple (substs E t)))
| trm_while t1 t2 => wp_while (aux t1) (aux t2)
| trm_for x t1 t2 t3 => wp_for' (aux t1) (aux t2) (fun X => wp (ctx_add x X E) t3)
| trm_tag g t1 => wp_tag g (aux t1)
| trm_protect x t1 => wp (ctx_rem x E) t1
| trm_tag g t0 =>
match g, t0 with
| tag_seq, trm_let x t1 (trm_protect y t2) =>
if eq_var_dec x y
then wp_seq' (aux t1) (wp (ctx_rem x E) t2)
else wp_fail
| _,_ => wp_fail
end
end.
(* match
| trm_tag g (trm_let x t1 (trm_protect y t2)) =>
if eq_nat_dec g tag_seq && eq_var_dec x y
then wp_seq (aux t1) (aux t2)
else ...
*)
(* ********************************************************************** *)
(* * Soundness proof *)
......@@ -318,10 +332,18 @@ Qed. (* TODO: simplify proof? *)
Lemma is_local_cf : forall E t,
is_local (wp E t).
Proof.
intros. gen E. induction t; intros;
intros. gen E. induction t; intros;
try solve [ apply is_local_local | eauto ].
{ simpl. rename t into g.
destruct g; try apply is_local_local.
destruct t0; try applys is_local_local.
destruct t0_2; try applys is_local_local.
case_if; try applys is_local_local. }
Qed.
(** [remove_local] applies to goal of the form [triple t (local F Q) Q]
and turns it into [triple t (F Q) Q] for a fresh [Q], then calls [xpull] *)
......@@ -329,8 +351,11 @@ Ltac remove_local :=
match goal with |- triple _ _ ?Q =>
applys triple_local_pre; try (clear Q; intros Q); xpull end.
(** Triples with [wp_fail] as precondition are always valid. *)
Lemma triple_wp_fail : forall t Q,
triple t (wp_fail Q) Q.
Proof using. intros. remove_local. intros. false. Qed.
(* TODO move *)
......@@ -395,8 +420,15 @@ Proof using.
{ remove_local. rewrite substs_app. apply triple_weakestpre_pre. }
{ admit. } (** will be handled differently *)
{ admit. }
{ rewrite substs_tag. applys rule_tag. unfold wp_tag. applys IHt. }
{ rewrite substs_protect. applys rule_protect. applys IHt. }
{ rename t into g. destruct g; try apply triple_wp_fail.
destruct t0; try apply triple_wp_fail.
destruct t0_2; try apply triple_wp_fail.
case_if; try apply triple_wp_fail. subst.
renames v0 to x, t0_1 to t1, t0_2 to t2.
rewrite substs_tag. applys rule_tag.
simpl in IHt. case_if. unfolds wp_let.
unfold wp_seq'. apply IHt. }
Qed.
Lemma triple_substs_of_wp : forall t E H Q,
......@@ -413,7 +445,7 @@ Proof using. introv M. xchanges M. applys triple_wp. Qed.
(* ********************************************************************** *)
(* * Alternative definition of the CF generator *)
(*
(*
Module WP2.
......@@ -558,16 +590,10 @@ Notation "'`If' v 'Then' F1 'Else' F2" :=
(at level 69) : charac.
Notation "'`Seq' F1 ;;; F2" :=
((wp_seq F1 F2))
((wp_seq' F1 F2))
(at level 68, right associativity,
format "'[v' '`Seq' '[' F1 ']' ;;; '/' '[' F2 ']' ']'") : charac.
Notation "'`Seq' x F1 ;;; F2" :=
(wp_tag tag_seq (wp_let F1 (fun x => F2)))
(at level 68, right associativity, x ident,
format "'[v' '`Seq' x '[' F1 ']' ;;; '/' '[' F2 ']' ']'") : charac.
(* LATER: how to remove x ? specific CF for tagged-let with a sequence-tag *)
Notation "'`Let' x ':=' F1 'in' F2" :=
((wp_let F1 (fun x => F2)))
(at level 69, x ident, right associativity,
......@@ -794,15 +820,56 @@ Definition val_incr :=
Lemma rule_incr : forall (p:loc) (n:int),
triple (val_incr p)
(p ~~~> n)
(fun r => \[r = val_unit] \* (p ~~~> (n+1))).
(fun r => (p ~~~> (n+1))).
Proof using.
intros. xcf.
xlet. { xapp. xapplys rule_get. }
intros x. hpull ;=> E. subst.
xlet. { xapp. xapplys rule_add. }
intros y. hpull ;=> E. subst.
xapp. xapplys rule_set. auto.
Qed.
xapp. xapplys rule_set.
Qed.
Definition val_incr2 :=
ValFun 'p :=
val_incr 'p ;;;
val_incr 'p.
Lemma rule_incr2 : forall (p:loc) (n:int),
triple (val_incr2 p)
(p ~~~> n)
(fun r => (p ~~~> (n+2))).
Proof using.
intros. xcf.
xlet. { xapp. xapplys rule_incr. }
hnf. intros _.
xapp. xapplys rule_incr.
hnf. intros _.
math_rewrite (n+2 = n+1+1). hsimpl.
Qed.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment