let post_call_poly1305_blocks (h1:HS.mem) (inp_b:PS.uint8_p) (src:bytes) (h_in pad r:int) (k:nat
  {B.length inp_b = 8 * PU.readable_words (length src) /\ k <= B.length inp_b / 16}) =
    let len = length src in
    PS.math_aux inp_b (PU.readable_words len);
    let inp_db = IT.get_downview inp_b in
    let inp_sb = B.as_seq h1 inp_b in
    let inp_mem = PU.seqTo128 (PS.uint64_to_nat_seq (UV.as_seq h1 (UV.mk_buffer inp_db Vale.Interop.Views.up_view64))) in
    let h_call = poly1305_hash_blocks (modp h_in) pad r inp_mem k in
    let h_spec = poly1305_hash_blocks (modp h_in) pad r (block_fun src) k in
    h_call == h_spec
let post_call_poly1305_blocks
      (h1: HS.mem)
      (inp_b: PS.uint8_p)
      (src: bytes)
      (h_in pad r: int)
      (k: nat{B.length inp_b = 8 * PU.readable_words (length src) /\ k <= B.length inp_b / 16})
     =
let len = length src in
PS.math_aux inp_b (PU.readable_words len);
let inp_db = IT.get_downview inp_b in
let inp_sb = B.as_seq h1 inp_b in
let inp_mem =
  PU.seqTo128 (PS.uint64_to_nat_seq (UV.as_seq h1 (UV.mk_buffer inp_db Vale.Interop.Views.up_view64)
        ))
in
let h_call = poly1305_hash_blocks (modp h_in) pad r inp_mem k in
let h_spec = poly1305_hash_blocks (modp h_in) pad r (block_fun src) k in
h_call == h_spec
Vale.Poly1305.CallingFromLowStar.fst.checked
Vale.Wrapper.X64.Poly.fsti.checked Vale.Poly1305.Util.fsti.checked Vale.Poly1305.Math.fsti.checked Vale.Interop.Views.fsti.checked Vale.Interop.Types.fst.checked Vale.Def.Words.Seq_s.fsti.checked Vale.AsLowStar.LowStarSig.fst.checked prims.fst.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Endianness.fsti.checked FStar.Calc.fsti.checked
Vale.Poly1305.CallingFromLowStar.fst
FStar.Monotonic.HyperStack.mem Vale.Wrapper.X64.Poly.uint8_p Vale.Poly1305.Equiv.bytes Prims.int Prims.nat Prims.l_and Prims.b2t Prims.op_Equality LowStar.Monotonic.Buffer.length FStar.UInt8.t LowStar.Buffer.trivial_preorder FStar.Mul.op_Star Vale.Poly1305.Util.readable_words FStar.Seq.Base.length Lib.IntTypes.uint_t Lib.IntTypes.U8 Lib.IntTypes.SEC Prims.op_LessThanOrEqual Prims.op_Division Prims.eq2 Vale.Poly1305.Spec_s.poly1305_hash_blocks Vale.Poly1305.Spec_s.modp Vale.Poly1305.Equiv.block_fun Vale.Poly1305.Util.t_seqTo128 Vale.Poly1305.Util.seqTo128 Vale.Wrapper.X64.Poly.uint64_to_nat_seq LowStar.BufferView.Up.as_seq FStar.UInt64.t LowStar.BufferView.Up.mk_buffer Vale.Interop.Views.up_view64 FStar.Seq.Base.seq LowStar.Monotonic.Buffer.as_seq LowStar.BufferView.Down.buffer Vale.Interop.Types.get_downview Vale.Arch.HeapTypes_s.TUInt8 Prims.unit Vale.Wrapper.X64.Poly.math_aux Prims.logical
module Vale.Poly1305.CallingFromLowStar
open FStar.Mul

