val lemma_be_to_n_is_nat_from_bytes (s:FE.bytes) : Lemma
  (ensures FE.be_to_n s == BS.nat_from_bytes_be (to_bytes s))
  (decreases (length s))
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))
val lemma_be_to_n_is_nat_from_bytes (s:FE.bytes) : Lemma
  (ensures FE.be_to_n s == BS.nat_from_bytes_be (to_bytes s))
  (decreases (length s))
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))
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
FStar.Endianness.bytes Prims.op_GreaterThan FStar.Seq.Base.length FStar.UInt8.t Vale.Arch.BufferFriend.lemma_be_to_n_is_nat_from_bytes FStar.Seq.Base.slice Prims.op_Subtraction Prims.bool Prims.unit
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)))
val lemma_be_to_n_is_nat_from_bytes (s:FE.bytes) : Lemma
  (ensures FE.be_to_n s == BS.nat_from_bytes_be (to_bytes s))
  (decreases (length s))
s: FStar.Endianness.bytes
  -> FStar.Pervasives.Lemma
      (ensures
        FStar.Endianness.be_to_n s ==
        Lib.ByteSequence.nat_from_bytes_be (Vale.Arch.BufferFriend.to_bytes s))
      (decreases FStar.Seq.Base.length s)