Module Imandra_interactive.Instance

Verification of properties

Direct access to verification of functions

type t = Imandra_surface.Top_result.instance_result =
| I_unsat of {
proof : Imandra_document.Document.t option;
proof_graph : string option;
callgraph : Imandra_surface.Top_result.callgraph option;
}
| I_unsat_upto of {
callgraph : Imandra_surface.Top_result.callgraph option;
upto : Imandra_surface.Event.upto;
}
| I_sat of {
model_str_ocaml : string;
model_str_pretty : string;
model : Imandra_surface.Top_result.model;
model_reflect : Imandra_surface.Code_fragment.t option;
callgraph : Imandra_surface.Top_result.callgraph option;
proof : Imandra_document.Document.t option;
}
| I_unknown of {
callgraph : Imandra_surface.Top_result.callgraph option;
instances : Imandra_document.Document.t option;
proof : Imandra_document.Document.t option;
reason : string;
}

Result of a verification call

val pp : Ppx_deriving_runtime.Format.formatter -> t -> Ppx_deriving_runtime.unit
val show : t -> Ppx_deriving_runtime.string
val top : ?scope:Opentelemetry.Trace.scope -> ?full:bool -> ?fc:bool -> ?upto:Imandra_surface.Event.upto -> ?quiet:bool -> ?simp:bool -> ?hints:Imandra_surface.Uid.t Imandra_surface.Hints.t -> ?reflect:bool -> string -> t

Main entry point for finding an instance satisfying a property (a boolean function)

  • parameter reflect

    if true, the instance is reflected in a "CX" module.

  • parameter simp

    if true, simplify goal before starting the proof search

  • parameter fc

    if true, use forward chaining rules

  • parameter full

    if true, proofs/callgraphs are computed (at a performance cost). Default false.

    For example, here we define a property named "f" (which turns out to have an instance), and verify it.

    (* satisfiable property *)
# let f x = x + 1 = 100 ;;
val f : Z.t -> bool = <fun>

                      # Instance.top ~reflect:true "f" ;;
Counterexample:
  let x = 99
module CX : sig val x : Z.t end
            - : Instance.t = I_sat …

                                   # CX.x ;;
- : Z.t = 99

          (* it's an instance alright! *)
          # f CX.x ;;
- : bool = true

    We obtain a counter-example (as a I_sat value) containing a model), but Imandra also reflects the instance in the OCaml environment as a CX module with a value x : Z.t. This instance can be used to compute, like any other OCaml value.