Add the safety properties of x86 mlkem_reduce for 4 variants (IBT x Windows)

aqjune-aws · aqjune-aws · commit 2a0240c560b8 · 2025-12-06T04:21:32.000Z
This patch adds the safety properties of x86 mlkem_reduce for 4 variants: whether it has IBT or not, and whether it has Windows ABI or not.

This also has a lot of changes that affect safety proofs other than x86 mlkem_reduce:

- The name of PROVE_SAFETY_SPEC is changed to PROVE_SAFETY_SPEC_TAC
- The theorem for weakly_valid_component of bytes256 was wrong; I fixed it.
- The `mk_safety_spec` takes an extra argument for keeping the MAYCHANGE part of ensures. This is needed if the spec is going to be used for compositional reasoning.
diff --git a/arm/proofs/arm.ml b/arm/proofs/arm.ml
@@ -648,10 +648,11 @@ let ARM_QUICKSIM_TAC execth pats snums =
 (* More convenient wrappings of basic simulation flow.                       *)
 (* ------------------------------------------------------------------------- *)
 
-let ARM_SIM_TAC ?(preprocess_tac=ALL_TAC) ?(canonicalize_pc_diff=true)
+let ARM_SIM_TAC ?(preprocess_tac:tactic option) ?(canonicalize_pc_diff=true)
     execth snums =
   REWRITE_TAC(!simulation_precanon_thms) THEN
