Encode entry-function invariants on Source.Function

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

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

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,14 +431,55 @@ 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
   inputs : List (Local × Typ)
   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