Why3: debug, part 1

Lets say we have such WhyML code:

module Call1
  use int.Int

  type trace = { mutable f1_calls: int }

  let ghost trace : trace = { f1_calls = 0 }

  predicate f1_was_called (before after: int) = after = before + 1
  predicate f1_was_not_called (before after: int) = after = before  

  let ghost f1 () : unit
    writes { trace.f1_calls }
    ensures { f1_was_called (old trace.f1_calls) trace.f1_calls }
  =
    trace.f1_calls <- trace.f1_calls + 1

  let f2 (a1: int) : int
    writes { trace.f1_calls }
    ensures { result = if a1 = 0 then 100 else 101 }
    ensures { a1 = 0 -> f1_was_not_called (old trace.f1_calls) trace.f1_calls }
    ensures { a1 <> 0 -> f1_was_called (old trace.f1_calls) trace.f1_calls }
  = if a1 = 0 then begin
     f1 ();
     100
    end
    else begin
      f1 ();
      101
    end

  let main () : unit
    requires { trace.f1_calls = 0 }
    ensures { trace.f1_calls = 0 }
  =
    let _ = f2 0 in
    ()

end

it is explained here. If to prove it:

$ why3 prove Call1.mlw -P z3 
File Call1.mlw:
Goal f1'vc.
Prover result is: Valid (0.00s, 38 steps).

File Call1.mlw:
Goal f2'vc.
Prover result is: Unknown (sat) (0.00s, 258 steps).

File Call1.mlw:
Goal main'vc.
Prover result is: Valid (0.00s, 40 steps).

i.e., f2 cannot be proven. What does it mean?

See this - it is the source code of Why3 describing possible values of a prover result - one of them is Unknown:

