ch:typestate: ch:typestate

The branch derivations have the common output $\varnothing$: $$\frac{\mathsf{drain}:(x:\mathsf{File}[\mathsf{open}])⊸\varnothing =P_D\in \mathrm{\Omega }}{f:\mathsf{File}[\mathsf{open}]⊢\mathsf{drain}(f)⊣\varnothing }\mathrm{TS}-\mathrm{Call}$$ and $$\frac{\begin{array}{c}\mathsf{eof}\in \{\mathsf{open},\mathsf{eof}\}\\ {\displaystyle \frac{\phantom{X}}{\varnothing ⊢\mathsf{return}⊣\varnothing }}\mathrm{TS}-\mathrm{Return}\end{array}}{f:\mathsf{File}[\mathsf{eof}]⊢\mathsf{close}f;\mathsf{return}⊣\varnothing }\mathrm{TS}-\mathrm{Close}$$ Rule TS-Read places these two derivations over the displayed body $P_D$, deriving the declared input state and common empty output.

After the first close the context is empty. The second command would require a decomposition containing $f:\mathsf{File}[q]$ for $q\in \{\mathsf{open},\mathsf{eof}\}$. No such binding exists, so TS-Close cannot apply.

Let $\eta (f)=\eta (g)=\ell$, $H(\ell )=\mathsf{open}$, and give both variables type $\mathsf{File}[\mathsf{open}]$. Closing $f$ removes $H(\ell )$, while a noninjective static account could retain $g:\mathsf{File}[\mathsf{open}]$. The successor maps fail agreement at $g$; therefore the first conclusion of lemma 52.2 is false.

Add $$\frac{\mathrm{\Delta },f:\mathsf{File}[\mathsf{suspended}]⊢P⊣{\mathrm{\Delta }}^{\prime }}{\mathrm{\Delta },f:\mathsf{File}[\mathsf{open}]⊢\mathsf{suspend}f;P⊣{\mathrm{\Delta }}^{\prime }}\mathrm{TS}-\mathrm{Suspend}$$ and the corresponding rule from suspended to open for resume. The dynamic rules update $H(\eta (f))$ to the target state. In each preservation case, agreement gives the source state, the heap update establishes the target state, and the typing premise supplies the continuation derivation.

The only rule concluding a term headed by read is TS-Read. Its input context contains $f:\mathsf{File}[\mathsf{open}]$. Finite-map equality cannot identify this binding with $f:\mathsf{File}[\mathsf{eof}]$, so inversion yields no premise and no derivation.

Read returns $\mathsf{File}[\mathsf{open}]\oplus \mathsf{File}[\mathsf{eof}]$. Sum elimination checks the left branch under the first summand and the right branch under the second, requiring both to produce the same output context ${\mathrm{\Delta }}^{\prime }$. The scrutinee and each branch must consume its file component affinely; otherwise one branch can retain a stale copy. No term introduces a dual endpoint or a blocking communication, so session fidelity and deadlock freedom are absent.