Locks and unlocks in a library

[sjcjoosten]

Locks and unlocks should be built into vercors through a standard library, rather than having them in there natively.

[pieter-bos]

@bobismijnnaam, maybe you can reproduce some of your notes about first-class predicates here?

[bobismijnnaam]

Yes:

• Gobra implements first-class predicates, so we can always look there if we get stuck.
• Non-resource-typed arguments to first-class predicates are stored in a "predicate arguments" domain (similar to how values, eg integers, are stored in a sequence domain)
• An "uber" predicate is defined, containing all know predicate bodies.
• This uber predicate takes as an argument an instance of the earlier predicate arguments
• The bodies that this uber predicate contains is parameterized over the values extracted from the predicate arguments domain

I took a stab at a manual encoding of my understanding so far in the following file: higher_order_predicates_1.vpr.txt

Some leftover parts I haven't grasped yet:

• The uber predicate is effectively an if statement over all possible predicates. Therefore, there's always the final else case where you have to decide what to do if none of the if cases were true. In my encoding I decided to put "false" there, which is equivalent to stating that you know all predicate instances that can ever be constructed in the program. This is more or less the closed world assumption However there's a case for the open-world assumption, especially in the context of inheritance and abstract predicate families. I don't have a concrete proposal yet but I think you could also put an opaque predicate instance in the final else case, to indicate there are some resources to manage but you will never be allowed to inspect them.
• I think this encoding can be reused/abused to also encode a form of higher-order (ghost?) functions. There's a small attempt at that at the bottom of the earlier file, but @niomaster already poked quite a few holes in it earlier, so I think this still needs some more thinking.