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. https://github.com/kframework/wasm-semantics/pull/193 https://github.com/kframework/wasm-semantics/pull/198 https://github.com/kframework/wasm-semantics/pull/202 https://github.com/kframework/wasm-semantics/pull/203
• @traiansf investigated the symbolic execution issues with KWasm overload operator, and implemented the initial unification modulo overloads in Haskell backend: https://github.com/kframework/kore/pull/882 https://github.com/kframework/kore/pull/908
• @ehildenb made an executable K specification of the set_free_balance function https://github.com/runtimeverification/polkadot-verification/pull/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 https://github.com/kframework/wasm-semantics/pull/204 https://github.com/runtimeverification/polkadot-verification/pull/18
• Discussions between many team members at RV about feasibility of proposed verification approach: https://github.com/runtimeverification/polkadot-verification/issues/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 https://github.com/runtimeverification/polkadot-verification/issues/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: https://github.com/runtimeverification/polkadot-verification/pull/22
• Parsing/passing more conformance tests: https://github.com/kframework/wasm-semantics/pull/208
• Explicit subsorts for Wasm tokens for Haskell backend (not allowed to have constructors in DomainValue sorts): https://github.com/kframework/wasm-semantics/pull/204
• Setup KWasm to allow hacky extensions for Polkadot to sidestep K unparsing issue
• Begin work on K unparsing issue: https://github.com/kframework/k/pull/764
• Get testing harness to run on random inputs, but crashes with coverage enabled: https://github.com/runtimeverification/polkadot-verification/pull/13
• Begin work on fusing axioms from semantics together to form summaries: https://github.com/kframework/kore/pull/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): https://github.com/kframework/k/issues/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. https://github.com/runtimeverification/polkadot-verification/issues/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 https://github.com/kframework/kore/pull/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: https://github.com/runtimeverification/polkadot-verification/issues/20

[ehildenb]

Thursday September 19, 2019

Done

• Fixed some sort bugs in KWasm causing Haskell backend to trip: https://github.com/kframework/wasm-semantics/pull/212
• Merged pyk execution harness for KWasm/polkadot: https://github.com/runtimeverification/polkadot-verification/pull/18
• Design doc for fusing multiple rules together in Kore is reviewed and merged: https://github.com/kframework/kore/pull/938
• Fusion of list of rules into one semantic predicate saying "these two rules apply in sequence": https://github.com/kframework/kore/pull/961
• Building KWasm in --coverage mode for generating rule traces: https://github.com/runtimeverification/polkadot-verification/pull/28
• More minor corrections to KWasm makefile: https://github.com/kframework/wasm-semantics/pull/217
• Proofs about memory setting/storing ironed out, semantics tuned: https://github.com/kframework/wasm-semantics/pull/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: https://github.com/runtimeverification/polkadot-verification/issues/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:https://github.com/runtimeverification/polkadot-verification/issues/35

[ehildenb]

Thursday September 26, 2019

Done

• Symbolic loop invariant proof finally fleshed out: kframework/wasm-semantics#220
• More supported conformance tests for KWasm: kframework/wasm-semantics#218
• Successfully running some small proofs on KWasm with Haskell backend: kframework/wasm-semantics#221
• Expose CLI for doing rule merging with Haskell backend: kframework/kore#983
• Extracting rule traces for feeding into Haskell backend: #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: kframework/k#804
• Using rule unique IDs instead of labels for merging rules with Haskell backend: kframework/kore#1016
• Structured representation of K attributes in JSON serialization: kframework/k#806
• Fixes to rule merger which makes sure variables in rules to be merged are disjoint: kframework/kore#1039
• Update pyk library to support full JSON serialization/deserialization: kframework/k#809
• Auto-unparsing based on JSON encoded definition: kframework/k#807
• Split at semantic level on non-deterministic memory growth: kframework/wasm-semantics#226
• Allow overriding memory constraints of Java backend: kframework/wasm-semantics#227
• Updated project roadmap issue: #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): #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: kframework/k#820

Done

• Better rule minimization in pyk library: kframework/k#811
• Auto unparsing using new features of pyk library: #40
• Don't crash on missing smtlib expressions: kframework/kore#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: https://github.com/runtimeverification/polkadot-verification/pull/44
• PR discussed: https://github.com/runtimeverification/polkadot-verification/issues/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.

[ehildenb]

Thursday October 31, 2019

Done