type prover_answer = 
| Valid                   (* The task is valid according to the prover *)
| Invalid                 (* The task is invalid *)
| Timeout                 (* The task timeouts, ie it takes more time than specified *)
| OutOfMemory             (* The task runs out of memory *)
| StepLimitExceeded       (* The task required more steps than the limit provided *)
| Unknown of string       (* The prover can't determine if the task is valid *)
| Failure of string       (* The prover reports a failure *)
| HighFailure of string   (* An error occured during the call to the prover
                             or none of the given regexps match the output of the prover *)

Why3 forms a request to SMT and the result of SMT is "sat":

Prover result is: Unknown (sat) (0.00s, 258 steps).
                           ^^^
                         t h i s

There are 2 different questions a solver can ask about a Why3 verification condition (VC):

• Is the formula satisfiable (sat)? Can it be true under some assignment of values?
• Is the formula unsatisfiable (unsat)? Is there no assignment of values that makes it true?

For verification, Why3 normally wants to prove that the VC is valid. An equivalent way to do that is to ask whether its negation is unsatisfiable.

So, possible answers of SMT in short are:

Solver result	Meaning for verification
unsat	No counterexample exists; the VC is proved.
sat	A counterexample exists; the VC is not valid.
unknown	The solver cannot decide.

Why3 translates the prover's responses into its own result categories, including Valid, Invalid, and Unknown - see prover answer.

So, the result is "The prover can't determine if the task is valid", and SMT returned "sat".

We can check it watching the requests to the SMT solver. First, create directories, let's say "A" and "B" (mkdir A B) and then:

$ why3 prove Call1.mlw -P z3 -T Call1 -G "f2'vc" -o A

This command saves the request corresponding to the goal f2 to SMT in a directory A/, there you can see only one file, e.g., Call1-Call1-f2qtvc.smt2. Another terminology - SMT solver trace.

If to execute:

$ why3 prove Call1.mlw -P z3 -o B

There:

B
├── Call1-Call1-f1qtvc.smt2
├── Call1-Call1-f2qtvc.smt2
└── Call1-Call1-mainqtvc.smt2

1 directory, 3 files

There are 3 requests of SMT regarding 3 goals (f1, f2, main). But we have a problem with f2 only, so lets see it:

;;; generated by SMT-LIB2 driver
;;; SMT-LIB2 driver: bit-vectors, common part
;;; generated by SMT-LIB strings
;;; SMT-LIB2: integer arithmetic
(declare-datatypes ((trace 0))
  (((traceqtmk (f1_calls Int)))))

;; "f1_was_called"
(define-fun f1_was_called ((before Int) (after Int)) Bool
  (= after (+ before 1)))

;; Goal "f2'vc"
;; File "Call1.mlw", line 17, characters 6-8
(assert
  (not
  (forall ((trace1 Int))
    (forall ((a1 Int))
      (ite (= a1 0)
        (forall ((trace2 Int))
          (=>
            (f1_was_called trace1 trace2)
            (and
              (= 100 (ite (= a1 0) 100 101))
              (and
                (=> (= a1 0) (= trace2 trace1))
                (=> (not (= a1 0)) (f1_was_called trace1 trace2))))))
        (forall ((trace2 Int))
          (=>
            (f1_was_called trace1 trace2)
            (and
              (= 101 (ite (= a1 0) 100 101))
              (and
                (=> (= a1 0) (= trace2 trace1))
                (=> (not (= a1 0)) (f1_was_called trace1 trace2)))))))))))

(check-sat)

And we can try it in SMT (currently, I use Z3):

$ z3 Call1-Call1-f2qtvc.smt2 
sat

The same "sat". Commands in this listing are Lisp-like language processes by Z3 SMT solver which has a documentation listing these functions-commands - here:

• delcare-datatypes is for our type: traceqtmk is its constructor, 0 is the arity (i.e., trace does not take arguments).
• (define-fun f1_was_called ...) defines our original predicate.
• ;; Goal "f2'vc" - the comment opening the code of the goal's VC
• VC starts with (assert ...) with negation (see not).
• forall introduces quantifiers: ∀trace1∈Z,∀a1∈Z: ....
• (ite cond then_expr else_expr) - if..then..else
• (=> P Q) is classical implication.
• (check-sat) asks Z3 whether all the asserted constraints can be satisfied simultaneously.

Lets rewrite this SMT commands IGNORING CURRENTLY LEADING "NOT" (it's like to write G remembering that the whole formula is ¬G), ok, so G:

∀a1,t1,t2∈Z
a1=0
  /\
  t2=t1+1 -> 100 = (a1=0 /\ 100)
                   \/
                   (a1≠0 /\ 101)
             /\
             (a1=0 -> t2=t1)
             /\
             (a1≠0 -> t2=t1+1)
\/             
a1≠0
  /\
  t2=t1+1 -> 101 = (a1=0 /\ 100)
                   \/
                   (a1≠0 /\ 101)
             /\
             (a1=0 -> t2=t1)
             /\
             (a1≠0 -> t2=t1+1)

∀a1,t1,t2∈Z
a1=0
  /\
  t2=t1+1 -> 100 = 100
             /\
             (⊤ -> ⊥)
             /\
             (⊥ -> ⊤)
\/             
a1≠0
  /\
  t2=t1+1 -> 101 = ⊥
                   \/
                   101
             /\
             (⊥ -> ⊥)
             /\
             (⊤ -> ⊤)

∀a1,t1,t2∈Z
a1=0
  /\
  t2=t1+1 -> ⊤
             /\
             ⊥
             /\
             ⊤
\/             
a1≠0
  /\
  t2=t1+1 -> 101 = 101
             /\
             ⊤
             /\
             ⊤

∀a1,t1,t2∈Z
a1=0
  /\
  t2=t1+1 -> ⊥
\/             
a1≠0
  /\
  t2=t1+1 -> ⊤

Now, looking at the implication's truth table:

p	q	p->q
0	0	1
0	1	1
1	0	0
1	1	1

we see that (see the result p->q relative to p, q is ⊥ or ⊤):

P -> ⊥ ≡ ¬P       █ 
P -> ⊤ ≡ ⊤        ▄ 

taking these 2 into account we get now:

∀a1,t1,t2∈Z
a1=0
  /\
  ¬(t2=t1+1)
\/             
a1≠0
  /\
  ⊤

We can write it as ∀a1,t1,t2∈Z: t2≠t1+1 \/ a1≠0. SMT works with integer domain and easy finds counterexamples, e.g., t2=6, t1=5 and t2=t1+1 in this case which is a contradiction to the universal quantifiers telling "for ANY integers", any, at least for 5, 6 it is not true. We ignored negation, so this is G and it's false, ¬G though is true. It leads to "sat" answer from SMT.

What is this? This is a successful prof treating by Why3 as proving that f2 is Unknown. Why? Because a1=0 /\ ... and a1≠0 /\ ... are ensures {..} in our f2:

...
    ensures { a1 = 0 -> f1_was_not_called (old trace.f1_calls) trace.f1_calls }
    ensures { a1 <> 0 -> f1_was_called (old trace.f1_calls) trace.f1_calls }
...

This is the first way to understand the reason of Unknown.

2 separate conclusions:

• calls of functions (like of f1()) usually are replaced by their postconditions (if they were declared)
• as you see SMT request could be simplified before to be form for SMT, but Why3 did not do it, it means that more strict logical description of situation (more asserts, invariants, ...) can help to make the request more optimal. It makes sense when you hit timeouts, out of memory, too slow prooving...

Another way to see how Why3 came to the conclusion Unknown is to print the whole theory with:

$ why3 prove Call1.mlw -P z3 --print-theory

The result is:

 1   theory Call1
 2     
 3     (* use why3.BuiltIn.BuiltIn *)
 4     
 5     (* use why3.Bool.Bool *)
 6     
 7     (* use why3.Unit.Unit *)
 8     
 9     (* use int.Int *)
10     
11     type trace =
12       | Trace'mk (f1_calls:int)
13     
14     (* meta model_record function f1_calls *)
15     
16     predicate f1_was_called (before:int) (after:int) = after = (before + 1)
17     
18     predicate f1_was_not_called (before:int) (after:int) = after = before
19     
20     goal f1'vc :
21       forall trace:int.
22        let trace'unused = Trace'mk trace in
23        let trace'unused1 = Trace'mk trace in
24        let f1_calls'result'unused = trace in
25        let o = trace + 1 in
26        let (+)'result'unused = o in
27        forall trace1:int.
28         let trace'unused2 = Trace'mk trace1 in
29         trace1 = o -> f1_was_called trace trace1
30     
31     goal f2'vc :
32       forall trace:int.
33        let trace1 = Trace'mk trace in
34        forall a1:int.
35         let trace'unused = trace1 in
36         let (=)'result'unused = (if a1 = 0 then True else False) in
37         if a1 = 0
38         then let trace'unused1 = trace1 in
39              forall trace2:int.
40               let trace'unused2 = Trace'mk trace2 in
41               f1_was_called trace trace2 ->
42               (let result'unused = 100 in
43                100 = (if a1 = 0 then 100 else 101) &&
44                (a1 = 0 -> f1_was_not_called trace trace2) &&
45                (not a1 = 0 -> f1_was_called trace trace2))
46         else let trace'unused1 = trace1 in
47              forall trace2:int.
48               let trace'unused2 = Trace'mk trace2 in
49               f1_was_called trace trace2 ->
50               (let result'unused = 101 in
51                101 = (if a1 = 0 then 100 else 101) &&
52                (a1 = 0 -> f1_was_not_called trace trace2) &&
53                (not a1 = 0 -> f1_was_called trace trace2))
54     
55     goal main'vc :
56       forall trace:int.
57        let trace'unused = Trace'mk trace in
58        trace = 0 ->
59        (let trace'unused1 = Trace'mk trace in
60         forall trace1:int.
61          let trace'unused2 = Trace'mk trace1 in
62          let _'unused = (if true then 100 else 101) in
63          (true -> f1_was_not_called trace trace1) /\
64          (false -> f1_was_called trace trace1) ->
65          (let f2'result'unused = (if true then 100 else 101) in trace1 = 0))
66     
67   end

The line 31 is the f2 goal. It corresponds to SMT script. First if a1 = 0 is the same if in the original f2 function. It introduces 2 branches (they mostly repeat each other bcs they are the same in the original f2). Inside these branches we see ensures {..}:

...
43  100 = (if a1 = 0 then 100 else 101) &&
44  (a1 = 0 -> f1_was_not_called trace trace2) &&
45  (not a1 = 0 -> f1_was_called trace trace2))
...
51  101 = (if a1 = 0 then 100 else 101) &&
52  (a1 = 0 -> f1_was_not_called trace trace2) &&
53  (not a1 = 0 -> f1_was_called trace trace2))
...

