Stack-object example

[JuneRousseau]

This PR implements the stack object example from Monotone Cerise, adapted to the Griotte setup.

Among others, in addition to the original checks on the passed stack object, we also need to check that the passed SO does not overlap with our stack frame. In Monotone Cerise, this is guaranteed by the machine, because functions arguments are passed via the stack, and stack capabilities are Directed, meaning that they can't point upward.

[JuneRousseau]

Checking that the passed argument is a capability with at least read permission is very annoying without an instruction for getting more precise permission. See https://github.com/logsem/cerise-stack-monotone/blob/master/theories/examples/macros/checkra.v .
I think we can do the reverse enumeration (all the permissions that are not R or more), but it's still 8 tests.

[JuneRousseau]

The existing specification of the switcher return is too strong for proving the stack object example:
the unknown revoked addresses that we need to use to fix the final world are not all revoked from the same world,
and proving therefore, proving the world fixing requires multiple worlds for the different revoked addresses.

Intuitively, it comes from the fact that the passed SO contains words that are safe-to-share as public transitions of the world from the state pre-adversary call.
An unsafe example would be to pass a local capability for which we want no-capture: in the presence of passed SO, the callee can captures local capabilities via the passed SO, making it impossible to revoke via the switcher.

So, to make it work, we need a generalisation of the switcher specification: see switcher_ret_specification_gen in 340e39d.