diff --git a/proofs/hol_light/aarch64/proofs/keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm.ml b/proofs/hol_light/aarch64/proofs/keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm.ml
index e24b914cf..7686f7ac3 100644
--- a/proofs/hol_light/aarch64/proofs/keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm.ml
+++ b/proofs/hol_light/aarch64/proofs/keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm.ml
@@ -992,7 +992,7 @@ let keccak_f1600_x4_v8a_scalar_mc = define_assert_from_elf
 ];;
 (*** BYTECODE END ***)
 
-let KECCAK_F1600_X4_V8A_SCALAR_EXEC = ARM_MK_EXEC_RULE keccak_f1600_x4_v8a_scalar_mc;;
+let KECCAK_F1600_X4_V8A_SCALAR_HYBRID_EXEC = ARM_MK_EXEC_RULE keccak_f1600_x4_v8a_scalar_mc;;
 
 (*** Additional lazy/deferred rotations in the implementation, row-major ***)
 
@@ -1003,7 +1003,7 @@ let deferred_rotates = define
     25;  8; 18;  1;  6;
     10; 15; 56; 27; 36;
     39; 41; 2; 62; 55]`;;
-let KECCAK_F1600_X4_V8A_SCALAR_EXEC = ARM_MK_EXEC_RULE keccak_f1600_x4_v8a_scalar_mc;;
+let KECCAK_F1600_X4_V8A_SCALAR_HYBRID_EXEC = ARM_MK_EXEC_RULE keccak_f1600_x4_v8a_scalar_mc;;
 
 (* ------------------------------------------------------------------------- *)
 (* Code length constants                                                     *)
@@ -1013,29 +1013,29 @@ let LENGTH_KECCAK_F1600_X4_V8A_SCALAR_MC =
   REWRITE_CONV[keccak_f1600_x4_v8a_scalar_mc] `LENGTH keccak_f1600_x4_v8a_scalar_mc`
   |> CONV_RULE (RAND_CONV LENGTH_CONV);;
 
-let KECCAK_F1600_X4_V8A_SCALAR_PREAMBLE_LENGTH = new_definition
-  `KECCAK_F1600_X4_V8A_SCALAR_PREAMBLE_LENGTH = 44`;;
+let KECCAK_F1600_X4_V8A_SCALAR_HYBRID_PREAMBLE_LENGTH = new_definition
+  `KECCAK_F1600_X4_V8A_SCALAR_HYBRID_PREAMBLE_LENGTH = 44`;;
 
-let KECCAK_F1600_X4_V8A_SCALAR_POSTAMBLE_LENGTH = new_definition
-  `KECCAK_F1600_X4_V8A_SCALAR_POSTAMBLE_LENGTH = 48`;;
+let KECCAK_F1600_X4_V8A_SCALAR_HYBRID_POSTAMBLE_LENGTH = new_definition
+  `KECCAK_F1600_X4_V8A_SCALAR_HYBRID_POSTAMBLE_LENGTH = 48`;;
 
-let KECCAK_F1600_X4_V8A_SCALAR_CORE_START = new_definition
-  `KECCAK_F1600_X4_V8A_SCALAR_CORE_START = KECCAK_F1600_X4_V8A_SCALAR_PREAMBLE_LENGTH`;;
+let KECCAK_F1600_X4_V8A_SCALAR_HYBRID_CORE_START = new_definition
+  `KECCAK_F1600_X4_V8A_SCALAR_HYBRID_CORE_START = KECCAK_F1600_X4_V8A_SCALAR_HYBRID_PREAMBLE_LENGTH`;;
 
-let KECCAK_F1600_X4_V8A_SCALAR_CORE_END = new_definition
-  `KECCAK_F1600_X4_V8A_SCALAR_CORE_END = LENGTH keccak_f1600_x4_v8a_scalar_mc - KECCAK_F1600_X4_V8A_SCALAR_POSTAMBLE_LENGTH`;;
+let KECCAK_F1600_X4_V8A_SCALAR_HYBRID_CORE_END = new_definition
+  `KECCAK_F1600_X4_V8A_SCALAR_HYBRID_CORE_END = LENGTH keccak_f1600_x4_v8a_scalar_mc - KECCAK_F1600_X4_V8A_SCALAR_HYBRID_POSTAMBLE_LENGTH`;;
 
 let LENGTH_SIMPLIFY_CONV =
   REWRITE_CONV[LENGTH_KECCAK_F1600_X4_V8A_SCALAR_MC;
-              KECCAK_F1600_X4_V8A_SCALAR_CORE_START; KECCAK_F1600_X4_V8A_SCALAR_CORE_END;
-              KECCAK_F1600_X4_V8A_SCALAR_PREAMBLE_LENGTH; KECCAK_F1600_X4_V8A_SCALAR_POSTAMBLE_LENGTH] THENC
+              KECCAK_F1600_X4_V8A_SCALAR_HYBRID_CORE_START; KECCAK_F1600_X4_V8A_SCALAR_HYBRID_CORE_END;
+              KECCAK_F1600_X4_V8A_SCALAR_HYBRID_PREAMBLE_LENGTH; KECCAK_F1600_X4_V8A_SCALAR_HYBRID_POSTAMBLE_LENGTH] THENC
   NUM_REDUCE_CONV THENC REWRITE_CONV [ADD_0];;
 
 (* ------------------------------------------------------------------------- *)
 (* Correctness proof                                                         *)
 (* ------------------------------------------------------------------------- *)
 
-let KECCAK_F1600_X4_V8A_SCALAR_CORRECT = prove
+let KECCAK_F1600_X4_V8A_SCALAR_HYBRID_CORRECT = prove
  (`!a rc A1 A2 A3 A4 pc stackpointer.
       aligned 16 stackpointer /\
       nonoverlapping (a,800) (stackpointer,216) /\
@@ -1044,7 +1044,7 @@ let KECCAK_F1600_X4_V8A_SCALAR_CORRECT = prove
                [(word pc,LENGTH keccak_f1600_x4_v8a_scalar_mc); (rc,192)]
       ==> ensures arm
            (\s. aligned_bytes_loaded s (word pc) keccak_f1600_x4_v8a_scalar_mc /\
-                read PC s = word (pc + KECCAK_F1600_X4_V8A_SCALAR_CORE_START) /\
+                read PC s = word (pc + KECCAK_F1600_X4_V8A_SCALAR_HYBRID_CORE_START) /\
                 read SP s = stackpointer /\
                 C_ARGUMENTS [a; rc] s /\
                 wordlist_from_memory(a,25) s = A1 /\
@@ -1052,7 +1052,7 @@ let KECCAK_F1600_X4_V8A_SCALAR_CORRECT = prove
                 wordlist_from_memory(word_add a (word 400),25) s = A3 /\
                 wordlist_from_memory(word_add a (word 600),25) s = A4 /\
                 wordlist_from_memory(rc,24) s = round_constants)