;;         SMT request:
(= 100 (ite (= a1 0) 100 101))
(and
  (=> (= a1 0) (= trace2 trace1))
  (=> (not (= a1 0)) (f1_was_called trace1 trace2))))))

The same. The printed theory is the code translated +/- to the SMT request.

Another very interesting place is:

...
47     forall trace2:int.
48      let trace'unused2 = Trace'mk trace2 in
49      f1_was_called trace trace2 ->
...

and if you ask "but where is my call of f1?" then - this is. The function f1 effects the ghost variable trace, so it is created by its constructor Trace'mk (sure under universal quantifier forall trace2:int) and then we see checking of the f1's postcondition: f1_was_called trace trace2. Pay attention, it is represented as a left side of an implication:

It means that the postcondition of f1() is used as a hypothesis for the subsequent proof obligation.

The surrounding quantifiers, implications, and branch conditions determine how that relation is used.

Now, looking at the printed theory, you can also find the problem:

...
if a1 = 0
then let trace'unused1 = trace1 in                                               
     forall trace2:int.                                                a1 = 0 :
      let trace'unused2 = Trace'mk trace2 in                           ~~~~~~~~     
      f1_was_called trace trace2 ->                     ‼  trace2 = trace + 1 ->       ⇽ f1() call
      (let result'unused = 100 in                          result = 100                  ~~~~~~~~~
       100 = (if a1 = 0 then 100 else 101) &&              100 = 100 &&
       (a1 = 0 -> f1_was_not_called trace trace2) &&    ⁈  a1 = 0 -> (trace2 = trace) &&
       (not a1 = 0 -> f1_was_called trace trace2))         a1 <> 0 -> (trace2 = trace + 1)
