GraphQL · Lean · Rust
Duckki Oe
A Rust Engineer’s Guide to Lean ↗GraphQL/*.lean translates the English GraphQL specificationstructure FieldDefinition where
name : Name
outputType : TypeRef
arguments : List InputValueDefinition := []
structure InputValueDefinition where
name : Name
inputType : TypeRef
defaultValue : Option ConstInputValue := none
inductive TypeRef where
| named : Name -> TypeRef
| list : TypeRef -> TypeRef
| nonNull : TypeRef -> TypeRef
structure FieldDefinition where
name : Name
outputType : TypeRef
arguments : List InputValueDefinition := []
structure InputValueDefinition where
name : Name
inputType : TypeRef
defaultValue : Option ConstInputValue := none
inductive TypeRef where
| named : Name -> TypeRef
| list : TypeRef -> TypeRef
| nonNull : TypeRef -> TypeRef
structure FieldDefinition where
name : Name
outputType : TypeRef
arguments : List InputValueDefinition := []
structure InputValueDefinition where
name : Name
inputType : TypeRef
defaultValue : Option ConstInputValue := none
inductive TypeRef where
| named : Name -> TypeRef
| list : TypeRef -> TypeRef
| nonNull : TypeRef -> TypeRef
users(limit: Int = 10): [User!]!
def usersField : FieldDefinition :=
{ name := "users"
outputType := .nonNull (.list (.nonNull (.named "User")))
arguments :=
[{ name := "limit", inputType := .named "Int",
defaultValue := some (.int 10) }] }
Option separates absent defaults from explicit nullstructure Operation where
name : Option Name := none
operationType : OperationType := .query
variableDefinitions :
List VariableDefinition := []
selectionSet : List Selection
structure VariableDefinition where
name : Name
typeRef : TypeRef
defaultValue : Option ConstInputValue := none
inductive Selection where
| field
(responseName : Name)
(fieldName : Name)
(arguments : List Argument)
(directives : List DirectiveApplication)
(selectionSet : List Selection)
| inlineFragment
(typeCondition : Option Name)
(directives : List DirectiveApplication)
(selectionSet : List Selection)
structure Operation where
name : Option Name := none
operationType : OperationType := .query
variableDefinitions :
List VariableDefinition := []
selectionSet : List Selection
structure VariableDefinition where
name : Name
typeRef : TypeRef
defaultValue : Option ConstInputValue := none
inductive Selection where
| field
(responseName : Name)
(fieldName : Name)
(arguments : List Argument)
(directives : List DirectiveApplication)
(selectionSet : List Selection)
| inlineFragment
(typeCondition : Option Name)
(directives : List DirectiveApplication)
(selectionSet : List Selection)
... on User { name id @include(if: $withId) }
def userSelection : Selection :=
.inlineFragment (some "User") []
[.field "name" "name" [] [] [],
.field "id" "id" [] [.include (.variable "withId")] []]
def operationDefinitionValid (schema : Schema) (operation : Operation) : Prop :=
operation.operationType = .query
∧ schema.isCompositeType (operation.rootType schema)
∧ variableDefinitionsValid schema operation.variableDefinitions
∧ operation.selectionSet ≠ []
∧ selectionSetValid schema operation.variableDefinitions
(operation.rootType schema) operation.selectionSet
∧ FieldMerge.fieldsInSetCanMerge schema (operation.rootType schema)
operation.selectionSet
∧ operationVariablesUsed operation
query Larger { users { id name } }
query Smaller { users { id } }
Which direction holds?
query Larger { users { id name } }
query Smaller { users { id } }
Larger includes Smaller. Smaller does not include Larger.
query Left {
node(id: "42") {
id
name
}
}
query Right($withId: Boolean!) {
node(id: "42") {
... on User {
name
id @include(if: $withId)
}
}
}
query Left {
node(id: "42") {
id
name
}
}
query Right($withId: Boolean!) {
node(id: "42") {
... on User {
name
id @include(if: $withId)
}
}
}
Left includes Right. Right does not include Left.
query Left {
node(id: "42") {
id
name
}
}
query Right($withId: Boolean!) {
node(id: "42") {
... on User {
name
id @include(if: $withId)
}
}
}
| Concrete node type | Right selects name | Right selects id | Left covers it |
|---|---|---|---|
| User, withId = true | yes | yes | yes |
| User, withId = false | yes | no | yes |
| Team, either value | no | no | yes |
includes schema left right: left covers every right-selected pathstructure FieldHead where
fieldName : Name
arguments : List Argument
outputType : TypeRef
structure PathStep where
parentObject : Name
responseName : Name
field : FieldHead
Concrete path Query.node → User.id
| Step | Concrete parent | Response name | Field | Arguments | Output |
|---|---|---|---|---|---|
| 1 | Query | node | node | id = "42" | Node |
| 2 | User | id | id | none | ID! |
structure FieldHead where
fieldName : Name
arguments : List Argument
outputType : TypeRef
structure PathStep where
parentObject : Name
responseName : Name
field : FieldHead
Concrete path Query.node → User.id
| Step | Concrete parent | Response name | Field | Arguments | Output |
|---|---|---|---|---|---|
| 1 | Query | node | node | id = "42" | Node |
| 2 | User | id | id | none | ID! |
def collectedFieldsSelectPath (schema : Schema) (variableValues : VariableValues)
(groupedFields : List (Name × List ExecutableField))
(path : List PathStep) : Prop :=
match path with
| [] => False
| [step] =>
∃ fields,
(step.responseName, fields) ∈ groupedFields
∧ ∃ field, field ∈ fields ∧ executableFieldMatchesPathStep schema field step
| step :: next :: rest =>
∃ fields,
(step.responseName, fields) ∈ groupedFields
∧ (∃ field, field ∈ fields ∧ executableFieldMatchesPathStep schema field step)
∧ schema.typeIncludesObject step.field.outputType.namedType next.parentObject
∧ collectedFieldsSelectPath schema variableValues
(collectSubfields schema variableValues next.parentObject
(.object next.parentObject PUnit.unit) fields)
(next :: rest)
Match this stepCheck next object typeFollow the suffix
def collectedFieldsSelectPath (schema : Schema) (variableValues : VariableValues)
(groupedFields : List (Name × List ExecutableField))
(path : List PathStep) : Prop :=
match path with
| [] => False
| [step] =>
∃ fields,
(step.responseName, fields) ∈ groupedFields
∧ ∃ field, field ∈ fields ∧ executableFieldMatchesPathStep schema field step
| step :: next :: rest =>
∃ fields,
(step.responseName, fields) ∈ groupedFields
∧ (∃ field, field ∈ fields ∧ executableFieldMatchesPathStep schema field step)
∧ schema.typeIncludesObject step.field.outputType.namedType next.parentObject
∧ collectedFieldsSelectPath schema variableValues
(collectSubfields schema variableValues next.parentObject
(.object next.parentObject PUnit.unit) fields)
(next :: rest)
Match this stepCheck next object typeFollow the suffix
def collectedFieldsSelectPath (schema : Schema) (variableValues : VariableValues)
(groupedFields : List (Name × List ExecutableField))
(path : List PathStep) : Prop :=
match path with
| [] => False
| [step] =>
∃ fields,
(step.responseName, fields) ∈ groupedFields
∧ ∃ field, field ∈ fields ∧ executableFieldMatchesPathStep schema field step
| step :: next :: rest =>
∃ fields,
(step.responseName, fields) ∈ groupedFields
∧ (∃ field, field ∈ fields ∧ executableFieldMatchesPathStep schema field step)
∧ schema.typeIncludesObject step.field.outputType.namedType next.parentObject
∧ collectedFieldsSelectPath schema variableValues
(collectSubfields schema variableValues next.parentObject
(.object next.parentObject PUnit.unit) fields)
(next :: rest)
Match this stepCheck next object typeFollow the suffix
def includes (schema : Schema) (left right : Operation) : Prop :=
sharedVariableDefinitionsSyntacticallyCompatible left.variableDefinitions
right.variableDefinitions
∧ ∀ (assignment : BoolCase),
boolVarsComplete
(comparisonConditionVariables left.selectionSet right.selectionSet)
(boolCaseVariableValues assignment)
-> ∀ path,
ResponsePath.operationSelectsPath schema right assignment path
-> ResponsePath.operationSelectsPath schema left assignment path
Right-selected → left-selectedEvery Boolean assignmentCompatible shared declarations
Every path selected by right must also be selected by left.
def includes (schema : Schema) (left right : Operation) : Prop :=
sharedVariableDefinitionsSyntacticallyCompatible left.variableDefinitions
right.variableDefinitions
∧ ∀ (assignment : BoolCase),
boolVarsComplete
(comparisonConditionVariables left.selectionSet right.selectionSet)
(boolCaseVariableValues assignment)
-> ∀ path,
ResponsePath.operationSelectsPath schema right assignment path
-> ResponsePath.operationSelectsPath schema left assignment path
Right-selected → left-selectedEvery Boolean assignmentCompatible shared declarations
Check every relevant Boolean assignment; supply all variables used by directives.
def includes (schema : Schema) (left right : Operation) : Prop :=
sharedVariableDefinitionsSyntacticallyCompatible left.variableDefinitions
right.variableDefinitions
∧ ∀ (assignment : BoolCase),
boolVarsComplete
(comparisonConditionVariables left.selectionSet right.selectionSet)
(boolCaseVariableValues assignment)
-> ∀ path,
ResponsePath.operationSelectsPath schema right assignment path
-> ResponsePath.operationSelectsPath schema left assignment path
Right-selected → left-selectedEvery Boolean assignmentCompatible shared declarations
def includes (schema : Schema) (left right : Operation) : Prop :=
sharedVariableDefinitionsSyntacticallyCompatible left.variableDefinitions
right.variableDefinitions
∧ ∀ (assignment : BoolCase),
boolVarsComplete
(comparisonConditionVariables left.selectionSet right.selectionSet)
(boolCaseVariableValues assignment)
-> ∀ path,
ResponsePath.operationSelectsPath schema right assignment path
-> ResponsePath.operationSelectsPath schema left assignment path
Right-selected → left-selectedEvery Boolean assignmentCompatible shared declarations
def includesBoolReference (schema : Schema) (left right : Operation) : Bool :=
if left.rootType schema == right.rootType schema
&& sharedVariableDefinitionsSyntacticallyCompatibleBool left.variableDefinitions
right.variableDefinitions then
let parentType := right.rootType schema
let variables := comparisonConditionVariables left.selectionSet right.selectionSet
let fuel := right.size + 1
booleanVariableAssignments variables
|>.all
fun variableValues =>
selectionSetIncludesBoolWithFuel schema fuel parentType
variableValues left.selectionSet right.selectionSet
else
false
lines, including local helpers
First AI implementation of an inclusion decision procedure
includesdef IncludesBoolReferenceSound (schema : Schema) (left right : Operation) : Prop :=
SchemaWellFormedness.schemaWellFormed schema
-> Validation.operationDefinitionValid schema left
-> Validation.operationDefinitionValid schema right
-> includesBoolReference schema left right = true
-> includes schema left right
def IncludesBoolReferenceComplete (schema : Schema) (left right : Operation) : Prop :=
SchemaWellFormedness.schemaWellFormed schema
-> Validation.operationDefinitionValid schema left
-> Validation.operationDefinitionValid schema right
-> includes schema left right
-> includesBoolReference schema left right = true
Under these assumptions, acceptance and inclusion are equivalent.
def IncludesBoolReferenceSound (schema : Schema) (left right : Operation) : Prop :=
SchemaWellFormedness.schemaWellFormed schema
-> Validation.operationDefinitionValid schema left
-> Validation.operationDefinitionValid schema right
-> includesBoolReference schema left right = true
-> includes schema left right
def IncludesBoolReferenceComplete (schema : Schema) (left right : Operation) : Prop :=
SchemaWellFormedness.schemaWellFormed schema
-> Validation.operationDefinitionValid schema left
-> Validation.operationDefinitionValid schema right
-> includes schema left right
-> includesBoolReference schema left right = true
Under these assumptions, acceptance and inclusion are equivalent.
def IncludesBoolReferenceSound (schema : Schema) (left right : Operation) : Prop :=
SchemaWellFormedness.schemaWellFormed schema
-> Validation.operationDefinitionValid schema left
-> Validation.operationDefinitionValid schema right
-> includesBoolReference schema left right = true
-> includes schema left right
def IncludesBoolReferenceComplete (schema : Schema) (left right : Operation) : Prop :=
SchemaWellFormedness.schemaWellFormed schema
-> Validation.operationDefinitionValid schema left
-> Validation.operationDefinitionValid schema right
-> includes schema left right
-> includesBoolReference schema left right = true
Under these assumptions, acceptance and inclusion are equivalent.
Definition or premise change: propose a diff for human approval.
Proof-only task: edit Proofs/; keep definitions and statements frozen.
theorem includesBoolReference_sound {schema : Schema} {left right : Operation}
: IncludesBoolReferenceSound schema left right := by
intro hschema hleft hright hcheck
obtain ⟨hroot, hdefinitions, hchecks⟩ :=
includesBoolReference_to_selectionSetChecks hcheck
apply includes_of_complete_reference_checks hschema hleft hright hroot
· exact of_decide_eq_true hdefinitions
· intro assignment _hcomplete
exact hchecks (boolCaseVariableValues assignment)
theorem includesBoolReference_sound {schema : Schema} {left right : Operation}
: IncludesBoolReferenceSound schema left right := by
intro hschema hleft hright hcheck
obtain ⟨hroot, hdefinitions, hchecks⟩ :=
includesBoolReference_to_selectionSetChecks hcheck
apply includes_of_complete_reference_checks hschema hleft hright hroot
· exact of_decide_eq_true hdefinitions
· intro assignment _hcomplete
exact hchecks (boolCaseVariableValues assignment)
Illustrative exchange
Define query inclusion so every selection in one query also occurs in the other query.
AI: Compare response names alone, or preserve field identity and arguments?
Preserve field provenance. Every right-selected path must be left-selected under every relevant Boolean assignment.
Human: Check the examples and direction; approve the specification.
Illustrative exchange
Define query inclusion so every selection in one query also occurs in the other query.
AI: Compare response names alone, or preserve field identity and arguments?
Preserve field provenance. Every right-selected path must be left-selected under every relevant Boolean assignment.
Human: Check the examples and direction; approve the specification.
Illustrative exchange
Implement a checker deciding includes; propose soundness and completeness.AI: The claims assume a well-formed schema and valid operations.
Our caller establishes those conditions. It's reasonable to assume them.
Human: Approve the domain and correctness statements; freeze the definitions.
Prove the frozen statements; report counterexamples or unresolved obligations.
AI: Return checked proofs, or explain a separate proposal to revise the specification, premises, or code.
Illustrative exchange
Implement a checker deciding includes; propose soundness and completeness.AI: The claims assume a well-formed schema and valid operations.
Our caller establishes those conditions. It's reasonable to assume them.
Human: Approve the domain and correctness statements; freeze the definitions.
Prove the frozen statements; report counterexamples or unresolved obligations.
AI: Return checked proofs, or explain a separate proposal to revise the specification, premises, or code.
Illustrative exchange
Implement a checker deciding includes; propose soundness and completeness.AI: The claims assume a well-formed schema and valid operations.
Our caller establishes those conditions. It's reasonable to assume them.
Human: Approve the domain and correctness statements; freeze the definitions.
Prove the frozen statements; report counterexamples or unresolved obligations.
AI: Return checked proofs, or explain a separate proposal to revise the specification, premises, or code.
Propose an algorithmic refinement that avoids redundant work.
Human: Skim the proposed algorithm and approve promising definition changes.
Rebuild the correctness proofs without changing those definitions.
Human: Evaluate the proved refinement. Repeat if useful; this step is optional.
Propose an algorithmic refinement that avoids redundant work.
Human: Skim the proposed algorithm and approve promising definition changes.
Rebuild the correctness proofs without changing those definitions.
Human: Evaluate the proved refinement. Repeat if useful; this step is optional.
Reviewed meaning → approved definitions → checked proof.
A definition change returns through review before proof work resumes.
Lean agent: Write a porting guide for includesBoolReference.Human: Review the guide’s executable dependencies, representations, and assumptions.
Rust agent: Implement includesBoolReference in Rust using this guide.Human: Review API integration, representations, and modeled preconditions.
Lean agent: Write a porting guide for includesBoolReference.Human: Review the guide’s executable dependencies, representations, and assumptions.
Rust agent: Implement includesBoolReference in Rust using this guide.Human: Review API integration, representations, and modeled preconditions.
Build a differential fuzz harness for Rust against the Lean oracle.
AI: Run campaigns; shrink mismatches, repair, and retain regressions.
Human: Review the domain, oracle protocol, test cases, and coverage.
Build a differential fuzz harness for Rust against the Lean oracle.
AI: Run campaigns; shrink mismatches, repair, and retain regressions.
Human: Review the domain, oracle protocol, test cases, and coverage.
Profile this Rust implementation using representative workloads. Separate Rust-only changes from algorithm changes requiring a Lean update.
AI: Profile a release build and report hotspots.
Human: Check the workload and review a proposal before changing Lean.
Profile this Rust implementation using representative workloads. Separate Rust-only changes from algorithm changes requiring a Lean update.
AI: Profile a release build and report hotspots.
Human: Check the workload and review a proposal before changing Lean.
Review this Rust optimization proposal and refine the Lean implementation.
Human: Approve the behavior to preserve and proof obligation; freeze the Lean diff.
Rebuild the proofs against the approved definitions.
Counterexample: reject. Unresolved: investigate. After proof: updated Rust + comparison and profile reports.
Review this Rust optimization proposal and refine the Lean implementation.
Human: Approve the behavior to preserve and proof obligation; freeze the Lean diff.
Rebuild the proofs against the approved definitions.
Counterexample: reject. Unresolved: investigate. After proof: updated Rust + comparison and profile reports.
The cursor becomes a red laser pointer over slide content. Links and controls keep their normal cursor.
URLs keep the slide and reveal, for example #05/2. Use browser printing to export final slide states.