global size_of/layout does not work across multiple modules

[ouuan]

Now the global size_of / global layout syntax only works inside the module that defines it. It does not work across multiple modules, while it can be defined only once per crate.

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

use vstd::prelude::*;
use core::mem::size_of;

verus! {

global size_of usize == 8;

fn main() {
    assert(size_of::<usize>() == 8);
}

}

mod foo {

use vstd::prelude::*;
use core::mem::size_of;

verus! {

// global size_of usize == 8;

fn foo() {
    assert(size_of::<usize>() == 8);
}

}

}

note: recommendation not met
  --> /playground/src/main.rs:24:12
   |
24 |     assert(size_of::<usize>() == 8);
   |            ^^^^^^^^^^^^^^^^^^
   |
  ::: /playground/verus/source/vstd/layout.rs:61:9
   |
61 |         size_of::<V>() as usize as int == size_of::<V>(),
   |         ------------------------------------------------ recommendation not met

error: assertion failed
  --> /playground/src/main.rs:24:12
   |
24 |     assert(size_of::<usize>() == 8);
   |            ^^^^^^^^^^^^^^^^^^^^^^^ assertion failed