Skip to content

Commit 9a18b77

Browse files
feat(proofs): unify Agda suite, audit gates, and run-notices catalogue (#81)
## Summary This PR unifies the full formal-verification Agda proof suite, resolves module and audit collisions across the estate, and imports the memory/numerics audit and run-notices catalogue. ### Changes Included 1. **Unify Agda Formal Verification Suite ()**: - Imports and type-checks all 22 modules across the codebase in a single gate entry: - **Numeric Core (Issue #1)**: `Prelude`, `Proportions`, `ExactCounts`, `PermutationTest`, `BenjaminiHochberg`, `DecimalRounding` - **Composition (Issue #21)**: `Composition.Tree`, `Composition.Node`, `Composition.Sum` - **ILR Bases (Issue #20)**: `ILR.SBP`, `ILR.Contrast`, `ILR.Kernel`, `ILR.Invariance`, `ILR.Orthonormal`, `ILR.Comb`, `ILR.Integer` - **Evidence Mode (Issue #7)**: `Evidence.Prelude`, `Evidence.Residual`, `Evidence.Echo`, `Evidence.Warrant`, `Evidence.Signed`, `Evidence.Decision` - Uses non-polluting namespace imports to avoid symbol collisions (e.g. `Sign`). 2. **Gate Machinery & Self-Test Harmonization**: - `proofs/tests/axiom-audit.sh`: Audits all 23 modules under `MetaManifold/`, verifying `--safe`, zero postulates, no FFI/holes, and 100% reachability from `MetaManifold.All`. - `proofs/tests/gate-selftest.sh`: Verified 10/10 mutation and control checks reject deliberate breakages and accept the pristine tree. 3. **Memory, Numerics, and Backend Audit**: - Adds `docs/audit/2026-09-26-memory-numerics-warning-audit.md` (21-finding read-and-trace audit). - Adds `docs/notices/README.md` and `docs/notices/catalogue.md` (60-item run-notice taxonomy and contracts). - Updates `.gitignore` to track `docs/notices/`. 4. **Hygiene & Governance**: - SPDX licence headers added across all new documentation (`docs/statistics/formal-verification.md`, `proofs/HANDOFF.md`, `proofs/PROOF-STATUS.md`). - Clean formatting (`scripts/check-format.sh` -> OK on 502 files). ### Verification | Check | Result | |---|---| | `proofs/bootstrap.sh` | **OK** (all 23 modules checked cleanly) | | `proofs/tests/axiom-audit.sh` | **OK** (23/23 reachable, clean) | | `proofs/tests/gate-selftest.sh` | **10/10 controls pass** | | `scripts/check-spdx.sh` | **OK** (381 files covered) | | `scripts/check-format.sh` | **OK** (502 files checked) |
2 parents e6726fa + 4341cc3 commit 9a18b77

10 files changed

Lines changed: 1580 additions & 9 deletions

File tree

‎.gitignore‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -276,6 +276,11 @@ docs/*
276276
!docs/formal/**
277277
!docs/triage/
278278
!docs/triage/**
279+
# The run-notice model and its catalogue: the notice ids are a maintained
280+
# contract between the backend, the manifest and the UI, and they are
281+
# drift-tested against src/, so they are repository state, not local notes.
282+
!docs/notices/
283+
!docs/notices/**
279284
# …but the generated PR-#7 stack patches are derived artefacts: regenerate
280285
# with docs/triage/pr7-split/make-stacks.sh instead of committing them.
281286
docs/triage/pr7-split/patches/*.patch

‎docs/audit/2026-09-26-memory-numerics-warning-audit.md‎

Lines changed: 1037 additions & 0 deletions
Large diffs are not rendered by default.

‎docs/notices/README.md‎

Lines changed: 317 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,317 @@
1+
<!--
2+
SPDX-License-Identifier: CC-BY-SA-4.0
3+
-->
4+
5+
# Run Notices — the user-facing notice model
6+
7+
**Status: design, 2026-09-26.** Nothing here is implemented. It is written
8+
before the code, in the style this repository already uses for
9+
`docs/statistics/method-conditions/*`: where this document and the code
10+
disagree, the document is right and the code is the bug.
11+
12+
**Why it exists.** Today every notice the system produces is a `String` pushed
13+
onto a `Vector{String}`. The strings are individually good — often better than
14+
most software manages — but they carry no category, no severity, no stable
15+
identifier and no statement of whether the numbers may be used. Consequences:
16+
17+
- the UI cannot act on them, so `DangerBanner.tsx` re-derives its own four
18+
reasons from the config while `AnalysisConfig.jl:1345-1360` derives a
19+
different list for the backend banner. Two lists, one question, no shared
20+
source — the drift this repository's own comments warn about when a hook and
21+
a CI check re-implement the same rule.
22+
- a run whose estimator did not run can be reported safe
23+
(`docs/audit/2026-09-26-memory-numerics-warning-audit.md` §W1), because
24+
nothing in the notice says "this blocks export".
25+
- a check that is a stub and a check that found nothing look identical
26+
(`has_batch_confounding => false`, §N3).
27+
- the log and the result cannot be correlated: the log has a timestamp and the
28+
manifest has a list, and there is no key between them.
29+
30+
**Non-goals.** This is not an error-handling framework, not a replacement for
31+
exceptions, and not a logging library. Exceptions still mean "we stopped";
32+
`@warn`/`@error` still mean "operator, look at the log". A `RunNotice` means
33+
*"someone reading these results has to know this"*, and it travels **with the
34+
result**, not only with the log.
35+
36+
---
37+
38+
## 1. The six categories
39+
40+
The category is decided by *the question the notice answers*, not by where it
41+
is raised. Getting this wrong is how "we did not check" gets read as "we
42+
checked and found nothing".
43+
44+
| Category | Question it answers | Typical examples |
45+
|---|---|---|
46+
| `technical_resource` | Did the machine have the room, the time, the precision? | allocation churn, peak memory, a benchmark threshold, a check that is **not implemented**, R warnings raised outside the handler |
47+
| `dependency_environment` | Was the toolchain there and reachable? | R absent, `vegan` absent, `MASS` absent, R runtime busy, CI produced no verdict |
48+
| `data_quality` | Is the input table what we think it is? | zero variance, library-size outliers, low prevalence/abundance, all-zero samples or taxa, samples dropped below depth |
49+
| `method_limitation` | Does the chosen method mean what a reader will think it means? | data-derived dendrogram basis, non-isometric balance weights, `rarefy`, an inert configuration parameter, `theta` at a boundary |
50+
| `result_safety` | May these numbers be read as a finding? | estimation `:not_run`, NaN-filled ordination coordinates, healing that rewrote values, SBP p-hacking guard |
51+
| `fatal` | Did we stop? | hard-stop with a DANGER banner, refusal of a refused dispersion method, refusal of an unrooted tree |
52+
53+
Two rules that fall out of the table and are worth stating as invariants:
54+
55+
- **A diagnostic that did not run is `technical_resource`, never
56+
`data_quality`.** Its summary must say it did not run.
57+
- **"Nothing was produced" is `result_safety` (or `fatal`), never silence.** A
58+
run with no statistics is not a safe run.
59+
60+
## 2. Severity
61+
62+
| Severity | Meaning | UI treatment |
63+
|---|---|---|
64+
| `info` | recorded for provenance; nobody needs to act | collapsed, one line |
65+
| `notice` | worth knowing; changes how you read a number | collapsed, one line |
66+
| `warning` | interpretation required before use | expanded, amber |
67+
| `danger` | do not present these numbers as a finding without saying this | expanded, red, banner on every figure |
68+
| `fatal` | nothing was produced | replaces the result view |
69+
70+
**Invariants** (these are the assertions in `test/unit/test_notices.jl`):
71+
72+
1. `result_usable == false` ⟹ `blocks_export == true`.
73+
2. `severity == fatal` ⟹ `result_usable == false` **and** the result object
74+
holds no statistics.
75+
3. `category == fatal` ⟺ `severity == fatal`.
76+
4. `category == technical_resource` ⟹ `result_usable == true`. (The machine
77+
struggling is never a reason to distrust the numbers.)
78+
5. `category == result_safety` ⟹ `blocks_export == true`.
79+
6. Every notice has a non-empty `summary`, `detail` and `id`; `action` may be
80+
empty only when `severity ∈ {info, notice}`.
81+
7. Every `id` emitted anywhere in the codebase appears in
82+
`docs/notices/catalogue.md`, and every `id` in the catalogue is emitted
83+
somewhere. This is the same drift guard `PipelineLog._LOG_REGISTRY` already
84+
enforces for log files (`src/core/log.jl:77-84`, `test/unit/test_log.jl`),
85+
applied to notices.
86+
87+
## 3. The field model
88+
89+
```julia
90+
module Notices
91+
92+
using Dates, OrderedCollections
93+
94+
export RunNotice, NoticeCategory, NoticeSeverity,
95+
TECHNICAL_RESOURCE, DEPENDENCY_ENVIRONMENT, DATA_QUALITY,
96+
METHOD_LIMITATION, RESULT_SAFETY, FATAL_CATEGORY,
97+
emit!, notices, blocks_export?, result_usable?
98+
99+
@enum NoticeCategory technical_resource dependency_environment data_quality
100+
method_limitation result_safety fatal_category
101+
102+
@enum NoticeSeverity info notice warning danger fatal
103+
104+
"""
105+
RunNotice
106+
107+
One thing a reader of these results has to know. See docs/notices/README.md.
108+
`rev` is the catalogue revision of this id's wording, so a stored notice can be
109+
rendered against the catalogue that was current when it was emitted.
110+
"""
111+
struct RunNotice
112+
id :: String # stable, dotted, see §4
113+
category :: NoticeCategory
114+
severity :: NoticeSeverity
115+
summary :: String # ≤ 120 chars, one line, UI
116+
detail :: String # paragraphs, no length limit
117+
action :: String # what to do; "" if nothing
118+
result_usable :: Bool
119+
blocks_export :: Bool
120+
log_ref :: String # see §5
121+
data :: OrderedDict{String,Any} # structured context, JSON-safe
122+
rev :: Int
123+
end
124+
```
125+
126+
The nine fields the brief asks for are `category`, `severity`, `id`, `summary`,
127+
`detail`, `action`, `result_usable`, `blocks_export` and `log_ref`. The two
128+
additions:
129+
130+
- **`data`** — structured context (`bytes`, `taxa`, `threshold`, `count`,
131+
`package`, `waited_seconds`). Without it every consumer has to parse the
132+
`summary` to find the number, and the summary has to be rewritten to change
133+
a threshold. Every notice carries its numbers here, and the summary
134+
interpolates them.
135+
- **`rev`** — the catalogue revision. A manifest written last year has to
136+
render against last year's wording, or a reworded notice silently changes
137+
the meaning of a stored result.
138+
139+
### Serialisation
140+
141+
One shape, three targets (manifest, HTTP response, DOI bundle). JSON:
142+
143+
```json
144+
{
145+
"id": "ilr.dendrogram.data_derived",
146+
"rev": 1,
147+
"category": "method_limitation",
148+
"severity": "warning",
149+
"summary": "The balance dendrogram was built from the same table that is tested.",
150+
"detail": "The variation matrix Var(log(x_i/x_j)) ... no sample metadata, so it cannot see group labels, but it is not independent of the data.",
151+
"action": "Pre-register the dendrogram method, or use a phylogenetic or SBP basis chosen without reference to this table.",
152+
"result_usable": true,
153+
"blocks_export": false,
154+
"banner_required": true,
155+
"log_ref": "run=7c1d… seq=17 origin=src/analysis/ilr_basis.jl:1265",
156+
"data": { "taxa": 1204, "method": "ward", "variation_matrix_bytes": 5798304 }
157+
}
158+
```
159+
160+
`banner_required` is **derived**, not stored: `severity ∈ {danger, fatal} ∨
161+
(category == method_limitation ∧ severity == warning)`. The repository already
162+
promises "Bannered in every figure and DOI bundle" for dangerous
163+
configurations; deriving the flag means the UI and the backend cannot disagree
164+
about which notices get a banner — the failure mode described at the top of
165+
this document.
166+
167+
The Nickel contract belongs beside the other schemas in `config/schemas/`,
168+
following `analysis_config.ncl` and `doi_publication.ncl`.
169+
170+
## 4. Stable identifiers
171+
172+
Rules, so that the set is checkable and grep-able:
173+
174+
```
175+
<area>.<subject>.<condition>
176+
```
177+
178+
- `<area>` is the module that owns the semantics:
179+
`config`, `exec`, `estimation`, `ilr`, `scaling`, `r`, `analysis`, `bench`,
180+
`provenance`, `pipeline`, `ci`.
181+
- `<subject>.<condition>` is lowercase `snake_case`, no digits that encode
182+
values, no free text, no interpolation. `ilr.sbp.p_hacking_guard`, not
183+
`ilr.sbp.3_matrices_tried`.
184+
- An `id` is **immutable**. To change what a notice means, add a new `id` and
185+
retire the old one (retired ids stay in the catalogue with
186+
`status: retired` so old manifests still render).
187+
- Values never live in the `id`; they live in `data`. `exec.heal.nan_inf`
188+
carries `{"nan_count": 3, "inf_count": 0, "epsilon": 1e-6}` — so the
189+
catalogue has one entry, not one per count.
190+
191+
## 5. The technical log reference
192+
193+
`log_ref` answers *"where do I look for the details?"* — the question a
194+
scientist asks after reading the summary. The repository already has the
195+
precedent: `PipelineLog.CMD_MARKER` exists so that
196+
`grep '^\[MetaManifold\] cmd: '` recovers every command a run issued
197+
(`src/core/log.jl:53-59`).
198+
199+
Format:
200+
201+
```
202+
run=<run_id> seq=<n> origin=<file>:<line> [logger=<key>] [log=<relative path>]
203+
```
204+
205+
- `run_id` — a UUID per `prepare_analysis_table`/`run_analysis` pair *and* per
206+
HTTP request that produces a chart. **New:** the server has no correlation
207+
id today.
208+
- `seq` — a per-run counter, so two healings in one run are distinguishable
209+
and the log order is recoverable.
210+
- `origin` — the emission site. Recorded by the emitter, not derived, because
211+
`@__FILE__`/`@__LINE__` at the call site is the only thing that survives a
212+
refactor of the message text.
213+
- `log` — for pipeline stages, the registry-relative path from
214+
`PipelineLog._TOOL_LOG_FILES`, so `grep "$run_id" combined_pipeline.log`
215+
works.
216+
217+
The convention: `grep "$run_id"` in the process log returns every log line the
218+
run produced, in order. That is one `@info`-with-`run_id` change in the emitter
219+
and it makes every notice traceable.
220+
221+
## 6. Emission
222+
223+
Notices are emitted **alongside** the existing free-text warnings, not instead
224+
of them, until every consumer has migrated. Concretely:
225+
226+
```julia
227+
push!(warnings, "Low prevalence/abundance: $(n_low) taxa below min_prevalence=$(mp) — will be filtered")
228+
emit!(sink, RunNotice(
229+
id = "exec.filter.low_prevalence", rev = 1,
230+
category = DATA_QUALITY, severity = :warning,
231+
summary = "$(n_low) of $(n_taxa) taxa are below min_prevalence=$(mp) and were filtered.",
232+
detail = "…",
233+
action = "…",
234+
result_usable = true, blocks_export = false,
235+
log_ref = log_ref(run, origin),
236+
data = OrderedDict("n_filtered" => n_low, "threshold" => mp)))
237+
```
238+
239+
Two rules for the migration:
240+
241+
- **No notice is emitted without its free-text twin, and vice versa**, until
242+
the drift test in §2(7) has been green for one release.
243+
- **Nothing is removed from the manifest.** `diagnostics.warnings` stays;
244+
`diagnostics.notices` is added. A manifest that already exists must still
245+
render.
246+
247+
Emission points, in the order they are worth doing:
248+
249+
| where | what becomes notices |
250+
|---|---|
251+
| `Execution.run_analysis` | `estimation.not_run`, and the `is_dangerous` fix (§W1) |
252+
| `Execution.self_diagnostics` | all eight `warnings` strings, plus `exec.batch_confounding.not_implemented` |
253+
| `Execution.safe_self_healing` / the healing block | `exec.heal.*`, with positions (§N2) |
254+
| `ILRBasis.ilr_transform` | the four `warnings` and the `dangers` |
255+
| `Scaling.*_factors` | the five scaling warnings |
256+
| `Analysis._ensure_r`, `run_nmds`, `run_permanova` | `r.vegan_unavailable`, `r.runtime_busy`, `ord.*.not_run` |
257+
| `Estimation._not_run` / `_assemble` | `estimation.not_run`, `estimation.feature_failed` |
258+
| HTTP routes | attach the response's notice list to the JSON body, so a degraded chart says so in the payload and not only in the log |
259+
| `bench/ilr_bases/*` | `bench.allocation_churn`, `bench.peak_rss_growth` with the phase in `data` |
260+
261+
## 7. What the UI does with them
262+
263+
The contract is small, and it is the whole point of the model:
264+
265+
1. Group by `category`, order by `severity` descending.
266+
2. Render `summary` in the list; `detail` and `action` on expand; `log_ref` as
267+
a copyable string.
268+
3. **If any notice has `blocks_export`, disable the export/DOI action and say
269+
which notice blocked it.** Today nothing can ask that question.
270+
4. **If any notice has `result_usable == false`, the numbers are not rendered
271+
as a results table.** They are rendered as a statement about the run.
272+
5. Every notice with `banner_required` is rendered on every figure, as
273+
`DangerBanner` already promises for dangerous configurations.
274+
6. `DangerBanner.tsx` stops deriving its own list from the config and renders
275+
the `config.*` notices the backend emitted — one source, both surfaces.
276+
277+
## 8. What this model deliberately does not do
278+
279+
- **It does not decide policy at emission time.** The category and severity are
280+
constants in the catalogue; the emitter supplies the data. Otherwise the same
281+
condition gets classified differently in two places, which is the drift this
282+
is meant to remove.
283+
- **It does not suppress anything.** The brief's "do not suppress warnings
284+
globally" is satisfied by construction: notices are additive, the free text
285+
stays, and `severity = info` means "recorded", not "hidden". The audit found
286+
no global suppression today and this model adds none.
287+
- **It does not replace the DANGER banner.** The banner is the human-readable
288+
rendering of the `danger` notices plus the config's own acknowledgements. One
289+
list, rendered two ways.
290+
- **It does not carry results.** A notice describes a run, not a feature.
291+
Per-feature statuses stay where they are (`status = "failed"` with a `note`
292+
per row in `Estimation`), and `estimation.feature_failed` is the *aggregate*
293+
notice that points at them.
294+
295+
## 9. Open questions for the owner
296+
297+
1. **Does `result_usable == false` block export, or require an
298+
acknowledgement?** The model currently blocks. The repository already has
299+
`DANGER_ACK_TOKEN` for *configuration* risk; extending the same mechanism to
300+
*result* risk is a decision, not a default.
301+
2. **Are `technical_resource` notices in the manifest, or only in the log?**
302+
They are provenance-relevant (a run that peaked at 4 GiB is a fact about the
303+
run) but they are not science. The catalogue marks each with
304+
`manifest: yes/no`.
305+
3. **Who owns the `r.*` notices' wording** — MetaManifold, or the standalone
306+
runtime package that would eventually own the R hand-off? Recommendation:
307+
MetaManifold, because "vegan is not installed" is a sentence about this
308+
product's results.
309+
310+
---
311+
312+
## Files
313+
314+
| File | Contents |
315+
|---|---|
316+
| `docs/notices/README.md` | this document — the model |
317+
| `docs/notices/catalogue.md` | every notice id, with category, severity, wording and the audit finding it came from |

0 commit comments

Comments
 (0)