val lognot'
  (#t:inttype { supported_type t })
  (#l:secrecy_level)
  (x: uint_t t l)
: Tot (y: uint_t t l { v y == U.lognot #(bits 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
val lognot'
  (#t:inttype { supported_type t })
  (#l:secrecy_level)
  (x: uint_t t l)
: Tot (y: uint_t t l { v y == U.lognot #(bits 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)
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 Lib.IntTypes.logxor Lib.IntTypes.ones Prims.unit FStar.UInt.nth_lemma Lib.IntTypes.bits FStar.UInt.lognot QUIC.Secret.Int.Base.v FStar.UInt.logxor Prims.eq2 Prims.int Prims.l_or Lib.IntTypes.range FStar.UInt.size
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'
val lognot'
  (#t:inttype { supported_type t })
  (#l:secrecy_level)
  (x: uint_t t l)
: Tot (y: uint_t t l { v y == U.lognot #(bits t) (v x) })
x: Lib.IntTypes.uint_t t l
  -> y:
    Lib.IntTypes.uint_t t l
      {QUIC.Secret.Int.Base.v y == FStar.UInt.lognot (QUIC.Secret.Int.Base.v x)}