jasmin
jasmin copied to clipboard
jasmin-lang
Language for high-assurance and high-speed cryptography
The code and the proof seem too complex. We need to take a close look to know how to improve the current situation.
Branch: glob_array3_slh We allow `#inline` annotation for `if` inside a `for` loop for SCT checking. We need a checker which will ensure that these `inline if`'s are resolved and removed...
VPMULL_16u8 is accepted by the typing and then compiled to an instruction that do not exists. The point is that the instruction exists but has no semantic. The type checking...
I create this issue to have something written down. In pretyping, we have 3 kinds of variables : param, global and local, and it seems to me that the interactions...
Apparently before PR https://github.com/jasmin-lang/jasmin/pull/82, some people were relying on a pattern involving inline functions and `reg ptr` arguments used as a scratchpad. Here is a small example. ``` inline fn...
We were reported a few bugs (https://github.com/jasmin-lang/jasmin/issues/128, https://github.com/jasmin-lang/jasmin/issues/130, https://github.com/jasmin-lang/jasmin/issues/135) of the extraction to EasyCrypt recently, it would be good to have tests for it, because it seems we have none...
Benjamin tried to extract `examples/test_set0.jazz` and to parse the output with EasyCrypt and it appeared that `MOV` was not known as an operator.
In particular, the one reading `cannot expand variable ? (defined at line ?) (the default scale must be used)`. Probably adding the involved `wsize` and/or rephrasing could help.
In the following code ``` fn f (reg const ptr u64[2] a) -> reg u64 { reg u64 res; reg mut ptr u64[2] b; b = a; b[0] = 1;...
# Adding non-inlined `for` loops to Jasmin This RFC proposes the addition of non-inlined `for` loops to Jasmin. Currently, Jasmin supports `while` loops, but `for` loops are always inlined, i.e....
Metadata
Owner
Metadata
Language for high-assurance and high-speed cryptography