-           (\s. read PC s = word(pc + KECCAK_F1600_X4_V8A_SCALAR_CORE_END) /\
+           (\s. read PC s = word(pc + KECCAK_F1600_X4_V8A_SCALAR_HYBRID_CORE_END) /\
                 wordlist_from_memory(a,25) s = keccak 24 A1 /\
                 wordlist_from_memory(word_add a (word 200),25) s =
                 keccak 24 A2 /\
@@ -1071,7 +1071,7 @@ let KECCAK_F1600_X4_V8A_SCALAR_CORRECT = prove
   MAP_EVERY X_GEN_TAC
    [`a:int64`; `rc:int64`; `A1:int64 list`; `A2:int64 list`;
     `A3:int64 list`; `A4:int64 list`; `pc:num`; `stackpointer:int64`] THEN
-  REWRITE_TAC[fst KECCAK_F1600_X4_V8A_SCALAR_EXEC] THEN
+  REWRITE_TAC[fst KECCAK_F1600_X4_V8A_SCALAR_HYBRID_EXEC] THEN
   REWRITE_TAC[MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI; C_ARGUMENTS;
               ALL; ALLPAIRS; NONOVERLAPPING_CLAUSES] THEN
   DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN
@@ -1131,7 +1131,7 @@ let KECCAK_F1600_X4_V8A_SCALAR_CORRECT = prove
     MEMORY_128_FROM_64_TAC "a" 0 12 THEN
     MEMORY_128_FROM_64_TAC "a" 200 12 THEN
     ASM_REWRITE_TAC[WORD_ADD_0] THEN REPEAT STRIP_TAC THEN
-    ARM_STEPS_TAC KECCAK_F1600_X4_V8A_SCALAR_EXEC (1--443) THEN
+    ARM_STEPS_TAC KECCAK_F1600_X4_V8A_SCALAR_HYBRID_EXEC (1--443) THEN
     ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
      [CONV_TAC(LAND_CONV WORDLIST_FROM_MEMORY_CONV) THEN
       CONV_TAC(ONCE_DEPTH_CONV NORMALIZE_RELATIVE_ADDRESS_CONV) THEN
@@ -1202,7 +1202,7 @@ let KECCAK_F1600_X4_V8A_SCALAR_CORRECT = prove
       CONV_TAC(ONCE_DEPTH_CONV EL_CONV) THEN REWRITE_TAC[];
       ALL_TAC] THEN
 
-    ARM_STEPS_TAC KECCAK_F1600_X4_V8A_SCALAR_EXEC (1--386) THEN
+    ARM_STEPS_TAC KECCAK_F1600_X4_V8A_SCALAR_HYBRID_EXEC (1--386) THEN
     ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN
     REWRITE_TAC[CONJ_ASSOC] THEN CONJ_TAC THENL
      [REWRITE_TAC[GSYM CONJ_ASSOC];
@@ -1240,7 +1240,7 @@ let KECCAK_F1600_X4_V8A_SCALAR_CORRECT = prove
     X_GEN_TAC `i:num` THEN STRIP_TAC THEN
     CONV_TAC(ONCE_DEPTH_CONV WORDLIST_FROM_MEMORY_CONV) THEN
     CONV_TAC(ONCE_DEPTH_CONV NORMALIZE_RELATIVE_ADDRESS_CONV) THEN
-    ARM_SIM_TAC KECCAK_F1600_X4_V8A_SCALAR_EXEC [1] THEN
+    ARM_SIM_TAC KECCAK_F1600_X4_V8A_SCALAR_HYBRID_EXEC [1] THEN
     VAL_INT64_TAC `i:num` THEN
     ASM_REWRITE_TAC[] THEN CONV_TAC(DEPTH_CONV WORD_NUM_RED_CONV);
 
@@ -1294,7 +1294,7 @@ let KECCAK_F1600_X4_V8A_SCALAR_CORRECT = prove
     ASM_REWRITE_TAC[round_constants; CONS_11; GSYM CONJ_ASSOC] THEN
     REWRITE_TAC[GSYM round_constants] THEN
     ENSURES_INIT_TAC "s0" THEN
-    ARM_STEPS_TAC KECCAK_F1600_X4_V8A_SCALAR_EXEC (1--442) THEN
+    ARM_STEPS_TAC KECCAK_F1600_X4_V8A_SCALAR_HYBRID_EXEC (1--442) THEN
 
     ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
      [CONV_TAC(LAND_CONV WORDLIST_FROM_MEMORY_CONV) THEN
@@ -1369,7 +1369,7 @@ let KECCAK_F1600_X4_V8A_SCALAR_CORRECT = prove
       CONV_TAC(ONCE_DEPTH_CONV EL_CONV) THEN REWRITE_TAC[];
       ALL_TAC] THEN
 
-    ARM_STEPS_TAC KECCAK_F1600_X4_V8A_SCALAR_EXEC (1--386) THEN
+    ARM_STEPS_TAC KECCAK_F1600_X4_V8A_SCALAR_HYBRID_EXEC (1--386) THEN
     ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN
     REWRITE_TAC[CONJ_ASSOC] THEN CONJ_TAC THENL
      [REWRITE_TAC[GSYM CONJ_ASSOC];
@@ -1409,7 +1409,7 @@ let KECCAK_F1600_X4_V8A_SCALAR_CORRECT = prove
     X_GEN_TAC `i:num` THEN STRIP_TAC THEN
     CONV_TAC(ONCE_DEPTH_CONV WORDLIST_FROM_MEMORY_CONV) THEN
     CONV_TAC(ONCE_DEPTH_CONV NORMALIZE_RELATIVE_ADDRESS_CONV) THEN
-    ARM_SIM_TAC KECCAK_F1600_X4_V8A_SCALAR_EXEC [1] THEN
+    ARM_SIM_TAC KECCAK_F1600_X4_V8A_SCALAR_HYBRID_EXEC [1] THEN
     VAL_INT64_TAC `i:num` THEN
     ASM_REWRITE_TAC[] THEN CONV_TAC(DEPTH_CONV WORD_NUM_RED_CONV);
 
@@ -1433,7 +1433,7 @@ let KECCAK_F1600_X4_V8A_SCALAR_CORRECT = prove
   ASM_REWRITE_TAC[round_constants; CONS_11; GSYM CONJ_ASSOC] THEN
   REWRITE_TAC[GSYM round_constants] THEN
   ENSURES_INIT_TAC "s0" THEN
-  ARM_STEPS_TAC KECCAK_F1600_X4_V8A_SCALAR_EXEC (1--83) THEN
+  ARM_STEPS_TAC KECCAK_F1600_X4_V8A_SCALAR_HYBRID_EXEC (1--83) THEN
   ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN
   CONV_TAC(ONCE_DEPTH_CONV WORDLIST_FROM_MEMORY_CONV) THEN
   CONV_TAC(ONCE_DEPTH_CONV NORMALIZE_RELATIVE_ADDRESS_CONV) THEN
@@ -1448,7 +1448,7 @@ let KECCAK_F1600_X4_V8A_SCALAR_CORRECT = prove
 (* NOTE: This must be kept in sync with the CBMC specification
  * in mlkem/src/fips202/native/aarch64/src/fips202_native_aarch64.h *)
 
-let KECCAK_F1600_X4_V8A_SCALAR_SUBROUTINE_CORRECT = prove
+let KECCAK_F1600_X4_V8A_SCALAR_HYBRID_SUBROUTINE_CORRECT = prove
  (`!a rc A1 A2 A3 A4 pc stackpointer returnaddress.
       aligned 16 stackpointer /\
       nonoverlapping (a,800) (word_sub stackpointer (word 224),224) /\
@@ -1483,8 +1483,8 @@ let KECCAK_F1600_X4_V8A_SCALAR_SUBROUTINE_CORRECT = prove
     (WORDLIST_FROM_MEMORY_CONV THENC
      ONCE_DEPTH_CONV NORMALIZE_RELATIVE_ADDRESS_CONV) in
   CONV_TAC TWEAK_CONV THEN
-  ARM_ADD_RETURN_STACK_TAC ~pre_post_nsteps:(11,11) KECCAK_F1600_X4_V8A_SCALAR_EXEC
-   (CONV_RULE TWEAK_CONV (CONV_RULE LENGTH_SIMPLIFY_CONV KECCAK_F1600_X4_V8A_SCALAR_CORRECT))
+  ARM_ADD_RETURN_STACK_TAC ~pre_post_nsteps:(11,11) KECCAK_F1600_X4_V8A_SCALAR_HYBRID_EXEC
+   (CONV_RULE TWEAK_CONV (CONV_RULE LENGTH_SIMPLIFY_CONV KECCAK_F1600_X4_V8A_SCALAR_HYBRID_CORRECT))
   `[D8; D9; D10; D11; D12; D13; D14; D15;
     X19; X20; X21; X22; X23; X24; X25; X26; X27; X28; X29; X30]` 224);;
 
@@ -1498,10 +1498,10 @@ needs "mlkem_native/aarch64/proofs/subroutine_signatures.ml";;
 let full_spec,public_vars = mk_safety_spec
     ~keep_maychanges:false
     (assoc "sha3_keccak4_f1600" subroutine_signatures)
-    KECCAK_F1600_X4_V8A_SCALAR_SUBROUTINE_CORRECT
-    KECCAK_F1600_X4_V8A_SCALAR_EXEC;;
+    KECCAK_F1600_X4_V8A_SCALAR_HYBRID_SUBROUTINE_CORRECT
+    KECCAK_F1600_X4_V8A_SCALAR_HYBRID_EXEC;;
 
-let KECCAK_F1600_X4_V8A_SCALAR_SUBROUTINE_SAFE = time prove
+let KECCAK_F1600_X4_V8A_SCALAR_HYBRID_SUBROUTINE_SAFE = time prove
  (`exists f_events.
        forall e a rc pc stackpointer returnaddress.
            aligned 16 stackpointer /\
@@ -1530,4 +1530,4 @@ let KECCAK_F1600_X4_V8A_SCALAR_SUBROUTINE_SAFE = time prove
                         [a,800; word_sub stackpointer (word 224),224])
                (\s s'. true)`,
   ASSERT_CONCL_TAC full_spec THEN
-  PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars KECCAK_F1600_X4_V8A_SCALAR_EXEC);;
+  PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars KECCAK_F1600_X4_V8A_SCALAR_HYBRID_EXEC);;
diff --git a/proofs/hol_light/aarch64/proofs/keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm.ml b/proofs/hol_light/aarch64/proofs/keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm.ml
index fcbe468e0..d0ca13b3e 100644
--- a/proofs/hol_light/aarch64/proofs/keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm.ml
+++ b/proofs/hol_light/aarch64/proofs/keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm.ml
@@ -898,7 +898,7 @@ let keccak_f1600_x4_v8a_v84a_scalar_mc = define_assert_from_elf
 ];;
 (*** BYTECODE END ***)
 
-let KECCAK_F1600_X4_V8A_V84A_SCALAR_EXEC = ARM_MK_EXEC_RULE keccak_f1600_x4_v8a_v84a_scalar_mc;;
+let KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_EXEC = ARM_MK_EXEC_RULE keccak_f1600_x4_v8a_v84a_scalar_mc;;
 
 (*** Additional lazy/deferred rotations in the implementation, row-major ***)
 
@@ -918,29 +918,29 @@ let LENGTH_KECCAK_F1600_X4_V8A_V84A_SCALAR_MC =
   REWRITE_CONV[keccak_f1600_x4_v8a_v84a_scalar_mc] `LENGTH keccak_f1600_x4_v8a_v84a_scalar_mc`
   |> CONV_RULE (RAND_CONV LENGTH_CONV);;
 
-let KECCAK_F1600_X4_V8A_V84A_SCALAR_PREAMBLE_LENGTH = new_definition
-  `KECCAK_F1600_X4_V8A_V84A_SCALAR_PREAMBLE_LENGTH = 44`;;
+let KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_PREAMBLE_LENGTH = new_definition
+  `KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_PREAMBLE_LENGTH = 44`;;
 
-let KECCAK_F1600_X4_V8A_V84A_SCALAR_POSTAMBLE_LENGTH = new_definition
-  `KECCAK_F1600_X4_V8A_V84A_SCALAR_POSTAMBLE_LENGTH = 48`;;
+let KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_POSTAMBLE_LENGTH = new_definition
+  `KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_POSTAMBLE_LENGTH = 48`;;
 
-let KECCAK_F1600_X4_V8A_V84A_SCALAR_CORE_START = new_definition
-  `KECCAK_F1600_X4_V8A_V84A_SCALAR_CORE_START = KECCAK_F1600_X4_V8A_V84A_SCALAR_PREAMBLE_LENGTH`;;
+let KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_CORE_START = new_definition
+  `KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_CORE_START = KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_PREAMBLE_LENGTH`;;
 
-let KECCAK_F1600_X4_V8A_V84A_SCALAR_CORE_END = new_definition
-  `KECCAK_F1600_X4_V8A_V84A_SCALAR_CORE_END = LENGTH keccak_f1600_x4_v8a_v84a_scalar_mc - KECCAK_F1600_X4_V8A_V84A_SCALAR_POSTAMBLE_LENGTH`;;
+let KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_CORE_END = new_definition
+  `KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_CORE_END = LENGTH keccak_f1600_x4_v8a_v84a_scalar_mc - KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_POSTAMBLE_LENGTH`;;
 
 let LENGTH_SIMPLIFY_CONV =
   REWRITE_CONV[LENGTH_KECCAK_F1600_X4_V8A_V84A_SCALAR_MC;
-              KECCAK_F1600_X4_V8A_V84A_SCALAR_CORE_START; KECCAK_F1600_X4_V8A_V84A_SCALAR_CORE_END;
-              KECCAK_F1600_X4_V8A_V84A_SCALAR_PREAMBLE_LENGTH; KECCAK_F1600_X4_V8A_V84A_SCALAR_POSTAMBLE_LENGTH] THENC
+              KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_CORE_START; KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_CORE_END;
+              KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_PREAMBLE_LENGTH; KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_POSTAMBLE_LENGTH] THENC
   NUM_REDUCE_CONV THENC REWRITE_CONV [ADD_0];;
 
 (* ------------------------------------------------------------------------- *)
 (* Correctness proof                                                         *)
 (* ------------------------------------------------------------------------- *)
 
-let KECCAK_F1600_X4_V8A_V84A_SCALAR_CORRECT = prove
+let KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_CORRECT = prove
  (`!a rc A1 A2 A3 A4 pc stackpointer.
       aligned 16 stackpointer /\
       nonoverlapping (a,800) (stackpointer,216) /\
@@ -949,7 +949,7 @@ let KECCAK_F1600_X4_V8A_V84A_SCALAR_CORRECT = prove
                [(word pc,LENGTH keccak_f1600_x4_v8a_v84a_scalar_mc); (rc,192)]
       ==> ensures arm
            (\s. aligned_bytes_loaded s (word pc) keccak_f1600_x4_v8a_v84a_scalar_mc /\
-                read PC s = word (pc + KECCAK_F1600_X4_V8A_V84A_SCALAR_CORE_START) /\
+                read PC s = word (pc + KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_CORE_START) /\
                 read SP s = stackpointer /\
                 C_ARGUMENTS [a; rc] s /\
                 wordlist_from_memory(a,25) s = A1 /\
@@ -957,7 +957,7 @@ let KECCAK_F1600_X4_V8A_V84A_SCALAR_CORRECT = prove
                 wordlist_from_memory(word_add a (word 400),25) s = A3 /\
                 wordlist_from_memory(word_add a (word 600),25) s = A4 /\
                 wordlist_from_memory(rc,24) s = round_constants)
-           (\s. read PC s = word(pc + KECCAK_F1600_X4_V8A_V84A_SCALAR_CORE_END) /\
+           (\s. read PC s = word(pc + KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_CORE_END) /\
                 wordlist_from_memory(a,25) s = keccak 24 A1 /\
                 wordlist_from_memory(word_add a (word 200),25) s =
                 keccak 24 A2 /\
@@ -976,7 +976,7 @@ let KECCAK_F1600_X4_V8A_V84A_SCALAR_CORRECT = prove
   MAP_EVERY X_GEN_TAC
    [`a:int64`; `rc:int64`; `A1:int64 list`; `A2:int64 list`;
     `A3:int64 list`; `A4:int64 list`; `pc:num`; `stackpointer:int64`] THEN
-  REWRITE_TAC[fst KECCAK_F1600_X4_V8A_V84A_SCALAR_EXEC] THEN
+  REWRITE_TAC[fst KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_EXEC] THEN
   REWRITE_TAC[MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI; C_ARGUMENTS;
               ALL; ALLPAIRS; NONOVERLAPPING_CLAUSES] THEN
   DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN
@@ -1036,7 +1036,7 @@ let KECCAK_F1600_X4_V8A_V84A_SCALAR_CORRECT = prove
     MEMORY_128_FROM_64_TAC "a" 0 12 THEN
     MEMORY_128_FROM_64_TAC "a" 200 12 THEN
     ASM_REWRITE_TAC[WORD_ADD_0] THEN REPEAT STRIP_TAC THEN
-    ARM_STEPS_TAC KECCAK_F1600_X4_V8A_V84A_SCALAR_EXEC (1--396) THEN
+    ARM_STEPS_TAC KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_EXEC (1--396) THEN
     ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
      [CONV_TAC(LAND_CONV WORDLIST_FROM_MEMORY_CONV) THEN
       CONV_TAC(ONCE_DEPTH_CONV NORMALIZE_RELATIVE_ADDRESS_CONV) THEN
@@ -1107,7 +1107,7 @@ let KECCAK_F1600_X4_V8A_V84A_SCALAR_CORRECT = prove
       CONV_TAC(ONCE_DEPTH_CONV EL_CONV) THEN REWRITE_TAC[];
       ALL_TAC] THEN
 
-    ARM_STEPS_TAC KECCAK_F1600_X4_V8A_V84A_SCALAR_EXEC (1--339) THEN
+    ARM_STEPS_TAC KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_EXEC (1--339) THEN
     ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN
     REWRITE_TAC[CONJ_ASSOC] THEN CONJ_TAC THENL
      [REWRITE_TAC[GSYM CONJ_ASSOC];
@@ -1145,7 +1145,7 @@ let KECCAK_F1600_X4_V8A_V84A_SCALAR_CORRECT = prove
     X_GEN_TAC `i:num` THEN STRIP_TAC THEN
     CONV_TAC(ONCE_DEPTH_CONV WORDLIST_FROM_MEMORY_CONV) THEN
     CONV_TAC(ONCE_DEPTH_CONV NORMALIZE_RELATIVE_ADDRESS_CONV) THEN
-    ARM_SIM_TAC KECCAK_F1600_X4_V8A_V84A_SCALAR_EXEC [1] THEN
+    ARM_SIM_TAC KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_EXEC [1] THEN
     VAL_INT64_TAC `i:num` THEN
     ASM_REWRITE_TAC[] THEN CONV_TAC(DEPTH_CONV WORD_NUM_RED_CONV);
 
@@ -1199,7 +1199,7 @@ let KECCAK_F1600_X4_V8A_V84A_SCALAR_CORRECT = prove
     ASM_REWRITE_TAC[round_constants; CONS_11; GSYM CONJ_ASSOC] THEN
     REWRITE_TAC[GSYM round_constants] THEN
     ENSURES_INIT_TAC "s0" THEN
-    ARM_STEPS_TAC KECCAK_F1600_X4_V8A_V84A_SCALAR_EXEC (1--395) THEN
+    ARM_STEPS_TAC KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_EXEC (1--395) THEN
 
     ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
      [CONV_TAC(LAND_CONV WORDLIST_FROM_MEMORY_CONV) THEN
@@ -1274,7 +1274,7 @@ let KECCAK_F1600_X4_V8A_V84A_SCALAR_CORRECT = prove
       CONV_TAC(ONCE_DEPTH_CONV EL_CONV) THEN REWRITE_TAC[];
       ALL_TAC] THEN
 
-    ARM_STEPS_TAC KECCAK_F1600_X4_V8A_V84A_SCALAR_EXEC (1--339) THEN
+    ARM_STEPS_TAC KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_EXEC (1--339) THEN
     ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN
     REWRITE_TAC[CONJ_ASSOC] THEN CONJ_TAC THENL
      [REWRITE_TAC[GSYM CONJ_ASSOC];
@@ -1314,7 +1314,7 @@ let KECCAK_F1600_X4_V8A_V84A_SCALAR_CORRECT = prove
     X_GEN_TAC `i:num` THEN STRIP_TAC THEN
     CONV_TAC(ONCE_DEPTH_CONV WORDLIST_FROM_MEMORY_CONV) THEN
     CONV_TAC(ONCE_DEPTH_CONV NORMALIZE_RELATIVE_ADDRESS_CONV) THEN
-    ARM_SIM_TAC KECCAK_F1600_X4_V8A_V84A_SCALAR_EXEC [1] THEN
+    ARM_SIM_TAC KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_EXEC [1] THEN
     VAL_INT64_TAC `i:num` THEN
     ASM_REWRITE_TAC[] THEN CONV_TAC(DEPTH_CONV WORD_NUM_RED_CONV);
 
@@ -1338,7 +1338,7 @@ let KECCAK_F1600_X4_V8A_V84A_SCALAR_CORRECT = prove
   ASM_REWRITE_TAC[round_constants; CONS_11; GSYM CONJ_ASSOC] THEN
   REWRITE_TAC[GSYM round_constants] THEN
   ENSURES_INIT_TAC "s0" THEN
-  ARM_STEPS_TAC KECCAK_F1600_X4_V8A_V84A_SCALAR_EXEC (1--83) THEN
+  ARM_STEPS_TAC KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_EXEC (1--83) THEN
   ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN
   CONV_TAC(ONCE_DEPTH_CONV WORDLIST_FROM_MEMORY_CONV) THEN
   CONV_TAC(ONCE_DEPTH_CONV NORMALIZE_RELATIVE_ADDRESS_CONV) THEN
@@ -1353,7 +1353,7 @@ let KECCAK_F1600_X4_V8A_V84A_SCALAR_CORRECT = prove
 (* NOTE: This must be kept in sync with the CBMC specification
  * in mlkem/src/fips202/native/aarch64/src/fips202_native_aarch64.h *)
 
-let KECCAK_F1600_X4_V8A_V84A_SCALAR_SUBROUTINE_CORRECT = prove
+let KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_SUBROUTINE_CORRECT = prove
  (`!a rc A1 A2 A3 A4 pc stackpointer returnaddress.
       aligned 16 stackpointer /\
       nonoverlapping (a,800) (word_sub stackpointer (word 224),224) /\
@@ -1388,8 +1388,8 @@ let KECCAK_F1600_X4_V8A_V84A_SCALAR_SUBROUTINE_CORRECT = prove
     (WORDLIST_FROM_MEMORY_CONV THENC
      ONCE_DEPTH_CONV NORMALIZE_RELATIVE_ADDRESS_CONV) in
   CONV_TAC TWEAK_CONV THEN
-  ARM_ADD_RETURN_STACK_TAC ~pre_post_nsteps:(11,11) KECCAK_F1600_X4_V8A_V84A_SCALAR_EXEC
-   (CONV_RULE TWEAK_CONV (CONV_RULE LENGTH_SIMPLIFY_CONV KECCAK_F1600_X4_V8A_V84A_SCALAR_CORRECT))
+  ARM_ADD_RETURN_STACK_TAC ~pre_post_nsteps:(11,11) KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_EXEC
+   (CONV_RULE TWEAK_CONV (CONV_RULE LENGTH_SIMPLIFY_CONV KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_CORRECT))
   `[D8; D9; D10; D11; D12; D13; D14; D15;
     X19; X20; X21; X22; X23; X24; X25; X26; X27; X28; X29; X30]` 224);;
 
@@ -1403,10 +1403,10 @@ needs "mlkem_native/aarch64/proofs/subroutine_signatures.ml";;
 let full_spec,public_vars = mk_safety_spec
     ~keep_maychanges:false
     (assoc "sha3_keccak4_f1600_alt" subroutine_signatures)
-    KECCAK_F1600_X4_V8A_V84A_SCALAR_SUBROUTINE_CORRECT
-    KECCAK_F1600_X4_V8A_V84A_SCALAR_EXEC;;
+    KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_SUBROUTINE_CORRECT
+    KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_EXEC;;
 
-let KECCAK_F1600_X4_V8A_V84A_SCALAR_SUBROUTINE_SAFE = time prove
+let KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_SUBROUTINE_SAFE = time prove
  (`exists f_events.
        forall e a rc pc stackpointer returnaddress.
            aligned 16 stackpointer /\
@@ -1435,4 +1435,4 @@ let KECCAK_F1600_X4_V8A_V84A_SCALAR_SUBROUTINE_SAFE = time prove
                         [a,800; word_sub stackpointer (word 224),224])
                (\s s'. true)`,
   ASSERT_CONCL_TAC full_spec THEN
-  PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars KECCAK_F1600_X4_V8A_V84A_SCALAR_EXEC);;
+  PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars KECCAK_F1600_X4_V8A_V84A_SCALAR_HYBRID_EXEC);;
diff --git a/proofs/hol_light/aarch64/proofs/poly_mulcache_compute_aarch64_asm.ml b/proofs/hol_light/aarch64/proofs/poly_mulcache_compute_aarch64_asm.ml
index 4d08fc03d..c44556ac9 100644
--- a/proofs/hol_light/aarch64/proofs/poly_mulcache_compute_aarch64_asm.ml
+++ b/proofs/hol_light/aarch64/proofs/poly_mulcache_compute_aarch64_asm.ml
@@ -155,7 +155,7 @@ let poly_mulcache_compute_GOAL = `!dst src zetas zetas_twisted x pc.
 (* Proof                                                                     *)
 (* ------------------------------------------------------------------------- *)
 
-let MLKEM_MULCACHE_COMPUTE_CORRECT = prove(poly_mulcache_compute_GOAL,
+let MLKEM_POLY_MULCACHE_COMPUTE_CORRECT = prove(poly_mulcache_compute_GOAL,
     CONV_TAC LENGTH_SIMPLIFY_CONV THEN
     REWRITE_TAC [MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI;
       NONOVERLAPPING_CLAUSES; ALL; C_ARGUMENTS; fst poly_mulcache_compute_EXEC;
@@ -240,7 +240,7 @@ let MLKEM_MULCACHE_COMPUTE_CORRECT = prove(poly_mulcache_compute_GOAL,
 (* NOTE: This must be kept in sync with the CBMC specification
  * in mlkem/src/native/aarch64/src/arith_native_aarch64.h *)
 
-let MLKEM_MULCACHE_COMPUTE_SUBROUTINE_CORRECT = prove
+let MLKEM_POLY_MULCACHE_COMPUTE_SUBROUTINE_CORRECT = prove
  (`!dst src zetas zetas_twisted x pc returnaddress.
     ALL (nonoverlapping (dst, 256))
         [(word pc, LENGTH poly_mulcache_compute_mc);
@@ -279,7 +279,7 @@ let MLKEM_MULCACHE_COMPUTE_SUBROUTINE_CORRECT = prove
     PURE_REWRITE_CONV [WORD_ADD_0] in
   CONV_TAC TWEAK_CONV THEN
   ARM_ADD_RETURN_NOSTACK_TAC poly_mulcache_compute_EXEC
-   (CONV_RULE TWEAK_CONV (CONV_RULE LENGTH_SIMPLIFY_CONV MLKEM_MULCACHE_COMPUTE_CORRECT)));;
+   (CONV_RULE TWEAK_CONV (CONV_RULE LENGTH_SIMPLIFY_CONV MLKEM_POLY_MULCACHE_COMPUTE_CORRECT)));;
 
 
 (* ------------------------------------------------------------------------- *)
@@ -291,10 +291,10 @@ needs "mlkem_native/aarch64/proofs/subroutine_signatures.ml";;
 let full_spec,public_vars = mk_safety_spec
     ~keep_maychanges:false
     (assoc "mlkem_mulcache_compute" subroutine_signatures)
-    MLKEM_MULCACHE_COMPUTE_SUBROUTINE_CORRECT
+    MLKEM_POLY_MULCACHE_COMPUTE_SUBROUTINE_CORRECT
     poly_mulcache_compute_EXEC;;
 
