Remove --no-array-field-sensitivity for all proofs

rod-chapman · rod-chapman · commit de80b7fd309d · 2026-04-20T15:25:34.000+01:00
1. Remove --no-array-field-sensitivty from all per-function Makefiles

2. Update Makefile.common to:
   a. Reject --slice-formula if specified in a per-function Makefile, since
      it is already added by default in Makefile.common now.
   b. Reject --no-array-field-sensitivity if specified in a per-function Makefile

Signed-off-by: Rod Chapman &lt;rodchap@amazon.com&gt;
diff --git a/proofs/cbmc/Makefile.common b/proofs/cbmc/Makefile.common
@@ -538,13 +538,26 @@ PROOF_GOTO ?= $(GOTODIR)/$(PROOF)
 SPACE :=$() $()
 COMMA :=,
 
+################################################################
+# CBMC team recommend that --no-array-field-sensitivity should never be used
+# with CBMC 6.9.0 and above when --slice-formula has been specified
+ifeq ($(findstring --no-array-field-sensitivity,$(CBMCFLAGS)),--no-array-field-sensitivity)
+$(error CBMC option --no-array-field-sensitivity must not be used with CBMC 6.9.0 and above)
+endif
+
+################################################################
+# CBMC team recommend that --slice-formula should _always_ be used
+# so we reject it here if it is already specified in a per-function Makefile
+ifeq ($(findstring --slice-formula,$(CBMCFLAGS)),--slice-formula)
+$(error CBMC option --slice-formula is set by default in Makefile.common, so should not be specified in a function-specific Makefile)
+endif
+
 ################################################################
 # CBMC flags common to all proofs
 CBMCFLAGS += $(CBMC_FLAG_FLUSH)
 CBMCFLAGS += --object-bits $(CBMC_OBJECT_BITS)
 CBMCFLAGS += --slice-formula
 
-
 ################################################################
 # Set C compiler defines
 DEFINES += -DCBMC=1
diff --git a/proofs/cbmc/keccak_squeeze_once/Makefile b/proofs/cbmc/keccak_squeeze_once/Makefile
@@ -29,16 +29,6 @@ USE_DYNAMIC_FRAMES=1
 EXTERNAL_SAT_SOLVER=
 CBMCFLAGS=--bitwuzla
 
-# For this proof we tell CBMC to
-#  - not decompose arrays into their individual cells
-#  - to slice constraints that are not in the cone of influence of the proof obligations
-# These options simplify them modelling of arrays and produce much more compact
-# SMT files, leaving all array-type reasoning to the SMT solver.
-#
-# For functions that use large and multi-dimensional arrays, this yields
-# a substantial improvement in proof performance.
-CBMCFLAGS += --no-array-field-sensitivity
-
 FUNCTION_NAME = mlk_keccak_squeeze_once
 
 # If this proof is found to consume huge amounts of RAM, you can set the
diff --git a/proofs/cbmc/keccak_squeezeblocks/Makefile b/proofs/cbmc/keccak_squeezeblocks/Makefile
@@ -29,16 +29,6 @@ USE_DYNAMIC_FRAMES=1
 EXTERNAL_SAT_SOLVER=
 CBMCFLAGS=--bitwuzla
 
-# For this proof we tell CBMC to
-#  - not decompose arrays into their individual cells
-#  - to slice constraints that are not in the cone of influence of the proof obligations
-# These options simplify them modelling of arrays and produce much more compact
-# SMT files, leaving all array-type reasoning to the SMT solver.
-#
-# For functions that use large and multi-dimensional arrays, this yields
-# a substantial improvement in proof performance.
-CBMCFLAGS += --no-array-field-sensitivity
-
 FUNCTION_NAME = mlk_keccak_squeezeblocks
 
 # If this proof is found to consume huge amounts of RAM, you can set the
diff --git a/proofs/cbmc/keccak_squeezeblocks_x4/Makefile b/proofs/cbmc/keccak_squeezeblocks_x4/Makefile
@@ -29,16 +29,6 @@ USE_DYNAMIC_FRAMES=1
 EXTERNAL_SAT_SOLVER=
 CBMCFLAGS=--bitwuzla
 
