Commit 0f1d099b authored by charguer's avatar charguer
Browse files

toutbon

parent e2be220f
......@@ -4,7 +4,6 @@ MAJOR TODAY
- rename xextract to xpull; and xgen to xpush.
- Sys.max_array_length
......
......@@ -613,7 +613,7 @@ Proof using.
app f [k v l] \[] \[= list_update k v l ]).
{ xmatch.
{ xrets~. }
{ xapps~. xret. xextracts. xif.
{ xapps~. xret. xpulls. xif.
{ xrets. case_if. auto. }
{ xapp_spec infix_emark_eq_gen_spec. intros M. xif.
{ xrets. case_if~. }
......@@ -809,7 +809,7 @@ Lemma assert_in_seq_spec :
app assert_in_seq [tt] \[] \[= 4].
Proof using.
xcf. xlet. xassert. { xrets. } xrets.
xextracts. xrets~.
xpulls. xrets~.
Qed.
......@@ -825,7 +825,7 @@ Qed.
Lemma if_term_spec :
app if_term [tt] \[] \[= 1].
Proof using.
xcf. xfun. xapp. xret. xextracts.
xcf. xfun. xapp. xret. xpulls.
xif. xrets~.
Qed.
......@@ -844,7 +844,7 @@ Proof using.
xseq. xif (Hexists n, \[n >= 0] \* r ~~> n).
{ xapp. xsimpl. math. }
{ xrets. math. }
{ (*xclean.*) xextract ;=>> P. xapp. xextracts. xsimpl. math. }
{ (*xclean.*) xpull ;=>> P. xapp. xpulls. xsimpl. math. }
Qed.
......@@ -862,7 +862,7 @@ Proof using.
intros k. induction_wf IH: (downto 0) k; intros Hk.
applys (rm HR). xlet.
{ xapps. xrets. }
{ xextracts. xif.
{ xpulls. xif.
{ xseq. xapps. xapps. simpl. xapplys IH. hnf. skip. skip. skip. } (* TODO math. *)
{ xrets. math. skip. } } (* TODO math. *)
xapps. xsimpl~. }
......@@ -870,9 +870,9 @@ Proof using.
{ xwhile_inv (fun b k => \[k >= 0] \* \[b = isTrue (k > 0)]
\* n ~~> k \* c ~~> (3-k)) (downto 0).
{ xsimpl*. math. }
{ intros S LS b k FS. xextract. intros. xlet.
{ intros S LS b k FS. xpull. intros. xlet.
{ xapps. xrets. }
{ xextracts. xif.
{ xpulls. xif.
{ xseq. xapps. xapps. simpl. xapplys FS.
hnf. skip. skip. eauto. skip. eauto. eauto. } (* TODO math. *)
{ xret. xsimpl. math. math. } } }
......@@ -880,8 +880,8 @@ Proof using.
{ xwhile_inv_basic (fun b k => \[k >= 0] \* \[b = isTrue (k > 0)]
\* n ~~> k \* c ~~> (3-k)) (downto 0).
{ xsimpl*. math. }
{ intros b k. xextract ;=> Hk Hb. xapps. xrets. xauto*. math. }
{ intros k. xextract ;=> Hk Hb. xapps. xapps. xsimpl. skip. eauto. skip. hnf. skip. }
{ intros b k. xpull ;=> Hk Hb. xapps. xrets. xauto*. math. }
{ intros k. xpull ;=> Hk Hb. xapps. xapps. xsimpl. skip. eauto. skip. hnf. skip. }
{ => k Hk Hb. xapp. xsimpl. skip. (* math.*) } }
{ (* using a measure [fun k => abs k] *)
xwhile_inv_basic (fun b k => \[k >= 0] \* \[b = isTrue (k > 0)]
......@@ -914,8 +914,8 @@ Proof using.
{ xwhile_inv_basic (fun (b:bool) (_:unit) => \[b = false]) (fun (_ _:unit) => False).
{ intros_all. constructor. auto_false. }
{ xsimpl*. }
{ intros. xextracts. xrets~. }
{ intros. xextract. auto_false. }
{ intros. xpulls. xrets~. }
{ intros. xpull. auto_false. }
{ xsimpl~. }
}
Qed.
......@@ -1022,7 +1022,7 @@ Proof using.
{ xgo*. subst. xclean. auto. }
(* todo: maybe extend [xauto_common] with [logics]? or would it be too slow? *)
}
xextracts. xif. xrets~.
xpulls. xif. xrets~.
Qed.
Lemma lazyop_mixex_spec :
......@@ -1051,11 +1051,11 @@ Proof using.
dup 2.
{
xcf. xapps. xfun. xfun. xfun.
xapps. { xapps. xrets~. } xextracts.
xapps. { xassert. xapps. xrets~. xapps. xrets~. } xextracts.
xapps. { xapps. xrets~. } xpulls.
xapps. { xassert. xapps. xrets~. xapps. xrets~. } xpulls.
xapps. { xassert. xapps. xrets~. xfun.
xrets~ (fun f => \[AppCurried f [a b] := (Ret (a + b)%I)] \* r ~~> 2). eauto. }
xextract ;=> Hf.
xpull ;=> Hf.
xapp. xrets~.
(* TODO: can we make xret guess the post?
The idea is to have [(Ret f) H ?Q] where [f:func] and [f] has a spec in hyps
......@@ -1072,8 +1072,8 @@ Proof using.
Qed.
(* Details:
xcf. xapps. xfun. xfun.
xapps. { xapps. xrets~. } xextracts.
xapps. { xassert. xapps. xrets~. xrets~. } xextracts.
xapps. { xapps. xrets~. } xpulls.
xapps. { xassert. xapps. xrets~. xrets~. } xpulls.
xrets~.
*)
......@@ -1216,7 +1216,7 @@ Definition Sitems A (L:list A) r :=
Lemma sitems_push_spec : forall (A:Type) (r:loc) (L:list A) (x:A),
app sitems_push [x r] (r ~> Sitems L) (# r ~> Sitems (x::L)).
Proof using.
xcf. xunfold Sitems. xextract ;=> n E.
xcf. xunfold Sitems. xpull ;=> n E.
xapps. xapps. xapps. xapp. xsimpl. rew_list; math.
Qed.
......@@ -1255,7 +1255,7 @@ Lemma sitems_push_spec' : forall (A:Type) (r:loc) (L:list A) (x:A),
app sitems_push [x r] (r ~> Sitems L) (# r ~> Sitems (x::L)).
Proof using.
xcf. dup 2.
{ xopen r. xextract ;=> n E. skip. }
{ xopen r. xpull ;=> n E. skip. }
{ xopenx r ;=> n E. xapps. xapps. xapps. xapp.
xclose r. rew_list; math. xsimpl~. }
Qed.
......
let max_array_length = 1000
module type HashedType = sig
type t
val equal: t -> t -> bool
val hash: t -> int
end
(* A note on array bounds checks. In OCaml, a call [Array.get a i] is always
checked, a call [Array.unsafe_get a i] is never checked, and an array access
expression [a.(i)] is checked if and only if the compile-time flag [-unsafe]
is not passed. In the code that follows, we use the latter form. When
processed by CFML, without [-unsafe], this form is translated to
[Array.get a i], and we prove that the array index is within bounds. When
compiled with OCaml, we pass [-unsafe], so the check is not performed. *)
(* In this code, array indices are always within bounds, even if the client is
unverified. This claim is informal, though; at present, we cannot explicitly
reason about an unverified client in CFML. *)
module Make (H : HashedType) = struct
type key = H.t
(* A bucket is is a list of (unboxed) pairs of a key and a value. *)
type 'a bucket =
Empty
| Cons of H.t * 'a * 'a bucket
(* The [data] field holds an array of buckets. The length of this array is
always a power of two. Information about the key [k] is stored at index
[index h k] in this array. The [population] field records how many
bindings (i.e. key-data pairs) are present in the table. The [init] field
records the table's initial capacity; it is used only by [reset]. *)
type 'a table = {
mutable data: 'a bucket array;
mutable population: int;
init: int;
type 'a vector = {
mutable default : 'a;
mutable size : int;
mutable data : 'a array;
}
let length t =
t.size
let default t =
t.default
let make size def =
(* assert (size >= 0); *)
{ default = def;
size;
data = Array.make size def;
}
type 'a t = 'a table
(* [power_2_above x n] requires [x] to be a power of two, and ensures that
its result [y] is a power of two and satisfies [x <= y]. *)
(* It does NOT guarantee [n <= y]. In reality, this will be the case unless
[max_array_length] is reached. We do not exceed [max_array_length],
because we know that this will cause a failure when attempting to
allocate the array. Also, this guarantees that the function terminates
before an overflow can occur. These aspects are outside of the scope of
the formal proof. *)
let rec power_2_above x n =
if x >= n then x
else if x * 2 > max_array_length then x
else power_2_above (x * 2) n
let create init =
let init = power_2_above 16 init in
{ data = Array.make init Empty; population = 0; init }
let clear h =
h.population <- 0;
Array.fill h.data 0 (Array.length h.data) Empty
let reset h =
h.population <- 0;
h.data <- Array.make h.init Empty
let copy h = {
data = Array.copy h.data;
population = h.population;
init = h.init
let init size default f =
(* assert (size >= 0); *)
{ default;
size;
data = Array.init size f;
}
let population h =
h.population
let length =
population
let index h k =
(H.hash k) land (Array.length h.data - 1)
(* [insert_bucket data mask b] inserts the key-data pairs in [b],
back-to-front, into the array [data]. *)
(* [mask] must be [Array.length data - 1]. *)
(* TEMPORARY measure to see if [mask] is useful *)
let rec insert_bucket data mask = function
| Empty ->
()
| Cons (k, x, b) ->
insert_bucket data mask b; (* preserve the original order of elements *)
let i = (H.hash k) land mask in (* inlined [index] *)
data.(i) <- Cons (k, x, data.(i))
let resize h =
let odata = h.data in
let nsize = Array.length odata * 2 in
if nsize < max_array_length then begin
let ndata = Array.make nsize Empty in
h.data <- ndata;
let mask = nsize - 1 in
(* We could use [Array.iter] and rely on the OCaml compiler to inline
it. The flambda compiler can do it. Still, it seems preferable to
use an explicit loop. *)
for i = 0 to Array.length odata - 1 do
insert_bucket ndata mask odata.(i)
done
end
let increment_population h =
h.population <- h.population + 1;
if h.population > 2 * Array.length h.data then resize h
let add h k x =
let i = index h k in
h.data.(i) <- (Cons (k, x, h.data.(i)));
increment_population h
let rec remove_bucket h k = function
| Empty ->
Empty
| Cons (k', i, next) ->
if H.equal k' k
then begin h.population <- h.population - 1; next end
else Cons (k', i, remove_bucket h k next)
let remove h k =
let i = index h k in
h.data.(i) <- remove_bucket h k h.data.(i)
let rec find_rec k = function
| Empty ->
None
| Cons (k', d, rest) ->
if H.equal k' k then Some d else find_rec k rest
let find h k =
find_rec k h.data.(index h k)
let find_all h k =
let rec find_in_bucket = function
| Empty ->
[]
| Cons(k', d, rest) ->
if H.equal k' k
then d :: find_in_bucket rest
else find_in_bucket rest in
find_in_bucket h.data.(index h k)
let replace h k x =
let i = index h k in
let b = remove_bucket h k h.data.(i) in
h.data.(i) <- Cons (k, x, b);
increment_population h
let mem h k =
match find h k with None -> false | Some _ -> true
let rec iter_bucket f = function
| Empty ->
()
| Cons(k, x, b) ->
f k x;
iter_bucket f b
let iter f h =
let data = h.data in
for i = 0 to Array.length data - 1 do
iter_bucket f data.(i)
done
let fold f h init =
let rec do_bucket accu b =
match b with
Empty ->
accu
| Cons(k, d, rest) ->
do_bucket (f k d accu) rest in
Array.fold_left do_bucket init h.data
type statistics = {
num_bindings: int;
num_buckets: int;
max_bucket_length: int;
bucket_histogram: int array
let get t i =
(* assert (i >= 0 && i < t.size); *)
t.data.(i)
let set t i v =
(* assert (i >= 0 && i < t.size); *)
t.data.(i) <- v
let transfer src dst nb =
for i = 0 to nb - 1 do
dst.(i) <- src.(i);
done
(* Distinguer le resize_extacly & resize_at_least *)
(* Option de remplir avec default quand on shrink *)
(* set_physical_size *)
(* get_physical_size *)
let resize t new_capa =
(* assert (new_capa >= 0); *)
let old_data = t.data in
t.data <- Array.make new_capa t.default;
transfer old_data t.data t.size
let push t x =
let capa = Array.length t.data in
if t.size = capa then
resize t (2 * (capa + 1));
t.data.(t.size) <- x;
t.size <- t.size + 1
(* TODO: Return option *)
let pop t =
(* assert (t.size > 0); *)
t.size <- t.size - 1;
let x = t.data.(t.size) in
let capa = Array.length t.data in
if (capa > 4) && (t.size <= capa / 4) then
resize t (capa / 2);
x
let is_empty t =
t.size = 0
let copy t =
{ default = t.default;
size = t.size;
data = Array.copy t.data;
}
let rec bucket_length accu = function
| Empty -> accu
| Cons(_, _, rest) -> bucket_length (accu + 1) rest
let stats h =
let mbl =
Array.fold_left (fun m b -> max m (bucket_length 0 b)) 0 h.data in
let histo = Array.make (mbl + 1) 0 in
Array.iter
(fun b ->
let l = bucket_length 0 b in
histo.(l) <- histo.(l) + 1)
h.data;
{ num_bindings = h.population;
num_buckets = Array.length h.data;
max_bucket_length = mbl;
bucket_histogram = histo }
end
let to_array t =
let s = length t in
Array.init s (fun i -> get t i)
let of_array default a =
{ default;
size = Array.length a;
data = Array.copy a;
}
......@@ -221,7 +221,7 @@ Proof using.
simpls. applys~ local_frame_gc M.
rewrite~ app_ge_2_unfold. rewrite~ app_ge_2_unfold in M.
applys~ local_frame M. intros g.
hextract as HR LR. hsimpl (HR \* H2). applys* IHxs LR.
hpull as HR LR. hsimpl (HR \* H2). applys* IHxs LR.
Qed.
Lemma app_weaken : forall B f xs H (Q Q':B->hprop),
......@@ -243,7 +243,7 @@ Proof using.
simpls. applys~ local_frame M.
rewrite~ app_ge_2_unfold. rewrite~ app_ge_2_unfold in M.
applys~ local_frame M. intros g.
hextract as HR LR. hsimpl (HR \* H'). applys* IHxs.
hpull as HR LR. hsimpl (HR \* H'). applys* IHxs.
Qed.
Lemma app_weaken : forall B f xs H (Q Q':B->hprop),
......@@ -276,7 +276,7 @@ Proof using.
intros h Hh. specializes M Hh.
destruct M as (H1&H2&Q1&R1&R2&R3). exists___. splits.
eauto. eauto.
intros g. hextract as H' L. hsimpl (H' \* H2).
intros g. hpull as H' L. hsimpl (H' \* H2).
applys app_wgframe L. hsimpl. hchange R3. hsimpl. }
Qed.
......@@ -370,15 +370,15 @@ Proof using.
rewrite curried_ge_2_unfold in C; [|math].
tests E: (zs = nil).
{ unfold app_def at 1. eapply local_weaken_post. auto. applys (rm C).
intros g. hextract as [M1 M2]. hsimpl. split.
intros g. hpull as [M1 M2]. hsimpl. split.
rew_list. applys_eq M1 2. math.
introv E AK. rew_list in *. applys M2. math. auto. }
{ asserts Pzs: (0 < length zs). { destruct zs. tryfalse. rew_list. math. }
rew_list in N. rewrite~ app_ge_2_unfold.
eapply local_weaken_post. auto. applys (rm C). clear C. (* todo: make work rm *)
intros h. hextract as [M1 M2]. hsimpl.
intros h. hpull as [M1 M2]. hsimpl.
applys app_weaken. applys (rm IH) M1. math. math. clear IH.
intros g. hextract as [N1 N2]. hsimpl. split.
intros g. hpull as [N1 N2]. hsimpl. split.
{ rew_list. applys_eq N1 2. math. }
{ introv P1 P2. rew_list in P1.
applys N2. math.
......
......@@ -1283,7 +1283,7 @@ Tactic Notation "xunfold" constr(E) "at" constr(n) :=
(********************************************************************)
(* ** Shared tactics *)
Ltac prepare_goal_hextract_himpl tt :=
Ltac prepare_goal_hpull_himpl tt :=
match goal with
| |- @rel_le unit _ _ _ => let t := fresh "_tt" in intros t; destruct t
| |- @rel_le _ _ _ _ => let r := fresh "r" in intros r
......@@ -1337,27 +1337,27 @@ Ltac remove_empty_heaps_formula tt :=
(** Lemmas *)
Lemma hextract_start : forall H H',
Lemma hpull_start : forall H H',
\[] \* H ==> H' -> H ==> H'.
Proof using. intros. rew_heap in *. auto. Qed.
Lemma hextract_stop : forall H H',
Lemma hpull_stop : forall H H',
H ==> H' -> H \* \[] ==> H'.
Proof using. intros. rew_heap in *. auto. Qed.
Lemma hextract_keep : forall H1 H2 H3 H',
Lemma hpull_keep : forall H1 H2 H3 H',
(H2 \* H1) \* H3 ==> H' -> H1 \* (H2 \* H3) ==> H'.
Proof using. intros. rewrite (star_comm H2) in H. rew_heap in *. auto. Qed.
Lemma hextract_starify : forall H1 H2 H',
Lemma hpull_starify : forall H1 H2 H',
H1 \* (H2 \* \[]) ==> H' -> H1 \* H2 ==> H'.
Proof using. intros. rew_heap in *. auto. Qed.
Lemma hextract_assoc : forall H1 H2 H3 H4 H',
Lemma hpull_assoc : forall H1 H2 H3 H4 H',
H1 \* (H2 \* (H3 \* H4)) ==> H' -> H1 \* ((H2 \* H3) \* H4) ==> H'.
Proof using. intros. rew_heap in *. auto. Qed.
Lemma hextract_prop : forall H1 H2 H' (P:Prop),
Lemma hpull_prop : forall H1 H2 H' (P:Prop),
(P -> H1 \* H2 ==> H') -> H1 \* (\[P] \* H2) ==> H'.
Proof using.
introv W. intros h Hh.
......@@ -1366,7 +1366,7 @@ Proof using.
rewrite heap_union_neutral_l in *. splits~.
Qed.
Lemma hextract_empty : forall H1 H2 H',
Lemma hpull_empty : forall H1 H2 H',
(H1 \* H2 ==> H') -> H1 \* (\[] \* H2) ==> H'.
Proof using.
introv W. intros h Hh. destruct Hh as (h1&h2'&?&(h2&h3&M&?&?&?)&?&?).
......@@ -1374,11 +1374,11 @@ Proof using.
rewrite heap_union_neutral_l in *. splits~.
Qed.
Lemma hextract_id : forall A (x X : A) H1 H2 H',
Lemma hpull_id : forall A (x X : A) H1 H2 H',
(x = X -> H1 \* H2 ==> H') -> H1 \* (x ~> Id X \* H2) ==> H'.
Proof using. intros. unfold Id. apply~ hextract_prop. Qed.
Proof using. intros. unfold Id. apply~ hpull_prop. Qed.
Lemma hextract_exists : forall A H1 H2 H' (J:A->hprop),
Lemma hpull_exists : forall A H1 H2 H' (J:A->hprop),
(forall x, H1 \* J x \* H2 ==> H') -> H1 \* (heap_is_pack J \* H2) ==> H'.
Proof using.
introv W. intros h Hh.
......@@ -1389,77 +1389,77 @@ Qed.
(** Tactics *)
Ltac hextract_setup tt :=
prepare_goal_hextract_himpl tt;
Ltac hpull_setup tt :=
prepare_goal_hpull_himpl tt;
lets: ltac_mark;
apply hextract_start.
apply hpull_start.
Ltac hextract_cleanup tt :=
apply hextract_stop;
Ltac hpull_cleanup tt :=
apply hpull_stop;
remove_empty_heaps_left tt;
tryfalse;
gen_until_mark.
Ltac hextract_step tt :=
Ltac hpull_step tt :=
match goal with |- _ \* ?HN ==> _ =>
match HN with
| ?H \* _ =>
match H with
| \[] => apply hextract_empty
| \[_] => apply hextract_prop; intros
| _ ~> Id _ => apply hextract_id; intros
| heap_is_pack _ => apply hextract_exists; intros
| _ \* _ => apply hextract_assoc
| _ => apply hextract_keep
| \[] => apply hpull_empty
| \[_] => apply hpull_prop; intros
| _ ~> Id _ => apply hpull_id; intros
| heap_is_pack _ => apply hpull_exists; intros
| _ \* _ => apply hpull_assoc
| _ => apply hpull_keep
end
| \[] => fail 1
| ?H => apply hextract_starify
| ?H => apply hpull_starify
end end.
Ltac hextract_main tt :=
hextract_setup tt;
(repeat (hextract_step tt));
hextract_cleanup tt.
Ltac hpull_main tt :=
hpull_setup tt;
(repeat (hpull_step tt));