-let MLKEM_MULCACHE_COMPUTE_SUBROUTINE_SAFE = time prove
+let MLKEM_POLY_MULCACHE_COMPUTE_SUBROUTINE_SAFE = time prove
  (`exists f_events.
        forall e dst src zetas zetas_twisted pc returnaddress.
            ALL (nonoverlapping (dst,256))
diff --git a/proofs/hol_light/aarch64/proofs/poly_tomont_aarch64_asm.ml b/proofs/hol_light/aarch64/proofs/poly_tomont_aarch64_asm.ml
index 73fb3c234..123d3a02e 100644
--- a/proofs/hol_light/aarch64/proofs/poly_tomont_aarch64_asm.ml
+++ b/proofs/hol_light/aarch64/proofs/poly_tomont_aarch64_asm.ml
@@ -132,7 +132,7 @@ let POLY_TOMONT_GOAL = `!ptr x pc.
 (* Proof                                                                     *)
 (* ------------------------------------------------------------------------- *)
 
-let MLKEM_TOMONT_CORRECT = prove(POLY_TOMONT_GOAL,
+let MLKEM_POLY_TOMONT_CORRECT = prove(POLY_TOMONT_GOAL,
     CONV_TAC LENGTH_SIMPLIFY_CONV THEN
     REWRITE_TAC [MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI;
       NONOVERLAPPING_CLAUSES; C_ARGUMENTS; fst POLY_TOMONT_EXEC] THEN
@@ -215,7 +215,7 @@ let MLKEM_TOMONT_CORRECT = prove(POLY_TOMONT_GOAL,
 (* NOTE: This must be kept in sync with the CBMC specification
  * in mlkem/src/native/aarch64/src/arith_native_aarch64.h *)
 
-let MLKEM_TOMONT_SUBROUTINE_CORRECT = prove
+let MLKEM_POLY_TOMONT_SUBROUTINE_CORRECT = prove
  (`!ptr x pc returnaddress.
     nonoverlapping (word pc, LENGTH poly_tomont_asm_mc) (ptr, 512)
     ==>
@@ -254,7 +254,7 @@ let MLKEM_TOMONT_SUBROUTINE_CORRECT = prove
     PURE_REWRITE_CONV [WORD_ADD_0] in
   CONV_TAC TWEAK_CONV THEN
   ARM_ADD_RETURN_NOSTACK_TAC POLY_TOMONT_EXEC
-   (CONV_RULE TWEAK_CONV (CONV_RULE LENGTH_SIMPLIFY_CONV MLKEM_TOMONT_CORRECT)));;
+   (CONV_RULE TWEAK_CONV (CONV_RULE LENGTH_SIMPLIFY_CONV MLKEM_POLY_TOMONT_CORRECT)));;
 
 (* ------------------------------------------------------------------------- *)
 (* Constant-time and memory safety proof.                                    *)
@@ -266,10 +266,10 @@ needs "mlkem_native/aarch64/proofs/subroutine_signatures.ml";;
 let full_spec,public_vars = mk_safety_spec
     ~keep_maychanges:false
     (assoc "mlkem_tomont" subroutine_signatures)
-    MLKEM_TOMONT_SUBROUTINE_CORRECT
+    MLKEM_POLY_TOMONT_SUBROUTINE_CORRECT
     POLY_TOMONT_EXEC;;
 
-let MLKEM_TOMONT_SUBROUTINE_SAFE = time prove
+let MLKEM_POLY_TOMONT_SUBROUTINE_SAFE = time prove
  (`exists f_events.
        forall e ptr pc returnaddress.
            nonoverlapping (word pc,LENGTH poly_tomont_asm_mc) (ptr,512)
diff --git a/proofs/hol_light/aarch64/proofs/polyvec_basemul_acc_montgomery_cached_k2_aarch64_asm.ml b/proofs/hol_light/aarch64/proofs/polyvec_basemul_acc_montgomery_cached_k2_aarch64_asm.ml
index 40247306a..db963b936 100644
--- a/proofs/hol_light/aarch64/proofs/polyvec_basemul_acc_montgomery_cached_k2_aarch64_asm.ml
+++ b/proofs/hol_light/aarch64/proofs/polyvec_basemul_acc_montgomery_cached_k2_aarch64_asm.ml
@@ -340,7 +340,7 @@ let poly_basemul_acc_montgomery_cached_k2_GOAL = `forall srcA srcB srcBt dst x0
  (* Proof                                                                     *)
  (* ------------------------------------------------------------------------- *)
 
-let poly_basemul_acc_montgomery_cached_k2_SPEC = prove(poly_basemul_acc_montgomery_cached_k2_GOAL,
+let MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K2_CORRECT = prove(poly_basemul_acc_montgomery_cached_k2_GOAL,
      CONV_TAC LENGTH_SIMPLIFY_CONV THEN
      REWRITE_TAC [MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI;
        MODIFIABLE_SIMD_REGS;
@@ -410,7 +410,7 @@ let poly_basemul_acc_montgomery_cached_k2_SPEC = prove(poly_basemul_acc_montgome
 
 (* NOTE: This needs to be kept in sync with the CBMC spec in
  * mlkem/src/native/aarch64/src/arith_native_aarch64.h *)
-let MLKEM_BASEMUL_K2_SUBROUTINE_CORRECT = prove(
+let MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K2_SUBROUTINE_CORRECT = prove(
    `forall srcA srcB srcBt dst x0 y0 y0t x1 y1 y1t pc stackpointer returnaddress.
       aligned 16 stackpointer /\
       ALLPAIRS nonoverlapping
@@ -450,7 +450,7 @@ let MLKEM_BASEMUL_K2_SUBROUTINE_CORRECT = prove(
   REWRITE_TAC[fst poly_basemul_acc_montgomery_cached_k2_EXEC] THEN
   CONV_TAC TWEAK_CONV THEN
   ARM_ADD_RETURN_STACK_TAC ~pre_post_nsteps:(5,5) poly_basemul_acc_montgomery_cached_k2_EXEC
-     (REWRITE_RULE[fst poly_basemul_acc_montgomery_cached_k2_EXEC] (CONV_RULE TWEAK_CONV (CONV_RULE LENGTH_SIMPLIFY_CONV poly_basemul_acc_montgomery_cached_k2_SPEC)))
+     (REWRITE_RULE[fst poly_basemul_acc_montgomery_cached_k2_EXEC] (CONV_RULE TWEAK_CONV (CONV_RULE LENGTH_SIMPLIFY_CONV MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K2_CORRECT)))
       `[D8; D9; D10; D11; D12; D13; D14; D15]` 64  THEN
    WORD_ARITH_TAC)
 ;;
@@ -466,10 +466,10 @@ needs "mlkem_native/aarch64/proofs/subroutine_signatures.ml";;
 let full_spec,public_vars = mk_safety_spec
     ~keep_maychanges:false
     (assoc "mlkem_basemul_k2" subroutine_signatures)
-    MLKEM_BASEMUL_K2_SUBROUTINE_CORRECT
+    MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K2_SUBROUTINE_CORRECT
     poly_basemul_acc_montgomery_cached_k2_EXEC;;
 
-let MLKEM_BASEMUL_K2_SUBROUTINE_SAFE = time prove
+let MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K2_SUBROUTINE_SAFE = time prove
  (`exists f_events.
        forall e srcA srcB srcBt dst pc stackpointer returnaddress.
            aligned 16 stackpointer /\
diff --git a/proofs/hol_light/aarch64/proofs/polyvec_basemul_acc_montgomery_cached_k3_aarch64_asm.ml b/proofs/hol_light/aarch64/proofs/polyvec_basemul_acc_montgomery_cached_k3_aarch64_asm.ml
index e511f8df9..5582ac808 100644
--- a/proofs/hol_light/aarch64/proofs/polyvec_basemul_acc_montgomery_cached_k3_aarch64_asm.ml
+++ b/proofs/hol_light/aarch64/proofs/polyvec_basemul_acc_montgomery_cached_k3_aarch64_asm.ml
@@ -404,7 +404,7 @@ let basemul3_odd = define
   (* Proof                                                                     *)
   (* ------------------------------------------------------------------------- *)
 
- let poly_basemul_acc_montgomery_cached_k3_SPEC = prove (poly_basemul_acc_montgomery_cached_k3_GOAL,
+ let MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K3_CORRECT = prove (poly_basemul_acc_montgomery_cached_k3_GOAL,
        CONV_TAC LENGTH_SIMPLIFY_CONV THEN
        REWRITE_TAC [MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI;
         MODIFIABLE_SIMD_REGS;
@@ -474,7 +474,7 @@ let basemul3_odd = define
 
  (* NOTE: This needs to be kept in sync with the CBMC spec in
   * mlkem/src/native/aarch64/src/arith_native_aarch64.h *)
- let MLKEM_BASEMUL_K3_SUBROUTINE_CORRECT = prove(
+ let MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K3_SUBROUTINE_CORRECT = prove(
     `forall srcA srcB srcBt dst x0 y0 y0t x1 y1 y1t x2 y2 y2t pc stackpointer returnaddress.
        aligned 16 stackpointer /\
        ALLPAIRS nonoverlapping
@@ -520,7 +520,7 @@ let basemul3_odd = define
    REWRITE_TAC[fst poly_basemul_acc_montgomery_cached_k3_EXEC] THEN
    CONV_TAC TWEAK_CONV THEN
    ARM_ADD_RETURN_STACK_TAC ~pre_post_nsteps:(5,5) poly_basemul_acc_montgomery_cached_k3_EXEC
-      (REWRITE_RULE[fst poly_basemul_acc_montgomery_cached_k3_EXEC] (CONV_RULE TWEAK_CONV (CONV_RULE LENGTH_SIMPLIFY_CONV poly_basemul_acc_montgomery_cached_k3_SPEC)))
+      (REWRITE_RULE[fst poly_basemul_acc_montgomery_cached_k3_EXEC] (CONV_RULE TWEAK_CONV (CONV_RULE LENGTH_SIMPLIFY_CONV MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K3_CORRECT)))
        `[D8; D9; D10; D11; D12; D13; D14; D15]` 64  THEN
     WORD_ARITH_TAC)
  ;;
@@ -535,10 +535,10 @@ needs "mlkem_native/aarch64/proofs/subroutine_signatures.ml";;
 let full_spec,public_vars = mk_safety_spec
     ~keep_maychanges:false
     (assoc "mlkem_basemul_k3" subroutine_signatures)
-    MLKEM_BASEMUL_K3_SUBROUTINE_CORRECT
+    MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K3_SUBROUTINE_CORRECT
     poly_basemul_acc_montgomery_cached_k3_EXEC;;
 
-let MLKEM_BASEMUL_K3_SUBROUTINE_SAFE = time prove
+let MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K3_SUBROUTINE_SAFE = time prove
  (`exists f_events.
        forall e srcA srcB srcBt dst pc stackpointer returnaddress.
            aligned 16 stackpointer /\
diff --git a/proofs/hol_light/aarch64/proofs/polyvec_basemul_acc_montgomery_cached_k4_aarch64_asm.ml b/proofs/hol_light/aarch64/proofs/polyvec_basemul_acc_montgomery_cached_k4_aarch64_asm.ml
index c4954594e..1b46d50ca 100644
--- a/proofs/hol_light/aarch64/proofs/polyvec_basemul_acc_montgomery_cached_k4_aarch64_asm.ml
+++ b/proofs/hol_light/aarch64/proofs/polyvec_basemul_acc_montgomery_cached_k4_aarch64_asm.ml
@@ -469,7 +469,7 @@ let basemul4_odd = define
    (* Proof                                                                     *)
    (* ------------------------------------------------------------------------- *)
 
-  let poly_basemul_acc_montgomery_cached_k4_SPEC = prove(poly_basemul_acc_montgomery_cached_k4_GOAL,
+  let MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K4_CORRECT = prove(poly_basemul_acc_montgomery_cached_k4_GOAL,
         CONV_TAC LENGTH_SIMPLIFY_CONV THEN
         REWRITE_TAC [MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI;
          MODIFIABLE_SIMD_REGS;
@@ -539,7 +539,7 @@ let basemul4_odd = define
 
   (* NOTE: This needs to be kept in sync with the CBMC spec in
    * mlkem/src/native/aarch64/src/arith_native_aarch64.h *)
-  let MLKEM_BASEMUL_K4_SUBROUTINE_CORRECT = prove(
+  let MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K4_SUBROUTINE_CORRECT = prove(
      `forall srcA srcB srcBt dst x0 y0 y0t x1 y1 y1t x2 y2 y2t x3 y3 y3t pc stackpointer returnaddress.
         aligned 16 stackpointer /\
         ALLPAIRS nonoverlapping
@@ -592,7 +592,7 @@ let basemul4_odd = define
     REWRITE_TAC[fst poly_basemul_acc_montgomery_cached_k4_EXEC] THEN
     CONV_TAC TWEAK_CONV THEN
     ARM_ADD_RETURN_STACK_TAC ~pre_post_nsteps:(5,5) poly_basemul_acc_montgomery_cached_k4_EXEC
-       (REWRITE_RULE[fst poly_basemul_acc_montgomery_cached_k4_EXEC] (CONV_RULE TWEAK_CONV (CONV_RULE LENGTH_SIMPLIFY_CONV poly_basemul_acc_montgomery_cached_k4_SPEC)))
+       (REWRITE_RULE[fst poly_basemul_acc_montgomery_cached_k4_EXEC] (CONV_RULE TWEAK_CONV (CONV_RULE LENGTH_SIMPLIFY_CONV MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K4_CORRECT)))
         `[D8; D9; D10; D11; D12; D13; D14; D15]` 64  THEN
      WORD_ARITH_TAC)
   ;;
@@ -607,10 +607,10 @@ needs "mlkem_native/aarch64/proofs/subroutine_signatures.ml";;
 let full_spec,public_vars = mk_safety_spec
     ~keep_maychanges:false
     (assoc "mlkem_basemul_k4" subroutine_signatures)
-    MLKEM_BASEMUL_K4_SUBROUTINE_CORRECT
+    MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K4_SUBROUTINE_CORRECT
     poly_basemul_acc_montgomery_cached_k4_EXEC;;
 
-let MLKEM_BASEMUL_K4_SUBROUTINE_SAFE = time prove
+let MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K4_SUBROUTINE_SAFE = time prove
  (`exists f_events.
        forall e srcA srcB srcBt dst pc stackpointer returnaddress.
            aligned 16 stackpointer /\
diff --git a/proofs/hol_light/x86_64/proofs/keccak_f1600_x4_avx2_asm.ml b/proofs/hol_light/x86_64/proofs/keccak_f1600_x4_avx2_asm.ml
index 4bd1123a2..19aebb270 100644
--- a/proofs/hol_light/x86_64/proofs/keccak_f1600_x4_avx2_asm.ml
+++ b/proofs/hol_light/x86_64/proofs/keccak_f1600_x4_avx2_asm.ml
@@ -751,32 +751,32 @@ let keccak_f1600_x4_avx2_mc = define_assert_from_elf
 
 let keccak_f1600_x4_avx2_tmc = define_trimmed "keccak_f1600_x4_avx2_tmc" keccak_f1600_x4_avx2_mc;;
 
-let KECCAK_F1600_X4_AVX2_EXEC = X86_MK_CORE_EXEC_RULE keccak_f1600_x4_avx2_tmc;;
-let keccak_f1600_x4_avx2_TMC_EXEC = KECCAK_F1600_X4_AVX2_EXEC;;
+let KECCAK_F1600_X4_EXEC = X86_MK_CORE_EXEC_RULE keccak_f1600_x4_avx2_tmc;;
+let keccak_f1600_x4_avx2_TMC_EXEC = KECCAK_F1600_X4_EXEC;;
 
-let LENGTH_KECCAK_F1600_X4_AVX2_TMC =
+let LENGTH_KECCAK_F1600_X4_TMC =
   REWRITE_CONV[keccak_f1600_x4_avx2_tmc] `LENGTH keccak_f1600_x4_avx2_tmc`
   |> CONV_RULE(RAND_CONV LENGTH_CONV);;
 
 (* Preamble: MOV r11, rsp (3) + AND rsp, -32 (4) + SUB rsp, 768 (7) = 14 bytes *)
-let KECCAK_F1600_X4_AVX2_PREAMBLE_LENGTH = new_definition
-  `KECCAK_F1600_X4_AVX2_PREAMBLE_LENGTH = 14`;;
+let KECCAK_F1600_X4_PREAMBLE_LENGTH = new_definition
+  `KECCAK_F1600_X4_PREAMBLE_LENGTH = 14`;;
 
 (* Postamble: MOV rsp, r11 (3 bytes) + RET (1 byte) = 4 bytes *)
-let KECCAK_F1600_X4_AVX2_POSTAMBLE_LENGTH = new_definition
-  `KECCAK_F1600_X4_AVX2_POSTAMBLE_LENGTH = 4`;;
+let KECCAK_F1600_X4_POSTAMBLE_LENGTH = new_definition
+  `KECCAK_F1600_X4_POSTAMBLE_LENGTH = 4`;;
 
-let KECCAK_F1600_X4_AVX2_CORE_END = new_definition
-  `KECCAK_F1600_X4_AVX2_CORE_END = LENGTH keccak_f1600_x4_avx2_tmc - KECCAK_F1600_X4_AVX2_POSTAMBLE_LENGTH`;;
+let KECCAK_F1600_X4_CORE_END = new_definition
+  `KECCAK_F1600_X4_CORE_END = LENGTH keccak_f1600_x4_avx2_tmc - KECCAK_F1600_X4_POSTAMBLE_LENGTH`;;
 
 let LENGTH_SIMPLIFY_CONV =
-  REWRITE_CONV[LENGTH_KECCAK_F1600_X4_AVX2_TMC;
-              KECCAK_F1600_X4_AVX2_CORE_END;
-              KECCAK_F1600_X4_AVX2_PREAMBLE_LENGTH;
-              KECCAK_F1600_X4_AVX2_POSTAMBLE_LENGTH] THENC
+  REWRITE_CONV[LENGTH_KECCAK_F1600_X4_TMC;
+              KECCAK_F1600_X4_CORE_END;
+              KECCAK_F1600_X4_PREAMBLE_LENGTH;
+              KECCAK_F1600_X4_POSTAMBLE_LENGTH] THENC
   NUM_REDUCE_CONV THENC REWRITE_CONV [ADD_0];;
 
-let KECCAK_F1600_X4_AVX2_CORRECT = prove
+let KECCAK_F1600_X4_CORRECT = prove
   (`!rc_pointer:int64 bitstate_in:int64 rho8_ptr:int64 rho56_ptr:int64 A1 A2 A3 A4 pc:num stackpointer:int64.
   PAIRWISE nonoverlapping
   [(word pc, LENGTH keccak_f1600_x4_avx2_tmc);
@@ -787,7 +787,7 @@ let KECCAK_F1600_X4_AVX2_CORRECT = prove
    (rho56_ptr, 32)]
   ==> ensures x86
          (\s. bytes_loaded s (word pc) (BUTLAST keccak_f1600_x4_avx2_tmc) /\
-              read RIP s = word (pc + KECCAK_F1600_X4_AVX2_PREAMBLE_LENGTH) /\
+              read RIP s = word (pc + KECCAK_F1600_X4_PREAMBLE_LENGTH) /\
               read RSP s = stackpointer /\
               read RDI s = bitstate_in /\
               C_ARGUMENTS [bitstate_in; rc_pointer; rho8_ptr; rho56_ptr] s /\
@@ -798,7 +798,7 @@ let KECCAK_F1600_X4_AVX2_CORRECT = prove
               wordlist_from_memory(word_add bitstate_in (word 200),25) s = A2 /\
               wordlist_from_memory(word_add bitstate_in (word 400),25) s = A3 /\
               wordlist_from_memory(word_add bitstate_in (word 600),25) s = A4)
-             (\s. read RIP s = word(pc + KECCAK_F1600_X4_AVX2_CORE_END) /\
+             (\s. read RIP s = word(pc + KECCAK_F1600_X4_CORE_END) /\
                   wordlist_from_memory(bitstate_in,25) s = keccak 24 A1 /\
                   wordlist_from_memory(word_add bitstate_in (word 200),25) s = keccak 24 A2 /\
                   wordlist_from_memory(word_add bitstate_in (word 400),25) s = keccak 24 A3 /\
@@ -882,7 +882,7 @@ let KECCAK_F1600_X4_AVX2_CORRECT = prove
     MEMORY_256_FROM_64_TAC "rho56_ptr" 0 4 THEN
     ASM_REWRITE_TAC[WORD_ADD_0] THEN
     REPEAT STRIP_TAC THEN
-    X86_STEPS_TAC KECCAK_F1600_X4_AVX2_EXEC (1--96) THEN
+    X86_STEPS_TAC KECCAK_F1600_X4_EXEC (1--96) THEN
     ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN
     REPEAT CONJ_TAC THENL
     [PURE_ONCE_REWRITE_TAC[ARITH_RULE `8 * 0 = 0`] THEN
@@ -940,7 +940,7 @@ let KECCAK_F1600_X4_AVX2_CORRECT = prove
     MEMORY_256_FROM_64_TAC "rho8_ptr" 0 4 THEN
     MEMORY_256_FROM_64_TAC "rho56_ptr" 0 4 THEN
     ASM_REWRITE_TAC[WORD_ADD_0] THEN REPEAT STRIP_TAC THEN
-    X86_STEPS_TAC KECCAK_F1600_X4_AVX2_EXEC (1--223) THEN
+    X86_STEPS_TAC KECCAK_F1600_X4_EXEC (1--223) THEN
     ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN
     REPEAT CONJ_TAC THENL
       [REWRITE_TAC[WORD_ADD];
@@ -992,7 +992,7 @@ let KECCAK_F1600_X4_AVX2_CORRECT = prove
     MEMORY_256_FROM_64_TAC "rho8_ptr" 0 4 THEN
     MEMORY_256_FROM_64_TAC "rho56_ptr" 0 4 THEN
     ASM_REWRITE_TAC[WORD_ADD_0] THEN REPEAT STRIP_TAC THEN
-    X86_STEPS_TAC KECCAK_F1600_X4_AVX2_EXEC (1--1) THEN
+    X86_STEPS_TAC KECCAK_F1600_X4_EXEC (1--1) THEN
     ENSURES_FINAL_STATE_TAC THEN
     ASM_REWRITE_TAC[];
 
@@ -1015,7 +1015,7 @@ let KECCAK_F1600_X4_AVX2_CORRECT = prove
     CONV_TAC NUM_REDUCE_CONV THEN
     REWRITE_TAC [keccak; keccak_round] THEN
     ENSURES_INIT_TAC "s0" THEN
-    X86_STEPS_TAC KECCAK_F1600_X4_AVX2_EXEC (1--96) THEN
+    X86_STEPS_TAC KECCAK_F1600_X4_EXEC (1--96) THEN
     REPEAT(FIRST_X_ASSUM(STRIP_ASSUME_TAC o
       CONV_RULE(READ_MEMORY_SPLIT_CONV 2) o
       check (can (term_match [] `read qqq s:int256 = xxx`) o concl))) THEN
@@ -1025,9 +1025,9 @@ let KECCAK_F1600_X4_AVX2_CORRECT = prove
     BITBLAST_TAC]);;
 
 
-let KECCAK_F1600_X4_AVX2_FULL_EXEC = X86_MK_EXEC_RULE keccak_f1600_x4_avx2_tmc;;
+let KECCAK_F1600_X4_FULL_EXEC = X86_MK_EXEC_RULE keccak_f1600_x4_avx2_tmc;;
 
-let KECCAK_F1600_X4_AVX2_NOIBT_SUBROUTINE_CORRECT = prove
+let KECCAK_F1600_X4_NOIBT_SUBROUTINE_CORRECT = prove
  (`!rc_pointer:int64 bitstate_in:int64 rho8_ptr:int64 rho56_ptr:int64 A1 A2 A3 A4 pc:num stackpointer:int64 returnaddress.
   PAIRWISE nonoverlapping
   [(word pc, LENGTH keccak_f1600_x4_avx2_tmc);
@@ -1069,14 +1069,14 @@ let KECCAK_F1600_X4_AVX2_NOIBT_SUBROUTINE_CORRECT = prove
   WORD_FORALL_OFFSET_TAC 0x31f THEN
   REWRITE_TAC[MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI] THEN
   REWRITE_TAC[PAIRWISE; ALL; C_ARGUMENTS; NONOVERLAPPING_CLAUSES] THEN
-  REWRITE_TAC[fst KECCAK_F1600_X4_AVX2_FULL_EXEC] THEN
+  REWRITE_TAC[fst KECCAK_F1600_X4_FULL_EXEC] THEN
   REWRITE_TAC[WORDLIST_FROM_MEMORY] THEN
   CONV_TAC(ONCE_DEPTH_CONV NUM_MULT_CONV) THEN
   REPEAT STRIP_TAC THEN
 
   (* Step through the three preamble instructions. *)
   ENSURES_INIT_TAC "s0" THEN
-  X86_STEPS_TAC KECCAK_F1600_X4_AVX2_FULL_EXEC (1--3) THEN
+  X86_STEPS_TAC KECCAK_F1600_X4_FULL_EXEC (1--3) THEN
 
   (* Abbreviate the data-dependent slack introduced by `and rsp, -32`.
      `delta` is the number of bytes (0..31) the alignment shaved off rsp;
@@ -1101,7 +1101,7 @@ let KECCAK_F1600_X4_AVX2_NOIBT_SUBROUTINE_CORRECT = prove
     `rho8_ptr:int64`; `rho56_ptr:int64`;
     `A1:int64 list`; `A2:int64 list`; `A3:int64 list`; `A4:int64 list`;
     `pc:num`; `word_add stackpointer (word delta):int64`]
-   (CONV_RULE LENGTH_SIMPLIFY_CONV KECCAK_F1600_X4_AVX2_CORRECT)) THEN
+   (CONV_RULE LENGTH_SIMPLIFY_CONV KECCAK_F1600_X4_CORRECT)) THEN
   ANTS_TAC THENL
    [REPEAT(FIRST_X_ASSUM(MP_TAC o check (is_imp o concl))) THEN
     REWRITE_TAC[PAIRWISE; ALL; C_ARGUMENTS; NONOVERLAPPING_CLAUSES] THEN
@@ -1112,16 +1112,16 @@ let KECCAK_F1600_X4_AVX2_NOIBT_SUBROUTINE_CORRECT = prove
   REWRITE_TAC[C_ARGUMENTS; SOME_FLAGS] THEN
   REWRITE_TAC[WORDLIST_FROM_MEMORY] THEN
   CONV_TAC(ONCE_DEPTH_CONV NUM_MULT_CONV) THEN
-  X86_BIGSTEP_TAC KECCAK_F1600_X4_AVX2_FULL_EXEC "s4" THENL
+  X86_BIGSTEP_TAC KECCAK_F1600_X4_FULL_EXEC "s4" THENL
    [MATCH_MP_TAC BYTES_LOADED_BUTLAST THEN ASM_REWRITE_TAC[];
     ALL_TAC] THEN
-  X86_STEPS_TAC KECCAK_F1600_X4_AVX2_FULL_EXEC (5--6) THEN
+  X86_STEPS_TAC KECCAK_F1600_X4_FULL_EXEC (5--6) THEN
   ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[]);;
 
 (* NOTE: This must be kept in sync with the CBMC specification
  * in dev/fips202/x86_64/src/fips202_native_x86_64.h *)
 
-let KECCAK_F1600_X4_AVX2_SUBROUTINE_CORRECT = prove
+let KECCAK_F1600_X4_SUBROUTINE_CORRECT = prove
  (`!rc_pointer:int64 bitstate_in:int64 rho8_ptr:int64 rho56_ptr:int64 A1 A2 A3 A4 pc:num stackpointer:int64 returnaddress.
   PAIRWISE nonoverlapping
   [(word pc, LENGTH keccak_f1600_x4_avx2_mc);
@@ -1160,7 +1160,7 @@ let KECCAK_F1600_X4_AVX2_SUBROUTINE_CORRECT = prove
   MATCH_ACCEPT_TAC(ADD_IBT_RULE
     (CONV_RULE TWEAK_CONV
       (REWRITE_RULE[PAIRWISE; ALL; NONOVERLAPPING_CLAUSES]
-        KECCAK_F1600_X4_AVX2_NOIBT_SUBROUTINE_CORRECT))));;
+        KECCAK_F1600_X4_NOIBT_SUBROUTINE_CORRECT))));;
 
 (* ========================================================================= *)
 (* Constant-time and memory safety proof.                                    *)
@@ -1173,10 +1173,10 @@ needs "mlkem_native/x86_64/proofs/subroutine_signatures.ml";;
 let full_spec,public_vars = mk_safety_spec
     ~keep_maychanges:true
     (assoc "keccak_f1600_x4_avx2" subroutine_signatures)
-    (CONV_RULE LENGTH_SIMPLIFY_CONV KECCAK_F1600_X4_AVX2_CORRECT)
-    KECCAK_F1600_X4_AVX2_EXEC;;
+    (CONV_RULE LENGTH_SIMPLIFY_CONV KECCAK_F1600_X4_CORRECT)
+    KECCAK_F1600_X4_EXEC;;
 
-let KECCAK_F1600_X4_AVX2_SAFE = time prove
+let KECCAK_F1600_X4_SAFE = time prove
  (`exists f_events.
        forall e rc_pointer bitstate_in rho8_ptr rho56_ptr pc stackpointer.
            PAIRWISE nonoverlapping
@@ -1187,12 +1187,12 @@ let KECCAK_F1600_X4_AVX2_SAFE = time prove
                (\s.
                     bytes_loaded s (word pc)
                     (BUTLAST keccak_f1600_x4_avx2_tmc) /\
-                    read RIP s = word (pc + KECCAK_F1600_X4_AVX2_PREAMBLE_LENGTH) /\
+                    read RIP s = word (pc + KECCAK_F1600_X4_PREAMBLE_LENGTH) /\
                     read RSP s = stackpointer /\
                     C_ARGUMENTS [bitstate_in; rc_pointer; rho8_ptr; rho56_ptr] s /\
                     read events s = e)
                (\s.
-                    read RIP s = word (pc + KECCAK_F1600_X4_AVX2_CORE_END) /\
+                    read RIP s = word (pc + KECCAK_F1600_X4_CORE_END) /\
                     (exists e2.
                          read events s = APPEND e2 e /\
                          e2 = f_events rc_pointer rho8_ptr rho56_ptr bitstate_in pc stackpointer /\
@@ -1211,7 +1211,7 @@ let KECCAK_F1600_X4_AVX2_SAFE = time prove
   CONV_TAC(ONCE_DEPTH_CONV LENGTH_SIMPLIFY_CONV) THEN
   ASSERT_CONCL_TAC full_spec THEN
   REWRITE_TAC[PAIRWISE; ALL; NONOVERLAPPING_CLAUSES] THEN
-  PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars KECCAK_F1600_X4_AVX2_EXEC);;
+  PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars KECCAK_F1600_X4_EXEC);;
 
 
 (* ========================================================================= *)
@@ -1254,7 +1254,7 @@ let FRAME_CONTAINED = prove
   REWRITE_TAC[VAL_WORD_ADD; VAL_WORD; DIMINDEX_64; CONG] THEN
   CONV_TAC MOD_DOWN_CONV THEN AP_THM_TAC THEN AP_TERM_TAC THEN ARITH_TAC);;
 
-let KECCAK_F1600_X4_AVX2_NOIBT_SUBROUTINE_SAFE = time prove
+let KECCAK_F1600_X4_NOIBT_SUBROUTINE_SAFE = time prove
  (`exists f_events.
        forall e rc_pointer bitstate_in rho8_ptr rho56_ptr pc stackpointer returnaddress.
           PAIRWISE nonoverlapping
@@ -1288,7 +1288,7 @@ let KECCAK_F1600_X4_AVX2_NOIBT_SUBROUTINE_SAFE = time prove
                             stackpointer,8]))
                (\s s'. true)`,
   let EXPAND_PAIRWISE_CONV = REWRITE_CONV[PAIRWISE; ALL; NONOVERLAPPING_CLAUSES] in
-  let inner_safe = CONV_RULE LENGTH_SIMPLIFY_CONV KECCAK_F1600_X4_AVX2_SAFE in
+  let inner_safe = CONV_RULE LENGTH_SIMPLIFY_CONV KECCAK_F1600_X4_SAFE in
   let execth = X86_MK_EXEC_RULE keccak_f1600_x4_avx2_tmc in
   CONV_TAC(ONCE_DEPTH_CONV EXPAND_PAIRWISE_CONV) THEN
   (* Skolemize the inner SAFE's existential f_events into a free term
@@ -1311,7 +1311,7 @@ let KECCAK_F1600_X4_AVX2_NOIBT_SUBROUTINE_SAFE = time prove
                (word_sub
                   (word_and stackpointer (word 0xffffffffffffffe0))
                   (word 0x300)))):uarch_event list` THEN
-  REWRITE_TAC[LENGTH_KECCAK_F1600_X4_AVX2_TMC] THEN
+  REWRITE_TAC[LENGTH_KECCAK_F1600_X4_TMC] THEN
   REPEAT GEN_TAC THEN
   REWRITE_TAC[NONOVERLAPPING_CLAUSES; ALL; PAIRWISE; C_ARGUMENTS] THEN
   REWRITE_TAC[fst execth] THEN
@@ -1368,7 +1368,7 @@ let KECCAK_F1600_X4_AVX2_NOIBT_SUBROUTINE_SAFE = time prove
          ((inner_f_events:int64->int64->int64->int64->num->int64->uarch_event list)
             rc_pointer rho8_ptr rho56_ptr bitstate_in pc
             (word_add (word_sub stackpointer (word 0x31f)) (word delta))))` THEN
-  REWRITE_TAC[LENGTH_KECCAK_F1600_X4_AVX2_TMC] THEN
+  REWRITE_TAC[LENGTH_KECCAK_F1600_X4_TMC] THEN
   REWRITE_TAC[APPEND] THEN
   REWRITE_TAC[memaccess_inbounds; ALL] THEN
   (* The two postamble events are trivially in bounds: EventJump is
@@ -1395,7 +1395,7 @@ let KECCAK_F1600_X4_AVX2_NOIBT_SUBROUTINE_SAFE = time prove
   REWRITE_TAC[EX] THEN
   ASM_MESON_TAC[CONTAINED_REFL; FRAME_CONTAINED]);;
 
-let KECCAK_F1600_X4_AVX2_SUBROUTINE_SAFE = time prove
+let KECCAK_F1600_X4_SUBROUTINE_SAFE = time prove
  (`exists f_events.
        forall e rc_pointer bitstate_in rho8_ptr rho56_ptr pc stackpointer returnaddress.
           PAIRWISE nonoverlapping
@@ -1432,4 +1432,4 @@ let KECCAK_F1600_X4_AVX2_SUBROUTINE_SAFE = time prove
   CONV_TAC(ONCE_DEPTH_CONV EXPAND_PAIRWISE_CONV) THEN
   MATCH_ACCEPT_TAC(ADD_IBT_RULE
     (REWRITE_RULE[PAIRWISE; ALL; NONOVERLAPPING_CLAUSES]
-      KECCAK_F1600_X4_AVX2_NOIBT_SUBROUTINE_SAFE)));;
+      KECCAK_F1600_X4_NOIBT_SUBROUTINE_SAFE)));;
diff --git a/proofs/hol_light/x86_64/proofs/nttfrombytes_avx2_asm.ml b/proofs/hol_light/x86_64/proofs/nttfrombytes_avx2_asm.ml
index 9dff0b0ce..91d069df6 100644
--- a/proofs/hol_light/x86_64/proofs/nttfrombytes_avx2_asm.ml
+++ b/proofs/hol_light/x86_64/proofs/nttfrombytes_avx2_asm.ml
@@ -297,16 +297,16 @@ let LENGTH_MLKEM_FROMBYTES_TMC =
   REWRITE_CONV[mlkem_frombytes_tmc] `LENGTH mlkem_frombytes_tmc`
   |> CONV_RULE(RAND_CONV LENGTH_CONV);;
 
-let MLKEM_FROMBYTES_POSTAMBLE_LENGTH = new_definition
-  `MLKEM_FROMBYTES_POSTAMBLE_LENGTH = 1`;;
+let MLKEM_NTTFROMBYTES_POSTAMBLE_LENGTH = new_definition
+  `MLKEM_NTTFROMBYTES_POSTAMBLE_LENGTH = 1`;;
 
-let MLKEM_FROMBYTES_CORE_END = new_definition
-  `MLKEM_FROMBYTES_CORE_END = LENGTH mlkem_frombytes_tmc - MLKEM_FROMBYTES_POSTAMBLE_LENGTH`;;
+let MLKEM_NTTFROMBYTES_CORE_END = new_definition
+  `MLKEM_NTTFROMBYTES_CORE_END = LENGTH mlkem_frombytes_tmc - MLKEM_NTTFROMBYTES_POSTAMBLE_LENGTH`;;
 
 let LENGTH_SIMPLIFY_CONV =
   REWRITE_CONV[LENGTH_MLKEM_FROMBYTES_TMC;
-              MLKEM_FROMBYTES_CORE_END;
-              MLKEM_FROMBYTES_POSTAMBLE_LENGTH] THENC
+              MLKEM_NTTFROMBYTES_CORE_END;
+              MLKEM_NTTFROMBYTES_POSTAMBLE_LENGTH] THENC
   NUM_REDUCE_CONV THENC REWRITE_CONV [ADD_0];;
 
 let avx_order = new_definition
@@ -336,7 +336,7 @@ let AVX_ORDER_UNORDER = prove(
 
 let DIMINDEX_12 = DIMINDEX_CONV `dimindex(:12)`;;
 
-let MLKEM_FROMBYTES_CORRECT = prove(
+let MLKEM_NTTFROMBYTES_CORRECT = prove(
     `!r a (l:(12 word) list) pc.
         aligned 32 a /\
         aligned 32 r /\
@@ -348,7 +348,7 @@ let MLKEM_FROMBYTES_CORRECT = prove(
                   read RIP s = word pc /\
                   C_ARGUMENTS [r; a] s /\
                   read (memory :> bytes(a, 384)) s = num_of_wordlist l)
-             (\s. read RIP s = word (pc + MLKEM_FROMBYTES_CORE_END) /\
+             (\s. read RIP s = word (pc + MLKEM_NTTFROMBYTES_CORE_END) /\
                   (LENGTH l = 256
                    ==> read(memory :> bytes(r, 512)) s =
                        num_of_wordlist (MAP word_zx (unpermute_list l):int16 list)))
@@ -439,7 +439,7 @@ let MLKEM_FROMBYTES_CORRECT = prove(
   REWRITE_TAC[NUM_OF_WORDLIST_EQ] THEN ASM_REWRITE_TAC[] THEN
   REPEAT CONJ_TAC THEN CONV_TAC WORD_BLAST);;
 
-let MLKEM_FROMBYTES_NOIBT_SUBROUTINE_CORRECT = prove(
+let MLKEM_NTTFROMBYTES_NOIBT_SUBROUTINE_CORRECT = prove(
     `!r a (l:(12 word) list) pc.
         aligned 32 a /\
         aligned 32 r /\
@@ -463,12 +463,12 @@ let MLKEM_FROMBYTES_NOIBT_SUBROUTINE_CORRECT = prove(
               MAYCHANGE [RSP] ,, MAYCHANGE [memory :> bytes(r, 512)])`,
   CONV_TAC LENGTH_SIMPLIFY_CONV THEN
   X86_PROMOTE_RETURN_NOSTACK_TAC mlkem_frombytes_tmc
-    (CONV_RULE LENGTH_SIMPLIFY_CONV MLKEM_FROMBYTES_CORRECT));;
+    (CONV_RULE LENGTH_SIMPLIFY_CONV MLKEM_NTTFROMBYTES_CORRECT));;
 
 (* NOTE: This must be kept in sync with the CBMC specification
  * in mlkem/src/native/x86_64/src/arith_native_x86_64.h *)
 
-let MLKEM_FROMBYTES_SUBROUTINE_CORRECT = prove(
+let MLKEM_NTTFROMBYTES_SUBROUTINE_CORRECT = prove(
     `!r a (l:(12 word) list) pc.
         aligned 32 a /\
         aligned 32 r /\
@@ -490,7 +490,7 @@ let MLKEM_FROMBYTES_SUBROUTINE_CORRECT = prove(
                        num_of_wordlist (MAP word_zx (unpermute_list l):int16 list)))
              (MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,,
               MAYCHANGE [RSP] ,, MAYCHANGE [memory :> bytes(r, 512)])`,
-  MATCH_ACCEPT_TAC(ADD_IBT_RULE MLKEM_FROMBYTES_NOIBT_SUBROUTINE_CORRECT));;
+  MATCH_ACCEPT_TAC(ADD_IBT_RULE MLKEM_NTTFROMBYTES_NOIBT_SUBROUTINE_CORRECT));;
 
 (* ------------------------------------------------------------------------- *)
 (* Constant-time and memory safety proof.                                    *)
@@ -502,10 +502,10 @@ needs "mlkem_native/x86_64/proofs/subroutine_signatures.ml";;
 let full_spec,public_vars = mk_safety_spec
     ~keep_maychanges:true
     (assoc "mlkem_frombytes" subroutine_signatures)
-    MLKEM_FROMBYTES_CORRECT
+    MLKEM_NTTFROMBYTES_CORRECT
     mlkem_frombytes_TMC_EXEC;;
 
-let MLKEM_FROMBYTES_SAFE = time prove
+let MLKEM_NTTFROMBYTES_SAFE = time prove
  (`exists f_events.
        forall e r a pc.
            aligned 32 a /\
@@ -520,7 +520,7 @@ let MLKEM_FROMBYTES_SAFE = time prove
                     C_ARGUMENTS [r; a] s /\
                     read events s = e)
                (\s.
-                    read RIP s = word (pc + MLKEM_FROMBYTES_CORE_END) /\
+                    read RIP s = word (pc + MLKEM_NTTFROMBYTES_CORE_END) /\
                     (exists e2.
                          read events s = APPEND e2 e /\
                          e2 = f_events a r pc /\
@@ -536,7 +536,7 @@ let MLKEM_FROMBYTES_SAFE = time prove
   CONV_TAC LENGTH_SIMPLIFY_CONV THEN
   PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars mlkem_frombytes_TMC_EXEC);;
 
-let MLKEM_FROMBYTES_NOIBT_SUBROUTINE_SAFE = time prove
+let MLKEM_NTTFROMBYTES_NOIBT_SUBROUTINE_SAFE = time prove
  (`exists f_events.
        forall e r a pc stackpointer returnaddress.
           aligned 32 a /\
@@ -564,10 +564,10 @@ let MLKEM_FROMBYTES_NOIBT_SUBROUTINE_SAFE = time prove
                            [r,512; stackpointer,8]))
                (\s s'. true)`,
   X86_PROMOTE_RETURN_NOSTACK_TAC mlkem_frombytes_tmc
-    (CONV_RULE LENGTH_SIMPLIFY_CONV MLKEM_FROMBYTES_SAFE) THEN
+    (CONV_RULE LENGTH_SIMPLIFY_CONV MLKEM_NTTFROMBYTES_SAFE) THEN
   DISCHARGE_SAFETY_PROPERTY_TAC);;
 
-let MLKEM_FROMBYTES_SUBROUTINE_SAFE = time prove
+let MLKEM_NTTFROMBYTES_SUBROUTINE_SAFE = time prove
  (`exists f_events.
        forall e r a pc stackpointer returnaddress.
           aligned 32 a /\
@@ -594,4 +594,4 @@ let MLKEM_FROMBYTES_SUBROUTINE_SAFE = time prove
                            [a,384; r,512; stackpointer,8]
                            [r,512; stackpointer,8]))
                (\s s'. true)`,
-  MATCH_ACCEPT_TAC(ADD_IBT_RULE MLKEM_FROMBYTES_NOIBT_SUBROUTINE_SAFE));;
+  MATCH_ACCEPT_TAC(ADD_IBT_RULE MLKEM_NTTFROMBYTES_NOIBT_SUBROUTINE_SAFE));;
diff --git a/proofs/hol_light/x86_64/proofs/ntttobytes_avx2_asm.ml b/proofs/hol_light/x86_64/proofs/ntttobytes_avx2_asm.ml
index 5d77b2b75..3828d2432 100644
--- a/proofs/hol_light/x86_64/proofs/ntttobytes_avx2_asm.ml
+++ b/proofs/hol_light/x86_64/proofs/ntttobytes_avx2_asm.ml
@@ -277,16 +277,16 @@ let LENGTH_MLKEM_TOBYTES_TMC =
   REWRITE_CONV[mlkem_tobytes_tmc] `LENGTH mlkem_tobytes_tmc`
   |> CONV_RULE(RAND_CONV LENGTH_CONV);;
 
-let MLKEM_TOBYTES_POSTAMBLE_LENGTH = new_definition
-  `MLKEM_TOBYTES_POSTAMBLE_LENGTH = 1`;;
+let MLKEM_NTTTOBYTES_POSTAMBLE_LENGTH = new_definition
+  `MLKEM_NTTTOBYTES_POSTAMBLE_LENGTH = 1`;;
 
-let MLKEM_TOBYTES_CORE_END = new_definition
-  `MLKEM_TOBYTES_CORE_END = LENGTH mlkem_tobytes_tmc - MLKEM_TOBYTES_POSTAMBLE_LENGTH`;;
+let MLKEM_NTTTOBYTES_CORE_END = new_definition
+  `MLKEM_NTTTOBYTES_CORE_END = LENGTH mlkem_tobytes_tmc - MLKEM_NTTTOBYTES_POSTAMBLE_LENGTH`;;
 
 let LENGTH_SIMPLIFY_CONV =
   REWRITE_CONV[LENGTH_MLKEM_TOBYTES_TMC;
-              MLKEM_TOBYTES_CORE_END;
-              MLKEM_TOBYTES_POSTAMBLE_LENGTH] THENC
+              MLKEM_NTTTOBYTES_CORE_END;
+              MLKEM_NTTTOBYTES_POSTAMBLE_LENGTH] THENC
   NUM_REDUCE_CONV THENC REWRITE_CONV [ADD_0];;
 
 let avx_order = new_definition
@@ -301,7 +301,7 @@ let permute_list = new_definition
 let BIT_BOUND = BITBLAST_RULE
   `!x:int16. val x < 3329 ==> ~bit 12 x /\ ~bit 13 x /\ ~bit 14 x /\ ~bit 15 x`;;
 
-let MLKEM_TOBYTES_CORRECT = prove(
+let MLKEM_NTTTOBYTES_CORRECT = prove(
   `!r a (l:int16 list) pc.
         aligned 32 a /\
         aligned 32 r /\
@@ -313,7 +313,7 @@ let MLKEM_TOBYTES_CORRECT = prove(
                   read RIP s = word pc /\
                   C_ARGUMENTS [r; a] s /\
                   read (memory :> bytes(a, 512)) s = num_of_wordlist l)
-             (\s. read RIP s = word (pc + MLKEM_TOBYTES_CORE_END) /\
+             (\s. read RIP s = word (pc + MLKEM_NTTTOBYTES_CORE_END) /\
                   (LENGTH l = 256
                    ==> (!i. i < LENGTH l ==> val(EL i l) < 3329)
                    ==> read(memory :> bytes(r, 384)) s =
@@ -396,7 +396,7 @@ let MLKEM_TOBYTES_CORRECT = prove(
   ABBREV_TAC `twae = &2:real` THEN REAL_ARITH_TAC
 );;
 
-let MLKEM_TOBYTES_NOIBT_SUBROUTINE_CORRECT = prove
+let MLKEM_NTTTOBYTES_NOIBT_SUBROUTINE_CORRECT = prove
 (`!r a (l:int16 list) pc.
         aligned 32 a /\
         aligned 32 r /\
@@ -421,12 +421,12 @@ let MLKEM_TOBYTES_NOIBT_SUBROUTINE_CORRECT = prove
                MAYCHANGE [memory :> bytes(r, 384)])`,
   CONV_TAC LENGTH_SIMPLIFY_CONV THEN
   X86_PROMOTE_RETURN_NOSTACK_TAC mlkem_tobytes_tmc
-    (CONV_RULE LENGTH_SIMPLIFY_CONV MLKEM_TOBYTES_CORRECT));;
+    (CONV_RULE LENGTH_SIMPLIFY_CONV MLKEM_NTTTOBYTES_CORRECT));;
 
 (* NOTE: This must be kept in sync with the CBMC specification
  * in mlkem/src/native/x86_64/src/arith_native_x86_64.h *)
 
-let MLKEM_TOBYTES_SUBROUTINE_CORRECT = prove
+let MLKEM_NTTTOBYTES_SUBROUTINE_CORRECT = prove
 (`!r a (l:int16 list) pc.
         aligned 32 a /\
         aligned 32 r /\
@@ -449,7 +449,7 @@ let MLKEM_TOBYTES_SUBROUTINE_CORRECT = prove
                        num_of_wordlist (MAP word_zx (permute_list l):(12 word)list)))
              (MAYCHANGE [RSP] ,, MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,,
                MAYCHANGE [memory :> bytes(r, 384)])`,
-  MATCH_ACCEPT_TAC(ADD_IBT_RULE MLKEM_TOBYTES_NOIBT_SUBROUTINE_CORRECT));;
+  MATCH_ACCEPT_TAC(ADD_IBT_RULE MLKEM_NTTTOBYTES_NOIBT_SUBROUTINE_CORRECT));;
 
 (* ------------------------------------------------------------------------- *)
 (* Constant-time and memory safety proof.                                    *)
@@ -461,10 +461,10 @@ needs "mlkem_native/x86_64/proofs/subroutine_signatures.ml";;
 let full_spec,public_vars = mk_safety_spec
     ~keep_maychanges:true
     (assoc "mlkem_tobytes" subroutine_signatures)
-    MLKEM_TOBYTES_CORRECT
+    MLKEM_NTTTOBYTES_CORRECT
     mlkem_tobytes_TMC_EXEC;;
 
-let MLKEM_TOBYTES_SAFE = time prove
+let MLKEM_NTTTOBYTES_SAFE = time prove
  (`exists f_events.
        forall e r a pc.
            aligned 32 a /\
@@ -479,7 +479,7 @@ let MLKEM_TOBYTES_SAFE = time prove
                     C_ARGUMENTS [r; a] s /\
                     read events s = e)
                (\s.
-                    read RIP s = word (pc + MLKEM_TOBYTES_CORE_END) /\
+                    read RIP s = word (pc + MLKEM_NTTTOBYTES_CORE_END) /\
                     (exists e2.
                          read events s = APPEND e2 e /\
                          e2 = f_events a r pc /\
@@ -495,7 +495,7 @@ let MLKEM_TOBYTES_SAFE = time prove
   CONV_TAC LENGTH_SIMPLIFY_CONV THEN
   PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars mlkem_tobytes_TMC_EXEC);;
 
-let MLKEM_TOBYTES_NOIBT_SUBROUTINE_SAFE = time prove
+let MLKEM_NTTTOBYTES_NOIBT_SUBROUTINE_SAFE = time prove
  (`exists f_events.
        forall e r a pc stackpointer returnaddress.
           aligned 32 a /\
@@ -523,10 +523,10 @@ let MLKEM_TOBYTES_NOIBT_SUBROUTINE_SAFE = time prove
                            [r,384; stackpointer,8]))
                (\s s'. true)`,
   X86_PROMOTE_RETURN_NOSTACK_TAC mlkem_tobytes_tmc
-    (CONV_RULE LENGTH_SIMPLIFY_CONV MLKEM_TOBYTES_SAFE) THEN
+    (CONV_RULE LENGTH_SIMPLIFY_CONV MLKEM_NTTTOBYTES_SAFE) THEN
   DISCHARGE_SAFETY_PROPERTY_TAC);;
 
-let MLKEM_TOBYTES_SUBROUTINE_SAFE = time prove
+let MLKEM_NTTTOBYTES_SUBROUTINE_SAFE = time prove
  (`exists f_events.
        forall e r a pc stackpointer returnaddress.
           aligned 32 a /\
@@ -553,4 +553,4 @@ let MLKEM_TOBYTES_SUBROUTINE_SAFE = time prove
                            [a,512; r,384; stackpointer,8]
                            [r,384; stackpointer,8]))
                (\s s'. true)`,
-  MATCH_ACCEPT_TAC(ADD_IBT_RULE MLKEM_TOBYTES_NOIBT_SUBROUTINE_SAFE));;
+  MATCH_ACCEPT_TAC(ADD_IBT_RULE MLKEM_NTTTOBYTES_NOIBT_SUBROUTINE_SAFE));;
diff --git a/proofs/hol_light/x86_64/proofs/nttunpack_avx2_asm.ml b/proofs/hol_light/x86_64/proofs/nttunpack_avx2_asm.ml
index 06ce5cdf7..9e1c9c8db 100644
--- a/proofs/hol_light/x86_64/proofs/nttunpack_avx2_asm.ml
+++ b/proofs/hol_light/x86_64/proofs/nttunpack_avx2_asm.ml
@@ -272,16 +272,16 @@ let LENGTH_MLKEM_UNPACK_TMC =
   REWRITE_CONV[mlkem_unpack_tmc] `LENGTH mlkem_unpack_tmc`
   |> CONV_RULE(RAND_CONV LENGTH_CONV);;
 