-  ENSURES_INIT_TAC "s0" THEN preprocess_tac THEN
+  ENSURES_INIT_TAC "s0" THEN
+  (match preprocess_tac with Some t -> t | None -> ALL_TAC) THEN
   ARM_STEPS_TAC execth snums THEN
   ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN
   (if canonicalize_pc_diff then
diff --git a/arm/proofs/bignum_copy_row_from_table.ml b/arm/proofs/bignum_copy_row_from_table.ml
@@ -627,6 +627,7 @@ needs "arm/proofs/consttime.ml";;
 needs "arm/proofs/subroutine_signatures.ml";;
 
 let full_spec,public_vars = mk_safety_spec
+    ~keep_maychanges:false
     (assoc "bignum_copy_row_from_table" subroutine_signatures)
     BIGNUM_COPY_ROW_FROM_TABLE_SUBROUTINE_CORRECT
     BIGNUM_COPY_ROW_FROM_TABLE_EXEC;;
diff --git a/arm/proofs/bignum_copy_row_from_table_16.ml b/arm/proofs/bignum_copy_row_from_table_16.ml
@@ -347,6 +347,7 @@ needs "arm/proofs/consttime.ml";;
 needs "arm/proofs/subroutine_signatures.ml";;
 
 let full_spec,public_vars = mk_safety_spec
+    ~keep_maychanges:false
     (assoc "bignum_copy_row_from_table_16" subroutine_signatures)
     BIGNUM_COPY_ROW_FROM_TABLE_16_SUBROUTINE_CORRECT
     BIGNUM_COPY_ROW_FROM_TABLE_16_EXEC;;
diff --git a/arm/proofs/bignum_copy_row_from_table_32.ml b/arm/proofs/bignum_copy_row_from_table_32.ml
@@ -373,6 +373,7 @@ needs "arm/proofs/consttime.ml";;
 needs "arm/proofs/subroutine_signatures.ml";;
 
 let full_spec,public_vars = mk_safety_spec
+    ~keep_maychanges:false
     (assoc "bignum_copy_row_from_table_32" subroutine_signatures)
     BIGNUM_COPY_ROW_FROM_TABLE_32_SUBROUTINE_CORRECT
     BIGNUM_COPY_ROW_FROM_TABLE_32_EXEC;;
diff --git a/arm/proofs/bignum_copy_row_from_table_8n.ml b/arm/proofs/bignum_copy_row_from_table_8n.ml
@@ -887,6 +887,7 @@ needs "arm/proofs/consttime.ml";;
 needs "arm/proofs/subroutine_signatures.ml";;
 
 let full_spec,public_vars = mk_safety_spec
+    ~keep_maychanges:false
     (assoc "bignum_copy_row_from_table_8n" subroutine_signatures)
     BIGNUM_COPY_ROW_FROM_TABLE_8N_SUBROUTINE_CORRECT
     BIGNUM_COPY_ROW_FROM_TABLE_8N_EXEC;;
diff --git a/arm/proofs/bignum_emontredc_8n.ml b/arm/proofs/bignum_emontredc_8n.ml
@@ -2956,6 +2956,7 @@ needs "arm/proofs/consttime.ml";;
 needs "arm/proofs/subroutine_signatures.ml";;
 
 let full_spec,public_vars = mk_safety_spec
+    ~keep_maychanges:false
     (assoc "bignum_emontredc_8n" subroutine_signatures)
     BIGNUM_EMONTREDC_8N_SUBROUTINE_CORRECT
     BIGNUM_EMONTREDC_8N_EXEC;;
diff --git a/arm/proofs/bignum_ge.ml b/arm/proofs/bignum_ge.ml
@@ -366,6 +366,7 @@ needs "arm/proofs/consttime.ml";;
 needs "arm/proofs/subroutine_signatures.ml";;
 
 let full_spec,public_vars = mk_safety_spec
+    ~keep_maychanges:false
     (assoc "bignum_ge" subroutine_signatures)
     BIGNUM_GE_SUBROUTINE_CORRECT
     BIGNUM_GE_EXEC;;
diff --git a/arm/proofs/bignum_mul.ml b/arm/proofs/bignum_mul.ml
@@ -461,6 +461,7 @@ needs "arm/proofs/consttime.ml";;
 needs "arm/proofs/subroutine_signatures.ml";;
 
 let full_spec,public_vars = mk_safety_spec
+    ~keep_maychanges:false
     (assoc "bignum_mul" subroutine_signatures)
     BIGNUM_MUL_SUBROUTINE_CORRECT
     BIGNUM_MUL_EXEC;;
diff --git a/arm/proofs/bignum_optsub.ml b/arm/proofs/bignum_optsub.ml
@@ -197,6 +197,7 @@ needs "arm/proofs/consttime.ml";;
 needs "arm/proofs/subroutine_signatures.ml";;
 
 let full_spec,public_vars = mk_safety_spec
+    ~keep_maychanges:false
     (assoc "bignum_optsub" subroutine_signatures)
     BIGNUM_OPTSUB_SUBROUTINE_CORRECT
     BIGNUM_OPTSUB_EXEC;;
diff --git a/arm/proofs/bignum_sqr.ml b/arm/proofs/bignum_sqr.ml
@@ -588,6 +588,7 @@ needs "arm/proofs/consttime.ml";;
 needs "arm/proofs/subroutine_signatures.ml";;
 
 let full_spec,public_vars = mk_safety_spec
+    ~keep_maychanges:false
     (assoc "bignum_sqr" subroutine_signatures)
     BIGNUM_SQR_SUBROUTINE_CORRECT
     BIGNUM_SQR_EXEC;;
diff --git a/arm/proofs/consttime.ml b/arm/proofs/consttime.ml
@@ -11,16 +11,18 @@ needs "common/consttime.ml";;
 
 let mk_safety_spec
     ?(coda_pc_range:(int*int) option) (* when coda is used: (begin, len) *)
+    ~(keep_maychanges:bool)
     (fnargs,xx,meminputs,memoutputs,memtemps)
     (subroutine_correct_th:thm) exec: term*(term list) =
   let read_sth_eq (f:term->bool):term->bool =
     fun t -> is_eq t && let l = lhs t in is_binary "read" l &&
       let l' = fst (dest_binary "read" l) in f l' in
-  gen_mk_safety_spec ?coda_pc_range (fnargs,xx,meminputs,memoutputs,memtemps)
+  gen_mk_safety_spec ?coda_pc_range ~keep_maychanges
+    (fnargs,xx,meminputs,memoutputs,memtemps)
     subroutine_correct_th exec
     (read_sth_eq (fun t -> t = `SP`)) (read_sth_eq (fun t -> t = `X30`));;
 
-let PROVE_SAFETY_SPEC ?(public_vars:term list option) exec:tactic =
-  GEN_PROVE_SAFETY_SPEC ?public_vars:public_vars exec
+let PROVE_SAFETY_SPEC_TAC ?(public_vars:term list option) exec:tactic =
+  GEN_PROVE_SAFETY_SPEC_TAC ?public_vars:public_vars exec
     [ALIGNED_BYTES_LOADED_APPEND_CLAUSE]
     ARM_SINGLE_STEP_TAC;;
diff --git a/arm/proofs/mlkem_basemul_k2.ml b/arm/proofs/mlkem_basemul_k2.ml
@@ -401,6 +401,7 @@ needs "arm/proofs/consttime.ml";;
 needs "arm/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_BASEMUL_K2_EXEC;;
@@ -436,4 +437,4 @@ let MLKEM_BASEMUL_K2_SUBROUTINE_SAFE = time prove
                         [dst,512; word_sub stackpointer (word 64),64])
                (\s s'. true)`,
   ASSERT_CONCL_TAC full_spec THEN
-  PROVE_SAFETY_SPEC ~public_vars:public_vars MLKEM_BASEMUL_K2_EXEC);;
+  PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars MLKEM_BASEMUL_K2_EXEC);;
diff --git a/arm/proofs/mlkem_basemul_k3.ml b/arm/proofs/mlkem_basemul_k3.ml
@@ -486,6 +486,7 @@ needs "arm/proofs/consttime.ml";;
 needs "arm/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_BASEMUL_K3_EXEC;;
