Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Meeting Notes #19

Open
ehildenb opened this issue Sep 5, 2019 · 49 comments
Open

Meeting Notes #19

ehildenb opened this issue Sep 5, 2019 · 49 comments

Comments

@ehildenb
Copy link
Member

ehildenb commented Sep 5, 2019 •
edited
Loading

Unfortunately I didn't think to keep meeting notes from the previous meetings, but I'll do so here for upcoming meetings.
@ehildenb
Copy link
Member Author

ehildenb commented Sep 5, 2019 •
edited
Loading

Thursday September 5, 2019

Done

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 ehildenb mentioned this issue Sep 5, 2019
Closed
@ehildenb
Copy link
Member Author

ehildenb commented Sep 9, 2019

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
Copy link
Member Author

ehildenb commented Sep 11, 2019 •
edited
Loading

Thursday September 12, 2019

Done

Discussion

ToDo

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

@ehildenb
Copy link
Member Author

ehildenb commented Sep 13, 2019 •
edited
Loading

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
Copy link
Member Author

ehildenb commented Sep 13, 2019 •
edited
Loading

Thursday September 19, 2019

Done

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
Copy link
Member Author

ehildenb commented Sep 17, 2019 •
edited
Loading

Monday September 23, 2019

Discussion

@ehildenb
Copy link
Member Author

ehildenb commented Sep 24, 2019 •
edited
Loading

Thursday September 26, 2019

Done

Discussion

  • Updated milestones proposal.

@ehildenb
Copy link
Member Author

ehildenb commented Sep 30, 2019 •
edited
Loading

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
Copy link
Member Author

ehildenb commented Sep 30, 2019 •
edited
Loading

Thursday September 03, 2019

Done

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
Copy link
Member Author

ehildenb commented Oct 3, 2019

Monday October 07, 2019

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

@ehildenb
Copy link
Member Author

ehildenb commented Oct 3, 2019 •
edited
Loading

Thursday October 10, 2019

Might be done

Done

@ehildenb
Copy link
Member Author

ehildenb commented Oct 22, 2019 •
edited
Loading

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
Copy link
Member Author

ehildenb commented Oct 24, 2019 •
edited
Loading

Thursday October 24, 2019

Discussion

@ehildenb
Copy link
Member Author

ehildenb commented Oct 25, 2019 •
edited
Loading

Tuesday October 29, 2019

Discussion

@ehildenb
Copy link
Member Author

ehildenb commented Oct 25, 2019 •
edited by hjorthjort
Loading

Thursday October 31, 2019

Done

Discussion

### `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
Copy link
Member Author

ehildenb commented Nov 5, 2019 •
edited
Loading

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
Copy link
Member Author

ehildenb commented Nov 7, 2019

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
Copy link
Member Author

ehildenb commented Nov 15, 2019 •
edited
Loading

Tuesday November 19, 2019

Done

Discussion

@ehildenb
Copy link
Member Author

ehildenb commented Dec 5, 2019

December 05, 2019

@ehildenb
Copy link
Member Author

ehildenb commented Dec 12, 2019 •
edited
Loading

December 12, 2019

Pending Review

In Progress

Status Update

#20 (comment)

@ehildenb
Copy link
Member Author

ehildenb commented Dec 19, 2019 •
edited
Loading

Thursday December 19, 2019

@ehildenb
Copy link
Member Author

ehildenb commented Jan 9, 2020 •
edited
Loading

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
Copy link
Member Author

ehildenb commented Jan 16, 2020 •
edited
Loading

Thursday January 16, 2020

  • Clarify milestones? Including bullet point 3 here in milestone 2? Project Roadmap #42 (comment)
  • 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: Simple proofs about semantics #77

@ehildenb
Copy link
Member Author

ehildenb commented Jan 23, 2020 •
edited
Loading

Thursday January 23, 2020

  • Contract ironed out, have until Friday to change things. Looks fine to me.
  • Still waiting on review for this one: Simple proofs about semantics #77
  • Been working on applying trace generator -> rule merger to generated Wasm source code, which led me to update the generated sources: Source updates #81
  • Regression found in K frontend affecting KWasm when trying to update to newest parser (to avoid using 42GB RAM), tracking issue here: Regression in Frontend around FST serialization code for KWasm 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
Copy link
Member Author

ehildenb commented Feb 6, 2020

