How to verify Why3 output of Proof Obligations

0
votes

I believe I can generate proofs using why3 with different provers,

  1. frama-c -wp -wp-prover cvc4 -wp-rte -wp-out proof swap.c
  2. frama-c -wp -wp-prover z3-ce -wp-rte -wp-out proof swap.c
  3. frama-c -wp -wp-prover alt-ergo -wp-rte -wp-out proof swap.c

This generates different 'why' files. I would like to validate the proof obligations with an external program. It seems each proof obligation is in a different format; LispClojure and OCaml? What exactly is the format? Is it correct that these are proof and are sufficient to show the contract/proof is correct without proving that Z3, alt-ergo, etc are correct?

swap.c

For the wp tutorial,

int h = 42;
/*@
  requires \valid(a) && \valid(b);
  assigns *a, *b;
  ensures *a == \old(*b) && *b == \old(*a);
*/
void swap(int* a, int* b)
{
    int tmp = *a;
    *a = *b;
    *b = tmp;
}

int main()
{
    int a = 24;
    int b = 37;

    //@ assert h == 42;

    swap(&a, &b);

    //@ assert a == 37 && b == 24;
    //@ assert h == 42;
    
    return 0;
}

This works fine and the frama-c-gui shows me how to develop contracts and annotations.

Alter-ergo

(* WP Task for Prover Alt-Ergo,2.4.1 *) (* this is the prelude for Alt-Ergo, version >= 2.4.0 *) (* this is a prelude for Alt-Ergo integer arithmetic *) (* this is a prelude for Alt-Ergo real arithmetic *) type string

logic match_bool : bool, 'a, 'a -> 'a

axiom match_bool_True :   (forall z:'a. forall z1:'a. (match_bool(true, z, z1) = z))

The full proof is truncated for brevity.

z3-ce

(* WP Task for Prover Z3,4.8.11,counterexamples *) ;;; generated by SMT-LIB2 driver ;;; SMT-LIB2 driver: bit-vectors, common part ;;; generated by SMT-LIB strings ;;; generated by SMT-LIB strings (set-option :produce-models true) ;;; SMT-LIB2: integer arithmetic ;;; SMT-LIB2: real arithmetic (declare-sort uni 0)

(declare-sort ty 0)

(declare-fun sort (ty uni) Bool)

(declare-fun witness (ty) uni)

The full proof is truncated for brevity.

1
frama-cwhy3
ZMT-LIB is found at the URL smtlib.cs.uiowa.edu. It looks like both Z3 and CVC4 use this format as output. Still not sure about Alt-Ergo. - artless noise
Removing the first line (* WP Task for Prover...) and I can use cvc4 --lang smt2 file.why and z3 -smt2 file.why process the files, where 'file.why' was produced with that prover. I can not verify z3 output with cvc4, for instance... smtlib grammar in flex/bison - artless noise

1 Answers

1
votes

I have to admit that I'm not completely sure that I completely understand what you want to achieve here, but here are the answers to your questions:

It seems each proof obligation is in a different format; Lisp and OCaml? What exactly is the format?

These files represent the formulas that are given to the provers you ask Frama-C to launch. The format depends on the prover. If I recall correctly, for many provers, this will be smtlib, or tptp, but some provers such as Alt-Ergo can also enjoy a custom output. The generation of the file is described by Why3's driver files, as mentioned (quite briefly) in section 12.4 of the Why3 manual.

Is it correct that these are proof ?

No, these are formulas to be validated by the prover they have been generated for.

and are sufficient to show the contract/proof is correct without proving that Z3, alt-ergo, etc are correct?

No. If the provers you use have a bug, they might mistakenly tell you that a given proof obligation is valid. Some provers are able to provide a proof trace (e.g. if you tweak a driver to use the get-proof command of smtlib), but as far as I know, the format of such a trace is prover-specific, so that it would probably be difficult to have it checked by an external tool.