Mutable Value Semantics and inout Access

Prerequisites. Direct starred prerequisites: none. No later core chapter depends on this route.

Let $p,q:s$, where the structure $s$ has two mutable integer fields. Value assignment requires $$q:=p;q.x:=7⟹p.x\text{ is unchanged}.$$ Temporary mutable access imposes a different obligation: must be rejected because its two arguments expose overlapping parts of one representation. Copy independence proves the first claim; an access-conflict check must prove the second.

Trees, paths, and pointer stores

The calculus in this chapter is Swiftlet [RSZ^+22]. A structure context $\mathrm{\Delta }$ maps structure names to qualified field declarations, and a term context $\mathrm{\Gamma }$ maps names to qualified types. Qualifiers are $m\in \{\mathsf{let},\mathsf{var}\}$. The fragment needed below is A Swiftlet expression $e$ is an integer, array or structure literal, a name or path, a function declaration or call, a conditional, a binding, an assignment, a sequence, or a cast. The load-bearing forms are displayed by A runtime value in this fragment is $$v::=c\mid [{\ell }_1,\dots ,{\ell }_k]\mid [{\ell }_1,\dots ,{\ell }_k{]}^s\mid \lambda (\overrightarrow{x}:\overrightarrow{p},\eta ,e)\mid \mathsf{box}(\ell ).$$ For a well-typed stored value, ${\mathrm{typeof}}_{\mathrm{\Delta },\pi }(v)$ denotes its unique source type. A boxed value has source type $\mathsf{Any}$; its referenced stored value retains the concrete type used by a checked downcast. A path is an lvalue description, not a storable reference. The array-element qualifier is inherited from the path: an element reached through a $\mathsf{let}$ expression is immutable, while an element reached through a mutable path has qualifier $\mathsf{var}$.

A small-step state contains a pointer store $\pi$ and a nonempty stack $\eta ={\eta }_1,\dots ,{\eta }_n$, with ${\eta }_1$ the innermost, hence currently accessible, frame: $$\pi :\mathsf{Loc}\rightharpoonup \{\mathsf{let},\mathsf{var}\}\times \mathsf{Val},{\eta }_i:\mathsf{Name}\rightharpoonup \mathsf{Loc}.$$ Arrays and structures store the locations of their immediate parts.

Swiftlet excludes recursive structure declarations, so these representations are finite trees. The lvalue judgment and its five load-bearing rules are $$\mathrm{\Delta };\mathrm{\Gamma }{⊢}_{\mathsf{path}}r:m\tau ,$$ $$\frac{\mathrm{\Gamma }(x)=m\tau }{\mathrm{\Delta };\mathrm{\Gamma }{⊢}_{\mathsf{path}}x:m\tau }\mathrm{T}-\mathrm{Path}-\mathrm{Name}$$

$\mathrm{\Delta };\mathrm{\Gamma }⊢e:s$$\mathrm{\Delta }(s)(f)=m\tau$

$\mathrm{\Delta };\mathrm{\Gamma }{⊢}_{\mathsf{path}}e.f:\mathsf{let}\tau$

$\mathrm{\Delta };\mathrm{\Gamma }{⊢}_{\mathsf{path}}r:\mathsf{var}s$$\mathrm{\Delta }(s)(f)=\mathsf{var}\tau$

$\mathrm{\Delta };\mathrm{\Gamma }{⊢}_{\mathsf{path}}r.f:\mathsf{var}\tau$

$\mathrm{\Delta };\mathrm{\Gamma }⊢e_1:[\tau ]$$\mathrm{\Delta };\mathrm{\Gamma }⊢e_2:\mathbb{Z}$

$\mathrm{\Delta };\mathrm{\Gamma }{⊢}_{\mathsf{path}}{e}_1[e_2]:\mathsf{let}\tau$

$\mathrm{\Delta };\mathrm{\Gamma }{⊢}_{\mathsf{path}}r:\mathsf{var}[\tau ]$$\mathrm{\Delta };\mathrm{\Gamma }⊢e:\mathbb{Z}$

$\mathrm{\Delta };\mathrm{\Gamma }{⊢}_{\mathsf{path}}r[e]:\mathsf{var}\tau$

The source keeps immutable expression roots and mutable path roots separate; in particular, an immutable field cannot become a mutable access merely because its enclosing structure is mutable.

