ADR1 #2
ADR1 #2
Conversation
|
@thpani @andrey-kuprianov pinging since I can't set reviewers |
This looks like a constraint somewhere in the project settings |
| 2. Creating `.json`-format TLA+ input (Apalache specific) | ||
|
|
||
| ## Solution | ||
| Regarding Smart contracts, I propose using JSON directly (1.), as it seems unlikely that we'd want to implement significantly broader capabilities for smart contracts in Solarkraft. |
There was a problem hiding this comment.
I am still not sure about JSON. Remember, we had to make a few decisions in the ITF format. Actually, why don't we just use the same fragment as in ITF?
There was a problem hiding this comment.
I mean, we can use the same fragment, the point I was trying to make is that instead of designing an IR for State, we write State directly as JSON. The format of that JSON is an orthogonal issue.
There was a problem hiding this comment.
Yes, we can write it in json and map it to rust with serde
There was a problem hiding this comment.
I agree with Igor, it's not like State maps 1:1 onto JSON types.
Would be good to record this somewhere.
| ## Solution | ||
| Regarding Smart contracts, I propose using JSON directly (1.), as it seems unlikely that we'd want to implement significantly broader capabilities for smart contracts in Solarkraft. | ||
|
|
||
| Regarding the Monitor Executor, I propose implementing direct name matching initially (1.1.), as it should be easy enough to implement (1.2.) in the future, should we have a need for it. |
There was a problem hiding this comment.
+1 for one-to-one name matching.
Co-authored-by: Igor Konnov <[email protected]>
There was a problem hiding this comment.
Thanks for the write-up, clear presentation so far!
Some things that I'm missing in the current exposition:
-
You introduce the Smart Contract Interface in the beginning, but it's not clear to me how interactions are passed between the Extractor and Executor.
-
Are there any pitfalls with
EXTENDing the monitor spec?
How would it look in practice?
I think it would help to take a toy example (e.g. one of the example contracts) and take it through the proposed steps here manually.
doc/ADR/ADR_001.md
Outdated
| 1. Resolving names: | ||
| 1. Require monitor names to match the names of the variables in smart contracts (and thus State) exactly | ||
| 2. Implement a _name binding_ standard, for example a simple CSV file, which tells the executor which State fields correspond to which TLA+ state variables | ||
| 2. Building TLA+: | ||
| 1. Creating `.tla`-format files (such as those output as intermediate values by Apalache) | ||
| 2. Creating `.json`-format TLA+ input (Apalache specific) |
There was a problem hiding this comment.
Renders as code block, please dedent.
| 2. Creating `.json`-format TLA+ input (Apalache specific) | ||
|
|
||
| ## Solution | ||
| Regarding Smart contracts, I propose using JSON directly (1.), as it seems unlikely that we'd want to implement significantly broader capabilities for smart contracts in Solarkraft. |
There was a problem hiding this comment.
I agree with Igor, it's not like State maps 1:1 onto JSON types.
Would be good to record this somewhere.
doc/ADR/ADR_001.md
Outdated
| [types]: https://developers.stellar.org/docs/learn/smart-contract-internals/types/custom-types | ||
| [RPC]: https://developers.stellar.org/network/soroban-rpc/methods | ||
| [RPCguide]: https://developers.stellar.org/docs/smart-contracts/guides/rpc | ||
| [gLE]: https://developers.stellar.org/docs/smart-contracts/guides/rpc/retrieve-contract-code-python |
Co-authored-by: Thomas Pani <[email protected]>
Adds initial design documentation.
Rendered doc