Memory Governance Protocol: Standards for Linear Resource Management

1. The Strategic Imperative for Rigorous Resource Governance

In the discipline of high-assurance systems engineering, manual resource management is no longer a sustainable practice; it is a systemic liability. The historical prevalence of "bitrot" and "footguns"—specifically use-after-free, double-free, and memory leaks—originates from a fundamental mismatch between human cognitive limits and the state-space complexity of modern software. This protocol mandates a transition from fragile programmer discipline to the mathematical certainty of linear logic. By enforcing a formal memory governance protocol, we replace "forgiving" language designs that mask instability with "restraining" mechanisms that guarantee reliability by construction.

Systemic reliability is predicated upon the "Fits-in-head Simplicity" of the underlying specification. To mitigate vendor lock-in and the catastrophic risks of "language lawyering"—where ambiguous behavior leads to exploit vectors—the protocol adheres to a design with minimal Kolmogorov complexity. When a specification is brief enough to be fully mastered by a single architect, the language ceases to be a source of uncertainty and becomes a rigid tool for building "pyramids": static, crystalline structures engineered for decades of maintenance-free operation. Systemic reliability is further predicated upon a rigorous taxonomy of data; we therefore partition the type system into two distinct universes.

1. The Binary Universe: Partitioning Free and Linear Types

The foundation of resource safety is the strategic partitioning of all data into two mutually exclusive universes. This taxonomy allows the compiler to apply divergent governance rules based on the inherent risk and lifecycle requirements of the data.

The Taxonomy of Universes

Universe Characteristics Examples
The Free Universe Unrestricted types that may be copied, shared, or discarded at will. These carry no lifecycle obligations. Int32, Bool, Float64, and structs composed exclusively of free types.
The Linear Universe Restricted types representing finite, unique resources. Linearity is "viral": any composite structure containing a linear type is promoted to the Linear Universe. Pointers, File handles, Database connections, and unforgeable Capabilities.

The "Use-Once Rule" and its Enforcement

The protocol mandates that every linear value be consumed exactly once. The compiler enforces this through three mandatory static checks:

1. Silent Discard Prevention: A linear value cannot be ignored or allowed to go out of scope without consumption. Every resource must reach an explicit terminal state.
2. Double-Consumption Prevention: Once a linear value is passed to a function or destructured, it is "consumed." Any subsequent reference to that variable is a terminal compile-time error.
3. The "0.5 Use" Violation: Within conditional branching (if or case statements), a linear value must be consumed in every branch or none of them. Consuming a resource in only one branch is a 0.5-use violation, as the post-junction state of the resource is non-deterministic.

Furthermore, a critical constraint is enforced regarding iteration: a linear variable defined outside a loop body is strictly forbidden from appearing within that loop body. Because the loop may execute zero or many times, the compiler cannot guarantee the "exactly once" requirement.

Strategic Value

Partitioning types into these universes enables the performance benefits of functional programming—specifically referential transparency—without the non-deterministic latency of a runtime garbage collector. This architecture transforms the compiler into a lifecycle enforcement engine, transitioning from abstract theory to the practical management of resource states.

1. Protocol for Enforcing Resource Lifecycles

Architectural integrity requires mapping implicit programmer intent into explicit, compiler-enforced state transitions. The architect must enforce a Standard Lifecycle Graph (Open → Use → Close) to ensure all resources follow a deterministic path from birth to termination.

The Standard Lifecycle Components

• The Constructor (Open): Linear types are birthed via explicit constructors (e.g., openFile). This is the only valid entry point for a linear handle into the environment.
• The Mutator/Threading Pattern (Use): To maintain linearity during mutation, the protocol utilizes "threading." A function consumes the existing handle and returns a "new" linear handle to the same underlying resource. This ensures the resource has exactly one owner at any point in time, enabling safe imperative mutation with functional-style equational reasoning.
• The Terminus (Close): Every lifecycle must conclude with a mandatory destructor (e.g., closeFile). This function consumes the linear value and returns nothing, satisfying the "Use-Once Rule" and signaling the safe disposal of the resource.

Elimination of Lifecycle Vulnerabilities

The "Use-Once Rule" provides a complete static solution to the three primary categories of lifecycle failure, effectively striking them from the graph:

• Leaks: Forbidden by the prohibition of silent discards.
• Use-After-Close: Forbidden because the Close function consumes the handle; any subsequent use is flagged as a double-consumption error.
• Double-Close: Forbidden because the first Close consumes the value, making a second call a compile-time violation.

While strict linearity is the safest state, sophisticated borrowing mechanisms are required to ensure the system remains ergonomic and adheres to the Principle of Least Privilege.

1. Advanced Governance: Borrowing and Permission Degradation

