Repository navigation
chore(specs): make the spec validator and CI enforce code/test/Lean consistency; fix spec drift against 2.11.0 - #1473
Merged
minguyen9988 merged 9 commits intoSep 20, 2026
Conversation
…istency The validator previously checked headings by regex, five literal invariant strings and a hardcoded list of Lean files. It now: scans every .lean file for sorry/admit/native_decide and cross-checks lakefile roots against Replication/*.lean; resolves every backticked repo path and com.altinity class in Codebase Mapping sections; verifies every SomethingTest/SomethingIT(.method()) and Replication.Module.name citation in Verification sections; requires Invariant I1..I13 headings; adds --changed-base <ref> (fail on */src/main/** or *.g4 changes without a specs/ or formal_specs/ change unless HEAD carries [spec-exempt: reason]) and --lake. A file/token allowlist waives findings in specs owned by in-flight changes and prints them as warnings. Unit tests under scripts/tests cover each check with temp-dir fixtures and a real temporary git repo. Spec 11.01 rewritten to describe exactly this. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
…quest Adds .github/workflows/spec-governance.yml (pull_request on all branches, push to 2.11.0): checkout with full history, elan installed with no default toolchain so lake resolves the version pinned in formal_specs/lean/lean-toolchain, lake build, a grep gate for sorry/admit/native_decide, the validator self-tests, and python3 scripts/validate_specs.py --changed-base origin/<base branch> (previous tip on push). Spec 11.03 now states that CI builds the proofs, lists all nine modules, notes that the shipped version formula is not modelled, and adds a Known coverage gaps section listing every @disabled JUnit class/method and the TestFlows xfail registry. Jinja-Render-Check: rendered=1; formats=yaml,shell; result=pass Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
…an coverage table CONSTITUTION section 3 said ten invariants while defining I1-I13; specs/README.md, AGENTS.md, copilot-instructions.md and the Smart Ralph protocol said I1-I10. All now say thirteen / I1-I13. Invariants.lean labelled ReplayIdempotency as Invariant I8 although I8 is Durable Offset Quiescence; the docstring is corrected without renaming the definition. CONSTITUTION section 5 claimed Invariants.lean covers I1-I7; it and a new additive section in formal_specs/lean/README.md now carry a per-invariant table: I1-I4 proved in the ordinal model (I2 model-only, shipped formula not modelled), I11/I12/I13 proved, I5 and I8 in progress in concurrent work, I6/I7/I9/I10 without a Lean proposition. specs/README.md index entries for 02.03 and 10.03 follow the corrected spec titles. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
…art inversion defect shouldResetSequenceNumberWhenSecondHasPassed was an empty body. It now drives the real static nextSequenceNumber on reset state and asserts the actual boundary: ts+1500 does not reset (diff == 1), ts+2500 resets to SEQUENCE_START and re-anchors, and versions stay strictly increasing within the run. knownDefectNewerEventAfterRestartRanksBelowOlderPreRestartEvent reproduces, through nextSequenceNumber itself across a simulated restart, the known carry defect documented in DebeziumOffsetManagement: a newer event 1 ms later at a higher binlog position is versioned below an older pre-restart event. It asserts the inversion EXISTS today and is named so it must be flipped when the encoding is fixed. No production code is changed. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
… 2.11.0 Paths, symbols and defaults now match the tree: DebeziumOffsetManagement lives under executor/ (OFFSET_COMMIT_LOCK); there is no JdbcOffsetBackingStore class in this repo, the offset store is Debezium's, the table DDL is the offset.storage.jdbc.offset.table.ddl config key and the connector-side reader is cdc/DebeziumOffsetStorage (plain selects, no FINAL); the replica status view is the replica.status.view config SQL executed by cdc/DebeziumJdbcStorageOperations.createViewForShowReplicaStatus, created in the offset database with seconds_behind_source from JSONExtractUInt(offset_val, 'ts_sec') (not system., not argMax); HikariDbSource replaces the non-existent HikariCPConnectionPool; GroupInsertQueryWithBatchRecords / PreparedStatementExecutor / PreparedStatementFieldMapper live under db/batch/ and QueryFormatter / CacheInvalidationManager directly under db/; TRUNCATE flushes staged rows, calls metadata.truncateTable and continues with no cache invalidation; updateRelocatesSortingKey(ClickHouseStruct) reads the sorting key from a supplier; CacheInvalidationManager uses tableVersions.merge and folds the epoch into getVersion, proofs expire lazily and there is no clearProvenAbsentColumns; buffer.flush.time.ms defaults to 30 and buffer.max.records to 100000, and the batch entry point is addToPreparedStatementBatch (no insertBatch); ClickHouseBatchExecutor.isPaused is volatile, not private; ClickHouseDebeziumEmbeddedApplication methods are static and AppInjector is not in an injector sub-package; the dispatch loop versions every ChangeEvent including DDL and heartbeats, the DDL offset is acknowledged inside performDDLOperation and the executor resumes in a finally. Every Verification section now cites tests that exist (class and method) or says 'not yet covered by an automated test (gap)'. Spec 10.01 notes the retriable path has no backoff today. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
…rd the known defects Specs 01.04 and 02.01-02.04 now describe the code as shipped: the floor sequenceMaxSourceTs is raised by every record (positioned or not) and applied only to first deliveries; the counter resets only when effectiveTs is at least 2000 ms past the anchor (diff > 1), not at 1 s; the ten-digit seeds SEQUENCE_START / SEQUENCE_START_INITIAL carry into the six digits the 1e6 multiplier leaves, so the formula is a sum that shifts the effective time by about one second; ClickHouseStruct.calculateVersion prefers the GTID (SnowFlakeId(ts_ms, gtid) with snowflake.id default true), so the sequence formula is used only without a GTID and the GTID path bypasses the floor. Each spec carries a 'Known defect (tracked, not yet fixed)' section quoting the DebeziumOffsetManagement Javadoc worked example, notes that ReplaySafetyTest does not pin that arithmetic (SequenceSeedOverflowTest and the new DebeziumChangeEventCaptureTest method do), and states precisely that version_strictly_monotonic is about the encodeVersion coordinate encoding while the engine model versions by ordinal 2*i, so the shipped formula and floor are not modelled. Spec 02.06 gains the caveats where the GapMono hypothesis of upgrade_safe is not established by the code: the restart carry, a lagging connector at upgrade time, and UInt64-max sentinel rows written by older versions. Versioning code is unchanged. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
…h-form allowlist tokens Review findings on the spec-first gate. (1) The exemption marker was read from HEAD only; on a pull_request run actions/checkout defaults to the synthetic merge commit, whose auto-generated message never carries it, so a legitimately exempted source-only PR failed the required workflow. validate_specs.py --changed-base now searches the messages of every commit in <base>..HEAD, and spec-governance.yml checks out github.event.pull_request.head.sha (fetch-depth 0 kept) so HEAD is the contributor's commit. Regression tests build a base branch, a PR branch whose head carries the marker, and a no-ff merge-commit checkout; they assert the gate passes with the marker (also when it sits on an earlier commit in the range) and still fails without it. (2) The allowlist parser stripped everything after the first '#', mis-parsing token-level waivers such as FooTest#method; '#' now starts a comment only at line start or after whitespace, with a parser test and an end-to-end waiver test. Spec 11.01 updated for both semantics. Jinja-Render-Check: rendered=1; formats=yaml,shell; result=pass Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
…-drift Forward-merge of #1470, #1471 and #1472 into the governance branch. Conflicts resolved by keeping both sides where both are true: CONSTITUTION section 5 (module bullets for DdlBarrier, OffsetFifo and DdlTranslation plus the coverage table, whose I5 and I8 rows are now Lean-covered), specs 03.01, 03.05, 10.04 and 11.03 (corrected Codebase Mapping and real test citations from both sides; theorem list renumbered). validate_specs.py keeps the rewritten validator; the hardcoded LEAN_MODULES list is obsolete because the rewrite discovers modules from the lakefile and the directory. Two consequences of the stricter validator on the merged tree are fixed here: spec 01.06 cited ControlRecordLogLevelTest.isControlRecordClassification, which the class does not declare (replaced by an honest gap line), and eight allowlist entries for specs that have since landed are pruned. Versioning specs 01.04, 02.01, 02.02, 02.04 and 02.06 now state the governing compatibility constraint: the emitted _version domain (ts_ms * 1_000_000 + counter with the 2.8.0 seeds) is the contract shared with 2.8.0, 2.9.1 and 2.10.x and must not change in either direction; the restart carry is inherited 2.8.0 behaviour preserved by design, and any improvement is confined to where the restart floor starts and must ship with an upgrade/downgrade matrix. Verified on the merged tree: validate_specs.py PASSED (3 allowlisted warnings for the still-open writer PR), validator self-tests 39 passed, lake build 14 modules zero sorry, DebeziumChangeEventCaptureTest 23/23, SequenceSeedOverflowTest 3/3, and merged regression classes green (MySqlDDLParserListenerImplTest 135, DdlDrainDeadlockTest 6, ControlRecordLogLevelTest 3, OffsetHandoffOrderTest 6). The 11 destructive-looking sites in this merge are all inherited from the already-merged #1472: DDL-translator unit-test expectation strings (DROP TABLE IF EXISTS / DROP COLUMN IF EXISTS / DROP INDEX inside ALTER fixtures) and the Lean inductive constructor tag dropColumn in DdlTranslation.lean. None executes anything; no runtime drop path is added by this merge. Destructive-Op-Check: sites=11; result=pass
…ns, retire the allowlist Merge origin/2.11.0 (writer fixes, #1474) into the governance branch. Conflicts (specs only), resolved to what the merged code does: - 08.03 proven-absent protocol: only an ALIAS column is ever proven absent (#1474) AND the proof is stamped with the table's current version and discarded once invalidateTable/invalidateAll bumps it (this branch); CacheInvalidationManager implements both. - 11.03 model design: base's same-version tombstone and FINAL tie-rule text, plus this branch's note that the shipped version formula, floor, seeds and GTID precedence are not modelled; 3.2 keeps the ReplayIdempotency note and the CI-gate heading with base's default_target explanation of lake build. Validator on the merged tree: every concurrent rewrite the allowlist waivers were parked behind has now landed, so the seven remaining allowlisted findings are fixed at the source and the allowlist carries no entries: - 04.03: QueryFormatter path is db/ (not db/operations/); there is no createColumns(); cites NullValueColumnDropTest and NullColumnValueRoundTripIT instead of tests that never existed. - 06.02: cites PauseDrainAtomicityTest / PauseDrainRaceTest instead of the non-existent ClickHouseBatchExecutorTest. - 06.03: MySQLDDLParserService.java (case). - 07.01: cites ClickHouseDataTypeMapperTest.getClickHouseDataType / getUnsignedClickHouseType and ClickHouseDataTypeMapperInt8Test. - 07.03: cites the DebeziumConverterTest boundary round-trips. - Pruned the five waivers the validator reported as no longer needed (02.05, 05.02, 07.07, 08.04, 08.05). Local verification: validate_specs.py PASSED (59 specs, 309 citations, 0 warnings); scripts/tests 39 passed; lake build 12 modules, no sorry / admit / native_decide; DebeziumChangeEventCaptureTest 23/23, SequenceSeedOverflowTest 3/3, DdlDrainDeadlockTest 6/6, OffsetHandoffOrderTest 6/6, MySqlDDLParserListenerImplTest 135/135, NullValueColumnDropTest 6/6.
minguyen9988
deleted the
chore-spec-validator-ci-enforcement-and-spec-drift
branch
September 20, 2026 14:09
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What
Verification