Thursday February 6, 2020

  • Update to K has finally been pushed through KWasm, which fixes a couple of issues with Search script stuff Update dependency: deps/wasm-semantics #85.
  • Search script is ready for review and merge: Search script - randomly test Polkadot sources #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
Copy link
Member Author

ehildenb commented Mar 19, 2020 •
edited
Loading

Thursday March 19, 2020

@ehildenb
Copy link
Member Author

ehildenb commented Apr 2, 2020 •
edited
Loading

Thursday April 2, 2020

  • Next PR which applies rule merging to actual execution traces is ready: Apply rule merging to search through executions #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
Copy link
Member Author

ehildenb commented Apr 16, 2020 •
edited by hjorthjort
Loading

Thursday April 16, 2020

@ehildenb
Copy link
Member Author

ehildenb commented Apr 16, 2020 •
edited
Loading

Thursday April 23, 2020

@hjorthjort
Copy link
Contributor

hjorthjort commented Apr 30, 2020 •
edited by ehildenb
Loading

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: Remove context lookup for locals wasm-semantics#330.
  • Working on getting rid of custom ByteMap sort in favor of Bytes sort that backend supports directly here: Remove ByteMap sort, use Bytes directly wasm-semantics#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: Update substrate version used #100

@hjorthjort
Copy link
Contributor

hjorthjort commented May 14, 2020 •
edited by ehildenb
Loading

Thursday May 14, 2020

@ehildenb
Copy link
Member Author

Thursday May 21, 2020

@ehildenb
Copy link
Member Author

ehildenb commented May 28, 2020 •
edited by hjorthjort
Loading

Thursday May 28, 2020

@ehildenb
Copy link
Member Author

ehildenb commented May 30, 2020 •
edited
Loading

Thursday June 5, 2020

@ehildenb
Copy link
Member Author

ehildenb commented Jun 10, 2020 •
edited by hjorthjort
Loading

Thursday June 11, 2020

@ehildenb
Copy link
Member Author

ehildenb commented Jun 14, 2020 •
edited by hjorthjort
Loading

Thursday June 18, 2020

  • Sequence instructions in advance with a function: Explicit instruction sequencing 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: Search updates #113, Updates to pyk library for processing rule merges k#1342, and Update merged rule output #114

  • Remove the $PGM variable from the KWasm semantics, leave running up to the embedder. Embedded Wasm wasm-semantics#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. Main cell issues k#1347

@hjorthjort
Copy link
Contributor

hjorthjort commented Jun 24, 2020 •
edited by ehildenb
Loading

Thursday June 25, 2020

@hjorthjort
Copy link
Contributor

hjorthjort commented Jun 30, 2020 •
edited
Loading

Thursday July 2, 2020

@hjorthjort
Copy link
Contributor

hjorthjort commented Jul 8, 2020 •
edited
Loading

Thursday July 9, 2020

@hjorthjort
Copy link
Contributor

hjorthjort commented Jul 15, 2020 •
edited
Loading

Thursday July 16, 2020

  • Removed half of #ContextLookup for types: Remove #ContextLookup for types when allocating functions wasm-semantics#368

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

  • Remove #ContextLookup for labels, and desugar function bodies in pre-pass: Unfold instructions, remove #ContextLookup for labels wasm-semantics#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
Copy link
Contributor

hjorthjort commented Jul 22, 2020 •
edited
Loading

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: Update dependency: deps/wasm-semantics #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 Make a rule merging test specifically for this repository #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
Copy link
Contributor

hjorthjort commented Jul 27, 2020 •
edited
Loading

Thursday 30 July, 2020

  • Have shown that merged rules get used in execution. Demonstrate that merged rules get used during 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

@FlorianFranzen FlorianFranzen mentioned this issue Aug 5, 2020
Open
@hjorthjort
Copy link
Contributor

hjorthjort commented Aug 19, 2020 •
edited
Loading

Thursday 20 August, 2020

@hjorthjort
Copy link
Contributor

Thursday 27 August, 2020

@hjorthjort
Copy link
Contributor

hjorthjort commented Aug 28, 2020 •
edited
Loading

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
Copy link
Member Author

ehildenb commented Sep 3, 2020 •
edited
Loading

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
Copy link
Contributor

hjorthjort commented Sep 10, 2020 •
edited
Loading

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
Copy link
Contributor

Thursday September 17, 2020

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

@hjorthjort
Copy link
Contributor

hjorthjort commented Dec 10, 2020 •
edited
Loading

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@hjorthjort @ehildenb