Lean backend silently emits a bodyless axiom for a function with a return nested two loop-levels deep, instead of erroring

[ivmat]

Environment

Aeneas: 45061fa
Charon: 40ee060a8df43f4e7e0842d3f05387b0a4426aaf
Backend: Lean 4
Extraction: charon cargo --preset=aeneas --dest then aeneas
Summary

A Rust function containing an early return nested two loop-levels deep (a return inside a while that is itself inside another loop) does not fail extraction — the Lean backend reports success but emits a bodyless axiom for the function instead of a definition. The documented limitation ("returns inside nested loops / breaks to outer loops are not supported yet") is understood; the problem is that the unsupported case degrades silently to an axiom rather than failing loudly. An axiom asserts nothing about the function's behavior, so any Lean proof built on top of it is vacuous, and a user can ship a "verified" lid without noticing it is unconstrained.

Minimal repro code

pub enum E { Bad }

// A `return` nested two loop-levels deep: inside the inner `while`, inside the outer `while`.
pub fn f(xs: &[u8]) -> Result<(), E> {
    let mut i = 0;
    while i < xs.len() {                 // outer loop
        let mut j = i;
        while j < xs.len() {             // inner loop
            if xs[j] == 0x80 {
                return Err(E::Bad);      // <-- return at loop-depth 2
            }
            if xs[j] & 0x80 == 0 { break; }
            j += 1;
        }
        i = j + 1;
    }
    Ok(())
}

Extract with charon cargo --preset=aeneas then aeneas. Observed: the generated Lean contains axiom f : ... (no body). Expected: a hard error (as other unsupported constructs produce, cf. #1206), or at minimum a warning naming the function and the reason when an axiom is emitted where a definition was expected.

Real-world context

Hit while verifying a DER/ASN.1 OID validator (validate_oid) in a Kani+Aeneas-verified Rust crate (github.com/ivmat/rs-verified-der). Early returns inside nested loops are a common Rust parser idiom, so the silent-axiom trap is easy to hit and hard to notice.

Workaround

Rewrite the function as a single loop with an explicit state variable so every early return sits at loop-depth 1. Concretely, the nested while-in-while above becomes one loop carrying an at_subid_start (or equivalent) flag; behavior is preserved (verified: all pre-existing Kani harnesses + full test suite re-passed) and, as a bonus, the flatter shape verified substantially faster.

Question for maintainers

Is the silent-axiom emission intended (vs. a hard error), and is the single-loop-with-explicit-state refactor the recommended workaround, or is there a preferred approach?