val get_bitfield16
      (value: U16.t)
      (bitsFrom: U32.t{U32.v bitsFrom < 16})
      (bitsTo: U32.t{U32.v bitsFrom < U32.v bitsTo /\ U32.v bitsTo <= 16})
    : i: U16.t{FStar.UInt.size (U16.v i) (U32.v bitsTo - U32.v bitsFrom)}
let get_bitfield16 (value:U16.t)
                   (bitsFrom:U32.t{U32.v bitsFrom < 16})
                   (bitsTo:U32.t{U32.v bitsFrom < U32.v bitsTo /\ U32.v bitsTo <= 16})
   : i:U16.t{FStar.UInt.size (U16.v i) (U32.v bitsTo - U32.v bitsFrom)}
   = LBF.uint16.LBF.get_bitfield_gen value bitsFrom bitsTo
val get_bitfield16
      (value: U16.t)
      (bitsFrom: U32.t{U32.v bitsFrom < 16})
      (bitsTo: U32.t{U32.v bitsFrom < U32.v bitsTo /\ U32.v bitsTo <= 16})
    : i: U16.t{FStar.UInt.size (U16.v i) (U32.v bitsTo - U32.v bitsFrom)}
let get_bitfield16
      (value: U16.t)
      (bitsFrom: U32.t{U32.v bitsFrom < 16})
      (bitsTo: U32.t{U32.v bitsFrom < U32.v bitsTo /\ U32.v bitsTo <= 16})
    : i: U16.t{FStar.UInt.size (U16.v i) (U32.v bitsTo - U32.v bitsFrom)} =
LBF.uint16.LBF.get_bitfield_gen value bitsFrom bitsTo
EverParse3d.Prelude.StaticHeader.fst.checked
prims.fst.checked LowParse.BitFields.fsti.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.UInt.fsti.checked FStar.Pervasives.fsti.checked
EverParse3d.Prelude.StaticHeader.fst
FStar.UInt16.t FStar.UInt32.t Prims.b2t Prims.op_LessThan FStar.UInt32.v Prims.l_and Prims.op_LessThanOrEqual LowParse.BitFields.__proj__Mkuint_t__item__get_bitfield_gen LowParse.BitFields.uint16 FStar.UInt.size FStar.UInt16.v Prims.op_Subtraction
module EverParse3d.Prelude.StaticHeader

module U64 = FStar.UInt64
module U32 = FStar.UInt32
module U16 = FStar.UInt16
module U8 = FStar.UInt8
module LBF = LowParse.BitFields

////////////////////////////////////////////////////////////////////////////////
// Bit fields
////////////////////////////////////////////////////////////////////////////////

// The get_bitfield operators are least significant bit first by default
// following MSVC (https://learn.microsoft.com/en-us/cpp/c-language/c-bit-fields)
let get_bitfield8
  (value:U8.t)
  (bitsFrom:U32.t{U32.v bitsFrom < 8})
  (bitsTo:U32.t{U32.v bitsFrom < U32.v bitsTo /\ U32.v bitsTo <= 8})
: Tot (i:U8.t{FStar.UInt.size (U8.v i) (U32.v bitsTo - U32.v bitsFrom)})
= LBF.get_bitfield_eq_2 #8 (U8.v value) (U32.v bitsFrom) (U32.v bitsTo);
  (* NOTE: due to https://github.com/FStarLang/karamel/issues/102 I need to introduce explicit let-bindings here *)
  let op1 = value `U8.shift_left` (8ul `U32.sub` bitsTo) in
  let op2 = op1 `U8.shift_right` ((8ul `U32.sub` bitsTo) `U32.add` bitsFrom) in
  op2

let get_bitfield16 (value:U16.t)
                   (bitsFrom:U32.t{U32.v bitsFrom < 16})
                   (bitsTo:U32.t{U32.v bitsFrom < U32.v bitsTo /\ U32.v bitsTo <= 16})
val get_bitfield16
      (value: U16.t)
      (bitsFrom: U32.t{U32.v bitsFrom < 16})
      (bitsTo: U32.t{U32.v bitsFrom < U32.v bitsTo /\ U32.v bitsTo <= 16})
    : i: U16.t{FStar.UInt.size (U16.v i) (U32.v bitsTo - U32.v bitsFrom)}

    value: FStar.UInt16.t ->
    bitsFrom: FStar.UInt32.t{FStar.UInt32.v bitsFrom < 16} ->
    bitsTo:
      FStar.UInt32.t{FStar.UInt32.v bitsFrom < FStar.UInt32.v bitsTo /\ FStar.UInt32.v bitsTo <= 16}
  -> i:
    FStar.UInt16.t
      {FStar.UInt.size (FStar.UInt16.v i) (FStar.UInt32.v bitsTo - FStar.UInt32.v bitsFrom)}