Lvalue evaluation, written $\mathrm{\Delta }⊢\pi ;\eta ;r{⟶}_{\mathsf{lv}}{\pi }^{\prime };{\eta }^{\prime };r^{\prime }$, starts with

${\eta }_1(x)=\ell$$\pi (\ell )=mv$

$\mathrm{\Delta }⊢\pi ;\eta ;x{⟶}_{\mathsf{lv}}\pi ;\eta ;{\ell }^m$

$\mathrm{\Delta }⊢\pi ;\eta ;r{⟶}_{\mathsf{lv}}{\pi }^{\prime };{\eta }^{\prime };r^{\prime }$

$\mathrm{\Delta }⊢\pi ;\eta ;r.f{⟶}_{\mathsf{lv}}{\pi }^{\prime };{\eta }^{\prime };r^{\prime }.f$

$m^{\prime }=min(m,m_i)$$\pi (\ell )=m[{\ell }_1,\dots ,{\ell }_k{]}^s$$\mathrm{\Delta }(s)(f_i)=m_i{\tau }_i$

$\mathrm{\Delta }⊢\pi ;\eta ;{\ell }^m.f_i{⟶}_{\mathsf{lv}}\pi ;\eta ;{\ell }_i^{m^{\prime }}$

$\pi (\ell )=m[{\ell }_1,\dots ,{\ell }_k]$

$\mathrm{\Delta }⊢\pi ;\eta ;{\ell }^m[c]{⟶}_{\mathsf{lv}}\pi ;\eta ;{\ell }_{c+1}^m$

The omitted PSS-Array and PSS-Index congruence rules first reduce the array path and its index. The meet $m^{\prime }=min(m,m_i)$ in PSS-Prop is the dynamic reason that an immutable field remains immutable below a mutable root.

Proof of Lemma 49.2 — Unique descent

Proof. Induct on the path. PSS-Name selects the root. A field or element step follows one child of the current tree, so the selected accessible set is a subset of its predecessor’s. Subsets of disjoint root representations remain disjoint. ◻

Swiftlet’s helper $\mathrm{copy}(\pi ,v)=({\pi }^{\prime },v^{\prime })$ recursively allocates fresh locations for compound values, closures, and boxed $\mathsf{Any}$ values.

Proof of Proposition 49.3 — Copy produces an independent value

Proof. Type preservation is the source’s Lemma A.2. For independence, induct on the definition of $\mathrm{copy}$. A compound case chooses fresh child locations and invokes the induction hypothesis once for each child. The finite union in definition 49.1 is disjoint from the old roots and from the unions produced by earlier copies. ◻

The source states type preservation as Lemma A.2 and the corresponding memory preservation fact as Lemma A.3. Mutual freshness of successive copies is the additional invariant proved above.

The source relation and a sound repair

Racordon et al.’s Definition 4.1 writes . Despite the suggestive glyph, its fourth rule makes it an access-relatedness relation, not literal syntactic prefix. It is the least reflexive, transitive relation closed by and Here $\mathrm{const}(e)$ holds exactly when $e$ is an integer literal, as in the paper’s deliberately conservative definition. Thus and may be separated, whereas when either index is unknown.

The published relation does not close related paths on the left. Consequently it relates to but need not relate to . If $i$ and $j$ evaluate to the same index, those nested paths alias. The two-sentence proof of source Lemma A.1 does not resolve this case. We therefore do not use that lemma at its unrestricted published signature.

This conservative repair deliberately rejects : the unknown array choice is settled before the distinct fields are reached. It also rejects unknown indices below an already distinct root or component. It is stronger than Definition 4.1 and is not attributed to the source.

Proof of Lemma 49.6 — Static separation implies physical disjointness

Proof. Because both component lists are stable, path evaluation performs only PSS-Name, congruence, PSS-Prop, and PSS-Elem; it leaves the store unchanged. Different roots are handled by lemma 49.2. On a common root, induction over the equal prefix shows that both evaluations have selected the same location after each pair of equal fields or equal literal indices. The first unequal fields or literal indices therefore select distinct children of that one tree. Their subtrees are disjoint, and further stable descent preserves disjointness. Every case without such a witness is classified as a conflict. ◻

For the opening call, because the first path ends before the second. By contrast, distinct fields and are separated at their first unequal component.

Calling by temporary access

