 ### migrated cfml2

parent 652229b2
 (** This file contains common declarations for examples in lifted Separation Logic, using lifted characteristic formulae. Author: Arthur Charguéraud. License: MIT. *) From Sep Require Export LambdaSepLifted LambdaCFLifted. From Sep Require Export LambdaStructLifted. From TLC Require Export LibList LibListZ. Open Scope liblist_scope. Open Scope Z_scope. (* Open Scope charac. TODO: not needed? *) Ltac auto_star ::= jauto. (** Common preambule to be copied: Set Implicit Arguments. Generalizable Variables A B. *) (** Optional type declarations, e.g.: Implicit Types p : loc. Implicit Types n : int. *)
This diff is collapsed.
 (** This file formalizes basic examples in plain Separation Logic, both using triples directly and using characteristic formulae. Author: Arthur Charguéraud. License: MIT. *) Set Implicit Arguments. From Sep Require Import LambdaSep LambdaCF TLCbuffer LambdaStruct. Generalizable Variables A B. Ltac auto_star ::= jauto. Implicit Type p q : loc. Implicit Types n : int. (* ********************************************************************** *) (* * Basic functions *) (* ---------------------------------------------------------------------- *) (** Increment function -- details *) (* From LambdaStruct Definition val_incr := ValFun 'p := Let 'n := val_get 'p in Let 'm := 'n '+ 1 in val_set 'p 'm. *) (** Low-level proof *) Lemma rule_incr_1 : forall p n, triple (val_incr p) (p ~~~> n) (fun r => \[r = val_unit] \* (p ~~~> (n+1))). Proof using. intros. applys rule_app_fun. reflexivity. simpl. applys rule_let. { applys rule_get. } simpl. intros x. apply rule_extract_hprop. intros E. subst. applys rule_let. { applys rule_frame_consequence (p ~~~> n). { hsimpl. } { 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_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, triple (val_incr p) (p ~~~> n) (fun r => \[r = val_unit] \* (p ~~~> (n+1))). Proof using. intros. applys rule_app_fun. reflexivity. simpl. applys rule_let. { applys rule_get. } simpl. intros x. xpull. intros E. subst. applys rule_let. { xapplys rule_add. } simpl. intros y. xpull. intro_subst. xapplys rule_set. auto. Qed. (** Same proof using characteristic formulae without tactics *) Lemma rule_incr_3 : forall p n, triple (val_incr p) (p ~~~> n) (fun r => \[r = val_unit] \* (p ~~~> (n+1))). Proof using. 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. xapplys rule_add. } intros y. xpull. intros E. subst. applys local_erase. xapplys rule_set. auto. Qed. (** Same proof using support for nary functions *) Lemma rule_incr_4 : forall p n, triple (val_incr p) (p ~~~> n) (fun r => \[r = val_unit] \* (p ~~~> (n+1))). Proof using. 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. (* then continue as before *) Abort. (** Same proof using characteristic formulae with tactics *) Lemma rule_incr_5 : forall p n, triple (val_incr p) (p ~~~> n) (fun r => \[r = val_unit] \* (p ~~~> (n+1))). Proof using. xcf. xlet as x. xapp. xpull. intro_subst. xlet as y. xapp. xpull. intro_subst. xapp. hsimpl. auto. Qed. (** Same proof using characteristic formulae with more tactics *) Lemma rule_incr_6 : forall p n, triple (val_incr p) (p ~~~> n) (fun r => \[r = val_unit] \* (p ~~~> (n+1))). Proof using. xcf. xapp as x. intro_subst. xapp as y. intro_subst. xapps. hsimpl~. Qed. (** Same proof using characteristic formulae with yet more powerful tactics *) Lemma rule_incr__7 : forall p n, triple (val_incr p) (p ~~~> n) (fun r => \[r = val_unit] \* (p ~~~> (n+1))). Proof using. xcf. xapps. xapps. xapps. hsimpl~. Qed. Hint Extern 1 (Register_spec val_incr) => Provide rule_incr__7. (* ---------------------------------------------------------------------- *) (** Calling incr from a larger context *) Lemma rule_incr_with_other_1 : forall p n q m, triple (val_incr p) (p ~~~> n \* q ~~~> m) (fun r => \[r = val_unit] \* (p ~~~> (n+1)) \* q ~~~> m). Proof using. intros. applys rule_frame_consequence (q ~~~> m). { hsimpl. } { rew_heap. apply rule_incr_5. } { intros r. hsimpl. auto. } Qed. Lemma rule_incr_with_other_2 : forall p n q m, triple (val_incr p) (p ~~~> n \* q ~~~> m) (fun r => \[r = val_unit] \* (p ~~~> (n+1)) \* q ~~~> m). Proof using. intros. xapply rule_incr_5. { hsimpl. } { intros r. hsimpl. auto. } Qed. Lemma rule_incr_with_other : forall p n q m, triple (val_incr p) (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, triple (val_incr p) (p ~~~> n \* H) (fun r => \[r = val_unit] \* (p ~~~> (n+1)) \* H). Proof using. intros. xapps. hsimpl~. Qed. (* ---------------------------------------------------------------------- *) (** Swap function *) Definition val_swap := 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, triple (val_swap p q) (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, triple (val_swap p p) (p ~~~> v) (fun r => \[r = val_unit] \* p ~~~> v). Proof using. xcf. xapps. xapps. xapp~. xapps. hsimpl~. Qed. (* ---------------------------------------------------------------------- *) (** Succ function using incr *) Definition val_succ_using_incr := ValFun 'n := Let 'p := val_ref 'n in val_incr 'p ;;; Let 'x := val_get 'p in 'x. 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~. (* not possible: applys local_erase. unfold cf_val. hsimpl. *) xvals~. Qed. (* ---------------------------------------------------------------------- *) (** Two calls to incr *) (* let val_incr_twice r = incr r; incr r *) Definition val_incr_twice := ValFun 'p := val_incr 'p ;;; val_incr 'p. Lemma rule_incr_twice : forall p n, triple (val_incr_twice p) (p ~~~> n) (fun r => \[r = val_unit] \* p ~~~> (n+2)). Proof using. xcf. xapp. auto. xapps. (* same as [xapp; hpull] *) intros; subst. math_rewrite ((n + 1) + 1 = (n + 2)). (* TODO: avoid this ?*) hsimpl. auto. Qed. (* ---------------------------------------------------------------------- *) (** Basic let-binding example *) Definition val_example_let := ValFun 'n := Let 'a := 'n '+ 1 in Let 'b := 'n '- 1 in 'a '+ 'b. Lemma rule_val_example_let : forall n, triple (val_example_let n) \[] (fun r => \[r = 2*n]). Proof using. xcf. xapps. xapps. xapp. hsimpl. intros. subst. fequals. math. Qed. (* ---------------------------------------------------------------------- *) (** Basic one references *) (* let val_example_one_ref n = let i = ref 0 in incr i; !i *) Definition val_example_one_ref := ValFun 'n := Let 'k := 'n '+ 1 in Let 'i := 'ref 'k in val_incr 'i ;;; '!'i. Lemma rule_example_one_ref : forall n, triple (val_example_one_ref n) \[] (fun r => \[r = n+2]). Proof using. xcf. xapp. intros; subst. xapp. intros I i ?. subst. xapp. auto. xapp. intros r. hsimpl. intros; subst. fequals. math. Qed. (* ---------------------------------------------------------------------- *) (** Basic two references *) (* let val_example_two_ref n = let i = ref 0 in let r = ref n in decr r; incr i; r := !i + !r; !i + !r *) Definition val_example_two_ref := ValFun 'n := Let 'i := 'ref 0 in Let 'r := 'ref 'n in val_decr 'r ;;; val_incr 'i ;;; Let 'i1 := '!'i in Let 'r1 := '!'r in Let 's := 'i1 '+ 'r1 in 'r ':= 's ;;; Let 'i2 := '!'i in Let 'r2 := '!'r in 'i2 '+ 'r2. 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. xapp ;=> r r' Er. subst. xapp~. xapp~. xapps. xapps. xapps. xapps~. xapps. xapps. xapps. hsimpl. intros. subst. fequals. math. Qed.
 (** This file formalizes examples of first-class functions in plain Separation Logic, using lifted characteristic formulae. Author: Arthur Charguéraud. License: MIT. *) Set Implicit Arguments. From Sep Require Import Example. Generalizable Variables A B. Implicit Types p : loc. Implicit Types n : int. (* ********************************************************************** *) (* * Apply function *) Definition val_apply : val := ValFun 'f 'x := ('f 'x). 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. Proof using. introv M. xcf. (* todo why not simplified? *) unfold Substn, substn; simpl; rew_enc_dyn. xapp. hsimpl~. 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) POST Q. Proof using. intros. xpull ;=> M. applys~ Rule_apply. Qed. (* ********************************************************************** *) (* * RefApply function *) Definition val_refapply : val := 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 (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~. 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 (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~. Qed. (* ********************************************************************** *) (* * Twice function *) Definition val_twice : val := 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. Proof using. introv M1 M2. xcf. xseq. xapp M1. xapp M2. hsimpl~. Qed. (* ********************************************************************** *) (* * Repeat function *) Definition val_repeat : val := ValFun 'n 'f := For 'i := 1 To 'n Do 'f '() Done. Axiom xfor_inv_lemma : forall (I:int->hprop), forall (a:int) (b:int) (F:int->Formula) H H', (a <= b+1) -> (H ==> I a \* H') -> (forall i, a <= i <= b -> ^(F i) (I i) (fun (_:unit) => I(i+1))) -> ^(Cf_for a b F) H (fun (_:unit) => I (b+1) \* H'). Lemma Rule_consequence_post : forall t `{Enc A} (Q':A->hprop) H (Q:A->hprop), Triple t H Q' -> Q' ===> Q -> Triple t H Q. Proof using. introv MH M MQ. applys* Rule_consequence MH. Qed. Lemma xfor_simplify_inequality_lemma : forall (n:int), ((n-1)+1) = n. 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) PRE (I i) POST (fun (_:unit) => I (i+1))) -> 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 *) 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. } } { math_rewrite (n+1-1=n). hsimpl. } (* todo : avoid math_rewrite, thanks to hsimpl simplification of invariants *) Qed. (* ********************************************************************** *) (* * Iteration (iter, fold, map, find) on lists: see [ExampleList.v] *) (* ********************************************************************** *) (* * Counter function *) Implicit Types g : val. (* ---------------------------------------------------------------------- *) (** Representation *) Definition MCount (n:int) (g:val) : hprop := Hexists p, (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 *) (* ---------------------------------------------------------------------- *) (** Specification *) 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. hpulls. xunfold MCount. hsimpl~. Qed. (* ---------------------------------------------------------------------- *) (** Implementation *) Definition val_mkcounter : val := ValFun 'u := Let 'p := val_ref 0 in (Fun 'v := val_incr 'p ;;; val_get 'p). (* ---------------------------------------------------------------------- *) (** Verification *) Lemma Rule_mkcounter : Triple (val_mkcounter ``val_unit) \[] (fun g => g ~> MCount 0). Proof using. xcf. xapps ;=> r. xval. xunfold MCount. hsimpl. { intros n'. xcf. xapp~. xapp. hsimpl~. } Qed. Hint Extern 1 (Register_Spec val_mkcounter) => Provide Rule_mkcounter. (* ---------------------------------------------------------------------- *) (** Demo *) Definition trm_test_mkcounter : trm := Let 'c := val_mkcounter '() in Let 'n := 'c '() in Let 'm := 'c '() in val_add 'n 'm. Lemma rule_test_mkcounter : Triple trm_test_mkcounter \[] (fun r => \[r = 3]). Proof using. xcf_trm 100%nat. (* todo: make xcf work *) xapp as C. xapps Rule_MCount. xapps Rule_MCount. xapps. hsimpl~. Qed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
 (* WORK IN PROGRESS (***********************************************************************) (** Stack *) module StackList = struct type 'a t = { mutable items : 'a list; mutable size : int } let create () = { items = []; size = 0 } let size s = s.size let is_empty s = s.size = 0 let push x s = s.items <- x :: s.items; s.size <- s.size + 1 let pop s = match s.items with