A Formal Proof of Absence of Memory Leaks in Argentum Programming Language for the Single-Threaded Case

1. Definitions and Setup

Object Types:

1. Mutable Objects (M): Objects that can be modified, owned by at most one composite pointer (C) and referenced by zero or more temp (T) and weak (W) pointers.
2. Immutable Objects (F): Objects that cannot be modified after creation, referenced by one or more shared pointers (S).

Pointer Types:

3. Composite Pointer (C): Represents exclusive ownership of an M object. At most one C pointer exists per M object at any time. Contributes to the object's reference count.
4. Temp Pointer (T): Short-lived, stack-bound references to M objects, extending their lifetime while in scope. Contributes to the reference count.
5. Weak Pointer (W): Non-owning references to M objects, with no impact on reference count. Dereferencing via a lock-and-check operation yields an Optional<T> (either a T pointer or None if the target is deallocated or never existed).
6. Shared Pointer (S): References to F objects, allowing multiple owners. Contributes to the reference count of F objects.

Graph Representation:

1. Vertices: Objects (M or F).
2. Edges:
   1. Ownership Edges: C (from parent M to child M), S (from any object to F), T (from stack to M).
   2. Non-Ownership Edges: W (from any object or stack to M).
3. The object graph is a directed graph
   G = (V, E),
   where V = M ∪ F and E = E_C ∪ E_S ∪ E_W ∪ E_T.
   Ownership edges E_C ∪ E_S form the primary structure,
   with E_C forming a tree (acyclic due to single ownership)
   and E_S forming a directed acyclic graph (DAG) due to immutability.

Reference Counting:

• For an M object, the reference count RC_M=∣C∣+∣T∣, where ∣C∣ ≤ 1 and ∣T∣ ≥ 0. The object is deallocated when RC_M=0.
• For an F object, the reference count RC_F=∣S∣. The object is deallocated when RC_F=0.
• W pointers do not contribute to RC_M.

Invariants:

1. Single Ownership (I1): For any M object, ∣C∣≤1. No multiparenting is allowed.
2. Stack-Bound Temps (I2): T pointers exist only in stack frames and cannot be stored in heap objects.
3. Immutability (I3): F objects cannot reference M objects, and their fields cannot be modified post-construction.
4. Weak Safety (I4): Dereferencing a W pointer requires a lock-and-check operation, yielding an Optional<T> that increments RC_M if non-empty.
5. No Uninitialized Pointers (I5): T, C, S pointers are initialized upon creation (no null or uninitialized states). W pointers are created empty.
6. Assignment Safety (I6): Assignment to a field or type C pointer (TARGET.FIELD=V_EXPR) follows a five-step process ensuring no cycles or dangling references:
   1. tempTarget = evaluate(TARGET)  // Produces a T pointer
   2. tempVal = evaluate(V_EXPR) // Produces a C pointer
   3. dispose(tempTarget.FIELD)  // Releases the old C pointer in FIELD
   4. tempTarget.FIELD = tempVal // Assigns the new C pointer without modifying counters
   5. dispose(tempTarget) // Releases the temp pointer,
      where `dispose` decrements object's RC_M counter and frees object on RC_M=0.
7. C-erasing (I7). Any read from any variable, field, or container item of type C pointer produces a temporary value of type T pointer. I.e. It is impossible to extract any context data in the form of a C pointer.
8. C-bubbling (I8). Returning a C pointer from a scope moves it outside the scope preserving its C pointer type.
9. Weak Drop (I9). Upon object destruction all W pointers targeting this object become empty.

Goal: Prove that no pointer operations create cycles in the ownership graph (E_C ∪ E_S), ensuring all objects are deallocated when their reference count reaches zero, thus preventing memory leaks.

---

2. Proof Structure

We prove leak freedom through four statements, showing that each pointer type avoids ownership cycles and ensures objects are reclaimed when no longer referenced.

Statement 1: Temp Pointer (T) Operations Do Not Create Cycles

Claim: T pointers cannot form cycles in the ownership graph because they reside only on the stack.

Proof:

• By Invariant I2, T pointers are stack-bound and exist only within lexical scopes (e.g., function parameters, local variables). They cannot be stored in heap objects (fields or containers).
• Stack frames are organized in a nested, acyclic structure (call stack). Each T pointer is created in a stack frame and destroyed when the frame exits.
• Since E_T⊆Stack × M and does not connect heap objects, T pointers do not contribute to cycles in the heap-based ownership graph E_C ∪ E_S.
• When a T pointer goes out of scope, its reference count decrement ensures the target M object is deallocated if RC_M = 0, preventing leaks.

Conclusion: T pointers are acyclic by design and do not cause memory leaks.

Statement 2: Composite Pointer (C) Operations Do Not Create Cycles

Claim: Assignments to C fields or containers (e.g., TARGET.FIELD := V_EXPR) cannot form cycles in E_C.

Proof:

• Consider the assignment TARGET.FIELD := V_EXPR, where TARGET evaluates to an M object (via a T pointer, per Invariant I5), FIELD is a C-typed field, and V_EXPR evaluates to a C pointer to an M object.
• The assignment follows the five-step process (Invariant I6):
  • tempTarget = TARGET.evaluate → Produces a T pointer to the target M object, incrementing RC_M.
  • tempVal = V_EXPR.evaluate → Produces a C pointer to a new or copied M object with RC_M=1.
  • dispose(tempTarget.FIELD) → Releases the previous C pointer in FIELD, decrementing RC_M of the old object (deallocating if RC_M=0).
  • tempTarget.FIELD = move(tempVal) → Assigns the new C pointer, transferring ownership without affecting reference counts.
  • dispose(tempTarget) → Decrements RC_M of the target object.
