graphql-lean-bench

This repository is a proof bench for the GraphQL theory in Lean. Its purpose is to test AI agent's capability of computer science theorem proving.

The main goal is to prove:

GraphQL.NormalForm.groundTypeNormalFormSemanticsPreservation

That proof should be developed without modifying the existing top-level definition files under GraphQL/*.lean. It is fine, and preferred, to add proof modules in GraphQL/Proof/ when the proof needs supporting lemmas.

The editable proof-bench attachment point is:

GraphQL.Proof.groundTypeNormalFormSemanticsPreservation

It contains the public proposition above with a sorry placeholder. Replace that placeholder with the proof, and import any supporting proof modules from GraphQL/Proof.lean.

Bench Rules

• Treat GraphQL/Schema.lean, GraphQL/SchemaWellFormedness.lean, GraphQL/Operation.lean, GraphQL/Validation.lean, GraphQL/Execution.lean, GraphQL/DataModel.lean, and GraphQL/NormalForm.lean as fixed definitions.
• Do not weaken the public theorem statement to make the proof easier.
• Add proof-facing lemmas in new proof modules rather than changing the model.
• Tests and examples may be extended when they clarify expected behavior, but they should not substitute for the preservation proof.

Allowed changes for proof slices:

• GraphQL/Proof.lean,
• new module directories under GraphQL/,
• new tests under Tests/,

Definition Files

The top-level GraphQL library is the definition surface for this bench:

• GraphQL/Schema.lean: schema syntax, input values, constant input values, type references, scalar/object/interface/union/enum/input-object definitions, schema lookup, possible-object semantics, type classification, and subtype checks.
• GraphQL/SchemaWellFormedness.lean: schema well-formedness predicates, including uniqueness, non-empty members, valid type references/defaults, root query object validity, and object/interface implementation compatibility.
• GraphQL/Operation.lean: operation syntax, arguments, variable definitions, modeled @skip/@include directives, selections, inline fragments, response names, field grouping, and selection-set merging helpers.
• GraphQL/Validation.lean: operation validity predicates, including variable and argument checks, recursive input-value checks, directive validation, selection validity, inline-fragment applicability, leaf/composite selection shape, and same-response-name field merge compatibility.
• GraphQL/Execution.lean: bounded execution over abstract resolvers, field collection by response name, directive filtering, field resolution, value completion, and query execution at explicit depth.
• GraphQL/DataModel.lean: graph-backed store model, path-based object identity, field access canonicalization, store well-typedness, store-backed resolvers, and data-model operation equivalence.
• GraphQL/NormalForm.lean: ground-type normal-form predicates, directive-free predicates, normal-form construction, operation equivalence, and the public semantic-preservation statements.
• GraphQL/Proof.lean: editable proof-bench entry point containing the target theorem and its initial sorry.
• GraphQL.lean: sole default build target; it imports the definition modules and then GraphQL/Proof.lean.

Tests

The Tests library provides executable examples and regression coverage for the definitions:

• Tests/Common.lean: shared sample schema and operations.
• Tests/Validation.lean: validation examples, including argument and operation-validity cases.
• Tests/Execution.lean: resolver-based execution examples and response equality helpers.
• Tests/DataModel.lean: graph store examples covering field access, canonical argument comparison, path construction, store well-typedness, and semantic uniqueness conditions.
• Tests/NormalForm.lean: directive-free and normalized-execution smoke checks for the sample operation.
• Tests.lean: aggregate import for the test library.

Run the full project with:

lake build

Spec Conformance And Differences

The reference specification target is the GraphQL September 2025 Edition. This bench models a scoped, query-only GraphQL fragment large enough to state execution and ground-type-normal-form preservation.

Covered or partially covered areas include:

• query operation execution,
• object, interface, union, enum, scalar, input object, list, and non-null type references as represented in the schema model,
• schema well-formedness separated from raw syntax,
• field selection validation, argument validation, variable-use compatibility, leaf/composite selection shape, inline-fragment applicability, and same-response-name merge compatibility,
• modeled @skip and @include directives,
• possible-object semantics for abstract types,
• a graph-backed data model and store-backed resolver interpretation,
• ground-type normal-form construction for field merging and abstract-type grounding.

Intentionally out of scope for this bench:

• mutation and subscription execution,
• named fragment definitions and fragment spreads,
• custom directives and directive definitions beyond the modeled executable directives,
• full input and result coercion,
• scalar and enum coercion details,
• introspection and meta-fields,
• execution errors, request errors, errors, extensions, and null bubbling,
• response serialization details.

Values entering validation and execution are treated as already coerced where scalar semantics would otherwise matter. The proof should make those model boundaries explicit instead of silently relying on broader GraphQL behavior.

Ground Type Normal Form

Ground type normal form is project-specific proof machinery, not a GraphQL spec feature. The concept follows the normal-form line from Hartig and Perez, "Semantics and complexity of GraphQL," WWW 2018: their normal form combines ground-typed selection sets with non-redundancy so that abstract selections are made explicit over concrete object types and repeated response work is removed.

This bench's normalizer rewrites an operation selection set by:

• merging fields that share a response name, using validation facts to justify that the merged field head represents the same executable field group, and
• grounding abstract return types by replacing abstract child selections with inline fragments for the possible concrete object types.

The target theorem states semantic preservation for directive-free operations: under a well-formed schema, a valid operation, and operationDirectiveFree operation, executing the original operation and executing normalizeOperation schema operation produce equivalent results at the same explicit execution depth for all resolver environments, variable values, and source values. Store-backed equivalence over graph data is the separate groundNormalFormCorrect predicate.

Proof Roadmap

The expected proof shape is:

1. Extract validation facts from operationDefinitionValid: root selection-set validity, field lookup validity, child selection validity, merge compatibility, and directive-free consequences.
2. Prove execution collection facts for directive-free selections, especially response-name grouping and inline-fragment traversal behavior.
3. Prove normalizer structural facts: removing grouped fields, collecting matching fields, and preserving response-name coverage.
4. Prove field-merge preservation: the normalized representative field resolves the same field and arguments as the original executable group.
5. Prove abstract branch preservation: possible-object inline fragments select the same runtime object branch as execution over the original abstract selection.
6. Lift selection-set preservation to operation-level executeQueryAtDepth equivalence.

The store-backed data-model statement can then be handled by instantiating the resolver-parametric theorem with DataModel.Store.resolvers.

GraphCoQL Reference

GraphCoQL is the closest known mechanized reference:

• Repository: https://github.com/imfd/GraphCoQL
• Lean port: duckki/GraphCoQL.lean
• Paper: "A Mechanized Formalization of GraphQL", CPP 2020, Tomas Diaz, Federico Olmedo, and Eric Tanter.
• The GraphCoQL paper mechanizes and corrects parts of the normal-form program from Hartig and Perez, "Semantics and complexity of GraphQL," WWW 2018.

Use GraphCoQL as a reference point for the broad proof strategy and for the idea of a ground-typed normal form, not as a proof script to port.

Review Checklist

Before a proof slice is ready for review:

• lake build succeeds.
• rg -n "admit|axiom|unsafe" GraphQL Tests returns no proof-bypass additions.
• rg -n "sorry" GraphQL Tests returns only the intended goal placeholder in GraphQL/Proof.lean, until the proof is complete.
• Top-level definition modules are unchanged unless the change was explicitly requested.
• The public proposition GraphQL.NormalForm.groundTypeNormalFormSemanticsPreservation is not weakened.