Skip to content

Commit 47d2b91

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
docs: add GQL safety model — two-tier architecture with TypeLL levels
GQL maps to the same 10 TypeLL safety levels as VQL-UT. Dependent type features (BoundedNat, NonEmptyString, collection schemas) folded into safety pipeline at L2/L8/L9. Retires "GQL-DT" as a separate concept. GqldtPreview component retained as safety preview visualisation. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent a9527a5 commit 47d2b91

1 file changed

Lines changed: 141 additions & 0 deletions

File tree

‎lithoglyph/docs/gql-safety-model.adoc‎

Lines changed: 141 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,141 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
4+
= GQL Safety Model — Two-Tier Architecture
5+
:toc: left
6+
:toclevels: 3
7+
:sectnums:
8+
9+
== Overview
10+
11+
GQL (Graph Query Language) follows the same two-tier model as VQL:
12+
13+
[cols="1,2,3", options="header"]
14+
|===
15+
| Tier | What | How
16+
17+
| **GQL**
18+
| The query language
19+
| Graph queries with dependent types (`CREATE COLLECTION ... WITH DEPENDENT_TYPES`).
20+
What users write.
21+
22+
| **GQL Safety Pipeline**
23+
| Progressive type safety
24+
| Applies TypeLL's 10 levels behind GQL automatically. Simple queries exit early.
25+
Proof-carrying queries activate L9-L10.
26+
|===
27+
28+
== Relationship to VQL-UT
29+
30+
The 10 safety levels originate in **TypeLL** (the core type theory). VQL-UT is
31+
the reference implementation for database queries. GQL maps its own constructs
32+
to the same 10 levels — it does not have a separate "-UT" repo.
33+
34+
[source]
35+
----
36+
TypeLL (type theory core — defines the 10 levels)
37+
│
38+
├──→ VQL-UT (reference implementation, VeriSimDB)
39+
├──→ KQL (applies same levels, QuandleDB)
40+
└──→ GQL (applies same levels, LithoGlyph)
41+
----
42+
43+
== GQL Safety Levels
44+
45+
[cols="^1,<3,<5", options="header"]
46+
|===
47+
| Level | Name | GQL Mapping
48+
49+
| L1 | Construction Safety | Query injection prevention (safe graph traversal parsing)
50+
| L2 | Schema Pinning | Collection schema checked with dependent types (`BoundedNat`, `NonEmptyString`)
51+
| L3 | Resource Linearity | Graph traversal cursor/connection leak prevention
52+
| L4 | Session Protocols | Query session state machine (connect → traverse → close)
53+
| L5 | Effect Tracking | Side-effect auditing for graph mutations
54+
| L6 | Scope Isolation | Collection namespace boundaries
55+
| L7 | Information Flow | Graph data lineage and provenance tracking
56+
| L8 | Quantitative Bounds | Bounded traversal depth (prevent infinite graph walks)
57+
| L9 | Proof Attachment | Dependent type proofs on collection schemas
58+
| L10 | Cross-Cutting | Composition safety across graph joins and federation
59+
|===
60+
61+
== GQL-Specific Type Features
62+
63+
GQL has dependent types built into its collection definitions:
64+
65+
[cols="<3,^1,<4", options="header"]
66+
|===
67+
| Feature | Level | Description
68+
69+
| Bounded Numeric Types
70+
| L2, L8
71+
| `BoundedNat min max` — numeric fields with compile-time range proofs.
72+
Prevents out-of-range values at the type level.
73+
74+
| Required/Optional Strings
75+
| L2
76+
| `NonEmptyString` vs `Option String` — required fields cannot be null/empty
77+
at the type level.
78+
79+
| Confidence Types
80+
| L9
81+
| `Confidence` type for prompt-scored fields with dependent bounds.
82+
83+
| Provenance Tracking
84+
| L7
85+
| `WITH PROVENANCE_TRACKING` on collections — graph lineage at the schema level.
86+
87+
| Dependent Collection Schemas
88+
| L2, L9
89+
| `CREATE COLLECTION ... WITH DEPENDENT_TYPES` — schema fields carry type-level
90+
constraints verified by Idris2 ABI (`src/Lith/`).
91+
|===
92+
93+
== GQL-DT Preview
94+
95+
The LithoGlyph Studio includes a GQL-DT preview panel (`studio/lib/bs/src/GqldtPreview.res`)
96+
that generates dependent-type-annotated GQL from collection definitions. This component
97+
visualises how L2 and L9 safety levels apply to a given schema.
98+
99+
=== Historical Note
100+
101+
"GQL-DT" was the original name for GQL's dependent type features. It is not a separate
102+
product — it describes how GQL uses dependent types within the safety pipeline, primarily
103+
at levels L2 and L9. The `GqldtPreview` component name is retained for compatibility but
104+
represents "GQL safety preview" rather than a separate execution mode.
105+
106+
== Implementation Status
107+
108+
[cols="^1,<3,^1", options="header"]
109+
|===
110+
| Level | Status | Notes
111+
112+
| L1-L2 | Implemented | Collection schemas with dependent types (ReScript + Factor + Zig)
113+
| L3-L4 | Designed | Multi-backend connections (Factor core, Forth core, Zig core)
114+
| L5-L7 | Partial | Provenance tracking specified, mutations audited
115+
| L8 | Designed | Bounded traversal depth for graph walks
116+
| L9 | Partial | GqldtPreview generates dependent type annotations
117+
| L10 | Designed | Cross-collection composition safety
118+
|===
119+
120+
== Implementation Stack
121+
122+
LithoGlyph has three core implementations:
123+
124+
[cols="<2,<2,<4", options="header"]
125+
|===
126+
| Core | Language | Purpose
127+
128+
| `core-factor/` | Factor | GQL engine with C API bridge (`gql-c-api/`)
129+
| `core-forth/` | Forth | Minimal GQL engine
130+
| `core-zig/` | Zig | FFI-compatible GQL engine (Idris2 ABI at `src/Lith/`)
131+
|===
132+
133+
The Idris2 ABI definitions in `src/Lith/` (LithBridge, LithForeign, LithLayout) provide
134+
the formal type proofs that underpin levels L2 and L9.
135+
136+
== Reference
137+
138+
* `studio/lib/bs/src/GqldtPreview.res` — GQL dependent type preview component
139+
* `src/Lith/` — Idris2 ABI definitions (LithBridge, LithForeign, LithLayout)
140+
* `ARCHITECTURE.adoc` — Full system architecture
141+
* https://github.com/hyperpolymath/vql-ut[VQL-UT] — Reference implementation of the 10-level safety pipeline

0 commit comments

Comments
 (0)