Meeting Notes - Githubissues

makerdao / mkr-mcd-spec

High level KSpecification for the MCD System by Runtime Verification and Maker Foundation

GNU General Public License v3.0

28 stars 9 forks source link

Meeting Notes #22

Open ehildenb opened 4 years ago

ehildenb commented 4 years ago

Unfortunately we didn't take meeting notes from the beginning, but hopefully this helps the project owners on the MKR side report progress.

ehildenb commented 4 years ago

Tuesday September 03, 2019

Done

Harness for turning calls in sneak-tx-tracking.
Merge initial semantics of Jug.
Generate Sphinx "Read the Docs" documentation of KMCD.
Reworked definition to match modular structure of (https://github.com/makerdao/developerguides/blob/master/mcd/mcd-101/mcd-101.md#smart-contract-modules).

Discussion

Maybe following the diagram (https://github.com/makerdao/developerguides/blob/master/mcd/mcd-101/mcd-101.md#smart-contract-modules) doesn't make as much sense, since it may not be accurate. This one is more accurate, but perhaps too granular: https://www.notion.so/MCD-System-c4df43ded9aa47f7b3770cb7ea6a79e7. Also, need to consider where something like end.sol will be modelled, which "changes the game" by changing which types of interactions are allowed in the actual data modules.
Maybe dai.k actually should be rolled into collateral.k. But dai does have mint and burn which makes it behave slightly differently than other collateral.
OK with format of Read the Docs format, can we auto-publish it somewhere? Maybe even a github.io page initially?
Commit stripped down version of results.json to repository, don't worry too much about obfuscating the data. Update it occasionally.

ToDo

Mariano will try wrapped-eth/eth first, and maybe move onto dai if it's not done by then.
Everett will figure out build issues with moving onto modular structure.
Setup an actual testing harness instead of just printing what it would test.
GitHub pages automatic publishing of the documentation.

ehildenb commented 4 years ago

Tuesday September 10, 2019

Done

GitHub pages setup, need to improve styling and setup automatic releases to it: https://runtimeverification.github.io/mkr-mcd-spec/
Finished stubbing out remaining semantics, to have indication of remaining TODOs: https://github.com/runtimeverification/mkr-mcd-spec/pull/21. Need to wait on PRs into K.
Fixed some bugs in configuration composition in K, which were blocking the modular specification of MCD: https://github.com/kframework/k/pull/741
Found and (nearly) fixed some bugs in printing out configurations uncovered by this repository: https://github.com/kframework/k/pull/757
Implemented semantics for spot. Currently blocked on the PR for stubs above.
More of the semantics of Dai, also blocked on refactoring for stubs.

Discussion

Changes to the auction to add dump risk parameter, and automated increase in value of auction at tick intervals.
Behind schedule on semantics, more time will be diverted for this project.

ToDo

Move from manual publishing to GitHub pages to automated publishing.
Finish testing harness setup.
Get stubs PR merged.
Get dai-semantics merged.

ehildenb commented 4 years ago

Thursday September 12, 2019

Discussion

Deciding how to allocate resources on project to finish in more timely manner.
Daejun and Dwight can make some time available, but certainly not full time or planning work.
Musab may be a choice for project management.
Everett would like to scale back to 1 day/week at most, can do the management work, hard to lead 3 projects at once.
Dwight can do 1-2 days a weeks, guided dev work and architectural decisions.
Daejun can do 1 day a week, guided dev work.
Guy can do 2-3 days a week, guided dev work.
Tasks assigned for the next week, need to investigate the authorization/state-roll back functionality and decide if a coarse model (global state rollback) or fine model (each step does it's own state rollback) is needed.
Decided we will probably need rational numbers for storing values, which can be upstreamed into K proper. This will be handled by @daejunpark.

ehildenb commented 4 years ago

Tuesday September 17, 2019

Done

stubs PR merged, refactored semantics builds and passes tests: https://github.com/runtimeverification/mkr-mcd-spec/pull/21
Automatic publishing of GitHub pages: https://github.com/runtimeverification/mkr-mcd-spec/pull/26
Initial semantics of Dai ERC20-ish fungible token merged: https://github.com/runtimeverification/mkr-mcd-spec/pull/20
Named productions projections merged into K for prettier records: https://github.com/kframework/k/pull/774
Semantics of Spot merged: https://github.com/runtimeverification/mkr-mcd-spec/pull/27
Fixes to K scanner/parser: https://github.com/kframework/k/pull/780 https://github.com/kframework/k/pull/787
rat.k merged into K, semantics switched over to it: https://github.com/kframework/k/pull/779
Flip semantics: https://github.com/runtimeverification/mkr-mcd-spec/pull/39

Discussion

Code question: https://github.com/runtimeverification/mkr-mcd-spec/issues/36#issuecomment-532363912
Conventions which are being used in new control flow refactoring PRs (re: auth, init, how call works vs. transact, etc...)
Modelling external tokens directly, or just have a generic gem interface. Do we need to model dai token directly for example? We aren't planning on modelling MKR token directly, for example, just with a generic gem.
"Is there any reason for modelling MKR other than as a generic <gem>? Outside from mint/burn, we probably don't need to."
Not hard to have generic gems which contain their own behaviors as data. So we can have gems which have mint/burn and ones that don't. Perhaps we want to keep gems which are used as collateral separate from those that aren't? eg. MKR and Dai are just gems interface-wise, but they have special connotations in the system.

ToDo

Gem semantics
Flap semantics: https://github.com/runtimeverification/mkr-mcd-spec/pull/37
Flop semantics: https://github.com/runtimeverification/mkr-mcd-spec/pull/46
WETH semantics: https://github.com/runtimeverification/mkr-mcd-spec/pull/44
Vat refactor for direct translation: https://github.com/runtimeverification/mkr-mcd-spec/pull/48
Control flow refactoring: https://github.com/runtimeverification/mkr-mcd-spec/pull/49

ehildenb commented 4 years ago

Thursday September 19, 2019

Discussion

Going to try implementing type synonyms in K for Rat which mark the needed precision of each. Hopefully this helps with being able to do refinement proofs "up to epsilon" of the solidity implementation.
Made a new column https://github.com/runtimeverification/mkr-mcd-spec/projects/1#column-6553063 which are "checks" that we should do before asking for reviews on each PR, and which will be discharge independently after reaching Milestone 2 of the engagement.
Added a card for semantics of Cat, which can be picked up next after Gem/Flap/Flop.
Decided that gems will be identified by their semantic names (eg. "MKR", "DAI", and "WETH"), rather than contract address, and contract address will be a data field. This will make it more apparent which gems are being manipulated by the contracts inside MCD.
How can be build more excitement around this model from the MKR side? Potentially we can start working on the future directions part, eg. (i) generating documentation, (ii) statistical model checking, or (iii) fuzzing/test generation for the Solidity code.

ehildenb commented 4 years ago

Tuesday September 24, 2019

Might Be Done

Done

Vat refactor for direct translation: #48
Control flow refactoring: #49
Gem semantics: #52
_^Rat_ for use in #pow, refinements of use of Rat in K: kframework/k#785
Switch to more precise names for all Rat operators describing precision needed: #58
Use String type for bytes32 in Solidity: #60
Flap/Flop semantics: #56

Discussion

Approaching milestone 2 with the above merged and end.sol implementation.

Develop the K specification of the high-level behaviors of the MCD corecontracts. This will describe entry/exit points of the contracts, and overall state-updates that eachoperation in the system should have.

To claim victory, we need to (i) implement the note modifier, and (ii) implement the specific GemJoin contracts found in: https://github.com/makerdao/dss-deploy/blob/master/src/join.sol, (iii) implement vow.sol, and (iv) implement end.sol.
From internal meeting:

How can be build more excitement around this model from the MKR side? Potentially we can start working on the future directions part, eg. (i) generating documentation, (ii) statistical model checking, or (iii) fuzzing/test generation for the Solidity code.
- Would be cool to be at the point where we add components to the model and check "does it do what we intend?" (sounds like a vote for (ii)).
- (ii) allows confidence in new features, (iii) allows confidence in implementation matching the intended features.
- Gut priorities are (ii) -> (iii) -> (i).
- Will describe/propose these options more clearly, they'll discuss internally, then we'll have a call to clarify any remaining issues/questions.

ehildenb commented 4 years ago

Thursday September 26, 2019

Discussion

Can interest rates be negative for pot? https://github.com/runtimeverification/mkr-mcd-spec/pull/57#discussion_r327856613
We need to begin testing the semantics to have confidence in it.
Tasks added for modelling emitted events, both note events and contract-specific events.
Implementing the specific gem-joins seems somewhat out of scope for the project: https://github.com/runtimeverification/mkr-mcd-spec/issues/63

ehildenb commented 4 years ago

Tuesday October 1, 2019

Done

Semantics of Pot: #57
Semantics of Joiners: #61
Semantics of Vow: #66
Semantics of end.sol: #69
Separate semantics of each contract into its own file: #71
Semantics of Cat: #72
Proposed extensions/uses of the semantics: #64

Discussion

Conformance testing needs to happen before extensions/uses of the semantics are made.
Current understanding is that DSR is intended to be greater than 1, but that it may be in the future less than 1. What is currently enforcing this condition is that sub reverts on underflow on this line: https://github.com/makerdao/dss/blob/master/src/pot.sol#L139. Maybe a clearer way to do it is to assert that file doesn't set it too low or something: https://github.com/makerdao/dss/blob/master/src/pot.sol#L122
The reason to include #63 in the model is to ensure robustness of internal accounting, eg. "all gems tracked in the system can be removed". Because those gem-join are storing actual collateral, they are an important attack surface to model. Moving forward, it would be great to be able to say "this token complies enough with expected behavior to not throw the system out of balance". Let's leave this out for this milestone and revisit once we get testing/fuzzing in place.
This next week is going to be on modeling the notes/events. Following this week (and DevCon), we will begin conformance testing and light fuzzing. After that is completed, we can look more closely at what it takes to do full-blown statistical model checking and whether it will fit in the current engagement.

ehildenb commented 4 years ago

Thursday October 03, 2019

Discussion

Scope of project moving forward? See discussion above, refer to initial engagement scope. Also refer to issue #64. Should we replace the remaining milestones (after 2) with ones regarding statistical model checking?

ehildenb commented 4 years ago

Tuesday October 08, 2019

Done

note modifier log events are emitted now: #75
Method/contract specific log events emitted: #76
Add test data and initial test-extraction code: #73

Discussion

Milestone 2 reached.
Future extensions, trying to come up with some estimate of what doing (i) conformance testing, (ii) fuzzing, and (iii) statistical model checking would look like. Rough estimate is 4-5 weeks for conformance testing (i). Then for (ii) we need to (a) come up with allowed methods to be called by external users, (b) generate "likely" workflows of method calls that are reasonable (with the goal of not generating un-interesting "reverting" calls), and (c) generate fragments of those workflows with random input data to run the model on (and the Solidity code? which would probably be an extra milestone). Estimate of (iii) would be pending more discussion with Musab.

ehildenb commented 4 years ago

Thursday October 10, 2019

Discussion

Some help with the K specs of UrnHandler deployment (will send example of contract deployment verification done for Eth 2.0 deposit contract).
MKR MCD launch is 5 weeks out. Last chance to abort launch is November 15, ideally any issues are found before (November 5th). Need to accelerate random testing approach to start the computers running by November 1st ideally.
Much of the original anticipated value was in being able to test new features rolled out to MCD system, but MKR is more interested in finding bugs pre-launch.
To have assurance that random testing is working, we can break the model in the same ways that the original implementation was found to be broken (from the bug bounty program), and see if our statement of properties about the system actually catches "bad" execution traces.
Concrete steps that need to be taken:
- Setup testing harness on existing data provided by MKR.
- Write down macro-variables of system which we are interested in stating properties about (measurable quantities about system). Example of this would be "sum of the urn balances", where "urn balance" is the scaled urn collateral minus the scaled urn debt.
- State properties of these macro variables which we hope to be true, and translate those properties into checks over execution traces in the testing harness.
- Start the random random tester running on the current system, see if it finds any property violations.
- Break the system with the bugs already found in bounty program, and start random tester on that system. Spend remainder of time tuning the tester to find the existing bugs, and any improvements get applied back to tester running on corrected system. Tuning here will mean two things, either (i) better selection of transaction sequences to try, or (ii) more properties to select for.

ehildenb commented 4 years ago

Tuesday October 22, 2019

Meetings interrupted by DevCon, should be back on track.

Done

Simplify state roll back mechanisms: #79
Add file methods for setting up tests: #80

Discussion

Is it the case that the authentication scheme proposed by #81 is correct? That is, is it the case that all MCD contracts are warding each other in a real world deployment? No, we probably want auth at the call boundary, not at the transact boundary, so that we can model "accidental" updates which end up introducing calls to the wrong internal contracts down the line.
Go over lucash-pot-end example.

ehildenb commented 4 years ago

Thursday October 24, 2019

Discussion

@malturki will be helping to (i) finish out the remaining bug bounty test cases, and (ii) setup the random testing harness.
Went over random testing harness (still work just local on @ehildenb machine), but @malturki had some ideas about how to improve.
Went over lucash-pot-end example.
Adapted authorization scheme given feedback from last meeting.

ehildenb commented 4 years ago

Tuesday October 29, 2019

Done

ward/authentication scheme implemented: #81
Test for lucash-pot-end: #82

Discussion

Assign next bugs. @malturki has agreed to take lucash-pot, @ehildenb can take lucash-flip-end. That leaves lucash-flap-end.
Go in-depth review into lucash-flap-end and lucash-flip-end attacks, flesh out skeleton of how they work.

ehildenb commented 4 years ago

Thursday October 31, 2019

Discussion

Not much time to go over lucash-pot yet for @malturki. Has been reviewing the KMCD spec so far.
Went over wards authentication scheme with @malturki, caught two bugs, MCStep typo and *-live on rely and deny.
Allocated flip-end bug to @gtrepta .

ehildenb commented 4 years ago

Tuesday November 05, 2019

Might Be Done

lucash-pot bug: #89

Discussion

Jug . drip is in charge of rate-accumulation so that people are charged stability fees. Pot . drip is for users to accumulate interest on their held Dai. Governance is in charge of periodically calling Jug . drip, but a user may be able to implement the Pot . drip attack between calls of Jug . drip if the calls are not frequent enough.

Pot . drip Jug . drip Vat . frob -> Pot . join -> (delayed as much as possible, but not past the next Jug . drip) Pot . drip -> Pot . exit -> Vat . frob Jug . drip

It's important that the Vat . frob happens on either side so that the dai used to make the attack is not charged the stability fee.

ehildenb commented 4 years ago

Thursday November 7, 2019

Fastest path to guided random tester?

ehildenb commented 4 years ago

Tuesday November 12, 2019

Might Be Done

Refactoring property checker: #104
Small updates to model: #105

Done

flap-end bug: #86
flip-end bug: #85
pot bug: #83
More documentation on how to run attacks: #88
Log TimeStep events: #95
Common attack prelude: #97
Factor out common prelude into K module: #98
Log Exception events too: #99
Update K dependency, fix some small bugs: #101, #102
Property checker of event log: #100

Discussion

Next milestone achieved (reproduce existing bug bounty bugs).
Is the random tester working yet? Almost to the point where we have support for the four attacks being found by random testing, need to get it merged.
Likely won't have meaningful results by launch at this point. Continue work on this project? @ehildenb still thinks it can be valuable, up to MKR. Looks like we will continue to work on the project.
Upgrade path planned? No upgrade path in place yet, MKR team will work post-launch on upgrade-ability. But currently the common consensus is that an End . cage would be needed for upgrade, since moving the Vat storage would be too gas-expensive/delicate (esp. translating the Vat . hope/nope calls that have been made thus far). No plans yet for MCD2.0 launch, but having potential refactorings listed would still be useful so it could be included in an MCD2.0 launch if it happens.

ehildenb commented 4 years ago

Tuesday November 19, 2019

Done

Refactoring property checker: #104
Small updates to model: #105
Initial trace generator infrastructure: #106
Same rule keys for map accesses fixed in semantics: #108
Randomly generated witnesses for lucash attacks: #109
Confirm that violations are found with assert construct: #110

In Progress

@malturki is working on generalizing the properties.
@ehildenb is working on generalizing the trace generation.

Discussion

Is <vat-sin> ever non-zero for a user who is not the Vow? Just on inspecting the semantics, it looks like it's not the case that <vat-sin> is ever changed for a user other than Vow.
Saying that Flap . kick was un-authed, what would be a reasonable maximum BID? This affects the random tester because it looks like the reasonable maximum is however much Gem "MKR" the Flap contract currently holds is the maximum, but that seems to have little correspondence to the contract doing the kicking. Is there a reasonable scenario where BID starts as non-zero?
Could do a proof a proof that any non-auth step does not change the equality <vat-sin>[Vow] == <vat-vice>

ehildenb commented 4 years ago

Tuesday November 26, 2019

Might be done

Properties over vat: #120

Done

Switched over to byte-arrays as random input to KMCD, remove depth bound: #111
Updates to pyk library to better handle KMCD: kframework/k#921
Switch mcd-pyk.py script to run/generate random inputs: #112

Discussion

@iamchrissmith added: Question for Nov 26: Project timeline/schedule. @ehildenb added estimated delivery dates to the Google Doc for the remaining milestones.
@malturki and @ehildenb are having trouble coming up with sensible properties to check for in random testing. We've mostly had meetings/discussions since last week about this, but cannot seem to come up with generalizations of the attack properties which do not over-generalize. The main problem seems to be that many behaviors are allowed in the system, it's completely reasonable that someones total allocation of resources changes without any input or resources (eg. rates adjust, or they put their Dai in the Pot). So we were hoping that we could enlist more MKR folks to help on this front, maybe accelerate the pair-programming sessions to the point where they can meaningfully help write properties over the specification.

Potential Properties

Ideas for properties: Total system debt excluding frob and Flip auctions which don't cover the tab should not grow by more than DSR - stability fee (and should probably even shrink).
User puts 10 gem into urn, whatever they do, they cannot get more than 10 gem back out. This is regardless of DSR/stability fee and other adjustments due to auctions that can happen. A user can convert MKR to Dai via a Flap auction, and then convert the vat-dai to vat-gem via a Flip auction. So you could put 10 gem into an urn, and get another 10 gem via a sequence of auctions (a Flap auction to get enough vat-dai to pay back stability fee + to bid on a Flip auction for the gem), and then exit all 20 gem from the Vat (after closing your CDPs).
Bidding on an auction will always result in getting resulting gem/dai of auction, or your last bid, but not both.
When End . cage goes through, whatever Dai you have (including vat-dai and dai locked in auctions) represents your total share of the overall gem in the system, and thus how much gem you should be paid out (adjusted for the price of that gem). Narrows possible sequences to only ones which are not require(live), can we take this into account in the test generation?

ehildenb commented 4 years ago

Tuesday December 03, 2019

Done

Some measurables over the Vat: #120

Might be done

Symbolic BFS of state-space: #124

Pair Programming Agenda

Answer any questions about the questions about the semantics?
How to formalize properties, and trying to formalize a few new properties.

Potential Properties

After End . cage, the total debt/dai in system should not increase (except for maybe Flip auctions?).
Things that should only change before/after End . thaw.
So at these events can log some specific measurables of the system.
After End . cage, a user should not be able to decrease an urns Ink except via End . skim or Vat . fork. Another variation would be that the total amount of ink does not go down.
After End . cage the debt drawn per collateral shouldn't change.
Total amount of ERC20 dai in circulation should be equal to the <vat-dai> for the adapter for erc20 dai.
Any move from <vat-dai> to ERC20 Dai can be followed by a move back of equal or lesser value (assuming no Dai . ... calls).

From the chat:

Chris Smith10:05 AM https://github.com/runtimeverification/mkr-mcd-spec Gonzalo Balabasquer10:37 AM flux doesn't change ink Andy Chorlian10:41 AM Still trying to make sure I get how this works but could something along the lines of this work? Dai joined to the pot can never exit for less than the amount joined? Chris Smith10:42 AM i like that one @andy Kurt Barry10:42 AM ^I think you could actually set the dsr < 1 Andy Chorlian10:43 AM it is a uint how would that work? Chris Smith10:43 AM you could, but eventually the drip is going to hit a negative here: https://github.com/makerdao/dss/blob/master/src/pot.sol#L143 if you set dsr to more than 0 but less than 1 you get a "negative" DSR Andy Chorlian10:44 AM oh I am dumb Chris Smith10:44 AM and would decrease the Pie per user until you ran out of Chi and then drips would fail Gonzalo Balabasquer10:47 AM not sure if I followed the last part, you never can have dsr set lower to 1 otherwise drip will always fail Chris Smith10:48 AM @gonza, if we let DSR run for a bit, we build up some Chi, then we could set it to less than 1 and decrease the chi for a set period of time, right? Gonzalo Balabasquer10:48 AM nope this "uint chi_ = sub(tmp, chi);" will always fail if dsr is set lower to 1 "tmp = rmul(rpow(dsr, now - rho, ONE), chi);" is always lower than chi if dsr is lower than 1 Chris Smith10:49 AM because tmp would immediately be larger than chi? or yeah i meant smaller Gonzalo Balabasquer10:50 AM right Chris Smith10:51 AM ahh ok, so going back to andy's original suggestion, Dai joined to the pot can never exit for less than the amount joined? Gonzalo Balabasquer10:54 AM I'd phrase it as the amount of DAI taken when joining X amount of pie has to be same or lower than the one returned when exiting X amount of pie. Kurt Barry10:56 AM That should work then. Aside: that is a rather tricky way to enforce dsr > 1... Of course, our code is full of all sorts of important things that are only subtly enforced in safe math checks. Chris Smith10:58 AM 4pm ET: https://meet.google.com/weu-axjy-baz

ehildenb commented 4 years ago

Tuesday December 10, 2019

Addition/cleanup of vat-dai-measurables: #128
Migrate repository to MakerDAO organization (do during meeting to handle various permissions issues).
Begin working on blog post?

ehildenb commented 4 years ago

Tuesday December 17, 2019

Added some paragraphs to completion doc: https://docs.google.com/document/d/1aNWxj3f1mwHypwRqbj5mlLRNftvvd9RvQM8noC3KarY/edit?ts=5deec570&pli=1
Merged updates from pair-programming (without turning on properties): #129
Made update to make property failures more apparent about where/how they failed: #130
Confirmed that totalDebtBounded finds the known bugs with lucash-pot and lucash-pot-end.

ehildenb commented 4 years ago

Tuesday January 13, 2019

Enable updating to K master again by disabling ? variables: #137
Add target test-random which runs random tester: #136
Running each simulation takes 20-30s, but the actual runtime of the LLVM backend is roughly 0.03s. @dwightguth is investigating why the Frontend is taking so long, but for now I'm going to generate Kore for the LLVM backend to consume directly.
136 demonstrates how to run random tests, but as @kmbarry1 pointed out, the output of the Flap-Kick and Flip-Kick attack tests doesn't make much sense. We need a better property for capturing what is going on with these attacks: https://github.com/makerdao/mkr-mcd-spec/pull/136#discussion_r366145963
kframework/k#1022 improves the time per run from 20-30s to 2-3s, along with adding --no-sort-collections. Will allow us to avoid generating Kore directly and still be able to use frontend.

ehildenb commented 4 years ago

Tuesday January 21, 2019

Kurt's gist: https://gist.github.com/kmbarry1/476aac5adcd987780d402a92ae529b75
I've been working on (1) having the reported attacks stop as soon as violation is found (so no attack minimization is needed), and (2) fixing up the way symbolic backend treats the random choices. Neither is ready for merge.
Could go over the sequence generation approach today, with time permitting, as we haven't reviewed that yet.

ehildenb commented 4 years ago

Tuesday January 28, 2019

Pull request for reporting minimized violations: #145
Dockerfile minimization: #146
@kmbarry1 fixes to sorts of Bit types: #147
Simple fix to PotChiPieDai invariant (discussion, better way to do it?): #150
Some simple usability improvements: #149
Anyone else have a chance to run the tool?
@kmbarry1 get a chance to work on discussed invariants last week?

AddGenerator ( ( ( GenFlapKick | GenFlapTick | GenFlapTend | GenFlapDeal ) ) ; GenEndCage ; ( ( GenFlapTick | GenFlapYank ) ) )

vat.dai(Flap) - sumOfAllLots >= 0 Gem.MKR(Flap) - sumOfAllBids >= 0

// If Flap.deal event adjusts constant appropriately: sum(Gem.MKR.balances without Flap) + sumOfAllBids == constant // (deals are handled accordingly)

sum(Gem.MKR.balances without Flap) + sumOfAllBids <= Gem.MKR.totalSupply
Bridge between RV Slack and MKR channel? From @godsflaw: perhaps this: https://zapier.com/apps/rocketchat/integrations/slack
Need to work in two directions from here, (1) generalizing the steps that can be generated by kmcd-prelude.md, and (2) conformance testing. Conformance testing I can output a log of transactions generated by the accounts in some consumable format (JSON?), can someone on the MKR team take care of making a testing harness to feed this into the actual Solidity implementation? If we can turn it into proper signed transactions somehow, we can feed it into any web3 client (including KEVM). Otherwise we can hack something together with KEVM, but it may take longer.

Rough translation:
```
 transact ADMIN Pot . file dsr 23 /Rat 20
 TimeStep 1
 transact "Bobby" Vat . move "Bobby" Pot 495 /Rat 64
```
becomes:
```
 admin.Potfile("dsr", 23/20);
 hevm.warp(now + 1);
 bobby.vatMove(address(bobby), address(Pot), 495 / 64);
 assertEq(vat.dai(address(bobby)), SOME_NUMBER);
```

ehildenb commented 4 years ago

Tuesday February 3, 2020

Due to prepping user-studies running this week for Firefly, didn't have much time to work this week.
Discuss @kmbarry1 's PR: #152
Opened issue for non-intuitive error message: https://github.com/kframework/k/issues/1079
Added documentation for cell collections: https://github.com/kframework/k/pull/1080

ehildenb commented 4 years ago

Friday February 07, 2020

DEPLOY-PRELUDE (suggested by @kmbarry1 ). Sounds good for now, seems simplest way to do it, also perhaps a bit more transparent than hardcoding into initial configuration.

Solidity code emission #155

Example output (does it look feasible?):

 ADMIN.Vat_rely(address(Pot));
 ADMIN.Vat_rely(address(End));
 ADMIN.Pot_rely(address(End));
 ADMIN.Vow_rely(address(Pot));
 ADMIN.Vow_rely(address(End));
 ADMIN.Cat_rely(address(End));
 ADMIN.Flap_rely(address(Vow));
 ADMIN.Flop_rely(address(Vow));
 ADMIN.Pot_file("vow", address(Vow));
 ADMIN.Vat_rely(address(GemJoin_gold));
 ADMIN.Spot_setPrice("gold", 1);
 ADMIN.Flip_gold_rely(address(End));
 ADMIN.Gem_MKR_mint(address(Flap), 20);
 ADMIN.Vat_file("Line", 1000000000000);
 ADMIN.Vat_file("spot", "gold", 3000000000);
 ADMIN.Vat_file("line", "gold", 1000000000000);
 ADMIN.Vow_file("bump", 1000000000);
 ADMIN.Gem_gold_mint(address(Alice), 20);
 ADMIN.Gem_gold_mint(address(Bobby), 20);
 Alice.Vat_hope(address(Pot));
 Alice.Vat_hope(address(Flip_gold));
 Alice.Vat_hope(address(End));
 Bobby.Vat_hope(address(Pot));
 Bobby.Vat_hope(address(Flip_gold));
 Bobby.Vat_hope(address(End));
 Alice.Vat_slip("gold", address(Alice), 10);
 Alice.Gem_gold_transferFrom(address(Alice), address(GemJoin_gold), 10);
 Alice.GemJoin_gold_join(address(Alice), 10);
 Bobby.Vat_slip("gold", address(Bobby), 10);
 Bobby.Gem_gold_transferFrom(address(Bobby), address(GemJoin_gold), 10);
 Bobby.GemJoin_gold_join(address(Bobby), 10);
 Alice.Vat_frob("gold", address(Alice), address(Alice), address(Alice), 10, 10);
 Bobby.Vat_frob("gold", address(Bobby), address(Bobby), address(Bobby), 10, 10);
 Pot.Vat_move(address(Pot), address(Vow), 0);
 ADMIN.Vat_cage();
 ADMIN.Cat_cage();
 Vow.Vat_move(address(Flap), address(Vow), 0);
 End.Flap_cage(0);
 End.Flop_cage();
 End.Vat_heal(0);
 ADMIN.Vow_cage();
 ADMIN.Pot_cage();
 ADMIN.End_cage();
 Pot.Vat_hope(address(Alice));
 ANYONE.End_cage("gold");
 hevm.warp(2);
 hevm.warp(1);
 ANYONE.End_thaw();
 ANYONE.End_flow("gold");
 ANYONE.Vat_suck(address(Vow), address(Pot), 0);
 ANYONE.Pot_drip();
 ANYONE.Vat_grab("gold", address(Bobby), address(End), address(Vow), -10, -10);
 ANYONE.End_skim("gold", address(Bobby));
 ANYONE.Vat_grab("gold", address(Bobby), address(End), address(Vow), 0, 0);
 ANYONE.End_skim("gold", address(Bobby));
 Alice.Vat_move(address(Pot), address(Alice), 0);
 Alice.Pot_exit(0);
 Alice.Vat_move(address(Alice), address(Pot), 625_/Rat_64);
 Alice.Pot_join(625_/Rat_64);
 hevm.warp(1);
 ANYONE.Vat_suck(address(Vow), address(Pot), 0);
 ANYONE.Pot_drip();
 Alice.Vat_move(address(Pot), address(Alice), 625_/Rat_64);
 Alice.Pot_exit(625_/Rat_64);

ACTION Remove intermediate steps, intermediate steps should record caller not transaction initiator.

To regenerate (will add these to the repo README):

 find . -name kast.py # grab directory this is in as THAT_DIRECTORY
 export PYTHONPATH=THAT_DIRECTORY
 find . -name krun # grab the direcotry as KRUN_DIRECTORY
 export PATH=$KRUN_DIRECTORY:$PATH
 ./mcd-pyk.py random-test --help
 ./mcd-pyk.py random-test 100 1 --emit-solidity

Not sure where to jump in instructions for repo README, make clearer the delineation between setup and running. ACTION: Update readme with clearer innstructions.

Need to filter to only include top-level calls. ACTION: Will drop markers in the trace to say "this is an actual external call" and only keep those external calls.
What to do about fractions and scaling to wad/rad/ray? I think we'll have to manually hardcode those rules into the solidity generator. ACTION Solidity testing harness will handle fractions, just scale them all up by smallest of Rad/Ray/Wad (think 10^18?).
Assertions need to be added. I have local work making a minimized state delta between states (i) after attack prelude, and (ii) after generating steps. Can show what it looks like, discuss what assertions should look like some more. ACTION Actually do best-effort generation of assertions.
2 milestones left, (1) is throughput, and (2) is conformance. Let's discuss and define done for them.
Throughput seems pretty good right now, we know of one more optimization we can make to go from 2s/run to roughly 0.01s/run, which will be a major jump, but it will take a little while to implement (skip KAST format, directly feed input into backend). Right now we can find the known attacks relatively quickly with the existing random tester. ACTION Chris will review and let me know.
Conformance testing needs assertions and a testing harness. Maybe we can pair on someone's machine who has the dss testing harness setup, and we can take the output above and turn it into a test, taking notes about what needs to change in the output to make it work. DEFN: Able to generate solidity and automatically dump it into a template file (just have some string DUMP_CODE_HERE), and it runs in normal testing harness correctly, and if we break it it breaks correctly.

ehildenb commented 4 years ago

Tuesday February 11, 2020

Merged solidity emission from last week #155, has intermediate steps removed.
Documentation/cleanup PR #159.
4x speedup when using KServer observed (documented in PR #159).

Current output of asserting adder:

// Test Run
ADMIN.Vat_rely(PotLike(Pot));
ADMIN.Vat_rely(EndLike(End));
ADMIN.Pot_rely(EndLike(End));
ADMIN.Vow_rely(PotLike(Pot));
ADMIN.Vow_rely(EndLike(End));
ADMIN.Cat_rely(EndLike(End));
ADMIN.Flap_rely(VowLike(Vow));
ADMIN.Flop_rely(VowLike(Vow));
ADMIN.Pot_file("vow", VowLike(Vow));
ADMIN.Vat_rely(GemJoinLike(GemJoin_gold));
ADMIN.Spot_setPrice("gold", 1);
ADMIN.Flip_gold_rely(EndLike(End));
ADMIN.Gem_MKR_mint(FlapLike(Flap), 20);
ADMIN.Vat_file("Line", 1000000000000);
ADMIN.Vat_file("spot", "gold", 3000000000);
ADMIN.Vat_file("line", "gold", 1000000000000);
ADMIN.Vow_file("bump", 1000000000);
ADMIN.Gem_gold_mint(UserLike(Alice), 20);
ADMIN.Gem_gold_mint(UserLike(Bobby), 20);
Alice.Vat_hope(PotLike(Pot));
Alice.Vat_hope(FlipLike(Flip_gold));
Alice.Vat_hope(EndLike(End));
Bobby.Vat_hope(PotLike(Pot));
Bobby.Vat_hope(FlipLike(Flip_gold));
Bobby.Vat_hope(EndLike(End));
Alice.GemJoin_gold_join(UserLike(Alice), 10);
Bobby.GemJoin_gold_join(UserLike(Bobby), 10);
Alice.Vat_frob("gold", UserLike(Alice), UserLike(Alice), UserLike(Alice), 10, 10);
Bobby.Vat_frob("gold", UserLike(Bobby), UserLike(Bobby), UserLike(Bobby), 10, 10);
ADMIN.End_cage();
ANYONE.End_cage("gold");
ANYONE.End_thaw();
ANYONE.End_flow("gold");

// Assertions
CatLike.get_live == false;
EndLike.get_live == false;
EndLike.get_debt == 20;
EndLike.get_tag == "gold" |-> 1;
EndLike.get_art == "gold" |-> 20;
EndLike.get_fix == "gold" |-> 1;
FlapLike.get_live == false;
FlopLike.get_live == false;
VatLike.get_live == false;
VowLike.get_live == false;

ACTIONS

Alice.Vat_hope(PotLike(Pot)); => Alice.Vat_hope(address(Pot));
ADMIN.Gem_gold_mint(UserLike(Bobby), 20); => ADMIN.Gem_gold_mint(address(Bobby), 20);

EndLike.get_live == false; => assertTrue(End.live() == 0);
EndLike.get_debt == 20; => assertTrue(End.debt() == 20);
EndLike.get_tag == "gold" |-> 1; => assertTrue(End.tag("gold") == 1);

// without ABI encoder?
(,uint art) = Vat.urns("gold", address(Alice));
assertTrue(art == 30);

// needs pragma ABI encoder? perhaps needs wrapping of `Vat` in `VatLike`?
pragma experimental ABIEncoderV2;
assertTrue(Vat.urns("gold", address(Alice)).art == 30);

ACTION: Handle the fractions/ratios.

ehildenb commented 4 years ago

Monday March 30, 2020

Finish the Solidity code generation. @ehildenb will take care of.
Look at specs that are not passing (k-dss). @kmbarry1 will write it up.
Look at representing numbers directly as integers (either wrapped or with using appropriate operations). @ehildenb will look at.
Flop-auction bug, can we make a property for it? @kmbarry1 will send over presentation about it.
Setup weekly meetings at 9AM. @kmbarry1 will send calendar invite.

ehildenb commented 4 years ago

Monday April 06, 2020

Two PRs to work towards more assertions in Solidity code: #167, #168, and #169
Have reviewed the flop attack issue, looks like an issue where the "normal path" gets dead-locked by the "abnormal path". I think we can state this as a property about deadlocks in general, that is "Flop auctions should not be able to deadlock", and eventually generalized to "There should not be deadlocks in the system in general". Response: We can take snapshot of the state more frequently (instead of Measure()), so that we can go back over the trace and say things like "when it's the case that we would want to be able to Flop, are we always able to Flop?". Not really a deadlock property, but some sort of "system is live enough property".
Event recording is somewhat messy right now, because we're recording (i) the top-level transaction that fires, (ii) all intermediate calls (as if all calls had the note modifier), (iii) custom events that some functions emit, and (iv) exceptions, generation steps, etc.... It may be nice to clean this up by having a more structured log of the events that occur, specifically we could bundle all generated events with the transaction event that caused them. The one downside is this will make it trickier to specify properties that we want to hold at all intermediate states as well, not just at transaction boundaries. Response: We really only care about transaction-level consistency anyway, so let's go with a bit more structure and only have the properties checked over transaction calls. Later we can add back in ability to handle call-level properties.
Rat vs. Int: argument for Int is that the model is already targeting EVM pretty closely, so making it closer will not be a huge deal. Argument for Rat is that it remains system agnostic. I think there are not so many places where we do target EVM directly, but it is true that the important system is the one running on EVM. Response: Let's separate this change into two steps, (1) will be to make a new file kmcd-data.md which defines operators like rmul and rpow which handle the arithmetic that the system does, and then (2) we'll switch out underlying implementation in kmcd-data.md for Int instead of Rat.
@kmbarry1 will make an "attack" in tests/attacks which represents the failure to call Vow . flop after minimal setup.

ehildenb commented 4 years ago

Tuesday April 14, 2020

Proposed update to Flop issues: https://github.com/makerdao/dss/pull/110/files#r407994976
Draft PR factoring out Rat representation: https://github.com/makerdao/mkr-mcd-spec/pull/173. Still need to fix kmcd-props file and kmcd-prelude file.
Reviewed attack PR for Flop blocking attack, some minor feedback: https://github.com/makerdao/mkr-mcd-spec/pull/171

ehildenb commented 4 years ago

Monday April 20, 2020

PR to add implicit positiivity constraints on everything: #174
PR which implements proposed changes to auction contracts: #175 (note that we aren't lifting the assignment of GUY into the conditional, because it makes the K rules much uglier but doesn't actually change the behavior of the model, whereas conditionally calling the Vat . move does change the behavior).
PR factoring out Rat representation is ready: #173. It's blocked on #174. -beg> and -pad> are now Wad, but I don't know if it was the original intention in the code.
Dependency update job revealed a possible regression in llvm-backend (also affecting KEVM), I've been investigating: #172.

ehildenb commented 4 years ago

Tuesday April 28, 2020

Been a slow week.
Have addressed reviews here, favoring rmul like operations where specified: #173.
Have next PR ready locally, which switches to wrapped rational representation (with stronger type-checking in place): #177
Discuss how to migrate CI over to Maker servers (with Sava on the call).

ehildenb commented 4 years ago

Monday May 4, 2020

Have begun an implementation of Fixed Width integers in K, pending discussions with @dwightguth .
Have switched over kmcd-data.md to the Fixed Width integers, but am still having some difficulties getting it to build.
Have recently rolled out K dockerhub images, and am working on switching all the builds over to these images (to save 6-12 minutes per build). The PR is ready (pending some PRs into K landing), but not sure how this will affect the Travis stuff (@daimesava ).

ehildenb commented 4 years ago

Monday May 11, 2020

CircleCI PR ready for review: https://github.com/makerdao/mkr-mcd-spec/pull/180
Changes to Auction contracts ready for review: https://github.com/makerdao/mkr-mcd-spec/pull/175
Fixed point representation blocked on issue in K frontend, but also ready for re-review: https://github.com/makerdao/mkr-mcd-spec/pull/184

Now generating Solidity source code like this:

// Test Run
admin.vat_rely(address(goldJoin));
admin.spotter_setPrice("gold", 3000000000000000000000000000);
admin.spotter_file("mat", "gold", 1000000000000000000000000000);
admin.spotter_file("par", 1000000000000000000000000000);
admin.goldFlip_rely(address(end));
admin.vat_file("line", "gold", 1000000000000000000000000000000000000000000000000000000000);
admin.Gem_gold_mint(address(alice), 20000000000000000000);
admin.Gem_gold_mint(address(bobby), 20000000000000000000);
alice.vat_hope(address(pot));
alice.vat_hope(address(goldFlip));
alice.vat_hope(address(end));
alice.vat_hope(address(flop));
bobby.vat_hope(address(pot));
bobby.vat_hope(address(goldFlip));
bobby.vat_hope(address(end));
bobby.vat_hope(address(flop));
alice.goldJoin_join(address(alice), 10000000000000000000);
bobby.goldJoin_join(address(bobby), 10000000000000000000);
bobby.goldJoin_join(address(bobby), 8000000000000000000);
bobby.vat_move(address(bobby), address(alice), 0);
admin.pot_file("dsr", 1000000000000000000000000000);
hevm.warp(1);
bobby.vat_hope(address(alice));
hevm.warp(1);
hevm.warp(1);

// Assertions
// UNIMPLEMENTED << assertTrue( Gems.cell() == GemCellMapItem( <gem-id>
//  "gold"
//</gem-id> , <gem>
//  <gem-id>
//    "gold"
//  </gem-id>
//  <gem-wards>
//    .Set
//  </gem-wards>
//  <gem-balances>
//    "bobby" |-> FInt( 2000000000000000000 , 1000000000000000000 )
//    GemJoin "gold" |-> FInt( 28000000000000000000 , 1000000000000000000 )
//    "alice" |-> FInt( 10000000000000000000 , 1000000000000000000 )
//  </gem-balances>
//</gem> ) ); >>
assertTrue( vat.can(address(bobby), address(pot)) != 0 );
assertTrue( vat.can(address(bobby), address(flop)) != 0 );
assertTrue( vat.can(address(bobby), address(alice)) != 0 );
assertTrue( vat.can(address(bobby), address(goldFlip)) != 0 );
assertTrue( vat.can(address(bobby), address(end)) != 0 );
assertTrue( vat.can(address(alice), address(pot)) != 0 );
assertTrue( vat.can(address(alice), address(flop)) != 0 );
assertTrue( vat.can(address(alice), address(goldFlip)) != 0 );
assertTrue( vat.can(address(alice), address(end)) != 0 );
assertTrue( vat.gem("gold", address(end)) == 0 );
assertTrue( vat.gem("gold", address(alice)) == 10000000000000000000 );
assertTrue( vat.gem("gold", address(goldFlip)) == 0 );
assertTrue( vat.gem("gold", address(bobby)) == 18000000000000000000 );

Can someone make a testing harness that this can be dropped into? Who would be good for this?

ehildenb commented 4 years ago

Tuesday May 19, 2020

Changes to Flop contracts merged (updated expected output shows no violation): #175
Fixed point representation: #184
Improved random test generation: #186

ehildenb commented 4 years ago

Tuesday May 26, 2020

Setting up testing harness on CI to make sure we have the dependencies needed: #189
Need to get these changes merged: https://github.com/makerdao/mkr-mcd-spec-sol-tests/compare/test-harness
Have example full test file output:

pragma solidity ^0.5.12;

import "./MkrMcdSpecSolTests.t.sol";

contract TestExample is MkrMcdSpecSolTestsTest {

    function test0() public {

        // Test Run

        admin.vat_rely(address(goldJoin));
        admin.spotter_setPrice("gold", 3000000000000000000000000000);
        admin.spotter_file("mat", "gold", 1000000000000000000000000000);
        admin.spotter_file("par", 1000000000000000000000000000);
        admin.goldFlip_rely(address(end));
        admin.vat_file("line", "gold", 1000000000000000000000000000000000000000000000000000000000);
        admin.Gem_gold_mint(address(alice), 20000000000000000000);
        admin.Gem_gold_mint(address(bobby), 20000000000000000000);
        alice.vat_hope(address(pot));
        alice.vat_hope(address(goldFlip));
        alice.vat_hope(address(end));
        alice.vat_hope(address(flop));
        bobby.vat_hope(address(pot));
        bobby.vat_hope(address(goldFlip));
        bobby.vat_hope(address(end));
        bobby.vat_hope(address(flop));
        alice.goldJoin_join(address(alice), 10000000000000000000);
        bobby.goldJoin_join(address(bobby), 10000000000000000000);
        alice.vat_move(address(alice), address(alice), 0);
        admin.pot_file("dsr", 1000000000000000000000000000);
        hevm.warp(1);
        bobby.vat_hope(address(alice));
        hevm.warp(2);
        hevm.warp(1);

        // Assertions

        assertTrue( vat.can(address(bobby), address(pot)) != 0 );
        assertTrue( vat.can(address(bobby), address(flop)) != 0 );
        assertTrue( vat.can(address(bobby), address(alice)) != 0 );
        assertTrue( vat.can(address(bobby), address(goldFlip)) != 0 );
        assertTrue( vat.can(address(bobby), address(end)) != 0 );
        assertTrue( vat.can(address(alice), address(pot)) != 0 );
        assertTrue( vat.can(address(alice), address(flop)) != 0 );
        assertTrue( vat.can(address(alice), address(goldFlip)) != 0 );
        assertTrue( vat.can(address(alice), address(end)) != 0 );

    }

    function test1() public {

        // Test Run

        admin.vat_rely(address(goldJoin));
        admin.spotter_setPrice("gold", 3000000000000000000000000000);
        admin.spotter_file("mat", "gold", 1000000000000000000000000000);
        admin.spotter_file("par", 1000000000000000000000000000);
        admin.goldFlip_rely(address(end));
        admin.vat_file("line", "gold", 1000000000000000000000000000000000000000000000000000000000);
        admin.Gem_gold_mint(address(alice), 20000000000000000000);
        admin.Gem_gold_mint(address(bobby), 20000000000000000000);
        alice.vat_hope(address(pot));
        alice.vat_hope(address(goldFlip));
        alice.vat_hope(address(end));
        alice.vat_hope(address(flop));
        bobby.vat_hope(address(pot));
        bobby.vat_hope(address(goldFlip));
        bobby.vat_hope(address(end));
        bobby.vat_hope(address(flop));
        alice.goldJoin_join(address(alice), 10000000000000000000);
        bobby.goldJoin_join(address(bobby), 10000000000000000000);
        bobby.vat_move(address(bobby), address(alice), 0);
        alice.goldJoin_join(address(alice), 4000000000000000000);
        bobby.vat_hope(address(alice));
        admin.pot_file("dsr", 1000000000000000000000000000);
        hevm.warp(2);
        hevm.warp(2);
        hevm.warp(2);

        // Assertions

        // UNIMPLEMENTED << assertTrue( Gems.cell() == GemCellMapItem( <gem-id>
        //  "gold"
        //</gem-id> , <gem>
        //  <gem-id>
        //    "gold"
        //  </gem-id>
        //  <gem-wards>
        //    .Set
        //  </gem-wards>
        //  <gem-balances>
        //    "bobby" |-> FInt( 10000000000000000000 , 1000000000000000000 )
        //    GemJoin "gold" |-> FInt( 24000000000000000000 , 1000000000000000000 )
        //    "alice" |-> FInt( 6000000000000000000 , 1000000000000000000 )
        //  </gem-balances>
        //</gem> ) ); >>
        assertTrue( vat.can(address(bobby), address(pot)) != 0 );
        assertTrue( vat.can(address(bobby), address(flop)) != 0 );
        assertTrue( vat.can(address(bobby), address(alice)) != 0 );
        assertTrue( vat.can(address(bobby), address(goldFlip)) != 0 );
        assertTrue( vat.can(address(bobby), address(end)) != 0 );
        assertTrue( vat.can(address(alice), address(pot)) != 0 );
        assertTrue( vat.can(address(alice), address(flop)) != 0 );
        assertTrue( vat.can(address(alice), address(goldFlip)) != 0 );
        assertTrue( vat.can(address(alice), address(end)) != 0 );
        assertTrue( vat.gem("gold", address(end)) == 0 );
        assertTrue( vat.gem("gold", address(alice)) == 14000000000000000000 );
        assertTrue( vat.gem("gold", address(goldFlip)) == 0 );
        assertTrue( vat.gem("gold", address(bobby)) == 10000000000000000000 );

    }
}

ehildenb commented 4 years ago

Wednesday June 03, 2020

Can we change the meeting time to some day other than Monday? I'll be back in the US, so maybe we can even move it later in the day on some day.
Merged some updates, running MKR test harness on CI #189, got K update job to go through #187, and fixed some issues in the Makefile #190.
Have Transaction Level Logging refactor PR ready: #191
Have local work on automatically generating solidity files and feeding the result into dapp test (pending #191 being merged): #192.
Vat "Line" vs "line" issue with solidity code generation: #194.

ehildenb commented 4 years ago

Wednesday June 10, 2020

Slow week (updates to KEVM needed to be pushed through downstream projects).

Switching to native MD support: https://github.com/makerdao/mkr-mcd-spec/pull/195
Issue by Andy where calls which belong in the constructors are generating Solidity call events. Proposed solution is to add a function constructor to each contract and have the DEPLOY_PRELUDE call each constructor as a transaction. Then when generating solidity code we can just ignore any calls to constructor. Anything hardcoded in the DEPLOY_PRELUDE which is covered by these constructors can be removed.

ehildenb commented 4 years ago

Wednesday June 17, 2020

Worked on adding the DssOpen spec to the KEVM regression test-suite: kframework/evm-semantics#818. Led to several suggestions about how to improve the KLab on CI, mostly involving disabling state-logging by default when running proofs on CI, and only re-enabling state-logging when a given proof fails. This should be (at least) a 5x speedup, and even more if there is high disk-contention.
Local work on adding deploy contract logic to KMCD model, so that we have better conformance with how tests are setup/run, but also gives a more complete model of KMCD. This is leading to several bug-fixes/cleanups, but overall brings us closer to exactly matching the Solidity. Haven't had time to test out the solidity generation yet, still working through the bugs in how I have the deployment setup.

https://github.com/makerdao/k-dss/issues/17

ehildenb commented 4 years ago

Wednesday July 01, 2020

Some more work on DssOpen spec, and on porting VatMoveDiff spec over to KEVM regression test-suite. Led to long internal discussion about some simplification lemmas, and some minor performance improvements to KEVM. VatMoveDiff is passing, but the spec has several changes from original generated by KLab. DssOpen is close to passing, but needs more work.
Fixed K update job: #196
PR with trivial updates and minor changes to make next PR easier to review: #197
PR which adds semantics of DssDeploy ready too, but blocked on #197: #198
Solidity code generation is passing tests! Requires one small change to the prelude where we don't do transact Vow Vat . hope Flap, which is wishing the Flap for the Vow. Removing it only causes one exception in the test-suite, but I couldn't find any indication that this is called in the deploy process?

ehildenb commented 3 years ago

Wednesday July 08, 2020

Merged trivial updates to make deploy PR easier #197.
Opened PR which gives semantics to DssDeploy #198 (discussion about GemJoin MKR).
Opened PR which fixes the solidity code generation process in several cases, to where we are almost able to always pass the solidity tests #199.
Make assertRevert (or something similar) possible: https://github.com/makerdao/mkr-mcd-spec-sol-tests/pull/4
Summary of changes to KEVM upcoming: https://github.com/kframework/evm-semantics/pull/860#issuecomment-655649515
Example change to the encoding of storage: https://github.com/kframework/evm-semantics/pull/860/files#r451643155
Example lemmas which I've found are good at keeping local memory small: https://github.com/kframework/evm-semantics/pull/860#discussion_r451641065

ehildenb commented 3 years ago

Wednesday July 15, 2020

Merged #198, #199.
Absorb solidity testing submodule PR: #200.
Removing nonsense calls from the PRELUDEs: #201.
Use updated assertion structure for all statements: #202.
Named assertions for easier finding of bugs: #205 (issue with Solidity compiler version?)
Discussion about last milestone. We are able to conformance test against the existing semantics, so I'm ready to declare it done soon. Anything else that we'd like to see there?

Discussion

Solidity generation is working and able to conformance test successfully. Remaining known things are (i) there are some assertions that are not translatable, (ii) the Spot contract is not modelled faithfully because we don't use an external contract for the Pip, and (iii) storage values aren't initialized to zero by default.
To make the model more useful: (i) kmcd-props can have more properties added to it, and (ii) kmcd-prelude can have more generators added to it (to see more behaviors). (ii) is pretty mechanical, (i) requires thinking about what properties you want the model to have.

https://github.com/kframework/k/issues/1333:

module MY-MODULE
    imports oenuthe
    ....
endmodule

module VERIFICATION
    imports MY-MODULE
endmodule

module MY-SPEC
   imports VERIFICATION
endmodule

ehildenb commented 3 years ago

Wednesday July 29, 2020

I'm making sure that specs I worked on for MCD regression tests in KEVM are still working on latest master.
What to prioritize working on next?
- Is there something specific you'd like me to target the model at?
- Is improving performance of CI specs higher priority?

Something to target model at: Once there is more info on new liquidations, maybe we can target test generation with them. Likely a month or so out.

Otherwise focus on CI specs (ordered roughly by priority):

Some proofs are still not passing.
Adding regression tests to KEVM.
Some dynamic string issues with KEVM (string instead of bytes32 type). New Solidity versions won't automatically cast bytes32 => string type. Using bytes32 everywhere for formal verification (because dynamic length string is problematic). Maybe we could try adding length constraints to string everywhere? ERC20 standard requires the symbol/name to be string, so other tokens use that.
Infrastructure speedup (kompile ahead of time of kprove).

Let's pick out one such proof to start with:

https://reports.makerfoundation.com/k-dss/. Latest report https://reports.makerfoundation.com/k-dss/33d35d2934cfc47ccb98/. Jug.drip(), Pot.drip(), Cat.bite(), End.cage(), End.skip(), End.skim() are example failures.
Will start with End.cage(). https://reports.makerfoundation.com/k-dss/33d35d2934cfc47ccb98/#End_cage() The used KEVM and bin_runtime and lemmas are at the top of the page.

ehildenb commented 3 years ago

Wednesday August 19, 2020

Discuss trying Firefly on MKR contracts. Requires setting up a Truffle testing harness. May be interesting, because we can generate tests for uncovered code paths, but I doubt they will be very interesting tests since they only do depth 1 transactions, and the ones generated by the mkr-mcd-spec are out to any depth (so they actually can exercise code-paths). But we could setup the Truffle testing harness, and see if the generated test for mkr-mcd-spec increases code coverage, and if it does, add that as a unit test to the actual mkr repo. Definitely some interest, RV will attempt to setup Firefly on dss repo and report the results.
Let's link our chats. Bogdan would like to join in and linking them will just be easier for us to get more people on our team involved.
First PR merged with vat-move-diff spec: https://github.com/kframework/evm-semantics/pull/892/files.
- Uses abstract pre and concrete post state storage model STORAGE => STORAGE [ K1 <- V1' ] [ K2 <- V2' ] requires #lookup(STORAGE, K1) ==Int V1 andBool #lookup(STORAGE, K2) ==Int V2
Second PR merged with cat-exhaustive spec: https://github.com/kframework/evm-semantics/pull/896
- Discovered issue with EVMC_REVERT_NETWORK, needed to be EVMC_REVERT (have modified my KLab for this).
- https://github.com/kframework/evm-semantics/pull/896/files#diff-41986b7ce6e0e3f2412535f4609cfe48R81 is changed from #asWord(#take(4, #take(32, VCallData))) to #asWord(VCallData [ 0 .. 4 ]), because the newer KEVM has most lemmas/reasoning directly over _[_.._].
Third PR merged with dstoken-approve-fail-rough and cat-file-addr-pass-rough: https://github.com/kframework/evm-semantics/pull/897
- New syntax declared which is needed for many of the MCD proofs: #rangeBool, pow208, #WordPack*, #string2Word, and notAddrMask.
Fourth PR is ready, with proofs dai-adduu-fail-rough and vat-deny-diff-fail-rough.
- Proofs were already passing, but improved performance of dai proof from 99s => 48s, and vat proof from 27.2m => 3.2m. This did translate to a performance improvement across the entire k-dss as well.
Running some of the proofs, there is a marked improvement in performance with newer Z3 versions. I was accidentally running version 4.4.1, and running 4.8.6 resulted in many proofs which were infinitely parsing to parse much quicker.
I've setup my local k-dss to use a KEVM submodule directly (but still a globally installed KLab), and to re-use the lemmas there directly, without adding any. We should also make it use a submodule KLab, because the results I have are only valid for my version of KLab (since I've changed some of the term generation process). Currently, on KEVM master, in 7 hours, I have 77% of proofs passing (all within 10minute timeout), 3% timing out (longer than 10 minutes), and the remaining 20% are unknown. On my working branch for KEVM, the performance is further improved, and I have another 7% of the proofs passing within the 10 minute timeout. Performance is vastly improved over original k-dss as far as I can tell, on some proofs as much as 5X faster, only a handful are slower (up to 2X slower in some cases).
As far as I can tell, the end-cage-rough spec does not appear in the staging branch of k-dss, so not sure where it came from, was it added on another branch?

Steps to go from

make spec
make proofs
# klab get-gas SPEC_NAME/HASH (retrieve gas expressions from rough specs)
# klab solve-gas SPEC_NAME/HASH (build gas expressions, this step may not be needed or used actually)
# klab build (sees that there are accepted rough specs with gas expressions, builds the pass proof with exact gas expressions)
# klab prove PASS_SPEC
# klab build (sees that there are accepted pass specs for _lemmas_ of big proofs, so generate spec for big proofs)
# klab prove BIG_SPEC

ehildenb commented 3 years ago

Wednesday August 27, 2020

Done

PR with dai-adduu-fail-rough and vat-deny-diff-fail-rough: https://github.com/kframework/evm-semantics/pull/899
- Improves performance by roughly 40% across the board of 1st-tier specs.
- Drops overall pass rate by about 6% (to 71%), partially due to a flaky failure that happens because of Java stack size.
PR with dai-symbol-pass spec: https://github.com/kframework/evm-semantics/pull/901
- Adds #asByteStackInWidth abstraction (and nthbyteof stubs).
- Fixes a flaky failure we would see with some proofs due to Java stack size running out (have applied a similar patch to my KLab, -Xss=512m).
- 84.2% of rough specs passing within 4.4hrs. 1.8% timing out after 10min.
PR with updated storage model (both KLab generated and manually changed in KEVM regression tests): https://github.com/kframework/evm-semantics/pull/904
- Now instead of having hash2 inequalities as lemmas in verification.k (which were a little broader than needed), we explicitly generate the key inequalities as side-conditions on the generated specifications. I've already modified KLab to do this.
- Still profiling this change across k-dss test-suite, but more proofs are passing, and we see something like 16% performance increase across passing tests, and 22% across all tests. Roughly 88% of those proofs are passing now, and none hit the 10 minute timeout :). Takes about 3.5 hrs to run the rough proofs now.

In Progress

PR with dstoken-transferfrom-fail-rough, dsvalue-read-pass, cat-ilks-pass, flipper-tau-pass, and end-subuu-pass: https://github.com/kframework/evm-semantics/pull/902
- Parsing performance of this proof was really bad at first, dropped from roughly 6min => 1min (using abstract-pre concrete-post storage model and removing some uneeded parens in the side condition).
- Exhibits case where chop could not be simplified.
- More cases of key differences.
- Abstract-pre concrete-post storage model sometimes needs no-op writes simplified out, which this added a lemma for.
- Hashes aren't likely to overflow.
- Make sure bytearrays are all associated the same way.
Changes made so far to klab (go over): https://github.com/makerdao/klab/compare/master...ehildenb:pr
Setting up Firefly on dss repo. Have a couple questions (i) about how dapp test works (RPC?), and (ii) how dapp build works (with paths like ds-auth/auth.sol). We figured this out and were able to get the tests to build with Firefly, now working on actually running the tests with Firefly

ehildenb commented 3 years ago

Wednesday September 2, 2020

PR with dstoken-transferfrom-fail-rough, dsvalue-read-pass, cat-ilks-pass, flipper-tau-pass, and end-subuu-pass: https://github.com/kframework/evm-semantics/pull/902
PR with dstoken-burn-self-fail-rough, flipper-ttl-pass, and vat-addui-fail-rough: https://github.com/kframework/evm-semantics/pull/909. Unfortunately doesn't make vat-addui-fail-rough pass on k-dss repo because the --boundary-cells option on K semantics is breaking it (and KLab uses --boundary-cells k,pr, but also --boundary-cells k,callDepth is not working).
Only recording the REACHPROVED step in the statelog when doing the rough spec (for collecting gas) makes it 30% faster on the rough specs.
Initial generated report: https://sandbox.fireflyblockchain.com/app/report.html?reportId=c3f9b07a-94c9-46ee-a2a2-416535bfc07c
Have a working-ish solution to the staged proof builds going, but having targeted klab build SPEC_NAME would make the whole process much better. Currently we have to recall make spec a bunch of times in the process, which is (i) slow, and (ii) prone to race conditions. If we run only one proof at a time, it's no problem, but running in parallel is what we want to achieve. We should also have klab build-makefile, which builds the entire dependency graph of proofs so that it's easy to run them with a Makefile.

ehildenb commented 3 years ago

Wednesday September 16, 2020

PR which updates the WordPack abstraction to work in more cases without smt-lemma, which makes reasoning easier: https://github.com/kframework/evm-semantics/pull/916
PR which generalizes some of our bool2Word reasoning: https://github.com/kframework/evm-semantics/pull/918
Upcoming PR (waiting on 916) to add more signed arithmetic reasoning: https://github.com/kframework/evm-semantics/pull/913/files
Now we're passing all but Dai_permit_pass_rough (requires an signature recovery), and the rpow proofs (jug and pot).
Now the klab build setup can build individual specs, which takes about 5s per spec. Overall time building specs is worsened (running it 5s per spec rather than all at once), but the improvement in parallelizability/modularity of the test-suite is worth it. The pass_rough and the pass specs are all passing correct now, haven't seen a case where the pass_rough passes, but the pass does not. PR is here: https://github.com/makerdao/klab/pull/5
Added klab make command, for autogenerating a Makefile with proof depenedencies made explicit. With this approach, out of 1011 proofs, we can generated 864 of them, and are passing 813 of them (not including yesterday and todays updates). This process takes about 10 hours running 8 at a time.
Updated Firefly report showing coverage metrics on all contracts (except with hevm.warp tests): https://sandbox.fireflyblockchain.com/app/report.html?reportId=4a3e2109-300b-4640-be2d-6156ed561406
With new approach, only 4 proofs are failing in stage1 (Dai_permit, Pot_rpow, etc...). Able to generate (and prove) all the _pass proofs, and then the next stage of _rough proofs which depend on things like vat_mului...). The next stage of _rough proofs have about a 90% pass rate, but some of them are very slow. I need to check that the lemmas are being used, because I'm not sure. In one case the lemmas were being used, in another they weren't.
Small updates to evm-types/edsl to make things a little simpler: https://github.com/kframework/evm-semantics/pull/921

ehildenb commented 3 years ago

Wednesday September 23, 2020

Fixes to spec sources: https://github.com/makerdao/k-dss/pull/21
Some updates to signed arithmetic lemmas: https://github.com/kframework/evm-semantics/pull/922
Additions to KLab to do individual spec generation: https://github.com/makerdao/klab/pull/5
Arithmetic lemmas: https://github.com/kframework/evm-semantics/pull/923
On KEVM master commit https://github.com/kframework/evm-semantics/commit/4fc3ebfd4a0168f1642b96cf027fa8693714fa01 we have 861 of the 1011 proofs being generated, 767 of them passing in 20 minutes, 86 failing in 20 minutes, and 8 timing out (previous numbers were on mcd-proofs branch). This runs in 6hr10min (8 at a time).
On KEVM branch sarith https://github.com/kframework/evm-semantics/pull/923/commits/6ffa14111450c4c5e94d3f4ea248fe5f03890208 we have 867 of the 1011 proofs being generated, 789 of them passing in 20 minutes, 70 failing in 20 minutes, and 8 timing out. This runs in 5hr52min.
Improve rebuildability of specs using new klab make: https://github.com/makerdao/klab/pull/6
Working on simplifying the gas expressions produced by KLab from pass_rough specs. This includes not evaluating functions like Cmem or Csstore, and then having a more intelligent algorithm for building the gas specs. This seems to improve the performance of the pass_rough specs by about 22% (with state-logging still turned on).