val poly1305_update1_f:
    #s:field_spec
  -> p:precomp_r s
  -> nb:size_t
  -> len:size_t{v nb == v len / 16}
  -> text:lbuffer uint8 len
  -> i:size_t{v i < v nb}
  -> acc:felem s ->
  Stack unit
  (requires fun h ->
    live h p /\ live h text /\ live h acc /\
    disjoint acc p /\ disjoint acc text /\
    felem_fits h acc (2, 2, 2, 2, 2) /\
    F32xN.fmul_precomp_r_pre #(width s) h p)
  (ensures  fun h0 _ h1 ->
    modifies (loc acc) h0 h1 /\
    felem_fits h1 acc (2, 2, 2, 2, 2) /\
    (feval h1 acc).[0] ==
    LSeq.repeat_blocks_f #uint8 #S.felem 16
      (as_seq h0 text) (S.poly1305_update1 (feval h0 (gsub p 0ul 5ul)).[0] 16) (v nb) (v i) (feval h0 acc).[0])
let poly1305_update1_f #s pre nb len text i acc=
  assert ((v i + 1) * 16 <= v nb * 16);
  let block = sub #_ #_ #len text (i *! 16ul) 16ul in
  update1 #s pre block acc
val poly1305_update1_f:
    #s:field_spec
  -> p:precomp_r s
  -> nb:size_t
  -> len:size_t{v nb == v len / 16}
  -> text:lbuffer uint8 len
  -> i:size_t{v i < v nb}
  -> acc:felem s ->
  Stack unit
  (requires fun h ->
    live h p /\ live h text /\ live h acc /\
    disjoint acc p /\ disjoint acc text /\
    felem_fits h acc (2, 2, 2, 2, 2) /\
    F32xN.fmul_precomp_r_pre #(width s) h p)
  (ensures  fun h0 _ h1 ->
    modifies (loc acc) h0 h1 /\
    felem_fits h1 acc (2, 2, 2, 2, 2) /\
    (feval h1 acc).[0] ==
    LSeq.repeat_blocks_f #uint8 #S.felem 16
      (as_seq h0 text) (S.poly1305_update1 (feval h0 (gsub p 0ul 5ul)).[0] 16) (v nb) (v i) (feval h0 acc).[0])
let poly1305_update1_f #s pre nb len text i acc =
assert ((v i + 1) * 16 <= v nb * 16);
let block = sub #_ #_ #len text (i *! 16ul) 16ul in
update1 #s pre block acc
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 Hacl.Impl.Poly1305.Fields.precomp_r Lib.IntTypes.size_t Prims.eq2 Prims.int Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB Prims.op_Division Lib.Buffer.lbuffer Lib.IntTypes.uint8 Prims.b2t Prims.op_LessThan Hacl.Impl.Poly1305.Fields.felem Hacl.Impl.Poly1305.update1 Prims.unit Lib.Buffer.lbuffer_t Lib.Buffer.MUT Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC FStar.UInt32.uint_to_t FStar.UInt32.t Lib.Buffer.sub Lib.IntTypes.op_Star_Bang FStar.UInt32.__uint_to_t Prims._assert Prims.op_LessThanOrEqual FStar.Mul.op_Star Prims.op_Addition
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)

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 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.load_precompute_r_post #(width s) h precomp_b)

#push-options "--z3rlimit 150"
let precomp_inv_zeros #s precomp_b h =
  let r_b = gsub precomp_b 0ul (nlimb s) in
  let rn_b = gsub precomp_b (2ul *! nlimb s) (nlimb s) in
  let rn_b5 = gsub precomp_b (3ul *! nlimb s) (nlimb s) in
  as_seq_gsub h precomp_b 0ul (nlimb s);
  as_seq_gsub h precomp_b (2ul *! nlimb s) (nlimb s);
  as_seq_gsub h precomp_b (3ul *! nlimb s) (nlimb s);

  fmul_precomp_inv_zeros #s precomp_b h;

  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 rn_b) (LSeq.create (width s) 0);
  LSeq.eq_intro (feval h rn_b5) (LSeq.create (width s) 0);
  assert (F32xN.as_tup5 #(width s) h rn_b5 == F32xN.precomp_r5 (F32xN.as_tup5 h rn_b));
  assert (feval h rn_b == Vec.compute_rw (feval h r_b).[0])
#pop-options

let ctx_inv_zeros #s ctx h =
  // ctx = [acc_b; r_b; r_b5; rn_b; rn_b5]
  let acc_b = gsub ctx 0ul (nlimb s) in
  as_seq_gsub h ctx 0ul (nlimb s);
  LSeq.eq_intro (feval h acc_b) (LSeq.create (width s) 0);
  assert (felem_fits h acc_b (2, 2, 2, 2, 2));

  let precomp_b = gsub ctx (nlimb s) (precomplen s) in
  LSeq.eq_intro (as_seq h precomp_b) (Lib.Sequence.create (v (precomplen s)) (limb_zero s));
  precomp_inv_zeros #s precomp_b h


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

inline_for_extraction noextract
val poly1305_encode_block:
    #s:field_spec
  -> f:felem s
  -> b:lbuffer uint8 16ul ->
  Stack unit
  (requires fun h ->
    live h b /\ live h f /\ disjoint b f)
  (ensures  fun h0 _ h1 ->
    modifies (loc f) h0 h1 /\
    felem_fits h1 f (1, 1, 1, 1, 1) /\
    (feval h1 f).[0] == S.encode 16 (as_seq h0 b))

let poly1305_encode_block #s f b =
  load_felem_le f b;
  set_bit128 f


inline_for_extraction noextract
val poly1305_encode_blocks:
    #s:field_spec
  -> f:felem s
  -> b:lbuffer uint8 (blocklen s) ->
  Stack unit
  (requires fun h ->
    live h b /\ live h f /\ disjoint b f)
  (ensures  fun h0 _ h1 ->
    modifies (loc f) h0 h1 /\
    felem_fits h1 f (1, 1, 1, 1, 1) /\
    feval h1 f == Vec.load_blocks #(width s) (as_seq h0 b))

let poly1305_encode_blocks #s f b =
  load_felems_le f b;
  set_bit128 f


inline_for_extraction noextract
val poly1305_encode_last:
    #s:field_spec
  -> f:felem s
  -> len:size_t{v len < 16}
  -> b:lbuffer uint8 len ->
  Stack unit
  (requires fun h ->
    live h b /\ live h f /\ disjoint b f)
  (ensures  fun h0 _ h1 ->
    modifies (loc f) h0 h1 /\
    felem_fits h1 f (1, 1, 1, 1, 1) /\
    (feval h1 f).[0] == S.encode (v len) (as_seq h0 b))

let poly1305_encode_last #s f len b =
  push_frame();
  let tmp = create 16ul (u8 0) in
  update_sub tmp 0ul len b;
  let h0 = ST.get () in
  Hacl.Impl.Poly1305.Lemmas.nat_from_bytes_le_eq_lemma (v len) (as_seq h0 b);
  assert (BSeq.nat_from_bytes_le (as_seq h0 b) == BSeq.nat_from_bytes_le (as_seq h0 tmp));
  assert (BSeq.nat_from_bytes_le (as_seq h0 b) < pow2 (v len * 8));

  load_felem_le f tmp;
  let h1 = ST.get () in
  lemma_feval_is_fas_nat h1 f;
  set_bit f (len *! 8ul);
  pop_frame()


inline_for_extraction noextract
val poly1305_encode_r:
    #s:field_spec
  -> p:precomp_r s
  -> b:lbuffer uint8 16ul ->
  Stack unit
  (requires fun h ->
    live h b /\ live h p /\ disjoint b p)
  (ensures  fun h0 _ h1 ->
    modifies (loc p) h0 h1 /\
    F32xN.load_precompute_r_post #(width s) h1 p /\
    (feval h1 (gsub p 0ul 5ul)).[0] == S.poly1305_encode_r (as_seq h0 b))

let poly1305_encode_r #s p b =
  let lo = uint_from_bytes_le (sub b 0ul 8ul) in
  let hi = uint_from_bytes_le (sub b 8ul 8ul) in
  let mask0 = u64 0x0ffffffc0fffffff in
  let mask1 = u64 0x0ffffffc0ffffffc in
  let lo = lo &. mask0 in
  let hi = hi &. mask1 in
  load_precompute_r p lo hi

[@ Meta.Attribute.specialize ]
let poly1305_init #s ctx key =
  let acc = get_acc ctx in
  let pre = get_precomp_r ctx in

  let kr = sub key 0ul 16ul in
  set_zero acc;
  poly1305_encode_r #s pre kr


inline_for_extraction noextract
val update1:
    #s:field_spec
  -> p:precomp_r s
  -> b:lbuffer uint8 16ul
  -> acc:felem s ->
  Stack unit
  (requires fun h ->
    live h p /\ live h b /\ live h acc /\
    disjoint p acc /\ disjoint b acc /\
    felem_fits h acc (2, 2, 2, 2, 2) /\
    F32xN.fmul_precomp_r_pre #(width s) h p)
  (ensures  fun h0 _ h1 ->
    modifies (loc acc) h0 h1 /\
    felem_fits h1 acc (2, 2, 2, 2, 2) /\
    (feval h1 acc).[0] == S.poly1305_update1
      (feval h0 (gsub p 0ul 5ul)).[0] 16 (as_seq h0 b) (feval h0 acc).[0])

let update1 #s pre b acc =
  push_frame ();
  let e = create (nlimb s) (limb_zero s) in
  poly1305_encode_block e b;
  fadd_mul_r acc e pre;
  pop_frame ()


let poly1305_update1 #s ctx text =
  let pre = get_precomp_r ctx in
  let acc = get_acc ctx in
  update1 pre text acc


inline_for_extraction noextract
val poly1305_update_last:
    #s:field_spec
  -> p:precomp_r s
  -> len:size_t{v len < 16}
  -> b:lbuffer uint8 len
  -> acc:felem s ->
  Stack unit
  (requires fun h ->
    live h p /\ live h b /\ live h acc /\
    disjoint p acc /\ disjoint b acc /\
    felem_fits h acc (2, 2, 2, 2, 2) /\
    F32xN.fmul_precomp_r_pre #(width s) h p)
  (ensures  fun h0 _ h1 ->
    modifies (loc acc) h0 h1 /\
    felem_fits h1 acc (2, 2, 2, 2, 2) /\
    (feval h1 acc).[0] == S.poly1305_update1
      (feval h0 (gsub p 0ul 5ul)).[0] (v len) (as_seq h0 b) (feval h0 acc).[0])

#push-options "--z3rlimit 200"
let poly1305_update_last #s pre len b acc =
  push_frame ();
  let e = create (nlimb s) (limb_zero s) in
  poly1305_encode_last e len b;
  fadd_mul_r acc e pre;
  pop_frame ()
#pop-options

inline_for_extraction noextract
val poly1305_update_nblocks:
    #s:field_spec
  -> p:precomp_r s
  -> b:lbuffer uint8 (blocklen s)
  -> acc:felem s ->
  Stack unit
  (requires fun h ->
    live h p /\ live h b /\ live h acc /\
    disjoint acc p /\ disjoint acc b /\
    felem_fits h acc (3, 3, 3, 3, 3) /\
    F32xN.load_precompute_r_post #(width s) h p)
  (ensures  fun h0 _ h1 ->
    modifies (loc acc) h0 h1 /\
    felem_fits h1 acc (3, 3, 3, 3, 3) /\
    feval h1 acc ==
      Vec.poly1305_update_nblocks #(width s) (feval h0 (gsub p 10ul 5ul)) (as_seq h0 b) (feval h0 acc))

let poly1305_update_nblocks #s pre b acc =
  push_frame ();
  let e = create (nlimb s) (limb_zero s) in
  poly1305_encode_blocks e b;
  fmul_rn acc acc pre;
  fadd acc acc e;
  pop_frame ()


inline_for_extraction noextract
val poly1305_update1_f:
    #s:field_spec
  -> p:precomp_r s
  -> nb:size_t
  -> len:size_t{v nb == v len / 16}
  -> text:lbuffer uint8 len
  -> i:size_t{v i < v nb}
  -> acc:felem s ->
  Stack unit
  (requires fun h ->
    live h p /\ live h text /\ live h acc /\
    disjoint acc p /\ disjoint acc text /\
    felem_fits h acc (2, 2, 2, 2, 2) /\
    F32xN.fmul_precomp_r_pre #(width s) h p)
  (ensures  fun h0 _ h1 ->
    modifies (loc acc) h0 h1 /\
    felem_fits h1 acc (2, 2, 2, 2, 2) /\
    (feval h1 acc).[0] ==
    LSeq.repeat_blocks_f #uint8 #S.felem 16
      (as_seq h0 text) (S.poly1305_update1 (feval h0 (gsub p 0ul 5ul)).[0] 16) (v nb) (v i) (feval h0 acc).[0])
val poly1305_update1_f:
    #s:field_spec
  -> p:precomp_r s
  -> nb:size_t
  -> len:size_t{v nb == v len / 16}
  -> text:lbuffer uint8 len
  -> i:size_t{v i < v nb}
  -> acc:felem s ->
  Stack unit
  (requires fun h ->
    live h p /\ live h text /\ live h acc /\
    disjoint acc p /\ disjoint acc text /\
    felem_fits h acc (2, 2, 2, 2, 2) /\
    F32xN.fmul_precomp_r_pre #(width s) h p)
  (ensures  fun h0 _ h1 ->
    modifies (loc acc) h0 h1 /\
    felem_fits h1 acc (2, 2, 2, 2, 2) /\
    (feval h1 acc).[0] ==
    LSeq.repeat_blocks_f #uint8 #S.felem 16
      (as_seq h0 text) (S.poly1305_update1 (feval h0 (gsub p 0ul 5ul)).[0] 16) (v nb) (v i) (feval h0 acc).[0])

    p: Hacl.Impl.Poly1305.Fields.precomp_r s ->
    nb: Lib.IntTypes.size_t ->
    len: Lib.IntTypes.size_t{Lib.IntTypes.v nb == Lib.IntTypes.v len / 16} ->
    text: Lib.Buffer.lbuffer Lib.IntTypes.uint8 len ->
    i: Lib.IntTypes.size_t{Lib.IntTypes.v i < Lib.IntTypes.v nb} ->
    acc: Hacl.Impl.Poly1305.Fields.felem s
  -> FStar.HyperStack.ST.Stack Prims.unit