An access argument must denote a mutable path: Assignment has the same qualifier boundary: $$\frac{\begin{array}{c}\mathrm{\Delta };\mathrm{\Gamma }{⊢}_{\mathsf{path}}r:\mathsf{var}\tau \\ \mathrm{\Delta };\mathrm{\Gamma }⊢e:\tau \end{array}}{\mathrm{\Delta };\mathrm{\Gamma }⊢r=e:\mathsf{unit}}\mathrm{T}-\mathrm{Assign}$$ For example, if $\mathrm{\Delta }(s)(x)=\mathsf{var}\mathbb{Z}$ and $\mathrm{\Gamma }(o)=\mathsf{var}s$, then

Let a closure have parameters $x_i:p_i$, captured frame ${\eta }_{\lambda }$, and body $e$. The call step copies every ordinary value into a mutually fresh root ${\ell }_i$, maps every access parameter directly to the location selected by , and checks pairwise physical disjointness. Its new innermost frame extends ${\eta }_{\lambda }$. The generated form $e;\mathsf{pop}L$ records exactly the fresh copied roots $L$. Put $$I_{\mathsf{cpy}}=\{i\mid p_i={\tau }_i\},I_{\mathsf{ref}}=\{i\mid p_i=\mathsf{inout}{\tau }_i\}.$$ The static and dynamic call rules expose the two corresponding premises: $$\frac{\begin{array}{c}\mathrm{\Delta };\mathrm{\Gamma }⊢e:(p_1,\dots ,p_k)\to \tau \\ (\mathrm{\Delta };\mathrm{\Gamma }{⊢}_{\mathsf{arg}}{a}_i:p_i{)}_{1\le i\le k}\\ {\mathsf{exclusive}}_{\mathsf{B}}(a_1,\dots ,a_k)\end{array}}{\mathrm{\Delta };\mathrm{\Gamma }⊢e(a_1,\dots ,a_k):\tau }\mathrm{T}-\mathrm{Call}$$ Here ${\mathsf{exclusive}}_{\mathsf{B}}$ is exactly definition 49.5, including stability of every access path. After evaluation has produced a closure $\lambda (\overrightarrow{x}:\overrightarrow{p},{\eta }_{\lambda },e)$, ordinary values $v_i$, and access locations ${\ell }_i$, the root call step is $$\frac{\begin{array}{c}\{{\ell }_i\mid i\in I_{\mathsf{cpy}}\}\cap \mathrm{dom}(\pi )=\varnothing \\ \mathrm{\forall }i\ne j\in I_{\mathsf{ref}}.\mathrm{acc}(\pi ,{\ell }_i)\cap \mathrm{acc}(\pi ,{\ell }_j)=\varnothing \\ {\pi }^{\prime }=\pi [{\ell }_i\mapsto \mathsf{let}{v}_i\mid i\in I_{\mathsf{cpy}}]\\ {\eta }^{\prime }={\eta }_{\lambda }[x_i\mapsto {\ell }_i\mid i\in I_{\mathsf{cpy}}\cup I_{\mathsf{ref}}]\end{array}}{\mathrm{\Delta }⊢\pi ;\eta ;\lambda (\overrightarrow{x}:\overrightarrow{p},{\eta }_{\lambda },e)(\overrightarrow{v})⟶{\pi }^{\prime };{\eta }^{\prime },\eta ;e;\mathsf{pop}\{{\ell }_i\mid i\in I_{\mathsf{cpy}}\}}\mathrm{ESS}-\mathrm{Call}$$ In the conservative variant, the stable static premise lets lemma 49.6 establish the dynamic disjointness premise in the single final store: reducing access arguments performs no index-expression steps. On return, $${\pi }_0;{\eta }^{\prime },\eta ;v;\mathsf{pop}L⟶{\mathrm{drop}}^{\ast }({\pi }_0,L);\eta ;v,$$ where ${\mathrm{drop}}^{\ast }$ recursively removes the representations rooted at $L$. Borrowed caller locations are absent from $L$. Assignment reaches a root step only through a mutable lvalue: $$\frac{\begin{array}{c}\pi (\ell )=m{v}_0\\ {\pi }_0=\mathrm{drop}(\pi ,v_0)\\ {\pi }^{\prime }={\pi }_0[\ell \mapsto \mathsf{var}v]\end{array}}{\mathrm{\Delta }⊢\pi ;\eta ;{\ell }^{\mathsf{var}}=v;e⟶{\pi }^{\prime };\eta ;e}\mathrm{ESS}-\mathrm{Assign}$$ Successful checked downcast exposes the concrete stored value and copies it: $$\frac{\begin{array}{c}\tau \ne \mathsf{Any}\\ \pi (\ell )=\mathsf{let}v\\ {\mathrm{typeof}}_{\mathrm{\Delta },\pi }(v)=\tau \\ \mathrm{copy}(\pi ,v)=({\pi }^{\prime },v^{\prime })\end{array}}{\mathrm{\Delta }⊢\pi ;\eta ;\mathsf{box}(\ell )\mathsf{as}\tau ;e⟶{\pi }^{\prime };\eta ;v^{\prime };e}\mathrm{ESS}-\mathrm{Downcast}$$ Two and only two dynamic side-condition failures are designated runtime errors: a downcast $\mathsf{box}(\ell )\mathsf{as}\tau$, where $\pi (\ell )=\mathsf{let}v$ but ${\mathrm{typeof}}_{\mathrm{\Delta },\pi }(v)\ne \tau$, and an array access at a literal $c$ with or $c\ge k$. They are the failed premises of ESS-Downcast and PSS-Elem, respectively. No other stuck state is included in the error alternative below.

