val load_acc2:
    acc:felem 2
  -> b:lbuffer uint8 32ul
  -> Stack unit
    (requires fun h ->
      live h acc /\ live h b /\ disjoint acc b /\
      felem_fits h acc (2, 2, 2, 2, 2))
    (ensures  fun h0 _ h1 ->
      modifies (loc acc) h0 h1 /\
      felem_fits h1 acc (3, 3, 3, 3, 3) /\
      feval h1 acc == Vec.load_acc2 (as_seq h0 b) (feval h0 acc).[0])
let load_acc2 acc b =
  push_frame();
  let e = create 5ul (zero 2) in
  load_blocks e b;

  let acc0 = acc.(0ul) in
  let acc1 = acc.(1ul) in
  let acc2 = acc.(2ul) in
  let acc3 = acc.(3ul) in
  let acc4 = acc.(4ul) in
  let e0 = e.(0ul) in
  let e1 = e.(1ul) in
  let e2 = e.(2ul) in
  let e3 = e.(3ul) in
  let e4 = e.(4ul) in

  let (acc0, acc1, acc2, acc3, acc4) =
    load_acc5_2 (acc0, acc1, acc2, acc3, acc4) (e0, e1, e2, e3, e4) in
  acc.(0ul) <- acc0;
  acc.(1ul) <- acc1;
  acc.(2ul) <- acc2;
  acc.(3ul) <- acc3;
  acc.(4ul) <- acc4;
  pop_frame()
val load_acc2:
    acc:felem 2
  -> b:lbuffer uint8 32ul
  -> Stack unit
    (requires fun h ->
      live h acc /\ live h b /\ disjoint acc b /\
      felem_fits h acc (2, 2, 2, 2, 2))
    (ensures  fun h0 _ h1 ->
      modifies (loc acc) h0 h1 /\
      felem_fits h1 acc (3, 3, 3, 3, 3) /\
      feval h1 acc == Vec.load_acc2 (as_seq h0 b) (feval h0 acc).[0])
let load_acc2 acc b =
push_frame ();
let e = create 5ul (zero 2) in
load_blocks e b;
let acc0 = acc.(0ul) in
let acc1 = acc.(1ul) in
let acc2 = acc.(2ul) in
let acc3 = acc.(3ul) in
let acc4 = acc.(4ul) in
let e0 = e.(0ul) in
let e1 = e.(1ul) in
let e2 = e.(2ul) in
let e3 = e.(3ul) in
let e4 = e.(4ul) in
let acc0, acc1, acc2, acc3, acc4 =
  load_acc5_2 (acc0, acc1, acc2, acc3, acc4) (e0, e1, e2, e3, e4)
in
acc.(0ul) <- acc0;
acc.(1ul) <- acc1;
acc.(2ul) <- acc2;
acc.(3ul) <- acc3;
acc.(4ul) <- acc4;
pop_frame ()
Hacl.Impl.Poly1305.Field32xN_128.fst.checked
prims.fst.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.Poly1305.Vec.fst.checked Hacl.Spec.Poly1305.Field32xN.Lemmas.fst.checked Hacl.Spec.Poly1305.Field32xN.fst.checked Hacl.Impl.Poly1305.Field32xN.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.All.fst.checked FStar.HyperStack.fst.checked
Hacl.Impl.Poly1305.Field32xN_128.fst
Hacl.Impl.Poly1305.Field32xN.felem Lib.Buffer.lbuffer Lib.IntTypes.uint8 FStar.UInt32.__uint_to_t Hacl.Spec.Poly1305.Field32xN.uint64xN FStar.HyperStack.ST.pop_frame Prims.unit Lib.Buffer.op_Array_Assignment Hacl.Spec.Poly1305.Field32xN.felem5 Hacl.Spec.Poly1305.Field32xN.load_acc5_2 FStar.Pervasives.Native.Mktuple5 Lib.Buffer.op_Array_Access Lib.Buffer.MUT Hacl.Impl.Poly1305.Field32xN.load_blocks Lib.Buffer.lbuffer_t FStar.UInt32.uint_to_t FStar.UInt32.t Lib.Buffer.create Hacl.Spec.Poly1305.Field32xN.zero FStar.HyperStack.ST.push_frame
module Hacl.Impl.Poly1305.Field32xN_128

open FStar.HyperStack
open FStar.HyperStack.All
open FStar.Mul

open Lib.IntTypes
open Lib.Buffer

include Hacl.Spec.Poly1305.Field32xN
open Hacl.Spec.Poly1305.Field32xN.Lemmas

module Vec = Hacl.Spec.Poly1305.Vec
module ST = FStar.HyperStack.ST

open Hacl.Impl.Poly1305.Field32xN

/// See comments in Hacl.Impl.Poly1305.Field32xN_256

#set-options "--max_fuel 0 --max_ifuel 0 --z3rlimit 50 --using_facts_from '* -FStar.Seq'"


val load_acc2:
    acc:felem 2
  -> b:lbuffer uint8 32ul
  -> Stack unit
    (requires fun h ->
      live h acc /\ live h b /\ disjoint acc b /\
      felem_fits h acc (2, 2, 2, 2, 2))
    (ensures  fun h0 _ h1 ->
      modifies (loc acc) h0 h1 /\
      felem_fits h1 acc (3, 3, 3, 3, 3) /\
      feval h1 acc == Vec.load_acc2 (as_seq h0 b) (feval h0 acc).[0])
val load_acc2:
    acc:felem 2
  -> b:lbuffer uint8 32ul
  -> Stack unit
    (requires fun h ->
      live h acc /\ live h b /\ disjoint acc b /\
      felem_fits h acc (2, 2, 2, 2, 2))
    (ensures  fun h0 _ h1 ->
      modifies (loc acc) h0 h1 /\
      felem_fits h1 acc (3, 3, 3, 3, 3) /\
      feval h1 acc == Vec.load_acc2 (as_seq h0 b) (feval h0 acc).[0])
acc: Hacl.Impl.Poly1305.Field32xN.felem 2 -> b: Lib.Buffer.lbuffer Lib.IntTypes.uint8 32ul
  -> FStar.HyperStack.ST.Stack Prims.unit