Module Imandra_interactive.Verify

Verification of properties

Direct access to verification of functions

type t = Imandra_surface.Top_result.verify_result =
| V_proved of {
proof : Imandra_document.Document.t option;
proof_graph : string option;
callgraph : Imandra_surface.Top_result.callgraph option;
}
| V_proved_upto of {
callgraph : Imandra_surface.Top_result.callgraph option;
upto : Imandra_surface.Event.upto;
}
| V_refuted of {
model_str_ocaml : string;
model_str_pretty : string;
model : Imandra_surface.Top_result.model;
callgraph : Imandra_surface.Top_result.callgraph option;
proof : Imandra_document.Document.t option;
}
| V_unknown of {
callgraph : Imandra_surface.Top_result.callgraph option;
instances : Imandra_document.Document.t option;
proof : Imandra_document.Document.t option;
reason : string;
checkpoints : Imandra_surface.Term.t list option;
}

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 -> ?error_on_fail:bool -> string -> t

Main entry point for verifying a property (a boolean function)

  • parameter reflect

    if true, counterexamples are 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 not to be always valid), and verify it.

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

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

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

(* it's a counterexample alright! *)
 # f CX.x ;;
 - : bool = false

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