Handle External Dependencies

Real code calls libraries. It calls services. It calls math.exp. A model that required all of that to be formalised first would never get built, so IML gives you three ways to stand in for what you have not modelled. This guide covers choosing between them, and the syntax for each.

The choice is not cosmetic: it decides what your proofs actually mean, and whether the model can generate tests at all.

Opaque functions: a signature and nothing else

An opaque function is one ImandraX knows the type of and nothing more. Declare it and you can call it, type-check against it, and prove properties about code that uses it. The reasoning will assume nothing whatsoever about what happens inside.

(* `random` stands in for a library function we have not modelled. ImandraX
   knows only its type: it says nothing about which value comes back. *)
let random : int -> real = fun _seed -> 0.0 [@@opaque]
 
let bucket (seed : int) : int =
  let a = random seed in
  if a >. 0.4 then 1
  else if a >=. 0.0 then 2
  else 3
 
(* Provable with no assumptions at all: the branches cover every real. *)
verify (fun seed -> let t = bucket seed in t = 1 || t = 2 || t = 3)
 
(* Not provable: nothing rules out a negative draw, so bucket can return 3. *)
verify (fun seed -> let t = bucket seed in t = 1 || t = 2)

$ codelogician eval check-vg opaque.iml
eval_res: Success
vg_res_list:
- vg_req_index: 0
  kind: verify
  src: fun seed -> let t = bucket seed in t = 1 || t = 2 || t = 3
  vg_res:
    proved:
      proof_pp: |-
        { id = 1;
          concl =
 
          |----------------------------------------------------------------------
           (bucket seed =<int> 1)
           || ((bucket seed =<int> 2) || (bucket seed =<int> 3))
          ;
          view =
          T_ded
        … (328 more chars omitted)
- vg_req_index: 1
  kind: verify
  src: fun seed -> let t = bucket seed in t = 1 || t = 2
  vg_res:
    refuted:
      model:
        m_type: Counter_example
        src: |
          module M = struct
 
            let seed = 0
            let random (x_0:int) = (-1.0)
          end
 

The two results are worth comparing closely.

The first goal, that bucket returns 1, 2 or 3, is proved with no assumptions at all. It has to be: the three branches between them cover every real number, whatever random returns.

The second goal, that bucket returns 1 or 2, is refuted. The counterexample is the interesting part:

let seed = 0
let random (x_0:int) = (-1.0)

ImandraX did not find an input that breaks the property. It invented an implementation of random that breaks it: one returning -1.0. Since nothing in the model rules that out, it is a legitimate counterexample. This is the precise meaning of an opaque function: any claim about code that uses it is quantified over every possible implementation of that signature.

Which makes opaqueness useful and dangerous in the same breath. A proof over an opaque function is very strong, because it holds no matter what the dependency does. But a refutation may be telling you nothing about your system, only that you have not said enough about your dependency yet.

A further consequence: a model containing opaque functions is not executable, so it cannot produce test cases. See Autoformalization for why this matters to the workflow.

Axioms: stating the assumption you are already making

You know something about random that its type does not capture: the draw lands in [0, 1]. An axiom records exactly that, and no more:

let random : int -> real = fun _seed -> 0.0 [@@opaque]
 
(* Our assumption about the library: the draw lands in [0, 1]. *)
axiom in_unit_interval seed = random seed >=. 0.0 && random seed <=. 1.0
 
let bucket (seed : int) : int =
  let a = random seed in
  if a >. 0.4 then 1
  else if a >=. 0.0 then 2
  else 3
 
(* Now provable: the axiom rules out the negative draw. *)
verify (fun seed -> let t = bucket seed in t = 1 || t = 2)
  [@@by [%use in_unit_interval seed] @> auto]

$ codelogician eval check-vg opaque-axiom.iml
eval_res: Success
vg_res_list:
- vg_req_index: 0
  kind: verify
  src: fun seed -> let t = bucket seed in t = 1 || t = 2
  vg_res:
    proved:
      proof_pp: |-
        { id = 6;
          concl =
 
          |----------------------------------------------------------------------
           (bucket seed =<int> 1) || (bucket seed =<int> 2)
          ;
          view =
          T_deduction {
            premises =
            [("
        … (4366 more chars omitted)
 

The previously-refuted goal is now proved. The -1.0 implementation has been excluded, so the third branch is unreachable and bucket can only return 1 or 2.

Two things to keep in mind. First, the axiom has to be invoked explicitly, with [@@by [%use in_unit_interval seed] @> auto]. It is not assumed globally, so nothing changes for goals that do not use it. Second, an axiom is an assumption, not a fact: ImandraX takes your word for it. Write a false axiom and you can prove anything at all. An axiom is best read as a written-down claim about the outside world that someone could check independently, which is more than the implicit version most code ships with.

Approximations: standing in for the mathematically awkward

Most of the time a good approximation beats an assumption, because it makes the model executable again, which brings test generation back.

Some functions resist reasoning not because they are external but because of what they are. Trigonometric and exponential functions are the standard case. The usual approach is a truncated Taylor expansion:

let sin (x : real) =
    (* Truncated Taylor series approximation of `sin` for n=5 *)
    x -.
    (x *. x *. x) /. 6.0 +.
    (x *. x *. x *. x *. x) /. 120.0 -.
    (x *. x *. x *. x *. x *. x *. x) /. 5040.0 +.
    (x *. x *. x *. x *. x *. x *. x *. x *. x) /. 362880.0 -.
    (x *. x *. x *. x *. x *. x *. x *. x *. x *. x *. x) /. 39916800.0

This is not sin. It is a polynomial that agrees with sin closely near zero and diverges as x grows. Everything proved about a model using it is a statement about the polynomial. Whether that transfers to the real system depends on the input range you care about. Make that judgement deliberately, and write it down next to the approximation.

CodeLogician ships approximations for common functions, and you can substitute your own.

Choosing between the three

The usual progression is downward through that table. Start opaque, because it costs nothing and any proof you get is unconditionally strong. Add axioms when a refutation turns out to be an artefact of saying too little. Reach for an approximation when you want test cases, and then be explicit about the range it is good over.

Next

• Generate test cases: what becomes possible once the model is executable
• Opaque functions reference
• Verification with verify and instance
• Autoformalization: model status, and why executability gates test generation