wrongly reporting signature mismatch for external_fn_specification

[panda2134]

When constants are used in the type signature of arguments, external_fn_specification cannot be reliably used.

An example of this is shown in this minimal example. This line attempts to declare external_fn_specification for an external function. However, the following error is returned:

   Compiling ex_spec_reproduce v0.1.0 (/home/panda2134.linux/shadowfs-rs/ex_spec_reproduce)
error: external_fn_specification requires function type signature to match exactly (got `FnDef(DefId(0:20 ~ ex_spec_reproduce[5738]::verify::ex_read), [])` and `FnDef(DefId(0:15 ~ ex_spec_reproduce[5738]::ext::{impl#0}::read), [])`)
  --> src/verify.rs:13:5
   |
13 |     pub fn ex_read(s: &Device, out: &mut [u8; BLKSIZE]) {
   |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

error: verification failed

error: could not compile `ex_spec_reproduce` (lib) due to 1 previous error

I merged commits from the cargo-verus pull request into the main branch to verify the whole crate. The commit hash on main branch is 2996c51. In the case above, it seems like the constant BLKSIZE is causing the problem, because the issue disappears when BLKSIZE is replaced by 4096usize.

[panda2134]

I'm converting this into an issue because when I tested again I found that the bug has not been fixed in latest Verus.