Open hayley-leblanc opened 1 week ago
Nice one-word fix!
Thank you @hayley-leblanc. It would be good to add a regression test: let me know if I should take care of that.
I took a stab at writing a regression test and realized that my fix doesn't fully fix the issue (but I happened to somehow only test cases where it works when I was working on it, oops). I don't quite understand why it works in some cases and not others -- there is some odd behavior when using sizes/structs defined in a different module.
Some examples showing where the issue is fixed and where it's not:
Consider the following code:
mod m1 {
global size_of usize == 8;
}
mod m2 {
fn check_usize() {
assert(core::mem::size_of::<usize>() == 8);
}
}
In this example, the assertion on the size of usize
fails.
However, if we add a structure Foo
to m1
, set its size in m1
, use Foo
in m2
and add an assertion about its size like so:
mod m1 {
global size_of usize == 8;
pub struct Foo { val: u64 }
global size_of Foo == 8;
}
mod m2 {
use crate::m1::Foo;
fn check_usize() {
assert(core::mem::size_of::<usize>() == 8);
assert(core::mem::size_of::<Foo>() == 8);
}
}
Then both assertions pass. However, if we remove the assertion on the size of Foo
, then the assertion on the size of usize
fails.
A fix seems to be to broadcast use
the layout lemma generated by Verus (e.g., including broadcast use crate::m1::VERUS_layout_of_usize
in m2
) -- would it be sufficient to require users to do the broadcast use
(and document it), or would it be better to somehow automatically broadcast size lemmas to each module in the crate?
This PR addresses issue #1114 by making the broadcast proof fn
VERUS_layout_of_T
generated from theglobal size_of T
/global layout T
syntax public so that it is visible to all modules.