update to a rupicola/bedrock2 where wp is complete wrt exec

[samuelgruetter]

No description provided.

[andres-erbsen]

It would be nice to have a way that a function works correctly without putting it in an environment (perhaps like WeakestPrecondition.call) but the current change is eh-okay.

[samuelgruetter]

Currently, all our function specs are expressed in terms of WeakestPrecondition.call, which looks up the function to be called in the env, so we always have to add the hypothesis that it's in the env (which previously was also required, but in a less verbose way, by simply cons-ing it to the head of the functions list).
An alternative would be to say, all our function specs are expressed in terms of WeakestPrecondition.func (and probably, the prefix WeakestPrecondition should be changed to Semantics, then). That would mean, though, that spec_of instances already have to be able to refer to the implementation of the function being specified, so probably that's not what we want.
So for now, I don't see any immediately-obviously-good change to make right now, so, indeed, eh-okay 😅