Initial assertions in emitted Solidity

[ehildenb]

• Adds snapshotting to K definition.

• Adds klabel declarations to some important Event in the log, so that we can more easily pull them out in the mcd-pyk.py file.

• Changes the way contracts/addresses are wrapped in the generated solidity output.

• Prints out a minimized state delta as a K rewrite.

• Prints out initial attempt at assertions in the Solidity, now example emitted Solidity looks like:

      // Test Run
  ADMIN.Vat_rely(address(GemJoin_gold));
  ADMIN.Spot_setPrice("gold", 1);
  ADMIN.Flip_gold_rely(address(End));
  ADMIN.Vat_file("Line", 1000000000000);
  ADMIN.Vat_file("spot", "gold", 3000000000);
  ADMIN.Vat_file("line", "gold", 1000000000000);
  ADMIN.Vow_file("bump", 1000000000);
  ADMIN.Vow_file("hump", 0);
  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.GemJoin_gold_join(address(Alice), 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);
  Bobby.Vat_move(address(Bobby), address(Bobby), 135_/Rat_64);
  ADMIN.Pot_file("dsr", 273_/Rat_256);
  hevm.warp(2);
  Bobby.GemJoin_gold_join(address(Bobby), 265_/Rat_64);
  Alice.Vat_hope(address(Alice));
  hevm.warp(2);
  hevm.warp(2);
  
  // Assertions
  assertTrue( Gems.cell() == GemCellMapItem( <gem-id> "gold" </gem-id> , <gem> <gem-id> "gold" </gem-id> <gem-wards> .Set </gem-wards> <gem-balances> GemJoin "gold" |-> 1545 /Rat 64 "Bobby" |-> 375 /Rat 64 "Alice" |-> 10 </gem-balances> </gem> ) );
  assertTrue( Pot.dsr() == 273 /Rat 256 );
  assertTrue( Vat.can() == "Bobby" |-> SetItem( Flip "gold" ) SetItem( End ) SetItem( Pot ) "Alice" |-> SetItem( Flip "gold" ) SetItem( "Alice" ) SetItem( End ) SetItem( Pot ) );
  assertTrue( Vat.gem() == { "gold" , Flip "gold" } |-> 0 { "gold" , "Bobby" } |-> 265 /Rat 64 { "gold" , "Alice" } |-> 0 { "gold" , End } |-> 0 );
  

[iamchrissmith]

I would say lets get this merged in and improve from there, but the assertions example seems to be pretty heavy in the state changes and not quite solidity ready. I'll take a look at how that can be improved.

looks like there is an issue with this change. the jenkins is failing and i get an error locally

[kmbarry1]

Agree w/@iamchrissmith that the assertions will need some massaging, but I don't really see that as a reason to block this PR (except that Jenkins is complaining it can't build, of course).