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_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 =
let b_v = get_block_v w blocksize n inp i 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
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 }
  k * blocksize;
};
Seq.Properties.slice_slice inp
  (i * blocksize_v)
  ((i + 1) * blocksize_v)
  (i_b * blocksize)
  (i_b * blocksize + blocksize)
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 Lib.Sequence.lseq Prims.op_Addition Prims.l_and FStar.Seq.Properties.slice_slice Prims.unit FStar.Calc.calc_finish Prims.eq2 Prims.op_Subtraction Prims.Cons FStar.Preorder.relation Prims.Nil FStar.Calc.calc_step Prims.op_Minus FStar.Calc.calc_init FStar.Calc.calc_pack FStar.Math.Lemmas.paren_mul_right Prims.squash FStar.Math.Lemmas.distributivity_add_left FStar.Math.Lemmas.paren_add_right FStar.Math.Lemmas.swap_mul FStar.Math.Lemmas.lemma_mult_le_right FStar.Seq.Base.seq FStar.Seq.Base.slice Prims.op_Multiply Lib.Vec.Lemmas.get_block_v
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)
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)

    w: Prims.pos ->
    blocksize: Prims.pos{w * blocksize <= Lib.IntTypes.max_size_t} ->
    n: Prims.nat ->
    hi_f: Prims.nat{w * n <= hi_f} ->
    inp: Lib.Sequence.seq inp_t {Lib.Sequence.length inp = (w * n) * blocksize} ->
    a: (i: Prims.nat{i <= hi_f} -> Type) ->
    f: (i: Prims.nat{i < hi_f} -> _: Lib.Sequence.lseq inp_t blocksize -> _: a i -> a (i + 1)) ->
    i: Prims.nat{i < n /\ w * i + w <= w * n} ->
    k: Prims.nat{w * i <= k /\ k < w * i + w} ->
    acc: a k
  -> FStar.Pervasives.Lemma
    (ensures
      (let b_v = Lib.Vec.Lemmas.get_block_v w blocksize n inp i in
        let f_rep_s = Lib.Sequence.Lemmas.repeat_gen_blocks_f blocksize (w * i) hi_f w b_v a f in
        [@@ FStar.Pervasives.inline_let ]let _ = FStar.Math.Lemmas.paren_mul_right w n blocksize in
        let f_rep = Lib.Sequence.Lemmas.repeat_gen_blocks_f blocksize 0 (w * n) (w * n) inp a f in
        f_rep_s k acc == f_rep k acc))