Repository navigation
Add more detailed instructions on how to write predicates #121
Description
@lwli11 says
Well, maybe we could start with adding instructions on how to write predicates ourselves, like what elements are required, etc? The tutorial has an example, but not a rigorous definition. I think we could copy and slightly modify the example predicate, but not write one from scratch.
Activity
bcpierce00 commentedon Mar 6, 2025
Concrete suggestions (even sketchy ones) would be very very welcome -- we are revamping the tutorial right now, and this is exactly the sort of deeper explanation we'd like to offer.
dc-mak commentedon Mar 6, 2025
Perhaps the linked example of the cluster is an OK starting point?
I was thinking that you could structure it in terms of "if you want to X, you write Y" so "if you want to free, you need an Alloc token", or "if you want to do pointer arithmetic, you need allocs bounds" (I'm happy to help out with alloc* and pointer related things because that's all memory model things I need to write that at some point anyways).
bcpierce00 commentedon Mar 6, 2025
lwli11 commentedon Mar 6, 2025
How about starting with the structure of a predicate like in tutorials developers are used to, like: https://www.geeksforgeeks.org/python-functions/
So using the predicate example from the tutorial, predicate { u32 P, u32 Q } BothOwned (pointer p, pointer q), seems you start with the 'predicate' keyword, and then return type is ??? and parameters are ??, with the function name in the middle.
And then for the body, why don't you need requires/ensures, while still using take?
And then some info on where can you call predicates? Only in requires/ensures/loop invariants?
lwli11 commentedon Mar 6, 2025
Also, more examples for tricky cases would be appreciated. Especially for being able to declare variable-length arrays, which I know is possible with predicates but I can't get working. Thanks!