search

freespek / solarkraft

Solarkraft: a runtime monitoring tool for Soroban, powered by TLA+ and Apalache
Apache License 2.0
12 stars 0 forks source link

[Epic] M5: Input generation from runtime monitors #137

Open thpani opened 4 days ago

thpani commented 4 days ago

Extend Solarkraft to address the issue of test generation for Soroban smart contracts, similar to a "reverse" Solarkraft: instead of comparing fixed transaction inputs against a monitor specification, we use the monitor specification to generate test inputs.

Goal: Enable test generation of inputs against a fixed blockchain state, producing transaction inputs that make the contract invocation succeed or fail, respectively, according to user input. Stretch goal: Produce sequences of transactions.

Deliverables: Technical design doc, code and tests.

thpani commented 4 days ago

@konnov I made this as a starting point, feel free to spawn more detailed issues.