Skip to content

autoharness: E0080 abort when a const-generic fn has a const {} precondition on its usize param #4794

Closed

Description

@feliperodri

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.

Metadata

Metadata

Assignees

Labels

No labels
No labels

Type

Projects

No projects

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions