diff --git a/package/version b/package/version
index 3a28972df..010fbfb88 100644
--- a/package/version
+++ b/package/version
@@ -1 +1 @@
-0.1.148
+0.1.149
diff --git a/pykwasm/pyproject.toml b/pykwasm/pyproject.toml
index 2cd96eee5..6888c3279 100644
--- a/pykwasm/pyproject.toml
+++ b/pykwasm/pyproject.toml
@@ -4,13 +4,13 @@ build-backend = "hatchling.build"
 
 [project]
 name = "pykwasm"
-version = "0.1.148"
+version = "0.1.149"
 description = ""
 readme = "README.md"
 requires-python = "~=3.10"
 dependencies = [
     "kframework>=7.1.313",
-    "py-wasm@git+https://github.com/runtimeverification/py-wasm.git@0.2.1"
+    "py-wasm@git+https://github.com/runtimeverification/py-wasm.git@0.3.0"
 ]
 
 [[project.authors]]
diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md
index 8470abaff..78f192f75 100644
--- a/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md
+++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md
@@ -332,6 +332,21 @@ Instructions
     rule sequenceInstrs(I IS   ) => I ~> sequenceInstrs(IS)
 ```
 
+### Position-annotated instruction
+
+Helper wrapper to attach source position metadata to instructions for tracing/debugging.
+`offset` is **0-based** and indicates the starting byte position of the instruction in the original Wasm bytecode.
+`length` is the number of bytes the instruction spans.
+
+This constructor has no semantic effect and its execution simply unwraps the annotated instruction.
+The wrapper exists only for tracing and must not interfere with semantics.
+
+```k
+    syntax Instr ::= #instrWithPos(inner: Instr, offset: Int, length: Int)     [symbol(aInstrWithPos)]
+ // ---------------------------------------------------------------------------
+    rule <instrs> #instrWithPos(I, _, _) => I ... </instrs>
+```
+
 ### Traps
 
 `trap` is the error mechanism of Wasm.
diff --git a/pykwasm/src/pykwasm/kwasm_ast.py b/pykwasm/src/pykwasm/kwasm_ast.py
index a818e0a35..27a2b7704 100644
--- a/pykwasm/src/pykwasm/kwasm_ast.py
+++ b/pykwasm/src/pykwasm/kwasm_ast.py
@@ -189,6 +189,11 @@ def global_type(mut: KInner, valtype: KInner) -> KInner:
 # Instrs #
 ##########
 
+
+def INSTR_WITH_POS(instruction: KInner, start: int, end: int) -> KInner:
+    return KApply('aInstrWithPos', [instruction, KInt(start), KInt(end)])
+
+
 ########################
 # Control Instructions #
 ########################
diff --git a/pykwasm/src/pykwasm/wasm2kast.py b/pykwasm/src/pykwasm/wasm2kast.py
index 91cea1ff6..55ea382f5 100644
--- a/pykwasm/src/pykwasm/wasm2kast.py
+++ b/pykwasm/src/pykwasm/wasm2kast.py
@@ -12,6 +12,7 @@
 from wasm import instructions
 from wasm.datatypes import GlobalType, MemoryType, Mutability, TableType, TypeIdx, ValType, addresses
 from wasm.datatypes.element_segment import ElemModeActive, ElemModeDeclarative, ElemModePassive
+from wasm.instructions import InstructionWithPos
 from wasm.opcodes import BinaryOpcode
 from wasm.parsers import parse_module
 
@@ -141,9 +142,12 @@ def elem_mode(m: ElemMode) -> KInner:
 def elem_init(init: tuple[Iterable[BaseInstruction], ...]) -> Iterable[int | None]:
     def expr_to_int(expr: Iterable[BaseInstruction]) -> int | None:
         # 'expr' must be a constant expression consisting of a reference instruction
-        assert len(expr) == 1 or len(expr) == 2 and isinstance(expr[1], instructions.End), expr
+        assert len(expr) == 1 or len(expr) == 2 and expr[1].opcode == BinaryOpcode.END, expr
         instr = expr[0]
 
+        if isinstance(instr, InstructionWithPos):
+            instr = instr.instruction
+
         if isinstance(instr, instructions.RefFunc):
             return instr.funcidx
         if isinstance(instr, instructions.RefNull):
@@ -212,6 +216,9 @@ def instr(i):
     B = BinaryOpcode
     global block_id
     # TODO rewrite 'i.opcode == _' conditions as isinstance for better type-checking
+    if isinstance(i, InstructionWithPos):
+        inner = instr(i.instruction)
+        return a.INSTR_WITH_POS(inner, i.offset, i.length)
     if i.opcode == B.BLOCK:
         cur_block_id = block_id
         block_id += 1
diff --git a/pykwasm/uv.lock b/pykwasm/uv.lock
index ece16d297..b57cd4586 100644
--- a/pykwasm/uv.lock
+++ b/pykwasm/uv.lock
@@ -1,5 +1,5 @@
 version = 1
-revision = 3
+revision = 2
 requires-python = ">=3.10, <4"
 resolution-markers = [
     "python_full_version >= '3.11'",
@@ -432,7 +432,7 @@ name = "exceptiongroup"
 version = "1.3.1"
 source = { registry = "https://pypi.org/simple" }
 dependencies = [
-    { name = "typing-extensions", marker = "python_full_version < '3.13'" },
+    { name = "typing-extensions", marker = "python_full_version < '3.11'" },
 ]
 sdist = { url = "https://files.pythonhosted.org/packages/50/79/66800aadf48771f6b62f7eb014e352e5d06856655206165d775e675a02c9/exceptiongroup-1.3.1.tar.gz", hash = "sha256:8b412432c6055b0b7d14c310000ae93352ed6754f70fa8f7c34141f91c4e3219", size = 30371, upload-time = "2025-11-21T23:01:54.787Z" }
 wheels = [
@@ -1008,8 +1008,8 @@ wheels = [
 
 [[package]]
 name = "py-wasm"
-version = "0.2.0"
-source = { git = "https://github.com/runtimeverification/py-wasm.git?rev=0.2.1#e5fb6ed5b1aebf1c0d67087397b3c1240ff412da" }
+version = "0.3.0"
+source = { git = "https://github.com/runtimeverification/py-wasm.git?rev=0.3.0#07677b120f40b86d5b7839e2dde42889967dcfce" }
 dependencies = [
     { name = "cytoolz", marker = "implementation_name == 'cpython'" },
     { name = "mypy-extensions" },
@@ -1055,7 +1055,7 @@ wheels = [
 
 [[package]]
 name = "pykwasm"
-version = "0.1.146"
+version = "0.1.148"
 source = { editable = "." }
 dependencies = [
     { name = "kframework" },
@@ -1084,7 +1084,7 @@ dev = [
 [package.metadata]
 requires-dist = [
     { name = "kframework", specifier = ">=7.1.313" },
-    { name = "py-wasm", git = "https://github.com/runtimeverification/py-wasm.git?rev=0.2.1" },
+    { name = "py-wasm", git = "https://github.com/runtimeverification/py-wasm.git?rev=0.3.0" },
 ]
 
 [package.metadata.requires-dev]