Skip to content

Instantly share code, notes, and snippets.

@gdsfh

gdsfh/BlockReader.v Secret

Created August 14, 2013 15:15
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save gdsfh/47b34f009e25cee8c254 to your computer and use it in GitHub Desktop.
Save gdsfh/47b34f009e25cee8c254 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
BlockReader.v
Require Import ZArith.
Open Scope Z_scope.
Require Import String.
Open Scope string_scope.
Definition named_goal (A : Type) (s : string) := A.
Notation _as s := (_ : named_goal _ s).
Tactic Notation "proving" "goal" constr(name) :=
match goal with
| |- named_goal _ name => unfold named_goal
| _ => fail 1 "current goal is not '" name "'"
end
.
Definition named_goalP (A : Prop) (s : string) := A.
Notation _asP s := (_ : named_goalP _ s).
Tactic Notation "proving" "goalP" constr(name) :=
match goal with
| |- named_goalP _ name => unfold named_goalP
| _ => fail 1 "current goalP is not '" name "'"
end
.
Definition bs := 512
.
Definition bs2 := 2 * bs
.
(* field beginning with Capital letter are not present in OCaml code *)
(* file emulation *)
Record file :=
{ Ofs : Z (* current offset for next read *)
}
.
(* array is defined as "something containing file data".
in OCaml it's just a string of length "bs2".
here all fields are not present in OCaml (as no real data
exists in model).
*)
Record array :=
{ Arr_ofs : Z (* offset of data beginning *)
; Arr_len : Z (* length of data *)
; File_ofs : Z (* from which file offset these data was read *)
; Aarr : Arr_ofs >= 0 /\ Arr_len >= 0 /\ Arr_ofs + Arr_len <= bs2
; Aalign : File_ofs mod bs = Arr_ofs mod bs
}
.
(* represents the main OCaml data structure used to read from file.
here "buf_ofs" and "buf_len" are physically stored unlike in "array",
and we have guarantees that they are equal to "array"'s ones.
*)
Record buffer :=
{ buf_ofs : Z
; buf_len : Z
; buf_arr : array
; Bbufarr : buf_ofs = buf_arr.(Arr_ofs) /\ buf_len = buf_arr.(Arr_len)
; buf_len_to_eof : Z (* how many bytes we can read from file *)
; Beof : buf_len_to_eof >= 0
}
.
Record world :=
{ w_file : file
; w_buf : buffer
; Wbuffile : w_buf.(buf_arr).(File_ofs) + w_buf.(buf_len) = w_file.(Ofs)
}
.
Ltac spl :=
match goal with
| H : _ /\ _ |- _ => destruct H; spl
| _ => idtac
end
.
Ltac destr_type t :=
match goal with
| v : t |- _ => destruct v; destr_type t
| _ => idtac
end
.
Ltac nom := try reflexivity; try assumption; abstract omega
.
Ltac subst_lets :=
match goal with
| A := _ |- _ => subst A; subst_lets
| _ => idtac
end
.
Definition read_into_buffer
(sz : Z)
(w : world)
{Hsz_pos : sz > 0}
{Hsz_fits : w.(w_buf).(buf_ofs) + w.(w_buf).(buf_len) + sz <= bs2}
{Heof : sz <= w.(w_buf).(buf_len_to_eof)}
:
{ w' : world
| w'.(w_buf).(buf_len_to_eof) = w.(w_buf).(buf_len_to_eof) - sz
/\ w'.(w_file).(Ofs) = w.(w_file).(Ofs) + sz
/\ w'.(w_buf).(buf_len) = w.(w_buf).(buf_len) + sz
/\ w'.(w_buf).(buf_ofs) = w.(w_buf).(buf_ofs)
/\ w'.(w_buf).(buf_arr).(File_ofs) = w.(w_buf).(buf_arr).(File_ofs)
}
.
refine (
let fil := w.(w_file) in
let buf := w.(w_buf) in
let fil' := {| Ofs := fil.(Ofs) + sz |} in
let ba := buf.(buf_arr) in
let Arr_ofs' := ba.(Arr_ofs) in
let Arr_len' := ba.(Arr_len) + sz in
let File_ofs' := ba.(File_ofs) in
let Aarr' : Arr_ofs' >= 0 /\ Arr_len' >= 0 /\ Arr_ofs' + Arr_len' <= bs2 := _ in
let Aalign' : File_ofs' mod bs = Arr_ofs' mod bs := _ in
_
); repeat split; try (destruct ba; subst; subst_lets; simpl in *; spl; nom).
(**)
subst ba.
destruct w as [ w0_file w0_buf W0buffile ]; simpl in *.
subst fil buf.
destruct w0_buf; simpl in *.
spl.
subst Arr_ofs' Arr_len'.
nom.
(**)
refine (
let ba' :=
{| Arr_ofs := ba.(Arr_ofs)
; Arr_len := ba.(Arr_len) + sz
; File_ofs := ba.(File_ofs)
; Aarr := Aarr'
; Aalign := Aalign'
|}
in
let B'bufarr : buf_ofs buf = Arr_ofs ba' /\ buf_len buf + sz = Arr_len ba' := _ in
_
); repeat split; try (subst ba; destruct buf; simpl in *; nom).
(**)
refine (
let B'eof : buf.(buf_len_to_eof) - sz >= 0 := _ in
_
).
(**)
destruct w; simpl in *; subst buf; nom.
(**)
refine (
let buf' :=
{| buf_ofs := buf.(buf_ofs)
; buf_len := buf.(buf_len) + sz
; buf_arr := ba'
; buf_len_to_eof := buf.(buf_len_to_eof) - sz
; Bbufarr := B'bufarr
; Beof := B'eof
|}
in
let W'buffile : ba'.(File_ofs) + buf'.(buf_len) = fil'.(Ofs) := _ in
exist
_
{| w_file := fil'
; w_buf := buf'
; Wbuffile := W'buffile
|}
_
); subst fil' Arr_ofs' Arr_len' File_ofs'; simpl in *;
destr_type world; subst; simpl in *; subst_lets; nom
.
Defined.
(* all fields are not present in OCaml, since consumer is just a string. *)
Record consumer :=
{ Con_to_read : Z
; Con_ofs : Z
; Con_file_ofs_from : Z
(* when reading into substring to "init_ofs", it's "real_file_ofs - init_ofs" *)
; Cto_read : Con_to_read >= 0
; Cofs : Con_ofs >= 0
}
.
Lemma modplus : forall a b c n,
a mod n = b mod n -> (a + c) mod n = (b + c) mod n.
intros a b c n H.
refine (Zplus_eqm _ _ _ _ _ _ _).
exact H.
refine (eqm_refl _ _).
Defined.
Definition blit_from_buffer
(w : world)
(con : consumer)
(con_ofs_dest : Z)
(len : Z)
{Cofs : con.(Con_ofs) = con_ofs_dest}
{Ccontoread_gt_0 : con.(Con_to_read) > 0}
{Cfits : len <= con.(Con_to_read)}
{Clen_gt_0 : len > 0}
{Bhas : w.(w_buf).(buf_len) >= len}
{Cfileofs : con.(Con_file_ofs_from) + con.(Con_ofs)
= w.(w_buf).(buf_arr).(File_ofs)
}
:
{ wc' : world * consumer
| let (w', c') := wc' in
w'.(w_buf).(buf_arr).(File_ofs) = w.(w_buf).(buf_arr).(File_ofs) + len
/\ c'.(Con_to_read) = con.(Con_to_read) - len
/\ c'.(Con_ofs) = con.(Con_ofs) + len
/\ c'.(Con_file_ofs_from) = con.(Con_file_ofs_from)
/\ w'.(w_buf).(buf_ofs) = w.(w_buf).(buf_ofs) + len
/\ w'.(w_buf).(buf_len) = w.(w_buf).(buf_len) - len
/\ c'.(Con_file_ofs_from) + c'.(Con_ofs) = w'.(w_buf).(buf_arr).(File_ofs)
/\ w'.(w_buf).(buf_len_to_eof) = w.(w_buf).(buf_len_to_eof)
}
.
refine (
let buf := w.(w_buf) in
let ba := buf.(buf_arr) in
let Arr_ofs' := ba.(Arr_ofs) + len in
let Arr_len' := ba.(Arr_len) - len in
let File_ofs' := ba.(File_ofs) + len in
let Aarr' : Arr_ofs' >= 0 /\ Arr_len' >= 0 /\ Arr_ofs' + Arr_len' <= bs2 := _ in
let Aalign' : File_ofs' mod bs = Arr_ofs' mod bs := _ in
let ba' :=
{| Arr_ofs := Arr_ofs'
; Arr_len := Arr_len'
; File_ofs := File_ofs'
; Aarr := Aarr'
; Aalign := Aalign'
|}
in
let buf_ofs' := buf.(buf_ofs) + len in
let buf_len' := buf.(buf_len) - len in
let Bbufarr' : buf_ofs' = ba'.(Arr_ofs) /\ buf_len' = ba'.(Arr_len) := _ in
let buf_len_to_eof' := buf.(buf_len_to_eof) in
let Beof' : buf_len_to_eof' >= 0 := _ in
let buf' :=
{| buf_ofs := buf_ofs'
; buf_len := buf_len'
; buf_arr := ba'
; Bbufarr := Bbufarr'
; buf_len_to_eof := buf_len_to_eof'
; Beof := Beof'
|}
in
let Wbuffile' : buf'.(buf_arr).(File_ofs) + buf'.(buf_len)
= w.(w_file).(Ofs) := _ in
let w' :=
{| w_file := w.(w_file)
; w_buf := buf'
; Wbuffile := Wbuffile'
|}
in
let Con_to_read' := con.(Con_to_read) - len in
let Con_ofs' := con.(Con_ofs) + len in
let Cto_read' : Con_to_read' >= 0 := _ in
let Cofs' : Con_ofs' >= 0 := _ in
let con' :=
{| Con_to_read := Con_to_read'
; Con_ofs := Con_ofs'
; Con_file_ofs_from := con.(Con_file_ofs_from)
; Cto_read := Cto_read'
; Cofs := Cofs'
|}
in
exist _ (w', con') _
); repeat split;
subst_lets;
destr_type world; simpl in *;
destr_type buffer; simpl in *; spl;
destr_type array; simpl in *; spl;
destr_type consumer; simpl in *; spl;
try refine (modplus _ _ _ _ _);
try nom
.
Defined.
Definition blit_all
(w : world)
(con : consumer)
(con_ofs_dest : Z)
{Cofs : con.(Con_ofs) = con_ofs_dest}
{Ccontoread_gt_0 : con.(Con_to_read) > 0}
{Bhasless : w.(w_buf).(buf_len) < con.(Con_to_read)}
{Cfileofs : con.(Con_file_ofs_from) + con.(Con_ofs)
= w.(w_buf).(buf_arr).(File_ofs)
}
:
{ wc' : (world * consumer)
| let (w', c') := wc' in
let old_len := w.(w_buf).(buf_len) in
w'.(w_buf).(buf_arr).(File_ofs)
= w.(w_buf).(buf_arr).(File_ofs) + old_len
/\ c'.(Con_to_read) = con.(Con_to_read) - old_len
/\ c'.(Con_ofs) = con.(Con_ofs) + old_len
/\ c'.(Con_file_ofs_from) = con.(Con_file_ofs_from)
/\ w'.(w_buf).(buf_len) = 0
/\ c'.(Con_file_ofs_from) + c'.(Con_ofs) = w'.(w_buf).(buf_arr).(File_ofs)
/\ w'.(w_buf).(buf_len_to_eof) = w.(w_buf).(buf_len_to_eof)
/\ w'.(w_buf).(buf_ofs) = w.(w_buf).(buf_ofs) + w.(w_buf).(buf_len)
}
.
refine (
let buf := w.(w_buf) in
let old_len := buf.(buf_len) in
match Z_dec old_len 0 with
| inleft (left old_len_lt_0) => False_rect _ _
| inright old_len_eq_0 => exist _ (w, con) _
| inleft (right old_len_gt_0) =>
let (wc', wc'pf) := @blit_from_buffer
w
con
con_ofs_dest
old_len
Cofs
Ccontoread_gt_0
(_ : old_len <= con.(Con_to_read))
old_len_gt_0
(_ : w.(w_buf).(buf_len) >= old_len)
Cfileofs
in
exist _ wc' _
end
); try destruct wc'; simpl in *; repeat split;
destr_type world; subst buf; spl; subst old_len; simpl in *; try nom;
destr_type buffer; spl; simpl in *; try nom;
destr_type array; spl; simpl in *; try nom.
Defined.
Lemma mod_bounds : forall (a b : Z) (_ : a >= 0) (_ : b > 0),
a mod b >= 0 /\ a mod b < b.
intros a b H1 H2.
unfold Zmod.
assert (d := Z_div_mod a b H2).
set (qr := Zdiv_eucl a b).
replace (Zdiv_eucl a b) with (qr) in *; try reflexivity.
destruct qr.
now abstract omega.
Defined.
Definition mod_on_notneg (a b : Z) (Ha : a >= 0) (Hb : b > 0) : a mod b >= 0
:= proj1 (mod_bounds a b Ha Hb).
Definition mod_lt (a b : Z) (Ha : a >= 0) (Hb : b > 0) : a mod b < b
:= proj2 (mod_bounds a b Ha Hb).
Definition direct_read0
(con : consumer)
(ofs : Z)
(len : Z)
(w : world)
{Clen : len <= con.(Con_to_read)}
{ArgLen : len >= 0}
{ArgOfs : con.(Con_ofs) = ofs}
{Fhas : len <= w.(w_buf).(buf_len_to_eof)}
{Bempty : w.(w_buf).(buf_len) = 0}
{Cfileofs : con.(Con_file_ofs_from) + con.(Con_ofs)
= w.(w_buf).(buf_arr).(File_ofs)
}
:
{ wc' : world * consumer
| let (w', c') := wc' in
let buf' := w'.(w_buf) in
c'.(Con_ofs) = con.(Con_ofs) + len
/\ c'.(Con_file_ofs_from) = con.(Con_file_ofs_from)
/\ w'.(w_buf).(buf_len_to_eof) >= 0
/\ w'.(w_buf).(buf_len_to_eof) = w.(w_buf).(buf_len_to_eof) - len
/\ c'.(Con_file_ofs_from) + c'.(Con_ofs) = w'.(w_buf).(buf_arr).(File_ofs)
/\ w'.(w_buf).(buf_len) = 0
/\ w'.(w_buf).(buf_ofs) = (w.(w_buf).(buf_ofs) + len) mod bs
/\ w'.(w_file).(Ofs) = w.(w_file).(Ofs) + len
/\ c'.(Con_to_read) = con.(Con_to_read) - len
/\ w'.(w_buf).(buf_arr).(File_ofs) = w.(w_buf).(buf_arr).(File_ofs) + len
}
.
refine (
(* in OCaml here is just Unix.read + modifying buf.buf_ofs *)
let Con_to_read' := con.(Con_to_read) - len in
let Con_ofs' := con.(Con_ofs) + len in
let Cto_read' : Con_to_read' >= 0 := _ in
let Cofs' : Con_ofs' >= 0 := _ in
let con' :=
{| Con_to_read := Con_to_read'
; Con_ofs := Con_ofs'
; Con_file_ofs_from := con.(Con_file_ofs_from)
; Cto_read := Cto_read'
; Cofs := Cofs'
|}
in
let buf := w.(w_buf) in
let ba := buf.(buf_arr) in
let fil' := {| Ofs := w.(w_file).(Ofs) + len |} in
let Arr_ofs' := (ba.(Arr_ofs) + len) mod bs in
let Arr_len' := 0 in
let (m1, m2) := Z_mod_lt (ba.(Arr_ofs) + len) bs (_ : bs > 0) in
let Aarr' : Arr_ofs' >= 0 /\ Arr_len' >= 0 /\ Arr_ofs' + Arr_len' <= bs2 := _ in
let File_ofs' := ba.(File_ofs) + len in
let Aalign' : File_ofs' mod bs = Arr_ofs' mod bs := _ in
let ba' :=
{| Arr_ofs := Arr_ofs'
; Arr_len := Arr_len'
; File_ofs := File_ofs'
; Aarr := Aarr'
; Aalign := Aalign'
|}
in
let buf_ofs' := (buf.(buf_ofs) + len) mod bs in
let buf_len' := 0 in
let Bbufarr' : buf_ofs' = ba'.(Arr_ofs) /\ buf_len' = ba'.(Arr_len) := _ in
let buf_len_to_eof' := buf.(buf_len_to_eof) - len in
let Beof' : buf_len_to_eof' >= 0 := _ in
let buf' :=
{| buf_ofs := buf_ofs'
; buf_len := buf_len'
; buf_arr := ba'
; Bbufarr := Bbufarr'
; buf_len_to_eof := buf_len_to_eof'
; Beof := Beof'
|}
in
let Wbuffile' : buf'.(buf_arr).(File_ofs) + buf'.(buf_len) = fil'.(Ofs) := _ in
let w' :=
{| w_file := fil'
; w_buf := buf'
; Wbuffile := Wbuffile'
|}
in
exist _ (w', con') _
); subst_lets; destr_type (world * consumer)%type; simpl in *; repeat split;
destr_type world;
destr_type buffer; spl; simpl in *;
subst_lets;
destr_type consumer; simpl in *; try nom;
destr_type array; spl; simpl in *; try nom;
unfold bs2, bs in *;
simpl in *; try nom;
try (refine (mod_on_notneg _ _ _ _); nom);
try rewrite Zmod_mod;
try (refine (modplus _ _ _ _ _); subst; nom);
try nom
.
Defined.
Lemma Z_ge_of_gt : forall a b (H : a > b), a >= b. intros; omega. Defined.
Definition direct_read
(con : consumer)
(ofs : Z)
(len : Z)
(w : world)
{Clen : len <= con.(Con_to_read)}
{ArgLen : len > 0}
{ArgOfs : con.(Con_ofs) = ofs}
{Fhas : len <= w.(w_buf).(buf_len_to_eof)}
{Bempty : w.(w_buf).(buf_len) = 0}
{Cfileofs : con.(Con_file_ofs_from) + con.(Con_ofs)
= w.(w_buf).(buf_arr).(File_ofs)
}
:
{ wc' : world * consumer
| let (w', c') := wc' in
let buf' := w'.(w_buf) in
c'.(Con_ofs) = con.(Con_ofs) + len
/\ c'.(Con_file_ofs_from) = con.(Con_file_ofs_from)
/\ w'.(w_buf).(buf_len_to_eof) >= 0
/\ w'.(w_buf).(buf_len_to_eof) = w.(w_buf).(buf_len_to_eof) - len
/\ c'.(Con_file_ofs_from) + c'.(Con_ofs) = w'.(w_buf).(buf_arr).(File_ofs)
/\ w'.(w_buf).(buf_len) = 0
/\ w'.(w_buf).(buf_ofs) = (w.(w_buf).(buf_ofs) + len) mod bs
/\ w'.(w_file).(Ofs) = w.(w_file).(Ofs) + len
/\ c'.(Con_to_read) = con.(Con_to_read) - len
/\ w'.(w_buf).(buf_arr).(File_ofs) = w.(w_buf).(buf_arr).(File_ofs) + len
}
:=
@direct_read0
con
ofs
len
w
Clen
(Z_ge_of_gt _ _ ArgLen)
ArgOfs
Fhas
Bempty
Cfileofs
.
Lemma mod_plus_0 : forall a n, (a + 0) mod n = a mod n.
intros a n.
replace (0) with (0 * n) by nom.
rewrite Z_mod_plus_full; reflexivity.
Defined.
Lemma mod_minus_n : forall a n, (a - n) mod n = a mod n.
intros a n.
rewrite Zminus_mod.
replace (n mod n) with (0).
replace (a mod n - 0) with (a mod n) by nom.
rewrite Zmod_mod.
now reflexivity.
rewrite Z_mod_same_full.
now reflexivity.
Defined.
Definition move_buffer_on_bs
(w : world)
{Bempty : w.(w_buf).(buf_len) = 0}
{Bofs : w.(w_buf).(buf_ofs) >= bs}
:
{ w' : world
| w'.(w_buf).(buf_ofs) = w.(w_buf).(buf_ofs) - bs
/\ w'.(w_buf).(buf_len) = 0
/\ w'.(w_buf).(buf_len_to_eof) = w.(w_buf).(buf_len_to_eof)
/\ w'.(w_file) = w.(w_file)
/\ w'.(w_buf).(buf_arr).(File_ofs) = w.(w_buf).(buf_arr).(File_ofs)
}
.
refine (
(* in OCaml it's just "buf.buf_ofs -= bs" *)
let buf := w.(w_buf) in
let ba := buf.(buf_arr) in
let Arr_ofs' := ba.(Arr_ofs) - bs in
let Arr_len' := 0 in
let File_ofs' := ba.(File_ofs) in
let Aarr' : Arr_ofs' >= 0 /\ Arr_len' >= 0 /\ Arr_ofs' + Arr_len' <= bs2 := _ in
let Aalign' : File_ofs' mod bs = Arr_ofs' mod bs := _ in
let ba' :=
{| Arr_ofs := Arr_ofs'
; Arr_len := Arr_len'
; File_ofs := File_ofs'
; Aarr := Aarr'
; Aalign := Aalign'
|}
in
let buf_ofs' := buf.(buf_ofs) - bs in
let buf_len' := 0 in
let buf_arr := ba' in
let Bbufarr' : buf_ofs' = ba'.(Arr_ofs) /\ buf_len' = ba'.(Arr_len) := _ in
let buf_len_to_eof' := buf.(buf_len_to_eof) in
let Beof' : buf_len_to_eof' >= 0 := _ in
let buf' :=
{| buf_ofs := buf_ofs'
; buf_len := buf_len'
; buf_arr := ba'
; Bbufarr := Bbufarr'
; buf_len_to_eof := buf_len_to_eof'
; Beof := Beof'
|}
in
let Wbuffile' : ba'.(File_ofs) + buf'.(buf_len) = w.(w_file).(Ofs) := _ in
let w' :=
{| w_file := w.(w_file)
; w_buf := buf'
; Wbuffile := Wbuffile'
|}
in
exist _ w' _
); subst_lets; try (repeat split); try unfold bs2, bs in *; try nom;
try now (
destr_type world;
destr_type buffer;
simpl in *; spl;
destr_type array;
spl; simpl in *;
try (rewrite Bempty in *; clear Bempty);
try unfold bs2, bs in *;
try (rewrite mod_minus_n; now assumption);
nom
)
.
Defined.
Lemma mod1 : forall a k n, n > 0 -> a >= k * n -> a - (a mod n) >= k * n.
intros a k n Hn Hgt.
set (aa := a - k * n).
replace (a) with (aa + k * n) in *; try (subst aa; nom).
rewrite Z_mod_plus_full.
assert (aa - aa mod n >= 0).
assert (Hn' : 0 < n) by nom.
assert (Hgt' : 0 <= aa) by nom.
assert (m0 := Zmod_le aa n Hn' Hgt'); nom.
nom.
Defined.
Lemma mod2 : forall a b c n (Hca : c = a) (Hb : b >= 0) (Hn : n > 0),
(c + ((b - b mod n) - a)) mod n = 0
.
intros.
rewrite Hca in *. clear Hca.
assert (e : (a + ((b - b mod n) - a)) = (b - b mod n)) by nom.
rewrite e. clear e.
rewrite Zminus_mod_idemp_r.
assert (e : b - b = 0) by nom.
rewrite e. clear e.
exact (Zmod_0_l n).
Defined.
Definition consume_into_substring
(con : consumer)
(ofs : Z)
(len : Z)
(w : world)
{Clen : len = con.(Con_to_read)}
{ArgLen : len > 0}
{ArgOfs : con.(Con_ofs) = ofs}
{Fhas : len <= w.(w_buf).(buf_len) + w.(w_buf).(buf_len_to_eof)}
{Cfileofs : con.(Con_file_ofs_from) + con.(Con_ofs)
= w.(w_buf).(buf_arr).(File_ofs)
}
:
{ wc' : world * consumer
| let (w', c') := wc' in
let buf' := w'.(w_buf) in
c'.(Con_to_read) = 0
/\ c'.(Con_ofs) = con.(Con_ofs) + len
/\ c'.(Con_file_ofs_from) = con.(Con_file_ofs_from)
/\ w'.(w_buf).(buf_len_to_eof) >= 0
/\ c'.(Con_file_ofs_from) + c'.(Con_ofs)
= w'.(w_buf).(buf_arr).(File_ofs)
}
.
refine (
let buf := w.(w_buf) in
match Z_le_gt_dec len buf.(buf_len) with
| left le =>
(* len <= buf_len *)
let (wc', wc'pf) :=
blit_from_buffer
w
con
ofs
len
in
exist _ wc' _
| right len_gt_buf_len =>
(* len > buf_len *)
(* offsets are relative to buffer's beginning *)
let enb := buf.(buf_ofs) + buf.(buf_len)
(* end of "what we have in buffer" *) in
let enr := buf.(buf_ofs) + len (* end of "what we want to read" *) in
let enf := enb + buf.(buf_len_to_eof) (* end of "file region we can read" *) in
(* (enr > enb <- len > buf_len) *)
match Z_dec enf enr with
| inleft (left enf_lt_enr) => False_rect _ _
| inright enf_eq_enr =>
(* here: enf = enr => caller reads everything up to file eof. So:
blit all from buffer,
direct_read buf.len_to_eof
*)
let (wc1val, wc1pf) :=
blit_all
w
con
ofs
in
let w1 := fst wc1val in
let c1 := snd wc1val in
let l := w1.(w_buf).(buf_len_to_eof) in
let (wc2val, wc2pf) :=
direct_read
c1
(ofs + buf.(buf_len))
l
w1
in
exist _ wc2val _
| inleft (right enf_gt_enr) =>
(* here: enr < enf => caller reads less than "to eof".
a lot of cases.
*)
match Z_le_gt_dec enf bs2 with
| left enf_le_bs2 =>
(* case I: enf <= bs2 => file till eof fits the buffer:
0 bs bs2
|...............|...............|
^buf_ofs ^enb13 ^enb2 ^enf
^enr3 ^enr12
enf <= bs2 ( -> enf <= bs*3)
enb13 <= bs \/ enb2 > bs
here:
read "enf - enb"
(it's greater than 0, because of
"enr < enf /\ enr > enb"),
blit "len".
possible combinations: (enb13, enr12),
(enb13, enr3), (enb2, enr12).
impossible one: (enb2, enr3).
(naming: common digit => possible,
enb2 >= enr3, so impossible.)
*)
let (w1, w1pf) :=
read_into_buffer
(enf - enb)
w
in
let (wc2val, wc2pf) :=
blit_from_buffer
w1
con
ofs
len
in
exist _ wc2val _
| right enf_gt_bs2 =>
match Z_le_gt_dec enf (bs * 3) with
| left enf_le_bs3 =>
(* here: bs*2 < enf <= bs*3.
cases:
II: enb >= bs: after blitting from buffer
the rest of file fits the buffer.
III: enb < bs: more expensive case: blit_all,
direct_read "enr - enf".
*)
match Z_ge_lt_dec enb bs with
| left enb_ge_bs =>
(* case II:
0 bs bs2 bs*3
|.........|.........|.........|
^buf_ofs ^enb ^enf
^enr1 ^enr2
enf > bs2
enf <= bs*3
enb >= bs
enr1 <= bs2 \/ enr2 > bs2
[bs .. bs2) can be either empty or full, but after
blitting we surely can get rid of [0 .. bs).
here:
blit_all
(buf_ofs' := enb, buf_len' := 0)
move empty buffer to "-bs"
(buf_ofs'' := buf_ofs' - bs, enb'' := buf_ofs'',
enf'' := enf - bs, enr'' := enr - bs)
0 bs bs2
|..........|..........|
^buf_ofs'' ^enf''
^enb'' ^enr2''
^enr1''
read_into_buffer to ofs=buf_ofs'' len=enf''-enb''
(till eof)
blit "enr'' - enb''" to consumer, dest_ofs=ofs+buf_len
*)
let (wc1val, wc1pf) :=
blit_all
w
con
ofs
in
let Case1 := "II/1" in
let w1 := fst wc1val in
let buf_ofs' := enb in
let c1 := snd wc1val in
let (w2, w2pf) :=
move_buffer_on_bs
w1
in
let c2 := c1 in
let buf_ofs'' := buf_ofs' - bs in
let enb'' := buf_ofs'' in
let enf'' := enf - bs in
let enr'' := enr - bs in
let (w3, w3pf) :=
read_into_buffer
(enf'' - enb'')
w2
in
let c3 := c2 in
let (wc4, wc4pf) :=
blit_from_buffer
w3
c3
(ofs + buf.(buf_len))
(enr'' - enb'')
in
exist _ wc4 _
| right enb_lt_bs =>
(* case III:
0 bs bs2 bs*3
|............|............|............|
^buf_ofs ^enb ^enr1 ^enr2 ^enf
enf > bs2
enf <= bs*3
enb < bs ( -> [0 .. bs) has data)
enr1 <= bs2 \/ enr2 > bs2
here:
blit_all
(buf_ofs' := enb, buf_len' := 0)
direct_read "enr - enb" to ofs "ofs + buf_len"
it will move buffer:
0 bs bs2
|.................|................|
^buf_ofs1'' ^enf1''
^buf_ofs2'' ^enf2''
but we don't care.
*)
let (wc1, wc1pf) :=
blit_all
w
con
ofs
in
let w1 := fst wc1 in
let c1 := snd wc1 in
let (wc2, wc2pf) :=
direct_read
c1
(ofs + buf.(buf_len))
(enr - enb)
w1
in
exist _ wc2 _
end
| right enf_gt_bs3 =>
(* here: enf > bs3 *)
match Z_gt_le_dec enr bs2 with
| right enr_le_bs2 =>
(* case IV: enr <= bs2 (enb < enr -> enb < bs2),
enf is far.
0 bs bs2
|........|........|....~~|~~~~|~~....
^enb1 ^enb2 ^enf
^enr1 ^enr12
here:
read_into_buffer "bs2 - enb",
blit "enr - enb".
*)
let (w1, w1pf) :=
read_into_buffer
(bs2 - enb)
w
in
let c1 := con in
let (wc2, wc2pf) :=
blit_from_buffer
w1
c1
ofs
len
in
exist _ wc2 _
| left enr_gt_bs2 =>
(* enr > bs2 *)
let enr_block_begin := enr - (enr mod bs) in
(* cases:
_: enr < enr_block_begin: impossible
V: enr = enr_block_begin: no need to read after enr
VI: enr > enr_block_begin,
enf - enr_block_begin > bs2:
we can't fill the buffer with file contents
till eof during last read, so last read will fill
the whole buffer, "bs2".
VII: enr > enr_block_begin,
enf - enr_block_begin <= bs2 -> we can do it,
last read will be "enf - enr_block_begin",
then blit "enr - enr_block_begin"
In any case we will do first:
blit_all,
direct_read0 "enr_block_begin - enb" to "ofs + buf_len"
*)
let (wc1, wc1pf) :=
blit_all
w
con
ofs
in
let w1 := fst wc1 in
let c1 := snd wc1 in
let enr_ge_bs2 : enr >= bs2 := _ in
let P1 := mod1 _ 2 bs _ enr_ge_bs2 in
let (wc2, wc2pf) :=
direct_read0
c1
(ofs + buf.(buf_len))
(enr_block_begin - enb)
w1
in
let w2 := fst wc2 in
let c2 := snd wc2 in
match Z_dec enr enr_block_begin with
| inleft (left enr_lt_begin) => False_rect _ _
| inright enr_eq_begin =>
(* case V *)
exist _ wc2 _
| inleft (right enr_gt_begin) =>
let dir_align :
(w1.(w_buf).(buf_ofs) +
(buf.(buf_ofs) + len -
(enr mod bs) - (buf.(buf_ofs) + buf.(buf_len)))
) mod bs = 0
:= _ in
let dir_align2 : w2.(w_buf).(buf_ofs) = 0 := _ in
match Z_gt_le_dec (enf - enr_block_begin) bs2 with
| left rest_doesn't_fit =>
(* enf - enr_block_begin > bs2 *)
(* case VI *)
let (w3, w3pf) :=
read_into_buffer
bs2
w2
in
let c3 := c2 in
let (wc4, wc4pf) :=
blit_from_buffer
w3
c3
(ofs + w.(w_buf).(buf_len) + enr_block_begin - enb)
(enr - enr_block_begin)
in
exist _ wc4 _
| right rest_fits =>
(* enf - enr_block_begin <= bs2 *)
(* case VII *)
let (w3, w3pf) :=
read_into_buffer
(enf - enr_block_begin)
w2
in
let c3 := c2 in
let (wc4, wc4pf) :=
blit_from_buffer
w3
c3
(ofs + w.(w_buf).(buf_len) + enr_block_begin - enb)
(enr - enr_block_begin)
in
exist _ wc4 _
end
end
end
end
end
end
end
);
(try unfold bs2, bs in *);
subst_lets;
try nom;
destr_type (world * consumer)%type;
simpl in *; subst_lets; simpl in *; spl; try nom;
destr_type world; simpl in *; subst_lets; simpl in *; try nom;
repeat split; try nom;
destr_type buffer; simpl in *; spl; try nom;
destr_type array; simpl in *; spl; try nom;
(let rec mods :=
match goal with
| H : ?a mod ?b >= 0 |- context [ ?a mod ?b ] => idtac
| |- context [ ?a mod ?b ] =>
let n_modnotneg := fresh "mods_r_ge0" in
let n_anotneg := fresh "mods_a_ge0" in
let n_bpos := fresh "mods_b_gt0" in
assert (n_anotneg : a >= 0) by nom;
assert (n_bpos : b > 0) by nom;
assert (n_modnotneg := mod_on_notneg a b n_anotneg n_bpos);
assert (n_modlt := mod_lt a b n_anotneg n_bpos);
mods
| _ => idtac
end
in
mods
);
unfold bs2, bs in *;
try refine (mod2 _ _ _ _ _ _ _);
try nom;
(match goal with
| |- context [Z_gt_le_dec ?a ?b] => destruct (Z_gt_le_dec a b)
| _ => idtac
end
);
try nom;
destr_type consumer; simpl in *; spl; try nom;
idtac
.
Defined.
Definition consume_string
(len : Z)
(w : world)
{ArgLen : len > 0}
{Fhas : len <= w.(w_buf).(buf_len) + w.(w_buf).(buf_len_to_eof)}
:
{ wc' : world * consumer
| let (w', c') := wc' in
let buf' := w'.(w_buf) in
c'.(Con_to_read) = 0
/\ c'.(Con_ofs) = len
/\ w'.(w_buf).(buf_len_to_eof) >= 0
/\ c'.(Con_file_ofs_from) + c'.(Con_ofs)
= w'.(w_buf).(buf_arr).(File_ofs)
}
.
refine (
let buf := w.(w_buf) in
let Cto_read0 : len >= 0 := _ in
let Cofs0 : 0 >= 0 := _ in
let con :=
{| Con_to_read := len
; Con_ofs := 0
; Con_file_ofs_from := buf.(buf_arr).(File_ofs)
; Cto_read := Cto_read0
; Cofs := Cofs0
|}
in
match Z_le_gt_dec len buf.(buf_len) with
| left le =>
(* here in OCaml code will be "String.sub", that's why we are proving
this case separately, outside of "consume_into_substring"
*)
let (wc', wc'sig) :=
blit_from_buffer
w
con
0
len
in
exist _ wc' _
| right gt =>
let (wc', wc'sig) :=
consume_into_substring
con
0
len
w
in
exist _ wc' _
end
); try subst buf; simpl in *; try nom; destr_type (world * consumer)%type;
simpl in *; spl; simpl in *; repeat split; try nom;
destr_type world; destr_type buffer; spl; simpl in *; nom.
Defined.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment