Specify alloc::Layout#1972
Conversation
| pearlite! { | ||
| align != 0 && | ||
| (exists<a: Int> a.pow2() == align) && | ||
| size <= isize::MAX@ && |
There was a problem hiding this comment.
| size <= isize::MAX@ && | |
| 0 <= size && size <= isize::MAX@ && |
|
|
||
| /// Requirements for creating a [`Layout`]. | ||
| #[logic(open)] | ||
| pub fn layout_requirements(size: Int, align: Int) -> bool { |
There was a problem hiding this comment.
One possibility would be to require size and align to be positive usize values that fit an isize. I think that would simplify quite a few specs.
There was a problem hiding this comment.
Also, there is one missing requirement:
size, when rounded up to the nearest multiple of align,
must not overflowisize(i.e., the rounded value must be
less than or equal toisize::MAX).
There was a problem hiding this comment.
Yeah, but the actual program values this specifies are usize, so you would still need to require that they are in bounds for isize
There was a problem hiding this comment.
I don't think your requirements implies this requirement, which is part of Rust's documentation.
There was a problem hiding this comment.
One possibility would be to require
sizeandalignto be positiveusizevalues that fit anisize. I think that would simplify quite a few specs.
That's what I originally did, but this is annoying since size_of_logic/align_of_logic return Ints, so you need some shenanigans to pass them to layout_requirements.
There was a problem hiding this comment.
I see. We need a way to caset from Int to machine integers.
| res.size_log() == s && | ||
| res.align_log() == align_of_logic::<T>() | ||
| } else { | ||
| exists<err> result == Err(err) |
|
Generally, this is typically the kind of modules where I would expect a formal proof to make sure none of the spec is unsound. |
2 participants
No description provided.