I’ve been taking a look at the Formal Verification that Maker uses and trying to learn more about KEVM and the K language in general.
I’m trying to start (small) and take a look at a simple proof in mkr-authority’s bytes4 support, but I have a few questions regarding the code:
1. Rule for setRoot proof (magic number is bitwise not of 2^160) - how is this number calculated?
rule 115792089237316195423570985007226406215939081747436879206741300988257197096960 &Int X => 0 requires #rangeAddress(X) Lemmas for bytes4 support syntax TypedArg ::= #bytes4( Int )
I found one of the lemmas provided some more information regarding the calculation of the
bytes4 support in the comments - which is calculated from:
(2^32 - 1) * 2^224. How does this derivation work?
syntax Int ::= "maxBytes4" rule maxBytes4 => 115792089210356248756420345214020892766250353992003419616917011526809519390720 [macro] /* (2^32 - 1) * 2^224 */
2. minUint256 value in lemmas
I noticed the
minUint256 gets used when checking the
#getValue lemma. Is the value of a minimum uint256 a constant that’s made accessible by KEVM/K?
syntax Int ::= #getValue ( TypedArg ) [function] rule #getValue(#bytes4( DATA )) => DATA requires minUInt256 <=Int DATA andBool DATA <=Int maxBytes4