Section 09: ARC Header Compression

Context: The current runtime (ori_rt) unconditionally uses i64 for the reference count, with MAX_REFCOUNT = i64::MAX. The ARC pipeline already computes borrow/ownership information, so specializing RC count handling is a plausible next step. This section now explicitly commits to the smaller-header path: changing only the width of strong_count is insufficient unless the surrounding V5 layout is redesigned so bounded-count variants actually occupy fewer than 32 bytes.

Warning (V5 header, 2026-03-22): The RC header is now 32 bytes with 4 fields: data_size (i64), elem_dec_fn (ptr), elem_count (i64), strong_count (i64). This plan was drafted when the header had only 2 fields (data_size + strong_count). Any narrowing strategy must account for all 4 fields, not just the refcount. The rc_ops! macro code in Section 09.3 does not account for elem_dec_fn or elem_count and must be updated before implementation.

Backend-neutral authority: AIMS does not select an LLVM/VM allocation mechanism, counter, or RC-header width. It freezes OwnerBound, exact OwnershipObservationFacts, locality/lifetime, cleanup, external-visibility, and thread-reachability by stable allocation identity. The ownership-observation carrier preserves additional-credit, release, and sharing-observation event identities without prescribing how any event executes. VmLayoutPlan and CompiledLayoutPlan independently choose mechanisms, storage, and width, and validation proves each choice satisfies those facts.

The kernel-checked RL-14 through RL-21 corpus now states neutral facts plus VM/compiled satisfaction obligations. Its 130/130 dual-discharge gate, 40-proof section-08 gate, and exact VM-profile gate are green. Remaining work is production fact generation, exact-identity binding, and physical-plan validation. Any older sketch below that puts sharing analysis in ori_repr, returns a universal IntWidth, or assumes one header layout is superseded by this contract.

The challenge has two owners: AIMS must soundly bound simultaneous logical owners and freeze every additional-credit, release, and sharing-observation event without target knowledge. Each physical layout planner must then choose an encoding whose capacity, lifetime, external-boundary, cleanup, and thread-safety capabilities satisfy those facts.

Reference implementations:

• Swift stdlib/public/SwiftShims/RefCount.h: Encodes refcount + flags in a single 64-bit word using bitfields. Stores strong count, unowned count, and flags (immutable, immortal, deallocating) in one word.
• Lean4 src/runtime/object.h: Uses 32-bit RC + tag in a single word. RC overflow bumps to “immortal” (never freed).
• CPython: Uses Py_ssize_t (platform word size) — simple but wastes memory.

Depends on: §02 (triviality and logical drop evidence) and §08 (neutral locality/lifetime facts). Neither prerequisite decides whether a physical header exists.

09.1 Freeze AIMS Owner and Ownership-Observation Facts

File(s): AIMS ownership/provenance analysis, ArcPipelineBatchOutcome, and ExecutableProgram fact tables

Compute an upper bound on simultaneous ownership obligations once, without choosing a backend header or storage class. Key every result by stable allocation-site identity and transport it validation-only.

• Define neutral owner-bound and ownership-observation facts, matching the kernel/checker carrier exactly:

  #[derive(Debug, Clone, Copy, PartialEq, Eq)]
  pub enum OwnerBound {
      /// At most `additional_owners + 1` simultaneous logical owners.
      Bounded(u32),
      /// Unknown or dynamically unbounded.
      Unbounded,
  }
  
  pub struct ExactOwnershipObservationFacts {
      pub sharing_observation_events: Box<[OwnershipEventId]>,
      pub additional_credit_events: Box<[OwnershipEventId]>,
      pub release_events: Box<[OwnershipEventId]>,
      pub externally_observable: bool,
  }
  
  pub enum OwnershipObservationFacts {
      Exact(ExactOwnershipObservationFacts),
      Unknown,
  }

  Bounded(0) plus no additional-credit or sharing-observation events and closed external visibility makes a physical no-counter plan eligible. The plan must still map every release event to one exact satisfaction action, including structural lifetime discharge or a proof-backed no-op, and preserve logical child/user cleanup. “No counter” and “no header” are never AIMS facts.

