Pre- and Post-conditions
Assertions (and other code) are written in pre- and post-conditions of
scenario steps. They can be added with the function add_spec:
val add_spec : ?pre:(check list) -> ?post:(check_list) -> step -> step
The pre-condition will be executed before propagating the message matched by this step, and the post-condition will be executed after propagating the message.
💡 Note that, because a post-condition is executed after the message is propagated to its intended destination, there are no guarantees that it is already taken into account by the node. In particular, checking properties on the state of the destination node/baker after the propagation is most of the time meaningless.