val fmul_precomp_inv_zeros: #s:field_spec -> precomp_b:lbuffer (limb s) (precomplen s) -> h:mem ->
  Lemma
  (requires as_seq h precomp_b == Lib.Sequence.create (v (precomplen s)) (limb_zero s))
  (ensures  F32xN.fmul_precomp_r_pre #(width s) h precomp_b)
let fmul_precomp_inv_zeros #s precomp_b h =
  let r_b = gsub precomp_b 0ul (nlimb s) in
  let r_b5 = gsub precomp_b (nlimb s) (nlimb s) in
  as_seq_gsub h precomp_b 0ul (nlimb s);
  as_seq_gsub h precomp_b (nlimb s) (nlimb s);

  Hacl.Spec.Poly1305.Field32xN.Lemmas.precomp_r5_zeros (width s);
  LSeq.eq_intro (feval h r_b) (LSeq.create (width s) 0);
  LSeq.eq_intro (feval h r_b5) (LSeq.create (width s) 0);
  assert (F32xN.as_tup5 #(width s) h r_b5 == F32xN.precomp_r5 (F32xN.as_tup5 h r_b))
val fmul_precomp_inv_zeros: #s:field_spec -> precomp_b:lbuffer (limb s) (precomplen s) -> h:mem ->
  Lemma
  (requires as_seq h precomp_b == Lib.Sequence.create (v (precomplen s)) (limb_zero s))
  (ensures  F32xN.fmul_precomp_r_pre #(width s) h precomp_b)
let fmul_precomp_inv_zeros #s precomp_b h =
let r_b = gsub precomp_b 0ul (nlimb s) in
let r_b5 = gsub precomp_b (nlimb s) (nlimb s) in
as_seq_gsub h precomp_b 0ul (nlimb s);
as_seq_gsub h precomp_b (nlimb s) (nlimb s);
Hacl.Spec.Poly1305.Field32xN.Lemmas.precomp_r5_zeros (width s);
LSeq.eq_intro (feval h r_b) (LSeq.create (width s) 0);
LSeq.eq_intro (feval h r_b5) (LSeq.create (width s) 0);
assert (F32xN.as_tup5 #(width s) h r_b5 == F32xN.precomp_r5 (F32xN.as_tup5 h r_b))
Hacl.Impl.Poly1305.fst.checked
Spec.Poly1305.fst.checked prims.fst.checked Meta.Attribute.fst.checked Lib.Sequence.fsti.checked Lib.Loops.fsti.checked Lib.LoopCombinators.fst.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Lib.ByteBuffer.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.Poly1305.Vec.fst.checked Hacl.Spec.Poly1305.Field32xN.Lemmas.fst.checked Hacl.Spec.Poly1305.Equiv.fst.checked Hacl.Impl.Poly1305.Lemmas.fst.checked Hacl.Impl.Poly1305.Fields.fst.checked Hacl.Impl.Poly1305.Field32xN.fst.checked Hacl.Impl.Poly1305.Bignum128.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.All.fst.checked FStar.HyperStack.fst.checked
Hacl.Impl.Poly1305.fst
Hacl.Impl.Poly1305.Fields.field_spec Lib.Buffer.lbuffer Hacl.Impl.Poly1305.Fields.limb Hacl.Impl.Poly1305.Fields.precomplen FStar.Monotonic.HyperStack.mem Prims._assert Prims.eq2 Hacl.Spec.Poly1305.Field32xN.felem5 Hacl.Impl.Poly1305.Fields.width Hacl.Impl.Poly1305.Field32xN.as_tup5 Hacl.Spec.Poly1305.Field32xN.precomp_r5 Prims.unit Lib.Sequence.eq_intro Spec.Poly1305.felem Hacl.Impl.Poly1305.Fields.feval Lib.Sequence.create Hacl.Spec.Poly1305.Field32xN.Lemmas.precomp_r5_zeros Lib.Buffer.as_seq_gsub Lib.Buffer.MUT Hacl.Impl.Poly1305.Fields.nlimb FStar.UInt32.__uint_to_t Lib.Buffer.lbuffer_t Hacl.Spec.Poly1305.Field32xN.uint64xN FStar.UInt32.uint_to_t FStar.UInt32.t Lib.Buffer.gsub
module Hacl.Impl.Poly1305

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

open Lib.IntTypes
open Lib.Buffer
open Lib.ByteBuffer

open Hacl.Impl.Poly1305.Fields
open Hacl.Impl.Poly1305.Bignum128

module ST = FStar.HyperStack.ST
module BSeq = Lib.ByteSequence
module LSeq = Lib.Sequence

module S = Spec.Poly1305
module Vec = Hacl.Spec.Poly1305.Vec
module Equiv = Hacl.Spec.Poly1305.Equiv
module F32xN = Hacl.Impl.Poly1305.Field32xN

friend Lib.LoopCombinators


let _: squash (inversion field_spec) = allow_inversion field_spec


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

inline_for_extraction noextract
let get_acc #s (ctx:poly1305_ctx s) : Stack (felem s)
  (requires fun h -> live h ctx)
  (ensures  fun h0 acc h1 -> h0 == h1 /\ live h1 acc /\ acc == gsub ctx 0ul (nlimb s))
  = sub ctx 0ul (nlimb s)


inline_for_extraction noextract
let get_precomp_r #s (ctx:poly1305_ctx s) : Stack (precomp_r s)
  (requires fun h -> live h ctx)
  (ensures  fun h0 pre h1 -> h0 == h1 /\ live h1 pre /\ pre == gsub ctx (nlimb s) (precomplen s))
  = sub ctx (nlimb s) (precomplen s)


unfold
let op_String_Access #a #len = LSeq.index #a #len

let as_get_acc #s h ctx = (feval h (gsub ctx 0ul (nlimb s))).[0]

let as_get_r #s h ctx = (feval h (gsub ctx (nlimb s) (nlimb s))).[0]

let state_inv_t #s h ctx =
  felem_fits h (gsub ctx 0ul (nlimb s)) (2, 2, 2, 2, 2) /\
  F32xN.load_precompute_r_post #(width s) h (gsub ctx (nlimb s) (precomplen s))


#reset-options "--z3rlimit 100 --max_fuel 0 --max_ifuel 0 --record_options"
let reveal_ctx_inv' #s ctx ctx' h0 h1 =
  let acc_b = gsub ctx 0ul (nlimb s) in
  let acc_b' = gsub ctx' 0ul (nlimb s) in
  let r_b = gsub ctx (nlimb s) (nlimb s) in
  let r_b' = gsub ctx' (nlimb s) (nlimb s) in
  let precom_b = gsub ctx (nlimb s) (precomplen s) in
  let precom_b' = gsub ctx' (nlimb s) (precomplen s) in
  as_seq_gsub h0 ctx 0ul (nlimb s);
  as_seq_gsub h1 ctx 0ul (nlimb s);
  as_seq_gsub h0 ctx (nlimb s) (nlimb s);
  as_seq_gsub h1 ctx (nlimb s) (nlimb s);
  as_seq_gsub h0 ctx (nlimb s) (precomplen s);
  as_seq_gsub h1 ctx (nlimb s) (precomplen s);
  as_seq_gsub h0 ctx' 0ul (nlimb s);
  as_seq_gsub h1 ctx' 0ul (nlimb s);
  as_seq_gsub h0 ctx' (nlimb s) (nlimb s);
  as_seq_gsub h1 ctx' (nlimb s) (nlimb s);
  as_seq_gsub h0 ctx' (nlimb s) (precomplen s);
  as_seq_gsub h1 ctx' (nlimb s) (precomplen s);
  assert (as_seq h0 acc_b == as_seq h1 acc_b');
  assert (as_seq h0 r_b == as_seq h1 r_b');
  assert (as_seq h0 precom_b == as_seq h1 precom_b')


val fmul_precomp_inv_zeros: #s:field_spec -> precomp_b:lbuffer (limb s) (precomplen s) -> h:mem ->
  Lemma
  (requires as_seq h precomp_b == Lib.Sequence.create (v (precomplen s)) (limb_zero s))
  (ensures  F32xN.fmul_precomp_r_pre #(width s) h precomp_b)
val fmul_precomp_inv_zeros: #s:field_spec -> precomp_b:lbuffer (limb s) (precomplen s) -> h:mem ->
  Lemma
  (requires as_seq h precomp_b == Lib.Sequence.create (v (precomplen s)) (limb_zero s))
  (ensures  F32xN.fmul_precomp_r_pre #(width s) h precomp_b)

    precomp_b:
      Lib.Buffer.lbuffer (Hacl.Impl.Poly1305.Fields.limb s) (Hacl.Impl.Poly1305.Fields.precomplen s) ->
    h: FStar.Monotonic.HyperStack.mem
  -> FStar.Pervasives.Lemma
      (requires
        Lib.Buffer.as_seq h precomp_b ==
        Lib.Sequence.create (Lib.IntTypes.v (Hacl.Impl.Poly1305.Fields.precomplen s))
          (Hacl.Impl.Poly1305.Fields.limb_zero s))
      (ensures Hacl.Impl.Poly1305.Field32xN.fmul_precomp_r_pre h precomp_b)