Boogie

[Civl] Added explicit gates to atomic actions (#911)

This PR allows gates of atomic actions to be explicitly specified. The
convention is as follows:

var {:layer 0,1} x: int;

yield invariant YieldInv();
invariant ...

atomic action Foo()
requires x > 0; // gate (must be sufficient to prove absence of failures
in atomic action)
requires call YieldInv(); // precondition used only in special
circumstances
{
   assert x != 0;
}

---------

Co-authored-by: Shaz Qadeer <shaz@meta.com>