Introduce TypeScript monitors #135
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Immutable.fromJS deeply converts all JS objects to Maps.
For deserializing storage, we want the target object to instead be
Map -> JS object {instance:, persistent:, temporary:} -> Map.
Thus, we provide a custom loader instead.
|
@konnov This is a rather large change-set, so I recommend reviewing by commit. |
konnov
approved these changes
Oct 17, 2024
| /* the monitor */ | ||
|
|
||
| class TimelockMonitor extends SolarkraftJsMonitor { | ||
| deposit( |
There was a problem hiding this comment.
I like this. One idea: When you write deposit, this may be confusing, as you do not describe the behavior of deposit. Would it make sense to have a name like on_deposit, before_deposit, or deposit_ensures?
There was a problem hiding this comment.
Good point! I think on_deposit would work well.
I've put it in #141 to follow up on.
solarkraft/src/types.ts
Outdated
| */ | ||
| import { Either } from '@sweet-monads/either' | ||
|
|
||
| export type Result<T> = Either<string, T> |
This was referenced Oct 17, 2024
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
In order to evaluate how we write monitors, we need to iterate quickly based on several case studies.
The current TLA+ instrumentation is a bit too brittle to iterate quickly, and we have not fully understood how to translate Soroban's heterogeneous/duck-typed storage into TLA+ types.
Thus, we introduce a monitor driver for writing monitors in TypeScript.
Using the TS monitor driver introduced in this PR, writing a monitor in TypeScript is very simple: Create a TS class that extends
SolarkraftJsMonitorand provide methods corresponding to the contract functions. In the body of those functions, usereverts_ifandsucceeds_withmethods to specify the conditions under which the contract should revert or succeed. The monitor is then (programmatically) verified by instantiating the monitor class and calling theverifymethod with the hashes of the transactions to be verified.For an example, see f6e994e.
Closes #134