Further fine-tune Int2Bytes(Int, Endianness, Signedness) equations …

…for booster (#4533)

The previous change #4522 was insufficient to make the equations usable
in `booster`. Matches with literal `Int` constants will still be
indeterminate, so this PR removes the literals from the rule LHSs.

* Use `0 ==Int I` instead of a syntactic _match_ in the equation for
argument `0`. This enables evaluating terms with `I ==Int 0` in the path
condition.
* Remove equation with literal `-1` and widen requires in equation for
negative arguments (previously `I <Int -1`, now `I <Int 0`). The result
is the same as before with no extra equation required.

k-distribution/include/kframework/builtin/domains.md

@@ -2210,14 +2210,14 @@ module BYTES
   imports BYTES-KORE
   imports private INT
 
+  rule Int2Bytes(I::Int, _::Endianness, _)        => .Bytes
+    requires I ==Int 0
   rule Int2Bytes(I::Int, E::Endianness, Unsigned) => Int2Bytes((log2Int(I) +Int 8) /Int 8, I, E)
     requires I >Int 0 [preserves-definedness]
-  rule Int2Bytes(0, _::Endianness, _) => .Bytes
-  rule Int2Bytes(I::Int, E::Endianness, Signed) => Int2Bytes((log2Int(I) +Int 9) /Int 8, I, E)
+  rule Int2Bytes(I::Int, E::Endianness, Signed  ) => Int2Bytes((log2Int(I) +Int 9) /Int 8, I, E)
     requires I >Int 0 [preserves-definedness]
-  rule Int2Bytes(I::Int, E::Endianness, Signed) => Int2Bytes((log2Int(~Int I) +Int 9) /Int 8, I, E)
-    requires I <Int -1 [preserves-definedness]
-  rule Int2Bytes(-1, E::Endianness, Signed) => Int2Bytes(1, -1, E)
+  rule Int2Bytes(I::Int, E::Endianness, Signed  ) => Int2Bytes((log2Int(~Int I) +Int 9) /Int 8, I, E)
+    requires I <Int 0 [preserves-definedness]
 endmodule
 ```