Remove #distinctBits. (#642)

* Remove #distinctBits. * Set Version: 0.1.61 * Fix lemma * Set Version: 0.1.62 --------- Co-authored-by: devops <[email protected]> Co-authored-by: Jost Berthold <[email protected]>
runtimeverification · Jun 13, 2024 · 1cd4068 · 1cd4068
1 parent 41a08da
commit 1cd4068
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 7 deletions.
diff --git a/package/version b/package/version
@@ -1 +1 @@
-0.1.61
+0.1.62
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.61"
+version = "0.1.62"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/kwasm-lemmas.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/kwasm-lemmas.md
@@ -286,12 +286,13 @@ Bounds on `#getRange`:
 
     rule #getRange(_, _, WIDTH)             <Int MAX => true requires 2 ^Int (8 *Int WIDTH) <=Int MAX                                       [simplification]
     rule #getRange(_, _, WIDTH) <<Int SHIFT <Int MAX => true requires 2 ^Int ((8 *Int WIDTH) +Int SHIFT) <=Int MAX                          [simplification]
-    rule VAL1 +Int VAL2                     <Int MAX => true requires VAL1 <Int MAX andBool VAL2 <Int MAX andBool #distinctBits(VAL1, VAL2) [simplification]
+    rule (#getRange(_, _, WIDTH1) #as VAL1) +Int ((#getRange(_, _, WIDTH2) <<Int SHIFT) #as VAL2) <Int MAX => true
+        requires VAL1 <Int MAX
+          andBool VAL2 <Int MAX
+          andBool WIDTH1 *Int 8 <=Int SHIFT
+          andBool 2 ^Int ((8 *Int WIDTH2) +Int SHIFT) <=Int MAX
+        [simplification]
 
-    syntax Bool ::= #distinctBits ( Int , Int ) [function, no-evaluators]
- // ------------------------------------------------------
-    rule #distinctBits(#getRange(_, _, WIDTH), #getRange(_, _, _) <<Int SHIFT) => true requires WIDTH *Int 8 <=Int SHIFT
-      [simplification]
 ```
 
 `#wrap` over `#getRange`: