Meeting Notes

[ehildenb]

Unfortunately I didn't think to keep meeting notes from the previous meetings, but I'll do so here for upcoming meetings.

[ehildenb]

Thursday September 5, 2019

Done

• @hjorthjort categorized all the passing/failing conformance tests for us on KWasm, broken into passing, not-passing, and unparsable categories. Many tests become parsable with some minimal preprocessing. Conformance tests: Add make target, some semantics bug fixes  wasm-semantics#193 Build updates for quieter more reliable build wasm-semantics#198 Conformance tests tests: Add preprocessing wasm-semantics#202 Conformance tests: more preprocessing wasm-semantics#203
• @traiansf investigated the symbolic execution issues with KWasm overload operator, and implemented the initial unification modulo overloads in Haskell backend: Unification modulo overloaded constructors proposal haskell-backend#882 Implementing overloaded unification haskell-backend#908
• @ehildenb made an executable K specification of the set_free_balance function Executable spec - initial high-level K files describing desired behavior #15
• @ehildenb added pyk programmatic runner/initial state builder, updating several parts of KWasm build system and updating the way tokens are handled by the haskell backend Organization and adding token declarations wasm-semantics#204 Add environment module, initial unparsers/configuration builders for KWasm #18
• Discussions between many team members at RV about feasibility of proposed verification approach: Proposed Verification Approach #20

Discussion

