feat(raft-log-replication): header contract — log model, callbacks, entry points (tasks 1.1-1.3)

Extend src/lib/raft/raft.h for the TLA+ log half (raft.tla logVars/leaderVars):
- raft_state_t: log_len, next_index[], match_index[] (no entry bytes stored —
  terms via on_get_entry_term, bytes in the adapter); raft_config_t.initial_log_len.
- raft_callbacks_t: 4 REQUIRED log callbacks on_persist_entry, on_get_entry_term,
  on_send_append_entries, on_truncate_from.
- Entry points + raft_append_result_t: raft_log_append (ClientRequest),
  raft_send_append_entries (AppendEntries emit), raft_on_append_entries_request
  (Handle + UpdateTerm-first), raft_on_append_entries_reply.

Concretized on_send_append_entries's varargs "entries handle" placeholder to an
explicit n_entries (0/1); design.md updated to match. Header compiles clean with
and without XCE_TESTING (-Wall -Wextra -fsyntax-only).
This commit is contained in:
Rongsong Shen 2026-06-21 14:15:15 +00:00
parent 20e59d0b42
commit 6b5b201a64
3 changed files with 111 additions and 6 deletions

View file

@ -338,10 +338,13 @@ int on_persist_entry(void *ctx, uint64_t index, uint64_t term,
uint64_t on_get_entry_term(void *ctx, uint64_t index);
/* REQUIRED: transmit one AppendEntries to peer_idx with prevLog{Index,Term},
* leaderCommit, and an entries handle. */
* leaderCommit, and n_entries (0 = heartbeat, 1 = one entry). The library holds
* no entry bytes, so when n_entries==1 the adapter sources the single entry at
* prev_log_index+1 from its own log. [Concretizes the original varargs "entries
* handle" placeholder; impl 2026-06-21.] */
int on_send_append_entries(void *ctx, int peer_idx,
uint64_t prev_log_index, uint64_t prev_log_term,
uint64_t leader_commit /*, entries handle */ ...);
uint64_t leader_commit, int n_entries);
/* REQUIRED: delete local entries at index..end. */
int on_truncate_from(void *ctx, uint64_t index);

View file

@ -6,14 +6,14 @@
## 1. Header contract: log model, callbacks, entry points
- [ ] 1.1 Extend `raft.h` with the log model state and config restore field
- [x] 1.1 Extend `raft.h` with the log model state and config restore field
- Add `uint64_t log_len;`, `uint64_t next_index[RAFT_MAX_PEERS];`, `uint64_t match_index[RAFT_MAX_PEERS];` to `raft_state_t`
- Add `uint64_t initial_log_len;` to `raft_config_t` (restored WAL length at boot, default 0; library never reads storage)
- Observable completion: `raft.h` compiles; `sizeof(raft_state_t)` grows by the new fixed fields; no entry-byte storage added
- _Requirements: 1.1, 1.2, 3.1_
- _Boundary: raft.h_
- [ ] 1.2 Add the four new REQUIRED callbacks to `raft_callbacks_t` (verbatim contract)
- [x] 1.2 Add the four new REQUIRED callbacks to `raft_callbacks_t` (verbatim contract)
- Declare `on_persist_entry`, `on_get_entry_term`, `on_send_append_entries`, `on_truncate_from` with the exact signatures from design.md / brief
- Document each as REQUIRED and the `on_get_entry_term` → `0`-means-absent convention
- Observable completion: the four function-pointer members exist in `raft_callbacks_t` with the verbatim signatures; header doc comments match the Authoritative shared contract
@ -21,7 +21,8 @@
- _Boundary: raft.h_
- _Depends: 1.1_
- [ ] 1.3 Declare the three new entry points and `raft_append_result_t`
- [x] 1.3 Declare the three new entry points and `raft_append_result_t`
- NOTE (impl 2026-06-21): `on_send_append_entries`'s design "entries handle `...`" varargs placeholder was concretized to an explicit `int n_entries` (0=heartbeat, 1=one entry at `prev_log_index+1`; adapter sources the bytes since the library holds none). design.md §"Seam — raft_callbacks_t additions" updated to match. Downstream `raft-commit-safety` / `raft-sim-conformance` consume this concrete shape.
- Declare `raft_append_result_t`; declare `raft_log_append`, `raft_send_append_entries`, `raft_on_append_entries_request`, `raft_on_append_entries_reply` with the design.md signatures
- Observable completion: header declares all new entry points; a stub TU including `raft.h` compiles
- _Requirements: 2.1, 3.3, 4.7, 5.1_