Meeting Notes

[ehildenb]

One meeting per comment, please.

[ehildenb]

Tuesday October 22, 2019

Discussion

• Project goals were discussed, and expected deliverables. An extra statement clarifying the concrete value added was added to the proposal, along the lines of "KWasm will be ready to use for commercial verification by RV and other companies".
• The blog posts will read as a series explaining KWasm verification, as well as the tuning process we go through for it. The first post will just be "Introducing KWasm and this series on verifying Wasm code using KWasm", and then each subsequent post will be one of the algorithms selected for verification. Ideally the sequence of blog posts will also serve as a KWasm verification primer for those looking to get into it themselves.
• Flying out to NYC once a month is too much from the RV side, would prefer lower frequency. Happy to give a formal verification talk/tutorial/workshop when we're out there though.
• Added one deliverable; jellopaper.org like documentation generation for the KWasm semantics.
• First code will be a WRC20 written by hand, and the accompanying blog post describing any verification challenges and what the resulting specification means.

[ehildenb]

Tuesday October 29, 2019

Done

• Parsing WRC20 spec correctly: Add parsing WRC20 spec to set of proofs #235
• List of issues with WRC20 parsing: List of issues with WRC20 spec #238
• Initial blog post draft: https://docs.google.com/document/d/1rGILYFDxPH8pKVpGft7v4NH4EWJqgYsstL267P9FISw/edit

Discussion