• Implement per-allocation owner-bound analysis:

  pub fn compute_owner_bound(
      alloc: AllocId,
      arc_func: &ArcFunction,
      aims_facts: &AimsAllocationFacts,
      loop_info: &LoopInfo,
  ) -> OwnerBound {
      // External or unknown visibility may permit ownership births absent from
      // this closed event set. Lifetime/locality alone says nothing about the
      // simultaneous owner count.
      if aims_facts.external_visibility(alloc) != ExternalVisibility::Closed {
          return OwnerBound::Unbounded;
      }
  
      // AIMS proves that only the original logical owner can exist.
      if aims_facts.ownership_observations(alloc).has_no_additional_credits() {
          return OwnerBound::Bounded(0);
      }
  
      // Collect logical additional-credit events, never physical RC operations.
      let Some(credits) = aims_facts
          .ownership_observations(alloc)
          .exact_additional_credit_events()
      else {
          return OwnerBound::Unbounded;
      };
  
      // SOUNDNESS: Static instruction count ≠ dynamic execution count.
      // A single credit event inside a loop body can execute N times, creating
      // up to N simultaneous references. We must bail to Unbounded if
      // any credit event is inside a loop or reachable via recursion.
      let any_credit_in_loop = credits.iter().any(|credit| {
          loop_info.is_in_loop(credit.block)
      });
      if any_credit_in_loop {
          // Future: if §03 range analysis can bound the loop iteration
          // count, AIMS could freeze
          // OwnerBound::Bounded(credit_count * max_iters).
          // For now, conservatively bail.
          return OwnerBound::Unbounded;
      }
  
      // Similarly, if this function is (mutually) recursive and the
      // allocation flows into the recursive call, the static count
      // is not a sound bound.
      if arc_func.is_recursive() && arc_func.alloc_flows_to_self_call(alloc) {
          return OwnerBound::Unbounded;
      }
  
      // The closed, acyclic event set executes each ownership birth at most
      // once. Summing all such births is conservative even across branches;
      // releases may lower the real peak but are not needed for soundness.
      let additional_owner_count = credits.len();
      u32::try_from(additional_owner_count)
          .map_or(OwnerBound::Unbounded, OwnerBound::Bounded)
  }

• Interprocedural refinement:

  • A parameter contributes zero new owners only when its exact ParamContract proves borrow-only/no-retain; ArgEscaping alone is insufficient.
  • Passing a value to N proven borrow-only parameters keeps the same bound.
  • Collection insertion contributes only the exact ownership births proved by the call/collection contract. A capacity-based bound is legal only when range evidence bounds capacity and the operation cannot repeat through a loop, recursion, callback, or unknown call; otherwise use Unbounded.

• /tpr-review passed — independent review found no critical or major issues (or all findings triaged)

• /impl-hygiene-review passed — hygiene review clean. MUST run AFTER /tpr-review is clean.

• Subsection close-out (09.1) — MANDATORY before starting the next subsection. Run /improve-tooling retrospectively on THIS subsection’s debugging journey (per .claude/skills/improve-tooling/SKILL.md “Per-Subsection Workflow”): which diagnostics/ scripts you ran, where you added dbg!/tracing calls, where output was hard to interpret, where test failures gave unhelpful messages, where you ran the same command sequence repeatedly. Forward-look: what tool/log/diagnostic would shorten the next regression in this code path by 10 minutes? Implement improvements NOW (zero deferral) and commit each via SEPARATE /commit-push using a valid conventional-commit type (build(diagnostics): ... — surfaced by section-09.1 retrospective — build/test/chore/ci/docs are valid; tools(...) is rejected by the lefthook commit-msg hook). Mandatory even when nothing felt painful. If genuinely no gaps, document briefly: “Retrospective 09.1: no tooling gaps”. Update this subsection’s status in section frontmatter to complete.

• /sync-claude section-close doc sync — verify Claude artifacts across all section commits. Map changed crates to rules files, check CLAUDE.md, canon.md. Fix drift NOW.

• Repo hygiene check — run diagnostics/repo-hygiene.sh --check and clean any detected temp files.

09.2 Verified VM and Compiled Layout Projection

File(s): VmLayoutPlan, CompiledLayoutPlan, target-independent capacity validation, and projection proofs

• Map one frozen OwnerBound plus OwnershipObservationFacts into backend-private satisfaction actions and storage.

• A VM may use side tables, packed schema metadata, or a host-width counter; compiled targets may choose inline i8/i16/i32/i64 counters.

• Neither choice feeds back into AIMS or becomes the other’s ABI.

