val nat_from_bytes_le_is_le_bytes_to_nat64 (b:BS.bytes) : Lemma
  (requires length b == 8)
  (ensures
    length (of_bytes b) == 8 /\
    BS.nat_from_bytes_le b == le_bytes_to_nat64 (Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8 (of_bytes b))
  )
let nat_from_bytes_le_is_le_bytes_to_nat64 b =
  let open Vale.Def.Words.Seq_s in
  let open Vale.Def.Words.Two_s in
  let open Vale.Def.Words.Four_s in
  let open Vale.Lib.Seqs_s in
  let sn = seq_uint8_to_seq_nat8 (of_bytes b) in
  let s01 = seq_nat8_to_seq_nat32_LE sn in
  calc (==) {
    index s01 0;
    == {}
    index (seq_map (four_to_nat 8) (seq_to_seq_four_LE sn)) 0;
    == {reveal_opaque (`%seq_to_seq_four_LE) (seq_to_seq_four_LE #nat8)}
    four_to_nat 8 (Mkfour sn.[0] sn.[1] sn.[2] sn.[3]);
    == {nat_from_bytes_le_is_le_bytes_to_nat32 (slice b 0 4)}
    BS.nat_from_bytes_le (slice b 0 4);
  };
  calc (==) {
    index s01 1;
    == {}
    index (seq_map (four_to_nat 8) (seq_to_seq_four_LE sn)) 1;
    == {reveal_opaque (`%seq_to_seq_four_LE) (seq_to_seq_four_LE #nat8)}
    four_to_nat 8 (Mkfour sn.[4] sn.[5] sn.[6] sn.[7]);
    == {nat_from_bytes_le_is_le_bytes_to_nat32 (slice b 4 8)}
    BS.nat_from_bytes_le (slice b 4 8);
  };
  calc (==) {
    le_bytes_to_nat64 sn <: int;
    == {le_bytes_to_nat64_reveal ()}
    two_to_nat 32 (seq_to_two_LE s01) <: int;
    == {assert_norm (two_to_nat 32 (seq_to_two_LE s01) == index s01 0 + pow2 32 * index s01 1)}
    index s01 0 + pow2 32 * index s01 1;
    == {}
    BS.nat_from_bytes_le (slice b 0 4) + pow2 32 * BS.nat_from_bytes_le (slice b 4 8) <: int;
    == {BS.nat_from_intseq_le_slice_lemma #LI.U8 #LI.SEC #8 b 4}
    BS.nat_from_bytes_le b <: int;
  }
val nat_from_bytes_le_is_le_bytes_to_nat64 (b:BS.bytes) : Lemma
  (requires length b == 8)
  (ensures
    length (of_bytes b) == 8 /\
    BS.nat_from_bytes_le b == le_bytes_to_nat64 (Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8 (of_bytes b))
  )
let nat_from_bytes_le_is_le_bytes_to_nat64 b =
let open Vale.Def.Words.Seq_s in
let open Vale.Def.Words.Two_s in
let open Vale.Def.Words.Four_s in
let open Vale.Lib.Seqs_s in
let sn = seq_uint8_to_seq_nat8 (of_bytes b) in
let s01 = seq_nat8_to_seq_nat32_LE sn in
calc ( == ) {
  index s01 0;
  ( == ) { () }
  index (seq_map (four_to_nat 8) (seq_to_seq_four_LE sn)) 0;
  ( == ) { reveal_opaque (`%seq_to_seq_four_LE) (seq_to_seq_four_LE #nat8) }
  four_to_nat 8 (Mkfour sn.[ 0 ] sn.[ 1 ] sn.[ 2 ] sn.[ 3 ]);
  ( == ) { nat_from_bytes_le_is_le_bytes_to_nat32 (slice b 0 4) }
  BS.nat_from_bytes_le (slice b 0 4);
};
calc ( == ) {
  index s01 1;
  ( == ) { () }
  index (seq_map (four_to_nat 8) (seq_to_seq_four_LE sn)) 1;
  ( == ) { reveal_opaque (`%seq_to_seq_four_LE) (seq_to_seq_four_LE #nat8) }
  four_to_nat 8 (Mkfour sn.[ 4 ] sn.[ 5 ] sn.[ 6 ] sn.[ 7 ]);
  ( == ) { nat_from_bytes_le_is_le_bytes_to_nat32 (slice b 4 8) }
  BS.nat_from_bytes_le (slice b 4 8);
};
calc ( == ) {
  le_bytes_to_nat64 sn <: int;
  ( == ) { le_bytes_to_nat64_reveal () }
  two_to_nat 32 (seq_to_two_LE s01) <: int;
  ( == ) { assert_norm (two_to_nat 32 (seq_to_two_LE s01) == index s01 0 + pow2 32 * index s01 1) }
  index s01 0 + pow2 32 * index s01 1;
  ( == ) { () }
  BS.nat_from_bytes_le (slice b 0 4) + pow2 32 * BS.nat_from_bytes_le (slice b 4 8) <: int;
  ( == ) { BS.nat_from_intseq_le_slice_lemma #LI.U8 #LI.SEC #8 b 4 }
  BS.nat_from_bytes_le b <: int;
}
Vale.Arch.BufferFriend.fst.checked
Vale.Wrapper.X64.Poly.fsti.checked Vale.Poly1305.Util.fsti.checked Vale.Lib.Seqs_s.fst.checked Vale.Interop.Views.fsti.checked Vale.Interop.Types.fst.checked Vale.Def.Words.Two_s.fsti.checked Vale.Def.Words.Seq_s.fsti.checked Vale.Def.Words.Four_s.fsti.checked prims.fst.checked LowStar.BufferView.Up.fst.checked Lib.RawIntTypes.fst.checked Lib.IntTypes.fst.checked Lib.ByteSequence.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Endianness.fst.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
Vale.Arch.BufferFriend.fst
Lib.ByteSequence.bytes FStar.Calc.calc_finish Prims.int Prims.eq2 Vale.Def.Types_s.le_bytes_to_nat64 Lib.ByteSequence.nat_from_bytes_le Lib.IntTypes.SEC Prims.Cons FStar.Preorder.relation Prims.Nil Prims.unit FStar.Calc.calc_step Prims.op_Addition FStar.Seq.Base.slice Lib.IntTypes.uint_t Lib.IntTypes.U8 FStar.Mul.op_Star Prims.pow2 FStar.Seq.Base.index Vale.Def.Words_s.nat32 Vale.Def.Words.Two_s.two_to_nat Vale.Def.Words.Seq_s.seq_to_two_LE FStar.Calc.calc_init FStar.Calc.calc_pack Vale.Def.Types_s.le_bytes_to_nat64_reveal Prims.squash FStar.Pervasives.assert_norm Lib.ByteSequence.nat_from_intseq_le_slice_lemma Vale.Def.Words.Four_s.four_to_nat Vale.Def.Words_s.Mkfour Vale.Def.Words_s.natN Vale.Arch.BufferFriend.op_String_Access Vale.Def.Words_s.nat8 Vale.Lib.Seqs_s.seq_map Vale.Def.Words_s.four Vale.Def.Words.Seq_s.seq_to_seq_four_LE FStar.Pervasives.reveal_opaque FStar.Seq.Base.seq Vale.Def.Types_s.nat8 Prims.op_Modulus FStar.Seq.Base.length Prims.op_Division Vale.Arch.BufferFriend.nat_from_bytes_le_is_le_bytes_to_nat32 Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8 Vale.Arch.BufferFriend.of_bytes
module Vale.Arch.BufferFriend
open FStar.Mul
friend Lib.IntTypes
friend Lib.RawIntTypes
friend Lib.ByteSequence
friend LowStar.BufferView.Up
friend FStar.Endianness

module PU = Vale.Poly1305.Util
module IT = Vale.Interop.Types
module PS = Vale.Wrapper.X64.Poly
module BS = Lib.ByteSequence
module Raw = Lib.RawIntTypes

unfold let (.[]) = index

let to_bytes s = s
let of_bytes b = b

let lemma_to_bytes_slice b i j = ()
let lemma_of_bytes_slice b i j = ()

let lemma_up_as_seq_index #b h vb i =
  let s0 = DV.as_seq h (UV.as_down_buffer vb) in
  let v = UV.get_view vb in
  let n = UV.View?.n v in
  let start = i * n in
  let s_i = slice s0 start (start + n) in
  UV.as_seq_sel h vb i;
  assert (index (UV.as_seq h vb) i == UV.View?.get v s_i)

let same_seq_downview8 b h =
  let db = DV.mk_buffer_view b (Vale.Interop.Views.down_view8) in
  DV.length_eq db;
  let s = B.as_seq h b in
  let sdb = DV.as_seq h db in
  let aux (i:nat{i < B.length b}) : Lemma (Seq.index sdb i == Seq.index s i)
    = DV.as_seq_sel h db i;
      DV.get_sel h db i;
      Vale.Interop.Views.put8_reveal ()
  in
  Classical.forall_intro aux;
  assert (Seq.equal s sdb)

let lemma_raw_nat_from_bytes_le_0 (b:BS.bytes) : Lemma
  (requires length b == 0)
  (ensures BS.nat_from_bytes_le b == 0)
  =
  ()

#reset-options "--z3cliopt smt.arith.nl=true"
let lemma_raw_nat_from_bytes_le_n (b:BS.bytes) : Lemma
  (requires length b > 0)
  (ensures BS.nat_from_bytes_le b == Raw.uint_to_nat b.[0] + pow2 8 * (BS.nat_from_bytes_le (slice b 1 (length b))))
  =
  ()

let rec lemma_le_to_n_is_nat_from_bytes (s:FE.bytes) =
  //FE.reveal_le_to_n s;
  if length s > 0 then lemma_le_to_n_is_nat_from_bytes (Seq.tail s)

let rec lemma_n_to_le_is_nat_to_bytes (len:nat) (n:nat) =
  //FE.reveal_n_to_le len n;
  if len > 0 then
  (
    FStar.Math.Lemmas.pow2_plus 8 (8 * (len - 1));
    lemma_n_to_le_is_nat_to_bytes (len - 1) (n / 256);
    ()
  );
  assert (equal (FE.n_to_le len n) (of_bytes (BS.nat_to_bytes_le len n)))

let rec lemma_be_to_n_is_nat_from_bytes (s:FE.bytes) =
  if length s > 0 then lemma_be_to_n_is_nat_from_bytes (Seq.slice s 0 (length s - 1))

let rec lemma_n_to_be_is_nat_to_bytes (len: nat) (n: nat) =
  if len > 0 then (
    FStar.Math.Lemmas.pow2_plus 8 (8 * (len - 1));
    lemma_n_to_be_is_nat_to_bytes (len - 1) (n / 256)
  );
  assert (equal (FE.n_to_be len n) (of_bytes (BS.nat_to_bytes_be len n)))

#reset-options

let nat_from_bytes_le_is_four_to_nat b =
  let s = b in
  lemma_raw_nat_from_bytes_le_n s; assert (b.[0] == s.[0]); let s = slice s 1 (length s) in
  lemma_raw_nat_from_bytes_le_n s; assert (b.[1] == s.[0]); let s = slice s 1 (length s) in
  lemma_raw_nat_from_bytes_le_n s; assert (b.[2] == s.[0]); let s = slice s 1 (length s) in
  lemma_raw_nat_from_bytes_le_n s; assert (b.[3] == s.[0]); let s = slice s 1 (length s) in
  lemma_raw_nat_from_bytes_le_0 s;
  assert_norm (
    BS.nat_from_bytes_le b ==
    Vale.Def.Words.Four_s.four_to_nat 8 (Vale.Def.Words.Four_s.four_map Raw.uint_to_nat (Vale.Def.Words.Seq_s.seq_to_four_LE b))
  )

let nat_from_bytes_le_is_le_bytes_to_nat32 b =
  let open Vale.Def.Words.Seq_s in
  let open Vale.Def.Words.Four_s in
  let open Vale.Lib.Seqs_s in
  let sn = seq_uint8_to_seq_nat8 (of_bytes b) in
  let s = seq_nat8_to_seq_nat32_LE sn in
  calc (==) {
    le_bytes_to_nat32 sn;
    == {}
    four_to_nat 8 (Mkfour sn.[0] sn.[1] sn.[2] sn.[3]);
    == {nat_from_bytes_le_is_four_to_nat b}
    BS.nat_from_bytes_le b;
  }
val nat_from_bytes_le_is_le_bytes_to_nat64 (b:BS.bytes) : Lemma
  (requires length b == 8)
  (ensures
    length (of_bytes b) == 8 /\
    BS.nat_from_bytes_le b == le_bytes_to_nat64 (Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8 (of_bytes b))
  )
b: Lib.ByteSequence.bytes
  -> FStar.Pervasives.Lemma (requires FStar.Seq.Base.length b == 8)
      (ensures
        FStar.Seq.Base.length (Vale.Arch.BufferFriend.of_bytes b) == 8 /\
        Lib.ByteSequence.nat_from_bytes_le b ==
        Vale.Def.Types_s.le_bytes_to_nat64 (Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8 (Vale.Arch.BufferFriend.of_bytes
                  b)))