Relax k dependency and rename conflicting variables for Skribe compatibility (#731)

* use caret requirement

* ID => IDENT

* poetry lock

* MOD => MDL

* SUB => SUBSTR

* downgrade k

* Set Version: 0.1.131

* pykwasm/: sync poetry files 7.1.268

* flake.{nix,lock}: update Nix derivations

---------

Co-authored-by: devops <[email protected]>

Author: bbyalcinkaya

.github/workflows/update-version.yml

@@ -42,7 +42,7 @@ jobs:
       - name: 'Update pyk release tag'
         run: |
           K_VERSION=$(cat deps/k_release)
-          sed -i 's!kframework = "[v0-9\.]*"!kframework = "'${K_VERSION}'"!' pykwasm/pyproject.toml
+          sed -i 's!kframework = "^[v0-9\.]*"!kframework = "'^${K_VERSION}'"!' pykwasm/pyproject.toml
           poetry -C pykwasm update
           git add pykwasm/ && git commit -m "pykwasm/: sync poetry files ${K_VERSION}" || true
       - name: 'Update Nix flake inputs'

package/version

@@ -1 +1 @@
-0.1.130
+0.1.131

pykwasm/poetry.lock

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

pykwasm/pyproject.toml

@@ -277,11 +277,11 @@ This rule handles adding an `OptionalId` as a map key, but only when it is a pro
     syntax Map  ::= #saveId    (Map, OptionalId, Int) [function, total]
     syntax Bool ::= #canSaveId (Map, OptionalId)      [function, total]
  // -------------------------------------------------------
-    rule #saveId (MAP, ID:OptionalId, _)   => MAP             requires notBool isIdentifier(ID)
-    rule #saveId (MAP, ID:Identifier, IDX) => MAP [ID <- IDX]
+    rule #saveId (MAP, IDENT:OptionalId, _)   => MAP             requires notBool isIdentifier(IDENT)
+    rule #saveId (MAP, IDENT:Identifier, IDX) => MAP [IDENT <- IDX]
 
-    rule #canSaveId (_,   ID:OptionalId) => true                     requires notBool isIdentifier(ID)
-    rule #canSaveId (MAP, ID:Identifier) => notBool ID in_keys(MAP)
+    rule #canSaveId (_,   IDENT:OptionalId) => true                     requires notBool isIdentifier(IDENT)
+    rule #canSaveId (MAP, IDENT:Identifier) => notBool IDENT in_keys(MAP)
 ```
 
 `Int` is the basic form of index, and indices always need to resolve to integers.

pykwasm/src/pykwasm/kdist/wasm-semantics/data.md

@@ -80,8 +80,8 @@ module SPARSE-BYTES
      andBool size(SBI) <=Int S
 
   rule substrSparseBytes(SBChunk(SBI) REST, S, E)
-    => #let SUB = substrSBItem(SBI, S, E)
-       #in SUB substrSparseBytes(REST, 0, E -Int size(SBI))
+    => #let SUBSTR = substrSBItem(SBI, S, E)
+       #in SUBSTR substrSparseBytes(REST, 0, E -Int size(SBI))
     requires 0 <=Int S andBool S <=Int E
      andBool size(SBI) >Int S
 

pykwasm/src/pykwasm/kdist/wasm-semantics/data/sparse-bytes.k

@@ -211,8 +211,8 @@ We allow 2 kinds of actions:
     rule <instrs> ( invoke ENAME:WasmString .Instrs ) => invoke CUR ENAME ... </instrs>
          <curModIdx> CUR </curModIdx>
 
-    rule <instrs> ( invoke ID:Identifier ENAME:WasmString .Instrs ) => invoke MODIDX ENAME ... </instrs>
-         <moduleIds> ... ID |-> MODIDX ... </moduleIds>
+    rule <instrs> ( invoke IDENT:Identifier ENAME:WasmString .Instrs ) => invoke MODIDX ENAME ... </instrs>
+         <moduleIds> ... IDENT |-> MODIDX ... </moduleIds>
 
     rule <instrs> invoke MODIDX:Int ENAME:WasmString => ( invoke FUNCADDRS {{ IDX }} orDefault -1 ):Instr ... </instrs>
          <moduleInst>
@@ -226,8 +226,8 @@ We allow 2 kinds of actions:
     rule <instrs> ( get NAME:WasmString ) => get CUR NAME  ... </instrs>
          <curModIdx> CUR </curModIdx>
 
-    rule <instrs> ( get MOD:Identifier NAME:WasmString ) => get MODIDX NAME ... </instrs>
-         <moduleIds> ... MOD |-> MODIDX ... </moduleIds>
+    rule <instrs> ( get MDL:Identifier NAME:WasmString ) => get MODIDX NAME ... </instrs>
+         <moduleIds> ... MDL |-> MODIDX ... </moduleIds>
 
     rule <instrs> get MODIDX:Int NAME:WasmString => VAL ... </instrs>
          <moduleInst>
@@ -254,8 +254,8 @@ We will reference modules by name in imports.
          <nextModuleIdx> NEXT </nextModuleIdx>
       requires NEXT >Int 0
 
-    rule <instrs> ( register S ID:Identifier ) => ( register S IDX ) ... </instrs>
-         <moduleIds> ... ID |-> IDX ... </moduleIds>
+    rule <instrs> ( register S IDENT:Identifier ) => ( register S IDX ) ... </instrs>
+         <moduleIds> ... IDENT |-> IDX ... </moduleIds>
 
     rule <instrs> ( register S:WasmString IDX:Int ) => .K ... </instrs>
          <moduleRegistry> ... .Map => S |-> IDX ... </moduleRegistry>
@@ -372,7 +372,7 @@ Except `assert_return` and `assert_trap`, the remaining rules are directly reduc
     rule <instrs> (assert_malformed  _MOD          _DESC) => .K ... </instrs>
     rule <instrs> (assert_invalid    _MOD          _DESC) => .K ... </instrs>
     rule <instrs> (assert_unlinkable _MOD          _DESC) => .K ... </instrs>
-    rule <instrs> (assert_trap       MOD:ModuleDecl DESC) => sequenceStmts(text2abstract(MOD .Stmts)) ~> #assertTrap DESC ... </instrs>
+    rule <instrs> (assert_trap       MDL:ModuleDecl DESC) => sequenceStmts(text2abstract(MDL .Stmts)) ~> #assertTrap DESC ... </instrs>
 ```
 
 And we implement some helper assertions to help testing.