To minimize the surface area of potential misuse, the protocol mandates the "Principle of Least Privilege" when interacting with linear resources. Borrowing allows an architect to treat a linear value as if it were a free value within a delineated context, enabling temporary permission degradation.

The Permission Hierarchy

1. Read-Only References (&[T, R]): The lowest permission; guarantees the value is neither mutated nor deallocated.
2. Read-Write References (&![T, R]): The mid-level permission; allows mutation of the internal state but strictly forbids destruction.
3. Ownership (The Linear Value): The highest permission; required for resource disposal or transfer of ownership.

Regions and Memory Safety

Borrowing is governed by Regions. A borrow is mathematically forbidden from escaping the statement or block where it was introduced. This ensures the underlying resource cannot be consumed or destroyed while references are live. By using explicit regions and kinds, the protocol achieves memory safety without the "fighting the borrow checker" learning curve common in more heuristic-based ownership systems; the rules are inductive, simple, and predictable. To maintain this safety, specific standards must be met when the system interacts with non-linear external environments.

1. Managing the Trust Boundary: FFI and Unsafe Modules

A robust governance protocol must define the "Trust Boundary"—the interface between safe, linear code and external, non-linear environments (typically C-based Foreign Function Interfaces).

Protocol for Linear Interface/Non-Linear Interior

The protocol mandates a "Linear Interface/Non-Linear Interior" design. Inside the trust boundary, we use Destructuring to "explode" a linear struct into its constituent fields.

Motivation for Destructuring: In the Linear Universe, accessing a single field of a struct (e.g., p.x) consumes the entire container. If the container is not destructured, any other linear fields within it would be leaked and become inaccessible. Destructuring allows the architect to dismantle the struct, manipulate the underlying non-linear handles (like a raw C file pointer), and re-assemble the fields into a fresh linear wrapper before returning it to the client.

Requirements for Unsafe Modules

Any module bridging the trust boundary must be explicitly audited and must meet these standards:

• The Unsafe_Module pragma must be declared in the body.
• Permissions for Austral.Memory and the External_Name pragma (required for identifying foreign functions) must be explicitly invoked.

This centralization allows for focused security audits of the "unsafe" bridge while the rest of the application remains protected by the linear compiler. This architecture enables higher-level security abstractions, such as capabilities.

1. Capability-Based Security Standards

Modern software architectures are uniquely vulnerable to supply chain attacks, where compromised dependencies leverage uniform root permissions to exfiltrate data. This protocol enforces "Permissioned Code" through Linear Capabilities.

Capabilities as Unforgeable Proofs of Authority

A capability is a linear value that serves as an unforgeable proof of authority. These prevent unauthorized access to effectful operations and mitigate side-channel risks, such as Spectre or timing attacks, by restricting access to high-resolution timers.

• The Root Capability: The absolute authority granted only at the program entry point.
• Hierarchical Capabilities: Derived from the Root (e.g., a Directory capability derived from a Filesystem capability), allowing granular access to specific sub-trees of the system.

The Four Immutable Properties of Capabilities

1. Uniqueness: They cannot be duplicated.
2. Revocability: They can be destroyed (consuming the authority).
3. Transferability: They can be surrendered to other modules.
4. Origin: They cannot be acquired "from thin air"; they must be explicitly passed down the call stack.

This enables an architect to audit the "effectful reach" of any library simply by inspecting its function signatures. If a library does not accept a Filesystem capability, it is physically impossible for it to access the disk.

1. Failure Protocols: Contract Violations and Program Termination

The final component of this governance protocol is the philosophy of "Scuttling the Ship." When a system reaches an unrecoverable state, it must prioritize security over attempts at recovery.

The Taxonomy of Failure

• Recoverable Failures: Anticipated conditions (e.g., "File Not Found") are handled as standard control flow via Option and Result types.
• Contract Violations: Bugs, arithmetic overflows, or out-of-bounds access. In an ML-style system, the "Normal" and "Abnormal" paths are given equal consideration; therefore, a contract violation implies the abstract machine is corrupted.

Rejection of Traditional Exception Handling (REOE)

This protocol explicitly rejects REOE (Raise Exception on Error) due to its inherent "Double Throw Problem." Consider fclose: it returns an error code. In an RAII-based system, a destructor cannot easily handle this error without potentially throwing a second exception, which usually leads to immediate, messy termination. Austral refuses to ignore these return codes or hide function calls.

Protocol for Contract Violations

The protocol mandates that on any contract violation, the program must terminate immediately without executing cleanup code.

1. Security: Recovery efforts in a corrupted state are primary attack vectors for an adversary.
2. Predictability: Immediate termination prevents the execution of "hidden" recursive destructors in an unstable environment.

This "brittle" and "crystalline" approach ensures that the software is a rigid pyramid of logic—stable, secure, and built for decades of operation.