Skip to content

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

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.

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

Labels

No labels
No labels

Type

Projects

No projects

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions