Commit 0827c780 authored by charguer's avatar charguer
Browse files

merged_master

parents 0f1d099b 41a6303d
......@@ -10,6 +10,7 @@ settings.sh
.*.aux
.coq-native
.coqide
_CoqProject
# CFML
lib/tlc
*.cmj
......
.PHONY: all tools coqlib ocamllib quick doc clean
.PHONY: all tools coqlib stdlib quick doc clean
###############################################################################
#
......@@ -21,9 +21,9 @@ TOOLS := $(CFML)/lib/tools
###############################################################################
# Targets
all: ocamllib coqlib
all: stdlib coqlib
quick: ocamllib coqlib_quick
quick: stdlib_quick coqlib_quick
coqlib:
$(MAKE) -C lib/coq proof
......@@ -35,14 +35,16 @@ coqlib_quick:
coqlib_quick_cf:
$(MAKE) -C lib/coq quick_cf
#------ TODO: ocamllib is deprecated
stdlib: tools coqlib
$(MAKE) -C lib/stdlib
ocamllib: tools
$(MAKE) -C lib/ocaml
stdlib_quick: tools coqlib_quick
$(MAKE) -C lib/stdlib quick
demos: all
$(MAKE) -C examples
###############################################################################
# Tools
......@@ -58,13 +60,13 @@ tools:
clean_gen:
$(MAKE) -C generator clean
clean_ocamllib:
$(MAKE) -C lib/ocaml clean
clean_stdlib:
$(MAKE) -C lib/stdlib clean
clean_coqlib:
$(MAKE) -C lib/coq clean
clean: clean_gen clean_ocamllib clean_coqlib
clean: clean_gen clean_stdlib clean_coqlib
###############################################################################
......
Set Implicit Arguments.
Require Export CFSpec CFPrint CFPrim
LibListZ LibMap LibInt.
Generalizable Variables a A.
(********************************************************************)
(** Imperative Representation for base types *)
Global Opaque heap_is_empty hdata heap_is_single heap_is_empty_st.
(* todo: check needed *)
Global Opaque Zplus. (* todo: move *)
Transparent hdata. (* todo: should use hdata_simpl instead *)
Require Import LibSet.
Open Scope container_scope.
(*------------------------------------------------------------------*)
(* ** References *)
Definition Ref a A (T:htype A a) (V:A) (l:loc) :=
Hexists v, heap_is_single l v \* v ~> T V.
Instance Ref_Heapdata : forall a A (T:htype A a),
(Heapdata (@Ref a A T)).
Proof using.
intros. applys Heapdata_prove. intros x X1 X2.
unfold Ref. hdata_simpl. hextract as x1 x2.
hchange (@star_is_single_same_loc x). hsimpl.
Qed.
Open Local Scope heap_scope_advanced.
Notation "'~~>' v" := (~> Ref (@Id _) v)
(at level 32, no associativity) : heap_scope_advanced.
(*
Notation "l '~~>' v" := (l ~> Ref (@Id _) v)
(at level 32, no associativity) : heap_scope.
*)
Notation "l '~~>' v" := (hdata (@Ref _ _ (@Id _) v) l)
(at level 32, no associativity) : heap_scope.
Lemma focus_ref : forall (l:loc) a A (T:htype A a) V,
l ~> Ref T V ==> Hexists v, l ~~> v \* v ~> T V.
Proof. intros. unfold Ref, hdata. unfold Id. hsimpl~. Qed.
Lemma unfocus_ref : forall (l:loc) a (v:a) A (T:htype A a) V,
l ~~> v \* v ~> T V ==> l ~> Ref T V.
Proof. intros. unfold Ref. hdata_simpl. hsimpl. subst~. Qed.
Lemma heap_is_single_impl_null : forall (l:loc) A (v:A),
heap_is_single l v ==> heap_is_single l v \* \[l <> null].
Proof.
intros. intros h Hh. forwards*: heap_is_single_null. exists___*.
Qed.
Lemma focus_ref_null : forall a A (T:htype A a) V,
null ~> Ref T V ==> \[False].
Proof.
intros. unfold Ref, hdata. hextract as v.
hchanges (@heap_is_single_impl_null null).
Qed.
Global Opaque Ref.
Implicit Arguments focus_ref [a A].
Implicit Arguments unfocus_ref [a A].
(*------------------------------------------------------------------*)
(* ** Tuple 2 *)
Definition Tup2 A1 A2 a1 a2 (T1:A1->a1->hprop) (T2:A2->a2->hprop) P p :=
let '(X1,X2) := P in let '(x1,x2) := p in x1 ~> T1 X1 \* x2 ~> T2 X2.
Lemma focus_tup2 : forall a1 a2 (p:a1*a2) A1 A2 (T1:htype A1 a1) (T2:htype A2 a2) V1 V2,
p ~> Tup2 T1 T2 (V1,V2) ==> let '(x1,x2) := p in x1 ~> T1 V1 \* x2 ~> T2 V2.
Proof. auto. Qed.
Lemma unfocus_tup2 : forall a1 (x1:a1) a2 (x2:a2) A1 A2 (T1:htype A1 a1) (T2:htype A2 a2) V1 V2,
x1 ~> T1 V1 \* x2 ~> T2 V2 ==> (x1,x2) ~> Tup2 T1 T2 (V1,V2).
Proof. intros. unfold Tup2. hdata_simpl. auto. Qed.
Global Opaque Tup2.
(*------------------------------------------------------------------*)
(* ** Tuple 3 *)
Definition Tup3 A1 A2 A3 a1 a2 a3 (T1:A1->a1->hprop) (T2:A2->a2->hprop) (T3:A3->a3->hprop) P p :=
let '(X1,X2,X3) := P in let '(x1,x2,x3) := p in x1 ~> T1 X1 \* x2 ~> T2 X2 \* x3 ~> T3 X3.
Lemma focus_tup3 : forall a1 a2 a3 (p:a1*a2*a3) A1 A2 A3 (T1:htype A1 a1) (T2:htype A2 a2) (T3:A3->a3->hprop) V1 V2 V3,
p ~> Tup3 T1 T2 T3 (V1,V2,V3) ==> let '(x1,x2,x3) := p in x1 ~> T1 V1 \* x2 ~> T2 V2 \* x3 ~> T3 V3.
Proof. auto. Qed.
Lemma unfocus_tup3 : forall a1 (x1:a1) a2 (x2:a2) a3 (x3:a3) A1 A2 A3 (T1:htype A1 a1) (T2:htype A2 a2) (T3:A3->a3->hprop) V1 V2 V3,
x1 ~> T1 V1 \* x2 ~> T2 V2 \* x3 ~> T3 V3 ==> (x1,x2,x3) ~> Tup3 T1 T2 T3 (V1,V2,V3).
Proof. intros. unfold Tup3. hdata_simpl. auto. Qed.
Global Opaque Tup3.
(*------------------------------------------------------------------*)
(* ** Lists *)
Fixpoint List A a (T:A->a->hprop) (L:list A) (l:list a) : hprop :=
match L,l with
| nil, nil => \[l = nil] (* %todo: True*)
| X::L', x::l' => x ~> T X \* l' ~> List T L'
| _,_=> \[False]
end.
Lemma focus_nil : forall A a (T:A->a->hprop),
\[] ==> nil ~> List T nil.
Proof. intros. simpl. hdata_simpl. hsimpl~. Qed.
Lemma unfocus_nil : forall a (l:list a) A (T:A->a->hprop),
l ~> List T nil ==> \[l = nil].
Proof. intros. simpl. hdata_simpl. destruct l. auto. hsimpl. Qed.
Lemma unfocus_nil' : forall A (L:list A) a (T:A->a->hprop),
nil ~> List T L ==> \[L = nil].
Proof.
intros. destruct L.
simpl. hdata_simpl. hsimpl~.
simpl. hdata_simpl. hsimpl.
Qed.
Lemma focus_cons : forall a (l:list a) A (X:A) (L':list A) (T:A->a->hprop),
(l ~> List T (X::L')) ==>
Hexists x l', (x ~> T X) \* (l' ~> List T L') \* \[l = x::l'].
Proof.
intros. simpl. hdata_simpl. destruct l as [|x l'].
hsimpl.
hsimpl~ x l'.
Qed.
Lemma focus_cons' : forall a (x:a) (l:list a) A (L:list A) (T:A->a->hprop),
(x::l) ~> List T L ==>
Hexists X L', \[L = X::L'] \* (x ~> T X) \* (l ~> List T L').
Proof. intros. destruct L; simpl; hdata_simpl; hsimpl~. Qed.
Lemma unfocus_cons : forall a (x:a) (l:list a) A (X:A) (L:list A) (T:A->a->hprop),
(x ~> T X) \* (l ~> List T L) ==>
((x::l) ~> List T (X::L)).
Proof. intros. simpl. hdata_simpl. hsimpl. Qed.
Global Opaque List.
(************************************************************)
(** Locations *)
Parameter ml_phy_eq_spec : Spec ml_phy_eq x y |R>>
pure R (= (x '= y :> loc)).
Parameter ml_phy_neq_spec : Spec ml_phy_neq x y |R>>
pure R (= (x '<> y :> loc)).
Hint Extern 1 (RegisterSpec ml_phy_eq) => Provide ml_phy_eq_spec.
Hint Extern 1 (RegisterSpec ml_phy_neq) => Provide ml_phy_neq_spec.
(************************************************************)
(** References *)
Parameter ml_ref_spec : forall a,
Spec ml_ref (v:a) |R>>
R \[] (~~> v).
Parameter ml_get_spec : forall a,
Spec ml_get (l:loc) |R>>
forall (v:a), keep R (l ~~> v) (fun x => \[x = v]).
Parameter ml_set_spec : forall a,
Spec ml_set (l:loc) (v:a) |R>>
forall (v':a), R (l ~> Ref Id v') (# l ~> Ref Id v).
Parameter ml_sset_spec : forall a a',
Spec ml_sset (l:loc) (v:a) |R>>
forall (v':a'), R (l ~~> v') (# l ~~> v).
Parameter ml_incr_spec :
Spec ml_incr (l:loc) |R>>
forall n, R (l ~~> n) (# l ~~> (n+1)).
Parameter ml_decr_spec :
Spec ml_decr (l:loc) |R>>
forall n, R (l ~~> n) (# l ~~> (n-1)).
Parameter ml_free_spec :
Spec ml_free (l:loc) |R>>
forall A (v:A), R (l ~> Ref Id v) (# \[]).
Hint Extern 1 (RegisterSpec ml_ref) => Provide ml_ref_spec.
Hint Extern 1 (RegisterSpec ml_get) => Provide ml_get_spec.
Hint Extern 1 (RegisterSpec ml_set) => Provide ml_set_spec.
Hint Extern 1 (RegisterSpec ml_sset) => Provide ml_sset_spec.
Hint Extern 1 (RegisterSpec ml_incr) => Provide ml_incr_spec.
Hint Extern 1 (RegisterSpec ml_decr) => Provide ml_decr_spec.
Hint Extern 1 (RegisterSpec ml_free) => Provide ml_free_spec.
(************************************************************)
(** Group of References *)
Require Import CFTactics.
Parameter ml_ref_spec_group : forall a,
Spec ml_ref (v:a) |R>> forall (M:map loc a),
R (Group (Ref Id) M) (fun (l:loc) =>
Group (Ref Id) (M[l:=v]) \* \[l \notindom M]).
Lemma ml_get_spec_group : forall a,
Spec ml_get (l:loc) |R>> forall (M:map loc a),
forall `{Inhab a}, l \indom M ->
keep R (Group (Ref Id) M) (fun x => \[x = M[l]]).
Proof.
intros. xweaken. intros l R LR HR M IA IlM. simpls.
rewrite~ (Group_rem l M). xapply (HR (M[l])); hsimpl~.
Qed.
Lemma ml_set_spec_group : forall a,
Spec ml_set (l:loc) (v:a) |R>> forall (M:map loc a),
forall `{Inhab a}, l \indom M ->
R (Group (Ref Id) M) (# Group (Ref Id) (M[l:=v])).
Proof.
intros. xweaken. intros l v R LR HR M IA IlM. simpls.
rewrite~ (Group_rem l M).
xapply (HR (M[l])). hsimpl.
intros _. hchanges~ (Group_add' l M).
Qed.
(************************************************************)
(** Boolean *)
Parameter ml_eqb_int_spec : Spec ml_eqb (x:int) (y:int) |R>>
pure R (= (x '= y)).
Parameter ml_and_spec : Spec ml_and x y |R>>
pure R (= (x && y)).
Parameter ml_or_spec : Spec ml_or x y |R>>
pure R (= (x || y)).
Hint Extern 1 (RegisterSpec ml_eqb) => Provide ml_eqb_int_spec.
Hint Extern 1 (RegisterSpec ml_and) => Provide ml_and_spec.
Hint Extern 1 (RegisterSpec ml_and) => Provide ml_or_spec.
(************************************************************)
(** Arithmetic *)
Parameter ml_plus_spec : Spec ml_plus x y |R>>
pure R (= (x + y)%Z).
Parameter ml_minus_spec : Spec ml_minus x y |R>>
pure R (= (x - y)%Z).
Parameter ml_div_spec : Spec ml_div x y |R>>
(y <> 0) ->
R \[] (fun z => \[z = Z.quot x y]).
Goal Z.quot 5 3 = 1.
Proof. reflexivity. Qed.
Goal Z.quot (-5) 3 = -1.
Proof. reflexivity. Qed.
Goal Z.quot 5 (-3) = -1.
Proof. reflexivity. Qed.
Goal Z.quot (-5) (-3) = 1.
Proof. reflexivity. Qed.
Parameter ml_mod_spec : Spec ml_mod x y |R>>
(y <> 0) ->
R \[] (fun z => \[z = Z.rem x y]).
Goal Z.rem 5 3 = 2.
Proof. reflexivity. Qed.
Goal Z.rem (-5) 3 = -2.
Proof. reflexivity. Qed.
Goal Z.rem 5 (-3) = 2.
Proof. reflexivity. Qed.
Goal Z.rem (-5) (-3) = -2.
Proof. reflexivity. Qed.
Parameter ml_leq_spec : Spec ml_leq x y |R>>
pure R (= (x <= y)%I).
Parameter ml_geq_spec : Spec ml_geq x y |R>>
pure R (= (x >= y)%I).
Parameter ml_lt_spec : Spec ml_lt x y |R>>
pure R (= (x < y)%I).
Parameter ml_gt_spec : Spec ml_gt x y |R>>
pure R (= (x > y)%I).
Hint Extern 1 (RegisterSpec ml_plus) => Provide ml_plus_spec.
Hint Extern 1 (RegisterSpec ml_minus) => Provide ml_minus_spec.
Hint Extern 1 (RegisterSpec ml_div) => Provide ml_div_spec.
Hint Extern 1 (RegisterSpec ml_mod) => Provide ml_mod_spec.
Hint Extern 1 (RegisterSpec ml_leq) => Provide ml_leq_spec.
Hint Extern 1 (RegisterSpec ml_geq) => Provide ml_geq_spec.
Hint Extern 1 (RegisterSpec ml_lt) => Provide ml_lt_spec.
Hint Extern 1 (RegisterSpec ml_gt) => Provide ml_gt_spec.
(* ********************************************************************** *)
(* Bitwise arithmetic operators. *)
Parameter ml_land_spec : Spec ml_land x y |R>>
pure R (= (Z.land x y)).
Goal Z.land 7 28 = 4.
Proof. reflexivity. Qed.
Goal Z.land (-7) 28 = 24.
Proof. reflexivity. Qed.
Goal Z.land 7 (-28) = 4.
Proof. reflexivity. Qed.
Goal Z.land (-7) (-28) = -32.
Proof. reflexivity. Qed.
Hint Extern 1 (RegisterSpec ml_land) => Provide ml_land_spec.
Parameter ml_lor_spec : Spec ml_lor x y |R>>
pure R (= (Z.lor x y)).
Goal Z.lor 7 28 = 31.
Proof. reflexivity. Qed.
Goal Z.lor (-7) 28 = -3.
Proof. reflexivity. Qed.
Goal Z.lor 7 (-28) = -25.
Proof. reflexivity. Qed.
Goal Z.lor (-7) (-28) = -3.
Proof. reflexivity. Qed.
Hint Extern 1 (RegisterSpec ml_lor) => Provide ml_lor_spec.
Parameter ml_lxor_spec : Spec ml_lxor x y |R>>
pure R (= (Z.lxor x y)).
Goal Z.lxor 7 28 = 27.
Proof. reflexivity. Qed.
Goal Z.lxor (-7) 28 = -27.
Proof. reflexivity. Qed.
Goal Z.lxor 7 (-28) = -29.
Proof. reflexivity. Qed.
Goal Z.lxor (-7) (-28) = 29.
Proof. reflexivity. Qed.
Hint Extern 1 (RegisterSpec ml_lxor) => Provide ml_lxor_spec.
Definition lnot (x : Z) : Z := -(x + 1).
Parameter ml_lnot_spec : Spec ml_lnot x |R>>
pure R (= (lnot x)).
Goal lnot 44 = -45.
Proof. reflexivity. Qed.
Goal lnot (-44) = 43.
Proof. reflexivity. Qed.
Hint Extern 1 (RegisterSpec ml_lnot) => Provide ml_lnot_spec.
Parameter ml_lsl_spec : Spec ml_lsl x y |R>>
0 <= y ->
(* y < Sys.word_size -> *)
pure R (= (Z.shiftl x y)).
Goal Z.shiftl 7 2 = 28.
Proof. reflexivity. Qed.
Goal Z.shiftl (-7) 2 = -28.
Proof. reflexivity. Qed.
Hint Extern 1 (RegisterSpec ml_lsl) => Provide ml_lsl_spec.
Parameter ml_lsr_spec : Spec ml_lsr x y |R>>
(* We temporarily? restrict [lsr] to nonnegative integers,
so it behaves like [asr]. Anyway, [lsr] really operates
on unsigned integers, and this notion is missing in CFML. *)
0 <= x ->
0 <= y ->
(* y < Sys.word_size -> *)
pure R (= (Z.shiftr x y)).
Goal Z.shiftr 7 2 = 1.
Proof. reflexivity. Qed.
Hint Extern 1 (RegisterSpec ml_lsr) => Provide ml_lsr_spec.
Parameter ml_asr_spec : Spec ml_asr x y |R>>
0 <= y ->
(* y < Sys.word_size -> *)
pure R (= (Z.shiftr x y)).
Goal Z.shiftr 7 2 = 1.
Proof. reflexivity. Qed.
Goal Z.shiftr (-7) 2 = -2.
Proof. reflexivity. Qed.
Hint Extern 1 (RegisterSpec ml_asr) => Provide ml_asr_spec.
(************************************************************)
(** Pairs *)
Parameter ml_fst_spec : forall a1 a2,
Spec ml_fst (p:a1*a2) |R>>
pure R (= fst p).
Parameter ml_snd_spec : forall a1 a2,
Spec ml_snd (p:a1*a2) |R>>
pure R (= snd p).
Hint Extern 1 (RegisterSpec ml_fst) => Provide ml_fst_spec.
Hint Extern 1 (RegisterSpec ml_snd) => Provide ml_snd_spec.
(************************************************************)
(** Arrays *)
Parameter ml_max_array_length_spec :
0 <= ml_max_array_length.
(* We could also axiomatize that this is a power of 2. *)
(************************************************************)
(** Lists *)
Parameter ml_list_iter_spec : forall a,
Spec ml_list_iter f l |R>> forall (I:list a->hprop),
(forall x t, (App f x;) (I (x::t)) (# I t)) ->
R (I l) (# I nil).
Hint Extern 1 (RegisterSpec ml_list_iter) => Provide ml_list_iter_spec.
(************************************************************)
(** Stacks *)
Module Stack_ml.
Definition t (A:Type) := loc.
End Stack_ml.
Parameter ml_stack_create : func.
Parameter ml_stack_is_empty : func.
Parameter ml_stack_push : func.
Parameter ml_stack_pop : func.
(************************************************************)
(** Stream *)
(* TODO *)
Definition stream := list.
Definition stream_cell := list.
(********************************************************************)
(** IO manipulations *)
Parameter Channel : forall (L:list dynamic) (l:loc), hprop.
Notation "l ~>> L" := (l ~> Channel L)
(at level 32, no associativity).
Parameter ml_read_int_spec :
Spec ml_read_int () |R>> forall L (n:int),
R (stdin ~>> (dyn n::L)) (fun x => \[x = n] \* stdin ~>> L).
Parameter ml_print_int_spec :
Spec ml_print_int (n:int) |R>> forall L,
R (stdout ~>> L) (# stdout ~>> L & (dyn n)).
Hint Extern 1 (RegisterSpec ml_read_int) => Provide ml_read_int_spec.
Hint Extern 1 (RegisterSpec ml_print_int) => Provide ml_print_int_spec.
(* Tools for stdio *)
Definition list_dyn A (L:list A) :=
LibList.map dyn L.
Lemma list_dyn_nil : forall A,
list_dyn (@nil A) = nil.
Proof. auto. Qed.
Lemma list_dyn_cons : forall A X (L:list A),
list_dyn (X::L) = (dyn X)::(list_dyn L).
Proof. auto. Qed.
Lemma list_dyn_last : forall A X (L:list A),
list_dyn (L&X) = (list_dyn L) & (dyn X).
Proof. intros. unfold list_dyn. rew_list~. Qed.
Hint Rewrite list_dyn_nil list_dyn_cons list_dyn_last: rew_app.
Hint Rewrite list_dyn_nil list_dyn_cons list_dyn_last : rew_map.
Hint Rewrite list_dyn_nil list_dyn_cons list_dyn_last: rew_list.
......@@ -665,6 +665,10 @@ directly replaced with <code>Q1 tt ==> Q2 tt</code>.
<p> [xfor_inv I as i C] can be used to also specify the hypothesis
providing the bounds for the loop counter.
<p>Tip: by default, [xfor] and its variants do not allow dropping
permissions after the loop terminates. If this flexibility is
required, then one should use [xgc] followed by [xfor].</p>
<!-- -------------------------------------------------- -->
<h3>xapply</h3>