Add more detailed instructions on how to write predicates

[dc-mak]

@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.

rems-project/cerberus#848 (comment)

[bcpierce00]

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]

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]

Yes, this might be a good starting point / case study. I guess it belongs in the section on arrays. (I need to do some more work on understanding it!)

[lwli11]

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]

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!