Why3, custom libraries, transformations

"Format" is an established term in Why3. It's an input file format. Language to be honest. Why3 support more than one input language (usually theorem provers support only one), they are:

For Why3 1.8.x, the standard formats are:

• WhyML - .mlw - the normal Why3 language for programs, specifications, lemmas, and goals.
• micro-C - .c - a small C subset intended mainly for teaching.
• micro-Python - .py - a small Python subset, also mainly for teaching.
• MLCFG - .mlcfg - an extension of WhyML with unstructured/goto-style function bodies.
• Coma - .coma - an intermediate verification language.
• S-expressions - an internal/intermediate representation of Why3 syntax, when Why3 was built with S-expression support.
• etc...

You can list supported formats by YOUR installation of Why3 by the command:

$ why3 show formats
coma ["coma"]
  Continuation Machine language

dimacs ["cnf"]
  Parser for dimacs format.

equlin ["equlin"]
  Generate random linear arithmetic problems. The first line gives the seed.
  Each other line describes a goal and contains three numbers:
    - the number of variables
    - the number of equations
    - the maximum absolute value of coefficients.

micro-C ["c"]
  micro-C format

mlcfg ["mlcfg",
"stdout"]
  whyml extended with functions implemented by control-flow-graphs

python ["py"]
  mini-Python format

sexp ["sexp"]
  WhyML code in s-expressions format

tptp ["p", "ax"]
  TPTP format (CNF FOF FOFX TFF)

whyml ["mlw", "why"]
  WhyML programming and specification language

Read more about them in the Documentation of Why3.

To use some library (with computational code or logical code), you should import it with:

use Some_Library
use Another_Library as AL

and to use symbols from them directly or prefixed (if you used ... as prefix). After installation, you can find Why3 libraries here: /usr/share/why3/stdlib. There are .mlw libraries looking as:

(** {1 Basic Algebra Theories} *)

(** {2 Associativity} *)

module Assoc

  type t
  function op t t : t
  axiom Assoc : forall x y z : t. op (op x y) z = op x (op y z)

end

(** {2 Commutativity} *)

module Comm

  type t
  function op t t : t
  axiom Comm : forall x y : t. op x y = op y x

end
...

You import it with use and its "theories" (old name for "module"-s) with their lemmas, axioms, functions, types, predicates, etc - are in your code, your code can be based on some lemma now.

