val lemma_call_poly1305 (h0 h1:HS.mem) (ctx_b:PS.uint8_p) (inp_b:PS.uint8_p) (src key:bytes) : Lemma
  (requires (
    let open PU in
    let len = length src in
    B.live h1 ctx_b /\
    // copied from Vale.Wrapper.X64.Poly.poly1305:
    B.live h0 ctx_b /\ B.live h0 inp_b /\
    B.length ctx_b == 192 /\
    B.length inp_b == 8 * readable_words len /\
    // interface to Poly1305.Equiv:
    equal (BF.of_bytes key) (slice (B.as_seq h0 ctx_b) 24 56) /\
    equal (BF.of_bytes src) (slice (B.as_seq h1 inp_b) 0 len)
  ))
  (ensures (
    let open PU in
    let open PM in
    let open PS in
    let open IT in
    assert (view_n TUInt8 == 1);
    assert (view_n TUInt64 == 8);
    let len = length src in

    // copied from Vale.Wrapper.X64.Poly.poly1305:
    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 key_r0 = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h0 ctx_b 3) in
    let key_r1 = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h0 ctx_b 4) in
    let key_s0 = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h0 ctx_b 5) in
    let key_s1 = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h0 ctx_b 6) in
    let h_in = lowerUpper192 (lowerUpper128 h0_in h1_in) h2_in in
    let key_r = lowerUpper128 key_r0 key_r1 in
    let key_s = lowerUpper128 key_s0 key_s1 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 h10 = lowerUpper128 h0_out h1_out in
    let db = get_downview inp_b in
    math_aux inp_b (readable_words len);
    let inp_mem = seqTo128 (uint64_to_nat_seq (UV.as_seq h1 (UV.mk_buffer db Vale.Interop.Views.up_view64))) in
    let n = 0x10000000000000000 in
    let h_call = poly1305_hash_blocks (modp h_in) (n * n) (make_r key_r) inp_mem (len / 16) in
    let h_call' = poly1305_hash_all (modp h_in) key_r key_s inp_mem len in

    // interface to Poly1305.Equiv:
    let key_r_spec:nat128 = nat_from_bytes_le (slice key 0 16) in
    let key_s_spec:nat128 = nat_from_bytes_le (slice key 16 32) in
    let h_spec = poly1305_hash_blocks (modp h_in) (n * n) (make_r key_r) (block_fun src) (len / 16) in
    let h_spec' = poly1305_hash_all (modp h_in) key_r key_s (block_fun src) len in
    let tag = BF.to_bytes (slice (B.as_seq h1 ctx_b) 0 16) in
    key_r == key_r_spec /\ key_s == key_s_spec /\ h_call == h_spec /\ h_call' == h_spec' /\
    h10 == nat_from_bytes_le tag
  ))