@@ -521,4 +522,4 @@ let MLKEM_BASEMUL_K3_SUBROUTINE_SAFE = time prove
                         [dst,512; word_sub stackpointer (word 64),64])
                (\s s'. true)`,
   ASSERT_CONCL_TAC full_spec THEN
-  PROVE_SAFETY_SPEC ~public_vars:public_vars MLKEM_BASEMUL_K3_EXEC);;
+  PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars MLKEM_BASEMUL_K3_EXEC);;
diff --git a/arm/proofs/mlkem_basemul_k4.ml b/arm/proofs/mlkem_basemul_k4.ml
@@ -570,6 +570,7 @@ needs "arm/proofs/consttime.ml";;
 needs "arm/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_BASEMUL_K4_EXEC;;
@@ -605,4 +606,4 @@ let MLKEM_BASEMUL_K4_SUBROUTINE_SAFE = time prove
                         [dst,512; word_sub stackpointer (word 64),64])
                (\s s'. true)`,
   ASSERT_CONCL_TAC full_spec THEN
-  PROVE_SAFETY_SPEC ~public_vars:public_vars MLKEM_BASEMUL_K4_EXEC);;
+  PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars MLKEM_BASEMUL_K4_EXEC);;
diff --git a/arm/proofs/mlkem_intt.ml b/arm/proofs/mlkem_intt.ml
@@ -614,6 +614,7 @@ needs "arm/proofs/consttime.ml";;
 needs "arm/proofs/subroutine_signatures.ml";;
 
 let full_spec,public_vars = mk_safety_spec
+    ~keep_maychanges:false
     (assoc "mlkem_intt" subroutine_signatures)
     MLKEM_INTT_SUBROUTINE_CORRECT
     MLKEM_INTT_EXEC;;
@@ -648,4 +649,4 @@ let MLKEM_INTT_SUBROUTINE_SAFE = time prove
                         [a,512; word_sub stackpointer (word 64),64])
                (\s s'. true)`,
   ASSERT_CONCL_TAC full_spec THEN
-  PROVE_SAFETY_SPEC ~public_vars:public_vars MLKEM_INTT_EXEC);;
+  PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars MLKEM_INTT_EXEC);;
diff --git a/arm/proofs/mlkem_mulcache_compute.ml b/arm/proofs/mlkem_mulcache_compute.ml
@@ -246,6 +246,7 @@ needs "arm/proofs/consttime.ml";;
 needs "arm/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_MULCACHE_COMPUTE_EXEC;;
