Chapter 10  Technical Informations

• Structure of Session Files
• Prover Detection
• The why3.conf Configuration File
• Drivers for External Provers
• Transformations

10.1  Structure of Session Files

The proof session state is stored in an XML file named <dir>/why3session.xml, where <dir> is the directory of the project. The XML file follows the DTD given in share/why3session.dtd and reproduced below.

10.2  Prover Detection

All the necessary data configuration for the automatic detection of installed provers is stored in the file provers-detection-data.conf typically located in directory /usr/local/share/why3 after installation. The contents of this file is reproduced below.

10.3  The why3.conf Configuration File

One can use a custom configuration file. The Why3 tools look for it in the following order:

1. the file specified by the -C or --config options,
2. the file specified by the environment variable WHY3CONFIG if set,
3. the file $HOME/.why3.conf ($USERPROFILE/.why3.conf under Windows) or, in the case of local installation, why3.conf in the top directory of Why3 sources.

If none of these files exist, a built-in default configuration is used.

The configuration file is a human-readable text file, which consists of association pairs arranged in sections. Below is an example of configuration file.

[main]
loadpath = "/usr/local/share/why3/theories"
loadpath = "/usr/local/share/why3/modules"
magic = 14
memlimit = 0
plugin = "/usr/local/lib/why3/plugins/tptp"
plugin = "/usr/local/lib/why3/plugins/genequlin"
plugin = "/usr/local/lib/why3/plugins/hypothesis_selection"
running_provers_max = 4
timelimit = 2

[ide]
default_editor = "editor %f"
error_color = "orange"
goal_color = "gold"
iconset = "fatcow"
intro_premises = true
premise_color = "chartreuse"
print_labels = false
print_locs = false
print_time_limit = false
saving_policy = 2
task_height = 404
tree_width = 512
verbose = 0
window_height = 1173
window_width = 1024

[prover]
command = "'why3-cpulimit' 0 %m -s coqtop -batch -I %l/coq-tactic -R %l/coq Why3 -l %f"
driver = "/usr/local/share/why3/drivers/coq.drv"
editor = "coqide"
in_place = false
interactive = true
name = "Coq"
shortcut = "coq"
version = "8.3pl4"

[prover]
command = "'why3-cpulimit' %t %m -s alt-ergo %f"
driver = "/usr/local/share/why3/drivers/alt_ergo_0.93.drv"
editor = ""
in_place = false
interactive = false
name = "Alt-Ergo"
shortcut = "altergo"
shortcut = "alt-ergo"
version = "0.93.1"

[editor coqide]
command = "coqide -I %l/coq-tactic -R %l/coq Why3 %f"
name = "CoqIDE"

A section begins with a header inside square brackets and ends at the beginning of the next section. The header of a section can be only one identifier, main and ide in the example, or it can be composed by a family name and one family argument, prover is one family name, coq and alt-ergo are the family argument.

Sections contain associations key=value. A value is either an integer (e.g. -555), a boolean (true, false), or a string (e.g. "emacs"). Some specific keys can be attributed multiple values and are thus allowed to occur several times inside a given section. In that case, the relative order of these associations matter.

10.4  Drivers for External Provers

Drivers for external provers are readable files from directory drivers. Experimented users can modify them to change the way the external provers are called, in particular which transformations are applied to goals.

[TO BE COMPLETED LATER]

10.5  Transformations

This section documents the available transformations. We first describe the most important ones, and then we provide a quick documentation of the others, first the non-splitting ones, e.g. those which produce exactly one goal as result, and the others which produce any number of goals.

Notice that the set of available transformations in your own installation is given by

why3 --list-transforms

10.5.1  Inlining definitions

Those transformations generally amount to replace some applications of function or predicate symbols with its definition.

inline_trivial

expands and removes definitions of the form

function f x_1 ... x_n = (g e_1 ... e_k) predicate p x_1 ... x_n = (q e_1 ... e_k)

when each e_i is either a ground term or one of the x_j, and each x₁ … x_n occurs at most once in all the e_i.

inline_goal

expands all outermost symbols of the goal that have a non-recursive definition.

inline_all

expands all non-recursive definitions.

10.5.2  Induction Transformations

induction_ty_lex

: This transformation performs structural, lexicographic induction on goals involving universally quantified variables of algebraic data types, such as lists, trees, etc. For instance, it transforms the following goal

goal G: forall l: list 'a. length l >= 0

into this one:

goal G : forall l:list 'a. match l with | Nil -> length l >= 0 | Cons a l1 -> length l1 >= 0 -> length l >= 0 end

When induction can be applied to several variables, the transformation picks one heuristically. A label "induction" can be used to force induction over one particular variable, e.g. with

goal G: forall l1 "induction" l2 l3: list 'a. l1 ++ (l2 ++ l3) = (l1 ++ l2) ++ l3

