Borrowing

Temporary Authority

Ownership answers who is responsible for a value. Borrowing answers who may temporarily access that value while ownership remains elsewhere.

A borrow has semantic facts such as:

• borrow kind;
• the referent Place or finite set of possible Places;
• the holder that keeps the borrow live;
• where the borrow begins;
• where its authority is still needed;
• its mutability authority;
• its source provenance.

These facts are tracked by the compiler. They are not fields the programmer manually stores in a reference object.

Borrow Kinds

Sec has two core safe borrow kinds:

ref T
ref mut T

The distinction is an authority distinction, not merely a spelling difference.

Shared Borrow

let view := ref value

A shared borrow permits reading the referent.

It does not permit mutation through that shared reference.

Any number of compatible shared borrows may coexist over overlapping storage:

let first := ref value
let second := ref value

Inspect(first)
Inspect(second)

The owner remains the owner throughout these borrows.

Mutable Borrow

let writable := ref mut value

A mutable borrow permits reading and writing the referent through the borrowed authority.

It reserves exclusive mutable authority over the overlapping Place for its live range.

Therefore an overlapping mutable borrow cannot coexist with:

• another unrelated mutable borrow;
• an overlapping shared borrow;
• direct conflicting use through the owner;
• an ownership-invalidating operation on the same Place.

Legal parent/child reborrowing is the important exception and is described later in this chapter.

Borrowing Is Not Ownership

Neither ref T nor ref mut T becomes owner of the referenced T.

let mut item := CreateItem()
let writable := ref mut item

item remains the owner. writable temporarily holds exclusive borrowed authority.

Mutable authority also does not imply permission to move an owned move-only subvalue out of borrowed storage.

Borrow Conflict Matrix

For overlapping Places, the fundamental compatibility rules are:

This matrix applies only when the Places overlap. Proven disjoint Places may remain independently usable.

Creating Borrows

An explicit shared local borrow is written:

let view := ref value

An explicit mutable local borrow is written:

let view := ref mut value

Borrow creation begins temporary access authority. It does not copy the referent and does not move ownership.

Explicit Borrowing Requires an Addressable Place

General explicit borrow syntax requires a reusable addressable Place with sufficient authority.

Examples of borrowable Places include:

value
object.Field
values[index]

A non-addressable computed expression cannot be borrowed merely because its result type could otherwise be referenced:

let view := ref (left + right)       // invalid
let item := ref CreateItem()         // invalid as a general local borrow

Sec 0.1 does not generally extend arbitrary temporary-expression lifetimes to make such borrows valid.

The Borrowed Place Must Contain a Valid Value

Borrow creation requires an initialized value available on the current path.

This is invalid:

let mut item: Item
let view := ref item

The Place is uninitialized.

This is also invalid after ownership transfer:

let item := CreateItem()
Consume(<-item)

let view := ref item

The Place is unavailable.

A conditionally available Place must first be refined to an available path before it can be borrowed.

Availability and Borrow Compatibility Are Separate

Ownership availability asks whether the current owner still owns a value in a Place. Borrow compatibility asks whether that Place may currently be accessed with the requested shared or mutable authority.

if package.Payload is available {
    Use(package.Payload)
}

proves ownership availability only. It does not prove that no conflicting borrow is active.

A Place may therefore be Available and still be temporarily inaccessible through the owner because an exclusive mutable borrow is live.

Mutability Authority

A shared borrow may be created from immutable or mutable storage when reading is permitted.

let immutable := 10
let shared := ref immutable

A mutable borrow requires actual mutable authority:

let mut value := 10
let writable := ref mut value

This is invalid:

let value := 10
let writable := ref mut value

ref mut does not upgrade immutable storage to mutable storage.

Borrow Live Ranges

Sec derives borrow live ranges from control flow and actual use. The programmer does not write lifetime parameters or lifetime annotations.

let mut value := 10

let view := ref value
Inspect(view)

value = 20

If view has no later reachable use or surviving dependency, its shared borrow may end after Inspect(view).

The lexical scope of view may therefore be longer than the semantic borrow live range.

Borrow Holders

Borrowed authority remains live while something still needs it.

Borrow holders can include:

• a reference value;
• a slice or view;
• a copied shared reference;
• a moved mutable-reference holder;
• a closure capture;
• a returned-reference dependency;
• a defer dependency;
• a parameter binding;
• a compiler-known temporary relation.

Copying ref T creates another holder and may keep the shared borrow live longer.

Moving a ref mut T holder transfers the holder's borrow obligation to the destination. It does not end the borrow of the referent.

