val get_bitfield
  (#t: inttype { supported_type t })
  (#l: secrecy_level)
  (x: uint_t t l)
  (lo: U32.t)
  (hi: U32.t { U32.v lo < U32.v hi /\ U32.v hi <= bits t })
: Tot (y: uint_t t l { v y == BF.get_bitfield #(bits t) (v x) (U32.v lo) (U32.v hi) })
let get_bitfield
  #t #l x lo hi
= BF.get_bitfield_eq_2 #(bits t) (v x) (U32.v lo) (U32.v hi);
  // due to https://github.com/FStarLang/karamel/issues/102 we need explicit intermediate operations here
  let op1 = x `shift_left` (U32.uint_to_t (bits t) `U32.sub` hi) in
  let op2 = op1 `shift_right` (U32.uint_to_t (bits t) `U32.sub` hi `U32.add` lo) in
  op2
val get_bitfield
  (#t: inttype { supported_type t })
  (#l: secrecy_level)
  (x: uint_t t l)
  (lo: U32.t)
  (hi: U32.t { U32.v lo < U32.v hi /\ U32.v hi <= bits t })
: Tot (y: uint_t t l { v y == BF.get_bitfield #(bits t) (v x) (U32.v lo) (U32.v hi) })
let get_bitfield #t #l x lo hi =
BF.get_bitfield_eq_2 #(bits t) (v x) (U32.v lo) (U32.v hi);
let op1 = x `shift_left` ((U32.uint_to_t (bits t)) `U32.sub` hi) in
let op2 = op1 `shift_right` (((U32.uint_to_t (bits t)) `U32.sub` hi) `U32.add` lo) in
op2
QUIC.Secret.Int.fst.checked
QUIC.Secret.Int.Aux.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked
QUIC.Secret.Int.fst
Lib.IntTypes.inttype Prims.b2t QUIC.Secret.Int.Base.supported_type Lib.IntTypes.secrecy_level Lib.IntTypes.uint_t FStar.UInt32.t Prims.l_and Prims.op_LessThan FStar.UInt32.v Prims.op_LessThanOrEqual Lib.IntTypes.bits Lib.IntTypes.int_t Lib.IntTypes.shift_right FStar.UInt32.add FStar.UInt32.sub FStar.UInt32.uint_to_t Lib.IntTypes.shift_left Prims.unit LowParse.BitFields.get_bitfield_eq_2 QUIC.Secret.Int.Base.v Prims.eq2 Prims.int Prims.l_or Lib.IntTypes.range FStar.UInt.size Prims.pow2 Prims.op_Subtraction LowParse.BitFields.get_bitfield
module QUIC.Secret.Int
module Aux = QUIC.Secret.Int.Aux

let usub
  #t #sec x y
= x `sub` y

let cast_up
  #t1 t2 #sec x
= cast t2 SEC x

let cast_down
  #t1 t2 #sec x
= cast t2 SEC x

let hide
  #t #sec x
= cast t SEC x

let reveal
  #t #sec x
= mk_int #t (v x)


let lognot'
  #t #l x
= U.nth_lemma #(bits t) (U.lognot (v x)) (v x `U.logxor` v (ones t l));
  x `logxor` ones t l

let logand_one_bit = Aux.logand_one_bit

let logor_one_bit = Aux.logor_one_bit

let logxor_one_bit = Aux.logxor_one_bit

let secret_bool = Aux.secret_bool

let lognot_one_bit = Aux.lognot_one_bit

#push-options "--z3rlimit 64"

#restart-solver

let get_bitfield
val get_bitfield
  (#t: inttype { supported_type t })
  (#l: secrecy_level)
  (x: uint_t t l)
  (lo: U32.t)
  (hi: U32.t { U32.v lo < U32.v hi /\ U32.v hi <= bits t })
: Tot (y: uint_t t l { v y == BF.get_bitfield #(bits t) (v x) (U32.v lo) (U32.v hi) })

    x: Lib.IntTypes.uint_t t l ->
    lo: FStar.UInt32.t ->
    hi:
      FStar.UInt32.t
        {FStar.UInt32.v lo < FStar.UInt32.v hi /\ FStar.UInt32.v hi <= Lib.IntTypes.bits t}
  -> y:
    Lib.IntTypes.uint_t t l
      { QUIC.Secret.Int.Base.v y ==
        LowParse.BitFields.get_bitfield (QUIC.Secret.Int.Base.v x)
          (FStar.UInt32.v lo)
          (FStar.UInt32.v hi) }