Ownership, borrowing, and affine protocols

The finite protocol of chapter 19 has states $$q::=\mathsf{O}(A)\mid \mathsf{D}\mid {\mathsf{S}}_B(A)\mid {\mathsf{X}}_{\overline{\alpha }}(A),$$ where $B$ is a nonempty finite set and $\overline{\alpha }$ a nonempty lifetime stack. The complete state-changing rules are

$k\notin \mathrm{dom}(\mathrm{\Omega })$

$\mathcal{L};\mathrm{\Omega },h:\mathsf{O}(A)⊢\mathsf{move}h\mathsf{as}k\Rightarrow \mathcal{L};\mathrm{\Omega },h:\mathsf{D},k:\mathsf{O}(A)$

$\mathcal{L};\mathrm{\Omega },h:\mathsf{O}(A)⊢\mathsf{drop}h\Rightarrow \mathcal{L};\mathrm{\Omega },h:\mathsf{D}$

$\alpha \notin \mathcal{L}$

$\mathcal{L};\mathrm{\Omega },h:\mathsf{O}(A)⊢{\mathsf{beginS}}_{\alpha }h\Rightarrow \mathcal{L}\alpha ;\mathrm{\Omega },h:{\mathsf{S}}_{\{\alpha \}}(A)$

$\alpha \notin \mathcal{L}$

$\mathcal{L};\mathrm{\Omega },h:{\mathsf{S}}_B(A)⊢{\mathsf{beginS}}_{\alpha }h\Rightarrow \mathcal{L}\alpha ;\mathrm{\Omega },h:{\mathsf{S}}_{B\cup \{\alpha \}}(A)$

$B\setminus \{\alpha \}\ne \varnothing$

$\mathcal{L}\alpha ;\mathrm{\Omega },h:{\mathsf{S}}_B(A)⊢{\mathsf{endS}}_{\alpha }h\Rightarrow \mathcal{L};\mathrm{\Omega },h:{\mathsf{S}}_{B\setminus \{\alpha \}}(A)$

$B=\{\alpha \}$

$\mathcal{L}\alpha ;\mathrm{\Omega },h:{\mathsf{S}}_B(A)⊢{\mathsf{endS}}_{\alpha }h\Rightarrow \mathcal{L};\mathrm{\Omega },h:\mathsf{O}(A)$

$\alpha \notin \mathcal{L}$

$\mathcal{L};\mathrm{\Omega },h:\mathsf{O}(A)⊢{\mathsf{beginX}}_{\alpha }h\Rightarrow \mathcal{L}\alpha ;\mathrm{\Omega },h:{\mathsf{X}}_{\alpha }(A)$

$\beta \notin \mathcal{L}$

$\mathcal{L};\mathrm{\Omega },h:{\mathsf{X}}_{\overline{\alpha }}(A)⊢{\mathsf{reborrowX}}_{\beta }h\Rightarrow \mathcal{L}\beta ;\mathrm{\Omega },h:{\mathsf{X}}_{\overline{\alpha }\beta }(A)$

$\overline{\alpha }\ne ϵ$

$\mathcal{L}\beta ;\mathrm{\Omega },h:{\mathsf{X}}_{\overline{\alpha }\beta }(A)⊢{\mathsf{endX}}_{\beta }h\Rightarrow \mathcal{L};\mathrm{\Omega },h:{\mathsf{X}}_{\overline{\alpha }}(A)$

$\mathcal{L}\alpha ;\mathrm{\Omega },h:{\mathsf{X}}_{\alpha }(A)⊢{\mathsf{endX}}_{\alpha }h\Rightarrow \mathcal{L};\mathrm{\Omega },h:\mathsf{O}(A)$

Access and sequencing are

$q\in \{\mathsf{O}(A),{\mathsf{S}}_B(A),{\mathsf{X}}_{\overline{\alpha }}(A)\}$

$\mathcal{L};\mathrm{\Omega },h:q⊢\mathsf{read}h\Rightarrow \mathcal{L};\mathrm{\Omega },h:q$

$q\in \{\mathsf{O}(A),{\mathsf{X}}_{\overline{\alpha }}(A)\}$$v:A$

$\mathcal{L};\mathrm{\Omega },h:q⊢\mathsf{write}hv\Rightarrow \mathcal{L};\mathrm{\Omega },h:q$

$\mathcal{L};\mathrm{\Omega }⊢c_1\Rightarrow {\mathcal{L}}_1;{\mathrm{\Omega }}_1$${\mathcal{L}}_1;{\mathrm{\Omega }}_1⊢c_2\Rightarrow {\mathcal{L}}_2;{\mathrm{\Omega }}_2$

$\mathcal{L};\mathrm{\Omega }⊢c_1;c_2\Rightarrow {\mathcal{L}}_2;{\mathrm{\Omega }}_2$

The runtime realization performs the same mode update. Move transfers the payload to the fresh destination, drop removes it, read leaves it unchanged, and write replaces it by the displayed closed value. Agreement is $\mathcal{L};R{\vDash }_{\mathsf{own}}\mathrm{\Omega }$; it requires equal domains and modes, well-typed live payloads, and every lifetime in a shared set or exclusive stack to occur in $\mathcal{L}$ with the stack-induced order.

The affine target representation for the local simulation is $$\mathcal{R}(\mathcal{L};\mathrm{\Omega })=\mathsf{Life}(\mathcal{L})\otimes {\mathsf{Cap}}_{h_1}(\mathrm{\Omega }(h_1))\otimes \cdots \otimes {\mathsf{Cap}}_{h_m}(\mathrm{\Omega }(h_m)),$$ where $h_1,\dots ,h_m$ is the ordered domain of $\mathrm{\Omega }$. Each primitive protocol derivation contributes an affine constant from the representation of its premise to the representation of its conclusion; sequencing is affine composition. The primitive contracts on the canonical input in one target step.

The selected Affe rules are $$\frac{\phantom{X}}{C⊢\mathrm{\Gamma },x:\sigma =({\mathrm{\Gamma }}_1,[x:\sigma {]}_b^n)⋉({\mathrm{\Gamma }}_2,x:\sigma )}\mathrm{Susp},$$

$[x:{\tau }_x{]}_b^n\in \mathrm{\Gamma }$$C{⊢}_x\mathrm{\Gamma }{⇝}_{\mathsf{reg}}{\mathrm{\Gamma }}^{\prime }$$C\mid {\mathrm{\Gamma }}^{\prime }⊢e:\tau$$C⊢\mathrm{kind}(\tau )\le {\mathsf{L}}_{n-1}$

$C\mid \mathrm{\Gamma }⊢\{|e|{\}}_{x,b}^n:\tau$

$C_x,{\tau }_x=\mathrm{inst}(\mathrm{\Gamma },\sigma )$$C⊢C_x\wedge \mathrm{drop}(\mathrm{\Gamma }\setminus x)$

The paper-facing Pure Borrow interface includes Pure Borrow keeps its two executions distinct. A mutative configuration is $(H;\mu ;x)$ and steps by ${⟼}_{\mathsf{m}}$; a denotational configuration is $(G;x)$ and steps by ${⟼}_{\mathsf{d}}$. Allocation, update, lifetime end, and reclamation respectively mutate global memory in the first semantics and construct a pure reference, update a borrow history, move the history to a dead token, and replay that history in the second. The association judgment is $M{\bowtie }_{A}D$. These signatures do not identify either execution with the finite protocol above.