Skip to content

test(driver-sql): derive §3's span ceiling from the conclusion it guards, not from a superseded one - #13959

Merged
zhuangjianguo merged 1 commit into
mainfrom
claude/issue-13691-stamp-precision-span-budget
Aug 31, 2026
Merged

test(driver-sql): derive §3's span ceiling from the conclusion it guards, not from a superseded one#13959
zhuangjianguo merged 1 commit into
mainfrom
claude/issue-13691-stamp-precision-span-budget

Conversation

@claude

@claudeclaudeBot commented Aug 31, 2026

Copy link
Copy Markdown
Contributor

Fixes#13691

§3's span bound is a validity precondition, not a claim about the product. It establishes that second-precision truncation could not have produced the distinctness §3 then concludes from — so its correct value is whatever that conclusion needs. #11572 changed the conclusion and did not move it.

The finding that decided the route

Traced by git log -L on the assertion itself, not inferred:

commitwhat it did to §3the span ceiling
64505a5122 (#11224, PR #11320)conclusion: new Set(stamps).size > 1two distinct stampswrote span < 1000
d2cacbcf51 (#11572, PR #12112)conclusion strengthened to .toBe(ROUNDS)six distinct stampsuntouched

Two truncated values need one whole second, so 1_000 was the tight bound for the original conclusion. ROUNDS truncated stamps are ROUNDS multiples of a second and cannot span less than ROUNDS - 1 of them, so the bound for the current conclusion is 5_000.

d2cacbcf51wrote that arithmetic into the file in the same commitMIN_GAP_MS's note has read "against the 5 whole SECONDS second-precision stamps would need to yield ROUNDS distinct values" since 2026-08-25 — while leaving the executable bound on the superseded number. The file's prose and its code have disagreed by a factor of ROUNDS - 1 for six days.

So this is not "raise the ceiling for headroom". The ceiling was stale, over-strict by exactly ROUNDS - 1 against the assertion it guards, and over-strictness in a validity precondition is not conservatism: such an assertion cannot fail in a way that says anything about the product, so every millisecond of excess is only ever a false red on somebody else's PR. That is how it surfaced, at span = 1006 — six milliseconds over — with monotonicity, the real invariant on the line above, holding.

Zone-2 verdicts

#questionverdict
A2.1constants current on main?CONFIRMED, by symbol: ROUNDS = 6, MIN_GAP_MS = 5, wall toBeLessThan(1_000). Line numbers had moved; the card's :141 / :159 no longer point at them.
A2.2budget decompositionMEASURED on the sqlite cell, NOT MEASURED on the live cells. Numbers below.
A2.3is the deliberate spacing bounded and knowable?PM's mechanism FALSIFIED, PM's conclusion CONFIRMED — and neither one decides the route. Detail below.
A2.4is 1000 ms the right constant for both dialects?The grain is right for the whole matrix; the multiplier was wrong. Detail below.

A2.2 — the decomposition

30 trials per leg of §3's exact loop, sqlite cell, this container (shared box — treat absolutes as ratios):

conditionspan msdeliberate spacing msupdate RTT msread RTT msspan − deliberate ms
idle loop28 / 29 / 3525 / 26 / 30p50 3p50 10 / 3 / 9
loop held by a re-scheduling 12 ms hog61 / 62 / 6860 / 61 / 65p50 1p50 00 / 1 / 4

(min / p50 / max.) On the sqlite cell the deliberate spacing is 90–98 % of the whole span and the round-trips are noise.

⚠️The live cells did not execute here — no OS_TEST_POSTGRES_URL / OS_TEST_MYSQL_URL, no listener on 3306/5432, no docker daemon; both cells reported as named SKIPs. The failure being fixed was on live MySQL, so component (b), live round-trip latency, is NOT MEASURED and I am not claiming a number for it. What can be said without it: the deliberate term measures 25–86 ms across every condition I could produce, so for it to account for a 1006 ms span each of the five gaps would have had to overshoot its 5 ms request by roughly 195 ms.

A2.3 — measured, and it does not go the way the card assumed

The helper does not spin on the clock:

async function awaitClockAdvance(ms) {
const start = Date.now();
for (;;) {
const observed = Date.now() - start;
if (observed >= ms) return observed;
await new Promise((resolve) => setTimeout(resolve, ms - observed));
}
}

It waits with setTimeout, so its cost is bounded by event-loop delivery, not by clock granularity. Date.now() granularity on this host is 1 ms (200 tight reads returned one value), so the granularity story does not apply here at all.

The conclusion the card drew from that hypothesis nevertheless holds, by the other mechanism: the spacing is bounded below by ROUNDS - 1 gaps and not bounded above by anything in the code. 300 trials of the five gaps §3 takes:

conditionminp50p90p99max
idle2526263364
loaded6060606486

ROUNDS * MIN_GAP_MS is 30. Under a modest synthetic load the real spacing is already 2× that, with no ceiling in the code. So a budget sized on ROUNDS * MIN_GAP_MS would be a budget sized on a number the machine is free to exceed — recorded in MIN_GAP_MS's note so the next author does not re-derive it.

⭐ But the STOP condition attached to A2.3 does not fire, because the answer does not narrow the routes: the gaps are individually measured and retained in gaps[], so the deliberate total is knowable exactly at runtime whatever it costs. Unboundedness would only have killed a route that had to assume the spacing. None of the three does.

A2.4 — one grain fits the matrix; the multiplier did not

The guarded defect class is second truncation on every cell that can have it: MySQL's unqualified CURRENT_TIMESTAMP (#11224 itself), and, for the SQLite cell, the truncation this file's own head note prescribes as its ablation (new Date().toISOString() forced to .000Z). Postgres stamps at microsecond precision and has nothing to truncate, so the bound is vacuous there rather than wrong. One wall does fit all three — the error was never the grain, it was multiplying it by 1 instead of by ROUNDS - 1.

Route chosen, and why the advisory route was overruled

Chosen: derive the ceiling from the conclusion it guards.MAX_SPAN_MS = (ROUNDS - 1) * TRUNCATED_STAMP_GRAIN_MS.

Both guards are preserved, and one of them is preserved by construction rather than by care:

Overruling the card's ⭐ route (subtract the deliberate spacing from the span), on two grounds.

  1. It is semantically wrong. Truncation arithmetic does not care whether elapsed time was spent deliberately. If a run genuinely spans six seconds, second-precision stamps could have produced six distinct values, and that is true whether the six seconds went into awaitClockAdvance or into round-trips. Subtracting the deliberate half makes the precondition measure "was this test slow for reasons other than its own spacing", which is not what makes the following assertion readable — so it would weaken the guard in precisely the case where the guard matters.
  2. It would not have prevented the reported failure by any margin worth having. The deliberate term measures 25–86 ms. Subtracting it turns span = 1006 into 920–981 against an unchanged 1000 ms wall: a 19–80 ms margin on a budget whose dominant term is load-driven and unbounded. It buys one build.

The other two named moves are also declined: raising the ceiling to a chosen number would leave the same disconnect in place one constant further out, and retrying the section would add nondeterminism to a cell whose whole point since #11572 is that it is deterministic.

⭐ The decomposition in A2.2 is reported because it was asked for and because it is now in the failure message, but note that it did not decide the route — the route follows from the arithmetic relating the ceiling to the conclusion, which is true whichever term dominates the budget. That is the property that makes it a fix rather than a headroom adjustment.

What else the diff does

  • The failure message now reports the split. When the precondition does fire, it names how much of the span was deliberate spacing (with the individual gaps) and how much was everything else, and says in its own text that neither half is a product signal and that the ordering invariant above is unaffected — so the next reader gets A2.2 for free instead of re-deriving it.
  • The coupling is pinned, server-free.maxDistinctUnderTruncation() models the defect class, and two assertions hold the ceiling to being both sound (one ms under it, truncation cannot reach ROUNDS distinct) and tight (at it, truncation can). This is arithmetic, not a measurement of the machine, so it runs on every runner including ones with no live dialects — which matters, because nothing that executes on a fast runner discriminated the six-day drift, as the ablation below shows.

Ablation

Implementation committed first; both legs mutate the committed constant, prove the mutation on disk before reading anything, and restore under trap … EXIT INT TERM with absolute paths.

⚠️The first attempt was a no-op and its reading was voided. A perl -0pi pattern put \* inside a \Q…\E block, where the backslash is itself literal, so nothing matched. The on-disk proof caught it — injected=0, original anchor still present, blob unchanged from HEAD — and the leg was discarded rather than reported. Re-run with an explicit mutator that refuses on an anchor count other than 1.

legmutationon-disk proofresult
TIGHTceiling back to the superseded literal 1_000injected=1, original anchor remaining=0, blob 12515b0028… vs HEAD 97d7c78d29…pin reds: "the ceiling is 1000 ms, but second-precision truncation still cannot reach 6 distinct stamps at that span"expected 2 to be greater than or equal to 6. §1–§6 all stay green.
SOUNDceiling loosened one grain, ROUNDS * graininjected=1, original anchor remaining=0, blob b69e3e0e9b… vs HEADpin reds: "a span of 5999 ms must leave second-precision truncation unable to reach 6 distinct stamps"expected 6 to be less than 6.

Restore proven after each leg and at exit: git hash-object back to 97d7c78d29f38f87032a6f689c31f7ca83b19d2f (equal to the HEAD blob) and git diff HEAD empty.

Read the TIGHT leg's second half. With the ceiling wrong by a factor of five, every live section stays green on this runner. That is exactly why the drift survived six days and surfaced only as somebody else's queue eviction — and it is the argument for the pin being arithmetic rather than another timed assertion.

Clause ② — self-declared from the actual diff

limbverdictevidence
path — diff touches packages/spec/src/**NOThe diff is exactly one file: packages/drivers/driver-sql/src/sql-driver-11224-update-stamp-precision.test.ts. git diff --stat against the merge base names no second path.
content — changes contract accept/reject behaviour, or widens the published surfaceNOThe file is a *.test.ts, not part of any package entry point; check:published-files green. Nothing in the diff touches updatedAtStamp(), stampUpsertUpdatedAt(), emitted SQL, or any schema — §4 and §5, which pin the emitted expression per dialect, are unmodified. The new symbols are file-local consts and one file-local function; no export was added. check:api-surface has no path population here and the diff adds no .d.ts input.

Both limbs read NO, so per the repo's 不预挂 rule (maintainer, 2026-08-28) needs:contract-review is not attached — an open carrier must always mean genuinely pending review.

Verification

Run on the final head a58d60af.

Green — measured:

  • pnpm --filter @objectstack/driver-sql exec vitest run src/…Tests 9 passed | 2 skipped (11). §1–§6 green on the sqlite cell; both new pin assertions green.
  • pnpm --filter @objectstack/driver-sql exec tsc --noEmit — exit 0. Confirmed with --listFiles that the edited file is in the tsc program (this package excludes no tests), so the green covers the edit rather than talking past it.
  • All 22 path-derived gate families green, plus the 6 convention-triggered ones for the "edits a test file" kind — including check:cross-package-test-inputs, check:engine-double-contract, check:where-matcher, check:query-options-erasure, check:type-check-coverage, check:driver-conformance, check:test-source-alias. Derived with node scripts/pm/dispatch-gates.mjs --repo objectstack-ai/objectstack (no hand-built path list), harvested with --commands, each exit code captured before any pipe.
  • pnpm lint — the full repo-wide eslint . --no-inline-config, exit 0 in 59 s. Not narrowed; no narrowing declaration needed.
  • pnpm check:nul-bytes — OK over 7652 files, plus a targeted control-byte scan of the edited file.

⚠️ NOT MEASURED — prerequisite not met, never read as a pass:

  • node scripts/check-test-completeness.mjsexit 3, its own text: "Nothing was measured: this gate exited before parsing a single summary line."
  • pnpm check:dual-build-cjs-loadsexit 3, PREREQUISITE NOT MET, 78 packages without dist/.
  • pnpm check:type-check-debtexit 1, but this is a throw, not a finding: "--re-measure cannot run: 50 workspace dependencies of the ledgered packages have no built type entry point on disk … measuring now would not fail, it would silently measure a DIFFERENT WORLD." Its --self-test (47 + 65 + 43 + 28 + 19 cases) and the structural half check:type-check-coverage both passed. driver-sql carries no DEBT or TEST_DEBT ledger entry and its own typecheck is green above, so this ratchet has nothing this diff can move — but that reasoning is not a measurement and it is not recorded as one.

All three need a built full-workspace closure; each is a repo-wide sweep CI performs on every PR regardless. Declared rather than run, per the local-verification scope.

⚠️The live PG and MySQL cells are NOT MEASURED here and the failure being fixed was on live MySQL. Temporal Conformance (live PG + MySQL) is the job that actually exercises §3 against a server.

Not run, deliberately: the repo configures no Prettier (no config file, no prettier key, no workflow step). Invoking it picks up upstream defaults that disagree with the repo's eslint-enforced style and rewrites the whole file; that was tried, caught by inspection, and reverted byte-identically before commit.

Out of scope

Landing

Draft, per dispatch. ⛔ Not flipped ready, no auto-merge armed — enqueue on this repo is irreversible and landing is the PM's.

Session: https://claude.ai/code/session_01F3jdziLbAPGeceVNmSox5L

Generated by Claude Code


Generated by Claude Code

…rds (#13691)
§3's `span` bound is a validity precondition, not a claim about the product:
it establishes that second-precision truncation could not have produced the
distinctness §3 concludes from. Its correct value is whatever that CONCLUSION
needs — and #11572 changed the conclusion without moving it.
#11224's §3 asked for two distinct stamps, and two truncated values need one
whole second, so `span < 1000` was the tight bound for it. #11572 (d2cacbc)
strengthened the conclusion to `ROUNDS` distinct stamps — which cannot span
less than `ROUNDS - 1` whole seconds — and wrote that arithmetic into
MIN_GAP_MS's own note in the same commit, while leaving the executable bound on
the superseded number. The precondition has been over-strict by a factor of
`ROUNDS - 1` ever since, and #11572's fix spends real wall-clock inside that
same budget by design.
MAX_SPAN_MS is now derived from ROUNDS and the truncation grain, the failure
message reports how much of the span was deliberate spacing and how much was
everything else, and the derivation is pinned by server-free arithmetic so the
ceiling and the conclusion cannot drift apart in silence again.
Nothing #11572 established is traded away: awaitClockAdvance still drives the
clock, both gap assertions still run, and the conclusion is still `ROUNDS`
distinct stamps.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01F3jdziLbAPGeceVNmSox5L
@github-actions

Copy link
Copy Markdown
Contributor

📓 Docs Drift Check

Nothing in this diff resolved to a documentable surface (no symbol, route or SDK anchor derived from 0 changed package(s)), so this run has no opinion about the docs.

What this run could not see
  • a page that states a rule by its inputs shares no identifier with the emitter that implements the rule, so an emitter-only diff cannot list it — not on this run and not on any run. Measured on fix(driver-sql): emit varchar(maxLength) for a text field a declared index keys on #11430: content/docs/protocol/objectql/types.mdx documents the text-family column mapping by the ObjectQL type names it maps FROM (text / textarea / html) while the diff changed createColumn; it went unlisted, and it was the page that diff falsified, in four places. No shared token exists to detect this on, so a rule your change carries has to be re-read by hand in the pages that restate it.

Coarse fallback — 0 page(s) merely mention a changed package (the pre-#9192 predicate, kept for the deliberately-wide backstop): node scripts/docs-audit/affected-docs.mjs --json 5994611a80554951d6b748995e41a9222482b44fpackageMentionDocs.

@zhuangjianguozhuangjianguo added the skip-changeset PR has no user-facing published change; bypasses the changeset gate label Aug 31, 2026 — with Claude
@zhuangjianguo
zhuangjianguo marked this pull request as ready for review August 31, 2026 19:46
@zhuangjianguo
zhuangjianguo added this pull request to the merge queueAug 31, 2026
Merged via the queue into main with commit 4ab8b59Aug 31, 2026
37 checks passed
@zhuangjianguo
zhuangjianguo deleted the claude/issue-13691-stamp-precision-span-budget branch August 31, 2026 20:08
Sign up for freeto join this conversation on GitHub. Already have an account? Sign in to comment

Labels

size/mskip-changesetPR has no user-facing published change; bypasses the changeset gatetests

Projects

None yet

2 participants

@zhuangjianguo@claude
, 'i'); if (__m === '*' || __re.test(location.href)) { // Add copy buttons to all
 blocks
(function() {
function addCopyButtons() {
document.querySelectorAll('pre code').forEach(function(codeBlock) {
if (codeBlock.parentElement.hasAttribute('data-copy-added')) return;
codeBlock.parentElement.setAttribute('data-copy-added', 'true');
var btn = document.createElement('button');
btn.textContent = 'Copy';
btn.style.cssText = 'position:absolute;top:4px;right:4px;padding:2px 8px;font-size:11px;background:#4ecdc4;border:none;border-radius:4px;color:#1a1a2e;cursor:pointer;opacity:0.7;transition:opacity 0.2s;';
btn.onmouseover = function() { this.style.opacity = '1'; };
btn.onmouseout = function() { this.style.opacity = '0.7'; };
btn.onclick = function() {
navigator.clipboard.writeText(codeBlock.textContent).then(function() {
btn.textContent = 'Copied!';
setTimeout(function() { btn.textContent = 'Copy'; }, 1500);
});
};
codeBlock.parentElement.style.position = 'relative';
codeBlock.parentElement.appendChild(btn);
});
}
addCopyButtons();
// Re-run on dynamic content
var observer = new MutationObserver(addCopyButtons);
observer.observe(document.body, { childList: true, subtree: true });
})();
}
} catch(__e) { console.warn('[Userscript:Add Copy Buttons to Code Blocks]', __e); }
})();
(function(){
try {
var __m = "github.com";
var __re = new RegExp('^' + "github\\.com" + '
test(driver-sql): derive §3's span ceiling from the conclusion it guards, not from a superseded one by claude[bot] · Pull Request #13959 · objectstack-ai/objectstack · GitHub
Skip to content

test(driver-sql): derive §3's span ceiling from the conclusion it guards, not from a superseded one - #13959

Merged
zhuangjianguo merged 1 commit into
mainfrom
claude/issue-13691-stamp-precision-span-budget
Aug 31, 2026
Merged

test(driver-sql): derive §3's span ceiling from the conclusion it guards, not from a superseded one#13959
zhuangjianguo merged 1 commit into
mainfrom
claude/issue-13691-stamp-precision-span-budget

Conversation

@claude

@claudeclaudeBot commented Aug 31, 2026

Copy link
Copy Markdown
Contributor

Fixes#13691

§3's span bound is a validity precondition, not a claim about the product. It establishes that second-precision truncation could not have produced the distinctness §3 then concludes from — so its correct value is whatever that conclusion needs. #11572 changed the conclusion and did not move it.

The finding that decided the route

Traced by git log -L on the assertion itself, not inferred:

commitwhat it did to §3the span ceiling
64505a5122 (#11224, PR #11320)conclusion: new Set(stamps).size > 1two distinct stampswrote span < 1000
d2cacbcf51 (#11572, PR #12112)conclusion strengthened to .toBe(ROUNDS)six distinct stampsuntouched

Two truncated values need one whole second, so 1_000 was the tight bound for the original conclusion. ROUNDS truncated stamps are ROUNDS multiples of a second and cannot span less than ROUNDS - 1 of them, so the bound for the current conclusion is 5_000.

d2cacbcf51wrote that arithmetic into the file in the same commitMIN_GAP_MS's note has read "against the 5 whole SECONDS second-precision stamps would need to yield ROUNDS distinct values" since 2026-08-25 — while leaving the executable bound on the superseded number. The file's prose and its code have disagreed by a factor of ROUNDS - 1 for six days.

So this is not "raise the ceiling for headroom". The ceiling was stale, over-strict by exactly ROUNDS - 1 against the assertion it guards, and over-strictness in a validity precondition is not conservatism: such an assertion cannot fail in a way that says anything about the product, so every millisecond of excess is only ever a false red on somebody else's PR. That is how it surfaced, at span = 1006 — six milliseconds over — with monotonicity, the real invariant on the line above, holding.

Zone-2 verdicts

#questionverdict
A2.1constants current on main?CONFIRMED, by symbol: ROUNDS = 6, MIN_GAP_MS = 5, wall toBeLessThan(1_000). Line numbers had moved; the card's :141 / :159 no longer point at them.
A2.2budget decompositionMEASURED on the sqlite cell, NOT MEASURED on the live cells. Numbers below.
A2.3is the deliberate spacing bounded and knowable?PM's mechanism FALSIFIED, PM's conclusion CONFIRMED — and neither one decides the route. Detail below.
A2.4is 1000 ms the right constant for both dialects?The grain is right for the whole matrix; the multiplier was wrong. Detail below.

A2.2 — the decomposition

30 trials per leg of §3's exact loop, sqlite cell, this container (shared box — treat absolutes as ratios):

conditionspan msdeliberate spacing msupdate RTT msread RTT msspan − deliberate ms
idle loop28 / 29 / 3525 / 26 / 30p50 3p50 10 / 3 / 9
loop held by a re-scheduling 12 ms hog61 / 62 / 6860 / 61 / 65p50 1p50 00 / 1 / 4

(min / p50 / max.) On the sqlite cell the deliberate spacing is 90–98 % of the whole span and the round-trips are noise.

⚠️The live cells did not execute here — no OS_TEST_POSTGRES_URL / OS_TEST_MYSQL_URL, no listener on 3306/5432, no docker daemon; both cells reported as named SKIPs. The failure being fixed was on live MySQL, so component (b), live round-trip latency, is NOT MEASURED and I am not claiming a number for it. What can be said without it: the deliberate term measures 25–86 ms across every condition I could produce, so for it to account for a 1006 ms span each of the five gaps would have had to overshoot its 5 ms request by roughly 195 ms.

A2.3 — measured, and it does not go the way the card assumed

The helper does not spin on the clock:

async function awaitClockAdvance(ms) {
const start = Date.now();
for (;;) {
const observed = Date.now() - start;
if (observed >= ms) return observed;
await new Promise((resolve) => setTimeout(resolve, ms - observed));
}
}

It waits with setTimeout, so its cost is bounded by event-loop delivery, not by clock granularity. Date.now() granularity on this host is 1 ms (200 tight reads returned one value), so the granularity story does not apply here at all.

The conclusion the card drew from that hypothesis nevertheless holds, by the other mechanism: the spacing is bounded below by ROUNDS - 1 gaps and not bounded above by anything in the code. 300 trials of the five gaps §3 takes:

conditionminp50p90p99max
idle2526263364
loaded6060606486

ROUNDS * MIN_GAP_MS is 30. Under a modest synthetic load the real spacing is already 2× that, with no ceiling in the code. So a budget sized on ROUNDS * MIN_GAP_MS would be a budget sized on a number the machine is free to exceed — recorded in MIN_GAP_MS's note so the next author does not re-derive it.

⭐ But the STOP condition attached to A2.3 does not fire, because the answer does not narrow the routes: the gaps are individually measured and retained in gaps[], so the deliberate total is knowable exactly at runtime whatever it costs. Unboundedness would only have killed a route that had to assume the spacing. None of the three does.

A2.4 — one grain fits the matrix; the multiplier did not

The guarded defect class is second truncation on every cell that can have it: MySQL's unqualified CURRENT_TIMESTAMP (#11224 itself), and, for the SQLite cell, the truncation this file's own head note prescribes as its ablation (new Date().toISOString() forced to .000Z). Postgres stamps at microsecond precision and has nothing to truncate, so the bound is vacuous there rather than wrong. One wall does fit all three — the error was never the grain, it was multiplying it by 1 instead of by ROUNDS - 1.

Route chosen, and why the advisory route was overruled

Chosen: derive the ceiling from the conclusion it guards.MAX_SPAN_MS = (ROUNDS - 1) * TRUNCATED_STAMP_GRAIN_MS.

Both guards are preserved, and one of them is preserved by construction rather than by care:

Overruling the card's ⭐ route (subtract the deliberate spacing from the span), on two grounds.

  1. It is semantically wrong. Truncation arithmetic does not care whether elapsed time was spent deliberately. If a run genuinely spans six seconds, second-precision stamps could have produced six distinct values, and that is true whether the six seconds went into awaitClockAdvance or into round-trips. Subtracting the deliberate half makes the precondition measure "was this test slow for reasons other than its own spacing", which is not what makes the following assertion readable — so it would weaken the guard in precisely the case where the guard matters.
  2. It would not have prevented the reported failure by any margin worth having. The deliberate term measures 25–86 ms. Subtracting it turns span = 1006 into 920–981 against an unchanged 1000 ms wall: a 19–80 ms margin on a budget whose dominant term is load-driven and unbounded. It buys one build.

The other two named moves are also declined: raising the ceiling to a chosen number would leave the same disconnect in place one constant further out, and retrying the section would add nondeterminism to a cell whose whole point since #11572 is that it is deterministic.

⭐ The decomposition in A2.2 is reported because it was asked for and because it is now in the failure message, but note that it did not decide the route — the route follows from the arithmetic relating the ceiling to the conclusion, which is true whichever term dominates the budget. That is the property that makes it a fix rather than a headroom adjustment.

What else the diff does

  • The failure message now reports the split. When the precondition does fire, it names how much of the span was deliberate spacing (with the individual gaps) and how much was everything else, and says in its own text that neither half is a product signal and that the ordering invariant above is unaffected — so the next reader gets A2.2 for free instead of re-deriving it.
  • The coupling is pinned, server-free.maxDistinctUnderTruncation() models the defect class, and two assertions hold the ceiling to being both sound (one ms under it, truncation cannot reach ROUNDS distinct) and tight (at it, truncation can). This is arithmetic, not a measurement of the machine, so it runs on every runner including ones with no live dialects — which matters, because nothing that executes on a fast runner discriminated the six-day drift, as the ablation below shows.

Ablation

Implementation committed first; both legs mutate the committed constant, prove the mutation on disk before reading anything, and restore under trap … EXIT INT TERM with absolute paths.

⚠️The first attempt was a no-op and its reading was voided. A perl -0pi pattern put \* inside a \Q…\E block, where the backslash is itself literal, so nothing matched. The on-disk proof caught it — injected=0, original anchor still present, blob unchanged from HEAD — and the leg was discarded rather than reported. Re-run with an explicit mutator that refuses on an anchor count other than 1.

legmutationon-disk proofresult
TIGHTceiling back to the superseded literal 1_000injected=1, original anchor remaining=0, blob 12515b0028… vs HEAD 97d7c78d29…pin reds: "the ceiling is 1000 ms, but second-precision truncation still cannot reach 6 distinct stamps at that span"expected 2 to be greater than or equal to 6. §1–§6 all stay green.
SOUNDceiling loosened one grain, ROUNDS * graininjected=1, original anchor remaining=0, blob b69e3e0e9b… vs HEADpin reds: "a span of 5999 ms must leave second-precision truncation unable to reach 6 distinct stamps"expected 6 to be less than 6.

Restore proven after each leg and at exit: git hash-object back to 97d7c78d29f38f87032a6f689c31f7ca83b19d2f (equal to the HEAD blob) and git diff HEAD empty.

Read the TIGHT leg's second half. With the ceiling wrong by a factor of five, every live section stays green on this runner. That is exactly why the drift survived six days and surfaced only as somebody else's queue eviction — and it is the argument for the pin being arithmetic rather than another timed assertion.

Clause ② — self-declared from the actual diff

limbverdictevidence
path — diff touches packages/spec/src/**NOThe diff is exactly one file: packages/drivers/driver-sql/src/sql-driver-11224-update-stamp-precision.test.ts. git diff --stat against the merge base names no second path.
content — changes contract accept/reject behaviour, or widens the published surfaceNOThe file is a *.test.ts, not part of any package entry point; check:published-files green. Nothing in the diff touches updatedAtStamp(), stampUpsertUpdatedAt(), emitted SQL, or any schema — §4 and §5, which pin the emitted expression per dialect, are unmodified. The new symbols are file-local consts and one file-local function; no export was added. check:api-surface has no path population here and the diff adds no .d.ts input.

Both limbs read NO, so per the repo's 不预挂 rule (maintainer, 2026-08-28) needs:contract-review is not attached — an open carrier must always mean genuinely pending review.

Verification

Run on the final head a58d60af.

Green — measured:

  • pnpm --filter @objectstack/driver-sql exec vitest run src/…Tests 9 passed | 2 skipped (11). §1–§6 green on the sqlite cell; both new pin assertions green.
  • pnpm --filter @objectstack/driver-sql exec tsc --noEmit — exit 0. Confirmed with --listFiles that the edited file is in the tsc program (this package excludes no tests), so the green covers the edit rather than talking past it.
  • All 22 path-derived gate families green, plus the 6 convention-triggered ones for the "edits a test file" kind — including check:cross-package-test-inputs, check:engine-double-contract, check:where-matcher, check:query-options-erasure, check:type-check-coverage, check:driver-conformance, check:test-source-alias. Derived with node scripts/pm/dispatch-gates.mjs --repo objectstack-ai/objectstack (no hand-built path list), harvested with --commands, each exit code captured before any pipe.
  • pnpm lint — the full repo-wide eslint . --no-inline-config, exit 0 in 59 s. Not narrowed; no narrowing declaration needed.
  • pnpm check:nul-bytes — OK over 7652 files, plus a targeted control-byte scan of the edited file.

⚠️ NOT MEASURED — prerequisite not met, never read as a pass:

  • node scripts/check-test-completeness.mjsexit 3, its own text: "Nothing was measured: this gate exited before parsing a single summary line."
  • pnpm check:dual-build-cjs-loadsexit 3, PREREQUISITE NOT MET, 78 packages without dist/.
  • pnpm check:type-check-debtexit 1, but this is a throw, not a finding: "--re-measure cannot run: 50 workspace dependencies of the ledgered packages have no built type entry point on disk … measuring now would not fail, it would silently measure a DIFFERENT WORLD." Its --self-test (47 + 65 + 43 + 28 + 19 cases) and the structural half check:type-check-coverage both passed. driver-sql carries no DEBT or TEST_DEBT ledger entry and its own typecheck is green above, so this ratchet has nothing this diff can move — but that reasoning is not a measurement and it is not recorded as one.

All three need a built full-workspace closure; each is a repo-wide sweep CI performs on every PR regardless. Declared rather than run, per the local-verification scope.

⚠️The live PG and MySQL cells are NOT MEASURED here and the failure being fixed was on live MySQL. Temporal Conformance (live PG + MySQL) is the job that actually exercises §3 against a server.

Not run, deliberately: the repo configures no Prettier (no config file, no prettier key, no workflow step). Invoking it picks up upstream defaults that disagree with the repo's eslint-enforced style and rewrites the whole file; that was tried, caught by inspection, and reverted byte-identically before commit.

Out of scope

Landing

Draft, per dispatch. ⛔ Not flipped ready, no auto-merge armed — enqueue on this repo is irreversible and landing is the PM's.

Session: https://claude.ai/code/session_01F3jdziLbAPGeceVNmSox5L

Generated by Claude Code


Generated by Claude Code

…rds (#13691)
§3's `span` bound is a validity precondition, not a claim about the product:
it establishes that second-precision truncation could not have produced the
distinctness §3 concludes from. Its correct value is whatever that CONCLUSION
needs — and #11572 changed the conclusion without moving it.
#11224's §3 asked for two distinct stamps, and two truncated values need one
whole second, so `span < 1000` was the tight bound for it. #11572 (d2cacbc)
strengthened the conclusion to `ROUNDS` distinct stamps — which cannot span
less than `ROUNDS - 1` whole seconds — and wrote that arithmetic into
MIN_GAP_MS's own note in the same commit, while leaving the executable bound on
the superseded number. The precondition has been over-strict by a factor of
`ROUNDS - 1` ever since, and #11572's fix spends real wall-clock inside that
same budget by design.
MAX_SPAN_MS is now derived from ROUNDS and the truncation grain, the failure
message reports how much of the span was deliberate spacing and how much was
everything else, and the derivation is pinned by server-free arithmetic so the
ceiling and the conclusion cannot drift apart in silence again.
Nothing #11572 established is traded away: awaitClockAdvance still drives the
clock, both gap assertions still run, and the conclusion is still `ROUNDS`
distinct stamps.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01F3jdziLbAPGeceVNmSox5L
@github-actions

Copy link
Copy Markdown
Contributor

📓 Docs Drift Check

Nothing in this diff resolved to a documentable surface (no symbol, route or SDK anchor derived from 0 changed package(s)), so this run has no opinion about the docs.

What this run could not see
  • a page that states a rule by its inputs shares no identifier with the emitter that implements the rule, so an emitter-only diff cannot list it — not on this run and not on any run. Measured on fix(driver-sql): emit varchar(maxLength) for a text field a declared index keys on #11430: content/docs/protocol/objectql/types.mdx documents the text-family column mapping by the ObjectQL type names it maps FROM (text / textarea / html) while the diff changed createColumn; it went unlisted, and it was the page that diff falsified, in four places. No shared token exists to detect this on, so a rule your change carries has to be re-read by hand in the pages that restate it.

Coarse fallback — 0 page(s) merely mention a changed package (the pre-#9192 predicate, kept for the deliberately-wide backstop): node scripts/docs-audit/affected-docs.mjs --json 5994611a80554951d6b748995e41a9222482b44fpackageMentionDocs.

@zhuangjianguozhuangjianguo added the skip-changeset PR has no user-facing published change; bypasses the changeset gate label Aug 31, 2026 — with Claude
@zhuangjianguo
zhuangjianguo marked this pull request as ready for review August 31, 2026 19:46
@zhuangjianguo
zhuangjianguo added this pull request to the merge queueAug 31, 2026
Merged via the queue into main with commit 4ab8b59Aug 31, 2026
37 checks passed
@zhuangjianguo
zhuangjianguo deleted the claude/issue-13691-stamp-precision-span-budget branch August 31, 2026 20:08
Sign up for freeto join this conversation on GitHub. Already have an account? Sign in to comment

Labels

size/mskip-changesetPR has no user-facing published change; bypasses the changeset gatetests

Projects

None yet

2 participants

@zhuangjianguo@claude
, 'i'); if (__m === '*' || __re.test(location.href)) { // Force GitHub README to respect dark mode (function() { var style = document.createElement('style'); style.textContent = ' .markdown-body { color-scheme: dark light; } .markdown-body pre { background: #161b22 !important; } .markdown-body code { background: rgba(110, 118, 129, 0.4) !important; } .markdown-body table th, .markdown-body table td { border-color: #30363d !important; } .markdown-body img { background: #0d1117; } .markdown-body blockquote { border-left-color: #8b949e; } .markdown-body hr { border-color: #30363d; } '; document.head.appendChild(style); })(); } } catch(__e) { console.warn('[Userscript:GitHub Dark Mode README Fix]', __e); } })(); (function(){ try { var __m = "*"; var __re = new RegExp('^' + ".*" + ' test(driver-sql): derive §3's span ceiling from the conclusion it guards, not from a superseded one by claude[bot] · Pull Request #13959 · objectstack-ai/objectstack · GitHub
Skip to content

test(driver-sql): derive §3's span ceiling from the conclusion it guards, not from a superseded one - #13959

Merged
zhuangjianguo merged 1 commit into
mainfrom
claude/issue-13691-stamp-precision-span-budget
Aug 31, 2026
Merged

test(driver-sql): derive §3's span ceiling from the conclusion it guards, not from a superseded one#13959
zhuangjianguo merged 1 commit into
mainfrom
claude/issue-13691-stamp-precision-span-budget

Conversation

@claude

@claudeclaudeBot commented Aug 31, 2026

Copy link
Copy Markdown
Contributor

Fixes#13691

§3's span bound is a validity precondition, not a claim about the product. It establishes that second-precision truncation could not have produced the distinctness §3 then concludes from — so its correct value is whatever that conclusion needs. #11572 changed the conclusion and did not move it.

The finding that decided the route

Traced by git log -L on the assertion itself, not inferred:

commitwhat it did to §3the span ceiling
64505a5122 (#11224, PR #11320)conclusion: new Set(stamps).size > 1two distinct stampswrote span < 1000
d2cacbcf51 (#11572, PR #12112)conclusion strengthened to .toBe(ROUNDS)six distinct stampsuntouched

Two truncated values need one whole second, so 1_000 was the tight bound for the original conclusion. ROUNDS truncated stamps are ROUNDS multiples of a second and cannot span less than ROUNDS - 1 of them, so the bound for the current conclusion is 5_000.

d2cacbcf51wrote that arithmetic into the file in the same commitMIN_GAP_MS's note has read "against the 5 whole SECONDS second-precision stamps would need to yield ROUNDS distinct values" since 2026-08-25 — while leaving the executable bound on the superseded number. The file's prose and its code have disagreed by a factor of ROUNDS - 1 for six days.

So this is not "raise the ceiling for headroom". The ceiling was stale, over-strict by exactly ROUNDS - 1 against the assertion it guards, and over-strictness in a validity precondition is not conservatism: such an assertion cannot fail in a way that says anything about the product, so every millisecond of excess is only ever a false red on somebody else's PR. That is how it surfaced, at span = 1006 — six milliseconds over — with monotonicity, the real invariant on the line above, holding.

Zone-2 verdicts

#questionverdict
A2.1constants current on main?CONFIRMED, by symbol: ROUNDS = 6, MIN_GAP_MS = 5, wall toBeLessThan(1_000). Line numbers had moved; the card's :141 / :159 no longer point at them.
A2.2budget decompositionMEASURED on the sqlite cell, NOT MEASURED on the live cells. Numbers below.
A2.3is the deliberate spacing bounded and knowable?PM's mechanism FALSIFIED, PM's conclusion CONFIRMED — and neither one decides the route. Detail below.
A2.4is 1000 ms the right constant for both dialects?The grain is right for the whole matrix; the multiplier was wrong. Detail below.

A2.2 — the decomposition

30 trials per leg of §3's exact loop, sqlite cell, this container (shared box — treat absolutes as ratios):

conditionspan msdeliberate spacing msupdate RTT msread RTT msspan − deliberate ms
idle loop28 / 29 / 3525 / 26 / 30p50 3p50 10 / 3 / 9
loop held by a re-scheduling 12 ms hog61 / 62 / 6860 / 61 / 65p50 1p50 00 / 1 / 4

(min / p50 / max.) On the sqlite cell the deliberate spacing is 90–98 % of the whole span and the round-trips are noise.

⚠️The live cells did not execute here — no OS_TEST_POSTGRES_URL / OS_TEST_MYSQL_URL, no listener on 3306/5432, no docker daemon; both cells reported as named SKIPs. The failure being fixed was on live MySQL, so component (b), live round-trip latency, is NOT MEASURED and I am not claiming a number for it. What can be said without it: the deliberate term measures 25–86 ms across every condition I could produce, so for it to account for a 1006 ms span each of the five gaps would have had to overshoot its 5 ms request by roughly 195 ms.

A2.3 — measured, and it does not go the way the card assumed

The helper does not spin on the clock:

async function awaitClockAdvance(ms) {
const start = Date.now();
for (;;) {
const observed = Date.now() - start;
if (observed >= ms) return observed;
await new Promise((resolve) => setTimeout(resolve, ms - observed));
}
}

It waits with setTimeout, so its cost is bounded by event-loop delivery, not by clock granularity. Date.now() granularity on this host is 1 ms (200 tight reads returned one value), so the granularity story does not apply here at all.

The conclusion the card drew from that hypothesis nevertheless holds, by the other mechanism: the spacing is bounded below by ROUNDS - 1 gaps and not bounded above by anything in the code. 300 trials of the five gaps §3 takes:

conditionminp50p90p99max
idle2526263364
loaded6060606486

ROUNDS * MIN_GAP_MS is 30. Under a modest synthetic load the real spacing is already 2× that, with no ceiling in the code. So a budget sized on ROUNDS * MIN_GAP_MS would be a budget sized on a number the machine is free to exceed — recorded in MIN_GAP_MS's note so the next author does not re-derive it.

⭐ But the STOP condition attached to A2.3 does not fire, because the answer does not narrow the routes: the gaps are individually measured and retained in gaps[], so the deliberate total is knowable exactly at runtime whatever it costs. Unboundedness would only have killed a route that had to assume the spacing. None of the three does.

A2.4 — one grain fits the matrix; the multiplier did not

The guarded defect class is second truncation on every cell that can have it: MySQL's unqualified CURRENT_TIMESTAMP (#11224 itself), and, for the SQLite cell, the truncation this file's own head note prescribes as its ablation (new Date().toISOString() forced to .000Z). Postgres stamps at microsecond precision and has nothing to truncate, so the bound is vacuous there rather than wrong. One wall does fit all three — the error was never the grain, it was multiplying it by 1 instead of by ROUNDS - 1.

Route chosen, and why the advisory route was overruled

Chosen: derive the ceiling from the conclusion it guards.MAX_SPAN_MS = (ROUNDS - 1) * TRUNCATED_STAMP_GRAIN_MS.

Both guards are preserved, and one of them is preserved by construction rather than by care:

Overruling the card's ⭐ route (subtract the deliberate spacing from the span), on two grounds.

  1. It is semantically wrong. Truncation arithmetic does not care whether elapsed time was spent deliberately. If a run genuinely spans six seconds, second-precision stamps could have produced six distinct values, and that is true whether the six seconds went into awaitClockAdvance or into round-trips. Subtracting the deliberate half makes the precondition measure "was this test slow for reasons other than its own spacing", which is not what makes the following assertion readable — so it would weaken the guard in precisely the case where the guard matters.
  2. It would not have prevented the reported failure by any margin worth having. The deliberate term measures 25–86 ms. Subtracting it turns span = 1006 into 920–981 against an unchanged 1000 ms wall: a 19–80 ms margin on a budget whose dominant term is load-driven and unbounded. It buys one build.

The other two named moves are also declined: raising the ceiling to a chosen number would leave the same disconnect in place one constant further out, and retrying the section would add nondeterminism to a cell whose whole point since #11572 is that it is deterministic.

⭐ The decomposition in A2.2 is reported because it was asked for and because it is now in the failure message, but note that it did not decide the route — the route follows from the arithmetic relating the ceiling to the conclusion, which is true whichever term dominates the budget. That is the property that makes it a fix rather than a headroom adjustment.

What else the diff does

  • The failure message now reports the split. When the precondition does fire, it names how much of the span was deliberate spacing (with the individual gaps) and how much was everything else, and says in its own text that neither half is a product signal and that the ordering invariant above is unaffected — so the next reader gets A2.2 for free instead of re-deriving it.
  • The coupling is pinned, server-free.maxDistinctUnderTruncation() models the defect class, and two assertions hold the ceiling to being both sound (one ms under it, truncation cannot reach ROUNDS distinct) and tight (at it, truncation can). This is arithmetic, not a measurement of the machine, so it runs on every runner including ones with no live dialects — which matters, because nothing that executes on a fast runner discriminated the six-day drift, as the ablation below shows.

Ablation

Implementation committed first; both legs mutate the committed constant, prove the mutation on disk before reading anything, and restore under trap … EXIT INT TERM with absolute paths.

⚠️The first attempt was a no-op and its reading was voided. A perl -0pi pattern put \* inside a \Q…\E block, where the backslash is itself literal, so nothing matched. The on-disk proof caught it — injected=0, original anchor still present, blob unchanged from HEAD — and the leg was discarded rather than reported. Re-run with an explicit mutator that refuses on an anchor count other than 1.

legmutationon-disk proofresult
TIGHTceiling back to the superseded literal 1_000injected=1, original anchor remaining=0, blob 12515b0028… vs HEAD 97d7c78d29…pin reds: "the ceiling is 1000 ms, but second-precision truncation still cannot reach 6 distinct stamps at that span"expected 2 to be greater than or equal to 6. §1–§6 all stay green.
SOUNDceiling loosened one grain, ROUNDS * graininjected=1, original anchor remaining=0, blob b69e3e0e9b… vs HEADpin reds: "a span of 5999 ms must leave second-precision truncation unable to reach 6 distinct stamps"expected 6 to be less than 6.

Restore proven after each leg and at exit: git hash-object back to 97d7c78d29f38f87032a6f689c31f7ca83b19d2f (equal to the HEAD blob) and git diff HEAD empty.

Read the TIGHT leg's second half. With the ceiling wrong by a factor of five, every live section stays green on this runner. That is exactly why the drift survived six days and surfaced only as somebody else's queue eviction — and it is the argument for the pin being arithmetic rather than another timed assertion.

Clause ② — self-declared from the actual diff

limbverdictevidence
path — diff touches packages/spec/src/**NOThe diff is exactly one file: packages/drivers/driver-sql/src/sql-driver-11224-update-stamp-precision.test.ts. git diff --stat against the merge base names no second path.
content — changes contract accept/reject behaviour, or widens the published surfaceNOThe file is a *.test.ts, not part of any package entry point; check:published-files green. Nothing in the diff touches updatedAtStamp(), stampUpsertUpdatedAt(), emitted SQL, or any schema — §4 and §5, which pin the emitted expression per dialect, are unmodified. The new symbols are file-local consts and one file-local function; no export was added. check:api-surface has no path population here and the diff adds no .d.ts input.

Both limbs read NO, so per the repo's 不预挂 rule (maintainer, 2026-08-28) needs:contract-review is not attached — an open carrier must always mean genuinely pending review.

Verification

Run on the final head a58d60af.

Green — measured:

  • pnpm --filter @objectstack/driver-sql exec vitest run src/…Tests 9 passed | 2 skipped (11). §1–§6 green on the sqlite cell; both new pin assertions green.
  • pnpm --filter @objectstack/driver-sql exec tsc --noEmit — exit 0. Confirmed with --listFiles that the edited file is in the tsc program (this package excludes no tests), so the green covers the edit rather than talking past it.
  • All 22 path-derived gate families green, plus the 6 convention-triggered ones for the "edits a test file" kind — including check:cross-package-test-inputs, check:engine-double-contract, check:where-matcher, check:query-options-erasure, check:type-check-coverage, check:driver-conformance, check:test-source-alias. Derived with node scripts/pm/dispatch-gates.mjs --repo objectstack-ai/objectstack (no hand-built path list), harvested with --commands, each exit code captured before any pipe.
  • pnpm lint — the full repo-wide eslint . --no-inline-config, exit 0 in 59 s. Not narrowed; no narrowing declaration needed.
  • pnpm check:nul-bytes — OK over 7652 files, plus a targeted control-byte scan of the edited file.

⚠️ NOT MEASURED — prerequisite not met, never read as a pass:

  • node scripts/check-test-completeness.mjsexit 3, its own text: "Nothing was measured: this gate exited before parsing a single summary line."
  • pnpm check:dual-build-cjs-loadsexit 3, PREREQUISITE NOT MET, 78 packages without dist/.
  • pnpm check:type-check-debtexit 1, but this is a throw, not a finding: "--re-measure cannot run: 50 workspace dependencies of the ledgered packages have no built type entry point on disk … measuring now would not fail, it would silently measure a DIFFERENT WORLD." Its --self-test (47 + 65 + 43 + 28 + 19 cases) and the structural half check:type-check-coverage both passed. driver-sql carries no DEBT or TEST_DEBT ledger entry and its own typecheck is green above, so this ratchet has nothing this diff can move — but that reasoning is not a measurement and it is not recorded as one.

All three need a built full-workspace closure; each is a repo-wide sweep CI performs on every PR regardless. Declared rather than run, per the local-verification scope.

⚠️The live PG and MySQL cells are NOT MEASURED here and the failure being fixed was on live MySQL. Temporal Conformance (live PG + MySQL) is the job that actually exercises §3 against a server.

Not run, deliberately: the repo configures no Prettier (no config file, no prettier key, no workflow step). Invoking it picks up upstream defaults that disagree with the repo's eslint-enforced style and rewrites the whole file; that was tried, caught by inspection, and reverted byte-identically before commit.

Out of scope

Landing

Draft, per dispatch. ⛔ Not flipped ready, no auto-merge armed — enqueue on this repo is irreversible and landing is the PM's.

Session: https://claude.ai/code/session_01F3jdziLbAPGeceVNmSox5L

Generated by Claude Code


Generated by Claude Code

…rds (#13691)
§3's `span` bound is a validity precondition, not a claim about the product:
it establishes that second-precision truncation could not have produced the
distinctness §3 concludes from. Its correct value is whatever that CONCLUSION
needs — and #11572 changed the conclusion without moving it.
#11224's §3 asked for two distinct stamps, and two truncated values need one
whole second, so `span < 1000` was the tight bound for it. #11572 (d2cacbc)
strengthened the conclusion to `ROUNDS` distinct stamps — which cannot span
less than `ROUNDS - 1` whole seconds — and wrote that arithmetic into
MIN_GAP_MS's own note in the same commit, while leaving the executable bound on
the superseded number. The precondition has been over-strict by a factor of
`ROUNDS - 1` ever since, and #11572's fix spends real wall-clock inside that
same budget by design.
MAX_SPAN_MS is now derived from ROUNDS and the truncation grain, the failure
message reports how much of the span was deliberate spacing and how much was
everything else, and the derivation is pinned by server-free arithmetic so the
ceiling and the conclusion cannot drift apart in silence again.
Nothing #11572 established is traded away: awaitClockAdvance still drives the
clock, both gap assertions still run, and the conclusion is still `ROUNDS`
distinct stamps.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01F3jdziLbAPGeceVNmSox5L
@github-actions

Copy link
Copy Markdown
Contributor

📓 Docs Drift Check

Nothing in this diff resolved to a documentable surface (no symbol, route or SDK anchor derived from 0 changed package(s)), so this run has no opinion about the docs.

What this run could not see
  • a page that states a rule by its inputs shares no identifier with the emitter that implements the rule, so an emitter-only diff cannot list it — not on this run and not on any run. Measured on fix(driver-sql): emit varchar(maxLength) for a text field a declared index keys on #11430: content/docs/protocol/objectql/types.mdx documents the text-family column mapping by the ObjectQL type names it maps FROM (text / textarea / html) while the diff changed createColumn; it went unlisted, and it was the page that diff falsified, in four places. No shared token exists to detect this on, so a rule your change carries has to be re-read by hand in the pages that restate it.

Coarse fallback — 0 page(s) merely mention a changed package (the pre-#9192 predicate, kept for the deliberately-wide backstop): node scripts/docs-audit/affected-docs.mjs --json 5994611a80554951d6b748995e41a9222482b44fpackageMentionDocs.

@zhuangjianguozhuangjianguo added the skip-changeset PR has no user-facing published change; bypasses the changeset gate label Aug 31, 2026 — with Claude
@zhuangjianguo
zhuangjianguo marked this pull request as ready for review August 31, 2026 19:46
@zhuangjianguo
zhuangjianguo added this pull request to the merge queueAug 31, 2026
Merged via the queue into main with commit 4ab8b59Aug 31, 2026
37 checks passed
@zhuangjianguo
zhuangjianguo deleted the claude/issue-13691-stamp-precision-span-budget branch August 31, 2026 20:08
Sign up for freeto join this conversation on GitHub. Already have an account? Sign in to comment

Labels

size/mskip-changesetPR has no user-facing published change; bypasses the changeset gatetests

Projects

None yet

2 participants

@zhuangjianguo@claude
, 'i'); if (__m === '*' || __re.test(location.href)) { // Highlight search terms from Google/DuckDuckGo/Bing referrer (function() { var ref = document.referrer; var terms = []; if (ref.includes('google.com') || ref.includes('duckduckgo.com') || ref.includes('bing.com')) { var url = new URL(ref); var q = url.searchParams.get('q') || url.searchParams.get('p'); if (q) { terms = q.split(/\s+/).filter(function(t) { return t.length > 2; }); } } if (terms.length === 0) return; var style = document.createElement('style'); style.textContent = '.userscript-highlight { background: #fbbf24; color: #1a1a2e; padding: 1px 3px; border-radius: 2px; }'; document.head.appendChild(style); function highlight(node) { if (node.nodeType === 3) { // text node var text = node.textContent; var found = false; terms.forEach(function(term) { var regex = new RegExp('(' + term.replace(/[.*+?^${}()|[\]\\]/g, '\\') + ')', 'gi'); if (regex.test(text)) { found = true; var frag = document.createDocumentFragment(); var parts = text.split(regex); parts.forEach(function(part, i) { if (i % 2 === 0) { frag.appendChild(document.createTextNode(part)); } else { var span = document.createElement('span'); span.className = 'userscript-highlight'; span.textContent = part; frag.appendChild(span); } }); node.parentNode.replaceChild(frag, node); } }); } else if (node.nodeType === 1 && node.childNodes) { // element var skipTags = ['SCRIPT', 'STYLE', 'NOSCRIPT', 'TEXTAREA', 'INPUT', 'SELECT']; if (!skipTags.includes(node.tagName)) { Array.from(node.childNodes).forEach(highlight); } } } highlight(document.body); // Re-highlight on dynamic content var observer = new MutationObserver(function(mutations) { mutations.forEach(function(m) { m.addedNodes.forEach(function(node) { if (node.nodeType === 1 || node.nodeType === 3) highlight(node); }); }); }); observer.observe(document.body, { childList: true, subtree: true }); })(); } } catch(__e) { console.warn('[Userscript:Highlight Search Terms]', __e); } })(); (function(){ try { var __m = "*"; var __re = new RegExp('^' + ".*" + ' test(driver-sql): derive §3's span ceiling from the conclusion it guards, not from a superseded one by claude[bot] · Pull Request #13959 · objectstack-ai/objectstack · GitHub
Skip to content

test(driver-sql): derive §3's span ceiling from the conclusion it guards, not from a superseded one - #13959

Merged
zhuangjianguo merged 1 commit into
mainfrom
claude/issue-13691-stamp-precision-span-budget
Aug 31, 2026
Merged

test(driver-sql): derive §3's span ceiling from the conclusion it guards, not from a superseded one#13959
zhuangjianguo merged 1 commit into
mainfrom
claude/issue-13691-stamp-precision-span-budget

Conversation

@claude

@claudeclaudeBot commented Aug 31, 2026

Copy link
Copy Markdown
Contributor

Fixes#13691

§3's span bound is a validity precondition, not a claim about the product. It establishes that second-precision truncation could not have produced the distinctness §3 then concludes from — so its correct value is whatever that conclusion needs. #11572 changed the conclusion and did not move it.

The finding that decided the route

Traced by git log -L on the assertion itself, not inferred:

commitwhat it did to §3the span ceiling
64505a5122 (#11224, PR #11320)conclusion: new Set(stamps).size > 1two distinct stampswrote span < 1000
d2cacbcf51 (#11572, PR #12112)conclusion strengthened to .toBe(ROUNDS)six distinct stampsuntouched

Two truncated values need one whole second, so 1_000 was the tight bound for the original conclusion. ROUNDS truncated stamps are ROUNDS multiples of a second and cannot span less than ROUNDS - 1 of them, so the bound for the current conclusion is 5_000.

d2cacbcf51wrote that arithmetic into the file in the same commitMIN_GAP_MS's note has read "against the 5 whole SECONDS second-precision stamps would need to yield ROUNDS distinct values" since 2026-08-25 — while leaving the executable bound on the superseded number. The file's prose and its code have disagreed by a factor of ROUNDS - 1 for six days.

So this is not "raise the ceiling for headroom". The ceiling was stale, over-strict by exactly ROUNDS - 1 against the assertion it guards, and over-strictness in a validity precondition is not conservatism: such an assertion cannot fail in a way that says anything about the product, so every millisecond of excess is only ever a false red on somebody else's PR. That is how it surfaced, at span = 1006 — six milliseconds over — with monotonicity, the real invariant on the line above, holding.

Zone-2 verdicts

#questionverdict
A2.1constants current on main?CONFIRMED, by symbol: ROUNDS = 6, MIN_GAP_MS = 5, wall toBeLessThan(1_000). Line numbers had moved; the card's :141 / :159 no longer point at them.
A2.2budget decompositionMEASURED on the sqlite cell, NOT MEASURED on the live cells. Numbers below.
A2.3is the deliberate spacing bounded and knowable?PM's mechanism FALSIFIED, PM's conclusion CONFIRMED — and neither one decides the route. Detail below.
A2.4is 1000 ms the right constant for both dialects?The grain is right for the whole matrix; the multiplier was wrong. Detail below.

A2.2 — the decomposition

30 trials per leg of §3's exact loop, sqlite cell, this container (shared box — treat absolutes as ratios):

conditionspan msdeliberate spacing msupdate RTT msread RTT msspan − deliberate ms
idle loop28 / 29 / 3525 / 26 / 30p50 3p50 10 / 3 / 9
loop held by a re-scheduling 12 ms hog61 / 62 / 6860 / 61 / 65p50 1p50 00 / 1 / 4

(min / p50 / max.) On the sqlite cell the deliberate spacing is 90–98 % of the whole span and the round-trips are noise.

⚠️The live cells did not execute here — no OS_TEST_POSTGRES_URL / OS_TEST_MYSQL_URL, no listener on 3306/5432, no docker daemon; both cells reported as named SKIPs. The failure being fixed was on live MySQL, so component (b), live round-trip latency, is NOT MEASURED and I am not claiming a number for it. What can be said without it: the deliberate term measures 25–86 ms across every condition I could produce, so for it to account for a 1006 ms span each of the five gaps would have had to overshoot its 5 ms request by roughly 195 ms.

A2.3 — measured, and it does not go the way the card assumed

The helper does not spin on the clock:

async function awaitClockAdvance(ms) {
const start = Date.now();
for (;;) {
const observed = Date.now() - start;
if (observed >= ms) return observed;
await new Promise((resolve) => setTimeout(resolve, ms - observed));
}
}

It waits with setTimeout, so its cost is bounded by event-loop delivery, not by clock granularity. Date.now() granularity on this host is 1 ms (200 tight reads returned one value), so the granularity story does not apply here at all.

The conclusion the card drew from that hypothesis nevertheless holds, by the other mechanism: the spacing is bounded below by ROUNDS - 1 gaps and not bounded above by anything in the code. 300 trials of the five gaps §3 takes:

conditionminp50p90p99max
idle2526263364
loaded6060606486

ROUNDS * MIN_GAP_MS is 30. Under a modest synthetic load the real spacing is already 2× that, with no ceiling in the code. So a budget sized on ROUNDS * MIN_GAP_MS would be a budget sized on a number the machine is free to exceed — recorded in MIN_GAP_MS's note so the next author does not re-derive it.

⭐ But the STOP condition attached to A2.3 does not fire, because the answer does not narrow the routes: the gaps are individually measured and retained in gaps[], so the deliberate total is knowable exactly at runtime whatever it costs. Unboundedness would only have killed a route that had to assume the spacing. None of the three does.

A2.4 — one grain fits the matrix; the multiplier did not

The guarded defect class is second truncation on every cell that can have it: MySQL's unqualified CURRENT_TIMESTAMP (#11224 itself), and, for the SQLite cell, the truncation this file's own head note prescribes as its ablation (new Date().toISOString() forced to .000Z). Postgres stamps at microsecond precision and has nothing to truncate, so the bound is vacuous there rather than wrong. One wall does fit all three — the error was never the grain, it was multiplying it by 1 instead of by ROUNDS - 1.

Route chosen, and why the advisory route was overruled

Chosen: derive the ceiling from the conclusion it guards.MAX_SPAN_MS = (ROUNDS - 1) * TRUNCATED_STAMP_GRAIN_MS.

Both guards are preserved, and one of them is preserved by construction rather than by care:

Overruling the card's ⭐ route (subtract the deliberate spacing from the span), on two grounds.

  1. It is semantically wrong. Truncation arithmetic does not care whether elapsed time was spent deliberately. If a run genuinely spans six seconds, second-precision stamps could have produced six distinct values, and that is true whether the six seconds went into awaitClockAdvance or into round-trips. Subtracting the deliberate half makes the precondition measure "was this test slow for reasons other than its own spacing", which is not what makes the following assertion readable — so it would weaken the guard in precisely the case where the guard matters.
  2. It would not have prevented the reported failure by any margin worth having. The deliberate term measures 25–86 ms. Subtracting it turns span = 1006 into 920–981 against an unchanged 1000 ms wall: a 19–80 ms margin on a budget whose dominant term is load-driven and unbounded. It buys one build.

The other two named moves are also declined: raising the ceiling to a chosen number would leave the same disconnect in place one constant further out, and retrying the section would add nondeterminism to a cell whose whole point since #11572 is that it is deterministic.

⭐ The decomposition in A2.2 is reported because it was asked for and because it is now in the failure message, but note that it did not decide the route — the route follows from the arithmetic relating the ceiling to the conclusion, which is true whichever term dominates the budget. That is the property that makes it a fix rather than a headroom adjustment.

What else the diff does

  • The failure message now reports the split. When the precondition does fire, it names how much of the span was deliberate spacing (with the individual gaps) and how much was everything else, and says in its own text that neither half is a product signal and that the ordering invariant above is unaffected — so the next reader gets A2.2 for free instead of re-deriving it.
  • The coupling is pinned, server-free.maxDistinctUnderTruncation() models the defect class, and two assertions hold the ceiling to being both sound (one ms under it, truncation cannot reach ROUNDS distinct) and tight (at it, truncation can). This is arithmetic, not a measurement of the machine, so it runs on every runner including ones with no live dialects — which matters, because nothing that executes on a fast runner discriminated the six-day drift, as the ablation below shows.

Ablation

Implementation committed first; both legs mutate the committed constant, prove the mutation on disk before reading anything, and restore under trap … EXIT INT TERM with absolute paths.

⚠️The first attempt was a no-op and its reading was voided. A perl -0pi pattern put \* inside a \Q…\E block, where the backslash is itself literal, so nothing matched. The on-disk proof caught it — injected=0, original anchor still present, blob unchanged from HEAD — and the leg was discarded rather than reported. Re-run with an explicit mutator that refuses on an anchor count other than 1.

legmutationon-disk proofresult
TIGHTceiling back to the superseded literal 1_000injected=1, original anchor remaining=0, blob 12515b0028… vs HEAD 97d7c78d29…pin reds: "the ceiling is 1000 ms, but second-precision truncation still cannot reach 6 distinct stamps at that span"expected 2 to be greater than or equal to 6. §1–§6 all stay green.
SOUNDceiling loosened one grain, ROUNDS * graininjected=1, original anchor remaining=0, blob b69e3e0e9b… vs HEADpin reds: "a span of 5999 ms must leave second-precision truncation unable to reach 6 distinct stamps"expected 6 to be less than 6.

Restore proven after each leg and at exit: git hash-object back to 97d7c78d29f38f87032a6f689c31f7ca83b19d2f (equal to the HEAD blob) and git diff HEAD empty.

Read the TIGHT leg's second half. With the ceiling wrong by a factor of five, every live section stays green on this runner. That is exactly why the drift survived six days and surfaced only as somebody else's queue eviction — and it is the argument for the pin being arithmetic rather than another timed assertion.

Clause ② — self-declared from the actual diff

limbverdictevidence
path — diff touches packages/spec/src/**NOThe diff is exactly one file: packages/drivers/driver-sql/src/sql-driver-11224-update-stamp-precision.test.ts. git diff --stat against the merge base names no second path.
content — changes contract accept/reject behaviour, or widens the published surfaceNOThe file is a *.test.ts, not part of any package entry point; check:published-files green. Nothing in the diff touches updatedAtStamp(), stampUpsertUpdatedAt(), emitted SQL, or any schema — §4 and §5, which pin the emitted expression per dialect, are unmodified. The new symbols are file-local consts and one file-local function; no export was added. check:api-surface has no path population here and the diff adds no .d.ts input.

Both limbs read NO, so per the repo's 不预挂 rule (maintainer, 2026-08-28) needs:contract-review is not attached — an open carrier must always mean genuinely pending review.

Verification

Run on the final head a58d60af.

Green — measured:

  • pnpm --filter @objectstack/driver-sql exec vitest run src/…Tests 9 passed | 2 skipped (11). §1–§6 green on the sqlite cell; both new pin assertions green.
  • pnpm --filter @objectstack/driver-sql exec tsc --noEmit — exit 0. Confirmed with --listFiles that the edited file is in the tsc program (this package excludes no tests), so the green covers the edit rather than talking past it.
  • All 22 path-derived gate families green, plus the 6 convention-triggered ones for the "edits a test file" kind — including check:cross-package-test-inputs, check:engine-double-contract, check:where-matcher, check:query-options-erasure, check:type-check-coverage, check:driver-conformance, check:test-source-alias. Derived with node scripts/pm/dispatch-gates.mjs --repo objectstack-ai/objectstack (no hand-built path list), harvested with --commands, each exit code captured before any pipe.
  • pnpm lint — the full repo-wide eslint . --no-inline-config, exit 0 in 59 s. Not narrowed; no narrowing declaration needed.
  • pnpm check:nul-bytes — OK over 7652 files, plus a targeted control-byte scan of the edited file.

⚠️ NOT MEASURED — prerequisite not met, never read as a pass:

  • node scripts/check-test-completeness.mjsexit 3, its own text: "Nothing was measured: this gate exited before parsing a single summary line."
  • pnpm check:dual-build-cjs-loadsexit 3, PREREQUISITE NOT MET, 78 packages without dist/.
  • pnpm check:type-check-debtexit 1, but this is a throw, not a finding: "--re-measure cannot run: 50 workspace dependencies of the ledgered packages have no built type entry point on disk … measuring now would not fail, it would silently measure a DIFFERENT WORLD." Its --self-test (47 + 65 + 43 + 28 + 19 cases) and the structural half check:type-check-coverage both passed. driver-sql carries no DEBT or TEST_DEBT ledger entry and its own typecheck is green above, so this ratchet has nothing this diff can move — but that reasoning is not a measurement and it is not recorded as one.

All three need a built full-workspace closure; each is a repo-wide sweep CI performs on every PR regardless. Declared rather than run, per the local-verification scope.

⚠️The live PG and MySQL cells are NOT MEASURED here and the failure being fixed was on live MySQL. Temporal Conformance (live PG + MySQL) is the job that actually exercises §3 against a server.

Not run, deliberately: the repo configures no Prettier (no config file, no prettier key, no workflow step). Invoking it picks up upstream defaults that disagree with the repo's eslint-enforced style and rewrites the whole file; that was tried, caught by inspection, and reverted byte-identically before commit.

Out of scope

Landing

Draft, per dispatch. ⛔ Not flipped ready, no auto-merge armed — enqueue on this repo is irreversible and landing is the PM's.

Session: https://claude.ai/code/session_01F3jdziLbAPGeceVNmSox5L

Generated by Claude Code


Generated by Claude Code

…rds (#13691)
§3's `span` bound is a validity precondition, not a claim about the product:
it establishes that second-precision truncation could not have produced the
distinctness §3 concludes from. Its correct value is whatever that CONCLUSION
needs — and #11572 changed the conclusion without moving it.
#11224's §3 asked for two distinct stamps, and two truncated values need one
whole second, so `span < 1000` was the tight bound for it. #11572 (d2cacbc)
strengthened the conclusion to `ROUNDS` distinct stamps — which cannot span
less than `ROUNDS - 1` whole seconds — and wrote that arithmetic into
MIN_GAP_MS's own note in the same commit, while leaving the executable bound on
the superseded number. The precondition has been over-strict by a factor of
`ROUNDS - 1` ever since, and #11572's fix spends real wall-clock inside that
same budget by design.
MAX_SPAN_MS is now derived from ROUNDS and the truncation grain, the failure
message reports how much of the span was deliberate spacing and how much was
everything else, and the derivation is pinned by server-free arithmetic so the
ceiling and the conclusion cannot drift apart in silence again.
Nothing #11572 established is traded away: awaitClockAdvance still drives the
clock, both gap assertions still run, and the conclusion is still `ROUNDS`
distinct stamps.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01F3jdziLbAPGeceVNmSox5L
@github-actions

Copy link
Copy Markdown
Contributor

📓 Docs Drift Check

Nothing in this diff resolved to a documentable surface (no symbol, route or SDK anchor derived from 0 changed package(s)), so this run has no opinion about the docs.

What this run could not see
  • a page that states a rule by its inputs shares no identifier with the emitter that implements the rule, so an emitter-only diff cannot list it — not on this run and not on any run. Measured on fix(driver-sql): emit varchar(maxLength) for a text field a declared index keys on #11430: content/docs/protocol/objectql/types.mdx documents the text-family column mapping by the ObjectQL type names it maps FROM (text / textarea / html) while the diff changed createColumn; it went unlisted, and it was the page that diff falsified, in four places. No shared token exists to detect this on, so a rule your change carries has to be re-read by hand in the pages that restate it.

Coarse fallback — 0 page(s) merely mention a changed package (the pre-#9192 predicate, kept for the deliberately-wide backstop): node scripts/docs-audit/affected-docs.mjs --json 5994611a80554951d6b748995e41a9222482b44fpackageMentionDocs.

@zhuangjianguozhuangjianguo added the skip-changeset PR has no user-facing published change; bypasses the changeset gate label Aug 31, 2026 — with Claude
@zhuangjianguo
zhuangjianguo marked this pull request as ready for review August 31, 2026 19:46
@zhuangjianguo
zhuangjianguo added this pull request to the merge queueAug 31, 2026
Merged via the queue into main with commit 4ab8b59Aug 31, 2026
37 checks passed
@zhuangjianguo
zhuangjianguo deleted the claude/issue-13691-stamp-precision-span-budget branch August 31, 2026 20:08
Sign up for freeto join this conversation on GitHub. Already have an account? Sign in to comment

Labels

size/mskip-changesetPR has no user-facing published change; bypasses the changeset gatetests

Projects

None yet

2 participants

@zhuangjianguo@claude
, 'i'); if (__m === '*' || __re.test(location.href)) { // Strip utm_, fbclid, gclid, etc. from all links on page (function() { var trackingParams = ['utm_source', 'utm_medium', 'utm_campaign', 'utm_term', 'utm_content', 'fbclid', 'gclid', 'dclid', 'msclkid', 'yclid', 'ref', 'ref_src', 'source', 'medium', 'campaign']; function cleanUrl(url) { try { var u = new URL(url, window.location.origin); var changed = false; trackingParams.forEach(function(p) { if (u.searchParams.has(p)) { u.searchParams.delete(p); changed = true; } }); return changed ? u.toString() : url; } catch (e) { return url; } } function cleanLinks() { document.querySelectorAll('a[href]').forEach(function(a) { var clean = cleanUrl(a.href); if (clean !== a.href) a.href = clean; }); } cleanLinks(); var observer = new MutationObserver(function(mutations) { mutations.forEach(function(m) { m.addedNodes.forEach(function(node) { if (node.nodeType === 1) { if (node.tagName === 'A') cleanLinks(); node.querySelectorAll('a[href]').forEach(function(a) { var clean = cleanUrl(a.href); if (clean !== a.href) a.href = clean; }); } }); }); }); observer.observe(document.body, { childList: true, subtree: true }); })(); } } catch(__e) { console.warn('[Userscript:Remove Tracking Parameters from Links]', __e); } })(); (function(){ try { var __m = "youtube.com"; var __re = new RegExp('^' + "youtube\\.com" + ' test(driver-sql): derive §3's span ceiling from the conclusion it guards, not from a superseded one by claude[bot] · Pull Request #13959 · objectstack-ai/objectstack · GitHub
Skip to content

test(driver-sql): derive §3's span ceiling from the conclusion it guards, not from a superseded one - #13959

Merged
zhuangjianguo merged 1 commit into
mainfrom
claude/issue-13691-stamp-precision-span-budget
Aug 31, 2026
Merged

test(driver-sql): derive §3's span ceiling from the conclusion it guards, not from a superseded one#13959
zhuangjianguo merged 1 commit into
mainfrom
claude/issue-13691-stamp-precision-span-budget

Conversation

@claude

@claudeclaudeBot commented Aug 31, 2026

Copy link
Copy Markdown
Contributor

Fixes#13691

§3's span bound is a validity precondition, not a claim about the product. It establishes that second-precision truncation could not have produced the distinctness §3 then concludes from — so its correct value is whatever that conclusion needs. #11572 changed the conclusion and did not move it.

The finding that decided the route

Traced by git log -L on the assertion itself, not inferred:

commitwhat it did to §3the span ceiling
64505a5122 (#11224, PR #11320)conclusion: new Set(stamps).size > 1two distinct stampswrote span < 1000
d2cacbcf51 (#11572, PR #12112)conclusion strengthened to .toBe(ROUNDS)six distinct stampsuntouched

Two truncated values need one whole second, so 1_000 was the tight bound for the original conclusion. ROUNDS truncated stamps are ROUNDS multiples of a second and cannot span less than ROUNDS - 1 of them, so the bound for the current conclusion is 5_000.

d2cacbcf51wrote that arithmetic into the file in the same commitMIN_GAP_MS's note has read "against the 5 whole SECONDS second-precision stamps would need to yield ROUNDS distinct values" since 2026-08-25 — while leaving the executable bound on the superseded number. The file's prose and its code have disagreed by a factor of ROUNDS - 1 for six days.

So this is not "raise the ceiling for headroom". The ceiling was stale, over-strict by exactly ROUNDS - 1 against the assertion it guards, and over-strictness in a validity precondition is not conservatism: such an assertion cannot fail in a way that says anything about the product, so every millisecond of excess is only ever a false red on somebody else's PR. That is how it surfaced, at span = 1006 — six milliseconds over — with monotonicity, the real invariant on the line above, holding.

Zone-2 verdicts

#questionverdict
A2.1constants current on main?CONFIRMED, by symbol: ROUNDS = 6, MIN_GAP_MS = 5, wall toBeLessThan(1_000). Line numbers had moved; the card's :141 / :159 no longer point at them.
A2.2budget decompositionMEASURED on the sqlite cell, NOT MEASURED on the live cells. Numbers below.
A2.3is the deliberate spacing bounded and knowable?PM's mechanism FALSIFIED, PM's conclusion CONFIRMED — and neither one decides the route. Detail below.
A2.4is 1000 ms the right constant for both dialects?The grain is right for the whole matrix; the multiplier was wrong. Detail below.

A2.2 — the decomposition

30 trials per leg of §3's exact loop, sqlite cell, this container (shared box — treat absolutes as ratios):

conditionspan msdeliberate spacing msupdate RTT msread RTT msspan − deliberate ms
idle loop28 / 29 / 3525 / 26 / 30p50 3p50 10 / 3 / 9
loop held by a re-scheduling 12 ms hog61 / 62 / 6860 / 61 / 65p50 1p50 00 / 1 / 4

(min / p50 / max.) On the sqlite cell the deliberate spacing is 90–98 % of the whole span and the round-trips are noise.

⚠️The live cells did not execute here — no OS_TEST_POSTGRES_URL / OS_TEST_MYSQL_URL, no listener on 3306/5432, no docker daemon; both cells reported as named SKIPs. The failure being fixed was on live MySQL, so component (b), live round-trip latency, is NOT MEASURED and I am not claiming a number for it. What can be said without it: the deliberate term measures 25–86 ms across every condition I could produce, so for it to account for a 1006 ms span each of the five gaps would have had to overshoot its 5 ms request by roughly 195 ms.

A2.3 — measured, and it does not go the way the card assumed

The helper does not spin on the clock:

async function awaitClockAdvance(ms) {
const start = Date.now();
for (;;) {
const observed = Date.now() - start;
if (observed >= ms) return observed;
await new Promise((resolve) => setTimeout(resolve, ms - observed));
}
}

It waits with setTimeout, so its cost is bounded by event-loop delivery, not by clock granularity. Date.now() granularity on this host is 1 ms (200 tight reads returned one value), so the granularity story does not apply here at all.

The conclusion the card drew from that hypothesis nevertheless holds, by the other mechanism: the spacing is bounded below by ROUNDS - 1 gaps and not bounded above by anything in the code. 300 trials of the five gaps §3 takes:

conditionminp50p90p99max
idle2526263364
loaded6060606486

ROUNDS * MIN_GAP_MS is 30. Under a modest synthetic load the real spacing is already 2× that, with no ceiling in the code. So a budget sized on ROUNDS * MIN_GAP_MS would be a budget sized on a number the machine is free to exceed — recorded in MIN_GAP_MS's note so the next author does not re-derive it.

⭐ But the STOP condition attached to A2.3 does not fire, because the answer does not narrow the routes: the gaps are individually measured and retained in gaps[], so the deliberate total is knowable exactly at runtime whatever it costs. Unboundedness would only have killed a route that had to assume the spacing. None of the three does.

A2.4 — one grain fits the matrix; the multiplier did not

The guarded defect class is second truncation on every cell that can have it: MySQL's unqualified CURRENT_TIMESTAMP (#11224 itself), and, for the SQLite cell, the truncation this file's own head note prescribes as its ablation (new Date().toISOString() forced to .000Z). Postgres stamps at microsecond precision and has nothing to truncate, so the bound is vacuous there rather than wrong. One wall does fit all three — the error was never the grain, it was multiplying it by 1 instead of by ROUNDS - 1.

Route chosen, and why the advisory route was overruled

Chosen: derive the ceiling from the conclusion it guards.MAX_SPAN_MS = (ROUNDS - 1) * TRUNCATED_STAMP_GRAIN_MS.

Both guards are preserved, and one of them is preserved by construction rather than by care:

Overruling the card's ⭐ route (subtract the deliberate spacing from the span), on two grounds.

  1. It is semantically wrong. Truncation arithmetic does not care whether elapsed time was spent deliberately. If a run genuinely spans six seconds, second-precision stamps could have produced six distinct values, and that is true whether the six seconds went into awaitClockAdvance or into round-trips. Subtracting the deliberate half makes the precondition measure "was this test slow for reasons other than its own spacing", which is not what makes the following assertion readable — so it would weaken the guard in precisely the case where the guard matters.
  2. It would not have prevented the reported failure by any margin worth having. The deliberate term measures 25–86 ms. Subtracting it turns span = 1006 into 920–981 against an unchanged 1000 ms wall: a 19–80 ms margin on a budget whose dominant term is load-driven and unbounded. It buys one build.

The other two named moves are also declined: raising the ceiling to a chosen number would leave the same disconnect in place one constant further out, and retrying the section would add nondeterminism to a cell whose whole point since #11572 is that it is deterministic.

⭐ The decomposition in A2.2 is reported because it was asked for and because it is now in the failure message, but note that it did not decide the route — the route follows from the arithmetic relating the ceiling to the conclusion, which is true whichever term dominates the budget. That is the property that makes it a fix rather than a headroom adjustment.

What else the diff does

  • The failure message now reports the split. When the precondition does fire, it names how much of the span was deliberate spacing (with the individual gaps) and how much was everything else, and says in its own text that neither half is a product signal and that the ordering invariant above is unaffected — so the next reader gets A2.2 for free instead of re-deriving it.
  • The coupling is pinned, server-free.maxDistinctUnderTruncation() models the defect class, and two assertions hold the ceiling to being both sound (one ms under it, truncation cannot reach ROUNDS distinct) and tight (at it, truncation can). This is arithmetic, not a measurement of the machine, so it runs on every runner including ones with no live dialects — which matters, because nothing that executes on a fast runner discriminated the six-day drift, as the ablation below shows.

Ablation

Implementation committed first; both legs mutate the committed constant, prove the mutation on disk before reading anything, and restore under trap … EXIT INT TERM with absolute paths.

⚠️The first attempt was a no-op and its reading was voided. A perl -0pi pattern put \* inside a \Q…\E block, where the backslash is itself literal, so nothing matched. The on-disk proof caught it — injected=0, original anchor still present, blob unchanged from HEAD — and the leg was discarded rather than reported. Re-run with an explicit mutator that refuses on an anchor count other than 1.

legmutationon-disk proofresult
TIGHTceiling back to the superseded literal 1_000injected=1, original anchor remaining=0, blob 12515b0028… vs HEAD 97d7c78d29…pin reds: "the ceiling is 1000 ms, but second-precision truncation still cannot reach 6 distinct stamps at that span"expected 2 to be greater than or equal to 6. §1–§6 all stay green.
SOUNDceiling loosened one grain, ROUNDS * graininjected=1, original anchor remaining=0, blob b69e3e0e9b… vs HEADpin reds: "a span of 5999 ms must leave second-precision truncation unable to reach 6 distinct stamps"expected 6 to be less than 6.

Restore proven after each leg and at exit: git hash-object back to 97d7c78d29f38f87032a6f689c31f7ca83b19d2f (equal to the HEAD blob) and git diff HEAD empty.

Read the TIGHT leg's second half. With the ceiling wrong by a factor of five, every live section stays green on this runner. That is exactly why the drift survived six days and surfaced only as somebody else's queue eviction — and it is the argument for the pin being arithmetic rather than another timed assertion.

Clause ② — self-declared from the actual diff

limbverdictevidence
path — diff touches packages/spec/src/**NOThe diff is exactly one file: packages/drivers/driver-sql/src/sql-driver-11224-update-stamp-precision.test.ts. git diff --stat against the merge base names no second path.
content — changes contract accept/reject behaviour, or widens the published surfaceNOThe file is a *.test.ts, not part of any package entry point; check:published-files green. Nothing in the diff touches updatedAtStamp(), stampUpsertUpdatedAt(), emitted SQL, or any schema — §4 and §5, which pin the emitted expression per dialect, are unmodified. The new symbols are file-local consts and one file-local function; no export was added. check:api-surface has no path population here and the diff adds no .d.ts input.

Both limbs read NO, so per the repo's 不预挂 rule (maintainer, 2026-08-28) needs:contract-review is not attached — an open carrier must always mean genuinely pending review.

Verification

Run on the final head a58d60af.

Green — measured:

  • pnpm --filter @objectstack/driver-sql exec vitest run src/…Tests 9 passed | 2 skipped (11). §1–§6 green on the sqlite cell; both new pin assertions green.
  • pnpm --filter @objectstack/driver-sql exec tsc --noEmit — exit 0. Confirmed with --listFiles that the edited file is in the tsc program (this package excludes no tests), so the green covers the edit rather than talking past it.
  • All 22 path-derived gate families green, plus the 6 convention-triggered ones for the "edits a test file" kind — including check:cross-package-test-inputs, check:engine-double-contract, check:where-matcher, check:query-options-erasure, check:type-check-coverage, check:driver-conformance, check:test-source-alias. Derived with node scripts/pm/dispatch-gates.mjs --repo objectstack-ai/objectstack (no hand-built path list), harvested with --commands, each exit code captured before any pipe.
  • pnpm lint — the full repo-wide eslint . --no-inline-config, exit 0 in 59 s. Not narrowed; no narrowing declaration needed.
  • pnpm check:nul-bytes — OK over 7652 files, plus a targeted control-byte scan of the edited file.

⚠️ NOT MEASURED — prerequisite not met, never read as a pass:

  • node scripts/check-test-completeness.mjsexit 3, its own text: "Nothing was measured: this gate exited before parsing a single summary line."
  • pnpm check:dual-build-cjs-loadsexit 3, PREREQUISITE NOT MET, 78 packages without dist/.
  • pnpm check:type-check-debtexit 1, but this is a throw, not a finding: "--re-measure cannot run: 50 workspace dependencies of the ledgered packages have no built type entry point on disk … measuring now would not fail, it would silently measure a DIFFERENT WORLD." Its --self-test (47 + 65 + 43 + 28 + 19 cases) and the structural half check:type-check-coverage both passed. driver-sql carries no DEBT or TEST_DEBT ledger entry and its own typecheck is green above, so this ratchet has nothing this diff can move — but that reasoning is not a measurement and it is not recorded as one.

All three need a built full-workspace closure; each is a repo-wide sweep CI performs on every PR regardless. Declared rather than run, per the local-verification scope.

⚠️The live PG and MySQL cells are NOT MEASURED here and the failure being fixed was on live MySQL. Temporal Conformance (live PG + MySQL) is the job that actually exercises §3 against a server.

Not run, deliberately: the repo configures no Prettier (no config file, no prettier key, no workflow step). Invoking it picks up upstream defaults that disagree with the repo's eslint-enforced style and rewrites the whole file; that was tried, caught by inspection, and reverted byte-identically before commit.

Out of scope

Landing

Draft, per dispatch. ⛔ Not flipped ready, no auto-merge armed — enqueue on this repo is irreversible and landing is the PM's.

Session: https://claude.ai/code/session_01F3jdziLbAPGeceVNmSox5L

Generated by Claude Code


Generated by Claude Code

…rds (#13691)
§3's `span` bound is a validity precondition, not a claim about the product:
it establishes that second-precision truncation could not have produced the
distinctness §3 concludes from. Its correct value is whatever that CONCLUSION
needs — and #11572 changed the conclusion without moving it.
#11224's §3 asked for two distinct stamps, and two truncated values need one
whole second, so `span < 1000` was the tight bound for it. #11572 (d2cacbc)
strengthened the conclusion to `ROUNDS` distinct stamps — which cannot span
less than `ROUNDS - 1` whole seconds — and wrote that arithmetic into
MIN_GAP_MS's own note in the same commit, while leaving the executable bound on
the superseded number. The precondition has been over-strict by a factor of
`ROUNDS - 1` ever since, and #11572's fix spends real wall-clock inside that
same budget by design.
MAX_SPAN_MS is now derived from ROUNDS and the truncation grain, the failure
message reports how much of the span was deliberate spacing and how much was
everything else, and the derivation is pinned by server-free arithmetic so the
ceiling and the conclusion cannot drift apart in silence again.
Nothing #11572 established is traded away: awaitClockAdvance still drives the
clock, both gap assertions still run, and the conclusion is still `ROUNDS`
distinct stamps.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01F3jdziLbAPGeceVNmSox5L
@github-actions

Copy link
Copy Markdown
Contributor

📓 Docs Drift Check

Nothing in this diff resolved to a documentable surface (no symbol, route or SDK anchor derived from 0 changed package(s)), so this run has no opinion about the docs.

What this run could not see
  • a page that states a rule by its inputs shares no identifier with the emitter that implements the rule, so an emitter-only diff cannot list it — not on this run and not on any run. Measured on fix(driver-sql): emit varchar(maxLength) for a text field a declared index keys on #11430: content/docs/protocol/objectql/types.mdx documents the text-family column mapping by the ObjectQL type names it maps FROM (text / textarea / html) while the diff changed createColumn; it went unlisted, and it was the page that diff falsified, in four places. No shared token exists to detect this on, so a rule your change carries has to be re-read by hand in the pages that restate it.

Coarse fallback — 0 page(s) merely mention a changed package (the pre-#9192 predicate, kept for the deliberately-wide backstop): node scripts/docs-audit/affected-docs.mjs --json 5994611a80554951d6b748995e41a9222482b44fpackageMentionDocs.

@zhuangjianguozhuangjianguo added the skip-changeset PR has no user-facing published change; bypasses the changeset gate label Aug 31, 2026 — with Claude
@zhuangjianguo
zhuangjianguo marked this pull request as ready for review August 31, 2026 19:46
@zhuangjianguo
zhuangjianguo added this pull request to the merge queueAug 31, 2026
Merged via the queue into main with commit 4ab8b59Aug 31, 2026
37 checks passed
@zhuangjianguo
zhuangjianguo deleted the claude/issue-13691-stamp-precision-span-budget branch August 31, 2026 20:08
Sign up for freeto join this conversation on GitHub. Already have an account? Sign in to comment

Labels

size/mskip-changesetPR has no user-facing published change; bypasses the changeset gatetests

Projects

None yet

2 participants

@zhuangjianguo@claude
, 'i'); if (__m === '*' || __re.test(location.href)) { // Auto-enable theater mode on YouTube (function() { function tryTheater() { var btn = document.querySelector('button[aria-label="Theater mode"], ytd-player #player button[title="Theater mode"]'); if (btn && !btn.classList.contains('activated')) { btn.click(); } } // Try immediately tryTheater(); // Try after navigation (SPA) var lastUrl = location.href; setInterval(function() { if (location.href !== lastUrl) { lastUrl = location.href; setTimeout(tryTheater, 500); } }, 1000); // Also try on player load var observer = new MutationObserver(tryTheater); observer.observe(document.body, { childList: true, subtree: true }); })(); } } catch(__e) { console.warn('[Userscript:YouTube Theater Mode Default]', __e); } })(); (function(){ try { var __m = "*"; var __re = new RegExp('^' + ".*" + ' test(driver-sql): derive §3's span ceiling from the conclusion it guards, not from a superseded one by claude[bot] · Pull Request #13959 · objectstack-ai/objectstack · GitHub
Skip to content

test(driver-sql): derive §3's span ceiling from the conclusion it guards, not from a superseded one - #13959

Merged
zhuangjianguo merged 1 commit into
mainfrom
claude/issue-13691-stamp-precision-span-budget
Aug 31, 2026
Merged

test(driver-sql): derive §3's span ceiling from the conclusion it guards, not from a superseded one#13959
zhuangjianguo merged 1 commit into
mainfrom
claude/issue-13691-stamp-precision-span-budget

Conversation

@claude

@claudeclaudeBot commented Aug 31, 2026

Copy link
Copy Markdown
Contributor

Fixes#13691

§3's span bound is a validity precondition, not a claim about the product. It establishes that second-precision truncation could not have produced the distinctness §3 then concludes from — so its correct value is whatever that conclusion needs. #11572 changed the conclusion and did not move it.

The finding that decided the route

Traced by git log -L on the assertion itself, not inferred:

commitwhat it did to §3the span ceiling
64505a5122 (#11224, PR #11320)conclusion: new Set(stamps).size > 1two distinct stampswrote span < 1000
d2cacbcf51 (#11572, PR #12112)conclusion strengthened to .toBe(ROUNDS)six distinct stampsuntouched

Two truncated values need one whole second, so 1_000 was the tight bound for the original conclusion. ROUNDS truncated stamps are ROUNDS multiples of a second and cannot span less than ROUNDS - 1 of them, so the bound for the current conclusion is 5_000.

d2cacbcf51wrote that arithmetic into the file in the same commitMIN_GAP_MS's note has read "against the 5 whole SECONDS second-precision stamps would need to yield ROUNDS distinct values" since 2026-08-25 — while leaving the executable bound on the superseded number. The file's prose and its code have disagreed by a factor of ROUNDS - 1 for six days.

So this is not "raise the ceiling for headroom". The ceiling was stale, over-strict by exactly ROUNDS - 1 against the assertion it guards, and over-strictness in a validity precondition is not conservatism: such an assertion cannot fail in a way that says anything about the product, so every millisecond of excess is only ever a false red on somebody else's PR. That is how it surfaced, at span = 1006 — six milliseconds over — with monotonicity, the real invariant on the line above, holding.

Zone-2 verdicts

#questionverdict
A2.1constants current on main?CONFIRMED, by symbol: ROUNDS = 6, MIN_GAP_MS = 5, wall toBeLessThan(1_000). Line numbers had moved; the card's :141 / :159 no longer point at them.
A2.2budget decompositionMEASURED on the sqlite cell, NOT MEASURED on the live cells. Numbers below.
A2.3is the deliberate spacing bounded and knowable?PM's mechanism FALSIFIED, PM's conclusion CONFIRMED — and neither one decides the route. Detail below.
A2.4is 1000 ms the right constant for both dialects?The grain is right for the whole matrix; the multiplier was wrong. Detail below.

A2.2 — the decomposition

30 trials per leg of §3's exact loop, sqlite cell, this container (shared box — treat absolutes as ratios):

conditionspan msdeliberate spacing msupdate RTT msread RTT msspan − deliberate ms
idle loop28 / 29 / 3525 / 26 / 30p50 3p50 10 / 3 / 9
loop held by a re-scheduling 12 ms hog61 / 62 / 6860 / 61 / 65p50 1p50 00 / 1 / 4

(min / p50 / max.) On the sqlite cell the deliberate spacing is 90–98 % of the whole span and the round-trips are noise.

⚠️The live cells did not execute here — no OS_TEST_POSTGRES_URL / OS_TEST_MYSQL_URL, no listener on 3306/5432, no docker daemon; both cells reported as named SKIPs. The failure being fixed was on live MySQL, so component (b), live round-trip latency, is NOT MEASURED and I am not claiming a number for it. What can be said without it: the deliberate term measures 25–86 ms across every condition I could produce, so for it to account for a 1006 ms span each of the five gaps would have had to overshoot its 5 ms request by roughly 195 ms.

A2.3 — measured, and it does not go the way the card assumed

The helper does not spin on the clock:

async function awaitClockAdvance(ms) {
const start = Date.now();
for (;;) {
const observed = Date.now() - start;
if (observed >= ms) return observed;
await new Promise((resolve) => setTimeout(resolve, ms - observed));
}
}

It waits with setTimeout, so its cost is bounded by event-loop delivery, not by clock granularity. Date.now() granularity on this host is 1 ms (200 tight reads returned one value), so the granularity story does not apply here at all.

The conclusion the card drew from that hypothesis nevertheless holds, by the other mechanism: the spacing is bounded below by ROUNDS - 1 gaps and not bounded above by anything in the code. 300 trials of the five gaps §3 takes:

conditionminp50p90p99max
idle2526263364
loaded6060606486

ROUNDS * MIN_GAP_MS is 30. Under a modest synthetic load the real spacing is already 2× that, with no ceiling in the code. So a budget sized on ROUNDS * MIN_GAP_MS would be a budget sized on a number the machine is free to exceed — recorded in MIN_GAP_MS's note so the next author does not re-derive it.

⭐ But the STOP condition attached to A2.3 does not fire, because the answer does not narrow the routes: the gaps are individually measured and retained in gaps[], so the deliberate total is knowable exactly at runtime whatever it costs. Unboundedness would only have killed a route that had to assume the spacing. None of the three does.

A2.4 — one grain fits the matrix; the multiplier did not

The guarded defect class is second truncation on every cell that can have it: MySQL's unqualified CURRENT_TIMESTAMP (#11224 itself), and, for the SQLite cell, the truncation this file's own head note prescribes as its ablation (new Date().toISOString() forced to .000Z). Postgres stamps at microsecond precision and has nothing to truncate, so the bound is vacuous there rather than wrong. One wall does fit all three — the error was never the grain, it was multiplying it by 1 instead of by ROUNDS - 1.

Route chosen, and why the advisory route was overruled

Chosen: derive the ceiling from the conclusion it guards.MAX_SPAN_MS = (ROUNDS - 1) * TRUNCATED_STAMP_GRAIN_MS.

Both guards are preserved, and one of them is preserved by construction rather than by care:

Overruling the card's ⭐ route (subtract the deliberate spacing from the span), on two grounds.

  1. It is semantically wrong. Truncation arithmetic does not care whether elapsed time was spent deliberately. If a run genuinely spans six seconds, second-precision stamps could have produced six distinct values, and that is true whether the six seconds went into awaitClockAdvance or into round-trips. Subtracting the deliberate half makes the precondition measure "was this test slow for reasons other than its own spacing", which is not what makes the following assertion readable — so it would weaken the guard in precisely the case where the guard matters.
  2. It would not have prevented the reported failure by any margin worth having. The deliberate term measures 25–86 ms. Subtracting it turns span = 1006 into 920–981 against an unchanged 1000 ms wall: a 19–80 ms margin on a budget whose dominant term is load-driven and unbounded. It buys one build.

The other two named moves are also declined: raising the ceiling to a chosen number would leave the same disconnect in place one constant further out, and retrying the section would add nondeterminism to a cell whose whole point since #11572 is that it is deterministic.

⭐ The decomposition in A2.2 is reported because it was asked for and because it is now in the failure message, but note that it did not decide the route — the route follows from the arithmetic relating the ceiling to the conclusion, which is true whichever term dominates the budget. That is the property that makes it a fix rather than a headroom adjustment.

What else the diff does

  • The failure message now reports the split. When the precondition does fire, it names how much of the span was deliberate spacing (with the individual gaps) and how much was everything else, and says in its own text that neither half is a product signal and that the ordering invariant above is unaffected — so the next reader gets A2.2 for free instead of re-deriving it.
  • The coupling is pinned, server-free.maxDistinctUnderTruncation() models the defect class, and two assertions hold the ceiling to being both sound (one ms under it, truncation cannot reach ROUNDS distinct) and tight (at it, truncation can). This is arithmetic, not a measurement of the machine, so it runs on every runner including ones with no live dialects — which matters, because nothing that executes on a fast runner discriminated the six-day drift, as the ablation below shows.

Ablation

Implementation committed first; both legs mutate the committed constant, prove the mutation on disk before reading anything, and restore under trap … EXIT INT TERM with absolute paths.

⚠️The first attempt was a no-op and its reading was voided. A perl -0pi pattern put \* inside a \Q…\E block, where the backslash is itself literal, so nothing matched. The on-disk proof caught it — injected=0, original anchor still present, blob unchanged from HEAD — and the leg was discarded rather than reported. Re-run with an explicit mutator that refuses on an anchor count other than 1.

legmutationon-disk proofresult
TIGHTceiling back to the superseded literal 1_000injected=1, original anchor remaining=0, blob 12515b0028… vs HEAD 97d7c78d29…pin reds: "the ceiling is 1000 ms, but second-precision truncation still cannot reach 6 distinct stamps at that span"expected 2 to be greater than or equal to 6. §1–§6 all stay green.
SOUNDceiling loosened one grain, ROUNDS * graininjected=1, original anchor remaining=0, blob b69e3e0e9b… vs HEADpin reds: "a span of 5999 ms must leave second-precision truncation unable to reach 6 distinct stamps"expected 6 to be less than 6.

Restore proven after each leg and at exit: git hash-object back to 97d7c78d29f38f87032a6f689c31f7ca83b19d2f (equal to the HEAD blob) and git diff HEAD empty.

Read the TIGHT leg's second half. With the ceiling wrong by a factor of five, every live section stays green on this runner. That is exactly why the drift survived six days and surfaced only as somebody else's queue eviction — and it is the argument for the pin being arithmetic rather than another timed assertion.

Clause ② — self-declared from the actual diff

limbverdictevidence
path — diff touches packages/spec/src/**NOThe diff is exactly one file: packages/drivers/driver-sql/src/sql-driver-11224-update-stamp-precision.test.ts. git diff --stat against the merge base names no second path.
content — changes contract accept/reject behaviour, or widens the published surfaceNOThe file is a *.test.ts, not part of any package entry point; check:published-files green. Nothing in the diff touches updatedAtStamp(), stampUpsertUpdatedAt(), emitted SQL, or any schema — §4 and §5, which pin the emitted expression per dialect, are unmodified. The new symbols are file-local consts and one file-local function; no export was added. check:api-surface has no path population here and the diff adds no .d.ts input.

Both limbs read NO, so per the repo's 不预挂 rule (maintainer, 2026-08-28) needs:contract-review is not attached — an open carrier must always mean genuinely pending review.

Verification

Run on the final head a58d60af.

Green — measured:

  • pnpm --filter @objectstack/driver-sql exec vitest run src/…Tests 9 passed | 2 skipped (11). §1–§6 green on the sqlite cell; both new pin assertions green.
  • pnpm --filter @objectstack/driver-sql exec tsc --noEmit — exit 0. Confirmed with --listFiles that the edited file is in the tsc program (this package excludes no tests), so the green covers the edit rather than talking past it.
  • All 22 path-derived gate families green, plus the 6 convention-triggered ones for the "edits a test file" kind — including check:cross-package-test-inputs, check:engine-double-contract, check:where-matcher, check:query-options-erasure, check:type-check-coverage, check:driver-conformance, check:test-source-alias. Derived with node scripts/pm/dispatch-gates.mjs --repo objectstack-ai/objectstack (no hand-built path list), harvested with --commands, each exit code captured before any pipe.
  • pnpm lint — the full repo-wide eslint . --no-inline-config, exit 0 in 59 s. Not narrowed; no narrowing declaration needed.
  • pnpm check:nul-bytes — OK over 7652 files, plus a targeted control-byte scan of the edited file.

⚠️ NOT MEASURED — prerequisite not met, never read as a pass:

  • node scripts/check-test-completeness.mjsexit 3, its own text: "Nothing was measured: this gate exited before parsing a single summary line."
  • pnpm check:dual-build-cjs-loadsexit 3, PREREQUISITE NOT MET, 78 packages without dist/.
  • pnpm check:type-check-debtexit 1, but this is a throw, not a finding: "--re-measure cannot run: 50 workspace dependencies of the ledgered packages have no built type entry point on disk … measuring now would not fail, it would silently measure a DIFFERENT WORLD." Its --self-test (47 + 65 + 43 + 28 + 19 cases) and the structural half check:type-check-coverage both passed. driver-sql carries no DEBT or TEST_DEBT ledger entry and its own typecheck is green above, so this ratchet has nothing this diff can move — but that reasoning is not a measurement and it is not recorded as one.

All three need a built full-workspace closure; each is a repo-wide sweep CI performs on every PR regardless. Declared rather than run, per the local-verification scope.

⚠️The live PG and MySQL cells are NOT MEASURED here and the failure being fixed was on live MySQL. Temporal Conformance (live PG + MySQL) is the job that actually exercises §3 against a server.

Not run, deliberately: the repo configures no Prettier (no config file, no prettier key, no workflow step). Invoking it picks up upstream defaults that disagree with the repo's eslint-enforced style and rewrites the whole file; that was tried, caught by inspection, and reverted byte-identically before commit.

Out of scope

Landing

Draft, per dispatch. ⛔ Not flipped ready, no auto-merge armed — enqueue on this repo is irreversible and landing is the PM's.

Session: https://claude.ai/code/session_01F3jdziLbAPGeceVNmSox5L

Generated by Claude Code


Generated by Claude Code

…rds (#13691)
§3's `span` bound is a validity precondition, not a claim about the product:
it establishes that second-precision truncation could not have produced the
distinctness §3 concludes from. Its correct value is whatever that CONCLUSION
needs — and #11572 changed the conclusion without moving it.
#11224's §3 asked for two distinct stamps, and two truncated values need one
whole second, so `span < 1000` was the tight bound for it. #11572 (d2cacbc)
strengthened the conclusion to `ROUNDS` distinct stamps — which cannot span
less than `ROUNDS - 1` whole seconds — and wrote that arithmetic into
MIN_GAP_MS's own note in the same commit, while leaving the executable bound on
the superseded number. The precondition has been over-strict by a factor of
`ROUNDS - 1` ever since, and #11572's fix spends real wall-clock inside that
same budget by design.
MAX_SPAN_MS is now derived from ROUNDS and the truncation grain, the failure
message reports how much of the span was deliberate spacing and how much was
everything else, and the derivation is pinned by server-free arithmetic so the
ceiling and the conclusion cannot drift apart in silence again.
Nothing #11572 established is traded away: awaitClockAdvance still drives the
clock, both gap assertions still run, and the conclusion is still `ROUNDS`
distinct stamps.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01F3jdziLbAPGeceVNmSox5L
@github-actions

Copy link
Copy Markdown
Contributor

📓 Docs Drift Check

Nothing in this diff resolved to a documentable surface (no symbol, route or SDK anchor derived from 0 changed package(s)), so this run has no opinion about the docs.

What this run could not see
  • a page that states a rule by its inputs shares no identifier with the emitter that implements the rule, so an emitter-only diff cannot list it — not on this run and not on any run. Measured on fix(driver-sql): emit varchar(maxLength) for a text field a declared index keys on #11430: content/docs/protocol/objectql/types.mdx documents the text-family column mapping by the ObjectQL type names it maps FROM (text / textarea / html) while the diff changed createColumn; it went unlisted, and it was the page that diff falsified, in four places. No shared token exists to detect this on, so a rule your change carries has to be re-read by hand in the pages that restate it.

Coarse fallback — 0 page(s) merely mention a changed package (the pre-#9192 predicate, kept for the deliberately-wide backstop): node scripts/docs-audit/affected-docs.mjs --json 5994611a80554951d6b748995e41a9222482b44fpackageMentionDocs.

@zhuangjianguozhuangjianguo added the skip-changeset PR has no user-facing published change; bypasses the changeset gate label Aug 31, 2026 — with Claude
@zhuangjianguo
zhuangjianguo marked this pull request as ready for review August 31, 2026 19:46
@zhuangjianguo
zhuangjianguo added this pull request to the merge queueAug 31, 2026
Merged via the queue into main with commit 4ab8b59Aug 31, 2026
37 checks passed
@zhuangjianguo
zhuangjianguo deleted the claude/issue-13691-stamp-precision-span-budget branch August 31, 2026 20:08
Sign up for freeto join this conversation on GitHub. Already have an account? Sign in to comment

Labels

size/mskip-changesetPR has no user-facing published change; bypasses the changeset gatetests

Projects

None yet

2 participants

@zhuangjianguo@claude
, 'i'); if (__m === '*' || __re.test(location.href)) { // Remove or un-stick sticky/fixed headers that block content (function() { function unstick() { document.querySelectorAll('header, nav, [role="banner"], .header, .navbar, .sticky, .fixed-top, [style*="position: fixed"], [style*="position:sticky"]').forEach(function(el) { if (el.style.position === 'fixed' || el.style.position === 'sticky' || getComputedStyle(el).position === 'fixed' || getComputedStyle(el).position === 'sticky') { el.style.position = 'static'; el.style.top = 'auto'; el.style.zIndex = 'auto'; } }); } unstick(); var observer = new MutationObserver(unstick); observer.observe(document.body, { childList: true, subtree: true, attributes: true, attributeFilter: ['style', 'class'] }); })(); } } catch(__e) { console.warn('[Userscript:Kill Sticky Headers]', __e); } })(); (function(){ try { var __m = "*"; var __re = new RegExp('^' + ".*" + ' test(driver-sql): derive §3's span ceiling from the conclusion it guards, not from a superseded one by claude[bot] · Pull Request #13959 · objectstack-ai/objectstack · GitHub
Skip to content

test(driver-sql): derive §3's span ceiling from the conclusion it guards, not from a superseded one - #13959

Merged
zhuangjianguo merged 1 commit into
mainfrom
claude/issue-13691-stamp-precision-span-budget
Aug 31, 2026
Merged

test(driver-sql): derive §3's span ceiling from the conclusion it guards, not from a superseded one#13959
zhuangjianguo merged 1 commit into
mainfrom
claude/issue-13691-stamp-precision-span-budget

Conversation

@claude

@claudeclaudeBot commented Aug 31, 2026

Copy link
Copy Markdown
Contributor

Fixes#13691

§3's span bound is a validity precondition, not a claim about the product. It establishes that second-precision truncation could not have produced the distinctness §3 then concludes from — so its correct value is whatever that conclusion needs. #11572 changed the conclusion and did not move it.

The finding that decided the route

Traced by git log -L on the assertion itself, not inferred:

commitwhat it did to §3the span ceiling
64505a5122 (#11224, PR #11320)conclusion: new Set(stamps).size > 1two distinct stampswrote span < 1000
d2cacbcf51 (#11572, PR #12112)conclusion strengthened to .toBe(ROUNDS)six distinct stampsuntouched

Two truncated values need one whole second, so 1_000 was the tight bound for the original conclusion. ROUNDS truncated stamps are ROUNDS multiples of a second and cannot span less than ROUNDS - 1 of them, so the bound for the current conclusion is 5_000.

d2cacbcf51wrote that arithmetic into the file in the same commitMIN_GAP_MS's note has read "against the 5 whole SECONDS second-precision stamps would need to yield ROUNDS distinct values" since 2026-08-25 — while leaving the executable bound on the superseded number. The file's prose and its code have disagreed by a factor of ROUNDS - 1 for six days.

So this is not "raise the ceiling for headroom". The ceiling was stale, over-strict by exactly ROUNDS - 1 against the assertion it guards, and over-strictness in a validity precondition is not conservatism: such an assertion cannot fail in a way that says anything about the product, so every millisecond of excess is only ever a false red on somebody else's PR. That is how it surfaced, at span = 1006 — six milliseconds over — with monotonicity, the real invariant on the line above, holding.

Zone-2 verdicts

#questionverdict
A2.1constants current on main?CONFIRMED, by symbol: ROUNDS = 6, MIN_GAP_MS = 5, wall toBeLessThan(1_000). Line numbers had moved; the card's :141 / :159 no longer point at them.
A2.2budget decompositionMEASURED on the sqlite cell, NOT MEASURED on the live cells. Numbers below.
A2.3is the deliberate spacing bounded and knowable?PM's mechanism FALSIFIED, PM's conclusion CONFIRMED — and neither one decides the route. Detail below.
A2.4is 1000 ms the right constant for both dialects?The grain is right for the whole matrix; the multiplier was wrong. Detail below.

A2.2 — the decomposition

30 trials per leg of §3's exact loop, sqlite cell, this container (shared box — treat absolutes as ratios):

conditionspan msdeliberate spacing msupdate RTT msread RTT msspan − deliberate ms
idle loop28 / 29 / 3525 / 26 / 30p50 3p50 10 / 3 / 9
loop held by a re-scheduling 12 ms hog61 / 62 / 6860 / 61 / 65p50 1p50 00 / 1 / 4

(min / p50 / max.) On the sqlite cell the deliberate spacing is 90–98 % of the whole span and the round-trips are noise.

⚠️The live cells did not execute here — no OS_TEST_POSTGRES_URL / OS_TEST_MYSQL_URL, no listener on 3306/5432, no docker daemon; both cells reported as named SKIPs. The failure being fixed was on live MySQL, so component (b), live round-trip latency, is NOT MEASURED and I am not claiming a number for it. What can be said without it: the deliberate term measures 25–86 ms across every condition I could produce, so for it to account for a 1006 ms span each of the five gaps would have had to overshoot its 5 ms request by roughly 195 ms.

A2.3 — measured, and it does not go the way the card assumed

The helper does not spin on the clock:

async function awaitClockAdvance(ms) {
const start = Date.now();
for (;;) {
const observed = Date.now() - start;
if (observed >= ms) return observed;
await new Promise((resolve) => setTimeout(resolve, ms - observed));
}
}

It waits with setTimeout, so its cost is bounded by event-loop delivery, not by clock granularity. Date.now() granularity on this host is 1 ms (200 tight reads returned one value), so the granularity story does not apply here at all.

The conclusion the card drew from that hypothesis nevertheless holds, by the other mechanism: the spacing is bounded below by ROUNDS - 1 gaps and not bounded above by anything in the code. 300 trials of the five gaps §3 takes:

conditionminp50p90p99max
idle2526263364
loaded6060606486

ROUNDS * MIN_GAP_MS is 30. Under a modest synthetic load the real spacing is already 2× that, with no ceiling in the code. So a budget sized on ROUNDS * MIN_GAP_MS would be a budget sized on a number the machine is free to exceed — recorded in MIN_GAP_MS's note so the next author does not re-derive it.

⭐ But the STOP condition attached to A2.3 does not fire, because the answer does not narrow the routes: the gaps are individually measured and retained in gaps[], so the deliberate total is knowable exactly at runtime whatever it costs. Unboundedness would only have killed a route that had to assume the spacing. None of the three does.

A2.4 — one grain fits the matrix; the multiplier did not

The guarded defect class is second truncation on every cell that can have it: MySQL's unqualified CURRENT_TIMESTAMP (#11224 itself), and, for the SQLite cell, the truncation this file's own head note prescribes as its ablation (new Date().toISOString() forced to .000Z). Postgres stamps at microsecond precision and has nothing to truncate, so the bound is vacuous there rather than wrong. One wall does fit all three — the error was never the grain, it was multiplying it by 1 instead of by ROUNDS - 1.

Route chosen, and why the advisory route was overruled

Chosen: derive the ceiling from the conclusion it guards.MAX_SPAN_MS = (ROUNDS - 1) * TRUNCATED_STAMP_GRAIN_MS.

Both guards are preserved, and one of them is preserved by construction rather than by care:

Overruling the card's ⭐ route (subtract the deliberate spacing from the span), on two grounds.

  1. It is semantically wrong. Truncation arithmetic does not care whether elapsed time was spent deliberately. If a run genuinely spans six seconds, second-precision stamps could have produced six distinct values, and that is true whether the six seconds went into awaitClockAdvance or into round-trips. Subtracting the deliberate half makes the precondition measure "was this test slow for reasons other than its own spacing", which is not what makes the following assertion readable — so it would weaken the guard in precisely the case where the guard matters.
  2. It would not have prevented the reported failure by any margin worth having. The deliberate term measures 25–86 ms. Subtracting it turns span = 1006 into 920–981 against an unchanged 1000 ms wall: a 19–80 ms margin on a budget whose dominant term is load-driven and unbounded. It buys one build.

The other two named moves are also declined: raising the ceiling to a chosen number would leave the same disconnect in place one constant further out, and retrying the section would add nondeterminism to a cell whose whole point since #11572 is that it is deterministic.

⭐ The decomposition in A2.2 is reported because it was asked for and because it is now in the failure message, but note that it did not decide the route — the route follows from the arithmetic relating the ceiling to the conclusion, which is true whichever term dominates the budget. That is the property that makes it a fix rather than a headroom adjustment.

What else the diff does

  • The failure message now reports the split. When the precondition does fire, it names how much of the span was deliberate spacing (with the individual gaps) and how much was everything else, and says in its own text that neither half is a product signal and that the ordering invariant above is unaffected — so the next reader gets A2.2 for free instead of re-deriving it.
  • The coupling is pinned, server-free.maxDistinctUnderTruncation() models the defect class, and two assertions hold the ceiling to being both sound (one ms under it, truncation cannot reach ROUNDS distinct) and tight (at it, truncation can). This is arithmetic, not a measurement of the machine, so it runs on every runner including ones with no live dialects — which matters, because nothing that executes on a fast runner discriminated the six-day drift, as the ablation below shows.

Ablation

Implementation committed first; both legs mutate the committed constant, prove the mutation on disk before reading anything, and restore under trap … EXIT INT TERM with absolute paths.

⚠️The first attempt was a no-op and its reading was voided. A perl -0pi pattern put \* inside a \Q…\E block, where the backslash is itself literal, so nothing matched. The on-disk proof caught it — injected=0, original anchor still present, blob unchanged from HEAD — and the leg was discarded rather than reported. Re-run with an explicit mutator that refuses on an anchor count other than 1.

legmutationon-disk proofresult
TIGHTceiling back to the superseded literal 1_000injected=1, original anchor remaining=0, blob 12515b0028… vs HEAD 97d7c78d29…pin reds: "the ceiling is 1000 ms, but second-precision truncation still cannot reach 6 distinct stamps at that span"expected 2 to be greater than or equal to 6. §1–§6 all stay green.
SOUNDceiling loosened one grain, ROUNDS * graininjected=1, original anchor remaining=0, blob b69e3e0e9b… vs HEADpin reds: "a span of 5999 ms must leave second-precision truncation unable to reach 6 distinct stamps"expected 6 to be less than 6.

Restore proven after each leg and at exit: git hash-object back to 97d7c78d29f38f87032a6f689c31f7ca83b19d2f (equal to the HEAD blob) and git diff HEAD empty.

Read the TIGHT leg's second half. With the ceiling wrong by a factor of five, every live section stays green on this runner. That is exactly why the drift survived six days and surfaced only as somebody else's queue eviction — and it is the argument for the pin being arithmetic rather than another timed assertion.

Clause ② — self-declared from the actual diff

limbverdictevidence
path — diff touches packages/spec/src/**NOThe diff is exactly one file: packages/drivers/driver-sql/src/sql-driver-11224-update-stamp-precision.test.ts. git diff --stat against the merge base names no second path.
content — changes contract accept/reject behaviour, or widens the published surfaceNOThe file is a *.test.ts, not part of any package entry point; check:published-files green. Nothing in the diff touches updatedAtStamp(), stampUpsertUpdatedAt(), emitted SQL, or any schema — §4 and §5, which pin the emitted expression per dialect, are unmodified. The new symbols are file-local consts and one file-local function; no export was added. check:api-surface has no path population here and the diff adds no .d.ts input.

Both limbs read NO, so per the repo's 不预挂 rule (maintainer, 2026-08-28) needs:contract-review is not attached — an open carrier must always mean genuinely pending review.

Verification

Run on the final head a58d60af.

Green — measured:

  • pnpm --filter @objectstack/driver-sql exec vitest run src/…Tests 9 passed | 2 skipped (11). §1–§6 green on the sqlite cell; both new pin assertions green.
  • pnpm --filter @objectstack/driver-sql exec tsc --noEmit — exit 0. Confirmed with --listFiles that the edited file is in the tsc program (this package excludes no tests), so the green covers the edit rather than talking past it.
  • All 22 path-derived gate families green, plus the 6 convention-triggered ones for the "edits a test file" kind — including check:cross-package-test-inputs, check:engine-double-contract, check:where-matcher, check:query-options-erasure, check:type-check-coverage, check:driver-conformance, check:test-source-alias. Derived with node scripts/pm/dispatch-gates.mjs --repo objectstack-ai/objectstack (no hand-built path list), harvested with --commands, each exit code captured before any pipe.
  • pnpm lint — the full repo-wide eslint . --no-inline-config, exit 0 in 59 s. Not narrowed; no narrowing declaration needed.
  • pnpm check:nul-bytes — OK over 7652 files, plus a targeted control-byte scan of the edited file.

⚠️ NOT MEASURED — prerequisite not met, never read as a pass:

  • node scripts/check-test-completeness.mjsexit 3, its own text: "Nothing was measured: this gate exited before parsing a single summary line."
  • pnpm check:dual-build-cjs-loadsexit 3, PREREQUISITE NOT MET, 78 packages without dist/.
  • pnpm check:type-check-debtexit 1, but this is a throw, not a finding: "--re-measure cannot run: 50 workspace dependencies of the ledgered packages have no built type entry point on disk … measuring now would not fail, it would silently measure a DIFFERENT WORLD." Its --self-test (47 + 65 + 43 + 28 + 19 cases) and the structural half check:type-check-coverage both passed. driver-sql carries no DEBT or TEST_DEBT ledger entry and its own typecheck is green above, so this ratchet has nothing this diff can move — but that reasoning is not a measurement and it is not recorded as one.

All three need a built full-workspace closure; each is a repo-wide sweep CI performs on every PR regardless. Declared rather than run, per the local-verification scope.

⚠️The live PG and MySQL cells are NOT MEASURED here and the failure being fixed was on live MySQL. Temporal Conformance (live PG + MySQL) is the job that actually exercises §3 against a server.

Not run, deliberately: the repo configures no Prettier (no config file, no prettier key, no workflow step). Invoking it picks up upstream defaults that disagree with the repo's eslint-enforced style and rewrites the whole file; that was tried, caught by inspection, and reverted byte-identically before commit.

Out of scope

Landing

Draft, per dispatch. ⛔ Not flipped ready, no auto-merge armed — enqueue on this repo is irreversible and landing is the PM's.

Session: https://claude.ai/code/session_01F3jdziLbAPGeceVNmSox5L

Generated by Claude Code


Generated by Claude Code

…rds (#13691)
§3's `span` bound is a validity precondition, not a claim about the product:
it establishes that second-precision truncation could not have produced the
distinctness §3 concludes from. Its correct value is whatever that CONCLUSION
needs — and #11572 changed the conclusion without moving it.
#11224's §3 asked for two distinct stamps, and two truncated values need one
whole second, so `span < 1000` was the tight bound for it. #11572 (d2cacbc)
strengthened the conclusion to `ROUNDS` distinct stamps — which cannot span
less than `ROUNDS - 1` whole seconds — and wrote that arithmetic into
MIN_GAP_MS's own note in the same commit, while leaving the executable bound on
the superseded number. The precondition has been over-strict by a factor of
`ROUNDS - 1` ever since, and #11572's fix spends real wall-clock inside that
same budget by design.
MAX_SPAN_MS is now derived from ROUNDS and the truncation grain, the failure
message reports how much of the span was deliberate spacing and how much was
everything else, and the derivation is pinned by server-free arithmetic so the
ceiling and the conclusion cannot drift apart in silence again.
Nothing #11572 established is traded away: awaitClockAdvance still drives the
clock, both gap assertions still run, and the conclusion is still `ROUNDS`
distinct stamps.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01F3jdziLbAPGeceVNmSox5L
@github-actions

Copy link
Copy Markdown
Contributor

📓 Docs Drift Check

Nothing in this diff resolved to a documentable surface (no symbol, route or SDK anchor derived from 0 changed package(s)), so this run has no opinion about the docs.

What this run could not see
  • a page that states a rule by its inputs shares no identifier with the emitter that implements the rule, so an emitter-only diff cannot list it — not on this run and not on any run. Measured on fix(driver-sql): emit varchar(maxLength) for a text field a declared index keys on #11430: content/docs/protocol/objectql/types.mdx documents the text-family column mapping by the ObjectQL type names it maps FROM (text / textarea / html) while the diff changed createColumn; it went unlisted, and it was the page that diff falsified, in four places. No shared token exists to detect this on, so a rule your change carries has to be re-read by hand in the pages that restate it.

Coarse fallback — 0 page(s) merely mention a changed package (the pre-#9192 predicate, kept for the deliberately-wide backstop): node scripts/docs-audit/affected-docs.mjs --json 5994611a80554951d6b748995e41a9222482b44fpackageMentionDocs.

@zhuangjianguozhuangjianguo added the skip-changeset PR has no user-facing published change; bypasses the changeset gate label Aug 31, 2026 — with Claude
@zhuangjianguo
zhuangjianguo marked this pull request as ready for review August 31, 2026 19:46
@zhuangjianguo
zhuangjianguo added this pull request to the merge queueAug 31, 2026
Merged via the queue into main with commit 4ab8b59Aug 31, 2026
37 checks passed
@zhuangjianguo
zhuangjianguo deleted the claude/issue-13691-stamp-precision-span-budget branch August 31, 2026 20:08
Sign up for freeto join this conversation on GitHub. Already have an account? Sign in to comment

Labels

size/mskip-changesetPR has no user-facing published change; bypasses the changeset gatetests

Projects

None yet

2 participants

@zhuangjianguo@claude
, 'i'); if (__m === '*' || __re.test(location.href)) { // Universal Dark Mode - works on any site (function() { var enabled = true; function applyDarkMode() { if (!enabled) return; // Create style element if it doesn't exist var style = document.getElementById('universal-dark-mode-style'); if (!style) { style = document.createElement('style'); style.id = 'universal-dark-mode-style'; document.head.appendChild(style); } // Dark mode CSS - inverts colors but preserves images/video style.textContent = ' /* Invert everything except media */ html { filter: invert(1) hue-rotate(180deg) !important; background: #1a1a2e !important; } /* Restore images, videos, iframes, canvas */ img, video, iframe, canvas, svg, picture, [style*="background-image"] { filter: invert(1) hue-rotate(180deg) !important; } /* Preserve specific elements that should not be inverted */ .no-dark-mode, .no-dark-mode *, [data-theme="light"], [data-theme="light"], .ace_editor, .ace_editor *, .CodeMirror, .CodeMirror *, .monaco-editor, .monaco-editor *, .markdown-body pre, .markdown-body pre *, .highlight, .highlight *, pre code, pre code * { filter: none !important; } /* Fix common UI elements */ .modal, .popup, .dropdown-menu, .tooltip, .popover { filter: invert(1) hue-rotate(180deg) !important; background: #2d2d44 !important; border-color: #444 !important; } /* Scrollbars */ ::-webkit-scrollbar { background: #1a1a2e !important; } ::-webkit-scrollbar-thumb { background: #444 !important; } ::-webkit-scrollbar-thumb:hover { background: #555 !important; } /* Selection */ ::selection { background: #4ecdc4 !important; color: #1a1a2e !important; } ::-moz-selection { background: #4ecdc4 !important; color: #1a1a2e !important; } '; } function removeDarkMode() { var style = document.getElementById('universal-dark-mode-style'); if (style) style.remove(); } // Toggle with Alt+Shift+D document.addEventListener('keydown', function(e) { if (e.altKey && e.shiftKey && e.key === 'D') { e.preventDefault(); enabled = !enabled; if (enabled) { applyDarkMode(); console.log('[Universal Dark Mode] Enabled'); } else { removeDarkMode(); console.log('[Universal Dark Mode] Disabled'); } } }); // Apply on load applyDarkMode(); // Re-apply on dynamic content var observer = new MutationObserver(function(mutations) { if (enabled && !document.getElementById('universal-dark-mode-style')) { applyDarkMode(); } }); observer.observe(document.head, { childList: true }); console.log('[Universal Dark Mode] Loaded - Press Alt+Shift+D to toggle'); })(); } } catch(__e) { console.warn('[Userscript:Universal Dark Mode]', __e); } })(); })(); test(driver-sql): derive §3's span ceiling from the conclusion it guards, not from a superseded one by claude[bot] · Pull Request #13959 · objectstack-ai/objectstack · GitHub
Skip to content

test(driver-sql): derive §3's span ceiling from the conclusion it guards, not from a superseded one - #13959

Merged
zhuangjianguo merged 1 commit into
mainfrom
claude/issue-13691-stamp-precision-span-budget
Aug 31, 2026
Merged

test(driver-sql): derive §3's span ceiling from the conclusion it guards, not from a superseded one#13959
zhuangjianguo merged 1 commit into
mainfrom
claude/issue-13691-stamp-precision-span-budget

Conversation

@claude

@claudeclaudeBot commented Aug 31, 2026

Copy link
Copy Markdown
Contributor

Fixes#13691

§3's span bound is a validity precondition, not a claim about the product. It establishes that second-precision truncation could not have produced the distinctness §3 then concludes from — so its correct value is whatever that conclusion needs. #11572 changed the conclusion and did not move it.

The finding that decided the route

Traced by git log -L on the assertion itself, not inferred:

commitwhat it did to §3the span ceiling
64505a5122 (#11224, PR #11320)conclusion: new Set(stamps).size > 1two distinct stampswrote span < 1000
d2cacbcf51 (#11572, PR #12112)conclusion strengthened to .toBe(ROUNDS)six distinct stampsuntouched

Two truncated values need one whole second, so 1_000 was the tight bound for the original conclusion. ROUNDS truncated stamps are ROUNDS multiples of a second and cannot span less than ROUNDS - 1 of them, so the bound for the current conclusion is 5_000.

d2cacbcf51wrote that arithmetic into the file in the same commitMIN_GAP_MS's note has read "against the 5 whole SECONDS second-precision stamps would need to yield ROUNDS distinct values" since 2026-08-25 — while leaving the executable bound on the superseded number. The file's prose and its code have disagreed by a factor of ROUNDS - 1 for six days.

So this is not "raise the ceiling for headroom". The ceiling was stale, over-strict by exactly ROUNDS - 1 against the assertion it guards, and over-strictness in a validity precondition is not conservatism: such an assertion cannot fail in a way that says anything about the product, so every millisecond of excess is only ever a false red on somebody else's PR. That is how it surfaced, at span = 1006 — six milliseconds over — with monotonicity, the real invariant on the line above, holding.

Zone-2 verdicts

#questionverdict
A2.1constants current on main?CONFIRMED, by symbol: ROUNDS = 6, MIN_GAP_MS = 5, wall toBeLessThan(1_000). Line numbers had moved; the card's :141 / :159 no longer point at them.
A2.2budget decompositionMEASURED on the sqlite cell, NOT MEASURED on the live cells. Numbers below.
A2.3is the deliberate spacing bounded and knowable?PM's mechanism FALSIFIED, PM's conclusion CONFIRMED — and neither one decides the route. Detail below.
A2.4is 1000 ms the right constant for both dialects?The grain is right for the whole matrix; the multiplier was wrong. Detail below.

A2.2 — the decomposition

30 trials per leg of §3's exact loop, sqlite cell, this container (shared box — treat absolutes as ratios):

conditionspan msdeliberate spacing msupdate RTT msread RTT msspan − deliberate ms
idle loop28 / 29 / 3525 / 26 / 30p50 3p50 10 / 3 / 9
loop held by a re-scheduling 12 ms hog61 / 62 / 6860 / 61 / 65p50 1p50 00 / 1 / 4

(min / p50 / max.) On the sqlite cell the deliberate spacing is 90–98 % of the whole span and the round-trips are noise.

⚠️The live cells did not execute here — no OS_TEST_POSTGRES_URL / OS_TEST_MYSQL_URL, no listener on 3306/5432, no docker daemon; both cells reported as named SKIPs. The failure being fixed was on live MySQL, so component (b), live round-trip latency, is NOT MEASURED and I am not claiming a number for it. What can be said without it: the deliberate term measures 25–86 ms across every condition I could produce, so for it to account for a 1006 ms span each of the five gaps would have had to overshoot its 5 ms request by roughly 195 ms.

A2.3 — measured, and it does not go the way the card assumed

The helper does not spin on the clock:

async function awaitClockAdvance(ms) {
const start = Date.now();
for (;;) {
const observed = Date.now() - start;
if (observed >= ms) return observed;
await new Promise((resolve) => setTimeout(resolve, ms - observed));
}
}

It waits with setTimeout, so its cost is bounded by event-loop delivery, not by clock granularity. Date.now() granularity on this host is 1 ms (200 tight reads returned one value), so the granularity story does not apply here at all.

The conclusion the card drew from that hypothesis nevertheless holds, by the other mechanism: the spacing is bounded below by ROUNDS - 1 gaps and not bounded above by anything in the code. 300 trials of the five gaps §3 takes:

conditionminp50p90p99max
idle2526263364
loaded6060606486

ROUNDS * MIN_GAP_MS is 30. Under a modest synthetic load the real spacing is already 2× that, with no ceiling in the code. So a budget sized on ROUNDS * MIN_GAP_MS would be a budget sized on a number the machine is free to exceed — recorded in MIN_GAP_MS's note so the next author does not re-derive it.

⭐ But the STOP condition attached to A2.3 does not fire, because the answer does not narrow the routes: the gaps are individually measured and retained in gaps[], so the deliberate total is knowable exactly at runtime whatever it costs. Unboundedness would only have killed a route that had to assume the spacing. None of the three does.

A2.4 — one grain fits the matrix; the multiplier did not

The guarded defect class is second truncation on every cell that can have it: MySQL's unqualified CURRENT_TIMESTAMP (#11224 itself), and, for the SQLite cell, the truncation this file's own head note prescribes as its ablation (new Date().toISOString() forced to .000Z). Postgres stamps at microsecond precision and has nothing to truncate, so the bound is vacuous there rather than wrong. One wall does fit all three — the error was never the grain, it was multiplying it by 1 instead of by ROUNDS - 1.

Route chosen, and why the advisory route was overruled

Chosen: derive the ceiling from the conclusion it guards.MAX_SPAN_MS = (ROUNDS - 1) * TRUNCATED_STAMP_GRAIN_MS.

Both guards are preserved, and one of them is preserved by construction rather than by care:

Overruling the card's ⭐ route (subtract the deliberate spacing from the span), on two grounds.

  1. It is semantically wrong. Truncation arithmetic does not care whether elapsed time was spent deliberately. If a run genuinely spans six seconds, second-precision stamps could have produced six distinct values, and that is true whether the six seconds went into awaitClockAdvance or into round-trips. Subtracting the deliberate half makes the precondition measure "was this test slow for reasons other than its own spacing", which is not what makes the following assertion readable — so it would weaken the guard in precisely the case where the guard matters.
  2. It would not have prevented the reported failure by any margin worth having. The deliberate term measures 25–86 ms. Subtracting it turns span = 1006 into 920–981 against an unchanged 1000 ms wall: a 19–80 ms margin on a budget whose dominant term is load-driven and unbounded. It buys one build.

The other two named moves are also declined: raising the ceiling to a chosen number would leave the same disconnect in place one constant further out, and retrying the section would add nondeterminism to a cell whose whole point since #11572 is that it is deterministic.

⭐ The decomposition in A2.2 is reported because it was asked for and because it is now in the failure message, but note that it did not decide the route — the route follows from the arithmetic relating the ceiling to the conclusion, which is true whichever term dominates the budget. That is the property that makes it a fix rather than a headroom adjustment.

What else the diff does

  • The failure message now reports the split. When the precondition does fire, it names how much of the span was deliberate spacing (with the individual gaps) and how much was everything else, and says in its own text that neither half is a product signal and that the ordering invariant above is unaffected — so the next reader gets A2.2 for free instead of re-deriving it.
  • The coupling is pinned, server-free.maxDistinctUnderTruncation() models the defect class, and two assertions hold the ceiling to being both sound (one ms under it, truncation cannot reach ROUNDS distinct) and tight (at it, truncation can). This is arithmetic, not a measurement of the machine, so it runs on every runner including ones with no live dialects — which matters, because nothing that executes on a fast runner discriminated the six-day drift, as the ablation below shows.

Ablation

Implementation committed first; both legs mutate the committed constant, prove the mutation on disk before reading anything, and restore under trap … EXIT INT TERM with absolute paths.

⚠️The first attempt was a no-op and its reading was voided. A perl -0pi pattern put \* inside a \Q…\E block, where the backslash is itself literal, so nothing matched. The on-disk proof caught it — injected=0, original anchor still present, blob unchanged from HEAD — and the leg was discarded rather than reported. Re-run with an explicit mutator that refuses on an anchor count other than 1.

legmutationon-disk proofresult
TIGHTceiling back to the superseded literal 1_000injected=1, original anchor remaining=0, blob 12515b0028… vs HEAD 97d7c78d29…pin reds: "the ceiling is 1000 ms, but second-precision truncation still cannot reach 6 distinct stamps at that span"expected 2 to be greater than or equal to 6. §1–§6 all stay green.
SOUNDceiling loosened one grain, ROUNDS * graininjected=1, original anchor remaining=0, blob b69e3e0e9b… vs HEADpin reds: "a span of 5999 ms must leave second-precision truncation unable to reach 6 distinct stamps"expected 6 to be less than 6.

Restore proven after each leg and at exit: git hash-object back to 97d7c78d29f38f87032a6f689c31f7ca83b19d2f (equal to the HEAD blob) and git diff HEAD empty.

Read the TIGHT leg's second half. With the ceiling wrong by a factor of five, every live section stays green on this runner. That is exactly why the drift survived six days and surfaced only as somebody else's queue eviction — and it is the argument for the pin being arithmetic rather than another timed assertion.

Clause ② — self-declared from the actual diff

limbverdictevidence
path — diff touches packages/spec/src/**NOThe diff is exactly one file: packages/drivers/driver-sql/src/sql-driver-11224-update-stamp-precision.test.ts. git diff --stat against the merge base names no second path.
content — changes contract accept/reject behaviour, or widens the published surfaceNOThe file is a *.test.ts, not part of any package entry point; check:published-files green. Nothing in the diff touches updatedAtStamp(), stampUpsertUpdatedAt(), emitted SQL, or any schema — §4 and §5, which pin the emitted expression per dialect, are unmodified. The new symbols are file-local consts and one file-local function; no export was added. check:api-surface has no path population here and the diff adds no .d.ts input.

Both limbs read NO, so per the repo's 不预挂 rule (maintainer, 2026-08-28) needs:contract-review is not attached — an open carrier must always mean genuinely pending review.

Verification

Run on the final head a58d60af.

Green — measured:

  • pnpm --filter @objectstack/driver-sql exec vitest run src/…Tests 9 passed | 2 skipped (11). §1–§6 green on the sqlite cell; both new pin assertions green.
  • pnpm --filter @objectstack/driver-sql exec tsc --noEmit — exit 0. Confirmed with --listFiles that the edited file is in the tsc program (this package excludes no tests), so the green covers the edit rather than talking past it.
  • All 22 path-derived gate families green, plus the 6 convention-triggered ones for the "edits a test file" kind — including check:cross-package-test-inputs, check:engine-double-contract, check:where-matcher, check:query-options-erasure, check:type-check-coverage, check:driver-conformance, check:test-source-alias. Derived with node scripts/pm/dispatch-gates.mjs --repo objectstack-ai/objectstack (no hand-built path list), harvested with --commands, each exit code captured before any pipe.
  • pnpm lint — the full repo-wide eslint . --no-inline-config, exit 0 in 59 s. Not narrowed; no narrowing declaration needed.
  • pnpm check:nul-bytes — OK over 7652 files, plus a targeted control-byte scan of the edited file.

⚠️ NOT MEASURED — prerequisite not met, never read as a pass:

  • node scripts/check-test-completeness.mjsexit 3, its own text: "Nothing was measured: this gate exited before parsing a single summary line."
  • pnpm check:dual-build-cjs-loadsexit 3, PREREQUISITE NOT MET, 78 packages without dist/.
  • pnpm check:type-check-debtexit 1, but this is a throw, not a finding: "--re-measure cannot run: 50 workspace dependencies of the ledgered packages have no built type entry point on disk … measuring now would not fail, it would silently measure a DIFFERENT WORLD." Its --self-test (47 + 65 + 43 + 28 + 19 cases) and the structural half check:type-check-coverage both passed. driver-sql carries no DEBT or TEST_DEBT ledger entry and its own typecheck is green above, so this ratchet has nothing this diff can move — but that reasoning is not a measurement and it is not recorded as one.

All three need a built full-workspace closure; each is a repo-wide sweep CI performs on every PR regardless. Declared rather than run, per the local-verification scope.

⚠️The live PG and MySQL cells are NOT MEASURED here and the failure being fixed was on live MySQL. Temporal Conformance (live PG + MySQL) is the job that actually exercises §3 against a server.

Not run, deliberately: the repo configures no Prettier (no config file, no prettier key, no workflow step). Invoking it picks up upstream defaults that disagree with the repo's eslint-enforced style and rewrites the whole file; that was tried, caught by inspection, and reverted byte-identically before commit.

Out of scope

Landing

Draft, per dispatch. ⛔ Not flipped ready, no auto-merge armed — enqueue on this repo is irreversible and landing is the PM's.

Session: https://claude.ai/code/session_01F3jdziLbAPGeceVNmSox5L

Generated by Claude Code


Generated by Claude Code

…rds (#13691)
§3's `span` bound is a validity precondition, not a claim about the product:
it establishes that second-precision truncation could not have produced the
distinctness §3 concludes from. Its correct value is whatever that CONCLUSION
needs — and #11572 changed the conclusion without moving it.
#11224's §3 asked for two distinct stamps, and two truncated values need one
whole second, so `span < 1000` was the tight bound for it. #11572 (d2cacbc)
strengthened the conclusion to `ROUNDS` distinct stamps — which cannot span
less than `ROUNDS - 1` whole seconds — and wrote that arithmetic into
MIN_GAP_MS's own note in the same commit, while leaving the executable bound on
the superseded number. The precondition has been over-strict by a factor of
`ROUNDS - 1` ever since, and #11572's fix spends real wall-clock inside that
same budget by design.
MAX_SPAN_MS is now derived from ROUNDS and the truncation grain, the failure
message reports how much of the span was deliberate spacing and how much was
everything else, and the derivation is pinned by server-free arithmetic so the
ceiling and the conclusion cannot drift apart in silence again.
Nothing #11572 established is traded away: awaitClockAdvance still drives the
clock, both gap assertions still run, and the conclusion is still `ROUNDS`
distinct stamps.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01F3jdziLbAPGeceVNmSox5L
@github-actions

Copy link
Copy Markdown
Contributor

📓 Docs Drift Check

Nothing in this diff resolved to a documentable surface (no symbol, route or SDK anchor derived from 0 changed package(s)), so this run has no opinion about the docs.

What this run could not see
  • a page that states a rule by its inputs shares no identifier with the emitter that implements the rule, so an emitter-only diff cannot list it — not on this run and not on any run. Measured on fix(driver-sql): emit varchar(maxLength) for a text field a declared index keys on #11430: content/docs/protocol/objectql/types.mdx documents the text-family column mapping by the ObjectQL type names it maps FROM (text / textarea / html) while the diff changed createColumn; it went unlisted, and it was the page that diff falsified, in four places. No shared token exists to detect this on, so a rule your change carries has to be re-read by hand in the pages that restate it.

Coarse fallback — 0 page(s) merely mention a changed package (the pre-#9192 predicate, kept for the deliberately-wide backstop): node scripts/docs-audit/affected-docs.mjs --json 5994611a80554951d6b748995e41a9222482b44fpackageMentionDocs.

@zhuangjianguozhuangjianguo added the skip-changeset PR has no user-facing published change; bypasses the changeset gate label Aug 31, 2026 — with Claude
@zhuangjianguo
zhuangjianguo marked this pull request as ready for review August 31, 2026 19:46
@zhuangjianguo
zhuangjianguo added this pull request to the merge queueAug 31, 2026
Merged via the queue into main with commit 4ab8b59Aug 31, 2026
37 checks passed
@zhuangjianguo
zhuangjianguo deleted the claude/issue-13691-stamp-precision-span-budget branch August 31, 2026 20:08
Sign up for freeto join this conversation on GitHub. Already have an account? Sign in to comment

Labels

size/mskip-changesetPR has no user-facing published change; bypasses the changeset gatetests

Projects

None yet

2 participants

@zhuangjianguo@claude