No rule turns into an ordinary returnable value. This is temporary, second-class access, not a calculus of first-class borrows.

Independence and type safety

Expression reduction is $\mathrm{\Delta }⊢\pi ;\eta ;e⟶{\pi }^{\prime };{\eta }^{\prime };e^{\prime }$. It includes evaluation contexts, allocation, copy, path evaluation, call, assignment, cast, and pop.

Proof of Theorem 49.9 — Safety of the conservative Swiftlet variant

Proof. Follow the source inductions for Lemmas 4.1–4.2, with one repaired case. In a call, lemma 49.6 proves the dynamic disjointness premise. By proposition 49.3, the copied roots are fresh from one another and from all borrowed roots. Assignment uses T-Assign, PSS-Prop, and ESS-Assign, so it can update only a location reached with qualifier $\mathsf{var}$. Pop invokes ${\mathrm{drop}}^{\ast }$ only on copied roots. The remaining nine source syntax families—bindings, reads, literals, functions, conditionals, sequences, casts, evaluation contexts, and pop—are the finite case analysis printed in the proofs of Lemmas 4.1–4.2. They do not use the repaired call premise; their induction hypotheses reconstruct the corresponding rule and memory-typing judgment. ◻

Proof of Corollary 49.10 — Static guarantee

Proof. Induct on the reduction prefix. Preservation maintains memory well-typedness. Inversion of T-Assign gives a mutable path, PSS-Prop propagates the meet of root and field qualifiers, and ESS-Assign requires the final ${\ell }^{\mathsf{var}}$; together these prove that no immutable cell is overwritten. Inversion of ESS-Call gives pairwise disjointness for every exposed inout representation. ◻

The source states corresponding progress and preservation results as Lemmas 4.1–4.2 and packages them as Theorem 4.1. Because its access relation has the nested-index gap isolated above, this chapter does not claim that the published proof establishes the unrestricted theorem.

Representation correspondence and boundaries

Swiftlet also has a value-tree semantics in which abstract copying is the identity. A readback $|v{|}_{\mathrm{\Delta }}^{\pi }$ expands a pointer-store value.

Proof of Theorem 49.11 — Representation correspondence, source sketch

Imported proof. The JOT article labels this Theorem 4.2 and gives an induction-on-run-length proof sketch. It does not verify LLVM lowering, stack allocation, copy-on-write, reference counting, or any particular compiler revision. The exact source is Racordon et al.’s Theorem 4.2, with the natural and small-step semantics of its Sections 4.1–4.5 [RSZ^+22]. ◻

Current Swift access enforcement and Hylo yielding projections are comparison boundaries, not metatheory for Swiftlet. A yielding projection temporarily opens a component of a value to a caller without turning that component into an independently owned result. The pinned Swift design archive documents exclusive-access and yielding-access proposals [Swi17]; Hylo’s richer checker is described by Racordon and Abrahams [RA23]. Racordon’s dissertation gives background on assignment semantics, but owns none of the Swiftlet results [Rac19].

Sources.

Sections 4.1–4.5, Definitions 4.1–4.2, Lemmas 4.1–4.2, Theorems 4.1–4.2, and Appendix A of Racordon et al. own the published calculus and proof claims [RSZ^+22]. The conservative conflict relation and its disjointness proof are book-owned repairs.