Do not use as const with Z3 due to soundness issue#9011
Conversation
tautschnig
requested review from
TGWDB,
kroening,
martin-cs and
peterschrammel
as code owners
There was a problem hiding this comment.
Pull request overview
Disables the SMT2 as const array constant construct for the Z3 backend due to a soundness bug in Z3 (Z3Prover/z3#9550) that causes incorrect results.
Changes:
- Set
use_as_const = falsefor the Z3 solver path insmt2_convt's constructor.
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## develop #9011 +/- ##
===========================================
- Coverage 80.60% 80.59% -0.01%
===========================================
Files 1711 1711
Lines 189454 189472 +18
Branches 73 73
===========================================
- Hits 152712 152710 -2
- Misses 36742 36762 +20 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
|
mlkem-native test results using patched CBMC (and standard Z3 4.15.3) look good. No regressions. A bit slower at K=4, but not too bad. A bit faster for K=2 and K=3. |
|
mldsa-native test results using patched CBMC (and standard Z3 4.15.3) look good. No regressions. A bit faster too for all parameter sets. |
|
I have re-built and re-tested the latest commit on this branch for all parameter set of mlkem-native and mldsa-native. All results are good. Please proceed. |
The DATA_INVARIANT in parse_literal for root-obj expressions required the third element (Z3's 1-based real-root index) to be exactly "1". This is overly restrictive: Z3 chooses any of the polynomial's real roots based on the model it builds, and the chosen root depends on solver state. Concretely, the previous commit on this branch switches Z3 from 'as const' to 'lambda' for array constants. That input change is sufficient to make Z3 pick a different model in regression/cbmc/real-irrational1, where Z3 now returns (root-obj (+ (^ x 2) (- 2)) 2) (the second real root of x^2-2 = 0, i.e. +sqrt(2)) instead of index 1 (-sqrt(2)). CBMC then aborts on the invariant. The result of parsing a root-obj does not depend on the index: algebraic_numbert stores only the polynomial coefficients, not which root is chosen, so the constructed constant_exprt is the same for every index of the same polynomial. Drop the index constraint and document the rationale in the comment above the invariant. Without this change, regression/cbmc/real-irrational1/test.desc fails on the Z3 backend in CI. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
The unflatten() function reconstructs an SMT-array from a bit-vector by storing each element. It previously required `(as const T)` to build the base constant array, which is unavailable when use_as_const is disabled (as done for Z3 in the next commit due to a soundness issue). Replace with a lambda expression `(lambda ((idx T)) elem0)` that produces the same constant-array value without `as const`. Since Z3 rejects `get-value` on terms containing lambdas, also switch from `define-fun` to `declare-fun` + `assert` for SSA symbol definitions when `use_as_const` is false. This makes the symbol opaque to `get-value` while preserving the same logical constraint. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Disable `as const` for Z3 as it produces wrong results per Z3Prover/z3#9550.
|
|
Let's assume that Z3 fixes the underlying soundness problem, and we eventually adopt Z3 4.17.0. Will we revert this fix and go back to "as const" at that point? |
| convert_type(array_type); | ||
| out << ") "; | ||
| } | ||
| else |
There was a problem hiding this comment.
I missed that use_lambda_for_array is true here. Add a comment, or better a DATA_INVARIANT.
| } | ||
| else if(!use_as_const) | ||
| { | ||
| // When `as const` is unavailable, unflatten may emit lambda |
There was a problem hiding this comment.
This may affect solvers that aren't Z3. This needs another branch.
Disable
as constfor Z3 as it produces wrong results per Z3Prover/z3#9550.