In other words, with a trigger for proving that some_pred x : prop, this axiom introduces an equation in scope defining some_pred x in terms of its "deeply embedded" SMT representation as an application of l_forall to a lambda term.
This is overkill in many cases, especially when it can be determined from the head-constructor of the definition that some_pred x is trivially a prop.
The interaction of this behavior with context_pruning is especially unfortunate, since it means that as soon as some_pred is reachable (and Prims.unit and Prims.subtype_of, but these are almost always reachable), the deep embedding of some_pred also becomes reachable and context pruning ends up pulling in a whole bunch of definitions l_quant_interp etc. for the deeply embedded quantifier that are unnecessary.
So, this PR changes the behavior to the following:
When encoding a top-level "logical" definition like some_pred x, if the definition is a sub-singleton (syntactically determined from its head constructor), then instead of the axiom above, we now generate
The result is that when context pruning, we no longer needlessly bring deeply embedded quantified facts into scope, just by mentioned top-level logical symbols.
Many files that were already using context pruning verify much faster now:
E.g.,
FStar.Sequence.Base.fst: The context is in some cases half as big as previously, with no l_quant_interp facts retained. I observe a significant end-to-end verification time improvement (4.5s now vs 7.2s previously)
Kuiper.MatMul.fst: Previously 8.7s now 4.7s
etc.
There were only two meaningful regressions:
In F* Bug2172: We were relying on the deeply embedded quantifier to bring some constants into scope which results in instantiating an existential quantifier. This is very unpredictable and not something that one should expect to work. I've changed the test case accordingly.
In Pulse: ArraySwap.Proof, the symptom is very similar to Bug2172, where a doubly nested quantifier triggers in an unexpected way to make the proof work. This needed some adjusting. A better fix would be to write a proper pattern on those quantifiers, rather than leaving it to be picked heuristically by Z3.
Note, I've bumped the checked file version, since this changes the SMT encoding and cached declarations in checked files need to be invalidated.
That said, the old behavior is retained with --ext retain_old_prop_typing
Future improvements
If we get rid of the logical type altogether, then the prop-typing of top-level definitions should just follow from regular typing axioms. When that happens, we should be able to remove this special-casing of prop-typing altogether.
[Following up on #3440]
Say you define:
The existing behavior for this in the SMT encoding is to produce something like
In other words, with a trigger for proving that
some_pred x : prop, this axiom introduces an equation in scope definingsome_pred xin terms of its "deeply embedded" SMT representation as an application of l_forall to a lambda term.This is overkill in many cases, especially when it can be determined from the head-constructor of the definition that
some_pred xis trivially a prop.The interaction of this behavior with context_pruning is especially unfortunate, since it means that as soon as
some_predis reachable (and Prims.unit and Prims.subtype_of, but these are almost always reachable), the deep embedding ofsome_predalso becomes reachable and context pruning ends up pulling in a whole bunch of definitions l_quant_interp etc. for the deeply embedded quantifier that are unnecessary.So, this PR changes the behavior to the following:
When encoding a top-level "logical" definition like
some_pred x, if the definition is a sub-singleton (syntactically determined from its head constructor), then instead of the axiom above, we now generateThe result is that when context pruning, we no longer needlessly bring deeply embedded quantified facts into scope, just by mentioned top-level logical symbols.
Impact
I have a green on check-world: https://github.com/FStarLang/FStar/actions/runs/11097438556
Many files that were already using context pruning verify much faster now: E.g.,
FStar.Sequence.Base.fst: The context is in some cases half as big as previously, with no l_quant_interp facts retained. I observe a significant end-to-end verification time improvement (4.5s now vs 7.2s previously)
Kuiper.MatMul.fst: Previously 8.7s now 4.7s
etc.
There were only two meaningful regressions:
In F* Bug2172: We were relying on the deeply embedded quantifier to bring some constants into scope which results in instantiating an existential quantifier. This is very unpredictable and not something that one should expect to work. I've changed the test case accordingly.
In Pulse: ArraySwap.Proof, the symptom is very similar to Bug2172, where a doubly nested quantifier triggers in an unexpected way to make the proof work. This needed some adjusting. A better fix would be to write a proper pattern on those quantifiers, rather than leaving it to be picked heuristically by Z3.
Note, I've bumped the checked file version, since this changes the SMT encoding and cached declarations in checked files need to be invalidated.
That said, the old behavior is retained with
--ext retain_old_prop_typingFuture improvements
If we get rid of the logical type altogether, then the prop-typing of top-level definitions should just follow from regular typing axioms. When that happens, we should be able to remove this special-casing of prop-typing altogether.