Summary
--with-autoharness aborts with error[E0080] (const-eval failure) when the target library contains a const-generic function that enforces a precondition on its usize const parameter via a const {} block. Autoharness substitutes a fixed value (AUTOHARNESS_CONST_GENERIC_VALUE = 2) for every usize const generic without checking the function's own const preconditions, so the generated harness fails const-eval at codegen time, which is a hard error that aborts the entire run.
Where
kani-compiler/src/kani_middle/codegen_units.rs, choose_generic_instantiation:
AUTOHARNESS_CONST_GENERIC_VALUE is substituted for every usize const-generic parameter.
- The instance is accepted via
Instance::resolve(def, &args) + args_satisfy_predicates(...), which only validate trait bounds — not the function's required_consts (the const {} assertion blocks).
- The failure therefore only manifests later, during codegen, as an unrecoverable
E0080.
Reproducer
Run autoharness against a recent rust-lang/rust std (e.g. nightly-2026-08-21). core::escape now guards its const-generic helpers:
// library/core/src/escape.rs
const fn hex_escape<const N: usize>(byte: u8) -> ... { const { assert!(N >= 4) }; ... } // line 31/62
const fn escape_unicode<const N: usize>(c: char) -> ... { const { assert!(N >= 10 && N < u8::MAX as usize) }; ... } // line 138
Autoharness picks N = 2, producing:
error[E0080]: assertion failed: N >= 4 -> escape::hex_escape::<2>::{constant#1}
error[E0080]: assertion failed: N >= 4 -> escape::escape_ascii::<2>::{constant#1}
error[E0080]: assertion failed: N >= 10 && N < u8::MAX -> escape::escape_unicode::<2>::{constant#1}
error[E0080]: source element index exceeds input vector length -> portable-simd swizzle::<i32, 2>
All four abort codegen; --include-pattern/--exclude-pattern do not help because they filter which harnesses are verified, not which are codegen'd.
Impact
Blocks autoharness (and kani list/metrics with --with-autoharness) over the Rust standard library on current nightlies. Discovered in the verify-rust-std toolchain bump (PR #687).
Suggested fix
In choose_generic_instantiation, before accepting a const-generic instantiation, evaluate the instance's required_consts (or otherwise detect the const-eval failure) and reject the candidate — returning an Err/skip-reason (e.g. treat as an unsupported/skipped function) — instead of letting the failure reach codegen as a hard E0080.
Summary
--with-autoharnessaborts witherror[E0080](const-eval failure) when the target library contains a const-generic function that enforces a precondition on itsusizeconst parameter via aconst {}block. Autoharness substitutes a fixed value (AUTOHARNESS_CONST_GENERIC_VALUE = 2) for everyusizeconst generic without checking the function's own const preconditions, so the generated harness fails const-eval at codegen time, which is a hard error that aborts the entire run.Where
kani-compiler/src/kani_middle/codegen_units.rs,choose_generic_instantiation:AUTOHARNESS_CONST_GENERIC_VALUEis substituted for everyusizeconst-generic parameter.Instance::resolve(def, &args)+args_satisfy_predicates(...), which only validate trait bounds — not the function'srequired_consts(theconst {}assertion blocks).E0080.Reproducer
Run autoharness against a recent
rust-lang/ruststd (e.g. nightly-2026-08-21).core::escapenow guards its const-generic helpers:Autoharness picks
N = 2, producing:All four abort codegen;
--include-pattern/--exclude-patterndo not help because they filter which harnesses are verified, not which are codegen'd.Impact
Blocks autoharness (and
kani list/metrics with--with-autoharness) over the Rust standard library on current nightlies. Discovered in the verify-rust-std toolchain bump (PR #687).Suggested fix
In
choose_generic_instantiation, before accepting a const-generic instantiation, evaluate the instance'srequired_consts(or otherwise detect the const-eval failure) and reject the candidate — returning anErr/skip-reason (e.g. treat as an unsupported/skipped function) — instead of letting the failure reach codegen as a hardE0080.