Docs/occupancy typed reading

.github/workflows/occupancy.yml

@@ -0,0 +1,145 @@
+# SPDX-License-Identifier: AGPL-3.0-only
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# The occupancy reading of the vsearch stage (docs/occupancy-2026-10.adoc):
+#   * the two-thread disagreement test (test/occupancy_disagreement_test.jl) on
+#     the pinned vsearch, and
+#   * Session IR's counted bytes against the typed peak computed in Agda from
+#     the pinned proof siblings (scripts/check-occupancy.sh).
+#
+# This account allows only GitHub's own actions and its own, pinned by SHA, so
+# ci.yml (julia-actions, setup-bun, codecov) cannot start on this fork. That is
+# why everything here installs from pinned URLs checked against pinned SHA256s,
+# and why the disagreement test runs here as well as in ci.yml's full suite.
+name: Occupancy reading
+
+on:
+  push:
+    branches: [main]
+    paths:
+      - src/core/memory_probe.jl
+      - src/core/provenance.jl
+      - src/pipeline/tools.jl
+      - src/server/routes/pipeline.jl
+      - test/occupancy_disagreement_test.jl
+      - docs/occupancy/**
+      - docs/occupancy-2026-10.adoc
+      - scripts/check-occupancy.sh
+      - scripts/fetch-siblings.sh
+      - .github/workflows/occupancy.yml
+  # Any base branch, so a PR stacked on another one is checked too.
+  pull_request:
+    paths:
+      - src/core/memory_probe.jl
+      - src/core/provenance.jl
+      - src/pipeline/tools.jl
+      - src/server/routes/pipeline.jl
+      - test/occupancy_disagreement_test.jl
+      - docs/occupancy/**
+      - docs/occupancy-2026-10.adoc
+      - scripts/check-occupancy.sh
+      - scripts/fetch-siblings.sh
+      - .github/workflows/occupancy.yml
+
+permissions:
+  contents: read
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: ${{ github.event_name != 'push' }}
+
+env:
+  # Julia 1.12.5, the version Manifest.toml was resolved with. The checksum is
+  # julialang's own (bin/checksums/julia-1.12.5.sha256), as the official Docker
+  # image (docker-library/julia a39df01) records it.
+  JULIA_URL: https://julialang-s3.julialang.org/bin/linux/x64/1.12/julia-1.12.5-linux-x86_64.tar.gz
+  JULIA_SHA256: 41b84d727e4e96fbf3ed9e92fa195d773d247b9097f73fad688f8b699758bae7
+
+jobs:
+  disagreement:
+    name: Occupancy disagreement test
+    runs-on: ubuntu-24.04
+    timeout-minutes: 45
+    env:
+      # As in ci.yml: the root .Rprofile would otherwise bootstrap renv.
+      RENV_CONFIG_AUTOLOADER_ENABLED: "FALSE"
+    steps:
+      - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262  # v4.4.0
+        with:
+          persist-credentials: false
+
+      - name: Install Julia
+        run: |
+          source scripts/ci/fetch_pinned.sh
+          fetch_pinned "$JULIA_URL" julia.tar.gz
+          echo "$JULIA_SHA256  julia.tar.gz" | sha256sum -c -
+          sudo mkdir -p /opt/julia
+          sudo tar xzf julia.tar.gz -C /opt/julia --strip-components=1
+          rm julia.tar.gz
+          echo /opt/julia/bin >> "$GITHUB_PATH"
+
+      # RCall builds against R. The occupancy test uses no R package.
+      - name: Install R
+        run: |
+          sudo apt-get update -qq
+          sudo apt-get install -y --no-install-recommends r-base-core
+
+      - name: Instantiate the project
+        run: julia --project=. -e 'using Pkg; Pkg.instantiate()'
+
+      # The pinned vsearch (config/defaults/tool_versions.yml), refused unless it
+      # hashes to the pinned SHA256, as ci.yml installs it.
+      - name: Install vsearch
+        run: |
+          eval "$(julia --project=. -e '
+            using YAML
+            v = YAML.load_file("config/defaults/tool_versions.yml")["tools"]["vsearch"]
+            a = v["archives"]["linux-x86_64"]
+            println("VSEARCH_VERSION=", v["version"]); println("VSEARCH_URL=", a["url"]); println("VSEARCH_SHA256=", a["sha256"])')"
+          source scripts/ci/fetch_pinned.sh
+          fetch_pinned "$VSEARCH_URL" vsearch.tar.gz
+          echo "$VSEARCH_SHA256  vsearch.tar.gz" | sha256sum -c -
+          tar xzf vsearch.tar.gz --warning=no-unknown-keyword
+          sudo mv "vsearch-$VSEARCH_VERSION-linux-x86_64/bin/vsearch" /usr/local/bin/vsearch
+          rm -rf vsearch.tar.gz "vsearch-$VSEARCH_VERSION-linux-x86_64"
+          vsearch --version
+
+      - name: Three orders of the vsearch stage
+        run: julia --project=. -t 2 test/occupancy_disagreement_test.jl
+
+  typed-peak:
+    name: Occupancy typed peak
+    runs-on: ubuntu-24.04
+    # The Agda 2.6.4.3 Debian trixie packages, in a digest-pinned image, as the
+    # upstream proof job uses. The siblings need no standard library.
+    container: debian:trixie-20250929-slim@sha256:1caf1c703c8f7e15dcf2e7769b35000c764e6f50e4d7401c355fb0248f3ddfdb
+    timeout-minutes: 20
+    env:
+      DEBIAN_FRONTEND: noninteractive
+    steps:
+      # git before checkout, so the checkout is a repository and the siblings can be fetched.
+      - name: Install git, curl and Agda
+        run: |
+          apt-get update -qq
+          apt-get install -y --no-install-recommends ca-certificates curl git agda-bin=2.6.4.3-1+b2
+          agda --version | grep -qx 'Agda version 2.6.4.3'
+
+      - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262  # v4.4.0
+        with:
+          persist-credentials: false   # the siblings are public; nothing here pushes
+
+      # The Session IR stepper is Julia (standard library only).
+      - name: Install Julia
+        shell: bash
+        run: |
+          source scripts/ci/fetch_pinned.sh
+          fetch_pinned "$JULIA_URL" julia.tar.gz
+          echo "$JULIA_SHA256  julia.tar.gz" | sha256sum -c -
+          mkdir -p /opt/julia
+          tar xzf julia.tar.gz -C /opt/julia --strip-components=1
+          rm julia.tar.gz
+          echo /opt/julia/bin >> "$GITHUB_PATH"
+
+      - name: Counted bytes against typed peak
+        shell: bash
+        run: bash scripts/check-occupancy.sh

.gitignore

@@ -250,6 +250,9 @@ vignettes/*.pdf
 ## Documentation kept local except published release notes
 docs/*
 !docs/release-notes/
+# and the dated occupancy reading (MMW-01), whose table the gate checks
+!docs/occupancy-2026-10.adoc
+!docs/occupancy/
 
 # translation temp files
 
@@ -332,3 +335,7 @@ LocalPreferences.toml
 
 # Development server log (dev/dev.sh)
 dev/server.log
+
+# Proof siblings fetched by scripts/fetch-siblings.sh, and Agda interface files
+/_build/
+*.agdai

config/defaults/pipeline.yml

@@ -354,3 +354,18 @@ analysis:
     # Fraction of samples, 0 to 1, in which a taxon must have reads to be
     # tested. Taxa below it are listed as filtered, without a p-value.
     min_prevalence: 0.0
+
+## Occupancy probe (MMW-01)
+# Measures each attested stage's memory: Julia's allocation total, and the
+# sampled resident memory of the tools it runs as child processes (Linux /proc).
+# Recorded under the stage's `occupancy` key in attestation.yml. See the
+# header of src/core/memory_probe.jl.
+#
+# Off unless set, and deliberately left commented out here: the run config is
+# embedded in attestation.yml, so a default key would change every run's record
+# even with the probe off. Set it by editing a pipeline.yml (the config editor
+# only offers keys that have a factory default).
+# occupancy_probe:
+#   enabled: true
+#   # Sampling interval in milliseconds (at least 1).
+#   interval_ms: 10

docs/occupancy-2026-10.adoc

@@ -0,0 +1,125 @@
+// SPDX-License-Identifier: AGPL-3.0-only
+// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+= Occupancy of the vsearch stage
+:revdate: 2026-10-14
+
+The vsearch stage runs two independent searches, ASV and OTU. The full
+pipeline spawns them together; a single-stage re-run runs them one after the
+other. The high-water-mark (HWM) algebra of occupancy-types predicts that the
+stage's cost is the same in every order but its memory peak is not: serially
+the peak is the larger search's, concurrently it can be their sum
+(choreographic-types A-2 and A-3). This page records one measurement of that,
+on 2026-10-14, and checks it against the typed reading.
+
+== What was measured
+
+`MemoryProbe` (`src/core/memory_probe.jl`), off unless a pipeline.yml sets
+`occupancy_probe.enabled: true`, records for each attested stage:
+
+* `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`);
+* `child_peak_rss_kib`: the largest sum of the stage's children's VmRSS at
+  one sampling instant (the stage's occupancy).
+
+The run: `test/occupancy_disagreement_test.jl`, which runs the same two searches
+in three orders under the probe, on a fixture it generates: 1000 reference
+sequences of 400 bp, 300 ASV and 150 OTU queries. Linux 6.18 with 4 CPUs,
+Julia 1.12.5 with 2 threads, vsearch 2.30.5 with `--threads 1`. Sampling
+interval 10 ms.
+
+== Results
+
+[cols="2,1,1,1,1,1,1",options="header"]
+|===
+| Order | ASV peak (KiB) | OTU peak (KiB) | Stage peak, measured (KiB) | Counted bytes, Session IR | Typed peak, HWM | Julia allocation (bytes)
+| ASV then OTU | 9204 | 9180 | 9204 | 9204 | 9204 | 978432
+| OTU then ASV | 9152 | 9192 | 9192 | 9192 | 9192 | 978720
+| Concurrent   | 9176 | 9204 | 18380 | 18380 | 18380 | 978816
+|===
+
+* *Cost commutes.* The allocation totals agree to 0.04%. The test asserts
+  agreement within 1%; a planted extra search in one order breaks it (spread
+  25%).
+* *Each search's peak is the same in every order*, to within 0.6%
+  (9152-9204 KiB). Each search's VmHWM equals its sampled peak, so the
+  sampling caught the peaks.
+* *The stage peak is not the same.* Serially it is the larger search's
+  (9192-9204 KiB); concurrently it is 18380 KiB, twice that. This is the A-3
+  order dependence, and nothing in the stage's outputs shows it: the hits are
+  byte-identical in all three orders. The prediction would have been falsified
+  had the concurrent peak matched the serial one; it did not.
+* *Counted bytes equal the typed peak*, in all three orders. The counted bytes
+  come from occupancy-types' Session IR stepper running
+  `docs/occupancy/vsearch-*.sir`, one buffer per search. The typed peak is
+  computed, by `refl`, from occupancy-types' `Timeline` over resource-algebra's
+  HWM grade (`docs/occupancy/TypedPeak.agda`). A search alone exits holding
+  nothing (drift 0); in the concurrent order the first is still resident
+  when the second starts (drift = peak). The sequence law
+  `max (peak a) (drift a + peak b)` then gives the larger peak serially and the
+  sum concurrently.
+* *The measured stage peak also equals the typed peak* here. For the concurrent
+  order the typed peak is the interleaving in which both are resident at once;
+  a measurement could come in lower if the two searches' peaks did not
+  coincide. Here they did: each search's memory plateaus once its database is
+  loaded.
+
+== Status
+
+[cols="1,3,1,2",options="header"]
+|===
+| ID | Claim | Status | Artefact
+| 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`)
+| 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
+|===
+
+== Limits
+
+* *Sampled.* A per-task peak is the largest VmRSS seen at 10 ms intervals. VmHWM
+  is exact up to the last sample, but growth after it is not seen. A child that
+  lives for less than one interval may not be sampled at all (`samples: 0`).
+* *Child memory only.* The children are counted; the Julia process is not. Its
+  `julia_live_bytes_delta` is recorded, but without a forced collection it
+  reflects when the GC last ran, not what the stage kept.
+* *Allocation is process-wide.* While the study loop runs several runs'
+  pipelines at once, a stage's `julia_allocated_bytes` includes the others'
+  allocations too. The child figures are per stage, since each stage samples
+  only the children it started.
+* *Linux only*, since it reads /proc. For a stage offloaded with `remote:`,
+  the local child is an ssh client, so its memory says nothing about the work.
+* *One thread for vsearch.* With several threads, vsearch writes its hits in
+  whatever order the threads finish. `_sort_hits_by_query!` then does a
+  different amount of work, because its sort key splits each line on every
+  comparison. That moved the stage's allocation total by up to 12% between
+  repeats of the same order. So in production the cost is order-independent
+  only up to that noise; precomputing the sort key would remove it. This PR
+  does not change it.
+* *One host, one day.* CI runs the same test on every push and logs its own
+  numbers; they are not compared with these.
+
+== Reproducing
+
+----
+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
+----
+
+`scripts/fetch-siblings.sh` fetches the siblings at their pins into
+`_build/dependencies`: occupancy-types `af95728` and resource-algebra
+`cf9235c`.
+
+== As the proofs progress
+
+* *Per-buffer (n-ary) occupancy* in occupancy-types: each search is already one
+  buffer in the Session IR texts, so the typed peak could then be read per
+  search.
+* *Signed drift*: frees could be graded as negative drift, so the Julia side's
+  collections (the pipeline's `GC.gc(false)` hints) become modelled
+  reclamation rather than unmodelled noise.
+* *choreographic-types' operational `step` as a function*: the three orders
+  become three traces of one typed protocol. The frontier certificate its
+  two-thread application note describes could then be displayed in the WebUI.

docs/occupancy/TypedPeak.agda

@@ -0,0 +1,45 @@
+{-# 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 typed peak, computed (TESTED, by refl) with
+-- occupancy-types' Timeline over resource-algebra's HWM grade, both consumed
+-- by pin through scripts/fetch-siblings.sh:
+--   occupancy-types  af957280075699c659de0abd9a3b0defade77309
+--   resource-algebra cf9235c532712a783a404c359a1055f40134794a
+-- Nothing here re-declares their definitions.
+--
+-- Each search is one interaction graded by its measured peak, in KiB, from the
+-- 2026-10-14 run in docs/occupancy-2026-10.adoc. A search's process exits
+-- holding nothing, so run alone its drift is 0. Run concurrently, the first is
+-- still resident when the second starts, so that is graded with drift = peak.
+-- That is the interleaving the measurement observed (both resident at once).
+-- The algebra's sequence law, max (peak a) (drift a + peak b), then gives:
+-- serial = the larger peak; concurrent = the sum.
+module TypedPeak where
+
+open import ResourceAlgebra.Prelude
+open import ResourceAlgebra.Instances.HWM
+
+import OccupancyTypes.Timeline
+module TH = OccupancyTypes.Timeline HWM
+
+-- A search whose process has exited before the next one starts.
+exits : Nat → Grade
+exits p = hwm p 0 z≤n
+
+-- A search still resident when the next one starts.
+resident : Nat → Grade
+resident p = hwm p p (≤-refl p)
+
+-- ASV 9204 then OTU 9180.
+asv-then-otu : peak (TH.grade (exits 9204 TH.∷ exits 9180 TH.∷ TH.[])) ≡ 9204
+asv-then-otu = refl
+
+-- OTU 9192 then ASV 9152.
+otu-then-asv : peak (TH.grade (exits 9192 TH.∷ exits 9152 TH.∷ TH.[])) ≡ 9192
+otu-then-asv = refl
+
+-- ASV 9176 and OTU 9204 together.
+concurrent : peak (TH.grade (resident 9176 TH.∷ exits 9204 TH.∷ TH.[])) ≡ 18380
+concurrent = refl

docs/occupancy/reject/ConcurrentIsSerial.agda

@@ -0,0 +1,14 @@
+{-# 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: the claim that running the two searches concurrently leaves
+-- the peak where a serial run puts it (the larger of the two).
+module ConcurrentIsSerial where
+
+open import ResourceAlgebra.Prelude
+open import ResourceAlgebra.Instances.HWM
+open import TypedPeak
+
+wrong : peak (TH.grade (resident 9176 TH.∷ exits 9204 TH.∷ TH.[])) ≡ 9204
+wrong = refl

docs/occupancy/reject/SerialIsCost.agda

@@ -0,0 +1,14 @@
+{-# 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 a serial run's peak as the sum of the two peaks,
+-- i.e. occupancy as cost (occupancy-types R-6).
+module SerialIsCost where
+
+open import ResourceAlgebra.Prelude
+open import ResourceAlgebra.Instances.HWM
+open import TypedPeak
+
+wrong : peak (TH.grade (exits 9204 TH.∷ exits 9180 TH.∷ TH.[])) ≡ 18384
+wrong = refl