val to_vec_prefix (n 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)
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)
val to_vec_prefix (n 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)
let rec to_vec_prefix (n 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)
QUIC.UInt.fst.checked
prims.fst.checked FStar.UInt.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Math.Lemmas.fst.checked
QUIC.UInt.fst
Prims.nat FStar.UInt.uint_t Prims.op_Equality Prims.int Prims.bool QUIC.UInt.to_vec_prefix Prims.op_Subtraction Prims.op_Division Prims.unit Prims.b2t Prims.op_LessThanOrEqual Prims.squash Prims.l_and Prims.pow2 FStar.Seq.Base.equal FStar.UInt.to_vec FStar.Seq.Base.slice Prims.Nil FStar.Pervasives.pattern
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
  ))
val to_vec_prefix (n 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)
n: Prims.nat -> k: Prims.nat -> a: FStar.UInt.uint_t k
  -> FStar.Pervasives.Lemma (requires k <= n)
      (ensures
        Prims.pow2 k <= Prims.pow2 n /\
        FStar.Seq.Base.equal (FStar.UInt.to_vec a)
          (FStar.Seq.Base.slice (FStar.UInt.to_vec a) (n - k) n))
      (decreases k)