Monitor specs for Timelock using reverse reasoning

[andrey-kuprianov]

TLA+ specs modeled after https://github.com/stellar/soroban-examples/blob/v20.0.0/timelock/src/lib.rs

closes #37.

The TLA+ specs are complete in the sense that the instrumented version passes apalache-mc check as expected.

[Kukovec]

The overall approach idea LGTM, though I have raised a point RE mustfail/mustsucceed semantics in the comments.

Since you say the monitor spec is incomplete I haven't really looked into it much. Also, per your request, I've avoided giving proofreading-suggestions, though I would recommend doing a proofreading pass before merging once all conceptual discussions are out of the way.

[Kukovec]

As a user, would you really want this? This is essentially requiring that the monitor authors care and specify all of the possible transaction failing scenarios, which limits your ability to do abstractions or partial monitors.

[andrey-kuprianov]

No, you don't have to give all failure scenarios. If there is a failure case which is not in the spec, there simply will be a warning (which can be also suppressed if needed), no other consequences.

[Kukovec]

See above.

[andrey-kuprianov]

The same. The idea is that the monitor is configurable: it may either be completely silent in some cases, or issue a simple warning, or in most severe cases interfere and abort a transaction.

In the first stage of the project it will be at most a warning. But the ultimate goal is to provide the really protective solution for the live blockchain.

[Kukovec]

You say "default", is there ever a case where this wouldn't be so?

[andrey-kuprianov]

no, it's just an unfortunate wording:) it's fixed, to that, not default

[Kukovec]

Suggested change

Now, is the approach described above enough to achieve the goals (safety, liveness, completeness) stated above? Think about it for a sec, before clicking on the our answer below.

Not sure this really needs to be in the docs, this feels more like how you'd write up homework for students.

[andrey-kuprianov]

It's more in the style of a blog post, actually; I might eventually make it that. For now it doesn't matter, I suppose, it will change quite a few times...

[Kukovec]

What is this exists? I can't seem to find a definition or reference.

[andrey-kuprianov]

yeah, sorry, the defs are missing. exists is supposed to mean that the key is present in the ledger. We'll need to figure out the exact mapping between TLA+ and Soroban constructs

[Kukovec]

From what I can find, balance is not a record type: https://github.com/freespek/solarkraft/blob/32f48e5f26e4cce76df4703a1b29fd1752cd1677/doc/scf24/example/timelock_mon2.tla

I know you say this spec is not valid TLA+, but having variable declarations and their types would help a lot.

[andrey-kuprianov]

For the actual semantics of what both specs are supposed to represent, look at the Timelock contract. In particular, balance is an entry in the ledger with the Balance key, which points to the ClaimableBalance struct when the key is present.

[andrey-kuprianov]

I also agree that the defs of the structs and everything should be present eventually. The idea now is to evaluate the approach as a whole, and to fill in the missing pieces later.

Not directly related to this, but tangentially: the idea is that eventually the definitions wrt. the concrete contract could be auto-generated from the contract source code, so we won't have to write them by hand. But that's also not in the current stage, but in a subsequent one.

[konnov]

This looks like a writeup for a blogpost. I was trying to understand how the structure imposed here would fit into the standard pre/post-conditions approach. I guess, it imposes some kind of specific shape on the monitors.

[konnov]

Since we have to run solarkraft verify against the timelock transactions, how shall we do that? Perhaps, add notes on that?

[andrey-kuprianov]

Since we have to run solarkraft verify against the timelock transactions, how shall we do that? Perhaps, add notes on that?

That's a good point. Insofar it has been in isolation; I need to make sure it fits well with the rest. Will do that.

[thpani]

In general, I like the idea. This would make for an interesting blogpost, for sure.

In practice, I'm concerned that this will not be feasible in this round:
Remember that Apalache processes invariants into verification conditions and actions into transitions, without giving much guarantees about their correspondence. The quantifications you use here (none/any/all of X fire) will be hard to check, or at least require multiple instrumented specs and model-checker calls, which will become quite costly.

[andrey-kuprianov]

The quantifications you use here (none/any/all of X fire) will be hard to check, or at least require multiple instrumented specs and model-checker calls, which will become quite costly.

