From ee293de9829d1d2be2a8042f70fa1d92de0e2cc5 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 6 Mar 2026 11:59:13 +0100 Subject: [PATCH] test: add instantiateMVars tests and benchmark for delayed assignments (#12808) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR adds tests and a benchmark exercising `instantiateMVars` on metavariable assignment graphs with nested delayed assignments, in preparation for optimizing the delayed mvar resolution path. - `tests/elab/instantiateMVarsShadow.lean`: Two test cases for correctness when the same fvar is bound to different values at different scope levels (fvar shadowing and late-bind patterns). A buggy cache could return a stale result from one scope level in another. - `tests/elab/instantiateMVarsSharing.lean`: Verifies correct resolution and object sharing on a graph with nested delayed mvars producing `∀ s, (s = s → (s = s) ∧ (s = s)) ∧ (s = s)`. - `tests/elab_bench/delayed_assign.lean`: Constructs an O(n²) delayed mvar graph (n=700) and measures `instantiateMVars` resolution time, calibrated to ~1s total elaboration. 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 4.6 --- tests/elab/instantiateMVarsCrossScope.lean | 86 ++++++++++++ tests/elab/instantiateMVarsShadow.lean | 152 +++++++++++++++++++++ tests/elab/instantiateMVarsSharing.lean | 101 ++++++++++++++ tests/elab_bench/delayed_assign.lean | 55 ++++++++ tests/elab_bench/delayed_sharing.lean | 52 +++++++ 5 files changed, 446 insertions(+) create mode 100644 tests/elab/instantiateMVarsCrossScope.lean create mode 100644 tests/elab/instantiateMVarsShadow.lean create mode 100644 tests/elab/instantiateMVarsSharing.lean create mode 100644 tests/elab_bench/delayed_assign.lean create mode 100644 tests/elab_bench/delayed_sharing.lean diff --git a/tests/elab/instantiateMVarsCrossScope.lean b/tests/elab/instantiateMVarsCrossScope.lean new file mode 100644 index 0000000000..656bd77233 --- /dev/null +++ b/tests/elab/instantiateMVarsCrossScope.lean @@ -0,0 +1,86 @@ +import Lean + +open Lean Meta + +/-! +Test: cross-scope sharing in `instantiateMVars` with nested delayed mvars. + +A shared expression `succ_x := Nat.succ x_fvar` is visited at scope 1 +(as d2's argument, before scope 2 is pushed) and then at scope 2 +(inside d2's pending value). Since the result only depends on scope 1, +which hasn't changed, both visits should produce the same object. + + ?root := fun (a : Nat) => ?d1 a + ?d1 delayed [x] := ?body + ?body := ?d2 succ_x ← succ_x visited at scope 1 as d2's arg + ?d2 delayed [z] := ?inner + ?inner := Prod.mk z succ_x ← z = R1, succ_x visited at scope 2 + +The ordering guarantee comes from the delayed mvar resolution control +flow: arguments are visited before pushing the new scope, the pending +value is visited after. This does not depend on the order in which +application arguments are traversed. + +Expected result: fun (a : Nat) => (Nat.succ a, Nat.succ a) + +Both `Nat.succ a` subexpressions in the result should be the same +object (ptrEq), since the shared input `succ_x` produces the same +result at both scope levels. +-/ + +private def mkCrossScopeTest : MetaM Expr := do + let nat := mkConst ``Nat + withLocalDeclD `x nat fun x_fvar => + withLocalDeclD `z nat fun z_fvar => do + let succ_x := mkApp (mkConst ``Nat.succ) x_fvar + + -- ?inner := Prod.mk z succ_x + let pairTy := mkApp2 (mkConst ``Prod [.succ .zero, .succ .zero]) nat nat + let inner ← mkFreshExprMVar pairTy + inner.mvarId!.assign + (mkApp4 (mkConst ``Prod.mk [.succ .zero, .succ .zero]) nat nat z_fvar succ_x) + + -- ?d2 delayed [z] := ?inner, takes one Nat arg + let d2_ty ← mkArrow nat pairTy + let d2 ← mkFreshExprMVar d2_ty (kind := .syntheticOpaque) + assignDelayedMVar d2.mvarId! #[z_fvar] inner.mvarId! + + -- ?body := ?d2 succ_x + let body ← mkFreshExprMVar pairTy + body.mvarId!.assign (mkApp d2 succ_x) + + -- ?d1 delayed [x] := ?body + let d1_ty ← mkArrow nat pairTy + let d1 ← mkFreshExprMVar d1_ty (kind := .syntheticOpaque) + assignDelayedMVar d1.mvarId! #[x_fvar] body.mvarId! + + -- ?root := fun (a : Nat) => ?d1 a + let rootTy ← mkArrow nat pairTy + let root ← mkFreshExprMVar rootTy + root.mvarId!.assign (Lean.mkLambda `a .default nat (mkApp d1 (.bvar 0))) + return root + +-- Expected: fun (a : Nat) => (Nat.succ a, Nat.succ a) +private def mkExpected : Expr := + let nat := mkConst ``Nat + let succ_a := mkApp (mkConst ``Nat.succ) (.bvar 0) + let body := mkApp4 (mkConst ``Prod.mk [.succ .zero, .succ .zero]) nat nat succ_a succ_a + Lean.mkLambda `a .default nat body + +-- Extract the two components from the result +-- Result shape: fun (a : Nat) => @Prod.mk Nat Nat fst snd +private def extractComponents (e : Expr) : Expr × Expr := + let body := e.bindingBody! + let snd := body.appArg! + let fst := body.appFn!.appArg! + (fst, snd) + +run_meta do + let root ← mkCrossScopeTest + let expected := mkExpected + let result ← instantiateMVars root + unless result == expected do + throwError "cross-scope: wrong result, got {result}" + let (fst, snd) := extractComponents result + unless unsafe ptrEq fst snd do + throwError "cross-scope: fst and snd are not shared (not ptrEq)" diff --git a/tests/elab/instantiateMVarsShadow.lean b/tests/elab/instantiateMVarsShadow.lean new file mode 100644 index 0000000000..20eb1795c2 --- /dev/null +++ b/tests/elab/instantiateMVarsShadow.lean @@ -0,0 +1,152 @@ +import Lean + +open Lean Meta + +/-! +Test: fvar shadowing in nested delayed mvars. + +Two delayed mvars bind the same fvar `x_fvar` to different values. +A shared subexpression `succ_x := Nat.succ x_fvar` appears in both scopes. + + ?root := fun (a : Nat) => ?d1 a + ?d1 delayed [x_fvar] := ?body + ?body := Prod.mk succ_x (?d2 succ_x) ← succ_x is shared + ?d2 delayed [x_fvar] := ?inner + ?inner := succ_x ← same shared object + +Expected result: + fun (a : Nat) => (Nat.succ a, Nat.succ (Nat.succ a)) + +When resolving ?d1 with arg `a`: + - succ_x with x_fvar → a gives Nat.succ a (first component) + - ?d2 gets arg (Nat.succ a), so x_fvar → Nat.succ a + succ_x with x_fvar → Nat.succ a gives Nat.succ (Nat.succ a) (second component) + +A buggy cache could return the cached scope-1 result (Nat.succ a) for the scope-2 +visit, producing (Nat.succ a, Nat.succ a) instead. +-/ + +private def mkShadowTest : MetaM Expr := do + let nat := mkConst ``Nat + withLocalDeclD `x nat fun x_fvar => do + -- shared object referencing x_fvar + let succ_x := mkApp (mkConst ``Nat.succ) x_fvar + + -- ?inner := succ_x + let inner ← mkFreshExprMVar nat + inner.mvarId!.assign succ_x + + -- ?d2 delayed [x_fvar] := ?inner + let d2_ty ← mkArrow nat nat + let d2 ← mkFreshExprMVar d2_ty (kind := .syntheticOpaque) + assignDelayedMVar d2.mvarId! #[x_fvar] inner.mvarId! + + -- ?body := ⟨succ_x, ?d2 succ_x⟩ + let pairTy := mkApp2 (mkConst ``Prod [.succ .zero, .succ .zero]) nat nat + let body ← mkFreshExprMVar pairTy + body.mvarId!.assign + (mkApp4 (mkConst ``Prod.mk [.succ .zero, .succ .zero]) nat nat + succ_x (mkApp d2 succ_x)) + + -- ?d1 delayed [x_fvar] := ?body + let d1_ty ← mkArrow nat pairTy + let d1 ← mkFreshExprMVar d1_ty (kind := .syntheticOpaque) + assignDelayedMVar d1.mvarId! #[x_fvar] body.mvarId! + + -- ?root := fun (a : Nat) => ?d1 a + let rootTy ← mkArrow nat pairTy + let root ← mkFreshExprMVar rootTy + root.mvarId!.assign (Lean.mkLambda `a .default nat (mkApp d1 (.bvar 0))) + return root + +-- Expected: fun (a : Nat) => (Nat.succ a, Nat.succ (Nat.succ a)) +private def mkExpected : Expr := + let nat := mkConst ``Nat + let succ := mkConst ``Nat.succ + -- #0 refers to the lambda-bound `a` + let succ_a := mkApp succ (.bvar 0) + let succ_succ_a := mkApp succ succ_a + let body := mkApp4 (mkConst ``Prod.mk [.succ .zero, .succ .zero]) nat nat succ_a succ_succ_a + Lean.mkLambda `a .default nat body + +run_meta do + let root ← mkShadowTest + let result ← instantiateMVars root + let expected := mkExpected + unless result == expected do + throwError "shadow: expected\n {expected}\ngot\n {result}" + +/-! +Test: an fvar first seen unsubstituted, then substituted at a higher scope. + +A shared subexpression `succ_y := Nat.succ y_fvar` is used both: + - directly in the body of d1 (where y is NOT bound), and + - inside d2's pending value (where y IS bound). + + ?root := fun (a : Nat) => ?d1 a + ?d1 delayed [x] := ?body + ?body := Prod.mk succ_y (?d2 succ_y) ← succ_y shared + ?d2 delayed [y] := ?inner ← y is NOW bound + ?inner := succ_y ← same shared object + +Expected result: + fun (a : Nat) => (Nat.succ y_fvar, Nat.succ (Nat.succ y_fvar)) + +At scope 1 (d1), x → a. Visit body: + - succ_y: y is NOT in fvar_subst. Result is succ_y unchanged. + - ?d2 succ_y: arg succ_y visited → succ_y. Then d2 at scope 2 with y → succ_y. + - Visit ?inner = succ_y. y IS in fvar_subst → Nat.succ succ_y = Nat.succ (Nat.succ y_fvar). + +A buggy cache would return the scope-1 result (succ_y unchanged) at scope 2, +producing (Nat.succ y_fvar, Nat.succ y_fvar) instead. +-/ + +private def mkLateBindTest : MetaM (Expr × Expr) := do + let nat := mkConst ``Nat + withLocalDeclD `x nat fun x_fvar => + withLocalDeclD `y nat fun y_fvar => do + -- shared object referencing y_fvar (NOT x_fvar) + let succ_y := mkApp (mkConst ``Nat.succ) y_fvar + + -- ?inner := succ_y + let inner ← mkFreshExprMVar nat + inner.mvarId!.assign succ_y + + -- ?d2 delayed [y_fvar] := ?inner + let d2_ty ← mkArrow nat nat + let d2 ← mkFreshExprMVar d2_ty (kind := .syntheticOpaque) + assignDelayedMVar d2.mvarId! #[y_fvar] inner.mvarId! + + -- ?body := ⟨succ_y, ?d2 succ_y⟩ + let pairTy := mkApp2 (mkConst ``Prod [.succ .zero, .succ .zero]) nat nat + let body ← mkFreshExprMVar pairTy + body.mvarId!.assign + (mkApp4 (mkConst ``Prod.mk [.succ .zero, .succ .zero]) nat nat + succ_y (mkApp d2 succ_y)) + + -- ?d1 delayed [x_fvar] := ?body + let d1_ty ← mkArrow nat pairTy + let d1 ← mkFreshExprMVar d1_ty (kind := .syntheticOpaque) + assignDelayedMVar d1.mvarId! #[x_fvar] body.mvarId! + + -- ?root := fun (a : Nat) => ?d1 a + let rootTy ← mkArrow nat pairTy + let root ← mkFreshExprMVar rootTy + root.mvarId!.assign (Lean.mkLambda `a .default nat (mkApp d1 (.bvar 0))) + return (root, y_fvar) + +-- Expected: fun (a : Nat) => (Nat.succ y_fvar, Nat.succ (Nat.succ y_fvar)) +private def mkExpectedLateBind (y_fvar : Expr) : Expr := + let nat := mkConst ``Nat + let succ := mkConst ``Nat.succ + let succ_y := mkApp succ y_fvar + let succ_succ_y := mkApp succ succ_y + let body := mkApp4 (mkConst ``Prod.mk [.succ .zero, .succ .zero]) nat nat succ_y succ_succ_y + Lean.mkLambda `a .default nat body + +run_meta do + let (root, y_fvar) ← mkLateBindTest + let result ← instantiateMVars root + let expected := mkExpectedLateBind y_fvar + unless result == expected do + throwError "late-bind: expected\n {expected}\ngot\n {result}" diff --git a/tests/elab/instantiateMVarsSharing.lean b/tests/elab/instantiateMVarsSharing.lean new file mode 100644 index 0000000000..04bbc24c82 --- /dev/null +++ b/tests/elab/instantiateMVarsSharing.lean @@ -0,0 +1,101 @@ +import Lean + +open Lean Meta + +/-! +Test for sharing in `instantiateMVars` with delayed mvar assignments. + +We construct the metavariable assignment graph for the goal +`∀ s, (s = s → (s = s) ∧ (s = s)) ∧ (s = s)`: + + ?root := fun (s : Nat) => ?rootAux #0 + ?rootAux delayed [s_fvar] := ?body + ?body := @And.intro leftTy rightTy ?left right + ?left := fun (h : eq_ss) => ?leftAux #0 + ?leftAux delayed [h_fvar] := ?inner + ?inner := @And.intro eq_ss eq_ss h_fvar h_fvar + +where + + eq_ss := @Eq Nat s_fvar s_fvar ← single shared object + andTy := And eq_ss eq_ss ← contains eq_ss + leftTy := eq_ss → andTy ← forallE body contains eq_ss + rightTy := eq_ss + right := @Eq.refl Nat s_fvar + +After instantiation, the shared `eq_ss` input should produce shared results +at each binding depth: +- At depth 1: `@Eq Nat #0 #0` (used as rightTy, leftTy.domain, left.domain) +- At depth 2: `@Eq Nat #1 #1` (used as And args in leftTy body and And.intro + type args in inner body) +-/ + +private def mkTestRoot : MetaM Expr := do + let nat := mkConst ``Nat + withLocalDeclD `s nat fun s_fvar => do + let eq_ss ← mkEq s_fvar s_fvar -- shared object + + let andTy := mkApp2 (mkConst ``And) eq_ss eq_ss -- (s=s) ∧ (s=s) + let leftTy ← mkArrow eq_ss andTy -- s=s → (s=s) ∧ (s=s) + let rightTy := eq_ss -- s=s + let bodyTy := mkApp2 (mkConst ``And) leftTy rightTy + + let body ← mkFreshExprMVar bodyTy + let left ← mkFreshExprMVar leftTy + + withLocalDeclD `h eq_ss fun h_fvar => do + -- ?inner : (s=s) ∧ (s=s), proved by And.intro eq_ss eq_ss h h + let inner ← mkFreshExprMVar andTy + let leftDecl ← left.mvarId!.getDecl + let leftAux ← mkFreshExprMVarAt leftDecl.lctx leftDecl.localInstances + leftDecl.type .syntheticOpaque + assignDelayedMVar leftAux.mvarId! #[h_fvar] inner.mvarId! + left.mvarId!.assign (Lean.mkLambda `h .default eq_ss (mkApp leftAux (.bvar 0))) + inner.mvarId!.assign (mkApp4 (mkConst ``And.intro) eq_ss eq_ss h_fvar h_fvar) + + let right := mkApp2 (mkConst ``Eq.refl [1]) nat s_fvar + body.mvarId!.assign (mkApp4 (mkConst ``And.intro) leftTy rightTy left right) + + let rootTy ← mkForallFVars #[s_fvar] bodyTy + let root ← mkFreshExprMVar rootTy + let rootDecl ← root.mvarId!.getDecl + let rootAux ← mkFreshExprMVarAt rootDecl.lctx rootDecl.localInstances + rootDecl.type .syntheticOpaque + assignDelayedMVar rootAux.mvarId! #[s_fvar] body.mvarId! + root.mvarId!.assign (Lean.mkLambda `s .default nat (mkApp rootAux (.bvar 0))) + return root + +-- Instantiate and verify sharing +run_meta do + let root ← mkTestRoot + let result ← instantiateMVars root + + -- Result: fun (s : Nat) => @And.intro leftTy rightTy left right + let outerBody := result.bindingBody! + let rightTy := outerBody.appFn!.appFn!.appArg! + let leftTy := outerBody.appFn!.appFn!.appFn!.appArg! + let left := outerBody.appFn!.appArg! + + -- At depth 1: rightTy, leftTy.domain, and left.domain are all + -- instantiations of the shared `eq_ss` at the same depth → ptrEq. + unless unsafe ptrEq rightTy leftTy.bindingDomain! do + throwError "sharing: rightTy and leftTy.domain are not ptrEq" + unless unsafe ptrEq rightTy left.bindingDomain! do + throwError "sharing: rightTy and left.domain are not ptrEq" + + -- At depth 2: the two eq_ss args inside `And` in leftTy's body → ptrEq. + let andInLeftTyBody := leftTy.bindingBody! + unless unsafe ptrEq andInLeftTyBody.appFn!.appArg! andInLeftTyBody.appArg! do + throwError "sharing: And args in leftTy body are not ptrEq" + + -- At depth 2: the two type args inside `And.intro` in the inner body → ptrEq. + let innerBody := left.bindingBody! + let innerTyArg1 := innerBody.appFn!.appFn!.appFn!.appArg! + let innerTyArg2 := innerBody.appFn!.appFn!.appArg! + unless unsafe ptrEq innerTyArg1 innerTyArg2 do + throwError "sharing: And.intro type args in inner body are not ptrEq" + + -- Cross-expression: depth-2 eq_ss from leftTy body and inner body should + -- be the same object (same shared input at the same binding depth). + unless unsafe ptrEq andInLeftTyBody.appArg! innerTyArg1 do + throwError "sharing: eq_ss at depth 2 not shared across leftTy and inner" diff --git a/tests/elab_bench/delayed_assign.lean b/tests/elab_bench/delayed_assign.lean new file mode 100644 index 0000000000..edc834039b --- /dev/null +++ b/tests/elab_bench/delayed_assign.lean @@ -0,0 +1,55 @@ +import Lean + +/-! +This benchmark exercises `instantiateMVars` on a large metavariable +assignment graph with many nested delayed assignments. + +We construct a goal of the form + `∀ x₁ … xₙ, ((0 ≤ x₁) ∧ … ∧ True) ∧ … ∧ ((0 ≤ xₙ) ∧ … ∧ True)` +as a single mvar, solve it (creating O(n²) delayed mvars), and then +call `instantiateMVars` to fully resolve the result. +-/ + +set_option maxHeartbeats 40000000 + +open Lean Meta + +def mkLE (i : Nat) : Expr := + mkNatLE (mkNatLit 0) (mkBVar i) + +partial def solve (mvarId : MVarId) : MetaM Unit := do + let type ← instantiateMVars (← mvarId.getType) + if type.isForall then + let (_, mvarId) ← mvarId.intro1 + solve mvarId + else if type.isAppOf ``And then + let [mvarId₁, mvarId₂] ← mvarId.applyConst ``And.intro | failure + solve mvarId₁ + solve mvarId₂ + else if type.isAppOf ``LE.le then + let [] ← mvarId.applyConst ``Nat.zero_le | failure + else + let [] ← mvarId.applyConst ``True.intro | failure + +def mkBench (n : Nat) : MetaM MVarId := do + let type := mkType n + return (← mkFreshExprSyntheticOpaqueMVar type).mvarId! +where + mkResultType (i : Nat) : Expr := + match i with + | 0 => mkConst ``True + | i+1 => mkAnd (mkLE i) (mkResultType i) + + mkType (i : Nat) : Expr := + match i with + | 0 => mkResultType n + | i+1 => .forallE `x Nat.mkType (mkAnd (mkType i) (mkLE (n - i - 1))) .default + +-- n=200 is calibrated to take roughly 1s total elaboration time. +-- Use a small n unless TEST_BENCH=1, so that the test suite runs quickly. +run_meta do + let bench := (← IO.getEnv "TEST_BENCH") == some "1" + let n := if bench then 200 else 50 + let mvarId ← mkBench n + solve mvarId + discard <| instantiateMVars (mkMVar mvarId) diff --git a/tests/elab_bench/delayed_sharing.lean b/tests/elab_bench/delayed_sharing.lean new file mode 100644 index 0000000000..370bf6853d --- /dev/null +++ b/tests/elab_bench/delayed_sharing.lean @@ -0,0 +1,52 @@ +import Lean + +/-! +This benchmark exercises `instantiateMVars` sharing on an exponential DAG +of delayed metavariable assignments. + +We build a chain of n delayed mvars: + ?d₀ delayed [x] := x + ?dᵢ delayed [x] := Nat.add (?dᵢ₋₁ x) (?dᵢ₋₁ x) + ?root := fun (a : Nat) => ?dₙ a + +Without sharing, instantiating ?root would produce 2ⁿ leaf nodes. +With sharing, it produces O(n) unique subexpressions. +-/ + +set_option maxHeartbeats 40000000 + +open Lean Meta + +def mkSharingBench (n : Nat) : MetaM Expr := do + let nat := mkConst ``Nat + withLocalDeclD `x nat fun x_fvar => do + -- d₀ delayed [x] := x + let d₀Inner ← mkFreshExprMVar nat + d₀Inner.mvarId!.assign x_fvar + let d₀Ty ← mkArrow nat nat + let d₀ ← mkFreshExprMVar d₀Ty (kind := .syntheticOpaque) + assignDelayedMVar d₀.mvarId! #[x_fvar] d₀Inner.mvarId! + + let mut prev := d₀ + for _ in [:n] do + let app := mkApp prev x_fvar -- shared subexpression + let inner ← mkFreshExprMVar nat + inner.mvarId!.assign (mkApp2 (mkConst ``Nat.add) app app) + let dTy ← mkArrow nat nat + let d ← mkFreshExprMVar dTy (kind := .syntheticOpaque) + assignDelayedMVar d.mvarId! #[x_fvar] inner.mvarId! + prev := d + + -- root := fun a => dₙ a + let rootTy ← mkArrow nat nat + let root ← mkFreshExprMVar rootTy + root.mvarId!.assign (Lean.mkLambda `a .default nat (mkApp prev (.bvar 0))) + return root + +-- n=19 is calibrated to take roughly 1s total elaboration time. +-- Use a small n unless TEST_BENCH=1, so that the test suite runs quickly. +run_meta do + let bench := (← IO.getEnv "TEST_BENCH") == some "1" + let n := if bench then 19 else 10 + let root ← mkSharingBench n + discard <| instantiateMVars root