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

In [1]:
verify (fun x -> x + 1 > x)
Out[1]:
- : int -> bool = <fun>
Proved
proof
ground_instances0
definitions0
inductions0
search_time
0.350s
details
Expand
smt_stats
rlimit count10
mk bool var5
num allocs994833947
memory21.330000
max memory26.980000
Expand
  • start[0.350s] (:var_0: + 1) > :var_0:
  • simplify

    into
    true
    expansions
    []
    rewrite_steps
      forward_chaining
      • unsat

        (mp (asserted (not true)) (rewrite (= (not true) false)) false)
      In [2]:
      instance (fun x y -> x < 0 && x + y = 4)
      
      Out[2]:
      - : int -> Z.t -> bool = <fun>
      module CX : sig val x : int val y : int end
      
      Instance (after 0 steps, 0.049s):
       let (x : int) = (-1)
       let (y : int) = 5
      
      Instance
      proof attempt
      ground_instances0
      definitions0
      inductions0
      search_time
      0.049s
      details
      Expand
      smt_stats
      num checks1
      eliminated vars1
      rlimit count120
      mk bool var7
      eliminated applications2
      num allocs1054739831
      final checks1
      memory24.270000
      max memory26.980000
      Expand
      • start[0.049s] :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) = (-1) let (y : int) = 5 )
          In [3]:
          theorem succ_mono n m = succ n > succ m <==> n > m
          
          Out[3]:
          val succ_mono : int -> int -> bool = <fun>
          
          Proved
          proof
          ground_instances0
          definitions0
          inductions0
          search_time
          0.025s
          details
          Expand
          smt_stats
          rlimit count20
          mk bool var5
          num allocs1115734813
          memory27.360000
          max memory27.660000
          Expand
          • start[0.025s] (:var_0: + 1) > (:var_1: + 1) = :var_0: > :var_1:
          • simplify

            into
            true
            expansions
            []
            rewrite_steps
              forward_chaining
              • unsat

                (mp (asserted (not true)) (rewrite (= (not true) false)) false)
              In [4]:
              verify (fun n -> succ n <> 100)
              
              Out[4]:
              - : Z.t -> bool = <fun>
              module CX : sig val n : int end
              
              Counterexample (after 0 steps, 0.019s):
               let (n : int) = 99
              
              Refuted
              proof attempt
              ground_instances0
              definitions0
              inductions0
              search_time
              0.019s
              details
              Expand
              smt_stats
              eliminated vars1
              rlimit count29
              mk bool var5
              num allocs1250107670
              memory22.080000
              max memory27.660000
              Expand
              • start[0.019s] not (:var_0: + 1 = 100)
              • simplify

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