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

Experiment with simple mkr-mcd-spec specifications #233

Open ehildenb opened 3 years ago

ehildenb commented 3 years ago 
module SPEC

    // Property: Sum_u(Dai_u) == Debt

    claim <k> transact ADMIN MCDSTEP:MCDStep => . ... </k>
          <vat-debt> VAT_DEBT => ?VAT_DEBT' </vat-debt>
          <vat-dai>  VAT_DAIS => ?VAT_DAIS' </vat-dai>
      requires sumDai(keys_list(VAT_DAIS),   VAT_DAIS)   ==Int  VAT_DEBT
       andBool sumDai(keys_list(?VAT_DAIS'), ?VAT_DAIS') ==Int ?VAT_DEBT'

    // Property: Debt == Vice + Sum_{i,u}(debt_{i,u})

    claim <k> transact ADMIN MCDSTEP:MCDStep => . ... </k>
          <vat-vice> VICE => ?VICE' </vat-vice>
          <vat-debt> VAT_DEBT => ?VAT_DEBT' </vat-debt>
          <vat-ilks> VAT_ILKS => ?VAT_ILKS' </vat-ilks>
          <vat-urns> VAT_URNS => ?VAT_URNS' </vat-urns>
      requires VAT_DEBT   ==Int VICE   +Int sumDebts(VAT_URNS,   VAT_ILKS)
       andBool ?VAT_DEBT' ==Int ?VICE' +Int sumDebts(?VAT_URNS', ?VAT_ILKS')

endmodule