Hi!

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
```

Thanks!

Natalie