• Cycle Prevention: A cycle in E_C would require V_EXPR to evaluate to TARGET or an ancestor of TARGET in the ownership tree. However:
  • By Invariant I1, reading a C-typed field or variable yields a T pointer (Invariant I7), not a C pointer, preventing direct reassignment of TARGET or its ancestors.
  • V_EXPR must produce a new M object (via instantiation, copying, or function return as a C pointer, per Invariant I8). Since TARGET is evaluated first (Invariant I6a), V_EXPR cannot access tempTarget or its ancestors during evaluation, as they are not in scope or are only accessible as T pointers (Invariant I7).
  • Thus, the assigned object cannot be TARGET or its parent, ensuring E_C remains a tree (acyclic).
• Exception Safety: If an exception occurs in steps 1 or 2, tempTarget (if initialized) is disposed of, decrementing RC_M. Steps 3–5 are atomic and do not introduce dangling pointers.
• Deallocation: The dispose steps ensure that replaced objects are deallocated if their RC_M=0, preventing leaks.

Conclusion: C pointer assignments maintain an acyclic ownership tree, and objects are reclaimed when unreferenced.

Statement 3: Shared Pointer (S) Operations Cannot Form Cycles

Claim: Assignments to S fields cannot form cycles in E_S.

Proof:

• Consider the assignment TARGET.FIELD := V_EXPR, where FIELD is an S-typed field and V_EXPR evaluates to an S pointer to an F object.
• By Invariant I3, F objects are immutable and cannot reference M objects. The freeze operation (T to S) creates a new F object by copying an M object’s subtree, converting C pointers to S pointers in the copy (ensuring the new subtree is immutable).
• Cycle Prevention:
  • If TARGET is an F object, its fields are immutable (Invariant I3), so the assignment TARGET.FIELD := V_EXPR is not compilable, as F objects cannot be modified post-construction.
  • If TARGET is an M object, FIELD can accept an S pointer. Since V_EXPR produces a new F object (via freeze or reading an existing S pointer), it cannot reference TARGET (an M object), as F objects cannot point to M objects (Invariant I3).
  • Thus, E_S forms a DAG, as no assignment can create a cycle involving TARGET or its ancestors.
• Deallocation: When an S pointer is replaced, the old F object’s RC_F is decremented, and it is deallocated if RC_F=0.

Conclusion: S pointer operations maintain an acyclic DAG, and F objects are reclaimed when unreferenced.

Statement 4: Weak Pointer (W) Operations Cannot Cause Leaks

Claim: W pointers do not cause memory leaks, as they do not affect object lifetimes.

Proof:

• By definition, W pointers have no impact on RC_M. They reference M objects but do not prevent deallocation.
• Dereferencing a W pointer requires a lock-and-check operation, which returns an Optional<T>. If the target M object is alive, the operation yields a T pointer, incrementing RC_M. If the target is deallocated, it returns None, ensuring safe access (Invariant I4).
• Since W pointers do not contribute to E_C ∪ E_S, they cannot create cycles in the ownership graph. Their use in navigation (e.g., cross-references) is safe due to the lock-and-check requirement.
• When an M object is deallocated (RC_M=0), all W pointers to it become empty (I9), and subsequent lock-and-check operations return None, preventing use-after-free errors.

Conclusion: W pointers do not cause leaks or affect the ownership graph’s acyclicity.

---

3. Overall Proof of Leak Freedom

Theorem: The Argentum Ownership Model ensures no memory leaks, as all objects are deallocated when their reference count reaches zero, and no pointer operations create cycles in the ownership graph.

Proof:

• From Statements 1–4, the ownership graph E_C ∪ E_S is acyclic:
  • E_C forms a tree due to single ownership and assignment restrictions (Statement 2).
  • E_S forms a DAG due to immutability and freeze operation constraints (Statement 3).
  • T and W pointers do not contribute to cycles in E_C ∪ E_S (Statements 1 and 4).
• Reference Counting Correctness:
  • For M objects, RC_M = ∣C∣+∣T∣. When ∣C∣ = 0 (no parent) and ∣T∣ = 0 (no stack references), the object is deallocated, as dispose operations in assignments and scope exits decrement counts appropriately.
  • For F objects, RC_F = ∣S∣. When ∣S∣=0, the object is deallocated.
  • The five-step assignment rule (Invariant I6) ensures that replaced C or S pointers are properly disposed of, preventing dangling references or leaks.
• Exception Safety: Exceptions in expression evaluation (steps 1–2 of assignment) release temp pointers, maintaining reference count integrity.
• No Uninitialized or Null Pointers: Invariant I5 ensures all pointers are initialized, and W dereferences yield Optional<T>, handling absence safely.
• Since the ownership graph is acyclic and reference counts are accurately maintained, all objects are reachable only while referenced and are deallocated when RC = 0, ensuring no memory leaks.

Conclusion: The Argentum Ownership Model is leak-free in a single-threaded context, as proven by the acyclicity of the ownership graph and deterministic deallocation.

See also: multi-threaded case.