Revise the SMT encoding of top-level prop definitions

[nikswamy]

[Following up on #3440]

Say you define:

let some_pred (x:t) = forall y. p x y

The existing behavior for this in the SMT encoding is to produce something like

(forall x. (! (= (some_pred x) (Prims.l_forall (Tm_abs ...)) :pattern ((Prims.subtype_of (some_pred x) Prims.unit)))

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

(forall x. (! (implies (HasType x t) (Valid (Prims.subtype_of (some_pred x) Prims.unit)) :pattern ((Prims.subtype_of (some_pred x) Prims.unit))))

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.

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:

1. 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.

2. 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.