let lemma_call_poly1305 h0 h1 ctx_b inp_b src key =
  let open Vale.Def.Words.Seq_s in
  let open PU in
  let open PM in
  let open PS in
  let open IT in
  let len = length src in
  assert (view_n TUInt8 == 1);
  assert (view_n TUInt64 == 8);

  // copied from Vale.Wrapper.X64.Poly.poly1305:
  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 key_r0 = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h0 ctx_b 3) in
  let key_r1 = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h0 ctx_b 4) in
  let key_s0 = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h0 ctx_b 5) in
  let key_s1 = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h0 ctx_b 6) in
  let h_in = lowerUpper192 (lowerUpper128 h0_in h1_in) h2_in in
  let key_r = lowerUpper128 key_r0 key_r1 in
  let key_s = lowerUpper128 key_s0 key_s1 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 h = lowerUpper128 h0_out h1_out in
  let db = get_downview inp_b in
  math_aux inp_b (readable_words len);
  let inp_mem = seqTo128 (uint64_to_nat_seq (UV.as_seq h1 (UV.mk_buffer db Vale.Interop.Views.up_view64))) in
  let n = 0x10000000000000000 in
  let h_call = poly1305_hash_blocks (modp h_in) (n * n) (make_r key_r) inp_mem (len / 16) in
  let h_call' = poly1305_hash_all (modp h_in) key_r key_s inp_mem len in

  // interface to Poly1305.Equiv:
  let key_r_spec:nat128 = nat_from_bytes_le (slice key 0 16) in
  let key_s_spec:nat128 = nat_from_bytes_le (slice key 16 32) in
  let h_spec = poly1305_hash_blocks (modp h_in) (n * n) (make_r key_r) (block_fun src) (len / 16) in
  let h_spec' = poly1305_hash_all (modp h_in) key_r key_s (block_fun src) len 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;

  BF.nat_from_bytes_le_is_le_bytes_to_nat64 (slice key 0 8);
  calc (==) {
    key_r0;
    == {}
    UInt64.v (UV.sel h0 ctx_vb 3);
    == {UV.get_sel h0 ctx_vb 3; 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)) 24 32));
    == {BF.same_seq_downview8 ctx_b h0}
    nat_from_bytes_le (slice (slice key 0 16) 0 8);
  };

  BF.nat_from_bytes_le_is_le_bytes_to_nat64 (slice key 8 16);
  calc (==) {
    key_r1;
    == {}
    UInt64.v (UV.sel h0 ctx_vb 4);
    == {UV.get_sel h0 ctx_vb 4; 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)) 32 40));
    == {BF.same_seq_downview8 ctx_b h0}
    nat_from_bytes_le (slice (slice key 0 16) 8 16);
  };

  calc (==) {
    key_r;
    == {}
    lowerUpper128 key_r0 key_r1;
    == {lowerUpper128_reveal ()}
    nat_from_bytes_le (slice (slice key 0 16) 0 8) + pow2 64 * nat_from_bytes_le (slice (slice key 0 16) 8 16);
    == {BS.nat_from_intseq_le_slice_lemma #LI.U8 #LI.SEC #16 (slice key 0 16) 8}
    nat_from_bytes_le (slice key 0 16);
    == {}
    key_r_spec;
  };

  BF.nat_from_bytes_le_is_le_bytes_to_nat64 (slice key 16 24);
  calc (==) {
    key_s0;
    == {}
    UInt64.v (UV.sel h0 ctx_vb 5);
    == {UV.get_sel h0 ctx_vb 5; 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)) 40 48));
    == {BF.same_seq_downview8 ctx_b h0}
    nat_from_bytes_le (slice (slice key 16 32) 0 8);
  };

  BF.nat_from_bytes_le_is_le_bytes_to_nat64 (slice key 24 32);
  calc (==) {
    key_s1;
    == {}
    UInt64.v (UV.sel h0 ctx_vb 6);
    == {UV.get_sel h0 ctx_vb 6; 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)) 48 56));
    == {BF.same_seq_downview8 ctx_b h0}
    nat_from_bytes_le (slice (slice key 16 32) 8 16);
  };

  calc (==) {
    key_s;
    == {}
    lowerUpper128 key_s0 key_s1;
    == {lowerUpper128_reveal ()}
    nat_from_bytes_le (slice (slice key 16 32) 0 8) + pow2 64 * nat_from_bytes_le (slice (slice key 16 32) 8 16);
    == {BS.nat_from_intseq_le_slice_lemma #LI.U8 #LI.SEC #16 (slice key 16 32) 8}
    nat_from_bytes_le (slice key 16 32);
    == {}
    key_s_spec;
  };

  let r = iand key_r 0x0ffffffc0ffffffc0ffffffc0fffffff in
  let nBlocks = len / 16 in
  lemma_call_poly1305_blocks h1 inp_b src h_in pow2_128 r nBlocks;
  lemma_call_poly1305_all h1 inp_b src h_in key_r key_s;

  let tag = BF.to_bytes (slice (B.as_seq h1 ctx_b) 0 16) in

  BF.nat_from_bytes_le_is_le_bytes_to_nat64 (slice tag 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 tag 0 8);
  };

  BF.nat_from_bytes_le_is_le_bytes_to_nat64 (slice tag 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 tag 8 16);
  };

  calc (==) {
    h;
    == {}
    lowerUpper128 h0_out h1_out;
    == {lowerUpper128_reveal ()}
    nat_from_bytes_le (slice tag 0 8) + pow2 64 * nat_from_bytes_le (slice tag 8 16);
    == {BS.nat_from_intseq_le_slice_lemma #LI.U8 #LI.SEC #16 tag 8}
    nat_from_bytes_le tag;
  };

  ()
val lemma_call_poly1305 (h0 h1:HS.mem) (ctx_b:PS.uint8_p) (inp_b:PS.uint8_p) (src key:bytes) : Lemma
  (requires (
    let open PU in
    let len = length src in
    B.live h1 ctx_b /\
    // copied from Vale.Wrapper.X64.Poly.poly1305:
    B.live h0 ctx_b /\ B.live h0 inp_b /\
    B.length ctx_b == 192 /\
    B.length inp_b == 8 * readable_words len /\
    // interface to Poly1305.Equiv:
    equal (BF.of_bytes key) (slice (B.as_seq h0 ctx_b) 24 56) /\
    equal (BF.of_bytes src) (slice (B.as_seq h1 inp_b) 0 len)
  ))
  (ensures (
    let open PU in
    let open PM in
    let open PS in
    let open IT in
    assert (view_n TUInt8 == 1);
    assert (view_n TUInt64 == 8);
    let len = length src in

    // copied from Vale.Wrapper.X64.Poly.poly1305:
    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 key_r0 = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h0 ctx_b 3) in
    let key_r1 = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h0 ctx_b 4) in
    let key_s0 = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h0 ctx_b 5) in
    let key_s1 = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h0 ctx_b 6) in
    let h_in = lowerUpper192 (lowerUpper128 h0_in h1_in) h2_in in
    let key_r = lowerUpper128 key_r0 key_r1 in
    let key_s = lowerUpper128 key_s0 key_s1 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 h10 = lowerUpper128 h0_out h1_out in
    let db = get_downview inp_b in
    math_aux inp_b (readable_words len);
    let inp_mem = seqTo128 (uint64_to_nat_seq (UV.as_seq h1 (UV.mk_buffer db Vale.Interop.Views.up_view64))) in
    let n = 0x10000000000000000 in
    let h_call = poly1305_hash_blocks (modp h_in) (n * n) (make_r key_r) inp_mem (len / 16) in
    let h_call' = poly1305_hash_all (modp h_in) key_r key_s inp_mem len in

    // interface to Poly1305.Equiv:
    let key_r_spec:nat128 = nat_from_bytes_le (slice key 0 16) in
    let key_s_spec:nat128 = nat_from_bytes_le (slice key 16 32) in
    let h_spec = poly1305_hash_blocks (modp h_in) (n * n) (make_r key_r) (block_fun src) (len / 16) in
    let h_spec' = poly1305_hash_all (modp h_in) key_r key_s (block_fun src) len in
    let tag = BF.to_bytes (slice (B.as_seq h1 ctx_b) 0 16) in
    key_r == key_r_spec /\ key_s == key_s_spec /\ h_call == h_spec /\ h_call' == h_spec' /\
    h10 == nat_from_bytes_le tag
  ))
