Fix distinct unsoundness #890

Halbaroth · 2023-10-13T15:27:52Z

This PR quickly fixes the clash between the SMT-LIB specification of distinct and the implementation of this expression in AE.

Basically, we expand the expression distinct x_1 ... x_n into a conjunction of binary disequalities.

Notice that the model outputted for uf2.models.smt2 changes because I don't preserve the old order used in distinct.

Fix issue #889 for the v2.5.x branch.

This PR quickly fixes the clash between the SMT-LIB specification of `distinct` and the implementation of this expression in AE. Basically, we expand the expression `distinct x_1 ... x_n` into a conjunction of binary disequalities. Notice that the model outputted for `uf2.models.smt2` changes because I don't preserve the old order used in `distinct`. This fix doesn't change the smart constructor `mk_distinct`. We shouldn't change the API on the branch v2.5.x and I add a comment to advertise the user that this smart constructor doesn't behave as expected.

bclement-ocp · 2023-10-13T16:08:05Z

This fix doesn't change the smart constructor mk_distinct. We shouldn't change the API on the branch v2.5.x and I add a comment to advertise the user that this smart constructor doesn't behave as expected.

I disagree on this point. mk_distinct is supposed to build a distinct term; even if the API is undocumented, the intent (as expressed by the name mk_distinct) is clear to any reasonable user. mk_distinct not building a an "all-distinct" term is the bug that should be fixed.

(One other way to think about it: if we have a function mk_plus that actually created a multiplication, we would fix it in the function itself, we would not add workarounds)

Halbaroth · 2023-10-13T16:21:45Z

Besides, I checked that the constructor TANeq of the legacy parser is never used with a list of at least three elements.

The smart construct `mk_distinct` produces an SMT-LIB compliant expression.

bclement-ocp

even if the API is undocumented

It actually is: https://ocamlpro.github.io/alt-ergo/Input_file_formats/Native/02_types/02_01_builtin.html#comparisons

Please remove the cleanups that have no place in a hotfix and it should be good.

bclement-ocp · 2023-10-16T07:24:49Z

src/lib/structures/expr.ml

+  (* This fix makes sure that the smart constructor agrees with
+     the SMT-LIB specification when used with at least 3 arguments.
+     To prevent a soundness bug, we translate the expected expression into a
+     conjonction of binary disequations. *)


Note: this is not specifically related to the SMT-LIB specification but to the usual definition of distinct.

Also the comment should point to #889 which will track the fix in the next branch

Actually I didn't plan to apply this patch on next but I can.

Sorry, I maybe was not clear. #889 is not about this patch, #889 is about the issue with distinct. We don't need to apply the patch on next. We will fix the issue with distinct on next in a different way, which is fine, but we should still refer to it here.

bclement-ocp · 2023-10-16T07:37:48Z

src/lib/structures/expr.ml

+  let args = Array.of_list args in
+  let acc = ref vrai in
+  for i = 0 to Array.length args - 1 do
+    for j = i + 1 to Array.length args - 1 do
+      acc :=
+        mk_and (neg (mk_eq ~iff args.(i) args.(j))) !acc false
+    done;
+  done;
+  !acc


Nit: it doesn't really matter here as this is a hotfix but conversion to an array is not needed:

let distinct_from x acc ys = List.fold_left (fun acc y -> mk_and (neg (mk_eq ~iff x y)) acc) acc ys in let rec distinct_aux acc = function | [] -> acc | x :: ys -> distinct_aux (distinct_from x acc ys) ys in distinct_aux acc args

I know but I think the imperative version is the easier to read and a bit less error-prone. It's a matter of taste.

