val logor_one_bit_8
      (sec: secrecy_level)
      (x: int_t U8 sec {v x == 0 \/ v x == 1})
      (y: int_t U8 sec {v y == 0 \/ v y == 1})
    : Lemma (v (x `logor` y) == (if v x = 1 || v y = 1 then 1 else 0))
let logor_one_bit_8
  (sec: secrecy_level)
  (x: int_t U8 sec { v x == 0 \/ v x == 1 })
  (y: int_t U8 sec { v y == 0 \/ v y == 1 })
: Lemma
  (v (x `logor` y) == (if v x = 1 || v y = 1 then 1 else 0))
= logor_spec x y;
  allow_inversion secrecy_level;
  assert (U8.logor 0uy 0uy == 0uy);
  assert (U8.logor 0uy 1uy == 1uy);
  assert (U8.logor 1uy 0uy == 1uy);
  assert (U8.logor 1uy 1uy == 1uy)
val logor_one_bit_8
      (sec: secrecy_level)
      (x: int_t U8 sec {v x == 0 \/ v x == 1})
      (y: int_t U8 sec {v y == 0 \/ v y == 1})
    : Lemma (v (x `logor` y) == (if v x = 1 || v y = 1 then 1 else 0))
let logor_one_bit_8
      (sec: secrecy_level)
      (x: int_t U8 sec {v x == 0 \/ v x == 1})
      (y: int_t U8 sec {v y == 0 \/ v y == 1})
    : Lemma (v (x `logor` y) == (if v x = 1 || v y = 1 then 1 else 0)) =
logor_spec x y;
allow_inversion secrecy_level;
assert (U8.logor 0uy 0uy == 0uy);
assert (U8.logor 0uy 1uy == 1uy);
assert (U8.logor 1uy 0uy == 1uy);
assert (U8.logor 1uy 1uy == 1uy)
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.secrecy_level Lib.IntTypes.int_t Lib.IntTypes.U8 Prims.l_or Prims.eq2 Prims.int QUIC.Secret.Int.Base.v Prims._assert FStar.UInt8.t FStar.UInt8.logor FStar.UInt8.__uint_to_t Prims.unit FStar.Pervasives.allow_inversion Lib.IntTypes.logor_spec Prims.l_True Prims.squash Lib.IntTypes.logor Prims.op_BarBar Prims.op_Equality Prims.bool Prims.Nil FStar.Pervasives.pattern
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 })
: Tot (z: int_t t sec { v z == (if v x = 1 && v y = 1 then 1 else 0) })
= x `mul` y

let logor_one_bit_8
  (sec: secrecy_level)
  (x: int_t U8 sec { v x == 0 \/ v x == 1 })
  (y: int_t U8 sec { v y == 0 \/ v y == 1 })
: Lemma
val logor_one_bit_8
      (sec: secrecy_level)
      (x: int_t U8 sec {v x == 0 \/ v x == 1})
      (y: int_t U8 sec {v y == 0 \/ v y == 1})
    : Lemma (v (x `logor` y) == (if v x = 1 || v y = 1 then 1 else 0))

    sec: Lib.IntTypes.secrecy_level ->
    x:
      Lib.IntTypes.int_t Lib.IntTypes.U8 sec
        {QUIC.Secret.Int.Base.v x == 0 \/ QUIC.Secret.Int.Base.v x == 1} ->
    y:
      Lib.IntTypes.int_t Lib.IntTypes.U8 sec
        {QUIC.Secret.Int.Base.v y == 0 \/ QUIC.Secret.Int.Base.v y == 1}
  -> FStar.Pervasives.Lemma
    (ensures
      QUIC.Secret.Int.Base.v (Lib.IntTypes.logor x y) ==
      (match QUIC.Secret.Int.Base.v x = 1 || QUIC.Secret.Int.Base.v y = 1 with
        | true -> 1
        | _ -> 0))