Skip to content

Commit 56bfbee

Browse files
mkannwischermkannwischer
committed
CBMC: Remove --no-array-field-sensitivity from all proofs
Ports pq-code-package/mlkem-native#1654 Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>
1 parent 85b9dcb commit 56bfbee

17 files changed

Lines changed: 1 addition & 44 deletions

File tree

‎proofs/cbmc/compute_pack_z/Makefile‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -35,7 +35,6 @@ USE_DYNAMIC_FRAMES=1
3535
EXTERNAL_SAT_SOLVER=
3636
CBMCFLAGS=--external-smt2-solver $(PROOF_ROOT)/lib/z3_no_bv_extract --z3
3737
CBMCFLAGS += --slice-formula
38-
CBMCFLAGS += --no-array-field-sensitivity
3938

4039
FUNCTION_NAME = mld_compute_pack_z
4140

‎proofs/cbmc/keccak_squeezeblocks_x4/Makefile‎

Lines changed: 0 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -29,16 +29,6 @@ USE_DYNAMIC_FRAMES=1
2929
# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
3030
EXTERNAL_SAT_SOLVER=
3131
CBMCFLAGS=--bitwuzla
32-
33-
# For this proof we tell CBMC to
34-
# - not decompose arrays into their individual cells
35-
# - to slice constraints that are not in the cone of influence of the proof obligations
36-
# These options simplify them modelling of arrays and produce much more compact
37-
# SMT files, leaving all array-type reasoning to the SMT solver.
38-
#
39-
# For functions that use large and multi-dimensional arrays, this yields
40-
# a substantial improvement in proof performance.
41-
CBMCFLAGS += --no-array-field-sensitivity
4232
CBMCFLAGS += --slice-formula
4333

4434
FUNCTION_NAME = mld_keccak_squeezeblocks_x4

‎proofs/cbmc/keccakf1600x4_permute/Makefile‎

Lines changed: 0 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -28,16 +28,6 @@ USE_DYNAMIC_FRAMES=1
2828
# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
2929
EXTERNAL_SAT_SOLVER=
3030
CBMCFLAGS=--smt2
31-
32-
# For this proof we tell CBMC to
33-
# - not decompose arrays into their individual cells
34-
# - to slice constraints that are not in the cone of influence of the proof obligations
35-
# These options simplify them modelling of arrays and produce much more compact
36-
# SMT files, leaving all array-type reasoning to the SMT solver.
37-
#
38-
# For functions that use large and multi-dimensional arrays, this yields
39-
# a substantial improvement in proof performance.
40-
CBMCFLAGS += --no-array-field-sensitivity
4131
CBMCFLAGS += --slice-formula
4232

4333
FUNCTION_NAME = mld_keccakf1600x4_permute

‎proofs/cbmc/keccakf1600x4_permute_native/Makefile‎

Lines changed: 0 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -28,16 +28,6 @@ USE_DYNAMIC_FRAMES=1
2828
# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
2929
EXTERNAL_SAT_SOLVER=
3030
CBMCFLAGS=--smt2
31-
32-
# For this proof we tell CBMC to
33-
# - not decompose arrays into their individual cells
34-
# - to slice constraints that are not in the cone of influence of the proof obligations
35-
# These options simplify them modelling of arrays and produce much more compact
36-
# SMT files, leaving all array-type reasoning to the SMT solver.
37-
#
38-
# For functions that use large and multi-dimensional arrays, this yields
39-
# a substantial improvement in proof performance.
40-
CBMCFLAGS += --no-array-field-sensitivity
4131
CBMCFLAGS += --slice-formula
4232

4333
FUNCTION_NAME = mld_keccakf1600x4_permute_native

‎proofs/cbmc/pack_pk/Makefile‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@ USE_DYNAMIC_FRAMES=1
2525

2626
# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
2727
EXTERNAL_SAT_SOLVER=
28-
CBMCFLAGS=--smt2 --no-array-field-sensitivity --slice-formula
28+
CBMCFLAGS=--smt2 --slice-formula
2929

3030
FUNCTION_NAME = pack_pk
3131

‎proofs/cbmc/polyveck_chknorm/Makefile‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,6 @@ USE_DYNAMIC_FRAMES=1
2828
EXTERNAL_SAT_SOLVER=
2929
CBMCFLAGS=--smt2
3030
CBMCFLAGS += --slice-formula
31-
CBMCFLAGS += --no-array-field-sensitivity
3231

3332
FUNCTION_NAME = polyveck_chknorm
3433

‎proofs/cbmc/polyveck_pack_t0/Makefile‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,6 @@ USE_DYNAMIC_FRAMES=1
2727
EXTERNAL_SAT_SOLVER=
2828
CBMCFLAGS=--smt2
2929
CBMCFLAGS += --slice-formula
30-
CBMCFLAGS += --no-array-field-sensitivity
3130

3231
FUNCTION_NAME = polyveck_pack_t0
3332

‎proofs/cbmc/polyveck_pack_w1/Makefile‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,6 @@ USE_DYNAMIC_FRAMES=1
2626
# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
2727
EXTERNAL_SAT_SOLVER=
2828
CBMCFLAGS=--smt2
29-
CBMCFLAGS += --no-array-field-sensitivity
3029

3130
FUNCTION_NAME = polyveck_pack_w1
3231

‎proofs/cbmc/polyvecl_chknorm/Makefile‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,6 @@ USE_DYNAMIC_FRAMES=1
2828
EXTERNAL_SAT_SOLVER=
2929
CBMCFLAGS=--smt2
3030
CBMCFLAGS += --slice-formula
31-
CBMCFLAGS += --no-array-field-sensitivity
3231

3332
FUNCTION_NAME = polyvecl_chknorm
3433

‎proofs/cbmc/polyvecl_pointwise_acc_montgomery/Makefile‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,6 @@ USE_DYNAMIC_FRAMES=1
2828
EXTERNAL_SAT_SOLVER=
2929
CBMCFLAGS=--external-smt2-solver $(PROOF_ROOT)/lib/z3_smt_only --z3
3030
CBMCFLAGS += --slice-formula
31-
CBMCFLAGS += --no-array-field-sensitivity
3231

3332
FUNCTION_NAME = polyvecl_pointwise_acc_montgomery
3433

0 commit comments

Comments
 (0)