serQ v0.1.3

IR 11 is first tagged in this release. Regenerate IR from source when moving from v0.1.2 (IR 10); update downstream readers and re-record seeded simulation results.

A seed now names a workload: init and turn draws use streams keyed by (seed, session, turn), statement draws by (seed, session), independently of scheduling. Seeded numbers change. Deterministic oracle schedules and the prefix-cache trace remain unchanged.

The iteration is programmable: CStep.iteration contains Serve, Admit, Branch and Set operations; Program.registers and CExpr::Reg give stages state between iterations. The former CStep.only field is removed: serve only compiles to an iteration body. Serve keys read the current resident totals, including requests admitted in that iteration. Preempt::Lifo is replaced by By {keys, tail}; preempt lifo compiles to the equivalent key and head requeue. Victim keys can read position, admission and decoding. CPool.reserve_held keeps a reservation until its hold ends, CStep.granule constrains prefill allocation, and CStmt::Fork/Join express concurrent request legs.

A state-dependent hold or reservation waits instead of being rejected at queue entry; an over-cap head at run end is reported. A preempted hold caches its computed position rather than an uncomputed allocation. Validation rejects invisible context reads, unsafe hold indices and loops that cannot advance time; invalid amounts and indices, non-settling instants and zero-cost token iterations fail loudly.

Claims state mechanically checked properties of runs, with aggregates and demand, served and arrived contexts. The Lean model and generated claims now connect the paper programs to Dai, Bari and Kong results, including Poisson drift and recurrence results. The Lean fragment follows expression-dependent chunks and the LIFO encoding. Arbitrary iteration bodies, registers, reserve held, granules and fork/join remain outside it; the generators reject unsupported programs. The claims generator accepts the serve-only body it knows.

The examples exercise the new iteration, reservation, victim and granule mechanisms. pyserq adds deployment drawing. CLI, Python wheels and the Serq Lake package share this release; downstream consumers should pin v0.1.3 together.

What's Changed

