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 ()
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 ()
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.Buffer.lbuffer Lib.IntTypes.uint8 FStar.UInt32.__uint_to_t Hacl.Impl.Poly1305.Fields.felem FStar.HyperStack.ST.pop_frame Prims.unit Hacl.Impl.Poly1305.Fields.fadd_mul_r Hacl.Impl.Poly1305.poly1305_encode_block Lib.Buffer.lbuffer_t Lib.Buffer.MUT Hacl.Spec.Poly1305.Field32xN.uint64xN FStar.UInt32.uint_to_t FStar.UInt32.t Lib.Buffer.create Hacl.Impl.Poly1305.Fields.limb Hacl.Impl.Poly1305.Fields.nlimb Hacl.Impl.Poly1305.Fields.limb_zero FStar.HyperStack.ST.push_frame
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])
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])

    p: Hacl.Impl.Poly1305.Fields.precomp_r s ->
    b: Lib.Buffer.lbuffer Lib.IntTypes.uint8 16ul ->
    acc: Hacl.Impl.Poly1305.Fields.felem s
  -> FStar.HyperStack.ST.Stack Prims.unit