Commit 33172cf7 authored by charguer's avatar charguer

cleanedup example

parent 90b56650
......@@ -334,3 +334,143 @@ Tactic Notation "rew_heap" "*" "in" hyp(H) :=
*)
(*
Definition is_val (t:trm) : option val :=
match t with
| trm_val v => Some v
| _ => None
end.
| trm_if t0 t1 t2 =>
match is_val t0 with
| Some v => Trm_if_val v (aux t1) (aux t2)
| None => Trm_if (aux t0) (aux t1) (aux t2)
end
*)
(* REJECTED FOR TERMINATION REASONS
Definition is_val_fix (f:var) (t:trm) : option (vars*trm) :=
match t with
| trm_val (val_fix f' xs t) =>
if eq_var_dec f f' then None else Some (xs,t)
| _ => None
end.
Fixpoint Trm_of_trm (t : trm) : Trm :=
let aux := Trm_of_trm in
match t with
| trm_val v => Trm_val v
| trm_if t0 t1 t2 =>
match is_val t0 with
| Some v => Trm_if_val v (aux t1) (aux t2)
| None => Trm_if (aux t0) (aux t1) (aux t2)
end
| trm_seq t1 t2 => Trm_seq (aux t1) (aux t2)
| trm_let x t1 t2 =>
match is_val_fix x t1 with
| Some (xs,t1) => Trm_let_fix x xs (aux t1) (aux t2)
| None => Trm_let x (aux t1) (aux t2)
end
| trm_app v1 v2s => Trm_app v1 v2s
| trm_while t1 t2 => Trm_while (aux t1) (aux t2)
end.
*)
(*------------------------------------------------------------------*)
(*------------------------------------------------------------------*)
(*------------------------------------------------------------------*)
(* FOR LATER -- Alternative formulation
| red_new : forall ma mb ks vs l kvs,
No_duplicates ks ->
Forall3 (fun kv k v => kv = (val_pair (val_field k) v)) kvs ks vs ->
mb = (state_record l ks vs) ->
\# ma mb ->
red ma (prim_new kvs) (mb \+ ma) (val_loc l)
| red_if_val : forall m1 m2 v r t1 t2,
red m1 (If v = val_int 0 then t2 else t1) m2 r ->
red m1 (trm_if v t1 t2) m2 r
| red_while_true : forall m1 m2 m3 m4 t1 t2 v1 v2 v3,
red m1 t1 m2 v1 ->
v1 <> val_int 0 ->
red m2 t2 m3 v2 ->
red m3 (trm_while t1 t2) m4 v3 ->
red m1 (trm_while t1 t2) m4 val_unit
| red_while_false : forall m1 m2 t1 t2 v1,
red m1 t1 m2 v1 ->
v1 = val_int 0 ->
red m1 (trm_while t1 t2) m2 val_unit
*)
(* FOR LATER
Notation "'And_' v1 `&&` F2" :=
(!If (fun H Q => (v1 = true -> F2 H Q) /\ (v1 = false -> (Ret false) H Q)))
(at level 69, v1 at level 0) : trm_scope.
Notation "'Or_' v1 `||` F2" :=
(!If (fun H Q => (v1 = true -> (Ret true) H Q) /\ (v1 = false -> F2 H Q)))
(at level 69, v1 at level 0) : trm_scope.
Notation "'For' i '=' a 'To' b 'Do' F1 'Done_'" :=
(!For (fun H Q => forall S:int->~~unit, CFHeaps.is_local_pred S ->
(forall i H Q,
(If_ isTrue (i <= (b)%Z) Then (F1 ;; S (i+1)) Else (Ret tt)) H Q
-> S i H Q)
-> S a H Q))
(at level 69, i ident, a at level 0, b at level 0,
format "'[v' 'For' i '=' a 'To' b 'Do' '/' '[' F1 ']' '/' 'Done_' ']'")
: trm_scope.
*)
(* LATER
Notation "`{ f1 := x1 }'" :=
((f1, x1)::nil)
(at level 0, f1 at level 0)
: trm_scope.
Notation "`{ f1 := x1 ; f2 := x2 }'" :=
((f1, x1)::(f2, x2)::nil)
(at level 0, f1 at level 0, f2 at level 0)
: trm_scope.
Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 }'" :=
((f1, x1)::(f2, x2)::(f3, x3)::nil)
(at level 0, f1 at level 0, f2 at level 0, f3 at level 0)
: trm_scope.
Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 }'" :=
((f1, x1)::(f2, x2)::(f3, x3)::(f4, x4)::nil)
(at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0)
: trm_scope.
Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 ; f5 := x5 }'" :=
((f1, x1)::(f2, x2)::(f3, x3)::(f4, x4)::(f5, x5)::nil)
(at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0,
f5 at level 0)
: trm_scope.
Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 ; f5 := x5 ; f6 := x6 }'" :=
((f1, x1)::(f2, x2)::(f3, x3)::(f4, x4)::(f5, x5)::
(f6, x6)::nil)
(at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0,
f5 at level 0, f6 at level 0)
: trm_scope.
Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 ; f5 := x5 ; f6 := x6 ; f7 := x7 }'" :=
((f1, x1)::(f2, x2)::(f3, x3)::(f4, x4)::(f5, x5)::
(f6, x6)::(f7, x7)::nil)
(at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0,
f5 at level 0, f6 at level 0, f7 at level 0)
: trm_scope.
Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 ; f5 := x5 ; f6 := x6 ; f7 := x7 ; f8 := x8 }'" :=
((f1, x1)::(f2, x2)::(f3, x3)::(f4, x4)::(f5, x5)::
(f6, x6)::(f7, x7)::(f8, x8)::nil)
(at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0,
f5 at level 0, f6 at level 0, f7 at level 0, f8 at level 0)
: trm_scope.
*)
......@@ -57,6 +57,9 @@ Proof using. intros. unfolds. rewrite~ local_local. Qed.
Hint Resolve local_is_local.
Ltac xlocal_core tt ::=
try first [ applys local_is_local | applys is_local_triple | assumption ].
(********************************************************************)
(* ** Characteristic formula generator *)
......@@ -115,49 +118,6 @@ Coercion trm_of_Trm : Trm >-> trm.
(** Reciprocal translation from [trm] to [trm]. *)
(*
Definition is_val (t:trm) : option val :=
match t with
| trm_val v => Some v
| _ => None
end.
| trm_if t0 t1 t2 =>
match is_val t0 with
| Some v => Trm_if_val v (aux t1) (aux t2)
| None => Trm_if (aux t0) (aux t1) (aux t2)
end
*)
(* REJECTED FOR TERMINATION REASONS
Definition is_val_fix (f:var) (t:trm) : option (vars*trm) :=
match t with
| trm_val (val_fix f' xs t) =>
if eq_var_dec f f' then None else Some (xs,t)
| _ => None
end.
Fixpoint Trm_of_trm (t : trm) : Trm :=
let aux := Trm_of_trm in
match t with
| trm_val v => Trm_val v
| trm_if t0 t1 t2 =>
match is_val t0 with
| Some v => Trm_if_val v (aux t1) (aux t2)
| None => Trm_if (aux t0) (aux t1) (aux t2)
end
| trm_seq t1 t2 => Trm_seq (aux t1) (aux t2)
| trm_let x t1 t2 =>
match is_val_fix x t1 with
| Some (xs,t1) => Trm_let_fix x xs (aux t1) (aux t2)
| None => Trm_let x (aux t1) (aux t2)
end
| trm_app v1 v2s => Trm_app v1 v2s
| trm_while t1 t2 => Trm_while (aux t1) (aux t2)
end.
*)
Fixpoint Trm_of_trm (t : trm) : Trm :=
let aux := Trm_of_trm in
match t with
......@@ -249,11 +209,11 @@ End Reciprocal.
(*------------------------------------------------------------------*)
(* ** Definition of the [app] predicate *)
(** The proposition [app f v H Q] asserts that the application
of [f] to [v] has [H] as pre-condition and [Q] as post-condition. *)
(** The proposition [app f vs H Q] asserts that the application
of [f] to [vs] has [H] as pre-condition and [Q] as post-condition. *)
Definition app f v H Q :=
triple (trm_app f v) H Q.
Definition app f vs H Q :=
triple (trm_app f vs) H Q.
(*------------------------------------------------------------------*)
......@@ -308,14 +268,15 @@ Definition cf_fix2 (F1of : val -> val -> val -> formula)
(F2of F) H Q.
*)
Definition cf_false : formula := fun H Q =>
Definition cf_fail : formula := fun H Q =>
False.
(*------------------------------------------------------------------*)
(* ** Instance of [app] for primitive operations *)
(* TODO LATER
(* LATER
Lemma app_ref : forall v,
app prim_ref v \[] (fun r => Hexists l, \[r = val_loc l] \* l`.`f ~~> v).
Proof using. applys rule_ref. Qed.
......@@ -354,7 +315,7 @@ Definition cf_def cf (t:Trm) :=
end in
local (G (fun F => cf (subst_Trm [(f,F)] t2)))
| Trm_app f vs => local (cf_app f vs)
| Trm_while t1 t2 => local cf_false (* TODO: later *)
| Trm_while t1 t2 => local cf_fail (* TODO: later *)
end.
Definition cf := FixFun cf_def.
......@@ -497,15 +458,133 @@ Qed.
(********************************************************************)
(* ** Practical proofs using characteristic formulae *)
Theorem cf_sound_app : forall n F vs (f:var) (xs:vars) (t:trm) H Q,
F = val_fix f xs t ->
length xs = length vs ->
func_iter n cf_def cf (Trm_of_trm (subst_trm (List.combine (f::xs) (F::vs)) t)) H Q ->
app F vs H Q.
Proof using.
introv EF EL M. rewrite <- cf_unfold_iter in M.
applys* rule_app. applys~ cf_sound.
Qed.
Theorem cf_sound_app1 : forall n F v (f:var) (x:var) (t:trm) H Q,
F = val_fix f [x] t ->
func_iter n cf_def cf (Trm_of_trm (subst_trm (List.combine (f::x::nil) (F::v::nil)) t)) H Q ->
app F [v] H Q.
Proof using. introv EF M. applys* cf_sound_app. Qed.
(*------------------------------------------------------------------*)
(* ** Notation for characteristic formulae *)
Notation "'Ret' v" :=
(local (cf_val v))
(at level 69) : charac.
Notation "'If_' v 'Then' F1 'Else' F2" :=
(local (cf_if_val v F1 F2))
(at level 69, v at level 0) : charac.
Notation "'Seq_' F1 ;; F2" :=
(local (cf_seq F1 F2))
(at level 68, right associativity,
format "'[v' 'Seq_' '[' F1 ']' ;; '/' '[' F2 ']' ']'") : charac.
Notation "'Let' x ':=' F1 'in' F2" :=
(local (cf_let F1 (fun x => F2)))
(at level 69, x ident, right associativity,
format "'[v' '[' 'Let' x ':=' F1 'in' ']' '/' '[' F2 ']' ']'") : charac.
Notation "'App' f x1 ;" :=
(local (cf_app f [x1]))
(at level 68, f at level 0, x1 at level 0) : charac.
Notation "'App' f x1 x2 ;" :=
(local (cf_app f [x1; x2]))
(at level 68, f at level 0, x1 at level 0,
x2 at level 0) : charac.
Notation "'App' f x1 x2 x3 ;" :=
(local (cf_app f [x1; x2; x3]))
(at level 68, f at level 0, x1 at level 0, x2 at level 0,
x3 at level 0) : charac.
Notation "'App' f x1 x2 x3 x4 ;" :=
(local (cf_app f [x1; x2; x3; x4]))
(at level 68, f at level 0, x1 at level 0, x2 at level 0,
x3 at level 0, x4 at level 0) : charac.
Notation "'Fail'" :=
(local cf_fail)
(at level 69) : charac.
Open Scope charac.
(*--------------------------------------------------------*)
(* ** Tactic [xspec] *)
(** [xspec] shows the specification that [xapp] would use. More generally,
[xspec f] retreives from either the context or from
the database of characteristic formulae (i.e. "database_spec")
the specification associated with [f].
It places the specification as hypothesis at the head of the goal. *)
Definition database_spec := True.
Notation "'RegisterSpec' T" := (Register database_spec T)
(at level 69) : charac.
Tactic Notation "xspec" constr(f) :=
ltac_database_get database_spec f.
(*--------------------------------------------------------*)
(* ** Tactics for conducting proofs *)
Tactic Notation "xcf" :=
let f := match goal with |- app ?f _ _ _ => constr:(f) end in
applys cf_sound_app1 20%nat;
[ try reflexivity
| simpl; try fold f].
Tactic Notation "xret" :=
applys local_erase; unfold cf_val.
Tactic Notation "xif" :=
applys local_erase; split.
Tactic Notation "xlet" :=
applys local_erase; esplit; split.
Tactic Notation "xapp" constr(E) :=
applys local_erase; unfold cf_app;
xapplys E.
Tactic Notation "xapp" :=
applys local_erase; unfold cf_app;
let G := match goal with |- ?G => constr:(G) end in
xspec G;
let H := fresh "TEMP" in intros H;
xapplys H;
clear H.
Tactic Notation "xfail" :=
applys local_erase; unfold cf_fail.
(*--------------------------------------------------------*)
(* ** Registering specifications for primitive functions *)
Hint Extern 1 (RegisterSpec (app (val_prim prim_neq) _ _ _)) =>
Provide rule_neq.
Hint Extern 1 (RegisterSpec (app (val_prim prim_add) _ _ _)) =>
Provide rule_add.
......@@ -409,100 +409,3 @@ Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 }" :=
(at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0)
: trm_scope.
(*------------------------------------------------------------------*)
(*------------------------------------------------------------------*)
(*------------------------------------------------------------------*)
(* FOR LATER -- Alternative formulation
| red_new : forall ma mb ks vs l kvs,
No_duplicates ks ->
Forall3 (fun kv k v => kv = (val_pair (val_field k) v)) kvs ks vs ->
mb = (state_record l ks vs) ->
\# ma mb ->
red ma (prim_new kvs) (mb \+ ma) (val_loc l)
| red_if_val : forall m1 m2 v r t1 t2,
red m1 (If v = val_int 0 then t2 else t1) m2 r ->
red m1 (trm_if v t1 t2) m2 r
| red_while_true : forall m1 m2 m3 m4 t1 t2 v1 v2 v3,
red m1 t1 m2 v1 ->
v1 <> val_int 0 ->
red m2 t2 m3 v2 ->
red m3 (trm_while t1 t2) m4 v3 ->
red m1 (trm_while t1 t2) m4 val_unit
| red_while_false : forall m1 m2 t1 t2 v1,
red m1 t1 m2 v1 ->
v1 = val_int 0 ->
red m1 (trm_while t1 t2) m2 val_unit
*)
(* FOR LATER
Notation "'And_' v1 `&&` F2" :=
(!If (fun H Q => (v1 = true -> F2 H Q) /\ (v1 = false -> (Ret false) H Q)))
(at level 69, v1 at level 0) : trm_scope.
Notation "'Or_' v1 `||` F2" :=
(!If (fun H Q => (v1 = true -> (Ret true) H Q) /\ (v1 = false -> F2 H Q)))
(at level 69, v1 at level 0) : trm_scope.
Notation "'For' i '=' a 'To' b 'Do' F1 'Done_'" :=
(!For (fun H Q => forall S:int->~~unit, CFHeaps.is_local_pred S ->
(forall i H Q,
(If_ isTrue (i <= (b)%Z) Then (F1 ;; S (i+1)) Else (Ret tt)) H Q
-> S i H Q)
-> S a H Q))
(at level 69, i ident, a at level 0, b at level 0,
format "'[v' 'For' i '=' a 'To' b 'Do' '/' '[' F1 ']' '/' 'Done_' ']'")
: trm_scope.
*)
(* LATER
Notation "`{ f1 := x1 }'" :=
((f1, x1)::nil)
(at level 0, f1 at level 0)
: trm_scope.
Notation "`{ f1 := x1 ; f2 := x2 }'" :=
((f1, x1)::(f2, x2)::nil)
(at level 0, f1 at level 0, f2 at level 0)
: trm_scope.
Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 }'" :=
((f1, x1)::(f2, x2)::(f3, x3)::nil)
(at level 0, f1 at level 0, f2 at level 0, f3 at level 0)
: trm_scope.
Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 }'" :=
((f1, x1)::(f2, x2)::(f3, x3)::(f4, x4)::nil)
(at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0)
: trm_scope.
Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 ; f5 := x5 }'" :=
((f1, x1)::(f2, x2)::(f3, x3)::(f4, x4)::(f5, x5)::nil)
(at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0,
f5 at level 0)
: trm_scope.
Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 ; f5 := x5 ; f6 := x6 }'" :=
((f1, x1)::(f2, x2)::(f3, x3)::(f4, x4)::(f5, x5)::
(f6, x6)::nil)
(at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0,
f5 at level 0, f6 at level 0)
: trm_scope.
Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 ; f5 := x5 ; f6 := x6 ; f7 := x7 }'" :=
((f1, x1)::(f2, x2)::(f3, x3)::(f4, x4)::(f5, x5)::
(f6, x6)::(f7, x7)::nil)
(at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0,
f5 at level 0, f6 at level 0, f7 at level 0)
: trm_scope.
Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 ; f5 := x5 ; f6 := x6 ; f7 := x7 ; f8 := x8 }'" :=
((f1, x1)::(f2, x2)::(f3, x3)::(f4, x4)::(f5, x5)::
(f6, x6)::(f7, x7)::(f8, x8)::nil)
(at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0,
f5 at level 0, f6 at level 0, f7 at level 0, f8 at level 0)
: trm_scope.
*)
......@@ -9,6 +9,7 @@ Set Implicit Arguments.
Require Import LibCore ModelSepML ModelCFML.
Open Scope trm_scope.
Open Scope heap_scope.
Open Scope charac.
Ltac auto_star ::= jauto.
......@@ -50,9 +51,10 @@ Lemma MList_null : forall L,
Proof using.
intros. destruct L.
{ xunfold MList. applys himpl_antisym; hsimpl~. }
{ (* TODO: record points to null is false lemma
xunfold MList. applys himpl_antisym. *)
admit. }
{ xunfold MList. applys himpl_antisym.
{ hpull ;=> p'. hchange (hprop_record_not_null null); auto_false.
hpull; auto_false. }
{ hpull. } }
Qed.
Lemma MList_null_keep : forall L,
......@@ -110,12 +112,16 @@ Global Opaque MList.
(********************************************************************)
(* * TODO: explicit specification for "hd", will be computed on the fly *)
(* * Auxiliary lemmas *)
Parameter rule_get_tl : forall p x p',
triple (trm_app prim_get [val_loc p; val_field tl])
(p ~> Record `{ hd := x; tl := p'})
(fun r => \[r = p'] \* p ~> Record `{ hd := x; tl := p'}).
(* TODO: this specification will be computed on the fly using a tactic *)
Hint Extern 1 (RegisterSpec (app (val_prim prim_get) [_;val_field tl] _ _)) =>
Provide rule_get_tl.
(********************************************************************)
......@@ -157,15 +163,14 @@ Ltac simpl_subst := simpl; autorewrite with rew_subst.
(********************************************************************)
(* * Mutable list increment verification, using triples *)
(** Program specification and verification *)
Section ProofWithTriples.
Lemma mlist_incr_spec : forall L p,
triple (trm_app mlist_length [val_loc p])
(p ~> MList L)
(fun r => \[r = val_int (length L)] \* p ~> MList L).
Proof using.
intros L. induction_wf: list_sub_wf L.
intros p.
intros L. induction_wf: list_sub_wf L. intros p.
applys rule_app; try reflexivity.
Transparent mlist_length.
simpl_subst.
......@@ -183,189 +188,37 @@ Proof using.
applys rule_let.
{ xapplys IH. { subst~. } }
{ simpl_subst. intros r. xpull. intros Er. xchange (MList_uncons p).
subst r. xapplys rule_add. subst. rew_length. fequals. math. } } }
subst r. xapplys rule_add. subst. rew_length. fequals. math. } } }
Qed.
End ProofWithTriples.
(********************************************************************)
(* * Mutable list increment verification, using characteristic formulae *)
(** Remark: in Ltac script below, "=>" is an alias for "intros" *)
Notation "'Ret' v" :=
(local (cf_val v))
(at level 69) : charac.
Notation "'If_' v 'Then' F1 'Else' F2" :=
(local (cf_if_val v F1 F2))
(at level 69, v at level 0) : charac.
Notation "'Seq_' F1 ;; F2" :=
(local (cf_seq F1 F2))
(at level 68, right associativity,
format "'[v' 'Seq_' '[' F1 ']' ;; '/' '[' F2 ']' ']'") : charac.
Notation "'Let' x ':=' F1 'in' F2" :=
(local (cf_let F1 (fun x => F2)))
(at level 69, x ident, right associativity,
format "'[v' '[' 'Let' x ':=' F1 'in' ']' '/' '[' F2 ']' ']'") : charac.
Notation "'App' f x1 ;" :=
(local (cf_app f [x1]))
(at level 68, f at level 0, x1 at level 0) : charac.
Notation "'App' f x1 x2 ;" :=
(local (cf_app f [x1; x2]))
(at level 68, f at level 0, x1 at level 0,
x2 at level 0) : charac.
Open Scope charac.
(*--------------------------------------------------------*)
(* ** [xspec] *)
(** [xspec] shows the specification that [xapp] would use. More generally,
[xspec f] retreives from either the context or from
the database of characteristic formulae (i.e. "database_spec")
the specification associated with [f].
It places the specification as hypothesis at the head of the goal. *)
Definition database_spec := True.
Notation "'RegisterSpec' T" := (Register database_spec T)
(at level 69) : charac.
Tactic Notation "xspec" constr(f) :=
ltac_database_get database_spec f.
Hint Extern 1 (RegisterSpec (app (val_prim prim_neq) _ _ _)) =>
Provide rule_neq.
Hint Extern 1 (RegisterSpec (app (val_prim prim_get) [_;val_field tl] _ _)) =>
Provide rule_get_tl.
Hint Extern 1 (RegisterSpec (app (val_prim prim_add) _ _ _)) =>
Provide rule_add.
(*--------------------------------------------------------*)
(* ** [x-tactics] *)
Tactic Notation "xret" :=
applys local_erase; unfold cf_val.
Tactic Notation "xif" :=
applys local_erase; split.
Tactic Notation "xlet" :=
applys local_erase; esplit; split.