let lemma_call_poly1305 h0 h1 ctx_b inp_b src key =
let open Vale.Def.Words.Seq_s in
let open PU in
let open PM in
let open PS in
let open IT in
let len = length src 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 key_r0 = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h0 ctx_b 3) in
let key_r1 = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h0 ctx_b 4) in
let key_s0 = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h0 ctx_b 5) in
let key_s1 = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h0 ctx_b 6) in
let h_in = lowerUpper192 (lowerUpper128 h0_in h1_in) h2_in in
let key_r = lowerUpper128 key_r0 key_r1 in
let key_s = lowerUpper128 key_s0 key_s1 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 h = lowerUpper128 h0_out h1_out in
let db = get_downview inp_b in
math_aux inp_b (readable_words len);
let inp_mem =
  seqTo128 (uint64_to_nat_seq (UV.as_seq h1 (UV.mk_buffer db Vale.Interop.Views.up_view64)))
in
let n = 0x10000000000000000 in
let h_call = poly1305_hash_blocks (modp h_in) (n * n) (make_r key_r) inp_mem (len / 16) in
let h_call' = poly1305_hash_all (modp h_in) key_r key_s inp_mem len in
let key_r_spec:nat128 = nat_from_bytes_le (slice key 0 16) in
let key_s_spec:nat128 = nat_from_bytes_le (slice key 16 32) in
let h_spec = poly1305_hash_blocks (modp h_in) (n * n) (make_r key_r) (block_fun src) (len / 16) in
let h_spec' = poly1305_hash_all (modp h_in) key_r key_s (block_fun src) len 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;
BF.nat_from_bytes_le_is_le_bytes_to_nat64 (slice key 0 8);
calc ( == ) {
  key_r0;
  ( == ) { () }
  UInt64.v (UV.sel h0 ctx_vb 3);
  ( == ) { (UV.get_sel h0 ctx_vb 3;
    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)) 24 32));
  ( == ) { BF.same_seq_downview8 ctx_b h0 }
  nat_from_bytes_le (slice (slice key 0 16) 0 8);
};
BF.nat_from_bytes_le_is_le_bytes_to_nat64 (slice key 8 16);
calc ( == ) {
  key_r1;
  ( == ) { () }
  UInt64.v (UV.sel h0 ctx_vb 4);
  ( == ) { (UV.get_sel h0 ctx_vb 4;
    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)) 32 40));
  ( == ) { BF.same_seq_downview8 ctx_b h0 }
  nat_from_bytes_le (slice (slice key 0 16) 8 16);
};
calc ( == ) {
  key_r;
  ( == ) { () }
  lowerUpper128 key_r0 key_r1;
  ( == ) { lowerUpper128_reveal () }
  nat_from_bytes_le (slice (slice key 0 16) 0 8) +
  pow2 64 * nat_from_bytes_le (slice (slice key 0 16) 8 16);
  ( == ) { BS.nat_from_intseq_le_slice_lemma #LI.U8 #LI.SEC #16 (slice key 0 16) 8 }
  nat_from_bytes_le (slice key 0 16);
  ( == ) { () }
  key_r_spec;
};
BF.nat_from_bytes_le_is_le_bytes_to_nat64 (slice key 16 24);
calc ( == ) {
  key_s0;
  ( == ) { () }
  UInt64.v (UV.sel h0 ctx_vb 5);
  ( == ) { (UV.get_sel h0 ctx_vb 5;
    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)) 40 48));
  ( == ) { BF.same_seq_downview8 ctx_b h0 }
  nat_from_bytes_le (slice (slice key 16 32) 0 8);
};
BF.nat_from_bytes_le_is_le_bytes_to_nat64 (slice key 24 32);
calc ( == ) {
  key_s1;
  ( == ) { () }
  UInt64.v (UV.sel h0 ctx_vb 6);
  ( == ) { (UV.get_sel h0 ctx_vb 6;
    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)) 48 56));
  ( == ) { BF.same_seq_downview8 ctx_b h0 }
  nat_from_bytes_le (slice (slice key 16 32) 8 16);
};
calc ( == ) {
  key_s;
  ( == ) { () }
  lowerUpper128 key_s0 key_s1;
  ( == ) { lowerUpper128_reveal () }
  nat_from_bytes_le (slice (slice key 16 32) 0 8) +
  pow2 64 * nat_from_bytes_le (slice (slice key 16 32) 8 16);
  ( == ) { BS.nat_from_intseq_le_slice_lemma #LI.U8 #LI.SEC #16 (slice key 16 32) 8 }
  nat_from_bytes_le (slice key 16 32);
  ( == ) { () }
  key_s_spec;
};
let r = iand key_r 0x0ffffffc0ffffffc0ffffffc0fffffff in
let nBlocks = len / 16 in
lemma_call_poly1305_blocks h1 inp_b src h_in pow2_128 r nBlocks;
lemma_call_poly1305_all h1 inp_b src h_in key_r key_s;
let tag = BF.to_bytes (slice (B.as_seq h1 ctx_b) 0 16) in
BF.nat_from_bytes_le_is_le_bytes_to_nat64 (slice tag 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 tag 0 8);
};
BF.nat_from_bytes_le_is_le_bytes_to_nat64 (slice tag 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 tag 8 16);
};
calc ( == ) {
  h;
  ( == ) { () }
  lowerUpper128 h0_out h1_out;
  ( == ) { lowerUpper128_reveal () }
  nat_from_bytes_le (slice tag 0 8) + pow2 64 * nat_from_bytes_le (slice tag 8 16);
  ( == ) { BS.nat_from_intseq_le_slice_lemma #LI.U8 #LI.SEC #16 tag 8 }
  nat_from_bytes_le tag;
};
()
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.unit FStar.Calc.calc_finish Vale.Def.Words_s.nat128 Prims.eq2 Vale.Poly1305.Equiv.nat_from_bytes_le Lib.IntTypes.SEC Prims.Cons FStar.Preorder.relation Prims.Nil FStar.Calc.calc_step Prims.op_Addition FStar.Seq.Base.slice Lib.IntTypes.uint_t Lib.IntTypes.U8 FStar.Mul.op_Star Prims.pow2 Vale.Poly1305.Math.lowerUpper128 FStar.Calc.calc_init FStar.Calc.calc_pack Prims.squash Vale.Poly1305.Math.lowerUpper128_reveal Lib.ByteSequence.nat_from_intseq_le_slice_lemma FStar.UInt.uint_t FStar.UInt64.n Vale.Def.Types_s.le_bytes_to_nat64 Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8 LowStar.BufferView.Up.buffer_src Vale.Interop.Types.base_typ_as_type Vale.Arch.HeapTypes_s.TUInt64 LowStar.BufferView.Down.as_seq LowStar.BufferView.Up.as_down_buffer FStar.UInt64.v LowStar.BufferView.Up.sel Vale.Interop.Views.get64_reveal LowStar.BufferView.Up.get_sel Vale.Arch.BufferFriend.same_seq_downview8 Vale.Arch.BufferFriend.nat_from_bytes_le_is_le_bytes_to_nat64 Lib.Sequence.seq Lib.IntTypes.int_t Prims.l_and Prims.op_Equals_Equals_Equals FStar.Seq.Base.seq FStar.UInt8.t LowStar.Monotonic.Buffer.as_seq LowStar.Buffer.trivial_preorder Prims.nat FStar.Seq.Base.length Vale.Arch.BufferFriend.to_bytes Vale.Poly1305.CallingFromLowStar.lemma_call_poly1305_all Vale.Poly1305.CallingFromLowStar.lemma_call_poly1305_blocks Vale.Def.Words_s.pow2_128 Prims.int Prims.op_Division Vale.Def.Words_s.natN Vale.Def.Types_s.iand LowStar.BufferView.Up.length_eq LowStar.BufferView.Up.buffer LowStar.BufferView.Up.mk_buffer LowStar.BufferView.Down.buffer Vale.Interop.Types.get_downview Vale.Arch.HeapTypes_s.TUInt8 LowStar.BufferView.Up.view Vale.AsLowStar.LowStarSig.view_of_base_typ Vale.Poly1305.Spec_s.poly1305_hash_all Vale.Poly1305.Spec_s.modp Vale.Poly1305.Equiv.block_fun Vale.Poly1305.Spec_s.poly1305_hash_blocks Vale.Poly1305.Spec_s.make_r 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 Vale.Interop.Views.up_view64 Vale.Wrapper.X64.Poly.math_aux Vale.Poly1305.Util.readable_words Vale.AsLowStar.MemoryHelpers.low_buffer_read Vale.Poly1305.Math.lowerUpper192 LowStar.BufferView.Down.length_eq Prims._assert Vale.Interop.Types.view_n
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;
  }

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 rec lemma_call_poly1305_blocks (h1:HS.mem) (inp_b:PS.uint8_p) (src:bytes) (h_in pad r:int) (k:nat) : Lemma
  (requires (
    let len = length src in
    B.length inp_b = 8 * PU.readable_words len /\
    equal (BF.of_bytes src) (slice (B.as_seq h1 inp_b) 0 len) /\
    k <= len / 16
  ))
  (ensures (
(* REVIEW: this didn't type check because of the "let rec" (non-recursive "let" worked):
    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
*)
    post_call_poly1305_blocks h1 inp_b src h_in pad r k
  ))
  =
  let len = length src in
  if k > 0 then
  (
    lemma_call_poly1305_blocks h1 inp_b src h_in pad r (k - 1);
    lemma_block h1 inp_b len (k - 1);
    let inp_sb = B.as_seq h1 inp_b in
    let j1 = (k - 1) * size_block in
    let j2 = (k - 1) * size_block + size_block in
    assert (BF.to_bytes (BF.of_bytes src) == src);
    assert (equal (slice (BF.to_bytes inp_sb) j1 j2) (slice src j1 j2));
    ()
  )

