Commit 53b6ffab authored by charguer's avatar charguer

lifted cf, start

parent 33172cf7
......@@ -474,3 +474,108 @@ Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 ; f5 := x5 ; f6 := x6 ; f
(*
Lemma Rule_op : forall op (n1 n2:int),
Triple ((prim_op op) (val_pair (enc n1) (enc n2))) \[] (fun r => \[r = op n1 n2]).
Proof using.
intros. applys rule_consequence. { auto. } { applys rule_op. }
{ intros r. unfold PostEnc. hsimpl~ (op n1 n2). }
Qed.
Lemma Rule_if_trm : forall t0 t1 t2 H Q0 Q,
Triple t0 H Q0 ->
(forall X, Triple (trm_if X t1 t2) (Q0 X) Q) ->
Triple (trm_if_trm t0 t1 t2) H Q.
Admitted.
Lemma Rule_seq : forall t1 t2 H Q H',
Triple t1 H (fun v => H') ->
Triple t2 H' Q ->
Triple (trm_seq t1 t2) H Q.
Admitted.
Lemma Rule_while : forall t1 t2 H Q,
(forall (k:trm),
(forall H Q, triple (trm_if_trm t1 (trm_seq t2 k) val_unit) H Q -> triple k H Q) ->
triple k H Q) ->
triple (trm_while t1 t2) H Q.
Admitted.
*)
(* LATER
Definition mlist_incr_val : val :=
Fix mlist_incr [p] :=
_If trm_app val_neq [val_var p; val_loc null] Then (
Let x := prim_get [val_var p; val_field hd] in
Let q := prim_get [val_var p; val_field tl] in
Let y := trm_app val_add [val_var x; val_int 1] in
prim_set [val_var p; val_field hd; val_var y];;
trm_app mlist_incr [val_var q]
).
(*
Lemma mlist_incr_spec : forall p L,
triple (trm_app mlist_incr_val [p])
(p ~> MList L)
(p ~> MList L)
*)
(** Functions *)
Parameter val_fun : var -> vars -> trm -> trm.
Notation "'Fun' f [ x1 ] ':=' K" :=
(val_fun f (x1:nil) K)
(at level 69, f ident, x1 ident) : trm_scope.
Notation "'Fun' f [ x1 ] ':=' K" :=
(val_fun f (x1::nil) K)
(at level 69, f ident, x1 ident) : trm_scope.
Notation "'Fun' f [ x1 x2 ] ':=' K" :=
(val_fun f (x1::x2::nil) K)
(at level 69, f ident, x1 ident, x2 ident) : trm_scope.
Notation "'Fun' f [ x1 x2 x3 ] ':=' K" :=
(val_fun f (x1::x2::x3::nil) K)
(at level 69, f ident, x1 ident, x2 ident, x3 ident) : trm_scope.
Notation "'Fun' f [ x1 x2 x3 x4 ] ':=' K" :=
(val_fun f (x1::x2::x3::x4::nil) K)
(at level 69, f ident, x1 ident, x2 ident, x3 ident, x4 ident) : trm_scope.
Notation "'_If' x 'Then' F1" :=
(trm_if x F1 val_unit)
(at level 69, x at level 0) : trm_scope.
Notation "x `+` y" := (trm_app val_add [x; y])
(at level 69, right associativity) : trm_scope.
Notation "r `^` f" :=
((*trm_app*) prim_get ([ r ; val_field f ]:list val))
(at level 69, no associativity, f at level 0,
format "r `^` f") : trm_scope.
Notation "r `^` f `<-` v" :=
((*trm_app*) prim_set ([r ; val_field f ; v ]:list val))
(at level 69, no associativity, f at level 0,
format "r `^` f `<-` v") : trm_scope.
......@@ -16,9 +16,9 @@ SRC := $(shell cat FILES)
SRC := ModelState ModelLambda ModelSepFunctor ModelSepBasic ModelSepCredits ModelSepRO ModelCF ModelCFCredits ModelML ModelSepML ModelCFML ModelSepExamples
ifeq ($(ARTHUR),1)
SRC := ModelState ModelSepFunctor ModelML ModelSepML ModelCFML ModelSepExamples
endif
#ifeq ($(ARTHUR),1)
# SRC := ModelState ModelSepFunctor ModelML ModelSepML ModelCFML ModelSepExamples
#endif
PWD := $(shell pwd)
......
......@@ -35,15 +35,15 @@ Lemma local_local : forall B (F:~~B),
local (local F) = local F.
Proof using.
extens. intros H Q. iff M.
introv PH.
lets (H1&H2&Q1&PH12&N&Qle): M (rm PH).
lets (h1&h2&PH1&PH2&Ph12&Fh12): (rm PH12).
lets (H1'&H2'&Q1'&PH12'&N'&Qle'): N (rm PH1).
exists H1' (H2' \* H2) Q1'. splits.
{ rewrite <- hprop_star_assoc. exists~ h1 h2. }
{ auto. }
{ intros x. hchange (Qle' x). hchange (Qle x).
rew_heap. rewrite~ hprop_gc_merge. }
{ introv PH.
lets (H1&H2&Q1&PH12&N&Qle): M (rm PH).
lets (h1&h2&PH1&PH2&Ph12&Fh12): (rm PH12).
lets (H1'&H2'&Q1'&PH12'&N'&Qle'): N (rm PH1).
exists H1' (H2' \* H2) Q1'. splits.
{ rewrite <- hprop_star_assoc. exists~ h1 h2. }
{ auto. }
{ intros x. hchange (Qle' x). hchange (Qle x).
rew_heap. rewrite~ hprop_gc_merge. } }
{ apply~ local_erase. }
Qed.
......
......@@ -37,15 +37,15 @@ Lemma local_local : forall B (F:~~B),
local (local F) = local F.
Proof using.
extens. intros H Q. iff M.
introv PH.
lets (H1&H2&Q1&PH12&N&Qle): M (rm PH).
lets (h1&h2&PH1&PH2&Ph12&Fh12): (rm PH12).
lets (H1'&H2'&Q1'&PH12'&N'&Qle'): N (rm PH1).
exists H1' (H2' \* H2) Q1'. splits.
{ rewrite <- hprop_star_assoc. exists~ h1 h2. }
{ auto. }
{ intros x. hchange (Qle' x). hchange (Qle x).
rew_heap. rewrite~ hprop_gc_merge. }
{ introv PH.
lets (H1&H2&Q1&PH12&N&Qle): M (rm PH).
lets (h1&h2&PH1&PH2&Ph12&Fh12): (rm PH12).
lets (H1'&H2'&Q1'&PH12'&N'&Qle'): N (rm PH1).
exists H1' (H2' \* H2) Q1'. splits.
{ rewrite <- hprop_star_assoc. exists~ h1 h2. }
{ auto. }
{ intros x. hchange (Qle' x). hchange (Qle x).
rew_heap. rewrite~ hprop_gc_merge. } }
{ apply~ local_erase. }
Qed.
......@@ -245,11 +245,11 @@ Definition cf_app f vs : formula := fun H Q =>
Definition cf_fix (n:nat) (F1of : val -> vals -> formula)
(F2of : val -> formula) : formula := fun H Q =>
forall (F:val),
(forall Xs, length Xs = n -> (F1of F Xs) ===> app F Xs) ->
(forall Xs, List.length Xs = n -> (F1of F Xs) ===> app F Xs) ->
(F2of F) H Q.
Definition cf_fix0 (F1of : val -> formula)
(F2of : val -> formula) : formula := fun H Q =>
(F2of : val -> formula) : formula := fun H Q =>
forall (F:val),
(F1of F ===> app F nil) ->
(F2of F) H Q.
......@@ -311,7 +311,7 @@ Definition cf_def cf (t:Trm) :=
let G := match xs with
| nil => cf_fix0 (fun F => let E := List.combine (f::nil) (F::nil) in cf (subst_Trm E t1))
| x::nil => cf_fix1 (fun F X => let E := List.combine (f::x::nil) (F::X::nil) in cf (subst_Trm E t1))
| xs => cf_fix (length xs) (fun F Xs => let E := List.combine (f::xs) (F::Xs) in cf (subst_Trm E t1))
| xs => cf_fix (List.length xs) (fun F Xs => let E := List.combine (f::xs) (F::Xs) in cf (subst_Trm E t1))
end in
local (G (fun F => cf (subst_Trm [(f,F)] t2)))
| Trm_app f vs => local (cf_app f vs)
......@@ -463,7 +463,7 @@ Qed.
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 ->
List.length xs = List.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.
......
......@@ -190,7 +190,7 @@ Inductive red : state -> trm -> state -> val -> Prop :=
red m1 (trm_let x t1 t2) m3 r
| red_app : forall m1 m2 v1 v2s f xs xvs t r,
v1 = val_fix f xs t ->
length xs = length v2s ->
List.length xs = List.length v2s ->
xvs = List.combine (f::xs) (v1::v2s) ->
red m1 (subst_trm xvs t) m2 r ->
red m1 (trm_app v1 v2s) m2 r
......
......@@ -3,6 +3,9 @@
This file formalizes examples from standard Separation Logic,
as described in Arthur Charguéraud's lecture notes.
Author: Arthur Charguéraud.
License: MIT.
*)
Set Implicit Arguments.
......
This diff is collapsed.
......@@ -414,7 +414,7 @@ Qed.
Lemma rule_app : forall f xs F Vs t1 H Q E,
F = (val_fix f xs t1) ->
length Vs = length xs ->
List.length Vs = List.length xs ->
E = List.combine (f::xs) (F::Vs) ->
triple (subst_trm E t1) H Q ->
triple (trm_app F Vs) H Q.
......@@ -428,7 +428,7 @@ Qed.
Lemma rule_let_fix : forall f xs t1 t2 H Q,
(forall (F:val),
(forall Xs H' Q' E,
length Xs = length xs ->
List.length Xs = List.length xs ->
E = List.combine (f::xs) (F::Xs) ->
triple (subst_trm E t1) H' Q' ->
triple (trm_app F Xs) H' Q') ->
......
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