mark Int2Bytes(Int,Endianness,Signedness) rules as preserving defined…

…ness (#4522)

Without the annotation, `booster` won't use these rules.
The `/Int` division is partial but harmless in these rules.

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

@@ -2211,12 +2211,12 @@ module BYTES
   imports private INT
 
   rule Int2Bytes(I::Int, E::Endianness, Unsigned) => Int2Bytes((log2Int(I) +Int 8) /Int 8, I, E)
-    requires I >Int 0
+    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)
-    requires I >Int 0
+    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
+    requires I <Int -1 [preserves-definedness]
   rule Int2Bytes(-1, E::Endianness, Signed) => Int2Bytes(1, -1, E)
 endmodule
 ```