For example:

 1   module Test2
 2   
 3     use int.Int             (* for <, <=, etc *)
 4     use list.List           (* for list, Cons, Nil, etc *)
 5     use list.Length as LL   (* for list's length *)
 6     use list.Nth            (* for nth over lists *)
 7     use option.Option       (* for option, None, Some *)
 8   
 9     goal bounded_nth:
10       forall i: int, l: list 'a.
11         0 <= i < LL.length l ->
12         nth i l <> None
13   
14   end

and if to try to prove this bounded_nth goal:

$ why3 prove -P z3 Test2.mlw
File "Test2.mlw", line 10, character 4 to line 12, character 21:
Goal bounded_nth.
Prover result is: Timeout (5.00s, 7412868 steps).

then we hit timeout. We need some lemma to prove this claim (that nth returns something, i.e., not None if the index is bounded by the length of the list). But if to add:

...
use list.NthLength
...

then some important lemmas will come into our code, become available behind the scene and Why3 will use them to prove the goal:

$ why3 prove -P z3 Test2.mlw
File "Test2.mlw", line 11, character 4 to line 13, character 21:
Goal bounded_nth.
Prover result is: Valid (0.01s, 12337 steps).

The library "came" from the module NthLength written in /usr/share/why3/stdlib/list.mlw file. How does Why3 find it? If to call why3 config show, you will see:

...
[main]
default_editor = "xdg-open %f"
loadpath = "/usr/share/why3/stdlib"
magic = 14
memlimit = 1000
running_provers_max = 2
timelimit = 5.000000
...

this is the merge of default (embedded) settings and your home config which is $HOME/.why3.conf. Other directories used by why3:

$ why3 --print-datadir
/usr/share/why3

$ why3 --print-libdir
/usr/lib/x86_64-linux-gnu/ocaml/5.3.0/why3

You can add new directory for search (for libraries) using environment variable, config file or with CLI option -L <path>.

We can avoid import of list.NthLength and to write them by hand in the top of our Test2 module:

1   lemma nth_none_1:
2      forall l: list 'a, i: int. i < 0 -> nth i l = None
3 
4   lemma nth_none_2:
5      forall l : list 'a, i: int. i >= LL.length l -> nth i l = None
6 
7   lemma nth_none_3:
8      forall l: list 'a, i: int. nth i l = None -> i < 0 \/ i >= LL.length l

Then to try to prove it with:

$ why3 prove -L . -P z3 Test2.mlw
File "Test2.mlw", line 11, characters 5-55:
Goal nth_none_1.
Prover result is: Timeout (5.00s, 8394760 steps).

File "Test2.mlw", line 14, characters 5-67:
Goal nth_none_2.
Prover result is: Timeout (5.00s, 9386120 steps).

File "Test2.mlw", line 17, characters 5-75:
Goal nth_none_3.
Prover result is: Timeout (5.00s, 8412995 steps).

File "Test2.mlw", line 20, character 4 to line 22, character 21:
Goal bounded_nth.
Prover result is: Valid (0.00s, 12337 steps).

Proving of them is naturally induction based. To force Why3 to use induction, we apply transformation:

$ why3 prove -L . -P z3 --apply-transform induction_ty_lex Test2.mlw
File Test2.mlw:
Goal nth_none_1.
Prover result is: Valid (0.01s, 9815 steps).

File Test2.mlw:
Goal nth_none_2.
Prover result is: Valid (0.01s, 10099 steps).

File Test2.mlw:
Goal nth_none_3.
Prover result is: Valid (0.01s, 11017 steps).

File Test2.mlw:
Goal bounded_nth.
Prover result is: Valid (0.01s, 12067 steps).

Now everything is fine! No more timeouts. Why? Because we helped Why3 with a transformation. What is it?

In Why3, a transformation is a program that takes a verification goal (or a collection of goals) and rewrites it into one or more new goals. For example, transformations can:

• Simplify a goal or remove redundant hypotheses.
• Split a conjunction or a goal with multiple branches into separate goals.
• Introduce definitions or unfold them.
• Instantiate quantified formulas.
• Eliminate certain constructs or encode them into simpler logic.
• Prepare a goal for a particular prover, such as by changing its shape or encoding.

WhyML programs produce proof goals; Why3 transformations reshape those goals for proof.

Why3 transformations are broadly similar to tactics: they take a proof goal and change it into subgoals that are easier to prove. The distinction is mostly about how they’re used:

A Why3 transformation is a named, reusable operation in Why3’s proof workflow (for example, splitting a goal or simplifying it). A tactic often suggests an interactive proof command, possibly with a script or search procedure that applies several steps.

Why3 transformations can be applied interactively in the IDE or passed in CLI. Some are simple goal rewrites; others perform more substantial encodings or preprocessing. So “tactic-like” is a good analogy, though not every transformation corresponds to a single tactic step.

So, transformation - is rewriting. See the diagram:

                   WhyML source
                         |
                         v
           Why3 parses and type-checks
                         |
                         v
           Verification conditions (tasks)
                         |
                         v
            optional transformations           .---------.
         split, simplify, inline, etc.     <---  H E R E |
         (applied in the IDE or via CLI)       `---------'
                         |
                         v
          Task sent to a selected prover
                         |
                         v
           Why3 driver translates the task
           into the prover's input language
                         |
                         v
            SMT-LIB (for an SMT solver)
                         |
                         v
                    SMT solver
                         |
                         v
       Result: Valid/Invalid/Unknown/Timeout
                         |
                         v
        Why3 reports the result and records
              it in the proof session

Let's put this into a separate file called MyListLemmas.mlw:

 1   module MyListLemmas
 2   
 3     use int.Int
 4     use list.List
 5     use list.Length as LL
 6     use list.Nth
 7     use option.Option
 8   
 9     lemma nth_none_1:
10        forall l: list 'a, i: int. i < 0 -> nth i l = None
11   
12     lemma nth_none_2:
13        forall l : list 'a, i: int. i >= LL.length l -> nth i l = None
14   
15     lemma nth_none_3:
16        forall l: list 'a, i: int. nth i l = None -> i < 0 \/ i >= LL.length l
17   end

then "import" it with use MyListLemmas.MyListLemmas and prove the Test2 again:

 1   module Test2
 2   
 3     use int.Int
 4     use list.List
 5     use list.Length as LL
 6     use list.Nth
 7     use option.Option
 8     use MyListLemmas.MyListLemmas  (* <= ADDED USE ! *)
 9   
10     goal bounded_nth:
11       forall i: int, l: list 'a.
12         0 <= i < LL.length l ->
13         nth i l <> None
14   
15   end

$ why3 prove -L . -P z3 Test2.mlw
File "Test2.mlw", line 12, character 4 to line 14, character 21:
Goal bounded_nth.
Prover result is: Valid (0.00s, 12337 steps).

Voila! Works. Now prove MyListLemmas.mlw without transformations:

$ why3 prove -L . -P z3 MyListLemmas.mlw 
File "MyListLemmas.mlw", line 10, characters 5-55:
Goal nth_none_1.
Prover result is: Timeout (5.00s, 7327706 steps).

File "MyListLemmas.mlw", line 13, characters 5-67:
Goal nth_none_2.
Prover result is: Timeout (5.00s, 8989493 steps).

File "MyListLemmas.mlw", line 16, characters 5-75:
Goal nth_none_3.
Prover result is: Timeout (5.00s, 7688072 steps).

Timeouts! It seems Why3 TRUSTS IMPORTED SOURCES WITHOUT TO PROVE THEM!.

Look, let's create 2 files: Evil.mlw and Test3.mlw:

(* Evil.mlw *)
module Evil
  use int.Int
  lemma completely_false:
    false
end
---------------------------
(* Test3.mlw *)
module Test3
  use Evil.Evil
  lemma test:
    false
end

Let's prove Test3.mlw:

$ why3 prove -L . -P z3 Test3.mlw 
File "Test3.mlw", line 4, characters 4-9:
Goal test.
Prover result is: Valid (0.00s, 4 steps).

Incredible!!! Our suggestion was right!

If to comment out: (*use Evil.Evil*) line, then proving of Test3.mlw sure FAILS:

$ why3 prove -L . -P z3 Test3.mlw 
File "Test3.mlw", line 4, characters 4-9:
Goal test.
Prover result is: Unknown (sat) (0.00s, 7 steps).

So, Why3 trusts included/used theories (theory keyword was replaced by module in new versions):

W͟h͟y͟3͟ ͟D͟O͟E͟S͟ ͟N͟O͟T͟ ͟D͟O͟ ͟t͟h͟i͟s͟ ͟o͟n͟ ͟"͟u͟s͟e͟"͟                    W͟h͟y͟3͟ ͟D͟O͟E͟S͟ ͟t͟h͟i͟s͟

              ╳                                         ✔
              
          "use XYZ"                                 "use XYZ"
              |                                         |
              v                                         v
          find .mlw                                 find .mlw
              |                                         |
              v                                         v
    prove every lemma in it             l͟o͟a͟d͟ d͟e͟c͟l͟a͟r͟a͟t͟i͟o͟n͟s͟ o͟f͟ t͟h͟e͟ m͟o͟d͟u͟l͟e͟s͟
              |                                         |
              v                                         v
 import the proved results                 use them as trusted theories

ACL2 Theorem Prover is different here: its books are "CERTIFIED" - must be signed after successful proving - look more here about Certified Books in ACL2.

So if the theory contains: lemma P: A then the importing theory can use P as a fact without generating/proving P's VC.

As you see transformations are applied in CLI or in IDE, not in the source written in WhyML (in WhyML meta-program you can only add hints for transformations).

If to open MyListLemmas.mlw in the IDE (yeah, Why3 has IDE! Run it why3 ide MyListLemmas.mlw) then you will see something like (in the left panel):

Status | Theories/Goals               | Time
  ?      ▼ 🗁  MyListLemmas.mlw  
  ?        ▼ 🗁  MyListLemmas    
  ?          🗎 nth_none_1       
  ?          🗎 nth_none_2       
  ?          🗎 nth_none_3       

And you can try to prove them (all together with popup on the module "MyListLemmas" or individually, lemma by lemma) - just select the prover (CVC4, Z3, etc) - you will hit TIMEOUT!

But if to apply transformation (menu "Tools/Transformations (e-r)/induction_tylex") on the whole module and then to call proving with the popup on the module (!) (even CVC4 works fine now), you will get the result immediately, see the new picture of proven goals:

Status | Theories/Goals               | Time
  ✔      ▼ 🗁  MyListLemmas.mlw         
  ✔        ▼ 🗁  MyListLemmas           
  ✔          🗎 nth_none_1              
  ✔          ▼ 🛠 induction_ty_lex      
  ✔            ▼ 🗎 0                   
  ✔                \ CVC4 1.8           0.01 (steps: 4983)
  ✔      ▼ 🗁  MyListLemmas.mlw         
  ✔        ▼ 🗁  MyListLemmas           
  ✔          🗎 nth_none_2              
  ✔          ▼ 🛠 induction_ty_lex      
  ✔            ▼ 🗎 0                   
  ✔                \ CVC4 1.8           0.02 (steps: 5148)
  ✔      ▼ 🗁  MyListLemmas.mlw         
  ✔        ▼ 🗁  MyListLemmas           
  ✔          🗎 nth_none_3
  ✔          ▼ 🛠 induction_ty_lex      
  ✔            ▼ 🗎 0                   
  ✔                \ CVC4 1.8           0.02 (steps: 5322)

Now you can save it as a session or a ZIP file with a session. Why3 will save 2 files actually - the menu "File/Save session and files":

:
├── MyListLemmas
│   ├── why3session.xml
│   └── why3shapes.gz
├── MyListLemmas.mlw
:

Files are:

1. why3session.xml: session stores the transformations you performed on each verification condition, as well as the provers you ran.
2. why3shapes.gz: compressed database of proof shapes used by Why3’s proof-session replay.

The shapes file contains checksums and shapes of goals. Why3 uses these when source programs change, so it can identify corresponding/unchanged goals and merge/reconcile proof-session information.

why3shapes.gz is not required to replay a proof session.

When replaying a session - often after the source or Why3 setup has changed - Why3 can use these shapes to help match old proof attempts to the corresponding new goals and decide what can be replayed:

<saved Why3 session>
          |
          +-- proof tree: transformations and prover calls
          `-- why3shapes.gz: goal-shape data for matching/replay

OK, exit from the IDE where you proved the theory INTERACTIVELY. Now open it again:

$ why3 ide MyListLemmas.mlw

Magic!!! You see the same picture - the picture of proven goals even with wasted time:

• which transformations you chose
• which provers you tried
• which time limits you used
• which branches succeeded
• which branches failed...