@@ -275,4 +276,4 @@ let MLKEM_MULCACHE_COMPUTE_SUBROUTINE_SAFE = time prove
                         [dst,256])
                (\s s'. true)`,
   ASSERT_CONCL_TAC full_spec THEN
-  PROVE_SAFETY_SPEC ~public_vars:public_vars MLKEM_MULCACHE_COMPUTE_EXEC);;
+  PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars MLKEM_MULCACHE_COMPUTE_EXEC);;
diff --git a/arm/proofs/mlkem_ntt.ml b/arm/proofs/mlkem_ntt.ml
@@ -577,6 +577,7 @@ needs "arm/proofs/consttime.ml";;
 needs "arm/proofs/subroutine_signatures.ml";;
 
 let full_spec,public_vars = mk_safety_spec
+    ~keep_maychanges:false
     (assoc "mlkem_ntt" subroutine_signatures)
     MLKEM_NTT_SUBROUTINE_CORRECT
     MLKEM_NTT_EXEC;;
@@ -611,4 +612,4 @@ let MLKEM_NTT_SUBROUTINE_SAFE = time prove
                         [a,512; word_sub stackpointer (word 64),64])
                (\s s'. true)`,
   ASSERT_CONCL_TAC full_spec THEN
-  PROVE_SAFETY_SPEC ~public_vars:public_vars MLKEM_NTT_EXEC);;
+  PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars MLKEM_NTT_EXEC);;
diff --git a/arm/proofs/mlkem_reduce.ml b/arm/proofs/mlkem_reduce.ml
@@ -207,6 +207,7 @@ needs "arm/proofs/consttime.ml";;
 needs "arm/proofs/subroutine_signatures.ml";;
 
 let full_spec,public_vars = mk_safety_spec
+    ~keep_maychanges:false
     (assoc "mlkem_reduce" subroutine_signatures)
     MLKEM_REDUCE_SUBROUTINE_CORRECT
     MLKEM_REDUCE_EXEC;;
@@ -230,4 +231,4 @@ let MLKEM_REDUCE_SUBROUTINE_SAFE = time prove
                         memaccess_inbounds e2 [a,512; a,512] [a,512])
                (\s s'. true)`,
   ASSERT_CONCL_TAC full_spec THEN
-  PROVE_SAFETY_SPEC ~public_vars:public_vars MLKEM_REDUCE_EXEC);;
+  PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars MLKEM_REDUCE_EXEC);;
diff --git a/arm/proofs/mlkem_tobytes.ml b/arm/proofs/mlkem_tobytes.ml
@@ -222,6 +222,7 @@ needs "arm/proofs/consttime.ml";;
 needs "arm/proofs/subroutine_signatures.ml";;
 
 let full_spec,public_vars = mk_safety_spec
+    ~keep_maychanges:false
     (assoc "mlkem_tobytes" subroutine_signatures)
     MLKEM_TOBYTES_SUBROUTINE_CORRECT
     MLKEM_TOBYTES_EXEC;;
@@ -245,4 +246,4 @@ let MLKEM_TOBYTES_SUBROUTINE_SAFE = time prove
                         memaccess_inbounds e2 [a,512; r,384] [r,384])
                (\s s'. true)`,
   ASSERT_CONCL_TAC full_spec THEN
-  PROVE_SAFETY_SPEC ~public_vars:public_vars MLKEM_TOBYTES_EXEC);;
+  PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars MLKEM_TOBYTES_EXEC);;
diff --git a/arm/proofs/mlkem_tomont.ml b/arm/proofs/mlkem_tomont.ml
@@ -222,6 +222,7 @@ needs "arm/proofs/consttime.ml";;
 needs "arm/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_TOMONT_EXEC;;
