From 07cffa94bb2b848334baf9e6d7c969db1abd7836 Mon Sep 17 00:00:00 2001 From: Arthur Paulino Date: Fri, 22 May 2026 07:08:34 -0700 Subject: [PATCH] Encode entry-function invariants on `Source.Function` MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Add two propositional fields to `Source.Function`: - `entryMonomorphic : params = [] ∨ entry = false` - `entryPointerFree : sigPointerFree inputs output = true ∨ entry = false` `Typ.hasPointer` + `sigPointerFree` are new helpers. Smart constructors `monoNonEntry`, `monoEntry`, and `poly` discharge both props by construction. `Meta.elabFunction` dispatches via the `pub` keyword and uses `mkDecideProof` on `sigPointerFree` to reject pointer-typed entry signatures at parse time. `Check.mkDecls` re-derives the proof after alias expansion and surfaces a new `CheckError.entryHasPointer` if an alias hides a pointer in an entry signature. --- Ix/Aiur/Compiler/Check.lean | 11 ++++++- Ix/Aiur/Meta.lean | 46 ++++++++++++++++++---------- Ix/Aiur/Stages/Source.lean | 60 ++++++++++++++++++++++++++++++++++++- 3 files changed, 99 insertions(+), 18 deletions(-) diff --git a/Ix/Aiur/Compiler/Check.lean b/Ix/Aiur/Compiler/Check.lean index 935192b4..e95a4fcc 100644 --- a/Ix/Aiur/Compiler/Check.lean +++ b/Ix/Aiur/Compiler/Check.lean @@ -48,6 +48,7 @@ inductive CheckError | unconstrainedConstructor : Global → CheckError | infiniteType : Nat → Typ → CheckError | unresolvedMVar : Nat → CheckError + | entryHasPointer : Global → CheckError deriving Repr instance : ToString CheckError where @@ -175,7 +176,15 @@ def Source.Toplevel.mkDecls (toplevel : Source.Toplevel) : Except CheckError Sou let typ' ← expandTyp typ pure (loc, typ') let output' ← expandTyp function.output - let function' := { function with inputs := inputs', output := output' } + let function' : Source.Function ← + match hEntry : function.entry with + | true => + if hSig : sigPointerFree inputs' output' = true then + pure { function with inputs := inputs', output := output', entryPointerFree := Or.inl hSig } + else + throw $ .entryHasPointer function.name + | false => + pure { function with inputs := inputs', output := output', entryPointerFree := Or.inr hEntry } decls := decls.insert function.name (.function function') for dataType in toplevel.dataTypes do diff --git a/Ix/Aiur/Meta.lean b/Ix/Aiur/Meta.lean index 159e2193..783f9448 100644 --- a/Ix/Aiur/Meta.lean +++ b/Ix/Aiur/Meta.lean @@ -626,45 +626,59 @@ def elabFunction : ElabStxCat `aiur_function | `(aiur_function| $[pub%$e]? fn $i:ident() $[-> $ty:aiur_typ]? {$t:aiur_trm}) => do let g ← mkAppM ``Global.mk #[toExpr i.getId] let bindType ← mkAppM ``Prod #[mkConst ``Local, mkConst ``Typ] - let e := elabEntryBool e - mkAppM ``Source.Function.mk - #[g, ← elabEmptyList ``String, ← mkListLit bindType [], - ← elabRetTyp ty, ← elabTrm t, e] + let inputs ← mkListLit bindType [] + let output ← elabRetTyp ty + let body ← elabTrm t + mkMonoFun e g inputs output body | `(aiur_function| $[pub%$e]? fn $i:ident($b:aiur_bind $[, $bs:aiur_bind]*) $[-> $ty:aiur_typ]? {$t:aiur_trm}) => do let g ← mkAppM ``Global.mk #[toExpr i.getId] let bindType ← mkAppM ``Prod #[mkConst ``Local, mkConst ``Typ] - let e := elabEntryBool e - mkAppM ``Source.Function.mk - #[g, ← elabEmptyList ``String, - ← elabListCore b bs elabBind bindType, - ← elabRetTyp ty, ← elabTrm t, e] + let inputs ← elabListCore b bs elabBind bindType + let output ← elabRetTyp ty + let body ← elabTrm t + mkMonoFun e g inputs output body | `(aiur_function| fn $i:ident‹$p:ident $[, $ps:ident]*›() $[-> $ty:aiur_typ]? {$t:aiur_trm}) => do let g ← mkAppM ``Global.mk #[toExpr i.getId] let (_, paramsExpr) ← elabTypeParams p ps let bindType ← mkAppM ``Prod #[mkConst ``Local, mkConst ``Typ] - mkAppM ``Source.Function.mk + mkAppM ``Source.Function.poly #[g, paramsExpr, ← mkListLit bindType [], - ← elabRetTyp ty, ← elabTrm t, mkConst ``Bool.false] + ← elabRetTyp ty, ← elabTrm t] | `(aiur_function| fn $i:ident‹$p:ident $[, $ps:ident]*› ($b:aiur_bind $[, $bs:aiur_bind]*) $[-> $ty:aiur_typ]? {$t:aiur_trm}) => do let g ← mkAppM ``Global.mk #[toExpr i.getId] let (_, paramsExpr) ← elabTypeParams p ps let bindType ← mkAppM ``Prod #[mkConst ``Local, mkConst ``Typ] - mkAppM ``Source.Function.mk + mkAppM ``Source.Function.poly #[g, paramsExpr, ← elabListCore b bs elabBind bindType, - ← elabRetTyp ty, ← elabTrm t, mkConst ``Bool.false] + ← elabRetTyp ty, ← elabTrm t] | stx => throw $ .error stx "Invalid syntax for function" where - elabEntryBool : Option Syntax → Expr - | none => mkConst ``Bool.false - | some _ => mkConst ``Bool.true elabRetTyp : Option (TSyntax `aiur_typ) → TermElabM Expr | none => pure $ mkConst ``Typ.unit | some typ => elabTyp typ + /-- Build a monomorphic `Source.Function`. If `pubKw?` is `some _` + (public/entry function), require a `sigPointerFree` proof: signatures + with `.pointer` types are rejected with a Meta-level error. -/ + mkMonoFun (pubKw? : Option Syntax) (name inputs output body : Expr) : + TermElabM Expr := do + match pubKw? with + | none => + mkAppM ``Source.Function.monoNonEntry #[name, inputs, output, body] + | some kw => + let sigExpr ← mkAppM ``Source.sigPointerFree #[inputs, output] + let propExpr ← mkAppM ``Eq #[sigExpr, mkConst ``Bool.true] + let proof ← + try + Lean.Meta.mkDecideProof propExpr + catch _ => + throw $ .error kw + "Public (entry) function signatures cannot contain pointer types" + mkAppM ``Source.Function.monoEntry #[name, inputs, output, body, proof] declare_syntax_cat aiur_declaration syntax aiur_function : aiur_declaration diff --git a/Ix/Aiur/Stages/Source.lean b/Ix/Aiur/Stages/Source.lean index 19fb7e04..e44283ef 100644 --- a/Ix/Aiur/Stages/Source.lean +++ b/Ix/Aiur/Stages/Source.lean @@ -322,6 +322,23 @@ theorem eq_of_beq {a b : Typ} (h : beq a b = true) : a = b := by have hk : k < tl.length := by simp [List.length] at h; omega exact ihTl.2 k hk t' hb +/-- Does `t` contain any `.pointer` subterm? Used to forbid pointer types in +the signatures of `entry = true` (public) functions. -/ +def hasPointer : Typ → Bool + | .unit | .field | .ref _ | .mvar _ => false + | .pointer _ => true + | .tuple ts => ts.attach.any fun ⟨t, _⟩ => hasPointer t + | .array t _ => hasPointer t + | .app _ args => args.attach.any fun ⟨t, _⟩ => hasPointer t + | .function ins out => + hasPointer out || ins.attach.any fun ⟨t, _⟩ => hasPointer t +termination_by t => sizeOf t +decreasing_by + all_goals first + | decreasing_tactic + | (have := Array.sizeOf_lt_of_mem ‹_ ∈ _›; grind) + | (have := List.sizeOf_lt_of_mem ‹_ ∈ _›; grind) + end Typ instance : BEq Typ := ⟨Typ.beq⟩ @@ -414,6 +431,11 @@ structure TypeAlias where namespace Source +/-- `true` iff none of `inputs` nor `output` contain a `.pointer` subterm. +Used to enforce that public entry functions expose no pointer-typed values. -/ +def sigPointerFree (inputs : List (Local × Typ)) (output : Typ) : Bool := + !output.hasPointer && inputs.all (fun ⟨_, t⟩ => !t.hasPointer) + structure Function where name : Global params : List String @@ -421,7 +443,43 @@ structure Function where output : Typ body : Term entry : Bool - deriving Repr, Inhabited + /-- Polymorphic public entry points are forbidden by construction: + either the function is monomorphic (`params = []`) or not public + (`entry = false`). -/ + entryMonomorphic : params = [] ∨ entry = false := by + first | exact Or.inl rfl | exact Or.inr rfl + /-- Public entry points cannot expose pointer-typed values: either the + signature is pointer-free or the function is not public (`entry = false`). -/ + entryPointerFree : sigPointerFree inputs output = true ∨ entry = false := by + first | exact Or.inl rfl | exact Or.inr rfl + deriving Repr + +instance : Inhabited Function where + default := + { name := default, params := [], inputs := default, output := default, + body := default, entry := default, + entryMonomorphic := Or.inl rfl, + entryPointerFree := Or.inr rfl } + +/-- Smart constructor for non-entry monomorphic functions. -/ +def Function.monoNonEntry (name : Global) (inputs : List (Local × Typ)) + (output : Typ) (body : Term) : Function := + { name, params := [], inputs, output, body, entry := false, + entryMonomorphic := Or.inl rfl, entryPointerFree := Or.inr rfl } + +/-- Smart constructor for public entry functions. Requires a proof that the +signature contains no pointer types. -/ +def Function.monoEntry (name : Global) (inputs : List (Local × Typ)) + (output : Typ) (body : Term) + (h : sigPointerFree inputs output = true) : Function := + { name, params := [], inputs, output, body, entry := true, + entryMonomorphic := Or.inl rfl, entryPointerFree := Or.inl h } + +/-- Smart constructor for polymorphic functions (`entry = false` forced). -/ +def Function.poly (name : Global) (params : List String) (inputs : List (Local × Typ)) + (output : Typ) (body : Term) : Function := + { name, params, inputs, output, body, entry := false, + entryMonomorphic := Or.inr rfl, entryPointerFree := Or.inr rfl } structure Toplevel where dataTypes : Array DataType