Meeting notes

[hjorthjort]

2021-02-09

Completed

• CheckState
• Other minor semantic fixes
  • Correct finish and signalError for ending calls
  • Implement caching state before call
• Re-implement lottery contract -- it was succeeding in tests due to misplaced asserions in the Python code
  • Implement block timestamps.

Issues:

Memory problem

Semantics can't build, require too much time an memory. Likely due to configuration compostions.

Actions:

• [x] (Yi) Consult with Everett and Dwight in K channel
• [x] (Rikard) Take a look at why the current update of K into KWasm (upstream) is failing, that contains some memory improvements.
• [x] (Yi) Merge the configuration, remove the composition, see if it helps.

Discussion

What are next steps? What would be cool tools.

Everyone agree that symbolic execution, verification, and automatic test case generation would all be great. They are long-term, though.

Andrei suggested we should plug ElrondWasm into their regular CI when it's done, to test Arwen against the K semantics.

We could also make the Elrond semantics a more complete documentation document, like the jello paper.

Once we can generate a report for the Multisig contract we will give that to @virgil-serbanuta and other devs on the Elrond side for feedback and ideas on how it should become more useful.

Right now, the default approach is:

• Complete the tool, so that it can run all the Arwen tests.
• Create block-level coverage.

[hjorthjort]

2021-02-23

Done this week

• Yi: Fixed memory issue by adding priorities to all rules
• Fixing failing update. Failure was intermittent.
• Yi: Refactoring semantics into different files. PR open.
• Yi: Add a few multisig tests
• Merge lottery PR.

Discussion

Focus now: finish the semantics/clean up, be able to run basic tests, produce reports. Update the elrond-wasm-rs dependency.

Next step: investigate source mapping. What can we do, how well do existing source mapping tools work for our purposes.