val poly1305_heap_blocks (h:int) (pad:int) (r:int) (s:Seq.seq nat64) (k:int) : int
let poly1305_heap_blocks h pad r s k =
  if 0 <= k && k <= Seq.length s && k % 2 = 0 then
    poly1305_heap_blocks' h pad r s k
  else
    0
val poly1305_heap_blocks (h:int) (pad:int) (r:int) (s:Seq.seq nat64) (k:int) : int
let poly1305_heap_blocks h pad r s k =
if 0 <= k && k <= Seq.length s && k % 2 = 0 then poly1305_heap_blocks' h pad r s k else 0
Vale.Poly1305.Util.fst.checked
Vale.X64.State.fsti.checked Vale.X64.Memory.fsti.checked Vale.Poly1305.Bitvectors.fsti.checked prims.fst.checked FStar.Tactics.Canon.fst.checked FStar.Tactics.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lib.fst.checked FStar.Math.Lemmas.fst.checked
Vale.Poly1305.Util.fst
Prims.int FStar.Seq.Base.seq Vale.X64.Memory.nat64 Prims.op_AmpAmp Prims.op_LessThanOrEqual FStar.Seq.Base.length Prims.op_Equality Prims.op_Modulus Vale.Poly1305.Util.poly1305_heap_blocks' Prims.bool
module Vale.Poly1305.Util

open FStar.Tactics
open FStar.Tactics.Canon
open FStar.Math.Lemmas
open FStar.Math.Lib
open FStar.Mul
open Vale.X64.State   // needed for mem
open Vale.Poly1305.Bitvectors
open Vale.X64.Memory

//#reset-options "--z3cliopt smt.QI.EAGER_THRESHOLD=100 --z3cliopt smt.CASE_SPLIT=3 --z3cliopt smt.arith.nl=false --max_fuel 0 --max_ifuel 0 --smtencoding.elim_box true --eager_inference --smtencoding.nl_arith_repr wrapped --smtencoding.l_arith_repr native"

(* Getting a weird error otherwise, will file an issue
   when this gets merged in fstar branch *)
val poly1305_heap_blocks (h:int) (pad:int) (r:int) (s:Seq.seq nat64) (k:int) : int

    h: Prims.int ->
    pad: Prims.int ->
    r: Prims.int ->
    s: FStar.Seq.Base.seq Vale.X64.Memory.nat64 ->
    k: Prims.int
  -> Prims.int