Instrumentable spec #100

Kukovec · 2024-06-10T12:31:09Z

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 Investigate reverse reasoning for monitors #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 · 2024-06-10T12:35:13Z

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

Kukovec · 2024-06-10T13:06:33Z

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

First set of comments – I haven't looked at the TLA+ yet

I don't understand why you diverge from the existing scripts in ContractExamples/scripts/ so much. They would be much easier to use if they all follow the same function + style.
There's a LICENSE on solarkraft-examples that we have to comply with.

ContractExamples/scripts/init-timelock.sh

ContractExamples/scripts/prepare-timelock.sh

thpani · 2024-06-10T13:12:00Z

ContractExamples/scripts/prepare-timelock.sh

+    --token $TOKEN\
+    --amount 1 \
+    --claimants "[\"$(soroban keys address bob)\"]"\
+    --time_bound '{"kind": "After", "timestamp": 0}'


Maybe use a more realistic whitespace here?

Sorry, I meant more realistic timestamp 😅

"After 0" should mean that the claimants can claim whenever, which I thought would be easy to follow-up test. If you hardcode any fixed timestamp you either a) functionally get the same thing as 0 if that time has already passed, or b) have to actually wait before calling claim.

thpani · 2024-06-10T13:38:42Z

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 · 2024-06-10T13:43:18Z

...
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"

thpani

second set of comments

thpani · 2024-06-11T07:22:43Z

ContractExamples/contracts/timelock/LICENSE.md

thpani · 2024-06-11T07:22:49Z

ContractExamples/contracts/token/LICENSE.md

ContractExamples/scripts/prepare-timelock.sh

thpani · 2024-06-11T07:44:49Z

doc/timelock/state.tla

+instance_set(key, env) ==
+    env.storage_after \ env.storage_before = {key}


idk what the semantics of this are meant to be, but I would expect

key \in (env.storage_after \ env.storage_before)

In any case, the intention seems to be ambiguous and worth adding a comment.

So the original code here was

instance_storage' = instance_storage \union {key}

My understanding of the intent here was that the interpretation of this was "exactly key gets set" (since "key is set" could have been tested just via key \in instance_storage'), and I rewrote it that way, because A = B \cup {x} is true iff A differs from B by exactly x or if they both contain x, which I assumed to have been an oversight.
Your suggestion, x \in A\B would evaluate to true if A \ B equaled {x, y, z, ...} too (which may or may not have been the actual intent). Perhaps @andrey-kuprianov can comment best on what the intended semantics here were.

thpani · 2024-06-11T07:45:24Z

doc/timelock/state.tla

+
+\* @type: ($storageKey, $env) => Bool;
+instance_remove(key, env) ==
+    env.storage_before \ env.storage_after = {key}


Same as above

doc/timelock/deposit.tla

konnov

I had a very quick view at the PR:

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.
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?

Co-authored-by: Thomas Pani <[email protected]>

Kukovec · 2024-06-11T09:36:17Z

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

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:

Next == instrument_fields /\ method(...)
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 · 2024-06-11T14:07:01Z

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.

thpani

I guess this is fine – not the kind of PR I would've liked to review multiple times.

The discussion on UNCHANGED is lost on me, maybe @konnov still wants to comment.

doc/timelock/deposit.tla

.github/workflows/main.yml

thpani

Unblocking this given Igors comment

Co-authored-by: Thomas Pani <[email protected]>

Kukovec added 3 commits June 10, 2024 10:22

Copied contracts into our ContractExamples dir

836a5bb

scripts and hints

438aa3e

timelock monitor for deposit

c28489e

Kukovec requested review from thpani, konnov and andrey-kuprianov June 10, 2024 12:31

tests and attribution

49f457d

thpani reviewed Jun 10, 2024

View reviewed changes

pr comments

555dbb6

thpani reviewed Jun 11, 2024

View reviewed changes

konnov reviewed Jun 11, 2024

View reviewed changes

Apply suggestions from code review

ac50b5f

Co-authored-by: Thomas Pani <[email protected]>

Kukovec added 7 commits June 11, 2024 11:45

PR comments

4bf8239

rm'd README

44948bd

submodule init in tests

2e9be97

excluded submodule from build/test

70ffe88

2nd attempt at submodules

a0b4854

.

b5cbdfe

Exclude submodule tests

0941c93

thpani reviewed Jun 11, 2024

View reviewed changes

doc/timelock/deposit.tla Outdated Show resolved Hide resolved

.github/workflows/main.yml Outdated Show resolved Hide resolved

thpani approved these changes Jun 11, 2024

View reviewed changes

Apply suggestions from code review

5a8716c

Co-authored-by: Thomas Pani <[email protected]>

Kukovec merged commit 6ad18f1 into main Jun 11, 2024
3 checks passed

Kukovec deleted the jk/instrumentableSpec branch June 11, 2024 14:22

konnov added this to the M4: Case study milestone Jun 19, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Instrumentable spec #100

Instrumentable spec #100

Kukovec commented Jun 10, 2024

konnov commented Jun 10, 2024

Kukovec commented Jun 10, 2024 •

edited

Loading

thpani left a comment

thpani Jun 10, 2024

thpani Jun 11, 2024

Kukovec Jun 11, 2024

thpani commented Jun 10, 2024 •

edited

Loading

Kukovec commented Jun 10, 2024 •

edited

Loading

thpani left a comment

thpani Jun 11, 2024

thpani Jun 11, 2024

thpani Jun 11, 2024

Kukovec Jun 11, 2024

thpani Jun 11, 2024

konnov left a comment •

edited

Loading

Kukovec commented Jun 11, 2024 •

edited

Loading

konnov commented Jun 11, 2024

thpani left a comment

thpani left a comment

		instance_set(key, env) ==
		env.storage_after \ env.storage_before = {key}

Instrumentable spec #100

Instrumentable spec #100

Conversation

Kukovec commented Jun 10, 2024

konnov commented Jun 10, 2024

Kukovec commented Jun 10, 2024 • edited Loading

thpani left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

thpani commented Jun 10, 2024 • edited Loading

Kukovec commented Jun 10, 2024 • edited Loading

thpani left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

konnov left a comment • edited Loading

Choose a reason for hiding this comment

Kukovec commented Jun 11, 2024 • edited Loading

konnov commented Jun 11, 2024

thpani left a comment

Choose a reason for hiding this comment

thpani left a comment

Choose a reason for hiding this comment

Kukovec commented Jun 10, 2024 •

edited

Loading

thpani commented Jun 10, 2024 •

edited

Loading

Kukovec commented Jun 10, 2024 •

edited

Loading

konnov left a comment •

edited

Loading

Kukovec commented Jun 11, 2024 •

edited

Loading