allow #[verifier(external_body)] again on consts

[utaal]

Write test for regression introduced by bf90ae0 and reported by #1322, partial fix.

@tjhance can you take a look to see if you can spot why the test is failing (after I allowed Consts as items that can be external_body)? You've recently worked on this code, so you're probably the most familiar.

[tjhance]

This issue doesn't have to do with the external-refactor, i.e., I get this panic on 601e1e7 (commit before bf90ae0):

thread '<unnamed>' panicked at vir/src/poly.rs:405:66:
no entry found for key

(The key-not-found in question is VarIdent("%return", VirParam)). So I think we may have never supported this, or it was something else that broke it.

[utaal]

Thanks for checking! And sorry for the incorrect blame for the regression.

@matthias-brun can you confirm that this used to work? If so, we can bisect to find the culprit, or otherwise work on a solution.

[matthias-brun]

Ah, it looks like combining external_body with a const ensures used to cause a panic but now generates the error.

My original example didn't have the ensures.

use vstd::prelude::verus; verus!{

#[verifier(external_body)]
const A: usize = unimplemented!();
}

This one works fine on Verus commit 2dbda4a but generates the error on current main.

[tjhance]

I'd suggest we go ahead and merge this then, and file an issue for the external_body/ensures combo.