HOL-Light: Remove memaccess_inbounds duplicates workaround

mkannwischer · mkannwischer · commit 7da6768cf858 · 2026-04-22T11:26:50.000+08:00
- Resolves #1578 Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>
diff --git a/proofs/hol_light/aarch64/proofs/keccak_f1600_x1_scalar.ml b/proofs/hol_light/aarch64/proofs/keccak_f1600_x1_scalar.ml
@@ -522,15 +522,11 @@ let KECCAK_F1600_X1_SCALAR_SUBROUTINE_CORRECT = prove
 needs "arm/proofs/consttime.ml";;
 needs "aarch64/proofs/subroutine_signatures.ml";;
 
-needs "common/consttime_utils.ml";;
-
 let full_spec,public_vars = mk_safety_spec
     ~keep_maychanges:false
     (assoc "sha3_keccak_f1600" subroutine_signatures)
     KECCAK_F1600_X1_SCALAR_SUBROUTINE_CORRECT
     KECCAK_F1600_X1_SCALAR_EXEC;;
-(* Remove duplicates from memaccess_inbounds lists (s2n-bignum#350) *)
-let full_spec = ONCE_DEPTH_CONV MEMACCESS_INBOUNDS_DEDUP_CONV full_spec |> concl |> rhs;;
 
 let KECCAK_F1600_X1_SCALAR_SUBROUTINE_SAFE = time prove
  (`exists f_events.
diff --git a/proofs/hol_light/aarch64/proofs/keccak_f1600_x1_v84a.ml b/proofs/hol_light/aarch64/proofs/keccak_f1600_x1_v84a.ml
@@ -307,15 +307,11 @@ let KECCAK_F1600_X1_V84A_SUBROUTINE_CORRECT = prove
 needs "arm/proofs/consttime.ml";;
 needs "aarch64/proofs/subroutine_signatures.ml";;
 
-needs "common/consttime_utils.ml";;
-
 let full_spec,public_vars = mk_safety_spec
     ~keep_maychanges:false
     (assoc "sha3_keccak_f1600_alt" subroutine_signatures)
     KECCAK_F1600_X1_V84A_SUBROUTINE_CORRECT
     KECCAK_F1600_X1_V84A_EXEC;;
-(* Remove duplicates from memaccess_inbounds lists (s2n-bignum#350) *)
-let full_spec = ONCE_DEPTH_CONV MEMACCESS_INBOUNDS_DEDUP_CONV full_spec |> concl |> rhs;;
 
 let KECCAK_F1600_X1_V84A_SUBROUTINE_SAFE = time prove
  (`exists f_events.
diff --git a/proofs/hol_light/aarch64/proofs/keccak_f1600_x2_v84a.ml b/proofs/hol_light/aarch64/proofs/keccak_f1600_x2_v84a.ml
@@ -388,15 +388,11 @@ let KECCAK_F1600_X2_V84A_SUBROUTINE_CORRECT = prove
 needs "arm/proofs/consttime.ml";;
 needs "aarch64/proofs/subroutine_signatures.ml";;
 
-needs "common/consttime_utils.ml";;
-
 let full_spec,public_vars = mk_safety_spec
     ~keep_maychanges:false
     (assoc "sha3_keccak2_f1600" subroutine_signatures)
     KECCAK_F1600_X2_V84A_SUBROUTINE_CORRECT
     KECCAK_F1600_X2_V84A_EXEC;;
-(* Remove duplicates from memaccess_inbounds lists (s2n-bignum#350) *)
-let full_spec = ONCE_DEPTH_CONV MEMACCESS_INBOUNDS_DEDUP_CONV full_spec |> concl |> rhs;;
 
 let KECCAK_F1600_X2_V84A_SUBROUTINE_SAFE = time prove
  (`exists f_events.
diff --git a/proofs/hol_light/aarch64/proofs/keccak_f1600_x4_v8a_scalar.ml b/proofs/hol_light/aarch64/proofs/keccak_f1600_x4_v8a_scalar.ml
@@ -1495,15 +1495,11 @@ let KECCAK_F1600_X4_V8A_SCALAR_SUBROUTINE_CORRECT = prove
 needs "arm/proofs/consttime.ml";;
 needs "aarch64/proofs/subroutine_signatures.ml";;
 
-needs "common/consttime_utils.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;;
-(* Remove duplicates from memaccess_inbounds lists (s2n-bignum#350) *)
-let full_spec = ONCE_DEPTH_CONV MEMACCESS_INBOUNDS_DEDUP_CONV full_spec |> concl |> rhs;;
 
 let KECCAK_F1600_X4_V8A_SCALAR_SUBROUTINE_SAFE = time prove
  (`exists f_events.
diff --git a/proofs/hol_light/aarch64/proofs/keccak_f1600_x4_v8a_v84a_scalar.ml b/proofs/hol_light/aarch64/proofs/keccak_f1600_x4_v8a_v84a_scalar.ml
@@ -1400,15 +1400,11 @@ let KECCAK_F1600_X4_V8A_V84A_SCALAR_SUBROUTINE_CORRECT = prove
 needs "arm/proofs/consttime.ml";;
 needs "aarch64/proofs/subroutine_signatures.ml";;
 
-needs "common/consttime_utils.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;;
-(* Remove duplicates from memaccess_inbounds lists (s2n-bignum#350) *)
-let full_spec = ONCE_DEPTH_CONV MEMACCESS_INBOUNDS_DEDUP_CONV full_spec |> concl |> rhs;;
 
 let KECCAK_F1600_X4_V8A_V84A_SCALAR_SUBROUTINE_SAFE = time prove
  (`exists f_events.
diff --git a/proofs/hol_light/aarch64/proofs/mlkem_intt.ml b/proofs/hol_light/aarch64/proofs/mlkem_intt.ml
@@ -754,15 +754,11 @@ let MLKEM_INTT_SUBROUTINE_CORRECT = prove
 needs "arm/proofs/consttime.ml";;
 needs "aarch64/proofs/subroutine_signatures.ml";;
 
-needs "common/consttime_utils.ml";;
-
 let full_spec,public_vars = mk_safety_spec
     ~keep_maychanges:false
     (assoc "mlkem_intt" subroutine_signatures)
     MLKEM_INTT_SUBROUTINE_CORRECT
     MLKEM_INTT_EXEC;;
-(* Remove duplicates from memaccess_inbounds lists (s2n-bignum#350) *)
-let full_spec = ONCE_DEPTH_CONV MEMACCESS_INBOUNDS_DEDUP_CONV full_spec |> concl |> rhs;;
 
 let MLKEM_INTT_SUBROUTINE_SAFE = time prove
  (`exists f_events.
diff --git a/proofs/hol_light/aarch64/proofs/mlkem_ntt.ml b/proofs/hol_light/aarch64/proofs/mlkem_ntt.ml
@@ -689,15 +689,11 @@ let MLKEM_NTT_SUBROUTINE_CORRECT = prove
 needs "arm/proofs/consttime.ml";;
 needs "aarch64/proofs/subroutine_signatures.ml";;
 
-needs "common/consttime_utils.ml";;
-
 let full_spec,public_vars = mk_safety_spec
     ~keep_maychanges:false
     (assoc "mlkem_ntt" subroutine_signatures)
     MLKEM_NTT_SUBROUTINE_CORRECT
     MLKEM_NTT_EXEC;;
-(* Remove duplicates from memaccess_inbounds lists (s2n-bignum#350) *)
-let full_spec = ONCE_DEPTH_CONV MEMACCESS_INBOUNDS_DEDUP_CONV full_spec |> concl |> rhs;;
 
 let MLKEM_NTT_SUBROUTINE_SAFE = time prove
  (`exists f_events.
diff --git a/proofs/hol_light/aarch64/proofs/mlkem_poly_mulcache_compute.ml b/proofs/hol_light/aarch64/proofs/mlkem_poly_mulcache_compute.ml
@@ -286,7 +286,6 @@ let MLKEM_MULCACHE_COMPUTE_SUBROUTINE_CORRECT = prove
 (* Constant-time and memory safety proof.                                    *)
 (* ------------------------------------------------------------------------- *)
 
-needs "common/consttime_utils.ml";;
 needs "aarch64/proofs/subroutine_signatures.ml";;
 
 let full_spec,public_vars = mk_safety_spec
diff --git a/proofs/hol_light/aarch64/proofs/mlkem_poly_reduce.ml b/proofs/hol_light/aarch64/proofs/mlkem_poly_reduce.ml
@@ -279,15 +279,11 @@ let MLKEM_POLY_REDUCE_SUBROUTINE_CORRECT = prove
 needs "arm/proofs/consttime.ml";;
 needs "aarch64/proofs/subroutine_signatures.ml";;
 
-needs "common/consttime_utils.ml";;
-
 let full_spec,public_vars = mk_safety_spec
     ~keep_maychanges:false
     (assoc "mlkem_reduce" subroutine_signatures)
     MLKEM_POLY_REDUCE_SUBROUTINE_CORRECT
     MLKEM_POLY_REDUCE_EXEC;;
-(* Remove duplicates from memaccess_inbounds lists (s2n-bignum#350) *)
-let full_spec = ONCE_DEPTH_CONV MEMACCESS_INBOUNDS_DEDUP_CONV full_spec |> concl |> rhs;;
 
 let MLKEM_POLY_REDUCE_SUBROUTINE_SAFE = time prove
  (`exists f_events.
diff --git a/proofs/hol_light/aarch64/proofs/mlkem_poly_tobytes.ml b/proofs/hol_light/aarch64/proofs/mlkem_poly_tobytes.ml
@@ -275,7 +275,6 @@ let MLKEM_POLY_TOBYTES_SUBROUTINE_CORRECT = prove
 (* Constant-time and memory safety proof.                                    *)
 (* ------------------------------------------------------------------------- *)
 
-needs "common/consttime_utils.ml";;
 needs "aarch64/proofs/subroutine_signatures.ml";;
 
 let full_spec,public_vars = mk_safety_spec
diff --git a/proofs/hol_light/aarch64/proofs/mlkem_poly_tomont.ml b/proofs/hol_light/aarch64/proofs/mlkem_poly_tomont.ml
@@ -265,15 +265,11 @@ let MLKEM_TOMONT_SUBROUTINE_CORRECT = prove
 needs "arm/proofs/consttime.ml";;
 needs "aarch64/proofs/subroutine_signatures.ml";;
 
-needs "common/consttime_utils.ml";;
-
 let full_spec,public_vars = mk_safety_spec
     ~keep_maychanges:false
     (assoc "mlkem_tomont" subroutine_signatures)
     MLKEM_TOMONT_SUBROUTINE_CORRECT
     POLY_TOMONT_EXEC;;
-(* Remove duplicates from memaccess_inbounds lists (s2n-bignum#350) *)
-let full_spec = ONCE_DEPTH_CONV MEMACCESS_INBOUNDS_DEDUP_CONV full_spec |> concl |> rhs;;
 
 let MLKEM_TOMONT_SUBROUTINE_SAFE = time prove
  (`exists f_events.
diff --git a/proofs/hol_light/aarch64/proofs/mlkem_rej_uniform.ml b/proofs/hol_light/aarch64/proofs/mlkem_rej_uniform.ml
@@ -1682,7 +1682,6 @@ let MLKEM_REJ_UNIFORM_SUBROUTINE_CORRECT = prove
 (* ========================================================================= *)
 
 needs "arm/proofs/consttime.ml";;
-needs "common/consttime_utils.ml";;
 
 (* Helper: discharge the memsafe postcondition
      exists e2. read events s = APPEND e2 e /\ memaccess_inbounds e2 R W
diff --git a/proofs/hol_light/aarch64/proofs/mlkem_utils.ml b/proofs/hol_light/aarch64/proofs/mlkem_utils.ml
@@ -90,4 +90,3 @@ let MAP_UNTIL_TARGET_PC f n = fun (asl, w) ->
     core n (asl, w);;
 
 needs "arm/proofs/consttime.ml";;
-needs "common/consttime_utils.ml";;
diff --git a/proofs/hol_light/common/consttime_utils.ml b/proofs/hol_light/common/consttime_utils.ml
diff --git a/proofs/hol_light/x86_64/proofs/keccak_f1600_x4_avx2.ml b/proofs/hol_light/x86_64/proofs/keccak_f1600_x4_avx2.ml
@@ -1119,7 +1119,6 @@ let KECCAK_F1600_X4_AVX2_SUBROUTINE_CORRECT = prove
 
 needs "x86/proofs/consttime.ml";;
 needs "x86_64/proofs/subroutine_signatures.ml";;
-needs "common/consttime_utils.ml";;
 
 
 let full_spec,public_vars = mk_safety_spec
@@ -1128,10 +1127,6 @@ let full_spec,public_vars = mk_safety_spec
     (CONV_RULE LENGTH_SIMPLIFY_CONV KECCAK_F1600_X4_AVX2_CORRECT)
     KECCAK_F1600_X4_AVX2_EXEC;;
 
-(* Remove duplicates from memaccess_inbounds lists (s2n-bignum#350) *)
-let full_spec = ONCE_DEPTH_CONV MEMACCESS_INBOUNDS_DEDUP_CONV full_spec
-  |> concl |> rhs;;
-
 let KECCAK_F1600_X4_AVX2_SAFE = time prove
  (`exists f_events.
        forall e rc_pointer bitstate_in rho8_ptr rho56_ptr pc stackpointer.
diff --git a/proofs/hol_light/x86_64/proofs/mlkem_intt.ml b/proofs/hol_light/x86_64/proofs/mlkem_intt.ml
@@ -1278,20 +1278,16 @@ let MLKEM_INTT_SUBROUTINE_CORRECT  = prove
 
 needs "x86/proofs/consttime.ml";;
 needs "x86_64/proofs/subroutine_signatures.ml";;
-needs "common/consttime_utils.ml";;
-
 let full_spec,public_vars = mk_safety_spec
     ~keep_maychanges:true
     (assoc "mlkem_intt" subroutine_signatures)
     MLKEM_INTT_CORRECT
     MLKEM_INTT_TMC_EXEC;;
-(* Remove duplicates from memaccess_inbounds lists (s2n-bignum#350).
-   full_spec mixes numeric and symbolic buffer sizes: mk_safety_spec computes
+(* 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
    preconditions. Normalize to numeric form so ASSERT_CONCL_TAC matches the
    hand-written goal after LENGTH_SIMPLIFY_CONV. *)
-let full_spec = ONCE_DEPTH_CONV MEMACCESS_INBOUNDS_DEDUP_CONV full_spec |> concl |> rhs;;
 let full_spec = LENGTH_SIMPLIFY_CONV full_spec |> concl |> rhs;;
 
 let MLKEM_INTT_SAFE = time prove
diff --git a/proofs/hol_light/x86_64/proofs/mlkem_ntt.ml b/proofs/hol_light/x86_64/proofs/mlkem_ntt.ml
@@ -1288,20 +1288,17 @@ let MLKEM_NTT_SUBROUTINE_CORRECT  = prove
 
 needs "x86/proofs/consttime.ml";;
 needs "x86_64/proofs/subroutine_signatures.ml";;
-needs "common/consttime_utils.ml";;
 
 let full_spec,public_vars = mk_safety_spec
     ~keep_maychanges:true
     (assoc "mlkem_ntt" subroutine_signatures)
     MLKEM_NTT_CORRECT
     MLKEM_NTT_TMC_EXEC;;
-(* Remove duplicates from memaccess_inbounds lists (s2n-bignum#350).
-   full_spec mixes numeric and symbolic buffer sizes: mk_safety_spec computes
+(* 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
    preconditions. Normalize to numeric form so ASSERT_CONCL_TAC matches the
    hand-written goal after LENGTH_SIMPLIFY_CONV. *)
-let full_spec = ONCE_DEPTH_CONV MEMACCESS_INBOUNDS_DEDUP_CONV full_spec |> concl |> rhs;;
 let full_spec = LENGTH_SIMPLIFY_CONV full_spec |> concl |> rhs;;
 
 let MLKEM_NTT_SAFE = time prove
diff --git a/proofs/hol_light/x86_64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml b/proofs/hol_light/x86_64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml
@@ -1197,7 +1197,6 @@ let MLKEM_BASEMUL_K2_SUBROUTINE_CORRECT = prove(
 
 needs "x86/proofs/consttime.ml";;
 needs "x86_64/proofs/subroutine_signatures.ml";;
-needs "common/consttime_utils.ml";;
 
 let full_spec,public_vars = mk_safety_spec
     ~keep_maychanges:true
diff --git a/proofs/hol_light/x86_64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k3.ml b/proofs/hol_light/x86_64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k3.ml
@@ -1692,7 +1692,6 @@ let MLKEM_BASEMUL_K3_SUBROUTINE_CORRECT = prove(
 
 needs "x86/proofs/consttime.ml";;
 needs "x86_64/proofs/subroutine_signatures.ml";;
-needs "common/consttime_utils.ml";;
 
 let full_spec,public_vars = mk_safety_spec
     ~keep_maychanges:true
diff --git a/proofs/hol_light/x86_64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k4.ml b/proofs/hol_light/x86_64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k4.ml
@@ -2194,7 +2194,6 @@ let MLKEM_BASEMUL_K4_SUBROUTINE_CORRECT = prove(
 
 needs "x86/proofs/consttime.ml";;
 needs "x86_64/proofs/subroutine_signatures.ml";;
-needs "common/consttime_utils.ml";;
 
 let full_spec,public_vars = mk_safety_spec
     ~keep_maychanges:true
diff --git a/proofs/hol_light/x86_64/proofs/mlkem_reduce.ml b/proofs/hol_light/x86_64/proofs/mlkem_reduce.ml
@@ -475,15 +475,11 @@ let MLKEM_REDUCE_SUBROUTINE_CORRECT = prove
 needs "x86/proofs/consttime.ml";;
 needs "x86_64/proofs/subroutine_signatures.ml";;
 
-needs "common/consttime_utils.ml";;
-
 let full_spec,public_vars = mk_safety_spec
     ~keep_maychanges:true
     (assoc "mlkem_reduce" subroutine_signatures)
     MLKEM_REDUCE_CORRECT
     mlkem_reduce_TMC_EXEC;;
-(* Remove duplicates from memaccess_inbounds lists (s2n-bignum#350) *)
-let full_spec = ONCE_DEPTH_CONV MEMACCESS_INBOUNDS_DEDUP_CONV full_spec |> concl |> rhs;;
 
 let MLKEM_REDUCE_SAFE = time prove
  (`exists f_events.
diff --git a/proofs/hol_light/x86_64/proofs/mlkem_tomont.ml b/proofs/hol_light/x86_64/proofs/mlkem_tomont.ml
@@ -11,7 +11,6 @@
 needs "x86/proofs/base.ml";;
 
 needs "common/mlkem_specs.ml";;
-needs "common/consttime_utils.ml";;
 
 (* print_literal_from_elf "x86_64/mlkem/mlkem_tomont.o";; *)
 
@@ -366,15 +365,11 @@ let MLKEM_TOMONT_SUBROUTINE_CORRECT = prove(
 needs "x86/proofs/consttime.ml";;
 needs "x86_64/proofs/subroutine_signatures.ml";;
 
-needs "common/consttime_utils.ml";;
-
 let full_spec,public_vars = mk_safety_spec
     ~keep_maychanges:true
     (assoc "mlkem_tomont" subroutine_signatures)
     MLKEM_TOMONT_CORRECT
     mlkem_tomont_TMC_EXEC;;
-(* Remove duplicates from memaccess_inbounds lists (s2n-bignum#350) *)
-let full_spec = ONCE_DEPTH_CONV MEMACCESS_INBOUNDS_DEDUP_CONV full_spec |> concl |> rhs;;
 
 let MLKEM_TOMONT_SAFE = time prove
  (`exists f_events.
diff --git a/proofs/hol_light/x86_64/proofs/mlkem_unpack.ml b/proofs/hol_light/x86_64/proofs/mlkem_unpack.ml
@@ -434,15 +434,11 @@ let MLKEM_UNPACK_SUBROUTINE_CORRECT = prove(
 needs "x86/proofs/consttime.ml";;
 needs "x86_64/proofs/subroutine_signatures.ml";;
 
-needs "common/consttime_utils.ml";;
-
 let full_spec,public_vars = mk_safety_spec
     ~keep_maychanges:true
     (assoc "mlkem_unpack" subroutine_signatures)
     MLKEM_UNPACK_CORRECT
     mlkem_unpack_TMC_EXEC;;
-(* Remove duplicates from memaccess_inbounds lists (s2n-bignum#350) *)
-let full_spec = ONCE_DEPTH_CONV MEMACCESS_INBOUNDS_DEDUP_CONV full_spec |> concl |> rhs;;
 
 let MLKEM_UNPACK_SAFE = time prove
  (`exists f_events.
diff --git a/proofs/hol_light/x86_64/proofs/mlkem_utils.ml b/proofs/hol_light/x86_64/proofs/mlkem_utils.ml
@@ -8,4 +8,3 @@
 (* ========================================================================= *)
 
 needs "x86/proofs/consttime.ml";;
-needs "common/consttime_utils.ml";;
