CBMC: Remove unused array parameter

hanno-becker · hanno-becker · commit bf3082207ddf · 2025-03-27T16:24:08.000Z
We were informed by the CBMC team that the use of the CBMC
flag `--arrays-uf-always` should not be beneficial to our proofs.

This commit comments out this CBMC flag.

Signed-off-by: Hanno Becker &lt;beckphan@amazon.co.uk&gt;
diff --git a/proofs/cbmc/keccak_squeeze_once/Makefile b/proofs/cbmc/keccak_squeeze_once/Makefile
@@ -27,7 +27,18 @@ USE_DYNAMIC_FRAMES=1
 EXTERNAL_SAT_SOLVER=
 CBMCFLAGS=--bitwuzla
 
-CBMCFLAGS += --no-array-field-sensitivity --arrays-uf-always --slice-formula
+# For this proof we tell CBMC to
+#  1. not decompose arrays into their individual cells
+#  2. to model arrays directly as SMT-lib arrays
+#  3. 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
+# CBMCFLAGS += --arrays-uf-always
+CBMCFLAGS += --slice-formula
 
 FUNCTION_NAME = mlk_keccak_squeeze_once
 
diff --git a/proofs/cbmc/keccak_squeezeblocks/Makefile b/proofs/cbmc/keccak_squeezeblocks/Makefile
@@ -27,7 +27,18 @@ USE_DYNAMIC_FRAMES=1
 EXTERNAL_SAT_SOLVER=
 CBMCFLAGS=--bitwuzla
 
-CBMCFLAGS += --no-array-field-sensitivity --arrays-uf-always --slice-formula
+# For this proof we tell CBMC to
+#  1. not decompose arrays into their individual cells
+#  2. to model arrays directly as SMT-lib arrays
+#  3. 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
+# CBMCFLAGS += --arrays-uf-always
+CBMCFLAGS += --slice-formula
 
 FUNCTION_NAME = mlk_keccak_squeezeblocks
 
diff --git a/proofs/cbmc/keccak_squeezeblocks_x4/Makefile b/proofs/cbmc/keccak_squeezeblocks_x4/Makefile
@@ -27,7 +27,18 @@ USE_DYNAMIC_FRAMES=1
 EXTERNAL_SAT_SOLVER=
 CBMCFLAGS=--bitwuzla
 
-CBMCFLAGS += --no-array-field-sensitivity --arrays-uf-always --slice-formula
+# For this proof we tell CBMC to
+#  1. not decompose arrays into their individual cells
+#  2. to model arrays directly as SMT-lib arrays
+#  3. 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
+# CBMCFLAGS += --arrays-uf-always
+CBMCFLAGS += --slice-formula
 
 FUNCTION_NAME = mlk_keccak_squeezeblocks_x4
 
diff --git a/proofs/cbmc/keccakf1600_extract_bytes/Makefile b/proofs/cbmc/keccakf1600_extract_bytes/Makefile
@@ -27,8 +27,6 @@ USE_DYNAMIC_FRAMES=1
 EXTERNAL_SAT_SOLVER=
 CBMCFLAGS=--bitwuzla
 
-# CBMCFLAGS += --no-array-field-sensitivity --arrays-uf-always --slice-formula
-
 FUNCTION_NAME = mlk_keccakf1600_extract_bytes
 
 # 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
@@ -36,7 +36,9 @@ CBMCFLAGS=--smt2
 #
 # For functions that use large and multi-dimensional arrays, this yields
 # a substantial improvement in proof performance.
-CBMCFLAGS += --no-array-field-sensitivity --arrays-uf-always --slice-formula
+CBMCFLAGS += --no-array-field-sensitivity
+# CBMCFLAGS += --arrays-uf-always
+CBMCFLAGS += --slice-formula
 
 FUNCTION_NAME = mlk_keccakf1600_permute
 
diff --git a/proofs/cbmc/keccakf1600x4_extract_bytes/Makefile b/proofs/cbmc/keccakf1600x4_extract_bytes/Makefile
@@ -27,8 +27,6 @@ USE_DYNAMIC_FRAMES=1
 EXTERNAL_SAT_SOLVER=
 CBMCFLAGS=--bitwuzla
 
-# CBMCFLAGS += --no-array-field-sensitivity --arrays-uf-always --slice-formula
-
 FUNCTION_NAME = mlk_keccakf1600x4_extract_bytes
 
 # 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
@@ -36,7 +36,9 @@ CBMCFLAGS=--smt2
 #
 # For functions that use large and multi-dimensional arrays, this yields
 # a substantial improvement in proof performance.
-CBMCFLAGS += --no-array-field-sensitivity --arrays-uf-always --slice-formula
+CBMCFLAGS += --no-array-field-sensitivity
+# CBMCFLAGS += --arrays-uf-always
+CBMCFLAGS += --slice-formula
 
 FUNCTION_NAME = mlk_keccakf1600x4_permute
 
