feat: import gnpl from lithoglyph monorepo

[hyperpolymath]

Squashed, signed extraction of lithoglyph/gql-dt (GNPL / GQL-dt query language) into its reserved standalone repo. Template stubs superseded by real content.

Summary

Closes #

Type of change

• 🐛 Bug fix (non-breaking change that fixes an issue)
• ✨ New feature (non-breaking change that adds functionality)
• 💥 Breaking change (would change existing behaviour)
• 🕳️ Soundness fix (fixes a checker/proof false-negative)
• 📖 Documentation
• 🧹 Refactor / tech debt (behaviour-preserving)
• ⚡ Performance
• 🔧 Build / CI / tooling

How has this been verified?

Checklist

• My commits are signed (git commit -S).
• I ran the project's own checks/tests locally and they pass.
• New files carry the correct SPDX-License-Identifier (code/config MPL-2.0,
  prose CC-BY-SA-4.0); I did not relicense existing files.
• Docs are updated, and no public claim now overstates what the code does.
• I have not introduced a soundness hole (or I have flagged where I might have).

Notes for reviewers

---

Summary by Gitar

• Core implementation:
  • Imported GQL-DT dependently-typed query language core (src/GqlDt/) in Lean 4
  • Added lexical analyser (src/GqlDt/Lexer.lean) and corresponding test suite (test/LexerTest.lean)
• FFI and bridge:
  • Added Zig FFI implementations for ABI layout and database persistence (bridge/zig/, ffi/zig/)
  • Created build configuration files (lakefile.lean, gqldt.ipkg, Containerfile)
• Documentation and metadata:
  • Added machine-readable metadata and specifications (0-AI-MANIFEST.a2ml, spec/, docs/)

_{This will update automatically on new commits.}

[gitar-bot]

Note

Automatic reviews are paused because your trial's included automatic processing has been used for this period. Upgrade now, or comment "Gitar review" to run a review anytime.
Learn more

Code Review ✅ Approved 2 resolved / 2 findings

Imports the GNPL dependently-typed query language core and Zig FFI layer, but contains critical off-by-one errors in the lexer and unescaped query text in JSON serialization.

✅ 2 resolved

✅ Bug: Lexer peek off-by-one breaks operators, escapes, comments

📄 src/GqlDt/Lexer.lean:163-172 📄 src/GqlDt/Lexer.lean:266 📄 src/GqlDt/Lexer.lean:273-275 📄 src/GqlDt/Lexer.lean:298-305 📄 src/GqlDt/Lexer.lean:359-373
LexerState.peek returns the character at s.pos when called with offset = 0 (the loop hits n >= offset immediately and returns s.input.get s.pos), i.e. peek 0 is the current char, not the next one. Every call site passes peek 0 expecting the following character, so the lexer is systematically wrong: multi-char operators <=, >=, !=, <> are never recognized (each falls through to the single-char branch, e.g. <= lexes as < then =); a lone : is mis-lexed as :: and a lone - is treated as the start of a -- line comment (since curr and peek 0 are the same char, some '-', some '-' matches on a single dash); block comments /* are never entered and string escapes like drop the escaped char and emit a stray backslash. Fix by making the peek offset refer to characters ahead of the cursor (or change all call sites to peek 1, which correctly returns the next char).

✅ Security: gqldt_serialize_json does not escape query text

📄 ffi/zig/src/main.zig:330-344
gqldt_serialize_json builds {"query":"<text>"} by copying the raw query bytes verbatim between quotes. Any query containing a double-quote, backslash, or control character produces malformed/invalid JSON, and an attacker-influenced query can inject additional JSON structure into the output consumed downstream. Escape ", \, and control characters (or emit via a proper JSON encoder) and size the buffer check against the escaped length before copying.

Options

Display: compact → Showing less information.

Comment with these commands to change the behavior for this request:

Compact

gitar display:verbose

_{Was this helpful? React with 👍 / 👎 | Gitar}