Release v2.2.0

New Features

• Implemented SIMD execution via eval functions in the reference implementation. The extracted runtime now passes the full Wasm 2.0 test suite. This results in an increase in the secondary version number due to extending the underlying semantics (SIMD representation).

Refactorings and Infrastructural Changes

• Extraction now extracts Coq's String.string to OCaml native string instead of char list. The signature of various interfaces are updated accordingly.
• Extraction now extracts Coq's binary integers (N/Z/positive) to ZArith's BigInt instead. The original conversion functions are therefore deprecated. New conversion functions between ZArith's BigInt and OCaml's native int are added. This is to avoid cyclic dependencies in the parametric SIMD implementations.
• The testing script run_wast.sh and the makefile now support testing a subset of the test suite by passing in a filter argument. For example: make run_wast FILTER="simd" runs only the simd tests.

What's Changed

• SIMD execution by @raoxiaojia in #76

Full Changelog: v2.1.0...v2.2.0

Release 2.1.0

New Features

• Added the tail call feature extension proposal. This has not been tested against the test suite since the reference .wast parser doesn't implement it as part of the standard yet. This results in an increase in the secondary version number due to extending the underlying semantics.

Miscellaneous

• invert_e_typing now deals with thread_typing as well. Some of the old typing inversion code can be simplfied as a result.
• The legacy lookup notation !! in instantiation_properties.v is now removed. Users dependent on this notation can import it from the original stdpp library.

What's Changed

• Tail-call by @raoxiaojia in #73
• Removed legacy iris lookup notation by @raoxiaojia in #74
• memory type class: more properties by @womeier in #75

Full Changelog: v2.0.3...v2.1.0

Release 2.0.3

Release 2.0.3

New Features

• Added support for running .wast format test scripts. The extracted interpreter is now fully conformant with the Wasm official test suite (SIMD excluded). A mirror of the test suite repository is added as a GitHub submodule.
• Added support for passing arguments via the CLI.
• Added support for executing Wasm text format modules (.wat).
• Added an implementation of persistent arrays, adapted from an implementation in the Rocq kernel. The files are located src/Parray and licensed under GNU LGPL 2.1 license due to the original license requirement from the Rocq kernel code.
• Added native support for module import/export across multiple modules without manually saving the store states.
• Added implementation of the new sign extension numeric operation.

Refactorings

• Reworked the memory typeclass and properly encapsulated the provided interfaces; the proofs now only use the exposed interfaces instead of inspecting into the list memory implementation. Added a new vector (dynamic array) implementation of memory based on a parametric array, which is extracted to persistent arrays.

Dependency Updates

• Updated the repository to work with MathComp version 2.x.
• Added a new dependency on the Wasm reference implementation for parsing text format and .wast scripts.

Bugfixes

Parser

• Added utf8 validity check and size checks for names and custom sections in the parser.
• Added a check on requiring the datacount section in the parser.
• Added size bound to the leb128 numerics parsing.
• Fixed a bug where the parser only allows the shortest integer representation for certain leb128-coded arguments.
• Fixed a bug where the arguments of call_indirect were parsed in an incorrect order.
• Fixed a bug where the payloads of nan were parsed incorrectly.
• Prevented cases where the parser could run indefinitely for certain invalid Wasm modules with large length arguments.
• Fixed a bug where certain variants of i64.store instructions were parsed incorrectly.

Type system

• Fixed a bug where the typing of br_table was overly restrictive in unreachable code segments due to the subtyping rules.
• Added several missing cases in the ref field of the typing context generated during instantiation where the original context was overly restrictive.

Others

• Fixed a bug where alloc_module produced incorrect extern values in the export when the module also imports from the host. This bug was introduced during the 2.0 update when the exportinsts field was added to the module instance.
• Fixed several bugs in wrapper functions for CompCert numerics on the sign of infinities and zeros in some edge cases.

Miscellaneous

