100%

Foreclosed-by-type-system catalogue

Goal

Foreclosed-by-type-system catalogue. 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
  • spec Clause 23.5 — Runtime panic catalogue (the artifact this disposition mirrors)
  • missions.md §AIMS, §Compiler

Grounding constraint — provisional foreclosure, verify per-class against the realization

A class belongs in THIS section ONLY when the foreclosure holds at runtime, not merely in the surface grammar/type system. The intel recon (content/intel/foreclosed-typesystem--s-54852491.intel.md) flags two classes whose realization is currently RED — they disposition to aims-obligation (runtime-pinned, owned by aims-obligations section), NOT foreclosed:

  • alignment — open BUG-05-010 (niche payload under-alignment). Do NOT pin “foreclosed-clean”; route to aims-obligation with the bug as the open pin.
  • invalid-tag / uninitialized-read — open BUG-04-130 (tag-blind RC walk reads uninitialized garbage). Same — aims-obligation, not foreclosed.

definite_assignment returns 0 analysis symbols: Ori has no uninitialized-binding FORM (foreclosed by grammar, no analysis symbol to cite) — disposition foreclosed-by-grammar, pin = the parse/typeck rejection. The compiler’s own Rust ArithOp nodes describe Rust arithmetic hygiene, NOT Ori-program semantics — do not mis-scope them into a user-facing UB row.

Work Items

  • Catalogue the memory-safety + bounds classes (UAF, OOB, dangling, unterminated-cstring, write-to-readonly) -> Ori invariant (ARC + no raw deref) + spec clause; add a compile_fail/panic pin per class.
  • Catalogue arithmetic (div-by-zero, overflow, shift) -> panic semantics (spec 17.2/17.3) with pins. Alignment is NOT catalogued here — it is an aims-obligation (open BUG-05-010); uninit/dead-data is foreclosed-by-grammar (no binding form) with the parse/typeck rejection as the pin.
  • Catalogue the genuinely type-system-foreclosed validity invariants (invalid bool/char/str, uninhabited-variant via Never, invalid fn/vtable ptr, ABI mismatch) -> ori_types guarantees + #compile_fail pins. Invalid tag/discriminant + uninitialized-variant-read are NOT foreclosed here — they route to aims-obligation (open BUG-04-130).

Fresh intel (regenerated)

{ “schema_version”: 1, “target”: { “kind”: “plan-section”, “ref”: “ub-safety-threat-model/s-54852491” }, “generated_at”: “2026-06-25T16:35:59.027213+00:00”, “graph_state”: { “head_sha”: “b74d6b9a”, “last_code_import_at”: “2026-06-25T16:33:44.846Z”, “embedding_stale”: false, “insights_stale”: false, “cpg_stale”: false }, “surfaces”: {}, “summary”: “intel-package[plan-section:ub-safety-threat-model/s-54852491] 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: foreclosed-typesystem—s-54852491.intel.json)