val logxor_one_bit_32
      (sec: secrecy_level)
      (x: int_t U32 sec {v x == 0 \/ v x == 1})
      (y: int_t U32 sec {v y == 0 \/ v y == 1})
    : Lemma (v (x `logxor` y) == (if v x = v y then 0 else 1))
val logxor_one_bit_32
      (sec: secrecy_level)
      (x: int_t U32 sec {v x == 0 \/ v x == 1})
      (y: int_t U32 sec {v y == 0 \/ v y == 1})
    : Lemma (v (x `logxor` y) == (if v x = v y then 0 else 1))
let logxor_one_bit_32
  (sec: secrecy_level)
  (x: int_t U32 sec { v x == 0 \/ v x == 1 })
  (y: int_t U32 sec { v y == 0 \/ v y == 1 })
: Lemma
  (v (x `logxor` y) == (if v x = v y then 0 else 1))
= logxor_spec x y;
  allow_inversion secrecy_level;
  assert (U32.logxor 0ul 0ul == 0ul);
  assert (U32.logxor 0ul 1ul == 1ul);
  assert (U32.logxor 1ul 0ul == 1ul);
  assert (U32.logxor 1ul 1ul == 0ul)
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
  (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)

let logor_one_bit_16
  (sec: secrecy_level)
  (x: int_t U16 sec { v x == 0 \/ v x == 1 })
  (y: int_t U16 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 (U16.logor 0us 0us == 0us);
  assert (U16.logor 0us 1us == 1us);
  assert (U16.logor 1us 0us == 1us);
  assert (U16.logor 1us 1us == 1us)

let logor_one_bit_32
  (sec: secrecy_level)
  (x: int_t U32 sec { v x == 0 \/ v x == 1 })
  (y: int_t U32 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 (U32.logor 0ul 0ul == 0ul);
  assert (U32.logor 0ul 1ul == 1ul);
  assert (U32.logor 1ul 0ul == 1ul);
  assert (U32.logor 1ul 1ul == 1ul)

let logor_one_bit_64
  (sec: secrecy_level)
  (x: int_t U64 sec { v x == 0 \/ v x == 1 })
  (y: int_t U64 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 (U64.logor 0uL 0uL == 0uL);
  assert (U64.logor 0uL 1uL == 1uL);
  assert (U64.logor 1uL 0uL == 1uL);
  assert (U64.logor 1uL 1uL == 1uL)

let logor_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 })
: Lemma
  (v (x `logor` y) == (if v x = 1 || v y = 1 then 1 else 0))
= match t with
  | U8 -> logor_one_bit_8 sec x y
  | U16 -> logor_one_bit_16 sec x y
  | U32 -> logor_one_bit_32 sec x y
  | U64 -> logor_one_bit_64 sec x y

inline_for_extraction
[@"opaque_to_smt"]
noextract
let logor_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) })
= logor_one_bit' x y;
  x `logor` y



let logxor_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 `logxor` y) == (if v x = v y then 0 else 1))
= logxor_spec x y;
  allow_inversion secrecy_level;
  assert (U8.logxor 0uy 0uy == 0uy);
  assert (U8.logxor 0uy 1uy == 1uy);
  assert (U8.logxor 1uy 0uy == 1uy);
  assert (U8.logxor 1uy 1uy == 0uy)

let logxor_one_bit_16
  (sec: secrecy_level)
  (x: int_t U16 sec { v x == 0 \/ v x == 1 })
  (y: int_t U16 sec { v y == 0 \/ v y == 1 })
: Lemma
  (v (x `logxor` y) == (if v x = v y then 0 else 1))
= logxor_spec x y;
  allow_inversion secrecy_level;
  assert (U16.logxor 0us 0us == 0us);
  assert (U16.logxor 0us 1us == 1us);
  assert (U16.logxor 1us 0us == 1us);
  assert (U16.logxor 1us 1us == 0us)
/
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

    sec: Lib.IntTypes.secrecy_level ->
    x:
      Lib.IntTypes.int_t Lib.IntTypes.U32 sec
        {QUIC.Secret.Int.Base.v x == 0 \/ QUIC.Secret.Int.Base.v x == 1} ->
    y:
      Lib.IntTypes.int_t Lib.IntTypes.U32 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.logxor x y) ==
      (match QUIC.Secret.Int.Base.v x = QUIC.Secret.Int.Base.v y with
        | true -> 0
        | _ -> 1))
Lib.IntTypes.secrecy_level Lib.IntTypes.int_t Lib.IntTypes.U32 Prims.l_or Prims.eq2 Prims.int QUIC.Secret.Int.Base.v Prims._assert FStar.UInt32.t FStar.UInt32.logxor FStar.UInt32.__uint_to_t Prims.unit FStar.Pervasives.allow_inversion Lib.IntTypes.logxor_spec Prims.l_True Prims.squash Lib.IntTypes.logxor Prims.op_Equality Lib.IntTypes.range_t Prims.bool Prims.Nil FStar.Pervasives.pattern
let logxor_one_bit_32
      (sec: secrecy_level)
      (x: int_t U32 sec {v x == 0 \/ v x == 1})
      (y: int_t U32 sec {v y == 0 \/ v y == 1})
    : Lemma (v (x `logxor` y) == (if v x = v y then 0 else 1)) =
  
logxor_spec x y;
allow_inversion secrecy_level;
assert (U32.logxor 0ul 0ul == 0ul);
assert (U32.logxor 0ul 1ul == 1ul);
assert (U32.logxor 1ul 0ul == 1ul);
assert (U32.logxor 1ul 1ul == 0ul)