Remove the `-Znext-solver=coherence` pin: reimplement `pointer_generator` without `generic_const_exprs`

[feliperodri]

Summary

The nightly-2026-09-22 toolchain bump passes -Znext-solver=coherence to every crate Kani
compiles, opting all verified code out of the next-generation trait solver that rustc now enables
by default. That flag is a stopgap. It should come out, and the reason it exists —
kani::pointer_generator's generic_const_exprs signature — should go with it.

Why the flag is there

rustc enables the next-generation trait solver by default as of nightly-2026-09-22
(rust-lang/rust#160619), and that solver does not support generic_const_exprs
(rust-lang/rust#160895). rustc silently reverts to -Znext-solver=coherence for any crate that
enables the feature itself, so library/kani still builds. But Kani exposes the feature in a
public signature:

// library/kani_core/src/arbitrary/pointer.rs
pub fn pointer_generator<T, const NUM_ELTS: usize>()
-> PointerGenerator<{ core::mem::size_of::<T>() * NUM_ELTS }> {
    PointerGenerator::<{ core::mem::size_of::<T>() * NUM_ELTS }>::new()
}

A crate being verified does not enable the feature, so it gets the new solver and cannot call that
function:

error[E0284]: type annotations needed
   --> library/kani_core/src/arbitrary/pointer.rs:358:9
    = note: cannot satisfy `kani::pointer_generator<T, NUM_ELTS>::{constant#0} == _`

This is upstream behaviour rather than something Kani does wrong — it reproduces in two plain
crates outside Kani (one enabling generic_const_exprs and exposing such a signature, one calling
it), and -Znext-solver=coherence on the caller is what fixes it. Applying the same flag Kani-wide
is the same escape hatch rustc applies for itself.

Why it should not stay

• Verified code is type-checked by the solver rustc is migrating away from, so Kani can in
  principle accept or reject a program differently from cargo build. Divergence between "what
  rustc compiles" and "what Kani verifies" is exactly the kind of gap we do not want.
• The old solver will eventually be removed, at which point the flag stops working rather than
  degrading.
• It is applied globally in base_rustc_flags (kani-driver/src/call_single_file.rs), so it
  affects the single-file, cargo, and playback flows — every user, not just those calling
  pointer_generator.

What needs to happen

1. Reimplement pointer_generator so its public signature does not carry a computed const.
   Options worth weighing: take the buffer length as the const parameter and compute the element
   count internally; return an opaque wrapper that hides the length; or provide the generator
   through a trait with an associated const. Any of these is a user-facing API change, so it wants
   its own design discussion.
2. Audit library/kani for other generic_const_exprs uses that leak into public signatures
   (the crate-level #![feature(generic_const_exprs)] should ideally go away entirely).
3. Drop -Znext-solver=coherence from base_rustc_flags and confirm the regression suite passes
   with the next solver enabled — that run is also the first real signal of whether the new solver
   changes anything else for Kani.

Priority

High: this blocks Kani from tracking rustc's actual type-checking behaviour, and the cost of
discovering problems grows the longer verified code runs on the old solver. It should be resolved
well before upstream removes the old solver.

[feliperodri]

The flag this issue is about lands in #4833 (the nightly-2026-09-22 bump): -Znext-solver=coherence in base_rustc_flags, kani-driver/src/call_single_file.rs, with a comment pointing here. Removing it means reshaping pointer_generator first — the flag is what keeps that signature callable from crates that do not enable generic_const_exprs.