lei.chen/myxce
1
0
Fork 1
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

docs(raft-adapter-conformance): extend controller conformance record with this feature's findings

Browse source 
CLAUDE.md's TLA+ Action-to-Code Mapping table gains corrected/new rows:
production vs. dormant AppendEntries send mechanisms, WAL catch-up and
config-push reply integrity, and vote/PreVote failure routing across
all failure timings -- each citation independently re-verified against
live source. The old AppendEntries row's citations had already drifted
onto unrelated code before this task; corrected, not just appended to.
Protocol Verification Checklist gains 3 new items for the guarantees
this feature closes.

ha-term-safety/spec.json's known_limitations entry for the dormant
send-path drift gets an additive RESOLVED pointer back to this spec's
disposition, so a future reader lands on the answer instead of
re-discovering the drift.

Requirement 1 (systematic conformance audit deliverable) complete.
This commit is contained in:
Rongsong Shen 2026-07-30 03:39:56 +00:00
parent 396d90a85e
commit 52ae598dfe
3 changed files with 12 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

2
.kiro/specs/ha-term-safety/spec.json
View file

@ -27,7 +27,7 @@
"note": "First post-implementation validation run -- all 19 tasks (1.1-5.5) were already [x] with no prior validate_impl record. Full suite 9/9 green, 46/46 requirement acceptance criteria mapped, fresh 6-round live chaotic-multi-kill soak PASS (zero committed divergence/job loss), boundary/dependency direction clean (src/lib/raft untouched across all 35 tagged commits).",
"known_limitations": [
"design.md's 'Commit-source switch' section describes the originally-planned architecture (library commit_index replacing the term-blind safe-commit); as shipped (commit 83fbed2, reviewer-approved with a RED->GREEN Figure-8 safety proof), the durable-majority barrier + own-term WAL_NOOP gate remain authoritative and raft_commit_index is purely advisory (commit.c:154). Design doc not updated to match; behavior is correct and safety-proven, this is a documentation-drift note only.",
"design.md's AppendEntries send-side architecture (on_send_append_entries/raft_send_append_entries, task 2.3) is dormant in production per a later cross-spec comment (raft-ha-core-safety task 6.2, ha.c:2530-2536) -- the live send path is the pre-existing repl_broadcast, patched by task 3.4 to carry entry.term/prev_log_term. The receive side IS live and correctly processes these entries -- live-verified safe, just not what the design.md diagram depicts. Documentation-drift note only.",
"design.md's AppendEntries send-side architecture (on_send_append_entries/raft_send_append_entries, task 2.3) is dormant in production per a later cross-spec comment (raft-ha-core-safety task 6.2, ha.c:2530-2536) -- the live send path is the pre-existing repl_broadcast, patched by task 3.4 to carry entry.term/prev_log_term. The receive side IS live and correctly processes these entries -- live-verified safe, just not what the design.md diagram depicts. Documentation-drift note only. RESOLVED 2026-07-29: raft-adapter-conformance has now formally documented and regression-guarded this exact drift -- see src/controller/CLAUDE.md's TLA+ Action-to-Code Mapping table (the dormant nextIndex-driven sender row) and that spec's design.md 'Decision: dormant AppendEntries sender resolution' section for the authoritative disposition; a future reader should land there instead of re-discovering this drift.",
"ha.c:1844 has a stale 'TODO(ha-term-safety task 2.x): REPLACE these stubs' header comment whose own body lines each say '-- IMPLEMENTED'; a companion stale doc-comment sits in ha_convergence.c ~357-360 describing retired behavior. Cosmetic only, self-flagged in tasks.md's own 5.5 cleanup list, never executed."
]
}

2
.kiro/specs/raft-adapter-conformance/tasks.md
View file

@ -76,7 +76,7 @@
- _Requirements: 5.3_
- _Boundary: test_commit_barrier_reply.c_
- [ ] 6. Integration: extend the controller's durable conformance record with this feature's findings
- [x] 6. Integration: extend the controller's durable conformance record with this feature's findings
- Update `src/controller/CLAUDE.md`'s "TLA+ Action-to-Code Mapping" table and "Protocol Verification Checklist" with corrected/added rows covering: `AppendEntries` reply integrity (WAL catch-up and configuration push), vote/PreVote failure routing across all failure timings, and the dormant-sender resolution from task 4
- Append a one-line pointer to the existing `known_limitations` entry (index 30) in `.kiro/specs/ha-term-safety/spec.json`, referencing this spec's resolution of the dormant `on_send_append_entries` send-path drift
- Observable: the CLAUDE.md table cites the current, post-fix code paths for every action this feature touched, with no reference to the pre-fix silent-drop behavior as if it were still current; a reader of `ha-term-safety`'s known_limitations lands on this spec's resolution instead of re-discovering the drift