@@ -245,4 +246,4 @@ let MLKEM_TOMONT_SUBROUTINE_SAFE = time prove
                         memaccess_inbounds e2 [ptr,512; ptr,512] [ptr,512])
                (\s s'. true)`,
   ASSERT_CONCL_TAC full_spec THEN
-  PROVE_SAFETY_SPEC ~public_vars:public_vars MLKEM_TOMONT_EXEC);;
+  PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars MLKEM_TOMONT_EXEC);;
diff --git a/arm/proofs/sha3_keccak2_f1600.ml b/arm/proofs/sha3_keccak2_f1600.ml
@@ -351,6 +351,7 @@ needs "arm/proofs/consttime.ml";;
 needs "arm/proofs/subroutine_signatures.ml";;
 
 let full_spec,public_vars = mk_safety_spec
+    ~keep_maychanges:false
     (assoc "sha3_keccak2_f1600" subroutine_signatures)
     SHA3_KECCAK2_F1600_SUBROUTINE_CORRECT
     SHA3_KECCAK2_F1600_EXEC;;
@@ -384,4 +385,4 @@ let SHA3_KECCAK2_F1600_SUBROUTINE_SAFE = time prove
                         [a,400; word_sub stackpointer (word 64),64])
                (\s s'. true)`,
   ASSERT_CONCL_TAC full_spec THEN
-  PROVE_SAFETY_SPEC ~public_vars:public_vars SHA3_KECCAK2_F1600_EXEC);;
+  PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars SHA3_KECCAK2_F1600_EXEC);;
diff --git a/arm/proofs/sha3_keccak2_f1600_alt.ml b/arm/proofs/sha3_keccak2_f1600_alt.ml
@@ -398,6 +398,7 @@ needs "arm/proofs/consttime.ml";;
 needs "arm/proofs/subroutine_signatures.ml";;
 
 let full_spec,public_vars = mk_safety_spec
+    ~keep_maychanges:false
     (assoc "sha3_keccak2_f1600_alt" subroutine_signatures)
     SHA3_KECCAK2_F1600_ALT_SUBROUTINE_CORRECT
     SHA3_KECCAK2_F1600_ALT_EXEC;;
@@ -432,4 +433,4 @@ let SHA3_KECCAK2_F1600_ALT_SUBROUTINE_SAFE = time prove
                         [a,400; word_sub stackpointer (word 64),64])
                (\s s'. true)`,
   ASSERT_CONCL_TAC full_spec THEN
-  PROVE_SAFETY_SPEC ~public_vars:public_vars SHA3_KECCAK2_F1600_ALT_EXEC);;
+  PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars SHA3_KECCAK2_F1600_ALT_EXEC);;
diff --git a/arm/proofs/sha3_keccak4_f1600.ml b/arm/proofs/sha3_keccak4_f1600.ml
@@ -1277,6 +1277,7 @@ needs "arm/proofs/consttime.ml";;
 needs "arm/proofs/subroutine_signatures.ml";;
 
 let full_spec,public_vars = mk_safety_spec
+    ~keep_maychanges:false
     (assoc "sha3_keccak4_f1600" subroutine_signatures)
     SHA3_KECCAK4_F1600_SUBROUTINE_CORRECT
     SHA3_KECCAK4_F1600_EXEC;;
@@ -1310,4 +1311,4 @@ let SHA3_KECCAK4_F1600_SUBROUTINE_SAFE = time prove
                         [a,800; word_sub stackpointer (word 224),224])
                (\s s'. true)`,
   ASSERT_CONCL_TAC full_spec THEN
-  PROVE_SAFETY_SPEC ~public_vars:public_vars SHA3_KECCAK4_F1600_EXEC);;
+  PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars SHA3_KECCAK4_F1600_EXEC);;
diff --git a/arm/proofs/sha3_keccak4_f1600_alt.ml b/arm/proofs/sha3_keccak4_f1600_alt.ml
@@ -1463,6 +1463,7 @@ needs "arm/proofs/consttime.ml";;
 needs "arm/proofs/subroutine_signatures.ml";;
 
 let full_spec,public_vars = mk_safety_spec
