Commit d6da6634 authored by charguer's avatar charguer

Merge branch 'iris-proofmode-functorized'

parents 1ad5b175 3083aaa2
(**
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.
......@@ -10,7 +10,8 @@ License: MIT.
From Sep Require Export LambdaSepLifted LambdaCFLifted.
From Sep Require Export LambdaStructLifted.
From TLC Require Export LibListZ.
From TLC Require Export LibList LibListZ.
Open Scope liblist_scope.
Open Scope Z_scope.
(* Open Scope charac. TODO: not needed? *)
......
(**
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.
......@@ -26,16 +26,16 @@ Implicit Types n : int.
(** [val_swap] defined in [ExampleBasicNonlifted.v] *)
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)
Triple (val_swap ``p ``q)
PRE (p ~~> v \* q ~~> w)
POST (fun (r:unit) => p ~~> w \* q ~~> v).
Proof using.
xcf. xapps. xapps. xapps. xapps. hsimpl~.
Qed.
Lemma Rule_swap_eq : forall A1 `{EA1:Enc A1} (v:A1) p,
Triple (val_swap `p `p)
PRE (p ~~> v)
Triple (val_swap ``p ``p)
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,21 +47,21 @@ 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.
{ hsimpl. }
{ applys rule_set. }
{ intros r. applys himpl_hprop_l. intros E. subst.
applys himpl_hprop_r. { auto. } { auto. } }
{ intros r. applys himpl_hpure_l. intros E. subst.
applys himpl_hpure_r. { auto. } { auto. } }
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 '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
val_incr 'p ;;;
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 :=
val_incr '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 ;;
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,22 +319,22 @@ Qed.
*)
Definition val_example_two_ref :=
ValFun 'n :=
ValFun 'n :=
Let 'i := 'ref 0 in
Let 'r := 'ref 'n in
val_decr 'r ;;
val_incr 'i ;;
val_decr 'r ;;;
val_incr 'i ;;;
Let 'i1 := '!'i in
Let 'r1 := '!'r in
Let 's := 'i1 '+ 'r1 in
'r ':= 's ;;
'r ':= 's ;;;
Let 'i2 := '!'i in
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.
......@@ -25,8 +25,8 @@ Definition val_apply : val :=
Lemma Rule_apply : forall (f:func) `{EA:Enc A} (x:A),
forall (H:hprop) `{EB:Enc B} (Q:B->hprop),
Triple (f `x) H Q ->
Triple (val_apply `f `x) H Q.
Triple (f ``x) H Q ->
Triple (val_apply ``f ``x) H Q.
Proof using.
introv M. xcf. (* todo why not simplified? *)
unfold Substs; simpl; rew_enc_dyn.
......@@ -35,8 +35,8 @@ 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)
PRE (\[Triple (f `x) H Q] \* H)
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,14 +83,14 @@ Qed.
(* * Twice function *)
Definition val_twice : val :=
ValFun 'f :=
'f '() ;;
ValFun 'f :=
'f '() ;;;
'f '().
Lemma Rule_twice : forall (f:func) (H H':hprop) `{EB:Enc B} (Q:B->hprop),
Triple (f `tt) H (fun (_:unit) => H') ->
Triple (f `tt) H' Q ->
Triple (val_twice `f) H Q.
Triple (f ``tt) H (fun (_:unit) => H') ->
Triple (f ``tt) H' Q ->
Triple (val_twice ``f) H Q.
Proof using.
introv M1 M2. xcf. xseq. xapp M1. xapp M2. hsimpl~.
Qed.
......@@ -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,23 +127,23 @@ 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.
introv N M. xcf.
asserts_rewrite (`n = val_int n). auto. (* todo: investigate *)
asserts_rewrite (``n = val_int n). auto. (* todo: investigate *)
applys local_weaken_post. xlocal.
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.
(* ---------------------------------------------------------------------- *)
......@@ -188,15 +188,15 @@ Qed.
Definition val_mkcounter : val :=
ValFun 'u :=
Let 'p := val_ref 0 in
(Fun 'v := val_incr 'p ;; val_get 'p).
(Fun 'v := val_incr 'p ;;; val_get 'p).
(* ---------------------------------------------------------------------- *)
(** 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,32 +215,15 @@ 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.
xcf_trm 100%nat. (* todo: make xcf work *)
xapp as C.
xapps Rule_MCount.
xapps Rule_MCount.
xapps.
hsimpl~.
Qed.