Also a good point: I of course need to make sure that this fits well with the Apalache MC. Otoh, we could say that this is the general approach we use for structuring the monitor specs, and then in this phase cut some corners, e.g. perform certain translation steps manually, and automate them in the subsequent phases.

I will investigate.

[Kukovec]

I've noticed this PR seems to be creeping up on 1k LOC, would it be possible to split this into smaller PRs, which are easier to digest?

[Kukovec]

P1: claim, env, monitor, token

[Kukovec]

There's a broader issue here with how this is defined: If env, tx and instance_strorage are to be defined as TLA state variables, then instrumentation would have to instantiate them all, which is not what happens (see here)
The env gets passed as the 1st function argument, the data in tx is not instrumented at the moment, and neither is instance_storage, though the latter would probably be the easiest to simply add in.

[Kukovec]

I'd personally introduce an uninterpreted type here, e.g. "TBK" or even "TIME_BOUND_KIND", but it's not blocking

[Kukovec]

None of this is blocking, but from how the source code is structured:
https://github.com/yuzurush/soroban-contracts-101/blob/4f64753310b26c7853de1c9efcc0f6f2b349c15c/timelock/src/lib.rs#L104-L106
I see this (and the one below) conceptually as a MustFail_... predicate, since it panics if the condition doesn't hold, and executes a bunch of code afterwards if it does. So in my view:

Suggested change

	MustPass_claim_BeforeTimeBound(args) ==
	/\ Balance.time_bound.kind = "Before"
	/\ env.ledger_timestamp <= Balance.time_bound.timestamp
	MustFail_claim_BeforeTimeBound(args) ==
	/\ Balance.time_bound.kind = "Before"
	/\ env.ledger_timestamp > Balance.time_bound.timestamp

[Kukovec]

Similar to my comment in env, be conservative with VARIABLES, because they'd have to be instrumented, and I don't think this one is instrumented anywhere. Do we know how instrumentation behaves, repectively should behave, w.r.t. soroban_sdk::contractimport!?

[Kukovec]

Suggested change

	IF token \in DOMAIN token_balances THEN
	IF id \in DOMAIN token_balances[token] THEN
	token_balances[token][id]
	ELSE 0
	ELSE 0
	IF (token \in DOMAIN token_balances /\ id \in DOMAIN token_balances[token] )THEN
	token_balances[token][id]
	ELSE 0

Minor backend optimization, each ITE is a pick

[Kukovec]

See above

[Kukovec]

This is redundant, since the claim(...) operator only appears in the instrumented spec when the method name is "claim"

[thpani]

It's clear that this has been developed out of sync with the rest of the system.
I don't know what to do at this state, except to merge it and then try to incrementally make it work, which will be much harder than just incrementally adding working pieces from the beginning.

I have not looked at the tests. Could you add a shell script that executes them so we have some kind of QA here?

Below are some comments that I would like to see addressed before we merge this and take further steps.

[thpani]

When you say "not yet supported", why?

It looks like the token_balance module becomes irrelevant then and can be pruned.

[thpani]

I think we're mixing semantics here.
The comment says it will "panic" if the record doesn't exist, but we decided to initialize every missing field to Gen(). But I think then you want

Suggested change

	\* This trigger fires when the balance record content changes
	\* Notice that it will panic (won't fire) if the record doesn't exist
	MonitorTrigger_BalanceRecord_ContentChanged ==
	Balance /= Balance'
	\* This trigger fires when the balance record content changes
	MonitorTrigger_BalanceRecord_ContentChanged ==
	/\ instance_has("Balance")
	/\ next_instance_has("Balance")
	/\ Balance /= Balance'

[thpani]

I understand that this can be written this way, but not the rationale.

claim will also revert if it's called outside the timebound, so why isn't the dual of this simply in MustFail?

[thpani]

Isn't this implied by the triggers? If they fired, there must've been a successful tx.

[thpani]

Isn't this implied by the trigger? If it fired, there must've been a successful tx.

[thpani]

Why is MustFail_deposit_NotEnoughBalance not working?

In general, we should add issues for each of the ones that need to be commented out.

[Kukovec]

Per our discussion on Friday, I'm going to merge this as-is, and use it as a reference point to write a monitor which is syntactically more aligned with our current instrumentation strategy.