feat(occupancy): grade the probe's samples against the HWM algebra (#105)

.github/workflows/occupancy.yml

@@ -22,6 +22,9 @@ on:
       - src/pipeline/tools.jl
       - src/server/routes/pipeline.jl
       - test/occupancy_disagreement_test.jl
+      - test/unit/test_occupancy_grade.jl
+      - scripts/check-occupancy-grades.jl
+      - scripts/lint-occupancy-readings.sh
       - docs/occupancy/**
       - docs/occupancy-2026-10.adoc
       - scripts/check-occupancy.sh
@@ -35,6 +38,9 @@ on:
       - src/pipeline/tools.jl
       - src/server/routes/pipeline.jl
       - test/occupancy_disagreement_test.jl
+      - test/unit/test_occupancy_grade.jl
+      - scripts/check-occupancy-grades.jl
+      - scripts/lint-occupancy-readings.sh
       - docs/occupancy/**
       - docs/occupancy-2026-10.adoc
       - scripts/check-occupancy.sh
@@ -107,6 +113,15 @@ jobs:
       - name: Three orders of the vsearch stage
         run: julia --project=. -t 2 test/occupancy_disagreement_test.jl
 
+      # Fork issue #105: the grades the recorded run's windows imply, read back
+      # against its own measurement (docs/occupancy/schedules.yml).
+      - name: Graded reading of the recorded run
+        run: julia --project=. scripts/check-occupancy-grades.jl
+
+      # And no production code reads a peak without those grades.
+      - name: Occupancy readings are graded
+        run: bash scripts/lint-occupancy-readings.sh
+
   typed-peak:
     name: Occupancy typed peak
     runs-on: ubuntu-24.04

docs/occupancy-2026-10.adoc

@@ -18,8 +18,9 @@ on 2026-10-14, and checks it against the typed reading.
 
 * `julia_allocated_bytes`: the `Base.gc_num()` delta over the stage (cost);
 * per task (one spawned search): the largest sampled VmRSS of the child
-  process it started (`peak_rss_kib`), and the kernel's own VmHWM for it
-  (`hwm_kib`);
+  process it started (`peak_rss_kib`), the kernel's own VmHWM for it
+  (`hwm_kib`), and the sample window its children were live in
+  (`first_sample`, `last_sample`) — what its grade is read from;
 * `child_peak_rss_kib`: the largest sum of the stage's children's VmRSS at
   one sampling instant (the stage's occupancy).
 
@@ -65,6 +66,36 @@ interval 10 ms.
   coincide. Here they did: each search's memory plateaus once its database is
   loaded.
 
+== Reading the numbers
+
+A recorded `peak_rss_kib` is a reading, not an occupancy: what a stage occupied
+depends on what the next stage inherits from it. So the probe grades a stage's
+whole window (`MemoryProbe`'s `task_grades`, `stage_grade`,
+`predicted_peak_rss_kib`, `cost_bound_rss_kib`, `reclaimed_kib`) and attaches the
+result to a recorded stage as `grades`; a record with no sample windows is left
+ungraded rather than graded on an assumed order. Tasks are read in sampled order
+(first sample, ties by record order); a task's drift is its peak when the next
+task still held it, and 0 when it had exited.
+
+For the three orders above, the algebra's predicted peak reproduces the measured
+stage peak exactly — 9204, 9192 and 18380 KiB — and the slack against the cost
+bound is what the cuts reclaimed: 9180, 9152 and 0 KiB.
+`scripts/check-occupancy-grades.jl` checks that equality, occupancy≤cost and
+non-negative reclamation against this page's raw record, rebuilding each order's
+windows from `docs/occupancy/schedules.yml` (the file records no windows of its
+own; the Session IR texts in this directory state the same interleavings). The
+reclamation readings are theorems over the pinned siblings at these numbers:
+`docs/occupancy/GradedStages.agda` — `no-reclaim` for the concurrent stage,
+`reclaimed` for the serial one, where 9204 KiB are released at the frontier and
+the cost reading counts them — and the two protocol-level statements
+(`occupancy-at-cut`, `protocol-occupancy≤cost`) as the siblings' own two-step
+over the stage's timeline. `docs/occupancy/reject` gains a fourth rejection, for
+reading the concurrent stage's drift as 0.
+
+`scripts/lint-occupancy-readings.sh` keeps production code from reading the key
+directly: outside `src/core/memory_probe.jl`, an occupancy figure must go through
+those helpers.
+
 == Status
 
 [cols="1,3,1,2",options="header"]
@@ -73,7 +104,8 @@ interval 10 ms.
 | MMW-01.1 | With the flag off, a stage record has exactly its earlier keys; with it on, it gains `occupancy`; old records still parse and merge | TESTED | `test/occupancy_disagreement_test.jl` ("flag off", "round trip", "through the pipeline's _attest")
 | MMW-01.2 | For this workload, the vsearch stage's cost (Julia allocation) is the same in all three orders | TESTED | same file, "two-thread disagreement" (asserted, within 1%)
 | MMW-01.3 | For this workload, the stage peak depends on the order (A-3), and each search's own peak does not | TESTED | same file, recorded in the test log; table above
-| MMW-01.4 | For the three Session IR texts, the stepper's counted bytes equal the HWM typed peak | TESTED | `scripts/check-occupancy.sh` (stepper output against `TypedPeak.agda`; two rejections in `docs/occupancy/reject`)
+| MMW-01.4 | For the three Session IR texts, the stepper's counted bytes equal the HWM typed peak | TESTED | `scripts/check-occupancy.sh` (stepper output against `TypedPeak.agda`; three rejections in `docs/occupancy/reject`)
+| MMW-01.5 | The recorded run's grades reproduce its measured stage peaks, and the reclamation the pinned siblings' laws read off them is what the cuts freed | TESTED | `scripts/check-occupancy-grades.jl` (the recorded record), `docs/occupancy/GradedStages.agda` (`no-reclaim`, `reclaimed`, `occupancy-at-cut` at the measured numbers), `test/unit/test_occupancy_grade.jl`
 | bridge | Counted bytes are bounded by the typed peak in general (occupancy-types' v0 → typed bridge) | OPEN | unchanged; this page gives three instances, not a proof
 |===
 
@@ -106,6 +138,8 @@ interval 10 ms.
 ----
 julia --project=. -t 2 test/occupancy_disagreement_test.jl   # set OCCUPANCY_RESULTS=<file> for YAML
 bash scripts/check-occupancy.sh                               # needs julia and agda 2.6.4.x
+julia --project=. scripts/check-occupancy-grades.jl           # the recorded run's grades
+bash scripts/lint-occupancy-readings.sh                       # no ungraded readings in src/
 ----
 
 `scripts/fetch-siblings.sh` fetches the siblings at their pins into

docs/occupancy/GradedStages.agda

@@ -0,0 +1,95 @@
+{-# OPTIONS --safe --without-K #-}
+-- SPDX-License-Identifier: AGPL-3.0-only
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+-- The vsearch stage's grades, and occupancy-types' reclamation theorems at the
+-- measured numbers. Fork issue #105 asks for exactly this: grade the stages
+-- (alloc/hold/release) and compare the predicted peak with the measured one.
+-- TypedPeak.agda computes the typed peak by the algebra's sequence law; this
+-- module adds the grades the measurement itself gives, and the laws that say
+-- what the difference between a peak and a cost reading is: occupancy≤cost, and
+-- the strict reclamation at a cut where something is released.
+--
+-- Consumed, never re-declared, from the siblings scripts/fetch-siblings.sh pins
+-- and scripts/check-occupancy.sh checks:
+--   occupancy-types  af957280075699c659de0abd9a3b0defade77309
+--   resource-algebra cf9235c532712a783a404c359a1055f40134794a
+-- Everything is stated in this file's own Timeline instance (`TH`, as
+-- TypedPeak.agda does): the Grade-level laws are Reclaim's as they stand, and
+-- the two protocol-level ones are Reclaim's own two-step — its `cut-factor` over
+-- its `reclaim-law`/`occupancy≤cost` — applied to `xs` and `ys` of that instance.
+--
+-- A grade is `hwm peak drift _`: what an interaction reached, and what it still
+-- holds when the next one begins. The peaks below are the 2026-10-14 run's
+-- (docs/occupancy-2026-10.adoc, docs/occupancy/results-2026-10-14.yml), in KiB.
+module GradedStages where
+
+open import ResourceAlgebra.Prelude
+open import ResourceAlgebra.Instances.HWM
+open import OccupancyTypes.Order
+open import OccupancyTypes.Reclaim
+
+import OccupancyTypes.Timeline
+module TH = OccupancyTypes.Timeline HWM
+
+-- A search that has not been waited for when the next one starts: it still holds
+-- everything it reached, so the cut reclaims none of it.
+still : Nat → Grade
+still p = hwm p p (≤-refl p)
+
+-- A search that has exited before the next one starts: it holds nothing, so the
+-- cut reclaims all of it.
+gone : Nat → Grade
+gone p = hwm p 0 z≤n
+
+-- The full pipeline runs the two searches together: ASV is still resident when
+-- OTU starts, so the stage peak is their sum and nothing is reclaimed —
+-- Reclaim.no-reclaim's equality, whose `refl` argument discharges the theorem's
+-- own hypothesis (drift = peak) at the measured grade.
+run-together : peak (still 9176 ⊗h gone 9204) ≡ 18380
+run-together = no-reclaim (still 9176) refl (gone 9204)
+
+-- A single-stage re-run runs them one after the other: ASV has exited, so the
+-- cut reclaims its 9204 KiB and the stage peak is the larger search's
+-- (Reclaim.reclaim-law, by `refl`).
+run-in-turn : peak (gone 9204 ⊗h gone 9180) ≡ 9204
+run-in-turn = refl
+
+-- The same claim as Reclaim.reclaimed states it: with drift < peak at the cut
+-- and a suffix that does anything, occupancy is strictly below cost. 9204 KiB
+-- are released at the frontier, so the cost reading (18384 KiB) overstates the
+-- stage.
+run-in-turn<cost : peak (gone 9204 ⊗h gone 9180) < peak (gone 9204) + peak (gone 9180)
+run-in-turn<cost = reclaimed (gone 9204) (gone 9180) (s≤s z≤n) (s≤s z≤n)
+
+-- The stage's own timeline: ASV 9204 then OTU 9180, the shape of
+-- docs/occupancy/vsearch-asv-then-otu.sir.
+vsearch-timeline : TH.Timeline
+vsearch-timeline = gone 9204 TH.∷ gone 9180 TH.∷ TH.[]
+
+-- Cut anywhere in it: the suffix starts from the prefix's DRIFT, not its peak.
+-- The statement Reclaim.occupancy-at-cut proves, at the two-task cut.
+at-the-cut : peak (TH.grade vsearch-timeline) ≡
+             max (peak (TH.grade (gone 9204 TH.∷ TH.[])))
+                 (drift (TH.grade (gone 9204 TH.∷ TH.[])) +
+                  peak (TH.grade (gone 9180 TH.∷ TH.[])))
+at-the-cut =
+  trans (cong peak (TH.cut-factor (gone 9204 TH.∷ TH.[]) (gone 9180 TH.∷ TH.[_])))
+        (reclaim-law (TH.grade (gone 9204 TH.∷ TH.[]))
+                     (TH.grade (gone 9180 TH.∷ TH.[_])))
+
+-- And occupancy never exceeds cost, at every cut of a pipeline: the slack is
+-- what the cut reclaims (the statement Reclaim.protocol-occupancy≤cost proves,
+-- from Reclaim.occupancy≤cost along Reclaim.cut-factor).
+any-cut≤cost : ∀ (xs ys : TH.Timeline)
+             → peak (TH.grade (TH._++_ xs ys)) ≤ peak (TH.grade xs) + peak (TH.grade ys)
+any-cut≤cost xs ys =
+  subst (_≤ peak (TH.grade xs) + peak (TH.grade ys))
+        (sym (cong peak (TH.cut-factor xs ys)))
+        (occupancy≤cost (TH.grade xs) (TH.grade ys))
+
+-- For the two searches as measured, the sum bound and the reclaiming bound
+-- together bracket the concurrent stage's peak: 18380 KiB, no more than their
+-- cost and no less than the larger search alone.
+together≤cost : peak (still 9176 ⊗h gone 9204) ≤ peak (still 9176) + peak (gone 9204)
+together≤cost = occupancy≤cost (still 9176) (gone 9204)

docs/occupancy/reject/ConcurrentDriftIsZero.agda

@@ -0,0 +1,18 @@
+{-# OPTIONS --safe --without-K #-}
+-- SPDX-License-Identifier: AGPL-3.0-only
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+-- Must be REFUSED: reading the concurrent stage as one that hands on nothing.
+-- Running the two searches together leaves the ASV search resident when the OTU
+-- search starts, so the stage's drift is that search's peak — 9176 KiB, what a
+-- suffix would see — and not 0. Grading the drift as 0 would read the stage's
+-- COST as its occupancy, which is the very reading the measured overlap exists
+-- to refute.
+module ConcurrentDriftIsZero where
+
+open import ResourceAlgebra.Prelude
+open import ResourceAlgebra.Instances.HWM
+open import GradedStages
+
+wrong : drift (still 9176 ⊗h gone 9204) ≡ 0
+wrong = refl

docs/occupancy/schedules.yml

@@ -0,0 +1,21 @@
+# SPDX-License-Identifier: AGPL-3.0-only
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# The interleaving each order in results-2026-10-14.yml ran with, as the sample
+# window [first, last] of each of its tasks, in the task order the record keeps.
+# These are the same schedules the Session IR texts in this directory state
+# (vsearch-concurrent.sir runs the two searches together; the other two run them
+# one after the other), expressed in the probe's own sample indices: the windows
+# of a serial order do not overlap, and the concurrent order's do.
+#
+# Read by test/unit/test_occupancy_grade.jl and scripts/check-occupancy-grades.jl,
+# so the two cannot disagree about what the recorded run did.
+asv_then_otu:
+  - [1, 2]
+  - [3, 4]
+otu_then_asv:
+  - [1, 2]
+  - [3, 4]
+concurrent:
+  - [1, 4]
+  - [2, 5]

scripts/check-occupancy-grades.jl

@@ -0,0 +1,72 @@
+# SPDX-License-Identifier: AGPL-3.0-only
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# Gate for the graded reading of the recorded run (fork issue #105): rebuild each
+# order's timeline from its sample window (docs/occupancy/schedules.yml), grade it
+# with the module the probe itself uses (src/core/memory_probe.jl — included
+# rather than the whole package, so this needs OrderedCollections and YAML only),
+# and compare the algebra's predicted peak with the measured one.
+#
+# The recorded run is fixed evidence, so the comparison is an equality: this is
+# the reading docs/occupancy-2026-10.adoc publishes, and a change that moves it
+# must be a deliberate one. Two further claims hold of every order and are
+# checked: the prediction is never above the cost bound (occupancy≤cost) and the
+# slack between them is never negative (what the cuts reclaim).
+#
+# Run from the repository root:  julia --project=. scripts/check-occupancy-grades.jl
+include(joinpath(@__DIR__, "..", "src", "core", "memory_probe.jl"))
+using .MemoryProbe
+using YAML
+
+const ROOT      = normpath(joinpath(@__DIR__, ".."))
+const RESULTS   = joinpath(ROOT, "docs", "occupancy", "results-2026-10-14.yml")
+const SCHEDULES = joinpath(ROOT, "docs", "occupancy", "schedules.yml")
+
+orders    = YAML.load_file(RESULTS)["orders"]
+schedules = YAML.load_file(SCHEDULES)
+
+failures = 0
+function fail(message)
+    global failures += 1
+    println("FAIL: ", message)
+end
+
+println(rpad("order", 16), rpad("predicted", 11), rpad("measured", 11),
+        rpad("cost", 8), "reclaimed")
+# An order's timeline, from the peaks the probe recorded and the window each task
+# ran in. Nothing else is taken from the schedule: the grades are the
+# measurement's.
+function timeline(rec, windows)
+    tasks = Any[Dict{String,Any}("label"        => t["label"],
+                                 "peak_rss_kib" => t["peak_rss_kib"],
+                                 "first_sample" => windows[i][1],
+                                 "last_sample"  => windows[i][2])
+                for (i, t) in enumerate(rec["tasks"])]
+    Dict{String,Any}("child_peak_rss_kib" => rec["child_peak_rss_kib"], "tasks" => tasks)
+end
+
+for name in sort(collect(keys(orders)))
+    rec       = orders[name]
+    occ       = timeline(rec, schedules[name])
+    predicted = MemoryProbe.predicted_peak_rss_kib(occ)
+    cost      = MemoryProbe.cost_bound_rss_kib(occ)
+    reclaimed = MemoryProbe.reclaimed_kib(occ)
+    measured  = rec["child_peak_rss_kib"]
+    println(rpad(name, 16), rpad(string(predicted), 11), rpad(string(measured), 11),
+            rpad(string(cost), 8), string(reclaimed))
+
+    predicted == measured ||
+        fail("$name: predicted $predicted KiB != measured $measured KiB")
+    predicted <= cost ||
+        fail("$name: predicted $predicted KiB above the cost bound $cost KiB (occupancy≤cost)")
+    reclaimed >= 0 ||
+        fail("$name: reclaimed $reclaimed KiB is negative")
+    d = MemoryProbe.disagreement(occ)
+    d === nothing || fail("$name: $d")
+end
+
+if failures > 0
+    println("check-occupancy-grades: $failures failure(s)")
+    exit(1)
+end
+println("check-occupancy-grades: OK — the prediction reproduces the recorded measurement")

scripts/check-occupancy.sh

@@ -4,8 +4,9 @@
 #
 # Gate for the occupancy reading of the vsearch stage (docs/occupancy-2026-10.adoc):
 #   1. each Session IR text checks, and occupancy-types' stepper counts its bytes;
-#   2. TypedPeak.agda type-checks against the pinned siblings, and each module in
-#      docs/occupancy/reject is refused at its own declaration;
+#   2. TypedPeak.agda and GradedStages.agda type-check against the pinned
+#      siblings, and each module in docs/occupancy/reject is refused at its own
+#      declaration;
 #   3. the counted bytes equal the typed peak, order by order.
 # Needs julia and agda (2.6.4.x) on PATH. Exit 0 only if all three hold.
 set -euo pipefail
@@ -22,6 +23,29 @@
 mkdir -p "$logs"
 failures=0
 
+# GitHub renders an `::error` line as a check annotation, and annotations -- unlike
+# job logs -- can be read back through the API. A failure that only happens in CI
+# must be readable from a machine that cannot download the log, so every failure
+# below says what it was and repeats the prover's own last lines: % escapes to
+# %25 and newlines to %0A, as the workflow-command syntax requires.
+annotate() {  # title file log
+  [ -n "${GITHUB_ACTIONS:-}" ] || return 0
+  printf '::error file=%s,title=%s::%s\n' "$2" "$1" \
+    "$(awk 'NR > 1 { printf "%%0A" } { gsub(/%/, "%25"); printf "%s", $0 }' "$3" |
+       tail -c 6000)"
+}
+
+# One Agda module that must type-check, with its own log.
+check_agda() {  # file label
+  if ! agda "${flags[@]}" "$1" >"$logs/$2.log" 2>&1; then
+    cat "$logs/$2.log"
+    annotate "Agda refused $2" "$1" "$logs/$2.log"
+    echo "ERROR: $1 does not type-check" >&2
+    exit 1
+  fi
+  echo "PASS: $2"
+}
+
 # Order -> Session IR file and TypedPeak lemma.
 orders=(asv-then-otu otu-then-asv concurrent)
 
@@ -36,18 +60,26 @@
 done
 
 echo "== Typed peak (Agda, HWM Timeline)"
-agda "${flags[@]}" docs/occupancy/TypedPeak.agda >"$logs/TypedPeak.log" 2>&1 ||
-  { cat "$logs/TypedPeak.log"; echo "ERROR: TypedPeak.agda does not type-check" >&2; exit 1; }
-echo "PASS: TypedPeak.agda"
+check_agda docs/occupancy/TypedPeak.agda TypedPeak.agda
+
+# The graded reading (fork issue #105): occupancy-types' Reclaim theorems at the
+# measured grades, from the same pinned siblings. The recorded run's grades
+# against its measurement are checked by scripts/check-occupancy-grades.jl, which
+# needs the project's Julia packages and so runs in the disagreement job.
+check_agda docs/occupancy/GradedStages.agda GradedStages.agda
 for file in docs/occupancy/reject/*.agda; do
   name="$(basename -- "$file" .agda)"
   log="$logs/$name.log"
   if agda "${flags[@]}" -i docs/occupancy/reject "$file" >"$log" 2>&1; then
-    cat "$log"; echo "ERROR: invalid claim accepted: $name" >&2; failures=$((failures + 1)); continue
+    cat "$log"
+    annotate "Invalid claim accepted: $name" "$file" "$log"
+    echo "ERROR: invalid claim accepted: $name" >&2; failures=$((failures + 1)); continue
   fi
   if ! grep -Eq "/$name\.agda:[0-9]+,[0-9]+" "$log" || ! grep -q 'when checking that' "$log" ||
      grep -Eq 'Not in scope|Failed to find|Unsolved|Parse error' "$log"; then
-    cat "$log"; echo "ERROR: $name failed for the wrong reason" >&2; failures=$((failures + 1)); continue
+    cat "$log"
+    annotate "$name failed for the wrong reason" "$file" "$log"
+    echo "ERROR: $name failed for the wrong reason" >&2; failures=$((failures + 1)); continue
   fi
   echo "PASS: rejected $name ($(grep -m1 -E '[0-9]+ != [0-9]+' "$log"))"
 done
@@ -59,6 +91,8 @@
   printf '%-14s %10s %10s\n' "$o" "${counted[$o]}" "$typed"
   if [ -z "${counted[$o]}" ] || [ -z "$typed" ] || [ "${counted[$o]}" != "$typed" ]; then
     echo "ERROR: $o: counted ${counted[$o]:-?} != typed ${typed:-?}" >&2; failures=$((failures + 1))
+    echo "counted ${counted[$o]:-?} KiB != typed ${typed:-?} KiB" >"$logs/counted-$o.log"
+    annotate "Counted bytes != typed peak ($o)" docs/occupancy/TypedPeak.agda "$logs/counted-$o.log"
   fi
 done