val lognot_lemma: #t: inttype -> #l: secrecy_level ->
  a: int_t t l ->
  Lemma
    (requires v a = 0 \/ v a = ones_v t)
    (ensures (if v a = ones_v t then v (lognot a) == 0 else v (lognot a) == ones_v t))
let lognot_lemma #t #l a =
  match t with
  |U1 -> assert_norm(lognot (u1 0) == u1 1 /\ lognot (u1 1)  == u1 0)
  | U8 | U16 | U32 | U64 | U128 ->
    FStar.UInt.lognot_lemma_1 #(bits t);
    UInt.nth_lemma (FStar.UInt.lognot #(bits t) (UInt.ones (bits t))) (UInt.zero (bits t))
  | S8 | S16 | S32 | S64 | S128 ->
    Int.nth_lemma (FStar.Int.lognot #(bits t) (Int.zero (bits t))) (Int.ones (bits t));
    Int.nth_lemma (FStar.Int.lognot #(bits t) (Int.ones (bits t))) (Int.zero (bits t))
val lognot_lemma: #t: inttype -> #l: secrecy_level ->
  a: int_t t l ->
  Lemma
    (requires v a = 0 \/ v a = ones_v t)
    (ensures (if v a = ones_v t then v (lognot a) == 0 else v (lognot a) == ones_v t))
let lognot_lemma #t #l a =
match t with
| U1 -> assert_norm (lognot (u1 0) == u1 1 /\ lognot (u1 1) == u1 0)
| U8
| U16
| U32
| U64
| U128 ->
  FStar.UInt.lognot_lemma_1 #(bits t);
  UInt.nth_lemma (FStar.UInt.lognot #(bits t) (UInt.ones (bits t))) (UInt.zero (bits t))
| S8
| S16
| S32
| S64
| S128 ->
  Int.nth_lemma (FStar.Int.lognot #(bits t) (Int.zero (bits t))) (Int.ones (bits t));
  Int.nth_lemma (FStar.Int.lognot #(bits t) (Int.ones (bits t))) (Int.zero (bits t))
Lib.IntTypes.fst.checked
prims.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.UInt128.fsti.checked FStar.UInt.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Math.Lemmas.fst.checked FStar.Int8.fsti.checked FStar.Int64.fsti.checked FStar.Int32.fsti.checked FStar.Int16.fsti.checked FStar.Int128.fsti.checked FStar.Int.Cast.Full.fst.checked FStar.Int.Cast.fst.checked FStar.Int.fsti.checked FStar.BitVector.fst.checked
Lib.IntTypes.fst
Lib.IntTypes.inttype Lib.IntTypes.secrecy_level Lib.IntTypes.int_t FStar.Pervasives.assert_norm Prims.l_and Prims.eq2 Lib.IntTypes.U1 Lib.IntTypes.SEC Lib.IntTypes.lognot Lib.IntTypes.u1 FStar.UInt.nth_lemma Lib.IntTypes.bits FStar.UInt.lognot FStar.UInt.ones FStar.UInt.zero Prims.unit FStar.UInt.lognot_lemma_1 FStar.Int.nth_lemma FStar.Int.lognot FStar.Int.ones FStar.Int.zero
module Lib.IntTypes

open FStar.Math.Lemmas

#push-options "--max_fuel 0 --max_ifuel 1 --z3rlimit 200"

let pow2_2 _   = assert_norm (pow2 2 = 4)
let pow2_3 _   = assert_norm (pow2 3 = 8)
let pow2_4 _   = assert_norm (pow2 4 = 16)
let pow2_127 _ = assert_norm (pow2 127 = 0x80000000000000000000000000000000)

let bits_numbytes t = ()

let sec_int_t t = pub_int_t t

let sec_int_v #t u = pub_int_v u

let secret #t x = x

[@(strict_on_arguments [0])]
let mk_int #t #l x =
  match t with
  | U1 -> UInt8.uint_to_t x
  | U8 -> UInt8.uint_to_t x
  | U16 -> UInt16.uint_to_t x
  | U32 -> UInt32.uint_to_t x
  | U64 -> UInt64.uint_to_t x
  | U128 -> UInt128.uint_to_t x
  | S8 -> Int8.int_to_t x
  | S16 -> Int16.int_to_t x
  | S32 -> Int32.int_to_t x
  | S64 -> Int64.int_to_t x
  | S128 -> Int128.int_to_t x

val v_extensionality:
   #t:inttype
 -> #l:secrecy_level
 -> a:int_t t l
 -> b:int_t t l
 -> Lemma
  (requires v a == v b)
  (ensures  a == b)
let v_extensionality #t #l a b =
  match t with
  | U1   -> ()
  | U8   -> UInt8.v_inj a b
  | U16  -> UInt16.v_inj a b
  | U32  -> UInt32.v_inj a b
  | U64  -> UInt64.v_inj a b
  | U128 -> UInt128.v_inj a b
  | S8   -> Int8.v_inj a b
  | S16  -> Int16.v_inj a b
  | S32  -> Int32.v_inj a b
  | S64  -> Int64.v_inj a b
  | S128 -> Int128.v_inj a b

let v_injective #t #l a =
  v_extensionality a (mk_int (v a))

let v_mk_int #t #l n = ()

let u128 n = FStar.UInt128.uint64_to_uint128 (u64 n)

// KaRaMeL will extract this to FStar_Int128_int_to_t, which isn't provided
// We'll need to have FStar.Int128.int64_to_int128 to support int128_t literals
let i128 n =
  assert_norm (pow2 (bits S64 - 1) <= pow2 (bits S128 - 1));
  sint #S128 #SEC n

let size_to_uint32 x = x

let size_to_uint64 x = Int.Cast.uint32_to_uint64 x

let byte_to_uint8 x = x

let byte_to_int8 x = Int.Cast.uint8_to_int8 x

let op_At_Percent = Int.op_At_Percent

// FStar.UInt128 gets special treatment in KaRaMeL. There is no
// equivalent for FStar.Int128 at the moment, so we use the three
// assumed cast operators below.
//
// Using them will fail at runtime with an informative message.
// The commented-out implementations show that they are realizable.
//
// When support for `FStar.Int128` is added KaRaMeL, these casts must
// be added as special cases. When using builtin compiler support for
// `int128_t`, they can be implemented directly as C casts without
// undefined or implementation-defined behaviour.

assume
val uint128_to_int128: a:UInt128.t{v a <= maxint S128} -> b:Int128.t{Int128.v b == UInt128.v a}
//let uint128_to_int128 a = Int128.int_to_t (v a)

assume
val int128_to_uint128: a:Int128.t -> b:UInt128.t{UInt128.v b == Int128.v a % pow2 128}
//let int128_to_uint128 a = mk_int (v a % pow2 128)

assume
val int64_to_int128: a:Int64.t -> b:Int128.t{Int128.v b == Int64.v a}
//let int64_to_int128 a = Int128.int_to_t (v a)

val uint64_to_int128: a:UInt64.t -> b:Int128.t{Int128.v b == UInt64.v a}
let uint64_to_int128 a = uint128_to_int128 (Int.Cast.Full.uint64_to_uint128 a)

val int64_to_uint128: a:Int64.t -> b:UInt128.t{UInt128.v b == Int64.v a % pow2 128}
let int64_to_uint128 a = int128_to_uint128 (int64_to_int128 a)

val int128_to_uint64: a:Int128.t -> b:UInt64.t{UInt64.v b == Int128.v a % pow2 64}
let int128_to_uint64 a = Int.Cast.Full.uint128_to_uint64 (int128_to_uint128 a)

#push-options "--z3rlimit 1000"

[@(strict_on_arguments [0;2])]
let cast #t #l t' l' u =
  assert_norm (pow2 8 = 2 * pow2 7);
  assert_norm (pow2 16 = 2 * pow2 15);
  assert_norm (pow2 64 * pow2 64 = pow2 128);
  assert_norm (pow2 16 * pow2 48 = pow2 64);
  assert_norm (pow2 8 * pow2 56 = pow2 64);
  assert_norm (pow2 32 * pow2 32 = pow2 64);
  modulo_modulo_lemma (v u) (pow2 32) (pow2 32);
  modulo_modulo_lemma (v u) (pow2 64) (pow2 64);
  modulo_modulo_lemma (v u) (pow2 128) (pow2 64);
  modulo_modulo_lemma (v u) (pow2 16) (pow2 48);
  modulo_modulo_lemma (v u) (pow2 8) (pow2 56);
  let open FStar.Int.Cast in
  let open FStar.Int.Cast.Full in
  match t, t' with
  | U1, U1     -> u
  | U1, U8     -> u
  | U1, U16    -> uint8_to_uint16 u
  | U1, U32    -> uint8_to_uint32 u
  | U1, U64    -> uint8_to_uint64 u
  | U1, U128   -> UInt128.uint64_to_uint128 (uint8_to_uint64 u)
  | U1, S8     -> uint8_to_int8 u
  | U1, S16    -> uint8_to_int16 u
  | U1, S32    -> uint8_to_int32 u
  | U1, S64    -> uint8_to_int64 u
  | U1, S128   -> uint64_to_int128 (uint8_to_uint64 u)

  | U8, U1     -> UInt8.rem u 2uy
  | U8, U8     -> u
  | U8, U16    -> uint8_to_uint16 u
  | U8, U32    -> uint8_to_uint32 u
  | U8, U64    -> uint8_to_uint64 u
  | U8, U128   -> UInt128.uint64_to_uint128 (uint8_to_uint64 u)
  | U8, S8     -> uint8_to_int8 u
  | U8, S16    -> uint8_to_int16 u
  | U8, S32    -> uint8_to_int32 u
  | U8, S64    -> uint8_to_int64 u
  | U8, S128   -> uint64_to_int128 (uint8_to_uint64 u)

  | U16, U1    -> UInt8.rem (uint16_to_uint8 u) 2uy
  | U16, U8    -> uint16_to_uint8 u
  | U16, U16   -> u
  | U16, U32   -> uint16_to_uint32 u
  | U16, U64   -> uint16_to_uint64 u
  | U16, U128  -> UInt128.uint64_to_uint128 (uint16_to_uint64 u)
  | U16, S8    -> uint16_to_int8 u
  | U16, S16   -> uint16_to_int16 u
  | U16, S32   -> uint16_to_int32 u
  | U16, S64   -> uint16_to_int64 u
  | U16, S128  -> uint64_to_int128 (uint16_to_uint64 u)

  | U32, U1    -> UInt8.rem (uint32_to_uint8 u) 2uy
  | U32, U8    -> uint32_to_uint8 u
  | U32, U16   -> uint32_to_uint16 u
  | U32, U32   -> u
  | U32, U64   -> uint32_to_uint64 u
  | U32, U128  -> UInt128.uint64_to_uint128 (uint32_to_uint64 u)
  | U32, S8    -> uint32_to_int8 u
  | U32, S16   -> uint32_to_int16 u
  | U32, S32   -> uint32_to_int32 u
  | U32, S64   -> uint32_to_int64 u
  | U32, S128  -> uint64_to_int128 (uint32_to_uint64 u)

  | U64, U1    -> UInt8.rem (uint64_to_uint8 u) 2uy
  | U64, U8    -> uint64_to_uint8 u
  | U64, U16   -> uint64_to_uint16 u
  | U64, U32   -> uint64_to_uint32 u
  | U64, U64   -> u
  | U64, U128  -> UInt128.uint64_to_uint128 u
  | U64, S8    -> uint64_to_int8 u
  | U64, S16   -> uint64_to_int16 u
  | U64, S32   -> uint64_to_int32 u
  | U64, S64   -> uint64_to_int64 u
  | U64, S128  -> uint64_to_int128 u

  | U128, U1   -> UInt8.rem (uint64_to_uint8 (uint128_to_uint64 u)) 2uy
  | U128, U8   -> uint64_to_uint8 (UInt128.uint128_to_uint64 u)
  | U128, U16  -> uint64_to_uint16 (UInt128.uint128_to_uint64 u)
  | U128, U32  -> uint64_to_uint32 (UInt128.uint128_to_uint64 u)
  | U128, U64  -> UInt128.uint128_to_uint64 u
  | U128, U128 -> u
  | U128, S8   -> uint64_to_int8 (UInt128.uint128_to_uint64 u)
  | U128, S16  -> uint64_to_int16 (UInt128.uint128_to_uint64 u)
  | U128, S32  -> uint64_to_int32 (UInt128.uint128_to_uint64 u)
  | U128, S64  -> uint64_to_int64 (UInt128.uint128_to_uint64 u)
  | U128, S128 -> uint128_to_int128 u

  | S8, U1     -> UInt8.rem (int8_to_uint8 u) 2uy
  | S8, U8     -> int8_to_uint8 u
  | S8, U16    -> int8_to_uint16 u
  | S8, U32    -> int8_to_uint32 u
  | S8, U64    -> int8_to_uint64 u
  | S8, U128   -> int64_to_uint128 (int8_to_int64 u)
  | S8, S8     -> u
  | S8, S16    -> int8_to_int16 u
  | S8, S32    -> int8_to_int32 u
  | S8, S64    -> int8_to_int64 u
  | S8, S128   -> int64_to_int128 (int8_to_int64 u)

  | S16, U1    -> UInt8.rem (int16_to_uint8 u) 2uy
  | S16, U8    -> int16_to_uint8 u
  | S16, U16   -> int16_to_uint16 u
  | S16, U32   -> int16_to_uint32 u
  | S16, U64   -> int16_to_uint64 u
  | S16, U128  -> int64_to_uint128 (int16_to_int64 u)
  | S16, S8    -> int16_to_int8 u
  | S16, S16   -> u
  | S16, S32   -> int16_to_int32 u
  | S16, S64   -> int16_to_int64 u
  | S16, S128  -> int64_to_int128 (int16_to_int64 u)

  | S32, U1    -> UInt8.rem (int32_to_uint8 u) 2uy
  | S32, U8    -> int32_to_uint8 u
  | S32, U16   -> int32_to_uint16 u
  | S32, U32   -> int32_to_uint32 u
  | S32, U64   -> int32_to_uint64 u
  | S32, U128  -> int64_to_uint128 (int32_to_int64 u)
  | S32, S8    -> int32_to_int8 u
  | S32, S16   -> int32_to_int16 u
  | S32, S32   -> u
  | S32, S64   -> int32_to_int64 u
  | S32, S128  -> int64_to_int128 (int32_to_int64 u)

  | S64, U1    -> UInt8.rem (int64_to_uint8 u) 2uy
  | S64, U8    -> int64_to_uint8 u
  | S64, U16   -> int64_to_uint16 u
  | S64, U32   -> int64_to_uint32 u
  | S64, U64   -> int64_to_uint64 u
  | S64, U128  -> int64_to_uint128 u
  | S64, S8    -> int64_to_int8 u
  | S64, S16   -> int64_to_int16 u
  | S64, S32   -> int64_to_int32 u
  | S64, S64   -> u
  | S64, S128  -> int64_to_int128 u

  | S128, U1    -> UInt8.rem (uint64_to_uint8 (int128_to_uint64 u)) 2uy
  | S128, U8    -> uint64_to_uint8 (int128_to_uint64 u)
  | S128, U16   -> uint64_to_uint16 (int128_to_uint64 u)
  | S128, U32   -> uint64_to_uint32 (int128_to_uint64 u)
  | S128, U64   -> int128_to_uint64 u
  | S128, U128  -> int128_to_uint128 u
  | S128, S8    -> uint64_to_int8  (int128_to_uint64 u)
  | S128, S16   -> uint64_to_int16 (int128_to_uint64 u)
  | S128, S32   -> uint64_to_int32 (int128_to_uint64 u)
  | S128, S64   -> uint64_to_int64 (int128_to_uint64 u)
  | S128, S128  -> u

#pop-options

[@(strict_on_arguments [0])]
let ones t l =
  match t with
  | U1  -> 0x1uy
  | U8  -> 0xFFuy
  | U16 -> 0xFFFFus
  | U32 -> 0xFFFFFFFFul
  | U64 -> 0xFFFFFFFFFFFFFFFFuL
  | U128 ->
    let x = UInt128.uint64_to_uint128 0xFFFFFFFFFFFFFFFFuL in
    let y = (UInt128.shift_left x 64ul) `UInt128.add` x in
    assert_norm (UInt128.v y == pow2 128 - 1);
    y
  | _ -> mk_int (-1)

let zeros t l = mk_int 0

[@(strict_on_arguments [0])]
let add_mod #t #l a b =
  match t with
  | U1   -> UInt8.rem (UInt8.add_mod a b) 2uy
  | U8   -> UInt8.add_mod a b
  | U16  -> UInt16.add_mod a b
  | U32  -> UInt32.add_mod a b
  | U64  -> UInt64.add_mod a b
  | U128 -> UInt128.add_mod a b

let add_mod_lemma #t #l a b = ()

[@(strict_on_arguments [0])]
let add #t #l a b =
  match t with
  | U1   -> UInt8.add a b
  | U8   -> UInt8.add a b
  | U16  -> UInt16.add a b
  | U32  -> UInt32.add a b
  | U64  -> UInt64.add a b
  | U128 -> UInt128.add a b
  | S8   -> Int8.add a b
  | S16  -> Int16.add a b
  | S32  -> Int32.add a b
  | S64  -> Int64.add a b
  | S128 -> Int128.add a b

let add_lemma #t #l a b = ()

#push-options "--max_fuel 1"

[@(strict_on_arguments [0])]
let incr #t #l a =
  match t with
  | U1   -> UInt8.add a 1uy
  | U8   -> UInt8.add a 1uy
  | U16  -> UInt16.add a 1us
  | U32  -> UInt32.add a 1ul
  | U64  -> UInt64.add a 1uL
  | U128 -> UInt128.add a (UInt128.uint_to_t 1)
  | S8   -> Int8.add a 1y
  | S16  -> Int16.add a 1s
  | S32  -> Int32.add a 1l
  | S64  -> Int64.add a 1L
  | S128 -> Int128.add a (Int128.int_to_t 1)

let incr_lemma #t #l a = ()

#pop-options

[@(strict_on_arguments [0])]
let mul_mod #t #l a b =
  match t with
  | U1  -> UInt8.mul_mod a b
  | U8  -> UInt8.mul_mod a b
  | U16 -> UInt16.mul_mod a b
  | U32 -> UInt32.mul_mod a b
  | U64 -> UInt64.mul_mod a b

let mul_mod_lemma #t #l a b = ()

[@(strict_on_arguments [0])]
let mul #t #l a b =
  match t with
  | U1  -> UInt8.mul a b
  | U8  -> UInt8.mul a b
  | U16 -> UInt16.mul a b
  | U32 -> UInt32.mul a b
  | U64 -> UInt64.mul a b
  | S8  -> Int8.mul a b
  | S16 -> Int16.mul a b
  | S32 -> Int32.mul a b
  | S64 -> Int64.mul a b

let mul_lemma #t #l a b = ()

let mul64_wide a b = UInt128.mul_wide a b

let mul64_wide_lemma a b = ()

let mul_s64_wide a b = Int128.mul_wide a b

let mul_s64_wide_lemma a b = ()

[@(strict_on_arguments [0])]
let sub_mod #t #l a b =
  match t with
  | U1   -> UInt8.rem (UInt8.sub_mod a b) 2uy
  | U8   -> UInt8.sub_mod a b
  | U16  -> UInt16.sub_mod a b
  | U32  -> UInt32.sub_mod a b
  | U64  -> UInt64.sub_mod a b
  | U128 -> UInt128.sub_mod a b

let sub_mod_lemma #t #l a b = ()

[@(strict_on_arguments [0])]
let sub #t #l a b =
  match t with
  | U1   -> UInt8.sub a b
  | U8   -> UInt8.sub a b
  | U16  -> UInt16.sub a b
  | U32  -> UInt32.sub a b
  | U64  -> UInt64.sub a b
  | U128 -> UInt128.sub a b
  | S8   -> Int8.sub a b
  | S16  -> Int16.sub a b
  | S32  -> Int32.sub a b
  | S64  -> Int64.sub a b
  | S128 -> Int128.sub a b

let sub_lemma #t #l a b = ()

#push-options "--max_fuel 1"

[@(strict_on_arguments [0])]
let decr #t #l a =
  match t with
  | U1   -> UInt8.sub a 1uy
  | U8   -> UInt8.sub a 1uy
  | U16  -> UInt16.sub a 1us
  | U32  -> UInt32.sub a 1ul
  | U64  -> UInt64.sub a 1uL
  | U128 -> UInt128.sub a (UInt128.uint_to_t 1)
  | S8   -> Int8.sub a 1y
  | S16  -> Int16.sub a 1s
  | S32  -> Int32.sub a 1l
  | S64  -> Int64.sub a 1L
  | S128 -> Int128.sub a (Int128.int_to_t 1)

let decr_lemma #t #l a = ()

#pop-options

[@(strict_on_arguments [0])]
let logxor #t #l a b =
  match t with
  | U1   ->
    assert_norm (UInt8.logxor 0uy 0uy == 0uy);
    assert_norm (UInt8.logxor 0uy 1uy == 1uy);
    assert_norm (UInt8.logxor 1uy 0uy == 1uy);
    assert_norm (UInt8.logxor 1uy 1uy == 0uy);
    UInt8.logxor a b
  | U8   -> UInt8.logxor a b
  | U16  -> UInt16.logxor a b
  | U32  -> UInt32.logxor a b
  | U64  -> UInt64.logxor a b
  | U128 -> UInt128.logxor a b
  | S8   -> Int8.logxor a b
  | S16  -> Int16.logxor a b
  | S32  -> Int32.logxor a b
  | S64  -> Int64.logxor a b
  | S128 -> Int128.logxor a b

#push-options "--max_fuel 1"

val logxor_lemma_: #t:inttype -> #l:secrecy_level -> a:int_t t l -> b:int_t t l -> Lemma
  (v (a `logxor` (a `logxor` b)) == v b)
let logxor_lemma_ #t #l a b =
  match t with
  | U1 | U8 | U16 | U32 | U64 | U128 ->
    UInt.logxor_associative #(bits t) (v a) (v a) (v b);
    UInt.logxor_self #(bits t) (v a);
    UInt.logxor_commutative #(bits t) 0 (v b);
    UInt.logxor_lemma_1 #(bits t) (v b)
  | S8 | S16 | S32 | S64 | S128 ->
    Int.logxor_associative #(bits t) (v a) (v a) (v b);
    Int.logxor_self #(bits t) (v a);
    Int.logxor_commutative #(bits t) 0 (v b);
    Int.logxor_lemma_1 #(bits t) (v b)

let logxor_lemma #t #l a b =
  logxor_lemma_ #t a b;
  v_extensionality (logxor a (logxor a b)) b;
  begin
  match t with
  | U1 | U8 | U16 | U32 | U64 | U128 -> UInt.logxor_commutative #(bits t) (v a) (v b)
  | S8 | S16 | S32 | S64 | S128      -> Int.logxor_commutative #(bits t) (v a) (v b)
  end;
  v_extensionality (logxor a (logxor b a)) b;
  begin
  match t with
  | U1 | U8 | U16 | U32 | U64 | U128 -> UInt.logxor_lemma_1 #(bits t) (v a)
  | S8 | S16 | S32 | S64 | S128      -> Int.logxor_lemma_1 #(bits t) (v a)
  end;
  v_extensionality (logxor a (mk_int #t #l 0)) a

let logxor_lemma1 #t #l a b =
  match v a, v b with
  | _, 0 ->
    UInt.logxor_lemma_1 #(bits t) (v a)
  | 0, _ ->
    UInt.logxor_commutative #(bits t) (v a) (v b);
    UInt.logxor_lemma_1 #(bits t) (v b)
  | 1, 1 ->
    v_extensionality a b;
    UInt.logxor_self #(bits t) (v a)

let logxor_spec #t #l a b =
  match t with
  | U1 ->
    assert_norm (u1 0 `logxor` u1 0 == u1 0 /\ u1 0 `logxor` u1 1 == u1 1);
    assert_norm (u1 1 `logxor` u1 0 == u1 1 /\ u1 1 `logxor` u1 1 == u1 0);
    assert_norm (0 `logxor_v #U1` 0 == 0 /\ 0 `logxor_v #U1` 1 == 1);
    assert_norm (1 `logxor_v #U1` 0 == 1 /\ 1 `logxor_v #U1` 1 == 0)
  | _ -> ()

#pop-options

[@(strict_on_arguments [0])]
let logand #t #l a b =
  match t with
  | U1   ->
    assert_norm (UInt8.logand 0uy 0uy == 0uy);
    assert_norm (UInt8.logand 0uy 1uy == 0uy);
    assert_norm (UInt8.logand 1uy 0uy == 0uy);
    assert_norm (UInt8.logand 1uy 1uy == 1uy);
    UInt8.logand a b
  | U8   -> UInt8.logand a b
  | U16  -> UInt16.logand a b
  | U32  -> UInt32.logand a b
  | U64  -> UInt64.logand a b
  | U128 -> UInt128.logand a b
  | S8   -> Int8.logand a b
  | S16  -> Int16.logand a b
  | S32  -> Int32.logand a b
  | S64  -> Int64.logand a b
  | S128 -> Int128.logand a b

let logand_zeros #t #l a =
  match t with
  | U1 -> assert_norm (u1 0 `logand` zeros U1 l == u1 0 /\ u1 1 `logand` zeros U1 l == u1 0)
  | U8 | U16 | U32 | U64 | U128 -> UInt.logand_lemma_1 #(bits t) (v a)
  | S8 | S16 | S32 | S64 | S128 -> Int.logand_lemma_1 #(bits t) (v a)

let logand_ones #t #l a =
  match t with
  | U1 -> assert_norm (u1 0 `logand` ones U1 l == u1 0 /\ u1 1 `logand` ones U1 l == u1 1)
  | U8 | U16 | U32 | U64 | U128 -> UInt.logand_lemma_2 #(bits t) (v a)
  | S8 | S16 | S32 | S64 | S128 -> Int.logand_lemma_2 #(bits t) (v a)

let logand_lemma #t #l a b =
  logand_zeros #t #l b;
  logand_ones #t #l b;
  match t with
  | U1 ->
    assert_norm (u1 0 `logand` zeros U1 l == u1 0 /\ u1 1 `logand` zeros U1 l == u1 0);
    assert_norm (u1 0 `logand` ones U1 l == u1 0 /\ u1 1 `logand` ones U1 l == u1 1)
  | U8 | U16 | U32 | U64 | U128 -> UInt.logand_commutative #(bits t) (v a) (v b)
  | S8 | S16 | S32 | S64 | S128 -> Int.logand_commutative #(bits t) (v a) (v b)

let logand_spec #t #l a b =
  match t with
  | U1 ->
    assert_norm (u1 0 `logand` u1 0 == u1 0 /\ u1 0 `logand` u1 1 == u1 0);
    assert_norm (u1 1 `logand` u1 0 == u1 0 /\ u1 1 `logand` u1 1 == u1 1);
    assert_norm (0 `logand_v #U1` 0 == 0 /\ 0 `logand_v #U1` 1 == 0);
    assert_norm (1 `logand_v #U1` 0 == 0 /\ 1 `logand_v #U1` 1 == 1)
  | _ -> ()

let logand_le #t #l a b =
  match t with
  | U1 ->
    assert_norm (UInt8.logand 0uy 0uy == 0uy);
    assert_norm (UInt8.logand 0uy 1uy == 0uy);
    assert_norm (UInt8.logand 1uy 0uy == 0uy);
    assert_norm (UInt8.logand 1uy 1uy == 1uy)
  | U8 -> UInt.logand_le (UInt.to_uint_t 8 (v a)) (UInt.to_uint_t 8 (v b))
  | U16 -> UInt.logand_le (UInt.to_uint_t 16 (v a)) (UInt.to_uint_t 16 (v b))
  | U32 -> UInt.logand_le (UInt.to_uint_t 32 (v a)) (UInt.to_uint_t 32 (v b))
  | U64 -> UInt.logand_le (UInt.to_uint_t 64 (v a)) (UInt.to_uint_t 64 (v b))
  | U128 -> UInt.logand_le (UInt.to_uint_t 128 (v a)) (UInt.to_uint_t 128 (v b))

let logand_mask #t #l a b m =
  match t with
  | U1 ->
    assert_norm (UInt8.logand 0uy 0uy == 0uy);
    assert_norm (UInt8.logand 0uy 1uy == 0uy);
    assert_norm (UInt8.logand 1uy 0uy == 0uy);
    assert_norm (UInt8.logand 1uy 1uy == 1uy)
  | U8 -> UInt.logand_mask (UInt.to_uint_t 8 (v a)) m
  | U16 -> UInt.logand_mask (UInt.to_uint_t 16 (v a)) m
  | U32 -> UInt.logand_mask (UInt.to_uint_t 32 (v a)) m
  | U64 -> UInt.logand_mask (UInt.to_uint_t 64 (v a)) m
  | U128 -> UInt.logand_mask (UInt.to_uint_t 128 (v a)) m


[@(strict_on_arguments [0])]
let logor #t #l a b =
  match t with
  | U1   ->
    assert_norm (UInt8.logor 0uy 0uy == 0uy);
    assert_norm (UInt8.logor 0uy 1uy == 1uy);
    assert_norm (UInt8.logor 1uy 0uy == 1uy);
    assert_norm (UInt8.logor 1uy 1uy == 1uy);
    UInt8.logor a b
  | U8   -> UInt8.logor a b
  | U16  -> UInt16.logor a b
  | U32  -> UInt32.logor a b
  | U64  -> UInt64.logor a b
  | U128 -> UInt128.logor a b
  | S8   -> Int8.logor a b
  | S16  -> Int16.logor a b
  | S32  -> Int32.logor a b
  | S64  -> Int64.logor a b
  | S128 -> Int128.logor a b

#push-options "--max_fuel 1"

let logor_disjoint #t #l a b m =
  if m > 0 then
  begin
    UInt.logor_disjoint #(bits t) (v b) (v a) m;
    UInt.logor_commutative #(bits t) (v b) (v a)
  end
  else
  begin
    UInt.logor_commutative #(bits t) (v a) (v b);
    UInt.logor_lemma_1 #(bits t) (v b)
  end

#pop-options

let logor_zeros #t #l a =
  match t with
  |U1 -> assert_norm(u1 0 `logor` zeros U1 l == u1 0 /\ u1 1 `logor` zeros U1 l == u1 1)
  | U8 | U16 | U32 | U64 | U128 -> UInt.logor_lemma_1 #(bits t) (v a)
  | S8 | S16 | S32 | S64 | S128 -> Int.nth_lemma #(bits t) (Int.logor #(bits t) (v a) (Int.zero (bits t))) (v a)


let logor_ones #t #l a =
  match t with
  |U1 -> assert_norm(u1 0 `logor` ones U1 l == u1 1 /\ u1 1 `logor` ones U1 l == u1 1)
  | U8 | U16 | U32 | U64 | U128 -> UInt.logor_lemma_2 #(bits t) (v a)
  | S8 | S16 | S32 | S64 | S128 -> Int.nth_lemma (Int.logor #(bits t) (v a) (Int.ones (bits t))) (Int.ones (bits t))

let logor_lemma #t #l a b =
  logor_zeros #t #l b;
  logor_ones #t #l b;
  match t with
  | U1 ->
    assert_norm(u1 0 `logor` ones U1 l == u1 1 /\ u1 1 `logor` ones U1 l == u1 1);
    assert_norm(u1 0 `logor` zeros U1 l == u1 0 /\ u1 1 `logor` zeros U1 l == u1 1)
  | U8 | U16 | U32 | U64 | U128 -> UInt.logor_commutative #(bits t) (v a) (v b)
  | S8 | S16 | S32 | S64 | S128 -> Int.nth_lemma #(bits t) (Int.logor #(bits t) (v a) (v b)) (Int.logor #(bits t) (v b) (v a))

let logor_spec #t #l a b =
  match t with
  | U1 ->
    assert_norm(u1 0 `logor` ones U1 l == u1 1 /\ u1 1 `logor` ones U1 l == u1 1);
    assert_norm(u1 0 `logor` zeros U1 l == u1 0 /\ u1 1 `logor` zeros U1 l == u1 1);
    assert_norm (0 `logor_v #U1` 0 == 0 /\ 0 `logor_v #U1` 1 == 1);
    assert_norm (1 `logor_v #U1` 0 == 1 /\ 1 `logor_v #U1` 1 == 1)
  | _ -> ()


[@(strict_on_arguments [0])]
let lognot #t #l a =
  match t with
  | U1   -> UInt8.rem (UInt8.lognot a) 2uy
  | U8   -> UInt8.lognot a
  | U16  -> UInt16.lognot a
  | U32  -> UInt32.lognot a
  | U64  -> UInt64.lognot a
  | U128 -> UInt128.lognot a
  | S8   -> Int8.lognot a
  | S16  -> Int16.lognot a
  | S32  -> Int32.lognot a
  | S64  -> Int64.lognot a
  | S128 -> Int128.lognot a
val lognot_lemma: #t: inttype -> #l: secrecy_level ->
  a: int_t t l ->
  Lemma
    (requires v a = 0 \/ v a = ones_v t)
    (ensures (if v a = ones_v t then v (lognot a) == 0 else v (lognot a) == ones_v t))
a: Lib.IntTypes.int_t t l
  -> FStar.Pervasives.Lemma
      (requires Lib.IntTypes.v a = 0 \/ Lib.IntTypes.v a = Lib.IntTypes.ones_v t)
      (ensures
        ((match Lib.IntTypes.v a = Lib.IntTypes.ones_v t with
            | true -> Lib.IntTypes.v (Lib.IntTypes.lognot a) == 0
            | _ -> Lib.IntTypes.v (Lib.IntTypes.lognot a) == Lib.IntTypes.ones_v t)
          <:
          Type0))