graphql-lean

graphql-lean is a GraphQL formalization in Lean, based on the GraphQL September 2025 Edition.

Compared with prior theorem-prover formalizations such as GraphCoQL, this development fills important gaps in the formal treatment of GraphQL. Notably, it models @skip / @include directives, null bubbling, execution errors up to error counts, and named fragments. It also includes verified algorithmic alternatives to the spec executor and a directive-aware normalization theory.

Highlights

• GraphQL/ contains the public formal model of the scoped GraphQL 2025 spec: schema syntax and well-formedness, operation syntax, validation, execution, named fragments, execution algorithms, and public theory definitions.
• ExecutionCancelingSiblings verifies a spec-style executor that cancels sibling response positions after null bubbling.
• ExecutionUngrouped models a lightweight syntax-order execution that avoids building the collected field map, caches field results and retained composite sources by response position, and has checked preservation witnesses. Its uncached specialization is also verified for resolvers that are cheap to call repeatedly.
• ExecutionBreadth verifies a breadth-first execution model with vectorized resolver calls, inspired by gmac/graphql-breadth-js, against the spec-facing executor.
• NormalForm provides ground-type and complete normalization. Complete normalization supports modeled @skip / @include directives, unlike the earlier paper/Coq normalizers, and its canonicity theorems prove that semantic equivalence of operations can be reduced to comparison of normal forms.
• QueryInclusion provides a verified, condition-aware decision procedure for recursive response inclusion that preserves resolver-call provenance.
• TreeSummary provides fast syntactic and exact-case folds over feasible condition trees. Generic framework theorems lift local algebra obligations to execution soundness, while the exact backend also supports opt-in structural least-bound proofs.
• StaticCost performs IBM GraphQL Cost Directives static analysis over condition trees, with an external model for the custom directive metadata omitted from the core schema syntax. It reports separate type and field costs, and its execution-level proof bounds query-response cost when the completed response respects the model's list-size estimates.

GraphQL Layout

The public model is rooted at GraphQL.lean, which imports the definition surfaces below.

• GraphQL/Schema.lean: GraphQL type-system syntax, type references, lookup, possible-object helpers, default-value validity, and interface implementation compatibility helpers.
• GraphQL/SchemaWellFormedness.lean: schema well-formedness predicates for the modeled fragment.
• GraphQL/Operation.lean: core operation syntax, variable definitions, selections, inline fragments, and modeled directive applications.
• GraphQL/Validation.lean: operation validation predicates, including field validity, argument validity, variable-use checks, selection-shape checks, fragment applicability, and merge compatibility.
• GraphQL/Execution.lean: resolver-parametric spec-compliant execution with operation-variable defaults, schema-derived resolver argument maps, field collection, completion, null bubbling, and response envelopes containing data plus execution-error counts.
• GraphQL/NamedFragment/: fragment-aware operation syntax, validation, execution, translation, and inlining support.
• GraphQL/Algorithms/: non-spec execution algorithms, including sibling-canceling execution, source-caching and uncached ungrouped execution, and breadth-first execution.
• GraphQL/Theories/: public project theories, currently including normal forms, annotated execution, selection-condition extraction, and query inclusion, condition-tree extraction and interpretation, and compositional tree summaries.

Proof witnesses are under Proofs/. Ordinary tests are under Tests/GraphQL/, and generated or fixture-driven conformance tests are under Tests/Conformance/.

Build

lake build

Documentation

• docs/overview.md: module map and architecture overview.
• docs/spec-conformance.md: implemented spec-conformance scope and out-of-scope boundaries.
• docs/algorithms.md: algorithmic alternatives to the spec-facing executor and their proof status.
• docs/theories/query-inclusion.md: query-inclusion semantics, correctness domain, checker design, and proof structure.
• docs/theories/normal-form.md: normal-form definitions and preservation theorems.
• docs/theories/normal-form-uniqueness.md: canonicity and semantic-equivalence results for normal forms.
• docs/theories/condition-tree.md: condition-tree extraction, execution, reduction, and proof witnesses.
• docs/theories/tree-summary.md: contextual summary folds, annotated-response soundness, and the MaxResponseSize example.
• docs/theories/tree-summary-factorization.md: implementation and soundness argument for factorizing the fast syntactic backend's branch cases.
• docs/theories/static-cost.md: static cost and list-size model, cost rule, and tree-summary entry points.
• docs/development.md: developer guide.