Investigate unexpected branch splitting for some rules during opcode summarization.

[Stevengre]

Changes in evm.md in PR #2727 are introduced due to unexpected remainder caused by the previous rules.

During the summarization for BALANCE, rules ->

    rule <k> #access [ OP , AOP ] => #gasAccess(SCHED, AOP) ~> #deductGas ... </k>
         <schedule> SCHED </schedule>
      requires Ghasaccesslist << SCHED >> andBool #usesAccessList(OP)
    rule <k> #access [ _ , _ ] => .K ... </k> <schedule> _ </schedule> [owise]

will generate a correct branch with Ghasaccesslist << SCHED >> andBool #usesAccessList(OP) and an unexpected branch with unchanged state and condition of the split source. Finally, the unexpected branch leads to infinite splits for this case.

During summarizing SLOAD and SSTORE, rules ->

    rule <k> #accessStorage ACCT INDEX => .K ... </k>
         <accessedStorage> ... ACCT |-> (TS:Set => TS |Set SetItem(INDEX)) ... </accessedStorage>
         <schedule> SCHED </schedule>
         requires Ghasaccesslist << SCHED >>
         [preserves-definedness]
    rule <k> #accessStorage ACCT INDEX => .K ... </k>
         <accessedStorage> TS => TS[ACCT <- SetItem(INDEX)] </accessedStorage>
         <schedule> SCHED </schedule>
      requires Ghasaccesslist << SCHED >> andBool notBool ACCT in_keys(TS)
    rule <k> #accessStorage _ _ => .K ... </k>
         <schedule> SCHED </schedule>
      requires notBool Ghasaccesslist << SCHED >>

lead to a similar result. For this one, the backend doesn't know these three rules cover all the possibilities, but leave a condition with Ghasaccesslist << SCHED >> andBool ACCT in_keys(TS).