• Implement width selection:

  pub fn select_compiled_rc_layout(
      bound: OwnerBound,
      ownership_observations: &OwnershipObservationFacts,
      target: &TargetSpec,
      abi_visibility: AbiVisibility,
  ) -> CompiledRcLayout {
      // Target/ABI policy chooses a representation whose capacity is >= bound.
      // ABI-visible layouts may conservatively retain the canonical full width.
      todo!()
  }
  
  pub fn select_vm_rc_storage(
      bound: OwnerBound,
      ownership_observations: &OwnershipObservationFacts,
      schema: &VmObjectSchema,
  ) -> VmRcStorage {
      // VM-private object/side-table choice; no compiled width enters here.
      todo!()
  }

• Add one target-independent validator proving selected capacity covers OwnerBound, every required additional-credit/release/sharing-observation event has exactly one satisfaction mapping, lifetime is sufficient, cleanup/drop identity is preserved, and the chosen synchronization mechanism satisfies frozen ThreadReachability.

• Reject missing allocation IDs, stale bounds, under-capacity counters, ABI-incompatible compiled layouts, and VM schemas that erase required cleanup metadata.

• Overflow behavior:

  • If at runtime the refcount exceeds the header width → must NOT silently overflow
  • A bounded overflow is an internal fact/plan violation. Debug builds report the allocation/fact/plan identity and fail immediately; release builds abort safely rather than wrap, leak by promotion to immortal, or continue with a violated ownership invariant.
  • A separately proved widening/side-table escape hatch may be added only if its transition is atomic with respect to all owners and preserves cleanup.

• Generate per-width runtime functions:

  // ori_rt additions for narrow refcount headers.
  //
  // CRITICAL: The current V5 header is 32 bytes with 4 fields:
  //   data_size (i64), elem_dec_fn (ptr), elem_count (i64), strong_count (i64)
  //
  // Narrowing ONLY applies to strong_count. The other 3 fields
  // (data_size, elem_dec_fn, elem_count) remain at their canonical widths.
  //
  // IMPORTANT: If the header remains padded/aligned to 32 bytes, these
  // width-specific variants are a throughput/verification specialization,
  // NOT a memory-footprint optimization. Do not claim per-allocation byte
  // savings unless §09.3 first adopts a layout that is actually smaller
  // than the current 32-byte V5 header.
  extern "C" fn ori_rc_alloc_i8(size: usize, align: usize) -> *mut u8;
  extern "C" fn ori_rc_inc_i8(data_ptr: *mut u8);
  extern "C" fn ori_rc_dec_i8(data_ptr: *mut u8, drop_fn: Option<...>);
  extern "C" fn ori_rc_free_i8(data_ptr: *mut u8, size: usize, align: usize);
  // Similar for i16, i32.
  // drop_fn calls ori_rc_free_$suffix (generated by DropFunctionGenerator).

• /tpr-review passed — independent review found no critical or major issues (or all findings triaged)

• /impl-hygiene-review passed — hygiene review clean. MUST run AFTER /tpr-review is clean.

• Subsection close-out (09.2) — MANDATORY before starting the next subsection. Run /improve-tooling retrospectively on THIS subsection’s debugging journey (per .claude/skills/improve-tooling/SKILL.md “Per-Subsection Workflow”): which diagnostics/ scripts you ran, where you added dbg!/tracing calls, where output was hard to interpret, where test failures gave unhelpful messages, where you ran the same command sequence repeatedly. Forward-look: what tool/log/diagnostic would shorten the next regression in this code path by 10 minutes? Implement improvements NOW (zero deferral) and commit each via SEPARATE /commit-push using a valid conventional-commit type (build(diagnostics): ... — surfaced by section-09.2 retrospective — build/test/chore/ci/docs are valid; tools(...) is rejected by the lefthook commit-msg hook). Mandatory even when nothing felt painful. If genuinely no gaps, document briefly: “Retrospective 09.2: no tooling gaps”. Update this subsection’s status in section frontmatter to complete.

• /sync-claude section-close doc sync — verify Claude artifacts across all section commits. Map changed crates to rules files, check CLAUDE.md, canon.md. Fix drift NOW.

• Repo hygiene check — run diagnostics/repo-hygiene.sh --check and clean any detected temp files.

09.3 Projection-Specific Runtime Adapters

File(s): compiled ori_rt RC adapters, VM object/side-table implementation, and their layout-plan consumers

The compiled runtime must support its selected header layouts without code bloat. The VM implements the same logical owner-credit creation/release/drop events through its own validated object schema; it does not call width-specific compiled helpers unless its measured layout independently selects that adapter.

