Repository navigation
Add checkpoint recovery, CI evidence checks, and proof artifacts - #4
Merged
Merged
Conversation
Apply principle of least privilege for GITHUB_TOKEN: - Change top-level permissions to read-only - Jobs inherit read permissions, can escalate as needed This resolves Scorecard TokenPermissionsID alerts. Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
…ith negative controls
Contributor
Author
|
Important Review skippedThis PR was authored by the user configured for CodeRabbit reviews. CodeRabbit does not review PRs authored by this user. It's recommended to use a dedicated user account to post CodeRabbit review feedback. ⚙️ Run configurationConfiguration used: Organization UI Review profile: ASSERTIVE Plan: Essentials Run ID: You can disable this status message by setting the Use the checkbox below for a quick retry:
Comment |
7 of 13 tasks
hyperpolymath
added a commit
that referenced
this pull request
Oct 8, 2026
## Summary
This adds `Firmboot.WaterLeak.Durable`, a finite, disk-backed,
single-writer version of the water-warning experiment.
- **Journaling.** Every new valid command is journaled before it is
answered, in a 512-byte slot that is chained to the previous slot by
SHA-256.
- **What survives.** Accepted readings, pending warning obligations and
the first acknowledgement receipt survive the tested local process
crashes.
- **Gaps.** Readings that arrive after a sequence gap are buffered and
the gap is reported. A missing reading is never filled in.
- **Retries.** A retried operation ID returns its original reply.
The work existed only in an unpushed local commit, `7c29853` ("chore:
land estate governance sync", 2026-09-15). That commit had swept it in
alongside governance files that must not land. Its workflows do not
parse, and its composite actions are not in the template. This PR
extracts **only the durable-recovery code, its tests and its doc** onto
a fresh branch from `main` @ `7c2b90a`.
Files:
- `lib/firmboot/water_leak/durable.ex` and
`durable/{codec,journal,transition}.ex`: the service, the fixed binary
schema, the chained journal and deterministic replay.
- `test/firmboot/durable_test.exs`: 14 tests.
- `docs/durable-recovery.md`: the API, the commit boundary, the journal
format, bounds and the stated limits.
- `mix.exs`: `extra_applications: [:crypto]`, needed for
`:crypto.hash/2`. There are no new dependencies.
No linked issue.
## Type of change
- [ ] 🐛 Bug fix: not applicable.
- [x] ✨ New feature: a new module tree. No existing module is modified.
- [ ] 💥 Breaking change: none. `Firmboot.WaterLeak`,
`RecoveryExperiment` and #4's checkpoint replay are untouched.
- [ ] 🕳️ Soundness fix: not a checker or proof change.
- [x] 📖 Documentation: the new `docs/durable-recovery.md`.
- [ ] 🧹 Refactor / tech debt: not applicable.
- [ ] ⚡ Performance: not applicable. No timing claims are made.
- [ ] 🔧 Build / CI / tooling: the only build change is the one `mix.exs`
line above. No workflow is changed.
## 📌 New pins
- **PR head SHA: `b154e0a736768161ee350c6c660a61666cf1bdd5`**
- None. There is no `uses:` change, no `actions.lock` change, no new Hex
dependency (`mix.lock` is untouched) and no container digest. `:crypto`
is an OTP application that ships with Erlang.
## How has this been verified?
Everything was run locally in the PR worktree at the head above, with
system Elixir 1.18.3 on OTP 27.
- `MIX_ENV=test mix test`: **59 tests, 0 failures**. That is the
existing 45 plus the 14 new durable tests.
- One test runs all **720 arrival permutations** of a six-reading
fixture.
- Another runs **56 operation × crash-point cases**: each of 14
operations is killed at `before_write`, `partial_write`, `after_write`
and `after_sync`, and the final state is compared against an independent
fixture.
- `mix format --check-formatted`: exit 0.
- `reuse lint`: compliant, 89/89 files with copyright and licence
information.
- I checked the doc's numeric claims against the test file: there are 14
`test` blocks, a test named "all 720 arrival permutations…", and `for
index <- 0..13, point <- [4 points]` (56 cases).
- `git log -1 --show-signature`: good ED25519 signature, as
`required_signatures` needs.
- **Not covered by CI:** firmboot's CI (`verify.yml`) runs the Agda and
Lean checks, the experiment runners, the lock check and `reuse lint`,
but **never `mix test`**. The 14 new tests are therefore verified
**locally only**. That gap is pre-existing and also applies to the
existing 45 tests. It is recorded as a finding for the owner to
schedule, and this PR deliberately does not change `verify.yml` (see
Notes).
## Checklist
- [x] My commits are **signed**: SSH ED25519, verified locally.
- [x] I ran the project's own checks locally and they pass: `mix test`,
`mix format --check-formatted` and `reuse lint`, as above.
- [x] New files carry the correct licence. They use `REUSE.toml`
annotations rather than in-file headers, the same as every existing
`lib/` and `docs/` file: `lib/**` and `test/**` are MPL-2.0, `docs/**`
is CC-BY-SA-4.0. No file was relicensed.
- [x] Docs are updated, and no public claim now overstates what the code
does. The original doc described a 3-trial timing measurement, a JSON
evidence file and an assurance register, none of which are in this PR.
Those passages were removed, and the doc now says outright that it makes
no latency or throughput claims.
- [x] I have not introduced a soundness hole. No proof, checker or gate
is touched. The doc states that no theorem covers this file format or
replay implementation, and that the hash chain is not authentication or
rollback protection. The test suite includes the complete-prefix
rollback counterexample.
## Notes for reviewers
- **Not carried over from `7c29853`.** These stay in the local rescue
ref `refs/rescued/20261008-firmboot-unpushed/chore/bump-standards-pins`,
with a triage note in the owner's dev-notes inbox:
- its rewrite of `recovery_experiment.ex` and `water_leak_test.exs`. It
is a different design from #4's checkpoint replay, which merged later,
and taking it would revert #4's tests;
- its timing-measurement runner and recorded result
(`docs/evidence/recovery-local.json`);
- its assurance register (`ASSURANCE.md`, `docs/assurance/*`), which is
read only by an extended `scripts/assurance.py`. Python is banned in the
estate, so porting the checker is a separate decision;
- its `README.md`, `CONTINUITY.md`, `PURPOSE.md`, `VERIFICATION.md` and
`REUSE.toml` edits.
- **Why `verify.yml` is untouched.** Adding a `mix test` step is the
natural follow-up. Under the estate's KYAML rule, an edited workflow has
to be converted in the same PR, but only once the repo's gates are known
to read KYAML. That can't be established for firmboot yet: it has no
governance caller, and `gh actions-lock --verify-local` on flow-style
YAML has not been measured. So the step is left for a separate PR rather
than half-done here.
- `@doc` is on every public function in the four new modules. The `@impl
true` GenServer callbacks take their docs from the behaviour.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
https://claude.ai/code/session_015bTuGfwCcvjrmNFejydTML
Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
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
2 participants
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.
Add versioned water-leak journal checkpoints with exact replay, gap and truncation rejection, resource measurements, and recovery tests. Wire recovery and assurance checks with negative controls into CI, retain all verification results, and upload Lean proof logs while preserving failure status.
The combined two-commit change extends beyond fixing CI failures with new recovery functionality and evidence validation. Despite one commit’s permissions-related message, the diff contains no token-permission changes.
Validation was not run.
View coding task