correct some return types

formosa-crypto · Feb 18, 2025 · 7a22f64 · 7a22f64
1 parent fdb4f34
commit 7a22f64
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 7 deletions.
diff --git a/code/jasmin/mlkem_ref/mlkem_keccak_ref.jinc b/code/jasmin/mlkem_ref/mlkem_keccak_ref.jinc
@@ -159,9 +159,9 @@ fn _isha3_256_32
 
 #[returnaddress="stack"]
 fn _sha3_512_64
-( #spill_to_mmx reg ptr u8[64] out
+( #spill_to_mmx reg mut ptr u8[64] out
 , reg const ptr u8[64] in
-) -> stack u8[64]
+) -> reg ptr u8[64]
 { stack u64[25] st_s;
   reg ptr u64[25] st;
   reg u64 offset;

diff --git a/code/jasmin/mlkem_ref/poly.jinc b/code/jasmin/mlkem_ref/poly.jinc
@@ -4,7 +4,7 @@ require "reduce.jinc"
 require "mlkem_keccak_ref.jinc"
 require "zetas.jinc"
 
-fn _poly_add2(reg ptr u16[MLKEM_N] rp bp) -> stack u16[MLKEM_N]
+fn _poly_add2(reg mut ptr u16[MLKEM_N] rp, reg const ptr u16[MLKEM_N] bp) -> reg ptr u16[MLKEM_N]
 {
   reg u16 a;
   reg u16 b;
@@ -201,7 +201,7 @@ fn _i_poly_compress(reg ptr u8[MLKEM_POLYCOMPRESSEDBYTES] rp, reg ptr u16[MLKEM_
 }
 
 
-fn _poly_decompress(reg ptr u16[MLKEM_N] rp, reg u64 ap) -> stack u16[MLKEM_N]
+fn _poly_decompress(reg mut ptr u16[MLKEM_N] rp, reg u64 ap) -> reg ptr u16[MLKEM_N]
 {
   reg u8 t;
   reg u16 d0, d1;
@@ -276,7 +276,7 @@ fn _poly_frommont(reg ptr u16[MLKEM_N] rp) -> reg ptr u16[MLKEM_N]
   return rp; 
 }
 
-fn _poly_frommsg(reg ptr u16[MLKEM_N] rp, reg u64 ap) -> stack u16[MLKEM_N]
+fn _poly_frommsg(reg mut ptr u16[MLKEM_N] rp, reg u64 ap) -> reg ptr u16[MLKEM_N]
 {
   reg u8 c;
   reg u16 t;
@@ -338,7 +338,7 @@ fn _poly_frommsg(reg ptr u16[MLKEM_N] rp, reg u64 ap) -> stack u16[MLKEM_N]
 }
 
 
-fn _i_poly_frommsg(reg ptr u16[MLKEM_N] rp, reg ptr u8[32] ap) -> stack u16[MLKEM_N]
+fn _i_poly_frommsg(reg mut ptr u16[MLKEM_N] rp, reg ptr u8[32] ap) -> reg ptr u16[MLKEM_N]
 {
   reg u8 c;
   reg u16 t;

diff --git a/jasmin b/jasmin
+3 −6		.gitlab-ci.yml
+2 −1		CHANGELOG.md
+10 −0		Makefile.compiler
+1 −1		compiler/entry/jasmin2ec.ml
+1 −0		compiler/examples/gimli/proofs/.gitignore
+5 −11		compiler/examples/gimli/proofs/Makefile
+0 −1		compiler/examples/gimli/proofs/ec.config
+0 −17		compiler/examples/gimli/proofs/gimli_ctg.ec
+6 −24		compiler/src/pretyping.ml
+4 −1		compiler/src/toEC.ml
+1 −1		proofs/compiler/load_constants_in_cond.v
+1 −1		proofs/compiler/load_constants_in_cond_proof.v
+2 −2		proofs/compiler/riscv.v
+1 −1		proofs/compiler/riscv_lower_addressing.v
+1 −1		proofs/compiler/riscv_stack_zeroization_proof.v
+1 −1		proofs/compiler/x86_instr_decl.v
+1 −2		proofs/lang/utils.v