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

Solidity Generation Thread #160

Open iamchrissmith opened 4 years ago

iamchrissmith commented 4 years ago

I thought it would be good to have a place where we capture the Solidity output conversation outside the meeting notes issue. Current output notes:

    // 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);

Originally posted by @ehildenb in https://github.com/makerdao/mkr-mcd-spec/issues/22#issuecomment-584471391

iamchrissmith commented 4 years ago

One thing as I dig into this @ehildenb that might make it easier. The randont-test.out file has:

### Solidity
------------

Starting the Solidity, but it does not have a similar closing comment so maybe we have a

### End Solidity

tag so we can more easily grab the solidity.

also what would be the best identifier for each test. From this:

Running: krun --directory .build/defn/llvm /var/folders/bq/n6l0m1pj3s94hpl85c576d9r0000gn/T/tmpimullwdh --term --no-sort-collections --output json --parser cat

I would think it is the last piece: tmpimullwdh

If that is the case, would it be too difficult to put that in the solidity starting tag, something like:

### Solidity
#### ID: tmpimullwdh
------------
iamchrissmith commented 4 years ago

this PR addresses the solidity end block and the ID: https://github.com/makerdao/mkr-mcd-spec/pull/161

gbalabasquer commented 4 years ago

@ehildenb @iamchrissmith we will need to do some variable name changes in the export file, as some capitalised variables enter in conflict with the contract names. If we can also do some other changes will suit better with the deployer base contract we have already implemented reducing the amount of custom code for this repo.

Mandatory:

Vat => vat Vow => vow Cat => cat Pot => pot Flap => flap Flop => flop End => end Spot => spotter (not showed in this example but just in case in some other test is there)

Desired for consistency:

Alice => alice Bobby => bobby ADMIN => admin ANYONE => anyone Flip_gold => goldFlip GemJoin_gold=> goldJoin

I'll see if I find some other cases we need changes.

iamchrissmith commented 4 years ago

@gbalabasquer I created this PR to start to address these: https://github.com/makerdao/mkr-mcd-spec/pull/163

Let me know what you think