The functional layer (pure defs) allows us to get closer to source code. If the whole business logic can be written as pure functions, this even allows us to do composition by using one function (defined viapure def) within another one, e.g.,

pure def foo(s: S): S = {  // pre steps  val temp = bar(s)  // post steps  // specify return value}

One problem is that when looking at source code, it might not be clear whetherbar is a pure function, or whether it is, e.g., an synchronous RPC. In the later case, the above quint snippet wouldn't make sense anymore. it would need to correspond to

1. one action capturing the pre steps
2. a transition system modeling the RPC (potentially involving multiple protocol steps with non-determinism)
3. post steps depending on the outcome of the RPC (sub) execution.

Right now we can model these RPCs in TLA+ and quint. However, as the above list shows, we need to leave the functional level and go to the actions. It would be great if quint could be extended to lift this to the functional level from a syntax viewpoint, e.g.,

cfunction foo(s: S): S = {  // pre steps  val temp = call bar(s)  // post steps  // specify return value}

Under the hood, we could then importbar(s) from another quint specification, linking this line to either

• two actions in the bar spec (call_bar andreturn_bar).
• some precondition / postcondition relation (that abstracts thebar implemention by its more abstract properties).