Owner Access During a Shared Borrow

While only compatible shared borrows are active, direct owner reads of the overlapping Place remain legal.

Overlapping mutation or ownership invalidation is not allowed while the shared borrow remains live.

Blocked operations include:

• mutation;
• replacement;
• reinitialization that invalidates the borrowed incarnation;
• move;
• discard;
• destruction;
• structural mutation that invalidates the borrowed storage.

Owner Access During a Mutable Borrow

A mutable borrow reserves exclusive authority over its overlapping Place.

let mut value := 10
let writable := ref mut value

writable += 1

While writable remains live, competing direct access through value is invalid:

Print(value)       // invalid while the mutable borrow is live
value = 20         // invalid while the mutable borrow is live

Access through the mutable reference itself, or through a legal reborrow derived from it, is not treated as competing owner access.

Reborrowing

Reborrowing creates narrower or equal borrowed authority from an existing safe reference. It does not transfer ownership of the referent.

Passing a mutable reference to a borrowed parameter is normally a reborrow, not a move of the caller's mutable-reference holder.

Shared Reborrow

A shared reference can provide another shared borrow:

fn Inspect(value: ref Item) void {
    ...
}

fn Use(value: ref Item) void {
    Inspect(value)
}

A mutable reference may also provide a temporary shared reborrow. During that child borrow, conflicting mutable use through the parent is restricted.

Mutable Reborrow

A mutable reference may provide a child mutable reborrow:

fn Reset(value: ref mut Item) void {
    value.State = State.Empty
}

fn Process(value: ref mut Item) void {
    Reset(value)
    value.State = State.Ready
}

Passing value to Reset does not consume the caller's ref mut Item holder.

During the child reborrow, the parent may not exercise conflicting authority. After the child reborrow ends, the parent may become usable again.

Borrow Conflicts Are Based on Place Overlap

Borrow analysis operates on semantic Places, not merely root variable names.

Important rules include:

• a whole Place overlaps every descendant Place;
• equal Places overlap;
• distinct struct fields may be disjoint;
• constant indexes into non-overlapping elements may be disjoint;
• runtime indexes overlap conservatively unless proven otherwise;
• statically disjoint slice intervals may be borrowed independently;
• unknown provenance is handled conservatively.

Fields and Aggregate Places

Proven disjoint fields can be borrowed independently:

type Pair struct {
    Left: int,
    Right: int,
}

let mut pair := Pair {
    Left: 1,
    Right: 2,
}

let left := ref mut pair.Left
let right := ref mut pair.Right

Borrowing the whole aggregate overlaps every field.

Properties Are Not Automatically Independent Storage

A property uses member syntax, but that does not mean it is an independently addressable stored field.

Until compiler-known property metadata proves narrower behavior, property borrowing or mutation conservatively overlaps the receiver storage that the property may access.

Arrays and Indexed Places

Distinct compile-time constant indexes may be proven disjoint:

let left := ref mut values[0]
let right := ref mut values[1]

Dynamic indexes require proof:

let left := ref mut values[a]
let right := ref mut values[b]

The compiler cannot assume a != b merely because two different variables appear in source.

Slice Range Overlap

Statically known slice intervals are normalized for overlap analysis.

let first := ref mut values[0..<4]
let second := ref mut values[4..<8]

These ranges may be borrowed independently when proven disjoint.

A compile-time-known empty interval borrows no elements. Symbolic or runtime ranges overlap conservatively unless disjointness is proven.

Structural Mutation While Borrowed

A live element, slice or view borrow blocks structural operations that may invalidate the referenced storage.

let view := ref values[..]

try values.Append(10)    // invalid while view requires the current backing

Conflicting structural operations include those that may relocate backing storage, change element addresses, remove borrowed elements or replace the backing incarnation.

Borrowed Parameters

A shared borrowed parameter is declared:

fn Inspect(value: ref Item) void {
    ...
}

A mutable borrowed parameter is declared:

fn Reset(value: ref mut Item) void {
    value.State = State.Empty
}

In both cases the caller remains owner of the referent.

Owned Values Can Create Call-Bounded Borrows

At a function call, an owned compatible Place may be passed directly to a borrowed parameter:

fn Inspect(value: ref Item) void {
    ...
}

let item := CreateItem()
Inspect(item)

The call creates a call-bounded shared borrow. The caller does not need to write a separate ref marker.

Mutable call-bounded borrowing works the same way:

fn Reset(value: ref mut Item) void {
    ...
}

let mut item := CreateItem()
Reset(item)

