ZIL: A Lean4 Datalog DSL for Relational Project Descriptions, Inspired by Google Zanzibar

Introduction to ZIL

ZIL is a small relational language implemented as a domain-specific language (DSL) within Lean 4. Its purpose is to describe named objects, the relationships between them, and rules for deriving additional relationships. This allows for a structured representation of project components and their interconnections.

Relational Model and Examples

The core of ZIL's model is a three-part relation: subject ── relation ──▶ object. For instance, 'lean.Parser.parse ── implements ──▶ requirement.parseInput' illustrates how a declaration relates to a requirement. ZIL records how Lean 4's checked declarations relate to requirements, documents, tests, tasks, and other project elements.

This relational map can answer questions such as which declaration implements a specific requirement, which theorem validates a component, or which modules depend on a particular declaration. Developers, review tools, CI systems, documentation tools, and AI assistants can query these stored relationships.

Influence from Google Zanzibar

ZIL's relational model draws inspiration from the tuple-oriented model described in Google's Zanzibar paper, specifically its representation of authorization tuples. Zanzibar uses 'object#relation@user' to define relationships, such as 'doc:readme#owner@10' or 'group:eng#member@11'.

A key feature adopted from Zanzibar is the concept of a 'userset', where a tuple can refer to another relation, supporting group membership and inherited access. ZIL applies these compact relational building blocks not only to authorization models but also to broader project relationships, like 'declaration ── implements ──▶ requirement' or 'module ─── dependsOn ────▶ module'.

Syntax and Application

ZIL supports both a standalone tuple-shaped fact representation, such as 'doc:readme#owner@user:10.', and native Lean syntax. The Lean syntax uses 'zil_fact node(doc.readme) ⟶[owner] node(user.u10)' to represent these relationships. This integration within Lean 4 allows for the formal checking and management of project metadata.

The system aims to provide a unified way to understand and navigate complex project structures, facilitating tasks ranging from code review to automated documentation and AI-driven development assistance.