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)
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 = 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)
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.squash Prims.l_Forall Lib.Vec.Lemmas.repeat_gen_blocks_multi_vec_equiv_pre Prims._assert Prims.unit FStar.Calc.calc_finish Prims.eq2 Lib.Sequence.Lemmas.repeat_gen_blocks_multi Lib.LoopCombinators.repeat_right Prims.Cons FStar.Preorder.relation Prims.Nil FStar.Calc.calc_step FStar.Calc.calc_init FStar.Calc.calc_pack Lib.Sequence.Lemmas.lemma_repeat_gen_blocks_multi Lib.Vec.Lemmas.repeat_gen_blocks_slice Prims.op_Multiply Prims.l_and Lib.Sequence.Lemmas.repeat_gen_blocks_f FStar.Math.Lemmas.lemma_mult_le_left 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)

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))
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))

    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) ->
    a_vec: (i: Prims.nat{i <= n} -> Type) ->
    f: (i: Prims.nat{i < hi_f} -> _: Lib.Sequence.lseq inp_t blocksize -> _: a i -> a (i + 1)) ->
    f_v:
      (i: Prims.nat{i < n} -> _: Lib.Sequence.lseq inp_t (w * blocksize) -> _: a_vec i
          -> a_vec (i + 1)) ->
    normalize_v: (i: Prims.nat{i <= n} -> _: a_vec i -> a (w * i)) ->
    pre:
      Prims.squash (forall (i: Prims.nat{i < n})
            (b_v: Lib.Sequence.lseq inp_t (w * blocksize))
            (acc_v: a_vec i).
            Lib.Vec.Lemmas.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: Prims.nat{i < n} ->
    acc_v: a_vec i
  -> FStar.Pervasives.Lemma
    (ensures
      (let blocksize_v = w * blocksize in
        [@@ FStar.Pervasives.inline_let ]let _ =
          Lib.Vec.Lemmas.len_is_w_n_blocksize w blocksize n
        in
        let f_rep_v = Lib.Sequence.Lemmas.repeat_gen_blocks_f blocksize_v 0 n n inp a_vec f_v in
        let f_rep = Lib.Sequence.Lemmas.repeat_gen_blocks_f blocksize 0 (w * n) (w * n) inp a f in
        [@@ FStar.Pervasives.inline_let ]let _ =
          FStar.Math.Lemmas.lemma_mult_le_right w (i + 1) n
        in
        normalize_v (i + 1) (f_rep_v i acc_v) ==
        Lib.LoopCombinators.repeat_right (w * i) (w * (i + 1)) a f_rep (normalize_v i acc_v)))