Skip to content

Commit 22d891a

Browse files
virgil-serbanutavirgil-serbanuta
authored
Merge branch 'master' into sparse-bytes-lemmas
2 parents 8b17c66 + fd9c3f5 commit 22d891a

File tree

14 files changed

+105
-576
lines changed

14 files changed

+105
-576
lines changed

Diff for: ‎deps/k_release

+1-1
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
7.1.30
1+
7.1.38

Diff for: ‎flake.lock

+16-20
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

Diff for: ‎flake.nix

+39-43
Original file line numberDiff line numberDiff line change
@@ -2,17 +2,16 @@
22
description = "K Semantics of WebAssembly";
33

44
inputs = {
5-
k-framework.url = "github:runtimeverification/k/v7.1.30";
5+
k-framework.url = "github:runtimeverification/k/v7.1.38";
66
nixpkgs.follows = "k-framework/nixpkgs";
77
flake-utils.follows = "k-framework/flake-utils";
88
rv-utils.follows = "k-framework/rv-utils";
9-
pyk.url = "github:runtimeverification/k/v7.1.30?dir=pyk";
10-
nixpkgs-pyk.follows = "pyk/nixpkgs";
9+
pyk.url = "github:runtimeverification/k/v7.1.38?dir=pyk";
1110
poetry2nix.follows = "pyk/poetry2nix";
1211
};
1312

1413
outputs =
15-
{ self, k-framework, nixpkgs, flake-utils, rv-utils, pyk, ... }@inputs:
14+
{ self, k-framework, nixpkgs, flake-utils, rv-utils, pyk, poetry2nix }:
1615
let
1716
overlay = (final: prev:
1817
let
@@ -23,26 +22,15 @@
2322
] ./.);
2423