+    ~keep_maychanges:false
     (assoc "sha3_keccak4_f1600_alt" subroutine_signatures)
     SHA3_KECCAK4_F1600_ALT_SUBROUTINE_CORRECT
     SHA3_KECCAK4_F1600_ALT_EXEC;;
@@ -1497,4 +1498,4 @@ let SHA3_KECCAK4_F1600_ALT_SUBROUTINE_SAFE = time prove
                         [a,800; word_sub stackpointer (word 224),224])
                (\s s'. true)`,
   ASSERT_CONCL_TAC full_spec THEN
-  PROVE_SAFETY_SPEC ~public_vars:public_vars SHA3_KECCAK4_F1600_ALT_EXEC);;
+  PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars SHA3_KECCAK4_F1600_ALT_EXEC);;
diff --git a/arm/proofs/sha3_keccak4_f1600_alt2.ml b/arm/proofs/sha3_keccak4_f1600_alt2.ml
@@ -1369,6 +1369,7 @@ needs "arm/proofs/consttime.ml";;
 needs "arm/proofs/subroutine_signatures.ml";;
 
 let full_spec,public_vars = mk_safety_spec
+    ~keep_maychanges:false
     (assoc "sha3_keccak4_f1600_alt2" subroutine_signatures)
     SHA3_KECCAK4_F1600_ALT2_SUBROUTINE_CORRECT
     SHA3_KECCAK4_F1600_ALT2_EXEC;;
@@ -1403,4 +1404,4 @@ let SHA3_KECCAK4_F1600_ALT2_SUBROUTINE_SAFE = time prove
                         [a,800; word_sub stackpointer (word 224),224])
                (\s s'. true)`,
   ASSERT_CONCL_TAC full_spec THEN
-  PROVE_SAFETY_SPEC ~public_vars:public_vars SHA3_KECCAK4_F1600_ALT2_EXEC);;
+  PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars SHA3_KECCAK4_F1600_ALT2_EXEC);;
diff --git a/arm/proofs/sha3_keccak_f1600.ml b/arm/proofs/sha3_keccak_f1600.ml
@@ -492,6 +492,7 @@ needs "arm/proofs/consttime.ml";;
 needs "arm/proofs/subroutine_signatures.ml";;
 
 let full_spec,public_vars = mk_safety_spec
+    ~keep_maychanges:false
     (assoc "sha3_keccak_f1600" subroutine_signatures)
     SHA3_KECCAK_F1600_SUBROUTINE_CORRECT
     SHA3_KECCAK_F1600_EXEC;;
@@ -525,4 +526,4 @@ let SHA3_KECCAK_F1600_SUBROUTINE_SAFE = time prove
                         [a,200; word_sub stackpointer (word 128),128])
                (\s s'. true)`,
   ASSERT_CONCL_TAC full_spec THEN
-  PROVE_SAFETY_SPEC ~public_vars:public_vars SHA3_KECCAK_F1600_EXEC);;
+  PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars SHA3_KECCAK_F1600_EXEC);;
diff --git a/arm/proofs/sha3_keccak_f1600_alt.ml b/arm/proofs/sha3_keccak_f1600_alt.ml
@@ -277,6 +277,7 @@ needs "arm/proofs/consttime.ml";;
 needs "arm/proofs/subroutine_signatures.ml";;
 
 let full_spec,public_vars = mk_safety_spec
+    ~keep_maychanges:false
     (assoc "sha3_keccak_f1600_alt" subroutine_signatures)
     SHA3_KECCAK_F1600_ALT_SUBROUTINE_CORRECT
     SHA3_KECCAK_F1600_ALT_EXEC;;
