jasmin

jasmin copied to clipboard

Is this something useful? Are the options complex enough so that it is worth spending some time on that?

eponier

Non-inlined for loops

1

For loops whose bounds are not constant are not inlined. Consider, for instance: ``` export fn main (reg u64 io) -> reg u64 { inline int i; reg u64 res;...

eponier

In the following code ``` fn f () -> reg u64 { reg u64 r; r = 0; return r; } export fn main (reg u64 x) -> reg u64...

eponier

The storage modifier of the return type of a function is ignored

2

If we compile the following function in the `glob_array3` branch ``` inline fn sum (stack u64[2] a) -> stack u64 { reg u64 r; r = a[0]; r += a[1];...

eponier

Add `ROR` operator similar to `` for right shifts. This will allow us to avoid using intrinsics to get register shifts in ARM.

sarranz

There is a lot of duplication between the specific W8.SHIFT theory and the generic BitWordSH theory. There is an attempt there: ca3785e63d8ae2d1315630c608e7bb6bb1506e33 but that triggers an EasyCrypt bug.

vbgl

Port to MathComp 2

43

Requires https://github.com/jasmin-lang/coqword/pull/22

proux01

Security annotations for the speculative-ct checker are translated (weakened) when handled by the (non-speculative) CT checker.

vbgl

Initialisation at declaration site

5

This is a feature request to have the option to initialize a variable at declaration time, e.g. `reg u64 res = 1;`.

eponier

Remove deprecated legacy interface to the CT checker

2

Let’s make some room for a better interface.

vbgl