Vincent Laporte

Results 56 issues of Vincent Laporte

There are two implementations: - native, the default one, that assumes that build and host environments have same word sizes; - js, that only works with 32-bit host (suitable when...

ocaml

The pretty-printing to x86 asm is not compatible with recent assemblers. Here is an example program: ~~~ export fn test(reg u64 p) -> reg u128 { reg u128 r; r...

Pre-typing rejects the following program: ~~~ export fn rot(reg u128 x) -> reg u128 { x

bug
type-checking

This is a regression introduced in #847. The following program is no longer accepted by the SCT checker. ~~~ inline fn reset(stack u64 t) { [t] = 0; } export...

bug
constant-time

The following program should be rejected with a nice error message (which one?); it currently crashes. ~~~ inline fn aux(reg u8 x) -> inline int { inline int r; if...

bug

Here is an example of an insecure program: ~~~ inline fn f(reg u64 y x) { if y == x { } } export fn noct(#secret reg u64 x) {...

constant-time

This removes an unnecessary dependency.