search

project-everest / mitls-fstar

Verified implementation of TLS 1.3 in F*
https://www.mitls.org
Other
173 stars 16 forks source link

Range.fst query takes a long time with z3 4.5.0, while goes through quickly with z3 nightly build (48e37b0e1603) #164

Closed aseemr closed 6 years ago

aseemr commented 7 years ago

The lemma in question is: Range.fst:targetLength_converges. Following are the numbers:

With z3 4.5.0, using hints:

(.\Range.fst(295,0-296,27)@queries-Range-31.smt2) Query-stats (Range.targetLength_converges, 4) succeeded (with hint) in 1548525 milliseconds with fuel 1 and ifuel 1 and rlimit 544656000

With z3 4.5.0, not using hints:

(.\Range.fst(295,0-296,27)) Query-stats (Range.targetLength_converges, 4) succeeded in 263563 milliseconds with fuel 1 and ifuel 1 and rlimit 544656000

With z3 nightly build (48e37b0e1603), using hints:

(.\Range.fst(295,0-296,27)) Query-stats (Range.targetLength_converges, 4) succeeded (with hint) in 19690 milliseconds with fuel 1 and ifuel 1 and rlimit 544656000

We should revisit it when upgrading z3. Commenting the lemma for now.

s-zanella commented 7 years ago

Do you mean that you're adding an admit()? The lemma is used elsewhere.

aseemr commented 7 years ago

Oh yes, that's what I meant (777a6fe008636810c0aa091f12d3a78b7470c0f1).

markulf commented 7 years ago

Would it make sense to set a verification level, similar to a debug level?

This way the lemma could be proven for nightly builds and admitted otherwise?

s-zanella commented 6 years ago

We are now all using Z3 nightly and Range verifies in a reasonable time even without hints. I removed the admit() but kept a comment pointing to this issue in targetLength_converges in case this issue recurs.

Closed by https://github.com/mitls/mitls-fstar/commit/b58aac2f9aa36e2746ff937b405cea32893a2ee9