Reachable `assert` panic by `ensure` in spec

[Marsman1996]

PoC

use vstd::prelude::*;
verus! {
#[verus_spec(ensures true)]
pub const C: char = 'x';
fn main() {}
}

Panic Log

verus/source/vir/src/sst_to_air_func.rs

Line 701 in ac50b8f

assert!(!function.x.has.has_ensures); // no ensures allowed on spec functions yet

thread '<unnamed>' (47) panicked at vir/src/sst_to_air_func.rs:701:9:
assertion failed: !function.x.has.has_ensures
note: [run with `RUST_BACKTRACE=1` environment variable to display a backtrace](https://play.verus-lang.org/?version=stable&mode=basic&edition=2021#)

thread '<unnamed>' (47) panicked at rust_verify/src/verifier.rs:2154:29:
worker thread panicked

Env

Verus Version: 2026.02.11 c780c07

Playground Link

https://play.verus-lang.org/?version=stable&mode=basic&edition=2021&gist=8b8331645f3a4f612f184756d5e118dc

[Marsman1996]

With #2180 , it returns errors:

error: ensures clause unsupported on spec function
 --> ./test/ensure.rs:4:1
  |
4 | pub const C: char = 'x';
  | ^^^^^^^^^^^^^^^^^

error: aborting due to 1 previous error