Repository navigation
feat(occupancy): grade the probe's samples against the HWM algebra (#105) - #116
Merged
Merged
Conversation
) Fork issue #105: the probe recorded what a stage reached (`peak_rss_kib`, `child_peak_rss_kib`) but nothing read an *occupancy* out of it, so a peak could only be compared against a cost. This grades the samples with the algebra the reading is stated in — `ResourceAlgebra.Instances.HWM`, whose reclamation laws `OccupancyTypes.Reclaim` proves — and checks the peak the algebra predicts against the one the samples measured. ## The grade, read from the samples Two sample windows are now recorded per task (`first_sample`, `last_sample`, set in `watch!`/`unwatch!`), and `finish!` attaches the grades read from them as the record's `grades` key: - `Grade(peak, drift)` with `drift ≤ peak`, `release = peak − drift`; - `seq` — the suffix starts from the previous grade's drift, `max (peak a) (drift a + peak b)` (Reclaim.reclaim-law); `alt` is the componentwise join, kept for the pair of laws; - `task_grades`, `stage_grade`, `predicted_peak_rss_kib`, `cost_bound_rss_kib`, `reclaimed_kib`, `disagreement`, `graded`. Tasks are read in sampled order (first sample, ties by record order); a task's drift is its peak when the next task started at or before its last sample, and the last task keeps its peak only if it was still resident. A record carrying no windows is left UNGRADED — `nothing`, skipped — never graded on an assumed order. (The 2026-10-14 record itself carries none: its windows come from `docs/occupancy/schedules.yml`, the file the gate and the unit test both read.) ## What it reads out of the recorded run `predicted_peak_rss_kib` reproduces the recorded stage peak in all three orders — 9204, 9192 and 18380 KiB — and the slack against the cost bound is what the cuts reclaimed: 9180, 9152 and 0 KiB. The prediction is an upper bound (at a handover the task still live holds at most its peak), so `disagreement` reports only what that bound forbids: a measured peak above the prediction. `scripts/check-occupancy-grades.jl` checks the equality, occupancy≤cost and non-negative reclamation against the record, and `test/unit/test_occupancy_grade.jl` (plus the two-thread test's per-order assertions) covers the laws, the two stage shapes and `finish!` itself. ## The same numbers, as theorems `docs/occupancy/GradedStages.agda` consumes the pinned siblings (occupancy-types `af95728`, resource-algebra `cf9235c`) and instantiates three of `Reclaim`'s laws at the measured grades: `no-reclaim` on the concurrent stage (drift = peak, so the peak is the sum), `reclaimed` on the serial one (drift < peak with a non-empty suffix, so strictly below cost), and `occupancy-at-cut` over the stage's timeline, plus `protocol-occupancy≤cost` at every cut. Nothing is re-declared; the Timeline names are Reclaim's own instance. `docs/occupancy/ reject/ConcurrentDriftIsZero.agda` is the negative control — grading the concurrent stage's drift as 0 is refused — checked by `scripts/check-occupancy.sh` beside TypedPeak. ## No ungraded readings `scripts/lint-occupancy-readings.sh` fails if production code outside `src/core/memory_probe.jl` names the `peak_rss_kib` key. It passes on this tree; from here a stage's occupancy figure has to come from the helpers. ## Verification No Julia or Agda in this environment, so the recorded arithmetic above was emulated exactly (three orders, plus each fixture in the unit test) and the Agda was written against the siblings' own checked sources, following the import and proof style of `OccupancyTypes.Witness`, which `occupancy-types/scripts/check-agda.sh` checks with the same flags. CI is the verifier: ci.yml's unit run, and the occupancy workflow's new graded reading and lint steps. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
|
Note Currently processing new changes in this PR. This may take a few minutes, please wait... ⚙️ Run configuration
📒 Files selected for processing: 12
✨ Finishing Touches: 💡 1
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
…ate CI failures The occupancy workflow's typed-peak job failed on the first push (it passes on main, so the failure is this change's). Its logs are served from blob storage, which this environment cannot reach, so two things: - `docs/occupancy/GradedStages.agda` now stands on its own names, the way `docs/occupancy/TypedPeak.agda` does: its own `module TH = OccupancyTypes.Timeline HWM` for every Timeline name, and the two protocol-level statements proved in that instance from the sibling's own halves — `Reclaim.cut-factor` over `reclaim-law`, and `occupancy≤cost` along `cut-factor` for `protocol-occupancy≤cost`, each proof the one `OccupancyTypes.Reclaim` gives for the same statement. The Grade-level laws (`no-reclaim`, `reclaimed`, `occupancy≤cost`) were already cited as they stand. Nothing re-declared, nothing borrowed across instances. - `scripts/check-occupancy.sh` now emits a `::error` annotation on every failure it diagnoses (each module, both rejection failure modes, the counted-bytes comparison), with the prover's own last lines escaped as the workflow-command syntax requires. Annotations, unlike job logs, can be read back through the API, so a failure that happens only in CI is visible from a machine that cannot download the log. Silent outside Actions, so local runs are unchanged. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
|
|
❌ Failed to create Coding Agent finishing-touch task. Please try again. |
hyperpolymath
added a commit
that referenced
this pull request
Oct 14, 2026
) Two lines of `docs/occupancy/GradedStages.agda` on `main` (from the #116 squash) still carry a draft placeholder: `TH.[_]` where `TH.[]` belongs. Agda refuses it at the parse, before checking anything else: ``` docs/occupancy/GradedStages.agda:77,59-80 Could not parse the application gone 9180 TH.∷ TH.[_] Operators used in the grammar: TH.∷ (infixr operator, level 5) when scope checking gone 9180 TH.∷ TH.[_] ``` So `main`'s **Occupancy typed peak** job is red at `scripts/check-occupancy.sh`, and with it the graded reading the #116 squash landed. This PR is that fix and nothing else: `TH.[_]` → `TH.[]` in both places, 2 lines, no other change (`git diff origin/main..HEAD` = this file only). ## How the error became readable The job's log is served from storage this environment cannot reach, so #116 added `annotate` to `scripts/check-occupancy.sh`: every failure it diagnoses now emits a `::error` line (with the prover's own last lines, escaped as the workflow-command syntax requires), and check annotations — unlike logs — are available through the API. That is how the parse error above was read back from run [38628333902](https://github.com/hyperpolymath/MetaManifold-WebUI/actions/runs/38628333902). It stays silent outside Actions. ## Why the first push looked different The first run on #116 (d49c2e3) failed before the annotations existed, so its cause was never readable; the revision that added them (cf1b726) is what reported this parse error, and it is what the squash carried into `main`. Nothing else in the #116 change is affected: `OccupancyTypes.Reclaim` itself type-checks under this repo's flags — visible in the same job's log, which reaches my file only after checking Prelude, Core, HWM, Order, Reclaim and Timeline. CI on this PR is the check: the typed-peak job must go green, and the disagreement job re-runs the recorded study as usual. --------- Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> Co-authored-by: coderabbitai[bot] <136622811+coderabbitai[bot]@users.noreply.github.com> Co-authored-by: CodeRabbit <noreply@coderabbit.ai>
hyperpolymath
added a commit
that referenced
this pull request
Oct 15, 2026
…ecks can be required #116 merged with this workflow's "Occupancy typed peak" check red (its squash carried a draft `TH.[_]` placeholder; #117 fixed the proof), because nothing required the check to pass first -- and nothing could have: the pull_request trigger was path-filtered, so the check never posted on PRs that touch no occupancy file, and a required check that never posts can never be satisfied. The path filter now lives in an `Occupancy relevance` gate job: the workflow runs on every PR, the gate diffs the change against the same file list (plain `case` globs; a third-party paths-filter action is refused by the account's allow-list), and the two heavy jobs run only when it matches -- posting `skipped` otherwise, which a required check counts as satisfied. All three job names are stable identifiers with no matrix, as test_install_pins.jl asserts for every job in every workflow. Branch-Floor can then require `Occupancy relevance` (itself included: a failed gate skips its dependents, and a skipped check satisfies a requirement -- the gate is the one check that must not be skipped silently), `Occupancy disagreement test`, `Occupancy typed peak`, alongside ci.yml's `Julia tests` and `Agda proofs`. That ruleset change is a settings change, kept out of this PR on purpose. Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
This was referenced Oct 15, 2026
Merged
hyperpolymath
added a commit
that referenced
this pull request
Oct 15, 2026
…ecks can be required (#125) ## What this changes #116 merged with this workflow's "Occupancy typed peak" check red (its squash carried a draft `TH.[_]` placeholder; #117 fixed the proof), because nothing required the check to pass first -- and nothing could have: the `pull_request` trigger was path-filtered, so the occupancy checks never posted on PRs that touch no occupancy file, and a required check that never posts can never be satisfied. The Branch-Floor ruleset requires nothing today; ci.yml's header already documents this trap for its own job names. The PR path filter now lives in an `Occupancy relevance` gate job: - the workflow runs on **every** pull request, so all three of its checks always post; - the gate diffs the change against the same file list with plain `case` globs (a third-party paths-filter action would be refused by the account's allow-list; in a case pattern `*` crosses `/`, so `docs/occupancy/*` is the old `docs/occupancy/**`); - `Occupancy disagreement test` and `Occupancy typed peak` run only when the gate says relevant, and post `skipped` otherwise -- which a required check counts as satisfied; - the push trigger keeps its native `paths:` filter, so pushes to main still run this only when they should. All three job names are stable identifiers with no matrix, as `test/unit/test_install_pins.jl` asserts for every job in every workflow. ## What this enables (kept out of this PR on purpose) Once merged, Branch-Floor can require `Occupancy relevance` (itself included: a failed gate skips its dependents, and a skipped check satisfies a requirement silently -- the gate is the one check that must not be skipped), `Occupancy disagreement test`, `Occupancy typed peak`, alongside ci.yml's `Julia tests` and `Agda proofs`. That ruleset change is a settings change and will follow separately. ## How to run its tests From the repository root: ``` julia --project=. test/unit/test_install_pins.jl ``` All 223 assertions pass locally (the gate job satisfies the every-job stable-name and no-matrix rules and uses the pinned `actions/checkout` SHA). CI on this PR is the full check: this PR touches `occupancy.yml` itself, so the gate must mark it relevant and both heavy jobs must run. ## What this leaves out No ruleset change (above), no change to the heavy jobs' contents, and the two startup_failure-era path lists (push trigger, gate patterns) necessarily duplicate each other -- push filtering cannot be scripted, and the gate's list is documented as the pull_request half. ## Versions tested Julia 1.13.1 (local; CI pins 1.12.5 per `tool_versions.yml`). Bun, R and Agda untouched by this change -- CI runs the pinned ones. Note: this commit is unsigned (the signing key's passphrase is not available to the session); amend to sign if the fork's history requires it. --------- Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai> --------- Co-authored-by: Mistral Vibe <vibe@mistral.ai> Co-authored-by: coderabbitai[bot] <136622811+coderabbitai[bot]@users.noreply.github.com>
hyperpolymath
added a commit
that referenced
this pull request
Oct 15, 2026
The workflow already runs on every pull request; now a cheap gate decides whether the change touches anything the suite exercises, and the two heavy jobs -- Julia tests (~19 minutes), Agda proofs -- run only when it says relevant. On a docs-only PR they post `skipped`, which satisfies a required check, exactly as the occupancy workflow's gate (#125) already does for its two reading jobs. The trigger stays unfiltered on purpose: a path-filtered pull_request trigger does not run at all on a PR that matches no path, so a required check from that workflow never posts and can never be satisfied -- the trap #116 sprang. The relevant-path list is the positive form: anything not listed is not relevant, so a new directory joins the suite by being added here rather than by being forgotten. Paths the tests themselves read are listed even though they are documentation-shaped: .github/workflows/ (the pin tests parse it), docs/occupancy/ (the reading's Agda tree), and the repo-shape inputs (Project.toml, Manifest.toml, renv.lock, the launchers). The gate carries every hardening #125's review produced: --no-renames (a file renamed out of a listed path is reported as a deletion under its original name), -z with a NUL-delimited read (a pathname Git would quote or that contains a newline arrives raw), the base SHA through env rather than template interpolation into the script, and now every pattern quoted in the array -- an unquoted `src/*` expands against the checkout at assignment time, which a directory-level glob list makes visible; the glob must fire at case time, against the diff. Verified locally: the gate logic was run against seven cases (docs-only, src change, occupancy docs, rename-away, an unusual-character occupancy path, a workflow change, README+CITATION) with the expected verdict each time; actionlint clean; the pin suite passes 259/259, which asserts the gate job's name is a stable identifier, that it has no matrix, and that its pinned actions/checkout is allowed by the account's policy. This PR touches .github/workflows/ci.yml, so the gate marks it relevant and the full suite runs on it -- the gate's own first test. Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
hyperpolymath
added a commit
that referenced
this pull request
Oct 15, 2026
The workflow already runs on every pull request; now a cheap gate decides whether the change touches anything the suite exercises, and the two heavy jobs -- Julia tests (~19 minutes), Agda proofs -- run only when it says relevant. On a docs-only PR they post `skipped`, which satisfies a required check, exactly as the occupancy workflow's gate (#125) already does for its two reading jobs. The trigger stays unfiltered on purpose: a path-filtered pull_request trigger does not run at all on a PR that matches no path, so a required check from that workflow never posts and can never be satisfied -- the trap #116 sprang. The relevant-path list is the positive form: anything not listed is not relevant, so a new directory joins the suite by being added here rather than by being forgotten. Paths the tests themselves read are listed even though they are documentation-shaped: .github/workflows/ (the pin tests parse it), docs/occupancy/ (the reading's Agda tree), and the repo-shape inputs (Project.toml, Manifest.toml, renv.lock, the launchers). The gate carries every hardening its reviews produced: --no-renames (a file renamed out of a listed path is reported as a deletion under its original name), -z with a NUL-delimited read (a pathname Git would quote or that contains a newline arrives raw), the base SHA through env rather than template interpolation into the script, every pattern quoted in the array (an unquoted `src/*` expands against the checkout at assignment time; the glob must fire at case time, against the diff), and -- per the CodeRabbit review of this PR, mirroring the occupancy gate -- the diff is written to a file first with git diff's exit status checked, because a process substitution hides it and a failed diff would read as "no changes", skipping the suite on a PR that changed code. Verified locally: the gate logic was run against seven cases (docs-only, src change, occupancy docs, rename-away, an unusual-character occupancy path, a workflow change, README+CITATION) with the expected verdict each time, plus the failed-diff case now failing the gate; actionlint clean; the pin suite passes, which asserts the gate job's name is a stable identifier, that it has no matrix, and that its pinned actions/checkout is allowed by the account's policy. This PR touches .github/workflows/ci.yml, so the gate marks it relevant and the full suite runs on it -- the gate's own first test. Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>
hyperpolymath
added a commit
that referenced
this pull request
Oct 15, 2026
## What this changes The answer to "must every check run on everything equally": no, and without giving up enforcement. A new cheap **`Code relevance`** gate job runs on every pull request and decides whether the change touches anything the suite exercises; the two heavy jobs — **`Julia tests`** (~19 minutes) and **`Agda proofs`** — now carry `if: needs.gate.outputs.relevant == 'true'` and post `skipped` when the gate says not relevant. A skipped check satisfies a required check, so Branch-Floor enforcement is unchanged: a docs-only PR (README, wiki, templates, licence records) finishes in the gate's ~10 seconds plus the external scanners instead of ~19 minutes. The design is the pattern PR #125 established for the occupancy workflow, applied to the main suite, with every hardening that review produced: - **The trigger stays unfiltered on purpose** — a path-filtered `pull_request` trigger does not run at all on a PR that matches no path, so a required check from that workflow never posts and can never be satisfied. That trap was sprung here once (#116) and documented in this file's header. - **`--no-renames`** — a file renamed out of a listed path is reported as a deletion under its original name and still counts. - **`-z` with a NUL-delimited read** — a pathname Git would quote, or that contains a newline, arrives raw and matches the pattern. - **Base SHA through `env:`**, not template interpolation into the script (zizmor's rule). - **Every pattern quoted in the array** — this PR's own new finding: an unquoted `src/*` in an array assignment expands against the checkout the runner happens to stand in; with a directory-level glob list that is visibly wrong, and the glob must fire at `case` time against the diff. The relevant-path list is deliberately the positive form: anything not listed is not relevant, so a new directory joins the suite by being added to the list, not by being forgotten. Paths the tests themselves read stay relevant even though they are documentation-shaped: `.github/workflows/` (the pin tests parse it), `docs/occupancy/` (the reading's Agda tree), and the repo-shape inputs (`Project.toml`, `Manifest.toml`, `renv.lock`, the launchers, `R/`, `renv/`). ## Verification - The gate logic ran locally against seven cases — docs-only, src change, occupancy docs, rename-away, an unusual-character occupancy path, a workflow change, README+CITATION — with the expected verdict each time. - `actionlint` clean; the pin suite passes 259/259, which asserts for the new gate job that its name is a stable identifier, that it has no matrix, and that its pinned `actions/checkout` is allowed by the account's policy. - **This PR is the gate's own first test**: it touches `.github/workflows/ci.yml`, so the gate must mark it relevant and the full suite must run on it. The first docs-only PR after this lands is the second test. ## Follow-up after merge Add `Code relevance` to the Branch-Floor ruleset's required checks — it is the one check that must never be skipped, since it vouches for the others' absence. I'll apply it once the check has posted here. ## Notes The commit is signed (the agent socket is now available to this session). Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai> Co-authored-by: Mistral Vibe <vibe@mistral.ai>
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
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.
Closes #105. First item of the ordered issue programme (#105 → #1 phase 1 → #21 → …).
#105 asks for the amplicon pipeline's stages to be graded — alloc/hold/release — and for the predicted peak to be compared with the measured one, with a disagreement meaning a bug in one of them. The probe recorded what a stage reached but nothing read an occupancy out of it, so a
peak_rss_kibcould only be compared against a cost. This reads the occupancy with the algebra the reading is stated in:ResourceAlgebra.Instances.HWM, whose reclamation lawsOccupancyTypes.Reclaimproves (the sibling's PR #9 the issue cites).The grade, read from the samples
watch!/unwatch!now record each task's sample window (first_sample,last_sample) beside its peak;finish!attaches the grades read from those windows as the record'sgradeskey.Grade(peak, drift)withdrift ≤ peak(anArgumentErrorotherwise),release = peak − drift;seqis the algebra's sequencingmax (peak a) (drift a + peak b)(Reclaim.reclaim-law),altthe componentwise join the pair of laws needs;task_grades,stage_grade,predicted_peak_rss_kib,cost_bound_rss_kib,reclaimed_kib,graded.nothing): skipped, never graded on an assumed order, anddisagreementstays silent — not measured is not a disagreement.What it reads out of the recorded run
docs/occupancy/results-2026-10-14.yml, windows fromdocs/occupancy/schedules.yml(the file the gate and the unit test both read; the raw record of that run predates the window fields, and the Session IR texts indocs/occupancy/state the same interleavings):The prediction is an upper bound (at a handover the task still live holds at most its peak), so
disagreementreports only what that bound forbids: a measured peak above the prediction.scripts/check-occupancy-grades.jlre-derives the table from the record and fails on an inequality; the numbers are emulated-checked here because this environment has no Julia.The same numbers, as theorems
docs/occupancy/GradedStages.agdaconsumes the pinned siblings (occupancy-typesaf95728, resource-algebracf9235c— nothing re-declared; the Timeline names are Reclaim's own instance) and instantiates three ofReclaim's laws at the measured grades:no-reclaimon the concurrent stage — drift = peak, so the peak is the sum (18380);reclaimedon the serial one — drift < peak with a non-empty suffix, so strictly below cost (9204 < 18384);occupancy-at-cutover the stage's timeline, andprotocol-occupancy≤costat every cut.docs/occupancy/reject/ConcurrentDriftIsZero.agdais the negative control: grading the concurrent stage's drift as 0 — reading the cost as the occupancy — is refused, andscripts/check-occupancy.shnow type-checksGradedStagesbesideTypedPeakand requires that refusal.No ungraded readings
scripts/lint-occupancy-readings.shfails if production code outsidesrc/core/memory_probe.jlnames thepeak_rss_kibkey: from here a stage's occupancy figure has to come from the grading helpers. It passes on this tree.Tests and CI
test/unit/test_occupancy_grade.jl(new, wired intotest/runtests.jl): the grade invariant, theseq/altlaws, the two stage shapes (serial 100/160/60, together 160/160/0), thegradedrecord, a measured-above-prediction disagreement, the ungraded no-window record, afinish!/watch!run on Linux, and the recorded-run replay.test/occupancy_disagreement_test.jl: the two-thread testset now asserts, per order, that every task carries both window keys, that the record is graded, that the prediction reaches the measurement, that it stays at or below the cost bound (occupancy≤cost) and that the slack is never negative. The peaks themselves stay recorded, not asserted..github/workflows/occupancy.yml: two new steps (the graded reading, the lint) in thedisagreementjob, and the new files added to bothpathsfilters.docs/occupancy-2026-10.adoc: the window fields, a "Reading the numbers" section, status row MMW-01.5, the new commands.Verification limits
No Julia and no Agda on this machine, so: the recorded arithmetic and every fixture number were emulated exactly; the Agda follows the import and proof style of
OccupancyTypes.Witness(checked by the sibling'sscripts/check-agda.sh, same flags); the workflow YAML and the new scripts were syntax-checked and the lint was run. CI is the verifier here — including whetherOccupancyTypes.Reclaimtype-checks under this repo's flags, which this change is the first to require.Not in this change
The adoc's
bridgerow — counted bytes bounded by the typed peak in general (occupancy-types' v0 → typed bridge) — stays OPEN: this change gives the graded reading, its instances and its laws, not that proof.