From 372034ea01b42ee495bdfcc84c828b99fba7a570 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Wed, 13 May 2026 21:13:03 -0700 Subject: [PATCH 01/24] Add Core vs Rel comparison test suite (issue #4239) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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> --- src/tests/FStarC.Tests.CoreVsRel.fst | 724 +++++++++++++++++++++++++++ src/tests/FStarC.Tests.Test.fst | 1 + 2 files changed, 725 insertions(+) create mode 100644 src/tests/FStarC.Tests.CoreVsRel.fst diff --git a/src/tests/FStarC.Tests.CoreVsRel.fst b/src/tests/FStarC.Tests.CoreVsRel.fst new file mode 100644 index 00000000000..28cdb92ad4e --- /dev/null +++ b/src/tests/FStarC.Tests.CoreVsRel.fst @@ -0,0 +1,724 @@ +(* + Copyright 2025 Microsoft Research + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +*) +module FStarC.Tests.CoreVsRel +(* Tests comparing FStarC.TypeChecker.Core and FStarC.TypeChecker.Rel + on subtyping and equality of types without uvars. + Related to GitHub issue #4239: Core produces incorrect guards for + type abbreviation applications by treating them as injective. *) + +open FStarC +open FStarC.Effect +open FStarC.Errors +open FStarC.Syntax.Syntax +open FStarC.Tests.Pars +module S = FStarC.Syntax.Syntax +module U = FStarC.Syntax.Util +module N = FStarC.TypeChecker.Normalize +module Rel = FStarC.TypeChecker.Rel +module Core = FStarC.TypeChecker.Core +module Env = FStarC.TypeChecker.Env +open FStarC.TypeChecker.Common +open FStarC.TypeChecker.Env +open FStarC.Tests.Util + +open FStarC.Class.Show + +let tcenv () : ML _ = Pars.init() + +let success = mk_ref true + +let fail msg : ML unit = + Format.print_string msg; + success := false + +let guard_to_string env g : ML _ = match g with + | Trivial -> "trivial" + | NonTrivial f -> + N.term_to_string env f + +(* Run Core's check_term_subtyping, return guard or error *) +let run_core_subtyping (env:Env.env) (t0 t1:typ) + : ML (either (option typ) string) + = match Core.check_term_subtyping true true env t0 t1 with + | Inl None -> Inl None + | Inl (Some (g, _cb)) -> Inl (Some g) + | Inr err -> Inr (Core.print_error err) + +(* Run Core's check_term_equality, return guard or error *) +let run_core_equality (env:Env.env) (t0 t1:typ) + : ML (either (option typ) string) + = match Core.check_term_equality true true env t0 t1 with + | Inl None -> Inl None + | Inl (Some (g, _cb)) -> Inl (Some g) + | Inr err -> Inr (Core.print_error err) + +(* Run Rel's get_subtyping_prop, return guard_formula *) +let run_rel_subtyping (env:Env.env) (t0 t1:typ) + : ML (option guard_formula) + = match Rel.get_subtyping_prop env t0 t1 with + | None -> None + | Some g -> + let g = Rel.simplify_guard env g in + Some g.guard_f + +(* Run Rel's try_teq (no SMT), return guard_formula *) +let run_rel_equality (env:Env.env) (t0 t1:typ) + : ML (option guard_formula) + = match Rel.try_teq false env t0 t1 with + | None -> None + | Some g -> + let g = Rel.simplify_guard env g in + Some g.guard_f + +type outcome = + | BothTrivial (* both succeed with no guard *) + | BothGuarded (* both succeed with a guard *) + | CoreTrivialRelGuarded (* Core trivial, Rel has guard *) + | CoreGuardedRelTrivial (* Core has guard, Rel trivial *) + | CoreFailRelSucceed (* Core fails, Rel succeeds *) + | RelFailCoreSucceed (* Rel fails, Core succeeds *) + | BothFail (* both fail *) + +let show_outcome o = match o with + | BothTrivial -> "BothTrivial" + | BothGuarded -> "BothGuarded" + | CoreTrivialRelGuarded -> "CoreTrivialRelGuarded" + | CoreGuardedRelTrivial -> "CoreGuardedRelTrivial" + | CoreFailRelSucceed -> "CoreFailRelSucceed" + | RelFailCoreSucceed -> "RelFailCoreSucceed" + | BothFail -> "BothFail" + +(* Compare subtyping of t0 <: t1 in Core vs Rel. + Can optionally take a custom env (for tests with binders). *) +let compare_subtyping_env (i:int) (env:Env.env) (t0 t1:typ) (expected:outcome) + : ML unit + = Options.parse_cmd_line () |> ignore; + Format.print1 "CoreVsRel subtyping test %s ... " (show i); + let core_res = run_core_subtyping env t0 t1 in + let rel_res = run_rel_subtyping env t0 t1 in + let actual = + match core_res, rel_res with + | Inl None, Some Trivial -> BothTrivial + | Inl None, Some (NonTrivial _) -> CoreTrivialRelGuarded + | Inl None, None -> RelFailCoreSucceed + | Inl (Some _), Some Trivial -> CoreGuardedRelTrivial + | Inl (Some _), Some (NonTrivial _) -> BothGuarded + | Inl (Some _), None -> RelFailCoreSucceed + | Inr _, Some _ -> CoreFailRelSucceed + | Inr _, None -> BothFail + in + if actual = expected then ( + Format.print1 "ok [%s]\n" (show_outcome actual); + (match actual with + | BothGuarded -> + (match core_res with + | Inl (Some g) -> Format.print1 " Core guard: %s\n" (show g) + | _ -> ()); + (match rel_res with + | Some (NonTrivial f) -> Format.print1 " Rel guard: %s\n" (N.term_to_string env f) + | _ -> ()) + | _ -> ()) + ) else ( + fail (Format.fmt3 "FAILED: expected %s, got %s (test %s)\n" + (show_outcome expected) (show_outcome actual) (show i)); + (match core_res with + | Inl None -> Format.print_string " Core: trivial\n" + | Inl (Some g) -> Format.print1 " Core guard: %s\n" (show g) + | Inr err -> Format.print1 " Core error: %s\n" err); + (match rel_res with + | None -> Format.print_string " Rel: failed\n" + | Some Trivial -> Format.print_string " Rel: trivial\n" + | Some (NonTrivial f) -> Format.print1 " Rel guard: %s\n" (N.term_to_string env f)) + ); + Options.init () + +let compare_subtyping (i:int) (t0 t1:typ) (expected:outcome) : ML unit = + compare_subtyping_env i (tcenv ()) t0 t1 expected + +(* Compare equality of t0 and t1 in Core vs Rel. + Can optionally take a custom env (for tests with binders). *) +let compare_equality_env (i:int) (env:Env.env) (t0 t1:typ) (expected:outcome) + : ML unit + = Options.parse_cmd_line () |> ignore; + Format.print1 "CoreVsRel equality test %s ... " (show i); + let core_res = run_core_equality env t0 t1 in + let rel_res = run_rel_equality env t0 t1 in + let actual = + match core_res, rel_res with + | Inl None, Some Trivial -> BothTrivial + | Inl None, Some (NonTrivial _) -> CoreTrivialRelGuarded + | Inl None, None -> RelFailCoreSucceed + | Inl (Some _), Some Trivial -> CoreGuardedRelTrivial + | Inl (Some _), Some (NonTrivial _) -> BothGuarded + | Inl (Some _), None -> RelFailCoreSucceed + | Inr _, Some _ -> CoreFailRelSucceed + | Inr _, None -> BothFail + in + if actual = expected then ( + Format.print1 "ok [%s]\n" (show_outcome actual); + (match actual with + | BothGuarded -> + (match core_res with + | Inl (Some g) -> Format.print1 " Core guard: %s\n" (show g) + | _ -> ()); + (match rel_res with + | Some (NonTrivial f) -> Format.print1 " Rel guard: %s\n" (N.term_to_string env f) + | _ -> ()) + | _ -> ()) + ) else ( + fail (Format.fmt3 "FAILED: expected %s, got %s (test %s)\n" + (show_outcome expected) (show_outcome actual) (show i)); + (match core_res with + | Inl None -> Format.print_string " Core: trivial\n" + | Inl (Some g) -> Format.print1 " Core guard: %s\n" (show g) + | Inr err -> Format.print1 " Core error: %s\n" err); + (match rel_res with + | None -> Format.print_string " Rel: failed\n" + | Some Trivial -> Format.print_string " Rel: trivial\n" + | Some (NonTrivial f) -> Format.print1 " Rel guard: %s\n" (N.term_to_string env f)) + ); + Options.init () + +let compare_equality (i:int) (t0 t1:typ) (expected:outcome) : ML unit = + compare_equality_env i (tcenv ()) t0 t1 expected + +(* Test that a fragment typechecks (uses Rel, not Core). + Useful to verify that the full typechecker handles these cases. *) +let tc_fragment_ok (i:int) (frag:string) : ML unit = + Format.print1 "CoreVsRel tc_fragment test %s ... " (show i); + (try + Pars.pars_and_tc_fragment frag; + Format.print_string "ok\n" + with + | Error (_, msg, r, _) -> + fail (Format.fmt2 "FAILED: %s: %s\n" (FStarC.Range.string_of_range r) (Errors.rendermsg msg)) + | e -> + fail (Format.fmt1 "FAILED: unexpected exception: %s\n" (FStarC.Util.message_of_exn e))) + +(* Test that a fragment fails to typecheck (expects a Core error) *) +let tc_fragment_fail (i:int) (frag:string) : ML unit = + Format.print1 "CoreVsRel tc_fragment_fail test %s ... " (show i); + (try + Pars.pars_and_tc_fragment frag; + fail "FAILED: expected error but succeeded\n" + with + | Error _ -> + FStarC.Errors.report_all () |> ignore; + Format.print_string "ok (failed as expected)\n" + | _ -> + FStarC.Errors.report_all () |> ignore; + Format.print_string "ok (failed as expected)\n") + +(* ============================================================ *) +(* Test suite *) +(* ============================================================ *) + +let run_all () : ML bool = + Format.print_string "\n=== Testing Core vs Rel agreement ===\n"; + + (* ---- Setup type abbreviations used by multiple tests ---- *) + let _ = Pars.pars_and_tc_fragment + "let cvr_natlt (n: nat) = i:nat { i < n }\n\ + let cvr_ty0 n = x:int { x >= n }\n\ + let cvr_ty1 n = x:cvr_ty0 n { x > n }" + in + + (* ---------------------------------------------------------- + Group 1: Syntactically identical types (control cases) + Core and Rel should both return trivial. + ---------------------------------------------------------- *) + + (* Test 100: natlt n =?= natlt n — identical type abbrev applications *) + let _ = + let t0 = tc "cvr_natlt 42" in + let t1 = tc "cvr_natlt 42" in + compare_equality 100 t0 t1 BothTrivial + in + + (* Test 101: int =?= int — base type equality *) + let _ = + compare_equality 101 (tc "int") (tc "int") BothTrivial + in + + (* Test 102: natlt 42 <: natlt 42 — identical abbrev subtyping *) + let _ = + let t0 = tc "cvr_natlt 42" in + let t1 = tc "cvr_natlt 42" in + compare_subtyping 102 t0 t1 BothTrivial + in + + (* ---------------------------------------------------------- + Group 2: Simple refinement subtyping (no abbreviations) + These should work the same in Core and Rel. + ---------------------------------------------------------- *) + + (* Test 200: x:int{x > 0} <: int — refinement subtype of base *) + let _ = + compare_subtyping 200 (tc "x:int{ x > 0 }") (tc "int") BothTrivial + in + + (* Test 201: int <: x:int{x > 0} — base to refinement, needs guard *) + let _ = + compare_subtyping 201 (tc "int") (tc "x:int{ x > 0 }") BothGuarded + in + + (* Test 202: x:int{x > 0} <: x:int{x >= 0} — refinement to weaker refinement *) + let _ = + compare_subtyping 202 (tc "x:int{ x > 0 }") (tc "x:int{ x >= 0 }") BothGuarded + in + + (* Test 203: nat <: int — nat is a refinement of int *) + let _ = + compare_subtyping 203 (tc "nat") (tc "int") BothTrivial + in + + (* ---------------------------------------------------------- + Group 3: Type abbreviation subtyping with concrete args + ---------------------------------------------------------- *) + + (* Test 300: cvr_natlt 5 <: cvr_natlt 10 + After unfolding: i:nat{i < 5} <: i:nat{i < 10} *) + let _ = + compare_subtyping 300 (tc "cvr_natlt 5") (tc "cvr_natlt 10") BothGuarded + in + + (* Test 301: cvr_natlt 10 <: cvr_natlt 5 *) + let _ = + compare_subtyping 301 (tc "cvr_natlt 10") (tc "cvr_natlt 5") BothGuarded + in + + (* Test 302: cvr_ty0 5 <: cvr_ty0 10 *) + let _ = + compare_subtyping 302 (tc "cvr_ty0 5") (tc "cvr_ty0 10") BothGuarded + in + + (* Test 303: cvr_ty1 17 =?= x:cvr_ty0 17 { x > 17 } *) + let _ = + compare_equality 303 (tc "cvr_ty1 17") (tc "x:cvr_ty0 17 { x > 17 }") BothTrivial + in + + (* Test 304: cvr_ty0 17 =?= x:int { x >= 17 } *) + let _ = + compare_equality 304 (tc "cvr_ty0 17") (tc "x:int { x >= 17 }") BothTrivial + in + + (* ---------------------------------------------------------- + Group 4: Arrow types with type abbreviation domains + ---------------------------------------------------------- *) + + (* Test 400: (cvr_natlt 10 -> bool) <: (cvr_natlt 5 -> bool) + Contravariant domain: need cvr_natlt 5 <: cvr_natlt 10 *) + let _ = + compare_subtyping 400 (tc "cvr_natlt 10 -> bool") (tc "cvr_natlt 5 -> bool") BothGuarded + in + + (* Test 401: (cvr_natlt 5 -> bool) <: (cvr_natlt 10 -> bool) *) + let _ = + compare_subtyping 401 (tc "cvr_natlt 5 -> bool") (tc "cvr_natlt 10 -> bool") BothGuarded + in + + (* Test 402: (int -> cvr_natlt 10) <: (int -> cvr_natlt 5) + Covariant in codomain *) + let _ = + compare_subtyping 402 (tc "int -> Tot (cvr_natlt 10)") (tc "int -> Tot (cvr_natlt 5)") BothGuarded + in + + (* Test 403: (nat -> bool) <: (int -> bool) — contravariant domain needs guard *) + let _ = + compare_subtyping 403 (tc "nat -> bool") (tc "int -> bool") BothGuarded + in + + (* Test 404: (int -> bool) <: (nat -> bool) — trivial *) + let _ = + compare_subtyping 404 (tc "int -> bool") (tc "nat -> bool") BothTrivial + in + + (* ---------------------------------------------------------- + Group 5: Nested type abbreviation subtyping + ---------------------------------------------------------- *) + + (* Test 500: cvr_ty1 17 <: cvr_ty0 17 — dropping outer refinement *) + let _ = + compare_subtyping 500 (tc "cvr_ty1 17") (tc "cvr_ty0 17") BothTrivial + in + + (* Test 501: cvr_ty0 17 <: cvr_ty1 17 — needs refinement guard *) + let _ = + compare_subtyping 501 (tc "cvr_ty0 17") (tc "cvr_ty1 17") BothGuarded + in + + (* Test 502: cvr_ty1 5 <: cvr_ty0 10 *) + let _ = + compare_subtyping 502 (tc "cvr_ty1 5") (tc "cvr_ty0 10") BothGuarded + in + + (* ---------------------------------------------------------- + Group 6: Type abbreviation equality + ---------------------------------------------------------- *) + + (* Test 600: cvr_natlt 5 =?= cvr_natlt 10 + Core can produce a guard (forall i. i < 5 == i < 10); + Rel's try_teq with smt_ok=false can't solve this, so it fails. + This is an expected divergence: equality of distinct type + abbreviation applications is harder for Rel without SMT. *) + let _ = + compare_equality 600 (tc "cvr_natlt 5") (tc "cvr_natlt 10") RelFailCoreSucceed + in + + (* Test 601: cvr_natlt 5 =?= i:nat{ i < 5 } — unfolding should yield equality *) + let _ = + compare_equality 601 (tc "cvr_natlt 5") (tc "i:nat{ i < 5 }") BothTrivial + in + + (* ---------------------------------------------------------- + Group 7: Type abbreviation with binder variables (issue #4239) + This is where the Core bug manifests. + We push binder variables into the environment and then + call Core/Rel directly with type applications using those vars. + ---------------------------------------------------------- *) + + (* Helper: create an environment with binders n:nat, i:nat *) + let env_with_n_i () : ML (Env.env & bv & bv) = + let env = tcenv () in + let nat_t = tc "nat" in + let n_bv = S.gen_bv "n" None nat_t in + let env = Env.push_bv env n_bv in + let i_bv = S.gen_bv "i" None nat_t in + let env = Env.push_bv env i_bv in + (env, n_bv, i_bv) + in + + let cvr_natlt_head = tc "cvr_natlt" in + let cvr_ty0_head = tc "cvr_ty0" in + + (* Test 700: with n:nat, i:nat in env: + cvr_natlt n <: cvr_natlt n — trivially equal *) + let _ = + let env, n_bv, _i_bv = env_with_n_i () in + let n_name = S.bv_to_name n_bv in + let t0 = S.mk_Tm_app cvr_natlt_head [(n_name, None)] FStarC.Range.dummyRange in + compare_subtyping_env 700 env t0 t0 BothTrivial + in + + (* Test 701: with n:nat, i:nat in env: + cvr_natlt i <: cvr_natlt n + Core should unfold to (x:nat{x < i}) <: (x:nat{x < n}) + and produce guard: forall x:nat. x < i ==> x < n + BUG: Core may produce guard: i == n (injectivity) *) + let _ = + let env, n_bv, i_bv = env_with_n_i () in + let n_name = S.bv_to_name n_bv in + let i_name = S.bv_to_name i_bv in + let t0 = S.mk_Tm_app cvr_natlt_head [(i_name, None)] FStarC.Range.dummyRange in + let t1 = S.mk_Tm_app cvr_natlt_head [(n_name, None)] FStarC.Range.dummyRange in + compare_subtyping_env 701 env t0 t1 BothGuarded + in + + (* Test 702: with n:nat, i:nat in env: + cvr_natlt n <: cvr_natlt i (reverse direction) *) + let _ = + let env, n_bv, i_bv = env_with_n_i () in + let n_name = S.bv_to_name n_bv in + let i_name = S.bv_to_name i_bv in + let t0 = S.mk_Tm_app cvr_natlt_head [(n_name, None)] FStarC.Range.dummyRange in + let t1 = S.mk_Tm_app cvr_natlt_head [(i_name, None)] FStarC.Range.dummyRange in + compare_subtyping_env 702 env t0 t1 BothGuarded + in + + (* Test 703: with n:nat, i:nat in env: + cvr_ty0 i <: cvr_ty0 n *) + let _ = + let env, n_bv, i_bv = env_with_n_i () in + let n_name = S.bv_to_name n_bv in + let i_name = S.bv_to_name i_bv in + let t0 = S.mk_Tm_app cvr_ty0_head [(i_name, None)] FStarC.Range.dummyRange in + let t1 = S.mk_Tm_app cvr_ty0_head [(n_name, None)] FStarC.Range.dummyRange in + compare_subtyping_env 703 env t0 t1 BothGuarded + in + + (* Test 704: with n:nat, i:nat in env: + cvr_natlt i =?= cvr_natlt n (equality with variables) *) + let _ = + let env, n_bv, i_bv = env_with_n_i () in + let n_name = S.bv_to_name n_bv in + let i_name = S.bv_to_name i_bv in + let t0 = S.mk_Tm_app cvr_natlt_head [(i_name, None)] FStarC.Range.dummyRange in + let t1 = S.mk_Tm_app cvr_natlt_head [(n_name, None)] FStarC.Range.dummyRange in + (* Core produces guard i == n; Rel fails without SMT *) + compare_equality_env 704 env t0 t1 RelFailCoreSucceed + in + + (* Test 705: with n:nat, i:nat in env: + cvr_ty0 n <: cvr_ty0 n — reflexive subtyping with variables *) + let _ = + let env, n_bv, _i_bv = env_with_n_i () in + let n_name = S.bv_to_name n_bv in + let t0 = S.mk_Tm_app cvr_ty0_head [(n_name, None)] FStarC.Range.dummyRange in + compare_subtyping_env 705 env t0 t0 BothTrivial + in + + (* Test 706: with n:nat, i:nat in env: + cvr_ty0 i =?= cvr_ty0 n (equality with variables) + Same bug pattern as 704 but with different abbreviation. *) + let _ = + let env, n_bv, i_bv = env_with_n_i () in + let n_name = S.bv_to_name n_bv in + let i_name = S.bv_to_name i_bv in + let t0 = S.mk_Tm_app cvr_ty0_head [(i_name, None)] FStarC.Range.dummyRange in + let t1 = S.mk_Tm_app cvr_ty0_head [(n_name, None)] FStarC.Range.dummyRange in + compare_equality_env 706 env t0 t1 RelFailCoreSucceed + in + + (* ---------------------------------------------------------- + Group 8: Arrow types with variable type abbrev args (issue #4239) + ---------------------------------------------------------- *) + + (* Test 800: with n:nat, i:nat in env: + (cvr_natlt n -> bool) <: (cvr_natlt i -> bool) + Contravariant: need cvr_natlt i <: cvr_natlt n + This is the EXACT scenario from issue #4239. *) + let _ = + let env, n_bv, i_bv = env_with_n_i () in + let n_name = S.bv_to_name n_bv in + let i_name = S.bv_to_name i_bv in + let dom0 = S.mk_Tm_app cvr_natlt_head [(n_name, None)] FStarC.Range.dummyRange in + let dom1 = S.mk_Tm_app cvr_natlt_head [(i_name, None)] FStarC.Range.dummyRange in + let bool_t = tc "bool" in + let b0 = S.mk_binder (S.gen_bv "_" None dom0) in + let c0 = S.mk_Total bool_t in + let t0 = U.arrow [b0] c0 in + let b1 = S.mk_binder (S.gen_bv "_" None dom1) in + let c1 = S.mk_Total bool_t in + let t1 = U.arrow [b1] c1 in + compare_subtyping_env 800 env t0 t1 BothGuarded + in + + (* Test 801: with n:nat, i:nat in env: + (cvr_natlt i -> bool) <: (cvr_natlt n -> bool) + Contravariant: need cvr_natlt n <: cvr_natlt i *) + let _ = + let env, n_bv, i_bv = env_with_n_i () in + let n_name = S.bv_to_name n_bv in + let i_name = S.bv_to_name i_bv in + let dom0 = S.mk_Tm_app cvr_natlt_head [(i_name, None)] FStarC.Range.dummyRange in + let dom1 = S.mk_Tm_app cvr_natlt_head [(n_name, None)] FStarC.Range.dummyRange in + let bool_t = tc "bool" in + let b0 = S.mk_binder (S.gen_bv "_" None dom0) in + let c0 = S.mk_Total bool_t in + let t0 = U.arrow [b0] c0 in + let b1 = S.mk_binder (S.gen_bv "_" None dom1) in + let c1 = S.mk_Total bool_t in + let t1 = U.arrow [b1] c1 in + compare_subtyping_env 801 env t0 t1 BothGuarded + in + + (* Test 802: with n:nat, i:nat in env: + (cvr_ty0 n -> bool) <: (cvr_ty0 i -> bool) + Contravariant: need cvr_ty0 i <: cvr_ty0 n + Same bug pattern as 800 but with cvr_ty0 *) + let _ = + let env, n_bv, i_bv = env_with_n_i () in + let n_name = S.bv_to_name n_bv in + let i_name = S.bv_to_name i_bv in + let dom0 = S.mk_Tm_app cvr_ty0_head [(n_name, None)] FStarC.Range.dummyRange in + let dom1 = S.mk_Tm_app cvr_ty0_head [(i_name, None)] FStarC.Range.dummyRange in + let bool_t = tc "bool" in + let b0 = S.mk_binder (S.gen_bv "_" None dom0) in + let c0 = S.mk_Total bool_t in + let t0 = U.arrow [b0] c0 in + let b1 = S.mk_binder (S.gen_bv "_" None dom1) in + let c1 = S.mk_Total bool_t in + let t1 = U.arrow [b1] c1 in + compare_subtyping_env 802 env t0 t1 BothGuarded + in + + (* Test 803: with n:nat, i:nat in env: + (int -> cvr_natlt n) <: (int -> cvr_natlt i) + Covariant codomain with variable args *) + let _ = + let env, n_bv, i_bv = env_with_n_i () in + let n_name = S.bv_to_name n_bv in + let i_name = S.bv_to_name i_bv in + let int_t = tc "int" in + let cod0 = S.mk_Tm_app cvr_natlt_head [(n_name, None)] FStarC.Range.dummyRange in + let cod1 = S.mk_Tm_app cvr_natlt_head [(i_name, None)] FStarC.Range.dummyRange in + let b = S.mk_binder (S.gen_bv "_" None int_t) in + let t0 = U.arrow [b] (S.mk_Total cod0) in + let t1 = U.arrow [b] (S.mk_Total cod1) in + compare_subtyping_env 803 env t0 t1 BothGuarded + in + + (* ---------------------------------------------------------- + Group 9: Multi-argument type abbreviation applications + ---------------------------------------------------------- *) + + let _ = Pars.pars_and_tc_fragment + "let cvr_defn (x:nat) : nat -> nat -> Type0 = fun y z -> a:int { a + x == y + z }" + in + + (* Test 900: cvr_defn 0 1 2 =?= cvr_defn 0 1 2 — identical *) + let _ = + compare_equality 900 (tc "cvr_defn 0 1 2") (tc "cvr_defn 0 1 2") BothTrivial + in + + (* Test 901: cvr_defn 0 1 2 =?= a:int { a + 0 == 1 + 2 } — unfolded form *) + let _ = + compare_equality 901 (tc "cvr_defn 0 1 2") (tc "a:int { a + 0 == 1 + 2 }") BothTrivial + in + + (* Helper: create env with a:nat, b:nat, c:nat for multi-arg tests *) + let env_with_abc () : ML (Env.env & bv & bv & bv) = + let env = tcenv () in + let nat_t = tc "nat" in + let a_bv = S.gen_bv "a" None nat_t in + let env = Env.push_bv env a_bv in + let b_bv = S.gen_bv "b" None nat_t in + let env = Env.push_bv env b_bv in + let c_bv = S.gen_bv "c" None nat_t in + let env = Env.push_bv env c_bv in + (env, a_bv, b_bv, c_bv) + in + let cvr_defn_head = tc "cvr_defn" in + + (* Test 902: with a:nat, b:nat, c:nat in env: + cvr_defn a b c =?= cvr_defn a b c — reflexive *) + let _ = + let env, a_bv, b_bv, c_bv = env_with_abc () in + let args = [(S.bv_to_name a_bv, None); (S.bv_to_name b_bv, None); (S.bv_to_name c_bv, None)] in + let t0 = S.mk_Tm_app cvr_defn_head args FStarC.Range.dummyRange in + compare_equality_env 902 env t0 t0 BothTrivial + in + + (* Test 903: with a:nat, b:nat, c:nat in env: + cvr_defn a b c <: cvr_defn a c b — swapped args + Core will produce equational guard b == c && c == b; + Rel should unfold and compare refinement formulas. *) + let _ = + let env, a_bv, b_bv, c_bv = env_with_abc () in + let t0 = S.mk_Tm_app cvr_defn_head + [(S.bv_to_name a_bv, None); (S.bv_to_name b_bv, None); (S.bv_to_name c_bv, None)] + FStarC.Range.dummyRange in + let t1 = S.mk_Tm_app cvr_defn_head + [(S.bv_to_name a_bv, None); (S.bv_to_name c_bv, None); (S.bv_to_name b_bv, None)] + FStarC.Range.dummyRange in + compare_subtyping_env 903 env t0 t1 BothGuarded + in + + (* ---------------------------------------------------------- + Group 10: Dependent tuple / dtuple2 types + ---------------------------------------------------------- *) + + (* Test 1000: dtuple2 refinement subtyping *) + let _ = + let t0 = tc "dp:((dtuple2 int (fun (y:int) -> z:int{ z > y })) <: Type0) { let (| x, _ |) = dp in x > 17 }" in + let t1 = tc "(dtuple2 int (fun (y:int) -> z:int{ z > y }))" in + compare_subtyping 1000 t0 t1 BothTrivial + in + + (* ---------------------------------------------------------- + Group 11: Ascription / type cast subtyping + ---------------------------------------------------------- *) + + (* Test 1100: int <: refined nat with ascription *) + let _ = + let t0 = tc "int" in + let t1 = tc "j:(i:nat{ i > 17 } <: Type0){j > 42}" in + compare_subtyping 1100 t0 t1 BothGuarded + in + + (* ---------------------------------------------------------- + Group 12: Record field projection types + ---------------------------------------------------------- *) + + let _ = Pars.pars_and_tc_fragment + "type cvr_vprop' = { cvr_t:Type0 ; cvr_n:nat }" + in + + (* Test 1200: record field proj equality *) + let _ = + let t0 = tc "x:(({ cvr_t=bool; cvr_n=0 }).cvr_t <: Type0) { x == false }" in + let t1 = tc "x:bool{ x == false }" in + compare_equality 1200 t0 t1 BothTrivial + in + + (* ---------------------------------------------------------- + Group 13: Arrow type equality + ---------------------------------------------------------- *) + + (* Test 1300: (int -> bool) =?= (int -> bool) — trivial *) + let _ = + compare_equality 1300 (tc "int -> bool") (tc "int -> bool") BothTrivial + in + + (* Test 1301: (nat -> bool) =?= (int -> bool) — different domains + Rel can't prove arrow equality without SMT. + Core produces a guard (which is also buggy — equates refinement + formulas via injectivity: l_True == (i >= 0 == true)). *) + let _ = + compare_equality 1301 (tc "nat -> bool") (tc "int -> bool") RelFailCoreSucceed + in + + (* Test 1302: with n:nat, i:nat in env: + (cvr_natlt n -> bool) =?= (cvr_natlt i -> bool) (arrow equality with var args) + Core will produce equational guard; Rel fails without SMT. *) + let _ = + let env, n_bv, i_bv = env_with_n_i () in + let n_name = S.bv_to_name n_bv in + let i_name = S.bv_to_name i_bv in + let dom0 = S.mk_Tm_app cvr_natlt_head [(n_name, None)] FStarC.Range.dummyRange in + let dom1 = S.mk_Tm_app cvr_natlt_head [(i_name, None)] FStarC.Range.dummyRange in + let bool_t = tc "bool" in + let b0 = S.mk_binder (S.gen_bv "_" None dom0) in + let b1 = S.mk_binder (S.gen_bv "_" None dom1) in + let t0 = U.arrow [b0] (S.mk_Total bool_t) in + let t1 = U.arrow [b1] (S.mk_Total bool_t) in + compare_equality_env 1302 env t0 t1 RelFailCoreSucceed + in + + (* ---------------------------------------------------------- + Group 14: Full typechecker fragment tests (uses Rel, not Core) + These verify the reported issue #4239 examples work in + the full typechecker (which uses Rel for subtyping). + ---------------------------------------------------------- *) + + (* Test 1400: Nested type abbreviation coercion *) + tc_fragment_ok 1400 + "let cvr_nested_ok (n:nat) (x: cvr_ty0 n) : int = x"; + + (* Test 1401: Arrow subtyping with type abbrev domains *) + tc_fragment_ok 1401 + "let cvr_arrow_ok (n:nat) (x: cvr_natlt n -> bool) (i:nat{ i < n }) : cvr_natlt i -> bool = x"; + + (* Test 1402: Nested type abbreviation with variable args — full checker *) + tc_fragment_ok 1402 + "let cvr_ty1_sub (n:nat) (x: cvr_ty1 n) : cvr_ty0 n = x"; + + (* Test 1403: cvr_natlt subtyping to nat — full checker *) + tc_fragment_ok 1403 + "let cvr_natlt_to_nat (n:nat) (x: cvr_natlt n) : nat = x"; + + (* Test 1404: Concrete arg abbreviation subtyping — full checker *) + tc_fragment_ok 1404 + "let cvr_concrete_ok (x: cvr_natlt 5) : cvr_natlt 10 = x"; + + (* ---------------------------------------------------------- + Summary + ---------------------------------------------------------- *) + + if !success + then Format.print_string "Core vs Rel tests ok\n" + else Format.print_string "Core vs Rel tests FAILED\n"; + !success diff --git a/src/tests/FStarC.Tests.Test.fst b/src/tests/FStarC.Tests.Test.fst index 47692fb75f7..968e05a691e 100644 --- a/src/tests/FStarC.Tests.Test.fst +++ b/src/tests/FStarC.Tests.Test.fst @@ -62,6 +62,7 @@ let main () : ML unit = Pars.parse_incremental_decls_use_lang (); Norm.run_all (); if Unif.run_all () then () else exit 1; + if CoreVsRel.run_all () then () else exit 1; Data.run_all (); FStarC.Errors.report_all () |> ignore; From c969dba76ad14a4b93e5069f8640f84aac97463a Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Wed, 13 May 2026 21:25:23 -0700 Subject: [PATCH 02/24] Address #4239 When comparing `f a == f b`, first compare structurally with no guard to enable fast, guard-free proofs for common cases, e.g. `f a == f a`, unfolding and retrying as a fallback. --- pulse/test/Bug4239.fst | 28 +++++++++++++++++++++ src/typechecker/FStarC.TypeChecker.Core.fst | 13 +++++++--- 2 files changed, 37 insertions(+), 4 deletions(-) create mode 100644 pulse/test/Bug4239.fst diff --git a/pulse/test/Bug4239.fst b/pulse/test/Bug4239.fst new file mode 100644 index 00000000000..6fe5d55aa84 --- /dev/null +++ b/pulse/test/Bug4239.fst @@ -0,0 +1,28 @@ +module Bug4239 +open Pulse.Nolib +#lang-pulse + +let natlt (n: nat) = i:nat { i < n } + +let works #n (x: natlt n -> bool) (i: nat { i < n }) = + let a: (natlt i -> bool) = x in + () + +fn doesnt_work #n (x: natlt n -> bool) (i: nat { i < n }) { + let a: (natlt i -> bool) = x; + () +} + +module SZ = FStar.SizeT +type sz = FStar.SizeT.t +type szlt (n:int) = i:sz{SZ.v i < n} +fn bug + (x y : sz {SZ.v y <= SZ.v x}) + (k : szlt (SZ.v y)) +{ + assert pure (SZ.v k < SZ.v y); + assert pure (SZ.v y <= SZ.v x); + assert pure (SZ.v k < SZ.v x); + let k : szlt (SZ.v x) = k; // Fails, but should work + (); +} \ No newline at end of file diff --git a/src/typechecker/FStarC.TypeChecker.Core.fst b/src/typechecker/FStarC.TypeChecker.Core.fst index 8549588011b..1bf7eeb5a04 100644 --- a/src/typechecker/FStarC.TypeChecker.Core.fst +++ b/src/typechecker/FStarC.TypeChecker.Core.fst @@ -1316,15 +1316,20 @@ let rec check_relation' (g:env) (rel:relation) (t0 t1:typ) then prove `v.v1 == u.v1` *) let compare_head_and_args () = handle_with - (check_relation g EQUALITY head0 head1 ;! - check_relation_args g EQUALITY args0 args1) + //cf. Issue 4239 + //We first try to prove `f a == f b` structurally with no SMT guard + //this handles cases where `a == b` + //If that fails, then we unfold and try again + (no_guard + (check_relation g EQUALITY head0 head1 ;! + check_relation_args g EQUALITY args0 args1)) (fun _ -> maybe_unfold_side_and_retry Both t0 t1) in if guard_ok && - (rel=EQUALITY) && + (rel=EQUALITY) && (equatable g t0 || equatable g t1) then ( - handle_with + handle_with (no_guard (compare_head_and_args ())) (fun _ -> emit_guard t0 t1) ) From acd818fee035fa5c7147bd6d1ffb229b508125d3 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Thu, 14 May 2026 21:34:23 -0700 Subject: [PATCH 03/24] Fix CI failures in Core type abbreviation comparison (#4239) 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> --- src/tests/FStarC.Tests.CoreVsRel.fst | 111 ++++++++++++++++++++ src/typechecker/FStarC.TypeChecker.Core.fst | 48 +++++++-- 2 files changed, 152 insertions(+), 7 deletions(-) diff --git a/src/tests/FStarC.Tests.CoreVsRel.fst b/src/tests/FStarC.Tests.CoreVsRel.fst index 28cdb92ad4e..334370f6c63 100644 --- a/src/tests/FStarC.Tests.CoreVsRel.fst +++ b/src/tests/FStarC.Tests.CoreVsRel.fst @@ -714,6 +714,117 @@ let run_all () : ML bool = tc_fragment_ok 1404 "let cvr_concrete_ok (x: cvr_natlt 5) : cvr_natlt 10 = x"; + (* ---------------------------------------------------------- + Group 15: Non-refinement type abbreviation applications + These test the structural fallback (step 3 of compare_head_and_args): + type abbreviations that expand to non-refinement types + (e.g., function types, pairs) should succeed with arg-level + guards when unfolding fails or produces complex terms. + ---------------------------------------------------------- *) + + let _ = Pars.pars_and_tc_fragment + "let cvr_nonref_arr (n:int) (m:int) : Type = (x:int{x > n}) -> (y:int{y > m})\n\ + let cvr_nonref_wrap (n:int) : Type = (x:int{x > n}) -> int" + in + + let cvr_nonref_arr_head = tc "cvr_nonref_arr" in + let cvr_nonref_wrap_head = tc "cvr_nonref_wrap" in + + (* Helper: create environment with a:int, b:int *) + let env_with_ab_ints () : ML (Env.env & bv & bv) = + let env = tcenv () in + let int_t = tc "int" in + let a_bv = S.gen_bv "a" None int_t in + let env = Env.push_bv env a_bv in + let b_bv = S.gen_bv "b" None int_t in + let env = Env.push_bv env b_bv in + (env, a_bv, b_bv) + in + + (* Test 1500: cvr_nonref_arr 1 2 =?= cvr_nonref_arr 1 2 — identical *) + let _ = + compare_equality 1500 (tc "cvr_nonref_arr 1 2") (tc "cvr_nonref_arr 1 2") BothTrivial + in + + (* Test 1501: with a:int, b:int in env: + cvr_nonref_arr a b <: cvr_nonref_arr b a — swapped args. + Not a refinement type (it's an arrow), so structural fallback should + produce arg-level guards rather than failing. *) + let _ = + let env, a_bv, b_bv = env_with_ab_ints () in + let a_name = S.bv_to_name a_bv in + let b_name = S.bv_to_name b_bv in + let t0 = S.mk_Tm_app cvr_nonref_arr_head [(a_name, None); (b_name, None)] FStarC.Range.dummyRange in + let t1 = S.mk_Tm_app cvr_nonref_arr_head [(b_name, None); (a_name, None)] FStarC.Range.dummyRange in + compare_subtyping_env 1501 env t0 t1 BothGuarded + in + + (* Test 1502: with a:int, b:int in env: + cvr_nonref_arr a b <: cvr_nonref_arr a b — reflexive, should be trivial *) + let _ = + let env, a_bv, b_bv = env_with_ab_ints () in + let a_name = S.bv_to_name a_bv in + let b_name = S.bv_to_name b_bv in + let t0 = S.mk_Tm_app cvr_nonref_arr_head [(a_name, None); (b_name, None)] FStarC.Range.dummyRange in + compare_subtyping_env 1502 env t0 t0 BothTrivial + in + + (* Test 1503: with a:int in env: + cvr_nonref_wrap a =?= cvr_nonref_wrap a — reflexive *) + let _ = + let env, a_bv, _b_bv = env_with_ab_ints () in + let a_name = S.bv_to_name a_bv in + let t0 = S.mk_Tm_app cvr_nonref_wrap_head [(a_name, None)] FStarC.Range.dummyRange in + compare_equality_env 1503 env t0 t0 BothTrivial + in + + (* Test 1504: with a:int, b:int in env: + cvr_nonref_wrap a =?= cvr_nonref_wrap b — different args + Should produce arg-level guard a == b via structural fallback. *) + let _ = + let env, a_bv, b_bv = env_with_ab_ints () in + let a_name = S.bv_to_name a_bv in + let b_name = S.bv_to_name b_bv in + let t0 = S.mk_Tm_app cvr_nonref_wrap_head [(a_name, None)] FStarC.Range.dummyRange in + let t1 = S.mk_Tm_app cvr_nonref_wrap_head [(b_name, None)] FStarC.Range.dummyRange in + compare_equality_env 1504 env t0 t1 RelFailCoreSucceed + in + + (* ---------------------------------------------------------- + Group 16: Non-refinement type abbreviation with constant args + These test the third fallback in compare_head_and_args: + when args are non-equatable constants (like 2, 3), structural + comparison can't produce guards. The unfolded comparison with + guards handles this by exposing equatable functions (like + op_Equality) in the unfolded form. + ---------------------------------------------------------- *) + + let _ = Pars.pars_and_tc_fragment + "let cvr_const_app (m:nat) (n:nat) : Type = b:bool{ b == (m = n) }" + in + + (* Test 1600: cvr_const_app 2 2 =?= cvr_const_app 2 2 — identical *) + let _ = + compare_equality 1600 (tc "cvr_const_app 2 2") (tc "cvr_const_app 2 2") BothTrivial + in + + (* Test 1601: cvr_const_app 2 2 <: cvr_const_app 2 3 — different constant args. + This is the Bug4256 pattern: args are constants (non-equatable), + so the unfolded-with-guards fallback is needed. *) + let _ = + compare_subtyping 1601 (tc "cvr_const_app 2 2") (tc "cvr_const_app 2 3") BothGuarded + in + + (* Test 1602: cvr_const_app 2 3 =?= cvr_const_app 2 3 — identical *) + let _ = + compare_equality 1602 (tc "cvr_const_app 2 3") (tc "cvr_const_app 2 3") BothTrivial + in + + (* Test 1603: full checker integration — coercion between + non-refinement type abbrevs with constant args should work *) + tc_fragment_ok 1603 + "let cvr_const_ok (x: cvr_const_app 2 2) : cvr_const_app 2 2 = x"; + (* ---------------------------------------------------------- Summary ---------------------------------------------------------- *) diff --git a/src/typechecker/FStarC.TypeChecker.Core.fst b/src/typechecker/FStarC.TypeChecker.Core.fst index 1bf7eeb5a04..d831ec1bb72 100644 --- a/src/typechecker/FStarC.TypeChecker.Core.fst +++ b/src/typechecker/FStarC.TypeChecker.Core.fst @@ -1315,15 +1315,49 @@ let rec check_relation' (g:env) (rel:relation) (t0 t1:typ) first by trying to unify `v` and `u` and if it fails then prove `v.v1 == u.v1` *) let compare_head_and_args () = + let structural () = + check_relation g EQUALITY head0 head1 ;! + check_relation_args g EQUALITY args0 args1 + in handle_with //cf. Issue 4239 - //We first try to prove `f a == f b` structurally with no SMT guard - //this handles cases where `a == b` - //If that fails, then we unfold and try again - (no_guard - (check_relation g EQUALITY head0 head1 ;! - check_relation_args g EQUALITY args0 args1)) - (fun _ -> maybe_unfold_side_and_retry Both t0 t1) + //First try structural comparison without SMT guards. + //This handles cases where args are definitionally equal. + (no_guard (structural ())) + (fun _ -> + //If structural fails, try unfolding the type abbreviation. + if! unfolding_ok then ( + match maybe_unfold_side Both t0 t1 with + | None -> + //Can't unfold: fall back to structural with guards + structural () + | Some (t0', t1') -> + //Check if unfolding exposes a refinement type. + //If so, the refinement comparison produces properly + //weakened guards (e.g., natlt i <: natlt n gives + //forall x. x < i ==> x < n, not i == n). + let t0' = beta_iota_reduce t0' in + let t1' = beta_iota_reduce t1' in + match (Subst.compress t0').n, (Subst.compress t1').n with + | Tm_refine _, _ | _, Tm_refine _ -> + check_relation g rel t0' t1' + | _ -> + //Not a refinement: try three fallbacks in order. + //1. Unfolded without guards (handles structurally equal + // after unfolding). + //2. Structural with guards (handles equatable args like + // variables, producing simple arg-level guards for + // e.g. slprop type abbreviations). + //3. Unfolded with guards (handles non-equatable args + // like constants, where unfolding may expose equatable + // functions like op_Equality). + handle_with + (no_guard (check_relation g rel t0' t1')) + (fun _ -> + handle_with + (structural ()) + (fun _ -> check_relation g rel t0' t1')) + ) else structural ()) in if guard_ok && (rel=EQUALITY) && From 2dd2bd7b3a7a5e2e40d08d4706c595fe9b344c2d Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Wed, 20 May 2026 17:05:17 -0700 Subject: [PATCH 04/24] avoid some needless retries if the guards are not allowed by the context --- src/typechecker/FStarC.TypeChecker.Core.fst | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/typechecker/FStarC.TypeChecker.Core.fst b/src/typechecker/FStarC.TypeChecker.Core.fst index d831ec1bb72..ac5f6e43e6f 100644 --- a/src/typechecker/FStarC.TypeChecker.Core.fst +++ b/src/typechecker/FStarC.TypeChecker.Core.fst @@ -1330,7 +1330,9 @@ let rec check_relation' (g:env) (rel:relation) (t0 t1:typ) match maybe_unfold_side Both t0 t1 with | None -> //Can't unfold: fall back to structural with guards - structural () + if! guard_not_allowed + then err "structural check fails, guards not allowed, and cannot unfold further" + else structural () | Some (t0', t1') -> //Check if unfolding exposes a refinement type. //If so, the refinement comparison produces properly @@ -1342,6 +1344,9 @@ let rec check_relation' (g:env) (rel:relation) (t0 t1:typ) | Tm_refine _, _ | _, Tm_refine _ -> check_relation g rel t0' t1' | _ -> + if! guard_not_allowed then + check_relation g rel t0' t1' + else //Not a refinement: try three fallbacks in order. //1. Unfolded without guards (handles structurally equal // after unfolding). From 35d6086672021d8f86a6f0b4d313e026b76b65a6 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Wed, 20 May 2026 17:05:34 -0700 Subject: [PATCH 05/24] remind myself and agents of clean-2 --- .github/agents/FStarDev.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/.github/agents/FStarDev.md b/.github/agents/FStarDev.md index 23c4f70c415..ce5e63f9f40 100644 --- a/.github/agents/FStarDev.md +++ b/.github/agents/FStarDev.md @@ -185,6 +185,12 @@ make -j$(nproc) 3 FSTAR_EXTERNAL_STAGE0=/path/to/fstar.exe 3. Test: `make test-3` or run targeted tests 4. Repeat +If you make a change that modifies the behavior of the compiler and you need to test +that it does not introduce any regressions without doing a full bootstrap, you can do +`make clean-2` followed by `make`: this will rebuild the compiler, then the +standard library using the new compiler, then stage3 and Pulse etc, without needing to +rebuild stage0 and stage1. + Note: as the compiler is modified and rebuilt, the tests that succeeded are not invalidated to make iteration faster. A final `make -C tests clean && make test` is usually useful. From 191921682f1163777c36112c2a2988fa30ee35da Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Wed, 20 May 2026 17:23:28 -0700 Subject: [PATCH 06/24] handle terms marked with the injective attribute --- src/typechecker/FStarC.TypeChecker.Core.fst | 18 +++++++++++++----- 1 file changed, 13 insertions(+), 5 deletions(-) diff --git a/src/typechecker/FStarC.TypeChecker.Core.fst b/src/typechecker/FStarC.TypeChecker.Core.fst index ac5f6e43e6f..fc7c4b860f2 100644 --- a/src/typechecker/FStarC.TypeChecker.Core.fst +++ b/src/typechecker/FStarC.TypeChecker.Core.fst @@ -1030,6 +1030,12 @@ let maybe_relate_after_unfolding (g:Env.env) t0 t1 : ML side = else Right +let is_marked_injective env t = + match (U.un_uinst t).n with + | Tm_fvar fv -> + Env.fv_has_attr env fv PC.unifier_hint_injective_lid + | _ -> false + instance showable_rel : showable relation = { show = fun rel -> match rel with @@ -1314,11 +1320,11 @@ let rec check_relation' (g:env) (rel:relation) (t0 t1:typ) This is designed to be able to prove things like `v.v1 == u.v1` first by trying to unify `v` and `u` and if it fails then prove `v.v1 == u.v1` *) + let structural () = + check_relation g EQUALITY head0 head1 ;! + check_relation_args g EQUALITY args0 args1 + in let compare_head_and_args () = - let structural () = - check_relation g EQUALITY head0 head1 ;! - check_relation_args g EQUALITY args0 args1 - in handle_with //cf. Issue 4239 //First try structural comparison without SMT guards. @@ -1364,7 +1370,9 @@ let rec check_relation' (g:env) (rel:relation) (t0 t1:typ) (fun _ -> check_relation g rel t0' t1')) ) else structural ()) in - if guard_ok && + if is_marked_injective g.tcenv head0 + then structural () + else if guard_ok && (rel=EQUALITY) && (equatable g t0 || equatable g t1) then ( From d7499aacea8d8f3af20cb6241fd2b1c99a31096a Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Wed, 20 May 2026 18:31:44 -0700 Subject: [PATCH 07/24] CoreVsRel tests: Group 17 mimics ha_val_core / Pulse slprop pattern 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> --- src/tests/FStarC.Tests.CoreVsRel.fst | 108 +++++++++++++++++++++++++++ 1 file changed, 108 insertions(+) diff --git a/src/tests/FStarC.Tests.CoreVsRel.fst b/src/tests/FStarC.Tests.CoreVsRel.fst index 334370f6c63..4b006151f9e 100644 --- a/src/tests/FStarC.Tests.CoreVsRel.fst +++ b/src/tests/FStarC.Tests.CoreVsRel.fst @@ -825,6 +825,114 @@ let run_all () : ML bool = tc_fragment_ok 1603 "let cvr_const_ok (x: cvr_const_app 2 2) : cvr_const_app 2 2 = x"; + (* ---------------------------------------------------------- + Group 17: Pulse slprop / ha_val_core pattern + Mimics the pattern from ZetaHashAccumulator: + ha_val_core b1 X =?= ha_val_core b1 Y + where ha_val_core is a type abbreviation whose body uses + Pulse slprop connectives (star, exists_, pts_to) that are + abstract types. The body interleaves both arguments in + complex ways, making unfolded comparison produce complex + formula-level guards, while structural comparison (step 2) + produces a simple arg-level guard (X == Y). + + This demonstrates WHY step 2 (structural with guards) is + needed in the 3-way fallback: it produces a provable + arg-level guard where unfolded comparison would produce + complex connective-level guards that SMT can't handle. + ---------------------------------------------------------- *) + + (* Define a type abbreviation that mimics ha_val_core: + - Two args: 'core' (shared) and 'v' (differs between sides) + - Body interleaves both args in multiple positions + - Body is NOT a refinement at top level (it's an arrow/pair) + This models ha_val_core whose body is: + pts_to core.acc (fst h) ** (exists* n. pure (snd h == n) ** pts_to core.ctr n) *) + let _ = Pars.pars_and_tc_fragment + "let cvr_ha_like (core:int) (v:int) : Type = \ + (x:int{x > core + v}) -> (y:int{y > core * v}) -> bool" + in + + let cvr_ha_like_head = tc "cvr_ha_like" in + + (* Helper: create environment with c:int, a:int, b:int *) + let env_with_cab_ints () : ML (Env.env & bv & bv & bv) = + let env = tcenv () in + let int_t = tc "int" in + let c_bv = S.gen_bv "c" None int_t in + let env = Env.push_bv env c_bv in + let a_bv = S.gen_bv "a" None int_t in + let env = Env.push_bv env a_bv in + let b_bv = S.gen_bv "b" None int_t in + let env = Env.push_bv env b_bv in + (env, c_bv, a_bv, b_bv) + in + + (* Test 1700: cvr_ha_like c a =?= cvr_ha_like c a — reflexive, trivial *) + let _ = + let env, c_bv, a_bv, _b_bv = env_with_cab_ints () in + let c_name = S.bv_to_name c_bv in + let a_name = S.bv_to_name a_bv in + let t0 = S.mk_Tm_app cvr_ha_like_head [(c_name, None); (a_name, None)] FStarC.Range.dummyRange in + compare_equality_env 1700 env t0 t0 BothTrivial + in + + (* Test 1701: cvr_ha_like c a =?= cvr_ha_like c b — EQUALITY, different 2nd arg. + This is THE ha_val_core pattern: + - Core: structural fallback (step 2) produces guard (a == b). + Path: compare_head_and_args → no_guard(structural) fails → + unfold → non-refinement → 3-way: no_guard(unfolded) fails → + structural() succeeds with guard a == b. + - Rel: try_teq without SMT cannot prove equality of + the abbreviation applications → fails. + This is exactly why step 2 exists: without it, only step 3 + (unfolded with guards) would be tried, producing complex + formula-level guards from the arrow/refinement body. *) + let _ = + let env, c_bv, a_bv, b_bv = env_with_cab_ints () in + let c_name = S.bv_to_name c_bv in + let a_name = S.bv_to_name a_bv in + let b_name = S.bv_to_name b_bv in + let t0 = S.mk_Tm_app cvr_ha_like_head [(c_name, None); (a_name, None)] FStarC.Range.dummyRange in + let t1 = S.mk_Tm_app cvr_ha_like_head [(c_name, None); (b_name, None)] FStarC.Range.dummyRange in + compare_equality_env 1701 env t0 t1 RelFailCoreSucceed + in + + (* Test 1702: cvr_ha_like a b =?= cvr_ha_like b a — EQUALITY, both args swapped. + Core: structural (step 2) produces guard (a == b /\ b == a). + Rel: fails. *) + let _ = + let env, _c_bv, a_bv, b_bv = env_with_cab_ints () in + let a_name = S.bv_to_name a_bv in + let b_name = S.bv_to_name b_bv in + let t0 = S.mk_Tm_app cvr_ha_like_head [(a_name, None); (b_name, None)] FStarC.Range.dummyRange in + let t1 = S.mk_Tm_app cvr_ha_like_head [(b_name, None); (a_name, None)] FStarC.Range.dummyRange in + compare_equality_env 1702 env t0 t1 RelFailCoreSucceed + in + + (* Test 1703: cvr_ha_like c a <: cvr_ha_like c b — SUBTYPING variant. + Both Core and Rel can produce guards here: + - Core: structural (step 2) produces simple guard (a == b) + - Rel: unfolds to arrows, compares with variance, produces + formula-level guards (forall x. x > c+b ==> x > c+a, etc.) + Both succeed with guards, but Core's guard is simpler. *) + let _ = + let env, c_bv, a_bv, b_bv = env_with_cab_ints () in + let c_name = S.bv_to_name c_bv in + let a_name = S.bv_to_name a_bv in + let b_name = S.bv_to_name b_bv in + let t0 = S.mk_Tm_app cvr_ha_like_head [(c_name, None); (a_name, None)] FStarC.Range.dummyRange in + let t1 = S.mk_Tm_app cvr_ha_like_head [(c_name, None); (b_name, None)] FStarC.Range.dummyRange in + compare_subtyping_env 1703 env t0 t1 BothGuarded + in + + (* Test 1704: integration test — coercion through ha_val_core-like abbreviation. + With a hypothesis a == b in scope, the structural guard should be provable. *) + tc_fragment_ok 1704 + "let cvr_ha_coerce (c:int) (a:int) (b:int) \ + (pf: squash (a == b)) \ + (x: cvr_ha_like c a) : cvr_ha_like c b = x"; + (* ---------------------------------------------------------- Summary ---------------------------------------------------------- *) From f01b057efe1b8d7a67bb24d118fcc7ed38b2d764 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Wed, 20 May 2026 18:41:17 -0700 Subject: [PATCH 08/24] CoreVsRel tests: use try_teq smt_ok=true for fair comparison MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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> --- src/tests/FStarC.Tests.CoreVsRel.fst | 51 +++++++++++++--------------- 1 file changed, 24 insertions(+), 27 deletions(-) diff --git a/src/tests/FStarC.Tests.CoreVsRel.fst b/src/tests/FStarC.Tests.CoreVsRel.fst index 4b006151f9e..76fd16eea14 100644 --- a/src/tests/FStarC.Tests.CoreVsRel.fst +++ b/src/tests/FStarC.Tests.CoreVsRel.fst @@ -74,10 +74,10 @@ let run_rel_subtyping (env:Env.env) (t0 t1:typ) let g = Rel.simplify_guard env g in Some g.guard_f -(* Run Rel's try_teq (no SMT), return guard_formula *) +(* Run Rel's try_teq (with SMT guards enabled), return guard_formula *) let run_rel_equality (env:Env.env) (t0 t1:typ) : ML (option guard_formula) - = match Rel.try_teq false env t0 t1 with + = match Rel.try_teq true env t0 t1 with | None -> None | Some g -> let g = Rel.simplify_guard env g in @@ -370,12 +370,11 @@ let run_all () : ML bool = ---------------------------------------------------------- *) (* Test 600: cvr_natlt 5 =?= cvr_natlt 10 - Core can produce a guard (forall i. i < 5 == i < 10); - Rel's try_teq with smt_ok=false can't solve this, so it fails. - This is an expected divergence: equality of distinct type - abbreviation applications is harder for Rel without SMT. *) + Both produce guards: + - Core: forall i. i < 5 == i < 10 + - Rel: defers equality to SMT *) let _ = - compare_equality 600 (tc "cvr_natlt 5") (tc "cvr_natlt 10") RelFailCoreSucceed + compare_equality 600 (tc "cvr_natlt 5") (tc "cvr_natlt 10") BothGuarded in (* Test 601: cvr_natlt 5 =?= i:nat{ i < 5 } — unfolding should yield equality *) @@ -457,8 +456,8 @@ let run_all () : ML bool = let i_name = S.bv_to_name i_bv in let t0 = S.mk_Tm_app cvr_natlt_head [(i_name, None)] FStarC.Range.dummyRange in let t1 = S.mk_Tm_app cvr_natlt_head [(n_name, None)] FStarC.Range.dummyRange in - (* Core produces guard i == n; Rel fails without SMT *) - compare_equality_env 704 env t0 t1 RelFailCoreSucceed + (* Both produce guards: Core emits i == n; Rel defers to SMT *) + compare_equality_env 704 env t0 t1 BothGuarded in (* Test 705: with n:nat, i:nat in env: @@ -472,14 +471,14 @@ let run_all () : ML bool = (* Test 706: with n:nat, i:nat in env: cvr_ty0 i =?= cvr_ty0 n (equality with variables) - Same bug pattern as 704 but with different abbreviation. *) + Same pattern as 704: both produce guards. *) let _ = let env, n_bv, i_bv = env_with_n_i () in let n_name = S.bv_to_name n_bv in let i_name = S.bv_to_name i_bv in let t0 = S.mk_Tm_app cvr_ty0_head [(i_name, None)] FStarC.Range.dummyRange in let t1 = S.mk_Tm_app cvr_ty0_head [(n_name, None)] FStarC.Range.dummyRange in - compare_equality_env 706 env t0 t1 RelFailCoreSucceed + compare_equality_env 706 env t0 t1 BothGuarded in (* ---------------------------------------------------------- @@ -664,16 +663,15 @@ let run_all () : ML bool = in (* Test 1301: (nat -> bool) =?= (int -> bool) — different domains - Rel can't prove arrow equality without SMT. - Core produces a guard (which is also buggy — equates refinement - formulas via injectivity: l_True == (i >= 0 == true)). *) + Both produce guards: Core equates refinement formulas; + Rel defers domain equality to SMT. *) let _ = - compare_equality 1301 (tc "nat -> bool") (tc "int -> bool") RelFailCoreSucceed + compare_equality 1301 (tc "nat -> bool") (tc "int -> bool") BothGuarded in (* Test 1302: with n:nat, i:nat in env: (cvr_natlt n -> bool) =?= (cvr_natlt i -> bool) (arrow equality with var args) - Core will produce equational guard; Rel fails without SMT. *) + Both produce guards: Core emits equational guard; Rel defers to SMT. *) let _ = let env, n_bv, i_bv = env_with_n_i () in let n_name = S.bv_to_name n_bv in @@ -685,7 +683,7 @@ let run_all () : ML bool = let b1 = S.mk_binder (S.gen_bv "_" None dom1) in let t0 = U.arrow [b0] (S.mk_Total bool_t) in let t1 = U.arrow [b1] (S.mk_Total bool_t) in - compare_equality_env 1302 env t0 t1 RelFailCoreSucceed + compare_equality_env 1302 env t0 t1 BothGuarded in (* ---------------------------------------------------------- @@ -787,7 +785,7 @@ let run_all () : ML bool = let b_name = S.bv_to_name b_bv in let t0 = S.mk_Tm_app cvr_nonref_wrap_head [(a_name, None)] FStarC.Range.dummyRange in let t1 = S.mk_Tm_app cvr_nonref_wrap_head [(b_name, None)] FStarC.Range.dummyRange in - compare_equality_env 1504 env t0 t1 RelFailCoreSucceed + compare_equality_env 1504 env t0 t1 BothGuarded in (* ---------------------------------------------------------- @@ -879,15 +877,14 @@ let run_all () : ML bool = (* Test 1701: cvr_ha_like c a =?= cvr_ha_like c b — EQUALITY, different 2nd arg. This is THE ha_val_core pattern: - - Core: structural fallback (step 2) produces guard (a == b). + - Core: structural fallback (step 2) produces simple guard (a == b). Path: compare_head_and_args → no_guard(structural) fails → unfold → non-refinement → 3-way: no_guard(unfolded) fails → structural() succeeds with guard a == b. - - Rel: try_teq without SMT cannot prove equality of - the abbreviation applications → fails. - This is exactly why step 2 exists: without it, only step 3 - (unfolded with guards) would be tried, producing complex - formula-level guards from the arrow/refinement body. *) + - Rel: unfolds, compares arrows, defers domain equality to SMT, + producing complex formula-level guards. + Both succeed with guards, but Core's is simpler and more + SMT-friendly — this is why step 2 exists. *) let _ = let env, c_bv, a_bv, b_bv = env_with_cab_ints () in let c_name = S.bv_to_name c_bv in @@ -895,19 +892,19 @@ let run_all () : ML bool = let b_name = S.bv_to_name b_bv in let t0 = S.mk_Tm_app cvr_ha_like_head [(c_name, None); (a_name, None)] FStarC.Range.dummyRange in let t1 = S.mk_Tm_app cvr_ha_like_head [(c_name, None); (b_name, None)] FStarC.Range.dummyRange in - compare_equality_env 1701 env t0 t1 RelFailCoreSucceed + compare_equality_env 1701 env t0 t1 BothGuarded in (* Test 1702: cvr_ha_like a b =?= cvr_ha_like b a — EQUALITY, both args swapped. Core: structural (step 2) produces guard (a == b /\ b == a). - Rel: fails. *) + Rel: defers equality to SMT. *) let _ = let env, _c_bv, a_bv, b_bv = env_with_cab_ints () in let a_name = S.bv_to_name a_bv in let b_name = S.bv_to_name b_bv in let t0 = S.mk_Tm_app cvr_ha_like_head [(a_name, None); (b_name, None)] FStarC.Range.dummyRange in let t1 = S.mk_Tm_app cvr_ha_like_head [(b_name, None); (a_name, None)] FStarC.Range.dummyRange in - compare_equality_env 1702 env t0 t1 RelFailCoreSucceed + compare_equality_env 1702 env t0 t1 BothGuarded in (* Test 1703: cvr_ha_like c a <: cvr_ha_like c b — SUBTYPING variant. From a5514447f0412d5326c63acb79210f119cd424c1 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Wed, 20 May 2026 19:10:35 -0700 Subject: [PATCH 09/24] Pulse prover: prefer no-unfold slprop equivalence checking 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> --- pulse/src/checker/Pulse.Checker.Prover.fst | 13 ++++++++++++- pulse/src/checker/Pulse.Typing.Util.fst | 7 +++++++ pulse/src/checker/Pulse.Typing.Util.fsti | 7 +++++++ 3 files changed, 26 insertions(+), 1 deletion(-) diff --git a/pulse/src/checker/Pulse.Checker.Prover.fst b/pulse/src/checker/Pulse.Checker.Prover.fst index 0f057cb1a2a..4a55f35b239 100644 --- a/pulse/src/checker/Pulse.Checker.Prover.fst +++ b/pulse/src/checker/Pulse.Checker.Prover.fst @@ -733,7 +733,18 @@ let check_slprop_equiv_ext r (g:env) (p q:slprop) = let p = RU.deep_compress_safe p in let q = RU.deep_compress_safe q in - let res, issues = Pulse.Typing.Util.check_equiv_now (elab_env g) p q in + // For slprop comparisons, avoid implicit unfolding of type abbreviations. + // The Pulse prover has already matched atoms via MKeys at the right + // abstraction level; unfolding would produce complex connective-level + // guards instead of simple arg-level guards. + // Fall back to full check_equiv_now (with unfolding) if the no-unfold + // check fails. + let res, issues = + let r, _ = Pulse.Typing.Util.check_equiv_now_nounfold (elab_env g) p q in + match r with + | Some _ -> (r, []) + | None -> Pulse.Typing.Util.check_equiv_now (elab_env g) p q + in match res with | None -> fail_doc_with_subissues g (Some r) issues [ diff --git a/pulse/src/checker/Pulse.Typing.Util.fst b/pulse/src/checker/Pulse.Typing.Util.fst index 72817096f1b..af1d02004aa 100644 --- a/pulse/src/checker/Pulse.Typing.Util.fst +++ b/pulse/src/checker/Pulse.Typing.Util.fst @@ -32,6 +32,13 @@ let check_equiv_now_nosmt tcenv t0 t1 = let check_equiv_now_nosmt_unfold tcenv t0 t1 = T.t_check_equiv false true tcenv t0 t1 +(* Allows SMT guards but disables unfolding. + Structural comparison produces simple arg-level guards + without looking through type abbreviations. *) +let check_equiv_now_nounfold tcenv t0 t1 = + T.with_policy ForceSMT (fun () -> + T.t_check_equiv true false tcenv t0 t1) + let universe_of_now g e = T.with_policy ForceSMT (fun () -> T.universe_of g e) diff --git a/pulse/src/checker/Pulse.Typing.Util.fsti b/pulse/src/checker/Pulse.Typing.Util.fsti index e55f618f451..5b243277dd3 100644 --- a/pulse/src/checker/Pulse.Typing.Util.fsti +++ b/pulse/src/checker/Pulse.Typing.Util.fsti @@ -31,6 +31,13 @@ val check_equiv_now_nosmt (g:env) (t1 t2 : term) val check_equiv_now_nosmt_unfold (g:env) (t1 t2 : term) : Tac (option (squash (equiv_token g t1 t2)) & issues) +(* Like check_equiv_now, but disallows unfolding. + Produces structural arg-level guards without looking + through type abbreviations. Useful for slprop comparisons + where the abstraction level should be preserved. *) +val check_equiv_now_nounfold (g:env) (t1 t2 : term) + : Tac (option (squash (equiv_token g t1 t2)) & issues) + (* Like T.universe_of, but will make sure to not delay any VC. *) val universe_of_now : g:env -> e:term -> Tac (option (u:universe{typing_token g e (E_Total, pack_ln (Reflection.V2.Tv_Type u))}) & issues) From 923f3416bf8e9db377c0a0b7ed59c241ee3931ed Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Wed, 20 May 2026 23:21:16 -0700 Subject: [PATCH 10/24] Core: add check_term_equality_head_injective; Pulse prover uses it for 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> --- pulse/src/checker/Pulse.Checker.Prover.fst | 39 +++++++++----------- pulse/src/checker/Pulse.RuntimeUtils.fsti | 1 + pulse/src/checker/Pulse.Typing.Util.fst | 7 ---- pulse/src/checker/Pulse.Typing.Util.fsti | 7 ---- pulse/src/ml/Pulse_RuntimeUtils.ml | 19 ++++++++++ src/typechecker/FStarC.TypeChecker.Core.fst | 21 ++++++++++- src/typechecker/FStarC.TypeChecker.Core.fsti | 8 ++++ 7 files changed, 66 insertions(+), 36 deletions(-) diff --git a/pulse/src/checker/Pulse.Checker.Prover.fst b/pulse/src/checker/Pulse.Checker.Prover.fst index 4a55f35b239..931a8fe2401 100644 --- a/pulse/src/checker/Pulse.Checker.Prover.fst +++ b/pulse/src/checker/Pulse.Checker.Prover.fst @@ -733,27 +733,24 @@ let check_slprop_equiv_ext r (g:env) (p q:slprop) = let p = RU.deep_compress_safe p in let q = RU.deep_compress_safe q in - // For slprop comparisons, avoid implicit unfolding of type abbreviations. - // The Pulse prover has already matched atoms via MKeys at the right - // abstraction level; unfolding would produce complex connective-level - // guards instead of simple arg-level guards. - // Fall back to full check_equiv_now (with unfolding) if the no-unfold - // check fails. - let res, issues = - let r, _ = Pulse.Typing.Util.check_equiv_now_nounfold (elab_env g) p q in - match r with - | Some _ -> (r, []) - | None -> Pulse.Typing.Util.check_equiv_now (elab_env g) p q - in - match res with - | None -> - fail_doc_with_subissues g (Some r) issues [ - text "Could not prove equality of:"; - pp p; - pp q; - ] - | Some token -> - () + // For slprop comparisons, first try head-injective equality: + // treat the head symbol as injective and check argument-level equality + // with unfolding and guards allowed. This avoids unfolding slprop + // connectives while still allowing args to be simplified. + // Fall back to full check_equiv_now (with unfolding) if that fails. + if RU.check_equiv_head_injective (elab_env g) p q + then () + else + let res, issues = Pulse.Typing.Util.check_equiv_now (elab_env g) p q in + match res with + | None -> + fail_doc_with_subissues g (Some r) issues [ + text "Could not prove equality of:"; + pp p; + pp q; + ] + | Some token -> + () let on_name = R.inspect_fv (R.pack_fv <| Pulse.Reflection.Util.mk_pulse_lib_core_lid "on") let on_head_id : head_id = FVarHead on_name diff --git a/pulse/src/checker/Pulse.RuntimeUtils.fsti b/pulse/src/checker/Pulse.RuntimeUtils.fsti index 8fd039d1a69..1c9227aa458 100644 --- a/pulse/src/checker/Pulse.RuntimeUtils.fsti +++ b/pulse/src/checker/Pulse.RuntimeUtils.fsti @@ -77,6 +77,7 @@ val tc_term_phase1 (g:env) (t:T.term) (instantiate_imps:bool) : Dv (option (T.te val teq_nosmt_force (g:env) (ty1 ty2:T.term) : Dv bool val teq_nosmt_force_phase1 (g:env) (ty1 ty2:T.term) : Dv bool val teq_nosmt_phase1 (g:env) (ty1 ty2:T.term) : Dv bool +val check_equiv_head_injective (g:env) (ty1 ty2:T.term) : Dv bool val whnf_lax (g:env) (t:T.term) : T.term val hnf_lax (g:env) (t:T.term) : T.term val beta_lax (g:env) (t:T.term) : T.term diff --git a/pulse/src/checker/Pulse.Typing.Util.fst b/pulse/src/checker/Pulse.Typing.Util.fst index af1d02004aa..72817096f1b 100644 --- a/pulse/src/checker/Pulse.Typing.Util.fst +++ b/pulse/src/checker/Pulse.Typing.Util.fst @@ -32,13 +32,6 @@ let check_equiv_now_nosmt tcenv t0 t1 = let check_equiv_now_nosmt_unfold tcenv t0 t1 = T.t_check_equiv false true tcenv t0 t1 -(* Allows SMT guards but disables unfolding. - Structural comparison produces simple arg-level guards - without looking through type abbreviations. *) -let check_equiv_now_nounfold tcenv t0 t1 = - T.with_policy ForceSMT (fun () -> - T.t_check_equiv true false tcenv t0 t1) - let universe_of_now g e = T.with_policy ForceSMT (fun () -> T.universe_of g e) diff --git a/pulse/src/checker/Pulse.Typing.Util.fsti b/pulse/src/checker/Pulse.Typing.Util.fsti index 5b243277dd3..e55f618f451 100644 --- a/pulse/src/checker/Pulse.Typing.Util.fsti +++ b/pulse/src/checker/Pulse.Typing.Util.fsti @@ -31,13 +31,6 @@ val check_equiv_now_nosmt (g:env) (t1 t2 : term) val check_equiv_now_nosmt_unfold (g:env) (t1 t2 : term) : Tac (option (squash (equiv_token g t1 t2)) & issues) -(* Like check_equiv_now, but disallows unfolding. - Produces structural arg-level guards without looking - through type abbreviations. Useful for slprop comparisons - where the abstraction level should be preserved. *) -val check_equiv_now_nounfold (g:env) (t1 t2 : term) - : Tac (option (squash (equiv_token g t1 t2)) & issues) - (* Like T.universe_of, but will make sure to not delay any VC. *) val universe_of_now : g:env -> e:term -> Tac (option (u:universe{typing_token g e (E_Total, pack_ln (Reflection.V2.Tv_Type u))}) & issues) diff --git a/pulse/src/ml/Pulse_RuntimeUtils.ml b/pulse/src/ml/Pulse_RuntimeUtils.ml index 33cea324835..02704749774 100644 --- a/pulse/src/ml/Pulse_RuntimeUtils.ml +++ b/pulse/src/ml/Pulse_RuntimeUtils.ml @@ -224,6 +224,25 @@ let teq_nosmt (g:TcEnv.env) (ty1:S.term) (ty2:S.term) = let teq_nosmt_phase1 (g:TcEnv.env) (ty1:S.term) (ty2:S.term) = teq_nosmt {g with phase1=true; admit=true } ty1 ty2 +let check_equiv_head_injective (g:TcEnv.env) (ty1:S.term) (ty2:S.term) = + let issues, res = FStarC_Errors.catch_errors (fun _ -> + let g = TcEnv.set_range g ty1.pos in + FStarC_TypeChecker_Core.check_term_equality_head_injective g ty1 ty2) in + match res with + | Some (FStar_Pervasives.Inl None) -> true + | Some (FStar_Pervasives.Inl (Some (guard_f, commit))) -> + let guard_t = FStarC_TypeChecker_Env.guard_of_guard_formula + (FStarC_TypeChecker_Common.NonTrivial guard_f) in + let discharged = + FStarC_Errors.catch_errors (fun _ -> + FStarC_TypeChecker_Rel.discharge_guard g guard_t) in + (match discharged with + | ([], Some _) -> + commit (); + true + | _ -> false) + | _ -> false + let whnf_lax (g:TcEnv.env) (t:S.term) : S.term = FStarC_TypeChecker_Normalize.unfold_whnf' [TcEnv.Unascribe] g t diff --git a/src/typechecker/FStarC.TypeChecker.Core.fst b/src/typechecker/FStarC.TypeChecker.Core.fst index fc7c4b860f2..c91e8737e15 100644 --- a/src/typechecker/FStarC.TypeChecker.Core.fst +++ b/src/typechecker/FStarC.TypeChecker.Core.fst @@ -2382,4 +2382,23 @@ let check_term_subtyping guard_ok unfolding_ok g t0 t1 let ctx = { unfolding_ok = unfolding_ok; no_guard = not guard_ok; error_context = [("Subtyping", None)] } in match check_relation g (SUBTYPING None) t0 t1 ctx initial_cache with | Success ((_, g), cache) -> Inl (return_my_guard_and_tok_t g cache) - | Error err -> Inr err \ No newline at end of file + | Error err -> Inr err + +let check_term_equality_head_injective g t0 t1 + = let head0, args0 = U.leftmost_head_and_args t0 in + let head1, args1 = U.leftmost_head_and_args t1 in + let heads_match = + match (U.un_uinst head0).n, (U.un_uinst head1).n with + | Tm_fvar fv0, Tm_fvar fv1 -> fv_eq fv0 fv1 + | Tm_name x0, Tm_name x1 -> bv_eq x0 x1 + | _ -> equal_term head0 head1 + in + if not heads_match + then Inr ({ no_guard = false; unfolding_ok = true; error_context = [("HeadInjective", None)] }, + Errors.mkmsg "Head mismatch in check_term_equality_head_injective") + else + let g = initial_env g in + let ctx = { unfolding_ok = true; no_guard = false; error_context = [("HeadInjective", None)] } in + match check_relation_args g EQUALITY args0 args1 ctx initial_cache with + | Success ((_, g), cache) -> Inl (return_my_guard_and_tok_t g cache) + | Error err -> Inr err \ No newline at end of file diff --git a/src/typechecker/FStarC.TypeChecker.Core.fsti b/src/typechecker/FStarC.TypeChecker.Core.fsti index c7c890e82e6..689a2a8aaad 100644 --- a/src/typechecker/FStarC.TypeChecker.Core.fsti +++ b/src/typechecker/FStarC.TypeChecker.Core.fsti @@ -90,3 +90,11 @@ val check_term_equality (guard_ok:bool) (unfolding_ok:bool) (g:Env.env) (t0 t1:t val check_term_subtyping (guard_ok:bool) (unfolding_ok:bool) (g:Env.env) (t0 t1:typ) : ML (either (option guard_and_tok_t) error) + +(* Check equality of two terms assuming their head symbol is injective. + Decomposes both terms into head+args, verifies heads match, then checks + argument-wise equality with guards and unfolding allowed. + Used by the Pulse prover for slprop equivalence where the head symbol + (e.g., a vprop connective) should not be unfolded. *) +val check_term_equality_head_injective (g:Env.env) (t0 t1:typ) + : ML (either (option guard_and_tok_t) error) From 1569b462bc2cd3e4dd409e2852527fc25444f262 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Wed, 20 May 2026 23:21:23 -0700 Subject: [PATCH 11/24] Tests: add Group 18 head-injective API tests to CoreVsRel suite MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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> --- src/tests/FStarC.Tests.CoreVsRel.fst | 57 ++++++++++++++++++++++++++++ 1 file changed, 57 insertions(+) diff --git a/src/tests/FStarC.Tests.CoreVsRel.fst b/src/tests/FStarC.Tests.CoreVsRel.fst index 76fd16eea14..f5c78085a40 100644 --- a/src/tests/FStarC.Tests.CoreVsRel.fst +++ b/src/tests/FStarC.Tests.CoreVsRel.fst @@ -930,6 +930,63 @@ let run_all () : ML bool = (pf: squash (a == b)) \ (x: cvr_ha_like c a) : cvr_ha_like c b = x"; + (* ---------------------------------------------------------- + Group 18: Head-injective API tests + Tests the check_term_equality_head_injective API directly. + This API treats the head as injective and checks args with + unfolding + guards. Used by the Pulse prover for slprops. + ---------------------------------------------------------- *) + + (* Test 1800: head-injective on identical terms — trivial success *) + let _ = + let env, c_bv, a_bv, _b_bv = env_with_cab_ints () in + let c_name = S.bv_to_name c_bv in + let a_name = S.bv_to_name a_bv in + let t0 = S.mk_Tm_app cvr_ha_like_head [(c_name, None); (a_name, None)] FStarC.Range.dummyRange in + match Core.check_term_equality_head_injective env t0 t0 with + | Inl None -> + Format.print_string "Test 1800 (head-injective reflexive): PASS (trivial)\n" + | Inl (Some _) -> + Format.print_string "Test 1800 (head-injective reflexive): PASS (guarded, expected trivial)\n" + | Inr _ -> + Format.print_string "Test 1800 (head-injective reflexive): FAIL (error)\n"; + success := false + in + + (* Test 1801: head-injective on different args — should produce guard *) + let _ = + let env, c_bv, a_bv, b_bv = env_with_cab_ints () in + let c_name = S.bv_to_name c_bv in + let a_name = S.bv_to_name a_bv in + let b_name = S.bv_to_name b_bv in + let t0 = S.mk_Tm_app cvr_ha_like_head [(c_name, None); (a_name, None)] FStarC.Range.dummyRange in + let t1 = S.mk_Tm_app cvr_ha_like_head [(c_name, None); (b_name, None)] FStarC.Range.dummyRange in + match Core.check_term_equality_head_injective env t0 t1 with + | Inl (Some _) -> + Format.print_string "Test 1801 (head-injective diff args): PASS (guarded)\n" + | Inl None -> + Format.print_string "Test 1801 (head-injective diff args): FAIL (trivial, expected guard)\n"; + success := false + | Inr _ -> + Format.print_string "Test 1801 (head-injective diff args): FAIL (error)\n"; + success := false + in + + (* Test 1802: head-injective with mismatched heads — should fail *) + let _ = + let env, _c_bv, a_bv, _b_bv = env_with_cab_ints () in + let a_name = S.bv_to_name a_bv in + let int_t = tc "int" in + let t0 = S.mk_Tm_app cvr_ha_like_head [(a_name, None)] FStarC.Range.dummyRange in + let t1 = S.mk_Tm_app int_t [(a_name, None)] FStarC.Range.dummyRange in + match Core.check_term_equality_head_injective env t0 t1 with + | Inr _ -> + Format.print_string "Test 1802 (head-injective head mismatch): PASS (error)\n" + | Inl _ -> + Format.print_string "Test 1802 (head-injective head mismatch): FAIL (should have failed)\n"; + success := false + in + (* ---------------------------------------------------------- Summary ---------------------------------------------------------- *) From 429a655a43f3fca8f31529538cf0194df6e0d3a8 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Thu, 21 May 2026 08:26:50 -0700 Subject: [PATCH 12/24] Core: remove step 2 fallback; mark forall connectives injective MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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> --- pulse/lib/pulse/lib/Pulse.Lib.ForEvery.fst | 1 + pulse/lib/pulse/lib/Pulse.Lib.Forall.fsti | 1 + src/typechecker/FStarC.TypeChecker.Core.fst | 5 +---- 3 files changed, 3 insertions(+), 4 deletions(-) diff --git a/pulse/lib/pulse/lib/Pulse.Lib.ForEvery.fst b/pulse/lib/pulse/lib/Pulse.Lib.ForEvery.fst index 1705a1cdfe1..a6eb5bad6ff 100644 --- a/pulse/lib/pulse/lib/Pulse.Lib.ForEvery.fst +++ b/pulse/lib/pulse/lib/Pulse.Lib.ForEvery.fst @@ -111,6 +111,7 @@ let rec timeless_forevery_aux (#a: Type u#a) (p: a -> timeless_slprop) (s: shape timeless_exists' (fun y -> p y ** pure (mask y) ** forevery_aux p s (fun x -> mask x /\ x =!= y)) (fun y -> timeless_forevery_aux p s (fun x -> mask x /\ x =!= y)) +[@@unifier_hint_injective] let (forall+) #a (p: a -> slprop) : slprop = exists* (s: shape). forevery_aux (fun x -> p x) s (fun x -> True) diff --git a/pulse/lib/pulse/lib/Pulse.Lib.Forall.fsti b/pulse/lib/pulse/lib/Pulse.Lib.Forall.fsti index de27692a9bd..e2fa16c4c0f 100644 --- a/pulse/lib/pulse/lib/Pulse.Lib.Forall.fsti +++ b/pulse/lib/pulse/lib/Pulse.Lib.Forall.fsti @@ -26,6 +26,7 @@ module T = FStar.Tactics.V2 let forall_f (#a:Type u#a) (p:a->slprop) (#[T.exact (`emp)] v:slprop) = x:a -> stt_ghost unit emp_inames v (fun _ -> p x) +[@@ unifier_hint_injective] val ( forall* ) (#a:Type u#a) (p:a -> slprop) diff --git a/src/typechecker/FStarC.TypeChecker.Core.fst b/src/typechecker/FStarC.TypeChecker.Core.fst index c91e8737e15..b7ff2aeb220 100644 --- a/src/typechecker/FStarC.TypeChecker.Core.fst +++ b/src/typechecker/FStarC.TypeChecker.Core.fst @@ -1364,10 +1364,7 @@ let rec check_relation' (g:env) (rel:relation) (t0 t1:typ) // functions like op_Equality). handle_with (no_guard (check_relation g rel t0' t1')) - (fun _ -> - handle_with - (structural ()) - (fun _ -> check_relation g rel t0' t1')) + (fun _ -> check_relation g rel t0' t1') ) else structural ()) in if is_marked_injective g.tcenv head0 From ba461c88296f7e3c6bed42d533206f36ecb00e1c Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Fri, 22 May 2026 13:19:37 -0700 Subject: [PATCH 13/24] Core: blanket slprop injectivity via unifier_hint_injective_type MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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> --- pulse/lib/common/Pulse.Lib.Core.fsti | 5 +- src/parser/FStarC.Parser.Const.fst | 2 + src/typechecker/FStarC.TypeChecker.Core.fst | 87 ++++++++++++++++++++- src/typechecker/FStarC.TypeChecker.Rel.fst | 17 +++- ulib/FStar.Attributes.fsti | 12 +++ 5 files changed, 118 insertions(+), 5 deletions(-) diff --git a/pulse/lib/common/Pulse.Lib.Core.fsti b/pulse/lib/common/Pulse.Lib.Core.fsti index 8977abfeb82..74da5118017 100644 --- a/pulse/lib/common/Pulse.Lib.Core.fsti +++ b/pulse/lib/common/Pulse.Lib.Core.fsti @@ -67,7 +67,7 @@ val allow_ambiguous : unit (***** begin slprop_equiv *****) (* A full slprop. In universe 4 (currently!) *) -[@@erasable] +[@@erasable; unifier_hint_injective_type] val slprop : Type u#4 val timeless (p: slprop) : prop @@ -84,6 +84,7 @@ val timeless_pure (p:prop) : Lemma (timeless (pure p)) [SMTPat (timeless (pure p))] +[@@unifier_hint_not_injective] val ( ** ) (p q:slprop) : slprop val timeless_star (p q : slprop) @@ -92,6 +93,7 @@ val timeless_star (p q : slprop) (ensures timeless (p ** q)) [SMTPat (timeless (p ** q))] +[@@unifier_hint_not_injective] val ( exists* ) (#a:Type) (p:a -> slprop) : slprop val timeless_exists (#a:Type u#a) (p: a -> slprop) @@ -459,6 +461,7 @@ val loc_get () : stt_ghost loc_id emp_inames emp (fun l -> loc l) val loc_dup l : stt_ghost unit emp_inames (loc l) (fun _ -> loc l ** loc l) val loc_gather l #l' : stt_ghost unit emp_inames (loc l ** loc l') (fun _ -> loc l ** pure (l == l')) +[@@unifier_hint_not_injective] val on (l:loc_id) ([@@@mkey] p:slprop) : slprop val on_intro #l p : stt_ghost unit emp_inames (loc l ** p) (fun _ -> loc l ** on l p) val on_elim #l p : stt_ghost unit emp_inames (loc l ** on l p) (fun _ -> loc l ** p) diff --git a/src/parser/FStarC.Parser.Const.fst b/src/parser/FStarC.Parser.Const.fst index 3297a99c0f8..42836af343d 100644 --- a/src/parser/FStarC.Parser.Const.fst +++ b/src/parser/FStarC.Parser.Const.fst @@ -360,6 +360,8 @@ let normalize_for_extraction_type_lid = psconst "normalize_for_extraction_type" let tcdecltime_attr = attr "tcdecltime" let noextract_to_attr = attr "noextract_to" let unifier_hint_injective_lid = attr "unifier_hint_injective" +let unifier_hint_not_injective_lid = attr "unifier_hint_not_injective" +let unifier_hint_injective_type_lid = attr "unifier_hint_injective_type" let commute_nested_matches_lid = attr "commute_nested_matches" let ite_soundness_by_attr = attr "ite_soundness_by" let default_effect_attr = attr "default_effect" diff --git a/src/typechecker/FStarC.TypeChecker.Core.fst b/src/typechecker/FStarC.TypeChecker.Core.fst index b7ff2aeb220..f91479d2ad7 100644 --- a/src/typechecker/FStarC.TypeChecker.Core.fst +++ b/src/typechecker/FStarC.TypeChecker.Core.fst @@ -1033,7 +1033,28 @@ let maybe_relate_after_unfolding (g:Env.env) t0 t1 : ML side = let is_marked_injective env t = match (U.un_uinst t).n with | Tm_fvar fv -> - Env.fv_has_attr env fv PC.unifier_hint_injective_lid + // Explicit injective attribute always wins + if Env.fv_has_attr env fv PC.unifier_hint_injective_lid then true + // Explicit opt-out always wins + else if Env.fv_has_attr env fv PC.unifier_hint_not_injective_lid then false + // Check if the function is Delta_equational (match/if-based) + // Such functions should NOT be treated as injective since equality + // may hold by case analysis, not by argument equality. + else ( + match Env.delta_depth_of_fv env fv with + | S.Delta_equational_at_level _ -> false + | _ -> + // Check if return type has injective_type attribute + (match Env.try_lookup_lid env fv.fv_name with + | Some ((_, typ), _) -> + let _, ret_typ = U.arrow_formals typ in + let ret_head, _ = U.head_and_args ret_typ in + (match (U.un_uinst ret_head).n with + | Tm_fvar ret_fv -> + Env.fv_has_attr env ret_fv PC.unifier_hint_injective_type_lid + | _ -> false) + | _ -> false) + ) | _ -> false instance showable_rel : showable relation = { @@ -1368,7 +1389,41 @@ let rec check_relation' (g:env) (rel:relation) (t0 t1:typ) ) else structural ()) in if is_marked_injective g.tcenv head0 - then structural () + then ( + // For injective heads: first try structural without guard. + // If that fails and guards are allowed, compare each arg: + // 1. Try no_guard first (handles definitionally equal args) + // 2. For lambda args: use full check_relation (opens lambdas, + // allows unfolding inside the body, produces ∀-quantified guards) + // 3. For non-lambda args: emit_guard on original arg pair (avoids + // deeply unfolding into forms SMT can't handle) + handle_with + (no_guard (structural ())) + (fun _ -> + if not guard_ok + then err "injective head: structural check fails and guards not allowed" + else ( + check_relation g EQUALITY head0 head1 ;! + if List.length args0 = List.length args1 + then iter2 args0 args1 + (fun (a0, q0) (a1, q1) _ -> + check_aqual q0 q1;! + handle_with + (no_guard (check_relation g EQUALITY a0 a1)) + (fun _ -> + // For lambda args, use full check_relation which opens + // the lambda and allows unfolding inside the body. + // For non-lambda args, emit guard on original forms. + match (Subst.compress a0).n, (Subst.compress a1).n with + | Tm_abs _, Tm_abs _ -> + check_relation g EQUALITY a0 a1 + | _ -> + emit_guard a0 a1)) + () + else fail_str "Unequal number of arguments" + ) + ) + ) else if guard_ok && (rel=EQUALITY) && (equatable g t0 || equatable g t1) @@ -2396,6 +2451,32 @@ let check_term_equality_head_injective g t0 t1 else let g = initial_env g in let ctx = { unfolding_ok = true; no_guard = false; error_context = [("HeadInjective", None)] } in - match check_relation_args g EQUALITY args0 args1 ctx initial_cache with + // For each arg pair: try no_guard comparison, then for lambda args + // then emit guard on original arg pair + let emit_guard_for_arg a0 a1 : ML (result unit) = + let! _, t_typ = with_context "checking lhs while emitting guard" None (fun _ -> do_check g a0) in + let! u = universe_of_well_typed_term g t_typ in + guard g (U.mk_eq2 u t_typ a0 a1) + in + let check_args_with_per_arg_guards () = + if List.length args0 = List.length args1 + then iter2 args0 args1 + (fun (a0, q0) (a1, q1) _ -> + check_aqual q0 q1;! + handle_with + (no_guard (check_relation g EQUALITY a0 a1)) + (fun _ -> + // For lambda args, use full check_relation which opens + // the lambda and allows unfolding inside the body. + // For non-lambda args, emit guard on original forms. + match (Subst.compress a0).n, (Subst.compress a1).n with + | Tm_abs _, Tm_abs _ -> + check_relation g EQUALITY a0 a1 + | _ -> + emit_guard_for_arg a0 a1)) + () + else fail_str "Unequal number of arguments" + in + match check_args_with_per_arg_guards () ctx initial_cache with | Success ((_, g), cache) -> Inl (return_my_guard_and_tok_t g cache) | Error err -> Inr err \ No newline at end of file diff --git a/src/typechecker/FStarC.TypeChecker.Rel.fst b/src/typechecker/FStarC.TypeChecker.Rel.fst index 1eff12a0a95..bc69624af09 100644 --- a/src/typechecker/FStarC.TypeChecker.Rel.fst +++ b/src/typechecker/FStarC.TypeChecker.Rel.fst @@ -3659,7 +3659,22 @@ let solve_t'_aux (problem:tprob) (wl:worklist) : ML solution = let treat_as_injective = match (U.un_uinst head1).n with | Tm_fvar fv -> - Env.fv_has_attr env fv PC.unifier_hint_injective_lid + if Env.fv_has_attr env fv PC.unifier_hint_injective_lid then true + else if Env.fv_has_attr env fv PC.unifier_hint_not_injective_lid then false + else ( + match Env.delta_depth_of_fv env fv with + | S.Delta_equational_at_level _ -> false + | _ -> + (match Env.try_lookup_lid env fv.fv_name with + | Some ((_, typ), _) -> + let _, ret_typ = U.arrow_formals typ in + let ret_head, _ = U.head_and_args ret_typ in + (match (U.un_uinst ret_head).n with + | Tm_fvar ret_fv -> + Env.fv_has_attr env ret_fv PC.unifier_hint_injective_type_lid + | _ -> false) + | _ -> false) + ) | _ -> false in let is_reveal = U.is_fvar PC.reveal head1 || U.is_fvar PC.reveal head2 in diff --git a/ulib/FStar.Attributes.fsti b/ulib/FStar.Attributes.fsti index a0abb341c92..38eaa98e9b5 100644 --- a/ulib/FStar.Attributes.fsti +++ b/ulib/FStar.Attributes.fsti @@ -143,6 +143,18 @@ val tcdecltime : unit definition of `t`. *) val unifier_hint_injective : unit +(** This attribute opts a function out of injective treatment by + the unifier, even if it would otherwise be treated as injective + (e.g., due to its return type being marked with + unifier_hint_injective_type). *) +val unifier_hint_not_injective : unit + +(** This attribute on a type definition causes all functions returning + that type to be treated as injective by the unifier, unless they + are Delta_equational (i.e., defined by match/if) or explicitly + opted out via unifier_hint_not_injective. *) +val unifier_hint_injective_type : unit + (** This attribute is used to control the evaluation order and unfolding strategy for certain definitions. From 8e3fdf3bf443eaef87c607edd3435bfebe4003e2 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Sat, 23 May 2026 09:12:50 -0700 Subject: [PATCH 14/24] Remove redundant check_term_equality_head_injective API and explicit 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> --- pulse/lib/pulse/lib/Pulse.Lib.ForEvery.fst | 1 - pulse/lib/pulse/lib/Pulse.Lib.Forall.fsti | 1 - pulse/src/checker/Pulse.Checker.Prover.fst | 28 ++++------ pulse/src/checker/Pulse.RuntimeUtils.fsti | 1 - pulse/src/ml/Pulse_RuntimeUtils.ml | 19 ------- src/tests/FStarC.Tests.CoreVsRel.fst | 57 -------------------- src/typechecker/FStarC.TypeChecker.Core.fst | 47 +--------------- src/typechecker/FStarC.TypeChecker.Core.fsti | 8 --- 8 files changed, 11 insertions(+), 151 deletions(-) diff --git a/pulse/lib/pulse/lib/Pulse.Lib.ForEvery.fst b/pulse/lib/pulse/lib/Pulse.Lib.ForEvery.fst index a6eb5bad6ff..1705a1cdfe1 100644 --- a/pulse/lib/pulse/lib/Pulse.Lib.ForEvery.fst +++ b/pulse/lib/pulse/lib/Pulse.Lib.ForEvery.fst @@ -111,7 +111,6 @@ let rec timeless_forevery_aux (#a: Type u#a) (p: a -> timeless_slprop) (s: shape timeless_exists' (fun y -> p y ** pure (mask y) ** forevery_aux p s (fun x -> mask x /\ x =!= y)) (fun y -> timeless_forevery_aux p s (fun x -> mask x /\ x =!= y)) -[@@unifier_hint_injective] let (forall+) #a (p: a -> slprop) : slprop = exists* (s: shape). forevery_aux (fun x -> p x) s (fun x -> True) diff --git a/pulse/lib/pulse/lib/Pulse.Lib.Forall.fsti b/pulse/lib/pulse/lib/Pulse.Lib.Forall.fsti index e2fa16c4c0f..de27692a9bd 100644 --- a/pulse/lib/pulse/lib/Pulse.Lib.Forall.fsti +++ b/pulse/lib/pulse/lib/Pulse.Lib.Forall.fsti @@ -26,7 +26,6 @@ module T = FStar.Tactics.V2 let forall_f (#a:Type u#a) (p:a->slprop) (#[T.exact (`emp)] v:slprop) = x:a -> stt_ghost unit emp_inames v (fun _ -> p x) -[@@ unifier_hint_injective] val ( forall* ) (#a:Type u#a) (p:a -> slprop) diff --git a/pulse/src/checker/Pulse.Checker.Prover.fst b/pulse/src/checker/Pulse.Checker.Prover.fst index 931a8fe2401..0f057cb1a2a 100644 --- a/pulse/src/checker/Pulse.Checker.Prover.fst +++ b/pulse/src/checker/Pulse.Checker.Prover.fst @@ -733,24 +733,16 @@ let check_slprop_equiv_ext r (g:env) (p q:slprop) = let p = RU.deep_compress_safe p in let q = RU.deep_compress_safe q in - // For slprop comparisons, first try head-injective equality: - // treat the head symbol as injective and check argument-level equality - // with unfolding and guards allowed. This avoids unfolding slprop - // connectives while still allowing args to be simplified. - // Fall back to full check_equiv_now (with unfolding) if that fails. - if RU.check_equiv_head_injective (elab_env g) p q - then () - else - let res, issues = Pulse.Typing.Util.check_equiv_now (elab_env g) p q in - match res with - | None -> - fail_doc_with_subissues g (Some r) issues [ - text "Could not prove equality of:"; - pp p; - pp q; - ] - | Some token -> - () + let res, issues = Pulse.Typing.Util.check_equiv_now (elab_env g) p q in + match res with + | None -> + fail_doc_with_subissues g (Some r) issues [ + text "Could not prove equality of:"; + pp p; + pp q; + ] + | Some token -> + () let on_name = R.inspect_fv (R.pack_fv <| Pulse.Reflection.Util.mk_pulse_lib_core_lid "on") let on_head_id : head_id = FVarHead on_name diff --git a/pulse/src/checker/Pulse.RuntimeUtils.fsti b/pulse/src/checker/Pulse.RuntimeUtils.fsti index 1c9227aa458..8fd039d1a69 100644 --- a/pulse/src/checker/Pulse.RuntimeUtils.fsti +++ b/pulse/src/checker/Pulse.RuntimeUtils.fsti @@ -77,7 +77,6 @@ val tc_term_phase1 (g:env) (t:T.term) (instantiate_imps:bool) : Dv (option (T.te val teq_nosmt_force (g:env) (ty1 ty2:T.term) : Dv bool val teq_nosmt_force_phase1 (g:env) (ty1 ty2:T.term) : Dv bool val teq_nosmt_phase1 (g:env) (ty1 ty2:T.term) : Dv bool -val check_equiv_head_injective (g:env) (ty1 ty2:T.term) : Dv bool val whnf_lax (g:env) (t:T.term) : T.term val hnf_lax (g:env) (t:T.term) : T.term val beta_lax (g:env) (t:T.term) : T.term diff --git a/pulse/src/ml/Pulse_RuntimeUtils.ml b/pulse/src/ml/Pulse_RuntimeUtils.ml index 02704749774..33cea324835 100644 --- a/pulse/src/ml/Pulse_RuntimeUtils.ml +++ b/pulse/src/ml/Pulse_RuntimeUtils.ml @@ -224,25 +224,6 @@ let teq_nosmt (g:TcEnv.env) (ty1:S.term) (ty2:S.term) = let teq_nosmt_phase1 (g:TcEnv.env) (ty1:S.term) (ty2:S.term) = teq_nosmt {g with phase1=true; admit=true } ty1 ty2 -let check_equiv_head_injective (g:TcEnv.env) (ty1:S.term) (ty2:S.term) = - let issues, res = FStarC_Errors.catch_errors (fun _ -> - let g = TcEnv.set_range g ty1.pos in - FStarC_TypeChecker_Core.check_term_equality_head_injective g ty1 ty2) in - match res with - | Some (FStar_Pervasives.Inl None) -> true - | Some (FStar_Pervasives.Inl (Some (guard_f, commit))) -> - let guard_t = FStarC_TypeChecker_Env.guard_of_guard_formula - (FStarC_TypeChecker_Common.NonTrivial guard_f) in - let discharged = - FStarC_Errors.catch_errors (fun _ -> - FStarC_TypeChecker_Rel.discharge_guard g guard_t) in - (match discharged with - | ([], Some _) -> - commit (); - true - | _ -> false) - | _ -> false - let whnf_lax (g:TcEnv.env) (t:S.term) : S.term = FStarC_TypeChecker_Normalize.unfold_whnf' [TcEnv.Unascribe] g t diff --git a/src/tests/FStarC.Tests.CoreVsRel.fst b/src/tests/FStarC.Tests.CoreVsRel.fst index f5c78085a40..76fd16eea14 100644 --- a/src/tests/FStarC.Tests.CoreVsRel.fst +++ b/src/tests/FStarC.Tests.CoreVsRel.fst @@ -930,63 +930,6 @@ let run_all () : ML bool = (pf: squash (a == b)) \ (x: cvr_ha_like c a) : cvr_ha_like c b = x"; - (* ---------------------------------------------------------- - Group 18: Head-injective API tests - Tests the check_term_equality_head_injective API directly. - This API treats the head as injective and checks args with - unfolding + guards. Used by the Pulse prover for slprops. - ---------------------------------------------------------- *) - - (* Test 1800: head-injective on identical terms — trivial success *) - let _ = - let env, c_bv, a_bv, _b_bv = env_with_cab_ints () in - let c_name = S.bv_to_name c_bv in - let a_name = S.bv_to_name a_bv in - let t0 = S.mk_Tm_app cvr_ha_like_head [(c_name, None); (a_name, None)] FStarC.Range.dummyRange in - match Core.check_term_equality_head_injective env t0 t0 with - | Inl None -> - Format.print_string "Test 1800 (head-injective reflexive): PASS (trivial)\n" - | Inl (Some _) -> - Format.print_string "Test 1800 (head-injective reflexive): PASS (guarded, expected trivial)\n" - | Inr _ -> - Format.print_string "Test 1800 (head-injective reflexive): FAIL (error)\n"; - success := false - in - - (* Test 1801: head-injective on different args — should produce guard *) - let _ = - let env, c_bv, a_bv, b_bv = env_with_cab_ints () in - let c_name = S.bv_to_name c_bv in - let a_name = S.bv_to_name a_bv in - let b_name = S.bv_to_name b_bv in - let t0 = S.mk_Tm_app cvr_ha_like_head [(c_name, None); (a_name, None)] FStarC.Range.dummyRange in - let t1 = S.mk_Tm_app cvr_ha_like_head [(c_name, None); (b_name, None)] FStarC.Range.dummyRange in - match Core.check_term_equality_head_injective env t0 t1 with - | Inl (Some _) -> - Format.print_string "Test 1801 (head-injective diff args): PASS (guarded)\n" - | Inl None -> - Format.print_string "Test 1801 (head-injective diff args): FAIL (trivial, expected guard)\n"; - success := false - | Inr _ -> - Format.print_string "Test 1801 (head-injective diff args): FAIL (error)\n"; - success := false - in - - (* Test 1802: head-injective with mismatched heads — should fail *) - let _ = - let env, _c_bv, a_bv, _b_bv = env_with_cab_ints () in - let a_name = S.bv_to_name a_bv in - let int_t = tc "int" in - let t0 = S.mk_Tm_app cvr_ha_like_head [(a_name, None)] FStarC.Range.dummyRange in - let t1 = S.mk_Tm_app int_t [(a_name, None)] FStarC.Range.dummyRange in - match Core.check_term_equality_head_injective env t0 t1 with - | Inr _ -> - Format.print_string "Test 1802 (head-injective head mismatch): PASS (error)\n" - | Inl _ -> - Format.print_string "Test 1802 (head-injective head mismatch): FAIL (should have failed)\n"; - success := false - in - (* ---------------------------------------------------------- Summary ---------------------------------------------------------- *) diff --git a/src/typechecker/FStarC.TypeChecker.Core.fst b/src/typechecker/FStarC.TypeChecker.Core.fst index f91479d2ad7..8881183b40d 100644 --- a/src/typechecker/FStarC.TypeChecker.Core.fst +++ b/src/typechecker/FStarC.TypeChecker.Core.fst @@ -2434,49 +2434,4 @@ let check_term_subtyping guard_ok unfolding_ok g t0 t1 let ctx = { unfolding_ok = unfolding_ok; no_guard = not guard_ok; error_context = [("Subtyping", None)] } in match check_relation g (SUBTYPING None) t0 t1 ctx initial_cache with | Success ((_, g), cache) -> Inl (return_my_guard_and_tok_t g cache) - | Error err -> Inr err - -let check_term_equality_head_injective g t0 t1 - = let head0, args0 = U.leftmost_head_and_args t0 in - let head1, args1 = U.leftmost_head_and_args t1 in - let heads_match = - match (U.un_uinst head0).n, (U.un_uinst head1).n with - | Tm_fvar fv0, Tm_fvar fv1 -> fv_eq fv0 fv1 - | Tm_name x0, Tm_name x1 -> bv_eq x0 x1 - | _ -> equal_term head0 head1 - in - if not heads_match - then Inr ({ no_guard = false; unfolding_ok = true; error_context = [("HeadInjective", None)] }, - Errors.mkmsg "Head mismatch in check_term_equality_head_injective") - else - let g = initial_env g in - let ctx = { unfolding_ok = true; no_guard = false; error_context = [("HeadInjective", None)] } in - // For each arg pair: try no_guard comparison, then for lambda args - // then emit guard on original arg pair - let emit_guard_for_arg a0 a1 : ML (result unit) = - let! _, t_typ = with_context "checking lhs while emitting guard" None (fun _ -> do_check g a0) in - let! u = universe_of_well_typed_term g t_typ in - guard g (U.mk_eq2 u t_typ a0 a1) - in - let check_args_with_per_arg_guards () = - if List.length args0 = List.length args1 - then iter2 args0 args1 - (fun (a0, q0) (a1, q1) _ -> - check_aqual q0 q1;! - handle_with - (no_guard (check_relation g EQUALITY a0 a1)) - (fun _ -> - // For lambda args, use full check_relation which opens - // the lambda and allows unfolding inside the body. - // For non-lambda args, emit guard on original forms. - match (Subst.compress a0).n, (Subst.compress a1).n with - | Tm_abs _, Tm_abs _ -> - check_relation g EQUALITY a0 a1 - | _ -> - emit_guard_for_arg a0 a1)) - () - else fail_str "Unequal number of arguments" - in - match check_args_with_per_arg_guards () ctx initial_cache with - | Success ((_, g), cache) -> Inl (return_my_guard_and_tok_t g cache) - | Error err -> Inr err \ No newline at end of file + | Error err -> Inr err \ No newline at end of file diff --git a/src/typechecker/FStarC.TypeChecker.Core.fsti b/src/typechecker/FStarC.TypeChecker.Core.fsti index 689a2a8aaad..c7c890e82e6 100644 --- a/src/typechecker/FStarC.TypeChecker.Core.fsti +++ b/src/typechecker/FStarC.TypeChecker.Core.fsti @@ -90,11 +90,3 @@ val check_term_equality (guard_ok:bool) (unfolding_ok:bool) (g:Env.env) (t0 t1:t val check_term_subtyping (guard_ok:bool) (unfolding_ok:bool) (g:Env.env) (t0 t1:typ) : ML (either (option guard_and_tok_t) error) - -(* Check equality of two terms assuming their head symbol is injective. - Decomposes both terms into head+args, verifies heads match, then checks - argument-wise equality with guards and unfolding allowed. - Used by the Pulse prover for slprop equivalence where the head symbol - (e.g., a vprop connective) should not be unfolded. *) -val check_term_equality_head_injective (g:Env.env) (t0 t1:typ) - : ML (either (option guard_and_tok_t) error) From c4dbce162ca30801f2aa74e59c91ae6127f5c231 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Sat, 23 May 2026 12:42:01 -0700 Subject: [PATCH 15/24] Core: use per-arg guards in injective path; opt-out Bug110 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> --- pulse/test/LoopInvariants.fst.output.expected | 12 ++--- pulse/test/bug-reports/Bug110.fst | 2 +- .../ClosureError.fst.output.expected | 5 +- .../IfBranchMismatch.fst.output.expected | 8 +-- .../MatchBranchMismatch.fst.output.expected | 6 +-- .../NestedBlock.fst.output.expected | 2 +- .../NestedCall.fst.output.expected | 5 +- .../PrePostMismatch.fst.output.expected | 2 +- .../SequenceError.fst.output.expected | 2 +- ...nPostConditionMismatch.fst.output.expected | 8 +-- .../WhileInvPreservation.fst.output.expected | 6 +-- .../AdmitDoesNotSimpl.fst.output.expected | 12 ++--- src/typechecker/FStarC.TypeChecker.Core.fst | 2 +- .../Monoid.fst.json_output.expected | 48 +++++++++--------- .../error-messages/Monoid.fst.output.expected | 48 +++++++++--------- .../QuickTest.fst.json_output.expected | 2 +- .../QuickTest.fst.output.expected | 2 +- .../QuickTestNBE.fst.json_output.expected | 2 +- .../QuickTestNBE.fst.output.expected | 2 +- tests/tactics/Postprocess.fst.output.expected | 50 +++++++++---------- 20 files changed, 112 insertions(+), 114 deletions(-) diff --git a/pulse/test/LoopInvariants.fst.output.expected b/pulse/test/LoopInvariants.fst.output.expected index 2f4581de00b..dea24d67f67 100644 --- a/pulse/test/LoopInvariants.fst.output.expected +++ b/pulse/test/LoopInvariants.fst.output.expected @@ -1,4 +1,4 @@ -* Info at LoopInvariants.fst(65,4-65,8): +* Info at LoopInvariants.fst(65,6-65,8): - Expected failure: - Could not prove equality of: - Pulse.Lib.Reference.pts_to s 3 @@ -10,10 +10,10 @@ (s : Pulse.Lib.Reference.ref Prims.int) (meas : Prims.unit) (__ : Prims.squash (meas == ())) (__ : Prims.squash (true == true)) (__ : Prims.unit) - - VC = Pulse.Lib.Reference.pts_to s 3 == Pulse.Lib.Reference.pts_to s 2 - - See also LoopInvariants.fst(65,4-65,10) + - VC = Prims.l_False + - See also LoopInvariants.fst(65,9-65,10) -* Info at LoopInvariants.fst(76,4-76,8): +* Info at LoopInvariants.fst(76,6-76,8): - Expected failure: - Could not prove equality of: - Pulse.Lib.Reference.pts_to s 3 @@ -25,6 +25,6 @@ (s : Pulse.Lib.Reference.ref Prims.int) (meas : Prims.unit) (__ : Prims.squash (meas == ())) (__ : Prims.squash (true == true)) (__ : Prims.unit) - - VC = Pulse.Lib.Reference.pts_to s 3 == Pulse.Lib.Reference.pts_to s 2 - - See also LoopInvariants.fst(76,4-76,10) + - VC = Prims.l_False + - See also LoopInvariants.fst(76,9-76,10) diff --git a/pulse/test/bug-reports/Bug110.fst b/pulse/test/bug-reports/Bug110.fst index 8509f16ca27..7fe53e3dbaa 100644 --- a/pulse/test/bug-reports/Bug110.fst +++ b/pulse/test/bug-reports/Bug110.fst @@ -3,7 +3,7 @@ module Bug110 #lang-pulse open Pulse -[@@no_mkeys] assume val foo : int -> slprop +[@@no_mkeys; unifier_hint_not_injective] assume val foo : int -> slprop (* OK *) fn test1 (i j : int) diff --git a/pulse/test/error_messages/ClosureError.fst.output.expected b/pulse/test/error_messages/ClosureError.fst.output.expected index 07273a8c66f..7f5f57149f8 100644 --- a/pulse/test/error_messages/ClosureError.fst.output.expected +++ b/pulse/test/error_messages/ClosureError.fst.output.expected @@ -1,4 +1,4 @@ -* Info at ClosureError.fst(17,2-17,8): +* Info at ClosureError.fst(17,2-18,4): - Expected failure: - Could not prove equality of: - Pulse.Lib.Reference.pts_to r 0 @@ -13,6 +13,5 @@ -> fn requires Pulse.Class.PtsTo.pts_to r 1 ensures Pulse.Class.PtsTo.pts_to r 1) - - VC = Pulse.Lib.Reference.pts_to r 0 == Pulse.Lib.Reference.pts_to r 1 - - See also ClosureError.fst(17,2-18,4) + - VC = Prims.l_False diff --git a/pulse/test/error_messages/IfBranchMismatch.fst.output.expected b/pulse/test/error_messages/IfBranchMismatch.fst.output.expected index 31b0b93dd8d..9fee7a55499 100644 --- a/pulse/test/error_messages/IfBranchMismatch.fst.output.expected +++ b/pulse/test/error_messages/IfBranchMismatch.fst.output.expected @@ -1,4 +1,4 @@ -* Info at IfBranchMismatch.fst(14,4-14,8): +* Info at IfBranchMismatch.fst(14,6-14,8): - Expected failure: - Could not prove equality of: - Pulse.Lib.Reference.pts_to r 2 @@ -9,8 +9,8 @@ (r : Pulse.Lib.Reference.ref Prims.int) (b : Prims.bool) (_if_hyp : Prims.squash (Pulse.Lib.Core.rewrites_to_p b false)) (_if_br : Prims.unit) - - VC = Pulse.Lib.Reference.pts_to r 2 == Pulse.Lib.Reference.pts_to r 1 - - See also IfBranchMismatch.fst(14,4-14,10) + - VC = Prims.l_False + - See also IfBranchMismatch.fst(14,9-14,10) * Info at IfBranchMismatch.fst(30,4-30,6): - Expected failure: @@ -23,5 +23,5 @@ (r : Pulse.Lib.Reference.ref Prims.int) (b : Prims.bool) (_if_hyp : Prims.squash (Pulse.Lib.Core.rewrites_to_p b false)) (__ : Prims.unit) - - VC = Pulse.Lib.Reference.pts_to r 2 == Pulse.Lib.Reference.pts_to r 1 + - VC = Prims.l_False diff --git a/pulse/test/error_messages/MatchBranchMismatch.fst.output.expected b/pulse/test/error_messages/MatchBranchMismatch.fst.output.expected index 6398b24e0a4..b85d3d81543 100644 --- a/pulse/test/error_messages/MatchBranchMismatch.fst.output.expected +++ b/pulse/test/error_messages/MatchBranchMismatch.fst.output.expected @@ -1,4 +1,4 @@ -* Info at MatchBranchMismatch.fst(13,11-13,15): +* Info at MatchBranchMismatch.fst(13,13-13,15): - Expected failure: - Could not prove equality of: - Pulse.Lib.Reference.pts_to r 2 @@ -8,6 +8,6 @@ - Env = (r : Pulse.Lib.Reference.ref Prims.int) (x : Prims.int) (branch equality : Prims.squash (x == 1)) (_br : Prims.unit) - - VC = Pulse.Lib.Reference.pts_to r 2 == Pulse.Lib.Reference.pts_to r 1 - - See also MatchBranchMismatch.fst(13,11-13,17) + - VC = Prims.l_False + - See also MatchBranchMismatch.fst(13,16-13,17) diff --git a/pulse/test/error_messages/NestedBlock.fst.output.expected b/pulse/test/error_messages/NestedBlock.fst.output.expected index e00db1523b8..78b07a40f92 100644 --- a/pulse/test/error_messages/NestedBlock.fst.output.expected +++ b/pulse/test/error_messages/NestedBlock.fst.output.expected @@ -6,5 +6,5 @@ - Assertion failed - The SMT solver could not prove the query. - Env = (r : Pulse.Lib.Reference.ref Prims.int) - - VC = Pulse.Lib.Reference.pts_to r 1 == Pulse.Lib.Reference.pts_to r 0 + - VC = Prims.l_False diff --git a/pulse/test/error_messages/NestedCall.fst.output.expected b/pulse/test/error_messages/NestedCall.fst.output.expected index 6b40aac9b76..c1c059e674b 100644 --- a/pulse/test/error_messages/NestedCall.fst.output.expected +++ b/pulse/test/error_messages/NestedCall.fst.output.expected @@ -1,4 +1,4 @@ -* Info at NestedCall.fst(18,2-18,9): +* Info at NestedCall.fst(18,2-19,4): - Expected failure: - Could not prove equality of: - Pulse.Lib.Reference.pts_to r 5 @@ -6,6 +6,5 @@ - Assertion failed - The SMT solver could not prove the query. - Env = (r : Pulse.Lib.Reference.ref Prims.int) - - VC = Pulse.Lib.Reference.pts_to r 5 == Pulse.Lib.Reference.pts_to r 0 - - See also NestedCall.fst(18,2-19,4) + - VC = Prims.l_False diff --git a/pulse/test/error_messages/PrePostMismatch.fst.output.expected b/pulse/test/error_messages/PrePostMismatch.fst.output.expected index 1061f4c0beb..1011751443b 100644 --- a/pulse/test/error_messages/PrePostMismatch.fst.output.expected +++ b/pulse/test/error_messages/PrePostMismatch.fst.output.expected @@ -6,5 +6,5 @@ - Assertion failed - The SMT solver could not prove the query. - Env = (r : Pulse.Lib.Reference.ref Prims.int) (__ : Prims.unit) - - VC = Pulse.Lib.Reference.pts_to r 1 == Pulse.Lib.Reference.pts_to r 42 + - VC = Prims.l_False diff --git a/pulse/test/error_messages/SequenceError.fst.output.expected b/pulse/test/error_messages/SequenceError.fst.output.expected index 6f8b8dc5af9..4b44d091336 100644 --- a/pulse/test/error_messages/SequenceError.fst.output.expected +++ b/pulse/test/error_messages/SequenceError.fst.output.expected @@ -9,5 +9,5 @@ (r1 : Pulse.Lib.Reference.ref Prims.int) (r2 : Pulse.Lib.Reference.ref Prims.int) (__ : Prims.unit) (__ : Prims.unit) - - VC = Pulse.Lib.Reference.pts_to r2 2 == Pulse.Lib.Reference.pts_to r2 1 + - VC = Prims.l_False diff --git a/pulse/test/error_messages/TerminalActionPostConditionMismatch.fst.output.expected b/pulse/test/error_messages/TerminalActionPostConditionMismatch.fst.output.expected index 2baeab648ef..0805d379298 100644 --- a/pulse/test/error_messages/TerminalActionPostConditionMismatch.fst.output.expected +++ b/pulse/test/error_messages/TerminalActionPostConditionMismatch.fst.output.expected @@ -1,4 +1,4 @@ -* Info at TerminalActionPostConditionMismatch.fst(12,2-12,6): +* Info at TerminalActionPostConditionMismatch.fst(12,4-12,6): - Expected failure: - Could not prove equality of: - Pulse.Lib.Reference.pts_to r 2 @@ -8,8 +8,8 @@ - Env = (r : Pulse.Lib.Reference.ref Prims.int) (__ : Prims.unit) (__ : Prims.unit) - - VC = Pulse.Lib.Reference.pts_to r 2 == Pulse.Lib.Reference.pts_to r 1 - - See also TerminalActionPostConditionMismatch.fst(12,2-12,8) + - VC = Prims.l_False + - See also TerminalActionPostConditionMismatch.fst(12,7-12,8) * Info at TerminalActionPostConditionMismatch.fst(23,2-23,4): - Expected failure: @@ -21,5 +21,5 @@ - Env = (r : Pulse.Lib.Reference.ref Prims.int) (__ : Prims.unit) (__ : Prims.unit) - - VC = Pulse.Lib.Reference.pts_to r 2 == Pulse.Lib.Reference.pts_to r 1 + - VC = Prims.l_False diff --git a/pulse/test/error_messages/WhileInvPreservation.fst.output.expected b/pulse/test/error_messages/WhileInvPreservation.fst.output.expected index 6a896a2cf21..6a95e524052 100644 --- a/pulse/test/error_messages/WhileInvPreservation.fst.output.expected +++ b/pulse/test/error_messages/WhileInvPreservation.fst.output.expected @@ -1,4 +1,4 @@ -* Info at WhileInvPreservation.fst(15,4-15,8): +* Info at WhileInvPreservation.fst(15,6-15,8): - Expected failure: - Could not prove equality of: - Pulse.Lib.Reference.pts_to i 2 @@ -12,6 +12,6 @@ (__anf0 : Prims.int) (__ : Prims.squash (Pulse.Lib.Core.rewrites_to_p __anf0 0)) (__ : Prims.unit) - - VC = Pulse.Lib.Reference.pts_to i 2 == Pulse.Lib.Reference.pts_to i 0 - - See also WhileInvPreservation.fst(15,4-15,13) + - VC = Prims.l_False + - See also WhileInvPreservation.fst(15,12-15,13) diff --git a/pulse/test/nolib/AdmitDoesNotSimpl.fst.output.expected b/pulse/test/nolib/AdmitDoesNotSimpl.fst.output.expected index 0fae216df43..c17e95c3123 100644 --- a/pulse/test/nolib/AdmitDoesNotSimpl.fst.output.expected +++ b/pulse/test/nolib/AdmitDoesNotSimpl.fst.output.expected @@ -3,20 +3,20 @@ - Current context: foo x - In typing environment: - y#292 : int - x#290 : int + y#294 : int + x#292 : int - goto _return#345 requires foo x + goto _return#347 requires foo x * Info at AdmitDoesNotSimpl.fst(20,2-20,9): - Admitting continuation. - Current context: foo x - In typing environment: - y#292 : int - x#290 : int + y#294 : int + x#292 : int - goto _return#345 requires foo x + goto _return#347 requires foo x * Info at AdmitDoesNotSimpl.fst(27,2-27,9): - Admitting continuation. diff --git a/src/typechecker/FStarC.TypeChecker.Core.fst b/src/typechecker/FStarC.TypeChecker.Core.fst index 8881183b40d..32c351de9df 100644 --- a/src/typechecker/FStarC.TypeChecker.Core.fst +++ b/src/typechecker/FStarC.TypeChecker.Core.fst @@ -1413,7 +1413,7 @@ let rec check_relation' (g:env) (rel:relation) (t0 t1:typ) (fun _ -> // For lambda args, use full check_relation which opens // the lambda and allows unfolding inside the body. - // For non-lambda args, emit guard on original forms. + // For non-lambda args, emit per-arg guard. match (Subst.compress a0).n, (Subst.compress a1).n with | Tm_abs _, Tm_abs _ -> check_relation g EQUALITY a0 a1 diff --git a/tests/error-messages/Monoid.fst.json_output.expected b/tests/error-messages/Monoid.fst.json_output.expected index f75ae2b52d1..bd92256556f 100644 --- a/tests/error-messages/Monoid.fst.json_output.expected +++ b/tests/error-messages/Monoid.fst.json_output.expected @@ -299,8 +299,8 @@ let left_action_morphism f mf la lb = forall (g: ma) (x: a). lb.act (mf g) (f x) Module after type checking: module Monoid Declarations: [ -let right_unitality_lemma m u593 mult = forall (x: m). mult x u593 == x -let left_unitality_lemma m u593 mult = forall (x: m). mult u593 x == x +let right_unitality_lemma m u601 mult = forall (x: m). mult x u601 == x +let left_unitality_lemma m u601 mult = forall (x: m). mult u601 x == x let associativity_lemma m mult = forall (x: m) (y: m) (z: m). mult (mult x y) z == mult x (mult y z) unopteq type monoid (m: Type) = @@ -336,25 +336,25 @@ val monoid__uu___haseq: Prims.l_True /\ -let intro_monoid m u593 mult = Monoid.Monoid u593 mult () () () <: Prims.Pure (Monoid.monoid m) +let intro_monoid m u601 mult = Monoid.Monoid u601 mult () () () <: Prims.Pure (Monoid.monoid m) let nat_plus_monoid = let add x y = x + y <: Prims.nat in Monoid.intro_monoid Prims.nat 0 add let int_plus_monoid = Monoid.intro_monoid Prims.int 0 Prims.op_Addition let conjunction_monoid = - let u591 = FStar.Pervasives.singleton Prims.l_True in + let u599 = FStar.Pervasives.singleton Prims.l_True in let mult p q = p /\ q <: Prims.prop in let left_unitality_helper p = - (assert (mult u591 p <==> p); - FStar.PropositionalExtensionality.apply (mult u591 p) p) + (assert (mult u599 p <==> p); + FStar.PropositionalExtensionality.apply (mult u599 p) p) <: - FStar.Pervasives.Lemma (ensures mult u591 p == p) + FStar.Pervasives.Lemma (ensures mult u599 p == p) in let right_unitality_helper p = - (assert (mult p u591 <==> p); - FStar.PropositionalExtensionality.apply (mult p u591) p) + (assert (mult p u599 <==> p); + FStar.PropositionalExtensionality.apply (mult p u599) p) <: - FStar.Pervasives.Lemma (ensures mult p u591 == p) + FStar.Pervasives.Lemma (ensures mult p u599 == p) in let associativity_helper p1 p2 p3 = (assert (mult (mult p1 p2) p3 <==> mult p1 (mult p2 p3)); @@ -363,26 +363,26 @@ let conjunction_monoid = FStar.Pervasives.Lemma (ensures mult (mult p1 p2) p3 == mult p1 (mult p2 p3)) in FStar.Classical.forall_intro right_unitality_helper; - assert (Monoid.right_unitality_lemma Prims.prop u591 mult); + assert (Monoid.right_unitality_lemma Prims.prop u599 mult); FStar.Classical.forall_intro left_unitality_helper; - assert (Monoid.left_unitality_lemma Prims.prop u591 mult); + assert (Monoid.left_unitality_lemma Prims.prop u599 mult); FStar.Classical.forall_intro_3 associativity_helper; assert (Monoid.associativity_lemma Prims.prop mult); - Monoid.intro_monoid Prims.prop u591 mult + Monoid.intro_monoid Prims.prop u599 mult let disjunction_monoid = - let u591 = FStar.Pervasives.singleton Prims.l_False in + let u599 = FStar.Pervasives.singleton Prims.l_False in let mult p q = p \/ q <: Prims.prop in let left_unitality_helper p = - (assert (mult u591 p <==> p); - FStar.PropositionalExtensionality.apply (mult u591 p) p) + (assert (mult u599 p <==> p); + FStar.PropositionalExtensionality.apply (mult u599 p) p) <: - FStar.Pervasives.Lemma (ensures mult u591 p == p) + FStar.Pervasives.Lemma (ensures mult u599 p == p) in let right_unitality_helper p = - (assert (mult p u591 <==> p); - FStar.PropositionalExtensionality.apply (mult p u591) p) + (assert (mult p u599 <==> p); + FStar.PropositionalExtensionality.apply (mult p u599) p) <: - FStar.Pervasives.Lemma (ensures mult p u591 == p) + FStar.Pervasives.Lemma (ensures mult p u599 == p) in let associativity_helper p1 p2 p3 = (assert (mult (mult p1 p2) p3 <==> mult p1 (mult p2 p3)); @@ -391,12 +391,12 @@ let disjunction_monoid = FStar.Pervasives.Lemma (ensures mult (mult p1 p2) p3 == mult p1 (mult p2 p3)) in FStar.Classical.forall_intro right_unitality_helper; - assert (Monoid.right_unitality_lemma Prims.prop u591 mult); + assert (Monoid.right_unitality_lemma Prims.prop u599 mult); FStar.Classical.forall_intro left_unitality_helper; - assert (Monoid.left_unitality_lemma Prims.prop u591 mult); + assert (Monoid.left_unitality_lemma Prims.prop u599 mult); FStar.Classical.forall_intro_3 associativity_helper; assert (Monoid.associativity_lemma Prims.prop mult); - Monoid.intro_monoid Prims.prop u591 mult + Monoid.intro_monoid Prims.prop u599 mult let bool_and_monoid = let and_ b1 b2 = b1 && b2 in Monoid.intro_monoid Prims.bool true and_ @@ -474,7 +474,7 @@ let _ = Monoid.intro_monoid_morphism Monoid.neg Monoid.disjunction_monoid Monoid.conjunction_monoid let mult_act_lemma m a mult act = forall (x: m) (x': m) (y: a). act (mult x x') y == act x (act x' y) -let unit_act_lemma m a u595 act = forall (y: a). act u595 y == y +let unit_act_lemma m a u603 act = forall (y: a). act u603 y == y unopteq type left_action (mm: Monoid.monoid m) (a: Type) = | LAct : diff --git a/tests/error-messages/Monoid.fst.output.expected b/tests/error-messages/Monoid.fst.output.expected index f75ae2b52d1..bd92256556f 100644 --- a/tests/error-messages/Monoid.fst.output.expected +++ b/tests/error-messages/Monoid.fst.output.expected @@ -299,8 +299,8 @@ let left_action_morphism f mf la lb = forall (g: ma) (x: a). lb.act (mf g) (f x) Module after type checking: module Monoid Declarations: [ -let right_unitality_lemma m u593 mult = forall (x: m). mult x u593 == x -let left_unitality_lemma m u593 mult = forall (x: m). mult u593 x == x +let right_unitality_lemma m u601 mult = forall (x: m). mult x u601 == x +let left_unitality_lemma m u601 mult = forall (x: m). mult u601 x == x let associativity_lemma m mult = forall (x: m) (y: m) (z: m). mult (mult x y) z == mult x (mult y z) unopteq type monoid (m: Type) = @@ -336,25 +336,25 @@ val monoid__uu___haseq: Prims.l_True /\ -let intro_monoid m u593 mult = Monoid.Monoid u593 mult () () () <: Prims.Pure (Monoid.monoid m) +let intro_monoid m u601 mult = Monoid.Monoid u601 mult () () () <: Prims.Pure (Monoid.monoid m) let nat_plus_monoid = let add x y = x + y <: Prims.nat in Monoid.intro_monoid Prims.nat 0 add let int_plus_monoid = Monoid.intro_monoid Prims.int 0 Prims.op_Addition let conjunction_monoid = - let u591 = FStar.Pervasives.singleton Prims.l_True in + let u599 = FStar.Pervasives.singleton Prims.l_True in let mult p q = p /\ q <: Prims.prop in let left_unitality_helper p = - (assert (mult u591 p <==> p); - FStar.PropositionalExtensionality.apply (mult u591 p) p) + (assert (mult u599 p <==> p); + FStar.PropositionalExtensionality.apply (mult u599 p) p) <: - FStar.Pervasives.Lemma (ensures mult u591 p == p) + FStar.Pervasives.Lemma (ensures mult u599 p == p) in let right_unitality_helper p = - (assert (mult p u591 <==> p); - FStar.PropositionalExtensionality.apply (mult p u591) p) + (assert (mult p u599 <==> p); + FStar.PropositionalExtensionality.apply (mult p u599) p) <: - FStar.Pervasives.Lemma (ensures mult p u591 == p) + FStar.Pervasives.Lemma (ensures mult p u599 == p) in let associativity_helper p1 p2 p3 = (assert (mult (mult p1 p2) p3 <==> mult p1 (mult p2 p3)); @@ -363,26 +363,26 @@ let conjunction_monoid = FStar.Pervasives.Lemma (ensures mult (mult p1 p2) p3 == mult p1 (mult p2 p3)) in FStar.Classical.forall_intro right_unitality_helper; - assert (Monoid.right_unitality_lemma Prims.prop u591 mult); + assert (Monoid.right_unitality_lemma Prims.prop u599 mult); FStar.Classical.forall_intro left_unitality_helper; - assert (Monoid.left_unitality_lemma Prims.prop u591 mult); + assert (Monoid.left_unitality_lemma Prims.prop u599 mult); FStar.Classical.forall_intro_3 associativity_helper; assert (Monoid.associativity_lemma Prims.prop mult); - Monoid.intro_monoid Prims.prop u591 mult + Monoid.intro_monoid Prims.prop u599 mult let disjunction_monoid = - let u591 = FStar.Pervasives.singleton Prims.l_False in + let u599 = FStar.Pervasives.singleton Prims.l_False in let mult p q = p \/ q <: Prims.prop in let left_unitality_helper p = - (assert (mult u591 p <==> p); - FStar.PropositionalExtensionality.apply (mult u591 p) p) + (assert (mult u599 p <==> p); + FStar.PropositionalExtensionality.apply (mult u599 p) p) <: - FStar.Pervasives.Lemma (ensures mult u591 p == p) + FStar.Pervasives.Lemma (ensures mult u599 p == p) in let right_unitality_helper p = - (assert (mult p u591 <==> p); - FStar.PropositionalExtensionality.apply (mult p u591) p) + (assert (mult p u599 <==> p); + FStar.PropositionalExtensionality.apply (mult p u599) p) <: - FStar.Pervasives.Lemma (ensures mult p u591 == p) + FStar.Pervasives.Lemma (ensures mult p u599 == p) in let associativity_helper p1 p2 p3 = (assert (mult (mult p1 p2) p3 <==> mult p1 (mult p2 p3)); @@ -391,12 +391,12 @@ let disjunction_monoid = FStar.Pervasives.Lemma (ensures mult (mult p1 p2) p3 == mult p1 (mult p2 p3)) in FStar.Classical.forall_intro right_unitality_helper; - assert (Monoid.right_unitality_lemma Prims.prop u591 mult); + assert (Monoid.right_unitality_lemma Prims.prop u599 mult); FStar.Classical.forall_intro left_unitality_helper; - assert (Monoid.left_unitality_lemma Prims.prop u591 mult); + assert (Monoid.left_unitality_lemma Prims.prop u599 mult); FStar.Classical.forall_intro_3 associativity_helper; assert (Monoid.associativity_lemma Prims.prop mult); - Monoid.intro_monoid Prims.prop u591 mult + Monoid.intro_monoid Prims.prop u599 mult let bool_and_monoid = let and_ b1 b2 = b1 && b2 in Monoid.intro_monoid Prims.bool true and_ @@ -474,7 +474,7 @@ let _ = Monoid.intro_monoid_morphism Monoid.neg Monoid.disjunction_monoid Monoid.conjunction_monoid let mult_act_lemma m a mult act = forall (x: m) (x': m) (y: a). act (mult x x') y == act x (act x' y) -let unit_act_lemma m a u595 act = forall (y: a). act u595 y == y +let unit_act_lemma m a u603 act = forall (y: a). act u603 y == y unopteq type left_action (mm: Monoid.monoid m) (a: Type) = | LAct : diff --git a/tests/error-messages/QuickTest.fst.json_output.expected b/tests/error-messages/QuickTest.fst.json_output.expected index 1ce18c940a4..841cbf47f12 100644 --- a/tests/error-messages/QuickTest.fst.json_output.expected +++ b/tests/error-messages/QuickTest.fst.json_output.expected @@ -1 +1 @@ -{"msg":["Expected failure:","","The SMT solver could not prove the query.","Env = (va_s0 : QuickTest.vale_state)","VC =\n forall (ok: Prims.bool).\n (forall (p: (_: Prims.unit -> Prims.GTot Prims.prop)).\n (forall (u179: Prims.unit). {:pattern Prims.guard_free (p u179)} p ()) ==>\n FStar.Range.labeled (FStar.Sealed.seal QuickTest(1,2-3,4))\n \"\"\n (QuickTest.f 4 - QuickTest.f 4 == 0 /\\ QuickTest.f 4 == 0 /\\\n (forall (pure_result: Prims.unit).\n (forall (i: Prims.int). {:pattern QuickTest.f i}\n QuickTest.f i > 0) ==>\n p pure_result)))\n <:\n Prims.prop","Also see: QuickTest(1,2-3,4)","Other related locations: QuickTest.fst(116,12-116,20)"],"level":"Info","range":{"def":{"file_name":"QuickTest.fst","start_pos":{"line":131,"col":2},"end_pos":{"line":134,"col":34}},"use":{"file_name":"QuickTest.fst","start_pos":{"line":131,"col":2},"end_pos":{"line":134,"col":34}}},"number":19,"ctx":["While typechecking the top-level declaration `let va_lemma_Test2`","While typechecking the top-level declaration `[@@expect_failure] let va_lemma_Test2`"]} +{"msg":["Expected failure:","","The SMT solver could not prove the query.","Env = (va_s0 : QuickTest.vale_state)","VC =\n forall (ok: Prims.bool).\n (forall (p: (_: Prims.unit -> Prims.GTot Prims.prop)).\n (forall (u180: Prims.unit). {:pattern Prims.guard_free (p u180)} p ()) ==>\n FStar.Range.labeled (FStar.Sealed.seal QuickTest(1,2-3,4))\n \"\"\n (QuickTest.f 4 - QuickTest.f 4 == 0 /\\ QuickTest.f 4 == 0 /\\\n (forall (pure_result: Prims.unit).\n (forall (i: Prims.int). {:pattern QuickTest.f i}\n QuickTest.f i > 0) ==>\n p pure_result)))\n <:\n Prims.prop","Also see: QuickTest(1,2-3,4)","Other related locations: QuickTest.fst(116,12-116,20)"],"level":"Info","range":{"def":{"file_name":"QuickTest.fst","start_pos":{"line":131,"col":2},"end_pos":{"line":134,"col":34}},"use":{"file_name":"QuickTest.fst","start_pos":{"line":131,"col":2},"end_pos":{"line":134,"col":34}}},"number":19,"ctx":["While typechecking the top-level declaration `let va_lemma_Test2`","While typechecking the top-level declaration `[@@expect_failure] let va_lemma_Test2`"]} diff --git a/tests/error-messages/QuickTest.fst.output.expected b/tests/error-messages/QuickTest.fst.output.expected index 9bca78e46ec..6859465a6a2 100644 --- a/tests/error-messages/QuickTest.fst.output.expected +++ b/tests/error-messages/QuickTest.fst.output.expected @@ -5,7 +5,7 @@ - VC = forall (ok: Prims.bool). (forall (p: (_: Prims.unit -> Prims.GTot Prims.prop)). - (forall (u179: Prims.unit). {:pattern Prims.guard_free (p u179)} + (forall (u180: Prims.unit). {:pattern Prims.guard_free (p u180)} p ()) ==> FStar.Range.labeled (FStar.Sealed.seal QuickTest(1,2-3,4)) "" diff --git a/tests/error-messages/QuickTestNBE.fst.json_output.expected b/tests/error-messages/QuickTestNBE.fst.json_output.expected index a2040b3aa71..3d103eed164 100644 --- a/tests/error-messages/QuickTestNBE.fst.json_output.expected +++ b/tests/error-messages/QuickTestNBE.fst.json_output.expected @@ -1 +1 @@ -{"msg":["Expected failure:","","The SMT solver could not prove the query.","Env = (va_s0 : QuickTestNBE.vale_state)","VC =\n forall (ok: Prims.bool) (p: (_: Prims.unit -> Prims.GTot Prims.prop)).\n (forall (u193: Prims.unit). {:pattern Prims.guard_free (p u193)} p ()) ==>\n FStar.Range.labeled (FStar.Sealed.seal QuickTestNBE(1,2-3,4))\n \"\"\n (QuickTestNBE.f 4 - QuickTestNBE.f 4 == 0 /\\ QuickTestNBE.f 4 == 0 /\\\n (forall (pure_result: Prims.unit).\n (forall (i: Prims.int). {:pattern QuickTestNBE.f i}\n QuickTestNBE.f i > 0) ==>\n p pure_result))","Also see: QuickTestNBE(1,2-3,4)","Other related locations: QuickTestNBE.fst(116,16-116,18)"],"level":"Info","range":{"def":{"file_name":"QuickTestNBE.fst","start_pos":{"line":131,"col":2},"end_pos":{"line":134,"col":34}},"use":{"file_name":"QuickTestNBE.fst","start_pos":{"line":131,"col":2},"end_pos":{"line":134,"col":34}}},"number":19,"ctx":["While typechecking the top-level declaration `let va_lemma_Test2`","While typechecking the top-level declaration `[@@expect_failure] let va_lemma_Test2`"]} +{"msg":["Expected failure:","","The SMT solver could not prove the query.","Env = (va_s0 : QuickTestNBE.vale_state)","VC =\n forall (ok: Prims.bool) (p: (_: Prims.unit -> Prims.GTot Prims.prop)).\n (forall (u194: Prims.unit). {:pattern Prims.guard_free (p u194)} p ()) ==>\n FStar.Range.labeled (FStar.Sealed.seal QuickTestNBE(1,2-3,4))\n \"\"\n (QuickTestNBE.f 4 - QuickTestNBE.f 4 == 0 /\\ QuickTestNBE.f 4 == 0 /\\\n (forall (pure_result: Prims.unit).\n (forall (i: Prims.int). {:pattern QuickTestNBE.f i}\n QuickTestNBE.f i > 0) ==>\n p pure_result))","Also see: QuickTestNBE(1,2-3,4)","Other related locations: QuickTestNBE.fst(116,16-116,18)"],"level":"Info","range":{"def":{"file_name":"QuickTestNBE.fst","start_pos":{"line":131,"col":2},"end_pos":{"line":134,"col":34}},"use":{"file_name":"QuickTestNBE.fst","start_pos":{"line":131,"col":2},"end_pos":{"line":134,"col":34}}},"number":19,"ctx":["While typechecking the top-level declaration `let va_lemma_Test2`","While typechecking the top-level declaration `[@@expect_failure] let va_lemma_Test2`"]} diff --git a/tests/error-messages/QuickTestNBE.fst.output.expected b/tests/error-messages/QuickTestNBE.fst.output.expected index 60959a7b5e5..9dafe4a3c0f 100644 --- a/tests/error-messages/QuickTestNBE.fst.output.expected +++ b/tests/error-messages/QuickTestNBE.fst.output.expected @@ -4,7 +4,7 @@ - Env = (va_s0 : QuickTestNBE.vale_state) - VC = forall (ok: Prims.bool) (p: (_: Prims.unit -> Prims.GTot Prims.prop)). - (forall (u193: Prims.unit). {:pattern Prims.guard_free (p u193)} p ()) ==> + (forall (u194: Prims.unit). {:pattern Prims.guard_free (p u194)} p ()) ==> FStar.Range.labeled (FStar.Sealed.seal QuickTestNBE(1,2-3,4)) "" (QuickTestNBE.f 4 - QuickTestNBE.f 4 == 0 /\ QuickTestNBE.f 4 == 0 /\ diff --git a/tests/tactics/Postprocess.fst.output.expected b/tests/tactics/Postprocess.fst.output.expected index bbdd27ca9ae..868e2d03312 100644 --- a/tests/tactics/Postprocess.fst.output.expected +++ b/tests/tactics/Postprocess.fst.output.expected @@ -414,9 +414,9 @@ visible let xx : t1 = (C1 (fun uu___0 -> (match uu___0@0:(Tm_unknown) with [@ ] visible let q_as_lem : (p:(squash (l_Forall (fun x -> (b@1:(Tm_unknown) x@0:(Tm_unknown))))) -> x:a@2:(Tm_unknown) -> Lemma (unit)) = (fun p x -> ()) [@ ] -visible let congruence_fun : (f:(x:a@1:(Tm_unknown) -> Tot (b@1:(Tm_unknown) x@0:(Tm_unknown))) -> g:(x:a@2:(Tm_unknown) -> Tot (b@2:(Tm_unknown) x@0:(Tm_unknown))) -> x:(squash (l_Forall (fun x -> (eq2 (f@2:(Tm_unknown) x@0:(Tm_unknown)) (g@1:(Tm_unknown) x@0:(Tm_unknown)))))) -> Lemma (unit)) = (fun f g x -> (assert_by_tactic (eq2 (fun x -> (f@3:(Tm_unknown) x@0:(Tm_unknown))) (fun x -> (g@2:(Tm_unknown) x@0:(Tm_unknown)))) (fun uu___ -> let [@ (inline_let)]uu___#3324 : unit = () +visible let congruence_fun : (f:(x:a@1:(Tm_unknown) -> Tot (b@1:(Tm_unknown) x@0:(Tm_unknown))) -> g:(x:a@2:(Tm_unknown) -> Tot (b@2:(Tm_unknown) x@0:(Tm_unknown))) -> x:(squash (l_Forall (fun x -> (eq2 (f@2:(Tm_unknown) x@0:(Tm_unknown)) (g@1:(Tm_unknown) x@0:(Tm_unknown)))))) -> Lemma (unit)) = (fun f g x -> (assert_by_tactic (eq2 (fun x -> (f@3:(Tm_unknown) x@0:(Tm_unknown))) (fun x -> (g@2:(Tm_unknown) x@0:(Tm_unknown)))) (fun uu___ -> let [@ (inline_let)]uu___#3510 : unit = () in -let uu___#3325 : unit = let uu___#3326 : (list term) = let uu___#3327 : term = quote ((q_as_lem x@2:(Tm_unknown))) +let uu___#3511 : unit = let uu___#3512 : (list term) = let uu___#3513 : term = quote ((q_as_lem x@2:(Tm_unknown))) in (Cons uu___@0:(Tm_unknown) (Nil )) in @@ -438,56 +438,56 @@ visible let _onL : (a:uu___@0:(Tm_unknown) -> b:uu___@1:(Tm_unknown) -> c:uu__ [@ ] visible let onL : (uu___:unit -> Tac (unit)) = (fun uu___ -> (apply_lemma `(_onL)[])) [@ ] -visible let rec push_lifts' : (u:unit -> Tac (unit)) = (fun u -> let uu___#21873 : formula = let uu___#21874 : term = (cur_goal ()) +visible let rec push_lifts' : (u:unit -> Tac (unit)) = (fun u -> let uu___#21880 : formula = let uu___#21881 : term = (cur_goal ()) in (term_as_formula uu___@0:(Tm_unknown)) in (match uu___@0:(Tm_unknown) with - | (Comp (Eq uu___#21875) lhs#21876 rhs#21877) -> let uu___#21878 : named_term_view = (inspect lhs@1:(Tm_unknown)) + | (Comp (Eq uu___#21882) lhs#21883 rhs#21884) -> let uu___#21885 : named_term_view = (inspect lhs@1:(Tm_unknown)) in (match uu___@0:(Tm_unknown) with - | (Tv_App h#21879 t#21880) -> let uu___#21881 : named_term_view = (inspect h@1:(Tm_unknown)) + | (Tv_App h#21886 t#21887) -> let uu___#21888 : named_term_view = (inspect h@1:(Tm_unknown)) in (match uu___@0:(Tm_unknown) with - | (Tv_FVar fv#21882) -> (match (op_Equality (fv_to_string fv@0:(Tm_unknown)) "Postprocess.lift") with + | (Tv_FVar fv#21889) -> (match (op_Equality (fv_to_string fv@0:(Tm_unknown)) "Postprocess.lift") with | true -> (case_analyze (fst t@2:(Tm_unknown))) - |uu___#21883 -> (fail "not a lift (1)")) - |uu___#21884 -> (fail "not a lift (2)")) - |(Tv_Abs uu___#21885 uu___#21886) -> let uu___#21887 : unit = (fext ()) + |uu___#21890 -> (fail "not a lift (1)")) + |uu___#21891 -> (fail "not a lift (2)")) + |(Tv_Abs uu___#21892 uu___#21893) -> let uu___#21894 : unit = (fext ()) in (push_lifts' ()) - |uu___#21888 -> (fail "not a lift (3)")) - |uu___#21889 -> (fail "not an equality"))) - and case_analyze : (lhs:term -> Tac (unit)) = (fun lhs -> let ap#21892 : (l:term -> Tac (unit)) = (fun l -> let uu___#21896 : unit = (onL ()) + |uu___#21895 -> (fail "not a lift (3)")) + |uu___#21896 -> (fail "not an equality"))) + and case_analyze : (lhs:term -> Tac (unit)) = (fun lhs -> let ap#21899 : (l:term -> Tac (unit)) = (fun l -> let uu___#21903 : unit = (onL ()) in (apply_lemma l@1:(Tm_unknown))) in -let lhs#21897 : term = (norm_term (Cons weak (Cons hnf (Cons primops (Cons delta (Nil ))))) lhs@1:(Tm_unknown)) +let lhs#21904 : term = (norm_term (Cons weak (Cons hnf (Cons primops (Cons delta (Nil ))))) lhs@1:(Tm_unknown)) in -let uu___#21898 : (tuple2 term (list argv)) = (collect_app lhs@0:(Tm_unknown)) +let uu___#21905 : (tuple2 term (list argv)) = (collect_app lhs@0:(Tm_unknown)) in (match uu___@0:(Tm_unknown) with - | (Mktuple2 #._ #._ head#21899 args#21900) -> let uu___#21901 : named_term_view = (inspect head@1:(Tm_unknown)) + | (Mktuple2 #._ #._ head#21906 args#21907) -> let uu___#21908 : named_term_view = (inspect head@1:(Tm_unknown)) in (match uu___@0:(Tm_unknown) with - | (Tv_FVar fv#21902) -> (match (op_Equality (fv_to_string fv@0:(Tm_unknown)) "Postprocess.A1") with + | (Tv_FVar fv#21909) -> (match (op_Equality (fv_to_string fv@0:(Tm_unknown)) "Postprocess.A1") with | true -> (apply_lemma `(lemA)[]) - |uu___#21903 -> (match (op_Equality (fv_to_string fv@1:(Tm_unknown)) "Postprocess.B1") with - | true -> let uu___#21904 : unit = (ap@7:(Tm_unknown) `(lemB)[]) + |uu___#21910 -> (match (op_Equality (fv_to_string fv@1:(Tm_unknown)) "Postprocess.B1") with + | true -> let uu___#21911 : unit = (ap@7:(Tm_unknown) `(lemB)[]) in -let uu___#21905 : unit = (apply_lemma `(congB)[]) +let uu___#21912 : unit = (apply_lemma `(congB)[]) in (push_lifts' ()) - |uu___#21906 -> (match (op_Equality (fv_to_string fv@2:(Tm_unknown)) "Postprocess.C1") with - | true -> let uu___#21907 : unit = (ap@8:(Tm_unknown) `(lemC)[]) + |uu___#21913 -> (match (op_Equality (fv_to_string fv@2:(Tm_unknown)) "Postprocess.C1") with + | true -> let uu___#21914 : unit = (ap@8:(Tm_unknown) `(lemC)[]) in -let uu___#21908 : unit = (apply_lemma `(congC)[]) +let uu___#21915 : unit = (apply_lemma `(congC)[]) in (push_lifts' ()) - |uu___#21909 -> let uu___#21910 : unit = (tlabel "unknown fv") + |uu___#21916 -> let uu___#21917 : unit = (tlabel "unknown fv") in (trefl ())))) - |uu___#21911 -> let uu___#21912 : unit = (tlabel "head unk") + |uu___#21918 -> let uu___#21919 : unit = (tlabel "head unk") in (trefl ())))) [@ ] @@ -498,7 +498,7 @@ in visible let yy : t2 = (C2 (fun x -> (lift (match x@0:(Tm_unknown) with | 0 -> A1 |5 -> (B1 42) - |x#263 -> (B1 24))))) + |x#285 -> (B1 24))))) [@ ] visible let zz1 : t2 = (C2 (fun x -> (C2 (fun x -> A2)))) [@ ((postprocess_for_extraction_with push_lifts))] From 83ebc36d00b19ebbe96c6d0ec7e56ddb53677a31 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Tue, 26 May 2026 21:43:32 -0700 Subject: [PATCH 16/24] simplify logic of check_relation when heads match --- src/typechecker/FStarC.TypeChecker.Core.fst | 156 +++++++++----------- 1 file changed, 66 insertions(+), 90 deletions(-) diff --git a/src/typechecker/FStarC.TypeChecker.Core.fst b/src/typechecker/FStarC.TypeChecker.Core.fst index 32c351de9df..755ba8dc6d5 100644 --- a/src/typechecker/FStarC.TypeChecker.Core.fst +++ b/src/typechecker/FStarC.TypeChecker.Core.fst @@ -1334,105 +1334,81 @@ let rec check_relation' (g:env) (rel:relation) (t0 t1:typ) if not (head_matches && List.length args0 = List.length args1) then maybe_unfold_and_retry t0 t1 else ( - (* If we're proving equality, SMT queries are ok, and either head - is equatable: - - first try proving equality structurally, without a guard. - - if that fails, then emit an SMT query - This is designed to be able to prove things like `v.v1 == u.v1` - first by trying to unify `v` and `u` and if it fails - then prove `v.v1 == u.v1` *) let structural () = check_relation g EQUALITY head0 head1 ;! check_relation_args g EQUALITY args0 args1 in - let compare_head_and_args () = - handle_with - //cf. Issue 4239 - //First try structural comparison without SMT guards. - //This handles cases where args are definitionally equal. - (no_guard (structural ())) - (fun _ -> - //If structural fails, try unfolding the type abbreviation. - if! unfolding_ok then ( - match maybe_unfold_side Both t0 t1 with - | None -> - //Can't unfold: fall back to structural with guards - if! guard_not_allowed - then err "structural check fails, guards not allowed, and cannot unfold further" - else structural () - | Some (t0', t1') -> - //Check if unfolding exposes a refinement type. - //If so, the refinement comparison produces properly - //weakened guards (e.g., natlt i <: natlt n gives - //forall x. x < i ==> x < n, not i == n). - let t0' = beta_iota_reduce t0' in - let t1' = beta_iota_reduce t1' in - match (Subst.compress t0').n, (Subst.compress t1').n with - | Tm_refine _, _ | _, Tm_refine _ -> - check_relation g rel t0' t1' + //For injective heads: compare each arg independently. + // 1. Try no_guard first (handles definitionally equal args) + // 2. For lambda args: use full check_relation (opens lambdas, + // allows unfolding inside the body, produces ∀-quantified guards) + // 3. For non-lambda args: emit_guard on original arg pair + let injective_args () = + check_relation g EQUALITY head0 head1 ;! + if List.length args0 = List.length args1 + then iter2 args0 args1 + (fun (a0, q0) (a1, q1) _ -> + check_aqual q0 q1;! + handle_with + (no_guard (check_relation g EQUALITY a0 a1)) + (fun _ -> + match (Subst.compress a0).n, (Subst.compress a1).n with + | Tm_abs _, Tm_abs _ -> + check_relation g EQUALITY a0 a1 | _ -> - if! guard_not_allowed then - check_relation g rel t0' t1' - else - //Not a refinement: try three fallbacks in order. - //1. Unfolded without guards (handles structurally equal - // after unfolding). - //2. Structural with guards (handles equatable args like - // variables, producing simple arg-level guards for - // e.g. slprop type abbreviations). - //3. Unfolded with guards (handles non-equatable args - // like constants, where unfolding may expose equatable - // functions like op_Equality). - handle_with - (no_guard (check_relation g rel t0' t1')) - (fun _ -> check_relation g rel t0' t1') - ) else structural ()) + emit_guard a0 a1)) + () + else fail_str "Unequal number of arguments" + in + //For non-injective heads: try unfolding both sides and recurse. + //If unfolding exposes a refinement, the refinement comparison + //produces properly weakened guards (e.g., natlt i <: natlt n gives + //forall x. x < i ==> x < n, not i == n). + //If unfolding fails or is not allowed, fall back to structural. + let unfold_both_and_retry () = + if! unfolding_ok then ( + match maybe_unfold_side Both t0 t1 with + | None -> + //Can't unfold: fall back to structural with guards + if! guard_not_allowed + then err "structural check fails, guards not allowed, and cannot unfold further" + else structural () + | Some (t0', t1') -> + let t0' = beta_iota_reduce t0' in + let t1' = beta_iota_reduce t1' in + check_relation g rel t0' t1' + ) else ( + //Unfolding not allowed: fall back to structural with guards + if! guard_not_allowed + then err "structural check fails, guards not allowed, and unfolding not allowed" + else structural () + ) in - if is_marked_injective g.tcenv head0 - then ( - // For injective heads: first try structural without guard. - // If that fails and guards are allowed, compare each arg: - // 1. Try no_guard first (handles definitionally equal args) - // 2. For lambda args: use full check_relation (opens lambdas, - // allows unfolding inside the body, produces ∀-quantified guards) - // 3. For non-lambda args: emit_guard on original arg pair (avoids - // deeply unfolding into forms SMT can't handle) - handle_with - (no_guard (structural ())) - (fun _ -> + //Main logic: + //1. Always try no_guard(structural) first. + //2. If that fails: + // - injective head: per-arg comparison + // - non-injective head: unfold_both_and_retry + //3. If unfold_both_and_retry fails and equatable: emit_guard + handle_with + (no_guard (structural ())) + (fun _ -> + if is_marked_injective g.tcenv head0 + then ( if not guard_ok then err "injective head: structural check fails and guards not allowed" - else ( - check_relation g EQUALITY head0 head1 ;! - if List.length args0 = List.length args1 - then iter2 args0 args1 - (fun (a0, q0) (a1, q1) _ -> - check_aqual q0 q1;! - handle_with - (no_guard (check_relation g EQUALITY a0 a1)) - (fun _ -> - // For lambda args, use full check_relation which opens - // the lambda and allows unfolding inside the body. - // For non-lambda args, emit per-arg guard. - match (Subst.compress a0).n, (Subst.compress a1).n with - | Tm_abs _, Tm_abs _ -> - check_relation g EQUALITY a0 a1 - | _ -> - emit_guard a0 a1)) - () - else fail_str "Unequal number of arguments" - ) + else injective_args () ) - ) - else if guard_ok && - (rel=EQUALITY) && - (equatable g t0 || equatable g t1) - then ( - handle_with - (no_guard (compare_head_and_args ())) - (fun _ -> emit_guard t0 t1) - ) - else compare_head_and_args () + else if guard_ok && + (rel=EQUALITY) && + (equatable g t0 || equatable g t1) + then ( + handle_with + (no_guard (unfold_both_and_retry ())) + (fun _ -> emit_guard t0 t1) + ) + else unfold_both_and_retry () + ) ) | Tm_abs {bs=b0::b1::bs; body; rc_opt=ropt}, _ -> From 87f95fea0065c1bba289c5c07a5fb016df6cecbf Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Tue, 26 May 2026 22:08:31 -0700 Subject: [PATCH 17/24] rlimit bump --- pulse/lib/pulse/lib/Pulse.Lib.Swap.Spec.fst | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/pulse/lib/pulse/lib/Pulse.Lib.Swap.Spec.fst b/pulse/lib/pulse/lib/Pulse.Lib.Swap.Spec.fst index b77003b278a..c2a44977833 100644 --- a/pulse/lib/pulse/lib/Pulse.Lib.Swap.Spec.fst +++ b/pulse/lib/pulse/lib/Pulse.Lib.Swap.Spec.fst @@ -671,6 +671,9 @@ let array_swap_inner_invariant Seq.index s idx == Seq.index s0 (if i' < i || (i' = i && j' < j) then jump (n) (l) idx else idx) ) +#restart-solver +#push-options "--z3rlimit 10" + let array_swap_inner_invariant_end (#t: Type) (n: nat) @@ -693,6 +696,8 @@ let array_swap_inner_invariant_end // [SMTPat (array_swap_inner_invariant s0 n l bz s i j idx)] = () +#pop-options + module SZ = FStar.SizeT let sz_rem_spec From 487c96527731c4199118e9f6c4117054c6bce28e Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Wed, 27 May 2026 07:23:35 -0700 Subject: [PATCH 18/24] update expected output (gensym changes) for a new test --- tests/bug-reports/closed/Bug4274.fst.output.expected | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/bug-reports/closed/Bug4274.fst.output.expected b/tests/bug-reports/closed/Bug4274.fst.output.expected index 018389302a3..edef45e5665 100644 --- a/tests/bug-reports/closed/Bug4274.fst.output.expected +++ b/tests/bug-reports/closed/Bug4274.fst.output.expected @@ -3,8 +3,8 @@ - Current context: foo_pred x (Mkfoo_spec 10 10 vx.z' vx.z'') - In typing environment: - __#512 : squash (rewrites_to_p __anf0 10) - __anf0#511 : int + __#514 : squash (rewrites_to_p __anf0 10) + __anf0#513 : int vx#282 : erased foo_spec x#278 : foo From 0f0ceb2d924d69aa6c34b933258b1fa4a20d6dbe Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Wed, 27 May 2026 09:06:04 -0700 Subject: [PATCH 19/24] exists* does not need to opt-out of injectivity --- pulse/lib/common/Pulse.Lib.Core.fsti | 1 - 1 file changed, 1 deletion(-) diff --git a/pulse/lib/common/Pulse.Lib.Core.fsti b/pulse/lib/common/Pulse.Lib.Core.fsti index 74da5118017..e52e3e3d18c 100644 --- a/pulse/lib/common/Pulse.Lib.Core.fsti +++ b/pulse/lib/common/Pulse.Lib.Core.fsti @@ -93,7 +93,6 @@ val timeless_star (p q : slprop) (ensures timeless (p ** q)) [SMTPat (timeless (p ** q))] -[@@unifier_hint_not_injective] val ( exists* ) (#a:Type) (p:a -> slprop) : slprop val timeless_exists (#a:Type u#a) (p: a -> slprop) From a2ffaeb3562d7c6de77e05fde13f09eaa8d49d08 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Fri, 29 May 2026 11:03:37 -0700 Subject: [PATCH 20/24] Core: equatable return type approach for slprop functions 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> --- pulse/lib/common/Pulse.Lib.Core.fsti | 2 - pulse/test/bug-reports/Bug110.fst | 2 +- src/typechecker/FStarC.TypeChecker.Core.fst | 81 ++++++++++++++------- 3 files changed, 55 insertions(+), 30 deletions(-) diff --git a/pulse/lib/common/Pulse.Lib.Core.fsti b/pulse/lib/common/Pulse.Lib.Core.fsti index e52e3e3d18c..77d1caaadcd 100644 --- a/pulse/lib/common/Pulse.Lib.Core.fsti +++ b/pulse/lib/common/Pulse.Lib.Core.fsti @@ -84,7 +84,6 @@ val timeless_pure (p:prop) : Lemma (timeless (pure p)) [SMTPat (timeless (pure p))] -[@@unifier_hint_not_injective] val ( ** ) (p q:slprop) : slprop val timeless_star (p q : slprop) @@ -460,7 +459,6 @@ val loc_get () : stt_ghost loc_id emp_inames emp (fun l -> loc l) val loc_dup l : stt_ghost unit emp_inames (loc l) (fun _ -> loc l ** loc l) val loc_gather l #l' : stt_ghost unit emp_inames (loc l ** loc l') (fun _ -> loc l ** pure (l == l')) -[@@unifier_hint_not_injective] val on (l:loc_id) ([@@@mkey] p:slprop) : slprop val on_intro #l p : stt_ghost unit emp_inames (loc l ** p) (fun _ -> loc l ** on l p) val on_elim #l p : stt_ghost unit emp_inames (loc l ** on l p) (fun _ -> loc l ** p) diff --git a/pulse/test/bug-reports/Bug110.fst b/pulse/test/bug-reports/Bug110.fst index 7fe53e3dbaa..8509f16ca27 100644 --- a/pulse/test/bug-reports/Bug110.fst +++ b/pulse/test/bug-reports/Bug110.fst @@ -3,7 +3,7 @@ module Bug110 #lang-pulse open Pulse -[@@no_mkeys; unifier_hint_not_injective] assume val foo : int -> slprop +[@@no_mkeys] assume val foo : int -> slprop (* OK *) fn test1 (i j : int) diff --git a/src/typechecker/FStarC.TypeChecker.Core.fst b/src/typechecker/FStarC.TypeChecker.Core.fst index 755ba8dc6d5..81e84ce4c85 100644 --- a/src/typechecker/FStarC.TypeChecker.Core.fst +++ b/src/typechecker/FStarC.TypeChecker.Core.fst @@ -1033,28 +1033,29 @@ let maybe_relate_after_unfolding (g:Env.env) t0 t1 : ML side = let is_marked_injective env t = match (U.un_uinst t).n with | Tm_fvar fv -> - // Explicit injective attribute always wins - if Env.fv_has_attr env fv PC.unifier_hint_injective_lid then true - // Explicit opt-out always wins - else if Env.fv_has_attr env fv PC.unifier_hint_not_injective_lid then false - // Check if the function is Delta_equational (match/if-based) - // Such functions should NOT be treated as injective since equality - // may hold by case analysis, not by argument equality. - else ( - match Env.delta_depth_of_fv env fv with - | S.Delta_equational_at_level _ -> false - | _ -> - // Check if return type has injective_type attribute - (match Env.try_lookup_lid env fv.fv_name with - | Some ((_, typ), _) -> - let _, ret_typ = U.arrow_formals typ in - let ret_head, _ = U.head_and_args ret_typ in - (match (U.un_uinst ret_head).n with - | Tm_fvar ret_fv -> - Env.fv_has_attr env ret_fv PC.unifier_hint_injective_type_lid - | _ -> false) - | _ -> false) - ) + // Only explicit [@@unifier_hint_injective] counts + Env.fv_has_attr env fv PC.unifier_hint_injective_lid + | _ -> false + +// Check if a function head returns a type marked with [@@unifier_hint_injective_type]. +// Such functions get equatable treatment: if structural comparison fails, +// we emit a full application guard (or open lambdas if only lambda args differ). +// Excludes Delta_equational heads (match/if-based) since those should be unfolded. +let returns_equatable_type env t = + match (U.un_uinst t).n with + | Tm_fvar fv -> + (match Env.delta_depth_of_fv env fv with + | S.Delta_equational_at_level _ -> false + | _ -> + (match Env.try_lookup_lid env fv.fv_name with + | Some ((_, typ), _) -> + let _, ret_typ = U.arrow_formals typ in + let ret_head, _ = U.head_and_args ret_typ in + (match (U.un_uinst ret_head).n with + | Tm_fvar ret_fv -> + Env.fv_has_attr env ret_fv PC.unifier_hint_injective_type_lid + | _ -> false) + | _ -> false)) | _ -> false instance showable_rel : showable relation = { @@ -1387,9 +1388,11 @@ let rec check_relation' (g:env) (rel:relation) (t0 t1:typ) //Main logic: //1. Always try no_guard(structural) first. //2. If that fails: - // - injective head: per-arg comparison - // - non-injective head: unfold_both_and_retry - //3. If unfold_both_and_retry fails and equatable: emit_guard + // - explicitly injective head: per-arg comparison + // - returns equatable type: if only lambda args differ, open them; + // otherwise emit full application guard + // - equatable head (Delta_abstract etc.): same as equatable type + // - otherwise: unfold_both_and_retry handle_with (no_guard (structural ())) (fun _ -> @@ -1401,11 +1404,35 @@ let rec check_relation' (g:env) (rel:relation) (t0 t1:typ) ) else if guard_ok && (rel=EQUALITY) && - (equatable g t0 || equatable g t1) + (equatable g t0 || equatable g t1 || + returns_equatable_type g.tcenv head0) then ( handle_with (no_guard (unfold_both_and_retry ())) - (fun _ -> emit_guard t0 t1) + (fun _ -> + //Per-arg comparison with full application guard fallback: + //For each arg pair: + // - if no_guard(check_relation) succeeds, the arg is equal + // - if both are lambdas, use check_relation (may emit guard) + // - otherwise, bail to full application emit_guard + if List.length args0 <> List.length args1 + then emit_guard t0 t1 + else + handle_with + (check_relation g EQUALITY head0 head1 ;! + iter2 args0 args1 + (fun (a0, q0) (a1, q1) _ -> + check_aqual q0 q1;! + handle_with + (no_guard (check_relation g EQUALITY a0 a1)) + (fun _ -> + match (Subst.compress a0).n, (Subst.compress a1).n with + | Tm_abs _, Tm_abs _ -> + check_relation g EQUALITY a0 a1 + | _ -> + err "equatable: non-lambda arg differs")) + ()) + (fun _ -> emit_guard t0 t1)) ) else unfold_both_and_retry () ) From ae635a48f999e897c8c4edc87a3063946bd2c3fc Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Tue, 2 Jun 2026 08:46:12 -0700 Subject: [PATCH 21/24] Core: reduce stuck Tm_match terms before giving up MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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> --- pulse/test/bug-reports/Bug4239Variant.fst | 40 +++++++++++++++++++++ src/typechecker/FStarC.TypeChecker.Core.fst | 23 +++++++++++- 2 files changed, 62 insertions(+), 1 deletion(-) create mode 100644 pulse/test/bug-reports/Bug4239Variant.fst diff --git a/pulse/test/bug-reports/Bug4239Variant.fst b/pulse/test/bug-reports/Bug4239Variant.fst new file mode 100644 index 00000000000..cadb92974cb --- /dev/null +++ b/pulse/test/bug-reports/Bug4239Variant.fst @@ -0,0 +1,40 @@ +module Bug4239Variant + +#lang-pulse +open Pulse +module FE = FStar.FunctionalExtensionality + +assume val rel : Type0 -> Type0 -> Type0 +let type_spec (impl_elt: Type0) = dtuple2 Type0 (rel impl_elt) + +let mk_spec + (#impl_elt: Type0) + (#src_elt: Type0) + (r: rel impl_elt src_elt) +: Tot (Ghost.erased (type_spec impl_elt)) += Ghost.hide (| _, r |) + +let eq_test_for (#t: Type) (x1: t) : Type = + FE.restricted_t t (fun x2 -> (y: bool { y == true <==> x1 == x2 })) + +let eq_test (t: Type) : Type = + FE.restricted_t t (fun x1 -> eq_test_for x1) + +let mk_iterator + (#tkey: Type0) + (key_eq: Ghost.erased (eq_test tkey)) + (#ikey: Type0) + (#r1: rel ikey tkey) += + let kk : Ghost.erased (eq_test (dfst (mk_spec r1))) = key_eq in + () + +fn mk_iterator2 + (#tkey: Type0) + (key_eq: Ghost.erased (eq_test tkey)) + (#ikey: Type0) + (#r1: rel ikey tkey) +{ + let kk : Ghost.erased (eq_test (dfst (mk_spec r1))) = key_eq; + () +} \ No newline at end of file diff --git a/src/typechecker/FStarC.TypeChecker.Core.fst b/src/typechecker/FStarC.TypeChecker.Core.fst index 81e84ce4c85..b1b0109c674 100644 --- a/src/typechecker/FStarC.TypeChecker.Core.fst +++ b/src/typechecker/FStarC.TypeChecker.Core.fst @@ -1033,7 +1033,6 @@ let maybe_relate_after_unfolding (g:Env.env) t0 t1 : ML side = let is_marked_injective env t = match (U.un_uinst t).n with | Tm_fvar fv -> - // Only explicit [@@unifier_hint_injective] counts Env.fv_has_attr env fv PC.unifier_hint_injective_lid | _ -> false @@ -1520,6 +1519,28 @@ let rec check_relation' (g:env) (rel:relation) (t0 t1:typ) iter2 brs0 brs1 relate_branch ()) (fun _ -> fallback t0 t1) + | Tm_match _, _ + | _, Tm_match _ -> + //One side is a match and the other is not (both-match handled above). + //Try to reduce the match away by normalizing with delta + iota + primops. + //If the match reduces (e.g., scrutinee unfolds to a constructor), recurse. + //Otherwise, fall back. + let reduce_match t = + N.normalize [Env.Weak; Env.HNF; Env.Beta; Env.Iota; Env.Primops; + Env.UnfoldUntil delta_constant] g.tcenv t + in + let try_reduce () = + let t0' = reduce_match t0 in + let t1' = reduce_match t1 in + //Check that at least one side actually changed (made progress) + if equal_term t0 t0' && equal_term t1 t1' + then fallback t0 t1 + else check_relation g rel t0' t1' + in + handle_with + (try_reduce ()) + (fun _ -> fallback t0 t1) + | _ -> fallback t0 t1 and check_relation (g:env) (rel:relation) (t0 t1:typ) From 305e12abafba55357d893d79b25377d8d8c5e7e1 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Tue, 2 Jun 2026 11:53:44 -0700 Subject: [PATCH 22/24] update expected error output --- .../test/error_messages/ClosureError.fst.output.expected | 5 +++-- .../error_messages/IfBranchMismatch.fst.output.expected | 8 ++++---- .../MatchBranchMismatch.fst.output.expected | 6 +++--- pulse/test/error_messages/NestedBlock.fst.output.expected | 2 +- pulse/test/error_messages/NestedCall.fst.output.expected | 5 +++-- .../error_messages/PrePostMismatch.fst.output.expected | 2 +- .../test/error_messages/SequenceError.fst.output.expected | 2 +- ...erminalActionPostConditionMismatch.fst.output.expected | 8 ++++---- .../WhileInvPreservation.fst.output.expected | 6 +++--- 9 files changed, 23 insertions(+), 21 deletions(-) diff --git a/pulse/test/error_messages/ClosureError.fst.output.expected b/pulse/test/error_messages/ClosureError.fst.output.expected index 7f5f57149f8..07273a8c66f 100644 --- a/pulse/test/error_messages/ClosureError.fst.output.expected +++ b/pulse/test/error_messages/ClosureError.fst.output.expected @@ -1,4 +1,4 @@ -* Info at ClosureError.fst(17,2-18,4): +* Info at ClosureError.fst(17,2-17,8): - Expected failure: - Could not prove equality of: - Pulse.Lib.Reference.pts_to r 0 @@ -13,5 +13,6 @@ -> fn requires Pulse.Class.PtsTo.pts_to r 1 ensures Pulse.Class.PtsTo.pts_to r 1) - - VC = Prims.l_False + - VC = Pulse.Lib.Reference.pts_to r 0 == Pulse.Lib.Reference.pts_to r 1 + - See also ClosureError.fst(17,2-18,4) diff --git a/pulse/test/error_messages/IfBranchMismatch.fst.output.expected b/pulse/test/error_messages/IfBranchMismatch.fst.output.expected index 9fee7a55499..31b0b93dd8d 100644 --- a/pulse/test/error_messages/IfBranchMismatch.fst.output.expected +++ b/pulse/test/error_messages/IfBranchMismatch.fst.output.expected @@ -1,4 +1,4 @@ -* Info at IfBranchMismatch.fst(14,6-14,8): +* Info at IfBranchMismatch.fst(14,4-14,8): - Expected failure: - Could not prove equality of: - Pulse.Lib.Reference.pts_to r 2 @@ -9,8 +9,8 @@ (r : Pulse.Lib.Reference.ref Prims.int) (b : Prims.bool) (_if_hyp : Prims.squash (Pulse.Lib.Core.rewrites_to_p b false)) (_if_br : Prims.unit) - - VC = Prims.l_False - - See also IfBranchMismatch.fst(14,9-14,10) + - VC = Pulse.Lib.Reference.pts_to r 2 == Pulse.Lib.Reference.pts_to r 1 + - See also IfBranchMismatch.fst(14,4-14,10) * Info at IfBranchMismatch.fst(30,4-30,6): - Expected failure: @@ -23,5 +23,5 @@ (r : Pulse.Lib.Reference.ref Prims.int) (b : Prims.bool) (_if_hyp : Prims.squash (Pulse.Lib.Core.rewrites_to_p b false)) (__ : Prims.unit) - - VC = Prims.l_False + - VC = Pulse.Lib.Reference.pts_to r 2 == Pulse.Lib.Reference.pts_to r 1 diff --git a/pulse/test/error_messages/MatchBranchMismatch.fst.output.expected b/pulse/test/error_messages/MatchBranchMismatch.fst.output.expected index b85d3d81543..6398b24e0a4 100644 --- a/pulse/test/error_messages/MatchBranchMismatch.fst.output.expected +++ b/pulse/test/error_messages/MatchBranchMismatch.fst.output.expected @@ -1,4 +1,4 @@ -* Info at MatchBranchMismatch.fst(13,13-13,15): +* Info at MatchBranchMismatch.fst(13,11-13,15): - Expected failure: - Could not prove equality of: - Pulse.Lib.Reference.pts_to r 2 @@ -8,6 +8,6 @@ - Env = (r : Pulse.Lib.Reference.ref Prims.int) (x : Prims.int) (branch equality : Prims.squash (x == 1)) (_br : Prims.unit) - - VC = Prims.l_False - - See also MatchBranchMismatch.fst(13,16-13,17) + - VC = Pulse.Lib.Reference.pts_to r 2 == Pulse.Lib.Reference.pts_to r 1 + - See also MatchBranchMismatch.fst(13,11-13,17) diff --git a/pulse/test/error_messages/NestedBlock.fst.output.expected b/pulse/test/error_messages/NestedBlock.fst.output.expected index 78b07a40f92..e00db1523b8 100644 --- a/pulse/test/error_messages/NestedBlock.fst.output.expected +++ b/pulse/test/error_messages/NestedBlock.fst.output.expected @@ -6,5 +6,5 @@ - Assertion failed - The SMT solver could not prove the query. - Env = (r : Pulse.Lib.Reference.ref Prims.int) - - VC = Prims.l_False + - VC = Pulse.Lib.Reference.pts_to r 1 == Pulse.Lib.Reference.pts_to r 0 diff --git a/pulse/test/error_messages/NestedCall.fst.output.expected b/pulse/test/error_messages/NestedCall.fst.output.expected index c1c059e674b..6b40aac9b76 100644 --- a/pulse/test/error_messages/NestedCall.fst.output.expected +++ b/pulse/test/error_messages/NestedCall.fst.output.expected @@ -1,4 +1,4 @@ -* Info at NestedCall.fst(18,2-19,4): +* Info at NestedCall.fst(18,2-18,9): - Expected failure: - Could not prove equality of: - Pulse.Lib.Reference.pts_to r 5 @@ -6,5 +6,6 @@ - Assertion failed - The SMT solver could not prove the query. - Env = (r : Pulse.Lib.Reference.ref Prims.int) - - VC = Prims.l_False + - VC = Pulse.Lib.Reference.pts_to r 5 == Pulse.Lib.Reference.pts_to r 0 + - See also NestedCall.fst(18,2-19,4) diff --git a/pulse/test/error_messages/PrePostMismatch.fst.output.expected b/pulse/test/error_messages/PrePostMismatch.fst.output.expected index 1011751443b..1061f4c0beb 100644 --- a/pulse/test/error_messages/PrePostMismatch.fst.output.expected +++ b/pulse/test/error_messages/PrePostMismatch.fst.output.expected @@ -6,5 +6,5 @@ - Assertion failed - The SMT solver could not prove the query. - Env = (r : Pulse.Lib.Reference.ref Prims.int) (__ : Prims.unit) - - VC = Prims.l_False + - VC = Pulse.Lib.Reference.pts_to r 1 == Pulse.Lib.Reference.pts_to r 42 diff --git a/pulse/test/error_messages/SequenceError.fst.output.expected b/pulse/test/error_messages/SequenceError.fst.output.expected index 4b44d091336..6f8b8dc5af9 100644 --- a/pulse/test/error_messages/SequenceError.fst.output.expected +++ b/pulse/test/error_messages/SequenceError.fst.output.expected @@ -9,5 +9,5 @@ (r1 : Pulse.Lib.Reference.ref Prims.int) (r2 : Pulse.Lib.Reference.ref Prims.int) (__ : Prims.unit) (__ : Prims.unit) - - VC = Prims.l_False + - VC = Pulse.Lib.Reference.pts_to r2 2 == Pulse.Lib.Reference.pts_to r2 1 diff --git a/pulse/test/error_messages/TerminalActionPostConditionMismatch.fst.output.expected b/pulse/test/error_messages/TerminalActionPostConditionMismatch.fst.output.expected index 0805d379298..2baeab648ef 100644 --- a/pulse/test/error_messages/TerminalActionPostConditionMismatch.fst.output.expected +++ b/pulse/test/error_messages/TerminalActionPostConditionMismatch.fst.output.expected @@ -1,4 +1,4 @@ -* Info at TerminalActionPostConditionMismatch.fst(12,4-12,6): +* Info at TerminalActionPostConditionMismatch.fst(12,2-12,6): - Expected failure: - Could not prove equality of: - Pulse.Lib.Reference.pts_to r 2 @@ -8,8 +8,8 @@ - Env = (r : Pulse.Lib.Reference.ref Prims.int) (__ : Prims.unit) (__ : Prims.unit) - - VC = Prims.l_False - - See also TerminalActionPostConditionMismatch.fst(12,7-12,8) + - VC = Pulse.Lib.Reference.pts_to r 2 == Pulse.Lib.Reference.pts_to r 1 + - See also TerminalActionPostConditionMismatch.fst(12,2-12,8) * Info at TerminalActionPostConditionMismatch.fst(23,2-23,4): - Expected failure: @@ -21,5 +21,5 @@ - Env = (r : Pulse.Lib.Reference.ref Prims.int) (__ : Prims.unit) (__ : Prims.unit) - - VC = Prims.l_False + - VC = Pulse.Lib.Reference.pts_to r 2 == Pulse.Lib.Reference.pts_to r 1 diff --git a/pulse/test/error_messages/WhileInvPreservation.fst.output.expected b/pulse/test/error_messages/WhileInvPreservation.fst.output.expected index 6a95e524052..6a896a2cf21 100644 --- a/pulse/test/error_messages/WhileInvPreservation.fst.output.expected +++ b/pulse/test/error_messages/WhileInvPreservation.fst.output.expected @@ -1,4 +1,4 @@ -* Info at WhileInvPreservation.fst(15,6-15,8): +* Info at WhileInvPreservation.fst(15,4-15,8): - Expected failure: - Could not prove equality of: - Pulse.Lib.Reference.pts_to i 2 @@ -12,6 +12,6 @@ (__anf0 : Prims.int) (__ : Prims.squash (Pulse.Lib.Core.rewrites_to_p __anf0 0)) (__ : Prims.unit) - - VC = Prims.l_False - - See also WhileInvPreservation.fst(15,12-15,13) + - VC = Pulse.Lib.Reference.pts_to i 2 == Pulse.Lib.Reference.pts_to i 0 + - See also WhileInvPreservation.fst(15,4-15,13) From 03756a8e6b5afd7b4553e284cedcc23cab9d3dc7 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Wed, 3 Jun 2026 08:43:38 -0700 Subject: [PATCH 23/24] refine reduction of matches only when guards are not allowed --- src/typechecker/FStarC.TypeChecker.Core.fst | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/src/typechecker/FStarC.TypeChecker.Core.fst b/src/typechecker/FStarC.TypeChecker.Core.fst index b1b0109c674..69040b5ecc8 100644 --- a/src/typechecker/FStarC.TypeChecker.Core.fst +++ b/src/typechecker/FStarC.TypeChecker.Core.fst @@ -1520,7 +1520,7 @@ let rec check_relation' (g:env) (rel:relation) (t0 t1:typ) (fun _ -> fallback t0 t1) | Tm_match _, _ - | _, Tm_match _ -> + | _, Tm_match _ when guard_not_ok -> //One side is a match and the other is not (both-match handled above). //Try to reduce the match away by normalizing with delta + iota + primops. //If the match reduces (e.g., scrutinee unfolds to a constructor), recurse. @@ -1529,9 +1529,14 @@ let rec check_relation' (g:env) (rel:relation) (t0 t1:typ) N.normalize [Env.Weak; Env.HNF; Env.Beta; Env.Iota; Env.Primops; Env.UnfoldUntil delta_constant] g.tcenv t in + let maybe_reduce t = + match t.n with + | Tm_match _ -> reduce_match t + | _ -> t + in let try_reduce () = - let t0' = reduce_match t0 in - let t1' = reduce_match t1 in + let t0' = maybe_reduce t0 in + let t1' = maybe_reduce t1 in //Check that at least one side actually changed (made progress) if equal_term t0 t0' && equal_term t1 t1' then fallback t0 t1 From 814b5c098cdd25065dc4db8aa2df6b792abc2283 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Wed, 3 Jun 2026 08:47:08 -0700 Subject: [PATCH 24/24] fix bad merge --- pulse/lib/pulse/lib/Pulse.Lib.Swap.Spec.fst | 2 -- 1 file changed, 2 deletions(-) diff --git a/pulse/lib/pulse/lib/Pulse.Lib.Swap.Spec.fst b/pulse/lib/pulse/lib/Pulse.Lib.Swap.Spec.fst index 248352b88bf..f8ba9cfed19 100644 --- a/pulse/lib/pulse/lib/Pulse.Lib.Swap.Spec.fst +++ b/pulse/lib/pulse/lib/Pulse.Lib.Swap.Spec.fst @@ -697,8 +697,6 @@ let array_swap_inner_invariant_end = () #pop-options -#pop-options - module SZ = FStar.SizeT let sz_rem_spec