else let trace'unused1 = trace1 in                                                       
     forall trace2:int.                                                a1 <> 0 :
      let trace'unused2 = Trace'mk trace2 in                           ~~~~~~~~~
      f1_was_called trace trace2 ->                     ‼  trace2 = trace + 1 ->       ⇽ f1() call
      (let result'unused = 101 in                          result = 101                  ~~~~~~~~~
       101 = (if a1 = 0 then 100 else 101) &&              101 = 101 &&
       (a1 = 0 -> f1_was_not_called trace trace2) &&    ⁈  a1 = 0 -> (trace2 = trace) &&
       (not a1 = 0 -> f1_was_called trace trace2))         a1 <> 0 ->
...

and you see that finally we hit: trace2 = trace + 1 -> trace2 = trace, i.e., true -> false which is false, sure.

Debug based on the printed theory (like on SMT request) needs to make mental revrsed translation: from them - back to the original WhyML code. Interesting, that Why3 does not solve it but prepares the query to SMT and SMT simplifies those logical formulas to short answer: "sat".

Yet another approach for debugging is to use a special --debug CLI option (it requires different flags, you can see them with --list-debug-flags):

$ why3 prove Call1.mlw -P z3 --debug vc_debug

The output is an intermediate language used internally by Why3's VC generator, so syntax forms like HAVOC, VAL, STOP, WITH, etc. are part of Why3's internal program representation/VC-generation language:

It is how Why3 symbolically processes program expressions and constructs verification conditions (VC).

if a1 = 0 then
  100
else
  101

          Initial symbolic state:             
             • a1: int                        
             • trace.f1_calls: int            
                      |                       
          Test the condition a1 = 0           
                   /    \                     
                  /      \                    
             a1 = 0    a1 <> 0                
                /          \                  
       first branch       second branch       
       symbolic expr      symbolic expr       

 1   <vc_debug>Calling eval_match with keep_trace = true
 2   K VAL ;
 3     LET o = 0;
 4     LET result = trace'mk o;
 5     LET trace'mk'result = result;
 6     STOP true
 7   K VAL _;
 8     LET trace = trace1;
 9     LET o1 = 1;
10     LET o2 = trace1.f1_calls;
11     LET f1_calls'result = o2;
12     LET o3 = o2 + o1;
13     LET (+)'result = o3;
14     HAVOC { trace @rho -> { f1_calls1 -> [o3]; }};
15     VAL result1;
16     STOP f1_was_called (trace.f1_calls) (trace1.f1_calls)
17   vars = (trace1 -> trace2)
18   regs = (trace @rho -> trace2)
19   <vc_debug>Calling eval_match with keep_trace = true
20   K VAL a1;
21     LET trace3 = trace1;
22     LET o4 = 0;
23     LET o5 = if a1 = o4 then True else False;
24     LET (=)'result = o5;
25     IF o5
26     THEN LET o6 = ();
27          LET trace4 = trace1;
28          HAVOC { trace @rho -> { f1_calls1 -> []; }};
29          VAL _1 WITH f1_was_called (trace4.f1_calls) (trace1.f1_calls);
30          LET f1'result = _1;
31          LET result2 = 100
32     ELSE LET o7 = ();
33          LET trace5 = trace1;
34          HAVOC { trace @rho -> { f1_calls1 -> []; }};
35          VAL _2 WITH f1_was_called (trace5.f1_calls) (trace1.f1_calls);
36          LET f1'result1 = _2;
37          LET result2 = 101;
38     STOP result2 = (if a1 = 0 then 100 else 101) &&
39          (a1 = 0 -> f1_was_not_called (trace3.f1_calls) (trace1.f1_calls)) &&
40          (not a1 = 0 -> f1_was_called (trace3.f1_calls) (trace1.f1_calls))
41   vars = (trace1 -> trace6)
42   regs = (trace @rho -> trace6)
43   vars = (trace1 -> trace7)
44   regs = (trace @rho -> trace7)
45   <vc_debug>Calling eval_match with keep_trace = true
46   K VAL _3 WITH trace1.f1_calls = 0;
47     LET o8 = 0;
48     LET trace8 = trace1;
49     HAVOC { trace @rho -> { f1_calls1 -> []; }};
50     LET _4 = if o8 = 0 then 100 else 101 WITH
51         (o8 = 0 -> f1_was_not_called (trace8.f1_calls) (trace1.f1_calls)) /\
52         (not o8 = 0 -> f1_was_called (trace8.f1_calls) (trace1.f1_calls));
53     LET f2'result = _4;
54     LET result3 = ();
55     STOP trace1.f1_calls = 0
56   vars = (trace1 -> trace9)
57   regs = (trace @rho -> trace9)
58   <vc_debug>Calling eval_match with keep_trace = true
59   File Call1.mlw:
60   Goal f2'vc.
61   Prover result is: Unknown (sat) (0.00s, 258 steps).