• Add simple WRC20 proof: kframework/wasm-semantics#235
• Fixes to rule merging variable renaming: kframework/kore#1159
• Add set_reserved_balance spec: #46
• Generate coverage lists from Makefile: #44
• Remove K-TERM hack from repo: #47

Discussion

• Have been profiling the rule merging, to find issues in the semantics where rule merging is not working very efficient. Updates to wasm semantics pending: kframework/wasm-semantics#243
• Potential skeleton for set_balance:

### `set_balance` 
    syntax Bool ::= ensureRoot ( AccountId ) [function] 
 // --------------------------------------------------- 
    rule    ensureRoot(_)      => false                                            [owise] 
    rule [[ ensureRoot(ACCTID) => true  ]] <adminAccounts> ADMINS </adminAccounts> requires ACCTID in ADMINS 

    syntax Action ::= "set_balance" "(" AccountId "," AccountId "," Int "," Int ")" 
 // ------------------------------------------------------------------------------- 
    rule <k> set_balance(ORIGIN, WHO, FREE_BALANCE', RESERVED_BALANCE') 
          => imbalance_event(FREE_BALANCE, FREE_BALANCE') 
          ~> set_free_balance(WHO, FREE_BALANCE') 
          ~> imbalance_event(RESERVED_BALANCE, RESERVED_BALANCE') 
          ~> set_reserved_balance(WHO, RESERVED_BALANCE') 
         ... 
         </k> 
         <account> 
           <accountID> WHO </accountID> 
           <balance> FREE_BALANCE | RESERVED_BALANCE </balance> 
           ... 
         </account> 
      requires ensureRoot(ORIGIN) 

    rule <k> R:Result => . ... </k> 

    syntax Event ::= PositiveImbalance ( Int ) | NegativeImbalance ( Int ) 
 // ---------------------------------------------------------------------- 

    syntax Action ::= imbalance_event ( Int , Int ) 
 // ----------------------------------------------- 
    rule <k> imbalance_event(ORIG, NEW) => . ... </k> 
      requires NEW ==Int ORIG 

    rule <k> imbalance_event(ORIG, NEW) => . ... </k> 
         <events> ... (.List => PositiveImbalance(NEW -Int ORIG)) </events> 
      requires NEW >Int ORIG 

    rule <k> imbalance_event(ORIG, NEW) => . ... </k> 
         <events> ... (.List => NegativeImbalance(NEW -Int ORIG)) </events> 
      requires NEW <Int ORIG 

• PositiveImbalance/NegativeImbalance aren't actually emitting events, just squaring up total balance. Need to add a totalBalance cell for that, and square it up on this rule application.
• We're throwing away the return value of set_free_balance and set_reserved_balance with the rule <k> R:Result => . ... </k>, which probably should be handled better with call frames. For this example we don't need it, since the return values aren't being used.

Rule merging, concetually

Looks something like this.

If we have the initial program: (i32.const 1) ~> (i32.const 2) ~> (i32.add) and the Wasm semantics contain the following rules

1: <k> (ITYPE.const X) => <ITYPE> X ... </k>
2: <k> <ITYPE> VAL => . ... </k>
   <valstack> ST => <ITYPE> VAL : ST </valstack>
3: <k> (ITYPE.add) => <ITYPE> #trunc(ITYPE, X + Y) </k>
   <valstack> <ITYPE> X: <ITYPE> Y : ST => ST </valstack>

then the rules will be applied in this order: 1 2 1 2 3 2

The rule merger takes pairs of rules and merges them into a single step. So rule 1 and 2 would merge to

1_2_merged: <k> (ITYPE.const X) => . ... </k>
                          <valstack> ST => <ITYPE> X : ST </valstack>

And the entire sequence would merge to

1_2_1_2_3_merged: <k> (ITYPE.const X) ~> (ITYPE.const Y) ~> (ITYPE.add) => . ... </k>
                                  <valstack> ST => <ITYPE> #trunc(ITYPE, X + Y) : ST </valstack>

In the end we end up with one or more descriptions of the entire execution along one path in the Wasm code. These descriptions then become a full generated specification of the program (in our case the program is set_balance). We then prove an inclusion between the hand-written specification and our generated specifications.

[ehildenb]

Tuesday November 06, 2019

• Rule merging with an initial configuration? This would help to make sure that certain map lookups don't fail (eg. map lookup from <curModIdx> to <modInst>, or from function name to function index). Virgil thinks it's possible to do, starting to look more like guided symbolic execution.
• Need to try out new batch merger. Virgil thinks batch-size 2 will make the best performance, but we'll test and see what happens. Maybe it makes sense to delay simplifications during normal symbolic execution too, if it turns out that many rules at a time makes sense.

[ehildenb]

Thursday November 07, 2019

Discussion

• Went over set_balance with @DemiMarie-parity yesterday, fixed up some K errors, discussed next steps in the high-level K specification.
• @ehildenb has a tight November 15 deadline coming up, will be mostly in a holding pattern on this project until then.

[ehildenb]

Tuesday November 19, 2019

Done

• More of high-level spec fleshed out from pair-programming sessions: #48
• Finish high-level specs of most of balances module: #51

Discussion

• Demi will begin working on making specs of the properties we'd like to prove over the high-level model.
• Everett will continue working on producing summaries of the generated Wasm, spinning up on the project again.
• For #54 added some tips about how to define how the EntryAction are defined.
• Added some potential proofs to do: #55 #56 #57
• Added some tasks for issues in the model discovered in discussion: #58 #59 #60

[ehildenb]

December 05, 2019

• Automated rule merging over simple conformance tests: #66
• Harness for writing specifications about the high-level model: #68
• Submitted issue to Haskell backend team regarding proofs using with-config functions: kframework/kore#1324

[ehildenb]

December 12, 2019

Pending Review

• Harness for writing specifications about the high-level model: #68
• Automated rule merging over simple conformance tests: #66
• Results from pair programming, updates to model: #69

In Progress

• Work on issue in Haskell backend writing proofs with contextual functions: kframework/kore#1324
• Upstreaming coverage calculation code for generating rule traces: kframework/k#971

Status Update

https://github.com/runtimeverification/polkadot-verification/issues/20#issuecomment-565129659

[ehildenb]

Thursday December 19, 2019

• Discussion with Web3 grants team, remaining deliverable on existing grant is to conformance test against other implementations for Balances module.
• More work on fixing the issue with proving specs over the high-level properties (improved Map matching), still not working fully though: https://github.com/kframework/kore/issues/1324
• Work to get Polkadot semantics repo to work on latest K/KWasm: #70 and kframework/wasm-semantics#272

[ehildenb]

Thursday January 9, 2020

• License file? Any updates on using NCSA license? Response: No updates, usually use GPL.
• What to do about 3rd milestone in first grant? It says "integrate" into Polkadot CI system, which I think is probably not what is wanted. Response: Will run by Peter, could integrate into Polkadot Spec repo.
• Look over next proposal draft and see what people think. Response: Looks good, will also bring up to Peter.
• Drop to one weekly meeting, because nearing end of engagement. Response: Will drop the Wednesday meeting.

[ehildenb]

Thursday January 16, 2020

• Clarify milestones? Including bullet point 3 here in milestone 2? https://github.com/runtimeverification/polkadot-verification/issues/42#issuecomment-537985241
• Functionality for bullet point 3 already exists in the repository, hasn't been tested against the set_free_balance module yet. Need to provide stubbed out RE API to do that (which I can do). Would it be enough to be able to provide traces + rule merging for the traces using the stubbed out RE API?
• Pair programming, work on less inane proof for high-level specification: #77

[ehildenb]

Thursday January 23, 2020

• Contract ironed out, have until Friday to change things. Looks fine to me.
• Still waiting on review for this one: https://github.com/runtimeverification/polkadot-verification/pull/77
• Been working on applying trace generator -> rule merger to generated Wasm source code, which led me to update the generated sources: https://github.com/runtimeverification/polkadot-verification/pull/81
• Regression found in K frontend affecting KWasm when trying to update to newest parser (to avoid using 42GB RAM), tracking issue here: kframework/k#1053
• CI integration dropped as a milestone. Should we still migrate repo to Web3 or Parity control? Or wait?
• Today, can keep attempting to prove something (on one of your machines), or can go over in more depth how the trace generation works, and rule merging.

[ehildenb]

Thursday February 6, 2020

• Update to K has finally been pushed through KWasm, which fixes a couple of issues with Search script stuff #85.
• Search script is ready for review and merge: #84. It does not work correctly yet, but is working enough to begin testing on CI. Will walk through how to run it, and the current issue it is having (getting stuck during execution in unexpected way, will take stepping through execution in debugger to figure out why).

[ehildenb]

Thursday March 19, 2020

• Went ahead and merged long-standing PR for initial search functionality: https://github.com/runtimeverification/polkadot-verification/pull/84
• Opened next PR which has working search functionality (by stubbing out PRE methods): https://github.com/runtimeverification/polkadot-verification/pull/88/files
• Updating the Wasm semantics version we are using is not working currently, but there is an update to KWasm that we want to take advantage of now: https://github.com/runtimeverification/polkadot-verification/pull/87. In the process of investigating what's going on.
• One potential issue has been filed with the Haskell backend (also affects KEVM), which may fix the slowdown issue we see: https://github.com/kframework/kore/issues/1686. Need to investigate more why the update to the submodules won't go through.

[ehildenb]

Thursday April 2, 2020

• Next PR which applies rule merging to actual execution traces is ready: https://github.com/runtimeverification/polkadot-verification/pull/91
• Investigating why long-running direct rule merge fails. Currently bisecting to get the first rule it fails at, but it takes a long time (at least a day) to run.
• Also investigating some performance optimizations to Wasm semantics which lead to sped up rule merging (eg. 40% speedup for merging the first 60 rules). This involves the #ContextLookup, which the specification and other implementations resolve ahead of time, but we resolve on the fly. We're going to try and resolve the identifiers ahead of time in KWasm to make it so that we have one less map lookup pr local/global/function/table/memory lookup in the Wasm semantics, which should make rule merging more successful in general.
• Want to make sure that next grant includes milestone 4 from this grant.

[ehildenb]

Thursday April 16, 2020

• Investigating this rule (which causes rule merging to blow up):

  rule <k> label [ TYPES ] { _ } VALSTACK' => . ... </k> 
       <valstack> VALSTACK => #take(lengthValTypes(TYPES), VALSTACK) ++ VALSTACK' </valstack> 
       <labelDepth> DEPTH => DEPTH -Int 1 </labelDepth> 

  I suspect that it's because the #take(...) ends up on the <valstack> cell unsimplified, so later rules need to use unify with that.

• Ran into bug in definedness condition for Haskell backend, so need to update the submodule to make sure it still exists on master. Submodule update hasn't gone through in a while, working through the issues there: https://github.com/runtimeverification/polkadot-verification/pull/90

• Simple update to Jenkinsfile for readability: https://github.com/runtimeverification/polkadot-verification/pull/93

• Cleaning up technical debt discovered while working with Ewasm semantics: https://github.com/kframework/wasm-semantics/pull/309

• Adding prover capabilities for working with memory: https://github.com/kframework/wasm-semantics/pull/310/

[ehildenb]

Thursday April 23, 2020

• #take and #drop made total: kframework/wasm-semantics#311
• Able to use KWASM-LEMMAS module for rule merging simplification: kframework/wasm-semantics#312
• More functions marked total as result of analyzing sequences of rule merges of length 5: kframework/wasm-semantics#316.
• Removing ByteMap sort to avoid the #set/#get unsoundness: kframework/wasm-semantics#321.
• Starting to get rid of #ContextLookup in the semantics by preprocessing the module.
• ReadyLayerOne: We can hold a workshop where we (i) show how to use this repo? (ii) go through some KWasm proofs? (iii) present what we're trying to do with this work here?

[hjorthjort]

Thursday May 07, 2020

• Working on getting rid identifiers through preprocessing. Have a mostly working draft for doing it for locals, but it means many rules and much boilerplate if we take that approach for eliminating all identifiers. So I'm working on a more general preprocessing function that should be easier to extend. PR here: https://github.com/kframework/wasm-semantics/pull/330.
• Working on getting rid of custom ByteMap sort in favor of Bytes sort that backend supports directly here: https://github.com/kframework/wasm-semantics/pull/321. This reduces the lemmas needed dramatically in favor of the backend doing specialized reasoning over the bytemaps.
• Have been working on updating Substrate dependency to get a correct list of host functions that need to be modeled for next engagement, but having problems figuring out how to make sure the entry-points we need are present in the generated code: https://github.com/runtimeverification/polkadot-verification/pull/100

[hjorthjort]

Thursday May 14, 2020

• text2core function working, removes #ContextLookups. PR in draft, only documentation and formatting remains. kframework/wasm-semantics#333
• Switch to Bytes type works, and last proof is now running to completion, but takes quite a long time to run and doesn't simplify fully. Working on getting the runtime down. kframework/wasm-semantics#321

[ehildenb]

Thursday May 21, 2020

• Removing identifiers for locals: kframework/wasm-semantics#333
• Make #wrap operate over byte-widths (simplification): kframework/wasm-semantics#336
• Cleanups to Wasm semantics: kframework/wasm-semantics#337 and kframework/wasm-semantics#339
• Some fixes to #getRange and #setRange and a 50% reduction in runtime of proofs: kframework/wasm-semantics#338

[ehildenb]

Thursday May 28, 2020

• Were able to re-enable substrate build by pinning rustup toolchain: #103, #104.
• Working on getting Substrate version updated to latest which still has set_free_balance: #100
• Then have KWasm update coming through, #98, followed by switch to Dockerhub images #99.
• Removing bytes type: kframework/wasm-semantics#347
• Preprocessing to get rid of #ContextLookup:
  • Desugar all func/table/memory/global definitions: https://github.com/kframework/wasm-semantics/pull/345
  • Sort definitions into respective types: https://github.com/kframework/wasm-semantics/pull/346
  • Next step is to collect the identifiers, so that they can be resolved in the instructions.

[ehildenb]

Thursday June 5, 2020

• Docker images PR ready: #99
• KWasm updates (unfolding definitions and sorting definitions): kframework/wasm-semantics#345 and kframework/wasm-semantics#349.
  • Draft for removing context lookup for functions (blocked): https://github.com/kframework/wasm-semantics/pull/353/file
• Updates to KWasm build system: kframework/wasm-semantics#350 and kframework/wasm-semantics#351
• Updated build instructions: #108
• Search rule merging profiler tool getting merged for easier profiling of bad rule merges: #109

[ehildenb]

Thursday June 11, 2020

• Rule merge profiler added to this repo: #109
• ContextLookup removed for functions: kframework/wasm-semantics#355
• Names removed from valtypes: kframework/wasm-semantics#356
• Module meta-data added to be able to call polkadot host functions: kframework/wasm-semantics#357
• Update to Polkadot KWasm dependency with changes due to removal of context lookup: #110
• Still debating what to do about failed rule merges due to overloaded rules: kframework/wasm-semantics#354
• Working on merging rules and adding them to the semantics, and metering if that gives a performance improvement.

[ehildenb]

Thursday June 18, 2020

• Sequence instructions in advance with a function: kframework/wasm-semantics#360

• Now there is one rule which causes problems with merging, this one:

  rule <k> block VECTYP:VecType   IS end => sequenceInstrs(IS) ~> label VECTYP { .Instrs } VALSTACK ... </k> 
       <valstack> VALSTACK => .ValStack </valstack> 
       <labelDepth> DEPTH => DEPTH +Int 1 </labelDepth> 

• Have a strange issue where the execution traces on CI server are very short (just run initialization push; push; call code), but locally they are giving full execution traces and the corresponding rule merges.

• Small updates to pyk library, search script, and pykWasm to make more graceful failure modes and better pretty printing of merged rules: #113, kframework/k#1342, and #114

• Remove the $PGM variable from the KWasm semantics, leave running up to the embedder. https://github.com/kframework/wasm-semantics/pull/362

  • Remaining issue: K relies on heuristics to determine a "main cell", but it shouldn't be necessary to have one imported in the proofs. https://github.com/kframework/k/issues/1347

[hjorthjort]

Thursday June 25, 2020

• Haskell backend team begun adding support for merging rules with the priority attribute: https://github.com/kframework/kore/pull/1898
• Might need some changes to how rules with priority attribute are encoded by the frontend: https://github.com/kframework/k/issues/1355

[hjorthjort]

Thursday July 2, 2020

• Update time for future meetings
• We suspect some failing merges may go away with newer K updates, byt the update deps job is failing. The error is located and reported: https://github.com/kframework/k/issues/1389
• Added _ to unused variables in Wasm https://github.com/kframework/wasm-semantics/pull/366
• Get rid of bad warnings https://github.com/kframework/k/issues/1384
• Ran Docker image locally, make test-search results in long traces.
  • Probable cause: CI is running make polkadot-runtime-sources but not make polkadot-runtime-loaded. Since search.py grabs the name from the .wat file but runs the .json file, the names don't match and the call fails.
  • Proposed solution: Reset the generated sources after the Polkadot build step.

[hjorthjort]

Thursday July 9, 2020

• Fixed issue with --coverage kompilation crashing when importing BYTES: https://github.com/kframework/k/pull/1394
• Removing #ContextLookup for types:
  • https://github.com/kframework/wasm-semantics/pull/367
  • https://github.com/kframework/wasm-semantics/pull/368
• Fixed the (percieved) inconsistency between local and CI runs, where the trace would only be a few steps long on CI https://github.com/runtimeverification/polkadot-verification/pull/117
• Next meeting:
  • Set up a make target for building the set-balance.md module with LLVM backend
  • Set up a make target for unit testing the set-balance.md module.
  • Add a set_account function to the Actions in set_balance.md: https://github.com/paritytech/substrate/blob/e824e8ab0fadec9949ebb8b9e14d98703d6b8d44/frame/balances/src/lib.rs#L494
  • Define the function and change the configuation as necessary
  • Mark the old set*balance as "depracated"

[hjorthjort]

Thursday July 16, 2020

• Removed half of #ContextLookup for types: https://github.com/kframework/wasm-semantics/pull/368

  • Other cases of #ContextLookup are not used in the generated Wasm.

• Remove #ContextLookup for labels, and desugar function bodies in pre-pass: https://github.com/kframework/wasm-semantics/pull/371

• Hypothesis on why update deps is failing: mismatch between which main module is used in kpol vs kwasm.

• Project status

  • Won't be able to work much on this for the next month or so. We've reached all the milestones in the agreement. Is there anything else we need to fix before moving on?
  • Update deps job.
  • Show that merged rules are actually being used.

• Pair programming:

  • Understanding K: non-determinism, owise rules, priority.
  • Adding new Actions
  • Running the spec as a concrete program, for testing.

Milestone 3 Generate the Wasm execution specifications of the bytecode: ● a. Generate execution traces of the Wasm code using the LLVM backend and a fuzzing frontend. This will produce sequences of rules in the order that they are executed, called BALANCES-MODULE-TRACE_i (subscripted by _i for the fact that there are many traces). ● B. Do common subsequence analysis on the BALANCES-MODULE-TRACE_i to find common subsequences of rules, and ask the Haskell backend to merge those rules together into rules which take larger steps. Several heuristics for rule merging will be provided, which select different subsequences to do merging with, and we can see which ones perform best. ● Compile the generated merged rules into the semantics with higher priority than the original rules, so that they can be used for both symbolic and concrete execution.

[hjorthjort]

Thursday 22 July, 2020

• Last week's pair programming we went over how to define things in K and run it concretely, with the goal of implementing the high-level spec of a function.
• Fixed update deps job: #115 The main issue was that search.py was putting the instructions to be executed on the <k> cell, instead of the new <instrs> cell. The kwasm-polkadot-host.md also contained instances of using the <k> cell instead of the <instrs> cell.
  • We decided to stop supporting a test, which was running the standard KWasm unit tests. Those require the KWasm test embedding to run, which we don't support. In the future, we can add a test like that back in, but using a local test specifically for exercising the rule merger, see #118 .
• Re-ran rule merge, added the merged rules to the kwasm-polkadot-host.md file, and built. Build works with slight massaging, but not for rules with #Ceil side condition.

[hjorthjort]

Thursday 30 July, 2020

• Have shown that merged rules get used in execution. #120
  • Not all rules get used when they are given the same priority -- some rules seem to be generalizations of the others. Experimenting with priorities to get all merged rules used.
• K updates on wasm-semantics: issues with the latest update, pushing to get the second to latest update through.
• Rikard is away for the next two weeks. Suggest we cancel the next 2 meetings.
• The actual Polkadot runtime still have relevant functions of the kind we like to work on. It can be downloaded here: https://github.com/paritytech/polkadot/releases/tag/v0.8.19. Relevant functions:
  • default_byte
  • from
  • metadata
  • deposit_into_existing
  • issue
  • transfer
  • extend_lock
  • remove_lock
  • set_lock
  • repatriate_reserved
  • reserve
  • slash_reserved
  • unreserve
  • call_functions
  • module_constants_metadata
  • post_mutation
  • storage_metadata
  • update_locks
  • Grep for this: $<pallet_balances::Module<T_I>_as_frame_support::traits::Currency<<T_as_frame_system::Trait>::AccountId>>::transfer::h959b05a069cec0be

[hjorthjort]

Thursday 20 August, 2020

• New proposal draft written
  • Roadmap towards a refinement proof
  • More focus on specifying and proving rather than implementing a bunch of host functions.
  • Would allow specifications to be written both for Rust functions that do a lot, as well as lower level ones, like post_mutation. The approach would be to give specifications of lower-level functions, instead of actually calling them, "coding by contract"-style
  • This diagram provides an overview of what we propose, and how it ties into the previous grant. https://docs.google.com/drawings/d/1pTWB5xVzgzKFL3dEpwFhQL7lW3smsdvzrRwLly-Tumc/edit?usp=sharing
• Question: where can we found the actual implementation of the deposit_event function here: https://github.com/paritytech/substrate/blob/f92a86a9506f331a867d36b0aa6b0bff3e462536/frame/balances/src/lib.rs#L612
  • Answer: https://github.com/paritytech/substrate/blob/f92a86a9506f331a867d36b0aa6b0bff3e462536/frame/system/src/lib.rs#L907 　https://github.com/paritytech/substrate/blob/f92a86a9506f331a867d36b0aa6b0bff3e462536/frame/system/src/lib.rs#L937

[hjorthjort]

Thursday 27 August, 2020

• Update deps: https://github.com/runtimeverification/polkadot-verification/pull/125
• @Lederstrumpf can we get an approval on this: https://github.com/runtimeverification/polkadot-verification/pull/122
• Validated the proposed method for doing refinement proofs internally, and it's viable. Will likely mostly be a frontend-tool that converts refinement claims to reachability claims.

[hjorthjort]

Internal meeting about project directions

Performance measurement of grant 1

Add performance measurement code to see the performance impact of merged rules.

• On Haskell backend krun:
  • add --bug-report flag to the --haskell-backend-command "kore-exec --bug-report" Generates the inputs for the Haskell backend, and necessary command, as a nice tar-ball.
  • Possible other option: add --dry-run flag. This generates all the required files (by calling the frontend) as well as giving the command that needs to be called on the command line.

Future directions

• The same kind of refinement proofs we do for Wasm, but for x86.
• The first refinement proof will be from Rust -> Wasm. It may be possible to instrument the LLVM compiler to insert synchronization points into generated Wasm code and x86 code (from the same LLVM IR), and then do a refinement proof from Wasm -> x86, giving a transitive refinement Rust -> Wasm -> x86. It may or may not be feasible.

[ehildenb]

Thursday September 3, 2020

• Try using the official Polkadot runtime, because it will not optimize away the symbols we need to call in the Wasm. We should be able to just get the Wasm files from the GitHub release, don't need to build ourselves (for speeeeeddd and simplicity).
• Get performance numbers for merged rules on Haskell backend.
• Get draft grant to them by tomorrow for them to review at their Monday meeting.

[hjorthjort]

Thursday September 10, 2020

• Grant draft sent. Comments?

Necessary

• Add total price
  • Ideally break up the price per deliverables
• Write a motivation section:
  • Vision -- what are we trying to build in the grand scheme of things?
  • Approach -- why are we starting here, with this?
• Clarify the choice of functions: they are somewhat arbitrary, specifically because we are interested in building the principle of refinement proving in K and with KWasm, not because they are the most interesting functions.
• Add a deliverable: Tutorials and UX Mark it optional. It is something we can discuss if we want or not at the end of the other 2 deliverables. In essence, whether it makes sense or not, as well as which the most important UX bottlenecks are, depends on the outcome of the first 2 deliverables. If the tool is automatic and fast enough, and we find that people working on Polkadot can effectively write specs with some training, it's a great idea to make a tutorial and some simple UX packaging to put the tool in the hands of more developers. It might, however, be the case that there is no obvious developer demand for the tool as is at the end of this research grant. If so, there is not much point in putting in time and money to develop a tutorial or UX packaging. Instead, it may be more sensible to implement the host API, build a simpler specification language, tune performance, or any number of other things.

[hjorthjort]

Thursday September 17, 2020

• Grant updated.
• Doing some preliminary work on refinement proving.
• Looking at profiling, seeing parsing bugs.

[hjorthjort]

Thursday December 10, 2020

• Change verification target for grant 2: SPREE modules
  • Specifically, the transfer module
  • Regular Rust/Wasm modules, same host functions as the Polkadot runtime
  • @Lederstrumpf will find a good target module.
• Cancelling the recurring meetings for the time being.
• Grant can probably move forward with the exact verification target blank.
  • First milestone would be deciding on what to verify, some function of similar scope to deposit_event
  • If extra details are needed, call a new meeting for that specifically.