Remove MapIntToInt (#649)

* Remove MapIntToInt * Remove the map-int-to-int-file * Set Version: 0.1.64 * Set Version: 0.1.71 --------- Co-authored-by: devops <[email protected]> Co-authored-by: Jost Berthold <[email protected]>
runtimeverification · Jun 27, 2024 · b353017 · b353017
1 parent 91f83ca
commit b353017
Show file tree

Hide file tree

Showing 10 changed files with 33 additions and 496 deletions.
diff --git a/media/201903-report-chalmers.md b/media/201903-report-chalmers.md
@@ -800,7 +800,7 @@ This is the full definition of the `(memory.grow)` operation:
                    #then SIZE
                    #else -1
                  #fi ... </k>
-         <memAddrs> wrap(0) Int2Int|-> wrap(ADDR) </memAddrs>
+         <memAddrs> 0 |-> ADDR </memAddrs>
          <memInst>
            <memAddr> ADDR  </memAddr>
            <mmax>    MAX  </mmax>

diff --git a/media/memory-demo/memory-spec.k b/media/memory-demo/memory-spec.k
@@ -2,14 +2,14 @@ module MEMORY-SPEC
   imports WASM
 
   rule <k> ( memory.size ) => (i32.const SZ) ... </k>
-      <memAddrs> wrap(0) Int2Int|-> wrap(A) </memAddrs>
+      <memAddrs> 0 |-> A </memAddrs>
       <memInst>
         <memAddr> A </memAddr>
         <memSize> SZ </memSize>
       </memInst>
 
   rule <k> (memory.grow (i32.const X)) => (i32.const SZ) ...</k>
-      <memAddrs> wrap(0) Int2Int|-> wrap(A) </memAddrs>
+      <memAddrs> 0 |-> A </memAddrs>
       <memInst>
         <memAddr> A </memAddr>
         <memSize> SZ => (SZ +Int X) </memSize>
@@ -21,7 +21,7 @@ module MEMORY-SPEC
       andBool SZ >=Int 0
 
   rule <k> (memory.grow (i32.const X)) => (i32.const -1) ...</k>
-      <memAddrs> wrap(0) Int2Int|-> wrap(A) </memAddrs>
+      <memAddrs> 0 |-> A </memAddrs>
       <memInst>
         <memAddr> A </memAddr>
         <memSize> SZ </memSize>

diff --git a/media/memory-demo/wasm.k b/media/memory-demo/wasm.k
@@ -104,7 +104,7 @@ endmodule
     <spuriousMemoryFail> false </spuriousMemoryFail>
 
     rule <k> (( memory ) ~> ELSE) => ELSE </k>
-         <memAddrs> .MapIntToInt => wrap(0) Int2Int|-> wrap(NEXT) </memAddrs>
+         <memAddrs> .Map => 0 |-> NEXT </memAddrs>
          <nextMemAddr> NEXT => NEXT +Int 1 </nextMemAddr>
          <mems>
            (.Bag =>
@@ -118,7 +118,7 @@ endmodule
     syntax Instr ::= "(" "memory.size" ")"
  // --------------------------------------
     rule <k> ( memory.size ) => ( i32.const SZ ) ... </k>
-         <memAddrs> wrap(0) Int2Int|-> wrap(A) </memAddrs>
+         <memAddrs> 0 |-> A </memAddrs>
          <memInst>
            <memAddr> A  </memAddr>
            <memSize> SZ </memSize>
@@ -131,7 +131,7 @@ endmodule
     rule <k> (memory.grow I:Instr) => I ~> (memory.grow) ... </k>
     rule <k> (memory.grow) => (i32.const SZ) ... </k>
          <stack> < i32 > V : S => S </stack>
-         <memAddrs> wrap(0) Int2Int|-> wrap(A) </memAddrs>
+         <memAddrs> 0 |-> A </memAddrs>
          <memInst>
            <memAddr> A </memAddr>
            <memSize> SZ => SZ +Int V </memSize>

diff --git a/package/version b/package/version
@@ -1 +1 @@
-0.1.70
+0.1.71
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.70"
+version = "0.1.71"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",