You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
| Broader formal model coverage | Finite configured TLC models are closed above, including bounded prepare branch-priority/try-witness coverage, finite 3-, 5-, and 7-replica Accept-Deps optimized-recovery evidence coverage, finite 3-, 5-, and 7-replica abstract TryPreAccept response branch-slice coverage, finite 3-, 5-, and 7-replica TryPreAccept message-path coverage, finite 3-, 5-, and 7-replica committed-conflict evidence-query guard/fail-closed coverage, one finite three-voter committed-conflict evidence-staleness request-scoping slice (`tla/EPaxosEvidenceStaleness.cfg` generated `6/6` states), finite 3-, 5-, and 7-replica uncommitted-conflict force/defer quorum coverage, finite configuration-barrier/add/remove/chain pinning coverage, one finite normal configuration-transition retry-timer slice (`tla/EPaxosConfigTransitionRetry.cfg` generated `8/8` states), one finite normal configuration-transition response de-duplication slice (`tla/EPaxosConfigTransitionDedup.cfg` generated `16/16` states), one finite durable configuration replay slice, finite config recovery-after-removal, recovery-after-addition, lost/duplicate response de-duplication, and recovery retry-timer slices (`tla/EPaxosConfigRecovery.cfg` generated `44/30` states, `tla/EPaxosConfigAddRecovery.cfg` generated `15/15` states, `tla/EPaxosConfigRecoveryDedup.cfg` generated `11/11` states, and `tla/EPaxosConfigRecoveryRetry.cfg` generated `8/8` states), a finite rollback-allocation next-instance/skip/apply-order check, and a finite `TOQClockDiscipline.tla` bounded-skew/bounded-delay contract. The TOQ operational-clock boundary is now documented in `EPAXOS.MD` and `MODEL_EQ_REPORT.MD`: the core consumes embedder-provided clock, one-way-delay, and sync-group values, but does not implement synchronization, measurement, drift monitoring, or target-environment validation. Remaining open: arbitrary/general recovery under configuration changes beyond the finite recovery slices, arbitrary membership histories, arbitrary durable histories, joint consensus, arbitrary message loss and retry/rebroadcast behavior, complete optimized-recovery branch parity, unbounded proofs, external target proof, synchronized-clock implementation, one-way-delay measurement, runtime drift enforcement, and operational clock-discipline proof. |
126
-
| Deployment manifest | Example systemd artifacts now exist (`deploy/systemd/kvnode@.service`, `deploy/systemd/kvnode.env.example`) plus `tests/kvnode_systemd_manifest_audit.sh`, which renders the example EnvironmentFile into the `ExecStart` contract, emits `release_claim=none-target-environment-deployment-manifest-still-required`, and keeps `systemd-analyze verify` opt-in via `KVNODE_SYSTEMD_ANALYZE=yes`; these artifacts are checked by `tests/operations_readiness_audit.sh`. A reviewed and exercised target deployment under systemd/container/orchestration remains open before this can be a production manifest claim, so target-environment deployment execution remains open. |
126
+
| Deployment manifest | Example systemd artifacts now exist (`deploy/systemd/kvnode@.service`, `deploy/systemd/kvnode.env.example`) plus `tests/kvnode_systemd_manifest_audit.sh`, which renders the example EnvironmentFile into the `ExecStart` contract, emits `release_claim=none-target-environment-deployment-manifest-still-required`, keeps `systemd-analyze verify` opt-in via `KVNODE_SYSTEMD_ANALYZE=yes`, and supports `KVNODE_SYSTEMD_MANIFEST_REPORT=/path/report.env` for a machine-readable example/operator report. The report writes `status=example-operator-report`, `artifact=systemd-manifest-audit`, `rendered_exec=...`, `systemd_analyze=skipped|verified`, and `release_claim=none-target-environment-deployment-manifest-still-required`; the manifest report remains a local static-render non-claim and does not prove a target deployment. These artifacts are checked by `tests/operations_readiness_audit.sh`. A reviewed and exercised target deployment under systemd/container/orchestration remains open before this can be a production manifest claim, so target-environment deployment execution remains open. |
127
127
| Data lifecycle | Local destructive-storage remove/restore evidence exists, the KV example has exercised Pebble checkpoint/whole-directory restore plus offline and live-source checkpoint-backed repair tests for checksum-detected bit-level corruption, `examples/kv/cmd/kvcheckpoint` provides a maintained offline checkpoint/verify/verified-restore/repair helper, `TestRestoreRejectsCorruptCheckpointWithoutReplacingLiveData` verifies restore fails closed before replacement, `KVNODE_CHECKPOINT_REPORT=/path/report.env` lets successful helper operations write `status=example-operator-report` plus `release_claim=none-target-environment-data-lifecycle-drill-still-required`, `tests/kvnode_local_runner.go --mode data` stops one local loopback node and runs offline checkpoint/verify/restore/repair on a stopped local node before restart/catch-up verification, the runner uses distinct `checkpoint-report.env`, `verify-report.env`, `restore-report.env`, and `repair-report.env` paths under `data-lifecycle/*-report.env` and validates each report's `status`, `operation`, and `release_claim` before writing `data-lifecycle-summary.txt`, those reports record `operation=checkpoint`, `operation=verify`, `operation=restore`, `operation=repair`, and `result=success`, `data-lifecycle-summary.txt` records `data_lifecycle=offline-checkpoint-verify-restore-repair`, `reports=checkpoint-report.env,verify-report.env,restore-report.env,repair-report.env`, and `none-target-environment-data-lifecycle-drill-still-required`, and `docs/operations/kvnode-data-lifecycle-incident-runbook.md` documents checkpoint, verification, repair, restore, helper reports, checksum-mismatch, local data-lifecycle drill, and evidence-capture procedures. A reviewed operator backup/restore/disaster-recovery drill in the target environment remains open; target-environment backup/restore/disaster-recovery drill remains open. |
128
128
| Capacity envelope | `tests/kvnode_capacity_envelope.sh` is an opt-in bounded harness for throughput, latency, memory RSS, disk growth, queue depth, value size, scan limit, and peer-count samples; its `metadata.env` and `summary.md` emit `release_claim=none-target-environment-capacity-results-still-required` plus bounded single-line `environment_label` and `workload_label` provenance fields; `tests/kvnode_local_capacity_drill.sh` starts a disposable three-node loopback cluster and runs that harness against all three client/admin listeners with PIDs and data dirs while preserving the same release-claim non-claim and defaulting provenance to `environment_label=local-loopback` and `workload_label=local-capacity-drill`; `tests/kvnode_local_runner.go` is a custom Go runner that starts the same local-only three-node loopback shape, records bounded write/read/scan latency plus admin metric samples, accepts `KVNODE_GO_RUNNER_ENVIRONMENT_LABEL` and `KVNODE_GO_RUNNER_WORKLOAD_LABEL`, defaults them to `environment_label=local-loopback` and `workload_label=local-go-runner`, validates both as non-empty single-line values without `=` and with maximum length 128, and writes the labels to `metadata.env`, `capacity-summary.txt`, and final `summary.txt` when capacity mode runs. These checks state that the custom Go runner capacity labels document `KVNODE_GO_RUNNER_ENVIRONMENT_LABEL` and `KVNODE_GO_RUNNER_WORKLOAD_LABEL`; the defaulting custom Go runner provenance to `environment_label=local-loopback` and `workload_label=local-go-runner` behavior remains explicit; custom Go runner validates label values as non-empty, single-line, without `=`, and at most 128 characters; custom Go runner writes `environment_label` and `workload_label` to `metadata.env`, `capacity-summary.txt`, and capacity `summary.txt` when `capacity_ran=true`. `bash -n tests/kvnode_capacity_envelope.sh`, `bash tests/kvnode_capacity_envelope.sh --help`, `bash tests/kvnode_local_capacity_drill.sh --help`, `go run -tags kvnode_local_runner ./tests/kvnode_local_runner.go --help`, and `tests/operations_readiness_audit.sh` pass. Local loopback samples have passed, including the earlier single-node workstation sample, a three-node local wrapper sample with 5 ops per value-size phase, 64/1024-byte values, scan limits 1/8, a non-claim metadata sample with 1 op, 16-byte values, scan limit 1, peer_count=3, `release_claim=none-target-environment-capacity-results-still-required`, `environment_label=local-loopback`, and `workload_label=local-capacity-drill`, plus a custom Go runner sample with `KVNODE_GO_RUNNER_OPS_PER_PHASE=2`, `KVNODE_GO_RUNNER_VALUE_BYTES=16`, `KVNODE_GO_RUNNER_SCAN_LIMITS=1`, `status=local-go-runner-only`, and a custom Go runner provenance sample with `environment_label=local-loopback`, `workload_label=local-go-runner-capacity`, and `latency_rows=3`. This is workstation harness evidence only; measured target-environment capacity results remain open because target-environment capacity measurement remains open. |
129
129
| Incident readiness |`docs/operations/kvnode-data-lifecycle-incident-runbook.md` now covers storage failure, network partition, peer compromise, replay/checksum suspicion, and recovery stalls, with evidence-capture steps and non-claims; `tests/kvnode_incident_tabletop_drill.sh` locally rehearses the storage-failure and network-partition test-fault branches on a disposable loopback cluster and writes `release_claim=none-target-environment-operator-review-still-required` into raw tabletop evidence; `tests/kvnode_local_runner.go` also locally exercised `/faults/storage`, `/faults/transport`, `/readyz`, `/metrics`, and post-clear canaries with `status=local-go-runner-only`; `tests/operations_readiness_audit.sh` checks those artifacts. Operator-reviewed target-environment tabletop or live drill evidence remains open, so target-environment incident-response operator review remains open. |
Copy file name to clipboardExpand all lines: release/EPAXOS_READINESS_EVIDENCE.md
+3-2Lines changed: 3 additions & 2 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -192,6 +192,7 @@ Non-claims remain explicit: No target-environment remote claim, no in-place Pebb
192
192
- A local single-node loopback capacity-envelope sample passed with `KVNODE_CAPACITY_RUN=yes`, `KVNODE_CAPACITY_OPS_PER_PHASE=5`, `KVNODE_CAPACITY_VALUE_BYTES=64,1024`, and `KVNODE_CAPACITY_SCAN_LIMITS=1,8`; archived sample files are `local://kvnode-capacity-loopback-20260708T194748Z-summary.txt`, `local://kvnode-capacity-loopback-20260708T194748Z-latency.csv`, and `local://kvnode-capacity-loopback-20260708T194748Z-resources.csv`; generated summary reported 22 HTTP operations, 22.000 sampled operations/second, p50 0.007860s, p95 0.008602s, p99 0.008797s, and harness-only/non-production status.
193
193
-`bash tests/release_scope_audit.sh` passed in this session after release-scope updates.
194
194
-`bash tests/kvnode_systemd_manifest_audit.sh` passed after adding the deployment-manifest non-claim output; archived output is `local://kvnode-systemd-manifest-nonclaim-20260709-output.txt` and includes `rendered_exec=...`, `release_claim=none-target-environment-deployment-manifest-still-required`, and `systemd_analyze=skipped`.
195
+
-`KVNODE_SYSTEMD_MANIFEST_REPORT=/tmp/kvnode-systemd-manifest-report-20260709/report.env bash tests/kvnode_systemd_manifest_audit.sh` passed after adding the manifest report output; archived report is `local://kvnode-systemd-manifest-report-20260709-report.env` and includes `status=example-operator-report`, `artifact=systemd-manifest-audit`, `rendered_exec=...`, `systemd_analyze=skipped`, and `release_claim=none-target-environment-deployment-manifest-still-required`. This remains a local static-render non-claim; target-environment deployment execution remains open.
195
196
-`go test ./examples/kv/cmd/kvcheckpoint -count=1` passed after adding the maintained offline checkpoint helper; the CLI verifies checkpoints before `restore` and `repair` replaces a data directory.
196
197
-`go test ./examples/kv/cmd/kvcheckpoint -count=1` passed after adding `KVNODE_CHECKPOINT_REPORT` coverage; the tests prove successful `checkpoint`, `verify`, `restore`, and `repair` operations write `status=example-operator-report`, quoted paths, and `release_claim=none-target-environment-data-lifecycle-drill-still-required`, and that report-write failures do not mask underlying command failures.
197
198
-`KVNODE_INCIDENT_TABLETOP_RUN=yes KVNODE_INCIDENT_BASE_PORT=30080 KVNODE_INCIDENT_PEER_BASE_PORT=30180 KVNODE_INCIDENT_ADMIN_BASE_PORT=30280 KVNODE_INCIDENT_OUT_DIR=/tmp/kvnode-incident-nonclaim-20260709 bash tests/kvnode_incident_tabletop_drill.sh` passed on local loopback after adding the incident tabletop harness non-claim to generated metadata; archived sample files are `local://kvnode-incident-nonclaim-20260709-metadata.env` and `local://kvnode-incident-nonclaim-20260709-summary.txt`; generated evidence reported `status=local-tabletop-only`, `storage_fault=exercised-and-cleared`, `transport_fault=exercised-and-cleared`, post-clear canaries visible on all nodes, and `release_claim=none-target-environment-operator-review-still-required`.
@@ -228,7 +229,7 @@ Non-claims remain explicit: No target-environment remote claim, no in-place Pebb
228
229
-`deploy/systemd/kvnode.env.example`
229
230
- Example/operator environment file for a three-node topology.
230
231
-`tests/kvnode_systemd_manifest_audit.sh`
231
-
- Cross-platform static manifest exercise that validates required environment variables, renders the example `ExecStart`, emits `release_claim=none-target-environment-deployment-manifest-still-required`, checks peer/deadline/body-limit values, and keeps host-context `systemd-analyze verify` opt-in through `KVNODE_SYSTEMD_ANALYZE=yes`.
232
+
- Cross-platform static manifest exercise that validates required environment variables, renders the example `ExecStart`, emits `release_claim=none-target-environment-deployment-manifest-still-required`, writes an optional `KVNODE_SYSTEMD_MANIFEST_REPORT` example/operator report with `status=example-operator-report`, `rendered_exec=...`, and `systemd_analyze=skipped|verified`, checks peer/deadline/body-limit values, and keeps host-context `systemd-analyze verify` opt-in through `KVNODE_SYSTEMD_ANALYZE=yes`.
- Data lifecycle and incident runbook with the maintained `kvcheckpoint` offline helper, backup, semantic checkpoint verification, explicit repair, verified restore, checksum, destructive-storage, local incident tabletop, live-source recovery boundaries, and incident procedures.
234
235
-`docs/operations/kvnode-upgrade-rollback.md`
@@ -360,7 +361,7 @@ The following blockers are still listed in `RELEASE_SCOPE.md` and prevent a go d
360
361
-`tla/EPaxosConfigRecoveryDedup.tla` adds one finite staged lost+duplicate old-instance recovery de-duplication slice and generated `11/11` states, and `TestOldConfigRecoveryUsesPinnedVotersAfterRemoval` covers the matching Go duplicate-response path, but retries, timer rebroadcast, arbitrary message loss, arbitrary recovery under configuration changes, joint consensus, arbitrary membership histories, and unbounded proof remain open.
361
362
-`tla/EPaxosConfigRecoveryRetry.tla` adds one finite logical old-config recovery retry-timer slice and generated `8/8` states, and `TestOldConfigRecoveryRetryUsesPinnedVotersAfterRemoval` plus `TestOldConfigRecoveryRetryUsesPinnedVotersAfterAddition` cover the matching Go removal/addition retry paths, but arbitrary recovery histories, arbitrary retry histories, joint consensus, message loss, arbitrary membership histories, and unbounded proof remain open.
362
363
-`tla/EPaxosConfigAddRecovery.tla` adds one finite staged old-instance recovery-after-addition slice and generated `15/15` states, and `TestOldConfigRecoveryUsesPinnedVotersAfterAddition` covers the matching Go prepare/accept quorum path with added-voter responses rejected for old quorum progress, but arbitrary recovery under configuration changes, joint consensus, message loss, arbitrary membership histories, and unbounded proof remain open.
363
-
- Deployment manifest artifacts are example/operator material only; `tests/kvnode_systemd_manifest_audit.sh` renders and audits the example `ExecStart` contract and emits`release_claim=none-target-environment-deployment-manifest-still-required`, but reviewed execution under a target system manager, container, or orchestration environment remains open, so target-environment deployment execution remains open.
364
+
- Deployment manifest artifacts are example/operator material only; `tests/kvnode_systemd_manifest_audit.sh` renders and audits the example `ExecStart` contract, can write a `KVNODE_SYSTEMD_MANIFEST_REPORT` non-claim report with `status=example-operator-report`, `rendered_exec=...`, `systemd_analyze=skipped|verified`, and`release_claim=none-target-environment-deployment-manifest-still-required`, but reviewed execution under a target system manager, container, or orchestration environment remains open, so target-environment deployment execution remains open.
364
365
- Data lifecycle now has a maintained local offline `kvcheckpoint` helper, runbook/audit evidence, and a local Go runner data-lifecycle drill that stops one loopback node, runs offline checkpoint/verify/restore/repair with distinct validated helper reports, restarts it, and verifies catch-up canaries, but a reviewed operator backup/restore/disaster-recovery drill in the target environment remains open. The mixed-version drill's binary rollback keeps current data and does not exercise checkpoint restore.
365
366
- Target-environment capacity-envelope measurements remain open; local evidence now includes a single-node workstation sample, a three-node loopback shell wrapper sample, a machine-readable capacity non-claim sample, a shell-wrapper provenance sample, and a custom local Go runner provenance sample whose metadata/final/capacity summaries carry `environment_label=local-loopback` and `workload_label=local-go-runner-capacity`, but none is a measured target-environment capacity result, so target-environment capacity measurement remains open.
366
367
- Incident readiness has runbook/audit evidence, a local loopback tabletop shell harness, and a custom local Go runner for storage-failure and network-partition test-fault branches, but operator-reviewed target-environment tabletop or live drill evidence remains open.
0 commit comments