val logxor_uint_eq_zero_lem :#t:inttype{unsigned t} -> #l:secrecy_level -> a:uint_t t l -> b:uint_t t l ->
  Lemma (logxor a b == zeros t l <==> a == b)
val logxor_uint_eq_zero_lem :#t:inttype{unsigned t} -> #l:secrecy_level -> a:uint_t t l -> b:uint_t t l ->
  Lemma (logxor a b == zeros t l <==> a == b)
let logxor_uint_eq_zero_lem #t #l a b =
  assert(v (zeros t l) = 0);
  UInt.logxor_neq_nonzero #(bits t) (v a) (v b);
  assert(
    Lib.IntTypes.v a <> Lib.IntTypes.v b ==>
    UInt.logxor #(bits t) (Lib.IntTypes.v a) (Lib.IntTypes.v b) <> 0);
  logxor_spec a b;
  assert(v a <> v b ==> v (logxor a b) <> 0);
  assert((~(a == b)) ==> v (logxor a b) <> 0);
  UInt.logxor_self #(bits t) (v a);
  logxor_spec a a
module Impl.Noise.BufferEquality

open FStar.Mul
open FStar.HyperStack
open FStar.HyperStack.ST

open Lib.RawIntTypes
open Lib.IntTypes

open Lib.Sequence
module S = Lib.Sequence
module L = FStar.List
module Seq = FStar.Seq

open Lib.Buffer
open LowStar.BufferOps

module B = LowStar.Buffer
module BS = Lib.ByteSequence
module HS = FStar.HyperStack
module ST = FStar.HyperStack.ST
module G = FStar.Ghost

#set-options "--z3rlimit 50 --fuel 0 --ifuel 1"

(*** Buffer equality *)
// TODO: move?
val logxor_uint_eq_zero_lem :#t:inttype{unsigned t} -> #l:secrecy_level -> a:uint_t t l -> b:uint_t t l ->
  Lemma (logxor a b == zeros t l <==> a == b)
/
prims.fst.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked Lib.Sequence.fsti.checked Lib.RawIntTypes.fsti.checked Lib.Loops.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Lib.Buffer.fsti.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.fsti.checked FStar.Mul.fst.checked FStar.List.fst.checked FStar.Int.Cast.Full.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked FStar.BitVector.fst.checked
Impl.Noise.BufferEquality.fst
a: Lib.IntTypes.uint_t t l -> b: Lib.IntTypes.uint_t t l
  -> FStar.Pervasives.Lemma (ensures Lib.IntTypes.logxor a b == Lib.IntTypes.zeros t l <==> a == b)
Lib.IntTypes.inttype Prims.b2t Lib.IntTypes.unsigned Lib.IntTypes.secrecy_level Lib.IntTypes.uint_t Lib.IntTypes.logxor_spec Prims.unit FStar.UInt.logxor_self Lib.IntTypes.bits Lib.IntTypes.v Prims._assert Prims.l_imp Prims.l_not Prims.eq2 Prims.op_disEquality Prims.int Lib.IntTypes.logxor Lib.IntTypes.range_t FStar.UInt.logxor FStar.UInt.logxor_neq_nonzero Prims.op_Equality Lib.IntTypes.zeros
let logxor_uint_eq_zero_lem #t #l a b =
  
assert (v (zeros t l) = 0);
UInt.logxor_neq_nonzero #(bits t) (v a) (v b);
assert (Lib.IntTypes.v a <> Lib.IntTypes.v b ==>
    UInt.logxor #(bits t) (Lib.IntTypes.v a) (Lib.IntTypes.v b) <> 0);
logxor_spec a b;
assert (v a <> v b ==> v (logxor a b) <> 0);
assert ((~(a == b)) ==> v (logxor a b) <> 0);
UInt.logxor_self #(bits t) (v a);
logxor_spec a a