Imandra decomposition flags

In this notebook we'll go over various important flags and arguments accepted by Imandra's Decompose.top entrypoint into its Principal Region Decomposition machinery. As much as possible, we'll use concrete examples to clarify their behaviour.

Assuming

The ~assuming flag is used to add extra axioms as a side-condition to the decomposition of target function. This usually has the effect that regions that don't satisfy the side-condition will be pruned away (although it is not always the case when in presence of non-interpreted functions, see aggressive_rec for a mitigation) but it can also cause constraints to be pruned away or new regions to be discovered when used in combination with ctx_asm_simp.

The side-condition function must be a boolean predicate accepting the same arguments as the target function.

Let's see how it works:

In [1]:
let f x y = 
  if x > 0 then
    if x > y then
      Some (x - y)
    else
      Some (y - x)
  else
    None
    
let g x (y : int) = x > 0
Out[1]:
val f : int -> int -> Z.t option = <fun>
val g : int -> int -> bool = <fun>

Let's assume we only care to decompose feasible paths of f when g holds (i.e. when x > 0):

In [2]:
Decompose.top ~assuming:"g" "f"
Out[2]:
- : Imandra_reasoning.Decompose.t list = [<region>; <region>]
Regions details
No group selected.
ConstraintsInvariant
  • not (x <= 0)
  • not (x <= y)
F = Some (x + -1 * y)
  • not (x <= 0)
  • x <= y
F = Some (y + -1 * x)

As we can see, the call to Decompose.top pruned away the region where g didn't hold.

Compound

The ~compound flag instructs Imandra whether or not to expand compound logical statements in conditionals, such as conjunctions and disjunctions, into their constituent parts. With ~compound:true, the decomposition may in general be possible with fewer regions than otherwise, but region constraints and invariants may involve && and ||. This flag doesn't cause any constraints to be removed.

By default, ~compound:false is used.

Let's see how ~compound works in practice on a target function with a compound conditional:

In [3]:
let f x y =
  if x > 10 || y < 20 then
    1
  else
    2
Out[3]:
val f : int -> int -> Z.t = <fun>

If we decompose f with ~compound:false, we'll get 3 different regions:

In [4]:
Decompose.top ~compound:false "f"
Out[4]:
- : Imandra_reasoning.Decompose.t list = [<region>; <region>; <region>]
Regions details
No group selected.
ConstraintsInvariant
  • x <= 10
  • 20 <= y
F = 2
  • x <= 10
  • not (20 <= y)
F = 1
  • not (x <= 10)
F = 1

