Repository navigation
Conversation
lemmy
added
bug
This comment was marked as outdated.
This comment was marked as outdated.
CASE arms are unordered (CHOOSE among enabled results), but both SMT encodings lower CASE to an ordered ite: the default picks the first enabled arm, `--debug oldsmt` the last. Overlapping arms with different results thus yield false proofs. Tests in test/fast/regression, for SMT, Zenon, and Isabelle: - case_proved_test.tla: valid obligations that must be proved. - case_unproved_test.tla: valid obligations a backend does not prove; documents incompleteness and pins current behavior. - case_unsound_test.tla: invalid obligations that must not be proved. Part of #304 See also tlaplus/rfcs#26 Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com> Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
A CASE denotes CHOOSE among the results of its enabled arms; arms are
unordered. Standardize lowered CASE to an ordered ite, so SMT proved
that the first enabled arm wins, e.g. (CASE TRUE -> "u" [] TRUE -> "v")
= "u".
Each arm i but the last now gets an oracle, an uninterpreted Boolean
function case_choice_<n>_<i>_<type> of all guards and results. Arm i
is selected iff p_i /\ (oracle_i \/ ~(p_{i+1} \/ ... \/ p_n)): the
oracles arbitrate between overlapping arms, and since they are
uninterpreted no proof can rely on which arm wins. If exactly one
guard holds, the encoding behaves as the ordered ite; otherwise the
value is still one of the enabled results. Interpreting oracle_i as
[e_i = v], for the CHOOSE'n value v, shows soundness.
Encoding CASE as an opaque term would be sound but would lose disjoint
and OTHER cases, the common use in specs, and whether guards are
disjoint usually depends on hypotheses only the solver sees. With
oracles, SMT proves everything it did before, minus the false proofs.
CASEs that differ in arm count or arm order remain unprovably equal,
as in Zenon.
Before (proved):
(not (= (ite true u (ite true v case_error)) u))
After (not proved):
(declare-fun case_choice_2_1_Idv (Bool Bool Idv Idv) Bool)
(not (= (ite (and true (or (case_choice_2_1_Idv true true u v)
(not true)))
u
(ite true v case_error))
u))
The --debug oldsmt encoding is unchanged and still unsound.
Part of #304
See also tlaplus/rfcs#26
Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
Member
Author
|
@muenchnerkindl This PR could fix the old SMT encoding, but it currently doesn't. Given the other known issues with that encoding (e.g., #306), I'm not sure it's worth fixing. Conceptually, the proposed fix seems reasonable to me, but someone with more OCaml expertise should probably review the implementation. |
lemmy
marked this pull request as ready for review
October 14, 2026 23:37
This branch has not been deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
#304