Swiftlet access discipline

The Chapter 49 fragment fixes $$p::=\tau \mid \mathsf{inout}\tau ,r::=x\mid e.f\mid e_1[e_2],\pi :\mathsf{Loc}\rightharpoonup \{\mathsf{let},\mathsf{var}\}\times \mathsf{Val}.$$ Reachability is the reflexive subtree closure $$\mathrm{acc}(\pi ,\ell )=\{\ell \}\cup \bigcup _i\mathrm{acc}(\pi ,{\ell }_i)$$ when the value at $\ell$ contains child locations ${\ell }_i$. Roots named by distinct bindings in the currently accessible frame must have pairwise disjoint accessible sets.

Path typing preserves the qualifier carried by a variable and distinguishes immutable expressions from mutable paths:

$\mathrm{\Gamma }(x)=m\tau$

$\mathrm{\Delta };\mathrm{\Gamma }{⊢}_{\mathsf{path}}x:m\tau$

$\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$

Path selection is a separate small-step judgment. Its complete named rules are

${\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 access and assignment rules are

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

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

$\mathrm{\Delta };\mathrm{\Gamma }⊢r=e:\mathsf{unit}$

The published access relation is the least reflexive, transitive relation closed by right field/index extension,

and It lacks the left closure needed for nested unknown-index descendants. The book therefore uses definition 49.4. It accepts only paths whose array indices are literals, compares components from the root, and requires $$i\ne j\in I_{\mathsf{ref}}⟹\mathrm{\neg }(a_i{\bowtie }_{\mathsf{B}}{a}_j).$$ Ordinary arguments are recursively copied into mutually fresh callee roots. Access arguments map directly to existing mutable locations, and generated $\mathsf{pop}$ drops only copied roots. Rule T-Call carries the book exclusivity premise; ESS-Call carries the resulting physical-disjointness premise in the final store.

$\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)$

$\mathrm{\Delta };\mathrm{\Gamma }⊢e(a_1,\dots ,a_k):\tau$

$\{{\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}}]$

$\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}}\}$

Assignment reaches the root only when its path has retained the mutable qualifier:

$\pi (\ell )=m{v}_0$${\pi }_0=\mathrm{drop}(\pi ,v_0)$${\pi }^{\prime }={\pi }_0[\ell \mapsto \mathsf{var}v]$

$\mathrm{\Delta }⊢\pi ;\eta ;{\ell }^{\mathsf{var}}=v;e⟶{\pi }^{\prime };\eta ;e$

Checked downcast succeeds only by $$\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}.$$ Failure of its concrete-type premise is one of the two runtime-error forms; failure of PSS-Elem’s literal bound is the other.