@@ -310,4 +311,4 @@ let SHA3_KECCAK_F1600_ALT_SUBROUTINE_SAFE = time prove
                         [a,200; word_sub stackpointer (word 64),64])
                (\s s'. true)`,
   ASSERT_CONCL_TAC full_spec THEN
-  PROVE_SAFETY_SPEC ~public_vars:public_vars SHA3_KECCAK_F1600_ALT_EXEC);;
+  PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars SHA3_KECCAK_F1600_ALT_EXEC);;
diff --git a/arm/proofs/sha3_keccak_f1600_alt2.ml b/arm/proofs/sha3_keccak_f1600_alt2.ml
@@ -450,6 +450,7 @@ needs "arm/proofs/consttime.ml";;
 needs "arm/proofs/subroutine_signatures.ml";;
 
 let full_spec,public_vars = mk_safety_spec
+    ~keep_maychanges:false
     (assoc "sha3_keccak_f1600_alt2" subroutine_signatures)
     SHA3_KECCAK_F1600_ALT2_SUBROUTINE_CORRECT
     SHA3_KECCAK_F1600_ALT2_EXEC;;
@@ -483,4 +484,4 @@ let SHA3_KECCAK_F1600_ALT2_SUBROUTINE_SAFE = time prove
                         [a,200; word_sub stackpointer (word 208),208])
                (\s s'. true)`,
   ASSERT_CONCL_TAC full_spec THEN
-  PROVE_SAFETY_SPEC ~public_vars:public_vars SHA3_KECCAK_F1600_ALT2_EXEC);;
+  PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars SHA3_KECCAK_F1600_ALT2_EXEC);;
diff --git a/common/components.ml b/common/components.ml
@@ -367,7 +367,7 @@ add_strongly_valid_component_thms [STRONGLY_VALID_COMPONENT_ENTIRETY];;
 (* ------------------------------------------------------------------------- *)
 
 let extensionally_valid_component = define
- `extensionally_valid_component c <=>
+ `extensionally_valid_component (c:(S,A)component) <=>
         (?f. !y s. read c (write c y s) = f y) /\
         (!s. write c (read c s) s = s) /\
         (!y z s. write c z (write c y s) = write c z s)`;;
@@ -2279,9 +2279,9 @@ let VALID_COMPONENT_BYTES256 = prove
            STRONGLY_VALID_COMPONENT_BYTES256]);;
 
 let WEAKLY_VALID_COMPONENT_BYTES256 = prove
- (`!a:int64. weakly_valid_component (bytes128 a)`,
+ (`!a:int64. weakly_valid_component (bytes256 a)`,
   SIMP_TAC[VALID_IMP_WEAKLY_VALID_COMPONENT;
-           VALID_COMPONENT_BYTES128]);;
+           VALID_COMPONENT_BYTES256]);;
 
 add_valid_component_thms
   [VALID_COMPONENT_BYTES8; VALID_COMPONENT_BYTES16;
@@ -3509,6 +3509,10 @@ let ASSUMPTION_STATE_UPDATE_TAC =
 
 let NONSELFMODIFYING_STATE_UPDATE_TAC bth =
   DISCH_THEN(fun th ->
+    (if not (is_eq (concl th)) then failwith
+      ("NONSELFMODIFYING_STATE_UPDATE_TAC: the goal must have " ^
+       "`write ... = ... ==> ...` as conclusion, but got `" ^
+       (string_of_term (concl th)) ^ " ==> ...`") else ());
     MP_TAC th THEN
     FIRST_X_ASSUM (MP_TAC o SPEC (lhand (concl th)) o MATCH_MP bth) THEN
     ANTS_TAC THENL
diff --git a/common/consttime.ml b/common/consttime.ml
diff --git a/common/equiv.ml b/common/equiv.ml
diff --git a/common/misc.ml b/common/misc.ml
diff --git a/common/relational.ml b/common/relational.ml
diff --git a/common/safety.ml b/common/safety.ml
diff --git a/x86/proofs/consttime.ml b/x86/proofs/consttime.ml
diff --git a/x86/proofs/mlkem_reduce.ml b/x86/proofs/mlkem_reduce.ml
diff --git a/x86/proofs/x86.ml b/x86/proofs/x86.ml
