cosring

cosring

TL;DR

Consider two concentric rings with directed arrows and bi-directional chutes between the interior and exterior. In a 3-dimensional configuration, this really closely resembles eukaryotic transmembrane proteins like sodium ion channels, aquaporins, and surface ligand-mediated transport across a phospholipid bilayer.

What if... we tried programming this in 2-dimensions using Rust?

Rust enforces exclusive mutable access: only one "arrow" can hold mutable reference to a slot at a time. The outer node could own “write rights.” The inner node could own “read rights.”

Passing through the bidirectional arrow transfers ownership, ensuring at no time do producer and consumer both hold the same slot. This is like a coset partition of ownership states:

• W (slot writable, held by producer)
• R (slot readable, held by consumer)

Transition = moving through that one bidirectional arrow.

Why the Group-Theory Visualization Helps

Cosets split a group into disjoint sets so a data-structure could be splitting a buffer of slots into two disjoint ownership kinds: (i) Owned-by-producer, (ii) Owned-by-consumer. And just like cosets, the partition is clean: no overlap, no ambiguity. Concurrency hazards (double ownership, data races) vanish because the structure itself prevents them.

Definitions

Inspired by cosets in category theory (group theory) we can make a swanky ring buffer that is guaranteed to ensure Rust's ownership model using math!

Categories / Groups

In this context there are three categories:

1. The index (time/position) category I. It uses one object • with endomorphisms End(•) ≅ ℤ/nℤ. Think of the generator σ : • → • as advancing one step around the ring.
2. The local state category S. It employs two zero-sized objects Empty and Full with morphisms write : Empty → Full, read : Full → Empty without the constraint that read ∘ write = id; payloads make these not-actual-inverses good enough.)
3. The product category C = I × S with paired objects (i, state) such that i ∈ ℤ/nℤ.

Functors and Transitions

Let Σ : C → C be the endofunctor given by index shifting: Σ(i, x) = (i+1, x) and that Σ acts as identity on the S-component. Suppose local transitions live in the S-component at fixed i. Concretely we are assigning i to be a natural number corresponding to the slot. Then...

Write_i : (i, Empty) → (i, Full)
Read_i : (i, Full) → (i, Empty)

are two key commuting squares encode locality:

(shift then write) == (write then shift)

   (i, Empty) ──Write_i──▶ (i, Full)
       │                     │
       Σ                     Σ
       │                     │
 (i+1, Empty) ─Write_{i+1}▶ (i+1, Full)

and similarly

(shift then read) == (read then shift)

   (i, Full) ──Read_i──▶ (i, Empty)
       │                     │
       Σ                     Σ
       │                     │
 (i+1, Full) ─Read_{i+1}▶ (i+1, Empty)

A Ring Buffer Template

Next imagine an array of N slots. Take N to be 6. Then there are two cyclic indices with a write_head (outer hexagon) and a read_head (inner hexagon). Each slot has a state machine: Empty → Full → back to Empty.

Ownership (in the Rust sense) is modeled as:

Dealing with the Ring

• Producer owns idx, Consumer doesn't own its idx: this should correspond to bi-directional arrow usage from group theory and the Rust compiler's solver would prove single-ownership by construction
• In cases where the borrow cannot see the proof of single-ownership, formalize a proof adjacent to the block below:

impl<T, const N: usize> Ring<T, N> {
    /// Attempt to write a value at the producer's current position.
    /// 
    /// Proof sketch (safety):
    /// 1. Producer token implies exclusive ownership of this slot.
    /// 2. Consumer cannot observe this slot until `write` completes + token is handed over.
    /// 3. The borrow checker is satisfied because the token encodes exclusivity.
    /// Therefore: no aliasing of &mut T and &T can occur.
    pub fn write_at(&mut self, token: &mut ProducerToken, val: T) -> Result<(), T> {
        let idx = token.index;

        // INVARIANT: slot[idx] is logically "Empty" by token discipline.
        // Ghost state: (Producer owns idx) ∧ (Consumer does not own idx).

        if self.slots[idx].is_some() {
            // This cannot happen if invariants are upheld — consumer must have released.
            return Err(val);
        }

        // SAFETY PROOF (mutation):
        // Mut borrow of self.slots[idx] is sound, because token ensures:
        // ∄ consumer borrow at idx.
        self.slots[idx] = Some(val);

        // After effect:
        // slot[idx] is now "Full", ownership logically transferred to Consumer
        // (but Consumer won’t observe until token is handed over).
        token.index = (idx + 1) % N;

        Ok(())
    }

    /// Attempt to read a value at the consumer's current position.
    ///
    /// Proof sketch (safety):
    /// 1. Consumer token implies exclusive access to this slot *if full*.
    /// 2. Producer cannot overwrite until consumer completes + token is handed back.
    /// 3. Thus, no aliasing or data race.
    pub fn read_at(&mut self, token: &mut ConsumerToken) -> Option<T> {
        let idx = token.index;

        // INVARIANT: slot[idx] is logically "Full" by token discipline.
        // Ghost state: (Consumer owns idx) ∧ (Producer does not own idx).

        let val = self.slots[idx].take();

        // SAFETY PROOF (mutation):
        // Mut borrow of self.slots[idx] is sound, because token ensures:
        // ∄ producer borrow at idx while consumer owns it.

        if val.is_some() {
            // After effect:
            // slot[idx] is now "Empty", ownership logically transferred back to Producer.
            token.index = (idx + 1) % N;
        }

        val
    }
}