Refinement with Guards and Locally Inductive Invariants (LIIs)

[jcp19]

Implementation of the technique for refinement using guards from the paper A Refinement Methodology for Distributed Programs in Rust. It includes a definition of LIIs as an interface. Everything is defined in Gobra (there are no assumptions and abstract symbols other than the function chooseGuardV which is a limited form of Hilbert's choice operator) and thus, the implementation is proven sound (relative to Gobra).

Note that the specs of the methods in this package are not compatible with those of the package refinement, and thus, they should not be used together in the same program.

[ArquintL]

Note that the specs of the methods in this package are not compatible with those of the package refinement, and thus, they should not be used together in the same program.

Can you elaborate what this exactly means? Would it be simply useless to import refinement too or is there a threat to soundness?

[jcp19]

I don't think it can ever lead to a soundness issue because the the APIs for the event systems have slight differences, and the way you specify IO operations is different depending on whether you use one approach or the other. Nonetheless, I am considering deprecating the old approach, given that this one (1) is more expressive (allows for guards), (2) does not impose a big burden if guards are not used -- essentially, it imposes the same proof obligations as the other library in that case.

[ArquintL]

No worries. I just wanted to point out that the description of this PR makes it sound like there’s some (unclear) sidecondition that one has to respect for soundness.
I believe your intent was simply that the contracts are incompatible between the two approaches and thus one has to pick one if one ever wants to successfully prove a program