Commands

Imandra has a number of powerful verification commands:

  • verify <upto> <func>: takes a function representing a goal and attempts to prove it. If the proof attempt fails, Imandra will try to synthesize a concrete counterexample illustrating the failure. Found counterexamples are installed by Imandra in the CX module. When verifying a formula that doesn't depend on function parameters, verify (<expr>) is a shorthand for verify (fun () -> <expr>). If <upto> is provided as one of ~upto:<n> or ~upto_bound:<n>, verification will be bound by unrolling limits.

  • instance <upto> <func>: takes a function representing a goal and attempts to synthesize an instance (i.e., a concrete value) that satisfies it. It is useful for answering the question "What is an example value that satisfies this particular property?". Found instances are installed by Imandra in the CX module. If <upto> is provided as one of ~upto:<n> or ~upto_bound:<n>, instance search will be bound by unrolling limits.

  • theorem <name> <vars> = <body>: takes a name, variables and a function of the variables representing a goal to be proved. If Imandra proves the goal, the named theorem is installed and may be used in subsequent proofs. Theorems can be tagged with attributes instructing Imandra how the theorem should be (automatically) applied to prove other theorems in the future. Found counterexamples are installed by Imandra in the CX module.

  • lemma <name> <vars> = <body>: synonym of theorem, but idiomatically often used for "smaller" subsidiary results as one is working up to a larger theorem.

  • axiom <name> <vars> = <body>: declares an axiom, effectively the same as theorem but forcing Imandra to assume the truth of the conjecture, rather than verifying it. This is of course dangerous and should be used with extreme care.

Examples

Try this!
In [1]:
verify (fun x -> x + 1 > x)
Out[1]:
- : Z.t -> bool = <fun>
Proved
proof
ground_instances:0
definitions:0
inductions:0
search_time:
0.021s
details:
Expand
smt_stats:
rlimit count:14
num allocs:5297222
time:0.009000
memory:15.080000
max memory:15.080000
Expand
  • start[0.021s] ( :var_0: ) + 1 > ( :var_0: )

  • simplify

    into:
    true
    expansions:
    []
    rewrite_steps:
      forward_chaining:
      • Unsat
      Try this!
      In [2]:
      instance (fun x y -> x < 0 && x + y = 4)
      Out[2]:
      - : Z.t -> Z.t -> bool = <fun>
module CX : sig val x : Z.t val y : Z.t end

      Instance (after 0 steps, 0.016s):
let x : int = (-1)
let y : int = 5
      Instance
      proof attempt
      ground_instances:0
      definitions:0
      inductions:0
      search_time:
      0.016s
      details:
      Expand
      smt_stats:
      num checks:1
      eliminated vars:1
      rlimit count:154
      mk bool var:1
      eliminated applications:2
      num allocs:10838663
      final checks:1
      time:0.008000
      memory:15.250000
      max memory:15.580000
      Expand
      • start[0.016s] (( :var_0: ) < 0) && (( :var_0: ) + ( :var_1: ) = 4)

      • simplify

        into:
        not (0 <= ( :var_0: )) && (( :var_0: ) + ( :var_1: ) = 4)
        expansions:
        []
        rewrite_steps:
          forward_chaining:
          • Sat (Some let x : int = (Z.of_nativeint (-1n)) let y : int = (Z.of_nativeint (5n)) )
          Try this!
          In [3]:
          theorem succ_mono n m = succ n > succ m <==> n > m
          Out[3]:
          val succ_mono : Z.t -> Z.t -> bool = <fun>
          Proved
          proof
          ground_instances:0
          definitions:0
          inductions:0
          search_time:
          0.015s
          details:
          Expand
          smt_stats:
          rlimit count:24
          num allocs:17572280
          time:0.007000
          memory:15.450000
          max memory:15.580000
          Expand
          • start[0.015s]
  (( :var_0: ) + 1 > ( :var_1: ) + 1) = (( :var_0: ) > ( :var_1: ))

          • simplify

            into:
            true
            expansions:
            []
            rewrite_steps:
              forward_chaining:
              • Unsat
              Try this!
              In [4]:
              verify (fun n -> succ n <> 100)
              Out[4]:
              - : Z.t -> bool = <fun>
module CX : sig val n : Z.t end

              Counterexample (after 0 steps, 0.016s):
let n : int = 99
              Refuted
              proof attempt
              ground_instances:0
              definitions:0
              inductions:0
              search_time:
              0.016s
              details:
              Expand
              smt_stats:
              eliminated vars:1
              rlimit count:40
              num allocs:26120558
              time:0.008000
              memory:15.630000
              max memory:15.630000
              Expand
              • start[0.016s] not (( :var_0: ) + 1 = 100)

              • simplify

                into:
                not (( :var_0: ) = 99)
                expansions:
                []
                rewrite_steps:
                  forward_chaining:
                  • Sat (Some let n : int = (Z.of_nativeint (99n)) )