• Several performance-critical operations involving numerics now go through binary integers instead of nat.
• Added a call stack depth argument in the interpreter for modelling stack exhaustion for .wast test suite.
• Changed extraction of binary-integer-indexed list lookups to a modified function checking for the length first to avoid comparing large binary intergers to nat unnecessarily.

v2.0.2

Release 2.0.2

Upgrade to Coq 8.20

The codebase is now updated to work with Coq 8.20. The other dependencies have also been upgraded correspondingly. Note that we are currently using mathcomp version 1.x; this will possibly be updated in a future version.

New features

• Added implementation of the saturating float-to-int instruction.
• The opsem rules for numeric instructions now require a type checking in addition to the numeric proxy operators (unop/binop/...).
  This type checking is redundant when the type system is enforced. Instead, this change makes the opsem more self-contained as a
  standalone definition.

Refactorings

• The subtyping definitions are now refactored into a standalone file subtyping.v, relocating from operations.v.
• The subtyping relation for function types is now changed to live in Bool instead of Prop due to its full computability.
• A new file definitions.v is added for importing all base definitions of the mechanisation without any proofs. This can be useful for
  developments that only use the mechanised definitions but not the proofs.

Bugfix

• Fixed a bug where the signatures of the returned values are incorrect for certain float-to-int conversions.
• Fixed a bug where the binary parser incorrectly parses the order of arguments of the table.init instruction (should be reversed) and added a corresponding test.
• Fixed a bug where the binary parser incorrectly parses the order of memory arguments after a recent incorrect change (should be reversed) and added a corresponding test.

Feature Improvements

• Reworked the parser to be cleaner and significantly more efficient.
• Improved the error message when an export function with arguments are invoked (currently not supported).

What's Changed

• Updates for Coq 8.20 by @raoxiaojia in #52
• refactor indentation in run_ctx_invoke by @taichimaeda in #57
• Implementation of saturating truncation by @yanjs in #58
• Fix an error in float truncation operations by @yanjs in #60
• 8.20 cleanup by @raoxiaojia in #56
• Strengthen numeric opsems to be independent from type system by @raoxiaojia in #62 (thanks to @hackedy)
• Parser rework by @raoxiaojia in #63

Release 2.0.1

Release 2.0.1

This release is a cumulative update for the repository since the initial release for Wasm 2.0 features, including a bump on the dependency versions (now using Coq 8.19) and several refactorings and feature additions.

Upgrade to Coq 8.19

The codebase is now updated to work with Coq 8.19. The other dependencies have also been upgraded correspondingly.

Context interpreter refactoring

The context interpreter has been refactored to provide a more faithful version of the progress property.

Bugfix for certain numeric operations

The behaviour of shl_s has been fixed according to the spec. Further tests are still required as the numerical part is severely under-tested.

Added opaque implementation of vector instructions (SIMD)

Added the necessary instructions for the new 2.0 SIMD instructions to be parsed but without any concrete implementations. In a future version, add some hooks to the OCaml implementation of the reference interpreter to support concrete SIMD operations.

Binary printer backwards-compatibility

Added an additional check in the binary printer that tries to provide 1.0-compatible binary modules when a Wasm module only used the features from the Wasm 1.0 semantics set.

What's Changed

• remove ITree from dependencies, delete obsolete files by @womeier in #41
• trying to use Wasm 1.0 elem encoding when possible by @raoxiaojia in #43
• Update to Coq 8.19 by @raoxiaojia in #48
• Context interpreter refactors and cleanups by @raoxiaojia in #49
• Testing and fixing numerics shifts and rotations by @raoxiaojia in #45
• Abstract simd memargs by @raoxiaojia in #51

Full Changelog: v2.0...v2.0.1

v2.0

Release 2.0 + Subtyping

This release for Wasm 2.0 + Subtyping implemented the following changes in the official spec release 2.0:

• Multiple-value blocks;
• Reference types;
• Table instructions;
• Multiple tables;
• Bulk memory and table instructions.

In addition, this release also implemented the subtyping system from the future funcref/GC proposals.