diff --git a/proofs/cbmc/matvec_mul/Makefile b/proofs/cbmc/matvec_mul/Makefile
@@ -35,7 +35,9 @@ CBMCFLAGS=--smt2
 #
 # For functions that use large and multi-dimensional arrays, this yields
 # a substantial improvement in proof performance.
-CBMCFLAGS += --no-array-field-sensitivity --arrays-uf-always --slice-formula
+CBMCFLAGS += --no-array-field-sensitivity
+# CBMCFLAGS += --arrays-uf-always
+CBMCFLAGS += --slice-formula
 
 FUNCTION_NAME = mlk_matvec_mul
 
@@ -46,7 +48,7 @@ FUNCTION_NAME = mlk_matvec_mul
 # EXPENSIVE = true
 
 # This function is large enough to need...
-CBMC_OBJECT_BITS = 8
+CBMC_OBJECT_BITS = 10
 
 # If you require access to a file-local ("static") function or object to conduct
 # your proof, set the following (and do not include the original source file
diff --git a/proofs/cbmc/poly_permute_bitrev_to_custom/Makefile b/proofs/cbmc/poly_permute_bitrev_to_custom/Makefile
@@ -35,7 +35,9 @@ CBMCFLAGS=--smt2
 #
 # For functions that use large and multi-dimensional arrays, this yields
 # a substantial improvement in proof performance.
-CBMCFLAGS += --no-array-field-sensitivity --arrays-uf-always --slice-formula
+CBMCFLAGS += --no-array-field-sensitivity
+# CBMCFLAGS += --arrays-uf-always
+CBMCFLAGS += --slice-formula
 
 FUNCTION_NAME = mlk_poly_permute_bitrev_to_custom
 
diff --git a/proofs/cbmc/polyvec_add/Makefile b/proofs/cbmc/polyvec_add/Makefile
@@ -36,7 +36,9 @@ CBMCFLAGS=--smt2
 #
 # For functions that use large and multi-dimensional arrays, this yields
 # a substantial improvement in proof performance.
-CBMCFLAGS += --no-array-field-sensitivity --arrays-uf-always --slice-formula
+CBMCFLAGS += --no-array-field-sensitivity
+# CBMCFLAGS += --arrays-uf-always
+CBMCFLAGS += --slice-formula
 
 FUNCTION_NAME = mlk_polyvec_add
 
diff --git a/proofs/cbmc/polyvec_basemul_acc_montgomery_cached/Makefile b/proofs/cbmc/polyvec_basemul_acc_montgomery_cached/Makefile
@@ -26,7 +26,19 @@ 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 --arrays-uf-always --slice-formula
+
+# For this proof we tell CBMC to
+#  1. not decompose arrays into their individual cells
+#  2. to model arrays directly as SMT-lib arrays
+#  3. 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
+# CBMCFLAGS += --arrays-uf-always
+CBMCFLAGS += --slice-formula
 
 FUNCTION_NAME = mlk_polyvec_basemul_acc_montgomery_cached
 
diff --git a/proofs/cbmc/rej_uniform_native/Makefile b/proofs/cbmc/rej_uniform_native/Makefile
@@ -27,8 +27,6 @@ USE_DYNAMIC_FRAMES=1
 EXTERNAL_SAT_SOLVER=
 CBMCFLAGS=--bitwuzla
 
-#CBMCFLAGS += --no-array-field-sensitivity --arrays-uf-always --slice-formula
-
 FUNCTION_NAME = rej_uniform_native
 
 # If this proof is found to consume huge amounts of RAM, you can set the

Original file line number	Diff line number	Diff line change
`@@ -36,7 +36,9 @@ CBMCFLAGS=--smt2`
`36`	`36`	`#`
`37`	`37`	`# For functions that use large and multi-dimensional arrays, this yields`
`38`	`38`	`# a substantial improvement in proof performance.`
`39`		`-CBMCFLAGS += --no-array-field-sensitivity --arrays-uf-always --slice-formula`
	`39`	`+CBMCFLAGS += --no-array-field-sensitivity`
	`40`	`+# CBMCFLAGS += --arrays-uf-always`
	`41`	`+CBMCFLAGS += --slice-formula`
`40`	`42`
`41`	`43`	`FUNCTION_NAME = mlk_keccakf1600_permute`
`42`	`44`
Original file line number	Diff line number	Diff line change
`@@ -35,7 +35,9 @@ CBMCFLAGS=--smt2`
`35`	`35`	`#`
`36`	`36`	`# For functions that use large and multi-dimensional arrays, this yields`
`37`	`37`	`# a substantial improvement in proof performance.`
`38`		`-CBMCFLAGS += --no-array-field-sensitivity --arrays-uf-always --slice-formula`
	`38`	`+CBMCFLAGS += --no-array-field-sensitivity`
	`39`	`+# CBMCFLAGS += --arrays-uf-always`
	`40`	`+CBMCFLAGS += --slice-formula`
`39`	`41`
`40`	`42`	`FUNCTION_NAME = mlk_poly_permute_bitrev_to_custom`
`41`	`43`