creusot
creusot copied to clipboard
creusot-rs
State of `DeepModel` and `ShallowModel`.
I wonder if we we should re-evaluate the existence of both DeepModel and ShallowModel. Can we feasibly combine the two? Would it be excessive to get rid of ShallowModel entirely?
We can discuss ShallowModel, but this is mainly a matter of notations. We don't need that, we can ask for every type which need this do declare its own model function. But this is tedious and we won't have the @ notation.
What we can do, though, if we want to simplify the current status, which is far from ideal, is to add a trait ShallowModelIsDeepModel which inherits from DeepModel, and have a generic instance impl<T : ShallowModelIsDeepModel> ShallowModel for T. This would avoid the need to declare the two instances each time.
In addition, we could have derive macros that would allow creating these instances automatically for structs and enums.
An alternative is to have a default instance DeepModel => ShallowModel, and specialize it when we need to give a different ShallowModel instance. But I am a bit afraid that we might not be able to see that the dafault instance is not further specializable in practical cases, which is necessary to see its definition transparently....
Thinking about it, I wonder about something: why do you need to define a shallow model on structs, where the model type would be a struct itself ? I can't think of a use case for this. If you need to speak about the shallow model of the fields, then you should rather do @x.field.
Yet another option would be to define another specific notation for deep models...
Il very against a second notation for deep models, I am also starting to think we should make @ postfix like verus does (avoids a bunch of parens)
Thinking about it, I wonder about something: why do you need to define a shallow model on structs, where the model type would be a struct itself ? I can't think of a use case for this. If you need to speak about the shallow model of the fields, then you should rather do @x.field.
The main reason is when you need to call a function which takes a tuple / strict which corresponds to that shallow model.
I implemented this macro, but ... it does not work since we don't allow associated tpyes in declarations :(( I guess there's no way arund finally fixing that issue.
The main reason is when you need to call a function which takes a tuple / strict which corresponds to that shallow model.
I'm trying to understand why we don't need such a thing in other tools such as Why3, or even Coq.
Why cannot you pass the concrete (non-model) value to these functions? I imagine that's what we would do in Why3...
I don't see why an enumeration would be different than a struct here.
If I have a function which takes (Int, Int) and I have (u33, u32) what am I to do? More generally how would you write generic code over T : ShallowModel where T could be instantiated as a product type?
I don't see why an enumeration would be different than a struct here.
Agreed.
If I have a function which takes (Int, Int) and I have (u33, u32) what am I to do?
Then probably your function should take a (u32, u32) instead, and have the conversions in the body of the function. If there is a reason your functions is taking a pair of integers instead of each integer independently, then it means that "pair of integer" is some kind of abstraction that has a meaning in your proof, and you'd rather not have two different types for this abstraction.
That's basically what we would do in Why3. And this is likely to be better handled by provers because they will not have a (u33, u32) -> (Int, Int) translation to unfold.
More generally how would you write generic code over T : ShallowModel where T could be instantiated as a product type?
ShallowModel is a trait that should only be used for notation purposes (i.e., that's the trait associate with the @ notation). So you should not write code generic w.r.t. a type with this constraint.
But we already have code that is generic over it: instances like ones for borrows
But we already have code that is generic over it: instances like ones for borrows
I had a look at all the generic code over this trait. They are of two kinds:
-
Building notation instances from other notation instances. This is the case of
ShallowModelinstances forBox, borrows andGhost, and instances ofIndexLogicwhen the shallow model isSeq. I don't think this is problematic: this is just defining more notations. -
The definition of
SliceIndex. This one is sealed, so not really generic...
I wonder if you could use something like:
trait DeepModelForShallow {}
impl<T: DeepModelForShallow + ShallowModel> DeepModel for T
where T::ShallowModelTy: DeepModel{
type DeepModelTy = T::ShallowModelTy::DeepModelTy;
fn deep_model(self) -> Self::DeepModelTy {
self.shallow_model().deep_model()
}
}
I would require adding DeepModel implementations for the types in logic (eg. Seq, Mapping ...), but it seems like it is usually what you want, and has the nice property that x@ == y@ ==> x.deep_model() == y.deep_model().
There was an issue with instance overlaps when I last tried this, though I forget the specific issue I had.
I was agonizing over ShallowModel again recently (I really hate that trait; it feels unprincipled), but I think one thing that would comfort me is if we made x@ == y@ ==> x.deep_model() == y.deep_model() a law of deepmodel at the very least.
Part of this came up because I proved that x@ == y@ but the code contains assert_eq!(x, y) !!!!! which is defined on deep_model..
I don't know. It rather looks like a "good practice" than something which is required fundamentally.
I don't know. It rather looks like a "good practice" than something which is required fundamentally.
If we don't make it a law it becomes entirely ad-hoc and counter intuitive. in this case it was for Vec<Foo>, where i would expect this to hold. Additionally, I fail to see a type where we dont want / can't have this.
Almost all our specifications talk about things being ShallowModel Equal but we have no mechanism to relate that to == which is DeepModel equal; that's a bug.
Ok, right, I see the argument.
But then, that would mean that we require a ShallowModel for any type implementing DeepModel. Do we really want this?
But then, that would mean that we require a ShallowModel for any type implementing DeepModel. Do we really want this?
Not necessarily: we can word the law as such
#[requires(x@ == y@)] #[ensures(x.deep_model() == y.deep_model())]
fn shallow_implies_deep(x : Self, y : Self) where Self : ShallowModel;
Oh wow! Is that sound?
We probably already discussed that, but that's a bit frightening because we rely on the orphan rules to make sure that no instance is going to appear in a different crate....
We probably already discussed that, but that's a bit frightening because we rely on the orphan rules to make sure that no instance is going to appear in a different crate....
I don't understand this? This law would be required to be proved by each type implementing DeepModel, no other crate or type could sneak in a ShallowModel instance for the same type anyways...
If a type has DeepModel but not ShallowModel, then the proof obligation will not be required. But if in a later crate we implement ShallowModel, the proof obligation will not show up either.
That's my point: we are using orphan rules to guarantee soundness. That's a bit frightening to me, because orphan rules are designed for coherence, which is different to guarantee that such and such trait impl does not exist.
Coherence is important for the soundness of certain Rust apis as far as I know as well, I don't think this meaningfully changes things.
A thought which occured to me recently was that if we introduce #[pure] it would become possible to remove DeepModel entirely. We could then specify ParitalEq directly in terms of eq being an equivalence relation.
However, @jhjourdan pointed out that this could introduce issues for the solvers as they could find themselves required to prove that eq is a morphism for different operations (ie PartialOrd). I still think that the benefit is high enough that we should attempt the experiment when possible.
I seem like DeepModel is necessary to match how Creusot currently specifies T: PartialEq<U> since it forces T U to have the same DeepModelTy and guarantees that equality is transitive across types
You're right that we would only be able to specify homogenous equality :/ I think in practice this covers 99.9% of uses of PartialEq however.