Measurement + ResourceContract: values carry their provenance, limits carry evidence they refuse

[mdheller]

Two schemas, shipped together because the second $refs the first — a stacked PR would break the child on squash-merge.

Both come from turning today's macOS-forensics lens back on our own spec, and every defect cited below is one of mine.

---

1. Measurement.json — extraction, not invention

LawfulDispatchReceipt.json already carried source: [measured, declared] on law and evidence, with an allOf forcing evidenceTier: T2. Correct, and inlined in exactly one of 302 schemas — while cross-file $ref is already the house pattern (DataRef 10×, ContentRef 7×, Link 6×). Divergence between an inlined definition and its copies is how extension, Extension, DiagnosticExtension, diagnosticextension and diagnostic came to name one macOS extension point.

Three defects it makes unrepresentable

A census that dropped exactly the members it existed to count. 627 macOS sandbox containers; find -maxdepth 2 -name … 2>/dev/null returned 617. The ten lost — Safari, Safari.WebApp, mail, Notes, MobileSMS, news, stocks, Home, VoiceMemos, archiveutility — were precisely the TCC-protected ones. The instrument printed ten Operation not permitted lines; the redirect swallowed them. The drop rate correlates with sensitivity, so silent omission is worse than a wrong number. As a Measurement, that walk must declare unobserved: 10 and is ineligible by shape.

A fabricated legend. The /var/folders/<shard>/<hash>/{0,C,T} mapping was printed as derived — in the same change that criticised Apple for shipping that tree without one. The three confstr lookups that would have confirmed it had all failed. That is source: "assumed".

Skimmed coverage caveats. Both resource reports carried Duration Sampled shorter than Duration plus samples lost, in headers easy to pass over. Here they are sampling and unobserved — required, not footnotes.

gateEligible is a ceiling

true only when source is measured and unobserved is 0; false always available. A producer may downgrade its own reading — it may have come to distrust an instrument — but never upgrade one. Same asymmetry as the truth-product being a MEET.

Deliberately not named coverage: GuardrailEvalReport.coverage already means declared-vs-enforced clause counts, and one word with two meanings is the failure this prevents.

INVARIANT 5 reads LawfulDispatchReceipt at validation time and asserts its enum stays a subset. Drift is a failing test, not a silent fork.

36 checks, incl. 16 exhaustive source × unobserved × claimed combinations as documents, and a mutation test proving the allOf is what rejects.

---

2. ResourceContract.json — Action taken: none made unwritable

	limit	actual	action
Virtualization.VirtualMachine	50% CPU / 180s	66% / 137s	none
nsurlsessiond	2147.48 MB / 86400s	2147.50 MB	none

Declared, measured, exceeded, nothing happened. A threshold that only observes is not a limit, and carrying one is worse than carrying none, because its existence is read as a guarantee.

invariant	rule
1	enforcement != observe ⇒ negativeControl required and resolvable
2	enforcement == observe ⇒ observeOnlyReason required
3	scope == process ⇒ scopeRationale required
4	firedCount > 0 ⇒ lastFiredAt required
5	negativeControl resolves (validator — uri-reference is syntax only)
6	observedPeak must be a gate-eligible Measurement
7	the $ref target exists

Why scope earns its place. In the nsurlsessiond report the flagged process was 141 of 8,357 samples (2%), while node 24%, the app 17%, the VM 15% and git 9% — 66% between them, all charged to one resource coalition — tripped nothing, each staying under its own per-process threshold. Per-process limits are defeated by fan-out, and fan-out is what a build runner does by design. macOS had the aggregate accounting printed in the header and enforced per-process anyway.

INVARIANT 6 is what makes Measurement load-bearing rather than decorative: a limit calibrated by an unmeasured peak is not calibrated.

40 checks. The shipped negativeControl procedure states plainly that it has not yet been executed against a runner — an unrun procedure is honest; a fabricated observedPeak would be the paper control this schema exists to refuse.

Deliberately not checked

Whether observedPeak.value exceeds limit.value. Measurement has no unit on value — sampling.unit describes what was counted ('hourly samples'), not what the value measures ('bytes'). Comparing numbers whose units cannot be verified is the error class closed elsewhere today, so the check is omitted rather than bodged. Real fix is a unit field on Measurement — recorded as follow-up, not smuggled in.

---

Three errors caught during construction, all by artifact rather than exit code

the exhaustive sweep failed on first run	the validator asserted equality on gateEligible instead of a bound. The schema was right.
make validate printed OK: validate without running the new validator	the Makefile edit landed on the .PHONY line, not the validate: dependency line
—	fixed, and both wirings now carry their own negative control: break the example ⇒ rc=2; restore ⇒ rc=0

Branched off main, independent of #225.

[Copilot]

Pull request overview

Introduces a new normative Measurement schema (plus example) to encode how a value was obtained and to make gateEligible derived by contract, with a dedicated validator wired into make validate to enforce invariants and prevent drift with LawfulDispatchReceipt.

Changes:

• Adds schemas/Measurement.json defining source, instrument, sampling, unobserved, and the derived/ceiling semantics of gateEligible via JSON Schema invariants.
• Adds tools/validate_measurement.py and a shipped example document, with exhaustive/mutation-style checks and an anti-drift guard against LawfulDispatchReceipt.
• Wires the new validator into Makefile’s validate target.

Reviewed changes

Copilot reviewed 4 out of 4 changed files in this pull request and generated 3 comments.

File	Description
tools/validate_measurement.py	New validator enforcing Measurement invariants (including exhaustive combinations and mutation testing).
schemas/Measurement.json	New canonical Measurement schema defining eligibility semantics and required measurement metadata.
Makefile	Adds validate-measurement target and hooks it into make validate.
examples/measurement.example.json	Adds a concrete example Measurement document demonstrating unobserved/ineligibility shape.