# Logic and Program modes¶

Imandra has two modes: logic mode and program mode. When we launch Imandra Terminal (or an Imandra Jupyter Notebook session), we start off in logic mode.

In the terminal, we can identify that Imandra is in logic mode by the pound sign prompt (#).

In a notebook, we can inspect Imandra's current mode using the #config directive.

In [1]:
#config 1

Out[1]:
----------------------------------------------------------------------------
Configuration component: Mode
----------------------------------------------------------------------------
Value: logic
Help topics: program, logic
----------------------------------------------------------------------------


While in logic mode, we have access to Imandra's reasoning tools, such as verify and theorem.

In [2]:
let succ n = n + 1

Out[2]:
val succ : Z.t -> Z.t = <fun>

In [3]:
verify (fun n -> succ n > n)

Out[3]:
- : Z.t -> bool = <fun>

Proved
proof
ground_instances:0
definitions:0
inductions:0
search_time:
0.020s
details:
Expand
smt_stats:
 rlimit count: 16 num allocs: 646616 time: 0.008 memory: 5.14 max memory: 5.14
Expand
• start[0.020s] (( :var_0: ) + 1) > ( :var_0: )
• #### simplify

 into: true expansions: [] rewrite_steps: forward_chaining:
• Unsat

A future notebook will summarize the various reasoning tools, and explain when to use which one.

In logic mode, all definitions -- types, values and functions -- are entered into the logic. We can see all previous events in logic mode by inspecting the #history (aliased to #h).

In [4]:
#h;;

Out[4]:

### All events in session

0. Fun: succ
1. Verify: <expr>
dependency graph
In [5]:
#h succ

Out[5]:

### Fun: succ

iml:
definition
fun (n : int) -> n + 1
def:
name:succ
type:int -> int
recursive:false
def-depth:3
def-ty-depth:1
call signature:succ (n : int)
validated:in 0.001s
location:At jupyter cell 2:1,0--18 1 | let succ n = n + 1 ^^^^^^^^^^^^^^^^^^
hashes:
 succ: gcAPJo6BkTHG8s8oO1UoUq/kwjrx4ikf5BiLOnSzzlU

While in logic mode, we are restricted to a purely functional subset of OCaml, and our recursive functions must terminate.

If we try to define a non-termating function, for example, Imandra will reject it.

In [6]:
let rec bad_repeat x = x :: bad_repeat x

Out[6]:
val bad_repeat : 'a -> 'a list = <fun>

At jupyter cell 6:1,0--40
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Error[/server]:
unsupported: Validate: no measure provided, and Imandra cannot guess any.
Are you sure this function is actually terminating?
See https://docs.imandra.ai/imandra-docs/notebooks/proving-program-termination/
----------------------------------------------------------------------------
Context:
At jupyter cell 6:1,0--40
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Checking termination of function bad_repeat

In [7]:
#show bad_repeat

Out[7]:
Unknown element.


For more complex recursive functions, we may need to convince Imandra that the function terminates, for example by defining a "measure". See the notebook Proving Program Termination with Imandra for more details.

Our logic-mode definitions are allowed to call other definitions only if those other definitions have been admitted into the logic.

In [8]:
let say_hi () = print_endline "Hello!"

Out[8]:
At jupyter cell 8:1,16--29
1 | let say_hi () = print_endline "Hello!"
^^^^^^^^^^^^^

Error:
No function Stdlib_0.print_endline was defined in logic-mode
:ev {funs=( && ), _, ( || ), _, ( = ), _, ( <> ), _, not, _, implies, _,
explies, _, iff, _, ( + ), _, const, _, ( >= ), _, count.nativeint, _,
mk_nat, _, count.option, _, count.list, _, count.float, _, count.real,
_, count.string, _, ( < ), _, ( <= ), _, ( > ), _, min, _, max, _,
( <. ), _, ( <=. ), _, ( >. ), _, ( >=. ), _, min_r, _, max_r, _,
( ~- ), _, abs, _, ( - ), _, ( ~+ ), _, ( * ), _, ( / ), _, mod, _,
compare, _, count.Ordinal.t, _, Ordinal.of_int_unsafe, _, Ordinal.zero,
_, Ordinal.one, _, Ordinal.two, _, Ordinal.of_int, _, Ordinal.( << ), _,
Ordinal.plus, _, Ordinal.shift, _, Ordinal.pair, _, Ordinal.triple, _,
Ordinal.quad, _, Ordinal.simple_plus, _, Ordinal.of_list_rec, _,
Ordinal.of_list, _, Ordinal.is_valid_rec, _, Ordinal.is_valid, _,
Ordinal.( + ), _, Ordinal.( ~$), _, Ordinal.omega, _, Ordinal.omega_omega, _, count.Peano_nat.t, _, Peano_nat.zero, _, Peano_nat.succ, _, Peano_nat.of_int, _, Peano_nat.to_int, _, Peano_nat.plus, _, Peano_nat.leq, _, Peano_nat.( = ), _, Peano_nat.( <= ), _, Peano_nat.( + ), _, count.unit, _, count.result, _, count.Result.t, _, Result.return, _, Result.fail, _, Result.map, _, Result.map_err, _, Result.get_or, _, Result.map_or, _, Result.( >|= ), _, Result.flat_map, _, Result.( >>= ), _, Result.fold, _, Result.is_ok, _, Result.is_error, _, Result.monoid_product, _, Result.( let+ ), _, Result.and+, _, Result.( let* ), _, Result.and*, _, count.either, _, ( |> ), _, ( @@ ), _, id, _, %>, _, ( +. ), _, ( -. ), _, ( ~-. ), _, ( *. ), _, ( /. ), _, count.List.t, _, List.empty, _, List.is_empty, _, List.cons, _, List.return, _, List.hd, _, List.tl, _, List.append, _, List.append_to_nil, _, List.append_single, _, List.rev, _, List.length, _, List.len_nonnegative, _, List.len_zero_is_empty, _, List.split, _, List.map, _, List.map2, _, List.for_all, _, List.exists, _, List.fold_left, _, List.fold_right, _, List.mapi_with, _, List.mapi, _, List.filter, _, List.filter_map, _, List.flat_map, _, List.find, _, List.mem, _, List.mem_assoc, _, List.nth, _, List.assoc, _, List.take, _, List.drop, _, List.( -- ), _, measure_fun.List.( -- ), _, List.insert_sorted, _, List.sort, _, anon_fun.List.sort.1, _, List.is_sorted, _, List.monoid_product, _, anon_fun.List.monoid_product.1, _, anon_fun.List.monoid_product.2, _, List.( >|= ), _, List.( >>= ), _, List.( let+ ), _, List.and+, _, List.( let* ), _, List.and*, _, ( @ ), _, ( -- ), _, count.Int.t, _, Int.( + ), _, Int.( - ), _, Int.( ~- ), _, Int.( * ), _, Int.( / ), _, Int.mod, _, Int.( < ), _, Int.( <= ), _, Int.( > ), _, Int.( >= ), _, Int.min, _, Int.max, _, Int.abs, _, Int.to_string, _, Int.compare, _, Int.equal, _, count.Bool.t, _, count.Option.t, _, Option.map, _, Option.map_or, _, Option.is_some, _, Option.is_none, _, Option.return, _, Option.( >|= ), _, Option.flat_map, _, Option.( >>= ), _, Option.or_, _, Option.( <+> ), _, Option.exists, _, Option.for_all, _, Option.get_or, _, Option.fold, _, Option.( <$> ), _,
Option.monoid_product, _, Option.( let+ ), _, Option.and+, _,
Option.( let* ), _, Option.and*, _, count.Real.t, _, Real.of_int, _,
Real.( + ), _, Real.( - ), _, Real.( ~- ), _, Real.( * ), _, Real.( / ),
_, Real.( < ), _, Real.( <= ), _, Real.( > ), _, Real.( >= ), _,
Real.abs, _, Real.min, _, Real.max, _, Real.of_float, _, count.Map.t, _,
Map.get, _, Map.of_list, _, count.Multiset.t, _, Multiset.empty, _,
Multiset.add, _, Multiset.find, _, Multiset.mem, _, Multiset.remove, _,
Multiset.of_list, _, count.Set.t, _, Set.empty, _, Set.is_empty, _,
Set.is_valid, _, Set.mem, _, Set.subset, _, Set.add, _, Set.remove, _,
Set.inter, _, Set.union, _, Set.complement, _, Set.diff, _, Set.of_list,
_, Set.( ++ ), _, Set.( -- ), _, count.String.t, _, String.empty, _,
String.length, _, String.append, _, String.concat, _, String.prefix, _,
String.suffix, _, String.contains, _, String.unsafe_sub, _, String.sub,
_, String.of_int, _, String.unsafe_to_nat, _, String.to_nat, _, ( ^ ),
_, succ, _, pred, _, fst, _, snd, _, count.Float.t, _,
count.Float.Round.t, _, _verify_target, _, Float.( ~- ), _, Float.( + ),
_, Float.( - ), _, Float.( * ), _, Float.( / ), _, Float.nan, _,
Float.infinity, _, Float.( < ), _, Float.( <= ), _, Float.( > ), _,
Float.( >= ), _, Float.( = ), _, Float.( <> ), _, Float.neg, _,
Float.abs, _, Float.is_zero, _, Float.is_nan, _, Float.is_infinite, _,
Float.is_normal, _, Float.is_subnormal, _, Float.is_positive, _,
Float.is_negative, _, Float.min, _, Float.max, _, Float.rem, _,
Float.sqrt, _, count.LChar.t, _, LChar.zero, _, LChar.is_printable, _,
count.LString.t, _, LString.empty, _, LString.of_list, _,
LString.length, _, LString.len_pos, _, LString.len_zero_inversion, _,
LString.append, _, LString.( ^^ ), _, LString.for_all, _,
LString.exists, _, LString.concat, _, LString.is_printable, _,
LString.sub, _, LString.prefix, _, LString.suffix, _, LString.contains,
_, LString.take, _, LString.drop, _, succ, _, _verify_target, _;
tys=bool, _, int, _, list, _, option, _, nativeint, _, float, _, real,
_, string, _, Ordinal.t, _, Peano_nat.t, _, unit, _, result, _,
Result.t, _, either, _, List.t, _, Int.t, _, Bool.t, _, Option.t, _,
Real.t, _, Map.t, _, Multiset.t, _, Set.t, _, String.t, _, Float.t, _,
Float.Round.t, _, LChar.t, _, LString.t, _;}


In order to define such a side-effecting function, we switch to program mode. We do this using the #program directive.

In [9]:
#program;;

#config 1;;

Out[9]:
----------------------------------------------------------------------------
Configuration component: Mode
----------------------------------------------------------------------------
Value: program
Help topics: program, logic
----------------------------------------------------------------------------


In the terminal, we can identify that Imandra is in program mode by the angle bracket prompt (>).

Now that we are in program mode, we have the full power of OCaml at our fingertips!

In [10]:
let say_hi () = print_endline "Hello!"

Out[10]:
val say_hi : unit -> unit = <fun>

In [11]:
say_hi ()

Out[11]:
Hello!
- : unit = ()


When we switch back to logic mode (using the #logic directive), we can still refer to our program-mode definitions at the top level.

In [12]:
#logic;;

say_hi ()

Out[12]:
Hello!
- : unit = ()


But we are forbidden from using them in our logic-mode definitions.

In [13]:
let say_hi_from_logic_mode () = say_hi ()

Out[13]:
At jupyter cell 13:1,32--38
1 | let say_hi_from_logic_mode () = say_hi ()
^^^^^^

Error:
No function say_hi_6637 was defined in logic-mode
:ev {funs=( && ), _, ( || ), _, ( = ), _, ( <> ), _, not, _, implies, _,
explies, _, iff, _, ( + ), _, const, _, ( >= ), _, count.nativeint, _,
mk_nat, _, count.option, _, count.list, _, count.float, _, count.real,
_, count.string, _, ( < ), _, ( <= ), _, ( > ), _, min, _, max, _,
( <. ), _, ( <=. ), _, ( >. ), _, ( >=. ), _, min_r, _, max_r, _,
( ~- ), _, abs, _, ( - ), _, ( ~+ ), _, ( * ), _, ( / ), _, mod, _,
compare, _, count.Ordinal.t, _, Ordinal.of_int_unsafe, _, Ordinal.zero,
_, Ordinal.one, _, Ordinal.two, _, Ordinal.of_int, _, Ordinal.( << ), _,
Ordinal.plus, _, Ordinal.shift, _, Ordinal.pair, _, Ordinal.triple, _,
Ordinal.quad, _, Ordinal.simple_plus, _, Ordinal.of_list_rec, _,
Ordinal.of_list, _, Ordinal.is_valid_rec, _, Ordinal.is_valid, _,
Ordinal.( + ), _, Ordinal.( ~$), _, Ordinal.omega, _, Ordinal.omega_omega, _, count.Peano_nat.t, _, Peano_nat.zero, _, Peano_nat.succ, _, Peano_nat.of_int, _, Peano_nat.to_int, _, Peano_nat.plus, _, Peano_nat.leq, _, Peano_nat.( = ), _, Peano_nat.( <= ), _, Peano_nat.( + ), _, count.unit, _, count.result, _, count.Result.t, _, Result.return, _, Result.fail, _, Result.map, _, Result.map_err, _, Result.get_or, _, Result.map_or, _, Result.( >|= ), _, Result.flat_map, _, Result.( >>= ), _, Result.fold, _, Result.is_ok, _, Result.is_error, _, Result.monoid_product, _, Result.( let+ ), _, Result.and+, _, Result.( let* ), _, Result.and*, _, count.either, _, ( |> ), _, ( @@ ), _, id, _, %>, _, ( +. ), _, ( -. ), _, ( ~-. ), _, ( *. ), _, ( /. ), _, count.List.t, _, List.empty, _, List.is_empty, _, List.cons, _, List.return, _, List.hd, _, List.tl, _, List.append, _, List.append_to_nil, _, List.append_single, _, List.rev, _, List.length, _, List.len_nonnegative, _, List.len_zero_is_empty, _, List.split, _, List.map, _, List.map2, _, List.for_all, _, List.exists, _, List.fold_left, _, List.fold_right, _, List.mapi_with, _, List.mapi, _, List.filter, _, List.filter_map, _, List.flat_map, _, List.find, _, List.mem, _, List.mem_assoc, _, List.nth, _, List.assoc, _, List.take, _, List.drop, _, List.( -- ), _, measure_fun.List.( -- ), _, List.insert_sorted, _, List.sort, _, anon_fun.List.sort.1, _, List.is_sorted, _, List.monoid_product, _, anon_fun.List.monoid_product.1, _, anon_fun.List.monoid_product.2, _, List.( >|= ), _, List.( >>= ), _, List.( let+ ), _, List.and+, _, List.( let* ), _, List.and*, _, ( @ ), _, ( -- ), _, count.Int.t, _, Int.( + ), _, Int.( - ), _, Int.( ~- ), _, Int.( * ), _, Int.( / ), _, Int.mod, _, Int.( < ), _, Int.( <= ), _, Int.( > ), _, Int.( >= ), _, Int.min, _, Int.max, _, Int.abs, _, Int.to_string, _, Int.compare, _, Int.equal, _, count.Bool.t, _, count.Option.t, _, Option.map, _, Option.map_or, _, Option.is_some, _, Option.is_none, _, Option.return, _, Option.( >|= ), _, Option.flat_map, _, Option.( >>= ), _, Option.or_, _, Option.( <+> ), _, Option.exists, _, Option.for_all, _, Option.get_or, _, Option.fold, _, Option.( <$> ), _,
Option.monoid_product, _, Option.( let+ ), _, Option.and+, _,
Option.( let* ), _, Option.and*, _, count.Real.t, _, Real.of_int, _,
Real.( + ), _, Real.( - ), _, Real.( ~- ), _, Real.( * ), _, Real.( / ),
_, Real.( < ), _, Real.( <= ), _, Real.( > ), _, Real.( >= ), _,
Real.abs, _, Real.min, _, Real.max, _, Real.of_float, _, count.Map.t, _,
Map.get, _, Map.of_list, _, count.Multiset.t, _, Multiset.empty, _,
Multiset.add, _, Multiset.find, _, Multiset.mem, _, Multiset.remove, _,
Multiset.of_list, _, count.Set.t, _, Set.empty, _, Set.is_empty, _,
Set.is_valid, _, Set.mem, _, Set.subset, _, Set.add, _, Set.remove, _,
Set.inter, _, Set.union, _, Set.complement, _, Set.diff, _, Set.of_list,
_, Set.( ++ ), _, Set.( -- ), _, count.String.t, _, String.empty, _,
String.length, _, String.append, _, String.concat, _, String.prefix, _,
String.suffix, _, String.contains, _, String.unsafe_sub, _, String.sub,
_, String.of_int, _, String.unsafe_to_nat, _, String.to_nat, _, ( ^ ),
_, succ, _, pred, _, fst, _, snd, _, count.Float.t, _,
count.Float.Round.t, _, _verify_target, _, Float.( ~- ), _, Float.( + ),
_, Float.( - ), _, Float.( * ), _, Float.( / ), _, Float.nan, _,
Float.infinity, _, Float.( < ), _, Float.( <= ), _, Float.( > ), _,
Float.( >= ), _, Float.( = ), _, Float.( <> ), _, Float.neg, _,
Float.abs, _, Float.is_zero, _, Float.is_nan, _, Float.is_infinite, _,
Float.is_normal, _, Float.is_subnormal, _, Float.is_positive, _,
Float.is_negative, _, Float.min, _, Float.max, _, Float.rem, _,
Float.sqrt, _, count.LChar.t, _, LChar.zero, _, LChar.is_printable, _,
count.LString.t, _, LString.empty, _, LString.of_list, _,
LString.length, _, LString.len_pos, _, LString.len_zero_inversion, _,
LString.append, _, LString.( ^^ ), _, LString.for_all, _,
LString.exists, _, LString.concat, _, LString.is_printable, _,
LString.sub, _, LString.prefix, _, LString.suffix, _, LString.contains,
_, LString.take, _, LString.drop, _, succ, _, _verify_target, _;
tys=bool, _, int, _, list, _, option, _, nativeint, _, float, _, real,
_, string, _, Ordinal.t, _, Peano_nat.t, _, unit, _, result, _,
Result.t, _, either, _, List.t, _, Int.t, _, Bool.t, _, Option.t, _,
Real.t, _, Map.t, _, Multiset.t, _, Set.t, _, String.t, _, Float.t, _,
Float.Round.t, _, LChar.t, _, LString.t, _;}


Often, we want to define a type in logic mode and then a related function in program mode, for example a pretty-printer. For this case we can use the [@@program] annotation to define a one-off program-mode function while in logic mode.

In [14]:
type person = { name : string; favorite_color : string };;

let print_person (person : person) : string =
Printf.sprintf "%s prefers %s things" person.name person.favorite_color
[@@program];;

print_person { name = "Matt"; favorite_color = "green" };;

Out[14]:
type person = { name : string; favorite_color : string; }
val print_person : person -> string = <fun>
- : string = "Matt prefers green things"


Sometimes we also need to use program-mode functions in order to generate logic-mode values, this can be done using the [@@reflect] annotation:

In [15]:
let one = Z.of_string "1" [@@reflect]

Out[15]:
val one : Z.t = 1
- : unit = ()
- : unit = ()


This can be useful for several reasons, one of the most common ones is reading logic-mode values from files. Imandra also offers the lower-level facility Imandra.port to port program-mode values into logic-mode locals:

In [16]:
let x = print_endline "debug"; 1 [@@program];;
Imandra.port "y" "x";;
y;;

Out[16]:
debug
val x : Z.t = 1
val y : Z.t = 1
- : unit = ()
- : unit = ()
- : Z.t = 1


That concludes our overview of Imandra's logic and program modes!