From e260f2bf89dea104f3c621d9e98d387a1f94d5ff Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 22 Apr 2026 22:50:45 +0000 Subject: [PATCH 1/2] Add proj-of-prop soundness test MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The exported theorem builds a proof of `False` via a projection from a `Prop`-typed structure whose constructor was applied to an ill-typed argument: structure Wrapper : Prop where mk :: p : False theorem badFalse : False := (Wrapper.mk True.intro).p A checker that types a projection by inferring (rather than checking) its structure — trusting the structure to be well-typed rather than verifying the constructor's arguments against its binders — will accept this and return `badFalse : False`. A sound checker must reject it. Co-Authored-By: Claude Opus 4.7 (1M context) --- tests/proj-of-prop.lean | 27 +++++++++++++++++++++++++++ tests/proj-of-prop.yaml | 19 +++++++++++++++++++ 2 files changed, 46 insertions(+) create mode 100644 tests/proj-of-prop.lean create mode 100644 tests/proj-of-prop.yaml diff --git a/tests/proj-of-prop.lean b/tests/proj-of-prop.lean new file mode 100644 index 0000000..68a5604 --- /dev/null +++ b/tests/proj-of-prop.lean @@ -0,0 +1,27 @@ +import Lean +open Lean Meta Elab Term + +section Unchecked +syntax (name := unchecked) "unchecked" term : term + +@[term_elab «unchecked»] +def elabUnchecked : TermElab := fun stx expectedType? => do + match stx with + | `(unchecked $t) => + let some expectedType := expectedType? | + tryPostpone + throwError "invalid 'unchecked', expected type required" + let e ← elabTerm t none + let mvar ← mkFreshExprMVar expectedType MetavarKind.syntheticOpaque + mvar.mvarId!.assign e + return mvar + | _ => throwUnsupportedSyntax + +end Unchecked + +structure Wrapper : Prop where + mk :: + p : False + +set_option debug.skipKernelTC true in +theorem badFalse : False := (Wrapper.mk (unchecked True.intro)).p diff --git a/tests/proj-of-prop.yaml b/tests/proj-of-prop.yaml new file mode 100644 index 0000000..a709862 --- /dev/null +++ b/tests/proj-of-prop.yaml @@ -0,0 +1,19 @@ +description: | + A proof of `False` via a projection from a `Prop`-typed structure whose + constructor was applied to an ill-typed argument. The exported term is + + badFalse : False := (Wrapper.mk True.intro).p + + where `Wrapper : Prop` has a single field `p : False`, so `Wrapper.mk` + expects a proof of `False` but is given `True.intro : True`. + + A sound checker must reject this. A checker that types a projection by + inferring (rather than checking) its structure argument — i.e. that + trusts the structure to be well-typed instead of verifying the + constructor's argument types against its binders — will accept it, + because `Wrapper.mk True.intro` still formally inhabits `Wrapper` at + the structural level, and the `p` projection is then read back out at + the declared field type `False`. +leanfile: tests/proj-of-prop.lean +export-decls: ["badFalse"] +outcome: reject From 1d3f60c1a206a0a08d9076cce0f61c57ba03cb6c Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 22 Apr 2026 23:22:09 +0000 Subject: [PATCH 2/2] Fix proj-of-prop test to actually exercise the bug The previous version used `(Wrapper.mk True.intro).p` with `unchecked` + `debug.skipKernelTC`, but Lean's elaborator desugars `s.field` syntax into a call to the generated projection *function* (here `Wrapper.p`), never a raw `Expr.proj`. The exported declaration was therefore an `App`, which is caught by `infer_app`'s strict argument-type check -- so sound and unsound checkers all rejected it for the wrong reason. Construct the declaration programmatically instead, building the value as a literal `Expr.proj` around the ill-typed `Wrapper.mk True.intro`. Verified with `lka.py run`: the official Lean kernel rejects, nanoda and sonanoda both (incorrectly) accept. Co-Authored-By: Claude Opus 4.7 (1M context) --- tests/proj-of-prop.lean | 45 ++++++++++++++++++++++------------------- 1 file changed, 24 insertions(+), 21 deletions(-) diff --git a/tests/proj-of-prop.lean b/tests/proj-of-prop.lean index 68a5604..c8adaab 100644 --- a/tests/proj-of-prop.lean +++ b/tests/proj-of-prop.lean @@ -1,27 +1,30 @@ import Lean -open Lean Meta Elab Term - -section Unchecked -syntax (name := unchecked) "unchecked" term : term - -@[term_elab «unchecked»] -def elabUnchecked : TermElab := fun stx expectedType? => do - match stx with - | `(unchecked $t) => - let some expectedType := expectedType? | - tryPostpone - throwError "invalid 'unchecked', expected type required" - let e ← elabTerm t none - let mvar ← mkFreshExprMVar expectedType MetavarKind.syntheticOpaque - mvar.mvarId!.assign e - return mvar - | _ => throwUnsupportedSyntax - -end Unchecked +open Lean Elab Command structure Wrapper : Prop where mk :: p : False -set_option debug.skipKernelTC true in -theorem badFalse : False := (Wrapper.mk (unchecked True.intro)).p +/- +The value we want to add is + + Expr.proj `Wrapper 0 (Wrapper.mk True.intro) + +which has a `True.intro : True` sitting in the `Wrapper.mk` slot that +expects a `False`. The elaborator never emits a raw `Expr.proj` from +`(...).p` syntax (it desugars to the projection *function* `Wrapper.p`, +which would get caught at `infer_app`), so we construct the declaration +programmatically and hand it to `addDecl` under `debug.skipKernelTC`. +-/ + +run_cmd liftTermElabM do + let badValue : Expr := + .proj `Wrapper 0 (mkApp (mkConst ``Wrapper.mk) (mkConst ``True.intro)) + let decl : Declaration := .thmDecl { + name := `badFalse + levelParams := [] + type := mkConst ``False + value := badValue + } + withOptions (debug.skipKernelTC.set · true) do + addDecl decl