Functional composition in the distributed setting

[josef-widder]

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 via pure 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 whether bar 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 import bar(s) from another quint specification, linking this line to either

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

[konnov]

This is an interesting point. We have heard a request for pre/post-conditions in the recent user interview. They may actually solve the composition issue in a neat way.

[bugarela]

@shonfeder I was looking for something else and bumped into this. This seems pretty much the same thing we have been discussing with the action fusion. It actually states the problem much better than I had it in my head, and afaiu is similar to the scenario that me, Ivan and Jan have been talking about regarding synchronous message consumption between cosmwasm contracts.