serQ v0.1.2

IR version 10, as v0.1.1: no change to the IR or to what the interpreter does (one comment changed). This release brings the Lean model of the language into this repository and makes it the interpreter's.

The Lean model is the Serq package in lean/ (#245, docs/lean.md): syntax and pool semantics, the executable semantics Exec, the serving order, and the vLLM scenarios of tools/oracle/ as theorems generated by scripts/gen_lean_oracle.py; make lean checks it. Another Lake project requires it at a tag (serving-queue-theory does).

Exec is event-driven like the interpreter, events in (time, event number) order, with an iteration cost affine in tokens, prefilled, decoders, kv_decode and attention (#247, #248). Differential random testing against the interpreter (make drt, CI: 200 random cases and the 333-session trace with the whole A100 cost fit) found three differences in the Lean semantics, now fixed: a run of zero work yields, settle and a hold's end admit as the interpreter does (#249), and a preemption takes the engine resident admitted last and sets computed (#250); tests/lean-regress/ holds them as generated theorems. serq-lean-bench runs Exec on a workload (#246); the compiled code evicts an entry's blocks at once, proved equal to the definition (makeRoomFast_eq, @[csimp]).

Serq/Fill.lean proves that an iteration of the step engine is the greedy fill of its budget in serving order (#252, assign_iter_eq_fillIter, fillAmounts_fifo, fillAmounts_sum), the property a FIFO prefill queue needs from the engine.

What's Changed

• feat(lean): move the Lean model into serQ as the Serq package by @vrvrv in #245
• perf(lean): serq-lean-bench, and Exec fast enough to replay the trace by @vrvrv in #246
• feat(lean): event-driven Exec with an iteration cost by @vrvrv in #247
• feat(lean): kv_decode and attention in the iteration cost by @vrvrv in #248
• fix(lean): a run of zero work yields, as in the interpreter by @vrvrv in #249
• fix(lean): a preemption picks the interpreter's victim and leaves computed by @vrvrv in #250
• test(lean): differential random testing against the interpreter, in CI by @vrvrv in #251
• feat(lean): an iteration of the step engine fills its budget in serving order by @vrvrv in #252
• chore(release): v0.1.2, IR 10 by @vrvrv in #255

Full Changelog: v0.1.1...v0.1.2