Merge branch 'master' into sparse-bytes-lemmas

Author: virgil-serbanuta

deps/k_release

@@ -1 +1 @@
-7.1.30
+7.1.38

flake.lock

@@ -2,17 +2,16 @@
   description = "K Semantics of WebAssembly";
 
   inputs = {
-    k-framework.url = "github:runtimeverification/k/v7.1.30";
+    k-framework.url = "github:runtimeverification/k/v7.1.38";
     nixpkgs.follows = "k-framework/nixpkgs";
     flake-utils.follows = "k-framework/flake-utils";
     rv-utils.follows = "k-framework/rv-utils";
-    pyk.url = "github:runtimeverification/k/v7.1.30?dir=pyk";
-    nixpkgs-pyk.follows = "pyk/nixpkgs";
+    pyk.url = "github:runtimeverification/k/v7.1.38?dir=pyk";
     poetry2nix.follows = "pyk/poetry2nix";
   };
 
   outputs =
-    { self, k-framework, nixpkgs, flake-utils, rv-utils, pyk, ... }@inputs:
+    { self, k-framework, nixpkgs, flake-utils, rv-utils, pyk, poetry2nix }:
     let
       overlay = (final: prev:
         let
@@ -23,26 +22,15 @@
           ] ./.);
 
           version = self.rev or "dirty";
-
-          nixpkgs-pyk = import inputs.nixpkgs-pyk {
-            system = prev.system;
-            overlays = [ pyk.overlay ];
-          };
-
-          python310-pyk = nixpkgs-pyk.python310;
-
-          poetry2nix = inputs.poetry2nix.lib.mkPoetry2Nix { pkgs = nixpkgs-pyk; };
         in {
-          pyk = pyk.packages.${prev.system}.pyk;
-
           kwasm = prev.stdenv.mkDerivation {
             pname = "kwasm";
             inherit src version;
 
-            buildInputs = with final; [
+            buildInputs = with prev; [
               k-framework.packages.${system}.k
               final.kwasm-pyk 
-              python310-pyk
+              python310
             ];
 
             nativeBuildInputs = [ prev.makeWrapper ];
@@ -69,29 +57,33 @@
             '';
           };
 
-          kwasm-pyk = poetry2nix.mkPoetryApplication {
-            python = nixpkgs-pyk.python310;
+          kwasm-pyk = prev.poetry2nix.mkPoetryApplication {
+            python = prev.python310;
             projectDir = ./pykwasm;
-            overrides = poetry2nix.overrides.withDefaults
-            (finalPython: prevPython: {
-              pyk = nixpkgs-pyk.pyk-python310;
-              pygments = prevPython.pygments.overridePythonAttrs ( old: {
-                buildInputs = (old.buildInputs or [ ])
-                  ++ [ prevPython.hatchling ];
-              });
-              xdg-base-dirs = prevPython.xdg-base-dirs.overridePythonAttrs
-                (old: {
-                  propagatedBuildInputs = (old.propagatedBuildInputs or [ ])
-                    ++ [ finalPython.poetry ];
-                });
-              py-wasm = prevPython.py-wasm.overridePythonAttrs
-                (
-                  old: {
-                    buildInputs = (old.buildInputs or [ ]) ++ [ prevPython.setuptools ];
-                  }
-                );
+
+            overrides = prev.poetry2nix.overrides.withDefaults
+              (finalPython: prevPython: {
+                pyk = prev.pyk-python310;
+
+                pygments = prevPython.pygments.overridePythonAttrs
+                  (old: {
+                    buildInputs = (old.buildInputs or [ ])
+                      ++ [ prevPython.hatchling ];
+                    });
+
+                xdg-base-dirs = prevPython.xdg-base-dirs.overridePythonAttrs
+                  (old: {
+                    propagatedBuildInputs = (old.propagatedBuildInputs or [ ])
+                      ++ [ finalPython.poetry ];
+                  });
+
+                py-wasm = prevPython.py-wasm.overridePythonAttrs
+                  (old: {
+                    buildInputs = (old.buildInputs or [ ])
+                      ++ [ prevPython.setuptools ];
+                  });
               });
-            groups = [ ];
+
             checkGroups = [ ];
           };
 
@@ -108,11 +100,11 @@
               git
             ];
 
-            patchPhase = ''
+            patchPhase = with final; ''
               substituteInPlace Makefile                                                  \
-                --replace-fail '$(TEST)'        '${final.kwasm}/bin/kwasm'                \
-                --replace-fail '$(KDIST)'       '${nixpkgs-pyk.pyk-python310}/bin/kdist'  \
-                --replace-fail '$(SOURCE_DIR)'  '${final.kwasm}/wasm-semantics/source'
+                --replace-fail '$(TEST)'        '${kwasm}/bin/kwasm'                \
+                --replace-fail '$(KDIST)'       '${pyk-python310}/bin/kdist'  \
+                --replace-fail '$(SOURCE_DIR)'  '${kwasm}/wasm-semantics/source'
             '';
 
             buildPhase = ''
@@ -137,7 +129,11 @@
       let
         pkgs = import nixpkgs {
           inherit system;
-          overlays = [ overlay ];
+          overlays = [
+            poetry2nix.overlays.default
+            pyk.overlay
+            overlay
+          ];
         };
       in {
         packages = rec {

flake.nix

@@ -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>

media/201903-report-chalmers.md

@@ -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>

media/memory-demo/memory-spec.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>

media/memory-demo/wasm.k

@@ -1 +1 @@
-0.1.71
+0.1.73

package/version

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "pykwasm"
-version = "0.1.71"
+version = "0.1.73"
 description = ""
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",
@@ -23,7 +23,7 @@ wasm-semantics = "pykwasm.kdist.plugin"
 python = "^3.10"
 cytoolz = "^0.12.1"
 numpy = "^1.24.2"
-kframework = "7.1.30"
+kframework = "7.1.38"
 py-wasm = { git = "https://github.com/runtimeverification/py-wasm.git", tag="0.2.1" }
 
 [tool.poetry.group.dev.dependencies]