This is a call-specific borrowing rule, not a general implicit owner-to-reference conversion in arbitrary expressions.

Borrow Conflicts Between Call Arguments

Function arguments evaluate left to right, but the final call must satisfy borrow compatibility across overlapping call live ranges.

This is invalid:

fn UpdateBoth(
    left: ref mut Item,
    right: ref mut Item,
) void {
    ...
}

UpdateBoth(item, item)

The call would require two overlapping mutable borrows.

A mutable-reference argument also conflicts with another overlapping shared/reference or direct-access argument while their call live ranges overlap.

Method Receivers

Borrow rules apply to method receivers just as they apply to equivalent Places.

A method requiring shared access may be called through compatible shared authority. A method requiring mutation must receive compatible mutable/exclusive receiver authority.

Receiver borrowing is checked against argument borrowing. Borrowing never grants an ordinary method permission to consume complete self.

Branches and Control-Flow Joins

Borrow state is path-sensitive.

A borrow that remains live on any continuing incoming path remains potentially live after the merge.

Branch-local holders that cannot escape their branch can end before the merge. A terminating branch does not impose its borrow state on code it never reaches.

Finite sets of possible reference origins may be retained statically and checked against every alternative without runtime borrow tags.

Loops

Borrow validity must hold across every possible loop iteration and backedge.

A borrow that may survive a backedge is considered live when the next condition and iteration are validated.

Fresh non-escaping loop-body holders may end at the iteration boundary. continue contributes to the next-iteration borrow state, and break contributes to the post-loop exits it reaches.

Collection iteration also preserves structural-stability restrictions.

match Borrowing

Shared payload borrow:

match optional {
    Some(ref value) => Inspect(value)
    None => {}
}

Mutable payload borrow:

match optional {
    Some(ref mut value) => Reset(value)
    None => {}
}

The mutable form requires mutable authority over the reusable subject.

Pattern borrows are normally arm-scoped and are visible in that arm's where guard and body.

If a guarded candidate arm is rejected, borrow authority created only for that candidate ends before matching continues.

Borrowed subject authority never permits ownership move-out of a move-only payload.

Closure and Lambda Borrow Captures

Shared capture:

capture(ref value)

Mutable capture:

capture(ref mut value)

The closure environment keeps the corresponding borrowed authority live while it may still use the capture.

A closure containing a mutable-reference capture is move-only as a closure value.

Borrowed captures may escape only when every captured borrow remains valid for the complete possible escaped use.

capture(value) and capture(<-value) are copy/move operations, not borrow forms.

defer and Delayed Use

A registered defer may extend the effective future use of a value or reference until the deferred operation executes.

If the deferred operation will later read or borrow a Place, an earlier move, discard, destruction or invalidation that would make that future use invalid is rejected.

Place-sensitive defer analysis may narrow conflicts to proven sub-Places. Otherwise overlap is conservative.

Moving While Borrowed

Moving an owned Place is invalid while an incompatible overlapping borrow remains live.

let resource := OpenResource()
let view := ref resource

Consume(<-resource)    // invalid while view is live
Inspect(view)

Moving a proven disjoint sub-Place may remain legal when the active borrow does not overlap that sub-Place and the ownership/destruction rules permit the move.

discard While Borrowed

discard cannot destroy or invalidate a value while an incompatible overlapping borrow still requires it.

Discarding a reference holder ends that holder according to reference-value semantics. It does not discard or destroy the referent.

Replacement and Reinitialization

Replacing an available Place is invalid while an incompatible borrow overlaps the old value that replacement would destroy or invalidate.

let mut item := CreateItem()
let view := ref item

item = CreateItem()    // invalid while view is live

Reinitialization must likewise not invalidate a borrow that still legally designates the previous storage incarnation.

Collection backing replacement must reject or otherwise canonically invalidate incompatible references before replacement commits.

Destruction While Borrowed

Automatic destruction cannot occur while a live borrow still requires the value.

Borrow liveness may constrain the earliest legal destruction point. It does not transfer destruction responsibility from the owner to the reference holder.

Returned References Preserve Borrow Dependencies

A returned safe reference must satisfy the reference-origin and lifetime rules defined by the reference model.

A reference to ordinary function-local storage cannot be returned when that storage ends with the invocation.

Valid returned references may propagate authority from parameters, receivers, Arena/static domains, stable storage or other recognized origins.

FFI Borrowing

Where the FFI contract permits safe-reference parameters, ref T and ref mut T are non-null safe Sec borrows specialized to the foreign call boundary.

Such borrows are call-bounded unless an explicit foreign retention contract says otherwise.

