================
CELL PERMISSIONS
================

This document defines permission-associated cells. The words MUST, MUST NOT,
SHOULD, and MAY are normative.

TERMS
=====

A storage region controls the lifetime and reclamation of a cell's storage.

A permission owner is a non-Copy value. One explicit exclusive borrow of that
value backs one permission identity. A named permission region denotes that
identity. A permission controls access to all cells that have its identity.
It does not own or reclaim their storage.

A loan region is the lexical region of a payload reference and of the matching
borrow of the permission owner. Storage, permission, and loan regions are
separate regions.

An associated cell is a cell type that names a permission region. Every alias
of the cell has the same permission association.

TYPE AND CONSTRUCTION SYNTAX
============================

The associated cell type is:

    &'storage cell 'permission T

The first region is the storage region. The optional region after `cell` is
the permission region. Existing unassociated forms, such as `&cell T` and
`&'storage cell T`, keep their current meaning.

The associated construction form is:

    &cell 'permission place

`place` MUST be initialized and exclusively accessible when this expression
executes. Its storage region becomes the cell's storage region. The named
permission identity becomes the cell's permission association. Construction
MUST have the matching permission authority in scope.

An unassociated cell MAY provide value access when `T` is Copy. It MUST NOT
produce a shared or mutable reference to its payload.

PERMISSION AUTHORITY
====================

A lexical permission region MUST contain one explicit exclusive borrow of its
non-Copy owner. For example:

    let permission: 'permission = &mut owner in {
        // `permission` is the authority for `'permission`.
    }

A function that uses `'permission` in an associated cell type MUST also take
an explicit authority parameter of the form:

    permission: &'permission mut Owner

The function MUST use the same region in the cell type and the authority
parameter. Permission access is therefore an explicit call argument. The
language MUST NOT infer a transitive permission effect.

ACCESS AND LOANS
================

Direct Copy reads and whole-value writes through an associated cell require
available matching permission authority.

A payload reference MUST be created in an explicit lexical region block. The
same block MUST borrow the matching permission owner into the same loan
region.

For a shared payload reference, the block MUST borrow the permission owner
with `&`. Any number of shared payload references for that permission MAY be
live together. While one is live, mutation through every cell with that
permission MUST be rejected.

For a mutable payload reference, the block MUST borrow the permission owner
with `&mut`. While it is live, every other read, write, or payload borrow
through every cell with that permission MUST be rejected.

The payload reference MUST end at the lexical end of its loan region. It MUST
NOT escape the matching permission-owner borrow. It also MUST NOT outlive its
cell's storage region. Reclamation or reset of the storage region MUST remain
invalid while a payload reference into that storage is live. A payload loan
does not itself borrow the storage owner, so allocation that does not reclaim
or reset existing storage MAY continue.

Aliases, field extraction, assignment, substitution, and storage-region
shortening MUST preserve the permission association. If storage region
`'storage` is shortened to `'short`, the result is
`&'short cell 'permission T`; it is not relabeled to another permission.
Permission associations are invariant.

GENERICS AND CALLS
==================

A generic function MUST declare each permission region that occurs in an
associated cell parameter and MUST receive the matching explicit authority
parameter. Region inference and substitution MUST propagate the permission
association through cell types.

A call MUST use the same permission identity for an associated cell and its
authority argument. It MUST reject cross-permission access, relabeling, and
any call or callback that conflicts with a live loan. Two distinct permission
parameters in one signature MUST NOT map to the same actual permission
identity at a call.

After a payload reference is passed as an ordinary `&T` or `&mut T`, a helper
uses the ordinary reference rules. The helper does not need a cell permission
argument unless it also accesses an associated cell.

NON-COPY PAYLOADS
=================

An associated cell MAY contain a non-Copy payload only when that payload is
eligible for bulk discard under the existing ownership rules. Such a payload
MAY be borrowed by reference under the access and loan rules above.

An implicit payload value read MUST require Copy. A move of the payload or of
a payload field that would leave shared storage partly or wholly uninitialized
MUST be rejected.

Whole-value replacement is permitted. The operation MUST evaluate the new
value before it changes the cell. If evaluation fails, the cell MUST remain
unchanged. After successful evaluation, the operation MUST replace the old
value and bulk-discard the old value. It MUST NOT run a destructor.

Storage reclamation remains a bulk operation controlled only by the storage
region. Permission expiration does not reclaim storage. Freezing remains a
library-level state transition.

EXAMPLE
========

This example uses distinct storage, permission, and loan regions:

    record Permit {}
    record Item { value: u32 }

    fn addOne(item: &mut Item) {
        set item.value += 1;
    }

    fn update 'storage 'permission (
        item: &'storage cell 'permission Item,
        permission: &'permission mut Permit,
    ) {
        let authority: 'loan = &mut *permission,
            payload = &mut *item in {
            addOne(payload);
        }
    }

    fn example 'storage (storage: &Session 'storage) throws (AllocError) {
        let mut owner = Permit {};
        let permission: 'permission = &mut owner in {
            let place = try storage.new(Item { value: 0 });
            let item: &'storage cell 'permission Item =
                &cell 'permission *place;
            update(item, permission);
        }
    }

COMPILE-TIME AND RUNTIME CONTRACT
=================================

Permission identities, cell associations, and loan conflicts are compile-time
facts. They MUST NOT add garbage collection, runtime identity values, runtime
borrow checks, hidden arguments, hidden effects, or general alias analysis.

An associated cell MUST have the same pointer layout and runtime operations as
an unassociated cell. Permission metadata MUST NOT change emitted pointer
representation. This feature MUST NOT add destructors. Ordinary `&mut`,
`&cell`, field access, and `set` remain the access operations; the feature adds
no read or write block syntax.