Though all regions are disjoint, we can see that two regions have the same invariant and could be logically collapsed into just one region with a disjunctive constraint. (Hint: click on a region in the Voronoi diagram to see the region's constraints and invariant.) This is where ~compound:true helps us:

In [5]:
Decompose.top ~compound:true "f"
Out[5]:
- : Imandra_reasoning.Decompose.t list = [<region>; <region>]
Regions details
No group selected.
ConstraintsInvariant
  • x <= 10
  • 20 <= y
F = 2
  • not (x <= 10) || not (20 <= y)
F = 1

Note that ~compound:true doesn't simply operate on literal &&'s and ||'s in code, but is more general, taking the boolean meaning of nested if statements into account.

Reduce symmetry

The flag ~reduce_symmetry is like ~compound in the sense that it is used to reduce the number of regions output by a decomposition, but through very different means.

This flag is only meaningful when used in combination with side-conditions (assuming), and behaves like a no-op when no-side conditions are present.

When side-conditions are present and reduce_symmetry is true, Imandra uses the information it has been given by the assuming function to find and merge symmetric regions. At a high level, symmetric regions are regions that share some control flow paths which, modulo the assumptions, can be seen to behave identically and thus can be merged.

This flag can cause constraints to be eliminated, so it should be used only when decomposing as means of finding possible behavioural regions rather than as a way to get at all the possible execution paths of a function.

Let's see how this works in practice:

In [6]:
let f x y =
  if x + y = 10 then
    1
  else if x > y then
    1
  else
    2
Out[6]:
val f : int -> int -> Z.t = <fun>

For this particular example (with no compound conditionals), the setting of ~compound is immaterial, so for the sake of demonstrating the behaviour of ~reduce_symmetry:true, we'll decompose with the default ~compound:false setting. Note that in general, with more complex target and side-condition functions than the ones we use here as examples, it is not in general true that ~compound:true subsumes ~reduce_symmetry:true.

If we try to decompose f, we see that we get 3 different regions, as expected, corresponding to the three different branches.

In [7]:
Decompose.top "f"
Out[7]:
- : Imandra_reasoning.Decompose.t list = [<region>; <region>; <region>]
Regions details
No group selected.
ConstraintsInvariant
  • not (x + y = 10)
  • x <= y
F = 2
  • not (x + y = 10)
  • not (x <= y)
F = 1
  • x + y = 10
F = 1

Let's now try to insert a side condition g that simply states that x is always bigger than y:

In [8]:
let g (x:int) y = x > y;;

Decompose.top ~assuming:"g" "f"
Out[8]:
val g : int -> int -> bool = <fun>
- : Imandra_reasoning.Decompose.t list = [<region>; <region>]
Regions details
No group selected.
ConstraintsInvariant
  • not (x + y = 10)
  • not (x <= y)
F = 1
  • x + y = 10
F = 1

We've now excluded the third region, as we've asserted that it is never the case that x<=y.

However if we look carefully, we'll notice that both remaining regions have invariants that don't depend on the region constraints, thus if we're doing a decomposition just to analyze all the possible states our f can be in and not to get a concrete listing of all the possible paths through f, we'd like for this decomposition to collapse both regions into one.

In other words, we'd like imandra to understand that for our purposes, f could have been written instead like:

In [9]:
let f x y =
  if x <= y then
    2
  else
    1
Out[9]:
val f : int -> int -> Z.t = <fun>

This is where ~reduce_symmetry:true helps us:

In [10]:
Decompose.top ~assuming:"g" ~reduce_symmetry:true "f"
Out[10]:
- : Imandra_reasoning.Decompose.t list = [<region>]
Regions details
No group selected.
ConstraintsInvariant
    F = 1

    As you can see, not only did ~reduce_symmetry:true collapse both regions into one, but it also figured out that there are actually no constraints to be held true for this regions's invariant to hold, since all possible values of x and y will cause f x y to evaluate to 1, as we've restricted the functions' domain in the side-condition.

    For the curious, this is one of the big differencies between ~reduce_symmetry:true and ~compound:true in this case, as ~compound:true would've merged the two regions and had the constraints in a logical disjunction, but wouldn't have figured out that it could just as well remove the constraints altogether as they always hold true from the side-condition:

    In [11]:
    Decompose.top ~assuming:"g" ~compound:true "f"
    
    Out[11]:
    - : Imandra_reasoning.Decompose.t list = [<region>]
    
    Regions details
    No group selected.
    ConstraintsInvariant
    • not (x <= y)
    F = 1

    Ctx_asm_simp

    ~ctx_asm_simp is yet another flag that deals with trying to reduce the number of regions and improve performance. It instructs Imandra whether or not to take the side-conditions into accound when doing a pre-processing step of contextually simplifying the target function. When no side condition is present this is equivalent to a no-op.

    When set to true, this can help Imandra simplify some more state space away and make decomposition faster and produce less regions, however it is also possible that this will cause Imandra to spend a lot more time doing simplification and might even cause more regions to be produced, so careful consideration is needed before enabling this.

    Let's see how this flag works in practice:

    In [12]:
    let f x (y:int) =
      if y > 0 then
        if x > y  then
          1
        else
          2
      else
        if x < 0 then
          3
        else
          2
    
    Out[12]:
    val f : int -> int -> Z.t = <fun>
    

    If we decompose f we get all 4 regions, as expeted:

    In [13]:
    Decompose.top "f"
    
    Out[13]:
    - : Imandra_reasoning.Decompose.t list =
    [<region>; <region>; <region>; <region>]
    
    Regions details
    No group selected.
    ConstraintsInvariant
    • not (y <= 0)
    • not (x <= y)
    F = 1
    • not (y <= 0)
    • x <= y
    F = 2
    • y <= 0
    • not (0 <= x)
    F = 3
    • y <= 0
    • 0 <= x
    F = 2

    If we then introduce a side-condition g making the first and third branches unreachable:

    In [14]:
    let g x y =
      x + y = 1;;
      
    Decompose.top ~assuming:"g" "f";;
    
    Out[14]:
    val g : Z.t -> Z.t -> bool = <fun>
    - : Imandra_reasoning.Decompose.t list = [<region>; <region>]
    
    Regions details
    No group selected.
    ConstraintsInvariant
    • not (y <= 0)
    • x <= y
    F = 2
    • y <= 0
    • 0 <= x
    F = 2

    The 2 unreachable branches are correctly filtered out by the side-condition. However we notice that both feasabile paths have the same invariant and we would like to collapse them into a single region.

    Let's see how ~ctx_asm_simp:true helps us here:

    In [15]:
    Decompose.top ~compound:false ~ctx_asm_simp:true ~assuming:"g" "f"
    
    Out[15]:
    - : Imandra_reasoning.Decompose.t list = [<region>]
    
    Regions details
    No group selected.
    ConstraintsInvariant
      F = 2

      By letting Imandra use the side-condition while doing simplification, it can then realize there is just one possible behaviour for f given the side-condition g, and collapse the two regions.

      Max_ctx_simp

      ~max_ctx_simp is a numeric value (defaults to 100) which tells Imandra how "deep" to simplify conditional statements into separate regions. A higher number will mean that Imandra will spend more time trying to "simplify" the target function, which can lead to faster or better decomposition, but a value too high might also make Imandra work too hard trying to simplify a target function that would be more easily decomposed with a less deep simplification.

      In practice you'll very rarely need to tweak this flag.

      Basis

      ~basis is an optional list of functions that we want Imandra to leave opaque (i.e., disabled or uninterpreted). There are two main reasons for wanting to do this:

      • Abstraction fence: Function symbols in the basis will give a logical vernacular for describing regions and invariants. This is very similar to the use of disabled function symbols in Imandra theorem proving.

        A typical example: Consider a "date/time comparison" function Datetime.(<=) which is used in an IML model. If this comparison function is complex with many branches (comparing year, month, day, hour, minute, etc.), these constraints may pollute your decomposition with a huge number of regions ultimately describing "every possible way" one can have, e.g., Datetime.(x <= y) and this may obscure the meaning of the various regions. Instead, if we add Datetime.(<=) to the basis, then its definition will not be expanded and it can appear atomically in constraints and invariants. There are also ways to make use of Imandra rewrite rules and other lemmas, so that various exposed properties of the basis functions are respected (and contribute to simplification) during decomposition, culimatining in the use of interpret_basis (described below).

      • Performance/region space: When the interpretation of a function is too expensive (many branches, lots of complex nonlinear arithmetic), we may want to tell imandra to avoid interpreting it

      Note that putting certain functions in ~basis may actually cause a higher number of regions to be computed and much more deeply nested branches to be analyzed, thus also causing performance issues and having the exactly opposite effect than what desired, so be very careful and thoughtful about putting functions in ~basis. There are also correctness issues that can arise, see ~interpret-basis

      Let's see how this flag works in practice:

      In [16]:
      type my_num = Real of real | Int of int | NaN
      
      let add x y =
        match x, y with
        | Real f1, Real f2 -> Real (f1 +. f2)
        | Int i1, Int i2 -> Int (i1 + i2)
        | _, _ -> NaN
      
      let is_pos x =
        match x with
        | Real f -> f >. 0.0
        | Int i -> i > 0
        | NaN -> false
      
      let f x y =
        if is_pos (add x y) then
          1
        else
          2
      
      Out[16]:
      type my_num = Real of real | Int of int | NaN
      val add : my_num -> my_num -> my_num = <fun>
      val is_pos : my_num -> bool = <fun>
      val f : my_num -> my_num -> Z.t = <fun>
      

      Let's try to decompose f without anything in basis:

      In [17]:
      Decompose.top "f"
      
      Out[17]:
      - : Imandra_reasoning.Decompose.t list =
      [<region>; <region>; <region>; <region>; <region>; <region>; <region>]
      
      Regions details
      No group selected.
      ConstraintsInvariant
      • not Is_a(Real, y)
      • not Is_a(Int, y)
      F = 2
      • not Is_a(Real, y)
      • Is_a(Int, y)
      • not Is_a(Int, x)
      F = 2
      • not Is_a(Real, y)
      • Is_a(Int, y)
      • Is_a(Int, x)
      • (Destruct(Int, 0, x) + Destruct(Int, 0, y)) <= 0
      F = 2
      • not Is_a(Real, y)
      • Is_a(Int, y)
      • Is_a(Int, x)
      • not ((Destruct(Int, 0, x) + Destruct(Int, 0, y)) <= 0)
      F = 1
      • Is_a(Real, y)
      • not Is_a(Real, x)
      • not Is_a(Int, y)
      F = 2
      • Is_a(Real, y)
      • Is_a(Real, x)
      • (Destruct(Real, 0, x) +. Destruct(Real, 0, y)) <=. 0
      F = 2
      • Is_a(Real, y)
      • Is_a(Real, x)
      • not ((Destruct(Real, 0, x) +. Destruct(Real, 0, y)) <=. 0)
      F = 1

      As we can see decomposition for our f explodes because of the branching in is_pos and add, we can imagine the number of regions getting much larger as we support summation between Float and Int for example.

      Let's see how ~basis helps us here:

      In [18]:
      Decompose.top ~basis:["add";"is_pos"] "f"
      
      Out[18]:
      - : Imandra_reasoning.Decompose.t list = [<region>; <region>]
      
      Regions details
      No group selected.
      ConstraintsInvariant
      • not (is_pos (add x y))
      F = 2
      • is_pos (add x y)
      F = 1

      By putting add and is_pos in ~basis, we now only get the 2 "logical" regions of behaviour instead of a listing of all the possible code paths.

      Interpret basis

      ~interpret_basis is a flag which tells Imandra whether or not to take the interpretation of the functions in ~basis into account when lifting and when extracting sample values via the Mex module. It only has effect when ~basis is not empty.

      Note that ~interpret_basis cannot be used with recursive functions in basis.

      This flag has a strong effect on correctness when used in decompositions that have side-conditions that use functions in ~basis in branching points, as in the absence of side-conditions, setting this flag to false may cause unreachable regions to be output. Setting ~interpret_basis:false may have significant performance benefits, but could also cause a degradation in performance in certain cases; for those reasons we suggest to always set ~interpret_basis:true unless careful thought is given and the possible issues have been explored and are understood.

      Let's see how this flag works in practice:

      In [19]:
      let gt (x : int) (y : int) = x > y;;
      
      let f x y =
        if gt x y then
          if gt y x then
            1 (* this is unreachable! *)
          else
            2
        else
          3
      
      Out[19]:
      val gt : int -> int -> bool = <fun>
      val f : int -> int -> Z.t = <fun>
      

      If we try to simply decompose f, we get 2 regions:

      In [20]:
      Decompose.top "f"
      
      Out[20]:
      - : Imandra_reasoning.Decompose.t list = [<region>; <region>]
      
      Regions details
      No group selected.
      ConstraintsInvariant
      • not (x <= y)
      F = 2
      • x <= y
      F = 3

      Imandra has correctly figured out that the region with invariant F=1 is not admissible, since it's never the case that x>y && y>x.

      However, if we decide we need gt to be a basis function (for one of the reasions we've described earlier), Imandra doesn't have any visibility into what gt does and thus loses the ability to understand that if gt x y then not (gt y x), and we see that the unreachable region is output anyway:

      In [21]:
      Decompose.top ~basis:["gt"] "f"
      
      Out[21]:
      - : Imandra_reasoning.Decompose.t list = [<region>; <region>; <region>]
      
      Regions details
      No group selected.
      ConstraintsInvariant
      • not (gt x y)
      F = 3
      • gt x y
      • not (gt y x)
      F = 2
      • gt x y
      • gt y x
      F = 1

      If however, we set ~interpret_basis:true, Imandra will have visibility into gt at "region feasibility checks" even though it will keep it atomic in the constraints, and thus will be able to prove that gt x y ==> not (gt y x) which is sufficient to exclude that region:

      In [22]:
      Decompose.top ~interpret_basis:true ~basis:["gt"] "f"
      
      Out[22]:
      - : Imandra_reasoning.Decompose.t list = [<region>; <region>]
      
      Regions details
      No group selected.
      ConstraintsInvariant
      • not (gt x y)
      F = 3
      • gt x y
      • not (gt y x)
      F = 2

      Aggressive Recursion

      Sometimes, even ~interpret_basis:true won't be enough, and regions with falsifiable constraints will still be returned. This can be the case for a number of cases where it is not possible to provide an interpretation for a function, for example in the case of a recursive function that cannot be fully unrolled.

      In those cases, ~aggressive_rec:true can help us by applying the full unrolling and simplification machinery used for theorem proving and verification to each region before returning it, this means that we can install theorems as rewrite rules or forward-chaining rules to aid in this process:

      In [23]:
      let rec f x = if x <= 0 then 23 else f (x - 1)
      
      let g x = if f x = 23 then 1 else 2
      
      Out[23]:
      val f : int -> Z.t = <fun>
      val g : int -> Z.t = <fun>
      
      termination proof

      Termination proof

      call `f (x - 1)` from `f x`
      originalf x
      subf (x - 1)
      original ordinalOrdinal.Int (if x >= 0 then x else 0)
      sub ordinalOrdinal.Int (if (x - 1) >= 0 then x - 1 else 0)
      path[not (x <= 0)]
      proof
      detailed proof
      ground_instances1
      definitions0
      inductions0
      search_time
      0.012s
      details
      Expand
      smt_stats
      num checks3
      arith assert lower8
      arith pivots2
      rlimit count87563
      mk clause4
      datatype occurs check2
      mk bool var20
      arith assert upper3
      decisions2
      arith add rows3
      propagations2
      conflicts2
      arith fixed eqs2
      datatype accessor ax2
      arith conflicts1
      final checks1
      added eqs6
      del clause4
      arith eq adapter2
      memory45.470000
      max memory180.650000
      num allocs53819073087.000000
      Expand
      • start[0.012s]
          not (x <= 0)
          && (if x >= 0 then x else 0) >= 0
             && (if (x - 1) >= 0 then x - 1 else 0) >= 0
          ==> (x - 1) <= 0
              || Ordinal.Int (if (x - 1) >= 0 then x - 1 else 0) Ordinal.<<
                 Ordinal.Int (if x >= 0 then x else 0)
      • simplify
        into
        (not
         ((not (x <= 0) && (if x >= 0 then x else 0) >= 0)
          && (if x >= 1 then -1 + x else 0) >= 0)
         || x <= 1)
        || Ordinal.Int (if x >= 1 then -1 + x else 0) Ordinal.<<
           Ordinal.Int (if x >= 0 then x else 0)
        expansions
        []
        rewrite_steps
          forward_chaining
          • unroll
            expr
            (|Ordinal.<<_121| (|Ordinal.Int_112| (ite (>= x_2545 1) (+ (- 1) x_2545) 0))
                              (|Ord…
            expansions
            • unsat
              (let ((a!1 (not (= (ite (>= x_2545 0) x_2545 0) x_2545)))
                    (a!2 (>= (+ (ite (>= x_2545 0) x_254…

            It's quite clear that the only live region of g is the one that returns 1, but if we try to decompose it we see that Imandra doesn't realize that:

            In [24]:
            Decompose.top "g";;
            
            Out[24]:
            - : Imandra_reasoning.Decompose.t list = [<region>; <region>]
            
            Regions details
            No group selected.
            ConstraintsInvariant
            • not (f x = 23)
            F = 2
            • f x = 23
            F = 1

            Let's prove that f x does indeed always return 23 and register the theorem as a rewrite rule:

            In [25]:
            theorem _ x = f x = 23 [@@induct functional f] [@@rw]
            
            Out[25]:
            val _anonymous_theorem_1 : int -> bool = <fun>
            Goal:
            
            f x = 23.
            
            1 nontautological subgoal.
            
            Subgoal 1:
            
            |---------------------------------------------------------------------------
             f x = 23
            
            Verified up to bound 10 (after 0.018s).
            
            Must try induction.
            
            We shall induct according to a scheme derived from f.
            
            Induction scheme:
            
             (x <= 0 ==> φ x) && (not (x <= 0) && φ (x - 1) ==> φ x).
            
            2 nontautological subgoals.
            
            Subgoal 1.2:
            
             H0. x <= 0
            |---------------------------------------------------------------------------
             f x = 23
            
            But simplification reduces this to true, using the definition of f.
            
            Subgoal 1.1:
            
             H0. not (x <= 0)
             H1. f (-1 + x) = 23
            |---------------------------------------------------------------------------
             f x = 23
            
            But simplification reduces this to true, using the definition of f.
            
            
            Proved
            proof
            ground_instances0
            definitions2
            inductions1
            search_time
            0.051s
            Expand
            • start[0.051s, "Goal"] f :var_0: = 23
            • subproof

              f x = 23
              • start[0.051s, "1"] f x = 23
              • induction on (functional f)
                :scheme (x <= 0 ==> φ x) && (not (x <= 0) && φ (x - 1) ==> φ x)
              • Split ((not (x <= 0) || f x = 23)
                       && (not (not (x <= 0) && f (-1 + x) = 23) || f x = 23)
                       :cases [not (x <= 0) || f x = 23;
                               (x <= 0 || not (f (-1 + x) = 23)) || f x = 23])
                • subproof
                  (x <= 0 || not (f (-1 + x) = 23)) || f x = 23
                  • start[0.017s, "1.1"] (x <= 0 || not (f (-1 + x) = 23)) || f x = 23
                  • simplify
                    into
                    true
                    expansions
                    f
                    rewrite_steps
                      forward_chaining
                    • subproof
                      not (x <= 0) || f x = 23
                      • start[0.017s, "1.2"] not (x <= 0) || f x = 23
                      • simplify
                        into
                        true
                        expansions
                        f
                        rewrite_steps
                          forward_chaining

                    That was easy. We can now decompose g using ~aggressive_rec:true and we obtain just one region, as Imandra is able to apply our rewrite rule during simplification:

                    In [26]:
                    Decompose.top "g" ~aggressive_rec:true
                    
                    Out[26]:
                    - : Imandra_reasoning.Decompose.t list = [<region>]
                    
                    Regions details
                    No group selected.
                    ConstraintsInvariant
                      F = 1