Module placement: The width-specific functions MUST live inside rc/ (e.g., rc/narrow.rs with mod narrow; in rc/mod.rs). This is required because they call call_drop_fn and rc_underflow_abort, which are pub(super) — visible within rc/ but not from lib.rs or other modules. Tests go in rc/narrow/tests.rs (sibling convention) if the file becomes a directory module, or in rc/tests.rs if narrow.rs stays as a leaf file and tests are co-located with the existing rc/ test module.

Risk warning: The macro-generated RC operations below use raw pointer arithmetic and unsafe. Every unsafe block MUST have a // SAFETY: comment. The padded_header alignment logic is subtle — a bug causes data corruption in EVERY narrow-header allocation. Property-based testing with varying (size, align) pairs is essential. Note: ori_rt is a crate where unsafe IS allowed, so #![deny(unsafe_code)] does NOT apply here.

• Document the committed V5 layout strategy BEFORE writing any code:

  • This plan chooses Option A — true memory optimization.
  • Redesign the header so bounded-count variants are actually smaller than 32 bytes (for example via variable offsets or a packed/bitfield strategy).
  • Update elem_header.rs accessors and every caller that currently assumes fixed offsets.
  • The superseded “narrow count plus padding back to 32 bytes” layout is NOT an acceptable final design for this section.
  • Add compile-time assertions in rc/narrow.rs requiring every bounded variant to occupy < 32 bytes while preserving payload alignment.

• Implement narrow RC operations for the V5 header layout:

  CRITICAL DESIGN ISSUE: The rc_ops! macro from the original plan assumes a simple single-field header where the refcount is immediately before the payload (data_ptr.sub(1)). This does NOT match the current V5 header layout:

  V5 Header (32 bytes):
  ┌──────────────┬──────────────┬──────────────┬──────────────┐
  │ data_size    │ elem_dec_fn  │ elem_count   │ strong_count │
  │ (i64)        │ (ptr)        │ (i64)        │ (i64)        │
  └──────────────┴──────────────┴──────────────┴──────────────┘
                                                 ↑ this field narrows

  The narrow-header approach must:

  1. Keep data_size, elem_dec_fn, elem_count at their current widths (they are semantically different from refcount)
  2. Only narrow strong_count (the last field before payload)
  3. The rc_inc/rc_dec functions locate strong_count at a fixed negative offset from data_ptr — this offset changes when strong_count is narrowed
  4. The V5 header accessor functions in ori_rt/src/rc/elem_header.rs (store_elem_dec_fn, load_elem_dec_fn, etc.) use hardcoded offsets that must be updated or parameterized

  Implementation approach:

  • Define the chosen header struct(s) and update all offset accessors consistently for the new smaller layouts.
  • Generate ori_rc_alloc_i32, ori_rc_inc_i32, ori_rc_dec_i32 that use the narrow header struct
  • Update DropFunctionGenerator in ori_llvm to emit calls to width-specific free functions
  • Add only the padding required to maintain payload alignment; do not re-expand the bounded variants back to 32 bytes

  // Simplified sketch — the real implementation must handle V5 header fields
  // and prove the resulting layouts are genuinely smaller than 32 bytes.
  rc_narrow_ops!(i8, i8, i8::MAX);
  rc_narrow_ops!(i16, i16, i16::MAX);
  rc_narrow_ops!(i32, i32, i32::MAX);
  // i64 remains the existing 32-byte V5 implementation.

• Atomic variants:

  • For thread-shared values (§10 determines this), use atomic operations
  • For thread-local values, use plain loads/stores (much faster)

• /tpr-review passed — independent review found no critical or major issues (or all findings triaged)

• /impl-hygiene-review passed — hygiene review clean. MUST run AFTER /tpr-review is clean.

• Subsection close-out (09.3) — MANDATORY before starting the next subsection. Run /improve-tooling retrospectively on THIS subsection’s debugging journey (per .claude/skills/improve-tooling/SKILL.md “Per-Subsection Workflow”): which diagnostics/ scripts you ran, where you added dbg!/tracing calls, where output was hard to interpret, where test failures gave unhelpful messages, where you ran the same command sequence repeatedly. Forward-look: what tool/log/diagnostic would shorten the next regression in this code path by 10 minutes? Implement improvements NOW (zero deferral) and commit each via SEPARATE /commit-push using a valid conventional-commit type (build(diagnostics): ... — surfaced by section-09.3 retrospective — build/test/chore/ci/docs are valid; tools(...) is rejected by the lefthook commit-msg hook). Mandatory even when nothing felt painful. If genuinely no gaps, document briefly: “Retrospective 09.3: no tooling gaps”. Update this subsection’s status in section frontmatter to complete.

