From 1cd40684278953bbf617a0896c931bc4f8f32834 Mon Sep 17 00:00:00 2001
From: Virgil <25692529+virgil-serbanuta@users.noreply.github.com>
Date: Thu, 13 Jun 2024 09:28:43 +0300
Subject: [PATCH] Remove #distinctBits. (#642)

* Remove #distinctBits.

* Set Version: 0.1.61

* Fix lemma

* Set Version: 0.1.62

---------

Co-authored-by: devops <devops@runtimeverification.com>
Co-authored-by: Jost Berthold <jost.berthold@gmail.com>
---
 package/version                                       |  2 +-
 pykwasm/pyproject.toml                                |  2 +-
 .../src/pykwasm/kdist/wasm-semantics/kwasm-lemmas.md  | 11 ++++++-----
 3 files changed, 8 insertions(+), 7 deletions(-)

diff --git a/package/version b/package/version
index a2d633db7..fbde3d5ae 100644
--- a/package/version
+++ b/package/version
@@ -1 +1 @@
-0.1.61
+0.1.62
diff --git a/pykwasm/pyproject.toml b/pykwasm/pyproject.toml
index d5d3b21f6..0bcb2ac18 100644
--- 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. <contact@runtimeverification.com>",
diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/kwasm-lemmas.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/kwasm-lemmas.md
index 60c658bfa..cfb43da1f 100644
--- 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`: