Rule coverage and configuration well-formedness

The rules for checkBalanceUnderflow:

     rule <k> #checkBalanceUnderflow ACCT VALUE => #refund GCALL ~> #pushCallStack ~> #pushWorldState ~> #end EVMC_BALANCE_UNDERFLOW ... </k>
         <output> _ => .Bytes </output>
         <callGas> GCALL </callGas>
         <account>
           <acctID> ACCT </acctID>
           <balance> BAL </balance>
           ...
         </account>
      requires VALUE >Int BAL

    rule <k> #checkBalanceUnderflow ACCT VALUE => . ... </k>
         <account>
           <acctID> ACCT </acctID>
           <balance> BAL </balance>
           ...
         </account>
      requires VALUE <=Int BAL

only consider configurations in which the account with identifier ACCT is present.

Is this:

• an omission, in the sense that there should be a third rule when the account is not present; or
• a consequence of having a well-formed EVM configuration, in the sense that an account with identifier ACCT must always be present when there is an #checkBalanceUnderflow check?

Perhaps it would be a good idea if we went through the semantics to see if there are other sets of rules that are incomplete in this sense. Is there a way of understanding this automatically, perhaps on definition creation? @ehildenb @jberthold

Review the two checkBalanceUnderflow rules shown in the issue and the surrounding EVM semantics. First determine whether a missing account is permitted in a well-formed configuration, then inspect whether similar rule sets are incomplete. Done means documenting the conclusion and assessing whether definition creation can detect such cases automatically.