The new sign extension, non-trapping float-to-int conversion, and vector types are added but without any concrete implementation.

Updated Components:

• Base opsem/typing definitions;
• Preservation theorems;
• Interpreter and progress theorem;
• Instantiation;
• Instantiation soundness theorems;
• Type checker;
• Type checker correctness theorem;
• Binary printer/parser;
• Code pretty printer;
• Subtyping.

Major Structural Changes

Values vs Instructions

Due to the introduction of reference values, values are no longer necessarily basic instructions; function references and external references are expressed as administrative instructions due to their direct usage of store addresses instead of module indices. This change has broken some assumptions that many original proofs and definitions based on -- mostly those related to value typing (see below).
Total and partial conversion operations are now provided for conversion between values and their corresponding instructions:

• v_to_e/e_to_v for total conversions;
• e_to_v_opt for partial operations.

Value Typing and the Store

Due to the use of store addresses, the new reference values can only be typed given a store. This necessitated the introduction
of a separate value_typing relation with respect to a store. In addition, value typing relation now has to be done at the
e_typing level (for administrative instructions) as they can no longer be converted to basic instructions and typed using the const rule in be_typing. New value typing inversion lemmas were added to help reasoning with this change; search for terms involving value_typing and values_typing.

Threads

Threads are now properly spelt out as a separate type that constitutes the configuration tuple. The old thread-related definitions (e.g. s_typing) are renamed to the names used in the standard (e.g. thread_typing).

Type System and Subtyping

In addition, this release also implements subtyping introduced in the future funcret/GC proposal as a forward-looking move. There is currently no observable effect in Wasm 2.0 except for typing instructions past unconditional branches, as there is no non-trivial subtypings between any of the base value types. There exists a principal type (potentially with some free type parameters) for every value/instruction, which all possible types of it are supertypes of.
The largest impact of this type system change is that, in the future, values can no longer uniquely typed even if it is well typed. This is not the case in Wasm 2.0 yet, but examples can be introduced in future proposals.
The old weakening typing rules are replaced by a subtyping rule as a result of this change, which reflects the shift in the future proposals.

Refactorings and Feature Improvements

Host Formulation

The parametric host language is now defined using typeclasses.
The main major benefit is the automatic filling of implicit host parameter, instead of needing to redefine all operations involving anything downstream from function instances and stores. The proof context is also greatly simplified since all these redefinitions no longer exist to occupy a major chunk of the buffer window.

Numerics

• Refactored the old collection of conversion operations cvtop to be split up by their individual constructors to better match the spec.

Name Changes

• Changed the name of some types, instructions, and constructors to better match the official spec.
• Instance indices are now simplified to the base u32 type without additional constructors.

Pretty Printer

• Implemented pretty printing for conversion operations.

Typing

• Massively improved the scope and automation of the typing inversion lemmas.
• Provided a new tactic resolve_e_typing that automatically tries to resolve e_typing goals, dealing mostly with the operands.
• Provided a separate file for the new subtyping lemmas and tactics.

Type Checker

• Completely reimplemented the type checker, which should now be slightly more efficient (although this should hardly be observable).

Miscellaneous

• Introduced many additional excerpts in comments from the official spec for various definitions.

Bug Fixes

• Fixed a bug where the binary printer incorrectly prints all types of reinterpret conversions to 0xBC.
• Fixed a bug where the binary printer sometimes prints indices via a conversion to nat first.

---

What's Changed

• Wasm 2.0 Update by @raoxiaojia in #39

Full Changelog: v1.0...v2.0

v1.0

Release for Wasm 1.0. This release is published to create a permanent reference for Wasm 1.0 while the master branch moves on to the more recent versions of Wasm.

What's Changed

• Interpreter with improved context representation, and massive context refactoring by @raoxiaojia in #35
• Refactors for composition inversion lemmas and improved typing inversion tactics by @raoxiaojia in #36
• Computable version of inst_typing, and some associated fixes for cl_typing by @raoxiaojia in #37

Full Changelog: 0.2...v1.0