val logand_one_bit
      (#t: inttype{supported_type t})
      (#sec: secrecy_level)
      (x: int_t t sec {v x == 0 \/ v x == 1})
      (y: int_t t sec {v y == 0 \/ v y == 1})
    : Tot (z: int_t t sec {v z == (if v x = 1 && v y = 1 then 1 else 0)})
let logand_one_bit
  (#t: inttype { supported_type t })
  (#sec: secrecy_level)
  (x: int_t t sec { v x == 0 \/ v x == 1 })
  (y: int_t t sec { v y == 0 \/ v y == 1 })
: Tot (z: int_t t sec { v z == (if v x = 1 && v y = 1 then 1 else 0) })
= x `mul` y
val logand_one_bit
      (#t: inttype{supported_type t})
      (#sec: secrecy_level)
      (x: int_t t sec {v x == 0 \/ v x == 1})
      (y: int_t t sec {v y == 0 \/ v y == 1})
    : Tot (z: int_t t sec {v z == (if v x = 1 && v y = 1 then 1 else 0)})
let logand_one_bit
      (#t: inttype{supported_type t})
      (#sec: secrecy_level)
      (x: int_t t sec {v x == 0 \/ v x == 1})
      (y: int_t t sec {v y == 0 \/ v y == 1})
    : Tot (z: int_t t sec {v z == (if v x = 1 && v y = 1 then 1 else 0)}) =
x `mul` y
QUIC.Secret.Int.Aux.fst.checked
QUIC.Secret.Int.Base.fst.checked prims.fst.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.Aux.fst
Lib.IntTypes.inttype Prims.b2t QUIC.Secret.Int.Base.supported_type Lib.IntTypes.secrecy_level Lib.IntTypes.int_t Prims.l_or Prims.eq2 Prims.int QUIC.Secret.Int.Base.v Lib.IntTypes.mul Prims.op_AmpAmp Prims.op_Equality Prims.bool
module QUIC.Secret.Int.Aux
include QUIC.Secret.Int.Base

module U = FStar.UInt

module U8 = FStar.UInt8
module U16 = FStar.UInt16
module U32 = FStar.UInt32
module U64 = FStar.UInt64


noextract noeq type must_inline =

inline_for_extraction
noextract
[@"opaque_to_smt"]
let logand_one_bit
  (#t: inttype { supported_type t })
  (#sec: secrecy_level)
  (x: int_t t sec { v x == 0 \/ v x == 1 })
  (y: int_t t sec { v y == 0 \/ v y == 1 })
val logand_one_bit
      (#t: inttype{supported_type t})
      (#sec: secrecy_level)
      (x: int_t t sec {v x == 0 \/ v x == 1})
      (y: int_t t sec {v y == 0 \/ v y == 1})
    : Tot (z: int_t t sec {v z == (if v x = 1 && v y = 1 then 1 else 0)})

    x: Lib.IntTypes.int_t t sec {QUIC.Secret.Int.Base.v x == 0 \/ QUIC.Secret.Int.Base.v x == 1} ->
    y: Lib.IntTypes.int_t t sec {QUIC.Secret.Int.Base.v y == 0 \/ QUIC.Secret.Int.Base.v y == 1}
  -> z:
    Lib.IntTypes.int_t t sec
      { QUIC.Secret.Int.Base.v z ==
        (match QUIC.Secret.Int.Base.v x = 1 && QUIC.Secret.Int.Base.v y = 1 with
          | true -> 1
          | _ -> 0) }