Coverage checker + completeness gate

Goal

Coverage checker + completeness gate. 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

• Build the production coverage-checker (compiler_repo/scripts/ub-coverage-check.py) that asserts: every miri UB class has a disposition row AND every foreclosed/aims/data-race class cites a passing pin AND every gap cites a hardening anchor.
• Land the maintainer-facing threat-model artifact (the coverage matrix doc) and wire the checker as a regression gate; the checker reads green only when the matrix is complete.

Fresh intel (regenerated)

{ “schema_version”: 1, “target”: { “kind”: “plan-section”, “ref”: “ub-safety-threat-model/s-c998531f” }, “generated_at”: “2026-06-25T20:43:15.947232+00:00”, “graph_state”: { “head_sha”: “33100f3a”, “last_code_import_at”: “2026-06-25T20:39:26.278Z”, “embedding_stale”: true, “insights_stale”: false, “cpg_stale”: false }, “surfaces”: {}, “summary”: “intel-package[plan-section:ub-safety-threat-model/s-c998531f] 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: coverage-checker-gate—s-c998531f.intel.json)