Proof instability resulting from insertion of blank line in sources

[rod-chapman]

In the mlkem-native project, we have found that addition of blank lines in source code can cause unexpected differences in generated GOTO and SMT files, and subsequent proof instability.

This Issue documents this problem and adds a tiny test case that demonstrates one such difference. This may not be the only source of such instability, but this test case serves as a starting point to understand the issues.

Link to test case sources will be added below.

[rod-chapman]

Test case here https://github.com/rod-chapman/cbmc-examples/tree/main/issues/8820

[rod-chapman]

Using CBMC 6.8.0 in that directory, running "./go" yields:

test1.txt            vs test2.txt:                  40 lines differ
test1_plain.txt      vs test2_plain.txt:             0 lines differ
test1_dfcc.txt       vs test2_dfcc.txt:            324 lines differ
test1_dfcc_plain.txt vs test2_dfcc_plain.txt:        0 lines differ
SMT files:        8 lines differ

The first significant difference appears to be in the test1_dfcc.txt vs test2_dfcc.txt diff ... e.g. we see

18c18
<         // 182 file <builtin-library-__CPROVER_contracts_library> line 1147 function __CPROVER_contracts_link_deallocated
---
>         // 180 file <builtin-library-__CPROVER_contracts_library> line 1147 function __CPROVER_contracts_link_deallocated

What is the significance of the first number on those lines - e.g. the 182 changing to 180 ??

With the comments removed (filtering out lines starting with "// "), the "plain" GOTO listings appear to be essentially identical.

[rod-chapman]

Or possibly, there is a significant difference between the GOTO files, but goto-instrument --show-goto-functions is not showing it...

[hanno-becker]

@remi-delmas-3000 @tautschnig Any insight?

[tautschnig]

Commenting in here for completeness what has already been said in out-of-band communication: the formulae sent to the SMT solver are equisatisfiable, but declarations appear in a different order. That order is determined by iterations over hash maps, which means CBMC's operation is deterministic for a given platform and input, but the hash values can change when the input changes (including changes in line numbers). We need to better understand why the SMT solver is sensitive to such changes in the input.

We could certainly stabilise the order of iteration, but without further study of what order is best for the SMT solver we might just the cementing the status-quo rather than producing an actually optimal (in terms of solving time) ordering.

Also, this problem is likely strongly tied to the use of quantifiers, and we have ongoing (as far as time permits) work to avoid sending quantified formulae to the solver in the first place. My opinion is that this is the actual way to address the problem instead of putting up more workarounds.

[hanno-becker]

I don't know the internals, obviously, but to me the more natural first step here is to stabilize the SMT under irrelevant changes such as empty lines, rather than trying to understand how specific solvers deal with changes in SMT. The latter is ultimately out of CBMC's control, while the former is fully in its hand.

Also, this problem is likely strongly tied to the use of quantifiers, and we have ongoing (as far as time permits) work to avoid sending quantified formulae to the solver in the first place. My opinion is that this is the actual way to address the problem instead of putting up more workarounds.

I tried the quantifier-elimination branch on mlkem-native, but its performance seemed worse than the status-quo. So I don't have confidence yet that this will be a viable approach -- at least for our application.

[rod-chapman]

We do need to urgently unblock mldsa-native ASAP. In my experience, such stability problems should always be fixed as close to the point-of-introduction as possible. We should not try to "fix" Z3 to cope with instability introduced by goto-instrument, for example.