let binding/multiple update patterns

[mira-alford]

Hi!!

In my work using boogie, we are experimenting with multiple different models of memory, and are hiding it all behind a black box memory model variable/type and functions that operate on it. Unfortunately, some procedures need to ensure multiple updates to the memory model, which would ideally look something like:

procedure malloc();
  modifies $memory_model;
  // Introduce temporary variables: #memory_model1, #memory_model2, #memory_model3
  ensures $memory_model1 == update_function_1(old($memory_model));
  ensures $memory_model2 == update_function_2(memory_model1);
  ensures $memory_model3 == update_function_3(memory_model2);
  ensures $memory_model == memory_model3;

Obviously the above wont work as it is introducing temporary variables, ideally there would be some equivalent to let bindings or temporary variables in the ensures clause?
Regardless the solution right now looks something like this:

procedure malloc();
  modifies $memory_model;
  ensures $memory_model == update_function_3(update_function_2(update_function_1(old($memory_model))));

However it quite quickly becomes unreadable when we specify complex procedures that ensure lots of updates to the memory model.
I'm just curious if there are any good patterns for this kind of scenario that keep the boogie code readable? Assuming I don't want to reason about/modify the internals of the update functions or memory model.