val buf_eq_mask:
    #t:inttype{~(S128? t)}
  -> #len1:size_t
  -> #len2:size_t
  -> b1:lbuffer (int_t t SEC) len1
  -> b2:lbuffer (int_t t SEC) len2
  -> len:size_t{v len <= v len1 /\ v len <= v len2}
  -> res:lbuffer (int_t t SEC) (size 1) ->
  Stack (int_t t SEC)
    (requires fun h ->
      live h b1 /\ live h b2 /\ live h res /\ disjoint res b1 /\ disjoint res b2 /\
      v (bget h res 0) == v (ones t SEC))
    (ensures fun h0 z h1 ->
      modifies1 res h0 h1 /\
      v z == v (BS.seq_eq_mask (as_seq h0 b1) (as_seq h0 b2) (v len)))
let buf_eq_mask #t #len1 #len2 b1 b2 len res =
  let h0 = ST.get() in
  let inv h (i:nat{i <= v len}) =
    modifies1 res h0 h /\
    v (bget h res 0) == v (BS.seq_eq_mask (as_seq h0 b1) (as_seq h0 b2) i)
  in
  Lib.Loops.for 0ul len inv
    (fun i ->
      let z0 = res.(0ul) in
      res.(0ul) <- eq_mask b1.(i) b2.(i) &. res.(0ul);
      let z = res.(0ul) in
      assert (z == BS.seq_eq_mask_inner (as_seq h0 b1) (as_seq h0 b2) (v len) (v i) z0));
  res.(0ul)
val buf_eq_mask:
    #t:inttype{~(S128? t)}
  -> #len1:size_t
  -> #len2:size_t
  -> b1:lbuffer (int_t t SEC) len1
  -> b2:lbuffer (int_t t SEC) len2
  -> len:size_t{v len <= v len1 /\ v len <= v len2}
  -> res:lbuffer (int_t t SEC) (size 1) ->
  Stack (int_t t SEC)
    (requires fun h ->
      live h b1 /\ live h b2 /\ live h res /\ disjoint res b1 /\ disjoint res b2 /\
      v (bget h res 0) == v (ones t SEC))
    (ensures fun h0 z h1 ->
      modifies1 res h0 h1 /\
      v z == v (BS.seq_eq_mask (as_seq h0 b1) (as_seq h0 b2) (v len)))
let buf_eq_mask #t #len1 #len2 b1 b2 len res =
let h0 = ST.get () in
let inv h (i: nat{i <= v len}) =
  modifies1 res h0 h /\ v (bget h res 0) == v (BS.seq_eq_mask (as_seq h0 b1) (as_seq h0 b2) i)
in
Lib.Loops.for 0ul
  len
  inv
  (fun i ->
      let z0 = res.(0ul) in
      res.(0ul) <- eq_mask b1.(i) b2.(i) &. res.(0ul);
      let z = res.(0ul) in
      assert (z == BS.seq_eq_mask_inner (as_seq h0 b1) (as_seq h0 b2) (v len) (v i) z0));
res.(0ul)
Lib.ByteBuffer.fst.checked
prims.fst.checked LowStar.Endianness.fst.checked LowStar.Buffer.fst.checked Lib.Sequence.fsti.checked Lib.RawIntTypes.fsti.checked Lib.Loops.fsti.checked Lib.LoopCombinators.fsti.checked Lib.IntTypes.fst.checked Lib.IntTypes.fst.checked Lib.ByteSequence.fst.checked Lib.Buffer.fsti.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Math.Lemmas.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Endianness.fst.checked
Lib.ByteBuffer.fst
Lib.IntTypes.inttype Prims.l_not Prims.b2t Lib.IntTypes.uu___is_S128 Lib.IntTypes.size_t Lib.Buffer.lbuffer Lib.IntTypes.int_t Lib.IntTypes.SEC Prims.l_and Prims.op_LessThanOrEqual Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB Lib.IntTypes.size Lib.Buffer.op_Array_Access Lib.Buffer.MUT FStar.UInt32.__uint_to_t Prims.unit Lib.Loops.for Prims.op_LessThan Prims._assert Prims.eq2 Lib.ByteSequence.seq_eq_mask_inner Lib.Buffer.as_seq Lib.Buffer.op_Array_Assignment Lib.IntTypes.op_Amp_Dot Lib.IntTypes.eq_mask FStar.Monotonic.HyperStack.mem Prims.nat Prims.logical Lib.Buffer.modifies1 Lib.IntTypes.range_t Lib.Buffer.bget Lib.ByteSequence.seq_eq_mask FStar.HyperStack.ST.get
module Lib.ByteBuffer

open FStar.HyperStack
open FStar.HyperStack.ST
open LowStar.Buffer

open Lib.IntTypes
open Lib.Buffer

module ST = FStar.HyperStack.ST
module Loops = Lib.LoopCombinators
module Raw = Lib.RawIntTypes

friend Lib.ByteSequence
friend Lib.IntTypes
friend FStar.Endianness

module E = LowStar.Endianness