module BS = Lib.ByteSequence
module LI = Lib.IntTypes
module FE = FStar.Endianness
module PU = Vale.Poly1305.Util
module PM = Vale.Poly1305.Math
module IT = Vale.Interop.Types
module PS = Vale.Wrapper.X64.Poly

#reset-options "--z3rlimit 100"

let lemma_hash_init h0 h1 ctx_b is_zero =
  let open IT in
  let tag0 = BF.to_bytes (slice (B.as_seq h0 ctx_b) 0 24) in
  let tag1 = BF.to_bytes (slice (B.as_seq h1 ctx_b) 0 24) in
  assert (forall (i:int).{:pattern (index (BF.of_bytes tag0) i)} 0 <= i /\ i < 24 ==> index (BF.of_bytes tag0) i == B.get h0 ctx_b i);
  assert (forall (i:int).{:pattern (index (BF.of_bytes tag1) i)} 0 <= i /\ i < 24 ==> index (BF.of_bytes tag1) i == B.get h1 ctx_b i);
  // REVIEW: triggers F* "Unexpected error": assert (equal (BF.of_bytes tag0) (BF.of_bytes tag1));
  let workaround : squash (equal (BF.of_bytes tag0) (BF.of_bytes tag1)) = () in
  assert (view_n TUInt8 == 1);
  assert (view_n TUInt64 == 8);
  DV.length_eq (get_downview ctx_b);
  let h0_in = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h0 ctx_b 0) in
  let h1_in = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h0 ctx_b 1) in
  let h2_in = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h0 ctx_b 2) in
  let h0_out = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h1 ctx_b 0) in
  let h1_out = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h1 ctx_b 1) in
  let h2_out = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h1 ctx_b 2) in
  let view = Vale.AsLowStar.LowStarSig.view_of_base_typ TUInt64 in
  let ctx_db = get_downview ctx_b in
  let ctx_vb = UV.mk_buffer ctx_db view in
  UV.length_eq ctx_vb;
  let open Vale.Def.Words.Seq_s in
  BF.nat_from_bytes_le_is_le_bytes_to_nat64 (slice tag0 0 8);
  calc (==) {
    h0_in;
    == {}
    UInt64.v (UV.sel h0 ctx_vb 0);
    == {UV.get_sel h0 ctx_vb 0; Vale.Interop.Views.get64_reveal ()}
    le_bytes_to_nat64 (seq_uint8_to_seq_nat8 (slice (DV.as_seq h0 (UV.as_down_buffer ctx_vb)) 0 8));
    == {BF.same_seq_downview8 ctx_b h0}
    nat_from_bytes_le (slice tag0 0 8);
  };
  BF.nat_from_bytes_le_is_le_bytes_to_nat64 (slice tag1 0 8);
  calc (==) {
    h0_out;
    == {}
    UInt64.v (UV.sel h1 ctx_vb 0);
    == {UV.get_sel h1 ctx_vb 0; Vale.Interop.Views.get64_reveal ()}
    le_bytes_to_nat64 (seq_uint8_to_seq_nat8 (slice (DV.as_seq h1 (UV.as_down_buffer ctx_vb)) 0 8));
    == {BF.same_seq_downview8 ctx_b h1}
    nat_from_bytes_le (slice tag1 0 8);
  };
  BF.lemma_le_to_n_is_nat_from_bytes (BF.of_bytes (slice tag0 0 8));
  if is_zero then
    calc (==) {
      nat_from_bytes_le (slice tag0 0 8) <: nat;
      == {}
      FE.le_to_n (BF.of_bytes (slice tag0 0 8));
      == {BF.lemma_le_to_n_indexed (BF.of_bytes (slice tag0 0 8))}
      BF.le_to_n_indexed (BF.of_bytes (slice tag0 0 8));
      == {
        norm_spec [iota; zeta; primops; delta_only [`%BF.le_to_n_indexed_rec; `%pow2]]
          (BF.le_to_n_indexed_rec (BF.of_bytes (slice tag0 0 8)) 8)
      }
      0;
    };
  BF.nat_from_bytes_le_is_le_bytes_to_nat64 (slice tag0 8 16);
  calc (==) {
    h1_in;
    == {}
    UInt64.v (UV.sel h0 ctx_vb 1);
    == {UV.get_sel h0 ctx_vb 1; Vale.Interop.Views.get64_reveal ()}
    le_bytes_to_nat64 (seq_uint8_to_seq_nat8 (slice (DV.as_seq h0 (UV.as_down_buffer ctx_vb)) 8 16));
    == {BF.same_seq_downview8 ctx_b h0}
    nat_from_bytes_le (slice tag0 8 16);
  };
  BF.nat_from_bytes_le_is_le_bytes_to_nat64 (slice tag1 8 16);
  calc (==) {
    h1_out;
    == {}
    UInt64.v (UV.sel h1 ctx_vb 1);
    == {UV.get_sel h1 ctx_vb 1; Vale.Interop.Views.get64_reveal ()}
    le_bytes_to_nat64 (seq_uint8_to_seq_nat8 (slice (DV.as_seq h1 (UV.as_down_buffer ctx_vb)) 8 16));
    == {BF.same_seq_downview8 ctx_b h1}
    nat_from_bytes_le (slice tag1 8 16);
  };
  BF.lemma_le_to_n_is_nat_from_bytes (BF.of_bytes (slice tag0 8 16));
  if is_zero then
    calc (==) {
      nat_from_bytes_le (slice tag0 8 16) <: nat;
      == {}
      FE.le_to_n (BF.of_bytes (slice tag0 8 16));
      == {BF.lemma_le_to_n_indexed (BF.of_bytes (slice tag0 8 16))}
      BF.le_to_n_indexed (BF.of_bytes (slice tag0 8 16));
      == {
        norm_spec [iota; zeta; primops; delta_only [`%BF.le_to_n_indexed_rec; `%pow2]]
          (BF.le_to_n_indexed_rec (BF.of_bytes (slice tag0 8 16)) 8)
      }
      0;
    };
  BF.nat_from_bytes_le_is_le_bytes_to_nat64 (slice tag0 16 24);
  calc (==) {
    h2_in;
    == {}
    UInt64.v (UV.sel h0 ctx_vb 2);
    == {UV.get_sel h0 ctx_vb 2; Vale.Interop.Views.get64_reveal ()}
    le_bytes_to_nat64 (seq_uint8_to_seq_nat8 (slice (DV.as_seq h0 (UV.as_down_buffer ctx_vb)) 16 24));
    == {BF.same_seq_downview8 ctx_b h0}
    nat_from_bytes_le (slice tag0 16 24);
  };
  BF.nat_from_bytes_le_is_le_bytes_to_nat64 (slice tag1 16 24);
  calc (==) {
    h2_out;
    == {}
    UInt64.v (UV.sel h1 ctx_vb 2);
    == {UV.get_sel h1 ctx_vb 2; Vale.Interop.Views.get64_reveal ()}
    le_bytes_to_nat64 (seq_uint8_to_seq_nat8 (slice (DV.as_seq h1 (UV.as_down_buffer ctx_vb)) 16 24));
    == {BF.same_seq_downview8 ctx_b h1}
    nat_from_bytes_le (slice tag1 16 24);
  };
  BF.lemma_le_to_n_is_nat_from_bytes (BF.of_bytes (slice tag0 16 24));
  if is_zero then
    calc (==) {
      nat_from_bytes_le (slice tag0 16 24) <: nat;
      == {}
      FE.le_to_n (BF.of_bytes (slice tag0 16 24));
      == {BF.lemma_le_to_n_indexed (BF.of_bytes (slice tag0 16 24))}
      BF.le_to_n_indexed (BF.of_bytes (slice tag0 16 24));
      == {
        norm_spec [iota; zeta; primops; delta_only [`%BF.le_to_n_indexed_rec; `%pow2]]
          (BF.le_to_n_indexed_rec (BF.of_bytes (slice tag0 16 24)) 8)
      }
      0;
    };
  assert_norm (modp 0 == 0);
  if is_zero then
    calc (==) {
      PM.lowerUpper192 (PM.lowerUpper128 h0_in h1_in) h2_in;
      == {PM.lowerUpper128_reveal (); PM.lowerUpper192_reveal ()}
      0;
    }