-let MLKEM_UNPACK_POSTAMBLE_LENGTH = new_definition
-  `MLKEM_UNPACK_POSTAMBLE_LENGTH = 1`;;
+let MLKEM_NTTUNPACK_POSTAMBLE_LENGTH = new_definition
+  `MLKEM_NTTUNPACK_POSTAMBLE_LENGTH = 1`;;
 
-let MLKEM_UNPACK_CORE_END = new_definition
-  `MLKEM_UNPACK_CORE_END = LENGTH mlkem_unpack_tmc - MLKEM_UNPACK_POSTAMBLE_LENGTH`;;
+let MLKEM_NTTUNPACK_CORE_END = new_definition
+  `MLKEM_NTTUNPACK_CORE_END = LENGTH mlkem_unpack_tmc - MLKEM_NTTUNPACK_POSTAMBLE_LENGTH`;;
 
 let LENGTH_SIMPLIFY_CONV =
   REWRITE_CONV[LENGTH_MLKEM_UNPACK_TMC;
-              MLKEM_UNPACK_CORE_END;
-              MLKEM_UNPACK_POSTAMBLE_LENGTH] THENC
+              MLKEM_NTTUNPACK_CORE_END;
+              MLKEM_NTTUNPACK_POSTAMBLE_LENGTH] THENC
   NUM_REDUCE_CONV THENC REWRITE_CONV [ADD_0];;
 
 let avx_order = new_definition
