drule.ml: fail term_match early when a substitution would let a bound variable escape - #191

…ariable escape

In term_pmatch, a pattern variable that is in neither "env" nor lconsts was
assigned whatever subterm it met, including one with a free occurrence of a
variable bound over it on the target side. Such an assignment can never
reproduce the target, since INSTANTIATE renames the pattern's own binder rather
than capturing the variable, so PART_MATCH's closing alpha check rejected it --
but only after a full INSTANTIATE had already built a theorem.

That is what makes the basic rewrites EXISTS_SIMP and FORALL_SIMP
(`(?x. t) <=> t`, `(!x. t) <=> t`) so expensive on s2n-bignum-shaped goals
(awslabs/s2n-bignum#209): each failing attempt
against a `?y. body[y]` first ran a capture-avoiding substitution over the body
-- a "variant" scan, a vsubst traversal, a kernel INST and a failing ALPHA,
several traversals of the body in all. A vfree_in check against env in the
inserter replaces that with a single vfree_in scan, which stops at the first
occurrence of the bound variable: effectively constant time when the body
mentions y early, and still linear in the body but much cheaper when y occurs
only at the very end. Where the check does not fire it costs one extra scan of
the matched subterm, so a match that does succeed against a large subterm gets
somewhat slower.

term_match itself keeps its permissive behavior, which its documentation
already warns about, so the check is exposed as a separate term_match_checked
and only PART_MATCH and GEN_PART_MATCH are switched over. Every other caller is
unaffected; in particular net_of_thm still classifies permutative rewrites with
the permissive matcher, so rewrite nets come out exactly as before. The check
covers the first order case only -- the higher order paths in term_homatch can
still build an escaping instantiation -- and PART_MATCH's alpha check is
retained as the real guarantee. Which matches succeed should be unchanged.

UnitTests/basic_tests.ml gains five checks: term_match still accepts the
escaping match, term_match_checked rejects it, the two agree on a first order
match, REWR_CONV EXISTS_SIMP still fails on `?y. P y`, and it still succeeds on
`?y. T`. Help/term_match_checked.hlp documents the new function, and
Help/term_match.hlp points at it.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>