• feat(lang): the stochastic-process definition and the four rules it asked for by @vrvrv in #256
• fix(lang): the re-ready bound is per session, a hold's header may not draw by @vrvrv in #259
• docs(claude): ask why a bug happened and whether a check should refuse it by @vrvrv in #266
• feat(lang): serve only (p), and FasterTransformer as a use case by @vrvrv in #263
• feat(draw): draw what one request runs, not the workload's choices by @vrvrv in #264
• fix(lang): grow and growing need an enclosing hold of their pool by @vrvrv in #281
• fix(ir): budget_left needs a step stage by @vrvrv in #283
• fix(lang): a renewal gap must be a positive time, and not a panic by @vrvrv in #285
• fix(ir): a constant hold larger than every cap it may name does not link by @vrvrv in #287
• fix(ir): a poisson rate must be positive and finite by @vrvrv in #288
• docs(pyserq): the install section is the two pip lines by @vrvrv in #292
• feat(pyserq): draw, the deployment view as serq draw prints it by @vrvrv in #291
• fix(examples): the vLLM programs admit through the engine, as vLLM does by @vrvrv in #294
• fix(ir): a step's budget does not read budget_left by @vrvrv in #299
• fix(examples): the vLLM programs draw whole token counts by @vrvrv in #298
• fix(interp): a negative or NaN amount and a bad index are errors, not 0 by @vrvrv in #290
• refactor(ir): one CExpr walk, which a static eviction key no longer skips by @vrvrv in #300
• fix(lang): the parser folds an aggregate, so its let sizes an array by @vrvrv in #301
• refactor(interp): return what is removed, flag a preemption, one tolerance by @vrvrv in #302
• fix(lang): an arrival count is a whole number in range, not a cast by @vrvrv in #303
• refactor(interp): a hold's pools are structs, and one search finds the innermost by @vrvrv in #306
• docs(nav): pyserq is a top-level page beside the CLI reference by @vrvrv in #308
• fix(ir): validate checks what the interpreter assumes the linker checked by @vrvrv in #307
• test(interp): check that pools conserve what sessions hold, in a debug run by @vrvrv in #311
• feat(lang): claims, and three papers' propositions proved in Lean by @vrvrv in #304
• fix(ir): a hold whose body sets its index does not grow, load or release by it by @vrvrv in #312
• refactor(frontend): one draw walk and one substitution, on Expr by @vrvrv in #316
• fix(ir): a hold takes each pool once by @vrvrv in #315
• feat(lang): a validate error points at its statement's line by @vrvrv in #318
• fix(ir): a hold a pool may preempt reads no index that moves by @vrvrv in #319
• docs(site): a home page that says what serQ is for, and tabs by @vrvrv in #314
• docs(language): only what is true today, and shorter by @vrvrv in #320
• feat(lang): an iteration claim reads arrived, and Dai Theorem 2(b) pathwise by @vrvrv in #324
• feat(lean): Foster's criterion on a finite-support kernel by @vrvrv in #325
• docs(brand): the serQ logo in the README and on the site by @vrvrv in #321
• docs(use-cases): Bari Theorem 2 waits on the kernel, not on Foster by @vrvrv in #327
• fix(interp): a served resident preempted in its iteration leaves it by @vrvrv in #322
• fix(lang): vLLM caps a prefill only while another request is eligible by @vrvrv in #323
• feat(lean): a program with random arrivals as a Markov kernel, and Dai Theorem 2(b) on it by @vrvrv in #332
• feat(lean): Bari Theorem 2 on the kernel by @vrvrv in #333
• docs(getting-started): say that serQ runs from Python too by @vrvrv in #335
• fix(lang): an override refused on IR names what it overrides, not a flag by @vrvrv in #336
• refactor(view): one place maps a format name to its writer by @vrvrv in #338
• fix(interp): a preempted hold caches what it computed, not what it was allocated by @vrvrv in #340
• fix(lang): override errors speak of the let or def, not the CLI flag by @vrvrv in #341
• feat(lean): positive recurrence of Dai's and Bari's chains by @vrvrv in #342
• refactor(lean): a step's chunk is a function of the program's expression by @vrvrv in #343
• docs(language): a served victim caches its position, by choice by @vrvrv in #344
• fix(lean): DaiSim and BariSim name the chunk field chunkAt by @vrvrv in #346
• refactor(lean): one translator of IR expressions, with a leaf per moment by @vrvrv in #348
• ci: run on a merge queue's groups by @vrvrv in #349
• refactor(lean): the step lemmas of the semantics in one module by @vrvrv in #351
• refactor(lean): one slot invariant for DaiStable and BariStable by @vrvrv in #352
• feat(lean): Foster's drift for Poisson arrivals in Dai et al. and Bari et al. by @vrvrv in #359
• feat(lean): Bari et al. over g nodes with the random planner by @vrvrv in #358
• refactor(lean): the paper proofs beside the paper programs by @vrvrv in #361
• feat(lean): Kong Theorems 3.4 and 3.5, with Harris's inequality by @vrvrv in #353
• docs(design): engine neutrality, SGLang, TensorRT-LLM and TGI as serQ programs by @vrvrv in #354
• feat(ir): preempt by (keys) requeue head|tail, the victim a program chooses by @vrvrv in #360
• feat(ir): a step stage's iteration as a program body by @vrvrv in #362
• feat(ir): a step stage's registers, state NAME = c set by its body by @vrvrv in #367
• fix(interp): a reserve that reads the state waits instead of being rejected by @vrvrv in #369
• refactor(ir): a stage's serve only (p) is an iteration body; CStep.only removed by @vrvrv in #370
• feat(ir): reserve held, a reservation that lasts as long as its hold by @vrvrv in #371
• feat(ir): fork and join, a request's legs, for NIXL's push mode by @vrvrv in #372
• feat(ir): granule g, a prefill gets all it has left or a multiple of g by @vrvrv in #373
• docs(design): a shared prefix cache, a hold's prefix as a chain of keyed segments by @vrvrv in #375
• feat(lean): the empty engine recurs under Poisson arrivals in Dai et al. and Bari et al. by @vrvrv in #376
• feat(examples): the engines with the new constructs; a register is read by its hold's first pool by @vrvrv in #377
• feat(lean): every node of Bari et al.'s g nodes empty at once recurs by @vrvrv in #378
• chore(release): v0.1.3, IR 11 by @vrvrv in #379

Full Changelog: v0.1.2...v0.1.3