Foreign code must not retain a call-bounded safe-reference address after the call.

Nullable pointers, retained raw addresses, unproven aliases and raw pointer returns use RawPtr[T] or another explicit FFI abstraction.

Physical, Addressed and Volatile Storage

Borrowing a Sec value and observing volatile or physical storage are separate semantics.

A volatile read may produce an ordinary Sec snapshot whose later borrows follow normal Sec borrowing rules.

A physical address, MMIO mapping, register width or volatile contract does not by itself grant safe ref or ref mut authority.

Safe borrowing from hardware-backed storage must satisfy the specialized platform contract as well as ordinary reference and borrowing guarantees.

Borrow Compatibility and Generation Validity Are Separate

Runtime generation or epoch validity does not grant borrow authority.

A matching generation does not make conflicting mutable/shared borrows legal.

Conversely, a compile-time-valid borrow may still require runtime generation validation when temporal storage validity cannot be proven statically.

Constrained targets may use address-only references when lifetime and invalidation are statically proven; the borrowing rules remain unchanged.

Borrowing Does Not Make Shared State Thread-Safe

Borrow correctness and concurrency correctness are separate requirements.

A borrow crossing a task, thread or other concurrency boundary must also satisfy send/share, data-race, synchronization and concurrency-memory rules.

ref mut T exclusivity is not by itself proof of safe cross-thread transfer or synchronization.

Generics, Interfaces and Opaque Calls

Generic specialization preserves ref and ref mut parameter modes exactly.

A concrete type becoming copyable does not change a borrowed parameter into a by-value parameter, and a move-only type does not make a by-value parameter a borrow.

Interface and callable compatibility preserve borrow mode as part of the signature.

Opaque or imported calls with insufficient retention/effect information are analyzed conservatively rather than assumed to have a shorter borrow.

Borrow Checking Does Not Require Runtime Borrow State

Borrow legality is resolved before low-level backend code generation.

Backend lowering may erase borrow bookkeeping entirely when safety is proven statically.

Runtime metadata may still exist for independent requirements such as reference epoch validation or bounds.

Such metadata is not a runtime borrow checker.

Conservative widening may reject more programs when alias analysis loses precision, but it must never make an unsafe alias pattern legal.

Borrow Diagnostics

Borrow diagnostics should explain the programmer's conflicting actions directly.

A useful diagnostic identifies:

• the Place the programmer tried to use;
• the requested action;
• the existing shared or mutable borrow;
• where that borrow was created or retained;
• why the Places overlap;
• why the borrow is still live;
• what safe restructuring is available.

Shared borrow blocks mutation

cannot modify `value` while a shared borrow is still live

the shared borrow was created here:
    let view := ref value

and is used later here:
    Inspect(view)

help: move the mutation after the final use of `view`
help: narrow the borrowed Place when only a disjoint sub-Place is needed

Mutable borrow blocks owner access

cannot read `item` through the owner while `writable` has exclusive authority

the mutable borrow was created here:
    let writable := ref mut item

help: access the value through `writable`
help: end the mutable borrow before reading through `item`

Two dynamic indexes may overlap

cannot create two mutable borrows of these indexed Places

`values[left]` and `values[right]` may refer to the same element

help: prove the indexes disjoint
help: restructure the operation so the borrows do not overlap

Availability is not borrow authority

`package.Payload` is available, but it cannot be accessed through the owner here

an overlapping mutable borrow is still active

help: use the active borrowed authority
help: end the borrow before direct owner access

Diagnostics should not tell the programmer to add explicit lifetime syntax. Sec has no programmer-written lifetime annotations for ordinary borrowing.

Best Practices

• Use shared borrowing when temporary read access is sufficient.
• Use mutable borrowing only for the smallest Place that genuinely needs exclusive mutation.
• Keep borrow holders' useful live ranges short; the compiler can end authority after final use.
• Borrow disjoint fields or ranges instead of the complete aggregate when independent access is required.
• Do not assume two runtime indexes are disjoint unless the program proves it.
• Pass owned Places directly to ref/ref mut parameters; call-bounded borrowing does not require ceremonial call-site markers.
• Use <- only for ownership transfer, never to express borrowing.
• Use reborrowing when temporarily delegating authority from an existing reference.
• End slice/view/reference use before structural operations that may relocate backing storage.
• Remember that is available says nothing about current borrow conflicts.
• Do not move, discard, replace or destroy storage while a live borrow still requires it.
• Remember that borrowing proves alias authority, not synchronization or thread safety.

Summary

