resources/k.json: assert ACCT_ID is never 0

[asymmetric]

It's never possible for a contract to have address 0, so we shouldn't waste any time exploring this possibility in proofs.

[asymmetric]

@MrChico could we instead change this to requires 10 <=Int ACCTCODE?

[d-xo]

Won't this change just mean that this is explored the proofs for the fail specs instead?

[MrChico]

@MrChico could we instead change this to requires 10 <=Int ACCTCODE?

That's how it was before. We changed it like 2 months ago. For some good reason IIRC. Let me dig it up

[desaperados]

As I recall, we need to allow for zero addresses because there are cases when we do want to check for zero equality on address types (SomeAddressSlot == 0 for example). #notPrecompiledAddress was previously clobbering zero equality checks and was recently updated to avoid this. @asymmetric remember initialize?

[asymmetric]

Yeah OK, I agree that we shouldn't move this check to any of the precompile-checking functions/rules, because 0 is not a precompile address.

To summarize:

• notPrecompileAddress is used to check each storage slot of type address.
• This rule is used to check that the target of a CALL is not a precompile.

[asymmetric]

Won't this change just mean that this is explored the proofs for the fail specs instead?

@xwvvvvwx AFAIK the conditions in k.json are not negated in fail specs.

[asymmetric]

Is this OK to merge?