• Shouldn't be focusing on fixing KWasm for things we aren't supporting (eg. Floating point), but the first bullet is more about actually getting a list, not about fixing them. We had a discussion internally and we decided that we will largely freeze KWasm until Polkadot project is over.
• What is a K cell? Long discussion about K, including going over syntax/rules, functional rules, configuration declaration/state, and structural framing (omitting cells that aren't relevant for a rule).
• Discussion about different backends, OCaml/LLVM make a concrete interpreter, Java/Haskell backends are for symbolic execution.
• Go over abstract specification, check whether it makes sense.
• Go over proposed verification approach, questions about "why this way?", answer is (1) scaling to larger scale codebases, and (2) maintainability.

ToDo

• Check whether the side condition 0 <Int RESERVED_BALANCE in account-reaped rule actually should be EXISTENTIAL_DEPOSIT <Int RESERVED_BALANCE.
• @hjorthjort ?
• @traiansf ?
• @ehildenb get execution traces from llvm backend for set_free_balance.
• @virgil-serbanuta implement feature in haskell backend to apply pre-specified sequence of rules.

[ehildenb]

Monday September 9, 2019

Discussion

• @virgil-serbanuta is working on making the Haskell backend be able to apply sequence of specified rules directly on some toy semantic examples.
• @traiansf is back from vacation, and will work on making sure that the few simple KWasm proofs we have work with his overload changes.
• @ehildenb is working on getting execution traces from the LLVM backend.
• We discussed how to check 4 in Proposed Verification Approach #20 (completeness of the generated specifications). It was decided that our initial check (\/ lhs(SEMANTIC_RULES)) -> (\/ lhs(GENERATED_SPECS)) won't work, because the semantic rules contain completely unrelated steps for our initial state (which is basically just (invoke 156). Instead, we want to check that the generated rules cover the entire input space of our initial state, something like <k> (invoke 156) ... </k> <valStack> X : Y : Z : .ValStack </valStack> == \/ lhs(GENERATED_SPECS).
• We also discussed how to fuzz more effectively. Just trying random input numbers over the input space may have a hard time getting all branches of execution, especially when some branches may only be exercised in certain specific regions of the input space. One possible suggested approach was to only take sub-traces of execution up to branching points (basically the br_if opcode), have the haskell backend summarize that sub-trace. The summary will contain the constraints added by executing up to that point, so we can then ask Z3 for a model of the constraints up to that point along with the branch condition being true/false. For now we agreed that we'll just do simple random sampling from the input space.

[ehildenb]

Thursday September 12, 2019

Done

• KWasm and Polkadot updated to newest K which no longer needs Rust: Update dependencies #22
• Parsing/passing more conformance tests: Increase java memory when running and parsing, pass more conformance tests wasm-semantics#208
• Explicit subsorts for Wasm tokens for Haskell backend (not allowed to have constructors in DomainValue sorts): Organization and adding token declarations wasm-semantics#204
• Setup KWasm to allow hacky extensions for Polkadot to sidestep K unparsing issue
• Begin work on K unparsing issue: Kast unparsing module defaults to languageParsingModule k#764
• Get testing harness to run on random inputs, but crashes with coverage enabled: Invoking k #13
• Begin work on fusing axioms from semantics together to form summaries: Design doc for combining axioms. haskell-backend#938
• Work on simple memory proofs (i32.load followed by i32.store to the same address leaves state unchanged) to figure out what lemmas will be needed for basic memory operations.
• Localize and report prover crashing bug, seemingly related to how we sequence statments (Java backend): Error while matching rule pattern (Java backend) k#766

Discussion

• Went over internal meeting notes.
• Build not working on Syed's machine.
• What is Z3?
• What can non-K experts do to get more familiar with the project? Working with programmatic interface is a bad choice, since it requires deeper understanding of the guts of K. Instead would be good to pick up tasks regarding high-level specification, since the K specs are short/relatively easy to write (eg. Make high-level specification of set_balance #26). I would start with this example from the tutorial for learning K: https://github.com/kframework/k/blob/master/k-distribution/tutorial/1_k/2_imp/lesson_5/imp.k

ToDo

• Isolate build/run issues with LLVM backend on random inputs.
• Implement prototype rule fusion.

[ehildenb]

Monday September 16, 2019

Discussion

• Waiting on fixes to K/llvm-backend --coverage option for ability to get rule traces: ###K PR### ###LLVM PR###
• @hjorthjort is working on store K (load K) => . proof, with PR ###HERE###. This requires lemmas over #setRange(...#range(...)...) => ... and #range(...#setRange(...)...) => ..., which are true in the "intended" model of KWasm, but the functions #range and #setRange are non-trivial. So we are increasing our trusted base size by including these lemmas.
• @virgil-serbanuta has written a rule-merger, and has tried it on some unit tests, but not on integration tests yet Combining a sequence of rules into one haskell-backend#961. Needs to still (1) make a command-line interface, (2) write some integration tests over K specifications, and then (3) actually try to simplify the resulting formula (either on the way or all at the end).
• We've reached milestone 1 of the engagement (agree on code to be verified), invoice incoming. Perhaps we need to discuss how to chop up milestone 2 now that we've ironed out the actual steps we'll be taking for the verification engagement: Proposed Verification Approach #20

[ehildenb]

Thursday September 19, 2019

Done

• Fixed some sort bugs in KWasm causing Haskell backend to trip: Fixed a sort bug wasm-semantics#212
• Merged pyk execution harness for KWasm/polkadot: Add environment module, initial unparsers/configuration builders for KWasm #18
• Design doc for fusing multiple rules together in Kore is reviewed and merged: Design doc for combining axioms. haskell-backend#938
• Fusion of list of rules into one semantic predicate saying "these two rules apply in sequence": Combining a sequence of rules into one haskell-backend#961
• Building KWasm in --coverage mode for generating rule traces: Enable building KWasm in --coverage mode #28
• More minor corrections to KWasm makefile: Correct parameter for setting MAIN_DEF_FILE wasm-semantics#217
• Proofs about memory setting/storing ironed out, semantics tuned: Proofs: locals and memory identity proofs wasm-semantics#214

Discussion

• Discuss milestone 1 a bit.
• Meetup at DevCon in person? Who is going? Hack session on this project?
• Fill in PR links for above notes.
• More K tutorial, explain how strict works, explain how environment/substitution based semantics work/differ.
• Go over PRs/rule fusion.

[ehildenb]

Monday September 23, 2019

Discussion

• Current rule merger goes on rule labels, but that can be too cumbersome for real semantics where many rules are not labelled. Instead it should use rule identifiers: Make Haskell backend rule merger use rule IDs instead of labels #34
• @virgil-serbanuta brought up an issue with an explosion in how many rules will be generated when trying to do rule-merging because we don't have information from the original program to tell us which branch of map unification to take (for example). Here we discuss how to fix this:Discussion about how rule merging should look #35

[ehildenb]

Thursday September 26, 2019

Done

• Symbolic loop invariant proof finally fleshed out: Make loops spec symbolic wasm-semantics#220
• More supported conformance tests for KWasm: New supported tests wasm-semantics#218
• Successfully running some small proofs on KWasm with Haskell backend: Simple arithmetic spec proven with Haskell backend wasm-semantics#221
• Expose CLI for doing rule merging with Haskell backend: CLI for merging rewrite rules. haskell-backend#983
• Extracting rule traces for feeding into Haskell backend: Extract rule traces from simple test-suite #32

Discussion

• Updated milestones proposal.

[ehildenb]

Monday September 30, 2019

• Rule merging not working how we expected. We made sure that both @hjorthjort and @virgil-serbanuta can build the polkadot semantics on their machines, and reproduce the rule merging issue. Then we discussed the issue, and @virgil-serbanuta agreed to investigate and come up with a fix.
• Topics to include in paper? We discussed a submission for some PL or FM conference, describing this new verification approach and how it should scale better than traditional verification. The story would be "prior work doing bytecode verification exists with KEVM, but now trying to scale to real-world programs (instead of just smart contracts) will require a more automated approach".

[ehildenb]

Thursday September 03, 2019

Done

• Always generate unique-id rule map: Always generate unique id map k#804
• Using rule unique IDs instead of labels for merging rules with Haskell backend: Switch to UNIQUE_ID as rule identifiers for merging. haskell-backend#1016
• Structured representation of K attributes in JSON serialization: Structured JSON serialized attributes k#806
• Fixes to rule merger which makes sure variables in rules to be merged are disjoint: Rename merge haskell-backend#1039
• Update pyk library to support full JSON serialization/deserialization: Remaining json serialization for pyk k#809
• Auto-unparsing based on JSON encoded definition: Automatically generate symbol table from JSON definition k#807
• Split at semantic level on non-deterministic memory growth: Split growth rule wasm-semantics#226
• Allow overriding memory constraints of Java backend: Pyk updates, kwasm allows overriding K_OPTS wasm-semantics#227
• Updated project roadmap issue: Project Roadmap #42

Discussion

• How much can we share with the "press"? We were contacted by Meghan Michel from Commonwealth Labs about this project, asking for information. It looks like she's gathering information from lots of the grantees.
• Who will take on writing high-level K specs from the Polkadot side? Should we have a separate weekly meeting where we do some pair programming to bootstrap this effort?
• Updated project roadmap, including updated milestones (converted to issue for ease of tracking/updating): Project Roadmap #42
• DevCon is next week, do async update?
• Concerns about coverage not being in current milestones (but optional). How can we either (i) get completeness covered, or (ii) have high assurance of completeness? (i) would be by proving that all possible inputs are covered, and (ii) could be done by more clever fuzzing via executing up to branches and then forcefully taking each branch point.

[ehildenb]

Monday October 07, 2019

• Discuss completeness proof, can Haskell backend provide support for it easily?

[ehildenb]

Thursday October 10, 2019

Might be done

• Fix for duplicate symbols being sent to Haskell backend by frontend: [BUGFIX]: Haskell backend rejects definitions which import K-TERM k#820

Done

• Better rule minimization in pyk library: Better rule minimization for pyk unparsing k#811
• Auto unparsing using new features of pyk library: Auto unparsing based on definition, limit coverage to semantic rules #40
• Don't crash on missing smtlib expressions: Identify orphan SMT constructors haskell-backend#1056

[ehildenb]

Tuesday October 22, 2019

Discussion

• Now scheduled weekly pair-programming meetings with Polkadot devs.
• Rikard and Everett discussed the algorithm for deciding when to merge rules, based on two backend specific parameters (i) how much is saved by merging rules, and (ii) how much is lost by failing to apply a merged rule.
• Still working on KWasm proofs for Haskell backend, should be able to complete the non-looping ones soon. Sum-to-n proof works? But takes a lot of time.
• Want to try a massive rule merge (just merge all the rules from one of the simple test-sets) and see what happens, if the backend crashes, etc...
• Everett will get all the local work diced up and sent in as PRs so others can work on rule merging stuffs.
• Maybe not targeting PLDI, deadline is pretty tight right now. Maybe a deadline around December/January makes more sense.
• Rikard will make a list (and issue) about changes needed to WRC20 needed to make the proof work.

[ehildenb]

Thursday October 24, 2019

Discussion

• PR discussed: Generate coverage lists directly with Makefile #44
• PR discussed: Rule merge silently failing #45
• Discussed local work on 3 rule merging strategies, showed what output looks like.
• Briefly looked at WRC20 spec from Rikard: https://github.com/kframework/wasm-semantics/pull/235/files
• What to go over next week in pair programming session? Start in on high-level specs, and then if time revisit KWasm proofs.

[ehildenb]

Tuesday October 29, 2019

Discussion

• Progress on fixing rule merging @virgil-serbanuta ? Done.