lemmas/buf.md, lemmas-no-smt-spec.k: add powByteLen-lt-concrete-false to close asWord-unif-03/04 without asWord-eq-false

Removing the looping asWord-eq-false lemma un-masked a coverage gap: the lemmas-spec
asWord-unif-03/04 claims (#2604) decompose an out-of-range #asWord(B) ==Int CONST via
asWord-eq-num into CONST <Int #powByteLen(N), which must reduce to false. #powByteLen is
[no-evaluators] and #2859 added only the true-direction powByteLen-lt-concrete rule,
leaving the false direction to asWord-eq-false. Add the mutually-exclusive, loop-safe
false-direction companion so the concrete comparison is total, plus a focused regression
claim alongside the existing true-direction test.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Author: ehildenb

kevm-pyk/src/kevm_pyk/kproj/evm-semantics/buf.md

@@ -48,6 +48,13 @@ module BUF
     rule [powByteLen-lt-concrete]: CONST <Int #powByteLen(N) => true
         requires 0 <=Int N andBool CONST <Int 2 ^Int (8 *Int N)
         [simplification, concrete(CONST, N), preserves-definedness]
+    // Companion false-direction: a concrete CONST that does not fit into N bytes is not
+    // less than #powByteLen(N). Together with the rule above this makes the concrete
+    // comparison total. The two requires are mutually exclusive and neither RHS re-exposes
+    // `_ <Int #powByteLen(_)`, so the pair is loop-safe.
+    rule [powByteLen-lt-concrete-false]: CONST <Int #powByteLen(N) => false
+        requires 0 <=Int N andBool 2 ^Int (8 *Int N) <=Int CONST
+        [simplification, concrete(CONST, N), preserves-definedness]
     rule #write(WM, IDX, VAL) => WM [ IDX := #buf(1, VAL) ] [simplification]
 
     rule #bufStrict(SIZE, DATA) => #buf(SIZE, DATA)

tests/specs/functional/lemmas-no-smt-spec.k

@@ -85,4 +85,12 @@ module LEMMAS-NO-SMT-SPEC
     claim [powByteLen-lt-concrete]:
       <k> runLemma ( 31 <Int #powByteLen(32) ) => doneLemma ( true ) ... </k>
 
+    // powByteLen-lt-concrete-false: CONST <Int #powByteLen(N) => false when CONST does
+    // not fit into N bytes. The companion false-direction of the rule above; together they
+    // make the concrete comparison total. Regression for the `asWord-unif-03/04` lemmas-spec
+    // claims, which decompose an out-of-range `#asWord(B) ==Int CONST` into exactly this
+    // comparison and previously relied on the (removed, looping) `asWord-eq-false` to close.
+    claim [powByteLen-lt-concrete-false]:
+      <k> runLemma ( 2 ^Int 160 <Int #powByteLen(16) ) => doneLemma ( false ) ... </k>
+
 endmodule