Jasmin Lang Jasmin Versions Save

This is a minor release of Jasmin. Here is a brief description of a few of the changes it features.

Programmers no longer need to prove that memory accesses and (direct) array accesses are properly aligned. Jasmin programs have a well-defined semantics even if unaligned accesses occur.

The checker for Constant-Time security is now available as a separate jazzct tool. It also ensures that division and modulo operators may only be used with public arguments.

To better understand register-allocation issues, the new command-line option -pliveness displays the program annotated with liveness information.

The compiler now warns when some variable declarations are not used or shadow any earlier declaration.

Namespaces allow reusing names: two things may have the same name, as long as they belong to different namespaces. This feature can also be abused to reuse implementations, but it is not advised to do so.

Many smaller fixes and additions have also been incorporated in this minor release. Relevant details can be found through the CHANGELOG.

This is a minor release of Jasmin,featuring:

• fixes and improvements to the (still experimental) support for ARMv7 architecture (more intrinsics, better instruction selection, added support for flag combinations);
• array indexing expressions no longer need to be explicitly cast to the int type.

Find out more details in the CHANGELOG.

This is a minor release of Jasmin,featuring:

• a few improvements to the (still experimental) support for ARMv7 architecture;
• fixes to the semantics description of the target architectures;
• literal strings to define global arrays of bytes.

Find out more details in the CHANGELOG.

This is a major release of Jasmin. It contains a few noteworthy changes:

• local functions now use call and ret instructions;
• experimental support for the ARMv7 (i.e., Cortex-M4) architecture;
• a few aspects of the safety checker can be finely controlled through annotations or command-line flags;
• shift and rotation operators have a simpler semantics.

As usual, it also brings in various fixes and improvements, such as bit rotation operators and automatic slicing of the input program.

More details can be found in the CHANGELOG.

This is a minor release of Jasmin. It features a few fixes (e.g., to the semantics of a few x86 instructions) and additions (e.g., x86 instructions for carry-less multiplications). Moreover, it provides improved compatibility with the future major release of the Jasmin compiler (e.g., shift amounts can be explicitly truncated to the word size).

More details can be found in the CHANGELOG.

This is a minor release of Jasmin. It brings in the support of new x86 instructions, of new compound assignments (modulo and division), and, most importantly, many fixes, especially to the safety checker.

(Jasmin 2022.09.2 fixes an oversight in Jasmin 2022.09.1's AUTHORS file.)

More details can be found in the CHANGELOG.

This is the third stable release of Jasmin. It contains the following major improvements:

• a new instruction #randombytes to fill an array with “random” data;
• access to mmx registers;
• support for Windows calling convention, in addition to Linux, with -call-conv {windows|linux};
• else if blocks for readability;
• strict preservation of source-level intrinsics;
• an option to extract all the functions of a file to EasyCrypt;
• many fixes to the extraction to EasyCrypt.

It also brings in other new features, as well as new contributors, many fixes, and various improvements.

More details can be found in the CHANGELOG.

This is the second stable release of Jasmin. It capitalizes on more than two years of active development, so it contains a lot of new features, including breaking ones. Please beware of these breaking changes if you want to upgrade from an older version.

Here is a list of the most salient new features. Please take a look at the changelog for a more detailed and exhaustive list.

• Jasmin features proper internal functions, called subroutines, that are neither inline or export. Breaking change: using fn alone in a function declaration declares a subroutine, not an inline function anymore.
• Two storage modifiers, reg ptr and stack ptr, were introduced to store the address of an array in a register and on the stack, respectively. The main use of reg ptr arrays is to pass stack arrays as arguments to subroutines, since they do not accept stack arrays as arguments directly.
• Global immutable arrays are now supported. A global array must be initialized at the same time it is declared.
• It is now possible to manipulate slices of arrays, called sub-arrays. The concrete syntax is a[pos:len] to specify the slice of array a starting at index pos and of length len. pos and len must be compile-time constants.
• It is now possible to attach annotations to functions and instructions, using #[annotation] or #[annotation=value]. The compiler takes into account the ones that it knows about, and ignores the others.
• Including a Jasmin file in another one is now a native feature of Jasmin. The concrete syntax is require "file.jazz" or from ident require "file.jazz" for more complex use cases.
• Boolean flags and some combinations thereof can now be referred to by their names, improving readability.
• Variable declarations don't have to be at the start of the function body anymore, they can now appear anywhere in the body.
• The compiler includes a type-checker for cryptographic constant time that infers security types for functions, based on the security annotations given by the user. This is an alternative to using the constant time extraction to EasyCrypt. The type-checker should be easier to use in most cases.

If you are not interested in the Coq part of Jasmin, you can download the archive jasmin-compiler-v2022.04.0.tar.bz2 below which contains only OCaml code. See the installation instructions for more details.

This is the first stable release of Jasmin.