• /sync-claude section-close doc sync — verify Claude artifacts across all section commits. Map changed crates to rules files, check CLAUDE.md, canon.md. Fix drift NOW.

• Repo hygiene check — run diagnostics/repo-hygiene.sh --check and clean any detected temp files.

09.4 Completion Checklist

Test matrix for §09 (write failing tests FIRST, verify they fail, then implement):

• Design the V5-narrow header layout document in compiler/ori_rt/src/rc/narrow.rs BEFORE writing any code:
  • WHERE: write a // SAFETY: comment block and static_assert! macros as specified in §09.3
  • All unsafe blocks in narrow.rs MUST have // SAFETY: comments per hygiene rules
• Add static_assert! requiring size_of::<V5HeaderI32>() < 32, size_of::<V5HeaderI16>() < 32, and size_of::<V5HeaderI8>() < 32, with payload alignment preserved.
• AIMS freezes Bounded(0) plus exact empty additional-credit and sharing-observation sets only where the logical plan introduces no additional owner or sharing observation; the physical no-counter verdict belongs to plan validation
• Owner-bound analysis computes Bounded(N) for values with limited simultaneous logical ownership
• Every VM and compiled RC storage choice validates capacity against the same stable-ID bound
• ABI-visible compiled layouts and VM schemas remain independent projections; neither imports the other’s offsets/widths
• Runtime has ori_rc_alloc_i8, ori_rc_inc_i8, ori_rc_dec_i8 (and i16, i32) in compiler/ori_rt/src/rc/narrow.rs
• Header overflow in release mode aborts safely; it never wraps or converts a live obligation into a leak
• Header overflow in debug mode fails with allocation/fact/plan attribution
• Benchmarks and diagnostics report measured per-allocation savings from the real chosen layouts, not from nominal refcount widths
• ./test-all.sh green
• ./clippy-all.sh green
• ./diagnostics/valgrind-aot.sh clean
• The implementation keeps Option A explicit in code comments, layout assertions, and §12 benchmark expectations
• /tpr-review passed — independent Codex review found no critical or major issues (or all findings triaged)
• /impl-hygiene-review passed — implementation hygiene review clean (phase boundaries, SSOT, algorithmic DRY, naming). MUST run AFTER /tpr-review is clean.
• /improve-tooling retrospective completed — MANDATORY at section close, after both reviews are clean. Reflect on the section’s debugging journey (which diagnostics/ scripts you ran, which command sequences you repeated, where you added ad-hoc dbg!/tracing calls, where output was hard to interpret) and identify any tool/log/diagnostic improvement that would have made this section materially easier OR that would help the next section touching this area. Implement every accepted improvement NOW (zero deferral) and commit each via SEPARATE /commit-push. The retrospective is mandatory even when nothing felt painful — that is exactly when blind spots accumulate. See .claude/skills/improve-tooling/SKILL.md “Retrospective Mode” for the full protocol.

Exit Criteria: AIMS freezes one validated OwnerBound and exact OwnershipObservationFacts entry per applicable site without physical storage choices. VM and compiled layout plans independently satisfy those facts plus lifetime, external-boundary, cleanup, and thread-reachability obligations.

Any compiled bounded-count header claimed as a memory win is demonstrably smaller than 32 bytes; VM memory is measured from its actual schema. Evaluator/VM/LLVM debug/release/AOT behavior and ownership-event parity hold, teardown/leak gates are clean, and Valgrind is clean for compiled lanes.

09.R Third Party Review Findings

• [TPR-09-001][critical] section-09-arc-header.md:199-206 — Design contradicts exit criteria: narrow headers padded to 32 bytes yield zero memory savings. The plan at line 204 states “ALL narrow header variants remain 32 bytes” with padding to maintain elem_header.rs offset compatibility. Lines 173-175 claim “saves 4/6/7 bytes per allocation” and the exit criteria claims “~7MB savings” — both impossible with 32-byte padded headers. The entire section’s memory optimization premise collapses. Action: Either (a) redesign header layout with variable offsets (breaking elem_header.rs hardcoded offsets), (b) use Swift-style bitfield encoding in a single 64-bit word, (c) reframe the section around RC elision for Unique allocations (which saves the full 32 bytes — already done by §08 stack promotion), or (d) revise exit criteria to reflect actual benefit (narrower atomic operations for throughput, not memory reduction). Consensus: 3/3 reviewers, escalated from critical.