The Lean model¶

lean/ is a Lean 4 package (Serq, Mathlib v4.34.0) that gives serQ a formal semantics. The Rust interpreter is the reference implementation; the Lean package is the definition that theorems are about. Both are released together, so a release tag names one interpreter and one semantics.

Module	Contents
`Serq/Core.lean`	the syntax `Route Env V` of the `session` block and its surface syntax `[route\| … ]`; the rates of the stage kinds; the semantics of one pool (`Step`) and the memory invariant `allocated + cached ≤ cap` (`Step.invariant`)
`Serq/Exec.lean`	an executable semantics of the pool and step-engine fragment on the step clock (values in ℕ): `Exec.tick`, `Exec.run`, `Exec.runW`
`Serq/Serve.lean`	serving order of a step engine: without a per-request chunk cap, admission order is decode-first (`serve_eq_decode_first`); a cap breaks it (`chunk_cap_breaks_shape`)
`Serq/Oracle.lean`	the vLLM scheduler scenarios of `tools/oracle/` as theorems about the programs they were compiled from, checked by `decide +kernel`; generated by `scripts/gen_lean_oracle.py` from `tools/oracle/*.ir.json`, never edited by hand

Checks¶

make lean   # oracle theorems current, lake build, no sorry, axiom audit

scripts/check_lean.sh fails if Serq/Oracle.lean is stale with respect to tools/oracle/*.ir.json, if any declaration uses sorry, or if a theorem listed in lean/scripts/AxiomAudit.lean depends on an axiom other than propext, Classical.choice and Quot.sound. A first build needs the Mathlib cache: cd lean && lake exe cache get.

Using the package¶

A Lake project requires it at a release:

[[require]]
name = "Serq"
git = "https://github.com/vrvrv/serQ"
rev = "<tag or commit>"
subDir = "lean"

and imports Serq (or one module). The definitions live in the namespace SerqLang (the package is Serq): the names were SerqLang.* before the package moved here, and the projects that cite them keep them. serving-queue-theory does this: its queueing results start from Serq.Exec rather than from a queue model of its own.

What is not covered yet¶

The step engine runs on the step clock (one iteration per tick); iteration costs in seconds are not part of Exec yet. The session-level semantics outside the fragment (renewal arrivals, transfers between pools, flows over several stages) and the setting of computed on a preemption are not formalised (docs/language.md §9), and there is no proof that the Rust interpreter implements Exec: the oracle scenarios, run by both, are the evidence (docs/review.md §4 lists the tools that would close the gap).