2524
version = self.rev or "dirty";
26-
27-
nixpkgs-pyk = import inputs.nixpkgs-pyk {
28-
system = prev.system;
29-
overlays = [ pyk.overlay ];
30-
};
31-
32-
python310-pyk = nixpkgs-pyk.python310;
33-
34-
poetry2nix = inputs.poetry2nix.lib.mkPoetry2Nix { pkgs = nixpkgs-pyk; };
3525
in {
36-
pyk = pyk.packages.${prev.system}.pyk;
37-
3826
kwasm = prev.stdenv.mkDerivation {
3927
pname = "kwasm";
4028
inherit src version;
4129

42-
buildInputs = with final; [
30+
buildInputs = with prev; [
4331
k-framework.packages.${system}.k
4432
final.kwasm-pyk
45-
python310-pyk
33+
python310
4634
];
4735

4836
nativeBuildInputs = [ prev.makeWrapper ];
@@ -69,29 +57,33 @@
6957
'';
7058
};
7159

72-
kwasm-pyk = poetry2nix.mkPoetryApplication {
73-
python = nixpkgs-pyk.python310;
60+
kwasm-pyk = prev.poetry2nix.mkPoetryApplication {
61+
python = prev.python310;
7462
projectDir = ./pykwasm;
75-
overrides = poetry2nix.overrides.withDefaults
76-
(finalPython: prevPython: {
77-
pyk = nixpkgs-pyk.pyk-python310;
78-
pygments = prevPython.pygments.overridePythonAttrs ( old: {
79-
buildInputs = (old.buildInputs or [ ])
80-
++ [ prevPython.hatchling ];
81-
});
82-
xdg-base-dirs = prevPython.xdg-base-dirs.overridePythonAttrs
83-
(old: {
84-
propagatedBuildInputs = (old.propagatedBuildInputs or [ ])
85-
++ [ finalPython.poetry ];
86-
});
87-
py-wasm = prevPython.py-wasm.overridePythonAttrs
88-
(
89-
old: {
90-
buildInputs = (old.buildInputs or [ ]) ++ [ prevPython.setuptools ];
91-
}
92-
);
63+
64+
overrides = prev.poetry2nix.overrides.withDefaults
65+
(finalPython: prevPython: {
66+
pyk = prev.pyk-python310;
67+
68+
pygments = prevPython.pygments.overridePythonAttrs
69+
(old: {
70+
buildInputs = (old.buildInputs or [ ])
71+
++ [ prevPython.hatchling ];
72+
});
73+
74+
xdg-base-dirs = prevPython.xdg-base-dirs.overridePythonAttrs
75+
(old: {
76+
propagatedBuildInputs = (old.propagatedBuildInputs or [ ])
77+
++ [ finalPython.poetry ];
78+
});
79+
80+
py-wasm = prevPython.py-wasm.overridePythonAttrs
81+
(old: {
82+
buildInputs = (old.buildInputs or [ ])
83+
++ [ prevPython.setuptools ];
84+
});
9385
});
94-
groups = [ ];
86+
9587
checkGroups = [ ];
9688
};
9789

@@ -108,11 +100,11 @@
108100
git
109101
];
110102

111-
patchPhase = ''
103+
patchPhase = with final; ''
112104
substituteInPlace Makefile \
113-
--replace-fail '$(TEST)' '${final.kwasm}/bin/kwasm' \
114-
--replace-fail '$(KDIST)' '${nixpkgs-pyk.pyk-python310}/bin/kdist' \
115-
--replace-fail '$(SOURCE_DIR)' '${final.kwasm}/wasm-semantics/source'
105+
--replace-fail '$(TEST)' '${kwasm}/bin/kwasm' \
106+
--replace-fail '$(KDIST)' '${pyk-python310}/bin/kdist' \
107+
--replace-fail '$(SOURCE_DIR)' '${kwasm}/wasm-semantics/source'
116108
'';
117109

118110
buildPhase = ''
@@ -137,7 +129,11 @@
137129
let
138130
pkgs = import nixpkgs {
139131
inherit system;
140-
overlays = [ overlay ];
132+
overlays = [
133+
poetry2nix.overlays.default
134+
pyk.overlay
135+
overlay
136+
];
141137
};
142138
in {
143139
packages = rec {

Diff for: ‎media/201903-report-chalmers.md

+1-1
Original file line numberDiff line numberDiff line change
@@ -800,7 +800,7 @@ This is the full definition of the `(memory.grow)` operation:
800800
#then SIZE
801801
#else -1
802802
#fi ... </k>
803-
<memAddrs> wrap(0) Int2Int|-> wrap(ADDR) </memAddrs>
803+
<memAddrs> 0 |-> ADDR </memAddrs>
804804
<memInst>
805805
<memAddr> ADDR </memAddr>
806806
<mmax> MAX </mmax>

Diff for: ‎media/memory-demo/memory-spec.k

+3-3
Original file line numberDiff line numberDiff line change
@@ -2,14 +2,14 @@ module MEMORY-SPEC
22
imports WASM
33

44
rule <k> ( memory.size ) => (i32.const SZ) ... </k>
5-
<memAddrs> wrap(0) Int2Int|-> wrap(A) </memAddrs>
5+
<memAddrs> 0 |-> A </memAddrs>
66
<memInst>
77
<memAddr> A </memAddr>
88
<memSize> SZ </memSize>
99
</memInst>
1010

1111
rule <k> (memory.grow (i32.const X)) => (i32.const SZ) ...</k>
12-
<memAddrs> wrap(0) Int2Int|-> wrap(A) </memAddrs>
12+
<memAddrs> 0 |-> A </memAddrs>
1313
<memInst>
1414
<memAddr> A </memAddr>
1515
<memSize> SZ => (SZ +Int X) </memSize>
@@ -21,7 +21,7 @@ module MEMORY-SPEC
2121
andBool SZ >=Int 0
2222

2323
rule <k> (memory.grow (i32.const X)) => (i32.const -1) ...</k>
24-
<memAddrs> wrap(0) Int2Int|-> wrap(A) </memAddrs>
24+
<memAddrs> 0 |-> A </memAddrs>
2525
<memInst>
2626
<memAddr> A </memAddr>
2727
<memSize> SZ </memSize>

Diff for: ‎media/memory-demo/wasm.k

+3-3
Original file line numberDiff line numberDiff line change
@@ -104,7 +104,7 @@ endmodule
104104
<spuriousMemoryFail> false </spuriousMemoryFail>
105105

106106
rule <k> (( memory ) ~> ELSE) => ELSE </k>
107-
<memAddrs> .MapIntToInt => wrap(0) Int2Int|-> wrap(NEXT) </memAddrs>
107+
<memAddrs> .Map => 0 |-> NEXT </memAddrs>
108108
<nextMemAddr> NEXT => NEXT +Int 1 </nextMemAddr>
109109
<mems>
110110
(.Bag =>
@@ -118,7 +118,7 @@ endmodule
118118
syntax Instr ::= "(" "memory.size" ")"
119119
// --------------------------------------
120120
rule <k> ( memory.size ) => ( i32.const SZ ) ... </k>
121-
<memAddrs> wrap(0) Int2Int|-> wrap(A) </memAddrs>
121+
<memAddrs> 0 |-> A </memAddrs>
122122
<memInst>
123123
<memAddr> A </memAddr>
124124
<memSize> SZ </memSize>
@@ -131,7 +131,7 @@ endmodule
131131
rule <k> (memory.grow I:Instr) => I ~> (memory.grow) ... </k>
132132
rule <k> (memory.grow) => (i32.const SZ) ... </k>
133133
<stack> < i32 > V : S => S </stack>
134-
<memAddrs> wrap(0) Int2Int|-> wrap(A) </memAddrs>
134+
<memAddrs> 0 |-> A </memAddrs>
135135
<memInst>
136136
<memAddr> A </memAddr>
137137
<memSize> SZ => SZ +Int V </memSize>

Diff for: ‎package/version

+1-1
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
0.1.71
1+
0.1.73

Diff for: ‎pykwasm/poetry.lock

+15-15
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

Diff for: ‎pykwasm/pyproject.toml

+2-2
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
44

55
[tool.poetry]
66
name = "pykwasm"
7-
version = "0.1.71"
7+
version = "0.1.73"
88
description = ""
99
authors = [
1010
"Runtime Verification, Inc. <[email protected]>",
@@ -23,7 +23,7 @@ wasm-semantics = "pykwasm.kdist.plugin"
2323
python = "^3.10"
2424
cytoolz = "^0.12.1"
2525
numpy = "^1.24.2"
26-
kframework = "7.1.30"
26+
kframework = "7.1.38"
2727
py-wasm = { git = "https://github.com/runtimeverification/py-wasm.git", tag="0.2.1" }
2828

2929
[tool.poetry.group.dev.dependencies]

0 commit comments

Comments
 (0)