val lemma_map_blocks_multi_vec_equiv_pre_k:
    #a:Type
  -> w:pos
  -> blocksize:pos{w * blocksize <= max_size_t}
  -> n:nat
  -> hi_f:nat{w * n <= hi_f}
  -> f:(i:nat{i < hi_f} -> lseq a blocksize -> lseq a blocksize)
  -> f_v:(i:nat{i < n} -> lseq a (w * blocksize) -> lseq a (w * blocksize))
  -> i:nat{i < n}
  -> b_v:lseq a (w * blocksize)
  -> pre:squash (forall (k:nat{k < w * blocksize}). map_blocks_multi_vec_equiv_pre_k w blocksize n (w * n) f f_v i b_v k)
  -> acc_v:map_blocks_a a (w * blocksize) n i ->
  Lemma (map_blocks_multi_vec_equiv_pre #a w blocksize n hi_f f f_v i b_v acc_v)
let lemma_map_blocks_multi_vec_equiv_pre_k #a w blocksize n hi_f f f_v i b_v pre acc_v =
  //let lp = repeat_gen_blocks_map_f #a (w * blocksize) n f_v i b_v acc_v in
  //assert (lp == Seq.append acc_v (f_v i b_v));

  Math.Lemmas.lemma_mult_le_right w (i + 1) n;
  let f_sh = f_shift blocksize (w * i) hi_f w f in

  let aux (k:nat{k < w * blocksize}) : Lemma (Seq.index (f_v i b_v) k == Seq.index (map_blocks_multi blocksize w w b_v f_sh) k) =
    Math.Lemmas.cancel_mul_div w blocksize;
    let block = get_block_s #a #(w * blocksize) blocksize b_v k in
    let j = k / blocksize in // j < w
    div_mul_lt blocksize k w;

    calc (==) {
      Seq.index (map_blocks_multi blocksize w w b_v f_sh) k;
      (==) { index_map_blocks_multi blocksize w w b_v f_sh k }
      Seq.index (f_sh j block) (k % blocksize);
      (==) { assert (map_blocks_multi_vec_equiv_pre_k w blocksize n hi_f f f_v i b_v k) }
      Seq.index (f_v i b_v) k;
    } in

  calc (==) {
    map_blocks_multi_acc blocksize (w * i) hi_f w b_v f acc_v;
    (==) { map_blocks_multi_acc_is_map_blocks_multi blocksize (w * i) hi_f w b_v f acc_v }
    Seq.append acc_v (map_blocks_multi blocksize w w b_v f_sh);
    (==) { Classical.forall_intro aux; Seq.lemma_eq_intro (f_v i b_v) (map_blocks_multi blocksize w w b_v f_sh) }
    Seq.append acc_v (f_v i b_v);
    (==) { Seq.lemma_eq_intro (Seq.append acc_v (f_v i b_v)) (repeat_gen_blocks_map_f #a (w * blocksize) n f_v i b_v acc_v) }
    repeat_gen_blocks_map_f #a (w * blocksize) n f_v i b_v acc_v;
    }
val lemma_map_blocks_multi_vec_equiv_pre_k:
    #a:Type
  -> w:pos
  -> blocksize:pos{w * blocksize <= max_size_t}
  -> n:nat
  -> hi_f:nat{w * n <= hi_f}
  -> f:(i:nat{i < hi_f} -> lseq a blocksize -> lseq a blocksize)
  -> f_v:(i:nat{i < n} -> lseq a (w * blocksize) -> lseq a (w * blocksize))
  -> i:nat{i < n}
  -> b_v:lseq a (w * blocksize)
  -> pre:squash (forall (k:nat{k < w * blocksize}). map_blocks_multi_vec_equiv_pre_k w blocksize n (w * n) f f_v i b_v k)
  -> acc_v:map_blocks_a a (w * blocksize) n i ->
  Lemma (map_blocks_multi_vec_equiv_pre #a w blocksize n hi_f f f_v i b_v acc_v)
let lemma_map_blocks_multi_vec_equiv_pre_k #a w blocksize n hi_f f f_v i b_v pre acc_v =
Math.Lemmas.lemma_mult_le_right w (i + 1) n;
let f_sh = f_shift blocksize (w * i) hi_f w f in
let aux (k: nat{k < w * blocksize})
    : Lemma (Seq.index (f_v i b_v) k == Seq.index (map_blocks_multi blocksize w w b_v f_sh) k) =
  Math.Lemmas.cancel_mul_div w blocksize;
  let block = get_block_s #a #(w * blocksize) blocksize b_v k in
  let j = k / blocksize in
  div_mul_lt blocksize k w;
  calc ( == ) {
    Seq.index (map_blocks_multi blocksize w w b_v f_sh) k;
    ( == ) { index_map_blocks_multi blocksize w w b_v f_sh k }
    Seq.index (f_sh j block) (k % blocksize);
    ( == ) { assert (map_blocks_multi_vec_equiv_pre_k w blocksize n hi_f f f_v i b_v k) }
    Seq.index (f_v i b_v) k;
  }
in
calc ( == ) {
  map_blocks_multi_acc blocksize (w * i) hi_f w b_v f acc_v;
  ( == ) { map_blocks_multi_acc_is_map_blocks_multi blocksize (w * i) hi_f w b_v f acc_v }
  Seq.append acc_v (map_blocks_multi blocksize w w b_v f_sh);
  ( == ) { (Classical.forall_intro aux;
    Seq.lemma_eq_intro (f_v i b_v) (map_blocks_multi blocksize w w b_v f_sh)) }
  Seq.append acc_v (f_v i b_v);
  ( == ) { Seq.lemma_eq_intro (Seq.append acc_v (f_v i b_v))
    (repeat_gen_blocks_map_f #a (w * blocksize) n f_v i b_v acc_v) }
  repeat_gen_blocks_map_f #a (w * blocksize) n f_v i b_v acc_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 Prims.op_LessThan Lib.Sequence.lseq Prims.squash Prims.l_Forall Lib.Vec.Lemmas.map_blocks_multi_vec_equiv_pre_k Lib.Sequence.map_blocks_a FStar.Calc.calc_finish Lib.Sequence.seq Prims.eq2 Prims.int Lib.Sequence.length Prims.op_Addition Lib.Sequence.Lemmas.map_blocks_multi_acc Lib.Sequence.Lemmas.repeat_gen_blocks_map_f Prims.Cons FStar.Preorder.relation Prims.Nil Prims.unit FStar.Calc.calc_step FStar.Seq.Base.append Lib.Sequence.map_blocks_multi FStar.Calc.calc_init FStar.Calc.calc_pack Lib.Sequence.Lemmas.map_blocks_multi_acc_is_map_blocks_multi FStar.Seq.Base.lemma_eq_intro FStar.Classical.forall_intro FStar.Seq.Base.index Prims.op_Multiply Prims.l_True FStar.Pervasives.pattern Prims.op_Modulus Lib.Sequence.index_map_blocks_multi Prims._assert Lib.Sequence.div_mul_lt Prims.op_Division Lib.Sequence.Lemmas.get_block_s FStar.Math.Lemmas.cancel_mul_div Lib.Sequence.Lemmas.f_shift FStar.Math.Lemmas.lemma_mult_le_right
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)

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 repeat_gen_blocks_slice_k:
    #inp_t:Type0
  -> w:pos
  -> blocksize:pos{w * blocksize <= max_size_t}
  -> n:nat
  -> hi_f:nat{w * n <= hi_f}
  -> inp:seq inp_t{length inp = w * n * blocksize}
  -> a:(i:nat{i <= hi_f} -> Type)
  -> f:(i:nat{i < hi_f} -> lseq inp_t blocksize -> a i -> a (i + 1))
  -> i:nat{i < n /\ w * i + w <= w * n}
  -> k:nat{w * i <= k /\ k < w * i + w}
  -> acc:a k ->
  Lemma
   (let b_v = get_block_v w blocksize n inp i in
    let f_rep_s = repeat_gen_blocks_f blocksize (w * i) hi_f w b_v a f in
    Math.Lemmas.paren_mul_right w n blocksize;
    let f_rep   = repeat_gen_blocks_f blocksize 0 (w * n) (w * n) inp a f in

    f_rep_s k acc == f_rep k acc)

let repeat_gen_blocks_slice_k #inp_t w blocksize n hi_f inp a f i k acc =
  // Math.Lemmas.paren_mul_right w n blocksize;
  // let f_rep   = repeat_gen_blocks_f blocksize 0 (w * n) (w * n) inp a f in
  // Math.Lemmas.lemma_mult_le_right blocksize (k + 1) (w * n);
  // assert ((k + 1) * blocksize <= w * n * blocksize);
  // let block = Seq.slice inp (k * blocksize) (k * blocksize + blocksize) in
  // assert (f_rep k acc == f k block acc);

  let b_v = get_block_v w blocksize n inp i in
  //let f_rep_s = repeat_gen_blocks_f blocksize (w * i) hi_f w b_v a f in
  let i_b = k - w * i in
  Math.Lemmas.lemma_mult_le_right blocksize (i_b + 1) w;
  let block1 = Seq.slice b_v (i_b * blocksize) (i_b * blocksize + blocksize) in
  //assert (f_rep_s k acc == f k block1 acc);

  let blocksize_v = w * blocksize in
  calc (<=) {
    (i + 1) * blocksize_v;
    (<=) { Math.Lemmas.lemma_mult_le_right blocksize_v (i + 1) n }
    n * blocksize_v;
    (==) { Math.Lemmas.paren_mul_right n w blocksize }
    length inp;
    };

  calc (==) {
    i * blocksize_v + (k - w * i) * blocksize;
    (==) { Math.Lemmas.paren_mul_right i w blocksize }
    i * w * blocksize + (k - w * i) * blocksize;
    (==) { Math.Lemmas.distributivity_add_left (i * w) (k - w * i) blocksize }
    (i * w + (k - w * i)) * blocksize;
    (==) { }
    (i * w + (k + (- w * i))) * blocksize;
    (==) { Math.Lemmas.paren_add_right (i * w) k (- w * i) }
    (i * w + k + (- w * i)) * blocksize;
    (==) { Math.Lemmas.swap_mul i w } // JP: this was the important one that made the proof brittle
    k * blocksize;
    };

  Seq.Properties.slice_slice inp (i * blocksize_v) ((i + 1) * blocksize_v) (i_b * blocksize) (i_b * blocksize + blocksize)

val repeat_gen_blocks_slice:
    #inp_t:Type0
  -> w:pos
  -> blocksize:pos{w * blocksize <= max_size_t}
  -> n:nat
  -> hi_f:nat{w * n <= hi_f}
  -> inp:seq inp_t{length inp = w * n * blocksize}
  -> a:(i:nat{i <= hi_f} -> Type)
  -> f:(i:nat{i < hi_f} -> lseq inp_t blocksize -> a i -> a (i + 1))
  -> i:nat{i < n /\ w * i + w <= w * n}
  -> acc:a (w * i) ->
  Lemma
   (let b_v = get_block_v w blocksize n inp i in
    let f_rep_s = repeat_gen_blocks_f blocksize (w * i) hi_f w b_v a f in
    Math.Lemmas.paren_mul_right w n blocksize;
    let f_rep   = repeat_gen_blocks_f blocksize 0 (w * n) (w * n) inp a f in

    Loops.repeat_right (w * i) (w * i + w) a f_rep acc ==
    Loops.repeat_right (w * i) (w * i + w) a f_rep_s acc)

let repeat_gen_blocks_slice #inp_t w blocksize n hi_f inp a f i acc =
  let b_v = get_block_v w blocksize n inp i in
  let f_rep_s = repeat_gen_blocks_f blocksize (w * i) hi_f w b_v a f in
  Math.Lemmas.paren_mul_right w n blocksize;
  let f_rep   = repeat_gen_blocks_f blocksize 0 (w * n) (w * n) inp a f in

  Classical.forall_intro_2 (repeat_gen_blocks_slice_k #inp_t w blocksize n hi_f inp a f i);
  repeat_right_extensionality w (w * i) a a f_rep f_rep_s acc


val repeat_gen_blocks_multi_vec_step:
    #inp_t:Type0
  -> w:pos
  -> blocksize:pos{w * blocksize <= max_size_t}
  -> n:nat
  -> hi_f:nat{w * n <= hi_f}
  -> inp:seq inp_t{length inp = w * n * blocksize}
  -> a:(i:nat{i <= hi_f} -> Type)
  -> a_vec:(i:nat{i <= n} -> Type)
  -> f:(i:nat{i < hi_f} -> lseq inp_t blocksize -> a i -> a (i + 1))
  -> f_v:(i:nat{i < n} -> lseq inp_t (w * blocksize) -> a_vec i -> a_vec (i + 1))
  -> normalize_v:(i:nat{i <= n} -> a_vec i -> a (w * i))
  -> pre:squash(forall (i:nat{i < n}) (b_v:lseq inp_t (w * blocksize)) (acc_v:a_vec i).
      repeat_gen_blocks_multi_vec_equiv_pre w blocksize n hi_f a a_vec f f_v normalize_v i b_v acc_v)
  -> i:nat{i < n}
  -> acc_v:a_vec i ->
  Lemma
   (let blocksize_v = w * blocksize in
    len_is_w_n_blocksize w blocksize n;

    let f_rep_v = repeat_gen_blocks_f blocksize_v 0 n n inp a_vec f_v in
    let f_rep   = repeat_gen_blocks_f blocksize 0 (w * n) (w * n) inp a f in
    Math.Lemmas.lemma_mult_le_right w (i + 1) n;

    normalize_v (i + 1) (f_rep_v i acc_v) ==
    Loops.repeat_right (w * i) (w * (i + 1)) a f_rep (normalize_v i acc_v))

let repeat_gen_blocks_multi_vec_step #inp_t w blocksize n hi_f inp a a_vec f f_v normalize_v pre i acc_v =
  let b_v = get_block_v w blocksize n inp i in

  //let f_rep_v = repeat_gen_blocks_f blocksize_v 0 n n inp a_vec f_v in
  let f_rep   = repeat_gen_blocks_f blocksize 0 (w * n) (w * n) inp a f in
  Math.Lemmas.lemma_mult_le_left w (i + 1) n;
  let f_rep_s = repeat_gen_blocks_f blocksize (w * i) hi_f w b_v a f in

  let acc0 = normalize_v i acc_v in
  calc (==) {
    repeat_gen_blocks_multi blocksize (w * i) hi_f w b_v a f acc0;
    (==) { lemma_repeat_gen_blocks_multi blocksize (w * i) hi_f w b_v a f acc0 }
    Loops.repeat_right (w * i) (w * i + w) a f_rep_s acc0;
    (==) { repeat_gen_blocks_slice #inp_t w blocksize n hi_f inp a f i acc0 }
    Loops.repeat_right (w * i) (w * i + w) a f_rep acc0;
  };

  assert (repeat_gen_blocks_multi_vec_equiv_pre w blocksize n hi_f a a_vec f f_v normalize_v i b_v acc_v)

#push-options "--z3rlimit_factor 2"
let lemma_repeat_gen_blocks_multi_vec #inp_t w blocksize n hi_f inp a a_vec f f_v normalize_v acc_v0 =
  let len = length inp in
  let blocksize_v = w * blocksize in
  len_is_w_n_blocksize w blocksize n;

  let f_rep_v = repeat_gen_blocks_f blocksize_v 0 n n inp a_vec f_v in
  let f_rep   = repeat_gen_blocks_f blocksize 0 (w * n) (w * n) inp a f in

  let acc0 = normalize_v 0 acc_v0 in

  calc (==) {
    normalize_v n (repeat_gen_blocks_multi blocksize_v 0 n n inp a_vec f_v acc_v0);
    (==) { lemma_repeat_gen_blocks_multi blocksize_v 0 n n inp a_vec f_v acc_v0 }
    normalize_v n (Loops.repeat_right 0 n a_vec f_rep_v acc_v0);
    (==) {
      Classical.forall_intro_2 (repeat_gen_blocks_multi_vec_step w blocksize n hi_f inp a a_vec f f_v normalize_v ());
      lemma_repeat_gen_vec w n a a_vec normalize_v f_rep f_rep_v acc_v0 }
    Loops.repeat_right 0 (w * n) a f_rep acc0;
    (==) { lemma_repeat_gen_blocks_multi blocksize 0 (w * n) (w * n) inp a f acc0 }
    repeat_gen_blocks_multi blocksize 0 (w * n) (w * n) inp a f acc0;
    (==) { repeat_gen_blocks_multi_extensionality_zero blocksize 0 (w * n) hi_f (w * n) inp a a f f acc0 }
    repeat_gen_blocks_multi blocksize 0 hi_f (w * n) inp a f acc0;
  }
#pop-options

////////////////////////
// End of proof of lemma_repeat_gen_blocks_multi_vec
////////////////////////

#push-options "--z3rlimit 100 --retry 2"
let lemma_repeat_gen_blocks_vec #inp_t #c w blocksize inp n a a_vec f l f_v l_v normalize_v acc_v0 =
  let len = length inp in
  let blocksize_v = w * blocksize in
  let rem_v = len % blocksize_v in

  let res_v = repeat_gen_blocks blocksize_v 0 n inp a_vec f_v l_v acc_v0 in
  lemma_repeat_gen_blocks blocksize_v 0 n inp a_vec f_v l_v acc_v0;

  let len0 = w * n * blocksize in
  let blocks_v = Seq.slice inp 0 len0 in
  let last_v = Seq.slice inp len0 len in
  let acc_v = repeat_gen_blocks_multi blocksize_v 0 n n blocks_v a_vec f_v acc_v0 in
  assert (res_v == l_v n rem_v last_v acc_v);

  let acc0 = normalize_v 0 acc_v0 in
  calc (==) {
    l_v n rem_v last_v acc_v;
    (==) { assert (repeat_gen_blocks_vec_equiv_pre w blocksize n a a_vec f l l_v normalize_v rem_v last_v acc_v) }
    repeat_gen_blocks blocksize (w * n) (w * n + w) last_v a f l (normalize_v n acc_v);
    (==) { lemma_repeat_gen_blocks_multi_vec w blocksize n (w * n + w) blocks_v a a_vec f f_v normalize_v acc_v0 }
    repeat_gen_blocks blocksize (w * n) (w * n + w) last_v a f l
      (repeat_gen_blocks_multi blocksize 0 (w * n + w) (w * n) blocks_v a f acc0);
  };

  len_is_w_n_blocksize w blocksize n;
  //assert (len0 % blocksize = 0 /\ len0 / blocksize = w * n);
  //Math.Lemmas.paren_mul_right n w blocksize;
  //div_mul_lt blocksize rem_v w;
  //assert (rem_v / blocksize < w);
  repeat_gen_blocks_split blocksize len0 (w * n + w) 0 inp a f l acc0
#pop-options


val lemma_repeat_blocks_multi_vec_equiv_pre:
    #a:Type0
  -> #b:Type0
  -> #b_vec:Type0
  -> w:pos
  -> blocksize:pos{w * blocksize <= max_size_t}
  -> n:nat
  -> hi_f:nat{w * n <= hi_f}
  -> f:(lseq a blocksize -> b -> b)
  -> f_v:(lseq a (w * blocksize) -> b_vec -> b_vec)
  -> normalize_v:(b_vec -> b)
  -> pre:squash (forall (b_v:lseq a (w * blocksize)) (acc_v:b_vec).
         repeat_blocks_multi_vec_equiv_pre w blocksize f f_v normalize_v b_v acc_v)
  -> i:nat{i < n}
  -> b_v:lseq a (w * blocksize)
  -> acc_v:b_vec ->
  Lemma
   (repeat_gen_blocks_multi_vec_equiv_pre #a w blocksize n hi_f
     (Loops.fixed_a b) (Loops.fixed_a b_vec)
     (Loops.fixed_i f) (Loops.fixed_i f_v)
     (Loops.fixed_i normalize_v) i b_v acc_v)

let lemma_repeat_blocks_multi_vec_equiv_pre #a #b #b_vec w blocksize n hi_f f f_v normalize_v pre i b_v acc_v =
  assert (repeat_blocks_multi_vec_equiv_pre w blocksize f f_v normalize_v b_v acc_v);
  Math.Lemmas.cancel_mul_mod w blocksize;
  assert (normalize_v (f_v b_v acc_v) == repeat_blocks_multi blocksize b_v f (normalize_v acc_v));
  Math.Lemmas.cancel_mul_div w blocksize;

  Math.Lemmas.lemma_mult_le_right w (i + 1) n;

  calc (==) {
    repeat_blocks_multi blocksize b_v f (normalize_v acc_v);
    (==) { repeat_blocks_multi_is_repeat_gen_blocks_multi w blocksize b_v f (normalize_v acc_v) }
    repeat_gen_blocks_multi blocksize 0 w w b_v (Loops.fixed_a b) (Loops.fixed_i f) (normalize_v acc_v);
    (==) { repeat_gen_blocks_multi_extensionality_zero blocksize (w * i) hi_f w w b_v
           (Loops.fixed_a b) (Loops.fixed_a b) (Loops.fixed_i f) (Loops.fixed_i f) (normalize_v acc_v) }
    repeat_gen_blocks_multi blocksize (w * i) hi_f w b_v (Loops.fixed_a b) (Loops.fixed_i f) (normalize_v acc_v);
    }


let lemma_repeat_blocks_multi_vec #a #b #b_vec w blocksize inp f f_v normalize_v acc_v0 =
  let blocksize_v = w * blocksize in
  let len = length inp in
  let nw = len / blocksize_v in
  len_is_w_n_blocksize w blocksize nw;

  let acc0 = normalize_v acc_v0 in

  calc (==) {
    normalize_v (repeat_blocks_multi #a #b_vec blocksize_v inp f_v acc_v0);
    (==) { repeat_blocks_multi_is_repeat_gen_blocks_multi nw blocksize_v inp f_v acc_v0 }
    normalize_v (repeat_gen_blocks_multi blocksize_v 0 nw nw inp (Loops.fixed_a b_vec) (Loops.fixed_i f_v) acc_v0);
    (==) {
      Classical.forall_intro_3 (lemma_repeat_blocks_multi_vec_equiv_pre w blocksize nw (w * nw) f f_v normalize_v ());
      lemma_repeat_gen_blocks_multi_vec w blocksize nw (w * nw) inp (Loops.fixed_a b) (Loops.fixed_a b_vec)
	(Loops.fixed_i f) (Loops.fixed_i f_v) (Loops.fixed_i normalize_v) acc_v0 }
    repeat_gen_blocks_multi blocksize 0 (nw * w) (nw * w) inp (Loops.fixed_a b) (Loops.fixed_i f) acc0;
    (==) { repeat_blocks_multi_is_repeat_gen_blocks_multi (nw * w) blocksize inp f acc0 }
    repeat_blocks_multi blocksize inp f acc0;
    }


val lemma_repeat_blocks_vec_equiv_pre:
    #a:Type0
  -> #b:Type0
  -> #b_vec:Type0
  -> #c:Type0
  -> w:pos
  -> blocksize:pos{w * blocksize <= max_size_t}
  -> n:nat
  -> f:(lseq a blocksize -> b -> b)
  -> l:(len:nat{len < blocksize} -> lseq a len -> b -> c)
  -> l_v:(len:nat{len < w * blocksize} -> lseq a len -> b_vec -> c)
  -> normalize_v:(b_vec -> b)
  -> pre:squash (forall (rem:nat{rem < w * blocksize}) (b_v:lseq a rem) (acc_v:b_vec).
      repeat_blocks_vec_equiv_pre w blocksize f l l_v normalize_v rem b_v acc_v)
  -> rem:nat{rem < w * blocksize}
  -> b_v:lseq a rem
  -> acc_v:b_vec ->
  Lemma
   (repeat_gen_blocks_vec_equiv_pre #a #c w blocksize n
     (Loops.fixed_a b) (Loops.fixed_a b_vec)
     (Loops.fixed_i f) (Loops.fixed_i l) (Loops.fixed_i l_v)
     (Loops.fixed_i normalize_v) rem b_v acc_v)

let lemma_repeat_blocks_vec_equiv_pre #a #b #b_vec #c w blocksize n f l l_v normalize_v pre rem b_v acc_v =
  let nb_rem = rem / blocksize in
  div_mul_lt blocksize rem w;
  assert (nb_rem < w);

  let acc0 = normalize_v acc_v in

  calc (==) {
    Loops.fixed_i l_v n rem b_v acc_v;
    (==) { }
    l_v rem b_v acc_v;
    (==) { assert (repeat_blocks_vec_equiv_pre w blocksize f l l_v normalize_v rem b_v acc_v) }
    repeat_blocks blocksize b_v f l acc0;
    (==) { repeat_blocks_is_repeat_gen_blocks nb_rem blocksize b_v f l acc0 }
    repeat_gen_blocks blocksize 0 nb_rem b_v (Loops.fixed_a b) (Loops.fixed_i f) (Loops.fixed_i l) acc0;
    (==) { repeat_gen_blocks_extensionality_zero blocksize (w * n) (w * n + w) nb_rem nb_rem b_v
           (Loops.fixed_a b) (Loops.fixed_a b)
	   (Loops.fixed_i f) (Loops.fixed_i l)
	   (Loops.fixed_i f) (Loops.fixed_i l) acc0 }
    repeat_gen_blocks blocksize (w * n) (w * n + w) b_v (Loops.fixed_a b) (Loops.fixed_i f) (Loops.fixed_i l) acc0;
    }


let lemma_repeat_blocks_vec #a #b #b_vec #c w blocksize inp f l f_v l_v normalize_v acc_v0 =
  let blocksize_v = w * blocksize in
  let nb_v = length inp / blocksize_v in

  calc (==) {
    repeat_blocks blocksize_v inp f_v l_v acc_v0;
    (==) { repeat_blocks_is_repeat_gen_blocks nb_v blocksize_v inp f_v l_v acc_v0 }
    repeat_gen_blocks blocksize_v 0 nb_v inp (Loops.fixed_a b_vec) (Loops.fixed_i f_v) (Loops.fixed_i l_v) acc_v0;
    (==) { Classical.forall_intro_3 (lemma_repeat_blocks_multi_vec_equiv_pre w blocksize nb_v (w * nb_v + w) f f_v normalize_v ());
           Classical.forall_intro_3 (lemma_repeat_blocks_vec_equiv_pre #a #b #b_vec #c w blocksize nb_v f l l_v normalize_v ());
           lemma_repeat_gen_blocks_vec w blocksize inp nb_v
             (Loops.fixed_a b) (Loops.fixed_a b_vec) (Loops.fixed_i f) (Loops.fixed_i l)
             (Loops.fixed_i f_v) (Loops.fixed_i l_v) (Loops.fixed_i normalize_v) acc_v0 }
    repeat_gen_blocks blocksize 0 (w * nb_v + w) inp (Loops.fixed_a b) (Loops.fixed_i f) (Loops.fixed_i l) (normalize_v acc_v0);
    (==) { repeat_blocks_is_repeat_gen_blocks (w * nb_v + w) blocksize inp f l (normalize_v acc_v0) }
    repeat_blocks blocksize inp f l (normalize_v acc_v0);
  }


////////////////////////
// Start of proof of map_blocks_multi_vec lemma
////////////////////////

let lemma_f_map_ind w blocksize n i k =
  calc (<) {
    w * i + k / blocksize;
    (<) { div_mul_lt blocksize k w }
    w * i + w;
    (==) { Math.Lemmas.distributivity_add_right w i 1 }
    w * (i + 1);
    (<=) { Math.Lemmas.lemma_mult_le_left w (i + 1) n }
    w * n;
    }


val normalize_v_map:
    #a:Type
  -> w:pos
  -> blocksize:pos{w * blocksize <= max_size_t}
  -> n:nat
  -> i:nat{i <= n}
  -> map_blocks_a a (w * blocksize) n i ->
  map_blocks_a a blocksize (w * n) (w * i)

let normalize_v_map #a w blocksize n i b =
  Math.Lemmas.lemma_mult_le_right w i n;
  b


let map_blocks_multi_vec_equiv_pre
  (#a:Type)
  (w:pos)
  (blocksize:pos{w * blocksize <= max_size_t})
  (n:nat)
  (hi_f:nat{w * n <= hi_f})
  (f:(i:nat{i < hi_f} -> lseq a blocksize -> lseq a blocksize))
  (f_v:(i:nat{i < n} -> lseq a (w * blocksize) -> lseq a (w * blocksize)))
  (i:nat{i < n})
  (b_v:lseq a (w * blocksize))
  (acc_v:map_blocks_a a (w * blocksize) n i)
  : prop
 =
  Math.Lemmas.lemma_mult_le_right w (i + 1) n;

  repeat_gen_blocks_map_f #a (w * blocksize) n f_v i b_v acc_v `Seq.equal`
  map_blocks_multi_acc blocksize (w * i) hi_f w b_v f acc_v

// It means the following
// Seq.append acc_v (f_v i b_v) ==
// map_blocks_multi_acc blocksize (w * i) (w * n) w b_v f acc_v


val lemma_map_blocks_multi_vec_equiv_pre_k:
    #a:Type
  -> w:pos
  -> blocksize:pos{w * blocksize <= max_size_t}
  -> n:nat
  -> hi_f:nat{w * n <= hi_f}
  -> f:(i:nat{i < hi_f} -> lseq a blocksize -> lseq a blocksize)
  -> f_v:(i:nat{i < n} -> lseq a (w * blocksize) -> lseq a (w * blocksize))
  -> i:nat{i < n}
  -> b_v:lseq a (w * blocksize)
  -> pre:squash (forall (k:nat{k < w * blocksize}). map_blocks_multi_vec_equiv_pre_k w blocksize n (w * n) f f_v i b_v k)
  -> acc_v:map_blocks_a a (w * blocksize) n i ->
  Lemma (map_blocks_multi_vec_equiv_pre #a w blocksize n hi_f f f_v i b_v acc_v)

let lemma_map_blocks_multi_vec_equiv_pre_k #a w blocksize n hi_f f f_v i b_v pre acc_v =
  //let lp = repeat_gen_blocks_map_f #a (w * blocksize) n f_v i b_v acc_v in
  //assert (lp == Seq.append acc_v (f_v i b_v));
val lemma_map_blocks_multi_vec_equiv_pre_k:
    #a:Type
  -> w:pos
  -> blocksize:pos{w * blocksize <= max_size_t}
  -> n:nat
  -> hi_f:nat{w * n <= hi_f}
  -> f:(i:nat{i < hi_f} -> lseq a blocksize -> lseq a blocksize)
  -> f_v:(i:nat{i < n} -> lseq a (w * blocksize) -> lseq a (w * blocksize))
  -> i:nat{i < n}
  -> b_v:lseq a (w * blocksize)
  -> pre:squash (forall (k:nat{k < w * blocksize}). map_blocks_multi_vec_equiv_pre_k w blocksize n (w * n) f f_v i b_v k)
  -> acc_v:map_blocks_a a (w * blocksize) n i ->
  Lemma (map_blocks_multi_vec_equiv_pre #a w blocksize n hi_f f f_v i b_v acc_v)

    w: Prims.pos ->
    blocksize: Prims.pos{w * blocksize <= Lib.IntTypes.max_size_t} ->
    n: Prims.nat ->
    hi_f: Prims.nat{w * n <= hi_f} ->
    f: (i: Prims.nat{i < hi_f} -> _: Lib.Sequence.lseq a blocksize -> Lib.Sequence.lseq a blocksize) ->
    f_v:
      (i: Prims.nat{i < n} -> _: Lib.Sequence.lseq a (w * blocksize)
          -> Lib.Sequence.lseq a (w * blocksize)) ->
    i: Prims.nat{i < n} ->
    b_v: Lib.Sequence.lseq a (w * blocksize) ->
    pre:
      Prims.squash (forall (k: Prims.nat{k < w * blocksize}).
            Lib.Vec.Lemmas.map_blocks_multi_vec_equiv_pre_k w blocksize n (w * n) f f_v i b_v k) ->
    acc_v: Lib.Sequence.map_blocks_a a (w * blocksize) n i
  -> FStar.Pervasives.Lemma
    (ensures Lib.Vec.Lemmas.map_blocks_multi_vec_equiv_pre w blocksize n hi_f f f_v i b_v acc_v)