Preserve definedness in more cases (#2226)

* evm-types: marke ^Word as total * evm.md: marke SSTORE rule as preserving definedness * Set Version: 1.0.398 * Set Version: 1.0.399 * Set Version: 1.0.400 --------- Co-authored-by: devops <[email protected]> Co-authored-by: Andrei Văcaru <[email protected]>
runtimeverification · Dec 19, 2023 · 576b3cd · 576b3cd
1 parent b50a246
commit 576b3cd
Show file tree

Hide file tree

Showing 5 changed files with 6 additions and 5 deletions.
diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.399"
+version = "1.0.400"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py
@@ -6,4 +6,4 @@
     from typing import Final
 
 
-VERSION: Final = '1.0.399'
+VERSION: Final = '1.0.400'
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md
@@ -105,8 +105,8 @@ The helper `powmod` is a totalization of the operator `_^%Int__` (which comes wi
 `_^%Int__` is not defined when the modulus (third argument) is zero, but `powmod` is.
 
 ```k
-    syntax Int ::= Int "^Word" Int       [function]
-    syntax Int ::= powmod(Int, Int, Int) [function, total]
+    syntax Int ::= Int "^Word" Int       [function, total]
+                 | powmod(Int, Int, Int) [function, total]
  // ------------------------------------------------------
     rule W0 ^Word W1 => powmod(W0, W1, pow256)
 

diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md
@@ -1214,6 +1214,7 @@ These rules reach into the network state and load/store from account storage:
            <storage> STORAGE => STORAGE [ INDEX <- NEW ] </storage>
            ...
          </account>
+      [preserves-definedness]
 ```
 
 ### Call Operations

diff --git a/package/version b/package/version
@@ -1 +1 @@
-1.0.399
+1.0.400
Original file line number	Diff line number	Diff line change
Expand Up		@@ -6,4 +6,4 @@
		from typing import Final


		VERSION: Final = '1.0.399'
		VERSION: Final = '1.0.400'