It is not only a matter of taste (I also find the imperative version easier to read in this specific case); the imperative version is slower and uses more memory because of the call to Array.of_list. It is entirely negligible here (hence why it's a nit), just pointing that out.

bclement-ocp · 2023-10-16T07:49:04Z

src/lib/frontend/cnf.ml

+        | TAneq lt ->
          let lt = List.map (make_term up_qv name_base) lt in
          E.mk_distinct ~iff:true lt
+
+        | TAdistinct lt ->
+          E.mk_distinct ~iff:true (List.map (make_term up_qv name_base) lt)
+


Can we avoid these changes? They don't seem useful, and keeping the patch as tiny as possible makes it easier to cherry-pick and move around if needed.

Sure. Besides, we should use a different constructor for TAneq? It's not documented and I'm not sure what is the expected semantic for this constructor.

TAneq [x; y] is the constructor used for x <> y. "neq" is a fairly common shorthand for "not equal".

bclement-ocp · 2023-10-16T07:49:36Z

src/lib/frontend/d_cnf.ml

@@ -1337,7 +1337,7 @@ let rec mk_expr
            end

          | B.Distinct, _ ->
-            E.mk_distinct ~iff:true (List.map (fun t -> aux_mk_expr t) args)
+            E.mk_distinct ~iff:true (List.map aux_mk_expr args)


Same as above, can we undo this? There shouldn't be this sort of unrelated cleanup in a hotfix.

bclement-ocp · 2023-10-16T08:22:36Z

src/lib/frontend/cnf.ml

@@ -242,6 +242,7 @@ and make_form up_qv name_base ~toplevel f loc ~decl_kind : E.t =
        | TAneq lt | TAdistinct lt ->
          let lt = List.map (make_term up_qv name_base) lt in
          E.mk_distinct ~iff:true lt
+


Can you undo this whitespace change? Thanks.

Stevendeo

LGTM!

EDIT: I still had the notification to review the PR after it was merged

Halbaroth · 2023-10-19T10:11:32Z

:D

Halbaroth added the 💣 soundness label Oct 13, 2023

Halbaroth added this to the 2.5.2 milestone Oct 13, 2023

Halbaroth requested review from bclement-ocp and Stevendeo October 13, 2023 15:28

Halbaroth force-pushed the distinct-soundness branch 2 times, most recently from 83e7d92 to e81c18a Compare October 13, 2023 15:36

Halbaroth force-pushed the distinct-soundness branch from b164013 to c55c086 Compare October 13, 2023 16:23

Fix the smart constructor of mk_distinct

c55c086

The smart construct `mk_distinct` produces an SMT-LIB compliant expression.

bclement-ocp requested changes Oct 16, 2023

View reviewed changes

Halbaroth force-pushed the distinct-soundness branch from 634f3c9 to 2e9667e Compare October 16, 2023 08:19

Halbaroth requested a review from bclement-ocp October 16, 2023 08:19

bclement-ocp requested changes Oct 16, 2023

View reviewed changes

Halbaroth force-pushed the distinct-soundness branch from 2e9667e to af20710 Compare October 16, 2023 08:26

Halbaroth requested a review from bclement-ocp October 16, 2023 08:26

Clean up

af20710

bclement-ocp approved these changes Oct 16, 2023

View reviewed changes

Halbaroth merged commit 64ad841 into OCamlPro:v2.5.x Oct 16, 2023
10 checks passed

This was referenced Oct 18, 2023

The distinct expression clashes with the SMT-LIB specification #889

Closed

[new release] alt-ergo (4 packages) (2.5.2) ocaml/opam-repository#24641

Merged

Stevendeo reviewed Oct 18, 2023

View reviewed changes

bclement-ocp mentioned this pull request Jul 11, 2024

Native support for distinct #1157

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Fix distinct unsoundness #890

Fix distinct unsoundness #890

Halbaroth commented Oct 13, 2023 •

edited

Loading

bclement-ocp commented Oct 13, 2023

Halbaroth commented Oct 13, 2023

bclement-ocp left a comment

bclement-ocp Oct 16, 2023

bclement-ocp Oct 16, 2023

Halbaroth Oct 16, 2023

bclement-ocp Oct 16, 2023 •

edited

Loading

Halbaroth Oct 16, 2023

bclement-ocp Oct 16, 2023

Halbaroth Oct 16, 2023

bclement-ocp Oct 16, 2023

Halbaroth Oct 16, 2023

bclement-ocp Oct 16, 2023

Halbaroth Oct 16, 2023

bclement-ocp Oct 16, 2023

bclement-ocp Oct 16, 2023

bclement-ocp Oct 16, 2023

Stevendeo left a comment •

edited

Loading

Halbaroth commented Oct 19, 2023

Fix distinct unsoundness #890

Fix distinct unsoundness #890

Conversation

Halbaroth commented Oct 13, 2023 • edited Loading

bclement-ocp commented Oct 13, 2023

Halbaroth commented Oct 13, 2023

bclement-ocp left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

bclement-ocp Oct 16, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Stevendeo left a comment • edited Loading

Choose a reason for hiding this comment

Halbaroth commented Oct 19, 2023

Halbaroth commented Oct 13, 2023 •

edited

Loading

bclement-ocp Oct 16, 2023 •

edited

Loading

Stevendeo left a comment •

edited

Loading