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