Add extern_spec for NonZero - #2220
Conversation
jhjourdan
left a comment
jhjourdan
left a comment
There was a problem hiding this comment.
Thanks for the contribution! Could you please address the comments before we merge?
| extern_spec! { | ||
| mod core { | ||
| mod num { | ||
| trait ZeroablePrimitive: View<ViewTy = Int> + DeepModel<DeepModelTy = Int> {} | ||
| } | ||
| } | ||
| } |
There was a problem hiding this comment.
This is a no-op. Extern specs cannot be used to add a super trait to a trait. Could you please remove this?
There was a problem hiding this comment.
Oh, sure, I thought it might be unneeded and forgot.
There was a problem hiding this comment.
Then could you remove this?
There was a problem hiding this comment.
Done in the newest push, I forgot to commit it. 🙈
|
Also you need to fix formatting. Please run |
b7828b6 to
3121ca1
Compare
|
I thought a bit more about this, and I think it should be useful (e.g., for bitwise operations) to have an opaque logical function from |
`NonZero` is a standard library type that is used for layout optimizations as well as using the type system to prove basic invariants. So far creusot didn't support it. This adds basic support for the type, so far only adding `View`, `DeepModel` and `Invariant` impls as well as constructors and the `get` method.
2686b18 to
ae8ebd8
Compare
Using an opaque logic function was requested as it should be more useful.
ae8ebd8 to
a16c681
Compare
|
Is this what you had in mind? I also remembered that the code could be |
| #[cfg(creusot)] | ||
| impl<T: ZeroablePrimitive> Plain for NonZero<T> { | ||
| #[trusted] | ||
| #[ensures(*result == *snap)] | ||
| #[check(ghost)] | ||
| #[allow(unused_variables)] | ||
| fn into_ghost(snap: Snapshot<Self>) -> Ghost<Self> { | ||
| Ghost::conjure() | ||
| } | ||
| } |
There was a problem hiding this comment.
Do you really need that?
I am not very confortable with this instance, because it implies that there is no null value of NonZero at the logical level, which in turns implies that we cannot model NonZero<T> with T directly (if we do that, then we exclude 0 at the program/ghost level, but not at the logical level). Modeling NonZero<T> with T directly is a simple way of specifying that get_logic is injective (which is sometimes useful but tedious in general).
There was a problem hiding this comment.
Ah, so users should just call get() in ghost code and use the resulting value for proofs? The reason I added this was that I came across the trait, saw it implemented on a bunch of primitives with the rationale that they are not pointers so since this isn't a pointer either I though it could be added for completeness. But I don't personally need this.
Also note that char has a niche and also impls Plain so maybe that one is also wrong?
There was a problem hiding this comment.
The problem is not with having a niche or not. The point is that to implement Plain, the logical meaning of the type should be the same as the meaning in programs. It's not the case for pointer types because they carry ownership in programs. It's neither the case here because of the niche, which is not enforced in the logic because type invariants are not enforced in the logic.
That being said, I think we should consider adding the type invariant as a precondition of into_ghost, but this is another story...
There was a problem hiding this comment.
Anyway, please remove this instance and I'll merge.
2 participants
NonZerois a standard library type that is used for layout optimizations as well as using the type system to prove basic invariants. So far creusot didn't support it.This adds basic support for the type, so far only adding
View,DeepModelandInvariantimpls as well as constructors and thegetmethod.Closes #2217