From 600dfe34352e320024d05f75c99e2c0083589579 Mon Sep 17 00:00:00 2001 From: Manuel Barbosa Date: Tue, 11 Feb 2025 20:06:26 +0000 Subject: [PATCH] Most recent jasmin and jasmin2ec extraction --- code/Makefile.conf | 3 + code/jasmin/mlkem_avx2/extraction/Makefile | 11 +- .../jasmin/mlkem_avx2/extraction/jkem_avx2.ec | 366 ++++++++---------- .../mlkem_avx2_stack/extraction/Makefile | 11 +- .../extraction/jkem_avx2_stack.ec | 347 ++++++++--------- code/jasmin/mlkem_ref/extraction/Makefile | 11 +- code/jasmin/mlkem_ref/extraction/jkem.ec | 155 ++++---- jasmin | 2 +- proof/correctness/MLKEM_InnerPKE.ec | 2 +- proof/correctness/MLKEM_KEM.ec | 16 +- proof/correctness/MLKEM_Poly.ec | 2 +- proof/correctness/avx2/MLKEM_InnerPKE_avx2.ec | 2 +- .../avx2/MLKEM_InnerPKE_avx2_stack.ec | 2 +- proof/correctness/avx2/MLKEM_KEM_avx2.ec | 26 +- .../correctness/avx2/MLKEM_KEM_avx2_stack.ec | 28 +- .../avx2/MLKEM_PolyPolyVec_stack_bridges.ec | 4 +- .../avx2/MLKEM_PolyVec_avx2_vec.ec | 11 +- proof/correctness/avx2/MLKEM_Poly_avx2_vec.ec | 10 +- proof/correctness/avx2/MLKEM_keccak_avx2.ec | 3 +- 19 files changed, 482 insertions(+), 530 deletions(-) diff --git a/code/Makefile.conf b/code/Makefile.conf index ad166fde..e9a0204e 100644 --- a/code/Makefile.conf +++ b/code/Makefile.conf @@ -6,3 +6,6 @@ current_dir := $(dir $(realpath $(lastword $(MAKEFILE_LIST)))) # -------------------------------------------------------------------- JASMIN ?= $(current_dir)/../jasmin/compiler/ JASMINC ?= $(JASMIN)/jasminc -I Keccak:$(current_dir)/../formosa-keccak/src/amd64 +JASMIN2EC ?= JASMINPATH="Keccak=$(current_dir)/../formosa-keccak/src/amd64" $(JASMIN)/jasmin2ec + + diff --git a/code/jasmin/mlkem_avx2/extraction/Makefile b/code/jasmin/mlkem_avx2/extraction/Makefile index 51033d90..fbe7b8dd 100644 --- a/code/jasmin/mlkem_avx2/extraction/Makefile +++ b/code/jasmin/mlkem_avx2/extraction/Makefile @@ -9,11 +9,12 @@ # -------------------------------------------------------------------- all: ec -ec: - $(JASMINC) ../jkem.jazz -oec jkem_avx2.ec \ - -ec jade_kem_mlkem_mlkem768_amd64_avx2_keypair \ - -ec jade_kem_mlkem_mlkem768_amd64_avx2_enc \ - -ec jade_kem_mlkem_mlkem768_amd64_avx2_dec + +ec: + $(JASMIN2EC) ../jkem.jazz --array-model=old -o jkem_avx2.ec \ + -f jade_kem_mlkem_mlkem768_amd64_avx2_keypair \ + -f jade_kem_mlkem_mlkem768_amd64_avx2_enc \ + -f jade_kem_mlkem_mlkem768_amd64_avx2_dec clean: rm -f *.ec diff --git a/code/jasmin/mlkem_avx2/extraction/jkem_avx2.ec b/code/jasmin/mlkem_avx2/extraction/jkem_avx2.ec index d38e80de..f7365b65 100644 --- a/code/jasmin/mlkem_avx2/extraction/jkem_avx2.ec +++ b/code/jasmin/mlkem_avx2/extraction/jkem_avx2.ec @@ -13,7 +13,7 @@ WArray200 WArray224 WArray256 WArray512 WArray536 WArray800 WArray960 WArray1088 WArray1536 WArray2048 WArray2144 WArray4608. abbrev sample_shuffle_table = -(Array2048.of_list witness +((Array2048.of_list witness) [(W8.of_int (-1)); (W8.of_int (-1)); (W8.of_int (-1)); (W8.of_int (-1)); (W8.of_int (-1)); (W8.of_int (-1)); (W8.of_int (-1)); (W8.of_int (-1)); (W8.of_int 0); (W8.of_int (-1)); (W8.of_int (-1)); (W8.of_int (-1)); @@ -535,7 +535,7 @@ abbrev sample_ones = 454086624460063511464984254936031011189294057512315937409637584344757371137). abbrev sample_load_shuffle = -(Array32.of_list witness +((Array32.of_list witness) [(W8.of_int 0); (W8.of_int 1); (W8.of_int 1); (W8.of_int 2); (W8.of_int 3); (W8.of_int 4); (W8.of_int 4); (W8.of_int 5); (W8.of_int 6); (W8.of_int 7); (W8.of_int 7); (W8.of_int 8); (W8.of_int 9); (W8.of_int 10); (W8.of_int 10); @@ -545,7 +545,7 @@ abbrev sample_load_shuffle = (W8.of_int 14); (W8.of_int 14); (W8.of_int 15)]). abbrev gen_matrix_indexes = -(Array32.of_list witness +((Array32.of_list witness) [(W8.of_int 0); (W8.of_int 0); (W8.of_int 1); (W8.of_int 0); (W8.of_int 2); (W8.of_int 0); (W8.of_int 0); (W8.of_int 1); (W8.of_int 1); (W8.of_int 1); (W8.of_int 2); (W8.of_int 1); (W8.of_int 0); (W8.of_int 2); (W8.of_int 1); @@ -555,7 +555,7 @@ abbrev gen_matrix_indexes = (W8.of_int 2); (W8.of_int 1)]). abbrev pvc_shufbidx_s = -(Array32.of_list witness +((Array32.of_list witness) [(W8.of_int 0); (W8.of_int 1); (W8.of_int 2); (W8.of_int 3); (W8.of_int 4); (W8.of_int 8); (W8.of_int 9); (W8.of_int 10); (W8.of_int 11); (W8.of_int 12); (W8.of_int (-1)); (W8.of_int (-1)); (W8.of_int (-1)); (W8.of_int (-1)); @@ -580,7 +580,7 @@ abbrev pvd_mask_s = (W32.of_int 2145394680). abbrev pvd_sllvdidx_s = (W64.of_int 4). abbrev pvd_shufbdidx_s = -(Array32.of_list witness +((Array32.of_list witness) [(W8.of_int 0); (W8.of_int 1); (W8.of_int 1); (W8.of_int 2); (W8.of_int 2); (W8.of_int 3); (W8.of_int 3); (W8.of_int 4); (W8.of_int 5); (W8.of_int 6); (W8.of_int 6); (W8.of_int 7); (W8.of_int 7); (W8.of_int 8); (W8.of_int 8); @@ -592,7 +592,7 @@ abbrev pvd_shufbdidx_s = abbrev pvd_q_s = (W32.of_int 218182660). abbrev cbd_jshufbidx = -(Array32.of_list witness +((Array32.of_list witness) [(W8.of_int 0); (W8.of_int 1); (W8.of_int 2); (W8.of_int (-1)); (W8.of_int 3); (W8.of_int 4); (W8.of_int 5); (W8.of_int (-1)); (W8.of_int 6); (W8.of_int 7); (W8.of_int 8); (W8.of_int (-1)); (W8.of_int 9); @@ -603,14 +603,14 @@ abbrev cbd_jshufbidx = (W8.of_int 15); (W8.of_int (-1))]). abbrev pfm_idx_s = -(Array16.of_list witness +((Array16.of_list witness) [(W8.of_int 0); (W8.of_int 1); (W8.of_int 4); (W8.of_int 5); (W8.of_int 8); (W8.of_int 9); (W8.of_int 12); (W8.of_int 13); (W8.of_int 2); (W8.of_int 3); (W8.of_int 6); (W8.of_int 7); (W8.of_int 10); (W8.of_int 11); (W8.of_int 14); (W8.of_int 15)]). abbrev pfm_shift_s = -(Array4.of_list witness +((Array4.of_list witness) [(W32.of_int 3); (W32.of_int 2); (W32.of_int 1); (W32.of_int 0)]). abbrev pd_shift_s = (W32.of_int 8390656). @@ -618,7 +618,7 @@ abbrev pd_shift_s = (W32.of_int 8390656). abbrev pd_mask_s = (W32.of_int 15728655). abbrev pd_jshufbidx = -(Array32.of_list witness +((Array32.of_list witness) [(W8.of_int 0); (W8.of_int 0); (W8.of_int 0); (W8.of_int 0); (W8.of_int 1); (W8.of_int 1); (W8.of_int 1); (W8.of_int 1); (W8.of_int 2); (W8.of_int 2); (W8.of_int 2); (W8.of_int 2); (W8.of_int 3); (W8.of_int 3); (W8.of_int 3); @@ -628,7 +628,7 @@ abbrev pd_jshufbidx = (W8.of_int 7); (W8.of_int 7)]). abbrev pc_permidx_s = -(Array8.of_list witness +((Array8.of_list witness) [(W32.of_int 0); (W32.of_int 4); (W32.of_int 1); (W32.of_int 5); (W32.of_int 2); (W32.of_int 6); (W32.of_int 3); (W32.of_int 7)]). @@ -649,7 +649,7 @@ abbrev rOL56 = ). abbrev kECCAK_RHOTATES_RIGHT = -(Array6.of_list witness +((Array6.of_list witness) [(W256.of_int 144373339913893657577751063007562604548177214458152943091773); (W256.of_int 232252764209307188274174373867837442080505530800860351692863); (W256.of_int 156927543384667019098616994515559168111335794127330162507795); @@ -658,7 +658,7 @@ abbrev kECCAK_RHOTATES_RIGHT = (W256.of_int 313855086769334038206421612937983674734430261968315659321364)]). abbrev kECCAK_RHOTATES_LEFT = -(Array6.of_list witness +((Array6.of_list witness) [(W256.of_int 257361171150853911329517531560668107745210100483895842570243); (W256.of_int 169481746855440380633094220700393270212881784141188433969153); (W256.of_int 244806967680080549808651600052671544182051520814718623154221); @@ -667,7 +667,7 @@ abbrev kECCAK_RHOTATES_LEFT = (W256.of_int 87879424295413530700846981630247037558957052973733126340652)]). abbrev kECCAK1600_RC = -(Array24.of_list witness +((Array24.of_list witness) [(W64.of_int 1); (W64.of_int 32898); (W64.of_int (-9223372036854742902)); (W64.of_int (-9223372034707259392)); (W64.of_int 32907); (W64.of_int 2147483649); (W64.of_int (-9223372034707259263)); @@ -681,14 +681,14 @@ abbrev kECCAK1600_RC = (W64.of_int (-9223372034707259384))]). abbrev jdmontx16 = -(Array16.of_list witness +((Array16.of_list witness) [(W16.of_int 1353); (W16.of_int 1353); (W16.of_int 1353); (W16.of_int 1353); (W16.of_int 1353); (W16.of_int 1353); (W16.of_int 1353); (W16.of_int 1353); (W16.of_int 1353); (W16.of_int 1353); (W16.of_int 1353); (W16.of_int 1353); (W16.of_int 1353); (W16.of_int 1353); (W16.of_int 1353); (W16.of_int 1353)]). abbrev mqinvx16 = -(Array16.of_list witness +((Array16.of_list witness) [(W16.of_int 15099); (W16.of_int 15099); (W16.of_int 15099); (W16.of_int 15099); (W16.of_int 15099); (W16.of_int 15099); (W16.of_int 15099); (W16.of_int 15099); (W16.of_int 15099); @@ -697,35 +697,35 @@ abbrev mqinvx16 = (W16.of_int 15099)]). abbrev hhqx16 = -(Array16.of_list witness +((Array16.of_list witness) [(W16.of_int 832); (W16.of_int 832); (W16.of_int 832); (W16.of_int 832); (W16.of_int 832); (W16.of_int 832); (W16.of_int 832); (W16.of_int 832); (W16.of_int 832); (W16.of_int 832); (W16.of_int 832); (W16.of_int 832); (W16.of_int 832); (W16.of_int 832); (W16.of_int 832); (W16.of_int 832)]). abbrev hqx16_m1 = -(Array16.of_list witness +((Array16.of_list witness) [(W16.of_int 1664); (W16.of_int 1664); (W16.of_int 1664); (W16.of_int 1664); (W16.of_int 1664); (W16.of_int 1664); (W16.of_int 1664); (W16.of_int 1664); (W16.of_int 1664); (W16.of_int 1664); (W16.of_int 1664); (W16.of_int 1664); (W16.of_int 1664); (W16.of_int 1664); (W16.of_int 1664); (W16.of_int 1664)]). abbrev hqx16_p1 = -(Array16.of_list witness +((Array16.of_list witness) [(W16.of_int 1665); (W16.of_int 1665); (W16.of_int 1665); (W16.of_int 1665); (W16.of_int 1665); (W16.of_int 1665); (W16.of_int 1665); (W16.of_int 1665); (W16.of_int 1665); (W16.of_int 1665); (W16.of_int 1665); (W16.of_int 1665); (W16.of_int 1665); (W16.of_int 1665); (W16.of_int 1665); (W16.of_int 1665)]). abbrev maskx16 = -(Array16.of_list witness +((Array16.of_list witness) [(W16.of_int 4095); (W16.of_int 4095); (W16.of_int 4095); (W16.of_int 4095); (W16.of_int 4095); (W16.of_int 4095); (W16.of_int 4095); (W16.of_int 4095); (W16.of_int 4095); (W16.of_int 4095); (W16.of_int 4095); (W16.of_int 4095); (W16.of_int 4095); (W16.of_int 4095); (W16.of_int 4095); (W16.of_int 4095)]). abbrev jflox16 = -(Array16.of_list witness +((Array16.of_list witness) [(W16.of_int (-10079)); (W16.of_int (-10079)); (W16.of_int (-10079)); (W16.of_int (-10079)); (W16.of_int (-10079)); (W16.of_int (-10079)); (W16.of_int (-10079)); (W16.of_int (-10079)); (W16.of_int (-10079)); @@ -734,14 +734,14 @@ abbrev jflox16 = (W16.of_int (-10079))]). abbrev jfhix16 = -(Array16.of_list witness +((Array16.of_list witness) [(W16.of_int 1441); (W16.of_int 1441); (W16.of_int 1441); (W16.of_int 1441); (W16.of_int 1441); (W16.of_int 1441); (W16.of_int 1441); (W16.of_int 1441); (W16.of_int 1441); (W16.of_int 1441); (W16.of_int 1441); (W16.of_int 1441); (W16.of_int 1441); (W16.of_int 1441); (W16.of_int 1441); (W16.of_int 1441)]). abbrev jvx16 = -(Array16.of_list witness +((Array16.of_list witness) [(W16.of_int 20159); (W16.of_int 20159); (W16.of_int 20159); (W16.of_int 20159); (W16.of_int 20159); (W16.of_int 20159); (W16.of_int 20159); (W16.of_int 20159); (W16.of_int 20159); @@ -750,7 +750,7 @@ abbrev jvx16 = (W16.of_int 20159)]). abbrev jqinvx16 = -(Array16.of_list witness +((Array16.of_list witness) [(W16.of_int (-3327)); (W16.of_int (-3327)); (W16.of_int (-3327)); (W16.of_int (-3327)); (W16.of_int (-3327)); (W16.of_int (-3327)); (W16.of_int (-3327)); (W16.of_int (-3327)); (W16.of_int (-3327)); @@ -759,14 +759,14 @@ abbrev jqinvx16 = (W16.of_int (-3327))]). abbrev jqx16 = -(Array16.of_list witness +((Array16.of_list witness) [(W16.of_int 3329); (W16.of_int 3329); (W16.of_int 3329); (W16.of_int 3329); (W16.of_int 3329); (W16.of_int 3329); (W16.of_int 3329); (W16.of_int 3329); (W16.of_int 3329); (W16.of_int 3329); (W16.of_int 3329); (W16.of_int 3329); (W16.of_int 3329); (W16.of_int 3329); (W16.of_int 3329); (W16.of_int 3329)]). abbrev jzetas_inv_exp = -(Array400.of_list witness +((Array400.of_list witness) [(W16.of_int (-23131)); (W16.of_int (-7756)); (W16.of_int 20258); (W16.of_int 23860); (W16.of_int 17443); (W16.of_int (-23210)); (W16.of_int 20199); (W16.of_int 21498); (W16.of_int (-14469)); @@ -887,7 +887,7 @@ abbrev jzetas_inv_exp = (W16.of_int 0)]). abbrev jzetas_exp = -(Array400.of_list witness +((Array400.of_list witness) [(W16.of_int 31499); (W16.of_int 31499); (W16.of_int 2571); (W16.of_int 2571); (W16.of_int 14746); (W16.of_int 14746); (W16.of_int 2970); (W16.of_int 2970); (W16.of_int 13525); (W16.of_int 13525); @@ -1006,7 +1006,7 @@ abbrev jzetas_exp = (W16.of_int 0)]). abbrev jzetas_inv = -(Array128.of_list witness +((Array128.of_list witness) [(W16.of_int 1701); (W16.of_int 1807); (W16.of_int 1460); (W16.of_int 2371); (W16.of_int 2338); (W16.of_int 2333); (W16.of_int 308); (W16.of_int 108); (W16.of_int 2851); (W16.of_int 870); (W16.of_int 854); (W16.of_int 1510); @@ -1041,7 +1041,7 @@ abbrev jzetas_inv = (W16.of_int 1517); (W16.of_int 359); (W16.of_int 758); (W16.of_int 1441)]). abbrev jzetas = -(Array128.of_list witness +((Array128.of_list witness) [(W16.of_int 2285); (W16.of_int 2571); (W16.of_int 2970); (W16.of_int 1812); (W16.of_int 1493); (W16.of_int 1422); (W16.of_int 287); (W16.of_int 202); (W16.of_int 3158); (W16.of_int 622); (W16.of_int 1577); (W16.of_int 182); @@ -1309,7 +1309,6 @@ module M(SC:Syscall_t) = { return r; } proc keccakf1600_rho_offsets (i:int) : int = { - var aux:int; var r:int; var x:int; var y:int; @@ -2288,7 +2287,6 @@ module M(SC:Syscall_t) = { return t256; } proc __state_init_avx2 () : W256.t Array7.t = { - var aux:int; var st:W256.t Array7.t; var i:int; st <- witness; @@ -2301,16 +2299,16 @@ module M(SC:Syscall_t) = { } proc __pstate_init_avx2 (pst:W64.t Array25.t) : W64.t Array25.t * W256.t Array7.t = { - var aux:int; + var inc:int; var st:W256.t Array7.t; var z256:W256.t; var i:int; var z64:W64.t; st <- witness; z256 <- (set0_256); - aux <- (25 %/ 4); + inc <- (25 %/ 4); i <- 0; - while ((i < aux)) { + while ((i < inc)) { pst <- (Array25.init (WArray200.get64 @@ -2454,10 +2452,10 @@ module M(SC:Syscall_t) = { return (st3, st4, st5, st6); } proc __state_from_pstate_avx2 (pst:W64.t Array25.t) : W256.t Array7.t = { - var aux_2:W256.t; - var aux_1:W256.t; - var aux_0:W256.t; var aux:W256.t; + var aux_0:W256.t; + var aux_1:W256.t; + var aux_2:W256.t; var st:W256.t Array7.t; var t128_0:W128.t; var t128_1:W128.t; @@ -2482,12 +2480,12 @@ module M(SC:Syscall_t) = { (((W128.to_uint t128_1) %% (2 ^ 128)) + ((2 ^ 128) * (W128.to_uint t128_0)))); st.[6] <- (get256_direct (WArray200.init64 (fun i => pst.[i])) (21 * 8)); - (aux_2, aux_1, aux_0, aux) <@ __perm_reg3456_avx2 (st.[3], st.[4], + (aux, aux_0, aux_1, aux_2) <@ __perm_reg3456_avx2 (st.[3], st.[4], st.[5], st.[6]); - st.[3] <- aux_2; - st.[4] <- aux_1; - st.[5] <- aux_0; - st.[6] <- aux; + st.[3] <- aux; + st.[4] <- aux_0; + st.[5] <- aux_1; + st.[6] <- aux_2; return st; } proc __addstate_r3456_avx2 (st:W256.t Array7.t, r3:W256.t, r4:W256.t, @@ -3133,7 +3131,6 @@ module M(SC:Syscall_t) = { return (buf, st); } proc keccakf1600_4x_theta_sum (a:W256.t Array25.t) : W256.t Array5.t = { - var aux:int; var c:W256.t Array5.t; var x:int; var y:int; @@ -3172,7 +3169,6 @@ module M(SC:Syscall_t) = { } proc keccakf1600_4x_theta_rol (c:W256.t Array5.t, r8:W256.t, r56:W256.t) : W256.t Array5.t = { - var aux:int; var d:W256.t Array5.t; var x:int; d <- witness; @@ -3187,7 +3183,6 @@ module M(SC:Syscall_t) = { } proc keccakf1600_4x_rol_sum (a:W256.t Array25.t, d:W256.t Array5.t, y:int, r8:W256.t, r56:W256.t) : W256.t Array5.t = { - var aux:int; var b:W256.t Array5.t; var x:int; var x_:int; @@ -3212,7 +3207,6 @@ module M(SC:Syscall_t) = { } proc keccakf1600_4x_set_row (e:W256.t Array25.t, b:W256.t Array5.t, y:int, rc:W256.t) : W256.t Array25.t = { - var aux:int; var x:int; var x1:int; var x2:int; @@ -3235,7 +3229,6 @@ module M(SC:Syscall_t) = { } proc _keccakf1600_4x_round (e:W256.t Array25.t, a:W256.t Array25.t, rc:W256.t, r8:W256.t, r56:W256.t) : W256.t Array25.t = { - var aux:int; var c:W256.t Array5.t; var d:W256.t Array5.t; var y:int; @@ -7216,7 +7209,6 @@ module M(SC:Syscall_t) = { return (st, buf); } proc _poly_add2 (rp:W16.t Array256.t, bp:W16.t Array256.t) : W16.t Array256.t = { - var aux:int; var i:int; var a:W256.t; var b:W256.t; @@ -7236,7 +7228,6 @@ module M(SC:Syscall_t) = { return rp; } proc _poly_csubq (rp:W16.t Array256.t) : W16.t Array256.t = { - var aux:int; var qx16:W256.t; var i:int; var r:W256.t; @@ -7488,7 +7479,7 @@ module M(SC:Syscall_t) = { return rp; } proc _poly_compress (rp:W64.t, a:W16.t Array256.t) : W16.t Array256.t = { - var aux:int; + var inc:int; var x16p:W16.t Array16.t; var v:W256.t; var shift1:W256.t; @@ -7508,9 +7499,9 @@ module M(SC:Syscall_t) = { mask <- (VPBROADCAST_16u16 pc_mask_s); shift2 <- (VPBROADCAST_16u16 pc_shift2_s); permidx <- (get256 (WArray32.init32 (fun i_0 => pc_permidx_s.[i_0])) 0); - aux <- (256 %/ 64); + inc <- (256 %/ 64); i <- 0; - while ((i < aux)) { + while ((i < inc)) { f0 <- (get256 (WArray512.init16 (fun i_0 => a.[i_0])) (4 * i)); f1 <- (get256 (WArray512.init16 (fun i_0 => a.[i_0])) ((4 * i) + 1)); f2 <- (get256 (WArray512.init16 (fun i_0 => a.[i_0])) ((4 * i) + 2)); @@ -7541,7 +7532,7 @@ module M(SC:Syscall_t) = { } proc _poly_compress_1 (rp:W8.t Array128.t, a:W16.t Array256.t) : W8.t Array128.t * W16.t Array256.t = { - var aux:int; + var inc:int; var x16p:W16.t Array16.t; var v:W256.t; var shift1:W256.t; @@ -7561,9 +7552,9 @@ module M(SC:Syscall_t) = { mask <- (VPBROADCAST_16u16 pc_mask_s); shift2 <- (VPBROADCAST_16u16 pc_shift2_s); permidx <- (get256 (WArray32.init32 (fun i_0 => pc_permidx_s.[i_0])) 0); - aux <- (256 %/ 64); + inc <- (256 %/ 64); i <- 0; - while ((i < aux)) { + while ((i < inc)) { f0 <- (get256 (WArray512.init16 (fun i_0 => a.[i_0])) (4 * i)); f1 <- (get256 (WArray512.init16 (fun i_0 => a.[i_0])) ((4 * i) + 1)); f2 <- (get256 (WArray512.init16 (fun i_0 => a.[i_0])) ((4 * i) + 2)); @@ -7596,7 +7587,7 @@ module M(SC:Syscall_t) = { return (rp, a); } proc _poly_decompress (rp:W16.t Array256.t, ap:W64.t) : W16.t Array256.t = { - var aux:int; + var inc:int; var x16p:W16.t Array16.t; var q:W256.t; var x32p:W8.t Array32.t; @@ -7616,9 +7607,9 @@ module M(SC:Syscall_t) = { mask <- (VPBROADCAST_8u32 pd_mask_s); shift <- (VPBROADCAST_8u32 pd_shift_s); f <- (set0_256); - aux <- (256 %/ 16); + inc <- (256 %/ 16); i <- 0; - while ((i < aux)) { + while ((i < inc)) { h <- (zeroextu128 (loadW64 Glob.mem (W64.to_uint (ap + (W64.of_int (8 * i)))))); @@ -7637,7 +7628,6 @@ module M(SC:Syscall_t) = { return rp; } proc _poly_frombytes (rp:W16.t Array256.t, ap:W64.t) : W16.t Array256.t = { - var aux:int; var maskp:W16.t Array16.t; var mask:W256.t; var i:int; @@ -7749,7 +7739,7 @@ module M(SC:Syscall_t) = { return rp; } proc _poly_frommont (rp:W16.t Array256.t) : W16.t Array256.t = { - var aux:int; + var inc:int; var x16p:W16.t Array16.t; var qx16:W256.t; var qinvx16:W256.t; @@ -7763,9 +7753,9 @@ module M(SC:Syscall_t) = { qinvx16 <- (get256 (WArray32.init16 (fun i_0 => x16p.[i_0])) 0); x16p <- jdmontx16; dmontx16 <- (get256 (WArray32.init16 (fun i_0 => x16p.[i_0])) 0); - aux <- (256 %/ 16); + inc <- (256 %/ 16); i <- 0; - while ((i < aux)) { + while ((i < inc)) { t <- (get256 (WArray512.init16 (fun i_0 => rp.[i_0])) i); t <@ __fqmulx16 (t, dmontx16, qx16, qinvx16); rp <- @@ -7777,7 +7767,6 @@ module M(SC:Syscall_t) = { return rp; } proc _poly_frommsg_1 (rp:W16.t Array256.t, ap:W8.t Array32.t) : W16.t Array256.t = { - var aux:int; var x16p:W16.t Array16.t; var hqs:W256.t; var shift:W256.t; @@ -7851,7 +7840,7 @@ module M(SC:Syscall_t) = { return rp; } proc __cbd3 (rp:W16.t Array256.t, buf:W8.t Array128.t) : W16.t Array256.t = { - var aux:int; + var inc:int; var mask249_s:W32.t; var mask6DB_s:W32.t; var mask07_s:W32.t; @@ -7879,9 +7868,9 @@ module M(SC:Syscall_t) = { mask70 <- (VPBROADCAST_8u32 mask70_s); mask3 <- (VPBROADCAST_16u16 mask3_s); shufbidx <- (get256 (WArray32.init8 (fun i_0 => cbd_jshufbidx.[i_0])) 0); - aux <- (256 %/ 32); + inc <- (256 %/ 32); i <- 0; - while ((i < aux)) { + while ((i < inc)) { f0 <- (get256_direct (WArray128.init8 (fun i_0 => buf.[i_0])) (24 * i)); f0 <- (VPERMQ f0 (W8.of_int 148)); @@ -7926,7 +7915,7 @@ module M(SC:Syscall_t) = { return rp; } proc __cbd2 (rp:W16.t Array256.t, buf:W8.t Array128.t) : W16.t Array256.t = { - var aux:int; + var inc:int; var mask55_s:W32.t; var mask33_s:W32.t; var mask03_s:W32.t; @@ -7949,9 +7938,9 @@ module M(SC:Syscall_t) = { mask33 <- (VPBROADCAST_8u32 mask33_s); mask03 <- (VPBROADCAST_8u32 mask03_s); mask0F <- (VPBROADCAST_8u32 mask0F_s); - aux <- (256 %/ 64); + inc <- (256 %/ 64); i <- 0; - while ((i < aux)) { + while ((i < inc)) { f0 <- (get256 (WArray128.init8 (fun i_0 => buf.[i_0])) i); f1 <- (VPSRL_16u16 f0 (W128.of_int 1)); f0 <- (VPAND_256 mask55 f0); @@ -8093,7 +8082,6 @@ module M(SC:Syscall_t) = { return (rl0, rl1, rl2, rl3, rh0, rh1, rh2, rh3); } proc _poly_invntt (rp:W16.t Array256.t) : W16.t Array256.t = { - var aux:int; var zetasp:W16.t Array400.t; var qx16:W256.t; var i:int; @@ -8403,7 +8391,6 @@ module M(SC:Syscall_t) = { return (rl0, rl1, rl2, rl3, rh0, rh1, rh2, rh3); } proc _poly_ntt (rp:W16.t Array256.t) : W16.t Array256.t = { - var aux:int; var zetasp:W16.t Array400.t; var qx16:W256.t; var zeta0:W256.t; @@ -8666,7 +8653,6 @@ module M(SC:Syscall_t) = { return rp; } proc __poly_reduce (rp:W16.t Array256.t) : W16.t Array256.t = { - var aux:int; var qx16:W256.t; var vx16:W256.t; var i:int; @@ -8688,7 +8674,6 @@ module M(SC:Syscall_t) = { } proc _poly_sub (rp:W16.t Array256.t, ap:W16.t Array256.t, bp:W16.t Array256.t) : W16.t Array256.t = { - var aux:int; var i:int; var a:W256.t; var b:W256.t; @@ -8708,7 +8693,6 @@ module M(SC:Syscall_t) = { return rp; } proc _poly_tobytes (rp:W64.t, a:W16.t Array256.t) : W16.t Array256.t = { - var aux:int; var jqx16_p:W16.t Array16.t; var qx16:W256.t; var i:int; @@ -8787,7 +8771,7 @@ module M(SC:Syscall_t) = { } proc _poly_tomsg_1 (rp:W8.t Array32.t, a:W16.t Array256.t) : W8.t Array32.t * W16.t Array256.t = { - var aux:int; + var inc:int; var px16:W16.t Array16.t; var hq:W256.t; var hhq:W256.t; @@ -8803,9 +8787,9 @@ module M(SC:Syscall_t) = { hq <- (get256 (WArray32.init16 (fun i_0 => px16.[i_0])) 0); px16 <- hhqx16; hhq <- (get256 (WArray32.init16 (fun i_0 => px16.[i_0])) 0); - aux <- (256 %/ 32); + inc <- (256 %/ 32); i <- 0; - while ((i < aux)) { + while ((i < inc)) { f0 <- (get256 (WArray512.init16 (fun i_0 => a.[i_0])) (2 * i)); f1 <- (get256 (WArray512.init16 (fun i_0 => a.[i_0])) ((2 * i) + 1)); f0 <- (VPSUB_16u16 hq f0); @@ -8869,7 +8853,7 @@ module M(SC:Syscall_t) = { return r; } proc __polyvec_decompress (rp:W64.t) : W16.t Array768.t = { - var aux:int; + var inc:int; var r:W16.t Array768.t; var q:W256.t; var shufbidx:W256.t; @@ -8886,9 +8870,9 @@ module M(SC:Syscall_t) = { mask <- (VPBROADCAST_8u32 pvd_mask_s); k <- 0; while ((k < 3)) { - aux <- (256 %/ 16); + inc <- (256 %/ 16); i <- 0; - while ((i < aux)) { + while ((i < inc)) { f <- (loadW256 Glob.mem (W64.to_uint (rp + (W64.of_int ((320 * k) + (20 * i)))))); @@ -8910,7 +8894,7 @@ module M(SC:Syscall_t) = { return r; } proc __polyvec_compress (rp:W64.t, a:W16.t Array768.t) : unit = { - var aux:int; + var inc:int; var x16p:W16.t Array16.t; var v:W256.t; var v8:W256.t; @@ -8938,9 +8922,9 @@ module M(SC:Syscall_t) = { sllvdidx <- (VPBROADCAST_4u64 pvc_sllvdidx_s); shufbidx <- (get256 (WArray32.init8 (fun i_0 => pvc_shufbidx_s.[i_0])) 0); - aux <- ((3 * 256) %/ 16); + inc <- ((3 * 256) %/ 16); i <- 0; - while ((i < aux)) { + while ((i < inc)) { f0 <- (get256 (WArray1536.init16 (fun i_0 => a.[i_0])) i); f1 <- (VPMULL_16u16 f0 v8); f2 <- (VPADD_16u16 f0 off); @@ -8970,7 +8954,7 @@ module M(SC:Syscall_t) = { } proc __polyvec_compress_1 (rp:W8.t Array960.t, a:W16.t Array768.t) : W8.t Array960.t = { - var aux:int; + var inc:int; var x16p:W16.t Array16.t; var v:W256.t; var v8:W256.t; @@ -8998,9 +8982,9 @@ module M(SC:Syscall_t) = { sllvdidx <- (VPBROADCAST_4u64 pvc_sllvdidx_s); shufbidx <- (get256 (WArray32.init8 (fun i_0 => pvc_shufbidx_s.[i_0])) 0); - aux <- ((3 * 256) %/ 16); + inc <- ((3 * 256) %/ 16); i <- 0; - while ((i < aux)) { + while ((i < inc)) { f0 <- (get256 (WArray1536.init16 (fun i_0 => a.[i_0])) i); f1 <- (VPMULL_16u16 f0 v8); f2 <- (VPADD_16u16 f0 off); @@ -9510,9 +9494,9 @@ module M(SC:Syscall_t) = { rho:W8.t Array32.t, pos_entry:W64.t, transposed:W64.t) : W16.t Array1024.t * W8.t Array2144.t = { + var aux_0:W16.t Array256.t; var aux:W64.t; var aux_1:W8.t Array536.t; - var aux_0:W16.t Array256.t; var indexes:W8.t Array8.t; var state:W256.t Array25.t; var stx4:W256.t Array25.t; @@ -9615,9 +9599,8 @@ module M(SC:Syscall_t) = { } proc _gen_matrix_avx2 (matrix:W16.t Array2304.t, rho:W8.t Array32.t, transposed:W64.t) : W16.t Array2304.t = { - var aux:int; - var aux_1:W8.t Array536.t; - var aux_0:W16.t Array256.t; + var aux:W16.t Array256.t; + var aux_0:W8.t Array536.t; var buf_s:W8.t Array2144.t; var buf:W8.t Array2144.t; var i:int; @@ -9649,12 +9632,12 @@ module M(SC:Syscall_t) = { } pol <- (Array256.init (fun i_0 => matrix.[((8 * 256) + i_0)])); rc <- (W16.of_int 514); - (aux_0, aux_1) <@ __gen_matrix_sample_one_polynomial (pol, + (aux, aux_0) <@ __gen_matrix_sample_one_polynomial (pol, (Array536.init (fun i_0 => buf.[((536 * 0) + i_0)])), rho, rc); - pol <- aux_0; + pol <- aux; buf <- (Array2144.init - (fun i_0 => (if ((536 * 0) <= i_0 < ((536 * 0) + 536)) then aux_1.[ + (fun i_0 => (if ((536 * 0) <= i_0 < ((536 * 0) + 536)) then aux_0.[ (i_0 - (536 * 0))] else buf.[i_0])) @@ -9670,18 +9653,17 @@ module M(SC:Syscall_t) = { while ((i < 3)) { j <- 0; while ((j < 3)) { - aux_0 <@ _nttunpack ((Array256.init - (fun i_0 => matrix.[(((i * (3 * 256)) + - (j * 256)) + - i_0)]) - )); + aux <@ _nttunpack ((Array256.init + (fun i_0 => matrix.[(((i * (3 * 256)) + (j * 256)) + + i_0)]) + )); matrix <- (Array2304.init (fun i_0 => (if (((i * (3 * 256)) + (j * 256)) <= i_0 < (((i * (3 * 256)) + (j * 256)) + 256)) then - aux_0.[(i_0 - ((i * (3 * 256)) + (j * 256)))] else + aux.[(i_0 - ((i * (3 * 256)) + (j * 256)))] else matrix.[i_0])) ); j <- (j + 1); @@ -9692,11 +9674,11 @@ module M(SC:Syscall_t) = { } proc __indcpa_keypair (pkp:W64.t, skp:W64.t, randomnessp:W8.t Array32.t) : unit = { - var aux:int; - var aux_3:W16.t Array256.t; - var aux_2:W16.t Array256.t; - var aux_1:W16.t Array256.t; + var aux:W16.t Array256.t; var aux_0:W16.t Array256.t; + var aux_1:W16.t Array256.t; + var aux_2:W16.t Array256.t; + var inc:int; var i:int; var t64:W64.t; var inbuf:W8.t Array33.t; @@ -9718,9 +9700,9 @@ module M(SC:Syscall_t) = { publicseed <- witness; skpv <- witness; (* Erased call to spill *) - aux <- (32 %/ 8); + inc <- (32 %/ 8); i <- 0; - while ((i < aux)) { + while ((i < inc)) { t64 <- (get64 (WArray32.init8 (fun i_0 => randomnessp.[i_0])) i); inbuf <- (Array33.init @@ -9730,9 +9712,9 @@ module M(SC:Syscall_t) = { } inbuf.[32] <- (W8.of_int 3); buf <@ _sha3_512A_A33 (buf, inbuf); - aux <- (32 %/ 8); + inc <- (32 %/ 8); i <- 0; - while ((i < aux)) { + while ((i < inc)) { t64 <- (get64 (WArray64.init8 (fun i_0 => buf.[i_0])) i); publicseed <- (Array32.init @@ -9748,21 +9730,20 @@ module M(SC:Syscall_t) = { transposed <- (W64.of_int 0); aa <@ _gen_matrix_avx2 (aa, publicseed, transposed); nonce <- (W8.of_int 0); - (aux_3, aux_2, aux_1, aux_0) <@ _poly_getnoise_eta1_4x ((Array256.init - (fun i_0 => - skpv.[(0 + i_0)]) - ), + (aux, aux_0, aux_1, aux_2) <@ _poly_getnoise_eta1_4x ((Array256.init + (fun i_0 => + skpv.[(0 + i_0)])), (Array256.init (fun i_0 => skpv.[(256 + i_0)])), (Array256.init (fun i_0 => skpv.[((2 * 256) + i_0)])), (Array256.init (fun i_0 => e.[(0 + i_0)])), noiseseed, nonce); skpv <- (Array768.init - (fun i_0 => (if (0 <= i_0 < (0 + 256)) then aux_3.[(i_0 - 0)] else + (fun i_0 => (if (0 <= i_0 < (0 + 256)) then aux.[(i_0 - 0)] else skpv.[i_0])) ); skpv <- (Array768.init - (fun i_0 => (if (256 <= i_0 < (256 + 256)) then aux_2.[(i_0 - 256)] else + (fun i_0 => (if (256 <= i_0 < (256 + 256)) then aux_0.[(i_0 - 256)] else skpv.[i_0])) ); skpv <- @@ -9774,24 +9755,24 @@ module M(SC:Syscall_t) = { ); e <- (Array768.init - (fun i_0 => (if (0 <= i_0 < (0 + 256)) then aux_0.[(i_0 - 0)] else + (fun i_0 => (if (0 <= i_0 < (0 + 256)) then aux_2.[(i_0 - 0)] else e.[i_0])) ); nonce <- (W8.of_int 4); - (aux_3, aux_2, aux_1, aux_0) <@ _poly_getnoise_eta1_4x ((Array256.init - (fun i_0 => - e.[(256 + i_0)])), + (aux, aux_0, aux_1, aux_2) <@ _poly_getnoise_eta1_4x ((Array256.init + (fun i_0 => + e.[(256 + i_0)])), (Array256.init (fun i_0 => e.[((2 * 256) + i_0)])), (Array256.init (fun i_0 => pkpv.[(0 + i_0)])), (Array256.init (fun i_0 => pkpv.[(256 + i_0)])), noiseseed, nonce); e <- (Array768.init - (fun i_0 => (if (256 <= i_0 < (256 + 256)) then aux_3.[(i_0 - 256)] else + (fun i_0 => (if (256 <= i_0 < (256 + 256)) then aux.[(i_0 - 256)] else e.[i_0])) ); e <- (Array768.init - (fun i_0 => (if ((2 * 256) <= i_0 < ((2 * 256) + 256)) then aux_2.[ + (fun i_0 => (if ((2 * 256) <= i_0 < ((2 * 256) + 256)) then aux_0.[ (i_0 - (2 * 256))] else e.[i_0])) @@ -9803,29 +9784,28 @@ module M(SC:Syscall_t) = { ); pkpv <- (Array768.init - (fun i_0 => (if (256 <= i_0 < (256 + 256)) then aux_0.[(i_0 - 256)] else + (fun i_0 => (if (256 <= i_0 < (256 + 256)) then aux_2.[(i_0 - 256)] else pkpv.[i_0])) ); skpv <@ __polyvec_ntt (skpv); e <@ __polyvec_ntt (e); i <- 0; while ((i < 3)) { - aux_3 <@ __polyvec_pointwise_acc ((Array256.init - (fun i_0 => pkpv.[((i * 256) + i_0)]) - ), + aux <@ __polyvec_pointwise_acc ((Array256.init + (fun i_0 => pkpv.[((i * 256) + i_0)])), (Array768.init (fun i_0 => aa.[((i * (3 * 256)) + i_0)])), skpv); pkpv <- (Array768.init - (fun i_0 => (if ((i * 256) <= i_0 < ((i * 256) + 256)) then aux_3.[ + (fun i_0 => (if ((i * 256) <= i_0 < ((i * 256) + 256)) then aux.[ (i_0 - (i * 256))] else pkpv.[i_0])) ); - aux_3 <@ _poly_frommont ((Array256.init - (fun i_0 => pkpv.[((i * 256) + i_0)]))); + aux <@ _poly_frommont ((Array256.init + (fun i_0 => pkpv.[((i * 256) + i_0)]))); pkpv <- (Array768.init - (fun i_0 => (if ((i * 256) <= i_0 < ((i * 256) + 256)) then aux_3.[ + (fun i_0 => (if ((i * 256) <= i_0 < ((i * 256) + 256)) then aux.[ (i_0 - (i * 256))] else pkpv.[i_0])) @@ -9838,9 +9818,9 @@ module M(SC:Syscall_t) = { __polyvec_tobytes (skp, skpv); __polyvec_tobytes (pkp, pkpv); pkp <- (pkp + (W64.of_int (3 * 384))); - aux <- (32 %/ 8); + inc <- (32 %/ 8); i <- 0; - while ((i < aux)) { + while ((i < inc)) { t64 <- (get64 (WArray32.init8 (fun i_0 => publicseed.[i_0])) i); Glob.mem <- (storeW64 Glob.mem (W64.to_uint (pkp + (W64.of_int 0))) t64); @@ -9851,11 +9831,10 @@ module M(SC:Syscall_t) = { } proc __indcpa_enc_0 (sctp:W64.t, msgp:W8.t Array32.t, pkp:W64.t, noiseseed:W8.t Array32.t) : unit = { - var aux_3:int; - var aux_2:W16.t Array256.t; - var aux_1:W16.t Array256.t; - var aux_0:W16.t Array256.t; var aux:W16.t Array256.t; + var aux_0:W16.t Array256.t; + var aux_1:W16.t Array256.t; + var aux_2:W16.t Array256.t; var pkpv:W16.t Array768.t; var i:W64.t; var t64:W64.t; @@ -9903,7 +9882,7 @@ module M(SC:Syscall_t) = { aat <@ _gen_matrix_avx2 (aat, publicseed, transposed); lnoiseseed <- s_noiseseed; nonce <- (W8.of_int 0); - (aux_2, aux_1, aux_0, aux) <@ _poly_getnoise_eta1_4x ((Array256.init + (aux, aux_0, aux_1, aux_2) <@ _poly_getnoise_eta1_4x ((Array256.init (fun i_0 => sp_0.[(0 + i_0)])), (Array256.init (fun i_0 => sp_0.[(256 + i_0)])), @@ -9911,60 +9890,60 @@ module M(SC:Syscall_t) = { (Array256.init (fun i_0 => ep.[(0 + i_0)])), lnoiseseed, nonce); sp_0 <- (Array768.init - (fun i_0 => (if (0 <= i_0 < (0 + 256)) then aux_2.[(i_0 - 0)] else + (fun i_0 => (if (0 <= i_0 < (0 + 256)) then aux.[(i_0 - 0)] else sp_0.[i_0])) ); sp_0 <- (Array768.init - (fun i_0 => (if (256 <= i_0 < (256 + 256)) then aux_1.[(i_0 - 256)] else + (fun i_0 => (if (256 <= i_0 < (256 + 256)) then aux_0.[(i_0 - 256)] else sp_0.[i_0])) ); sp_0 <- (Array768.init - (fun i_0 => (if ((2 * 256) <= i_0 < ((2 * 256) + 256)) then aux_0.[ + (fun i_0 => (if ((2 * 256) <= i_0 < ((2 * 256) + 256)) then aux_1.[ (i_0 - (2 * 256))] else sp_0.[i_0])) ); ep <- (Array768.init - (fun i_0 => (if (0 <= i_0 < (0 + 256)) then aux.[(i_0 - 0)] else + (fun i_0 => (if (0 <= i_0 < (0 + 256)) then aux_2.[(i_0 - 0)] else ep.[i_0])) ); lnoiseseed <- s_noiseseed; nonce <- (W8.of_int 4); - (aux_2, aux_1, aux_0, aux) <@ _poly_getnoise_eta1_4x ((Array256.init + (aux, aux_0, aux_1, aux_2) <@ _poly_getnoise_eta1_4x ((Array256.init (fun i_0 => ep.[(256 + i_0)])), (Array256.init (fun i_0 => ep.[((2 * 256) + i_0)])), epp, (Array256.init (fun i_0 => bp.[(0 + i_0)])), lnoiseseed, nonce); ep <- (Array768.init - (fun i_0 => (if (256 <= i_0 < (256 + 256)) then aux_2.[(i_0 - 256)] else + (fun i_0 => (if (256 <= i_0 < (256 + 256)) then aux.[(i_0 - 256)] else ep.[i_0])) ); ep <- (Array768.init - (fun i_0 => (if ((2 * 256) <= i_0 < ((2 * 256) + 256)) then aux_1.[ + (fun i_0 => (if ((2 * 256) <= i_0 < ((2 * 256) + 256)) then aux_0.[ (i_0 - (2 * 256))] else ep.[i_0])) ); - epp <- aux_0; + epp <- aux_1; bp <- (Array768.init - (fun i_0 => (if (0 <= i_0 < (0 + 256)) then aux.[(i_0 - 0)] else + (fun i_0 => (if (0 <= i_0 < (0 + 256)) then aux_2.[(i_0 - 0)] else bp.[i_0])) ); sp_0 <@ __polyvec_ntt (sp_0); w <- 0; while ((w < 3)) { - aux_2 <@ __polyvec_pointwise_acc ((Array256.init - (fun i_0 => bp.[((w * 256) + i_0)])), + aux <@ __polyvec_pointwise_acc ((Array256.init + (fun i_0 => bp.[((w * 256) + i_0)])), (Array768.init (fun i_0 => aat.[((w * (3 * 256)) + i_0)])), sp_0); bp <- (Array768.init - (fun i_0 => (if ((w * 256) <= i_0 < ((w * 256) + 256)) then aux_2.[ + (fun i_0 => (if ((w * 256) <= i_0 < ((w * 256) + 256)) then aux.[ (i_0 - (w * 256))] else bp.[i_0])) @@ -9987,13 +9966,12 @@ module M(SC:Syscall_t) = { } proc __indcpa_enc_1 (ctp:W8.t Array1088.t, msgp:W8.t Array32.t, pkp:W64.t, noiseseed:W8.t Array32.t) : W8.t Array1088.t = { - var aux_3:int; - var aux_5:W8.t Array128.t; - var aux_4:W8.t Array960.t; - var aux_2:W16.t Array256.t; - var aux_1:W16.t Array256.t; - var aux_0:W16.t Array256.t; var aux:W16.t Array256.t; + var aux_0:W16.t Array256.t; + var aux_1:W16.t Array256.t; + var aux_2:W16.t Array256.t; + var aux_4:W8.t Array128.t; + var aux_3:W8.t Array960.t; var pkpv:W16.t Array768.t; var i:W64.t; var t64:W64.t; @@ -10040,7 +10018,7 @@ module M(SC:Syscall_t) = { aat <@ _gen_matrix_avx2 (aat, publicseed, transposed); lnoiseseed <- s_noiseseed; nonce <- (W8.of_int 0); - (aux_2, aux_1, aux_0, aux) <@ _poly_getnoise_eta1_4x ((Array256.init + (aux, aux_0, aux_1, aux_2) <@ _poly_getnoise_eta1_4x ((Array256.init (fun i_0 => sp_0.[(0 + i_0)])), (Array256.init (fun i_0 => sp_0.[(256 + i_0)])), @@ -10048,60 +10026,60 @@ module M(SC:Syscall_t) = { (Array256.init (fun i_0 => ep.[(0 + i_0)])), lnoiseseed, nonce); sp_0 <- (Array768.init - (fun i_0 => (if (0 <= i_0 < (0 + 256)) then aux_2.[(i_0 - 0)] else + (fun i_0 => (if (0 <= i_0 < (0 + 256)) then aux.[(i_0 - 0)] else sp_0.[i_0])) ); sp_0 <- (Array768.init - (fun i_0 => (if (256 <= i_0 < (256 + 256)) then aux_1.[(i_0 - 256)] else + (fun i_0 => (if (256 <= i_0 < (256 + 256)) then aux_0.[(i_0 - 256)] else sp_0.[i_0])) ); sp_0 <- (Array768.init - (fun i_0 => (if ((2 * 256) <= i_0 < ((2 * 256) + 256)) then aux_0.[ + (fun i_0 => (if ((2 * 256) <= i_0 < ((2 * 256) + 256)) then aux_1.[ (i_0 - (2 * 256))] else sp_0.[i_0])) ); ep <- (Array768.init - (fun i_0 => (if (0 <= i_0 < (0 + 256)) then aux.[(i_0 - 0)] else + (fun i_0 => (if (0 <= i_0 < (0 + 256)) then aux_2.[(i_0 - 0)] else ep.[i_0])) ); lnoiseseed <- s_noiseseed; nonce <- (W8.of_int 4); - (aux_2, aux_1, aux_0, aux) <@ _poly_getnoise_eta1_4x ((Array256.init + (aux, aux_0, aux_1, aux_2) <@ _poly_getnoise_eta1_4x ((Array256.init (fun i_0 => ep.[(256 + i_0)])), (Array256.init (fun i_0 => ep.[((2 * 256) + i_0)])), epp, (Array256.init (fun i_0 => bp.[(0 + i_0)])), lnoiseseed, nonce); ep <- (Array768.init - (fun i_0 => (if (256 <= i_0 < (256 + 256)) then aux_2.[(i_0 - 256)] else + (fun i_0 => (if (256 <= i_0 < (256 + 256)) then aux.[(i_0 - 256)] else ep.[i_0])) ); ep <- (Array768.init - (fun i_0 => (if ((2 * 256) <= i_0 < ((2 * 256) + 256)) then aux_1.[ + (fun i_0 => (if ((2 * 256) <= i_0 < ((2 * 256) + 256)) then aux_0.[ (i_0 - (2 * 256))] else ep.[i_0])) ); - epp <- aux_0; + epp <- aux_1; bp <- (Array768.init - (fun i_0 => (if (0 <= i_0 < (0 + 256)) then aux.[(i_0 - 0)] else + (fun i_0 => (if (0 <= i_0 < (0 + 256)) then aux_2.[(i_0 - 0)] else bp.[i_0])) ); sp_0 <@ __polyvec_ntt (sp_0); w <- 0; while ((w < 3)) { - aux_2 <@ __polyvec_pointwise_acc ((Array256.init - (fun i_0 => bp.[((w * 256) + i_0)])), + aux <@ __polyvec_pointwise_acc ((Array256.init + (fun i_0 => bp.[((w * 256) + i_0)])), (Array768.init (fun i_0 => aat.[((w * (3 * 256)) + i_0)])), sp_0); bp <- (Array768.init - (fun i_0 => (if ((w * 256) <= i_0 < ((w * 256) + 256)) then aux_2.[ + (fun i_0 => (if ((w * 256) <= i_0 < ((w * 256) + 256)) then aux.[ (i_0 - (w * 256))] else bp.[i_0])) @@ -10116,25 +10094,25 @@ module M(SC:Syscall_t) = { v <@ _poly_add2 (v, k); bp <@ __polyvec_reduce (bp); v <@ __poly_reduce (v); - aux_4 <@ __polyvec_compress_1 ((Array960.init + aux_3 <@ __polyvec_compress_1 ((Array960.init (fun i_0 => ctp.[(0 + i_0)])), bp); ctp <- (Array1088.init - (fun i_0 => (if (0 <= i_0 < (0 + 960)) then aux_4.[(i_0 - 0)] else + (fun i_0 => (if (0 <= i_0 < (0 + 960)) then aux_3.[(i_0 - 0)] else ctp.[i_0])) ); - (aux_5, aux_2) <@ _poly_compress_1 ((Array128.init - (fun i_0 => ctp.[((3 * 320) + i_0)])), + (aux_4, aux) <@ _poly_compress_1 ((Array128.init + (fun i_0 => ctp.[((3 * 320) + i_0)])), v); ctp <- (Array1088.init - (fun i_0 => (if ((3 * 320) <= i_0 < ((3 * 320) + 128)) then aux_5.[ + (fun i_0 => (if ((3 * 320) <= i_0 < ((3 * 320) + 128)) then aux_4.[ (i_0 - (3 * 320))] else ctp.[i_0])) ); - v <- aux_2; + v <- aux; return ctp; } proc __indcpa_dec_1 (msgp:W8.t Array32.t, ctp:W64.t, skp:W64.t) : W8.t Array32.t = { @@ -10161,7 +10139,7 @@ module M(SC:Syscall_t) = { return msgp; } proc __verify (ctp:W64.t, ctpc:W8.t Array1088.t) : W64.t = { - var aux:int; + var inc:int; var cnd:W64.t; var t64:W64.t; var h:W256.t; @@ -10179,9 +10157,9 @@ module M(SC:Syscall_t) = { cnd <- (W64.of_int 0); t64 <- (W64.of_int 1); h <- (set0_256); - aux <- (((3 * 320) + 128) %/ 32); + inc <- (((3 * 320) + 128) %/ 32); i <- 0; - while ((i < aux)) { + while ((i < inc)) { f <- (get256_direct (WArray1088.init8 (fun i_0 => ctpc.[i_0])) (32 * i)); g <- (loadW256 Glob.mem (W64.to_uint (ctp + (W64.of_int (32 * i))))); @@ -10192,9 +10170,9 @@ module M(SC:Syscall_t) = { ( _0, _1, _2, _3, zf) <- (VPTEST_256 h h); cnd <- ((! zf) ? t64 : cnd); off <- ((((3 * 320) + 128) %/ 32) * 32); - aux <- ((3 * 320) + 128); + inc <- ((3 * 320) + 128); i <- off; - while ((i < aux)) { + while ((i < inc)) { t1 <- (get8_direct (WArray1088.init8 (fun i_0 => ctpc.[i_0])) i); t2 <- (loadW8 Glob.mem (W64.to_uint (ctp + (W64.of_int i)))); t1 <- (t1 `^` t2); @@ -10207,7 +10185,7 @@ module M(SC:Syscall_t) = { return cnd; } proc __cmov (dst:W64.t, src:W8.t Array32.t, cnd:W64.t) : unit = { - var aux:int; + var inc:int; var scnd:W64.t; var m:W256.t; var i:int; @@ -10220,9 +10198,9 @@ module M(SC:Syscall_t) = { cnd <- (- cnd); scnd <- cnd; m <- (VPBROADCAST_4u64 scnd); - aux <- (32 %/ 32); + inc <- (32 %/ 32); i <- 0; - while ((i < aux)) { + while ((i < inc)) { f <- (get256_direct (WArray32.init8 (fun i_0 => src.[i_0])) (32 * i)); g <- (loadW256 Glob.mem (W64.to_uint (dst + (W64.of_int (32 * i))))); f <- (VPBLENDVB_256 f g m); @@ -10246,7 +10224,7 @@ module M(SC:Syscall_t) = { } proc __crypto_kem_keypair_jazz (pkp:W64.t, skp:W64.t, randomnessp:W8.t Array64.t) : unit = { - var aux:int; + var inc:int; var s_randomnessp:W8.t Array64.t; var s_pkp:W64.t; var s_skp:W64.t; @@ -10267,9 +10245,9 @@ module M(SC:Syscall_t) = { skp <- s_skp; skp <- (skp + (W64.of_int (3 * 384))); pkp <- s_pkp; - aux <- (((3 * 384) + 32) %/ 8); + inc <- (((3 * 384) + 32) %/ 8); i <- 0; - while ((i < aux)) { + while ((i < inc)) { t64 <- (loadW64 Glob.mem (W64.to_uint (pkp + (W64.of_int (8 * i))))); Glob.mem <- (storeW64 Glob.mem (W64.to_uint (skp + (W64.of_int 0))) t64); @@ -10290,9 +10268,9 @@ module M(SC:Syscall_t) = { } randomnessp <- s_randomnessp; randomnessp2 <- (Array32.init (fun i_0 => randomnessp.[(32 + i_0)])); - aux <- (32 %/ 8); + inc <- (32 %/ 8); i <- 0; - while ((i < aux)) { + while ((i < inc)) { t64 <- (get64 (WArray32.init8 (fun i_0 => randomnessp2.[i_0])) i); Glob.mem <- (storeW64 Glob.mem (W64.to_uint (skp + (W64.of_int 0))) t64); @@ -10303,8 +10281,8 @@ module M(SC:Syscall_t) = { } proc __crypto_kem_enc_jazz (ctp:W64.t, shkp:W64.t, pkp:W64.t, randomnessp:W8.t Array32.t) : unit = { - var aux:int; - var aux_0:W8.t Array32.t; + var aux:W8.t Array32.t; + var inc:int; var s_pkp:W64.t; var s_ctp:W64.t; var s_shkp:W64.t; @@ -10317,9 +10295,9 @@ module M(SC:Syscall_t) = { s_pkp <- pkp; s_ctp <- ctp; s_shkp <- shkp; - aux <- (32 %/ 8); + inc <- (32 %/ 8); i <- 0; - while ((i < aux)) { + while ((i < inc)) { t64 <- (get64 (WArray32.init8 (fun i_0 => randomnessp.[i_0])) i); buf <- (Array64.init @@ -10327,11 +10305,11 @@ module M(SC:Syscall_t) = { (WArray64.set64 (WArray64.init8 (fun i_0 => buf.[i_0])) i t64))); i <- (i + 1); } - aux_0 <@ _sha3_256A_M1184 ((Array32.init (fun i_0 => buf.[(32 + i_0)])), + aux <@ _sha3_256A_M1184 ((Array32.init (fun i_0 => buf.[(32 + i_0)])), pkp); buf <- (Array64.init - (fun i_0 => (if (32 <= i_0 < (32 + 32)) then aux_0.[(i_0 - 32)] else + (fun i_0 => (if (32 <= i_0 < (32 + 32)) then aux.[(i_0 - 32)] else buf.[i_0])) ); kr <@ _sha3_512A_A64 (kr, buf); @@ -10339,9 +10317,9 @@ module M(SC:Syscall_t) = { __indcpa_enc_0 (s_ctp, (Array32.init (fun i_0 => buf.[(0 + i_0)])), pkp, (Array32.init (fun i_0 => kr.[(32 + i_0)]))); shkp <- s_shkp; - aux <- (32 %/ 8); + inc <- (32 %/ 8); i <- 0; - while ((i < aux)) { + while ((i < inc)) { t64 <- (get64 (WArray64.init8 (fun i_0 => kr.[i_0])) i); Glob.mem <- (storeW64 Glob.mem (W64.to_uint (shkp + (W64.of_int (8 * i)))) t64); @@ -10350,8 +10328,8 @@ module M(SC:Syscall_t) = { return (); } proc __crypto_kem_dec_jazz (shkp:W64.t, ctp:W64.t, skp:W64.t) : unit = { - var aux_0:int; var aux:W8.t Array32.t; + var inc:int; var s_shkp:W64.t; var s_ctp:W64.t; var buf:W8.t Array64.t; @@ -10378,9 +10356,9 @@ module M(SC:Syscall_t) = { ); hp <- skp; hp <- (hp + (W64.of_int (32 + (((24 * 3) * 256) `|>>` 3)))); - aux_0 <- (32 %/ 8); + inc <- (32 %/ 8); i <- 0; - while ((i < aux_0)) { + while ((i < inc)) { t64 <- (loadW64 Glob.mem (W64.to_uint (hp + (W64.of_int (8 * i))))); buf <- (Array64.init diff --git a/code/jasmin/mlkem_avx2_stack/extraction/Makefile b/code/jasmin/mlkem_avx2_stack/extraction/Makefile index f2be4b8b..b1f703a6 100644 --- a/code/jasmin/mlkem_avx2_stack/extraction/Makefile +++ b/code/jasmin/mlkem_avx2_stack/extraction/Makefile @@ -9,11 +9,12 @@ # -------------------------------------------------------------------- all: ec -ec: - $(JASMINC) ../jkem.jazz -oec jkem_avx2_stack.ec \ - -ec jade_kem_mlkem_mlkem768_amd64_avx2_keypair_derand \ - -ec jade_kem_mlkem_mlkem768_amd64_avx2_enc_derand \ - -ec jade_kem_mlkem_mlkem768_amd64_avx2_dec + +ec: + $(JASMIN2EC) ../jkem.jazz --array-model=old -o jkem_avx2_stack.ec \ + -f jade_kem_mlkem_mlkem768_amd64_avx2_keypair_derand \ + -f jade_kem_mlkem_mlkem768_amd64_avx2_enc_derand \ + -f jade_kem_mlkem_mlkem768_amd64_avx2_dec clean: rm -f *.ec diff --git a/code/jasmin/mlkem_avx2_stack/extraction/jkem_avx2_stack.ec b/code/jasmin/mlkem_avx2_stack/extraction/jkem_avx2_stack.ec index 1e526d79..82e889ed 100644 --- a/code/jasmin/mlkem_avx2_stack/extraction/jkem_avx2_stack.ec +++ b/code/jasmin/mlkem_avx2_stack/extraction/jkem_avx2_stack.ec @@ -15,7 +15,7 @@ WArray800 WArray960 WArray1088 WArray1120 WArray1152 WArray1184 WArray1536 WArray2048 WArray2144 WArray2400 WArray4608. abbrev sample_shuffle_table = -(Array2048.of_list witness +((Array2048.of_list witness) [(W8.of_int (-1)); (W8.of_int (-1)); (W8.of_int (-1)); (W8.of_int (-1)); (W8.of_int (-1)); (W8.of_int (-1)); (W8.of_int (-1)); (W8.of_int (-1)); (W8.of_int 0); (W8.of_int (-1)); (W8.of_int (-1)); (W8.of_int (-1)); @@ -537,7 +537,7 @@ abbrev sample_ones = 454086624460063511464984254936031011189294057512315937409637584344757371137). abbrev sample_load_shuffle = -(Array32.of_list witness +((Array32.of_list witness) [(W8.of_int 0); (W8.of_int 1); (W8.of_int 1); (W8.of_int 2); (W8.of_int 3); (W8.of_int 4); (W8.of_int 4); (W8.of_int 5); (W8.of_int 6); (W8.of_int 7); (W8.of_int 7); (W8.of_int 8); (W8.of_int 9); (W8.of_int 10); (W8.of_int 10); @@ -547,7 +547,7 @@ abbrev sample_load_shuffle = (W8.of_int 14); (W8.of_int 14); (W8.of_int 15)]). abbrev gen_matrix_indexes = -(Array32.of_list witness +((Array32.of_list witness) [(W8.of_int 0); (W8.of_int 0); (W8.of_int 1); (W8.of_int 0); (W8.of_int 2); (W8.of_int 0); (W8.of_int 0); (W8.of_int 1); (W8.of_int 1); (W8.of_int 1); (W8.of_int 2); (W8.of_int 1); (W8.of_int 0); (W8.of_int 2); (W8.of_int 1); @@ -557,7 +557,7 @@ abbrev gen_matrix_indexes = (W8.of_int 2); (W8.of_int 1)]). abbrev pvc_shufbidx_s = -(Array32.of_list witness +((Array32.of_list witness) [(W8.of_int 0); (W8.of_int 1); (W8.of_int 2); (W8.of_int 3); (W8.of_int 4); (W8.of_int 8); (W8.of_int 9); (W8.of_int 10); (W8.of_int 11); (W8.of_int 12); (W8.of_int (-1)); (W8.of_int (-1)); (W8.of_int (-1)); (W8.of_int (-1)); @@ -582,7 +582,7 @@ abbrev pvd_mask_s = (W32.of_int 2145394680). abbrev pvd_sllvdidx_s = (W64.of_int 4). abbrev pvd_shufbdidx_s = -(Array32.of_list witness +((Array32.of_list witness) [(W8.of_int 0); (W8.of_int 1); (W8.of_int 1); (W8.of_int 2); (W8.of_int 2); (W8.of_int 3); (W8.of_int 3); (W8.of_int 4); (W8.of_int 5); (W8.of_int 6); (W8.of_int 6); (W8.of_int 7); (W8.of_int 7); (W8.of_int 8); (W8.of_int 8); @@ -594,7 +594,7 @@ abbrev pvd_shufbdidx_s = abbrev pvd_q_s = (W32.of_int 218182660). abbrev cbd_jshufbidx = -(Array32.of_list witness +((Array32.of_list witness) [(W8.of_int 0); (W8.of_int 1); (W8.of_int 2); (W8.of_int (-1)); (W8.of_int 3); (W8.of_int 4); (W8.of_int 5); (W8.of_int (-1)); (W8.of_int 6); (W8.of_int 7); (W8.of_int 8); (W8.of_int (-1)); (W8.of_int 9); @@ -605,14 +605,14 @@ abbrev cbd_jshufbidx = (W8.of_int 15); (W8.of_int (-1))]). abbrev pfm_idx_s = -(Array16.of_list witness +((Array16.of_list witness) [(W8.of_int 0); (W8.of_int 1); (W8.of_int 4); (W8.of_int 5); (W8.of_int 8); (W8.of_int 9); (W8.of_int 12); (W8.of_int 13); (W8.of_int 2); (W8.of_int 3); (W8.of_int 6); (W8.of_int 7); (W8.of_int 10); (W8.of_int 11); (W8.of_int 14); (W8.of_int 15)]). abbrev pfm_shift_s = -(Array4.of_list witness +((Array4.of_list witness) [(W32.of_int 3); (W32.of_int 2); (W32.of_int 1); (W32.of_int 0)]). abbrev pd_shift_s = (W32.of_int 8390656). @@ -620,7 +620,7 @@ abbrev pd_shift_s = (W32.of_int 8390656). abbrev pd_mask_s = (W32.of_int 15728655). abbrev pd_jshufbidx = -(Array32.of_list witness +((Array32.of_list witness) [(W8.of_int 0); (W8.of_int 0); (W8.of_int 0); (W8.of_int 0); (W8.of_int 1); (W8.of_int 1); (W8.of_int 1); (W8.of_int 1); (W8.of_int 2); (W8.of_int 2); (W8.of_int 2); (W8.of_int 2); (W8.of_int 3); (W8.of_int 3); (W8.of_int 3); @@ -630,7 +630,7 @@ abbrev pd_jshufbidx = (W8.of_int 7); (W8.of_int 7)]). abbrev pc_permidx_s = -(Array8.of_list witness +((Array8.of_list witness) [(W32.of_int 0); (W32.of_int 4); (W32.of_int 1); (W32.of_int 5); (W32.of_int 2); (W32.of_int 6); (W32.of_int 3); (W32.of_int 7)]). @@ -651,7 +651,7 @@ abbrev rOL56 = ). abbrev kECCAK_RHOTATES_RIGHT = -(Array6.of_list witness +((Array6.of_list witness) [(W256.of_int 144373339913893657577751063007562604548177214458152943091773); (W256.of_int 232252764209307188274174373867837442080505530800860351692863); (W256.of_int 156927543384667019098616994515559168111335794127330162507795); @@ -660,7 +660,7 @@ abbrev kECCAK_RHOTATES_RIGHT = (W256.of_int 313855086769334038206421612937983674734430261968315659321364)]). abbrev kECCAK_RHOTATES_LEFT = -(Array6.of_list witness +((Array6.of_list witness) [(W256.of_int 257361171150853911329517531560668107745210100483895842570243); (W256.of_int 169481746855440380633094220700393270212881784141188433969153); (W256.of_int 244806967680080549808651600052671544182051520814718623154221); @@ -669,7 +669,7 @@ abbrev kECCAK_RHOTATES_LEFT = (W256.of_int 87879424295413530700846981630247037558957052973733126340652)]). abbrev kECCAK1600_RC = -(Array24.of_list witness +((Array24.of_list witness) [(W64.of_int 1); (W64.of_int 32898); (W64.of_int (-9223372036854742902)); (W64.of_int (-9223372034707259392)); (W64.of_int 32907); (W64.of_int 2147483649); (W64.of_int (-9223372034707259263)); @@ -683,14 +683,14 @@ abbrev kECCAK1600_RC = (W64.of_int (-9223372034707259384))]). abbrev jdmontx16 = -(Array16.of_list witness +((Array16.of_list witness) [(W16.of_int 1353); (W16.of_int 1353); (W16.of_int 1353); (W16.of_int 1353); (W16.of_int 1353); (W16.of_int 1353); (W16.of_int 1353); (W16.of_int 1353); (W16.of_int 1353); (W16.of_int 1353); (W16.of_int 1353); (W16.of_int 1353); (W16.of_int 1353); (W16.of_int 1353); (W16.of_int 1353); (W16.of_int 1353)]). abbrev mqinvx16 = -(Array16.of_list witness +((Array16.of_list witness) [(W16.of_int 15099); (W16.of_int 15099); (W16.of_int 15099); (W16.of_int 15099); (W16.of_int 15099); (W16.of_int 15099); (W16.of_int 15099); (W16.of_int 15099); (W16.of_int 15099); @@ -699,35 +699,35 @@ abbrev mqinvx16 = (W16.of_int 15099)]). abbrev hhqx16 = -(Array16.of_list witness +((Array16.of_list witness) [(W16.of_int 832); (W16.of_int 832); (W16.of_int 832); (W16.of_int 832); (W16.of_int 832); (W16.of_int 832); (W16.of_int 832); (W16.of_int 832); (W16.of_int 832); (W16.of_int 832); (W16.of_int 832); (W16.of_int 832); (W16.of_int 832); (W16.of_int 832); (W16.of_int 832); (W16.of_int 832)]). abbrev hqx16_m1 = -(Array16.of_list witness +((Array16.of_list witness) [(W16.of_int 1664); (W16.of_int 1664); (W16.of_int 1664); (W16.of_int 1664); (W16.of_int 1664); (W16.of_int 1664); (W16.of_int 1664); (W16.of_int 1664); (W16.of_int 1664); (W16.of_int 1664); (W16.of_int 1664); (W16.of_int 1664); (W16.of_int 1664); (W16.of_int 1664); (W16.of_int 1664); (W16.of_int 1664)]). abbrev hqx16_p1 = -(Array16.of_list witness +((Array16.of_list witness) [(W16.of_int 1665); (W16.of_int 1665); (W16.of_int 1665); (W16.of_int 1665); (W16.of_int 1665); (W16.of_int 1665); (W16.of_int 1665); (W16.of_int 1665); (W16.of_int 1665); (W16.of_int 1665); (W16.of_int 1665); (W16.of_int 1665); (W16.of_int 1665); (W16.of_int 1665); (W16.of_int 1665); (W16.of_int 1665)]). abbrev maskx16 = -(Array16.of_list witness +((Array16.of_list witness) [(W16.of_int 4095); (W16.of_int 4095); (W16.of_int 4095); (W16.of_int 4095); (W16.of_int 4095); (W16.of_int 4095); (W16.of_int 4095); (W16.of_int 4095); (W16.of_int 4095); (W16.of_int 4095); (W16.of_int 4095); (W16.of_int 4095); (W16.of_int 4095); (W16.of_int 4095); (W16.of_int 4095); (W16.of_int 4095)]). abbrev jflox16 = -(Array16.of_list witness +((Array16.of_list witness) [(W16.of_int (-10079)); (W16.of_int (-10079)); (W16.of_int (-10079)); (W16.of_int (-10079)); (W16.of_int (-10079)); (W16.of_int (-10079)); (W16.of_int (-10079)); (W16.of_int (-10079)); (W16.of_int (-10079)); @@ -736,14 +736,14 @@ abbrev jflox16 = (W16.of_int (-10079))]). abbrev jfhix16 = -(Array16.of_list witness +((Array16.of_list witness) [(W16.of_int 1441); (W16.of_int 1441); (W16.of_int 1441); (W16.of_int 1441); (W16.of_int 1441); (W16.of_int 1441); (W16.of_int 1441); (W16.of_int 1441); (W16.of_int 1441); (W16.of_int 1441); (W16.of_int 1441); (W16.of_int 1441); (W16.of_int 1441); (W16.of_int 1441); (W16.of_int 1441); (W16.of_int 1441)]). abbrev jvx16 = -(Array16.of_list witness +((Array16.of_list witness) [(W16.of_int 20159); (W16.of_int 20159); (W16.of_int 20159); (W16.of_int 20159); (W16.of_int 20159); (W16.of_int 20159); (W16.of_int 20159); (W16.of_int 20159); (W16.of_int 20159); @@ -752,7 +752,7 @@ abbrev jvx16 = (W16.of_int 20159)]). abbrev jqinvx16 = -(Array16.of_list witness +((Array16.of_list witness) [(W16.of_int (-3327)); (W16.of_int (-3327)); (W16.of_int (-3327)); (W16.of_int (-3327)); (W16.of_int (-3327)); (W16.of_int (-3327)); (W16.of_int (-3327)); (W16.of_int (-3327)); (W16.of_int (-3327)); @@ -761,14 +761,14 @@ abbrev jqinvx16 = (W16.of_int (-3327))]). abbrev jqx16 = -(Array16.of_list witness +((Array16.of_list witness) [(W16.of_int 3329); (W16.of_int 3329); (W16.of_int 3329); (W16.of_int 3329); (W16.of_int 3329); (W16.of_int 3329); (W16.of_int 3329); (W16.of_int 3329); (W16.of_int 3329); (W16.of_int 3329); (W16.of_int 3329); (W16.of_int 3329); (W16.of_int 3329); (W16.of_int 3329); (W16.of_int 3329); (W16.of_int 3329)]). abbrev jzetas_inv_exp = -(Array400.of_list witness +((Array400.of_list witness) [(W16.of_int (-23131)); (W16.of_int (-7756)); (W16.of_int 20258); (W16.of_int 23860); (W16.of_int 17443); (W16.of_int (-23210)); (W16.of_int 20199); (W16.of_int 21498); (W16.of_int (-14469)); @@ -889,7 +889,7 @@ abbrev jzetas_inv_exp = (W16.of_int 0)]). abbrev jzetas_exp = -(Array400.of_list witness +((Array400.of_list witness) [(W16.of_int 31499); (W16.of_int 31499); (W16.of_int 2571); (W16.of_int 2571); (W16.of_int 14746); (W16.of_int 14746); (W16.of_int 2970); (W16.of_int 2970); (W16.of_int 13525); (W16.of_int 13525); @@ -1008,7 +1008,7 @@ abbrev jzetas_exp = (W16.of_int 0)]). abbrev jzetas_inv = -(Array128.of_list witness +((Array128.of_list witness) [(W16.of_int 1701); (W16.of_int 1807); (W16.of_int 1460); (W16.of_int 2371); (W16.of_int 2338); (W16.of_int 2333); (W16.of_int 308); (W16.of_int 108); (W16.of_int 2851); (W16.of_int 870); (W16.of_int 854); (W16.of_int 1510); @@ -1043,7 +1043,7 @@ abbrev jzetas_inv = (W16.of_int 1517); (W16.of_int 359); (W16.of_int 758); (W16.of_int 1441)]). abbrev jzetas = -(Array128.of_list witness +((Array128.of_list witness) [(W16.of_int 2285); (W16.of_int 2571); (W16.of_int 2970); (W16.of_int 1812); (W16.of_int 1493); (W16.of_int 1422); (W16.of_int 287); (W16.of_int 202); (W16.of_int 3158); (W16.of_int 622); (W16.of_int 1577); (W16.of_int 182); @@ -1289,7 +1289,6 @@ module M = { return r; } proc keccakf1600_rho_offsets (i:int) : int = { - var aux:int; var r:int; var x:int; var y:int; @@ -2027,7 +2026,6 @@ module M = { return t256; } proc __state_init_avx2 () : W256.t Array7.t = { - var aux:int; var st:W256.t Array7.t; var i:int; st <- witness; @@ -2040,16 +2038,16 @@ module M = { } proc __pstate_init_avx2 (pst:W64.t Array25.t) : W64.t Array25.t * W256.t Array7.t = { - var aux:int; + var inc:int; var st:W256.t Array7.t; var z256:W256.t; var i:int; var z64:W64.t; st <- witness; z256 <- (set0_256); - aux <- (25 %/ 4); + inc <- (25 %/ 4); i <- 0; - while ((i < aux)) { + while ((i < inc)) { pst <- (Array25.init (WArray200.get64 @@ -2193,10 +2191,10 @@ module M = { return (st3, st4, st5, st6); } proc __state_from_pstate_avx2 (pst:W64.t Array25.t) : W256.t Array7.t = { - var aux_2:W256.t; - var aux_1:W256.t; - var aux_0:W256.t; var aux:W256.t; + var aux_0:W256.t; + var aux_1:W256.t; + var aux_2:W256.t; var st:W256.t Array7.t; var t128_0:W128.t; var t128_1:W128.t; @@ -2221,12 +2219,12 @@ module M = { (((W128.to_uint t128_1) %% (2 ^ 128)) + ((2 ^ 128) * (W128.to_uint t128_0)))); st.[6] <- (get256_direct (WArray200.init64 (fun i => pst.[i])) (21 * 8)); - (aux_2, aux_1, aux_0, aux) <@ __perm_reg3456_avx2 (st.[3], st.[4], + (aux, aux_0, aux_1, aux_2) <@ __perm_reg3456_avx2 (st.[3], st.[4], st.[5], st.[6]); - st.[3] <- aux_2; - st.[4] <- aux_1; - st.[5] <- aux_0; - st.[6] <- aux; + st.[3] <- aux; + st.[4] <- aux_0; + st.[5] <- aux_1; + st.[6] <- aux_2; return st; } proc __addstate_r3456_avx2 (st:W256.t Array7.t, r3:W256.t, r4:W256.t, @@ -2418,7 +2416,6 @@ module M = { return st; } proc keccakf1600_4x_theta_sum (a:W256.t Array25.t) : W256.t Array5.t = { - var aux:int; var c:W256.t Array5.t; var x:int; var y:int; @@ -2457,7 +2454,6 @@ module M = { } proc keccakf1600_4x_theta_rol (c:W256.t Array5.t, r8:W256.t, r56:W256.t) : W256.t Array5.t = { - var aux:int; var d:W256.t Array5.t; var x:int; d <- witness; @@ -2472,7 +2468,6 @@ module M = { } proc keccakf1600_4x_rol_sum (a:W256.t Array25.t, d:W256.t Array5.t, y:int, r8:W256.t, r56:W256.t) : W256.t Array5.t = { - var aux:int; var b:W256.t Array5.t; var x:int; var x_:int; @@ -2497,7 +2492,6 @@ module M = { } proc keccakf1600_4x_set_row (e:W256.t Array25.t, b:W256.t Array5.t, y:int, rc:W256.t) : W256.t Array25.t = { - var aux:int; var x:int; var x1:int; var x2:int; @@ -2520,7 +2514,6 @@ module M = { } proc _keccakf1600_4x_round (e:W256.t Array25.t, a:W256.t Array25.t, rc:W256.t, r8:W256.t, r56:W256.t) : W256.t Array25.t = { - var aux:int; var c:W256.t Array5.t; var d:W256.t Array5.t; var y:int; @@ -6466,7 +6459,6 @@ module M = { return (st, buf); } proc _poly_add2 (rp:W16.t Array256.t, bp:W16.t Array256.t) : W16.t Array256.t = { - var aux:int; var i:int; var a:W256.t; var b:W256.t; @@ -6486,7 +6478,6 @@ module M = { return rp; } proc _poly_csubq (rp:W16.t Array256.t) : W16.t Array256.t = { - var aux:int; var qx16:W256.t; var i:int; var r:W256.t; @@ -6738,7 +6729,7 @@ module M = { return rp; } proc _poly_frommont (rp:W16.t Array256.t) : W16.t Array256.t = { - var aux:int; + var inc:int; var x16p:W16.t Array16.t; var qx16:W256.t; var qinvx16:W256.t; @@ -6752,9 +6743,9 @@ module M = { qinvx16 <- (get256 (WArray32.init16 (fun i_0 => x16p.[i_0])) 0); x16p <- jdmontx16; dmontx16 <- (get256 (WArray32.init16 (fun i_0 => x16p.[i_0])) 0); - aux <- (256 %/ 16); + inc <- (256 %/ 16); i <- 0; - while ((i < aux)) { + while ((i < inc)) { t <- (get256 (WArray512.init16 (fun i_0 => rp.[i_0])) i); t <@ __fqmulx16 (t, dmontx16, qx16, qinvx16); rp <- @@ -6766,7 +6757,7 @@ module M = { return rp; } proc __cbd3 (rp:W16.t Array256.t, buf:W8.t Array128.t) : W16.t Array256.t = { - var aux:int; + var inc:int; var mask249_s:W32.t; var mask6DB_s:W32.t; var mask07_s:W32.t; @@ -6794,9 +6785,9 @@ module M = { mask70 <- (VPBROADCAST_8u32 mask70_s); mask3 <- (VPBROADCAST_16u16 mask3_s); shufbidx <- (get256 (WArray32.init8 (fun i_0 => cbd_jshufbidx.[i_0])) 0); - aux <- (256 %/ 32); + inc <- (256 %/ 32); i <- 0; - while ((i < aux)) { + while ((i < inc)) { f0 <- (get256_direct (WArray128.init8 (fun i_0 => buf.[i_0])) (24 * i)); f0 <- (VPERMQ f0 (W8.of_int 148)); @@ -6841,7 +6832,7 @@ module M = { return rp; } proc __cbd2 (rp:W16.t Array256.t, buf:W8.t Array128.t) : W16.t Array256.t = { - var aux:int; + var inc:int; var mask55_s:W32.t; var mask33_s:W32.t; var mask03_s:W32.t; @@ -6864,9 +6855,9 @@ module M = { mask33 <- (VPBROADCAST_8u32 mask33_s); mask03 <- (VPBROADCAST_8u32 mask03_s); mask0F <- (VPBROADCAST_8u32 mask0F_s); - aux <- (256 %/ 64); + inc <- (256 %/ 64); i <- 0; - while ((i < aux)) { + while ((i < inc)) { f0 <- (get256 (WArray128.init8 (fun i_0 => buf.[i_0])) i); f1 <- (VPSRL_16u16 f0 (W128.of_int 1)); f0 <- (VPAND_256 mask55 f0); @@ -7008,7 +6999,6 @@ module M = { return (rl0, rl1, rl2, rl3, rh0, rh1, rh2, rh3); } proc _poly_invntt (rp:W16.t Array256.t) : W16.t Array256.t = { - var aux:int; var zetasp:W16.t Array400.t; var qx16:W256.t; var i:int; @@ -7318,7 +7308,6 @@ module M = { return (rl0, rl1, rl2, rl3, rh0, rh1, rh2, rh3); } proc _poly_ntt (rp:W16.t Array256.t) : W16.t Array256.t = { - var aux:int; var zetasp:W16.t Array400.t; var qx16:W256.t; var zeta0:W256.t; @@ -7581,7 +7570,6 @@ module M = { return rp; } proc __poly_reduce (rp:W16.t Array256.t) : W16.t Array256.t = { - var aux:int; var qx16:W256.t; var vx16:W256.t; var i:int; @@ -7603,7 +7591,6 @@ module M = { } proc _poly_sub (rp:W16.t Array256.t, ap:W16.t Array256.t, bp:W16.t Array256.t) : W16.t Array256.t = { - var aux:int; var i:int; var a:W256.t; var b:W256.t; @@ -8105,7 +8092,7 @@ module M = { } proc _i_poly_compress (rp:W8.t Array128.t, a:W16.t Array256.t) : W8.t Array128.t * W16.t Array256.t = { - var aux:int; + var inc:int; var x16p:W16.t Array16.t; var v:W256.t; var shift1:W256.t; @@ -8125,9 +8112,9 @@ module M = { mask <- (VPBROADCAST_16u16 pc_mask_s); shift2 <- (VPBROADCAST_16u16 pc_shift2_s); permidx <- (get256 (WArray32.init32 (fun i_0 => pc_permidx_s.[i_0])) 0); - aux <- (256 %/ 64); + inc <- (256 %/ 64); i <- 0; - while ((i < aux)) { + while ((i < inc)) { f0 <- (get256 (WArray512.init16 (fun i_0 => a.[i_0])) (4 * i)); f1 <- (get256 (WArray512.init16 (fun i_0 => a.[i_0])) ((4 * i) + 1)); f2 <- (get256 (WArray512.init16 (fun i_0 => a.[i_0])) ((4 * i) + 2)); @@ -8161,7 +8148,7 @@ module M = { } proc _i_poly_decompress (rp:W16.t Array256.t, a:W8.t Array128.t) : W16.t Array256.t = { - var aux:int; + var inc:int; var x16p:W16.t Array16.t; var q:W256.t; var x32p:W8.t Array32.t; @@ -8181,9 +8168,9 @@ module M = { mask <- (VPBROADCAST_8u32 pd_mask_s); shift <- (VPBROADCAST_8u32 pd_shift_s); f <- (set0_256); - aux <- (256 %/ 16); + inc <- (256 %/ 16); i <- 0; - while ((i < aux)) { + while ((i < inc)) { h <- (zeroextu128 (get64_direct (WArray128.init8 (fun i_0 => a.[i_0])) (8 * i))); @@ -8203,7 +8190,6 @@ module M = { } proc _i_poly_frombytes (rp:W16.t Array256.t, ap:W8.t Array384.t) : W16.t Array256.t = { - var aux:int; var maskp:W16.t Array16.t; var mask:W256.t; var i:int; @@ -8321,7 +8307,6 @@ module M = { return rp; } proc _i_poly_frommsg (rp:W16.t Array256.t, ap:W8.t Array32.t) : W16.t Array256.t = { - var aux:int; var x16p:W16.t Array16.t; var hqs:W256.t; var shift:W256.t; @@ -8396,7 +8381,6 @@ module M = { } proc _i_poly_tobytes (rp:W8.t Array384.t, a:W16.t Array256.t) : W8.t Array384.t * W16.t Array256.t = { - var aux:int; var jqx16_p:W16.t Array16.t; var qx16:W256.t; var i:int; @@ -8488,7 +8472,7 @@ module M = { } proc _i_poly_tomsg (rp:W8.t Array32.t, a:W16.t Array256.t) : W8.t Array32.t * W16.t Array256.t = { - var aux:int; + var inc:int; var px16:W16.t Array16.t; var hq:W256.t; var hhq:W256.t; @@ -8504,9 +8488,9 @@ module M = { hq <- (get256 (WArray32.init16 (fun i_0 => px16.[i_0])) 0); px16 <- hhqx16; hhq <- (get256 (WArray32.init16 (fun i_0 => px16.[i_0])) 0); - aux <- (256 %/ 32); + inc <- (256 %/ 32); i <- 0; - while ((i < aux)) { + while ((i < inc)) { f0 <- (get256 (WArray512.init16 (fun i_0 => a.[i_0])) (2 * i)); f1 <- (get256 (WArray512.init16 (fun i_0 => a.[i_0])) ((2 * i) + 1)); f0 <- (VPSUB_16u16 hq f0); @@ -8641,7 +8625,7 @@ module M = { return r; } proc __i_polyvec_decompress (rp:W8.t Array1088.t) : W16.t Array768.t = { - var aux:int; + var inc:int; var r:W16.t Array768.t; var q:W256.t; var shufbidx:W256.t; @@ -8658,9 +8642,9 @@ module M = { mask <- (VPBROADCAST_8u32 pvd_mask_s); k <- 0; while ((k < 3)) { - aux <- (256 %/ 16); + inc <- (256 %/ 16); i <- 0; - while ((i < aux)) { + while ((i < inc)) { f <- (get256_direct (WArray1088.init8 (fun i_0 => rp.[i_0])) ((320 * k) + (20 * i))); @@ -8683,7 +8667,7 @@ module M = { } proc __i_polyvec_compress (rp:W8.t Array960.t, a:W16.t Array768.t) : W8.t Array960.t = { - var aux:int; + var inc:int; var x16p:W16.t Array16.t; var v:W256.t; var v8:W256.t; @@ -8711,9 +8695,9 @@ module M = { sllvdidx <- (VPBROADCAST_4u64 pvc_sllvdidx_s); shufbidx <- (get256 (WArray32.init8 (fun i_0 => pvc_shufbidx_s.[i_0])) 0); - aux <- ((3 * 256) %/ 16); + inc <- ((3 * 256) %/ 16); i <- 0; - while ((i < aux)) { + while ((i < inc)) { f0 <- (get256 (WArray1536.init16 (fun i_0 => a.[i_0])) i); f1 <- (VPMULL_16u16 f0 v8); f2 <- (VPADD_16u16 f0 off); @@ -8785,8 +8769,8 @@ module M = { } proc __i_polyvec_tobytes (r:W8.t Array1152.t, a:W16.t Array768.t) : W8.t Array1152.t = { - var aux:W8.t Array384.t; var aux_0:W16.t Array256.t; + var aux:W8.t Array384.t; (aux, aux_0) <@ _i_poly_tobytes ((Array384.init (fun i => r.[(0 + i)])), (Array256.init (fun i => a.[(0 + i)]))); r <- @@ -9177,9 +9161,9 @@ module M = { rho:W8.t Array32.t, pos_entry:W64.t, transposed:W64.t) : W16.t Array1024.t * W8.t Array2144.t = { + var aux_0:W16.t Array256.t; var aux:W64.t; var aux_1:W8.t Array536.t; - var aux_0:W16.t Array256.t; var indexes:W8.t Array8.t; var state:W256.t Array25.t; var stx4:W256.t Array25.t; @@ -9282,9 +9266,8 @@ module M = { } proc _gen_matrix_avx2 (matrix:W16.t Array2304.t, rho:W8.t Array32.t, transposed:W64.t) : W16.t Array2304.t = { - var aux:int; - var aux_1:W8.t Array536.t; - var aux_0:W16.t Array256.t; + var aux:W16.t Array256.t; + var aux_0:W8.t Array536.t; var buf_s:W8.t Array2144.t; var buf:W8.t Array2144.t; var i:int; @@ -9316,12 +9299,12 @@ module M = { } pol <- (Array256.init (fun i_0 => matrix.[((8 * 256) + i_0)])); rc <- (W16.of_int 514); - (aux_0, aux_1) <@ __gen_matrix_sample_one_polynomial (pol, + (aux, aux_0) <@ __gen_matrix_sample_one_polynomial (pol, (Array536.init (fun i_0 => buf.[((536 * 0) + i_0)])), rho, rc); - pol <- aux_0; + pol <- aux; buf <- (Array2144.init - (fun i_0 => (if ((536 * 0) <= i_0 < ((536 * 0) + 536)) then aux_1.[ + (fun i_0 => (if ((536 * 0) <= i_0 < ((536 * 0) + 536)) then aux_0.[ (i_0 - (536 * 0))] else buf.[i_0])) @@ -9337,18 +9320,17 @@ module M = { while ((i < 3)) { j <- 0; while ((j < 3)) { - aux_0 <@ _nttunpack ((Array256.init - (fun i_0 => matrix.[(((i * (3 * 256)) + - (j * 256)) + - i_0)]) - )); + aux <@ _nttunpack ((Array256.init + (fun i_0 => matrix.[(((i * (3 * 256)) + (j * 256)) + + i_0)]) + )); matrix <- (Array2304.init (fun i_0 => (if (((i * (3 * 256)) + (j * 256)) <= i_0 < (((i * (3 * 256)) + (j * 256)) + 256)) then - aux_0.[(i_0 - ((i * (3 * 256)) + (j * 256)))] else + aux.[(i_0 - ((i * (3 * 256)) + (j * 256)))] else matrix.[i_0])) ); j <- (j + 1); @@ -9360,12 +9342,12 @@ module M = { proc __indcpa_keypair (pk:W8.t Array1184.t, sk:W8.t Array2400.t, randomnessp:W8.t Array32.t) : W8.t Array1184.t * W8.t Array2400.t = { - var aux:int; - var aux_4:W8.t Array1152.t; - var aux_3:W16.t Array256.t; - var aux_2:W16.t Array256.t; - var aux_1:W16.t Array256.t; + var aux:W16.t Array256.t; var aux_0:W16.t Array256.t; + var aux_1:W16.t Array256.t; + var aux_2:W16.t Array256.t; + var aux_3:W8.t Array1152.t; + var inc:int; var i:int; var t64:W64.t; var inbuf:W8.t Array33.t; @@ -9387,9 +9369,9 @@ module M = { publicseed <- witness; skpv <- witness; (* Erased call to spill *) - aux <- (32 %/ 8); + inc <- (32 %/ 8); i <- 0; - while ((i < aux)) { + while ((i < inc)) { t64 <- (get64 (WArray32.init8 (fun i_0 => randomnessp.[i_0])) i); inbuf <- (Array33.init @@ -9399,9 +9381,9 @@ module M = { } inbuf.[32] <- (W8.of_int 3); buf <@ _sha3_512A_A33 (buf, inbuf); - aux <- (32 %/ 8); + inc <- (32 %/ 8); i <- 0; - while ((i < aux)) { + while ((i < inc)) { t64 <- (get64 (WArray64.init8 (fun i_0 => buf.[i_0])) i); publicseed <- (Array32.init @@ -9417,21 +9399,20 @@ module M = { transposed <- (W64.of_int 0); aa <@ _gen_matrix_avx2 (aa, publicseed, transposed); nonce <- (W8.of_int 0); - (aux_3, aux_2, aux_1, aux_0) <@ _poly_getnoise_eta1_4x ((Array256.init - (fun i_0 => - skpv.[(0 + i_0)]) - ), + (aux, aux_0, aux_1, aux_2) <@ _poly_getnoise_eta1_4x ((Array256.init + (fun i_0 => + skpv.[(0 + i_0)])), (Array256.init (fun i_0 => skpv.[(256 + i_0)])), (Array256.init (fun i_0 => skpv.[((2 * 256) + i_0)])), (Array256.init (fun i_0 => e.[(0 + i_0)])), noiseseed, nonce); skpv <- (Array768.init - (fun i_0 => (if (0 <= i_0 < (0 + 256)) then aux_3.[(i_0 - 0)] else + (fun i_0 => (if (0 <= i_0 < (0 + 256)) then aux.[(i_0 - 0)] else skpv.[i_0])) ); skpv <- (Array768.init - (fun i_0 => (if (256 <= i_0 < (256 + 256)) then aux_2.[(i_0 - 256)] else + (fun i_0 => (if (256 <= i_0 < (256 + 256)) then aux_0.[(i_0 - 256)] else skpv.[i_0])) ); skpv <- @@ -9443,24 +9424,24 @@ module M = { ); e <- (Array768.init - (fun i_0 => (if (0 <= i_0 < (0 + 256)) then aux_0.[(i_0 - 0)] else + (fun i_0 => (if (0 <= i_0 < (0 + 256)) then aux_2.[(i_0 - 0)] else e.[i_0])) ); nonce <- (W8.of_int 4); - (aux_3, aux_2, aux_1, aux_0) <@ _poly_getnoise_eta1_4x ((Array256.init - (fun i_0 => - e.[(256 + i_0)])), + (aux, aux_0, aux_1, aux_2) <@ _poly_getnoise_eta1_4x ((Array256.init + (fun i_0 => + e.[(256 + i_0)])), (Array256.init (fun i_0 => e.[((2 * 256) + i_0)])), (Array256.init (fun i_0 => pkpv.[(0 + i_0)])), (Array256.init (fun i_0 => pkpv.[(256 + i_0)])), noiseseed, nonce); e <- (Array768.init - (fun i_0 => (if (256 <= i_0 < (256 + 256)) then aux_3.[(i_0 - 256)] else + (fun i_0 => (if (256 <= i_0 < (256 + 256)) then aux.[(i_0 - 256)] else e.[i_0])) ); e <- (Array768.init - (fun i_0 => (if ((2 * 256) <= i_0 < ((2 * 256) + 256)) then aux_2.[ + (fun i_0 => (if ((2 * 256) <= i_0 < ((2 * 256) + 256)) then aux_0.[ (i_0 - (2 * 256))] else e.[i_0])) @@ -9472,29 +9453,28 @@ module M = { ); pkpv <- (Array768.init - (fun i_0 => (if (256 <= i_0 < (256 + 256)) then aux_0.[(i_0 - 256)] else + (fun i_0 => (if (256 <= i_0 < (256 + 256)) then aux_2.[(i_0 - 256)] else pkpv.[i_0])) ); skpv <@ __polyvec_ntt (skpv); e <@ __polyvec_ntt (e); i <- 0; while ((i < 3)) { - aux_3 <@ __polyvec_pointwise_acc ((Array256.init - (fun i_0 => pkpv.[((i * 256) + i_0)]) - ), + aux <@ __polyvec_pointwise_acc ((Array256.init + (fun i_0 => pkpv.[((i * 256) + i_0)])), (Array768.init (fun i_0 => aa.[((i * (3 * 256)) + i_0)])), skpv); pkpv <- (Array768.init - (fun i_0 => (if ((i * 256) <= i_0 < ((i * 256) + 256)) then aux_3.[ + (fun i_0 => (if ((i * 256) <= i_0 < ((i * 256) + 256)) then aux.[ (i_0 - (i * 256))] else pkpv.[i_0])) ); - aux_3 <@ _poly_frommont ((Array256.init - (fun i_0 => pkpv.[((i * 256) + i_0)]))); + aux <@ _poly_frommont ((Array256.init + (fun i_0 => pkpv.[((i * 256) + i_0)]))); pkpv <- (Array768.init - (fun i_0 => (if ((i * 256) <= i_0 < ((i * 256) + 256)) then aux_3.[ + (fun i_0 => (if ((i * 256) <= i_0 < ((i * 256) + 256)) then aux.[ (i_0 - (i * 256))] else pkpv.[i_0])) @@ -9504,25 +9484,25 @@ module M = { pkpv <@ __polyvec_add2 (pkpv, e); pkpv <@ __polyvec_reduce (pkpv); (* Erased call to unspill *) - aux_4 <@ __i_polyvec_tobytes ((Array1152.init (fun i_0 => sk.[(0 + i_0)]) + aux_3 <@ __i_polyvec_tobytes ((Array1152.init (fun i_0 => sk.[(0 + i_0)]) ), skpv); sk <- (Array2400.init - (fun i_0 => (if (0 <= i_0 < (0 + 1152)) then aux_4.[(i_0 - 0)] else + (fun i_0 => (if (0 <= i_0 < (0 + 1152)) then aux_3.[(i_0 - 0)] else sk.[i_0])) ); - aux_4 <@ __i_polyvec_tobytes ((Array1152.init (fun i_0 => pk.[(0 + i_0)]) + aux_3 <@ __i_polyvec_tobytes ((Array1152.init (fun i_0 => pk.[(0 + i_0)]) ), pkpv); pk <- (Array1184.init - (fun i_0 => (if (0 <= i_0 < (0 + 1152)) then aux_4.[(i_0 - 0)] else + (fun i_0 => (if (0 <= i_0 < (0 + 1152)) then aux_3.[(i_0 - 0)] else pk.[i_0])) ); - aux <- (32 %/ 8); + inc <- (32 %/ 8); i <- 0; - while ((i < aux)) { + while ((i < inc)) { t64 <- (get64 (WArray32.init8 (fun i_0 => publicseed.[i_0])) i); pk <- (Array1184.init @@ -9536,13 +9516,13 @@ module M = { proc __indcpa_enc (ct:W8.t Array1088.t, msgp:W8.t Array32.t, pk:W8.t Array1184.t, noiseseed:W8.t Array32.t) : W8.t Array1088.t = { - var aux:int; - var aux_5:W8.t Array128.t; - var aux_4:W8.t Array960.t; - var aux_3:W16.t Array256.t; - var aux_2:W16.t Array256.t; - var aux_1:W16.t Array256.t; + var aux:W16.t Array256.t; var aux_0:W16.t Array256.t; + var aux_1:W16.t Array256.t; + var aux_2:W16.t Array256.t; + var aux_4:W8.t Array128.t; + var aux_3:W8.t Array960.t; + var inc:int; var pkpv:W16.t Array768.t; var w:int; var t64:W64.t; @@ -9570,9 +9550,9 @@ module M = { sp_0 <- witness; v <- witness; pkpv <@ __i_polyvec_frombytes ((Array1152.init (fun i => pk.[(0 + i)]))); - aux <- (32 %/ 8); + inc <- (32 %/ 8); w <- 0; - while ((w < aux)) { + while ((w < inc)) { t64 <- (get64_direct (WArray1184.init8 (fun i => pk.[i])) ((((3 * 384) %/ 8) + w) * 8)); @@ -9588,18 +9568,20 @@ module M = { aat <@ _gen_matrix_avx2 (aat, publicseed, transposed); lnoiseseed <- s_noiseseed; nonce <- (W8.of_int 0); - (aux_3, aux_2, aux_1, aux_0) <@ _poly_getnoise_eta1_4x ((Array256.init - (fun i => - sp_0.[(0 + i)])), + (aux, aux_0, aux_1, aux_2) <@ _poly_getnoise_eta1_4x ((Array256.init + (fun i => sp_0.[ + (0 + + i)]) + ), (Array256.init (fun i => sp_0.[(256 + i)])), (Array256.init (fun i => sp_0.[((2 * 256) + i)])), (Array256.init (fun i => ep.[(0 + i)])), lnoiseseed, nonce); sp_0 <- (Array768.init - (fun i => (if (0 <= i < (0 + 256)) then aux_3.[(i - 0)] else sp_0.[i]))); + (fun i => (if (0 <= i < (0 + 256)) then aux.[(i - 0)] else sp_0.[i]))); sp_0 <- (Array768.init - (fun i => (if (256 <= i < (256 + 256)) then aux_2.[(i - 256)] else + (fun i => (if (256 <= i < (256 + 256)) then aux_0.[(i - 256)] else sp_0.[i])) ); sp_0 <- @@ -9610,39 +9592,40 @@ module M = { ); ep <- (Array768.init - (fun i => (if (0 <= i < (0 + 256)) then aux_0.[(i - 0)] else ep.[i]))); + (fun i => (if (0 <= i < (0 + 256)) then aux_2.[(i - 0)] else ep.[i]))); lnoiseseed <- s_noiseseed; nonce <- (W8.of_int 4); - (aux_3, aux_2, aux_1, aux_0) <@ _poly_getnoise_eta1_4x ((Array256.init - (fun i => - ep.[(256 + i)])), + (aux, aux_0, aux_1, aux_2) <@ _poly_getnoise_eta1_4x ((Array256.init + (fun i => ep.[ + (256 + + i)]) + ), (Array256.init (fun i => ep.[((2 * 256) + i)])), epp, (Array256.init (fun i => bp.[(0 + i)])), lnoiseseed, nonce); ep <- (Array768.init - (fun i => (if (256 <= i < (256 + 256)) then aux_3.[(i - 256)] else - ep.[i])) + (fun i => (if (256 <= i < (256 + 256)) then aux.[(i - 256)] else ep.[i])) ); ep <- (Array768.init - (fun i => (if ((2 * 256) <= i < ((2 * 256) + 256)) then aux_2.[(i - + (fun i => (if ((2 * 256) <= i < ((2 * 256) + 256)) then aux_0.[(i - (2 * 256))] else ep.[i])) ); epp <- aux_1; bp <- (Array768.init - (fun i => (if (0 <= i < (0 + 256)) then aux_0.[(i - 0)] else bp.[i]))); + (fun i => (if (0 <= i < (0 + 256)) then aux_2.[(i - 0)] else bp.[i]))); sp_0 <@ __polyvec_ntt (sp_0); w <- 0; while ((w < 3)) { - aux_3 <@ __polyvec_pointwise_acc ((Array256.init - (fun i => bp.[((w * 256) + i)])), + aux <@ __polyvec_pointwise_acc ((Array256.init + (fun i => bp.[((w * 256) + i)])), (Array768.init (fun i => aat.[((w * (3 * 256)) + i)])), sp_0); bp <- (Array768.init - (fun i => (if ((w * 256) <= i < ((w * 256) + 256)) then aux_3.[ - (i - (w * 256))] else + (fun i => (if ((w * 256) <= i < ((w * 256) + 256)) then aux.[(i - + (w * 256))] else bp.[i])) ); w <- (w + 1); @@ -9655,21 +9638,21 @@ module M = { v <@ _poly_add2 (v, k); bp <@ __polyvec_reduce (bp); v <@ __poly_reduce (v); - aux_4 <@ __i_polyvec_compress ((Array960.init (fun i => ct.[(0 + i)])), + aux_3 <@ __i_polyvec_compress ((Array960.init (fun i => ct.[(0 + i)])), bp); ct <- (Array1088.init - (fun i => (if (0 <= i < (0 + 960)) then aux_4.[(i - 0)] else ct.[i]))); - (aux_5, aux_3) <@ _i_poly_compress ((Array128.init - (fun i => ct.[((3 * 320) + i)])), + (fun i => (if (0 <= i < (0 + 960)) then aux_3.[(i - 0)] else ct.[i]))); + (aux_4, aux) <@ _i_poly_compress ((Array128.init + (fun i => ct.[((3 * 320) + i)])), v); ct <- (Array1088.init - (fun i => (if ((3 * 320) <= i < ((3 * 320) + 128)) then aux_5.[(i - + (fun i => (if ((3 * 320) <= i < ((3 * 320) + 128)) then aux_4.[(i - (3 * 320))] else ct.[i])) ); - v <- aux_3; + v <- aux; return ct; } proc __indcpa_dec (msgp:W8.t Array32.t, ct:W8.t Array1088.t, @@ -9697,7 +9680,7 @@ module M = { return msgp; } proc __verify (ct:W8.t Array1088.t, ctpc:W8.t Array1088.t) : W64.t = { - var aux:int; + var inc:int; var cnd:W64.t; var t64:W64.t; var h:W256.t; @@ -9712,9 +9695,9 @@ module M = { cnd <- (W64.of_int 0); t64 <- (W64.of_int 1); h <- (set0_256); - aux <- (((3 * 320) + 128) %/ 32); + inc <- (((3 * 320) + 128) %/ 32); i <- 0; - while ((i < aux)) { + while ((i < inc)) { f <- (get256_direct (WArray1088.init8 (fun i_0 => ctpc.[i_0])) (32 * i)); g <- (get256_direct (WArray1088.init8 (fun i_0 => ct.[i_0])) (32 * i)); @@ -9746,7 +9729,7 @@ module M = { proc __crypto_kem_keypair_jazz (pk:W8.t Array1184.t, sk:W8.t Array2400.t, randomnessp:W8.t Array64.t) : W8.t Array1184.t * W8.t Array2400.t = { - var aux:int; + var inc:int; var s_randomnessp:W8.t Array64.t; var randomnessp1:W8.t Array32.t; var s_pkp:W8.t Array1184.t; @@ -9765,9 +9748,9 @@ module M = { randomnessp1 <- (Array32.init (fun i_0 => randomnessp.[(0 + i_0)])); (pk, sk) <@ __indcpa_keypair (pk, sk, randomnessp1); s_pkp <- pk; - aux <- (((3 * 384) + 32) %/ 8); + inc <- (((3 * 384) + 32) %/ 8); i <- 0; - while ((i < aux)) { + while ((i < inc)) { t64 <- (get64 (WArray1184.init8 (fun i_0 => pk.[i_0])) i); sk <- (Array2400.init @@ -9791,9 +9774,9 @@ module M = { } randomnessp <- s_randomnessp; randomnessp2 <- (Array32.init (fun i_0 => randomnessp.[(32 + i_0)])); - aux <- (32 %/ 8); + inc <- (32 %/ 8); i <- 0; - while ((i < aux)) { + while ((i < inc)) { t64 <- (get64_direct (WArray32.init8 (fun i_0 => randomnessp2.[i_0])) (i * 8)); sk <- @@ -9808,8 +9791,8 @@ module M = { proc __crypto_kem_enc_jazz (ct:W8.t Array1088.t, shk:W8.t Array32.t, pk:W8.t Array1184.t, randomnessp:W8.t Array32.t) : W8.t Array1088.t * W8.t Array32.t = { - var aux:int; - var aux_0:W8.t Array32.t; + var aux:W8.t Array32.t; + var inc:int; var s_pk:W8.t Array1184.t; var s_ct:W8.t Array1088.t; var s_shk:W8.t Array32.t; @@ -9825,9 +9808,9 @@ module M = { s_pk <- pk; s_ct <- ct; s_shk <- shk; - aux <- (32 %/ 8); + inc <- (32 %/ 8); i <- 0; - while ((i < aux)) { + while ((i < inc)) { t64 <- (get64 (WArray32.init8 (fun i_0 => randomnessp.[i_0])) i); buf <- (Array64.init @@ -9835,11 +9818,11 @@ module M = { (WArray64.set64 (WArray64.init8 (fun i_0 => buf.[i_0])) i t64))); i <- (i + 1); } - aux_0 <@ _sha3_256A_A1184 ((Array32.init (fun i_0 => buf.[(32 + i_0)])), + aux <@ _sha3_256A_A1184 ((Array32.init (fun i_0 => buf.[(32 + i_0)])), pk); buf <- (Array64.init - (fun i_0 => (if (32 <= i_0 < (32 + 32)) then aux_0.[(i_0 - 32)] else + (fun i_0 => (if (32 <= i_0 < (32 + 32)) then aux.[(i_0 - 32)] else buf.[i_0])) ); kr <@ _sha3_512A_A64 (kr, buf); @@ -9847,9 +9830,9 @@ module M = { ct <@ __indcpa_enc (ct, (Array32.init (fun i_0 => buf.[(0 + i_0)])), pk, (Array32.init (fun i_0 => kr.[(32 + i_0)]))); shk <- s_shk; - aux <- (32 %/ 8); + inc <- (32 %/ 8); i <- 0; - while ((i < aux)) { + while ((i < inc)) { t64 <- (get64 (WArray64.init8 (fun i_0 => kr.[i_0])) i); shk <- (Array32.init @@ -9861,8 +9844,8 @@ module M = { } proc __crypto_kem_dec_jazz (shk:W8.t Array32.t, ct:W8.t Array1088.t, sk:W8.t Array2400.t) : W8.t Array32.t = { - var aux_0:int; var aux:W8.t Array32.t; + var inc:int; var s_shk:W8.t Array32.t; var s_ct:W8.t Array1088.t; var s_sk:W8.t Array2400.t; @@ -9901,9 +9884,9 @@ module M = { (Array64.init (fun i_0 => (if (0 <= i_0 < (0 + 32)) then aux.[(i_0 - 0)] else buf.[i_0])) ); - aux_0 <- (32 %/ 8); + inc <- (32 %/ 8); i <- 0; - while ((i < aux_0)) { + while ((i < inc)) { t64 <- (get64_direct (WArray2400.init8 (fun i_0 => s_sk.[i_0])) ((i + (((((3 * 384) + ((3 * 384) + 32)) + (2 * 32)) - (2 * 32)) %/ 8)) * @@ -9923,9 +9906,9 @@ module M = { cnd <@ __verify (ct, ctc); s_cnd <- cnd; ct <- s_ct; - aux_0 <- (32 %/ 8); + inc <- (32 %/ 8); i <- 0; - while ((i < aux_0)) { + while ((i < inc)) { t64 <- (get64_direct (WArray2400.init8 (fun i_0 => s_sk.[i_0])) ((i + (((((3 * 384) + ((3 * 384) + 32)) + (2 * 32)) - 32) %/ 8)) * 8)); @@ -9936,9 +9919,9 @@ module M = { (8 * i) t64))); i <- (i + 1); } - aux_0 <- (((3 * 320) + 128) %/ 8); + inc <- (((3 * 320) + 128) %/ 8); i <- 0; - while ((i < aux_0)) { + while ((i < inc)) { t64 <- (get64_direct (WArray1088.init8 (fun i_0 => ct.[i_0])) (i * 8)); zp_ct <- (Array1120.init diff --git a/code/jasmin/mlkem_ref/extraction/Makefile b/code/jasmin/mlkem_ref/extraction/Makefile index 98250d05..718bc591 100644 --- a/code/jasmin/mlkem_ref/extraction/Makefile +++ b/code/jasmin/mlkem_ref/extraction/Makefile @@ -9,11 +9,12 @@ # -------------------------------------------------------------------- all: ec -ec: - $(JASMINC) ../jkem.jazz -oec jkem.ec \ - -ec jade_kem_mlkem_mlkem768_amd64_ref_keypair \ - -ec jade_kem_mlkem_mlkem768_amd64_ref_enc \ - -ec jade_kem_mlkem_mlkem768_amd64_ref_dec + +ec: + $(JASMIN2EC) ../jkem.jazz --array-model=old -o jkem.ec \ + -f jade_kem_mlkem_mlkem768_amd64_ref_keypair \ + -f jade_kem_mlkem_mlkem768_amd64_ref_enc \ + -f jade_kem_mlkem_mlkem768_amd64_ref_dec clean: rm -f *.ec diff --git a/code/jasmin/mlkem_ref/extraction/jkem.ec b/code/jasmin/mlkem_ref/extraction/jkem.ec index 61fd7a2c..e6538af4 100644 --- a/code/jasmin/mlkem_ref/extraction/jkem.ec +++ b/code/jasmin/mlkem_ref/extraction/jkem.ec @@ -11,7 +11,7 @@ WArray33 WArray34 WArray40 WArray64 WArray128 WArray168 WArray192 WArray200 WArray256 WArray512 WArray960 WArray1088 WArray1536 WArray4608. abbrev jzetas_inv = -(Array128.of_list witness +((Array128.of_list witness) [(W16.of_int 1701); (W16.of_int 1807); (W16.of_int 1460); (W16.of_int 2371); (W16.of_int 2338); (W16.of_int 2333); (W16.of_int 308); (W16.of_int 108); (W16.of_int 2851); (W16.of_int 870); (W16.of_int 854); (W16.of_int 1510); @@ -46,7 +46,7 @@ abbrev jzetas_inv = (W16.of_int 1517); (W16.of_int 359); (W16.of_int 758); (W16.of_int 1441)]). abbrev jzetas = -(Array128.of_list witness +((Array128.of_list witness) [(W16.of_int 2285); (W16.of_int 2571); (W16.of_int 2970); (W16.of_int 1812); (W16.of_int 1493); (W16.of_int 1422); (W16.of_int 287); (W16.of_int 202); (W16.of_int 3158); (W16.of_int 622); (W16.of_int 1577); (W16.of_int 182); @@ -81,7 +81,7 @@ abbrev jzetas = (W16.of_int 958); (W16.of_int 1869); (W16.of_int 1522); (W16.of_int 1628)]). abbrev kECCAK1600_RC = -(Array24.of_list witness +((Array24.of_list witness) [(W64.of_int 1); (W64.of_int 32898); (W64.of_int (-9223372036854742902)); (W64.of_int (-9223372034707259392)); (W64.of_int 32907); (W64.of_int 2147483649); (W64.of_int (-9223372034707259263)); @@ -159,7 +159,6 @@ module M(SC:Syscall_t) = { return r; } proc keccakf1600_rho_offsets (i:int) : int = { - var aux:int; var r:int; var x:int; var y:int; @@ -200,7 +199,6 @@ module M(SC:Syscall_t) = { return x; } proc __theta_sum_ref (a:W64.t Array25.t) : W64.t Array5.t = { - var aux:int; var c:W64.t Array5.t; var x:int; var y:int; @@ -222,24 +220,22 @@ module M(SC:Syscall_t) = { return c; } proc __theta_rol_ref (c:W64.t Array5.t) : W64.t Array5.t = { - var aux:int; - var aux_0:W64.t; + var aux:W64.t; var d:W64.t Array5.t; var x:int; d <- witness; x <- 0; while ((x < 5)) { d.[x] <- c.[((x + 1) %% 5)]; - aux_0 <@ __rol_u64_ref (d.[x], 1); - d.[x] <- aux_0; + aux <@ __rol_u64_ref (d.[x], 1); + d.[x] <- aux; d.[x] <- (d.[x] `^` c.[(((x - 1) + 5) %% 5)]); x <- (x + 1); } return d; } proc __rol_sum_ref (a:W64.t Array25.t, d:W64.t Array5.t, y:int) : W64.t Array5.t = { - var aux:int; - var aux_0:W64.t; + var aux:W64.t; var b:W64.t Array5.t; var x:int; var x_:int; @@ -253,15 +249,14 @@ module M(SC:Syscall_t) = { r <@ keccakf1600_rhotates (x_, y_); b.[x] <- a.[(x_ + (y_ * 5))]; b.[x] <- (b.[x] `^` d.[x_]); - aux_0 <@ __rol_u64_ref (b.[x], r); - b.[x] <- aux_0; + aux <@ __rol_u64_ref (b.[x], r); + b.[x] <- aux; x <- (x + 1); } return b; } proc __set_row_ref (e:W64.t Array25.t, b:W64.t Array5.t, y:int, s_rc:W64.t) : W64.t Array25.t = { - var aux:int; var x:int; var x1:int; var x2:int; @@ -284,7 +279,6 @@ module M(SC:Syscall_t) = { } proc __round_ref (e:W64.t Array25.t, a:W64.t Array25.t, s_rc:W64.t) : W64.t Array25.t = { - var aux:int; var c:W64.t Array5.t; var d:W64.t Array5.t; var y:int; @@ -2011,7 +2005,7 @@ module M(SC:Syscall_t) = { return rp; } proc _poly_frombytes (rp:W16.t Array256.t, ap:W64.t) : W16.t Array256.t = { - var aux:int; + var inc:int; var i:int; var c0:W8.t; var c1:W8.t; @@ -2019,9 +2013,9 @@ module M(SC:Syscall_t) = { var d0:W16.t; var t:W16.t; var d1:W16.t; - aux <- (256 %/ 2); + inc <- (256 %/ 2); i <- 0; - while ((i < aux)) { + while ((i < inc)) { c0 <- (loadW8 Glob.mem (W64.to_uint (ap + (W64.of_int (3 * i))))); c1 <- (loadW8 Glob.mem (W64.to_uint (ap + (W64.of_int ((3 * i) + 1))))); @@ -2058,7 +2052,6 @@ module M(SC:Syscall_t) = { return rp; } proc _i_poly_frommsg (rp:W16.t Array256.t, ap:W8.t Array32.t) : W16.t Array256.t = { - var aux:int; var i:int; var c:W8.t; var t:W16.t; @@ -2111,7 +2104,6 @@ module M(SC:Syscall_t) = { } proc _poly_getnoise (rp:W16.t Array256.t, s_seed:W8.t Array32.t, nonce:W8.t) : W16.t Array256.t = { - var aux:int; var seed:W8.t Array32.t; var k:int; var c:W8.t; @@ -2310,7 +2302,6 @@ module M(SC:Syscall_t) = { } proc _i_poly_tomsg (rp:W8.t Array32.t, a:W16.t Array256.t) : W8.t Array32.t * W16.t Array256.t = { - var aux:int; var r:W8.t; var j:int; var i:int; @@ -2380,7 +2371,6 @@ module M(SC:Syscall_t) = { return r; } proc __polyvec_compress (rp:W64.t, a:W16.t Array768.t) : unit = { - var aux:int; var i:W64.t; var j:W64.t; var aa:W16.t Array768.t; @@ -2439,7 +2429,6 @@ module M(SC:Syscall_t) = { } proc __i_polyvec_compress (rp:W8.t Array960.t, a:W16.t Array768.t) : W8.t Array960.t = { - var aux:int; var i:W64.t; var j:W64.t; var aa:W16.t Array768.t; @@ -2496,7 +2485,6 @@ module M(SC:Syscall_t) = { return rp; } proc __polyvec_decompress (ap:W64.t) : W16.t Array768.t = { - var aux:int; var r:W16.t Array768.t; var i:W64.t; var j:W64.t; @@ -2731,7 +2719,6 @@ module M(SC:Syscall_t) = { return (ctr, rp); } proc __gen_matrix (seed:W8.t Array32.t, transposed:W64.t) : W16.t Array2304.t = { - var aux:int; var r:W16.t Array2304.t; var stransposed:W64.t; var j:int; @@ -2805,8 +2792,8 @@ module M(SC:Syscall_t) = { } proc __indcpa_keypair (spkp:W64.t, sskp:W64.t, randomnessp:W8.t Array32.t) : unit = { - var aux:int; - var aux_0:W16.t Array256.t; + var aux:W16.t Array256.t; + var inc:int; var i:int; var t64:W64.t; var inbuf:W8.t Array33.t; @@ -2833,9 +2820,9 @@ module M(SC:Syscall_t) = { r_noiseseed <- witness; s_noiseseed <- witness; skpv <- witness; - aux <- (32 %/ 8); + inc <- (32 %/ 8); i <- 0; - while ((i < aux)) { + while ((i < inc)) { t64 <- (get64 (WArray32.init8 (fun i_0 => randomnessp.[i_0])) i); inbuf <- (Array33.init @@ -2845,9 +2832,9 @@ module M(SC:Syscall_t) = { } inbuf.[32] <- (W8.of_int 3); buf <@ _sha3512_33 (buf, inbuf); - aux <- (32 %/ 8); + inc <- (32 %/ 8); i <- 0; - while ((i < aux)) { + while ((i < inc)) { t64 <- (get64 (WArray64.init8 (fun i_0 => buf.[i_0])) i); publicseed <- (Array32.init @@ -2865,105 +2852,102 @@ module M(SC:Syscall_t) = { zero <- (W64.of_int 0); a <@ __gen_matrix (publicseed, zero); nonce <- (W8.of_int 0); - aux_0 <@ _poly_getnoise ((Array256.init (fun i_0 => skpv.[(0 + i_0)])), + aux <@ _poly_getnoise ((Array256.init (fun i_0 => skpv.[(0 + i_0)])), s_noiseseed, nonce); skpv <- (Array768.init - (fun i_0 => (if (0 <= i_0 < (0 + 256)) then aux_0.[(i_0 - 0)] else + (fun i_0 => (if (0 <= i_0 < (0 + 256)) then aux.[(i_0 - 0)] else skpv.[i_0])) ); nonce <- (W8.of_int 1); - aux_0 <@ _poly_getnoise ((Array256.init (fun i_0 => skpv.[(256 + i_0)])), + aux <@ _poly_getnoise ((Array256.init (fun i_0 => skpv.[(256 + i_0)])), s_noiseseed, nonce); skpv <- (Array768.init - (fun i_0 => (if (256 <= i_0 < (256 + 256)) then aux_0.[(i_0 - 256)] else + (fun i_0 => (if (256 <= i_0 < (256 + 256)) then aux.[(i_0 - 256)] else skpv.[i_0])) ); nonce <- (W8.of_int 2); - aux_0 <@ _poly_getnoise ((Array256.init - (fun i_0 => skpv.[((2 * 256) + i_0)])), + aux <@ _poly_getnoise ((Array256.init + (fun i_0 => skpv.[((2 * 256) + i_0)])), s_noiseseed, nonce); skpv <- (Array768.init - (fun i_0 => (if ((2 * 256) <= i_0 < ((2 * 256) + 256)) then aux_0.[ + (fun i_0 => (if ((2 * 256) <= i_0 < ((2 * 256) + 256)) then aux.[ (i_0 - (2 * 256))] else skpv.[i_0])) ); nonce <- (W8.of_int 3); - aux_0 <@ _poly_getnoise ((Array256.init (fun i_0 => e.[(0 + i_0)])), + aux <@ _poly_getnoise ((Array256.init (fun i_0 => e.[(0 + i_0)])), s_noiseseed, nonce); e <- (Array768.init - (fun i_0 => (if (0 <= i_0 < (0 + 256)) then aux_0.[(i_0 - 0)] else - e.[i_0])) + (fun i_0 => (if (0 <= i_0 < (0 + 256)) then aux.[(i_0 - 0)] else e.[i_0])) ); nonce <- (W8.of_int 4); - aux_0 <@ _poly_getnoise ((Array256.init (fun i_0 => e.[(256 + i_0)])), + aux <@ _poly_getnoise ((Array256.init (fun i_0 => e.[(256 + i_0)])), s_noiseseed, nonce); e <- (Array768.init - (fun i_0 => (if (256 <= i_0 < (256 + 256)) then aux_0.[(i_0 - 256)] else + (fun i_0 => (if (256 <= i_0 < (256 + 256)) then aux.[(i_0 - 256)] else e.[i_0])) ); nonce <- (W8.of_int 5); - aux_0 <@ _poly_getnoise ((Array256.init - (fun i_0 => e.[((2 * 256) + i_0)])), + aux <@ _poly_getnoise ((Array256.init (fun i_0 => e.[((2 * 256) + i_0)])), s_noiseseed, nonce); e <- (Array768.init - (fun i_0 => (if ((2 * 256) <= i_0 < ((2 * 256) + 256)) then aux_0.[ + (fun i_0 => (if ((2 * 256) <= i_0 < ((2 * 256) + 256)) then aux.[ (i_0 - (2 * 256))] else e.[i_0])) ); skpv <@ __polyvec_ntt (skpv); e <@ __polyvec_ntt (e); - aux_0 <@ __polyvec_pointwise_acc ((Array768.init - (fun i_0 => a.[(0 + i_0)])), + aux <@ __polyvec_pointwise_acc ((Array768.init (fun i_0 => a.[(0 + i_0)]) + ), skpv); pkpv <- (Array768.init - (fun i_0 => (if (0 <= i_0 < (0 + 256)) then aux_0.[(i_0 - 0)] else + (fun i_0 => (if (0 <= i_0 < (0 + 256)) then aux.[(i_0 - 0)] else pkpv.[i_0])) ); - aux_0 <@ _poly_frommont ((Array256.init (fun i_0 => pkpv.[(0 + i_0)]))); + aux <@ _poly_frommont ((Array256.init (fun i_0 => pkpv.[(0 + i_0)]))); pkpv <- (Array768.init - (fun i_0 => (if (0 <= i_0 < (0 + 256)) then aux_0.[(i_0 - 0)] else + (fun i_0 => (if (0 <= i_0 < (0 + 256)) then aux.[(i_0 - 0)] else pkpv.[i_0])) ); - aux_0 <@ __polyvec_pointwise_acc ((Array768.init - (fun i_0 => a.[((3 * 256) + i_0)])), + aux <@ __polyvec_pointwise_acc ((Array768.init + (fun i_0 => a.[((3 * 256) + i_0)])), skpv); pkpv <- (Array768.init - (fun i_0 => (if (256 <= i_0 < (256 + 256)) then aux_0.[(i_0 - 256)] else + (fun i_0 => (if (256 <= i_0 < (256 + 256)) then aux.[(i_0 - 256)] else pkpv.[i_0])) ); - aux_0 <@ _poly_frommont ((Array256.init (fun i_0 => pkpv.[(256 + i_0)]))); + aux <@ _poly_frommont ((Array256.init (fun i_0 => pkpv.[(256 + i_0)]))); pkpv <- (Array768.init - (fun i_0 => (if (256 <= i_0 < (256 + 256)) then aux_0.[(i_0 - 256)] else + (fun i_0 => (if (256 <= i_0 < (256 + 256)) then aux.[(i_0 - 256)] else pkpv.[i_0])) ); - aux_0 <@ __polyvec_pointwise_acc ((Array768.init - (fun i_0 => a.[((2 * (3 * 256)) + i_0)]) - ), + aux <@ __polyvec_pointwise_acc ((Array768.init + (fun i_0 => a.[((2 * (3 * 256)) + i_0)])), skpv); pkpv <- (Array768.init - (fun i_0 => (if ((2 * 256) <= i_0 < ((2 * 256) + 256)) then aux_0.[ + (fun i_0 => (if ((2 * 256) <= i_0 < ((2 * 256) + 256)) then aux.[ (i_0 - (2 * 256))] else pkpv.[i_0])) ); - aux_0 <@ _poly_frommont ((Array256.init - (fun i_0 => pkpv.[((2 * 256) + i_0)]))); + aux <@ _poly_frommont ((Array256.init + (fun i_0 => pkpv.[((2 * 256) + i_0)]))); pkpv <- (Array768.init - (fun i_0 => (if ((2 * 256) <= i_0 < ((2 * 256) + 256)) then aux_0.[ + (fun i_0 => (if ((2 * 256) <= i_0 < ((2 * 256) + 256)) then aux.[ (i_0 - (2 * 256))] else pkpv.[i_0])) @@ -2975,9 +2959,9 @@ module M(SC:Syscall_t) = { __polyvec_tobytes (skp, skpv); __polyvec_tobytes (pkp, pkpv); pkp <- (pkp + (W64.of_int (3 * 384))); - aux <- (32 %/ 8); + inc <- (32 %/ 8); i <- 0; - while ((i < aux)) { + while ((i < inc)) { t64 <- (get64 (WArray32.init8 (fun i_0 => publicseed.[i_0])) i); Glob.mem <- (storeW64 Glob.mem (W64.to_uint (pkp + (W64.of_int 0))) t64); @@ -3129,9 +3113,9 @@ module M(SC:Syscall_t) = { } proc __iindcpa_enc (ctp:W8.t Array1088.t, msgp:W8.t Array32.t, pkp:W64.t, noiseseed:W8.t Array32.t) : W8.t Array1088.t = { + var aux:W16.t Array256.t; var aux_1:W8.t Array128.t; var aux_0:W8.t Array960.t; - var aux:W16.t Array256.t; var s_noiseseed:W8.t Array32.t; var sctp:W8.t Array1088.t; var pkpv:W16.t Array768.t; @@ -3312,16 +3296,16 @@ module M(SC:Syscall_t) = { return msgp; } proc __verify (ctp:W64.t, ctpc:W8.t Array1088.t) : W64.t = { - var aux:int; + var inc:int; var cnd:W64.t; var i:int; var t1:W8.t; var t2:W8.t; var t64:W64.t; cnd <- (W64.of_int 0); - aux <- ((3 * 320) + 128); + inc <- ((3 * 320) + 128); i <- 0; - while ((i < aux)) { + while ((i < inc)) { t1 <- (get8_direct (WArray1088.init8 (fun i_0 => ctpc.[i_0])) i); t2 <- (loadW8 Glob.mem (W64.to_uint (ctp + (W64.of_int i)))); t1 <- (t1 `^` t2); @@ -3334,7 +3318,6 @@ module M(SC:Syscall_t) = { return cnd; } proc __cmov (dst:W64.t, src:W8.t Array32.t, cnd:W64.t) : unit = { - var aux:int; var i:int; var t2:W8.t; var t1:W8.t; @@ -3353,7 +3336,7 @@ module M(SC:Syscall_t) = { } proc __crypto_kem_keypair_jazz (pkp:W64.t, skp:W64.t, randomnessp:W8.t Array64.t) : unit = { - var aux:int; + var inc:int; var s_randomnessp:W8.t Array64.t; var s_pkp:W64.t; var s_skp:W64.t; @@ -3374,9 +3357,9 @@ module M(SC:Syscall_t) = { skp <- s_skp; skp <- (skp + (W64.of_int (3 * 384))); pkp <- s_pkp; - aux <- (((3 * 384) + 32) %/ 8); + inc <- (((3 * 384) + 32) %/ 8); i <- 0; - while ((i < aux)) { + while ((i < inc)) { t64 <- (loadW64 Glob.mem (W64.to_uint (pkp + (W64.of_int (8 * i))))); Glob.mem <- (storeW64 Glob.mem (W64.to_uint (skp + (W64.of_int 0))) t64); @@ -3397,9 +3380,9 @@ module M(SC:Syscall_t) = { } randomnessp <- s_randomnessp; randomnessp2 <- (Array32.init (fun i_0 => randomnessp.[(32 + i_0)])); - aux <- (32 %/ 8); + inc <- (32 %/ 8); i <- 0; - while ((i < aux)) { + while ((i < inc)) { t64 <- (get64 (WArray32.init8 (fun i_0 => randomnessp2.[i_0])) i); Glob.mem <- (storeW64 Glob.mem (W64.to_uint (skp + (W64.of_int 0))) t64); @@ -3410,8 +3393,8 @@ module M(SC:Syscall_t) = { } proc __crypto_kem_enc_jazz (ctp:W64.t, shkp:W64.t, pkp:W64.t, randomnessp:W8.t Array32.t) : unit = { - var aux:int; - var aux_0:W8.t Array32.t; + var aux:W8.t Array32.t; + var inc:int; var s_pkp:W64.t; var s_ctp:W64.t; var s_shkp:W64.t; @@ -3424,9 +3407,9 @@ module M(SC:Syscall_t) = { s_pkp <- pkp; s_ctp <- ctp; s_shkp <- shkp; - aux <- (32 %/ 8); + inc <- (32 %/ 8); i <- 0; - while ((i < aux)) { + while ((i < inc)) { t64 <- (get64 (WArray32.init8 (fun i_0 => randomnessp.[i_0])) i); buf <- (Array64.init @@ -3435,11 +3418,11 @@ module M(SC:Syscall_t) = { i <- (i + 1); } pkp <- s_pkp; - aux_0 <@ _isha3_256_M1184 ((Array32.init (fun i_0 => buf.[(32 + i_0)])), + aux <@ _isha3_256_M1184 ((Array32.init (fun i_0 => buf.[(32 + i_0)])), pkp); buf <- (Array64.init - (fun i_0 => (if (32 <= i_0 < (32 + 32)) then aux_0.[(i_0 - 32)] else + (fun i_0 => (if (32 <= i_0 < (32 + 32)) then aux.[(i_0 - 32)] else buf.[i_0])) ); kr <@ _sha3_512_64 (kr, buf); @@ -3447,9 +3430,9 @@ module M(SC:Syscall_t) = { __indcpa_enc (s_ctp, (Array32.init (fun i_0 => buf.[(0 + i_0)])), pkp, (Array32.init (fun i_0 => kr.[(32 + i_0)]))); shkp <- s_shkp; - aux <- (32 %/ 8); + inc <- (32 %/ 8); i <- 0; - while ((i < aux)) { + while ((i < inc)) { t64 <- (get64 (WArray64.init8 (fun i_0 => kr.[i_0])) i); Glob.mem <- (storeW64 Glob.mem (W64.to_uint (shkp + (W64.of_int (8 * i)))) t64); @@ -3458,8 +3441,8 @@ module M(SC:Syscall_t) = { return (); } proc __crypto_kem_dec_jazz (shkp:W64.t, ctp:W64.t, skp:W64.t) : unit = { - var aux_0:int; var aux:W8.t Array32.t; + var inc:int; var s_shkp:W64.t; var s_ctp:W64.t; var buf:W8.t Array64.t; @@ -3486,9 +3469,9 @@ module M(SC:Syscall_t) = { ); hp <- skp; hp <- (hp + (W64.of_int (32 + (((24 * 3) * 256) `|>>` 3)))); - aux_0 <- (32 %/ 8); + inc <- (32 %/ 8); i <- 0; - while ((i < aux_0)) { + while ((i < inc)) { t64 <- (loadW64 Glob.mem (W64.to_uint (hp + (W64.of_int (8 * i))))); buf <- (Array64.init diff --git a/jasmin b/jasmin index fd320a9c..b46561be 160000 --- a/jasmin +++ b/jasmin @@ -1 +1 @@ -Subproject commit fd320a9c63f35a1fd2bb59fd1c39014b4397a851 +Subproject commit b46561bea9ba1ff66cbc78835f6fa2e04622cc56 diff --git a/proof/correctness/MLKEM_InnerPKE.ec b/proof/correctness/MLKEM_InnerPKE.ec index 0b1f4e64..74d4b7c3 100644 --- a/proof/correctness/MLKEM_InnerPKE.ec +++ b/proof/correctness/MLKEM_InnerPKE.ec @@ -941,7 +941,7 @@ seq 12 7 : (#pre /\ ={publicseed, noiseseed}). wp;ecall {1} (sha3_512_33_64 inbuf{1}). conseq />; 1: by move => /> &2 inb H rr Hrr1 Hrr2; rewrite (H rr Hrr1 Hrr2). - wp;while {1} (0<= i{1} <= aux{1} /\ aux{1} = 4 /\ + wp;while {1} (0<= i{1} <= inc{1} /\ inc{1} = 4 /\ seed{2} = randomnessp{1} /\ forall k, 0<= k < i{1} * 8 => inbuf{1}.[k] = seed{2}.[k]) (32- i{1} * 8); diff --git a/proof/correctness/MLKEM_KEM.ec b/proof/correctness/MLKEM_KEM.ec index a759fa09..a25f96ab 100644 --- a/proof/correctness/MLKEM_KEM.ec +++ b/proof/correctness/MLKEM_KEM.ec @@ -52,7 +52,7 @@ seq 18 4 : ( pk{2}.`1 = load_array1152 Glob.mem{1} (_pkp) /\ pk{2}.`2 = load_array32 Glob.mem{1} (_pkp + 1152) ); last first. -+ while {1} (aux{1} = 4 /\ ++ while {1} (inc{1} = 4 /\ z{2} = Array32.init (fun i => randomnessp2{1}.[i]) /\ to_uint skp{1} = _skp + 1152 + 1152 + 32 + 32 + i{1}*8 /\ valid_disj_reg _pkp (384*3+32) _skp (384*3 + 384*3 + 32 + 32 + 32 + 32) /\ @@ -161,7 +161,7 @@ seq 8 0 : (#{/~to_uint skp{1} = _skp}pre /\ ). + wp;while {1} (#{/~to_uint skp{1} = _skp}{~s_skp{1} = skp{1}}pre /\ - aux{1} = (3 * 384 + 32) %/ 8 /\ 0<=i{1} <= aux{1} /\ + inc{1} = (3 * 384 + 32) %/ 8 /\ 0<=i{1} <= inc{1} /\ to_uint skp{1} = _skp + 3*384 + i{1}*8 /\ (forall k, 0<= k < min (8 * i{1}) 1152 => pk{2}.`1.[k] = Glob.mem{1}.[_skp + 3*384 + k]) /\ @@ -310,12 +310,12 @@ seq 14 4 : (#[/1:-2]post /\ to_uint s_shkp{1} = _kp /\ (forall k, 0<=k<32 => kr{1}.[k]=_K{2}.[k])); last first. + while {1} (#[/1:-2]post - /\ aux{1} = 4 + /\ inc{1} = 4 /\ 0<=i{1}<=4 /\ valid_disj_reg _ctp 1088 _kp 32 /\ to_uint shkp{1} = _kp /\ (forall k, 0<=k<8*i{1} => _K{2}.[k] = (load_array32 Glob.mem{1} _kp).[k]) - /\ (forall k, 0<=k<32 => kr{1}.[k]=_K{2}.[k])) (aux{1} - i{1}). + /\ (forall k, 0<=k<32 => kr{1}.[k]=_K{2}.[k])) (inc{1} - i{1}). + auto => /> &hr H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 H10 H11;do split;4:smt(). + move : H;rewrite /touches2 => H a ab1 ab2. rewrite storeW64E get_storesE /=. @@ -350,7 +350,7 @@ wp;ecall {1} (sha_g buf{1}). wp;ecall {1} (pkH_sha mem (_pkp))(* ((Array32.init (fun (i : int) => buf{1}.[32 + i])))).*). seq 8 0 : (#pre /\ s_pkp{1} = pkp{1} /\ s_ctp{1} = ctp{1} /\ s_shkp{1} = shkp{1} /\ randomnessp{1} = Array32.init (fun i => buf{1}.[i])). + sp ; conseq />. - while {1} (0<=i{1}<=aux{1} /\ aux{1} = 4 /\ randomnessp{1} = coins{2} /\ (forall k, 0<=k randomnessp{1}.[k] = buf{1}.[k])) (aux{1} - i{1}); last first. + while {1} (0<=i{1}<=inc{1} /\ inc{1} = 4 /\ randomnessp{1} = coins{2} /\ (forall k, 0<=k randomnessp{1}.[k] = buf{1}.[k])) (inc{1} - i{1}); last first. + auto => /> &1 &2 *; split; 1: by smt(). move => buf i1; split; 1: smt(). by move => *; rewrite tP => k kn; rewrite initiE //= /#. @@ -409,7 +409,7 @@ lemma verify_correct_h mem (_ctp : int) ctp1 : (Array1088.init (fun i => loadW8 mem (_ctp + i)) <> ctp1 => res = W64.of_int 1)]. proc => /=. -wp; while (#pre /\ 0 <= i{hr} <= 1088 /\ aux{hr} = 1088 /\ 0<=to_uint cnd<256 /\ +wp; while (#pre /\ 0 <= i{hr} <= 1088 /\ inc{hr} = 1088 /\ 0<=to_uint cnd<256 /\ (to_uint cnd{hr} = 0 <=> forall k, 0 <= k < i{hr} => loadW8 mem (_ctp + k) = ctp1.[k])); last first. + auto => /> &hr ??; split; 1: by smt(). @@ -478,7 +478,7 @@ qed. lemma verify_ll : islossless Jkem.M(Jkem.Syscall).__verify. proc. -wp; while (0 <= i{hr} <= 1088 /\ aux{hr} = 1088) (1088 - i{hr}); last by auto => /> /#. +wp; while (0 <= i{hr} <= 1088 /\ inc{hr} = 1088) (1088 - i{hr}); last by auto => /> /#. by move => *; auto => /> /#. qed. @@ -603,7 +603,7 @@ wp; conseq (_: _ ==> rewrite tP => i ib; rewrite initiE //= /#. by rewrite tP => i ib; rewrite !initiE /#. -while {1} (0<=i{1}<=4 /\ aux_0{1} = 4 /\ to_uint hp{1} = _skp + 2336 /\ Glob.mem{1} = mem /\ +while {1} (0<=i{1}<=4 /\ inc{1} = 4 /\ to_uint hp{1} = _skp + 2336 /\ Glob.mem{1} = mem /\ valid_ptr _skp (384*3 + 384*3 + 32 + 32 + 32+ 32) /\ (forall (k : int), 32 <= k && k < 32 + 8*i{1} => buf{1}.[k] = mem.[_skp + 2336 + k - 32]) /\ forall (k : int), 0 <= k && k < 32 => buf{1}.[k] = aux{1}.[k]) (4 - i{1}); last first. diff --git a/proof/correctness/MLKEM_Poly.ec b/proof/correctness/MLKEM_Poly.ec index af427399..86749f48 100644 --- a/proof/correctness/MLKEM_Poly.ec +++ b/proof/correctness/MLKEM_Poly.ec @@ -711,7 +711,7 @@ lemma poly_frombytes_corr mem _p (_a : W8.t Array384.t): map W16.to_sint res{1} = res{2} /\ pos_bound256_cxq res{1} 0 256 2 ]. proc. -seq 1 1 : (#pre /\ aux{1} = 128); 1: by auto. +seq 1 1 : (#pre /\ inc{1} = 128); 1: by auto. while(#pre /\ i{1} = i{2} /\ 0 <= i{2} <= 128 /\ forall k, 0<=k to_sint rp{1}.[k] = r{2}.[k] /\ 0 <= to_sint rp{1}.[k] <2*q); last first. diff --git a/proof/correctness/avx2/MLKEM_InnerPKE_avx2.ec b/proof/correctness/avx2/MLKEM_InnerPKE_avx2.ec index 07b116f7..ffc76fa0 100644 --- a/proof/correctness/avx2/MLKEM_InnerPKE_avx2.ec +++ b/proof/correctness/avx2/MLKEM_InnerPKE_avx2.ec @@ -801,7 +801,7 @@ seq 16 18 : (#pre /\ ={publicseed, noiseseed,e,skpv,pkpv} /\ sskp{2} = skp{1} / sim 3 3. ecall{2} (sha3_512_33_64 inbuf{1}). ecall{1} (sha3_512A_A33_ph inbuf{1}) => /=. - wp; while (={i, aux, randomnessp0, inbuf}); first by auto. + wp; while (={i, inc, randomnessp0, inbuf}); first by auto. auto => /> &m ?????? inbuf ?? r. rewrite /SHA3_512_33_64 /= => H1 seed. rewrite !Array32.tP => H2 H3. diff --git a/proof/correctness/avx2/MLKEM_InnerPKE_avx2_stack.ec b/proof/correctness/avx2/MLKEM_InnerPKE_avx2_stack.ec index a061619f..8cdb0b44 100644 --- a/proof/correctness/avx2/MLKEM_InnerPKE_avx2_stack.ec +++ b/proof/correctness/avx2/MLKEM_InnerPKE_avx2_stack.ec @@ -424,7 +424,7 @@ seq 2 1 : move => i; rewrite size_take 1:/# size_to_list /= => ib. by rewrite !nth_take 1..4:/# get_to_list initiE 1:/# /= /#. -while (#{/~Glob.mem{2}}{~pkp{2}}pre /\ ={aux,i} /\ aux{1} = 4 /\ 0 <= i{1} <= 4 /\ +while (#{/~Glob.mem{2}}{~pkp{2}}pre /\ ={i} /\ aux{1} = inc{2} /\ inc{2} = 4 /\ 0 <= i{1} <= 4 /\ to_uint pkp{2} = 1152+8*i{1} /\ Glob.mem{2} = stores (stores witness (384 * 3 +32) (take 1152 (to_list sk0{1}))) 0 (take (1152 + 8*i{1}) (to_list pk0{1}))); last by auto => />;smt(take_size Array1184.size_to_list). diff --git a/proof/correctness/avx2/MLKEM_KEM_avx2.ec b/proof/correctness/avx2/MLKEM_KEM_avx2.ec index 4f0e131c..a114890a 100644 --- a/proof/correctness/avx2/MLKEM_KEM_avx2.ec +++ b/proof/correctness/avx2/MLKEM_KEM_avx2.ec @@ -47,7 +47,7 @@ seq 18 4 : ( pk{2}.`1 = load_array1152 Glob.mem{1} (_pkp) /\ pk{2}.`2 = load_array32 Glob.mem{1} (_pkp + 1152) ); last first. -+ while {1} (aux{1} = 4 /\ ++ while {1} (inc{1} = 4 /\ z{2} = Array32.init(fun i => randomnessp2{1}.[0 + i]) /\ to_uint skp{1} = _skp + 1152 + 1152 + 32 + 32 + i{1}*8 /\ valid_disj_reg _pkp (384*3+32) _skp (384*3 + 384*3 + 32 + 32 + 32 + 32) /\ @@ -156,7 +156,7 @@ seq 8 0 : (#{/~to_uint skp{1} = _skp}pre /\ ). + wp;while {1} (#{/~to_uint skp{1} = _skp}{~s_skp{1} = skp{1}}pre /\ - aux{1} = (3 * 384 + 32) %/ 8 /\ 0<=i{1} <= aux{1} /\ + inc{1} = (3 * 384 + 32) %/ 8 /\ 0<=i{1} <= inc{1} /\ to_uint skp{1} = _skp + 3*384 + i{1}*8 /\ (forall k, 0<= k < min (8 * i{1}) 1152 => pk{2}.`1.[k] = Glob.mem{1}.[_skp + 3*384 + k]) /\ @@ -307,12 +307,12 @@ seq 13 4 : (#[/1:-2]post /\ to_uint s_shkp{1} = _kp /\ (forall k, 0<=k<32 => kr{1}.[k]=_K{2}.[k])); last first. + while {1} (#[/1:-2]post - /\ aux{1} = 4 + /\ inc{1} = 4 /\ 0<=i{1}<=4 /\ valid_disj_reg _ctp 1088 _kp 32 /\ to_uint shkp{1} = _kp /\ (forall k, 0<=k<8*i{1} => _K{2}.[k] = (load_array32 Glob.mem{1} _kp).[k]) - /\ (forall k, 0<=k<32 => kr{1}.[k]=_K{2}.[k])) (aux{1} - i{1}). + /\ (forall k, 0<=k<32 => kr{1}.[k]=_K{2}.[k])) (inc{1} - i{1}). + auto => /> &hr H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 H10 H11;do split;4:smt(). + move : H;rewrite /touches2 => H a ab1 ab2. rewrite storeW64E get_storesE /=. @@ -347,7 +347,7 @@ wp; ecall {1} (sha3_512A_A64_ph buf{1}). wp; ecall {1} (sha3_256A_M1184_ph mem (_pkp)). seq 8 0 : (#pre /\ s_pkp{1} = pkp{1} /\ s_ctp{1} = ctp{1} /\ s_shkp{1} = shkp{1} /\ randomnessp{1} = Array32.init (fun i => buf{1}.[i])). + sp ; conseq />. - while {1} (0<=i{1}<=aux{1} /\ aux{1} = 4 /\ randomnessp{1} = coins{2} /\ (forall k, 0<=k randomnessp{1}.[k] = buf{1}.[k])) (aux{1} - i{1}); last first. + while {1} (0<=i{1}<=inc{1} /\ inc{1} = 4 /\ randomnessp{1} = coins{2} /\ (forall k, 0<=k randomnessp{1}.[k] = buf{1}.[k])) (inc{1} - i{1}); last first. + auto => /> &1 &2 *; split; 1: by smt(). move => buf i1; split; 1: smt(). by move => *; rewrite tP => k kn; rewrite initiE //= /#. @@ -406,7 +406,7 @@ lemma verify_correct_h mem (_ctp : int) ctp1 : res = W64.of_int 1)]. proc => /=. seq 8 : (#post); last first. -wp. conseq />. while(i=1088 /\ aux=1088 /\ #pre); 1: by auto => />. +wp. conseq />. while(i=1088 /\ inc=1088 /\ #pre); 1: by auto => />. + (*conseq />; 1: by smt(). *) conseq />; first by move => /> *; split; smt(). auto => />. @@ -416,7 +416,7 @@ wp. conseq />. while(i=1088 /\ aux=1088 /\ #pre); 1: by auto => />. + move => H5; move : (H3 H5) => -> /=; rewrite W64.minus_one /= wordP => i ib. by rewrite /(`>>`) shrwE ib /= /(W64.one) /= /bits2w /= initiE //= /int2bs /= /mkseq /= -iotaredE /= /#. -wp; while (#pre /\ 0 <= i{hr} <= 34 /\ aux{hr} = 34 /\ 0<=to_uint cnd<256 /\ +wp; while (#pre /\ 0 <= i{hr} <= 34 /\ inc{hr} = 34 /\ 0<=to_uint cnd<256 /\ (to_uint h{hr} = 0 <=> forall k, 0 <= k < i{hr}*32 => loadW8 mem (_ctp + k) = ctp1.[k])); last first. + auto => /> &hr ??; split; 1: by smt(). @@ -484,9 +484,9 @@ qed. lemma verify_ll : islossless Jkem_avx2.M(Jkem_avx2.Syscall).__verify. proc. seq 8 : (#post) => //; last first. -wp. conseq />. while(i=1088 /\ aux=1088 /\ #pre) (1088 - aux); 1,2: by auto => />. +wp. conseq />. while(i=1088 /\ inc=1088 /\ #pre) (1088 - inc); 1,2: by auto => />. wp. -while (0 <= i{hr} <= 34 /\ aux{hr} = 34) (34 - i{hr}). +while (0 <= i{hr} <= 34 /\ inc{hr} = 34) (34 - i{hr}). auto => /> /#. auto => /> /#. qed. @@ -521,8 +521,8 @@ seq 5 : (#post); last first. unroll ^while. -seq 5 : (#post /\ aux{hr}= 1 /\ i{hr}=1); last first. -+ wp; conseq />; while(i=1 /\ aux=1 /\ #pre); auto => /> /#. +seq 5 : (#post /\ inc{hr}= 1 /\ i{hr}=1); last first. ++ wp; conseq />; while(i=1 /\ inc=1 /\ #pre); auto => /> /#. rcondt 5; 1: by move => *; auto => />. @@ -579,7 +579,7 @@ seq 6 : (#post) => //; last first. unroll 6. -+ wp; conseq />; while(i=1 /\ aux=1 /\ #pre) (1-i); auto => /> /#. ++ wp; conseq />; while(i=1 /\ inc=1 /\ #pre) (1-i); auto => /> /#. qed. @@ -639,7 +639,7 @@ wp; conseq (_: _ ==> + move => k kbl kbh; rewrite initiE 1:/# /= ifF 1:/# /= /G_mhpk; congr; congr;congr. rewrite tP => i ib; rewrite initiE //= /#. by rewrite tP => i ib; rewrite !initiE /#. -while {1} (0<=i{1}<=4 /\ aux_0{1} = 4 /\ to_uint hp{1} = _skp + 2336 /\ Glob.mem{1} = mem /\ +while {1} (0<=i{1}<=4 /\ inc{1} = 4 /\ to_uint hp{1} = _skp + 2336 /\ Glob.mem{1} = mem /\ valid_ptr _skp (384*3 + 384*3 + 32 + 32 + 32+ 32) /\ (forall (k : int), 32 <= k && k < 32 + 8*i{1} => buf{1}.[k] = mem.[_skp + 2336 + k - 32]) /\ forall (k : int), 0 <= k && k < 32 => buf{1}.[k] = aux{1}.[k]) (4 - i{1}); last first. diff --git a/proof/correctness/avx2/MLKEM_KEM_avx2_stack.ec b/proof/correctness/avx2/MLKEM_KEM_avx2_stack.ec index 4eac785b..7e058d83 100644 --- a/proof/correctness/avx2/MLKEM_KEM_avx2_stack.ec +++ b/proof/correctness/avx2/MLKEM_KEM_avx2_stack.ec @@ -119,7 +119,7 @@ seq 11 1 : ( pk{2}.`1 = Array1152.init (fun i => pk0{1}.[i]) /\ pk{2}.`2 = Array32.init (fun i => pk0{1}.[i + 1152]) ); last first. -+ while {1} (aux{1} = 4 /\ ++ while {1} (inc{1} = 4 /\ coins{2}.`2 = randomnessp2{1} /\ sk{2} = Array1152.init (fun i => sk0{1}.[i]) /\ pk{2}.`1 = Array1152.init (fun i => sk0{1}.[i+1152]) /\ @@ -209,7 +209,7 @@ seq 3 0 : (#pre /\ ). + wp;while {1} (#pre /\ - aux{1} = (3 * 384 + 32) %/ 8 /\ 0<=i{1} <= aux{1} /\ + inc{1} = (3 * 384 + 32) %/ 8 /\ 0<=i{1} <= inc{1} /\ (forall k, 0<= k < min (8 * i{1}) 1152 => pk{2}.`1.[k] = sk0{1}.[1152+k]) /\ (forall k, 1152 <= k < min (8 * i{1}) (1152 + 32) => @@ -319,10 +319,10 @@ sp 14 0;wp. seq 9 4 : (#[/1:-2]post /\ (forall k, 0<=k<32 => kr{1}.[k]=_K{2}.[k])); last first. + wp;conseq />. while {1} ( - aux{1} = 4 + inc{1} = 4 /\ 0<=i{1}<=4 /\ (forall k, 0<=k<32 => kr{1}.[k]=_K{2}.[k]) - /\ (forall k, 0<=k<8*i{1} => _K{2}.[k] = shk0{1}.[k])) (aux{1} - i{1}). + /\ (forall k, 0<=k<8*i{1} => _K{2}.[k] = shk0{1}.[k])) (inc{1} - i{1}). + auto => /> &hr H H0 H1 H2 H3;do split;1,2,4:smt(). + move => k kb kbh; rewrite initiE 1:/# /=. rewrite get8_set64_directE 1,2:/# /=. @@ -340,7 +340,7 @@ wp; ecall {1} (sha3_512A_512A_A64_stack coins{2} (H_pk pk{2})). wp; ecall {1} (sha3_256A_M1184_ph_stack pk0{1}). seq 3 0 : (#pre /\ randomnessp{1} = Array32.init (fun i => buf{1}.[i])). + sp ; conseq />. - while {1} (0<=i{1}<=aux{1} /\ aux{1} = 4 /\ randomnessp{1} = coins{2} /\ (forall k, 0<=k randomnessp{1}.[k] = buf{1}.[k])) (aux{1} - i{1}); last first. + while {1} (0<=i{1}<=inc{1} /\ inc{1} = 4 /\ randomnessp{1} = coins{2} /\ (forall k, 0<=k randomnessp{1}.[k] = buf{1}.[k])) (inc{1} - i{1}); last first. + auto => /> &1 &2 *; split; 1: by smt(). move => buf i1; split; 1: smt(). by move => *; rewrite tP => k kn; rewrite initiE //= /#. @@ -380,7 +380,7 @@ lemma verify_correct_h_stack _ctp _ctp1 : res = W64.of_int 1)]. proc => /=. -wp; while (#pre /\ 0 <= i{hr} <= 34 /\ aux{hr} = 34 /\ +wp; while (#pre /\ 0 <= i{hr} <= 34 /\ inc{hr} = 34 /\ (to_uint h{hr} = 0 <=> forall k, 0 <= k < i{hr}*32 => _ctp.[k] = _ctp1.[k])); last first. + auto => />; split; 1: by smt(). @@ -445,7 +445,7 @@ qed. lemma verify_ll : islossless Jkem_avx2_stack.M.__verify. proc. wp. -while (0 <= i{hr} <= 34 /\ aux{hr} = 34) (34 - i{hr}). +while (0 <= i{hr} <= 34 /\ inc{hr} = 34) (34 - i{hr}). auto => /> /#. auto => /> /#. qed. @@ -563,7 +563,7 @@ seq 5 1 : (#pre /\ rewrite initiE 1:/# /= initiE 1:/# /= => <-. by rewrite /G_mhpk /SHA3_512_64_64 /= initiE 1:/# /=. - while {1} (0<=i{1}<=4 /\ aux_0{1} = 4 /\ + while {1} (0<=i{1}<=4 /\ inc{1} = 4 /\ (forall (k : int), 32 <= k && k < 32 + 8*i{1} => buf{1}.[k] = s_sk{1}.[2336 + k - 32]) /\ forall (k : int), 0 <= k && k < 32 => buf{1}.[k] = aux{1}.[k]) (4 - i{1}); last first. + auto => /> &1 &2 ??? /=;do split. @@ -650,7 +650,7 @@ seq 3 0 : (#pre /\ ). + wp;while {1} (#pre /\ - aux_0{1} = 4 /\ 0<=i{1} <= aux_0{1} /\ + inc{1} = 4 /\ 0<=i{1} <= inc{1} /\ (forall k, 0<= k < 8 * i{1} => z{2}.[k] = zp_ct{1}.[k])) (4 - i{1}). @@ -672,7 +672,7 @@ seq 3 0 : (#pre /\ by move => *; rewrite initiE 1:/# /= initiE 1:/# /=;smt(Array32.initiE). + wp;while {1} (#pre /\ - aux_0{1} = (3 * 320 + 128) %/ 8 /\ 0<=i{1} <= aux_0{1} /\ + inc{1} = (3 * 320 + 128) %/ 8 /\ 0<=i{1} <= inc{1} /\ (forall k, 0<= k < min (8 * i{1}) 960 => cph{2}.`1.[k] = zp_ct{1}.[32+k]) /\ (forall k, 960 <= k < min (8 * i{1}) (960 + 128) => @@ -680,8 +680,8 @@ seq 3 0 : (#pre /\ ((3 * 384 + 32) %/ 8 - i{1}). move => &m z;auto => /> &hr. - move => &1 zz;auto => /> &2; rewrite !tP. - move => pkv1 pkv2???prev0?? prev1 prev2?. + auto => />; rewrite !tP. + move => pkv1 pkv2 c?????prev0?? prev1 prev2?. do split. + move => k kb; rewrite initiE 1:/# /= initiE 1:/# /= initiE 1:/# /=. rewrite get8_set64_directE 1,2:/# /=. @@ -694,8 +694,8 @@ seq 3 0 : (#pre /\ rewrite get8_set64_directE 1,2:/# /=. case ((i{hr} + 4) * 8 <= 32 + k && 32 + k < (i{hr} + 4) * 8 + 8) => *. + rewrite WArray1088.get64E pack8bE 1:/# initiE 1:/# /=. - by rewrite /get8 initiE; smt(Array960.initiE). - + by rewrite /get8 initiE; smt(Array1120.initiE). + rewrite /get8 initiE /= 1:/#; move : c; smt(Array960.initiE). + + by rewrite /get8 initiE /= 1:/#; move : c; smt(Array1120.initiE). + move => k kb kbb; rewrite initiE 1:/# /=. rewrite get8_set64_directE 1,2:/# /=. case ((i{hr} + 4) * 8 <= 32 + k && 32 + k < (i{hr} + 4) * 8 + 8) => *. diff --git a/proof/correctness/avx2/MLKEM_PolyPolyVec_stack_bridges.ec b/proof/correctness/avx2/MLKEM_PolyPolyVec_stack_bridges.ec index 70eef8ae..c92ac2de 100644 --- a/proof/correctness/avx2/MLKEM_PolyPolyVec_stack_bridges.ec +++ b/proof/correctness/avx2/MLKEM_PolyPolyVec_stack_bridges.ec @@ -281,7 +281,7 @@ lemma polyvec_decompress_stack_equiv: load_array1088 Glob.mem{2} 1152 = arg{1} ==> ={res}]. proc. while (#pre /\ 0 <= k{1} <= 3 /\ ={k} /\ ={r,q,shufbidx,sllvdidx,mask});last by auto. -wp;while (#pre /\ aux{1} = 16 /\ 0 <= i{1} <= 16 /\ ={aux,i}); last by auto => /> /#. +wp;while (#pre /\ inc{1} = 16 /\ 0 <= i{1} <= 16 /\ ={inc,i}); last by auto => /> /#. auto => /> &2 ???????;split;last by smt(). rewrite tP => j jb; rewrite initiE 1:/# /= initiE 1:/# /=. do 8!(congr). @@ -297,7 +297,7 @@ lemma poly_decompress_stack_equiv: to_uint arg{2}.`2 = 1152+960 /\ load_array128 Glob.mem{2} (1152+960) = arg{1}.`2 ==> ={res}]. proc => /=. -while (#pre /\ aux{1} = 16 /\ 0 <= i{1} <= 16 /\ ={aux,i,x16p,x32p,q,shufbidx,mask,shift,f} /\ +while (#pre /\ inc{1} = 16 /\ 0 <= i{1} <= 16 /\ ={inc,i,x16p,x32p,q,shufbidx,mask,shift,f} /\ (forall k, 0<=k<16*i{1} => rp{1}.[k] = rp{2}.[k]));last by auto => />;smt(Array256.tP). auto => /> &1 &2 ?????;do split;1,2: smt(). + do 6!(congr). diff --git a/proof/correctness/avx2/MLKEM_PolyVec_avx2_vec.ec b/proof/correctness/avx2/MLKEM_PolyVec_avx2_vec.ec index e7bc2963..6370225e 100644 --- a/proof/correctness/avx2/MLKEM_PolyVec_avx2_vec.ec +++ b/proof/correctness/avx2/MLKEM_PolyVec_avx2_vec.ec @@ -449,8 +449,9 @@ proof. split. + rewrite /get256_direct /= => />. apply W32u8.allP => />. - do (rewrite initiE 1:/# /=). - smt(@Int @IntDiv @Array256 @W8). + do (rewrite initiE 1:/# /=). + do (split;[congr;[congr; smt() | smt()] | ]). + by smt(). move => a_eq resL10 />. split. + rewrite /f8u32_t4u64 /= => />. @@ -582,7 +583,7 @@ equiv veceq_polyvec_compress_1 : Mvec.polyvec_compress_1 ~Jkem_avx2.M(Jkem_avx2.Syscall).__polyvec_compress_1: ={Glob.mem, rp, a} ==> ={Glob.mem, res}. proof. proc. - while(={i, a, rp, Glob.mem, aux, v, v8, off, shift1, mask, shift2, sllvdidx, shufbidx} /\ 0 <= i{1} /\ aux{1} = 48). + while(={i, a, rp, Glob.mem, v, v8, off, shift1, mask, shift2, sllvdidx, shufbidx} /\ 0 <= i{1} /\ aux{1} = 48 /\ aux{1} = inc{2}). inline *. wp. skip. auto => /> /#. inline OpsV.iVPBROADCAST_16u16 OpsV.iVPBROADCAST_4u64 OpsV.iVPSLL_16u16. @@ -595,7 +596,7 @@ equiv veceq_polyvec_compress : Mvec.polyvec_compress ~Jkem_avx2.M(Jkem_avx2.Syscall).__polyvec_compress: ={Glob.mem, rp, a} ==> ={Glob.mem, res}. proof. proc. - while(={i, a, rp, Glob.mem, aux, v, v8, off, shift1, mask, shift2, sllvdidx, shufbidx} /\ 0 <= i{1} /\ aux{1} = 48). + while(={i, a, rp, Glob.mem, v, v8, off, shift1, mask, shift2, sllvdidx, shufbidx} /\ 0 <= i{1} /\ aux{1} = 48 /\ aux{1} = inc{2}). inline *. wp. skip. auto => /> /#. inline OpsV.iVPBROADCAST_16u16 OpsV.iVPBROADCAST_4u64 OpsV.iVPSLL_16u16. @@ -610,7 +611,7 @@ proof. proc. while(={Glob.mem, rp, q, shufbidx, sllvdidx, mask, k, r} /\ 0 <= k{1}). wp. - while(#pre /\ ={i, aux} /\ 0 <= i{1} /\ aux{1} = 16). + while(#pre /\ ={i} /\ 0 <= i{1} /\ aux{1} = 16 /\ aux{1} = inc{2}). inline OpsV.iVPMULHRS_256 OpsV.iVPAND_16u16 OpsV.iVPSRL_16u16 OpsV.iVPSLLV_8u32 OpsV.iVPSHUFB_256 OpsV.iVPERMQ_32u8 OpsV.iload32u8. wp; skip; auto => /> /#. wp; skip; auto => /> /#. diff --git a/proof/correctness/avx2/MLKEM_Poly_avx2_vec.ec b/proof/correctness/avx2/MLKEM_Poly_avx2_vec.ec index 34bfee8f..790a6f25 100644 --- a/proof/correctness/avx2/MLKEM_Poly_avx2_vec.ec +++ b/proof/correctness/avx2/MLKEM_Poly_avx2_vec.ec @@ -1624,7 +1624,7 @@ equiv veceq_poly_tomsg : Mvec.poly_tomsg_1 ~Jkem_avx2.M(Jkem_avx2.Syscall)._poly_tomsg_1: ={rp, a, Glob.mem} ==> ={res}. proof. proc. - while(={i, rp, a, aux, hq, hhq} /\ 0 <= i{1}). + while(={i, rp, a, hq, hhq} /\ 0 <= i{1} /\ aux{1} = inc{2}). inline *. wp. skip. auto => />. smt(). @@ -1674,7 +1674,7 @@ equiv veceq_poly_frommont: Mvec.poly_frommont ~Jkem_avx2.M(Jkem_avx2.Syscall)._poly_frommont: ={rp} ==> ={res}. proof. proc. - while(={rp, i, qx16, qinvx16, dmontx16, aux}). + while(={rp, i, qx16, qinvx16, dmontx16} /\ aux{1} = inc{2}). inline *. wp. skip. auto => />. wp. skip. auto => />. @@ -1684,7 +1684,7 @@ equiv veceq_poly_decompress: Mvec.poly_decompress ~Jkem_avx2.M(Jkem_avx2.Syscall)._poly_decompress: ={ap, Glob.mem} ==> ={res, Glob.mem}. proof. proc. - while(={ap, i, aux, q, mask, shift, shufbidx, Glob.mem} /\ + while(={ap, i, q, mask, shift, shufbidx, Glob.mem} /\ aux{1} = inc{2} /\ aux{1} = 16 /\ 0 <= i{1} /\ i{1} <= 16 /\ (forall k, 0 <= k < 16 * i{1} => rp{1}.[k] = rp{2}.[k])). inline *. @@ -1713,7 +1713,7 @@ equiv veceq_poly_compress_1: Mvec.poly_compress_1 ~Jkem_avx2.M(Jkem_avx2.Syscall)._poly_compress_1: ={rp, a, Glob.mem} ==> ={res, Glob.mem}. proof. proc. - while(={rp, a, i, aux, v, shift1, mask, shift2, permidx, Glob.mem}). + while(={rp, a, i, v, shift1, mask, shift2, permidx, Glob.mem} /\ aux{1} = inc{2}). inline *. wp. skip. auto => />. inline OpsV.iVPBROADCAST_16u16. @@ -1727,7 +1727,7 @@ equiv veceq_poly_compress: Mvec.poly_compress ~Jkem_avx2.M(Jkem_avx2.Syscall)._poly_compress: ={rp, a, Glob.mem} ==> ={res, Glob.mem}. proof. proc. - while(={rp, a, i, aux, v, shift1, mask, shift2, permidx, Glob.mem}). + while(={rp, a, i, v, shift1, mask, shift2, permidx, Glob.mem} /\ aux{1} = inc{2}). inline *. wp. skip. auto => />. inline OpsV.iVPBROADCAST_16u16. diff --git a/proof/correctness/avx2/MLKEM_keccak_avx2.ec b/proof/correctness/avx2/MLKEM_keccak_avx2.ec index 8e2005b5..9be02798 100644 --- a/proof/correctness/avx2/MLKEM_keccak_avx2.ec +++ b/proof/correctness/avx2/MLKEM_keccak_avx2.ec @@ -1410,7 +1410,8 @@ move=> []s3 ?? /= />. rewrite /absorb_spec_avx2x4 /match_state4x => ->. have L: forall x, x\in[0;2;4;6] => sub ((init (fun i=> _rc.[x+i])))%Array2 0 2 = sub _rc x 2. by move=> i /= []Hi; apply eq_in_mkseq => j Hj /=; rewrite initiE //=. -by rewrite !L //=; congr; congr; congr; smt(). +rewrite !L //=; congr; congr; congr;1..2,4..: smt(). +by smt(Array2.tP Array2.initiE). qed. lemma shake128x4_absorb_A32_A2_ll: islossless K._shake128x4_absorb_A32_A2.