@@ -302,7 +302,7 @@ let avx_unorder = new_definition
 let unpermute_list = new_definition
   `unpermute_list l = list_of_seq (\i. EL (avx_unorder i) l) 256`;;
 
-let MLKEM_UNPACK_CORRECT = prove(
+let MLKEM_NTTUNPACK_CORRECT = prove(
     `!a (l:int16 list) pc.
         aligned 32 a /\
         nonoverlapping (word pc, LENGTH mlkem_unpack_tmc) (a, 512)
@@ -311,7 +311,7 @@ let MLKEM_UNPACK_CORRECT = prove(
                   read RIP s = word pc /\
                   C_ARGUMENTS [a] s /\
                   read (memory :> bytes(a, 512)) s = num_of_wordlist l)
-             (\s. read RIP s = word (pc + MLKEM_UNPACK_CORE_END) /\
+             (\s. read RIP s = word (pc + MLKEM_NTTUNPACK_CORE_END) /\
                   (LENGTH l = 256
                    ==> read(memory :> bytes(a, 512)) s =
                        num_of_wordlist (unpermute_list l)))
@@ -380,7 +380,7 @@ let MLKEM_UNPACK_CORRECT = prove(
   ABBREV_TAC `twae = &2:real` THEN REAL_ARITH_TAC);;
 
 
-let MLKEM_UNPACK_NOIBT_SUBROUTINE_CORRECT = prove(
+let MLKEM_NTTUNPACK_NOIBT_SUBROUTINE_CORRECT = prove(
     `!a (l:int16 list) pc.
         aligned 32 a /\
         nonoverlapping (word pc, LENGTH mlkem_unpack_tmc) (a, 512) /\
@@ -401,12 +401,12 @@ let MLKEM_UNPACK_NOIBT_SUBROUTINE_CORRECT = prove(
               MAYCHANGE [memory :> bytes(a, 512)])`, 
   CONV_TAC LENGTH_SIMPLIFY_CONV THEN
   X86_PROMOTE_RETURN_NOSTACK_TAC mlkem_unpack_tmc
-    (CONV_RULE LENGTH_SIMPLIFY_CONV MLKEM_UNPACK_CORRECT));;
+    (CONV_RULE LENGTH_SIMPLIFY_CONV MLKEM_NTTUNPACK_CORRECT));;
 
 (* NOTE: This must be kept in sync with the CBMC specification
  * in mlkem/src/native/x86_64/src/arith_native_x86_64.h *)
 
-let MLKEM_UNPACK_SUBROUTINE_CORRECT = prove(
+let MLKEM_NTTUNPACK_SUBROUTINE_CORRECT = prove(
     `!a (l:int16 list) pc.
         aligned 32 a /\
         nonoverlapping (word pc, LENGTH mlkem_unpack_mc) (a, 512) /\
@@ -425,7 +425,7 @@ let MLKEM_UNPACK_SUBROUTINE_CORRECT = prove(
                        num_of_wordlist (unpermute_list l)))
              (MAYCHANGE [RSP] ,, MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,,
               MAYCHANGE [memory :> bytes(a, 512)])`, 
-  MATCH_ACCEPT_TAC(ADD_IBT_RULE MLKEM_UNPACK_NOIBT_SUBROUTINE_CORRECT));;
+  MATCH_ACCEPT_TAC(ADD_IBT_RULE MLKEM_NTTUNPACK_NOIBT_SUBROUTINE_CORRECT));;
 
 (* ------------------------------------------------------------------------- *)
 (* Constant-time and memory safety proof.                                    *)
@@ -437,10 +437,10 @@ needs "mlkem_native/x86_64/proofs/subroutine_signatures.ml";;
 let full_spec,public_vars = mk_safety_spec
     ~keep_maychanges:true
     (assoc "mlkem_unpack" subroutine_signatures)
-    MLKEM_UNPACK_CORRECT
+    MLKEM_NTTUNPACK_CORRECT
     mlkem_unpack_TMC_EXEC;;
 
-let MLKEM_UNPACK_SAFE = time prove
+let MLKEM_NTTUNPACK_SAFE = time prove
  (`exists f_events.
        forall e a pc.
            aligned 32 a /\ nonoverlapping (word pc,LENGTH mlkem_unpack_tmc) (a,512)
@@ -451,7 +451,7 @@ let MLKEM_UNPACK_SAFE = time prove
                     C_ARGUMENTS [a] s /\
                     read events s = e)
                (\s.
-                    read RIP s = word (pc + MLKEM_UNPACK_CORE_END) /\
+                    read RIP s = word (pc + MLKEM_NTTUNPACK_CORE_END) /\
                     (exists e2.
                          read events s = APPEND e2 e /\
                          e2 = f_events a pc /\
@@ -466,7 +466,7 @@ let MLKEM_UNPACK_SAFE = time prove
   CONV_TAC LENGTH_SIMPLIFY_CONV THEN
   PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars mlkem_unpack_TMC_EXEC);;
 
-let MLKEM_UNPACK_NOIBT_SUBROUTINE_SAFE = time prove
+let MLKEM_NTTUNPACK_NOIBT_SUBROUTINE_SAFE = time prove
  (`exists f_events.
        forall e a pc stackpointer returnaddress.
           aligned 32 a /\
@@ -489,10 +489,10 @@ let MLKEM_UNPACK_NOIBT_SUBROUTINE_SAFE = time prove
                                                [a,512; stackpointer,8]))
                (\s s'. true)`,
   X86_PROMOTE_RETURN_NOSTACK_TAC mlkem_unpack_tmc
-    (CONV_RULE LENGTH_SIMPLIFY_CONV MLKEM_UNPACK_SAFE) THEN
+    (CONV_RULE LENGTH_SIMPLIFY_CONV MLKEM_NTTUNPACK_SAFE) THEN
   DISCHARGE_SAFETY_PROPERTY_TAC);;
 
-let MLKEM_UNPACK_SUBROUTINE_SAFE = time prove
+let MLKEM_NTTUNPACK_SUBROUTINE_SAFE = time prove
  (`exists f_events.
        forall e a pc stackpointer returnaddress.
           aligned 32 a /\
@@ -514,4 +514,4 @@ let MLKEM_UNPACK_SUBROUTINE_SAFE = time prove
                          memaccess_inbounds e2 [a,512; stackpointer,8]
                                                [a,512; stackpointer,8]))
                (\s s'. true)`,
-  MATCH_ACCEPT_TAC(ADD_IBT_RULE MLKEM_UNPACK_NOIBT_SUBROUTINE_SAFE));;
+  MATCH_ACCEPT_TAC(ADD_IBT_RULE MLKEM_NTTUNPACK_NOIBT_SUBROUTINE_SAFE));;
diff --git a/proofs/hol_light/x86_64/proofs/poly_mulcache_compute_avx2_asm.ml b/proofs/hol_light/x86_64/proofs/poly_mulcache_compute_avx2_asm.ml
index 2d20b700b..be401ae22 100644
--- a/proofs/hol_light/x86_64/proofs/poly_mulcache_compute_avx2_asm.ml
+++ b/proofs/hol_light/x86_64/proofs/poly_mulcache_compute_avx2_asm.ml
@@ -112,7 +112,7 @@ let mlkem_mulcache_compute_mc = define_assert_from_elf "mlkem_mulcache_compute_m
 (*** BYTECODE END ***)
 
 let mlkem_mulcache_compute_tmc = define_trimmed "mlkem_mulcache_compute_tmc" mlkem_mulcache_compute_mc;;
