mark freshUInt and freshBool as preserving definedness (#159)

* mark freshUInt and freshBool as preserving definedness
Use of #bufStrict is safe in these rules because the argument range is explicitly restricted (and the argument is symbolic anyway)

Author: jberthold

package/version

@@ -1 +1 @@
-0.1.53
+0.1.54

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kontrol"
-version = "0.1.53"
+version = "0.1.54"
 description = "Foundry integration for KEVM"
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

src/kontrol/__init__.py

@@ -5,4 +5,4 @@
 if TYPE_CHECKING:
     from typing import Final
 
-VERSION: Final = '0.1.53'
+VERSION: Final = '0.1.54'

src/kontrol/kdist/foundry.md

@@ -495,6 +495,7 @@ This rule returns a symbolic integer of up to the bit width that was sent as an
       requires SELECTOR ==Int selector ( "freshUInt(uint8)" )
        andBool 0 <Int #asWord(ARGS) andBool #asWord(ARGS) <=Int 32
        ensures 0 <=Int ?WORD andBool ?WORD <Int 2 ^Int (8 *Int #asWord(ARGS))
+       [preserves-definedness]
 ```
 
 #### `freshBool` - Returns a single symbolic boolean.
@@ -509,9 +510,10 @@ This rule returns a symbolic boolean value being either 0 (false) or 1 (true).
 ```{.k .symbolic}
     rule [foundry.call.freshBool]:
          <k> #call_foundry SELECTOR _ => . ... </k>
-         <output> _ => #bufStrict(32, ?WORD) </output>
+         <output> _ => #buf(32, ?WORD) </output>
       requires SELECTOR ==Int selector ( "freshBool()" )
        ensures #rangeBool(?WORD)
+       [preserves-definedness]
 ```
 
 Expecting the next call to revert