Potential soundness issues in the interval module

[bclement-ocp]

Consider the following program.

let () =
  Options.set_debug_explanations true;
  Options.set_verbose true;
  let fresh q =
    Ex.singleton @@
    Ex.Dep (Expr.mk_term (Sy.Real q) [] Tbool)
  in
  let interval lo hi =
    new_borne_sup Ex.empty hi ~is_le:true @@
    new_borne_inf Ex.empty lo ~is_le:true @@
    undefined Tint
  in
  let sinterval lo hi =
    new_borne_sup (fresh hi) hi ~is_le:false @@
    new_borne_inf (fresh lo) lo ~is_le:false @@
    undefined Tint
  in
  let a = interval (Q.of_int 0) (Q.of_int 12) in
  let a = exclude (sinterval (Q.of_int 4) (Q.of_int 8)) a in
  Format.printf "a: %a@." pretty_print a;

  let b = interval (Q.of_int (20)) (Q.of_int (34)) in
  let b = exclude (sinterval (Q.of_int 24) (Q.of_int 32)) b in
  Format.printf "b: %a@." pretty_print b;

  let a_plus_b = add a b in
  Format.printf "a + b: %a@." pretty_print a_plus_b;

  let _ =
    try ignore @@ intersect a_plus_b (point (Q.of_int (31 + 8)) Treal Ex.empty) with
    NotConsistent ex -> Format.printf "FAIL: %a@." Ex.print ex; assert false
  in
  ()

This is code that only uses API exposed by the Intervals module (no internal API). My understanding based on these (undocumented) API calls is that this should encode the problem:

a in [0, 12]
Dep:4 /\ Dep:8 -> a not in [4, 8]
b in [20, 34]
Dep:24 /\ Dep:32 -> b not in [24, 32]

but it prints:

a: [0 {};4 {{Dep:4}}] U [8 {{Dep:8}};12 {}] {}
b: [20 {};24 {{Dep:24}}] U [32 {{Dep:32}};34 {}] {}
a + b: [20 {};38 {{Dep:4}}] U [40 {{Dep:8}{Dep:32}};46 {}] {}
FAIL: {{Dep:8}{Dep:4}{Dep:32}}

Notice that the dep for 24 is not included. But both Dep:24 and Dep:32 are required to exclude 31 from the domain of b (at least under my understanding of the meaning assigned to explanations…), and so it does not follow that this is a valid conflict.

--

This example is a bit tricky, and I couldn't find a reproducer in an input format. It seems to require having internal bounds with different explanations, which I had to bend the (public) functions of the module to construct. I am not sure this is really a requirement, maybe we could trigger the issue with two separate holes with different explanations, and that we might be able to construct in SMT-LIB; I just didn't dig that far.

In any case, this is still a problem: I can't make sense of this output, so there must be one of the calls above that is invalid and broke an invariant of the module, and i can't figure out which one (it doesn't help that the module is so poorly documented). This makes it hard to reason about what we can and cannot do with intervals outside of the module, let alone inside.

The core of the issue here is that the intervals obtained from [0, 4] + [20, 24] = [20, 28], [0, 4] + [32, 34] = [32, 38] and [8, 12] + [20, 24] = [28, 36] are merged and only the last explanation (from 4 + 34) is kept, but the others are still relevant and can allow values in [38, 40] (as the 8 + 31 example shows). If we use smaller intervals, all the explanations end up in the conflict (which I believe is correct, or at least I can make sense of):

a: [0 {};2 {{Dep:2}}] U [10 {{Dep:10}};12 {}] {}
b: [20 {};24 {{Dep:24}}] U [32 {{Dep:32}};34 {}] {}
a + b: [20 {};26 {{Dep:2}{Dep:24}}] U [30 {{Dep:10}};36 {{Dep:2}}] U [42 {{Dep:
10}{Dep:32}};46 {}] {}
FAIL: {{Dep:2}{Dep:10}{Dep:24}{Dep:32}}

Ultimately, we can trace this to the union_intervals function that can "forget" explanations in certain cases (typically in cases with a combination of small and large intervals).

I would consider this a soundness bug even though we don't have a reproducer; as stated above, it makes invariants of the Intervals API depend on details of the internal representation and as such code hard to reason about. I have started working on a re-implementation of the module in Coq (because I found through investigating this that I otherwise just couldn't trust my reasoning here).