Commit 85a1a9d2 authored by charguer's avatar charguer

credits

parent 0d6f2169
(**
This file formalizes characteristic formulae for
program verification using Separation Logic,
for the version that includes time credits.
Author: Arthur Charguéraud.
License: MIT.
*)
Set Implicit Arguments.
Require Export LibFix LambdaSepCredits. (* MODIFIED FOR CREDITS *)
Open Scope heap_scope.
Implicit Types v w : val.
(* ********************************************************************** *)
(* * Type of a formula *)
(** A formula is a binary relation relating a pre-condition
and a post-condition. *)
Definition formula := hprop -> (val -> hprop) -> Prop.
Global Instance Inhab_formula : Inhab formula.
Proof using. apply (prove_Inhab (fun _ _ => True)). Qed.
(* ********************************************************************** *)
(* * The [local] predicate *)
(** Nested applications [local] are redundant *)
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 <- hstar_assoc. exists~ h1 h2. }
{ auto. }
{ intros x. hchange (Qle' x). hchange (Qle x).
rew_heap. rewrite~ htop_hstar_htop. }
{ apply~ local_erase. }
Qed.
(** A definition whose head is [local] satisfies [is_local] *)
Lemma is_local_local : forall B (F:~~B),
is_local (local F).
Proof using. intros. unfolds. rewrite~ local_local. Qed.
Hint Resolve is_local_local.
(* ********************************************************************** *)
(* * Characteristic formula generator *)
(* ---------------------------------------------------------------------- *)
(* ** Input language for the characteristic formula generator,
where functions are named by a let-binding. *)
(** Extended syntax of terms, with a new construct [Trm_let_fix]
to represent the term [let rec f x = t1 in t2] *)
Inductive Trm : Type :=
| Trm_val : val -> Trm
| Trm_if_val : val -> Trm -> Trm -> Trm
| Trm_let : var -> Trm -> Trm -> Trm
| Trm_let_fix : var -> var -> Trm -> Trm -> Trm
| Trm_app : val -> val -> Trm.
(** Definition of capture-avoiding substitution on [Trm] *)
Fixpoint Subst (y : var) (w : val) (t : Trm) : Trm :=
match t with
| Trm_val v => Trm_val v
| Trm_if_val v t1 t2 => Trm_if_val v (Subst y w t1) (Subst y w t2)
| Trm_let x t1 t2 => Trm_let x (Subst y w t1) (If x = y then t2 else Subst y w t2)
| Trm_let_fix f x t1 t2 => Trm_let_fix f x
(if eq_var_dec x y then t1 else if eq_var_dec f y then t1 else Subst y w t1)
(if eq_var_dec f y then t2 else Subst y w t2)
| Trm_app v1 v2 => Trm_app v1 v2
end.
(** Translation from [Trm] to [trm], by encoding [Trm_let_fix]
using [trm_let] and [val_fix]. *)
Fixpoint trm_of_Trm (t : Trm) : trm :=
let aux := trm_of_Trm in
match t with
| Trm_val v => trm_val v
| Trm_if_val v t1 t2 => trm_if v (aux t1) (aux t2)
| Trm_let x t1 t2 => trm_let x (aux t1) (aux t2)
| Trm_let_fix f x t1 t2 => trm_let f (trm_fix f x (aux t1)) (aux t2)
| Trm_app v1 v2 => trm_app v1 v2
end.
Coercion trm_of_Trm : Trm >-> trm.
(* ---------------------------------------------------------------------- *)
(** Size function used as measure for the CF generator:
it computes the size of a term, where all values counting
for one unit, including closures viewed as values. *)
Fixpoint Trm_size (t:Trm) : nat :=
match t with
| Trm_val v => 1
| Trm_if_val v t1 t2 => 1 + Trm_size t1 + Trm_size t2
| Trm_let x t1 t2 => 1 + Trm_size t1 + Trm_size t2
| Trm_let_fix f x t1 t2 => 1 + Trm_size t1 + Trm_size t2
| Trm_app f v => 1
end.
Lemma Trm_size_subst : forall x v t,
Trm_size (Subst x v t) = Trm_size t.
Proof using.
intros. induction t; simpl; repeat case_if; auto.
Qed.
(* ---------------------------------------------------------------------- *)
(* ** 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. *)
Definition app t H Q :=
triple t H Q.
(* ---------------------------------------------------------------------- *)
(* ** Definition of CF blocks *)
(** These auxiliary definitions give the characteristic formula
associated with each term construct. *)
Definition cf_val (v:val) : formula := fun H Q =>
H ==> Q v.
Definition cf_if_val (v:val) (F1 F2:formula) : formula := fun H Q =>
If (v = val_int 0) then F2 H Q else F1 H Q.
Definition cf_let (F1:formula) (F2of:val->formula) : formula := fun H Q =>
exists Q1,
F1 H Q1
/\ (forall (X:val), (F2of X) (Q1 X) Q).
Definition cf_app (f:val) (v:val) : formula := fun H Q =>
app (f v) H Q.
(* MODIFIED FOR CREDITS *)
Definition Tick (F:formula) := fun H Q =>
exists H', pay_one H H' /\ F H' Q.
(* MODIFIED FOR CREDITS *)
Definition cf_fix (F1of:val->val->formula)
(F2of:val->formula) : formula := fun H Q =>
forall (F:val),
(forall X, (Tick (F1of F X)) ===> app (F X)) ->
(F2of F) H Q.
(* ---------------------------------------------------------------------- *)
(* ** Instance of [app] for primitive operations *)
Lemma app_ref : forall v,
app (val_ref v) \[] (fun r => Hexists l, \[r = val_loc l] \* l ~~~> v).
Proof using. applys rule_ref. Qed.
Lemma app_get : forall v l,
app (val_get (val_loc l)) (l ~~~> v) (fun x => \[x = v] \* (l ~~~> v)).
Proof using. applys rule_get. Qed.
Lemma app_set : forall w l v,
app (val_set (val_loc l) w) (l ~~~> v) (fun r => \[r = val_unit] \* l ~~~> w).
Proof using. applys rule_set. Qed.
(* ---------------------------------------------------------------------- *)
(* ** Definition of the CF generator *)
(** The CF generator is a recursive function, defined using the
optimal fixed point combinator (from TLC). [cf_def] gives the
function, and [cf] is then defined as the fixpoint of [cf_def].
Subsequently, the fixed-point equation is established. *)
Definition cf_def cf (t:Trm) :=
match t with
| Trm_val v => local (cf_val v)
| Trm_if_val v t1 t2 => local (cf_if_val v (cf t1) (cf t2))
| Trm_let x t1 t2 => local (cf_let (cf t1) (fun X => cf (Subst x X t2)))
| Trm_let_fix f x t1 t2 => local (cf_fix
(fun F X => cf (Subst f F (Subst x X t1)))
(fun F => cf (Subst f F t2)))
| Trm_app f v => local (cf_app f v)
end.
Definition cf := FixFun cf_def.
Ltac smath := simpl; math.
Hint Extern 1 (lt _ _) => smath.
Lemma cf_unfold : forall t,
cf t = cf_def cf t.
Proof using.
applys~ (FixFun_fix (measure Trm_size)). auto with wf.
intros f1 f2 t IH. unfold measure in IH. unfold cf_def.
destruct t; fequals.
{ rewrite~ IH. rewrite~ IH. }
{ rewrite~ IH. fequals.
apply func_ext_1. intros X. rewrite~ IH. rewrite~ Trm_size_subst. }
{ fequals.
{ apply func_ext_2. intros F X. rewrite~ IH. do 2 rewrite~ Trm_size_subst. }
{ apply func_ext_1. intros X. rewrite~ IH. rewrite~ Trm_size_subst. } }
Qed.
Ltac simpl_cf :=
rewrite cf_unfold; unfold cf_def.
(* ********************************************************************** *)
(* * Soundness proof *)
(* ---------------------------------------------------------------------- *)
(* ** Two substitution lemmas for the soundness proof *)
Hint Extern 1 (measure Trm_size _ _) => hnf; simpl; math.
(** Substitution commutes with the translation from [Trm] to [trm] *)
Lemma subst_trm_of_Trm : forall y w (t:Trm),
subst y w (trm_of_Trm t) = trm_of_Trm (Subst y w t).
Proof using.
intros. induction t; simpl; auto.
{ rewrite IHt1, IHt2. auto. }
{ rewrite IHt1, IHt2. do 2 case_if~. }
{ rewrite IHt1, IHt2. do 2 case_if~. }
Qed.
(** The size of a [Trm] is preserved by substitution of
a variable by a value. *)
Lemma Trm_size_subst_value : forall y (w:val) (t:Trm),
Trm_size (Subst y w t) = Trm_size t.
Proof using.
intros. induction t; simpl; auto; repeat case_if; auto.
Qed.
(* ---------------------------------------------------------------------- *)
(* ** Soundness of the CF generator *)
Lemma is_local_cf : forall T,
is_local (cf T).
Proof. intros. simpl_cf. destruct T; apply is_local_local. Qed.
Definition sound_for (t:trm) (F:formula) :=
forall H Q, F H Q -> triple t H Q.
Lemma sound_for_local : forall t (F:formula),
sound_for t F ->
sound_for t (local F).
Proof using.
unfold sound_for. introv SF. intros H Q M.
rewrite is_local_triple. applys local_weaken_body M. applys SF.
Qed.
Notation "'trm_fix'' f x t1" := (trm_func (Rec f) x t1)
(at level 69, f ident, x ident, t1 at level 0).
Lemma sound_for_cf : forall (t:Trm),
sound_for t (cf t).
Proof using.
intros t. induction_wf: Trm_size t.
rewrite cf_unfold. destruct t; simpl;
applys sound_for_local; intros H Q P.
{ applys~ rule_val. }
{ hnf in P. applys rule_if_val. case_if; applys~ IH. }
{ destruct P as (Q1&P1&P2). applys rule_let Q1.
{ applys~ IH. }
{ intros X. rewrite subst_trm_of_Trm.
applys~ IH. hnf. rewrite~ Trm_size_subst_value. } }
{ renames v to f, v0 to x. applys rule_let_fix. hnf in P.
intros F HF. rewrite subst_trm_of_Trm. applys IH.
{ hnf. rewrite~ Trm_size_subst_value. }
{ applys P. intros X H' Q' (Q''&HP&HB). (* MODIFIED FOR CREDITS *)
applys HF HP.
do 2 rewrite subst_trm_of_Trm. applys~ IH.
{ hnf. rewrite Trm_size_subst_value.
rewrite~ Trm_size_subst_value. } } }
{ applys P. }
Qed.
Theorem triple_of_cf : forall t H Q,
cf t H Q ->
triple t H Q.
Proof using. intros. applys* sound_for_cf. Qed.
Definition spec_fix (f:var) (x:var) (t1:trm) (F:val) :=
forall X H H' Q,
pay_one H H' ->
triple (subst f F (subst x X t1)) H' Q ->
triple (trm_app F X) H Q.
Lemma spec_fix_val_fix : forall f x t1,
spec_fix f x t1 (val_fix f x t1).
Proof using.
intros f x t1 X H H' Q HP M. intros HF h N. unfolds pay_one.
lets HP': himpl_frame_l HF (rm HP).
lets N': (rm HP') (rm N). rew_heap in N'.
destruct N' as (h1&h2&N1&N2&N3&N4).
lets N1': hcredits_inv (rm N1). inverts N1'.
lets (Na&Nb): heap_eq_forward (rm N4). simpls. subst.
lets~ (n&h'&v&R&K&C): (rm M) HF h2.
exists (n+1)%nat h' v. splits~.
{ applys* red_app_fix_val. fmap_red~. }
{ math. }
Qed.
Lemma rule_app_fix : forall f x F V t1 H H' Q,
F = (val_fix f x t1) ->
pay_one H H' ->
triple (subst f F (subst x V t1)) H' Q ->
triple (trm_app F V) H Q.
Proof using. introv EF N M. subst F. applys* spec_fix_val_fix. Qed.
(* TODO: choose which formulation to keep *)
Lemma rule_fix : forall f x t1 H Q,
(forall (F:val), spec_fix f x t1 F -> H ==> Q F) ->
triple (trm_fix f x t1) H Q.
Proof using.
introv M. forwards M': (rm M) (val_fix f x t1).
{ applys spec_fix_val_fix. }
{ applys~ rule_fix_val. }
Qed.
Lemma rule_if_val : forall v t1 t2 H Q,
triple (If v = val_int 0 then t2 else t1) H Q ->
triple (trm_if v t1 t2) H Q.
Proof using.
introv M. intros HF h N. forwards* (n&h'&v'&R&K&C): (rm M) HF h.
exists n h' v'. splits~. { applys~ red_if_val. }
Qed.
| red_if_val : forall n m1 m2 v r t1 t2,
red n m1 (If v = val_int 0 then t2 else t1) m2 r ->
red n m1 (trm_if v t1 t2) m2 r
(*
cuts G: (forall (k:nat) L, LibList.length L = n-k :> int ->
S k (Array L (p+k)%nat) (fun r => \[r = '()] \* (Array (make (length L) v) (p+k)%nat))).
......
......@@ -48,9 +48,9 @@ Inductive red : nat -> state -> trm -> state -> val -> Prop :=
red 0 m (trm_val v) m v
| red_fix : forall m f x t1,
red 0 m (trm_fix f x t1) m (val_fix f x t1)
| red_if_val : forall n m1 m2 v r t1 t2,
red n m1 (If v = val_int 0 then t2 else t1) m2 r ->
red n m1 (trm_if v t1 t2) m2 r
| red_if_bool : forall n m1 m2 (b:bool) r t1 t2,
red n m1 (if b then t1 else t2) m2 r ->
red n m1 (trm_if b t1 t2) m2 r
| red_let : forall n1 n2 m1 m2 m3 x t1 t2 v1 r,
red n1 m1 t1 m2 v1 ->
red n2 m2 (subst x v1 t2) m3 r ->
......@@ -412,14 +412,14 @@ Lemma himpl_frame_l : forall H2 H1 H1',
(H1 \* H2) ==> (H1' \* H2).
Proof using. introv W (h1&h2&?). exists* h1 h2. Qed.
Lemma local_local_aux : forall B,
let local := fun (F:(hprop->(B->hprop)->Prop)) H Q =>
Lemma local_local_aux : forall (B:Type),
let local := fun (F:(hprop->(B->hprop)->Prop)) (H:hprop) (Q:B->hprop) =>
( forall h, H h -> exists H1 H2 Q1,
(H1 \* H2) h
/\ F H1 Q1
/\ Q1 \*+ H2 ===> Q \*+ \Top) in
(\Top \* \Top = \Top) ->
forall F H Q,
forall F (H:hprop) (Q:B->hprop),
local (local F) H Q ->
local F H Q.
Proof using.
......@@ -442,8 +442,6 @@ End Properties.
End SepCreditsCore.
(* ********************************************************************** *)
(* * Properties of the logic *)
......@@ -461,7 +459,7 @@ Notation "l '~~~>' v" := (hsingle l v)
(at level 32, no associativity) : heap_scope.
Lemma hstar_hsingle_same_loc_disjoint : forall (l:loc) (v1 v2:val),
(l ~~~> v1) \* (l ~~> v2) ==> \[False].
(l ~~~> v1) \* (l ~~~> v2) ==> \[False].
Proof using.
intros. unfold hsingle.
intros h ((m1&n1)&(m2&n2)&(E1&X1&N1)&(E2&X2&N2)&D&E). false.
......@@ -598,7 +596,7 @@ Lemma rule_consequence : forall t H' Q' H Q,
Proof using.
introv MH M MQ. intros HF h N.
forwards (n&h'&v&R&K&C): (rm M) HF h. { hhsimpl~. }
exists n h' v. splits~. { hhsimpl~. }
exists n h' v. splits~. { hhsimpl. hchanges~ MQ. }
Qed.
Lemma rule_frame : forall t H Q H',
......@@ -638,14 +636,20 @@ Proof using.
{ hhsimpl. hchanges M. }
Qed.
Lemma rule_if_val : forall v t1 t2 H Q,
triple (If v = val_int 0 then t2 else t1) H Q ->
triple (trm_if v t1 t2) H Q.
Lemma rule_if_bool : forall (b:bool) t1 t2 H Q,
triple (if b then t1 else t2) H Q ->
triple (trm_if b t1 t2) H Q.
Proof using.
introv M. intros HF h N. forwards* (n&h'&v'&R&K&C): (rm M) HF h.
exists n h' v'. splits~. { applys~ red_if_val. }
exists n h' v'. splits~. { applys~ red_if_bool. }
Qed.
Lemma rule_if_bool' : forall (b:bool) t1 t2 H Q,
(b = true -> triple t1 H Q) ->
(b = false -> triple t2 H Q) ->
triple (trm_if b t1 t2) H Q.
Proof using. introv M1 M2. applys rule_if_bool. case_if*. Qed.
Lemma rule_let : forall x t1 t2 H Q Q1,
triple t1 H Q1 ->
(forall (X:val), triple (subst x X t2) (Q1 X) Q) ->
......@@ -680,16 +684,13 @@ Proof using.
{ math. }
Qed.
Definition spec_fix (f:var) (x:var) (t1:trm) (F:val) :=
forall X H H' Q,
pay_one H H' ->
triple (subst f F (subst x X t1)) H' Q ->
triple (trm_app F X) H Q.
Lemma spec_fix_val_fix : forall f x t1,
spec_fix f x t1 (val_fix f x t1).
Proof using.
intros f x t1 X H H' Q HP M. intros HF h N. unfolds pay_one.
Lemma rule_app_fix : forall f x F V t1 H H' Q,
F = (val_fix f x t1) ->
pay_one H H' ->
triple (subst f F (subst x V t1)) H' Q ->
triple (trm_app F V) H Q.
Proof using.
introv EF HP M. intros HF h N. unfolds pay_one.
lets HP': himpl_frame_l HF (rm HP).
lets N': (rm HP') (rm N). rew_heap in N'.
destruct N' as (h1&h2&N1&N2&N3&N4).
......@@ -698,34 +699,8 @@ Proof using.
lets~ (n&h'&v&R&K&C): (rm M) HF h2.
exists (n+1)%nat h' v. splits~.
{ applys* red_app_fix_val. fmap_red~. }
{ math. }
Qed.
Lemma rule_app_fix : forall f x F V t1 H H' Q,
F = (val_fix f x t1) ->
pay_one H H' ->
triple (subst f F (subst x V t1)) H' Q ->
triple (trm_app F V) H Q.
Proof using. introv EF N M. subst F. applys* spec_fix_val_fix. Qed.
(* TODO: choose which formulation to keep *)
Lemma rule_fix : forall f x t1 H Q,
(forall (F:val), spec_fix f x t1 F -> H ==> Q F) ->
triple (trm_fix f x t1) H Q.
Proof using.
introv M. forwards M': (rm M) (val_fix f x t1).
{ applys spec_fix_val_fix. }
{ applys~ rule_fix_val. }
Qed.
Lemma rule_let_fix : forall f x t1 t2 H Q,
(forall (F:val), spec_fix f x t1 F -> triple (subst f F t2) H Q) ->
triple (trm_let f (trm_fix f x t1) t2) H Q.
Proof using.
introv M. applys rule_let (fun F => \[spec_fix f x t1 F] \* H).
{ applys rule_fix. introv HF. hsimpl~. }
{ intros F. applys rule_extract_hprop. applys M. }
Qed.
{ math. }
Qed.
Section RulesPrimitiveOps.
Transparent hstar hsingle.
......@@ -744,7 +719,7 @@ Proof using.
Qed.
Lemma rule_get : forall v l,
triple (val_get (val_loc l)) (l ~~~> v) (fun x => \[x = v] \* (l ~~> v)).
triple (val_get (val_loc l)) (l ~~~> v) (fun x => \[x = v] \* (l ~~~> v)).
Proof using.
intros. intros HF h N. lets N': N.
destruct N as (h1&h2&(N1a&N1b)&N2&N3&N4).
......@@ -755,7 +730,7 @@ Proof using.
Qed.
Lemma rule_set : forall w l v,
triple (val_set (val_loc l) w) (l ~~~> v) (fun r => \[r = val_unit] \* l ~~> w).
triple (val_set (val_loc l) w) (l ~~~> v) (fun r => \[r = val_unit] \* l ~~~> w).
Proof using.
intros. intros HF h N. destruct N as (h1&h2&(N1a&N1b&N1c)&N2&N3&N4).
forwards (E1&E2): heap_eq_forward (rm N4). simpls.
......@@ -778,6 +753,7 @@ End RulesPrimitiveOps.
(* ********************************************************************** *)
(* * Bonus *)
(* ---------------------------------------------------------------------- *)
(* ** Triples satisfy the [local] predicate *)
......@@ -795,7 +771,7 @@ Proof using.
exists n h' v. splits~. rewrite <- htop_hstar_htop.
applys himpl_inv S2.
hchange (R3 v). rew_heap.
rewrite (hstar_comm_assoc \Top H'). hsimpl. }
rewrite (hstar_comm_assoc \Top H'). hsimpl. }
Qed.
......@@ -870,3 +846,25 @@ Proof using.
{ math. } }
Qed.
(* ---------------------------------------------------------------------- *)
(* ** Derived rule for let-binding of a recursive function *)
Definition spec_fix (f:var) (x:var) (t1:trm) (F:val) :=
forall X H H' Q,
pay_one H H' ->
triple (subst f F (subst x X t1)) H' Q ->
triple (trm_app F X) H Q.
Lemma rule_let_fix : forall f x t1 t2 H Q,
(forall (F:val), spec_fix f x t1 F -> triple (subst f F t2) H Q) ->
triple (trm_let f (trm_fix f x t1) t2) H Q.
Proof using.
introv M. applys rule_let (fun F => \[spec_fix f x t1 F] \* H).
{ applys rule_fix_val. hsimpl~.
intros F H' H'' Q' M1 M2. applys* rule_app_fix. }
{ intros F. applys rule_extract_hprop. applys M. }
Qed.
......@@ -17,7 +17,8 @@ SRC := $(shell cat FILES)
ifeq ($(ARTHUR),1)
# Fmap SepFunctor MLSemantics MLSep MLSepLifted MLCF MLCFLifted MLExamples LambdaSemantics LambdaSep LambdaSepCredits LambdaSepRO LambdaCF LambdaExamples LambdaCFCredits
# Note: double space below is important for export.sh
SRC := TLCbuffer Fmap SepFunctor SepTactics LambdaSemantics LambdaSep LambdaCF LambdaStruct LambdaSepLifted LambdaCFLifted LambdaStructLifted Example ExampleBasicNonlifted ExampleListNonlifted ExampleBasic ExampleList ExampleTrees ExampleUnionFind ExampleHigherOrder
BONUS := LambdaSepCredits
SRC := TLCbuffer Fmap SepFunctor SepTactics LambdaSemantics LambdaSep $(BONUS) LambdaCF LambdaStruct LambdaSepLifted LambdaCFLifted LambdaStructLifted Example ExampleBasicNonlifted ExampleListNonlifted ExampleBasic ExampleList ExampleTrees ExampleUnionFind ExampleHigherOrder
endif
PWD := $(shell pwd)
......
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