Walking skeleton: disposition taxonomy + coverage-matrix schema + seed checker
Goal
Walking skeleton: disposition taxonomy + coverage-matrix schema + seed checker. Facet of the UB-disposition model: every miri-enumerated UB class in this section’s scope is dispositioned and (where claimed foreclosed) pinned.
Implementation Sketch
Populate the coverage matrix rows owned by this section; ground every disposition in actual Ori spec/source (cite file:line or spec clause); add the pin / verification surface the disposition claims.
Spec References
- spec Clause 4.5 (04-conformance.md:32) — no silent UB
- missions.md §AIMS, §Compiler
Work Items
- Define the disposition taxonomy enum (foreclosed-typesystem | aims-obligation | data-race-foreclosed | ffi-unsafe-boundary | gap) and the coverage-matrix schema (one row per miri UB class: class id, miri source cite, disposition, Ori mechanism/spec clause, pin ref).
- Author a minimal end-to-end coverage-checker over >=3 seed classes (one per disposition bucket) that reads the matrix and emits a row-per-class report; prove it green on the seed set.
Fresh intel (regenerated)
{ “schema_version”: 1, “target”: { “kind”: “plan-section”, “ref”: “ub-safety-threat-model/s-b98a2749” }, “generated_at”: “2026-06-25T18:26:58.305729+00:00”, “graph_state”: { “head_sha”: “b74d6b9a”, “last_code_import_at”: “2026-06-25T18:23:27.446Z”, “embedding_stale”: false, “insights_stale”: false, “cpg_stale”: false }, “surfaces”: {}, “summary”: “intel-package[plan-section:ub-safety-threat-model/s-b98a2749] agent-authored dossier”, “degraded”: false, “dossier”: { “objective_symbols”: [], “tiers”: {}, “agent_authored”: true, “difficulty”: { “class”: “routine”, “research_online”: false, “research_mode”: “auto”, “signals”: [], “plan_dir”: “/home/eric/projects/ori_lang/plans/ub-safety-threat-model” } } }
(full dossier: walking-skeleton—s-b98a2749.intel.json)