What the compiler proves about your heap

This series has been making claims about memory one article at a time. This one collects them, because the collection is itself the point: not “Mica catches many bugs”, but a closed list — every classic heap bug, and for each one, exactly what happens.

Every row in that table was produced for this series by making the bug and reading the answer. The example for this article is built so you can do the same.

examples/HeapProofs is a workbench: a sound program — compiles clean, runs to exit 0 — where every section is one bug class held at bay, and every section’s comment names the one-line change that produces the bug and the report it earns. Make the change, rebuild, read the refusal, undo.

make -C examples/HeapProofs run

The obligation rows

The first three rows are the heap article’s machinery. Delete one dispose from the workbench:

obligation error 13102: heap cell is not released on every path: last use at
line 68, the path leaving at line 138 releases nothing — dispose it, defer
the dispose, return it, or bind it to an owner with 'until'

Read the two line numbers: the last use is where you stopped needing the cell, and the leaking path is the program’s last line — the analysis followed the cell all the way to the exit before concluding no path releases it.

Move a read below the release:

obligation error 13105: heap cell is dereferenced after it was already
released on every path reaching here — the cell allocated at line 77 is
used after its dispose; move the use before the release

Release twice:

obligation error 13104: heap cell is disposed again after it was already
released on every path reaching here — remove the repeated dispose of the
cell allocated at line 77

Each report names the allocation it indicts and the move that repairs it. These are not warnings — the build stops.

The rows no analysis can reach

Hide a release behind runtime data — a flag, a configuration, a message — and the proof honestly gives up. Those runs belong to the checked tier (--optimize checked), where every release poisons the cell’s header and every dereference tests for poison:

Mica runtime failure: reason=use_after_dispose (11)
Mica runtime context: file=H4.mica, line=17, column=27
Mica runtime source:     WriteLn("%lld", value p);

Mica runtime failure: reason=double_dispose (10)
Mica runtime context: file=P3.mica, line=12, column=5
Mica runtime source:     dispose p;

The division of labour is exact: the analysis refuses what your control flow proves; the checked tier traps what it cannot; and the class of silence — a stale read that returns plausible bytes and lets them propagate — has no tier anywhere in which it is the designed behaviour.

The rows that never reach the heap at all

Some classes die earlier. A pointer cannot leave the frame that owns its cell:

analyzer error 5150: cannot return pointer to local variable 'local': only
heap-origin pointers, pointer parameters, or lexical parent-scope variables
are allowed

A pointer cannot be read before its first assignment — the wild first read does not exist:

analyzer error 5167: identifier with pointer data type is used before its
initialization: p

A borrow cannot free, and cannot be laundered into an owner — the ownership article’s two refusals, 5200 and 5199, enforced inside the borrower’s own body.

The corruption floor

Two rows are traps at every optimization tier, because they are the floor under everything else — the two ways a program reads or writes memory that was never its own:

Mica runtime failure: reason=index_out_of_range (12)
Mica runtime context: file=B2.mica, line=12, column=22
Mica runtime source:     WriteLn("%lld", r[i]);

Mica runtime failure: reason=nil_dereference (9)
Mica runtime context: file=P2.mica, line=14, column=33
Mica runtime source:     WriteLn("child %lld", n.next.v);

Both were run at release,full_optimizations for this article, and both trapped identically. There is no build flag that trades these checks away — the aggregates article made that promise for indices, and it holds for nil. A wrong step is a named line, on x86-64 and ARM64 alike, never a lucky read of a neighbour.

That is the claim “no silent corruption” cashed out: every road from a type-correct Mica program to overwritten foreign memory ends in a refusal or a named-line trap. The workbench’s last section walks a linked list behind a # nil guard — drop the guard, and the trap above is what you get.

What this does not do

The checked-tier rows are the checked tier’s. A release build keeps lean dereferences, so a use-after-dispose that no analysis could prove is stale memory there. The floor rows — bounds and nil — hold at every tier; the poison rows hold at checked. Develop and soak under checked; choose the shipping tier by which rows your deployment can afford to lose.

A pointer stored into long-lived shared state degrades the proof. The obligation analysis classifies such cells as manually-verified rather than proven, and says so. The four discharge roads are the shapes it proves outright.

Cycles of owners trap rather than leak — under checked. The ownership article’s borrowed back edge is the legal spelling; a genuine owner cycle is a misuse the checked drain reports as cyclic_ownership, and a release build’s behaviour on that misuse is undefined by design.

None of this is a garbage collector. Nothing scans, nothing counts, nothing pauses. The proofs are static, the traps are one comparison, and the arena article runs the same programs with no OS allocator at all.

What the compiler proved

Fourteen rows, each one an answer produced by a real build or a real run — not a design intention. The workbench example is sound as written; every one-line mutation its comments name was made while writing this article, and every quoted report is what came back.

If you take one sentence from the whole memory section, take this one: in Mica, the interesting question about a heap bug is not “how do I find it?” but “which refusal or which trap is it?” — and the table at the top is the complete set of answers.

The table above covers the heap. The full trap vocabulary — every reason the runtime can name, arithmetic and casts and files included, with the tier each one runs on — is the reference chapter Traps and tiers.

Next

Defer, end to end — the one cleanup mechanism behind everything this section used: its exact ordering, its interplay with leave and loops, and why one mechanism serves scopes, generators, tasks and the heap alike.