-# For this proof we tell CBMC to
-#  - not decompose arrays into their individual cells
-#  - to slice constraints that are not in the cone of influence of the proof obligations
-# These options simplify them modelling of arrays and produce much more compact
-# SMT files, leaving all array-type reasoning to the SMT solver.
-#
-# For functions that use large and multi-dimensional arrays, this yields
-# a substantial improvement in proof performance.
-CBMCFLAGS += --no-array-field-sensitivity
-
 FUNCTION_NAME = mlk_keccak_squeezeblocks_x4
 
 # If this proof is found to consume huge amounts of RAM, you can set the
diff --git a/proofs/cbmc/keccakf1600_permute/Makefile b/proofs/cbmc/keccakf1600_permute/Makefile
@@ -28,16 +28,6 @@ USE_DYNAMIC_FRAMES=1
 EXTERNAL_SAT_SOLVER=
 CBMCFLAGS=--smt2
 
-# For this proof we tell CBMC to
-#  - not decompose arrays into their individual cells
-#  - to slice constraints that are not in the cone of influence of the proof obligations
-# These options simplify them modelling of arrays and produce much more compact
-# SMT files, leaving all array-type reasoning to the SMT solver.
-#
-# For functions that use large and multi-dimensional arrays, this yields
-# a substantial improvement in proof performance.
-CBMCFLAGS += --no-array-field-sensitivity
-
 FUNCTION_NAME = mlk_keccakf1600_permute
 
 # If this proof is found to consume huge amounts of RAM, you can set the
diff --git a/proofs/cbmc/keccakf1600_permute_c/Makefile b/proofs/cbmc/keccakf1600_permute_c/Makefile
@@ -28,16 +28,6 @@ USE_DYNAMIC_FRAMES=1
 EXTERNAL_SAT_SOLVER=
 CBMCFLAGS=--smt2
 
-# For this proof we tell CBMC to
-#  - not decompose arrays into their individual cells
-#  - to slice constraints that are not in the cone of influence of the proof obligations
-# These options simplify them modelling of arrays and produce much more compact
-# SMT files, leaving all array-type reasoning to the SMT solver.
-#
-# For functions that use large and multi-dimensional arrays, this yields
-# a substantial improvement in proof performance.
-CBMCFLAGS += --no-array-field-sensitivity
-
 FUNCTION_NAME = mlk_keccakf1600_permute_c
 
 # If this proof is found to consume huge amounts of RAM, you can set the
diff --git a/proofs/cbmc/keccakf1600x4_permute/Makefile b/proofs/cbmc/keccakf1600x4_permute/Makefile
@@ -28,16 +28,6 @@ USE_DYNAMIC_FRAMES=1
 EXTERNAL_SAT_SOLVER=
 CBMCFLAGS=--smt2
 
-# For this proof we tell CBMC to
-#  - not decompose arrays into their individual cells
-#  - to slice constraints that are not in the cone of influence of the proof obligations
-# These options simplify them modelling of arrays and produce much more compact
-# SMT files, leaving all array-type reasoning to the SMT solver.
-#
-# For functions that use large and multi-dimensional arrays, this yields
-# a substantial improvement in proof performance.
-CBMCFLAGS += --no-array-field-sensitivity
-
 FUNCTION_NAME = mlk_keccakf1600x4_permute
 
 # If this proof is found to consume huge amounts of RAM, you can set the
diff --git a/proofs/cbmc/matvec_mul/Makefile b/proofs/cbmc/matvec_mul/Makefile
@@ -27,16 +27,6 @@ USE_DYNAMIC_FRAMES=1
 EXTERNAL_SAT_SOLVER=
 CBMCFLAGS=--smt2
 
