Instrumentable spec

[Kukovec]

Implements half of #99 (only deposit for now)

Makes the following changes:

• Adds the two contracts (timelock, token) from soroban_examples under ContractExamples/contracts
• Adds a monitor based on #37 under docs/timelock, together with a type hints file to use with fetch
• Adds two scripts which:
  • initialize Docker and populate soroban with aliases
  • Automate the deployment of the two contracts and basic invocations, ending in a deposit call
• Changes instrumentation, s.t.:
  • env now gets instrumented with two additional fields, tracking which values were set in storage before and after the transaction
  • The order of conjuncts in Next is changed, so that it initializes before calling the method operator, avoiding use-before-assignment in the case where the method operator references primed variables
  • The way Variants!Variant arguments are passed is fixed.

[konnov]

we have to add proper attribution to the files we copy from elsewhere

[Kukovec]

Just a heads up regarding the commit you're about to see (TLA noise). Apalache translates UNCHANGED x not into x' = x, but into x' := x (using the assignment operator). This becomes a problem, because x' = x /\ UNCHANGED x triggers an "assigneed twice" exception in Apalache, since left-to-right analysis necessitates that the first conjunct, x' = x, be taken as an assignment as well. Semantically, there is no change, but since I had to change the conjunct order in Next instrumentation, I have to update the current test monitors using UNCHANGED as well.

[thpani]

This becomes a problem, because x' = x /\ UNCHANGED x triggers an "assigneed twice" exception in Apalache, since left-to-right analysis necessitates that the first conjunct, x' = x, be taken as an assignment as well. Semantically, there is no change, but since I had to change the conjunct order in Next instrumentation

Looks to me like you should emit UNCHANGED x, not x' = x, in the first place?

Otherwise,

I have to update the current test monitors using UNCHANGED as well.

it sounds like we'd have to discourage use of UNCHANGED in the monitor specs? Not particularly fond of that idea.

[Kukovec]

... it sounds like we'd have to discourage use of UNCHANGED in the monitor specs? Not particularly fond of that idea.

I'll try do dig up the conversation in the Apalache repo explaining why we translate unchanged as an assignment, but from memory, the TLDR is that x' = x is a regular condition, whereas UNCHANGED x is an actionable declaration of the shape of the successor state, and since Apalache has assignments, which base TLA lacks, the UNCHANGED -> := translation felt like it made sense at the time, even though it's working against us here.

Edit: I found the Apalache issue 1346, but it unfortunately just says "per our discussions"

[Kukovec]

1. Why don't we link the soroban examples via git modules? Otherwise, it would be real hard to keep code in sync, when soroban-examples are updated. Also, what's the point of copying the code from another project? We would have to take care of the licenses and other uninteresting stuff.

We could, but to my knowledge, there's no way to submodule in only a part of the repository, so we'd have to include all of soroban-examples. If we don't mind that, I'll go ahead and do a submodule

2. I don't get the discussion about UNCHANGED. Yes, we thought that forcing UNCHANGED to be an assignment was a good idea, but why do we introduce two assignments in the first place?

Assume that you have X in fields, and somewhere inside method there is an UNCHANGED X. Our instrumentation does:

Next ==
 /\ ...
 /\ X' = concrete_value_from_fields
 /\ method(...)

which expands to

X' = a1 /\ ... /\ UNCHANGED X

You have two options:

1. Next == instrument_fields /\ method(...)
2. Next == method(...) /\ instrument_fields

If you do (2), you cannot ever reference any primed variable inside your method(...) (i.e. inside any monitor invariant), because you end up with assignment-before-use in Apalache. If you do (1), which we currently do, you cannot us any manual assignment in the method(...) part, because you end up with assigned-twice in Apalache. UNCHANGED is currenty, besides manually writing in assignments, the only way in which assignments sneak into the monitor(...) part

[konnov]

I don't want to block this PR on UNCHANGED. IMO, let's open an issue on UNCHANGED, maybe we even have to revisit Apalache on that. If we can avoid issues with UNCHANGED in the current examples, let's do that.