induction will be applied on l1. If this label is attached on several variables, a lexicographic induction is performed on these variables, from left to right.

10.5.3  Simplification by Computation

These transformations simplify the goal by applying several kinds of simplification, described below. The transformations differ only by the kind of rules they apply:

compute_in_goal

aggressively applies all known computation/simplification rules

compute_specified

performs rewriting using only built-in operators and user-provided rules

The kinds of simplification are as follows.

• Computations with built-in symbols, e.g. operations on integers, when applied to explicit constants, are evaluated. This includes evaluation of equality when a decision can be made (on integer constants, on constructors of algebraic data types), Boolean evaluation, simplification of pattern-matching/conditional expression, extraction of record fields, and beta-reduction. At best, these computations reduce the goal to true and the transformations thus does not produce any sub-goal. For example, a goal like 6*7=42 is solved by those transformations.
• Unfolding of definitions, as done by inline_goal. compute_in_goal unfold all definitions, including recursive ones. For compute_specified, the user can enable unfolding of a specific logic symbol by attaching the meta rewrite_def to the symbol.

  function sqr (x:int) : int = x * x meta "rewrite_def" function sqr

• Rewriting using axioms or lemmas declared as rewrite rules. When an axiom (or a lemma) has one of the forms

  axiom a: forall ... t1 = t2

  or

  axiom a: forall ... f1 <-> f2

  then the user can declare

  meta "rewrite" prop a

  to turn this axiom into a rewrite rule. Rewriting is always done from left to right. Beware that there is no check for termination nor for confluence of the set of rewrite rules declared.

Bound on the number of reductions

The computations performed by these transformations can take an arbitrarily large number of steps, or even not terminate. For this reason, the number of steps is bounded by a maximal value, which is set by default to 1000. This value can be increased by another meta, e.g.

When this upper limit is reached, a warning is issued, and the partly-reduced goal is returned as the result of the transformation.

10.5.4  Other Non-Splitting Transformations

eliminate_algebraic

replaces algebraic data types by first-order definitions [7].

eliminate_builtin

removes definitions of symbols that are declared as builtin in the driver, i.e. with a “syntax” rule.

eliminate_definition_func

replaces all function definitions with axioms.

eliminate_definition_pred

replaces all predicate definitions with axioms.

eliminate_definition

applies both transformations above.

eliminate_mutual_recursion

replaces mutually recursive definitions with axioms.

eliminate_recursion

replaces all recursive definitions with axioms.

eliminate_if_term

replaces terms of the form if formula then t2 else t3 by lifting them at the level of formulas. This may introduce if then else in formulas.

eliminate_if_fmla

replaces formulas of the form if f1 then f2 else f3 by an equivalent formula using implications and other connectives.

eliminate_if

applies both transformations above.

eliminate_inductive

replaces inductive predicates by (incomplete) axiomatic definitions, i.e. construction axioms and an inversion axiom.

eliminate_let_fmla

eliminates let by substitution, at the predicate level.

eliminate_let_term

eliminates let by substitution, at the term level.

eliminate_let

applies both transformations above.

encoding_smt

encodes polymorphic types into monomorphic type [2].

encoding_tptp

encodes theories into unsorted logic.

introduce_premises

moves antecedents of implications and universal quantifications of the goal into the premises of the task.

simplify_array

automatically rewrites the task using the lemma Select_eq of theory map.Map.

simplify_formula

reduces trivial equalities t=t to true and then simplifies propositional structure: removes true, false, simplifies f ∧ f to f, etc.

simplify_recursive_definition

reduces mutually recursive definitions if they are not really mutually recursive, e.g.

function f : ... = .... g ... with g : ... = e

becomes

function g : ... = e function f : ... = ... g ...

if f does not occur in e.

simplify_trivial_quantification

simplifies quantifications of the form

forall x, x=t -> P(x)

or

forall x, t=x -> P(x)

when x does not occur in t into

P(t)

More generally, it applies this simplification whenever x=t appears in a negative position.

simplify_trivial_quantification_in_goal

is the same as above but it applies only in the goal.

split_premise

splits conjunctive premises.

10.5.5  Other Splitting Transformations

full_split_all

performs both split_premise and full_split_goal.

full_split_goal

puts the goal in a conjunctive form, returns the corresponding set of subgoals. The number of subgoals generated may be exponential in the size of the initial goal.

simplify_formula_and_task

is the same as simplify_formula but it also removes the goal if it is equivalent to true.

split_all

performs both split_premise and split_goal.

split_goal

if the goal is a conjunction of goals, returns the corresponding set of subgoals. The number of subgoals generated is linear in the size of the initial goal.

split_intro

moves the antecedents into the premises when a goal is an implication.