Rule coverage and configuration well-formedness

[PetarMax]

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

[palinatolmach]

As suggested by @PetarMax, one approach to solve this would be to introduce a third [owise] rule that would get executed if the configuration is not well-formed, which can result in some informative message to the user suggesting that ACCT should be present when #checkBalanceUnderflow is encountered.