(*
 * Despite befriending IntTypes this module enforces secrecy. The only exception,
 * for backwards compatibility, is `lbytes_eq`, which declassifies its result.
 *
 * We befriend IntTypes (or use RawIntTypes) to call into LowStar.Endianness library
 * for endianness conversions, which uses public machine integers.
 * E.g. `uint_to_bytes_le` loads a secret integer into a buffer of secret bytes by
 * internally casting the integer to a public machine integer, calling into LowStar,
 * and converting the result back to secret bytes.
 *
 * We use RawIntTypes when possible and only when this would be inconvenient
 * rely on opening the definitions in IntTypes. Specifically, only
 * `uint_from_bytes_le`, uint_from_bytes_be`, `uint_to_bytes_le`, and `uint_to_bytes_be`
 * rely on definitions in IntTypes. Alternatively, RawIntTypes could be used to cast
 * sequences and buffers of secret integers to sequences and buffers of machine integers,
 * but this would be too cumbersome.
*)

#set-options "--z3rlimit 50 --max_fuel 0 --max_ifuel 1"

let uint_to_be #t #l u =
  match t, l with
  | U1, _ -> u
  | U8, _ -> u
  | U16, PUB -> LowStar.Endianness.htobe16 u
  | U16, SEC -> Raw.u16_from_UInt16 (LowStar.Endianness.htobe16 (Raw.u16_to_UInt16 u))
  | U32, PUB -> LowStar.Endianness.htobe32 u
  | U32, SEC -> Raw.u32_from_UInt32 (LowStar.Endianness.htobe32 (Raw.u32_to_UInt32 u))
  | U64, PUB -> LowStar.Endianness.htobe64 u
  | U64, SEC -> Raw.u64_from_UInt64 (LowStar.Endianness.htobe64 (Raw.u64_to_UInt64 u))

let uint_to_le #t #l u =
  match t, l with
  | U1, _ -> u
  | U8, _ -> u
  | U16, PUB -> LowStar.Endianness.htole16 u
  | U16, SEC -> Raw.u16_from_UInt16 (LowStar.Endianness.htole16 (Raw.u16_to_UInt16 u))
  | U32, PUB -> LowStar.Endianness.htole32 u
  | U32, SEC -> Raw.u32_from_UInt32 (LowStar.Endianness.htole32 (Raw.u32_to_UInt32 u))
  | U64, PUB -> LowStar.Endianness.htole64 u
  | U64, SEC -> Raw.u64_from_UInt64 (LowStar.Endianness.htole64 (Raw.u64_to_UInt64 u))

let uint_from_be #t #l u =
  match t, l with
  | U1, _ -> u
  | U8, _ -> u
  | U16, PUB -> LowStar.Endianness.be16toh u
  | U16, SEC -> Raw.u16_from_UInt16 (LowStar.Endianness.be16toh (Raw.u16_to_UInt16 u))
  | U32, PUB -> LowStar.Endianness.be32toh u
  | U32, SEC -> Raw.u32_from_UInt32 (LowStar.Endianness.be32toh (Raw.u32_to_UInt32 u))
  | U64, PUB -> LowStar.Endianness.be64toh u
  | U64, SEC -> Raw.u64_from_UInt64 (LowStar.Endianness.be64toh (Raw.u64_to_UInt64 u))

let uint_from_le #t #l u =
  match t, l with
  | U1, _ -> u
  | U8, _ -> u
  | U16, PUB -> LowStar.Endianness.le16toh u
  | U16, SEC -> Raw.u16_from_UInt16 (LowStar.Endianness.le16toh (Raw.u16_to_UInt16 u))
  | U32, PUB -> LowStar.Endianness.le32toh u
  | U32, SEC -> Raw.u32_from_UInt32 (LowStar.Endianness.le32toh (Raw.u32_to_UInt32 u))
  | U64, PUB -> LowStar.Endianness.le64toh u
  | U64, SEC -> Raw.u64_from_UInt64 (LowStar.Endianness.le64toh (Raw.u64_to_UInt64 u))
val buf_eq_mask:
    #t:inttype{~(S128? t)}
  -> #len1:size_t
  -> #len2:size_t
  -> b1:lbuffer (int_t t SEC) len1
  -> b2:lbuffer (int_t t SEC) len2
  -> len:size_t{v len <= v len1 /\ v len <= v len2}
  -> res:lbuffer (int_t t SEC) (size 1) ->
  Stack (int_t t SEC)
    (requires fun h ->
      live h b1 /\ live h b2 /\ live h res /\ disjoint res b1 /\ disjoint res b2 /\
      v (bget h res 0) == v (ones t SEC))
    (ensures fun h0 z h1 ->
      modifies1 res h0 h1 /\
      v z == v (BS.seq_eq_mask (as_seq h0 b1) (as_seq h0 b2) (v len)))

    b1: Lib.Buffer.lbuffer (Lib.IntTypes.int_t t Lib.IntTypes.SEC) len1 ->
    b2: Lib.Buffer.lbuffer (Lib.IntTypes.int_t t Lib.IntTypes.SEC) len2 ->
    len:
      Lib.IntTypes.size_t
        {Lib.IntTypes.v len <= Lib.IntTypes.v len1 /\ Lib.IntTypes.v len <= Lib.IntTypes.v len2} ->
    res: Lib.Buffer.lbuffer (Lib.IntTypes.int_t t Lib.IntTypes.SEC) (Lib.IntTypes.size 1)
  -> FStar.HyperStack.ST.Stack (Lib.IntTypes.int_t t Lib.IntTypes.SEC)