ch:mutable-value-semantics: ch:mutable-value-semantics

Let the representation of $p$ have root ${\ell }_p$ and child locations ${\ell }_x,{\ell }_y$. Before copying, $$\mathrm{acc}(\pi ,{\ell }_p)=\{{\ell }_p,{\ell }_x,{\ell }_y\}.$$ The recursive copy chooses fresh ${\ell }_q,{\ell }_x^{\prime },{\ell }_y^{\prime }$, copies the two scalars, and produces $$\mathrm{acc}({\pi }^{\prime },{\ell }_q)=\{{\ell }_q,{\ell }_x^{\prime },{\ell }_y^{\prime }\},\mathrm{acc}({\pi }^{\prime },{\ell }_p)\cap \mathrm{acc}({\pi }^{\prime },{\ell }_q)=\varnothing .$$ Assignment to $q.x$ changes only ${\pi }^{\prime }({\ell }_x^{\prime })$, so ${\pi }^{\prime }({\ell }_x)=\pi ({\ell }_x)$ and $p.x$ is unchanged. A shallow copy that reused ${\ell }_x$ would put ${\ell }_x$ in both accessible sets, contradicting their disjointness.

The book check accepts at its first distinct fields, rejects when the first path ends, and accepts at the distinct constant indices. It rejects as soon as it meets the unknown index. Under the published relation, follows by reflexivity and right-field extension. The pairs and are unrelated. The published relation also fails to relate the final nested pair: its unknown-index rule relates the array paths, but it has no left congruence for extending both sides. Thus the book and source checks differ on the final pair.

Suppose ${\eta }_1(o)={\ell }_o$, the $p$-field of $\pi ({\ell }_o)$ is ${\ell }_p$, and the $x$-field of $\pi ({\ell }_p)$ is ${\ell }_x$. The lvalue trace begins with $$\frac{\begin{array}{c}{\eta }_1(o)={\ell }_o\\ \pi ({\ell }_o)=\mathsf{var}{v}_o\end{array}}{o{⟶}_{\mathsf{lv}}{\ell }_o^{\mathsf{var}}}\mathrm{PSS}-\mathrm{Name}.$$ Rule PSS-Struct lifts that step under $p$, after which $$\frac{\begin{array}{c}\pi ({\ell }_o)=\mathsf{var}[\dots ,{\ell }_p,\dots {]}^s\\ \mathrm{\Delta }(s)(p)=\mathsf{var}{s}_p\end{array}}{{\ell }_o^{\mathsf{var}}.p{⟶}_{\mathsf{lv}}{\ell }_p^{\mathsf{var}}}\mathrm{PSS}-\mathrm{Prop}$$ selects the first child. A second congruence step and PSS-Prop, using $\mathrm{\Delta }(s_p)(x)=\mathsf{var}\mathbb{Z}$, select ${\ell }_x^{\mathsf{var}}$. Both qualifier meets are $min(\mathsf{var},\mathsf{var})=\mathsf{var}$, so the displayed T-Inout derives the argument judgment. If $o.q.x$ follows a distinct first-field child ${\ell }_q$, the book comparison has an apart witness at $p\ne q$. Tree independence makes the subtrees rooted at ${\ell }_p$ and ${\ell }_q$ disjoint; their selected $x$-locations are therefore disjoint as well.

Let the ordinary array value have root ${\ell }_a$. Copying it creates a fresh root ${\ell }_a^{\prime }$ and fresh descendants; the callee’s ordinary parameter maps to ${\ell }_a^{\prime }$. Let the two access arguments resolve to ${\ell }_1,{\ell }_2$. Their callee parameters map directly to those existing locations. By the exercise hypothesis, ${\eta }_{\lambda }$ is already well formed. The copied set is disjoint from its roots and all caller roots by proposition 49.3; the borrowed sets are disjoint by lemma 49.6. Mutual freshness covers further ordinary parameters. The complete callee frame is well formed. Its $\mathsf{pop}$ drops ${\ell }_a^{\prime }$ and its descendants, but neither borrowed location.

If $a:[\mathbb{Z}]$, then $a[3]$ is well typed even when the runtime array has length two. Its evaluation reaches a designated out-of-bounds runtime error, one instance of the progress theorem’s error alternative. An overlapping access call is different: the conservative call premise fails, so the program has no typing derivation and is not deferred to runtime.

The premise is a finite small-step execution, from the initial state, of an expression also expressible in the natural semantics. The conclusion is a natural-semantics evaluation whose value equals the pointer-store value after readback. Copy-on-write needs a forward simulation showing that sharing and the uniqueness check preserve the abstract independent-copy result. LLVM lowering needs a typed source-to-IR simulation that relates source steps, allocation, and observable results to IR execution. The source’s semantic correspondence proves neither obligation.