search

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

Subsort all step types in mkr-mcd-spec #246

Open ehildenb opened 3 years ago

ehildenb commented 3 years ago

Something like (psuedo-code):

syntax VatStep ::= VatCDPOp VatCDPArgs
syntax VatCDPArgs ::= Address Address String Wad Wad Wad
syntax #args(ADDR1 ADDR2 ILK_ID AM1 AM2 AM3)
 => ListItem(#addr2String(ADDR1)) ListItem(#addr2String(ADDR2)) ....
syntax VatCDPOp ::= "grab" [token] | "frob"

syntax Args ::= VatCDPArgs
syntax Op ::= VatCDPOp

// declare in `kmcd-driver.md`
syntax String ::= #name(Op)
syntax List ::= #args(Op)

syntax #name(grab) => "grab"
// look in domains.md for `Token2String`. #name(OP) => Token2String(OP)