let lemma_call_poly1305_all (h1:HS.mem) (inp_b:PS.uint8_p) (src:bytes) (h_in:int) (key_r key_s:nat128) : Lemma
  (requires (
    let len = length src in
    B.length inp_b = 8 * PU.readable_words len /\
    equal (BF.of_bytes src) (slice (B.as_seq h1 inp_b) 0 len)
  ))
  (ensures (
    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_all (modp h_in) key_r key_s inp_mem len in
    let h_spec = poly1305_hash_all (modp h_in) key_r key_s (block_fun src) len in
    h_call == h_spec
  ))
  =
  let len = length src in
  let r = iand key_r 0x0ffffffc0ffffffc0ffffffc0fffffff in
  let nBlocks = len / 16 in
  let nExtra = len % 16 in
  lemma_call_poly1305_blocks h1 inp_b src h_in pow2_128 r nBlocks;
  if nExtra > 0 then lemma_block_extra h1 inp_b len;
  ()
val lemma_call_poly1305 (h0 h1:HS.mem) (ctx_b:PS.uint8_p) (inp_b:PS.uint8_p) (src key:bytes) : Lemma
  (requires (
    let open PU in
    let len = length src in
    B.live h1 ctx_b /\
    // copied from Vale.Wrapper.X64.Poly.poly1305:
    B.live h0 ctx_b /\ B.live h0 inp_b /\
    B.length ctx_b == 192 /\
    B.length inp_b == 8 * readable_words len /\
    // interface to Poly1305.Equiv:
    equal (BF.of_bytes key) (slice (B.as_seq h0 ctx_b) 24 56) /\
    equal (BF.of_bytes src) (slice (B.as_seq h1 inp_b) 0 len)
  ))
  (ensures (
    let open PU in
    let open PM in
    let open PS in
    let open IT in
    assert (view_n TUInt8 == 1);
    assert (view_n TUInt64 == 8);
    let len = length src in

    // copied from Vale.Wrapper.X64.Poly.poly1305:
    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 key_r0 = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h0 ctx_b 3) in
    let key_r1 = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h0 ctx_b 4) in
    let key_s0 = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h0 ctx_b 5) in
    let key_s1 = UInt64.v (MH.low_buffer_read TUInt8 TUInt64 h0 ctx_b 6) in
    let h_in = lowerUpper192 (lowerUpper128 h0_in h1_in) h2_in in
    let key_r = lowerUpper128 key_r0 key_r1 in
    let key_s = lowerUpper128 key_s0 key_s1 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 h10 = lowerUpper128 h0_out h1_out in
    let db = get_downview inp_b in
    math_aux inp_b (readable_words len);
    let inp_mem = seqTo128 (uint64_to_nat_seq (UV.as_seq h1 (UV.mk_buffer db Vale.Interop.Views.up_view64))) in
    let n = 0x10000000000000000 in
    let h_call = poly1305_hash_blocks (modp h_in) (n * n) (make_r key_r) inp_mem (len / 16) in
    let h_call' = poly1305_hash_all (modp h_in) key_r key_s inp_mem len in

    // interface to Poly1305.Equiv:
    let key_r_spec:nat128 = nat_from_bytes_le (slice key 0 16) in
    let key_s_spec:nat128 = nat_from_bytes_le (slice key 16 32) in
    let h_spec = poly1305_hash_blocks (modp h_in) (n * n) (make_r key_r) (block_fun src) (len / 16) in
    let h_spec' = poly1305_hash_all (modp h_in) key_r key_s (block_fun src) len in
    let tag = BF.to_bytes (slice (B.as_seq h1 ctx_b) 0 16) in
    key_r == key_r_spec /\ key_s == key_s_spec /\ h_call == h_spec /\ h_call' == h_spec' /\
    h10 == nat_from_bytes_le tag
  ))

    h0: FStar.Monotonic.HyperStack.mem ->
    h1: FStar.Monotonic.HyperStack.mem ->
    ctx_b: Vale.Wrapper.X64.Poly.uint8_p ->
    inp_b: Vale.Wrapper.X64.Poly.uint8_p ->
    src: Vale.Poly1305.Equiv.bytes ->
    key: Vale.Poly1305.Equiv.bytes
  -> FStar.Pervasives.Lemma
      (requires
        (let len = FStar.Seq.Base.length src in
          LowStar.Monotonic.Buffer.live h1 ctx_b /\ LowStar.Monotonic.Buffer.live h0 ctx_b /\
          LowStar.Monotonic.Buffer.live h0 inp_b /\ LowStar.Monotonic.Buffer.length ctx_b == 192 /\
          LowStar.Monotonic.Buffer.length inp_b == 8 * Vale.Poly1305.Util.readable_words len /\
          FStar.Seq.Base.equal (Vale.Arch.BufferFriend.of_bytes key)
            (FStar.Seq.Base.slice (LowStar.Monotonic.Buffer.as_seq h0 ctx_b) 24 56) /\
          FStar.Seq.Base.equal (Vale.Arch.BufferFriend.of_bytes src)
            (FStar.Seq.Base.slice (LowStar.Monotonic.Buffer.as_seq h1 inp_b) 0 len)))
      (ensures
        ([@@ FStar.Pervasives.inline_let ]let _ =
            assert (Vale.Interop.Types.view_n Vale.Arch.HeapTypes_s.TUInt8 == 1)
          in
          [@@ FStar.Pervasives.inline_let ]let _ =
            assert (Vale.Interop.Types.view_n Vale.Arch.HeapTypes_s.TUInt64 == 8)
          in
          let len = FStar.Seq.Base.length src in
          [@@ FStar.Pervasives.inline_let ]let _ =
            LowStar.BufferView.Down.length_eq (Vale.Interop.Types.get_downview ctx_b)
          in
          let h0_in =
            FStar.UInt64.v (Vale.AsLowStar.MemoryHelpers.low_buffer_read Vale.Arch.HeapTypes_s.TUInt8
                  Vale.Arch.HeapTypes_s.TUInt64
                  h0
                  ctx_b
                  0)
          in
          let h1_in =
            FStar.UInt64.v (Vale.AsLowStar.MemoryHelpers.low_buffer_read Vale.Arch.HeapTypes_s.TUInt8
                  Vale.Arch.HeapTypes_s.TUInt64
                  h0
                  ctx_b
                  1)
          in
          let h2_in =
            FStar.UInt64.v (Vale.AsLowStar.MemoryHelpers.low_buffer_read Vale.Arch.HeapTypes_s.TUInt8
                  Vale.Arch.HeapTypes_s.TUInt64
                  h0
                  ctx_b
                  2)
          in
          let key_r0 =
            FStar.UInt64.v (Vale.AsLowStar.MemoryHelpers.low_buffer_read Vale.Arch.HeapTypes_s.TUInt8
                  Vale.Arch.HeapTypes_s.TUInt64
                  h0
                  ctx_b
                  3)
          in
          let key_r1 =
            FStar.UInt64.v (Vale.AsLowStar.MemoryHelpers.low_buffer_read Vale.Arch.HeapTypes_s.TUInt8
                  Vale.Arch.HeapTypes_s.TUInt64
                  h0
                  ctx_b
                  4)
          in
          let key_s0 =
            FStar.UInt64.v (Vale.AsLowStar.MemoryHelpers.low_buffer_read Vale.Arch.HeapTypes_s.TUInt8
                  Vale.Arch.HeapTypes_s.TUInt64
                  h0
                  ctx_b
                  5)
          in
          let key_s1 =
            FStar.UInt64.v (Vale.AsLowStar.MemoryHelpers.low_buffer_read Vale.Arch.HeapTypes_s.TUInt8
                  Vale.Arch.HeapTypes_s.TUInt64
                  h0
                  ctx_b
                  6)
          in
          let h_in =
            Vale.Poly1305.Math.lowerUpper192 (Vale.Poly1305.Math.lowerUpper128 h0_in h1_in) h2_in
          in
          let key_r = Vale.Poly1305.Math.lowerUpper128 key_r0 key_r1 in
          let key_s = Vale.Poly1305.Math.lowerUpper128 key_s0 key_s1 in
          let h0_out =
            FStar.UInt64.v (Vale.AsLowStar.MemoryHelpers.low_buffer_read Vale.Arch.HeapTypes_s.TUInt8
                  Vale.Arch.HeapTypes_s.TUInt64
                  h1
                  ctx_b
                  0)
          in
          let h1_out =
            FStar.UInt64.v (Vale.AsLowStar.MemoryHelpers.low_buffer_read Vale.Arch.HeapTypes_s.TUInt8
                  Vale.Arch.HeapTypes_s.TUInt64
                  h1
                  ctx_b
                  1)
          in
          let h2_out =
            FStar.UInt64.v (Vale.AsLowStar.MemoryHelpers.low_buffer_read Vale.Arch.HeapTypes_s.TUInt8
                  Vale.Arch.HeapTypes_s.TUInt64
                  h1
                  ctx_b
                  2)
          in
          let h10 = Vale.Poly1305.Math.lowerUpper128 h0_out h1_out in
          let db = Vale.Interop.Types.get_downview inp_b in
          [@@ FStar.Pervasives.inline_let ]let _ =
            Vale.Wrapper.X64.Poly.math_aux inp_b (Vale.Poly1305.Util.readable_words len)
          in
          let inp_mem =
            Vale.Poly1305.Util.seqTo128 (Vale.Wrapper.X64.Poly.uint64_to_nat_seq (LowStar.BufferView.Up.as_seq
                      h1
                      (LowStar.BufferView.Up.mk_buffer db Vale.Interop.Views.up_view64)))
          in
          let n = 0x10000000000000000 in
          let h_call =
            Vale.Poly1305.Spec_s.poly1305_hash_blocks (Vale.Poly1305.Spec_s.modp h_in)
              (n * n)
              (Vale.Poly1305.Spec_s.make_r key_r)
              inp_mem
              (len / 16)
          in
          let h_call' =
            Vale.Poly1305.Spec_s.poly1305_hash_all (Vale.Poly1305.Spec_s.modp h_in)
              key_r
              key_s
              inp_mem
              len
          in
          let key_r_spec = Vale.Poly1305.Equiv.nat_from_bytes_le (FStar.Seq.Base.slice key 0 16) in
          let key_s_spec = Vale.Poly1305.Equiv.nat_from_bytes_le (FStar.Seq.Base.slice key 16 32) in
          let h_spec =
            Vale.Poly1305.Spec_s.poly1305_hash_blocks (Vale.Poly1305.Spec_s.modp h_in)
              (n * n)
              (Vale.Poly1305.Spec_s.make_r key_r)
              (Vale.Poly1305.Equiv.block_fun src)
              (len / 16)
          in
          let h_spec' =
            Vale.Poly1305.Spec_s.poly1305_hash_all (Vale.Poly1305.Spec_s.modp h_in)
              key_r
              key_s
              (Vale.Poly1305.Equiv.block_fun src)
              len
          in
          let tag =
            Vale.Arch.BufferFriend.to_bytes (FStar.Seq.Base.slice (LowStar.Monotonic.Buffer.as_seq h1
                      ctx_b)
                  0
                  16)
          in
          key_r == key_r_spec /\ key_s == key_s_spec /\ h_call == h_spec /\ h_call' == h_spec' /\
          h10 == Vale.Poly1305.Equiv.nat_from_bytes_le tag))