mark signed load instruction as preserving (#654)

* mark signed load instruction as preserving * Set Version: 0.1.66 * Substitute variable in comment Co-authored-by: Burak Bilge Yalçınkaya <[email protected]> --------- Co-authored-by: devops <[email protected]> Co-authored-by: Burak Bilge Yalçınkaya <[email protected]>
runtimeverification · Jun 21, 2024 · b560628 · b560628
1 parent e563935
commit b560628
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 2 deletions.
diff --git a/package/version b/package/version
@@ -1 +1 @@
-0.1.65
+0.1.66
diff --git a/pykwasm/pyproject.toml b/pykwasm/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "pykwasm"
-version = "0.1.65"
+version = "0.1.66"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md
@@ -1478,6 +1478,11 @@ Sort `Signedness` is defined in module `BYTES`.
       requires (EA +Int #numBytes(WIDTH)) >Int (SIZE *Int #pageSize())
 
     rule <instrs> load { ITYPE WIDTH EA   Signed DATA:SparseBytes } => #chop(< ITYPE > #signed(WIDTH, #getRange(DATA, EA, #numBytes(WIDTH)))) ... </instrs>
+        [preserves-definedness]
+        // #signed(WIDTH, N) is defined for 0 <= N <= #pow(WIDTH)
+        // #pow(WIDTH) == 2 ^ #width(WIDTH) == 2 ^ (#numBytes(WIDTH) * 8)
+        // and #getRange(_, _, SIZE) < 2 ^ (SIZE * 8)
+
     rule <instrs> load { ITYPE WIDTH EA Unsigned DATA:SparseBytes } => < ITYPE > #getRange(DATA, EA, #numBytes(WIDTH)) ... </instrs>
 ```