ch:capability-region-types: ch:capability-region-types

Problem and invariant. Audit a finite authority trace. Maintain one status per region: absent, unique, shared, or freed. Access requires live authority; free requires unique authority; halt requires that no live region remains.

Two representations. Represent the finite state by an association list from natural-number region names to status. Represent commands by constructors for new, access, share, free, and halt. A finite map gives faster lookup but makes the source-level transition order less visible; the association list is sufficient and keeps every update explicit. A rejected transition stops the trace.

First complete version. New changes absence to unique. Access preserves unique or shared. Share changes unique to shared and preserves shared. Free changes only unique to freed. Halt scans the state and accepts exactly when every entry is freed.

Remaining cases in metatheory order. Implement fresh allocation, live access, sharing, unique free, and halt, then add rejection for absent access, shared free, repeated free, and live halt. This follows the preservation proof’s region-extension, access, collection, and terminal cases. Halt produces a stopped result, so no later command can execute.

Observable result. The corpus prints five PASS lines: the good allocate–access–free trace, then rejections for access after free, free under shared authority, double free, and live halt. It finishes with All 5 Chapter 50 corpus cases passed.

A failing version. Permit FreeRegion to change shared to freed. The program remains well typed as Kappa code and its audit remains empty, but the shared-free negative oracle changes result.

Acceptance test. Run the four Appendix E commands with packaged Kappa v0.3.0. Require a silent check, the passing inline harness, the exact six-line run transcript, and an empty audit. Restore the accepted source after mutation and repeat the four commands.

Mathematical boundary. The status machine omits memory contents, types, capability equations, polymorphism, effects, and CPS translation. The named metatheorems are theorem 50.5, theorem 50.7; the finite run demonstrates four necessary rejections but proves neither one.