-# For this proof we tell CBMC to
-#  - not decompose arrays into their individual cells
-#  - to slice constraints that are not in the cone of influence of the proof obligations
-# These options simplify them modelling of arrays and produce much more compact
-# SMT files, leaving all array-type reasoning to the SMT solver.
-#
-# For functions that use large and multi-dimensional arrays, this yields
-# a substantial improvement in proof performance.
-CBMCFLAGS += --no-array-field-sensitivity
-
 FUNCTION_NAME = mlk_matvec_mul
 
 # If this proof is found to consume huge amounts of RAM, you can set the
diff --git a/proofs/cbmc/polymat_permute_bitrev_to_custom/Makefile b/proofs/cbmc/polymat_permute_bitrev_to_custom/Makefile
@@ -27,16 +27,6 @@ USE_DYNAMIC_FRAMES=1
 EXTERNAL_SAT_SOLVER=
 CBMCFLAGS=--smt2
 
-# For this proof we tell CBMC to
-#  - not decompose arrays into their individual cells
-#  - to slice constraints that are not in the cone of influence of the proof obligations
-# These options simplify them modelling of arrays and produce much more compact
-# SMT files, leaving all array-type reasoning to the SMT solver.
-#
-# For functions that use large and multi-dimensional arrays, this yields
-# a substantial improvement in proof performance.
-CBMCFLAGS += --no-array-field-sensitivity
-
 FUNCTION_NAME = mlk_polymat_permute_bitrev_to_custom
 
 # If this proof is found to consume huge amounts of RAM, you can set the
diff --git a/proofs/cbmc/polyvec_add/Makefile b/proofs/cbmc/polyvec_add/Makefile
@@ -27,16 +27,6 @@ USE_DYNAMIC_FRAMES=1
 EXTERNAL_SAT_SOLVER=
 CBMCFLAGS=--smt2
 
-# For this proof we tell CBMC to
-#  - not decompose arrays into their individual cells
-#  - to slice constraints that are not in the cone of influence of the proof obligations
-# These options simplify them modelling of arrays and produce much more compact
-# SMT files, leaving all array-type reasoning to the SMT solver.
-#
-# For functions that use large and multi-dimensional arrays, this yields
-# a substantial improvement in proof performance.
-CBMCFLAGS += --no-array-field-sensitivity
-
 FUNCTION_NAME = mlk_polyvec_add
 
 # If this proof is found to consume huge amounts of RAM, you can set the
diff --git a/proofs/cbmc/polyvec_basemul_acc_montgomery_cached/Makefile b/proofs/cbmc/polyvec_basemul_acc_montgomery_cached/Makefile
@@ -28,16 +28,6 @@ USE_DYNAMIC_FRAMES=1
 EXTERNAL_SAT_SOLVER=
 CBMCFLAGS=--smt2
 
-# For this proof we tell CBMC to
-#  - not decompose arrays into their individual cells
-#  - to slice constraints that are not in the cone of influence of the proof obligations
-# These options simplify them modelling of arrays and produce much more compact
-# SMT files, leaving all array-type reasoning to the SMT solver.
-#
-# For functions that use large and multi-dimensional arrays, this yields
-# a substantial improvement in proof performance.
-CBMCFLAGS += --no-array-field-sensitivity
-
 FUNCTION_NAME = mlk_polyvec_basemul_acc_montgomery_cached
 
 # If this proof is found to consume huge amounts of RAM, you can set the
diff --git a/proofs/cbmc/polyvec_compress_du/Makefile b/proofs/cbmc/polyvec_compress_du/Makefile
@@ -27,7 +27,6 @@ USE_DYNAMIC_FRAMES=1
 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
 EXTERNAL_SAT_SOLVER=
 CBMCFLAGS=--smt2
-CBMCFLAGS += --no-array-field-sensitivity
 
 FUNCTION_NAME = mlk_polyvec_compress_du
 
diff --git a/proofs/cbmc/polyvec_tobytes/Makefile b/proofs/cbmc/polyvec_tobytes/Makefile
@@ -26,7 +26,6 @@ USE_DYNAMIC_FRAMES=1
 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
 EXTERNAL_SAT_SOLVER=
 CBMCFLAGS=--smt2
-CBMCFLAGS += --no-array-field-sensitivity
 
 FUNCTION_NAME = mlk_polyvec_tobytes
 
