Render structured declarations with pinned package dependencies

.github/workflows/ci.yml

@@ -42,3 +42,6 @@ jobs:
 
       - name: Check Python test harnesses
         run: python3 -m py_compile tests/scripts/*.py
+
+      - name: Test structured declaration contract
+        run: python3 tests/scripts/structured.py

LeanEvalGenerator/Contract.lean

@@ -81,16 +81,16 @@ private def validateRequest (request : GenerateRequest) : IO Unit := do
       throw <| IO.userError s!"Duplicate problem id `{problem.id}`."
     problemIds := problemIds.push problem.id
 
-private def sha256 (content : String) : IO String := do
+def sha256 (content : String) : IO String := do
   let out ← IO.Process.output {
-    cmd := "sha256sum"
-    args := #["-"]
+    cmd := "openssl"
+    args := #["dgst", "-sha256", "-r"]
   } (some content)
   if out.exitCode != 0 then
-    throw <| IO.userError s!"sha256sum failed: {out.stderr.trimAscii.toString}"
+    throw <| IO.userError s!"openssl SHA-256 failed: {out.stderr.trimAscii.toString}"
   let digest := (out.stdout.splitOn " ").head!.trimAscii.toString
-  if digest.length != 64 then
-    throw <| IO.userError "sha256sum returned an invalid digest."
+  if digest.length != 64 || !digest.toList.all (fun c => c.isDigit || (c >= 'a' && c <= 'f')) then
+    throw <| IO.userError "openssl returned an invalid SHA-256 digest."
   return digest
 
 private def metadata (problem : ProblemInput) : LeanEvalGenerator.Core.EvalProblemMetadata := {

LeanEvalGenerator/Main.lean

@@ -1,4 +1,4 @@
-import LeanEvalGenerator.Contract
+import LeanEvalGenerator.Structured
 
 namespace LeanEvalGenerator
 
@@ -14,10 +14,16 @@ private def readRequest : List String → IO String
 def run (args : List String) : IO UInt32 := do
   try
     let payload ← readRequest args
-    let request ← match parseRequest payload with
-      | .ok request => pure request
-      | .error error => throw <| IO.userError s!"Invalid generator request: {error}"
-    let response ← render request
+    let value ← IO.ofExcept <| (Lean.Json.parse payload).mapError ("Invalid generator request: " ++ ·)
+    let version ← IO.ofExcept <| (value.getObjValAs? Nat "schemaVersion").mapError ("Invalid generator request: " ++ ·)
+    unless version == 1 || version == 2 do
+      throw <| IO.userError s!"Unsupported schemaVersion {version}; expected 1 or 2."
+    let response ← if version == 2 then do
+      let request ← IO.ofExcept <| (Structured.parse value).mapError ("Invalid generator request: " ++ ·)
+      Structured.render request
+    else do
+      let request ← IO.ofExcept <| (parseRequest payload).mapError ("Invalid generator request: " ++ ·)
+      render request
     IO.print response
     return 0
   catch error =>

LeanEvalGenerator/Structured.lean

@@ -0,0 +1,134 @@
+import LeanEvalGenerator.Contract
+
+/-! A source-free renderer for closed declaration signatures. No source slices,
+`.ilean` files, dependency discovery, or namespace reconstruction are used. -/
+namespace LeanEvalGenerator.Structured
+open Lean
+
+structure Declaration where
+  name : String
+  kind : String
+  type : String
+  levels : Array String
+  deriving FromJson, ToJson
+
+structure Problem where
+  id : String
+  title : String
+  imports : Array String
+  declarations : Array Declaration
+  deriving FromJson
+
+structure Request where
+  schemaVersion : Nat
+  leanToolchain : String
+  enableNanoda : Bool
+  dependencies : Array DependencyPin
+  templates : TemplateInputs
+  problems : Array Problem
+  deriving FromJson
+
+private def exactFields (value : Json) (fields : List String) : Except String Unit := do
+  let object ← value.getObj?
+  unless object.size == fields.length && object.all (fun k _ => fields.contains k) do
+    throw "Unexpected or missing structured request fields"
+
+def parse (value : Json) : Except String Request := do
+  exactFields value ["schemaVersion", "leanToolchain", "enableNanoda", "dependencies", "templates", "problems"]
+  exactFields (← value.getObjVal? "templates") ["workspaceTest"]
+  for d in (← value.getObjValAs? (Array Json) "dependencies") do
+    exactFields d ["name", "git", "rev"]
+  for p in (← value.getObjValAs? (Array Json) "problems") do
+    exactFields p ["id", "title", "imports", "declarations"]
+    for d in (← p.getObjValAs? (Array Json) "declarations") do
+      exactFields d ["name", "kind", "type", "levels"]
+  fromJson? value
+
+private def identifier (s : String) : Bool :=
+  !s.isEmpty && (s.toList.head!.isAlpha || s.startsWith "_") &&
+    s.toList.all (fun c => c.toNat < 128 && (c.isAlphanum || c == '_'))
+
+private def require (condition : Bool) (message : String) : IO Unit :=
+  unless condition do throw <| IO.userError message
+
+private def validate (r : Request) : IO Unit := do
+  require (r.schemaVersion == 2) "Expected schemaVersion 2"
+  require (!r.leanToolchain.trimAscii.isEmpty && !r.problems.isEmpty) "Empty toolchain or problems"
+  let mut packages := #[]
+  for d in r.dependencies do
+    require (identifier (d.name.replace "-" "_") && !packages.contains d.name)
+      "Invalid or duplicate package name"
+    require (!d.git.isEmpty && d.rev.length == 40 && d.rev.toList.all
+      (fun c => c.isDigit || ('a' ≤ c && c ≤ 'f'))) "Expected package URL and full lowercase commit SHA"
+    packages := packages.push d.name
+  let mut ids := #[]
+  for p in r.problems do
+    require (identifier p.id && !ids.contains p.id && !p.title.isEmpty) "Invalid or duplicate problem id"
+    ids := ids.push p.id
+    require (!p.imports.isEmpty && !p.declarations.isEmpty) "Empty imports or declarations"
+    -- Use Lean's parser to validate syntax boundaries, never an approximate lexer.
+    for name in p.imports do
+      let ctx := Parser.mkInputContext s!"import {name}\n" "<structured import>"
+      let (header, state, messages) ← Parser.parseHeader ctx
+      let imports := Elab.HeaderSyntax.imports header (includeInit := false)
+      require (!messages.hasErrors && ctx.atEnd state.pos && imports.size == 1 &&
+        imports[0]!.module.toString == name.toName.toString) "Invalid module import"
+    let mut names := #[]
+    for d in p.declarations do
+      require (identifier d.name && !names.contains d.name) "Invalid or duplicate declaration name"
+      names := names.push d.name
+      require (d.kind == "def" || d.kind == "theorem") "Expected def or theorem"
+      require (d.levels.all identifier && d.levels.toList.eraseDups.length == d.levels.size)
+        "Invalid universe parameters"
+      -- Type syntax belongs to the producer's Lean environment (which may
+      -- provide notation unknown to this renderer). It is trusted input,
+      -- just like v1 moduleContent, and must be validated by the consumer.
+      require (!d.type.trimAscii.isEmpty) "Empty declaration type"
+
+private def levelSuffix (d : Declaration) : String :=
+  if d.levels.isEmpty then "" else ".{" ++ String.intercalate ", " d.levels.toList ++ "}"
+
+private def declaration (d : Declaration) (solution : Bool := false) : String :=
+  let command := if d.kind == "def" then
+    (if solution then "@[reducible] " else "") ++ "noncomputable def" else "theorem"
+  let body := if solution then "@Submission." ++ d.name ++ levelSuffix d else "by\n  sorry"
+  s!"{command} {d.name}{levelSuffix d} : {d.type} := {body}\n\n"
+
+private def workspace (r : Request) (p : Problem) : Array (String × String) := Id.run do
+  let imports := String.join (p.imports.toList.map (fun n => s!"import {n}\n")) ++ "\n"
+  let holes := String.join (p.declarations.toList.map (declaration ·))
+  let challenge := imports ++ holes
+  let submission := imports ++ "import Submission.Helpers\n\nnamespace Submission\n\n" ++
+    holes ++ "end Submission\n"
+  let solution := imports ++ "import Submission\n\n" ++
+    String.join (p.declarations.toList.map (declaration · true))
+  let deps := String.join <| r.dependencies.toList.map fun d =>
+    s!"[[require]]\nname = {d.name.quote}\ngit = {d.git.quote}\nrev = {d.rev.quote}\n\n"
+  let lakefile := s!"name = {p.id.quote}\nversion = \"0.1.0\"\ndefaultTargets = [\"Challenge\", \"Solution\"]\ntestDriver = \"workspace_test\"\n\n" ++
+    deps ++ "[[lean_lib]]\nname = \"Challenge\"\n\n[[lean_lib]]\nname = \"Solution\"\n\n[[lean_lib]]\nname = \"Submission\"\n\n[[lean_exe]]\nname = \"workspace_test\"\nroot = \"WorkspaceTest\"\n"
+  let config := Json.mkObj [
+    ("challenge_module", toJson "Challenge"), ("solution_module", toJson "Solution"),
+    ("theorem_names", toJson (p.declarations.filter (·.kind == "theorem") |>.map (·.name))),
+    ("definition_names", toJson (p.declarations.filter (·.kind == "def") |>.map (·.name))),
+    ("enable_nanoda", toJson r.enableNanoda),
+    ("permitted_axioms", toJson #["propext", "Quot.sound", "Classical.choice"])]
+  return #[("Challenge.lean", challenge), ("Submission.lean", submission),
+    ("Submission/Helpers.lean", imports), ("Solution.lean", solution),
+    ("lakefile.toml", lakefile), ("lean-toolchain", r.leanToolchain.trimAscii.toString ++ "\n"),
+    ("WorkspaceTest.lean", r.templates.workspaceTest), ("config.json", config.pretty ++ "\n"),
+    ("holes.json", (Json.mkObj [("id", toJson p.id),
+      ("declarations", toJson p.declarations)]).pretty ++ "\n"),
+    ("README.md", s!"# {p.title}\n\nFill the holes in Submission.lean. Keep Challenge.lean and Solution.lean unchanged.\nRun `lake test` with the configured Comparator and sandbox.\n")]
+
+/-- Render only the supplied signatures; the consumer must compile the result
+under its pinned imports before publishing it as a challenge. -/
+def render (r : Request) : IO String := do
+  validate r
+  let mut files := #[]
+  for p in r.problems do
+    for (path, content) in workspace r p do
+      files := files.push <| Json.mkObj [("problemId", toJson p.id), ("path", toJson path),
+        ("content", toJson content), ("sha256", toJson (← LeanEvalGenerator.sha256 content))]
+  return (Json.mkObj [("schemaVersion", toJson (2 : Nat)), ("files", toJson files)]).pretty ++ "\n"
+
+end LeanEvalGenerator.Structured

README.md

@@ -27,3 +27,29 @@ The consumer owns hole resolution. A consumer resolves declarations under its
 pinned target environment, then passes the resulting ranges and dependency
 data to this renderer. Consumer-specific fixtures and source trees do not
 belong in this foundation package.
+
+## Structured declarations (version 2)
+
+Version 2 accepts package pins, imports, and ordered declarations with `name`,
+`kind`, `type`, and explicit `levels`. It renders Challenge, Submission and Solution
+without a context directory, source ranges, `.ilean`, helper discovery, or source
+rewriting. Definitions in Solution are reducible aliases to the submitted values,
+so later hole types can depend on earlier holes. Signatures contain all binders;
+Solution forwards them with an explicit `@` reference and universe arguments.
+
+The schemas are `schemas/request-v2.schema.json` and `schemas/response-v2.schema.json`.
+Types and the test-driver template are trusted source supplied by the consumer,
+just as moduleContent is trusted in v1. The consumer must validate the signatures
+with its own Lean environment and compile the generated Challenge before use.
+The renderer does not interpret type syntax using its potentially different Lean
+version. Import boundaries are validated with Lean's header parser. Version 1
+remains unchanged; no legacy source-processing path is used for v2 requests.
+
+Run `python3 tests/scripts/structured.py` to exercise real Git package resolution,
+dependent definition holes, polymorphic theorems, deterministic output and invalid
+request rejection, without any source context or compiler metadata.
+
+The renderer requires `openssl` on `PATH` for SHA-256 file digests (macOS and Linux);
+GNU `sha256sum` is not required. Deploy a reviewed generator revision built with its
+pinned Lean toolchain, and record the executable digest alongside the source revision.
+The wire schema version identifies the contract, not the executable provenance.

schemas/request-v2.schema.json

@@ -0,0 +1,124 @@
+{
+  "type": "object",
+  "properties": {
+    "schemaVersion": {
+      "const": 2
+    },
+    "leanToolchain": {
+      "type": "string"
+    },
+    "dependencies": {
+      "type": "array",
+      "items": {
+        "type": "object",
+        "properties": {
+          "name": {
+            "type": "string"
+          },
+          "git": {
+            "type": "string"
+          },
+          "rev": {
+            "type": "string",
+            "pattern": "^[0-9a-f]{40}$"
+          }
+        },
+        "required": [
+          "name",
+          "git",
+          "rev"
+        ],
+        "additionalProperties": false
+      }
+    },
+    "templates": {
+      "type": "object",
+      "properties": {
+        "workspaceTest": {
+          "type": "string"
+        }
+      },
+      "required": [
+        "workspaceTest"
+      ],
+      "additionalProperties": false
+    },
+    "problems": {
+      "type": "array",
+      "items": {
+        "type": "object",
+        "properties": {
+          "id": {
+            "type": "string"
+          },
+          "title": {
+            "type": "string"
+          },
+          "imports": {
+            "type": "array",
+            "items": {
+              "type": "string"
+            }
+          },
+          "declarations": {
+            "type": "array",
+            "items": {
+              "type": "object",
+              "properties": {
+                "name": {
+                  "type": "string",
+                  "pattern": "^[A-Za-z_][A-Za-z0-9_]*$"
+                },
+                "kind": {
+                  "enum": [
+                    "def",
+                    "theorem"
+                  ]
+                },
+                "type": {
+                  "type": "string",
+                  "minLength": 1
+                },
+                "levels": {
+                  "type": "array",
+                  "items": {
+                    "type": "string"
+                  }
+                }
+              },
+              "required": [
+                "name",
+                "kind",
+                "type",
+                "levels"
+              ],
+              "additionalProperties": false
+            }
+          }
+        },
+        "required": [
+          "id",
+          "title",
+          "imports",
+          "declarations"
+        ],
+        "additionalProperties": false
+      }
+    },
+    "enableNanoda": {
+      "type": "boolean"
+    }
+  },
+  "required": [
+    "schemaVersion",
+    "leanToolchain",
+    "dependencies",
+    "templates",
+    "problems",
+    "enableNanoda"
+  ],
+  "additionalProperties": false,
+  "$schema": "https://json-schema.org/draft/2020-12/schema",
+  "$id": "request-v2.schema.json",
+  "title": "Structured package-backed workspace request"
+}

schemas/response-v2.schema.json

@@ -0,0 +1,46 @@
+{
+  "$schema": "https://json-schema.org/draft/2020-12/schema",
+  "$id": "response-v2.schema.json",
+  "title": "Structured workspace response",
+  "type": "object",
+  "additionalProperties": false,
+  "required": [
+    "schemaVersion",
+    "files"
+  ],
+  "properties": {
+    "schemaVersion": {
+      "const": 2
+    },
+    "files": {
+      "type": "array",
+      "items": {
+        "type": "object",
+        "additionalProperties": false,
+        "required": [
+          "problemId",
+          "path",
+          "sha256",
+          "content"
+        ],
+        "properties": {
+          "problemId": {
+            "type": "string",
+            "minLength": 1
+          },
+          "path": {
+            "type": "string",
+            "minLength": 1
+          },
+          "sha256": {
+            "type": "string",
+            "pattern": "^[0-9a-f]{64}$"
+          },
+          "content": {
+            "type": "string"
+          }
+        }
+      }
+    }
+  }
+}