WIP : Yield isolation proof
This branch adds a formal isolation proof preservation of the yield service, with minimal additions to the model. As a result, most of the code that indeed modifies the state is not at all integrated in the model. The most obvious and critical piece of code that is not modeled properly is the writeContext
function that writes an execution context inside a partition's accessible memory. Currently this function does nothing in the model.