creusot
creusot copied to clipboard
creusot-rs
Ghost code v2
In #381 we gained support for an initial version of ghost code based on an adhoc language consisting of the intersection of Rust and Pearlite. This ghost code has borrow checking, but exists in a seperate 'universe' than normal rust values: you can move a value into ghost code but not out of it.
In general the semantics and syntax of v0 Ghost Code are unclear and in desperate need of formalization and specification.
Additionally, there is the issue of borrow checking. Today, ghost code is borrow checked but should that be the case? Should there be another layer of ghost code that follows the same rules as pearlite?
Here is how I see it:
- Ghost code should be purely functional, i.e., not borrow checked.
- If we need Ghost resources, then we could use ghost resource types such as Seq or synthetic tokens, as part of the non-ghost code. Functions of the Seq module will be no-ops operationally and will be inlined by the Rust compiler/LLVM optimizer.
If we need Ghost resources, then we could use ghost resource types such as Seq or synthetic tokens, as part of the non-ghost code. Functions of the Seq module will be no-ops operationally and will be inlined by the Rust compiler/LLVM optimizer.
I'm not sure that will really work, and makes guaranteeing erasure much harder: if ghost resources are in code then nothing prevents them from influencing control flow of the program. Additionally, I could want to mention logical resources (model etc...) in these ghost resources.
I still think that there are three levels at play, already: program code, linear ghost code, and pearlite (non-linear ghost code), why not just make those equally accessible in programs?
I'm not sure that will really work, and makes guaranteeing erasure much harder: if ghost resources are in code then nothing prevents them from influencing control flow of the program.
Well, none of these libraries would produce meaningful values at runtime.
Additionally, I could want to mention logical resources (model etc...) in these ghost resources.
In that case, these uses should not be considered for borrow checking, so they should be placed in Ghost/ghost! anyways.
I still think that there are three levels at play, already: program code, linear ghost code, and pearlite (non-linear ghost code), why not just make those equally accessible in programs?
I think there is no need to add an additional notion to the language. Ghost resources are just usual Rust values that have a zero-size runtime representation. But they have an actual logical model. Just like the current status of Int or Seq.
The other reason why I don't want to add this level of ghost code is that it's not really a new level of "ghostity", in the sense that it makes no sense to transform an actual program resource into a Ghost resource (this would mean, operationally, that resources get leaked, which is bad). So these resources are just another kind of resources the we want the borrow checker to take into account, in addition to plain physical resources.
Think of GhostCell: it is completely possible to write this type without special support for ghost resources from the compiler. And I don't see why we would have trouble specifying this in Creusot.
So these resources are just another kind of resources the we want the borrow checker to take into account, in addition to plain physical resources.
Yes but it feels natural that you would want to include non-program values in your ghost resources, values which may not be representable in programs.
Additionally, I have worries about the nature of the erasure here: I don't think we can guarantee that you get the same performance from code instrumented with ghost code and without, zero size or not.
Yes but it feels natural that you would want to include non-program values in your ghost resources, values which may not be representable in programs.
If the relevant thing is the value, then you can use Ghost. If the relevant thing is the physical resource, then they should not be included in ghost resources.
Additionally, I have worries about the nature of the erasure here: I don't think we can guarantee that you get the same performance from code instrumented with ghost code and without, zero size or not.
How is this different for Ghost? When you pass a Ghost parameter, it is seen by rustc as a zero-size value. I don't know whether there are situations where this has runtime cost, but the issue is the same.
A potential problem with this approach is that we may need to handle ghost resources differently depending on ghost information. I admit that we need some thoughts about this.
But in any case, in no way we should use physical data structures such as Vec in ghost code. This is just unsound, because Vec::push is not supposed to fail, but Vec::len is a bounded integer.
How is this different for Ghost? When you pass a Ghost parameter, it is seen by rustc as a zero-size value. I don't know whether there are situations where this has runtime cost, but the issue is the same.
Except the whole contents of the ghost! block are erased, leaving only the zero-sized values lingering.
A potential problem with this approach is that we may need to handle ghost resources differently depending on ghost information. I admit that we need some thoughts about this.
That's what I meant.
But in any case, in no way we should use physical data structures such as Vec in ghost code. This is just unsound, because Vec::push is not supposed to fail, but Vec::len is a bounded integer.
Well we can have proof obligations emanating from ghost code, that's no issue.
Well we can have proof obligations emanating from ghost code, that's no issue.
Which kind of proof obligation?
I don't think we want to require a precondition the Vec::push does not overflow. That's just too tedious. And anyways, this does not correspond to what happens in practice, because the program will likely crash by OOM way before the maximal length is reached.
In addition, such pre-condition can get in the way when we want to use Vec in ghost code. We don't want to have this to prove each time we want to add an element to a sequence.