100%

AIMS proof-obligation catalogue

Goal

AIMS proof-obligation 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
  • missions.md §AIMS, §Compiler

Grounding constraint — open-bug obligations route here, not to foreclosure

Two type-validity classes the intel recon (../foreclosed-typesystem--s-54852491 + its content/intel/ dossier) flagged are runtime obligations with OPEN realization bugs, NOT type-system foreclosures — they belong in this section:

  • alignment — BUG-05-010 (niche payload under-alignment). Disposition aims-obligation; the open bug IS the current (red) pin until fixed.
  • invalid-tag / uninitialized-read — BUG-04-130 (tag-blind RC walk reads uninitialized garbage). Same.

Both overlap the ACTIVE plans/aims-burden-tracking/ migration surface (arc.md §STOP): a default-path (predicate-stack) PASS is NEVER a “fixed” verdict and a default-path FAIL is NEVER an independent regression. The ONLY valid RC/AOT verdict surface is the gated burden probe ORI_DISABLE_PREDICATE_STACK_RC=1 ORI_VERIFY_ARC=1 ORI_VERIFY_EACH=1. Do NOT independently fix these RC clusters here — the matrix CITES the bug + the aims-burden floor; the fix routes to that plan.

Work Items

  • Map RC-balance / no-double-free / no-UAF to the AIMS Lean theorems CH-1 (lattice == burden bridge) + CH-2 (single elimination) + RL-comp (lowered burden ops preserve RC net balance) in the aims-proof corpus; record the theorem refs in the matrix. (CH-4 is AimsStateMap immutability, not lattice==burden — corrected.)
  • Tie each AIMS-obligation class to a runtime verification surface — the gated burden probe (ORI_DISABLE_PREDICATE_STACK_RC=1 ORI_VERIFY_ARC=1 ORI_VERIFY_EACH=1, the SOLE RC/AOT verdict per arc.md §STOP), the AOT leak tests under ORI_CHECK_LEAKS=1, valgrind aims_*.ori. Each obligation cites a passing verification; alignment (BUG-05-010) + invalid-tag/uninit-read (BUG-04-130) cite their open bug as the current red pin, routed to plans/aims-burden-tracking, never fixed inline.

Fresh intel (regenerated)

{ “schema_version”: 1, “target”: { “kind”: “plan-section”, “ref”: “ub-safety-threat-model/s-645189eb” }, “generated_at”: “2026-06-25T19:26:28.129463+00:00”, “graph_state”: { “head_sha”: “e6daa0f3”, “last_code_import_at”: “2026-06-25T19:22:57.178Z”, “embedding_stale”: true, “insights_stale”: false, “cpg_stale”: false }, “surfaces”: {}, “summary”: “intel-package[plan-section:ub-safety-threat-model/s-645189eb] 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: aims-obligations—s-645189eb.intel.json)