A new minor version of the Jasmin compiler is available. It features many bug fixes and improvements across many parts of the system.

Changes to the printing of Jasmin programs: annotations have less escaping; variables are declared closer to their first definition.

Changes to the generated assembly: more meta-data about function symbols; global variables are displayed in a more compact way.

Improvements to the documentation about constant-time programming and verification.

Enhancement of the tooling: program meta-data can be exported in machine-readable form; linting is more precise and easier to control; extraction to EasyCrypt targets its latest version; the safety checker no longer overlooks that array indices must not be negative; the constant-time checker has a new language for contracts and offers better control about its output.

Improvements to the Jasmin language: more operators are accepted in array sizes; variable declarations with initialization requires more rigor; a deprecated intrinsic has been removed; redundant zero-extension of primitives is now tolerated (with a warning).

Enhancements to the compiler: several variables with the same name can be spilled in a single function; the heuristic for allocating registers has been changed slightly and is allowed to rename (i.e., copy) arguments and returned values of export functions.

The curious reader is encouraged to read the more detailed CHANGELOG.