dev->master - #445
Open
jeffrey-l-turner wants to merge 64 commits into
Open
dev->master#445jeffrey-l-turner wants to merge 64 commits into
jeffrey-l-turner wants to merge 64 commits into
Conversation
…pies Replace Branch<R> = HashableSet<R> with Arc<HashableSet<R>> so branches are shared by reference through the merge pipeline instead of deep-copied. Update compute_branches and compute_conflict_map signatures, rejection handling, and all call sites and tests.
…limit PR 1 of the soak disk hygiene stack. Adds the deploy storage area with its positive configuration, 237 states clean, and its negative control, which exits 12 on RetainedWithinPhlo, plus the area README. Registers the positive configuration in the gate and adds the Deploy storage row to the formal-verification guide. Carries the stacked-PR plan so reviewers of the stack can read it; PR 4 removes it.
…ter PRs The plan's link to the work log and the README's link to the CbC tiers document target files that PR 2 and PR 4 add. The link checker scans every markdown file, so they resolve to the staging tip until the stack lands.
…ness property from the control Review remediations for PR #430. The README explains why weak fairness on the whole Next action proves Terminates in the metered configuration, since every running-phase step strictly decreases the phlo budget, and why the unmetered control cannot claim it. The control configuration now checks only the invariant the gate registers it for. The README also states that the tiers link is a stack permalink that becomes a relative path when the last PR lands. TLC after the change: positive 237 states clean with Terminates, control exit 12 on RetainedWithinPhlo.
PR 2 of the soak disk hygiene stack. The driver admits an iteration only inside the disk band, stops the soak when hygiene cannot clear the band, bounds every stop and cleanup command, completes the emergency response within one deadline, and publishes each breach record atomically. - scripts/run-merge-recovery-soak.sh with its host suite, the table-driven Docker harness and its Dockerfile, the emergency suite with 14 host fixtures, 8 real-daemon checks, and the metric and summary changes the driver needs - the B44 containment launcher and its native fixtures, a prototype the normal workflow does not use - the driver evidence record with rows B1 to B51, the slashing workflow record, and the work log for reviewers of PR 2 and PR 3 - ci.yml: the isolated disk admission step; merge-recovery-soak.yml: SOAK_EMERGENCY_DEADLINE_SECONDS 10 - Glossary: eleven driver terms; ToDos: three coordination bullets that PR 4 removes Verified: harness green on this tree, 42 scenarios; host suite, harness, real-daemon checks, and native fixtures green on a guarded runner on 2026-09-15 against an identical driver.
…3 adds The link checker scans every markdown file, and the claim arrives with PR 3, so the record links to the staging tip until the stack lands.
The record documents the TLA+ gate in slashing-tests.yml, which PR 3 changes, so it leaves this PR and lands with PR 3. Review finding on PR #431.
- soak-containment.py: reject the root group for the native workload identity and for the resolved account, and keep the cleanup path from masking the original error when the systemd query or stop fails - write-soak-summary.sh: restore dev's indentation, keep only the atomic write as the change - test-soak-disk-admission.sh: the disk-max-band header line now describes the assertion the harness makes
…gate PR 3 of the soak disk hygiene stack. Two consolidated TLA+ models, SoakDiskAdmission and SoakDiskGuardian, cover 23 driver corrections each, and every correction has a negative control that fails on the pre-fix driver. SoakStorageBudget and the six registered standalone metric and reserve models come with them. - scripts/ci/check-tla-invariants.sh: the NEGATIVE_CONTROLS registry, the registered control areas, the --soak-pr bounded tier, and the fixture hooks; the deploy storage and carrier index controls join the registry - scripts/ci/test-check-tla-invariants.sh: the gate fixture test, every registered control times seven outcomes plus the routing scenarios - slashing-tests.yml: the TLA+ job runs on every pull request with the 15-minute bounded tier and keeps the 240-minute nightly budget; ci.yml gains the fixture step - docs/claims/soak-disk-protection.md, the gate evidence record, the soak area README, the carrier index registered-controls text, and the soak row and gate text in the formal-verification guide Verified on this tree: bounded gate with 13 positives clean and all 61 negative controls violating their expected invariants.
MC_SoakDisk and its floor_only control extend the SoakDisk module that the consolidated models replaced. The stack does not carry that module, the registry does not name these configurations, and the work log lists them as superseded.
The record documents the TLA+ gate in slashing-tests.yml, which this PR changes, so it moves here from PR 2. Its links to the retired formal-gate claim and its evidence package are permalinks at the staging tip.
- evidence record: date the cycle G0/B2 tier and add a section for the current pull-request tier, 13 positives and 61 controls - reserve bound and retention reserve notes: both models are registered in the gate with their controls - RetentionReserve.tla: remove the unregistered liveness property that had no fairness condition - SoakDiskGuardian.tla: the exit-stop comment states what the model records - slashing-tests.yml: the log upload warns instead of failing on an early gate exit, and the job catalogue names the TLA+ job again
…ne and medium PR 4 of the soak disk hygiene stack. Adds the architecture note, two execution machines and four ordering media with verification split along that cut, and the CbC verification tiers document. Links both from the docs index and the formal-verification guide, and adds the three CbC glossary terms. Removes the coordination record the stack carried, now that the stack is complete: the stacked-PR plan from PR 1, the work log from PR 2, and the three soak coordination bullets in docs/ToDos.md. Git history and the staging branch on PR #406 keep them.
The classification loop ran the full gate 427 times, six rejection outcomes and one acceptance for each of the 61 controls, which took 8 minutes on the hosted runner and pushed the Lint job past its 15-minute limit. The rejection path is one code path in the gate, so the loop now exercises it on one control per registered area. The full-tier run checks the acceptance of every control's exact violation in one pass. Local runtime drops from over 10 minutes to 67 seconds.
- cbc-verification-tiers.md: the title and opening sentence use the glossary term Correct by Construction, and the Terms note says the document defines the four tier terms with glossary promotion as a follow-up - f1r3fly-consensus-neutral-sm.md: the interface-crate follow-up cites Section 12 for the thinner ordering trait
…th bash The repository ships Rust and bash. The disk-protection work introduced Python for pidfd-based process control, a systemd launcher prototype, and three root-only fixtures. This commit removes all of it. - The driver's Python sites are bash and jq. A process is identified by its PID paired with its start time from /proc/PID/stat, and exit is confirmed by polling that identity. The run-domain record check walks the path with stat and validates the record with jq. The startup probe requires a readable proc filesystem. The OCI tag update uses jq. - The crash monitor runs as bash -c 'crash_monitor "$@"' in its own session. The seven fixtures that used Python for pidfd checks use the same identity functions and assert that command line. - The B44 launcher prototype, its Python module, and the three native Python fixtures are removed. They stay on the source branch, and B44 stays open. - The fixture image and the harness tool check no longer install or require python3. - The evidence record, the stacked-PR plan, the ToDos bullet, the glossary entry (now process identity), and the work log record the mechanism, the check-then-act limit, and the verification. Verified on a Linux host with Docker: bash -n on every script, the image build, the host suite, all 42 disk-admission scenarios, and the crash-monitor, ownership, record, run-domain, and admission fixtures. The controller-loss fixture fails with the same verdict as the Python driver, which is the open B44 defect.
…ecution Carries the Python removal from the soak driver and fixtures across to PR 4. Three conflicts resolved toward this branch, which removes the stack's coordination record: the ToDos soak bullets stay removed, and the stacked-PR plan and the work log stay deleted. The glossary and the evidence record carry the process-identity mechanism and the fixture removal, so the port's substance survives without those files.
…signal batch The owner scan walked /proc/[0-9]* in shell glob order, which is lexicographic, so a child with a pid that sorts before its parent died first. On the Casper harness branch the benchmark client's sleep child took pid 128 while the client held pid 97, so the client fell through its sleep and returned before the stop reached it, and the benchmark-active-disk scenario failed. The Python scan it replaced read /proc in numeric order, which kills parents first. This branch passed only because its pids sorted the same both ways. The scan now sorts pids numerically, and the stop sends one batched kill for every target instead of one fork per pid, so the parent-to- child window shrinks from tens of milliseconds to microseconds. Same change as c20dc99 on formal/soak-casper-consensus. Verified here on a Linux host with Docker: benchmark-active-disk, crash-monitor death, and host stop ownership pass.
PR 2 of the soak disk hygiene stack. The driver admits an iteration only inside the disk band, stops the soak when hygiene cannot clear the band, bounds every stop and cleanup command, completes the emergency response within one deadline, and publishes each breach record atomically. - scripts/run-merge-recovery-soak.sh with its host suite, the table-driven Docker harness and its Dockerfile, the emergency suite with 14 host fixtures, 8 real-daemon checks, and the metric and summary changes the driver needs - the B44 containment launcher and its native fixtures, a prototype the normal workflow does not use - the driver evidence record with rows B1 to B51, the slashing workflow record, and the work log for reviewers of PR 2 and PR 3 - ci.yml: the isolated disk admission step; merge-recovery-soak.yml: SOAK_EMERGENCY_DEADLINE_SECONDS 10 - Glossary: eleven driver terms; ToDos: three coordination bullets that PR 4 removes Verified: harness green on this tree, 42 scenarios; host suite, harness, real-daemon checks, and native fixtures green on a guarded runner on 2026-09-15 against an identical driver.
…3 adds The link checker scans every markdown file, and the claim arrives with PR 3, so the record links to the staging tip until the stack lands.
The record documents the TLA+ gate in slashing-tests.yml, which PR 3 changes, so it leaves this PR and lands with PR 3. Review finding on PR #431.
- soak-containment.py: reject the root group for the native workload identity and for the resolved account, and keep the cleanup path from masking the original error when the systemd query or stop fails - write-soak-summary.sh: restore dev's indentation, keep only the atomic write as the change - test-soak-disk-admission.sh: the disk-max-band header line now describes the assertion the harness makes
…th bash The repository ships Rust and bash. The disk-protection work introduced Python for pidfd-based process control, a systemd launcher prototype, and three root-only fixtures. This commit removes all of it. - The driver's Python sites are bash and jq. A process is identified by its PID paired with its start time from /proc/PID/stat, and exit is confirmed by polling that identity. The run-domain record check walks the path with stat and validates the record with jq. The startup probe requires a readable proc filesystem. The OCI tag update uses jq. - The crash monitor runs as bash -c 'crash_monitor "$@"' in its own session. The seven fixtures that used Python for pidfd checks use the same identity functions and assert that command line. - The B44 launcher prototype, its Python module, and the three native Python fixtures are removed. They stay on the source branch, and B44 stays open. - The fixture image and the harness tool check no longer install or require python3. - The evidence record, the stacked-PR plan, the ToDos bullet, the glossary entry (now process identity), and the work log record the mechanism, the check-then-act limit, and the verification. Verified on a Linux host with Docker: bash -n on every script, the image build, the host suite, all 42 disk-admission scenarios, and the crash-monitor, ownership, record, run-domain, and admission fixtures. The controller-loss fixture fails with the same verdict as the Python driver, which is the open B44 defect.
…signal batch The owner scan walked /proc/[0-9]* in shell glob order, which is lexicographic, so a child with a pid that sorts before its parent died first. On the Casper harness branch the benchmark client's sleep child took pid 128 while the client held pid 97, so the client fell through its sleep and returned before the stop reached it, and the benchmark-active-disk scenario failed. The Python scan it replaced read /proc in numeric order, which kills parents first. This branch passed only because its pids sorted the same both ways. The scan now sorts pids numerically, and the stop sends one batched kill for every target instead of one fork per pid, so the parent-to- child window shrinks from tens of milliseconds to microseconds. Same change as c20dc99 on formal/soak-casper-consensus. Verified here on a Linux host with Docker: benchmark-active-disk, crash-monitor death, and host stop ownership pass.
fix(soak): protect the soak driver against disk exhaustion
…gate PR 3 of the soak disk hygiene stack. Two consolidated TLA+ models, SoakDiskAdmission and SoakDiskGuardian, cover 23 driver corrections each, and every correction has a negative control that fails on the pre-fix driver. SoakStorageBudget and the six registered standalone metric and reserve models come with them. - scripts/ci/check-tla-invariants.sh: the NEGATIVE_CONTROLS registry, the registered control areas, the --soak-pr bounded tier, and the fixture hooks; the deploy storage and carrier index controls join the registry - scripts/ci/test-check-tla-invariants.sh: the gate fixture test, every registered control times seven outcomes plus the routing scenarios - slashing-tests.yml: the TLA+ job runs on every pull request with the 15-minute bounded tier and keeps the 240-minute nightly budget; ci.yml gains the fixture step - docs/claims/soak-disk-protection.md, the gate evidence record, the soak area README, the carrier index registered-controls text, and the soak row and gate text in the formal-verification guide Verified on this tree: bounded gate with 13 positives clean and all 61 negative controls violating their expected invariants.
MC_SoakDisk and its floor_only control extend the SoakDisk module that the consolidated models replaced. The stack does not carry that module, the registry does not name these configurations, and the work log lists them as superseded.
The record documents the TLA+ gate in slashing-tests.yml, which this PR changes, so it moves here from PR 2. Its links to the retired formal-gate claim and its evidence package are permalinks at the staging tip.
- evidence record: date the cycle G0/B2 tier and add a section for the current pull-request tier, 13 positives and 61 controls - reserve bound and retention reserve notes: both models are registered in the gate with their controls - RetentionReserve.tla: remove the unregistered liveness property that had no fairness condition - SoakDiskGuardian.tla: the exit-stop comment states what the model records - slashing-tests.yml: the log upload warns instead of failing on an early gate exit, and the job catalogue names the TLA+ job again
The classification loop ran the full gate 427 times, six rejection outcomes and one acceptance for each of the 61 controls, which took 8 minutes on the hosted runner and pushed the Lint job past its 15-minute limit. The rejection path is one code path in the gate, so the loop now exercises it on one control per registered area. The full-tier run checks the acceptance of every control's exact violation in one pass. Local runtime drops from over 10 minutes to 67 seconds.
formal(soak): consolidated soak disk models and the negative-control gate
jltatbeach
approved these changes
Sep 19, 2026
docs: consensus-neutral execution and the verification split by machine and medium
jltatbeach
deployed
to
ephemeral-launch-internal
September 19, 2026 03:53 — with 
GitHub Actions
Active
GitHub Actions
Active
jltatbeach
deployed
to
protected-branch-image-publish
September 19, 2026 04:55 — with
GitHub Actions
Active
GitHub Actions
Active
…inates fix(crypto): keep the leading zero byte of a 64-byte coordinate pair
jltatbeach
deployed
to
ephemeral-launch-internal
September 19, 2026 05:17 — with
GitHub Actions
Active
GitHub Actions
Active
jltatbeach
deployed
to
protected-branch-image-publish
September 19, 2026 06:21 — with
GitHub Actions
Active
GitHub Actions
Active
jltatbeach
added this pull request to stack #446
September 19, 2026 18:19
jeffrey-l-turner
removed this pull request from stack #446
September 20, 2026 18:00
jeffrey-l-turner
added this pull request to stack #448
September 20, 2026 18:00
imbl 7.0.2 moves to imbl-sized-chunks 0.2.0, which fixes the double free in Chunk and InlineArray removal, and drops bitmaps. The bitmaps exception, ban, and pin test go with it.
spreston8
deployed
to
ephemeral-launch-internal
September 22, 2026 01:54 — with
GitHub Actions
Active
GitHub Actions
Active
This branch was successfully deployed
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
4 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.
No description provided.