You can pass all outputs to AI so it helps you to analyze it: the better together with WhyML original code. AI understands internal representation of the symbolic execution as well as SMT traces (queries), especially since their languages are good documented.

Another technique is to get counterexamples, but they are not so useful. They can be got from IDE (press 'G' while you are on the node which is the result of proving) or from CLI:

first, find the prover with counterexamples:

$ why3 config show
...
[prover]
alternative = "counterexamples"
command = "'/usr/bin/cvc4' --stats --tlimit-per=%T --lang=smt2 %f"
command_steps = "'/usr/bin/cvc4' --stats --rlimit=%S --lang=smt2 %f"
driver = "cvc4_17_counterexample"
editor = ""
in_place = false
interactive = false
name = "CVC4"
shortcut = "cvc4-ce"
version = "1.8"
...

then use this short name "cvc4-ce" (or call it with --check-ce CLI option):

$ why3 prove Call1.mlw -P cvc4-ce
File Call1.mlw:
Goal f1'vc.
Prover result is: Valid (0.01s, 231 steps).

File Call1.mlw:
Goal f2'vc.
Prover result is: Unknown (sat) (0.01s, 725 steps).
The following counterexample model has not been verified
  (not checking CE model, missing option --check-ce):
File int.mlw:
  Line 16:
    a1 : int = 0
File Call1.mlw:
  Line 6:
    trace : trace = {f1_calls = 0}
    trace : trace = {f1_calls = 0}
    trace : trace = {f1_calls = 0}
    trace : trace = {f1_calls = 0}
    trace : trace = {f1_calls = 2}
    trace : trace = {f1_calls = 2}
    trace : trace = {f1_calls = 0}
    trace : trace = {f1_calls = 0}
    trace : int = 0
    trace : int = 0
  Line 13:
    trace : int = 1
    trace : int = -1
  Line 17:
    a1 : int = 0
  Line 22:
    result : int = 100
    result : int = 100
    result : int = 0
    result : int = 0
    result of call at line 22, characters 7-13 : bool = true
    result of call at line 22, characters 7-13 : bool = true
  Line 23:
    trace : trace = {f1_calls = 1}
    trace : trace = {f1_calls = 1}
    trace : int = 1
  Line 27:
    trace : trace = {f1_calls = -2}
    trace : trace = {f1_calls = -2}
    trace : int = -1

File Call1.mlw:
Goal main'vc.
Prover result is: Valid (0.00s, 214 steps).

It seems the line numbers correspond to non-empty lines, see it with nl Call1.mlw. This:

  Line 17:
    a1 : int = 0

could be useful - exactly at a1=0 branch we unexpectedly call f1! Then this:

  Line 23:
    trace : trace = {f1_calls = 1}
    trace : trace = {f1_calls = 1}

but we expected it to be f1_calls = 0 (our ensures { a1 = 0 -> f1_was_not_called (old trace.f1_calls) trace.f1_calls } says it). So, counterexamples also can help, but they look confusing - they are not a trace corresponding to "calls" in some time line

A counterexample is most useful when it gives a concrete input or branch choice. It may be incomplete or awkwardly named, and it can include values that are irrelevant to the failure.

Finally, "Unknown (sat)" means the prover produced a satisfying model for the negated VC, but Why3/Z3 could not establish a proof. In this case, the sat model is the useful part: it exhibits the failing case.