• Borrowing grants temporary access authority without transferring ownership.
• Borrowing is compile-time aliasing and authority analysis.
• Sec does not require runtime borrow counters, borrow locks, garbage collection or explicit lifetime annotations.
• ref T represents shared borrowed authority.
• ref mut T represents exclusive mutable borrowed authority.
• Multiple compatible shared borrows may overlap.
• An overlapping shared and mutable borrow conflict.
• Two unrelated overlapping mutable borrows conflict.
• Mutable authority is not ownership authority.
• A shared borrow blocks overlapping mutation, replacement, move, discard, destruction and structural invalidation while live.
• A mutable borrow blocks competing direct owner reads and writes over the overlapping Place.
• Disjoint Places remain independently usable when the compiler proves non-overlap.
• Explicit local borrowing uses ref value or ref mut value.
• General explicit borrow creation requires a reusable addressable Place.
• Sec 0.1 does not generally extend arbitrary temporary-expression lifetimes for borrowing.
• An uninitialized, unavailable or unrefined conditionally available Place cannot be borrowed.
• Availability and borrow compatibility are independent dimensions.
• is available is not a borrow-status test.
• A Place may be available but temporarily inaccessible through its owner because a mutable borrow is live.
• A shared borrow may originate from immutable or mutable readable storage.
• A mutable borrow requires actual mutable authority.
• Borrow live ranges are derived from control flow and actual use rather than lexical scope alone.
• A borrow may end after its final reachable use when no surviving dependency remains.
• Copying a shared reference creates another borrow holder.
• Moving a mutable-reference holder transfers its borrow obligation rather than ending the referent borrow.
• Reborrowing creates narrower or equal authority from an existing reference.
• Passing ref mut T to a borrowed ref mut T parameter is a reborrow, not a move of the reference holder.
• During a child reborrow, the parent reference cannot exercise conflicting authority.
• After the child reborrow ends, the parent may become usable again.
• Borrow overlap is based on semantic Places and provenance.
• A whole Place overlaps every descendant Place.
• Distinct struct fields may be borrowed independently when proven disjoint.
• Properties are not automatically independent addressable storage.
• Distinct constant array indexes may be proven disjoint.
• Runtime indexes conservatively overlap unless disjointness is proven.
• Statically disjoint slice ranges may be borrowed independently.
• A compile-time-known empty range borrows no elements.
• Structural collection operations conflict with live borrows when they may invalidate backing storage.
• A parameter value: ref T receives shared borrowed authority.
• A parameter value: ref mut T receives mutable borrowed authority.
• The caller remains owner of the referent for both parameter forms.
• An owned Place may be passed directly to a borrowed parameter and create a call-bounded borrow.
• Call-bounded borrowing does not require a separate ref or ref mut call-site marker.
• Implicit call-site borrowing is not ownership transfer and must not be confused with <-.
• A call cannot create overlapping mutable argument borrows.
• A mutable argument borrow conflicts with overlapping shared/direct argument access while their live ranges overlap.
• Method receiver borrows obey the same overlap rules as equivalent Places.
• Borrow state is path-sensitive across branches.
• A borrow live on any continuing incoming path remains potentially live after a merge.
• Terminating paths do not contribute borrow state to later unreachable joins.
• Borrow validity must hold across loop backedges and later iterations.
• Some(ref value) creates a shared payload borrow in match.
• Some(ref mut value) creates a mutable payload borrow when the subject provides mutable authority.
• Match candidate borrows end when a guarded candidate is rejected.
• capture(ref value) retains a shared borrow in a closure.
• capture(ref mut value) retains a mutable borrow and blocks conflicting outer access.
• Escaping closures must not outlive their captured borrow origins.
• defer may extend the effective future use that keeps a borrow dependency live.
• Moving an owned Place is invalid while an incompatible overlapping borrow is live.
• discard cannot invalidate a live borrowed referent.
• Replacement and reinitialization cannot invalidate a still-required borrow.
• Automatic destruction cannot occur while a live borrow still requires the value.
• Returned references preserve their origin and borrow dependencies.
• FFI safe-reference parameters are call-bounded unless an explicit retention contract says otherwise.
• Physical addresses, MMIO mappings and volatile contracts do not automatically grant safe borrow authority.
• Generation/epoch validity and borrow compatibility are separate safety dimensions.
• Borrowing does not make shared state thread-safe.
• Generic specialization preserves declared borrow modes exactly.
• Borrow legality is resolved before low-level code generation.
• Backend lowering may erase borrow bookkeeping entirely when safety is statically proven.
• Runtime reference-validity metadata is not a runtime borrow checker.