module Lib.Sequence.Lemmas
open FStar.Mul
open Lib.IntTypes
open Lib.Sequence
// This is unnecessary because the same pragma is interleaved from the interface
#set-options "--z3rlimit 100 --max_fuel 0 --max_ifuel 0 \
--using_facts_from '-* +Prims +Lib.Sequence.Lemmas +Lib.Sequence +FStar.Seq'"
val lemma_map_blocks_vec_i:
#a:Type
-> w:size_pos
-> blocksize:size_pos{w * blocksize <= max_size_t}
-> inp:seq a
-> f:(block (length inp) blocksize -> lseq a blocksize -> lseq a blocksize)
-> g:(last (length inp) blocksize -> rem:size_nat{rem < blocksize} -> lseq a rem -> lseq a rem)
-> f_v:(block (length inp) (w * blocksize) -> lseq a (w * blocksize) -> lseq a (w * blocksize))
-> g_v:(last (length inp) (w * blocksize) -> rem:size_nat{rem < w * blocksize} -> lseq a rem -> lseq a rem)
-> pre:squash (forall (i:nat{i < length inp}). map_blocks_vec_equiv_pre w blocksize inp f g f_v g_v i)
-> i:nat{i < length inp} ->
Lemma (
let s = map_blocks blocksize inp f g in
let v = map_blocks (w * blocksize) inp f_v g_v in
Seq.index v i == Seq.index s i
)
let lemma_map_blocks_vec_i #a w blocksize inp f g f_v g_v pre i =
let len = length inp in
let blocksize_v = w * blocksize in
index_map_blocks blocksize inp f g i;
index_map_blocks blocksize_v inp f_v g_v i;
let s = map_blocks blocksize inp f g in
let v = map_blocks (w * blocksize) inp f_v g_v in
if i < (len / blocksize) * blocksize then
div_mul_lt blocksize i (len / blocksize)
else
begin
div_interval blocksize (len / blocksize) i;
div_mul_l i len w blocksize;
mod_interval_lt blocksize_v (i / blocksize_v) i len
end
let lemma_map_blocks_vec #a w blocksize inp f g f_v g_v =
Classical.forall_intro (lemma_map_blocks_vec_i w blocksize inp f g f_v g_v ())
#reset-options "--z3rlimit 50 --max_fuel 0 --max_ifuel 0"
let rec repeati_extensionality #a n f g acc0 =
if n = 0 then begin
Loops.eq_repeati0 n f acc0;
Loops.eq_repeati0 n g acc0 end
else begin
Loops.unfold_repeati n f acc0 (n-1);
Loops.unfold_repeati n g acc0 (n-1);
repeati_extensionality #a (n-1) f g acc0 end
let rec repeati_right_extensionality #a n lo_g hi_g f g acc0 =
if n = 0 then begin
Loops.eq_repeat_right 0 n (Loops.fixed_a a) f acc0;
Loops.eq_repeat_right lo_g (lo_g+n) (Loops.fixed_a a) g acc0 end
else begin
Loops.unfold_repeat_right 0 n (Loops.fixed_a a) f acc0 (n-1);
Loops.unfold_repeat_right lo_g (lo_g+n) (Loops.fixed_a a) g acc0 (lo_g+n-1);
repeati_right_extensionality #a (n-1) lo_g hi_g f g acc0 end
val aux_repeat_bf_s0:
#a:Type0
-> #b:Type0
-> blocksize:size_pos
-> len0:nat{len0 % blocksize = 0}
-> inp:seq a{len0 <= length inp}
-> f:(lseq a blocksize -> b -> b)
-> i:nat{i < len0 / blocksize}
-> acc:b ->
Lemma
(let len = length inp in
FStar.Math.Lemmas.lemma_div_le len0 len blocksize;
let repeat_bf_s0 = repeat_blocks_f blocksize (Seq.slice inp 0 len0) f (len0 / blocksize) in
let repeat_bf_t = repeat_blocks_f blocksize inp f (len / blocksize) in
repeat_bf_s0 i acc == repeat_bf_t i acc)
let aux_repeat_bf_s0 #a #b blocksize len0 inp f i acc =
let len = length inp in
FStar.Math.Lemmas.lemma_div_le len0 len blocksize;
let repeat_bf_s0 = repeat_blocks_f blocksize (Seq.slice inp 0 len0) f (len0 / blocksize) in
let repeat_bf_t = repeat_blocks_f blocksize inp f (len / blocksize) in
let nb = len0 / blocksize in
assert ((i + 1) * blocksize <= nb * blocksize);
let block = Seq.slice inp (i * blocksize) (i * blocksize + blocksize) in
assert (repeat_bf_s0 i acc == f block acc);
assert (repeat_bf_t i acc == f block acc)
#restart-solver
val lemma_aux: blocksize:pos -> len:nat -> len0:nat ->
Lemma
(requires len0 <= len /\ len0 % blocksize == 0)
(ensures len0 / blocksize + (len - len0) / blocksize == len / blocksize)
let lemma_aux bs len len0 =
calc (==) {
len0 / bs + (len - len0) / bs;
== { FStar.Math.Lemmas.lemma_div_exact len0 bs }
len0 / bs + (len - len0 / bs * bs) / bs;
== { FStar.Math.Lemmas.lemma_div_plus len (- len0 / bs) bs }
len0 / bs + len / bs - len0 / bs;
== { }
len / bs;
}
val lemma_aux2: blocksize:pos -> len:nat -> len0:nat -> i:nat ->
Lemma
(requires len0 <= len /\ len0 % blocksize == 0 /\ i < (len - len0) / blocksize)
(ensures len0 + i * blocksize + blocksize <= len)
let lemma_aux2 blocksize len len0 i =
let len1 = len - len0 in
FStar.Math.Lemmas.lemma_mult_le_right blocksize (i + 1) (len1 / blocksize);
assert (len0 + (i + 1) * blocksize <= len0 + len1 / blocksize * blocksize);
FStar.Math.Lemmas.multiply_fractions len blocksize;
assert (len1 / blocksize * blocksize <= len1);
assert (len0 + (i + 1) * blocksize <= len)
val lemma_aux3: blocksize:pos -> len:nat -> len0:nat -> i:nat ->
Lemma
(requires len0 <= len /\ len0 % blocksize == 0 /\ i < (len - len0) / blocksize)
(ensures (len0 / blocksize + i) * blocksize == len0 + i * blocksize)
let lemma_aux3 blocksize len len0 i =
calc (==) {
(len0 / blocksize + i) * blocksize;
(==) { FStar.Math.Lemmas.distributivity_add_left (len0 / blocksize) i blocksize }
len0 / blocksize * blocksize + i * blocksize;
(==) { FStar.Math.Lemmas.lemma_div_exact len0 blocksize }
len0 + i * blocksize;
}
val aux_repeat_bf_s1:
#a:Type0
-> #b:Type0
-> blocksize:size_pos
-> len0:nat{len0 % blocksize = 0}
-> inp:seq a{len0 <= length inp}
-> f:(lseq a blocksize -> b -> b)
-> i:nat{i < (length inp - len0) / blocksize}
-> acc:b ->
Lemma
(let len = length inp in
let len1 = len - len0 in
FStar.Math.Lemmas.lemma_div_le len0 len blocksize;
FStar.Math.Lemmas.lemma_div_le len1 len blocksize;
let t1 = Seq.slice inp len0 len in
let repeat_bf_s1 = repeat_blocks_f blocksize t1 f (len1 / blocksize) in
let repeat_bf_t = repeat_blocks_f blocksize inp f (len / blocksize) in
lemma_aux blocksize len len0;
repeat_bf_s1 i acc == repeat_bf_t (len0 / blocksize + i) acc)
let aux_repeat_bf_s1 #a #b blocksize len0 inp f i acc =
let len = length inp in
let len1 = len - len0 in
FStar.Math.Lemmas.lemma_div_le len0 len blocksize;
FStar.Math.Lemmas.lemma_div_le len1 len blocksize;
let t1 = Seq.slice inp len0 len in
let repeat_bf_s1 = repeat_blocks_f blocksize t1 f (len1 / blocksize) in
let repeat_bf_t = repeat_blocks_f blocksize inp f (len / blocksize) in
let i_start = len0 / blocksize in
let nb = len1 / blocksize in
lemma_aux blocksize len len0;
assert (i_start + nb = len / blocksize);
lemma_aux2 blocksize len len0 i;
let block = Seq.slice inp ((len0 / blocksize + i) * blocksize) ((len0 / blocksize + i) * blocksize + blocksize) in
lemma_aux3 blocksize len len0 i;
assert (block == Seq.slice inp (len0 + i * blocksize) (len0 + i * blocksize + blocksize));
assert (repeat_bf_t (len0 / blocksize + i) acc == f block acc);
//FStar.Math.Lemmas.lemma_mult_le_right blocksize (i + 1) (len1 / blocksize);
//assert (i * blocksize + blocksize <= len1);
assert (repeat_bf_s1 i acc == f (Seq.slice t1 (i * blocksize) (i * blocksize + blocksize)) acc);
//assert (len0 + (i + 1) * blocksize <= len);
FStar.Seq.Properties.slice_slice inp len0 len (i * blocksize) (i * blocksize + blocksize);
assert (repeat_bf_s1 i acc == f block acc)
val repeat_blocks_split12:
#a:Type0
-> #b:Type0
-> blocksize:size_pos
-> len0:nat{len0 % blocksize = 0}
-> inp:seq a{len0 <= length inp}
-> f:(lseq a blocksize -> b -> b)
-> acc0:b ->
Lemma
(let len = length inp in
let len1 = len - len0 in
FStar.Math.Lemmas.lemma_div_le len0 len blocksize;
FStar.Math.Lemmas.lemma_div_le len1 len blocksize;
let repeat_bf_s0 = repeat_blocks_f blocksize (Seq.slice inp 0 len0) f (len0 / blocksize) in
let repeat_bf_s1 = repeat_blocks_f blocksize (Seq.slice inp len0 len) f (len1 / blocksize) in
let repeat_bf_t = repeat_blocks_f blocksize inp f (len / blocksize) in
let acc1 = Loops.repeati (len0 / blocksize) repeat_bf_s0 acc0 in
Loops.repeati (len1 / blocksize) repeat_bf_s1 acc1 ==
Loops.repeati (len / blocksize) repeat_bf_t acc0)
let repeat_blocks_split12 #a #b blocksize len0 inp f acc0 =
let len = length inp in
let len1 = len - len0 in
FStar.Math.Lemmas.lemma_div_le len0 len blocksize;
FStar.Math.Lemmas.lemma_div_le len1 len blocksize;
let repeat_bf_s0 = repeat_blocks_f blocksize (Seq.slice inp 0 len0) f (len0 / blocksize) in
let repeat_bf_s1 = repeat_blocks_f blocksize (Seq.slice inp len0 len) f (len1 / blocksize) in
let repeat_bf_t = repeat_blocks_f blocksize inp f (len / blocksize) in
let acc1 = Loops.repeati (len0 / blocksize) repeat_bf_s0 acc0 in
calc (==) {
Loops.repeati (len0 / blocksize) repeat_bf_s0 acc0;
== { FStar.Classical.forall_intro_2 (aux_repeat_bf_s0 #a #b blocksize len0 inp f);
repeati_extensionality (len0 / blocksize) repeat_bf_s0 repeat_bf_t acc0 }
Loops.repeati (len0 / blocksize) repeat_bf_t acc0;
== { Loops.repeati_def (len0 / blocksize) repeat_bf_t acc0 }
Loops.repeat_right 0 (len0 / blocksize) (Loops.fixed_a b) repeat_bf_t acc0;
};
let i_start = len0 / blocksize in
let nb = len1 / blocksize in
lemma_aux blocksize len len0;
assert (i_start + nb = len / blocksize);
let acc3 = Loops.repeati (len1 / blocksize) repeat_bf_s1 acc1 in
calc (==) {
Loops.repeati (len1 / blocksize) repeat_bf_s1 acc1;
== { Loops.repeati_def (len1 / blocksize) repeat_bf_s1 acc1 }
Loops.repeat_right 0 nb (Loops.fixed_a b) repeat_bf_s1 acc1;
== { FStar.Classical.forall_intro_2 (aux_repeat_bf_s1 #a #b blocksize len0 inp f);
repeati_right_extensionality nb i_start (nb+i_start) repeat_bf_s1 repeat_bf_t acc1 }
Loops.repeat_right i_start (i_start+nb) (Loops.fixed_a b) repeat_bf_t acc1;
== { }
Loops.repeat_right (len0 / blocksize) (len / blocksize) (Loops.fixed_a b) repeat_bf_t acc1;
== { Loops.repeat_right_plus 0 (len0 / blocksize) (len / blocksize) (Loops.fixed_a b) repeat_bf_t acc0 }
Loops.repeat_right 0 (len / blocksize) (Loops.fixed_a b) repeat_bf_t acc0;
== { Loops.repeati_def (len / blocksize) repeat_bf_t acc0 }
Loops.repeati (len / blocksize) repeat_bf_t acc0;
}
#reset-options "--z3rlimit 200 --max_fuel 1 --max_ifuel 1"
val lemma_aux4: blocksize:pos -> len:nat -> len0:nat ->
Lemma
(requires len0 <= len /\ len0 % blocksize == 0)
(ensures len0 + (len - len0) / blocksize * blocksize == len / blocksize * blocksize)
let lemma_aux4 bs len len0 =
calc (==) {
len0 + (len - len0) / bs * bs;
== { FStar.Math.Lemmas.lemma_div_exact len0 bs }
len0 + (len - len0 / bs * bs) / bs * bs;
== { FStar.Math.Lemmas.lemma_div_plus len (- len0 / bs) bs }
len0 + (len / bs - len0 / bs) * bs;
== { FStar.Math.Lemmas.distributivity_sub_left (len / bs) (len0 / bs) bs }
len0 + len / bs * bs - len0 / bs * bs;
== { FStar.Math.Lemmas.lemma_div_exact len0 bs }
len0 + len / bs * bs - len0;
== { }
len / bs * bs;
}
let repeat_blocks_multi_split #a #b blocksize len0 inp f acc0 =
let len = length inp in
let len1 = len - len0 in
FStar.Math.Lemmas.modulo_addition_lemma len blocksize (- len0 / blocksize);
assert (len % blocksize == len1 % blocksize);
let t0 = Seq.slice inp 0 len0 in
let t1 = Seq.slice inp len0 len in
FStar.Math.Lemmas.lemma_div_le len0 len blocksize;
FStar.Math.Lemmas.lemma_div_le len1 len blocksize;
let repeat_bf_s0 = repeat_blocks_f blocksize t0 f (len0 / blocksize) in
let repeat_bf_s1 = repeat_blocks_f blocksize t1 f (len1 / blocksize) in
let repeat_bf_t = repeat_blocks_f blocksize inp f (len / blocksize) in
let acc1 = repeat_blocks_multi blocksize t0 f acc0 in
let acc2 = repeat_blocks_multi blocksize t1 f acc1 in
calc (==) {
repeat_blocks_multi blocksize t1 f acc1;
(==) { lemma_repeat_blocks_multi blocksize t1 f acc1 }
Loops.repeati (len1 / blocksize) repeat_bf_s1 acc1;
(==) { lemma_repeat_blocks_multi blocksize t0 f acc0 }
Loops.repeati (len1 / blocksize) repeat_bf_s1 (Loops.repeati (len0 / blocksize) repeat_bf_s0 acc0);
(==) { repeat_blocks_split12 blocksize len0 inp f acc0 }
Loops.repeati (len / blocksize) repeat_bf_t acc0;
(==) { lemma_repeat_blocks_multi blocksize inp f acc0 }
repeat_blocks_multi blocksize inp f acc0;
};
assert (repeat_blocks_multi blocksize t1 f acc1 == repeat_blocks_multi blocksize inp f acc0)
#set-options "--z3rlimit 150 --initial_ifuel 1 --max_ifuel 1"
#restart-solver
let repeat_blocks_split #a #b blocksize len0 inp f l acc0 =
let len = length inp in
let len1 = len - len0 in
FStar.Math.Lemmas.modulo_addition_lemma len blocksize (- len0 / blocksize);
assert (len % blocksize == len1 % blocksize);
let t0 = Seq.slice inp 0 len0 in
let t1 = Seq.slice inp len0 len in
FStar.Math.Lemmas.lemma_div_le len0 len blocksize;
FStar.Math.Lemmas.lemma_div_le len1 len blocksize;
let repeat_bf_s0 = repeat_blocks_f blocksize t0 f (len0 / blocksize) in
let repeat_bf_s1 = repeat_blocks_f blocksize t1 f (len1 / blocksize) in
let repeat_bf_t = repeat_blocks_f blocksize inp f (len / blocksize) in
let acc1 = repeat_blocks_multi blocksize t0 f acc0 in
let acc2 = repeat_blocks blocksize t1 f l acc1 in
let acc3 = Loops.repeati (len1 / blocksize) repeat_bf_s1 acc1 in
calc (==) {
repeat_blocks blocksize t1 f l acc1;
(==) { lemma_repeat_blocks blocksize t1 f l acc1 }
l (len1 % blocksize) (Seq.slice t1 (len1 / blocksize * blocksize) len1) acc3;
(==) { FStar.Math.Lemmas.modulo_addition_lemma len blocksize (- len0 / blocksize) }
l (len % blocksize) (Seq.slice (Seq.slice inp len0 len) (len1 / blocksize * blocksize) len1) acc3;
(==) { lemma_aux4 blocksize len len0; FStar.Seq.Properties.slice_slice inp len0 len (len1 / blocksize * blocksize) len1 }
l (len % blocksize) (Seq.slice inp (len / blocksize * blocksize) len) acc3;
(==) { lemma_repeat_blocks_multi blocksize t0 f acc0 }
l (len % blocksize) (Seq.slice inp (len / blocksize * blocksize) len)
(Loops.repeati (len1 / blocksize) repeat_bf_s1 (Loops.repeati (len0 / blocksize) repeat_bf_s0 acc0));
(==) { repeat_blocks_split12 blocksize len0 inp f acc0 }
l (len % blocksize) (Seq.slice inp (len / blocksize * blocksize) len) (Loops.repeati (len / blocksize) repeat_bf_t acc0);
(==) { lemma_repeat_blocks blocksize inp f l acc0 }
repeat_blocks blocksize inp f l acc0;
};
assert (repeat_blocks blocksize t1 f l acc1 == repeat_blocks blocksize inp f l acc0)
let unfold_repeatw #a w n f acc =
match w with
| 1 ->
Loops.unfold_repeati n f acc (n-1)
| 2 ->
Loops.unfold_repeati (2*n) f acc (2*n-2);
Loops.unfold_repeati (2*n) f acc (2*n-1)
| 4 ->
Loops.unfold_repeati (4*n) f acc (4*n-4);
Loops.unfold_repeati (4*n) f acc (4*n-3);
Loops.unfold_repeati (4*n) f acc (4*n-2);
Loops.unfold_repeati (4*n) f acc (4*n-1)
let rec lemma_repeati_vec #a #a_vec w n normalize_n f f_vec acc0_vec =
if n = 0 then begin
Loops.eq_repeati0 n f_vec acc0_vec;
Loops.eq_repeati0 (w * n) f (normalize_n acc0_vec) end
else begin
let acc0 = normalize_n acc0_vec in
lemma_repeati_vec #a #a_vec w (n-1) normalize_n f f_vec acc0_vec;
let next_p = Loops.repeati (n-1) f_vec acc0_vec in
let next_v = Loops.repeati (w*(n-1)) f acc0 in
assert (normalize_n next_p == next_v);
let res1 = Loops.repeati n f_vec acc0_vec in
let res2 = Loops.repeati (w*n) f acc0 in
Loops.unfold_repeati n f_vec acc0_vec (n-1);
assert (res1 == f_vec (n-1) next_p);
unfold_repeatw w n f acc0;
assert (res2 == repeat_w w n f (n-1) next_v);
assert (normalize_n res1 == res2)
end
#reset-options "--z3refresh --z3rlimit 300 --max_fuel 0 --max_ifuel 0"
val lemma_repeat_blocks_multi_load_acc:
#a:Type0
-> #b:Type0
-> #b_vec:Type0
-> w:lanes
-> blocksize:size_pos{w * blocksize <= max_size_t}
-> inp:seq a{w * blocksize <= length inp /\ length inp % (w * blocksize) = 0 /\ length inp % blocksize = 0}
-> f:(lseq a blocksize -> b -> b)
-> normalize_n:(b_vec -> b)
-> load_acc:(lseq a (w * blocksize) -> b -> b_vec)
-> acc0:b ->
Lemma
(requires
(let len0 = w * blocksize in
let t0 = Seq.slice inp 0 len0 in
let repeat_bf_t0 = repeat_blocks_f blocksize t0 f w in
normalize_n (load_acc t0 acc0) == repeat_w #b w 1 repeat_bf_t0 0 acc0))
(ensures
(let len0 = w * blocksize in
let t0 = Seq.slice inp 0 len0 in
normalize_n (load_acc t0 acc0) == repeat_blocks_multi #a #b blocksize t0 f acc0))
let lemma_repeat_blocks_multi_load_acc #a #b #b_vec w blocksize inp f normalize_n load_acc acc0 =
let len0 = w * blocksize in
let t0 = Seq.slice inp 0 len0 in
let repeat_bf_t0 = repeat_blocks_f blocksize t0 f w in
let acc1 = load_acc t0 acc0 in
calc (==) {
normalize_n acc1;
(==) { }
repeat_w #b w 1 repeat_bf_t0 0 acc0;
(==) { unfold_repeatw #b w 1 repeat_bf_t0 acc0; Loops.eq_repeati0 1 repeat_bf_t0 acc0 }
Loops.repeati w repeat_bf_t0 acc0;
(==) { lemma_repeat_blocks_multi #a #b blocksize t0 f acc0 }
repeat_blocks_multi #a #b blocksize t0 f acc0;
};
assert (normalize_n acc1 == repeat_blocks_multi #a #b blocksize t0 f acc0)
let lemma_aux1 w blocksize len =
let sb = w * blocksize in
let len1 = len - w * blocksize in
FStar.Math.Lemmas.modulo_addition_lemma len sb (- 1);
assert (len % sb == len1 % sb);
calc (==) {
len1 / blocksize;
(==) { FStar.Math.Lemmas.lemma_div_exact len1 sb }
(len1 / sb * sb) / blocksize;
(==) { FStar.Math.Lemmas.paren_mul_right (len1 / sb) w sb }
((len1 / sb * w) * blocksize) / blocksize;
(==) { FStar.Math.Lemmas.multiple_division_lemma (len1 / sb * w) blocksize }
len1 / sb * w;
(==) { FStar.Math.Lemmas.swap_mul (len1 / sb) w}
w * (len1 / sb);
};
assert (len1 / blocksize == w * (len1 / sb))
#set-options "--z3rlimit 300 --z3seed 1"
let lemma_repeat_blocks_multi_vec #a #b #b_vec w blocksize inp f f_vec normalize_n load_acc acc0 =
let len = length inp in
let len0 = w * blocksize in
let len1 = len - len0 in
FStar.Math.Lemmas.modulo_addition_lemma len len0 (- 1);
assert (len % len0 == len1 % len0);
FStar.Math.Lemmas.modulo_addition_lemma len blocksize (- w);
assert (len % blocksize == len1 % blocksize);
let t0 = Seq.slice inp 0 len0 in
let t1 = Seq.slice inp len0 len in
let nb_vec = len1 / (w * blocksize) in
let nb = len1 / blocksize in
lemma_aux1 w blocksize len;
assert (nb == w * nb_vec);
let repeat_bf_vec = repeat_blocks_f (w * blocksize) t1 f_vec nb_vec in
let repeat_bf_t0 = repeat_blocks_f blocksize t0 f w in
let repeat_bf_t1 = repeat_blocks_f blocksize t1 f nb in
let acc1 = load_acc t0 acc0 in
calc (==) {
normalize_n (repeat_blocks_multi (w * blocksize) t1 f_vec acc1);
(==) { lemma_repeat_blocks_multi (w * blocksize) t1 f_vec acc1 }
normalize_n (Loops.repeati nb_vec repeat_bf_vec acc1);
(==) { lemma_repeati_vec w nb_vec normalize_n repeat_bf_t1 repeat_bf_vec acc1 }
Loops.repeati nb repeat_bf_t1 (normalize_n acc1);
(==) { lemma_repeat_blocks_multi blocksize t1 f (normalize_n acc1) }
repeat_blocks_multi blocksize t1 f (normalize_n acc1);
(==) { lemma_repeat_blocks_multi_load_acc #a #b #b_vec w blocksize inp f normalize_n load_acc acc0 }
repeat_blocks_multi blocksize t1 f (repeat_blocks_multi #a #b blocksize t0 f acc0);
(==) { repeat_blocks_multi_split blocksize len0 inp f acc0 }
repeat_blocks_multi blocksize inp f acc0;
}