fstarlang-smtprofiling from smithery.ai

Invocation

This skill is used when:

Verifying F* (.fst) or interface (.fsti) files
Debugging verification failures and proof performance
Especially when proofs require high rlimits or fail unpredictably

Core Operations

Collect an .smt2 file for problematic proof

Wrap the part of the program to diagnose proof failures with

#push-options "--log_queries --z3refresh --query_stats --split_queries always"
let definition_to_be_debugged ...
#pop-options

Run F* on the file (with appropriate include paths)

fstar.exe Module.fst

The log messages will show the name of the .smt2 file logged for each proof obligation

Verify .smt2 file independently of F*

Find z3 in the path. It might be named z3-4.13.3, z3-4.15.1 etc., with a version number suffix

z3 queries-myquery.smt2

You can add z3 options like smt.qi.profile=true to see which quantifiers were firing too much and what to do about it

Interpreting a quantifier profile

Some quantifiers in F*'s SMT encoding always fire a lot---this is by design. Typically, quantifiers with unqualified names (Box_bool_proj_0) or those with names in Prims, or FStar. Pervasives will fire a lot.

Look for quantifiers in modules that are in files that you authored that are firing a lot---these might signify that you should write a pattern for those quantifiers, or control their instantiation explicitly.

More information on SMT profiling

Find the directory PoP-in-FStar on the local machine, or locate it here: https://github.com/FStarLang/PoP-in-FStar

The section under_the_hood/uth_smt.rst contains information about F*'s SMT encoding and how to profile.