val poly1305_do_:
    #w:field_spec
  -> k:lbuffer uint8 32ul // key
  -> aadlen:size_t
  -> aad:lbuffer uint8 aadlen // authenticated additional data
  -> mlen:size_t
  -> m:lbuffer uint8 mlen // plaintext
  -> ctx:Poly.poly1305_ctx w
  -> block:lbuffer uint8 16ul ->
  Stack unit
  (requires fun h ->
    live h k /\ live h aad /\ live h m /\ live h ctx /\ live h block /\
    disjoint ctx k /\ disjoint ctx aad /\ disjoint ctx m /\ disjoint ctx block /\
    disjoint block k /\ disjoint block aad /\ disjoint block m)
  (ensures fun h0 _ h1 ->
    modifies (loc ctx |+| loc block) h0 h1 /\
    (let acc, r = SpecPoly.poly1305_init (as_seq h0 k) in
    let acc = if (length aad <> 0) then Spec.poly1305_padded r (as_seq h0 aad) acc else acc in
    let acc = if (length m <> 0) then Spec.poly1305_padded r (as_seq h0 m) acc else acc in
    let block_s = LSeq.concat (BSeq.uint_to_bytes_le #U64 (u64 (length aad)))
      (BSeq.uint_to_bytes_le #U64 (u64 (length m))) in
    let acc = SpecPoly.poly1305_update1 r 16 block_s acc in
    Poly.as_get_acc h1 ctx == acc /\ as_seq h1 block == block_s /\
    Poly.state_inv_t h1 ctx))
let poly1305_do_ #w k aadlen aad mlen m ctx block =
  Poly.poly1305_init ctx k;
  if (aadlen <> 0ul) then (
    poly1305_padded ctx aadlen aad)
  else ();
  if (mlen <> 0ul) then (
    poly1305_padded ctx mlen m)
  else ();
  let h0 = ST.get () in
  update_sub_f h0 block 0ul 8ul
    (fun h -> BSeq.uint_to_bytes_le #U64 (to_u64 aadlen))
    (fun _ -> uint_to_bytes_le (sub block 0ul 8ul) (to_u64 aadlen));
  let h1 = ST.get () in
  //assert (LSeq.sub (as_seq h1 block) 0 8 == BSeq.uint_to_bytes_le #U64 (to_u64 aadlen));
  Poly.reveal_ctx_inv ctx h0 h1;
  update_sub_f h1 block 8ul 8ul
    (fun h -> BSeq.uint_to_bytes_le #U64 (to_u64 mlen))
    (fun _ -> uint_to_bytes_le (sub block 8ul 8ul) (to_u64 mlen));
  let h2 = ST.get () in
  //assert (LSeq.sub (as_seq h2 block) 8 8 == BSeq.uint_to_bytes_le #U64 (to_u64 mlen));
  LSeq.eq_intro (LSeq.sub (as_seq h2 block) 0 8) (BSeq.uint_to_bytes_le #U64 (to_u64 aadlen));
  LSeq.lemma_concat2 8 (BSeq.uint_to_bytes_le #U64 (to_u64 aadlen)) 8 (BSeq.uint_to_bytes_le #U64 (to_u64 mlen)) (as_seq h2 block);
  //assert (as_seq h2 block == LSeq.concat (BSeq.uint_to_bytes_le #U64 (to_u64 aadlen)) (BSeq.uint_to_bytes_le #U64 (to_u64 mlen)));
  Poly.reveal_ctx_inv ctx h1 h2;
  Poly.poly1305_update1 ctx block
val poly1305_do_:
    #w:field_spec
  -> k:lbuffer uint8 32ul // key
  -> aadlen:size_t
  -> aad:lbuffer uint8 aadlen // authenticated additional data
  -> mlen:size_t
  -> m:lbuffer uint8 mlen // plaintext
  -> ctx:Poly.poly1305_ctx w
  -> block:lbuffer uint8 16ul ->
  Stack unit
  (requires fun h ->
    live h k /\ live h aad /\ live h m /\ live h ctx /\ live h block /\
    disjoint ctx k /\ disjoint ctx aad /\ disjoint ctx m /\ disjoint ctx block /\
    disjoint block k /\ disjoint block aad /\ disjoint block m)
  (ensures fun h0 _ h1 ->
    modifies (loc ctx |+| loc block) h0 h1 /\
    (let acc, r = SpecPoly.poly1305_init (as_seq h0 k) in
    let acc = if (length aad <> 0) then Spec.poly1305_padded r (as_seq h0 aad) acc else acc in
    let acc = if (length m <> 0) then Spec.poly1305_padded r (as_seq h0 m) acc else acc in
    let block_s = LSeq.concat (BSeq.uint_to_bytes_le #U64 (u64 (length aad)))
      (BSeq.uint_to_bytes_le #U64 (u64 (length m))) in
    let acc = SpecPoly.poly1305_update1 r 16 block_s acc in
    Poly.as_get_acc h1 ctx == acc /\ as_seq h1 block == block_s /\
    Poly.state_inv_t h1 ctx))
let poly1305_do_ #w k aadlen aad mlen m ctx block =
Poly.poly1305_init ctx k;
if (aadlen <> 0ul) then (poly1305_padded ctx aadlen aad);
if (mlen <> 0ul) then (poly1305_padded ctx mlen m);
let h0 = ST.get () in
update_sub_f h0
  block
  0ul
  8ul
  (fun h -> BSeq.uint_to_bytes_le #U64 (to_u64 aadlen))
  (fun _ -> uint_to_bytes_le (sub block 0ul 8ul) (to_u64 aadlen));
let h1 = ST.get () in
Poly.reveal_ctx_inv ctx h0 h1;
update_sub_f h1
  block
  8ul
  8ul
  (fun h -> BSeq.uint_to_bytes_le #U64 (to_u64 mlen))
  (fun _ -> uint_to_bytes_le (sub block 8ul 8ul) (to_u64 mlen));
let h2 = ST.get () in
LSeq.eq_intro (LSeq.sub (as_seq h2 block) 0 8) (BSeq.uint_to_bytes_le #U64 (to_u64 aadlen));
LSeq.lemma_concat2 8
  (BSeq.uint_to_bytes_le #U64 (to_u64 aadlen))
  8
  (BSeq.uint_to_bytes_le #U64 (to_u64 mlen))
  (as_seq h2 block);
Poly.reveal_ctx_inv ctx h1 h2;
Poly.poly1305_update1 ctx block
Hacl.Impl.Chacha20Poly1305.fst.checked
Spec.Poly1305.fst.checked Spec.Chacha20Poly1305.fst.checked Spec.Chacha20.fst.checked prims.fst.checked Meta.Attribute.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Lib.ByteBuffer.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.Chacha20.Vec.fst.checked Hacl.Impl.Poly1305.Fields.fst.checked Hacl.Impl.Poly1305.fsti.checked Hacl.Impl.Chacha20Poly1305.PolyCore.fst.checked Hacl.Impl.Chacha20.Vec.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.All.fst.checked FStar.HyperStack.fst.checked
Hacl.Impl.Chacha20Poly1305.fst
Hacl.Impl.Poly1305.Fields.field_spec Lib.Buffer.lbuffer Lib.IntTypes.uint8 FStar.UInt32.__uint_to_t Lib.IntTypes.size_t Hacl.Impl.Poly1305.poly1305_ctx Hacl.Impl.Poly1305.poly1305_update1 Prims.unit Hacl.Impl.Poly1305.reveal_ctx_inv Lib.Sequence.lemma_concat2 Lib.IntTypes.uint_t Lib.IntTypes.U8 Lib.IntTypes.SEC Lib.ByteSequence.uint_to_bytes_le Lib.IntTypes.U64 Lib.IntTypes.to_u64 Lib.IntTypes.U32 Lib.IntTypes.PUB Lib.Buffer.as_seq Lib.Buffer.MUT Lib.Sequence.eq_intro Lib.Sequence.sub Lib.IntTypes.v FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get Lib.Buffer.update_sub_f Lib.Sequence.lseq Lib.ByteBuffer.uint_to_bytes_le Lib.Buffer.lbuffer_t Lib.IntTypes.int_t Lib.IntTypes.mk_int Lib.Buffer.sub Prims.op_disEquality FStar.UInt32.t Hacl.Impl.Chacha20Poly1305.PolyCore.poly1305_padded Prims.bool Hacl.Impl.Poly1305.poly1305_init
module Hacl.Impl.Chacha20Poly1305

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

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

open Hacl.Impl.Chacha20Poly1305.PolyCore
open Hacl.Impl.Poly1305.Fields

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

module Spec = Spec.Chacha20Poly1305
module SpecPoly = Spec.Poly1305
module Poly = Hacl.Impl.Poly1305

#reset-options "--z3rlimit 150 --max_fuel 0 --max_ifuel 1 --record_options"

val poly1305_do_:
    #w:field_spec
  -> k:lbuffer uint8 32ul // key
  -> aadlen:size_t
  -> aad:lbuffer uint8 aadlen // authenticated additional data
  -> mlen:size_t
  -> m:lbuffer uint8 mlen // plaintext
  -> ctx:Poly.poly1305_ctx w
  -> block:lbuffer uint8 16ul ->
  Stack unit
  (requires fun h ->
    live h k /\ live h aad /\ live h m /\ live h ctx /\ live h block /\
    disjoint ctx k /\ disjoint ctx aad /\ disjoint ctx m /\ disjoint ctx block /\
    disjoint block k /\ disjoint block aad /\ disjoint block m)
  (ensures fun h0 _ h1 ->
    modifies (loc ctx |+| loc block) h0 h1 /\
    (let acc, r = SpecPoly.poly1305_init (as_seq h0 k) in
    let acc = if (length aad <> 0) then Spec.poly1305_padded r (as_seq h0 aad) acc else acc in
    let acc = if (length m <> 0) then Spec.poly1305_padded r (as_seq h0 m) acc else acc in
    let block_s = LSeq.concat (BSeq.uint_to_bytes_le #U64 (u64 (length aad)))
      (BSeq.uint_to_bytes_le #U64 (u64 (length m))) in
    let acc = SpecPoly.poly1305_update1 r 16 block_s acc in
    Poly.as_get_acc h1 ctx == acc /\ as_seq h1 block == block_s /\
    Poly.state_inv_t h1 ctx))
[@Meta.Attribute.inline_]
val poly1305_do_:
    #w:field_spec
  -> k:lbuffer uint8 32ul // key
  -> aadlen:size_t
  -> aad:lbuffer uint8 aadlen // authenticated additional data
  -> mlen:size_t
  -> m:lbuffer uint8 mlen // plaintext
  -> ctx:Poly.poly1305_ctx w
  -> block:lbuffer uint8 16ul ->
  Stack unit
  (requires fun h ->
    live h k /\ live h aad /\ live h m /\ live h ctx /\ live h block /\
    disjoint ctx k /\ disjoint ctx aad /\ disjoint ctx m /\ disjoint ctx block /\
    disjoint block k /\ disjoint block aad /\ disjoint block m)
  (ensures fun h0 _ h1 ->
    modifies (loc ctx |+| loc block) h0 h1 /\
    (let acc, r = SpecPoly.poly1305_init (as_seq h0 k) in
    let acc = if (length aad <> 0) then Spec.poly1305_padded r (as_seq h0 aad) acc else acc in
    let acc = if (length m <> 0) then Spec.poly1305_padded r (as_seq h0 m) acc else acc in
    let block_s = LSeq.concat (BSeq.uint_to_bytes_le #U64 (u64 (length aad)))
      (BSeq.uint_to_bytes_le #U64 (u64 (length m))) in
    let acc = SpecPoly.poly1305_update1 r 16 block_s acc in
    Poly.as_get_acc h1 ctx == acc /\ as_seq h1 block == block_s /\
    Poly.state_inv_t h1 ctx))

    k: Lib.Buffer.lbuffer Lib.IntTypes.uint8 32ul ->
    aadlen: Lib.IntTypes.size_t ->
    aad: Lib.Buffer.lbuffer Lib.IntTypes.uint8 aadlen ->
    mlen: Lib.IntTypes.size_t ->
    m: Lib.Buffer.lbuffer Lib.IntTypes.uint8 mlen ->
    ctx: Hacl.Impl.Poly1305.poly1305_ctx w ->
    block: Lib.Buffer.lbuffer Lib.IntTypes.uint8 16ul
  -> FStar.HyperStack.ST.Stack Prims.unit