-let MLKEM_MULCACHE_COMPUTE_TMC_EXEC = X86_MK_CORE_EXEC_RULE mlkem_mulcache_compute_tmc;;
+let MLKEM_POLY_MULCACHE_COMPUTE_TMC_EXEC = X86_MK_CORE_EXEC_RULE mlkem_mulcache_compute_tmc;;
 
 let avx2_mulcache = define
  `avx2_mulcache f k =
@@ -130,20 +130,20 @@ let LENGTH_QDATA_FULL =
   REWRITE_CONV[qdata_full] `LENGTH qdata_full`
   |> CONV_RULE(RAND_CONV LENGTH_CONV);;
 
-let MLKEM_MULCACHE_COMPUTE_POSTAMBLE_LENGTH = new_definition
-  `MLKEM_MULCACHE_COMPUTE_POSTAMBLE_LENGTH = 1`;;
+let MLKEM_POLY_MULCACHE_COMPUTE_POSTAMBLE_LENGTH = new_definition
+  `MLKEM_POLY_MULCACHE_COMPUTE_POSTAMBLE_LENGTH = 1`;;
 
-let MLKEM_MULCACHE_COMPUTE_CORE_END = new_definition
-  `MLKEM_MULCACHE_COMPUTE_CORE_END = LENGTH mlkem_mulcache_compute_tmc - MLKEM_MULCACHE_COMPUTE_POSTAMBLE_LENGTH`;;
+let MLKEM_POLY_MULCACHE_COMPUTE_CORE_END = new_definition
+  `MLKEM_POLY_MULCACHE_COMPUTE_CORE_END = LENGTH mlkem_mulcache_compute_tmc - MLKEM_POLY_MULCACHE_COMPUTE_POSTAMBLE_LENGTH`;;
 
 let LENGTH_SIMPLIFY_CONV =
   REWRITE_CONV[LENGTH_MLKEM_MULCACHE_COMPUTE_TMC;
               LENGTH_QDATA_FULL;
-              MLKEM_MULCACHE_COMPUTE_CORE_END;
-              MLKEM_MULCACHE_COMPUTE_POSTAMBLE_LENGTH] THENC
+              MLKEM_POLY_MULCACHE_COMPUTE_CORE_END;
+              MLKEM_POLY_MULCACHE_COMPUTE_POSTAMBLE_LENGTH] THENC
   NUM_REDUCE_CONV THENC REWRITE_CONV [ADD_0];;
 
-let MLKEM_MULCACHE_COMPUTE_CORRECT = prove(
+let MLKEM_POLY_MULCACHE_COMPUTE_CORRECT = prove(
  `!r a zetas (zetas_list:int16 list) x pc.
     aligned 32 r /\
     aligned 32 a /\
@@ -157,7 +157,7 @@ let MLKEM_MULCACHE_COMPUTE_CORRECT = prove(
               C_ARGUMENTS [r; a; zetas] s /\
               wordlist_from_memory(zetas, 624) s = MAP (iword: int -> 16 word) qdata_full /\
               (!i. i < 256 ==> read(memory :> bytes16(word_add a (word(2 * i)))) s = x i))
-          (\s. read RIP s = word(pc + MLKEM_MULCACHE_COMPUTE_CORE_END) /\
+          (\s. read RIP s = word(pc + MLKEM_POLY_MULCACHE_COMPUTE_CORE_END) /\
                !i. i < 128
                    ==> let zi =
                       read(memory :> bytes16(word_add r (word(2 * i)))) s in
@@ -180,7 +180,7 @@ let MLKEM_MULCACHE_COMPUTE_CORRECT = prove(
   CONV_TAC NUM_REDUCE_CONV THEN
   REPEAT STRIP_TAC THEN
 
-  REWRITE_TAC [SOME_FLAGS; fst MLKEM_MULCACHE_COMPUTE_TMC_EXEC] THEN
+  REWRITE_TAC [SOME_FLAGS; fst MLKEM_POLY_MULCACHE_COMPUTE_TMC_EXEC] THEN
 
   GHOST_INTRO_TAC `init_ymm0:int256` `read YMM0` THEN
 
@@ -203,7 +203,7 @@ let MLKEM_MULCACHE_COMPUTE_CORRECT = prove(
   DISCARD_MATCHING_ASSUMPTIONS [`read (memory :> bytes16 a) s = x`] THEN
   CONV_TAC(LAND_CONV WORD_REDUCE_CONV) THEN STRIP_TAC THEN
 
-  MAP_EVERY (fun n -> X86_STEPS_TAC MLKEM_MULCACHE_COMPUTE_TMC_EXEC [n] THEN
+  MAP_EVERY (fun n -> X86_STEPS_TAC MLKEM_POLY_MULCACHE_COMPUTE_TMC_EXEC [n] THEN
                       SIMD_SIMPLIFY_TAC[ntt_montmul_alt])
         (1--59) THEN
   ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN
@@ -259,7 +259,7 @@ let MLKEM_MULCACHE_COMPUTE_CORRECT = prove(
     CONV_TAC INT_REDUCE_CONV])
 );;
 
-let MLKEM_MULCACHE_COMPUTE_NOIBT_SUBROUTINE_CORRECT  = prove(
+let MLKEM_POLY_MULCACHE_COMPUTE_NOIBT_SUBROUTINE_CORRECT  = prove(
  `!r a zetas (zetas_list:int16 list) x pc stackpointer returnaddress.
     aligned 32 r /\
     aligned 32 a /\
@@ -289,12 +289,12 @@ let MLKEM_MULCACHE_COMPUTE_NOIBT_SUBROUTINE_CORRECT  = prove(
   let TWEAK_CONV = ONCE_DEPTH_CONV WORDLIST_FROM_MEMORY_CONV in
   CONV_TAC TWEAK_CONV THEN
   X86_PROMOTE_RETURN_NOSTACK_TAC mlkem_mulcache_compute_tmc
-    (CONV_RULE TWEAK_CONV (CONV_RULE LENGTH_SIMPLIFY_CONV MLKEM_MULCACHE_COMPUTE_CORRECT)));;
+    (CONV_RULE TWEAK_CONV (CONV_RULE LENGTH_SIMPLIFY_CONV MLKEM_POLY_MULCACHE_COMPUTE_CORRECT)));;
 
 (* NOTE: This must be kept in sync with the CBMC specification
  * in mlkem/src/native/x86_64/src/arith_native_x86_64.h *)
 
-let MLKEM_MULCACHE_COMPUTE_SUBROUTINE_CORRECT = prove(
+let MLKEM_POLY_MULCACHE_COMPUTE_SUBROUTINE_CORRECT = prove(
  `!r a zetas (zetas_list:int16 list) x pc stackpointer returnaddress.
     aligned 32 r /\
     aligned 32 a /\
@@ -323,7 +323,7 @@ let MLKEM_MULCACHE_COMPUTE_SUBROUTINE_CORRECT = prove(
   let TWEAK_CONV = ONCE_DEPTH_CONV WORDLIST_FROM_MEMORY_CONV in
   CONV_TAC TWEAK_CONV THEN
   MATCH_ACCEPT_TAC(ADD_IBT_RULE
-  (CONV_RULE TWEAK_CONV MLKEM_MULCACHE_COMPUTE_NOIBT_SUBROUTINE_CORRECT)));;
+  (CONV_RULE TWEAK_CONV MLKEM_POLY_MULCACHE_COMPUTE_NOIBT_SUBROUTINE_CORRECT)));;
 
 (* ------------------------------------------------------------------------- *)
 (* Constant-time and memory safety proof.                                    *)
@@ -335,8 +335,8 @@ needs "mlkem_native/x86_64/proofs/subroutine_signatures.ml";;
 let full_spec,public_vars = mk_safety_spec
     ~keep_maychanges:true
     (assoc "mlkem_mulcache_compute" subroutine_signatures)
-    MLKEM_MULCACHE_COMPUTE_CORRECT
-    MLKEM_MULCACHE_COMPUTE_TMC_EXEC;;
+    MLKEM_POLY_MULCACHE_COMPUTE_CORRECT
+    MLKEM_POLY_MULCACHE_COMPUTE_TMC_EXEC;;
 (* full_spec mixes numeric and symbolic buffer sizes: mk_safety_spec computes
    624*2=1248 from the subroutine signature for memaccess_inbounds, but copies
    `LENGTH qdata_full * 2` verbatim from the correctness theorem's nonoverlapping
@@ -344,7 +344,7 @@ let full_spec,public_vars = mk_safety_spec
    hand-written goal after LENGTH_SIMPLIFY_CONV. *)
 let full_spec = LENGTH_SIMPLIFY_CONV full_spec |> concl |> rhs;;
 
-let MLKEM_MULCACHE_COMPUTE_SAFE = time prove
+let MLKEM_POLY_MULCACHE_COMPUTE_SAFE = time prove
  (`exists f_events.
        forall e r a zetas pc.
            aligned 32 r /\
@@ -361,7 +361,7 @@ let MLKEM_MULCACHE_COMPUTE_SAFE = time prove
                     C_ARGUMENTS [r; a; zetas] s /\
                     read events s = e)
                (\s.
-                    read RIP s = word (pc + MLKEM_MULCACHE_COMPUTE_CORE_END) /\
+                    read RIP s = word (pc + MLKEM_POLY_MULCACHE_COMPUTE_CORE_END) /\
                     (exists e2.
                          read events s = APPEND e2 e /\
                          e2 = f_events a zetas r pc /\
@@ -376,9 +376,9 @@ let MLKEM_MULCACHE_COMPUTE_SAFE = time prove
   CONV_TAC LENGTH_SIMPLIFY_CONV THEN
   ASSERT_CONCL_TAC full_spec THEN
   PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars
-    MLKEM_MULCACHE_COMPUTE_TMC_EXEC);;
+    MLKEM_POLY_MULCACHE_COMPUTE_TMC_EXEC);;
 
-let MLKEM_MULCACHE_COMPUTE_NOIBT_SUBROUTINE_SAFE = time prove
+let MLKEM_POLY_MULCACHE_COMPUTE_NOIBT_SUBROUTINE_SAFE = time prove
  (`exists f_events.
        forall e r a zetas pc stackpointer returnaddress.
           aligned 32 r /\
@@ -409,13 +409,13 @@ let MLKEM_MULCACHE_COMPUTE_NOIBT_SUBROUTINE_SAFE = time prove
   X86_PROMOTE_RETURN_NOSTACK_TAC mlkem_mulcache_compute_tmc
     (CONV_RULE
       (REWRITE_CONV[LENGTH_MLKEM_MULCACHE_COMPUTE_TMC;
-                    MLKEM_MULCACHE_COMPUTE_CORE_END;
-                    MLKEM_MULCACHE_COMPUTE_POSTAMBLE_LENGTH] THENC
+                    MLKEM_POLY_MULCACHE_COMPUTE_CORE_END;
+                    MLKEM_POLY_MULCACHE_COMPUTE_POSTAMBLE_LENGTH] THENC
        NUM_REDUCE_CONV THENC REWRITE_CONV [ADD_0])
-      MLKEM_MULCACHE_COMPUTE_SAFE) THEN
+      MLKEM_POLY_MULCACHE_COMPUTE_SAFE) THEN
   DISCHARGE_SAFETY_PROPERTY_TAC);;
 
-let MLKEM_MULCACHE_COMPUTE_SUBROUTINE_SAFE = time prove
+let MLKEM_POLY_MULCACHE_COMPUTE_SUBROUTINE_SAFE = time prove
  (`exists f_events.
        forall e r a zetas pc stackpointer returnaddress.
           aligned 32 r /\
@@ -443,4 +443,4 @@ let MLKEM_MULCACHE_COMPUTE_SUBROUTINE_SAFE = time prove
                             r,256; stackpointer,8]
                            [r,256; stackpointer,8]))
                (\s s'. true)`,
-  MATCH_ACCEPT_TAC(ADD_IBT_RULE MLKEM_MULCACHE_COMPUTE_NOIBT_SUBROUTINE_SAFE));;
+  MATCH_ACCEPT_TAC(ADD_IBT_RULE MLKEM_POLY_MULCACHE_COMPUTE_NOIBT_SUBROUTINE_SAFE));;
diff --git a/proofs/hol_light/x86_64/proofs/polyvec_basemul_acc_montgomery_cached_k2_avx2_asm.ml b/proofs/hol_light/x86_64/proofs/polyvec_basemul_acc_montgomery_cached_k2_avx2_asm.ml
index cb2ab478e..fa9c92594 100644
--- a/proofs/hol_light/x86_64/proofs/polyvec_basemul_acc_montgomery_cached_k2_avx2_asm.ml
+++ b/proofs/hol_light/x86_64/proofs/polyvec_basemul_acc_montgomery_cached_k2_avx2_asm.ml
@@ -808,16 +808,16 @@ let LENGTH_MLKEM_BASEMUL_K2_TMC =
   REWRITE_CONV[mlkem_basemul_k2_tmc] `LENGTH mlkem_basemul_k2_tmc`
   |> CONV_RULE(RAND_CONV LENGTH_CONV);;
 
