val lemma_logxor_lt (#n: pos) (a b: uint_t n) (k: nat{k <= n})
    : Lemma (requires a < pow2 k /\ b < pow2 k) (ensures a `logxor` b < pow2 k)
val lemma_logxor_lt (#n: pos) (a b: uint_t n) (k: nat{k <= n})
    : Lemma (requires a < pow2 k /\ b < pow2 k) (ensures a `logxor` b < pow2 k)
let lemma_logxor_lt (#n:pos) (a b:uint_t n) (k:nat{k <= n})
  : Lemma (requires a < pow2 k /\ b < pow2 k)
    (ensures a `logxor` b < pow2 k)
= if k = n
  then ()
  else if k = 0
  then begin
    assert_norm (pow2 0 == 1);
    assert (a == 0);
    assert (b == 0);
    logxor_self #n 0
  end
  else begin
    pow2_lt_compat n k;
    to_vec_inc n k a;
    to_vec_inc n k b;
    to_vec_inc n k (logxor #k a b);
    nth_lemma #n (logxor #k a b) (logxor #n a b)
  end
module QUIC.UInt
include FStar.UInt
open FStar.Math.Lemmas

#push-options "--z3rlimit 16"

let rec to_vec_prefix
  (n: nat)
  (k: nat)
  (a: uint_t k)
: Lemma
  (requires (k <= n))
  (ensures (
    pow2 k <= pow2 n /\
    to_vec #k a `Seq.equal` Seq.slice (to_vec #n a) (n - k) n
  ))
  (decreases k)
= if k = 0
  then ()
  else to_vec_prefix (n - 1) (k - 1) (a / 2)

let rec to_vec_inc
  (n: nat)
  (k: nat)
  (a: uint_t k)
: Lemma
  (requires (k <= n))
  (ensures (
    pow2 k <= pow2 n /\
    to_vec #n a `Seq.equal` (Seq.create (n - k) false `Seq.append` to_vec #k a)
  ))
  (decreases k)
= if k = 0
  then ()
  else to_vec_inc (n - 1) (k - 1) (a / 2)
/
prims.fst.checked FStar.UInt.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Math.Lemmas.fst.checked
QUIC.UInt.fst
a: FStar.UInt.uint_t n -> b: FStar.UInt.uint_t n -> k: Prims.nat{k <= n}
  -> FStar.Pervasives.Lemma (requires a < Prims.pow2 k /\ b < Prims.pow2 k)
      (ensures FStar.UInt.logxor a b < Prims.pow2 k)
Prims.pos FStar.UInt.uint_t Prims.nat Prims.b2t Prims.op_LessThanOrEqual Prims.op_Equality Prims.int Prims.l_or Prims.l_and Prims.op_GreaterThanOrEqual Prims.op_GreaterThan Prims.bool FStar.UInt.logxor_self Prims.unit Prims._assert Prims.eq2 FStar.Pervasives.assert_norm Prims.pow2 FStar.UInt.nth_lemma FStar.UInt.logxor QUIC.UInt.to_vec_inc FStar.Math.Lemmas.pow2_lt_compat Prims.op_LessThan Prims.squash Prims.Nil FStar.Pervasives.pattern
let lemma_logxor_lt (#n: pos) (a b: uint_t n) (k: nat{k <= n})
    : Lemma (requires a < pow2 k /\ b < pow2 k) (ensures a `logxor` b < pow2 k) =
  
if k = n
then ()
else
  if k = 0
  then
    (assert_norm (pow2 0 == 1);
      assert (a == 0);
      assert (b == 0);
      logxor_self #n 0)
  else
    (pow2_lt_compat n k;
      to_vec_inc n k a;
      to_vec_inc n k b;
      to_vec_inc n k (logxor #k a b);
      nth_lemma #n (logxor #k a b) (logxor #n a b))