Lease contracts — the register and its two detectors
Three different concurrency contracts shared the word “lease” in this estate, and a fourth was found while building the census. Nothing at a call site told you which one you were holding: the type is ILeaseManager / ILeaseStore / a queue lease either way, and the option is called LeaseTtl / LeaseDuration / ClaimTimeoutSeconds either way. The discriminator is where the renewal happens relative to the work.
This directory carries lease-category-register.json, the estate’s map of lease name → category → owning module, and the two conformance tests that enforce it.
Owner ruling 2026-08-28, option (b) — docs/product/decisions/20260828-owner-decisions-findings-program.md §D3. The ruling bought visibility and enforcement, not repairs: converging sites on © was not ruled, and fixing individual sites was not ruled. Known violations are registered, not fixed.
The four categories
| Renewal | What TTL expiry means | Safe against a hung holder? | |
|---|---|---|---|
| A | inline — the work path renews between units and failure enters the work | genuinely “no progress” | yes, at the next fenced write |
| B | detached background timer — failure never reaches the work | nothing; the lease renews while the work is wedged | no |
| C | background heartbeat that propagates loss back into the work | “no progress” | yes |
| D | acquire once, never renew | “the whole pass overran” | only if the write is fenced |
© has two sub-shapes — push (the work’s CancellationToken is cancelled) and pull (the work checks ownership at declared checkpoints before every write). At the 2026-08-28 ruling the estate contained exactly one ©, pull-based, and push-based © existed nowhere in src/— which is why “converge on ©” was not ruled: there was nothing to converge on. JOB-14 (sprint 012, 2026-09-01) since repaired scheduler.policy_run_jobs as the estate’s first push-based ©: the policy-dispatch heartbeat cancels the execution token on renewal loss.
(A) also has two sub-shapes that are not interchangeable — throw (Findings) and return false and unwind (Policy, Vulnerabilities) — and a conformance test has to assert different things for each.
Declaring a category
Every acquisition site in production src/ carries, on the line above the call:
// LeaseContract: D name=export-center:audit-bundle-job
var job = await _jobStore.LeaseNextAsync(workerId, leaseUntil, cancellationToken);
The category is declared per site, not per lease, because the same lease name is genuinely held under different contracts by different holders: findings:advisory-corpus-projection is (A) under the projector and (D) under operator recovery.
A marker is chosen over an attribute deliberately. An attribute would need a shared contract project referenced from all 16 owning modules, which is exactly the cross-service edge AGENTS.md §2.7A forbids. The estate already enforces a source-marker of this shape — // Determinism:Allowed reason=… in DeterminismCallSiteConformanceTests.
The two detectors
Both are required. The investigation showed that a hand-maintained register plus a behavioural detector is precisely the instrument that recorded 8 of 17 ILeaseManager sites and read as complete, because its completeness assertion iterated the register it was meant to complete.
Detector 1 — behavioural
src/Scanner/__Tests/StellaOps.Scanner.Worker.Tests/LeaseCategoryBehaviouralConformanceTests.cs
A fault-injecting lease whose RenewAsync always throws, plus a stage that hangs forever while recording whether its CancellationToken ever fires, driven through the real ScannerWorkerHostedService composition. (B) and © are separated by behaviour, not structure: both have a safety factor, clamps and jitter.
Anti-vacuity runs in both directions — a correct ©-push composition must be classified © (0.13 s to observe cancellation), and the real Scanner composition must NOT be (the full 5 s budget elapses). Scanner is the live red case: LeaseHeartbeatService holds no CancellationTokenSource and only throws, and its caller awaits processingTask alone with no Task.WhenAny, calling jobCts.Cancel() after the work has already finished.
Detector 2 — discovery
src/__Tests/architecture/StellaOps.Architecture.Tests/LeaseContractRegisterConformanceTests.cs
Builds the census from symbols in src/and reconciles it against the register in both directions:
- symbols → register: an acquisition site with neither a marker nor an exclusion fails;
- register → symbols: a register row whose declared site carries no matching marker fails, and a stale exclusion fails.
A closed symbol set is still a list, so a third plane pins the aperture: every production method name matching (Try)?(Acquire|Lease|Claim)*Async must be classified as scanned (closedSet), excluded (notALease, with a reason), or an explicitly counted unclassifiedCandidate. A new lease-shaped method family cannot enter the estate without failing this test.
Red-proved 2026-08-28 by deleting the vuln.consensus.projector row from the register: the detector failed naming ConsensusProjectionHost.cs:96. The same mutations are encoded in-process (Detector_GoesRed_When…) so the proof survives.
Shrink-only sections
knownViolations, apertureSymbols.notALease and apertureSymbols.unclassifiedCandidates are shrink-only, the same discipline as build-boundary/legacy-edge-register.json. Counts are pinned in the detector as MaxKnownViolations and MaxUnclassifiedApertureSymbols; lowering one records a burn-down, raising it is a reviewed act visible in that file’s diff. A genuinely new violation means the site is the thing to fix.
Each violation names the lease, its category, what is missing (fence, cancellation-propagation, renewal), the traced blast radius, and why it was not fixed here.
What this cannot enforce, stated so it is not over-bought
- An (A) site’s composite inter-renewal gap. The gap is pool acquisition +
BeginTransaction+ anEnsureFencedAsyncFOR SHAREthat can block behind a writer + the batch + the commit, and nothing bounds the sum. That is the class that fenced live on 2026-08-28 09:21:07Z. The checkable proxy is FND-23’s constraint: declare each component’s bound and validate the sum below the TTL. - A lease that is not acquired by a method call. The Excititor worker claims its lease with an HTTP POST; it is category (B), fenceless, and recorded in
knownLimitsrather than enforced. - Whether a category is the right one for a site. The detectors check that the declaration matches the implementation, not that the implementation is adequate.
