Session 2026-09-27: R0-B pieces 1-2 (Session IR, 14/14 green) + R1 stackcert scaffold + type-family coherence links

[arena-ai-coding-agent]

What

The 2026-09-27 session per ULTRAPLAN, in four blocks:

1. R0-B Piece 1 — Session IR spec + executable checker. 10-construct typed IR (Var,Let,Lam,App,Pair,Fst,Snd,Inl,Inr,Case,Close), 5 unit rules (var/let/case/close/epoch), R0-B unit, integer epoch stamps (step §4.3.1), store/step semantics with the epoch rule, resource counting + 3 demo lemmas, plus a stdlib-only Python package (src/session_ir) checked against examples/session_ir/manifest.json — 14/14 fixtures green, incl. 3 expected-rejection controls and a regression for the ordered-unpack fingerprint.
2. R0-B Piece 2 — New Exclusion Boundary §6. Explicit no-imports list (unknown families are not dependencies); open = session-only, never heap resources.
3. R1 — Stackcert scaffold (pinned, complete-by-construction). StackcertCore.lean (max-plus certificates, forward/reverse conjunctive (height,delta) passing, cert_sound — UNVERIFIED, #print axioms slot deliberately unfilled until lake env runs), OCaml stack-frame parsers with 4 expected-rejection controls (negative frame size, differing pushed-regs, negative delta, truncated header), gcc .su/.ci fixtures (no .o), Zephyr fixture request pinned in the retraction ledger. Kill question answered by CONJECTURE in src/stackcert/README.adoc.
4. Docs & coherence. docs/EXPLAINME.adoc claims map C1–C6 (honest TESTED/UNVERIFIED/CONJECTURE labels), session report, ULTRAPLAN §9 decision log, kill-test block audit gate (--audited), and the type-family map cross-links (last commit).

Honesty labels (as of this PR)

Claim	Status
Session IR checker, 14/14 fixtures	TESTED (just check-ir)
Kill-test block audit vs doc claims	TESTED (gate-green)
Occ spike / cert_sound / stackcert parser	UNVERIFIED — no Idris2/Lean toolchain; fixture requests pinned; check FAILS loudly by design, check --runnable-only is green
Kill questions answers	CONJECTURE, labelled as such

Commits are unsigned (no signing key in the sandbox); push was hook-validated.

Type-family coherence (context)

Tracked by nextgen-typing#118. Per-repo coordination issues filed: kategoria#76, typell#62, absolute-zero#175, januskey#137, secret-types#2. This PR's last commit is this repo's reciprocal half: README family-map section, glossary deferral to the estate shared glossary, ULTRAPLAN decision-log entries (registration + naming errata: tropical-resource-typing = tropical-types; katagoria → ideas-to-alphas ≠ kategoria).

How to check

just check-ir          # 14/14 + audit + shape gates — green
just check             # full gate — FAILS loudly at idris2/lean until fixtures land (by design)

[coderabbitai]

Important

Review skipped

Bot user detected.

To trigger a single review, invoke the @coderabbitai review command.

⚙️ Run configuration

Configuration used: Organization UI

Review profile: ASSERTIVE

Plan: Advanced

Run ID: 749d1e5d-e90d-4246-8eaa-fb8416908496

You can disable this status message by setting the reviews.review_status to false in the CodeRabbit configuration file.

Use the checkbox below for a quick retry:

• 🔍 Trigger review

---

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands.}