val logand_spec' (#t: inttype) (#l: secrecy_level) (a b: int_t t l)
    : Lemma (v (a `logand` b) == (v a) `logand_v` (v b)) [SMTPat (v (a `logand` b))]
let logand_spec'
  (#t:inttype)
  (#l:secrecy_level)
  (a:int_t t l)
  (b:int_t t l)
: Lemma (v (a `logand` b) == v a `logand_v` v b)
  [SMTPat (v (a `logand` b))]
= logand_spec a b
val logand_spec' (#t: inttype) (#l: secrecy_level) (a b: int_t t l)
    : Lemma (v (a `logand` b) == (v a) `logand_v` (v b)) [SMTPat (v (a `logand` b))]
let logand_spec' (#t: inttype) (#l: secrecy_level) (a b: int_t t l)
    : Lemma (v (a `logand` b) == (v a) `logand_v` (v b)) [SMTPat (v (a `logand` b))] =
logand_spec a b
QUIC.Secret.Int.fsti.checked
QUIC.Secret.Int.Base.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
QUIC.Secret.Int.fsti
Lib.IntTypes.inttype Lib.IntTypes.secrecy_level Lib.IntTypes.int_t Lib.IntTypes.logand_spec Prims.unit Prims.l_True Prims.squash Prims.eq2 Lib.IntTypes.range_t QUIC.Secret.Int.Base.v Lib.IntTypes.logand Lib.IntTypes.logand_v Prims.Cons FStar.Pervasives.pattern FStar.Pervasives.smt_pat Prims.Nil
module QUIC.Secret.Int
include QUIC.Secret.Int.Base

module U8 = FStar.UInt8
module U16 = FStar.UInt16
module U32 = FStar.UInt32
module U64 = FStar.UInt64
module U = FStar.UInt
module BF = LowParse.BitFields

inline_for_extraction
noextract
val usub
  (#t: inttype { unsigned t })
  (#sec: secrecy_level)
  (x: uint_t t sec)
  (y: uint_t t sec { v y <= v x })
: Tot (z: uint_t t sec { v z == v x - v y })

inline_for_extraction
noextract
val cast_up
  (#t1: inttype { unsigned t1 })
  (t2: inttype { unsigned t2 /\ bits t1 <= bits t2 })
  (#sec: secrecy_level)
  (x: uint_t t1 sec)
: Tot (y: uint_t t2 SEC { v y == v x })

inline_for_extraction
noextract
val cast_down
  (#t1: inttype { unsigned t1 })
  (t2: inttype { unsigned t2 })
  (#sec: secrecy_level)
  (x: uint_t t1 sec { v x < pow2 (bits t2) } )
: Tot (y: uint_t t2 SEC { v y == v x })

inline_for_extraction
noextract
val hide
  (#t: inttype { unsigned t })
  (#sec: secrecy_level)
  (x: uint_t t sec)
: Tot (y: uint_t t SEC { v y == v x })

inline_for_extraction
noextract
val reveal
  (#t: inttype { unsigned t })
  (#sec: secrecy_level)
  (x: uint_t t sec)
: GTot (y: uint_t t PUB { v y == v x })

let hide_reveal
  (#t: inttype { unsigned t })
  (x: uint_t t SEC)
: Lemma
  (hide (reveal x) == x)
  [SMTPat (hide (reveal x))]
= ()

let reveal_hide
  (#t: inttype { unsigned t })
  (x: uint_t t PUB)
: Lemma
  (reveal (hide x) == x)
  [SMTPat (reveal (hide x))]
= ()

(* Patterns *)

let logand_spec'
  (#t:inttype)
  (#l:secrecy_level)
  (a:int_t t l)
  (b:int_t t l)
: Lemma (v (a `logand` b) == v a `logand_v` v b)
val logand_spec' (#t: inttype) (#l: secrecy_level) (a b: int_t t l)
    : Lemma (v (a `logand` b) == (v a) `logand_v` (v b)) [SMTPat (v (a `logand` b))]
a: Lib.IntTypes.int_t t l -> b: Lib.IntTypes.int_t t l
  -> FStar.Pervasives.Lemma
      (ensures
        QUIC.Secret.Int.Base.v (Lib.IntTypes.logand a b) ==
        Lib.IntTypes.logand_v (QUIC.Secret.Int.Base.v a) (QUIC.Secret.Int.Base.v b))
      [SMTPat (QUIC.Secret.Int.Base.v (Lib.IntTypes.logand a b))]