val 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)})
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
val 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)})
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);
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
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.UInt8.t FStar.UInt32.t Prims.b2t Prims.op_LessThan FStar.UInt32.v Prims.l_and Prims.op_LessThanOrEqual FStar.UInt8.shift_right FStar.UInt32.add FStar.UInt32.sub FStar.UInt32.__uint_to_t FStar.UInt8.shift_left Prims.unit LowParse.BitFields.get_bitfield_eq_2 FStar.UInt8.v FStar.UInt.size 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})
val 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)})

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