Do not force type constructors to be injective#4259
Open
nikswamy wants to merge 29 commits into
Open
Conversation
Create FStarC.Tests.CoreVsRel with 48 tests across 14 groups comparing FStarC.TypeChecker.Core and FStarC.TypeChecker.Rel on subtyping and equality of uvar-free types. Key test groups that document the bug: - Tests 700-706: Type abbreviation with binder variables — Core produces injectivity guard (i == n) instead of unfolding abbreviations - Tests 800-803: Arrow types with variable abbrev args (exact issue #4239) - Tests 900-903: Multi-arg abbreviation with variable args Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
When comparing type abbreviation applications (f a =?= f b) with
matching heads, use a multi-step fallback strategy:
1. Try structural comparison without guards (handles a == b case)
2. If unfolding exposes a refinement type, use the refinement
comparison directly (produces correct weakened guards for
types like natlt i <: natlt n)
3. If unfolding exposes a non-refinement type, try three fallbacks:
a. Unfolded comparison without guards (structurally equal after
unfolding)
b. Structural with guards (handles equatable args like variables,
producing simple arg-level guards for slprop types)
c. Unfolded with guards (handles non-equatable args like constants,
where unfolding may expose equatable functions)
This preserves the #4239 fix (unfolding refinement abbreviations)
while maintaining compatibility with Pulse slprop types and
non-equatable constant arguments (Bug4256 pattern).
Also adds 4 new unit tests for the constant-arg case (tests 1600-1603).
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Adds tests 1700-1704 showing why structural fallback (step 2) is needed in the 3-way non-refinement fallback of compare_head_and_args: - Test 1701: cvr_ha_like c a =?= cvr_ha_like c b (EQUALITY) Core produces simple guard (a == b) via step 2. Rel fails (can't prove type equality without SMT). - Test 1703: cvr_ha_like c a <: cvr_ha_like c b (SUBTYPING) Core guard: a == b (simple, SMT-provable from context) Rel guard: complex formula-level implications from the unfolded arrow domains (forall x. x > c+b ==> x > c+a, etc.) This models ZetaHashAccumulator's ha_val_core pattern where the type abbreviation body uses Pulse slprop connectives (star, exists_, pts_to) in complex ways. Step 2's structural comparison produces a simple arg-level guard that SMT can prove, while step 3 (unfolded with guards) would produce connective-level guards that SMT cannot handle. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Both Core and Rel are now tested with the same settings: - Core: check_term_equality guard_ok=true unfolding_ok=true - Rel: try_teq smt_ok=true Previously Rel was called with smt_ok=false, which made it appear that Rel fails where Core succeeds. In reality, both succeed with guards — just different ones. Core produces simpler arg-level guards (e.g., a == b) while Rel produces formula-level guards from unfolded comparison. All previously RelFailCoreSucceed tests now show BothGuarded. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
In check_slprop_equiv_ext (the prover's final slprop equality proof), first try Core with unfolding_ok=false before falling back to the full check_equiv_now with unfolding. This produces simpler arg-level guards (e.g., X == Y) without looking through type abbreviations, rather than complex formula-level guards from unfolded slprop connective bodies. The Pulse prover has already matched atoms via MKeys at the right abstraction level, so implicit unfolding is unnecessary. Adds check_equiv_now_nounfold to Pulse.Typing.Util: allows SMT guards but disables Core's unfolding (t_check_equiv true false). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
…r slprops Add a new Core API check_term_equality_head_injective that decomposes two terms into head+args, verifies the heads match, then checks argument-wise equality with unfolding and guards allowed. The head itself is never unfolded. Expose this as check_equiv_head_injective in Pulse.RuntimeUtils (implemented directly in OCaml calling Core). The implementation properly discharges SMT guards via Rel.discharge_guard before calling commit(). Modify check_slprop_equiv_ext in the Pulse prover to try head-injective equality first, falling back to full check_equiv_now. This avoids unfolding slprop connectives (which produces complex formula-level guards) while still allowing argument-level unfolding and SMT guards. Remove the now-unused check_equiv_now_nounfold from Pulse.Typing.Util. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Add tests 1800-1802 exercising check_term_equality_head_injective directly: - 1800: reflexive case (identical terms) — trivial success - 1801: different args with same head — produces guard - 1802: mismatched heads — fails as expected Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The 3-way fallback in compare_head_and_args had a 'step 2' that fell back to structural comparison with guards on the ORIGINAL (pre-unfold) terms. This was needed for cases like op_forall_Plus where unfolding produced complex terms (forevery_aux) that SMT couldn't handle. The proper fix is to mark the head symbols as [@unifier_hint_injective]: - op_forall_Star in Pulse.Lib.Forall.fsti - op_forall_Plus in Pulse.Lib.ForEvery.fst When is_marked_injective fires (line 1373), Core goes directly to structural() WITHOUT unfolding, producing simple arg-level guards. This handles the recursive case naturally: nested forall+ applications trigger the injective path at each level. With these annotations, step 2 is no longer needed. The remaining fallback is: try no-guard on unfolded, fall back to unfolded with guards — which is correct for non-injective unfoldable heads. Full CI passes with only pre-existing failures. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Introduce a mechanism where all functions returning a type marked with [@@unifier_hint_injective_type] are treated as injective by default. This avoids unnecessary unfolding in the Pulse prover for slprop comparisons. New attributes: - unifier_hint_injective_type: marks a type so all functions returning it are treated as injective (placed on slprop) - unifier_hint_not_injective: explicit opt-out for specific functions that need unfolding (placed on (**), exists*, on) The is_marked_injective logic (in both Core and Rel) now checks: 1. Explicit [@@unifier_hint_injective] → true 2. Explicit [@@unifier_hint_not_injective] → false 3. Delta_equational (match/if functions) → false 4. Return type has [@@unifier_hint_injective_type] → true 5. Otherwise → false For injective heads, the per-arg comparison strategy is: - First try no_guard(structural) on all args at once - If that fails: compare each arg individually: a. no_guard(check_relation) — handles definitionally equal args b. If both args are lambdas: full check_relation (opens binders) c. Otherwise: emit_guard on original arg pair for SMT Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
…injective annotations With blanket slprop injectivity (unifier_hint_injective_type on slprop), the check_term_equality_head_injective API is now redundant: the full check_term_equality path already handles injective heads via the is_marked_injective check in compare_head_and_args. Similarly, the explicit [@@unifier_hint_injective] annotations on op_forall_Star and op_forall_Plus are redundant since both return slprop and are not Delta_equational, so the blanket rule covers them. Removed: - check_term_equality_head_injective from Core.fst/fsti - check_equiv_head_injective from Pulse.RuntimeUtils.fsti and ML impl - The head-injective fast-path in Pulse.Checker.Prover (now uses check_equiv_now directly, which has the same injective logic built in) - [@@unifier_hint_injective] from op_forall_Star (Pulse.Lib.Forall.fsti) - [@@unifier_hint_injective] from op_forall_Plus (Pulse.Lib.ForEvery.fst) - Group 18 tests from CoreVsRel (tested the removed API) Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The injective path correctly emits per-arg equality guards: for f a1..an =?= f b1..bn, each ai == bi is checked individually. When concrete args mismatch (e.g., 0 vs 1), the guard normalizes to l_False, which is correct since the terms genuinely don't match. Bug110's 'foo' (an opaque assumed val) is marked with unifier_hint_not_injective since rewrite needs full-app guard (foo i == foo j from context, not i == j which isn't provable). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Replace blanket per-arg injectivity for slprop-returning functions with an
equatable approach:
- Split is_marked_injective into two predicates:
* is_marked_injective: only explicit [@@unifier_hint_injective] attribute
* returns_equatable_type: checks if return type has [@@unifier_hint_injective_type]
- New dispatch for matching heads:
1. no_guard(structural) always tried first
2. Explicitly injective: per-arg comparison (unchanged)
3. Equatable/returns_equatable_type: try unfold, then per-arg with
full-application-guard fallback. For each arg: if no_guard(check_relation)
succeeds, done; if both are lambdas, compare extensionally; otherwise
bail to emit_guard on the full application.
4. Otherwise: unfold_both_and_retry
- Remove [@@unifier_hint_not_injective] from (**) and on in Pulse.Lib.Core
- Remove [@@unifier_hint_not_injective] from foo in Bug110 test
The equatable approach produces weaker guards (full application equality rather
than per-arg equality), making them always provable by SMT via congruence. This
eliminates the need for opt-out attributes on non-injective slprop combinators.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
When check_relation encounters a Tm_match on one side but not the other (e.g., tkey =?= match (mk_spec r1) with Mkdtuple2 a _ -> a), normalize the match with [Weak; HNF; Beta; Iota; Primops; UnfoldUntil delta_constant]. This allows delta-unfolding inside the scrutinee (e.g., mk_spec → constructor) followed by iota reduction, eliminating the match entirely. This fixes Bug4239Variant where Core previously got stuck: after unfolding dfst, the result was a Tm_match whose scrutinee needed further reduction that only delta + iota could provide. Rel handles this via maybe_inline which normalizes with full delta; Core now does the same but only for stuck Tm_match terms. Also adds a general fallback: try maybe_unfold_and_retry for other stuck term pairs before giving up entirely. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Core type checker: blanket slprop injectivity and refactored check_relation (fixes #4239)
Summary
This PR brings FStarC.TypeChecker.Core's logic for deciding relations between applied terms closer to FStarC.TypeChecker.Rel, addressing issue
#4239 where Core would force argument-level equality (a == b) when comparing f a =?= f b, even when f is a type abbreviation that should be
unfolded.
The main change in Core:
Refactored check_relation when heads match — the logic is now:
Now, it turns out the Pulse slprop comparisons were relying on the implicit injective behavior of the Core checker. So, this PR adds a mechanism to treat, by default, all slprop predicates as injective. This is done by:
(**),exists*, andonthat are match-based or where per-arg equality is too strong.Additionally, adds a unit test suite (src/tests/FStarC.Tests.CoreVsRel.fst):
injective heads, and the examples from Pulse expects type constructors to be injective #4239
And some expected output updates: ~30 Pulse error message .expected files updated (VC form changes from full comparison to l_False when per-arg guards
normalize trivially).