val fill_blocks:
    #t:Type0
  -> h0:mem
  -> len:size_t
  -> n:size_t{v n * v len <= max_size_t}
  -> output:lbuffer t (n *! len)
  -> a_spec:(i:size_nat{i <= v n} -> Type)
  -> refl:(mem -> i:size_nat{i <= v n} -> GTot (a_spec i))
  -> footprint:(i:size_nat{i <= v n} -> GTot
      (l:B.loc{B.loc_disjoint l (loc output) /\
               B.address_liveness_insensitive_locs `B.loc_includes` l}))
  -> spec:(mem -> GTot (i:size_nat{i < v n} -> a_spec i -> a_spec (i + 1) & Seq.lseq t (v len)))
  -> impl:(i:size_t{v i < v n} -> Stack unit
      (requires fun h1 ->
        (v i + 1) * v len <= max_size_t /\
        modifies (footprint (v i) |+| loc (gsub output 0ul (i *! len))) h0 h1)
      (ensures  fun h1 _ h2 ->
        (let block = gsub output (i *! len) len in
        let s, b = spec h0 (v i) (refl h1 (v i)) in
        footprint (v i + 1) `B.loc_includes` footprint (v i) /\
        B.modifies (B.loc_union (footprint (v i + 1)) (loc block)) h1 h2 /\
        refl h2 (v i + 1) == s /\ as_seq h2 block == b))) ->
  Stack unit
    (requires fun h -> h0 == h /\ live h output)
    (ensures  fun _ _ h1 ->
      B.modifies (B.loc_union (footprint (v n)) (loc output)) h0 h1 /\
     (let s, o = Seq.generate_blocks (v len) (v n) (v n) a_spec (spec h0) (refl h0 0) in
      refl h1 (v n) == s /\
      as_seq #_ #t h1 output == o))
let fill_blocks #t h0 len n output a_spec refl footprint spec impl =
  [@inline_let]
  let refl' h (i:nat{i <= v n}) : GTot (Sequence.generate_blocks_a t (v len) (v n) a_spec i) =
    refl h i, as_seq h (gsub output (size 0) (size i *! len))
  in
  [@inline_let]
  let footprint' i = B.loc_union (footprint i) (loc (gsub output 0ul (size i *! len))) in
  [@inline_let]
  let spec' h0 = Sequence.generate_blocks_inner t (v len) (v n) a_spec (spec h0)
  in
  let h0 = ST.get () in
  loop h0 n (Sequence.generate_blocks_a t (v len) (v n) a_spec) refl' footprint' spec'
  (fun i ->
    Loop.unfold_repeat_gen (v n) (Sequence.generate_blocks_a t (v len) (v n) a_spec)
      (Sequence.generate_blocks_inner t (v len) (v n) a_spec (spec h0)) (refl' h0 0) (v i);
    assert ((v i + 1) * v len == v i * v len + v len);
    assert (v i * v len <= max_size_t);
    let block = sub output (i *! len) len in
    let h0_ = ST.get() in
    impl i;
    let h = ST.get() in
    assert(modifies (B.loc_union (footprint (v i + 1)) (loc block)) h0_ h);
    assert ((v i + 1) * v len == v i * v len + v len);
    assert (B.loc_includes (loc (gsub output 0ul (i *! len +! len))) (loc block));
    assert (B.loc_includes (footprint' (v i + 1)) (loc (gsub output 0ul (i *! len +! len))));
    B.loc_includes_union_l (footprint (v i + 1)) (loc (gsub output 0ul (i *! len +! len))) (footprint (v i + 1));
    B.loc_includes_union_l (footprint (v i + 1)) (loc (gsub output 0ul (i *! len +! len))) (loc block);
    B.loc_includes_union_r (B.loc_union (footprint (v i + 1)) (loc (gsub output 0ul (i *! len +! len)))) (footprint (v i + 1)) (loc block);
    assert(B.loc_includes (B.loc_union (footprint (v i + 1)) (loc (gsub output 0ul (i *! len +! len)))) (B.loc_union (footprint (v i + 1)) (loc block)));
    FStar.Seq.lemma_split
      (as_seq h (gsub output (size 0) (i *! len +! len)))
      (v i * v len)
  );
  assert (Seq.equal
    (as_seq h0 (gsub output (size 0) (size 0 *! len))) FStar.Seq.empty);
  norm_spec [delta_only [`%Seq.generate_blocks]]
            (Seq.generate_blocks (v len) (v n) (v n) a_spec (spec h0) (refl h0 0));
  let h1 = ST.get() in
  assert(refl' h1 (v n) == Loop.repeat_gen (v n)
         (Sequence.generate_blocks_a t (v len) (v n) a_spec)
         (Sequence.generate_blocks_inner t (v len) (v n) a_spec (spec h0))
         (refl' h0 0));
  assert(B.loc_includes (loc output) (loc (gsub output 0ul (n *! len))));
  assert(B.modifies (B.loc_union (footprint (v n)) (loc (gsub output 0ul (n *! len)))) h0 h1);
  B.loc_includes_union_l (footprint (v n)) (loc output) (footprint (v n));
  B.loc_includes_union_l (footprint (v n)) (loc output) (loc (gsub output 0ul (n *! len)));
  //B.loc_includes_union_r (B.loc_union (footprint (v n)) (loc output)) (B.loc_union (footprint (v n)) (gsub output 0ul (n *! len)));
  assert(B.loc_includes (B.loc_union (footprint (v n)) (loc output)) (B.loc_union (footprint (v n)) (loc (gsub output 0ul (n *! len)))));
  assert(B.modifies (B.loc_union (footprint (v n)) (loc output)) h0 h1)
val fill_blocks:
    #t:Type0
  -> h0:mem
  -> len:size_t
  -> n:size_t{v n * v len <= max_size_t}
  -> output:lbuffer t (n *! len)
  -> a_spec:(i:size_nat{i <= v n} -> Type)
  -> refl:(mem -> i:size_nat{i <= v n} -> GTot (a_spec i))
  -> footprint:(i:size_nat{i <= v n} -> GTot
      (l:B.loc{B.loc_disjoint l (loc output) /\
               B.address_liveness_insensitive_locs `B.loc_includes` l}))
  -> spec:(mem -> GTot (i:size_nat{i < v n} -> a_spec i -> a_spec (i + 1) & Seq.lseq t (v len)))
  -> impl:(i:size_t{v i < v n} -> Stack unit
      (requires fun h1 ->
        (v i + 1) * v len <= max_size_t /\
        modifies (footprint (v i) |+| loc (gsub output 0ul (i *! len))) h0 h1)
      (ensures  fun h1 _ h2 ->
        (let block = gsub output (i *! len) len in
        let s, b = spec h0 (v i) (refl h1 (v i)) in
        footprint (v i + 1) `B.loc_includes` footprint (v i) /\
        B.modifies (B.loc_union (footprint (v i + 1)) (loc block)) h1 h2 /\
        refl h2 (v i + 1) == s /\ as_seq h2 block == b))) ->
  Stack unit
    (requires fun h -> h0 == h /\ live h output)
    (ensures  fun _ _ h1 ->
      B.modifies (B.loc_union (footprint (v n)) (loc output)) h0 h1 /\
     (let s, o = Seq.generate_blocks (v len) (v n) (v n) a_spec (spec h0) (refl h0 0) in
      refl h1 (v n) == s /\
      as_seq #_ #t h1 output == o))
let fill_blocks #t h0 len n output a_spec refl footprint spec impl =
[@@ inline_let ]let refl' h (i: nat{i <= v n})
    : GTot (Sequence.generate_blocks_a t (v len) (v n) a_spec i) =
  refl h i, as_seq h (gsub output (size 0) (size i *! len))
in
[@@ inline_let ]let footprint' i =
  B.loc_union (footprint i) (loc (gsub output 0ul (size i *! len)))
in
[@@ inline_let ]let spec' h0 = Sequence.generate_blocks_inner t (v len) (v n) a_spec (spec h0) in
let h0 = ST.get () in
loop h0
  n
  (Sequence.generate_blocks_a t (v len) (v n) a_spec)
  refl'
  footprint'
  spec'
  (fun i ->
      Loop.unfold_repeat_gen (v n)
        (Sequence.generate_blocks_a t (v len) (v n) a_spec)
        (Sequence.generate_blocks_inner t (v len) (v n) a_spec (spec h0))
        (refl' h0 0)
        (v i);
      assert ((v i + 1) * v len == v i * v len + v len);
      assert (v i * v len <= max_size_t);
      let block = sub output (i *! len) len in
      let h0_ = ST.get () in
      impl i;
      let h = ST.get () in
      assert (modifies (B.loc_union (footprint (v i + 1)) (loc block)) h0_ h);
      assert ((v i + 1) * v len == v i * v len + v len);
      assert (B.loc_includes (loc (gsub output 0ul (i *! len +! len))) (loc block));
      assert (B.loc_includes (footprint' (v i + 1)) (loc (gsub output 0ul (i *! len +! len))));
      B.loc_includes_union_l (footprint (v i + 1))
        (loc (gsub output 0ul (i *! len +! len)))
        (footprint (v i + 1));
      B.loc_includes_union_l (footprint (v i + 1))
        (loc (gsub output 0ul (i *! len +! len)))
        (loc block);
      B.loc_includes_union_r (B.loc_union (footprint (v i + 1))
            (loc (gsub output 0ul (i *! len +! len))))
        (footprint (v i + 1))
        (loc block);
      assert (B.loc_includes (B.loc_union (footprint (v i + 1))
                (loc (gsub output 0ul (i *! len +! len))))
            (B.loc_union (footprint (v i + 1)) (loc block)));
      FStar.Seq.lemma_split (as_seq h (gsub output (size 0) (i *! len +! len))) (v i * v len));
assert (Seq.equal (as_seq h0 (gsub output (size 0) (size 0 *! len))) FStar.Seq.empty);
norm_spec [delta_only [`%Seq.generate_blocks]]
  (Seq.generate_blocks (v len) (v n) (v n) a_spec (spec h0) (refl h0 0));
let h1 = ST.get () in
assert (refl' h1 (v n) ==
    Loop.repeat_gen (v n)
      (Sequence.generate_blocks_a t (v len) (v n) a_spec)
      (Sequence.generate_blocks_inner t (v len) (v n) a_spec (spec h0))
      (refl' h0 0));
assert (B.loc_includes (loc output) (loc (gsub output 0ul (n *! len))));
assert (B.modifies (B.loc_union (footprint (v n)) (loc (gsub output 0ul (n *! len)))) h0 h1);
B.loc_includes_union_l (footprint (v n)) (loc output) (footprint (v n));
B.loc_includes_union_l (footprint (v n)) (loc output) (loc (gsub output 0ul (n *! len)));
assert (B.loc_includes (B.loc_union (footprint (v n)) (loc output))
      (B.loc_union (footprint (v n)) (loc (gsub output 0ul (n *! len)))));
assert (B.modifies (B.loc_union (footprint (v n)) (loc output)) h0 h1)
Lib.Buffer.fst.checked
prims.fst.checked LowStar.ImmutableBuffer.fst.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked Lib.Sequence.fst.checked Lib.RawIntTypes.fsti.checked Lib.Memzero0.fsti.checked Lib.Loops.fsti.checked Lib.LoopCombinators.fst.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Monotonic.HyperHeap.fsti.checked FStar.Math.Lemmas.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
Lib.Buffer.fst
FStar.Monotonic.HyperStack.mem Lib.IntTypes.size_t Prims.b2t Prims.op_LessThanOrEqual FStar.Mul.op_Star Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB Lib.IntTypes.max_size_t Lib.Buffer.lbuffer Lib.IntTypes.op_Star_Bang Lib.IntTypes.size_nat LowStar.Monotonic.Buffer.loc Prims.l_and LowStar.Monotonic.Buffer.loc_disjoint Lib.Buffer.loc Lib.Buffer.MUT LowStar.Monotonic.Buffer.loc_includes LowStar.Monotonic.Buffer.address_liveness_insensitive_locs Prims.op_LessThan FStar.Pervasives.Native.tuple2 Prims.op_Addition Lib.Sequence.lseq Prims.unit Lib.Buffer.modifies Lib.Buffer.op_Bar_Plus_Bar Lib.Buffer.gsub FStar.UInt32.__uint_to_t LowStar.Monotonic.Buffer.modifies LowStar.Monotonic.Buffer.loc_union Prims.eq2 Lib.Buffer.as_seq Lib.Buffer.lbuffer_t Prims._assert LowStar.Monotonic.Buffer.loc_includes_union_l Lib.Sequence.generate_blocks_a Lib.LoopCombinators.repeat_gen Lib.Sequence.generate_blocks_inner FStar.HyperStack.ST.get FStar.Pervasives.norm_spec Prims.Cons FStar.Pervasives.norm_step FStar.Pervasives.delta_only Prims.string Prims.Nil Lib.Sequence.seq Prims.int Lib.Sequence.length Lib.Sequence.generate_blocks Lib.Sequence.equal Lib.IntTypes.size FStar.Seq.Base.empty Lib.Buffer.loop FStar.Seq.Properties.lemma_split Lib.IntTypes.op_Plus_Bang LowStar.Monotonic.Buffer.loc_includes_union_r Lib.Buffer.sub Lib.LoopCombinators.unfold_repeat_gen Prims.nat Prims.op_Subtraction Prims.pow2 FStar.Pervasives.Native.Mktuple2
module Lib.Buffer

open FStar.Mul

open Lib.IntTypes
open Lib.RawIntTypes

friend Lib.Sequence
friend Lib.LoopCombinators

module B = LowStar.Buffer
module IB = LowStar.ImmutableBuffer
module U32 = FStar.UInt32
module ST = FStar.HyperStack.ST
module HS = FStar.HyperStack
module Seq = Lib.Sequence
module ByteSeq = Lib.ByteSequence

#reset-options "--z3rlimit 350 --max_fuel 0 --max_ifuel 0"

let modifies_includes l1 l2 h0 h1 = ()
let modifies_trans l1 l2 h0 h1 h2 = ()
let live_sub #t #a #len b start n h = ()
let modifies_sub #t #a #len b start n h0 h1 = ()

let as_seq_gsub #t #a #len h b start n = ()

let sub #t #a #len b start n =
  match t with
  | MUT -> B.sub (b <: buffer a) start n
  | IMMUT -> IB.isub (b <: ibuffer a) start n
  | CONST -> CB.sub (b <: cbuffer a) start n

let index #t #a #len b i =
  match t with
  | MUT -> B.index (b <: buffer a) i
  | IMMUT -> IB.index (b <: ibuffer a) i
  | CONST -> CB.index (b <: cbuffer a) i

let upd #a #len b i v =
  let h0 = ST.get() in
  B.upd (b <: buffer a) i v;
  let h1 = ST.get() in
  assert (B.modifies (loc b) h0 h1);
  assert (modifies (loc b) h0 h1)

let bget_as_seq #t #a #len h b i = ()

let recall #t #a #len b =
  match t with
  | IMMUT -> B.recall (b <: ibuffer a)
  | MUT -> B.recall (b <: buffer a)
  | CONST -> B.recall (CB.cast (b <: cbuffer a))

let create #a clen init =
  B.alloca init (normalize_term clen)

#set-options "--max_fuel 1"

let createL #a init =
  B.alloca_of_list init

let createL_global #a init =
  CB.of_ibuffer (IB.igcmalloc_of_list #a root init)

let createL_mglobal #a init =
  B.mgcmalloc_of_list #a FStar.Monotonic.HyperHeap.root init

let recall_contents #a #len b s =
  B.recall_p (CB.to_ibuffer b) (cpred s)

(* JP: why triplicate the code? would it not extract if we just cast i to a monotonic buffer?! *)
let copy #t #a #len o i =
  match t with
  | MUT ->
    let h0 = ST.get () in
    LowStar.BufferOps.blit (i <: buffer a) 0ul (o <: buffer a) 0ul len;
    let h1 = ST.get () in
    assert (Seq.slice (as_seq h1 o) 0 (v len) == Seq.slice (as_seq h0 i) 0 (v len))
  | IMMUT ->
    let h0 = ST.get () in
    LowStar.BufferOps.blit (i <: ibuffer a) 0ul (o <: buffer a) 0ul len;
    let h1 = ST.get () in
    assert (Seq.slice (as_seq h1 o) 0 (v len) == Seq.slice (as_seq h0 i) 0 (v len))
  | CONST ->
    let h0 = ST.get () in
    LowStar.BufferOps.blit (CB.cast (i <: cbuffer a)) 0ul (o <: buffer a) 0ul len;
    let h1 = ST.get () in
    assert (Seq.slice (as_seq h1 o) 0 (v len) == Seq.slice (as_seq h0 i) 0 (v len))

let memset #a #blen b init len =
  B.fill #a #(fun _ _ -> True) #(fun _ _ -> True) b init len

#set-options "--max_fuel 0"

let update_sub #t #a #len dst start n src =
  match t with
  | MUT ->
      let h0 = ST.get () in
      LowStar.BufferOps.blit (src <: buffer a)
        0ul (dst <: buffer a) (size_to_UInt32 start) (size_to_UInt32 n);
      let h1 = ST.get () in
      assert (forall (k:nat{k < v n}). bget h1 dst (v start + k) == bget h0 src k);
      FStar.Seq.lemma_eq_intro
        (as_seq h1 dst)
        (Seq.update_sub #a #(v len) (as_seq h0 dst) (v start) (v n) (as_seq h0 src))
  | IMMUT ->
      let h0 = ST.get () in
      LowStar.BufferOps.blit (src <: ibuffer a)
        0ul (dst <: buffer a) (size_to_UInt32 start) (size_to_UInt32 n);
      let h1 = ST.get () in
      assert (forall (k:nat{k < v n}). bget h1 dst (v start + k) == bget h0 src k);
      FStar.Seq.lemma_eq_intro
        (as_seq h1 dst)
        (Seq.update_sub #a #(v len) (as_seq h0 dst) (v start) (v n) (as_seq h0 src))
  | CONST ->
      let h0 = ST.get () in
      LowStar.BufferOps.blit (CB.cast (src <: cbuffer a))
        0ul (dst <: buffer a) (size_to_UInt32 start) (size_to_UInt32 n);
      let h1 = ST.get () in
      assert (forall (k:nat{k < v n}). bget h1 dst (v start + k) == bget h0 src k);
      FStar.Seq.lemma_eq_intro
        (as_seq h1 dst)
        (Seq.update_sub #a #(v len) (as_seq h0 dst) (v start) (v n) (as_seq h0 src))

let update_sub_f #a #len h0 buf start n spec f =
  let tmp = sub buf start n in
  let h0 = ST.get () in
  f ();
  let h1 = ST.get () in
  assert (v (len -! (start +! n)) == v len - v (start +! n));
  B.modifies_buffer_elim (B.gsub #a buf 0ul start) (loc tmp) h0 h1;
  B.modifies_buffer_elim (B.gsub #a buf (start +! n) (len -! (start +! n))) (loc tmp) h0 h1;
  Sequence.lemma_update_sub (as_seq h0 buf) (v start) (v n) (spec h0) (as_seq h1 buf)

let concat2 #a #t0 #t1 len0 s0 len1 s1 s =
  let h0 = ST.get () in
  update_sub s (size 0) len0 s0;
  update_sub s len0 len1 s1;
  let h1 = ST.get () in
  Seq.eq_intro (Seq.sub (as_seq h1 s) 0 (v len0)) (as_seq h0 s0);
  Seq.lemma_concat2 (v len0) (as_seq h0 s0) (v len1) (as_seq h0 s1) (as_seq h1 s)

let concat3 #a #t0 #t1 #t2 len0 s0 len1 s1 len2 s2 s =
  let h0 = ST.get () in
  update_sub s (size 0) len0 s0;
  update_sub s len0 len1 s1;
  let h1 = ST.get () in
  Seq.eq_intro (Seq.sub (as_seq h1 s) 0 (v len0)) (as_seq h0 s0);
  update_sub s (len0 +! len1) len2 s2;
  let h2 = ST.get () in
  Seq.eq_intro (Seq.sub (as_seq h2 s) 0 (v len0)) (as_seq h0 s0);
  Seq.eq_intro (Seq.sub (as_seq h2 s) (v len0) (v len1)) (as_seq h0 s1);
  Seq.lemma_concat3 (v len0) (as_seq h0 s0) (v len1) (as_seq h0 s1) (v len2) (as_seq h0 s2) (as_seq h2 s)

let loop_nospec #h0 #a #len n buf impl =
  let inv h1 j = modifies (loc buf) h0 h1 in
  Lib.Loops.for (size 0) n inv impl

let loop_nospec2 #h0 #a1 #a2 #len1 #len2 n buf1 buf2 impl =
  let inv h1 j = modifies (union (loc buf1) (loc buf2)) h0 h1 in
  Lib.Loops.for (size 0) n inv impl

let loop_nospec3 #h0 #a1 #a2 #a3 #len1 #len2 #len3 n buf1 buf2 buf3 impl =
  let inv h1 j = modifies (union (loc buf3) (union (loc buf1) (loc buf2))) h0 h1 in
  Lib.Loops.for (size 0) n inv impl

let loop_range_nospec #h0 #a #len start n buf impl =
  let inv h1 j = modifies (loc buf) h0 h1 in
  Lib.Loops.for start (start +. n) inv impl

#set-options "--max_fuel 1"

let loop h0 n a_spec refl footprint spec impl =
  let inv h i = loop_inv h0 n a_spec refl footprint spec i h in
  Lib.Loops.for (size 0) n inv impl

let loop_refl h0 n a_spec refl footprint spec impl =
  let inv h i = loop_refl_inv h0 n a_spec refl footprint spec i h in
  Lib.Loops.for (size 0) n inv impl

let loop1 #b #blen h0 n acc spec impl =
  let inv h i = loop1_inv h0 n b blen acc spec i h in
  Lib.Loops.for (size 0) n inv impl

let loop2 #b0 #blen0 #b1 #blen1 h0 n acc0 acc1 spec impl =
  let inv h i = loop2_inv #b0 #blen0 #b1 #blen1 h0 n acc0 acc1 spec i h in
  Lib.Loops.for (size 0) n inv impl

#set-options "--max_fuel 0"

let salloc1_with_inv #a #res h len x footprint spec spec_inv impl =
  let h0 = ST.get() in
  push_frame();
  let h1 = ST.get() in
  B.fresh_frame_modifies h0 h1;
  let b = B.alloca x len in
  let h2 = ST.get() in
  let r = impl b in
  let h3 = ST.get() in
  Lib.Memzero0.memzero #a b len;
  let h4 = ST.get() in
  pop_frame();
  let h5 = ST.get() in
  B.popped_modifies h4 h5;
  spec_inv h2 h3 h5 r;
  r

inline_for_extraction 
let salloc1 #a #res h len x footprint spec impl =
  salloc1_with_inv #a #res h len x footprint spec
    (fun h1 h2 h3 (r:res) -> assert (spec r h2); assert (spec r h3))
    impl

inline_for_extraction 
let salloc_nospec #a #res h len x footprint impl =
  salloc1 #a #res h len x footprint (fun _ _ -> True) impl

inline_for_extraction 
val loopi_blocks_f:
    #a:Type0
  -> #b:Type0
  -> #blen:size_t
  -> blocksize:size_t{v blocksize > 0}
  -> inpLen:size_t
  -> inp:lbuffer a inpLen
  -> spec_f:(i:nat{i < v inpLen / v blocksize}
              -> Seq.lseq a (v blocksize)
              -> Seq.lseq b (v blen)
              -> Seq.lseq b (v blen))
  -> f:(i:size_t{v i < v inpLen / v blocksize}
       -> inp:lbuffer a blocksize
       -> w:lbuffer b blen -> Stack unit
          (requires fun h ->
            live h inp /\ live h w /\ disjoint inp w)
          (ensures  fun h0 _ h1 ->
            modifies (loc w) h0 h1 /\
            as_seq h1 w == spec_f (v i) (as_seq h0 inp) (as_seq h0 w)))
  -> nb:size_t{v nb == v inpLen / v blocksize}
  -> i:size_t{v i < v nb}
  -> w:lbuffer b blen ->
  Stack unit
    (requires fun h -> live h inp /\ live h w /\ disjoint inp w)
    (ensures  fun h0 _ h1 ->
      modifies (loc w) h0 h1 /\
      as_seq h1 w ==
      Sequence.repeati_blocks_f (v blocksize) (as_seq h0 inp) spec_f (v nb) (v i) (as_seq h0 w))

let loopi_blocks_f #a #b #blen bs inpLen inp spec_f f nb i w =
  Math.Lemmas.lemma_mult_le_right (v bs) (v i) (v nb);
  assert ((v i + 1) * v bs == v i * v bs + v bs);
  assert (v i * v bs + v bs <= v nb * v bs);
  assert (v nb * v bs <= v inpLen);
  let block = sub inp (i *! bs) bs in
  f i block w

inline_for_extraction 
val loopi_blocks_f_nospec:
    #a:Type0
  -> #b:Type0
  -> #blen:size_t
  -> blocksize:size_t{v blocksize > 0}
  -> inpLen:size_t
  -> inp:lbuffer a inpLen
  -> f:(i:size_t{v i < v inpLen / v blocksize}
       -> inp:lbuffer a blocksize
       -> w:lbuffer b blen -> Stack unit
          (requires fun h ->
            live h inp /\ live h w /\ disjoint inp w)
          (ensures  fun h0 _ h1 ->
            modifies (loc w) h0 h1))
  -> nb:size_t{v nb == v inpLen / v blocksize}
  -> i:size_t{v i < v nb}
  -> w:lbuffer b blen ->
  Stack unit
    (requires fun h -> live h inp /\ live h w /\ disjoint inp w)
    (ensures  fun h0 _ h1 -> modifies (loc w) h0 h1)

#set-options "--z3rlimit 300 --max_fuel 0"

let loopi_blocks_f_nospec #a #b #blen bs inpLen inp f nb i w =
  assert ((v i + 1) * v bs <= v nb * v bs);
  let block = sub inp (i *! bs) bs in
  f i block w

let loopi_blocks #a #b #blen bs inpLen inp spec_f spec_l f l w =
  let nb = inpLen /. bs in
  let rem = inpLen %. bs in
  [@ inline_let]
  let spec_fh h0 = Seq.repeati_blocks_f (v bs) (as_seq h0 inp) spec_f (v nb) in
  let h0 = ST.get () in
  loop1 #b #blen h0 nb w spec_fh
  (fun i ->
    Loop.unfold_repeati (v nb) (spec_fh h0) (as_seq h0 w) (v i);
    loopi_blocks_f #a #b #blen bs inpLen inp spec_f f nb i w);
  let last = sub inp (nb *! bs) rem in
  l nb rem last w

let loopi_blocks_nospec #a #b #blen bs inpLen inp f l w =
  let nb = inpLen /. bs in
  let rem = inpLen %. bs in
  let h0 = ST.get () in
  loop_nospec #h0 #b #blen nb w
  (fun i -> loopi_blocks_f_nospec #a #b #blen bs inpLen inp f nb i w);
  let last = sub inp (nb *. bs) rem in
  l nb rem last w

inline_for_extraction 
val loop_blocks_f:
    #a:Type0
  -> #b:Type0
  -> #blen:size_t
  -> blocksize:size_t{v blocksize > 0}
  -> inpLen:size_t
  -> inp:lbuffer a inpLen
  -> spec_f:(Seq.lseq a (v blocksize)
              -> Seq.lseq b (v blen)
              -> Seq.lseq b (v blen))
  -> f:(inp:lbuffer a blocksize
       -> w:lbuffer b blen -> Stack unit
          (requires fun h ->
            live h inp /\ live h w /\ disjoint inp w)
          (ensures  fun h0 _ h1 ->
            modifies (loc w) h0 h1 /\
            as_seq h1 w == spec_f (as_seq h0 inp) (as_seq h0 w)))
  -> nb:size_t{v nb == v inpLen / v blocksize}
  -> i:size_t{v i < v nb}
  -> w:lbuffer b blen ->
  Stack unit
    (requires fun h -> live h inp /\ live h w /\ disjoint inp w)
    (ensures  fun h0 _ h1 ->
      modifies (loc w) h0 h1 /\
      as_seq h1 w ==
      Sequence.repeat_blocks_f (v blocksize) (as_seq h0 inp) spec_f (v nb) (v i) (as_seq h0 w))

let loop_blocks_f #a #b #blen bs inpLen inp spec_f f nb i w =
  assert ((v i + 1) * v bs <= v nb * v bs);
  let block = sub inp (i *! bs) bs in
  f block w

#set-options "--z3rlimit 400 --fuel 1"

let loop_blocks_multi #a #b #blen bs nb inp spec_f f w =
  [@ inline_let]
  let spec_fh h0 = Seq.repeat_blocks_f (v bs) (as_seq h0 inp) spec_f (v nb) in
  let h0 = ST.get () in
  loop1 #b #blen h0 nb w spec_fh
    (fun i ->
      Loop.unfold_repeati (v nb) (spec_fh h0) (as_seq h0 w) (v i);
      loop_blocks_f #a #b #blen bs (bs *! nb) inp spec_f f nb i w)

let loop_blocks #a #b #blen bs nb rem inp spec_f spec_l f l w =
  [@ inline_let]
  let spec_fh h0 = Seq.repeat_blocks_f (v bs) (as_seq h0 inp) spec_f (v nb) in
  let h0 = ST.get () in
  loop1 #b #blen h0 nb w spec_fh
  (fun i ->
    Loop.unfold_repeati (v nb) (spec_fh h0) (as_seq h0 w) (v i);
    loop_blocks_f #a #b #blen bs (bs *! nb +! rem) inp spec_f f nb i w);
  let last = sub inp (nb *! bs) rem in
  l rem last w
val fill_blocks:
    #t:Type0
  -> h0:mem
  -> len:size_t
  -> n:size_t{v n * v len <= max_size_t}
  -> output:lbuffer t (n *! len)
  -> a_spec:(i:size_nat{i <= v n} -> Type)
  -> refl:(mem -> i:size_nat{i <= v n} -> GTot (a_spec i))
  -> footprint:(i:size_nat{i <= v n} -> GTot
      (l:B.loc{B.loc_disjoint l (loc output) /\
               B.address_liveness_insensitive_locs `B.loc_includes` l}))
  -> spec:(mem -> GTot (i:size_nat{i < v n} -> a_spec i -> a_spec (i + 1) & Seq.lseq t (v len)))
  -> impl:(i:size_t{v i < v n} -> Stack unit
      (requires fun h1 ->
        (v i + 1) * v len <= max_size_t /\
        modifies (footprint (v i) |+| loc (gsub output 0ul (i *! len))) h0 h1)
      (ensures  fun h1 _ h2 ->
        (let block = gsub output (i *! len) len in
        let s, b = spec h0 (v i) (refl h1 (v i)) in
        footprint (v i + 1) `B.loc_includes` footprint (v i) /\
        B.modifies (B.loc_union (footprint (v i + 1)) (loc block)) h1 h2 /\
        refl h2 (v i + 1) == s /\ as_seq h2 block == b))) ->
  Stack unit
    (requires fun h -> h0 == h /\ live h output)
    (ensures  fun _ _ h1 ->
      B.modifies (B.loc_union (footprint (v n)) (loc output)) h0 h1 /\
     (let s, o = Seq.generate_blocks (v len) (v n) (v n) a_spec (spec h0) (refl h0 0) in
      refl h1 (v n) == s /\
      as_seq #_ #t h1 output == o))

    h0: FStar.Monotonic.HyperStack.mem ->
    len: Lib.IntTypes.size_t ->
    n: Lib.IntTypes.size_t{Lib.IntTypes.v n * Lib.IntTypes.v len <= Lib.IntTypes.max_size_t} ->
    output: Lib.Buffer.lbuffer t (n *! len) ->
    a_spec: (i: Lib.IntTypes.size_nat{i <= Lib.IntTypes.v n} -> Type) ->
    refl:
      (_: FStar.Monotonic.HyperStack.mem -> i: Lib.IntTypes.size_nat{i <= Lib.IntTypes.v n}
          -> Prims.GTot (a_spec i)) ->
    footprint:
      (i: Lib.IntTypes.size_nat{i <= Lib.IntTypes.v n}
          -> Prims.GTot
            (l:
              LowStar.Monotonic.Buffer.loc
                { LowStar.Monotonic.Buffer.loc_disjoint l (Lib.Buffer.loc output) /\
                  LowStar.Monotonic.Buffer.loc_includes LowStar.Monotonic.Buffer.address_liveness_insensitive_locs
                    l })) ->
    spec:
      (_: FStar.Monotonic.HyperStack.mem
          -> Prims.GTot
            (i: Lib.IntTypes.size_nat{i < Lib.IntTypes.v n} -> _: a_spec i
                -> a_spec (i + 1) * Lib.Sequence.lseq t (Lib.IntTypes.v len))) ->
    impl:
      (i: Lib.IntTypes.size_t{Lib.IntTypes.v i < Lib.IntTypes.v n}
          -> FStar.HyperStack.ST.Stack Prims.unit)
  -> FStar.HyperStack.ST.Stack Prims.unit