-let MLKEM_BASEMUL_K2_POSTAMBLE_LENGTH = new_definition
-  `MLKEM_BASEMUL_K2_POSTAMBLE_LENGTH = 1`;;
+let MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K2_POSTAMBLE_LENGTH = new_definition
+  `MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K2_POSTAMBLE_LENGTH = 1`;;
 
-let MLKEM_BASEMUL_K2_CORE_END = new_definition
-  `MLKEM_BASEMUL_K2_CORE_END = LENGTH mlkem_basemul_k2_tmc - MLKEM_BASEMUL_K2_POSTAMBLE_LENGTH`;;
+let MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K2_CORE_END = new_definition
+  `MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K2_CORE_END = LENGTH mlkem_basemul_k2_tmc - MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K2_POSTAMBLE_LENGTH`;;
 
 let LENGTH_SIMPLIFY_CONV =
   REWRITE_CONV[LENGTH_MLKEM_BASEMUL_K2_TMC;
-              MLKEM_BASEMUL_K2_CORE_END;
-              MLKEM_BASEMUL_K2_POSTAMBLE_LENGTH] THENC
+              MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K2_CORE_END;
+              MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K2_POSTAMBLE_LENGTH] THENC
   NUM_REDUCE_CONV THENC REWRITE_CONV [ADD_0];;
 
 (* Enable simplification of word_subwords by default.
@@ -868,7 +868,7 @@ let pmulaccred1 = define
                (a1: int) (b1 : int) (c1 : int) (d1 : int) (dz1 : int) =
      (&(inverse_mod 3329 65536) * pmulacc1 a0 b0 c0 d0 dz0 a1 b1 c1 d1 dz1) rem &3329`;;
 
-let MLKEM_BASEMUL_K2_CORRECT = prove(
+let MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K2_CORRECT = prove(
   `!src1 src2 src2t dst a0 b0 c0 d0 dz0 a1 b1 c1 d1 dz1 pc.
         aligned 32 src1 /\
         aligned 32 src2 /\
@@ -911,7 +911,7 @@ let MLKEM_BASEMUL_K2_CORRECT = prove(
                    (!i. i < 16 ==> !j. j < 8
                         ==> read(memory :> bytes16
                              (word_add src2t (word (256 + 32*j + 2*i)))) s = dz1 i j))
-              (\s. read RIP s = word (pc + MLKEM_BASEMUL_K2_CORE_END) /\
+              (\s. read RIP s = word (pc + MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K2_CORE_END) /\
                    (!i. i < 16 ==> !j. j < 4
                         ==> (let j' = 2*j in
                               (abs(ival(a0 i j')) <= &2 pow 12  /\
@@ -1010,7 +1010,7 @@ let MLKEM_BASEMUL_K2_CORRECT = prove(
   CONV_TAC INT_RING
 );;
 
-let MLKEM_BASEMUL_K2_NOIBT_SUBROUTINE_CORRECT = prove(
+let MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K2_NOIBT_SUBROUTINE_CORRECT = prove(
   `!src1 src2 src2t dst a0 b0 c0 d0 dz0 a1 b1 c1 d1 dz1 pc stackpointer returnaddress.
         aligned 32 src1 /\
         aligned 32 src2 /\
@@ -1098,12 +1098,12 @@ let MLKEM_BASEMUL_K2_NOIBT_SUBROUTINE_CORRECT = prove(
                MAYCHANGE [memory :> bytes(dst, 512)])`,
   CONV_TAC LENGTH_SIMPLIFY_CONV THEN
   X86_PROMOTE_RETURN_NOSTACK_TAC mlkem_basemul_k2_tmc
-    (CONV_RULE LENGTH_SIMPLIFY_CONV MLKEM_BASEMUL_K2_CORRECT));;
+    (CONV_RULE LENGTH_SIMPLIFY_CONV MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K2_CORRECT));;
 
 (* NOTE: This must be kept in sync with the CBMC specification
  * in mlkem/src/native/x86_64/src/arith_native_x86_64.h *)
 
-let MLKEM_BASEMUL_K2_SUBROUTINE_CORRECT = prove(
+let MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K2_SUBROUTINE_CORRECT = prove(
   `!src1 src2 src2t dst a0 b0 c0 d0 dz0 a1 b1 c1 d1 dz1 pc stackpointer returnaddress.
         aligned 32 src1 /\
         aligned 32 src2 /\
@@ -1189,7 +1189,7 @@ let MLKEM_BASEMUL_K2_SUBROUTINE_CORRECT = prove(
                             ) (mod &3329)))
               (MAYCHANGE [RSP] ,, MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,,
                MAYCHANGE [memory :> bytes(dst, 512)])`,
-  MATCH_ACCEPT_TAC(ADD_IBT_RULE MLKEM_BASEMUL_K2_NOIBT_SUBROUTINE_CORRECT));;
+  MATCH_ACCEPT_TAC(ADD_IBT_RULE MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K2_NOIBT_SUBROUTINE_CORRECT));;
 
 (* ------------------------------------------------------------------------- *)
 (* Constant-time and memory safety proof.                                    *)
@@ -1201,10 +1201,10 @@ needs "mlkem_native/x86_64/proofs/subroutine_signatures.ml";;
 let full_spec,public_vars = mk_safety_spec
     ~keep_maychanges:true
     (assoc "mlkem_basemul_k2" subroutine_signatures)
-    MLKEM_BASEMUL_K2_CORRECT
+    MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K2_CORRECT
     mlkem_basemul_k2_tmc_EXEC;;
 
-let MLKEM_BASEMUL_K2_SAFE = time prove
+let MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K2_SAFE = time prove
  (`exists f_events.
        forall e src1 src2 src2t dst pc.
            aligned 32 src1 /\
@@ -1221,7 +1221,7 @@ let MLKEM_BASEMUL_K2_SAFE = time prove
                     C_ARGUMENTS [dst; src1; src2; src2t] s /\
                     read events s = e)
                (\s.
-                    read RIP s = word (pc + MLKEM_BASEMUL_K2_CORE_END) /\
+                    read RIP s = word (pc + MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K2_CORE_END) /\
                     (exists e2.
                          read events s = APPEND e2 e /\
                          e2 = f_events src1 src2 src2t dst pc /\
@@ -1239,7 +1239,7 @@ let MLKEM_BASEMUL_K2_SAFE = time prove
   CONV_TAC LENGTH_SIMPLIFY_CONV THEN
   PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars mlkem_basemul_k2_tmc_EXEC);;
 
-let MLKEM_BASEMUL_K2_NOIBT_SUBROUTINE_SAFE = time prove
+let MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K2_NOIBT_SUBROUTINE_SAFE = time prove
  (`exists f_events.
        forall e src1 src2 src2t dst pc stackpointer returnaddress.
           aligned 32 src1 /\
@@ -1269,10 +1269,10 @@ let MLKEM_BASEMUL_K2_NOIBT_SUBROUTINE_SAFE = time prove
                            [dst,512; stackpointer,8]))
                (\s s'. true)`,
   X86_PROMOTE_RETURN_NOSTACK_TAC mlkem_basemul_k2_tmc
-    (CONV_RULE LENGTH_SIMPLIFY_CONV MLKEM_BASEMUL_K2_SAFE) THEN
+    (CONV_RULE LENGTH_SIMPLIFY_CONV MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K2_SAFE) THEN
   DISCHARGE_SAFETY_PROPERTY_TAC);;
 
-let MLKEM_BASEMUL_K2_SUBROUTINE_SAFE = time prove
+let MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K2_SUBROUTINE_SAFE = time prove
  (`exists f_events.
        forall e src1 src2 src2t dst pc stackpointer returnaddress.
           aligned 32 src1 /\
@@ -1301,4 +1301,4 @@ let MLKEM_BASEMUL_K2_SUBROUTINE_SAFE = time prove
                             dst,512; stackpointer,8]
                            [dst,512; stackpointer,8]))
                (\s s'. true)`,
-  MATCH_ACCEPT_TAC(ADD_IBT_RULE MLKEM_BASEMUL_K2_NOIBT_SUBROUTINE_SAFE));;
+  MATCH_ACCEPT_TAC(ADD_IBT_RULE MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K2_NOIBT_SUBROUTINE_SAFE));;
diff --git a/proofs/hol_light/x86_64/proofs/polyvec_basemul_acc_montgomery_cached_k3_avx2_asm.ml b/proofs/hol_light/x86_64/proofs/polyvec_basemul_acc_montgomery_cached_k3_avx2_asm.ml
index 8a8eed1c1..077c6109b 100644
--- a/proofs/hol_light/x86_64/proofs/polyvec_basemul_acc_montgomery_cached_k3_avx2_asm.ml
+++ b/proofs/hol_light/x86_64/proofs/polyvec_basemul_acc_montgomery_cached_k3_avx2_asm.ml
@@ -1222,16 +1222,16 @@ let LENGTH_MLKEM_BASEMUL_K3_TMC =
   REWRITE_CONV[mlkem_basemul_k3_tmc] `LENGTH mlkem_basemul_k3_tmc`
   |> CONV_RULE(RAND_CONV LENGTH_CONV);;
 
-let MLKEM_BASEMUL_K3_POSTAMBLE_LENGTH = new_definition
-  `MLKEM_BASEMUL_K3_POSTAMBLE_LENGTH = 1`;;
+let MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K3_POSTAMBLE_LENGTH = new_definition
+  `MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K3_POSTAMBLE_LENGTH = 1`;;
 
-let MLKEM_BASEMUL_K3_CORE_END = new_definition
-  `MLKEM_BASEMUL_K3_CORE_END = LENGTH mlkem_basemul_k3_tmc - MLKEM_BASEMUL_K3_POSTAMBLE_LENGTH`;;
+let MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K3_CORE_END = new_definition
+  `MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K3_CORE_END = LENGTH mlkem_basemul_k3_tmc - MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K3_POSTAMBLE_LENGTH`;;
 
 let LENGTH_SIMPLIFY_CONV =
   REWRITE_CONV[LENGTH_MLKEM_BASEMUL_K3_TMC;
-              MLKEM_BASEMUL_K3_CORE_END;
-              MLKEM_BASEMUL_K3_POSTAMBLE_LENGTH] THENC
+              MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K3_CORE_END;
+              MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K3_POSTAMBLE_LENGTH] THENC
   NUM_REDUCE_CONV THENC REWRITE_CONV [ADD_0];;
 
 (* Enable simplification of word_subwords by default.
@@ -1288,7 +1288,7 @@ let pmulaccred1_k3 = define
                   (a2: int) (b2 : int) (c2 : int) (d2 : int) (dz2 : int) =
      (&(inverse_mod 3329 65536) * pmulacc1_k3 a0 b0 c0 d0 dz0 a1 b1 c1 d1 dz1 a2 b2 c2 d2 dz2) rem &3329`;;
 
-let MLKEM_BASEMUL_K3_CORRECT = prove(
+let MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K3_CORRECT = prove(
   `!src1 src2 src2t dst a0 b0 c0 d0 dz0 a1 b1 c1 d1 dz1 a2 b2 c2 d2 dz2 pc.
         aligned 32 src1 /\
         aligned 32 src2 /\
@@ -1347,7 +1347,7 @@ let MLKEM_BASEMUL_K3_CORRECT = prove(
                    (!i. i < 16 ==> !j. j < 8
                         ==> read(memory :> bytes16
                              (word_add src2t (word (512 + 32*j + 2*i)))) s = dz2 i j))
-              (\s. read RIP s = word (pc + MLKEM_BASEMUL_K3_CORE_END) /\
+              (\s. read RIP s = word (pc + MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K3_CORE_END) /\
                    (!i. i < 16 ==> !j. j < 4
                         ==> (let j' = 2*j in
                               (abs(ival(a0 i j')) <= &2 pow 12  /\
@@ -1455,7 +1455,7 @@ let MLKEM_BASEMUL_K3_CORRECT = prove(
   CONV_TAC INT_RING
 );;
 
-let MLKEM_BASEMUL_K3_NOIBT_SUBROUTINE_CORRECT = prove(
+let MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K3_NOIBT_SUBROUTINE_CORRECT = prove(
   `!src1 src2 src2t dst a0 b0 c0 d0 dz0 a1 b1 c1 d1 dz1 a2 b2 c2 d2 dz2 pc stackpointer returnaddress.
         aligned 32 src1 /\
         aligned 32 src2 /\
@@ -1568,12 +1568,12 @@ let MLKEM_BASEMUL_K3_NOIBT_SUBROUTINE_CORRECT = prove(
                MAYCHANGE [memory :> bytes(dst, 512)])`,
   CONV_TAC LENGTH_SIMPLIFY_CONV THEN
   X86_PROMOTE_RETURN_NOSTACK_TAC mlkem_basemul_k3_tmc
-    (CONV_RULE LENGTH_SIMPLIFY_CONV MLKEM_BASEMUL_K3_CORRECT));;
+    (CONV_RULE LENGTH_SIMPLIFY_CONV MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K3_CORRECT));;
 
 (* NOTE: This must be kept in sync with the CBMC specification
  * in mlkem/src/native/x86_64/src/arith_native_x86_64.h *)
 
-let MLKEM_BASEMUL_K3_SUBROUTINE_CORRECT = prove(
+let MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K3_SUBROUTINE_CORRECT = prove(
   `!src1 src2 src2t dst a0 b0 c0 d0 dz0 a1 b1 c1 d1 dz1 a2 b2 c2 d2 dz2 pc stackpointer returnaddress.
         aligned 32 src1 /\
         aligned 32 src2 /\
@@ -1684,7 +1684,7 @@ let MLKEM_BASEMUL_K3_SUBROUTINE_CORRECT = prove(
                             ) (mod &3329)))
               (MAYCHANGE [RSP] ,, MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,,
                MAYCHANGE [memory :> bytes(dst, 512)])`,
-  MATCH_ACCEPT_TAC(ADD_IBT_RULE MLKEM_BASEMUL_K3_NOIBT_SUBROUTINE_CORRECT));;
+  MATCH_ACCEPT_TAC(ADD_IBT_RULE MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K3_NOIBT_SUBROUTINE_CORRECT));;
 
 (* ------------------------------------------------------------------------- *)
 (* Constant-time and memory safety proof.                                    *)
@@ -1696,10 +1696,10 @@ needs "mlkem_native/x86_64/proofs/subroutine_signatures.ml";;
 let full_spec,public_vars = mk_safety_spec
     ~keep_maychanges:true
     (assoc "mlkem_basemul_k3" subroutine_signatures)
-    MLKEM_BASEMUL_K3_CORRECT
+    MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K3_CORRECT
     mlkem_basemul_k3_tmc_EXEC;;
 
-let MLKEM_BASEMUL_K3_SAFE = time prove
+let MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K3_SAFE = time prove
  (`exists f_events.
        forall e src1 src2 src2t dst pc.
            aligned 32 src1 /\
@@ -1716,7 +1716,7 @@ let MLKEM_BASEMUL_K3_SAFE = time prove
                     C_ARGUMENTS [dst; src1; src2; src2t] s /\
                     read events s = e)
                (\s.
-                    read RIP s = word (pc + MLKEM_BASEMUL_K3_CORE_END) /\
+                    read RIP s = word (pc + MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K3_CORE_END) /\
                     (exists e2.
                          read events s = APPEND e2 e /\
                          e2 = f_events src1 src2 src2t dst pc /\
@@ -1734,7 +1734,7 @@ let MLKEM_BASEMUL_K3_SAFE = time prove
   CONV_TAC LENGTH_SIMPLIFY_CONV THEN
   PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars mlkem_basemul_k3_tmc_EXEC);;
 
-let MLKEM_BASEMUL_K3_NOIBT_SUBROUTINE_SAFE = time prove
+let MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K3_NOIBT_SUBROUTINE_SAFE = time prove
  (`exists f_events.
        forall e src1 src2 src2t dst pc stackpointer returnaddress.
           aligned 32 src1 /\
@@ -1764,10 +1764,10 @@ let MLKEM_BASEMUL_K3_NOIBT_SUBROUTINE_SAFE = time prove
                            [dst,512; stackpointer,8]))
                (\s s'. true)`,
   X86_PROMOTE_RETURN_NOSTACK_TAC mlkem_basemul_k3_tmc
-    (CONV_RULE LENGTH_SIMPLIFY_CONV MLKEM_BASEMUL_K3_SAFE) THEN
+    (CONV_RULE LENGTH_SIMPLIFY_CONV MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K3_SAFE) THEN
   DISCHARGE_SAFETY_PROPERTY_TAC);;
 
-let MLKEM_BASEMUL_K3_SUBROUTINE_SAFE = time prove
+let MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K3_SUBROUTINE_SAFE = time prove
  (`exists f_events.
        forall e src1 src2 src2t dst pc stackpointer returnaddress.
           aligned 32 src1 /\
@@ -1796,4 +1796,4 @@ let MLKEM_BASEMUL_K3_SUBROUTINE_SAFE = time prove
                             dst,512; stackpointer,8]
                            [dst,512; stackpointer,8]))
                (\s s'. true)`,
-  MATCH_ACCEPT_TAC(ADD_IBT_RULE MLKEM_BASEMUL_K3_NOIBT_SUBROUTINE_SAFE));;
+  MATCH_ACCEPT_TAC(ADD_IBT_RULE MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K3_NOIBT_SUBROUTINE_SAFE));;
diff --git a/proofs/hol_light/x86_64/proofs/polyvec_basemul_acc_montgomery_cached_k4_avx2_asm.ml b/proofs/hol_light/x86_64/proofs/polyvec_basemul_acc_montgomery_cached_k4_avx2_asm.ml
index c127ff347..b834a98a3 100644
--- a/proofs/hol_light/x86_64/proofs/polyvec_basemul_acc_montgomery_cached_k4_avx2_asm.ml
+++ b/proofs/hol_light/x86_64/proofs/polyvec_basemul_acc_montgomery_cached_k4_avx2_asm.ml
@@ -1637,16 +1637,16 @@ let LENGTH_MLKEM_BASEMUL_K4_TMC =
   REWRITE_CONV[mlkem_basemul_k4_tmc] `LENGTH mlkem_basemul_k4_tmc`
   |> CONV_RULE(RAND_CONV LENGTH_CONV);;
 
-let MLKEM_BASEMUL_K4_POSTAMBLE_LENGTH = new_definition
-  `MLKEM_BASEMUL_K4_POSTAMBLE_LENGTH = 1`;;
+let MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K4_POSTAMBLE_LENGTH = new_definition
+  `MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K4_POSTAMBLE_LENGTH = 1`;;
 
-let MLKEM_BASEMUL_K4_CORE_END = new_definition
-  `MLKEM_BASEMUL_K4_CORE_END = LENGTH mlkem_basemul_k4_tmc - MLKEM_BASEMUL_K4_POSTAMBLE_LENGTH`;;
+let MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K4_CORE_END = new_definition
+  `MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K4_CORE_END = LENGTH mlkem_basemul_k4_tmc - MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K4_POSTAMBLE_LENGTH`;;
 
 let LENGTH_SIMPLIFY_CONV =
   REWRITE_CONV[LENGTH_MLKEM_BASEMUL_K4_TMC;
-              MLKEM_BASEMUL_K4_CORE_END;
-              MLKEM_BASEMUL_K4_POSTAMBLE_LENGTH] THENC
+              MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K4_CORE_END;
+              MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K4_POSTAMBLE_LENGTH] THENC
   NUM_REDUCE_CONV THENC REWRITE_CONV [ADD_0];;
 
 (* Enable simplification of word_subwords by default.
@@ -1715,7 +1715,7 @@ let pmulaccred1_k4 = define
      (&(inverse_mod 3329 65536) *
         pmulacc1_k4 a0 b0 c0 d0 dz0 a1 b1 c1 d1 dz1 a2 b2 c2 d2 dz2 a3 b3 c3 d3 dz3) rem &3329`;;
 
-let MLKEM_BASEMUL_K4_CORRECT = prove(
+let MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K4_CORRECT = prove(
   `!src1 src2 src2t dst a0 b0 c0 d0 dz0 a1 b1 c1 d1 dz1 a2 b2 c2 d2 dz2 a3 b3 c3 d3 dz3 pc.
         aligned 32 src1 /\
         aligned 32 src2 /\
@@ -1790,7 +1790,7 @@ let MLKEM_BASEMUL_K4_CORRECT = prove(
                    (!i. i < 16 ==> !j. j < 8
                         ==> read(memory :> bytes16
                              (word_add src2t (word (768 + 32*j + 2*i)))) s = dz3 i j))
-              (\s. read RIP s = word (pc + MLKEM_BASEMUL_K4_CORE_END) /\
+              (\s. read RIP s = word (pc + MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K4_CORE_END) /\
                    (!i. i < 16 ==> !j. j < 4
                         ==> (let j' = 2*j in
                               (abs(ival(a0 i j')) <= &2 pow 12  /\
@@ -1907,7 +1907,7 @@ let MLKEM_BASEMUL_K4_CORRECT = prove(
   CONV_TAC INT_RING
 );;
 
-let MLKEM_BASEMUL_K4_NOIBT_SUBROUTINE_CORRECT = prove(
+let MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K4_NOIBT_SUBROUTINE_CORRECT = prove(
   `!src1 src2 src2t dst a0 b0 c0 d0 dz0 a1 b1 c1 d1 dz1 a2 b2 c2 d2 dz2 a3 b3 c3 d3 dz3 pc stackpointer returnaddress.
         aligned 32 src1 /\
         aligned 32 src2 /\
@@ -2045,12 +2045,12 @@ let MLKEM_BASEMUL_K4_NOIBT_SUBROUTINE_CORRECT = prove(
                MAYCHANGE [memory :> bytes(dst, 512)])`,
   CONV_TAC LENGTH_SIMPLIFY_CONV THEN
   X86_PROMOTE_RETURN_NOSTACK_TAC mlkem_basemul_k4_tmc
-    (CONV_RULE LENGTH_SIMPLIFY_CONV MLKEM_BASEMUL_K4_CORRECT));;
+    (CONV_RULE LENGTH_SIMPLIFY_CONV MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K4_CORRECT));;
 
 (* NOTE: This must be kept in sync with the CBMC specification
  * in mlkem/src/native/x86_64/src/arith_native_x86_64.h *)
 
-let MLKEM_BASEMUL_K4_SUBROUTINE_CORRECT = prove(
+let MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K4_SUBROUTINE_CORRECT = prove(
   `!src1 src2 src2t dst a0 b0 c0 d0 dz0 a1 b1 c1 d1 dz1 a2 b2 c2 d2 dz2 a3 b3 c3 d3 dz3 pc stackpointer returnaddress.
         aligned 32 src1 /\
         aligned 32 src2 /\
@@ -2186,7 +2186,7 @@ let MLKEM_BASEMUL_K4_SUBROUTINE_CORRECT = prove(
                             ) (mod &3329)))
               (MAYCHANGE [RSP] ,, MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,,
                MAYCHANGE [memory :> bytes(dst, 512)])`,
-  MATCH_ACCEPT_TAC(ADD_IBT_RULE MLKEM_BASEMUL_K4_NOIBT_SUBROUTINE_CORRECT));;
+  MATCH_ACCEPT_TAC(ADD_IBT_RULE MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K4_NOIBT_SUBROUTINE_CORRECT));;
 
 (* ------------------------------------------------------------------------- *)
 (* Constant-time and memory safety proof.                                    *)
@@ -2198,10 +2198,10 @@ needs "mlkem_native/x86_64/proofs/subroutine_signatures.ml";;
 let full_spec,public_vars = mk_safety_spec
     ~keep_maychanges:true
     (assoc "mlkem_basemul_k4" subroutine_signatures)
-    MLKEM_BASEMUL_K4_CORRECT
+    MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K4_CORRECT
     mlkem_basemul_k4_tmc_EXEC;;
 
-let MLKEM_BASEMUL_K4_SAFE = time prove
+let MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K4_SAFE = time prove
  (`exists f_events.
        forall e src1 src2 src2t dst pc.
            aligned 32 src1 /\
@@ -2218,7 +2218,7 @@ let MLKEM_BASEMUL_K4_SAFE = time prove
                     C_ARGUMENTS [dst; src1; src2; src2t] s /\
                     read events s = e)
                (\s.
-                    read RIP s = word (pc + MLKEM_BASEMUL_K4_CORE_END) /\
+                    read RIP s = word (pc + MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K4_CORE_END) /\
                     (exists e2.
                          read events s = APPEND e2 e /\
                          e2 = f_events src1 src2 src2t dst pc /\
@@ -2236,7 +2236,7 @@ let MLKEM_BASEMUL_K4_SAFE = time prove
   CONV_TAC LENGTH_SIMPLIFY_CONV THEN
   PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars mlkem_basemul_k4_tmc_EXEC);;
 
-let MLKEM_BASEMUL_K4_NOIBT_SUBROUTINE_SAFE = time prove
+let MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K4_NOIBT_SUBROUTINE_SAFE = time prove
  (`exists f_events.
        forall e src1 src2 src2t dst pc stackpointer returnaddress.
           aligned 32 src1 /\
@@ -2266,10 +2266,10 @@ let MLKEM_BASEMUL_K4_NOIBT_SUBROUTINE_SAFE = time prove
                            [dst,512; stackpointer,8]))
                (\s s'. true)`,
   X86_PROMOTE_RETURN_NOSTACK_TAC mlkem_basemul_k4_tmc
-    (CONV_RULE LENGTH_SIMPLIFY_CONV MLKEM_BASEMUL_K4_SAFE) THEN
+    (CONV_RULE LENGTH_SIMPLIFY_CONV MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K4_SAFE) THEN
   DISCHARGE_SAFETY_PROPERTY_TAC);;
 
-let MLKEM_BASEMUL_K4_SUBROUTINE_SAFE = time prove
+let MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K4_SUBROUTINE_SAFE = time prove
  (`exists f_events.
        forall e src1 src2 src2t dst pc stackpointer returnaddress.
           aligned 32 src1 /\
@@ -2298,5 +2298,5 @@ let MLKEM_BASEMUL_K4_SUBROUTINE_SAFE = time prove
                             dst,512; stackpointer,8]
                            [dst,512; stackpointer,8]))
                (\s s'. true)`,
-  MATCH_ACCEPT_TAC(ADD_IBT_RULE MLKEM_BASEMUL_K4_NOIBT_SUBROUTINE_SAFE));;
+  MATCH_ACCEPT_TAC(ADD_IBT_RULE MLKEM_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED_K4_NOIBT_SUBROUTINE_SAFE));;
 
diff --git a/scripts/lint b/scripts/lint
index d85b9134a..d77e7c092 100755
--- a/scripts/lint
+++ b/scripts/lint
@@ -411,6 +411,80 @@ gh_group_start "Linting Doxygen comments"
 check-doxygen
 gh_group_end
 
+# Derive the theorem-name prefix from a proof routine's basename:
+#   - strip the platform suffix (_aarch64_asm or _avx2_asm)
+#   - uppercase
+#   - prepend MLKEM_ unless the routine is a keccak proof
+theorem-prefix()
+{
+  local routine="$1"
+  local platform_suffix="$2"
+  local base="${routine%${platform_suffix}}"
+  base=$(echo "$base" | tr '[:lower:]' '[:upper:]')
+  [[ $base == KECCAK_* ]] || base="MLKEM_${base}"
+  echo "$base"
+}
+
+check-theorems()
+{
+  local success=true
+  for arch in aarch64 x86_64; do
+    local proofs_dir="$ROOT/proofs/hol_light/$arch/proofs"
+    local platform_suffix="_aarch64_asm"
+    [[ $arch == "x86_64" ]] && platform_suffix="_avx2_asm"
+    local proofs
+    proofs=$("$ROOT/proofs/hol_light/$arch/list_proofs.sh")
+
+    for routine in $proofs; do
+      local file="$proofs_dir/${routine}.ml"
+      local prefix
+      prefix=$(theorem-prefix "$routine" "$platform_suffix")
+
+      # rej_uniform uses MEMSAFE in place of SAFE because no constant-time proof exists
+      local safe="SAFE"
+      [[ ${routine} == rej_uniform_* ]] && safe="MEMSAFE"
+
+      local expected=(
+        "${prefix}_CORRECT"
+        "${prefix}_SUBROUTINE_CORRECT"
+        "${prefix}_SUBROUTINE_${safe}"
+      )
+      if [[ $arch == "x86_64" ]]; then
+        expected+=(
+          "${prefix}_${safe}"
+          "${prefix}_NOIBT_SUBROUTINE_CORRECT"
+          "${prefix}_NOIBT_SUBROUTINE_${safe}"
+        )
+      fi
+
+      for theorem in "${expected[@]}"; do
+        if ! grep -qE "^[[:space:]]*let ${theorem}[[:space:]]+=[[:space:]]+(time[[:space:]]+)?prove" "$file"; then
+          gh_error "${routine}" "" "Missing theorem" "${file}: ${theorem} not found"
+          success=false
+        fi
+      done
+
+      if grep -q "CHEAT_TAC" "$file"; then
+        gh_error "${routine}" "" "CHEAT_TAC detected" "${file}: uses CHEAT_TAC"
+        success=false
+      fi
+    done
+  done
+
+  if $success; then
+    info "Check HOL-Light theorems"
+    gh_summary_success "Check HOL-Light theorems"
+  else
+    error "Check HOL-Light theorems"
+    SUCCESS=false
+    gh_summary_failure "Check HOL-Light theorems"
+  fi
+}
+
+gh_group_start "Check HOL-Light theorems"
+check-theorems
+gh_group_end
+
 if ! $SUCCESS; then
   if $IN_GITHUB_CONTEXT; then
     printf "%b%s%b\n" "${RED}" "The following checks failed, expand each for more details." "${NORMAL}"
diff --git a/scripts/tests b/scripts/tests
index 147c62f9a..98e7be1ab 100755
--- a/scripts/tests
+++ b/scripts/tests
@@ -1015,7 +1015,9 @@ class Tests:
         self.check_fail()
 
     def hol_light(self):
-        if platform.machine().lower() in ["arm64", "aarch64"]:
+        if self.args.arch:
+            arch = self.args.arch
+        elif platform.machine().lower() in ["arm64", "aarch64"]:
             arch = "aarch64"
         elif platform.machine().lower() in ["x86_64"]:
             arch = "x86_64"
@@ -1479,6 +1481,14 @@ def cli():
         default=False,
     )
 
+    hol_light_parser.add_argument(
+        "-a",
+        "--arch",
+        help="Architecture for which to list/run HOL_LIGHT proofs (aarch64 or x86_64).",
+        choices=["aarch64", "x86_64"],
+        default=None,
+    )
+
     # func arguments
     func_parser = cmd_subparsers.add_parser(
         "func",