Commit a28dbcd8 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Whitespace.

parent 96980126
(**
This file contains common declarations for examples in
This file contains common declarations for examples in
lifted Separation Logic, using lifted characteristic formulae.
Author: Arthur Charguéraud.
......
(**
This file formalizes basic examples in lifted Separation Logic,
This file formalizes basic examples in lifted Separation Logic,
both using lifted characteristic formulae.
Author: Arthur Charguéraud.
......@@ -27,7 +27,7 @@ Implicit Types n : int.
Lemma Rule_swap_neq : forall A1 A2 `{EA1:Enc A1} `{EA2:Enc A2} (v:A1) (w:A2) p q,
Triple (val_swap `p `q)
PRE (p ~~> v \* q ~~> w)
PRE (p ~~> v \* q ~~> w)
POST (fun (r:unit) => p ~~> w \* q ~~> v).
Proof using.
xcf. xapps. xapps. xapps. xapps. hsimpl~.
......@@ -35,7 +35,7 @@ Qed.
Lemma Rule_swap_eq : forall A1 `{EA1:Enc A1} (v:A1) p,
Triple (val_swap `p `p)
PRE (p ~~> v)
PRE (p ~~> v)
POST (fun (r:unit) => p ~~> v).
Proof using.
xcf. xapps. xapps. xapps. xapps. hsimpl~.
......@@ -47,9 +47,9 @@ Qed.
(** [val_example_let] defined in [ExampleBasicNonlifted.v] *)
Lemma Rule_val_example_let : forall n,
Lemma Rule_val_example_let : forall n,
Triple (val_example_let n)
PRE \[]
PRE \[]
POST (fun r => \[r = 2*n]).
Proof using.
xcf. xapps. xapps. xapp. hsimpl. math.
......@@ -61,9 +61,9 @@ Qed.
(** [val_example_one_ref] defined in [ExampleBasicNonlifted.v] *)
Lemma Rule_val_example_one_ref : forall n,
Lemma Rule_val_example_one_ref : forall n,
Triple (val_example_one_ref n)
PRE \[]
PRE \[]
POST (fun r => \[r = n+2]).
Proof using.
xcf. xapps. xapps ;=> r. xapp~. xapp~. hsimpl. math.
......@@ -75,9 +75,9 @@ Qed.
(** [val_example_two_ref] defined in [ExampleBasicNonlifted.v] *)
Lemma Rule_val_example_two_ref : forall n,
Lemma Rule_val_example_two_ref : forall n,
Triple (val_example_two_ref n)
PRE \[]
PRE \[]
POST (fun r => \[r = n+1]).
Proof using.
xcf. xapp ;=> i. xapp ;=> r.
......@@ -165,23 +165,23 @@ Qed.
let fib_for n =
let a = ref 0 in
let b = ref 1 in
for i = 0 to n-1 do
for i = 0 to n-1 do
let c = !a + !b in
a := !b;
b := c;
done;
!a
(***********************************************************************)
(** While loops *)
let example_while n =
let i = ref 0 in
let i = ref 0 in
let r = ref 0 in
while !i < n do
incr i;
incr r;
incr r;
done;
!r
......@@ -209,13 +209,13 @@ Qed.
(** Recursion *)
let rec facto_rec n =
if n <= 1
if n <= 1
then 1
else n * facto_rec(n-1)
let rec fib_rec n =
if n <= 1
then n
if n <= 1
then n
else fib_rec(n-1) + fib_rec(n-2)
......@@ -474,4 +474,4 @@ Qed.
(* </EXO> *)
Qed.
*)
\ No newline at end of file
*)
(**
This file formalizes basic examples in plain Separation Logic,
This file formalizes basic examples in plain Separation Logic,
both using triples directly and using characteristic formulae.
Author: Arthur Charguéraud.
......@@ -28,7 +28,7 @@ Implicit Types n : int.
(* From LambdaStruct
Definition val_incr :=
ValFun 'p :=
ValFun 'p :=
Let 'n := val_get 'p in
Let 'm := 'n '+ 1 in
val_set 'p 'm.
......@@ -36,9 +36,9 @@ Definition val_incr :=
(** Low-level proof *)
Lemma rule_incr_1 : forall p n,
Lemma rule_incr_1 : forall p n,
triple (val_incr p)
(p ~~~> n)
(p ~~~> n)
(fun r => \[r = val_unit] \* (p ~~~> (n+1))).
Proof using.
intros. applys rule_app_fun. reflexivity. simpl.
......@@ -47,7 +47,7 @@ Proof using.
applys rule_let.
{ applys rule_frame_consequence (p ~~~> n).
{ hsimpl. }
{ applys rule_add. }
{ applys rule_add. }
{ hsimpl. } }
simpl. intros y. apply rule_extract_hprop. intros E. subst.
applys rule_consequence.
......@@ -59,9 +59,9 @@ Qed.
(** Same proof using [xapply], [xapplys] and [xpull] *)
Lemma rule_incr_2 : forall p n,
Lemma rule_incr_2 : forall p n,
triple (val_incr p)
(p ~~~> n)
(p ~~~> n)
(fun r => \[r = val_unit] \* (p ~~~> (n+1))).
Proof using.
intros. applys rule_app_fun. reflexivity. simpl.
......@@ -74,16 +74,16 @@ Qed.
(** Same proof using characteristic formulae without tactics *)
Lemma rule_incr_3 : forall p n,
Lemma rule_incr_3 : forall p n,
triple (val_incr p)
(p ~~~> n)
(p ~~~> n)
(fun r => \[r = val_unit] \* (p ~~~> (n+1))).
Proof using.
intros. applys triple_app_fun_of_cf_iter 20%nat. reflexivity. simpl.
intros. applys triple_app_fun_of_cf_iter 20%nat. reflexivity. simpl.
applys local_erase. esplit. split.
{ applys local_erase. xapplys rule_get. }
intros x. xpull. intros E. subst.
applys local_erase. esplit. split.
applys local_erase. esplit. split.
{ applys local_erase. xapplys rule_add. }
intros y. xpull. intros E. subst.
applys local_erase. xapplys rule_set. auto.
......@@ -91,25 +91,25 @@ Qed.
(** Same proof using support for nary functions *)
Lemma rule_incr_4 : forall p n,
Lemma rule_incr_4 : forall p n,
triple (val_incr p)
(p ~~~> n)
(p ~~~> n)
(fun r => \[r = val_unit] \* (p ~~~> (n+1))).
Proof using.
intros. rew_nary. unfold val_incr.
intros. rew_nary. unfold val_incr.
rew_nary. rew_vals_to_trms. (* show coercion *)
applys triple_apps_funs_of_cf_iter 20%nat.
{ reflexivity. }
{ reflexivity. }
simpl.
simpl.
(* then continue as before *)
Abort.
(** Same proof using characteristic formulae with tactics *)
Lemma rule_incr_5 : forall p n,
Lemma rule_incr_5 : forall p n,
triple (val_incr p)
(p ~~~> n)
(p ~~~> n)
(fun r => \[r = val_unit] \* (p ~~~> (n+1))).
Proof using.
xcf. xlet as x. xapp. xpull. intro_subst.
......@@ -119,9 +119,9 @@ Qed.
(** Same proof using characteristic formulae with more tactics *)
Lemma rule_incr_6 : forall p n,
Lemma rule_incr_6 : forall p n,
triple (val_incr p)
(p ~~~> n)
(p ~~~> n)
(fun r => \[r = val_unit] \* (p ~~~> (n+1))).
Proof using.
xcf. xapp as x. intro_subst.
......@@ -132,11 +132,11 @@ Qed.
(** Same proof using characteristic formulae with yet more
powerful tactics *)
Lemma rule_incr__7 : forall p n,
Lemma rule_incr__7 : forall p n,
triple (val_incr p)
(p ~~~> n)
(p ~~~> n)
(fun r => \[r = val_unit] \* (p ~~~> (n+1))).
Proof using.
Proof using.
xcf. xapps. xapps. xapps. hsimpl~.
Qed.
......@@ -144,11 +144,11 @@ Hint Extern 1 (Register_spec val_incr) => Provide rule_incr__7.
(* ---------------------------------------------------------------------- *)
(** Calling incr from a larger context *)
(** Calling incr from a larger context *)
Lemma rule_incr_with_other_1 : forall p n q m,
Lemma rule_incr_with_other_1 : forall p n q m,
triple (val_incr p)
(p ~~~> n \* q ~~~> m)
(p ~~~> n \* q ~~~> m)
(fun r => \[r = val_unit] \* (p ~~~> (n+1)) \* q ~~~> m).
Proof using.
intros. applys rule_frame_consequence (q ~~~> m).
......@@ -157,9 +157,9 @@ Proof using.
{ intros r. hsimpl. auto. }
Qed.
Lemma rule_incr_with_other_2 : forall p n q m,
Lemma rule_incr_with_other_2 : forall p n q m,
triple (val_incr p)
(p ~~~> n \* q ~~~> m)
(p ~~~> n \* q ~~~> m)
(fun r => \[r = val_unit] \* (p ~~~> (n+1)) \* q ~~~> m).
Proof using.
intros. xapply rule_incr_5.
......@@ -167,15 +167,15 @@ Proof using.
{ intros r. hsimpl. auto. }
Qed.
Lemma rule_incr_with_other : forall p n q m,
Lemma rule_incr_with_other : forall p n q m,
triple (val_incr p)
(p ~~~> n \* q ~~~> m)
(p ~~~> n \* q ~~~> m)
(fun r => \[r = val_unit] \* (p ~~~> (n+1)) \* q ~~~> m).
Proof using. intros. xapps. hsimpl~. Qed.
Lemma rule_incr_with_frame : forall p n H,
Lemma rule_incr_with_frame : forall p n H,
triple (val_incr p)
(p ~~~> n \* H)
(p ~~~> n \* H)
(fun r => \[r = val_unit] \* (p ~~~> (n+1)) \* H).
Proof using. intros. xapps. hsimpl~. Qed.
......@@ -184,23 +184,23 @@ Proof using. intros. xapps. hsimpl~. Qed.
(** Swap function *)
Definition val_swap :=
ValFun 'p 'q :=
ValFun 'p 'q :=
Let 'x := val_get 'p in
Let 'y := val_get 'q in
val_set 'p 'y ;;;
val_set 'q 'x.
Lemma rule_swap_neq : forall p q v w,
Lemma rule_swap_neq : forall p q v w,
triple (val_swap p q)
(p ~~~> v \* q ~~~> w)
(p ~~~> v \* q ~~~> w)
(fun r => \[r = val_unit] \* p ~~~> w \* q ~~~> v).
Proof using.
xcf. xapps. xapps. xapp~. xapps. hsimpl~.
Qed.
Lemma rule_swap_eq : forall p v,
Lemma rule_swap_eq : forall p v,
triple (val_swap p p)
(p ~~~> v)
(p ~~~> v)
(fun r => \[r = val_unit] \* p ~~~> v).
Proof using.
xcf. xapps. xapps. xapp~. xapps. hsimpl~.
......@@ -211,15 +211,15 @@ Qed.
(** Succ function using incr *)
Definition val_succ_using_incr :=
ValFun 'n :=
ValFun 'n :=
Let 'p := val_ref 'n in
val_incr 'p ;;;
Let 'x := val_get 'p in
Let 'x := val_get 'p in
'x.
Lemma rule_succ_using_incr : forall n,
Lemma rule_succ_using_incr : forall n,
triple (val_succ_using_incr n)
\[]
\[]
(fun r => \[r = n+1]).
Proof using.
xcf. xapp as p. intros; subst. xapp~. xapps~.
......@@ -238,11 +238,11 @@ Qed.
*)
Definition val_incr_twice :=
ValFun 'p :=
ValFun 'p :=
val_incr 'p ;;;
val_incr 'p.
Lemma rule_incr_twice : forall p n,
Lemma rule_incr_twice : forall p n,
triple (val_incr_twice p)
(p ~~~> n)
(fun r => \[r = val_unit] \* p ~~~> (n+2)).
......@@ -259,14 +259,14 @@ Qed.
(** Basic let-binding example *)
Definition val_example_let :=
ValFun 'n :=
ValFun 'n :=
Let 'a := 'n '+ 1 in
Let 'b := 'n '- 1 in
'a '+ 'b.
Lemma rule_val_example_let : forall n,
Lemma rule_val_example_let : forall n,
triple (val_example_let n)
\[]
\[]
(fun r => \[r = 2*n]).
Proof using.
xcf. xapps. xapps. xapp.
......@@ -279,21 +279,21 @@ Qed.
(*
let val_example_one_ref n =
let i = ref 0 in
let i = ref 0 in
incr i;
!i
*)
Definition val_example_one_ref :=
ValFun 'n :=
ValFun 'n :=
Let 'k := 'n '+ 1 in
Let 'i := 'ref 'k in
val_incr 'i ;;;
'!'i.
Lemma rule_example_one_ref : forall n,
Lemma rule_example_one_ref : forall n,
triple (val_example_one_ref n)
\[]
\[]
(fun r => \[r = n+2]).
Proof using.
xcf.
......@@ -310,8 +310,8 @@ Qed.
(*
let val_example_two_ref n =
let i = ref 0 in
let r = ref n in
let i = ref 0 in
let r = ref n in
decr r;
incr i;
r := !i + !r;
......@@ -319,7 +319,7 @@ Qed.
*)
Definition val_example_two_ref :=
ValFun 'n :=
ValFun 'n :=
Let 'i := 'ref 0 in
Let 'r := 'ref 'n in
val_decr 'r ;;;
......@@ -332,9 +332,9 @@ Definition val_example_two_ref :=
Let 'r2 := '!'r in
'i2 '+ 'r2.
Lemma rule_example_two_ref : forall n,
Lemma rule_example_two_ref : forall n,
triple (val_example_two_ref n)
\[]
\[]
(fun r => \[r = n+1]).
Proof using.
xcf. xapp ;=> i i' Ei. subst.
......@@ -343,12 +343,3 @@ Proof using.
xapps. xapps. xapps.
hsimpl. intros. subst. fequals. math.
Qed.
(**
This file formalizes examples of first-class functions in plain
This file formalizes examples of first-class functions in plain
Separation Logic, using lifted characteristic formulae.
Author: Arthur Charguéraud.
......@@ -35,7 +35,7 @@ Qed.
Lemma Rule_apply' : forall (f:func) `{EA:Enc A} (x:A),
forall (H:hprop) `{EB:Enc B} (Q:B->hprop),
Triple (val_apply f `x)
Triple (val_apply f `x)
PRE (\[Triple (f `x) H Q] \* H)
POST Q.
Proof using. intros. xpull ;=> M. applys~ Rule_apply. Qed.
......@@ -46,19 +46,19 @@ Proof using. intros. xpull ;=> M. applys~ Rule_apply. Qed.
(* * RefApply function *)
Definition val_refapply : val :=
ValFun 'f 'r :=
ValFun 'f 'r :=
Let 'x := val_get 'r in
Let 'y := 'f 'x in
val_set 'r 'y.
Lemma Rule_refapply_pure : forall (f:func) `{EA:Enc A} (r:loc) (x:A),
forall `{EB:Enc B} (P:A->B->Prop),
Triple (f `x)
PRE \[]
POST (fun y => \[P x y])
Triple (f `x)
PRE \[]
POST (fun y => \[P x y])
->
Triple (val_refapply `f `r)
PRE (r ~~> x)
Triple (val_refapply `f `r)
PRE (r ~~> x)
POST (fun (_:unit) => Hexists y, \[P x y] \* r ~~> y).
Proof using.
introv M. xcf. xapps. xapp ;=> y E. xapp. hsimpl~.
......@@ -66,12 +66,12 @@ Qed.
Lemma Rule_refapply_effect : forall (f:func) `{EA:Enc A} (r:loc) (x:A),
forall `{EB:Enc B} (P:A->B->Prop) (H H':hprop),
Triple (f `x)
PRE H
POST (fun y => \[P x y] \* H')
Triple (f `x)
PRE H
POST (fun y => \[P x y] \* H')
->
Triple (val_refapply `f `r)
PRE (r ~~> x \* H)
Triple (val_refapply `f `r)
PRE (r ~~> x \* H)
POST (fun (_:unit) => Hexists y, \[P x y] \* r ~~> y \* H').
Proof using.
introv M. xcf. xapps. xapp ;=> y E. xapp. hsimpl~.
......@@ -83,7 +83,7 @@ Qed.
(* * Twice function *)
Definition val_twice : val :=
ValFun 'f :=
ValFun 'f :=
'f '() ;;;
'f '().
......@@ -100,8 +100,8 @@ Qed.
(* * Repeat function *)
Definition val_repeat : val :=
ValFun 'n 'f :=
For 'i := 1 To 'n Do
ValFun 'n 'f :=
For 'i := 1 To 'n Do
'f '()
Done.
......@@ -127,11 +127,11 @@ Proof using. math. Qed.
Lemma Rule_repeat : forall (I:int->hprop) (f:func) (n:int),
n >= 0 ->
(forall i, 0 <= i < n ->
Triple (f `tt)
Triple (f `tt)
PRE (I i)
POST (fun (_:unit) => I (i+1)))
->
Triple (val_repeat `n `f)
Triple (val_repeat `n `f)
PRE (I 0)
POST (fun (_:unit) => I n).
Proof using.
......@@ -141,9 +141,9 @@ Proof using.
applys local_erase. applys xfor_inv_lemma (fun i => (I (i-1))).
{ math. }
{ hsimpl. }
{ intros i Hi. xapp. { math. } { math_rewrite (i-1+1=i+1-1). hsimpl. } }
{ intros i Hi. xapp. { math. } { math_rewrite (i-1+1=i+1-1). hsimpl. } }
{ math_rewrite (n+1-1=n). hsimpl. }
(* todo : avoid math_rewrite,
(* todo : avoid math_rewrite,
thanks to hsimpl simplification of invariants *)
Qed.
......@@ -163,8 +163,8 @@ Implicit Types g : val.
Definition MCount (n:int) (g:val) : hprop :=
Hexists p, (p ~~> n) \*
\[ forall n', Triple (g val_unit)
(p ~~> n')
\[ forall n', Triple (g val_unit)
(p ~~> n')
(fun r => \[r = n'+1] \* (p ~~> (n'+1))) ].
(* TODO: fix priority of p ~~> (n'+1) differently *)
......@@ -177,9 +177,9 @@ Definition MCount (n:int) (g:val) : hprop :=
Lemma Rule_MCount : forall n g,
Triple (g '()) (g ~> MCount n) (fun r => \[ r = n+1 ] \* g ~> MCount (n+1)).
Proof using.
intros. xunfolds MCount at 1 ;=> p Hg. xapp.
intros. xunfolds MCount at 1 ;=> p Hg. xapp.
hpulls. xunfold MCount. hsimpl~.
Qed.
Qed.
(* ---------------------------------------------------------------------- *)
......@@ -194,9 +194,9 @@ Definition val_mkcounter : val :=
(* ---------------------------------------------------------------------- *)
(** Verification *)
Lemma Rule_mkcounter :
Triple (val_mkcounter `val_unit)
\[]
Lemma Rule_mkcounter :
Triple (val_mkcounter `val_unit)
\[]
(fun g => g ~> MCount 0).
Proof using.
xcf. xapps ;=> r. xval. xunfold MCount. hsimpl.
......@@ -215,9 +215,9 @@ Definition trm_test_mkcounter : trm :=
Let 'm := 'c '() in
val_add 'n 'm.
Lemma rule_test_mkcounter :
Triple trm_test_mkcounter
\[]
Lemma rule_test_mkcounter :
Triple trm_test_mkcounter
\[]
(fun r => \[r = 3]).
Proof using.
xcf. xapp as C.
......@@ -226,21 +226,3 @@ Proof using.
xapps.
hsimpl~.
Qed.
This diff is collapsed.
This diff is collapsed.
(* WORK IN PROGRESS
(* WORK IN PROGRESS
......@@ -11,28 +11,28 @@
module StackList = struct
type 'a t = {
type 'a t = {
mutable items : 'a list;
mutable size : int }
let create () =
{ items = [];
let create () =
{ items = [];
size = 0 }