Make broadcast size_of proof functions pub

[hayley-leblanc]

This PR addresses issue #1114 by making the broadcast proof fn VERUS_layout_of_T generated from the global size_of T/global layout T syntax public so that it is visible to all modules.

[y1ca1]

Nice one-word fix!

[utaal]

Thank you @hayley-leblanc. It would be good to add a regression test: let me know if I should take care of that.

[hayley-leblanc]

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?