Workflow change

[virgil-serbanuta]

Current workflow with examples:

1. Write the main Rust contract that should be published on the blockchain ( https://github.com/multiversx/mx-sdk-rs/tree/420368c7387e368405c0c8a2f3c202885185352c/contracts/examples/adder )
2. Write a Rust contract that tests the main Rust contract ( https://github.com/runtimeverification/mx-semantics/tree/master/tests/contracts/foundrylike )
3. In the test contract, add a foundry.json file pointing to the main contract ( https://github.com/runtimeverification/mx-semantics/blob/master/tests/contracts/foundrylike/foundry.json )
4. Compile the test contracts ( https://github.com/runtimeverification/mx-semantics/blob/master/generate-claims.sh#L11-L12 )
5. Fuzz the contract ( poetry -C kmultiversx run -- kasmer --directory "tests/contracts/foundrylike" )
6. Generate the claims ( https://github.com/runtimeverification/mx-semantics/blob/master/generate-claims.sh#L15 )
7. Verify the test contract ( poetry run python3 -m src.kmxwasm.property --claim $CLAIM --kcfg=$KCFG --booster )

This workflow also needs various things to be kompiled and poetry install commands.

Desired workflow:

1. Write the main Rust contract.
2. Write the test Rust contract.
3. Build the test contracts and link them together (the user should be able to also do this by hand if needed; this should also generate the foundry.json file, which should actually be named kasmer.json or something similar): kasmer build --main=deps/mx-sdk-rs/contracts/examples/adder --test=tests/contracts/foundrylike
4. Fuzz the contract: kasmer fuzz tests/contracts/foundrylike
5. Verify the contract: kasmer verify tests/contracts/foundrylike

The desired workflow could also look something like this (we're skipping the foundry.json file):

1. Write the main Rust contract.
2. Write the test Rust contract.
3. Build the test contracts: kasmer build --main=deps/mx-sdk-rs/contracts/examples/adder --test=tests/contracts/foundrylike
4. Fuzz the contract: kasmer fuzz --main=deps/mx-sdk-rs/contracts/examples/adder --test=tests/contracts/foundrylike
5. Verify the contract: kasmer verify --main=deps/mx-sdk-rs/contracts/examples/adder --test=tests/contracts/foundrylike

I'm not that good with user experience, so the following may or may not be a good idea. The verify command should allow users to debug:

1. Restart the proof if it was stopped in the middle (perhaps restart only on a specific branch) (verify --restart and verify --restart <N>)
2. Inspect the current state of the proof (execution tree, specific nodes) (verify --tree and verify --show-node <n>).
3. Remove nodes from the execution tree (verify --remove <n>).
4. Run with a different step, perhaps for a limited number of iterations (verify --step <m> --iterations <n>).
5. Use a different place for saving intermediate results (verify --job-name=<name>)

[tothtamas28]

How about:

• Add kasmer.json to the test contract root
  • The location of the file defines the test contract path
  • The contents of the file define the main contract path
• kasmerx [-C TEST-PATH] {build|prove|fuzz}

[tothtamas28]

I started implementing kasmerx build: #126

It assumes a file kasmerx.json in the test contract root, e.g. in mx-semantics/tests/contracts/foundrylike/kasmerx.json:

{
  "contract_path": "../../../deps/mx-sdk-rs/contracts/examples/adder"
}

Based on this information, the test and main contracts can be compiled with sc-meta. The next step I guess is to run kasmer --gen-claims.

@virgil-serbanuta, does this make sense so far?

[virgil-serbanuta]

Yes.

[bbyalcinkaya]

I think it might be better if it accepts multiple contracts, so instead of contract_path, it should be contract_paths. The test might require interaction between multiple contracts.

{
  "contract_paths": [
    "../../../deps/mx-sdk-rs/contracts/examples/adder"
  ]
}