Verus internal panic in check_decrease_int for mixed decreases measures #2127
Description
Compiling verus-experiments v0.1.0 (/home/xks/repos/murmur/verus-experiments)
verification results:: 1 verified, 0 errors
thread '<unnamed>' (104370) panicked at rust_verify/src/verifier.rs:834:21:
internal error: generated ill-typed AIR code: error 'in call to check_decrease_int, argument #2 has type "termination_panic!Instr." when it should have type "Int"' in expression '(check_decrease_int (let
((block!$0 (%Poly%vstd!seq.Seq<termination_panic!Instr.>. tmp%2)))
(vstd!seq.Seq.len.? $ TYPE%termination_panic!Instr. (Poly%vstd!seq.Seq<termination_panic!Instr.>.
block!$0
))
) decrease%init0 false
)'
stack backtrace:
0: __rustc::rust_begin_unwind
1: core::panicking::panic_fmt
2: rust_verify::verifier::Verifier::verify_bucket
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.
thread '<unnamed>' (104370) panicked at rust_verify/src/verifier.rs:2235:29:
worker thread panicked
stack backtrace:
0: __rustc::rust_begin_unwind
1: core::panicking::panic_fmt
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.
error: could not compile `verus-experiments` (bin "termination_panic")
Caused by:
process didn't exit successfully: `/home/xks/repos/murmur/tools/verus/dist/verus /home/xks/.rustup/toolchains/stable-x86_64-unknown-linux-gnu/bin/rustc --crate-name termination_panic --edition=2024 verus-experiments/src/bin/termination_panic.rs --error-format=json --json=diagnostic-rendered-ansi,artifacts,future-incompat --diagnostic-width=118 --crate-type bin --emit=dep-info,link -C embed-bitcode=no -C debuginfo=2 --warn=unexpected_cfgs --check-cfg 'cfg(verus_keep_ghost)' --check-cfg 'cfg(verus_keep_ghost_body)' --check-cfg 'cfg(verus_verify_core)' --check-cfg 'cfg(verus_no_vstd)' --check-cfg 'cfg(docsrs,test)' --check-cfg 'cfg(feature, values())' -C metadata=4cec84f8d3fc366d -C extra-filename=-4006e91d4ab2faa4 --out-dir /home/xks/repos/murmur/target/debug/deps -C incremental=/home/xks/repos/murmur/target/debug/incremental -L dependency=/home/xks/repos/murmur/target/debug/deps --extern verus_experiments=/home/xks/repos/murmur/target/debug/deps/libverus_experiments-725c5a6035e79743.rlib --extern verus_builtin=/home/xks/repos/murmur/target/debug/deps/libverus_builtin-706f8ab64a7a5a81.rlib --extern verus_builtin_macros=/home/xks/repos/murmur/target/debug/deps/libverus_builtin_macros-b5bb8a91402f2a13.so --extern vstd=/home/xks/repos/murmur/target/debug/deps/libvstd-940ef314c4422fd2.rlib` (exit status: 1)
code
use vstd::prelude::*;
verus! {
enum Instr {
A,
Loop { body: Vec<Instr> },
}
// Mutually-recursive spec fns with mismatched decreases measures:
// - size_block decreases on an int (block.len())
// - size_instr decreases on an Instr
//
// In the current Verus, this combination causes an internal AIR
// type error panic in check_decrease_int().
spec fn size_block(block: Seq<Instr>) -> nat
decreases block.len()
{
if block.len() == 0 {
0
} else {
1 + size_instr(block[0]) + size_block(block.subrange(1, block.len() as int))
}
}
spec fn size_instr(instr: Instr) -> nat
decreases instr
{
match instr {
Instr::A => 1,
Instr::Loop { body } => 1 + size_block(body@),
}
}
// Dummy entry point just to force the spec functions to be processed.
fn main() {
// The panic happens during verification, before exec code matters.
}
} // verus![dependencies]
vstd = "=0.0.0-2026-01-11-0057"
verus_builtin = "=0.0.0-2026-01-11-0057"
verus_builtin_macros = "=0.0.0-2025-12-07-0054"