val va_req_Poly1305
      (va_b0: va_code)
      (va_s0: va_state)
      (win: bool)
      (ctx_b inp_b: buffer64)
      (len_in finish_in: nat64)
    : prop
let va_req_Poly1305 (va_b0:va_code) (va_s0:va_state) (win:bool) (ctx_b:buffer64) (inp_b:buffer64)
  (len_in:nat64) (finish_in:nat64) : prop =
  (va_require_total va_b0 (va_code_Poly1305 win) va_s0 /\ va_get_ok va_s0 /\ (let
    (ctx_in:(va_int_range 0 18446744073709551615)) = (if win then va_get_reg64 rRcx va_s0 else
    va_get_reg64 rRdi va_s0) in let (inp_in:(va_int_range 0 18446744073709551615)) = (if win then
    va_get_reg64 rRdx va_s0 else va_get_reg64 rRsi va_s0) in let (n:(va_int_range
    18446744073709551616 18446744073709551616)) = 18446744073709551616 in let (p:(va_int_range
    1361129467683753853853498429727072845819 1361129467683753853853498429727072845819)) =
    va_mul_nat n n `op_Multiply` 4 - 5 in va_get_reg64 rRsp va_s0 == Vale.X64.Stack_i.init_rsp
    (va_get_stack va_s0) /\ Vale.X64.Memory.is_initial_heap (va_get_mem_layout va_s0) (va_get_mem
    va_s0) /\ Vale.X64.Decls.buffers_disjoint ctx_b inp_b /\ Vale.X64.Decls.validDstAddrs64
    (va_get_mem va_s0) ctx_in ctx_b 24 (va_get_mem_layout va_s0) Public /\
    Vale.X64.Decls.validSrcAddrs64 (va_get_mem va_s0) inp_in inp_b
    (Vale.Poly1305.Util.readable_words len_in) (va_get_mem_layout va_s0) Public /\ len_in == (if
    win then va_get_reg64 rR8 va_s0 else va_get_reg64 rRdx va_s0) /\ finish_in == (if win then
    va_get_reg64 rR9 va_s0 else va_get_reg64 rRcx va_s0) /\ (let h2_in =
    Vale.X64.Decls.buffer64_read ctx_b 2 (va_get_mem va_s0) in h2_in < 5 /\ inp_in + len_in <
    pow2_64 /\ finish_in < 2)))
val va_req_Poly1305
      (va_b0: va_code)
      (va_s0: va_state)
      (win: bool)
      (ctx_b inp_b: buffer64)
      (len_in finish_in: nat64)
    : prop
let va_req_Poly1305
      (va_b0: va_code)
      (va_s0: va_state)
      (win: bool)
      (ctx_b inp_b: buffer64)
      (len_in finish_in: nat64)
    : prop =
(va_require_total va_b0 (va_code_Poly1305 win) va_s0 /\ va_get_ok va_s0 /\
  (let ctx_in:(va_int_range 0 18446744073709551615) =
      (if win then va_get_reg64 rRcx va_s0 else va_get_reg64 rRdi va_s0)
    in
    let inp_in:(va_int_range 0 18446744073709551615) =
      (if win then va_get_reg64 rRdx va_s0 else va_get_reg64 rRsi va_s0)
    in
    let n:(va_int_range 18446744073709551616 18446744073709551616) = 18446744073709551616 in
    let p:(va_int_range 1361129467683753853853498429727072845819
        1361129467683753853853498429727072845819) =
      (va_mul_nat n n) `op_Multiply` 4 - 5
    in
    va_get_reg64 rRsp va_s0 == Vale.X64.Stack_i.init_rsp (va_get_stack va_s0) /\
    Vale.X64.Memory.is_initial_heap (va_get_mem_layout va_s0) (va_get_mem va_s0) /\
    Vale.X64.Decls.buffers_disjoint ctx_b inp_b /\
    Vale.X64.Decls.validDstAddrs64 (va_get_mem va_s0)
      ctx_in
      ctx_b
      24
      (va_get_mem_layout va_s0)
      Public /\
    Vale.X64.Decls.validSrcAddrs64 (va_get_mem va_s0)
      inp_in
      inp_b
      (Vale.Poly1305.Util.readable_words len_in)
      (va_get_mem_layout va_s0)
      Public /\ len_in == (if win then va_get_reg64 rR8 va_s0 else va_get_reg64 rRdx va_s0) /\
    finish_in == (if win then va_get_reg64 rR9 va_s0 else va_get_reg64 rRcx va_s0) /\
    (let h2_in = Vale.X64.Decls.buffer64_read ctx_b 2 (va_get_mem va_s0) in
      h2_in < 5 /\ inp_in + len_in < pow2_64 /\ finish_in < 2)))
