Definedness improvements (#651)

* total func. IUnop and ExtendS

* br_table definedness

* Set Version: 0.1.64

* make `#minWidth`, `#ctz`, and `#popcnt` total

* `br_table`: add `requires #lenInts(ES) >Int 0`

* updates after review
- return -1 for negative values
- return `undefined` for negative values
- `modInt 2` => `&Int`

* Set Version: 0.1.65

---------

Co-authored-by: devops <[email protected]>

package/version

@@ -1 +1 @@
-0.1.64
+0.1.65

pykwasm/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "pykwasm"
-version = "0.1.64"
+version = "0.1.65"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

pykwasm/src/pykwasm/kdist/wasm-semantics/numeric.md

@@ -115,9 +115,9 @@ module WASM-NUMERIC
 `*UnOp` takes one oprand and returns a `Val`.
 
 ```k
-    syntax Val ::= IValType "." IUnOp   Int   [klabel(intUnOp)    , function]
+    syntax Val ::= IValType "." IUnOp   Int   [klabel(intUnOp)    , function, total]
                  | FValType "." FUnOp   Float [klabel(floatUnOp)  , function]
-                 | IValType "." ExtendS Int   [klabel(extendSUnOp), function]
+                 | IValType "." ExtendS Int   [klabel(extendSUnOp), function, total]
  // ---------------------------------------------------------------------------
 ```
 
@@ -133,21 +133,33 @@ Note: The actual `ctz` operator considers the integer 0 to have *all* zero-bits,
 
 ```k
     rule ITYPE . clz    I1 => < ITYPE > #width(ITYPE) -Int #minWidth(I1)
+      requires 0 <=Int I1
     rule ITYPE . ctz    I1 => < ITYPE > #if I1 ==Int 0 #then #width(ITYPE) #else #ctz(I1) #fi
+      requires 0 <=Int I1
     rule ITYPE . popcnt I1 => < ITYPE > #popcnt(I1)
+      requires 0 <=Int I1
+    rule _:IValType . _:IUnOp I1 => undefined
+      requires I1 <Int 0
 
-    syntax Int ::= #minWidth ( Int ) [function]
-                 | #ctz      ( Int ) [function]
-                 | #popcnt   ( Int ) [function]
+    syntax Int ::= #minWidth ( Int ) [function, total]
+                 | #ctz      ( Int ) [function, total]
+                 | #popcnt   ( Int ) [function, total]
  // -------------------------------------------
-    rule #minWidth(0) => 0
-    rule #minWidth(N) => 1 +Int #minWidth(N >>Int 1)                                 requires N =/=Int 0
-
-    rule #ctz(0) => 0
-    rule #ctz(N) => #if N modInt 2 ==Int 1 #then 0 #else 1 +Int #ctz(N >>Int 1) #fi  requires N =/=Int 0
-
-    rule #popcnt(0) => 0
-    rule #popcnt(N) => #bool(N modInt 2 ==Int 1) +Int #popcnt(N >>Int 1)             requires N =/=Int 0
+    rule #minWidth(N) => 0                                                           requires N ==Int 0
+    rule #minWidth(N) => 1 +Int #minWidth(N >>Int 1)                                 requires N >Int 0
+    rule [minWidth-invalid]:
+         #minWidth(N) => -1                                                          requires N <Int 0
+
+    rule #ctz(N) => 0                                                                requires N ==Int 0
+    rule #ctz(N) => 0                                                                requires N >Int 0 andBool N &Int 1 ==Int 1
+    rule #ctz(N) => 1 +Int #ctz(N >>Int 1)                                           [owise]
+    rule [ctz-invalid]:
+         #ctz(N) => -1                                                               requires N <Int 0
+
+    rule #popcnt(N) => 0                                                             requires N ==Int 0
+    rule #popcnt(N) => #bool(N &Int 1 ==Int 1) +Int #popcnt(N >>Int 1)               requires N >Int 0
+    rule [popcnt-invalid]:
+         #popcnt(N) => -1                                                            requires N <Int 0
 ```
 
 Before we implement the rule for float point numbers, we first need to define a helper function.

pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md

@@ -520,6 +520,12 @@ Note that, unlike in the WebAssembly specification document, we do not need the
  // ---------------------------------------------------------------------
     rule <instrs> #br_table(ES) => #br(#getInts(ES, minInt(VAL, #lenInts(ES) -Int 1))) ... </instrs>
          <valstack> <i32> VAL : VALSTACK => VALSTACK </valstack>
+      requires 0 <=Int VAL
+       andBool #lenInts(ES) >Int 0
+      [preserves-definedness]
+      // preserves-definedness:
+      // - 0 <= VAL and minInt(VAL, #lenInts(ES) -Int 1) ensures #getInts(_) is defined
+
 ```
 
 Finally, we have the conditional and loop instructions.