diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 7704d8f..2758ca6 100644 --- a/.github/workflows/ci.yml +++ b/.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 diff --git a/LeanEvalGenerator/Contract.lean b/LeanEvalGenerator/Contract.lean index 0f706dd..9b0a672 100644 --- a/LeanEvalGenerator/Contract.lean +++ b/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 := { diff --git a/LeanEvalGenerator/Main.lean b/LeanEvalGenerator/Main.lean index a45b241..1f280f7 100644 --- a/LeanEvalGenerator/Main.lean +++ b/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 => diff --git a/LeanEvalGenerator/Structured.lean b/LeanEvalGenerator/Structured.lean new file mode 100644 index 0000000..76d398d --- /dev/null +++ b/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" "" + 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 diff --git a/README.md b/README.md index 70103ab..15b594a 100644 --- a/README.md +++ b/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. diff --git a/schemas/request-v2.schema.json b/schemas/request-v2.schema.json new file mode 100644 index 0000000..6d0cfb7 --- /dev/null +++ b/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" +} diff --git a/schemas/response-v2.schema.json b/schemas/response-v2.schema.json new file mode 100644 index 0000000..3746c7e --- /dev/null +++ b/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" + } + } + } + } + } +} diff --git a/tests/Context.lean b/tests/Context.lean index a45ee7f..e4c6d22 100644 --- a/tests/Context.lean +++ b/tests/Context.lean @@ -1,4 +1,4 @@ -import LeanEvalGenerator.Core.Generate +import LeanEvalGenerator.Contract open LeanEvalGenerator.Core @@ -19,6 +19,10 @@ private def expectEq (label actual expected : String) : IO Unit := do s!"{label} mismatch\nexpected:\n{repr expected}\nactual:\n{repr actual}" def main : IO Unit := do + expectEq "empty SHA-256" (← LeanEvalGenerator.sha256 "") + "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855" + expectEq "UTF-8 SHA-256" (← LeanEvalGenerator.sha256 "∀ n : ℕ, n = n\n") + "dc24fa7cb94558b9cdf90e20ca6372130a63a26c9c05640a00aab7e75b8d000a" let erdosStyle := "namespace Fixture\nset_option quotPrecheck false\n\n" ++ "local notation \"A\" => { x : Nat | x = 0 }\nvariable (n : Nat)\n" ++ diff --git a/tests/scripts/contract.py b/tests/scripts/contract.py index f10ee9e..be2f635 100644 --- a/tests/scripts/contract.py +++ b/tests/scripts/contract.py @@ -84,7 +84,7 @@ def main() -> int: wrong_version = invoke( json.dumps( { - "schemaVersion": 2, + "schemaVersion": 99, "contextRoot": ".", "leanToolchain": "leanprover/lean4:v0.0.0\n", "mathlib": {"name": "mathlib", "git": "x", "rev": "y"}, @@ -95,7 +95,7 @@ def main() -> int: ) assert wrong_version.returncode == 1 assert wrong_version.stdout == "" - assert "Unsupported schemaVersion 2; expected 1" in wrong_version.stderr + assert "Unsupported schemaVersion 99; expected 1 or 2" in wrong_version.stderr duplicate_tags = problem() duplicate_tags["tags"] = ["example", "example"] diff --git a/tests/scripts/structured.py b/tests/scripts/structured.py new file mode 100644 index 0000000..c260288 --- /dev/null +++ b/tests/scripts/structured.py @@ -0,0 +1,91 @@ +"""Source-free contract: no context tree or .ilean, including dependent holes.""" +import copy +import hashlib +import json +from pathlib import Path +import tempfile +import tomllib + +from contract import ROOT, invoke +import subprocess + +def run(args, cwd, env=None): + result = subprocess.run(args, cwd=cwd, env=env, text=True, capture_output=True) + if result.returncode: + raise AssertionError(f"{args}:\n{result.stdout}\n{result.stderr}") + return result.stdout.strip() + + +def package(root, name, module, content): + root.mkdir() + (root / "lakefile.toml").write_text( + f'name = "{name}"\n[[lean_lib]]\nname = "{module}"\n' + ) + (root / "lean-toolchain").write_text((ROOT / "lean-toolchain").read_text()) + (root / f"{module}.lean").write_text(content) + run(["git", "init", "-q"], root) + run(["git", "add", "."], root) + run(["git", "-c", "user.name=Fixture", "-c", "user.email=fixture@example.invalid", + "commit", "-qm", "fixture"], root) + return {"name": name, "git": str(root), "rev": run(["git", "rev-parse", "HEAD"], root)} + + + + +def main(): + with tempfile.TemporaryDirectory() as directory: + root = Path(directory) + support = package(root / 'support', 'fixture_support', 'FixtureSupport', + 'def FixtureSupport.value : Nat := 7\n') + request = {'schemaVersion': 2, 'enableNanoda': True, 'leanToolchain': (ROOT / 'lean-toolchain').read_text(), + 'dependencies': [support], 'templates': {'workspaceTest': 'def main : IO Unit := pure ()\n'}, + 'problems': [{'id': 'structured', 'title': 'Structured fixtures', + 'imports': ['FixtureSupport'], 'declarations': [ + {'name': 'answer', 'kind': 'def', 'type': 'Nat', 'levels': []}, + {'name': 'second', 'kind': 'def', 'type': 'Fin (answer + 1)', 'levels': []}, + {'name': 'problem', 'kind': 'theorem', + 'type': 'answer = FixtureSupport.value ∧ second.val ≤ answer', 'levels': []}, + {'name': 'poly', 'kind': 'theorem', + 'type': '∀ (α : Type u) (x : α), x = x', 'levels': ['u']}]}]} + result = invoke(json.dumps(request)) + assert result.returncode == 0, result.stderr + assert invoke(json.dumps(request)).stdout == result.stdout + response = json.loads(result.stdout) + assert response['schemaVersion'] == 2 + files = {f['path']: f['content'] for f in response['files']} + for f in response['files']: + assert hashlib.sha256(f['content'].encode()).hexdigest() == f['sha256'] + assert tomllib.loads(files['lakefile.toml'])['require'] == [support] + assert not any('Deps' in name or name.endswith('.ilean') for name in files) + workspace = root / 'workspace' + workspace.mkdir() + for name, content in files.items(): + p = workspace / name + p.parent.mkdir(parents=True, exist_ok=True) + p.write_text(content) + submission = workspace / 'Submission.lean' + text = submission.read_text() + for proof in ['exact 7', 'exact ⟨0, by decide⟩', 'constructor <;> decide', 'intro α x; rfl']: + text = text.replace('sorry', proof, 1) + submission.write_text(text) + run(['lake', 'update'], workspace) + run(['lake', 'build', 'Challenge', 'Solution'], workspace) + mutations = [ + lambda r: r.update(contextRoot='unused'), + lambda r: r['dependencies'][0].update(rev='master'), + lambda r: r['dependencies'].append(r['dependencies'][0]), + lambda r: r['problems'][0].update(imports=['FixtureSupport\naxiom bad : False']), + lambda r: r['problems'][0]['declarations'][0].update(name='../bad'), + lambda r: r['problems'][0]['declarations'][0].update(kind='axiom'), + lambda r: r['problems'][0]['declarations'][0].update(levels=['u\naxiom bad : False']), + lambda r: r['problems'][0]['declarations'].append(r['problems'][0]['declarations'][0]), + ] + for mutation in mutations: + bad = copy.deepcopy(request) + mutation(bad) + assert invoke(json.dumps(bad)).returncode != 0, bad + print('PASS structured rendering, real Git dependencies, dependent holes, universes, malformed requests') + + +if __name__ == '__main__': + main()