val get_block_v:
    #a:Type0
  -> w:pos
  -> blocksize:pos{w * blocksize <= max_size_t}
  -> n:nat
  -> s:seq a{length s = w * n * blocksize}
  -> i:nat{i < n} ->
  lseq a (w * blocksize)
let get_block_v #a w blocksize n s i =
  let blocksize_v = w * blocksize in
  Math.Lemmas.lemma_mult_le_right blocksize_v (i + 1) n;
  Math.Lemmas.paren_mul_right n w blocksize;
  let b_v = Seq.slice s (i * blocksize_v) ((i + 1) * blocksize_v) in
  b_v
val get_block_v:
    #a:Type0
  -> w:pos
  -> blocksize:pos{w * blocksize <= max_size_t}
  -> n:nat
  -> s:seq a{length s = w * n * blocksize}
  -> i:nat{i < n} ->
  lseq a (w * blocksize)
let get_block_v #a w blocksize n s i =
let blocksize_v = w * blocksize in
Math.Lemmas.lemma_mult_le_right blocksize_v (i + 1) n;
Math.Lemmas.paren_mul_right n w blocksize;
let b_v = Seq.slice s (i * blocksize_v) ((i + 1) * blocksize_v) in
b_v
Lib.Vec.Lemmas.fst.checked
prims.fst.checked FStar.Seq.Properties.fsti.checked FStar.Seq.Base.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Math.Lemmas.fst.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
Lib.Vec.Lemmas.fst
Prims.pos Prims.b2t Prims.op_LessThanOrEqual FStar.Mul.op_Star Lib.IntTypes.max_size_t Prims.nat Lib.Sequence.seq Prims.op_Equality Prims.int Lib.Sequence.length Prims.op_LessThan FStar.Seq.Base.seq FStar.Seq.Base.slice Prims.op_Addition Prims.unit FStar.Math.Lemmas.paren_mul_right FStar.Math.Lemmas.lemma_mult_le_right Lib.Sequence.lseq
module Lib.Vec.Lemmas

#set-options ""
#push-options "--z3rlimit 30 --max_fuel 0 --max_ifuel 0 \
  --using_facts_from '-* +Prims +FStar.Pervasives +FStar.Math.Lemmas +FStar.Seq -FStar.Seq.Properties.slice_slice \
    +Lib.IntTypes +Lib.Sequence +Lib.Sequence.Lemmas +Lib.LoopCombinators +Lib.Vec.Lemmas'"


let rec lemma_repeat_gen_vec w n a a_vec normalize_v f f_v acc_v0 =
  if n = 0 then begin
    Loops.eq_repeat_right 0 n a_vec f_v acc_v0;
    Loops.eq_repeat_right 0 (w * n) a f (normalize_v 0 acc_v0) end
  else begin
    let next_p = Loops.repeat_right 0 (n - 1) a_vec f_v acc_v0 in
    let next_v = Loops.repeat_right 0 (w * (n - 1)) a f (normalize_v 0 acc_v0) in

    calc (==) {
      Loops.repeat_right 0 (w * n) a f (normalize_v 0 acc_v0);
      (==) { Loops.repeat_right_plus 0 (w * (n - 1)) (w * n) a f (normalize_v 0 acc_v0) }
      Loops.repeat_right (w * (n - 1)) (w * n) a f next_v;
      (==) { lemma_repeat_gen_vec w (n - 1) a a_vec normalize_v f f_v acc_v0 }
      Loops.repeat_right (w * (n - 1)) (w * n) a f (normalize_v (n - 1) next_p);
      (==) { }
      normalize_v n (f_v (n - 1) next_p);
      (==) { Loops.unfold_repeat_right 0 n a_vec f_v acc_v0 (n - 1) }
      normalize_v n (Loops.repeat_right 0 n a_vec f_v acc_v0);
    } end


let lemma_repeati_vec #a #a_vec w n normalize_v f f_v acc_v0 =
  lemma_repeat_gen_vec w n (Loops.fixed_a a) (Loops.fixed_a a_vec) (Loops.fixed_i normalize_v) f f_v acc_v0;
  Loops.repeati_def n f_v acc_v0;
  Loops.repeati_def (w * n) f (normalize_v acc_v0)


let len_is_w_n_blocksize w blocksize n =
  let len = w * n * blocksize in
  Math.Lemmas.cancel_mul_mod (w * n) blocksize;
  //assert (len % blocksize = 0);
  Math.Lemmas.cancel_mul_div (w * n) blocksize;
  //assert (len / blocksize = w * n);

  Math.Lemmas.paren_mul_right n w blocksize;
  Math.Lemmas.cancel_mul_mod n (w * blocksize);
  Math.Lemmas.cancel_mul_div n (w * blocksize)


////////////////////////
// Start of proof of lemma_repeat_gen_blocks_multi_vec
////////////////////////

val get_block_v:
    #a:Type0
  -> w:pos
  -> blocksize:pos{w * blocksize <= max_size_t}
  -> n:nat
  -> s:seq a{length s = w * n * blocksize}
  -> i:nat{i < n} ->
  lseq a (w * blocksize)
val get_block_v:
    #a:Type0
  -> w:pos
  -> blocksize:pos{w * blocksize <= max_size_t}
  -> n:nat
  -> s:seq a{length s = w * n * blocksize}
  -> i:nat{i < n} ->
  lseq a (w * blocksize)

    w: Prims.pos ->
    blocksize: Prims.pos{w * blocksize <= Lib.IntTypes.max_size_t} ->
    n: Prims.nat ->
    s: Lib.Sequence.seq a {Lib.Sequence.length s = (w * n) * blocksize} ->
    i: Prims.nat{i < n}
  -> Lib.Sequence.lseq a (w * blocksize)