let lemma_block (h1:HS.mem) (inp_b:B.buffer UInt8.t) (len:nat) (i:nat) : Lemma
  (requires B.length inp_b = 8 * PU.readable_words len /\ i < B.length inp_b / 16)
  (ensures (
    PS.math_aux inp_b (PU.readable_words len);
    let inp_db = IT.get_downview inp_b in
    let inp_sb = B.as_seq h1 inp_b in
    let inp_mem = PU.seqTo128 (PS.uint64_to_nat_seq (UV.as_seq h1 (UV.mk_buffer inp_db Vale.Interop.Views.up_view64))) in
    inp_mem i == block_fun (BF.to_bytes inp_sb) i
  ))
  =
  PS.math_aux inp_b (PU.readable_words len);
  let inp_sb = B.as_seq h1 inp_b in
  let text = BF.to_bytes inp_sb in
  let inp_db = IT.get_downview inp_b in
  let inp_vb = UV.mk_buffer inp_db Vale.Interop.Views.up_view64 in
  let inp_su = UV.as_seq h1 inp_vb in
  let inp_mem = PU.seqTo128 (PS.uint64_to_nat_seq inp_su) in
  let inp_sd = DV.as_seq h1 (UV.as_down_buffer inp_vb) in
  let j1 = i * size_block in
  let j2 = i * size_block + size_block in
  Math.Lemmas.pow2_le_compat 128 (8 * (j2 - j1));
  UV.length_eq inp_vb;
  BF.same_seq_downview8 inp_b h1;
  BF.lemma_up_as_seq_index h1 inp_vb (2 * i);
  BF.lemma_up_as_seq_index h1 inp_vb (2 * i + 1);
  let open Vale.Def.Words.Seq_s in
  BF.nat_from_bytes_le_is_le_bytes_to_nat64 (slice text j1 (j1 + 8));
  calc (==) {
    UInt64.v (index inp_su (2 * i));
    == {Vale.Interop.Views.get64_reveal ()}
    UInt64.v (Vale.Interop.Views.get64_def (slice inp_sd j1 (j1 + 8)));
    == {}
    le_bytes_to_nat64 (seq_uint8_to_seq_nat8 (BF.of_bytes (slice text j1 (j1 + 8))));
    == {}
    nat_from_bytes_le (slice text j1 (j1 + 8));
  };
  BF.nat_from_bytes_le_is_le_bytes_to_nat64 (slice text (j1 + 8) (j1 + 16));
  calc (==) {
    UInt64.v (index inp_su (2 * i + 1));
    == {Vale.Interop.Views.get64_reveal ()}
    UInt64.v (Vale.Interop.Views.get64_def (slice inp_sd (j1 + 8) (j1 + 16)));
    == {}
    le_bytes_to_nat64 (seq_uint8_to_seq_nat8 (BF.of_bytes (slice text (j1 + 8) (j1 + 16))));
    == {}
    nat_from_bytes_le (slice text (j1 + 8) (j1 + 16));
  };
  calc (==) {
    inp_mem i;
    == {}
    UInt64.v (index inp_su (2 * i)) + pow2 64 * UInt64.v (index inp_su (2 * i + 1));
    == {}
    nat_from_bytes_le (slice text j1 (j1 + 8)) + pow2 64 * nat_from_bytes_le (slice text (j1 + 8) (j1 + 16));
    == {}
    nat_from_bytes_le (slice (slice text j1 j2) 0 8) + pow2 64 * nat_from_bytes_le (slice (slice text j1 j2) 8 16);
    == {BS.nat_from_intseq_le_slice_lemma #LI.U8 #LI.SEC #16 (slice text j1 j2) 8}
    nat_from_bytes_le (slice text j1 j2);
    == {}
    block_fun text i;
  }

let lemma_block_extra (h1:HS.mem) (inp_b:B.buffer UInt8.t) (len:nat) : Lemma
  (requires B.length inp_b = 8 * PU.readable_words len /\ len % 16 > 0)
  (ensures (
    PS.math_aux inp_b (PU.readable_words len);
    let i = len / 16 in
    let nExtra = len % 16 in
    let padLast = pow2 (nExtra * 8) in
    let inp_db = IT.get_downview inp_b in
    let inp_sb = B.as_seq h1 inp_b in
    let inp_ssb = slice inp_sb 0 len in
    let inp_mem = PU.seqTo128 (PS.uint64_to_nat_seq (UV.as_seq h1 (UV.mk_buffer inp_db Vale.Interop.Views.up_view64))) in
    inp_mem i % padLast == block_fun (BF.to_bytes inp_ssb) i % padLast
  ))
  =
  PS.math_aux inp_b (PU.readable_words len);
  let i = len / 16 in
  let nExtra = len % 16 in
  let padLast = pow2 (nExtra * 8) in
  let inp_db = IT.get_downview inp_b in
  let inp_sb = B.as_seq h1 inp_b in
  let inp_ssb = slice inp_sb 0 len in
  let inp_mem = PU.seqTo128 (PS.uint64_to_nat_seq (UV.as_seq h1 (UV.mk_buffer inp_db Vale.Interop.Views.up_view64))) in
  let j1 = i * size_block in
  let j2 = i * size_block + size_block in
  let text = BF.to_bytes inp_sb in
  let block = slice text j1 j2 in
  let nLo = nat_from_bytes_le (slice block 0 nExtra) in
  let nHi = nat_from_bytes_le (slice block nExtra 16) in
  calc (==) {
    inp_mem i % padLast;
    == {lemma_block h1 inp_b len i}
    block_fun text i % padLast;
    == {}
    nat_from_bytes_le block % padLast;
    == {BS.nat_from_intseq_le_slice_lemma #LI.U8 #LI.SEC #16 block nExtra}
    (nLo + padLast * nHi) % padLast;
    == {FStar.Math.Lemmas.swap_mul nHi padLast}
    (nLo + nHi * padLast) % padLast;
    == {FStar.Math.Lemmas.lemma_mod_plus nLo nHi padLast}
    nLo % padLast;
    == {}
    block_fun (BF.to_bytes inp_ssb) i % padLast;
  }
val post_call_poly1305_blocks : h1: FStar.Monotonic.HyperStack.mem ->
    inp_b: Vale.Wrapper.X64.Poly.uint8_p ->
    src: Vale.Poly1305.Equiv.bytes ->
    h_in: Prims.int ->
    pad: Prims.int ->
    r: Prims.int ->
    k:
      Prims.nat
        { LowStar.Monotonic.Buffer.length inp_b =
          8 * Vale.Poly1305.Util.readable_words (FStar.Seq.Base.length src) /\
          k <= LowStar.Monotonic.Buffer.length inp_b / 16 }
  -> Prims.logical

    h1: FStar.Monotonic.HyperStack.mem ->
    inp_b: Vale.Wrapper.X64.Poly.uint8_p ->
    src: Vale.Poly1305.Equiv.bytes ->
    h_in: Prims.int ->
    pad: Prims.int ->
    r: Prims.int ->
    k:
      Prims.nat
        { LowStar.Monotonic.Buffer.length inp_b =
          8 * Vale.Poly1305.Util.readable_words (FStar.Seq.Base.length src) /\
          k <= LowStar.Monotonic.Buffer.length inp_b / 16 }
  -> Prims.logical