• Want blog post out by this week, will ping @pmackay1982 about that.
• Went over WRC20 spec, maybe we should provide a high-level description (or implementation in Rust) for readability for users? Right now it's just the Wasm code directly.
• Have the list of issues with writing the spec (List of issues with WRC20 spec #238). Should we "fix" the K parser to handle this directly, or provide a wrapper script? For now, let's do one more by hand to make sure we know all the issues and see if any other clever solutions come up.
• Next tasks are breaking the verification tasks up and getting them assigned.

[ehildenb]

Tuesday November 05, 2019

Discussion

• Blog post rough draft is ready for review (thanks for the patience, it's gone through a few rounds of internal revision): https://docs.google.com/document/d/1rGILYFDxPH8pKVpGft7v4NH4EWJqgYsstL267P9FISw/edit. dLab folks will send instructions in MatterMost for how to submit the blog post and provide/get feedback.
• Factored out WRC20 code from spec as much as possible, which alleviated some parsing issues: Add syntax Stmts ::= "WRC20" [function] #241. Went through this a bit.
• Discussed how proofs in KWasm look, showed simple-arithmetic-spec.k and loops-spec.k, and how to see what commands to use to run them. make --dry-run test-prove prints out all the commands needed to run the proofs (after building the repo).

[sskeirik]

Tuesday November 12, 2019

Done

• A spec for $i64.reverse_bytes. Still to be proven.
• 27 lemmas/axioms added about modular arithmetic (which will be useful for other KWasm proofs).

Discussion

• Blog post published
• Potentially change meeting time for Rikard in Sweden
• Fellows meeting presentation details
• Details about reverse-bytes function proof and modular arithmetic

[hjorthjort]

Tuesday November 19, 2019

Done

• The Java backend now verifies the $i64.reverse_bytes spec: Reverse bytes spec #257.
  • 31 general lemmas added, most of them trivial or hand-proven.
  • 13 lemmas specific to this proof, 7 which should easily generalize to other proofs over memory.
  • Issue filed because Haskell backend cannot yet verify i64.reverse_bytes (KWASM: wrc20-spec.k haskell-backend#1269).
• The Haskell backend now better understands bytes as builtins, which can improve performance for derived interpreters that use bytes/byte arrays (in future, can consider migrating byte representation, if we want).
• The Haskell backend is now able to verify several simple KWasm specifications about:
  • local variables
  • loops
  • concrete and abstract memory accesses
  • simple arithmetic

In Progress

• The lemma used for $i64.reverse_bytes still need further checking and possibly generalization. Thus, the PR for $i64.reverse_bytes is still in draft state.
• Gearing up for second monthly blog post (but see point below).

Discussion

• Potentially change meeting time for Rikard in Sweden.
• Adjust monthly goals:
  1. The complexity involved in verifying KWasm functions that touch the memory was greater than This month's blog post will be a deep dive into verifying $i64.reverse_bytes; the various subtleties involved in reasoning about KWasm, e.g., modular arithmetic, data representation; and what kinds of lemmas are needed in order to verify the function.
  2. Next month we will push for a full verification of WRC20 and an associated blog post; by that time, Stephen will have more experience with the tools and will be able to contribute more actively.

[sskeirik]

Tuesday December 10, 2019

Done

• The two forthcoming blog posts are now in medium draft mode.
• First blog has already received extensive comments and will be ready modulo formatting.
• Gained substantial experience with collaborative editing workflow for Medium (unfortunately, Medium has no built-in serious collaboration features).

In Progress

• Review/formatting of second blog post.
• The next phase of WRC20 verification (after reverseBytes) is the do_balance function.

Discussion

[hjorthjort]

Tuesday December 17, 2019

Done

In Progress

• $do_balance spec. Stuck on Map lookups, investigating whether it's a bug/missing functionality in K, or some other issue.
• Bypassing all the map lookup steps and doing the proof from the start of the function, to make progress on the actual verification.

Discussion

• Discussed state of $do_balance based on your comments.
• Discussed plans to release first reverse_bytes blogpost this week and then the next reverse_bytes blogpost next week. The ball is in their court for this one.
• Walked through the slides with them for Thursday and got excellent comments.

[hjorthjort]

Tuesday January 7, 2020

• January will be a hiatus month: Stephen just finished his thesis and won't be working in January (back in February), and Rikard is working on finishing his thesis so no one will be able to work full time on the verification this month.
• The reverse-bytes spec is not working on the Haskell backend, looking into getting that to pass.
  • We think it may make for an interesting blog post to describe how we extend the Haskell backend to work for a spec that is sound in matching logic but is currently not supported.
• Status of blog posts
• Status of Fellows presentation next Tuesday

[sskeirik]

Tuesday February 11, 2020

Discussion

• Weekly townhall meetings were cancelled --- because RV is the only current participant; dlab is delaying next cohort and instead doing a lighter weight INCUBATE program that will be administered almost totally remotely
• Previous target $do_balance was trickier than anticipated because it involves the semantics of not just Wasm but also the Wasm embedder (in this case, EVM)
• Decide on next target. Some possibilities:
  • Continuing work on $do_balance
  • Extending Ewasm semantics to the full Ethereum platform, i.e. an Ethereum semantics with all smart contracts code in Wasm format instead of EVM bytecode --- and verify a very simple contract invocation

In Progress

• Goal for next week is to invoke a simple empty contract and prove that the state doesn't change as a way to get my feet wet
• Goal for coming month --- so roughly 4 weeks from now on March 10th-12th --- is to finish verification of $do_balance function and write up a blog post

[sskeirik]

Tuesday February 18, 2020

Discussion

• Proved that executing the empty program in the extended Ethereum semantics does not meaningfully change state

In Progress

• Work on K toolchain tutorial
• Next plan to invoke an empty contract and prove that the state doesn't change as a way to get my feet wet
• Discuss with Everett/Rikard and sketch out collaboratively a more concrete plan/goal for this month's deliverable; see previous meeting note for original goal for this month.
  • make sure that needed support is available
  • see if we can pick a goal that either has an adjustable scope in case of unforeseen difficulty or that we are confident can be handled
  • notify dlab when new plans are made

[sskeirik]

Tuesday February 25, 2020

Discussion

• (Postponed until next time?) Do a simple K toolchain tutorial
• Describe a bug fixed in the Wasm semantics
• Discuss current revised monthly target --- to verify a basic contract invocation and write an introductory blogpost

In Progress

• Verify a simple contract invocation
• Write blog post introducing how EWasm works and describing how to verify a simple contract invocation

[hjorthjort]

Thursday, March 19, 2020

Done

• Proof on the Haskell backend that we can invoke a contract
• $do_balance proof on Haskell backend
• reverse_bytes proof on Haskell backend
• Final blogpost: Ewasm and the $do_balance proof