Refactor #isPrecompiledAccount to support non-consecutive accounts

[anvacaru]

The #isPrecompiledAccount check currently uses an upper bound approach, validating addresses in the range [1, UB]. This worked because all precompiled contracts were at consecutive addresses (1-17 for Prague).

EIP-7951 introduces P256VERIFY at address 0x100 (256), breaking the contiguous assumption.

This PR removes the #precompiledAccountsUB and constructs the set of addresses for each schedule instead. #isPrecompiledAccounts(ACCTCODE, SCHEDULE) is updated to check if ACCTCODE is in #precompiledAccountsSet(SCHEDULE).

[ehildenb]

This change was made to speed up #isPrecompiledAccount evaluation dramatically in the case of symbolic accounts: #2328

So I think we would be introducing a performance regression.

maybe we can do something simpler, where we add on orBool clause ot #isPrecompiledAccount, so it doesn't need to do any set comparisons?

[anvacaru]

Oh, right, I forgot. In this case, I will close the PR and add a new isPrecompiledAccount rule in the PR for EIP-7951.

    rule [isPrecompiledAccountOsaka]: #isPrecompiledAccount(256, OSAKA) => true
    rule [isPrecompiledAccount]:      #isPrecompiledAccount(ACCTCODE, SCHED) => 0 <Int ACCTCODE andBool ACCTCODE <=Int #precompiledAccountsUB(SCHED) [owise]

[anvacaru]

Another approach would be to refactor isPrecompiledAccount to work in a similar manner in which schedule constants are looked up.

rule #isPrecompiledAccount(256, OSAKA) => true
rule #isPrecompiledAccount(N, OSAKA)  => #isPrecompiledAccount(N, PRAGUE) requires N =/=Int 256

rule #isPrecompiledAccount(N, PRAGUE) => true requires N >=Int 11 andBool N <=Int 17
rule #isPrecompiledAccount(N, PRAGUE) => #isPrecompiledAccount(N, CANCUN) requires N <Int 11
...

rule #isPrecompiledAccount(_,_) => false[owise]

or define isPrecompiledAccount for each schedule directly.

rule #isPrecompiledAccount(1, DEFAULT) => true
rule #isPrecompiledAccount(2, DEFAULT) => true
rule #isPrecompiledAccount(3, DEFAULT) => true
rule #isPrecompiledAccount(4, DEFAULT) => true

rule #isPrecompiledAccount(1, FRONTIER) => true
rule #isPrecompiledAccount(2, FRONTIER) => true
rule #isPrecompiledAccount(3, FRONTIER) => true
rule #isPrecompiledAccount(4, FRONTIER) => true
...
rule #isPrecompiledAccount(_,_) => false[owise]