Skip to content

Releases: runtimeverification/wasm-semantics

v0.1.157: Implement zero-dependency Wasm binary parser (#754)

Choose a tag to compare

@github-actions github-actions released this 30 Jul 07:52
212271b
* update `DataDefn` and `ExternDefn`, fix type annotations

* add binary parser for numbers

* parse modules

* add integrations tests and compare legacy and new parser

* format

* pyupgrade

* organize imports

* fix `<exports>`: migrate to typed export indices

* migrate to the new parser

* add `#instrWithPos` support

* Set Version: 0.1.157

* fix `elem_init` after instrWithPos

* remove unused `BlockMetaData`

* fix `limits` address-type flag bytes for memory64

The i64 (memory64/table64) limit encodings are 0x04/0x05 per the
Wasm 3.0 grammar; 0x02/0x03 are the shared-memory (threads) flags for
i32 and were being misdecoded as i64. Address type is discarded
downstream regardless, so this only affects which flag byte is
recognized as which type.

Adds regression tests covering the i32/i64 limit cases and confirming
the shared-memory flags are now rejected instead of misdecoded.

* fix custom sections not being consumed

parse_custom_section skipped the section id byte but then read_bytes(n, s)
used n (the id, always 0) as the length instead of reading the section's
size:u32 first. This left the stream misaligned after any custom section,
silently dropping every section that followed. Also switch the
"no more custom sections" sentinel from falsy bytes to explicit None,
since an empty-payload custom section is valid and isn't the same as
"not a custom section".

Adds a regression test that builds raw bytes with custom sections
interleaved between real sections and confirms the type/function/export
sections still parse correctly.

* add memory.copy and memory.fill opcode parsing

0xFC 10 (memory.copy) and 0xFC 11 (memory.fill) map to the existing
aCopy/aFill K constructs. Their memory index operands are parsed and
discarded, matching the existing memory.size/memory.grow handling,
since the K semantics has a single implicit memory.

Adds parametrized unit tests (zero and multi-byte memidx values, plus
a trailing sentinel byte) proving the parser consumes exactly the
memidx operands rather than a fixed byte count, and exercises both
opcodes through the full K interpreter via instrs.wat.

* fix binary parser to reject trailing data after module end

parse_module never checked that the input stream was fully consumed, so
an unrecognized section id or garbage appended after a well-formed
module was silently ignored instead of raising a parse error.

* remove unused iterate combinator from binary parser

Dead code: nothing in the parser calls it, and its broad exception
swallow (WasmParseError | IndexError | ValueError) risked masking
real bugs if it were ever reused.

* raise WasmParseError instead of ValueError on func/code length mismatch

zip(function_section, code_section, strict=True) surfaced a bare
Python ValueError on mismatch, unlike every other malformed-input
path in the parser, which raises WasmParseError.

* fix peek_bytes to restore stream position on partial-EOF read

reset(pos, s) only ran on the success path, so a short read at EOF
(fewer than n bytes remaining but more than zero) left the stream
advanced past the bytes it consumed while trying, violating peek's
no-side-effects contract.

* fix parsing of if instructions without an else branch

'if bt in* end' is a valid encoding that omits the 0x05 else opcode;
the parser only handled the explicit-else form and raised
'Unsupported opcode: 0x0b' on the then-branch terminator.

* reject non-zero memory indices instead of silently using memory 0

The K semantics models a single memory; multi-memory support is future
work. Previously the memory index was parsed and discarded in memarg,
memory.size/grow/copy/fill, active data segments, and memory exports,
so a valid multi-memory module would silently execute against memory 0.
Now memidx raises WasmParseError on any index other than 0.

* improve comment clarity in binary parser unit tests

Explain the constructed bytecode in TestCustomSections and
TestFuncCodeLengthMismatch, state the sentinel-byte contract once at
class level instead of four times, explain why the shared-memory limit
flags 0x02/0x03 must be rejected, note the intent behind the LEB128
boundary values, and untangle the peek_bytes test comment.

* scope the recursion limit to run_module and clean up dead code

sys.setrecursionlimit(1500000000) was an import-time side effect
inherited from the 2020 py-wasm-era script, and the value effectively
disabled Python's recursion guard. The limit is only needed because pyk
serializes kore terms recursively (pyk.kore.syntax.Pattern.write) and
the depth grows with module size: basic-features.wat needs about 4000,
while the default 1000 is enough for everything else. Set 20000 inside
run_module, never lowering an externally raised limit.

Also remove an assert made dead by check=True and a try/except that
re-raised as a bare Exception, hiding the original exception type.

* reject unsupported 64-bit addressing and non-funcref table imports

The limits parser decoded the memory64/table64 flags (0x04/0x05) and
returned the i64 address type, which every caller discarded; a table
import's reference type was likewise parsed and dropped since the K
ImportDefn sort has no reftype slot. In both cases a valid module using
the feature would silently execute with wrong (32-bit / funcref)
semantics. The K AST cannot represent either feature, so raise a parse
error instead, keeping the spec-correct handling in place as
commented-out skeleton for future support.

* improve parse error reporting and exception hygiene

Magic and version checks no longer rely on assert (stripped under
python -O) and report expected vs. actual bytes; invalid UTF-8 in a
name raises WasmParseError instead of leaking UnicodeDecodeError; the
blocktype error names the unsupported type-index (i33) form; and the
0xFC handler catches WasmParseError instead of Exception so internal
errors are not disguised as parse errors. No accept/reject behavior
changes.

* turn version-bump CI job into a check instead of auto-commit

* update uv lock

* remove obsolete unit test file `test_wasm2kast.py`

---------

Co-authored-by: devops <devops@runtimeverification.com>

v0.1.156: Update dependency: deps/k_release (#763)

Choose a tag to compare

@github-actions github-actions released this 31 May 14:23
194cccd
* deps/k_release: Set Version 7.1.324

* Set Version: 0.1.156

* pykwasm/: sync uv files 7.1.324

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

* deps/k_release: Set Version 7.1.325

* pykwasm/: sync uv files 7.1.325

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

* deps/k_release: Set Version 7.1.326

* deps/k_release: Set Version 7.1.327

* pykwasm/: sync uv files 7.1.327

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

* deps/k_release: Set Version v7.1.328

* deps/k_release: Set Version 7.1.328

* pykwasm/: sync uv files 7.1.328

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

* deps/k_release: Set Version 7.1.329

* pykwasm/: sync uv files 7.1.329

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

---------

Co-authored-by: devops <devops@runtimeverification.com>

v0.1.155: Update py-wasm dependency to 0.3.1 (#762)

Choose a tag to compare

@github-actions github-actions released this 21 May 19:20
bd5cbe7
* Update py-wasm: `0.3.0 = 0.3.1`

* Set Version: 0.1.155

* update uv.lock

---------

Co-authored-by: devops <devops@runtimeverification.com>

v0.1.154: Update dependency: deps/k_release (#760)

Choose a tag to compare

@github-actions github-actions released this 12 May 18:47
8701ee2
* deps/k_release: Set Version 7.1.323

* Set Version: 0.1.154

* pykwasm/: sync uv files 7.1.323

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

---------

Co-authored-by: devops <devops@runtimeverification.com>

v0.1.153: Update dependency: deps/k_release (#759)

Choose a tag to compare

@github-actions github-actions released this 10 May 23:59
6fecaa4
* deps/k_release: Set Version 7.1.322

* Set Version: 0.1.153

* pykwasm/: sync uv files 7.1.322

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

---------

Co-authored-by: devops <devops@runtimeverification.com>

v0.1.152: Update dependency: deps/k_release (#758)

Choose a tag to compare

@github-actions github-actions released this 08 May 18:02
5c6510f
* deps/k_release: Set Version 7.1.321

* Set Version: 0.1.152

* pykwasm/: sync uv files 7.1.321

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

---------

Co-authored-by: devops <devops@runtimeverification.com>

v0.1.151: Update dependency: deps/k_release (#757)

Choose a tag to compare

@github-actions github-actions released this 29 Apr 13:59
b66db69
* deps/k_release: Set Version 7.1.319

* Set Version: 0.1.151

* pykwasm/: sync uv files 7.1.319

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

---------

Co-authored-by: devops <devops@runtimeverification.com>

v0.1.150: Update dependency: deps/k_release (#756)

Choose a tag to compare

@github-actions github-actions released this 15 Apr 14:50
5ce9140
* deps/k_release: Set Version 7.1.318

* Set Version: 0.1.150

* pykwasm/: sync uv files 7.1.318

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

---------

Co-authored-by: devops <devops@runtimeverification.com>

v0.1.149

Choose a tag to compare

@github-actions github-actions released this 09 Apr 08:28
8d9ba33
Annotate Wasm AST nodes (`Instr`s) with bytecode position metadata fo…

v0.1.148: Remove Gitcoin Grant support section from README (#750)

Choose a tag to compare

@github-actions github-actions released this 24 Mar 18:26
4374213
* Remove Gitcoin Grant support section from README

Removed contribution link to Gitcoin Grant from README.

* Set Version: 0.1.148

---------

Co-authored-by: devops <devops@runtimeverification.com>