FStarLang/FStar

Possible unsoundness in the SMT encoding

Closed this issue · 2 comments

puyral commented

Hello,

I've been trying recently, out of curiosity, to change fstar's backend from z3 to vampire. I made the discovery that vampire is able to deduce unsat from any fstar file.

The bug in general

Here are the steps to reproduce:

  1. have an fstar file that leads to the generation of an smt file when using #push-options "--log_queries"
  2. make the resulting smt file more smt compliant, that is
  • add the arity to the sort declarations: (declare-sort Term) becomes (declare-sort Term 0)
  • rewrite the datatype declaration to be valid: (declare-datatypes () ((Fuel (ZFuel) (SFuel (prec Fuel))))) becomes (declare-datatypes ((Fuel 0) (((ZFuel) (SFuel (prec Fuel)))))
  • turn any implies into => and any iff into =
  • remove all the echo (this may be a limitation for vampire)

When this is done, vampire always returns:

% Warning: check-sat is not the last entry. Skipping the rest!
% Refutation found. Thanks to Tanya!
% SZS status Unsatisfiable for queries-Test3
% SZS output start Proof for queries-Test3
36. ! [X0 : 'Term()',X1 : 'Term()'] : ('HasType'(X0,X1) => 'Valid'(X1)) [input]
114. $false <=> 'Valid'('Prims.l_False') [input]
3182. ! [X0 : 'Term()'] : ('NoHoist'(X0,'HasType'('FStar.Pervasives.with_type@tok','Tm_arrow_99724436653747ac6f5a6a00c64ff8bc')) & ! [X2 : 'Term()',X1 : 'Term()'] : 'FStar.Pervasives.with_type'(X1,X2) = 'ApplyTT'('ApplyTT'('FStar.Pervasives.with_type@tok',X1),X2)) [input]
3184. ! [X0 : 'Term()',X1 : 'Term()'] : ('FStar.Pervasives.with_type'(X0,X1) = X1 & 'HasType'('FStar.Pervasives.with_type'(X0,X1),X0)) [input]
3268. ! [X0 : 'Term()'] : ('NoHoist'(X0,'HasType'('FStar.Pervasives.with_type@tok','Tm_arrow_99724436653747ac6f5a6a00c64ff8bc')) & ! [X1 : 'Term()',X2 : 'Term()'] : 'FStar.Pervasives.with_type'(X2,X1) = 'ApplyTT'('ApplyTT'('FStar.Pervasives.with_type@tok',X2),X1)) [rectify 3182]
3270. ! [X0 : 'Term()'] : ('NoHoist'(X0,bG8) & ! [X1 : 'Term()',X2 : 'Term()'] : 'FStar.Pervasives.with_type'(X2,X1) = 'ApplyTT'('ApplyTT'('FStar.Pervasives.with_type@tok',X2),X1)) [fool elimination 3268]
5908. ~'Valid'('Prims.l_False') [true and false elimination 114]
5909. ~'Valid'('Prims.l_False') [flattening 5908]
7619. ! [X0 : 'Term()',X1 : 'Term()'] : ('Valid'(X1) | ~'HasType'(X0,X1)) [ennf transformation 36]
18245. 'HasType'('FStar.Pervasives.with_type'(X0,X1),X0) [cnf transformation 3184]
18246. 'FStar.Pervasives.with_type'(X0,X1) = X1 [cnf transformation 3184]
18248. 'FStar.Pervasives.with_type'(X2,X1) = 'ApplyTT'('ApplyTT'('FStar.Pervasives.with_type@tok',X2),X1) [cnf transformation 3270]
39240. ~'Valid'('Prims.l_False') [cnf transformation 5909]
39332. 'Valid'(X1) | ~'HasType'(X0,X1) [cnf transformation 7619]
39446. 'ApplyTT'('ApplyTT'('FStar.Pervasives.with_type@tok',X0),X1) = X1 [definition unfolding 18246,18248]
39447. 'HasType'('ApplyTT'('ApplyTT'('FStar.Pervasives.with_type@tok',X0),X1),X0) [definition unfolding 18245,18248]
57751. 'HasType'(X1,X0) [forward demodulation 39447,39446]
68272. 'Valid'(X1) [subsumption resolution 39332,57751]
69295. $false [resolution 68272,39240]
% SZS output end Proof for queries-Test3
% ------------------------------
% Version: Vampire 4.7 (commit 8bd968421 on 2022-11-30 18:30:46 +0000)
% Linked with Z3 4.9.1.0 6ed071b44407cf6623b8d3c0dceb2a8fb7040cee z3-4.8.4-6427-g6ed071b44
% Termination reason: Refutation

% Memory used [KB]: 72664
% Time elapsed: 2.031 s
% ------------------------------
% ------------------------------

A suspicious axiom

Looking deeper, I could find one suspicious axiom:

(assert (! (forall ((@x0 Term) (@x1 Term))
 (! (and (= (FStar.Pervasives.with_type @x0
@x1)
@x1)
(HasType (FStar.Pervasives.with_type @x0
@x1)
@x0))
 :weight 0


:pattern ((FStar.Pervasives.with_type @x0
@x1))
:qid @with_type_primitive_axiom))
:named @with_type_primitive_axiom))

If I understand correctly, with this axiom, it is possible to prove that anything has any type.

A minimal example

From the following fstar program

module Test3
#push-options "--log_queries"

irreducible
let f (x:nat) = x

let g (_:unit) = 
    assert (f 2 == f 3 + f 1)

I can extract the following axioms and declaration:

(declare-datatypes () ((Fuel 
(ZFuel) 
(SFuel (prec Fuel)))))
(declare-sort Term )
(declare-fun Prims.l_False () Term)
(declare-fun Valid (Term) Bool)
(declare-fun MaxIFuel () Fuel)
(declare-fun HasTypeFuel (Fuel Term Term) Bool)
(define-fun HasType ((x Term) (t Term)) Bool
(HasTypeFuel MaxIFuel x t))
(declare-fun FStar.Pervasives.with_type (Term Term) Term)


(assert (! (iff false
(Valid Prims.l_False))
:named false_interp))

(assert (forall ((e Term) (t Term))
(! (implies (HasType e t)
(Valid t))
:pattern ((HasType e t)
(Valid t))
:qid __prelude_valid_intro)))

(assert (! (forall ((@x0 Term) (@x1 Term))
 (! (and (= (FStar.Pervasives.with_type @x0
@x1)
@x1)
(HasType (FStar.Pervasives.with_type @x0
@x1)
@x0))
 :weight 0


:pattern ((FStar.Pervasives.with_type @x0
@x1))
:qid @with_type_primitive_axiom))
:named @with_type_primitive_axiom))

(check-sat)

And then even z3 proves unsat

nikswamy commented

Thanks @puyral!

with_type e t is quite special and is emitted in F*'s encoding to SMT at specific points where the typechecker has proven internally that e has type t. F* disables model-based quantifier instantiation (MBQI) in Z3 and relies, especially for cases like this, on pattern-based quantifier instantiation. Indeed, even in your minimized SMT2 file, if you add (as F* does) (set-option :smt.mbqi false) (set-option :auto-config false), Z3 says unknown.

That said, as you point out, when seen as an axiom on its own, it is clearly unsound. Rather than relying on quantifier triggers, we should see if there's a way to remove the with_type construction altogether. Especially if that would enable F* to be used with vampire, that would be really nice. Stay tuned, we'll look into what it takes to remove with_type.

  • 👍1
aseemr commented

This was more or less unused, I removed it and pushed the changes to the master branch. Closing this issue, please reopen if needed. Thanks!