Vale.Poly1305.X64.fsti.checked
Vale.X64.State.fsti.checked Vale.X64.Stack_i.fsti.checked Vale.X64.QuickCodes.fsti.checked Vale.X64.QuickCode.fst.checked Vale.X64.Memory.fsti.checked Vale.X64.Machine_s.fst.checked Vale.X64.InsStack.fsti.checked Vale.X64.InsMem.fsti.checked Vale.X64.InsBasic.fsti.checked Vale.X64.Flags.fsti.checked Vale.X64.Decls.fsti.checked Vale.Poly1305.Util.fsti.checked Vale.Poly1305.Spec_s.fst.checked Vale.Poly1305.Math.fsti.checked Vale.Def.Types_s.fst.checked Vale.Def.Opaque_s.fsti.checked Vale.Arch.Types.fsti.checked Vale.Arch.HeapImpl.fsti.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Vale.Poly1305.X64.fsti
Vale.X64.Decls.va_code Vale.X64.Decls.va_state Prims.bool Vale.X64.Memory.buffer64 Vale.X64.Memory.nat64 Prims.l_and Vale.X64.Decls.va_require_total Vale.Poly1305.X64.va_code_Poly1305 Prims.b2t Vale.X64.Decls.va_get_ok Prims.eq2 Vale.Def.Words_s.nat64 Vale.X64.Decls.va_get_reg64 Vale.X64.Machine_s.rRsp Vale.X64.Stack_i.init_rsp Vale.X64.Decls.va_get_stack Vale.X64.Memory.is_initial_heap Vale.X64.Decls.va_get_mem_layout Vale.X64.Decls.va_get_mem Vale.X64.Decls.buffers_disjoint Vale.X64.Decls.validDstAddrs64 Vale.Arch.HeapTypes_s.Public Vale.X64.Decls.validSrcAddrs64 Vale.Poly1305.Util.readable_words Vale.X64.Machine_s.rR8 Vale.X64.Machine_s.rRdx Vale.X64.Machine_s.rR9 Vale.X64.Machine_s.rRcx Prims.op_LessThan Prims.op_Addition Vale.X64.Machine_s.pow2_64 Vale.X64.Decls.buffer64_read Vale.X64.Decls.va_int_range Prims.op_Subtraction Prims.op_Multiply Vale.X64.Decls.va_mul_nat Vale.X64.Machine_s.rRsi Vale.X64.Machine_s.rRdi Prims.prop
module Vale.Poly1305.X64
open Vale.Def.Opaque_s
open Vale.Def.Types_s
open Vale.Arch.Types
open Vale.Arch.HeapImpl
open Vale.X64.Machine_s
open Vale.X64.Memory
open Vale.X64.Stack_i
open Vale.X64.State
open Vale.X64.Decls
open Vale.X64.InsBasic
open Vale.X64.InsMem
open Vale.X64.InsStack
open Vale.X64.QuickCode
open Vale.X64.QuickCodes
open Vale.Poly1305.Spec_s
open Vale.Poly1305.Math
open Vale.Poly1305.Util
#reset-options "--z3rlimit 40"
//-- Poly1305

val va_code_Poly1305 : win:bool -> Tot va_code

val va_codegen_success_Poly1305 : win:bool -> Tot va_pbool
let va_req_Poly1305 (va_b0:va_code) (va_s0:va_state) (win:bool) (ctx_b:buffer64) (inp_b:buffer64)
val va_req_Poly1305
      (va_b0: va_code)
      (va_s0: va_state)
      (win: bool)
      (ctx_b inp_b: buffer64)
      (len_in finish_in: nat64)
    : prop

    va_b0: Vale.X64.Decls.va_code ->
    va_s0: Vale.X64.Decls.va_state ->
    win: Prims.bool ->
    ctx_b: Vale.X64.Memory.buffer64 ->
    inp_b: Vale.X64.Memory.buffer64 ->
    len_in: Vale.X64.Memory.nat64 ->
    finish_in: Vale.X64.Memory.nat64
  -> Prims.prop