val secret_bool
  (#t: inttype { supported_type t })
  (#sec: secrecy_level)
  (x: bool)
: Tot (z: int_t t sec { v z == (if x then 1 else 0) })
let secret_bool = Aux.secret_bool
val secret_bool
  (#t: inttype { supported_type t })
  (#sec: secrecy_level)
  (x: bool)
: Tot (z: int_t t sec { v z == (if x then 1 else 0) })
let secret_bool =
Aux.secret_bool
QUIC.Secret.Int.fst.checked
QUIC.Secret.Int.Aux.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked
QUIC.Secret.Int.fst
QUIC.Secret.Int.Aux.secret_bool
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
val secret_bool
  (#t: inttype { supported_type t })
  (#sec: secrecy_level)
  (x: bool)
: Tot (z: int_t t sec { v z == (if x then 1 else 0) })
x: Prims.bool
  -> z:
    Lib.IntTypes.int_t t sec
      { QUIC.Secret.Int.Base.v z ==
        (match x with
          | true -> 1
          | _ -> 0) }