is type inference feasible?
To answer these questions, we evaluated our prototype implementation
on two sets of benchmarks.Our experiments and the ConSORT source code are available
at https://www.fos.kuis.kyoto-u.ac.jp/projects/consort/.
The first set is adapted from JayHorn [1]}, [2]},
a verification tool for Java.
This test suite contains a combination of 82 safe and unsafe programs written in
Java. We chose this benchmark suite as, like ConSORT, JayHorn
is concerned with the automated verification of
programs in a language with mutable, aliased memory cells.
Further, although some of their benchmark programs tested Java
specific features, most could be adapted
into our low-level language.
The tests we could adapt provide a comparison with existing state-of-the-art
verification techniques.
A detailed breakdown of the adapted benchmark suite can be found in tab:breakdown.
<TABLE>The original JayHorn paper includes two additional benchmark sets, Mine Pump and CBMC.
Both our tool and recent JayHorn versions time out on the Mine Pump benchmark. Further,
the CBMC tests were either subsumed by our own test programs, tested Java specific
features, or tested program synthesis functionality. We therefore omitted both of these
benchmarks from our evaluation.
The second benchmark set consists of data structure
implementations and microbenchmarks written directly in our low-level
imperative language. We developed this suite to
test the expressive power of our type system and inference.
The programs included in this suite are:

Array-List Implementation of an unbounded list backed by an array.

Sorted-List Implementation of a mutable, sorted list maintained with an in-place insertion sort algorithm.

Shuffle Multiple live references are used to mutate the same location in program memory as in exmp:shuffle-example.

Mut-List Implementation of general linked lists with a clear operation.

Array-Inv A program which allocates a length \(n\)  array and writes the value \(i\)  at every index \(i\) .

Intro2 The motivating program shown in fig:hard-loop in sec:intro.

We introduced unsafe mutations to these programs to
check our tool for unsoundness and translated these programs
into Java for further comparison with JayHorn.
Our benchmarks and JayHorn's require a small number of trivially identified alias annotations.
The adapted JayHorn benchmarks contain a total of 6
annotations; the most for any individual test was 3.
The number of annotations required for our benchmark suite are shown in column
Ann. of tab:jh-results.
We first ran ConSORT on each program in our benchmark suite and ran version 0.7 of
JayHorn on the corresponding Java version. We recorded the final verification
result for both our tool and JayHorn. We also collected the
end-to-end runtime of ConSORT for each test;
we do not give a performance comparison with
JayHorn given the many differences in target languages.
For the JayHorn suite, we first ran our tool on the adapted version of
each test program and ran JayHorn on the original Java version. We also did not
collect runtime information for this set of experiments because our goal
is a comparison of tool precision, not performance.
All tests were run on a machine with 16 GB RAM and 4 Intel i5 CPUs at 2GHz
and with a timeout of 60 seconds (the same timeout
was used in [1]}). We used ConSORT's parallel backend (sec:infr)
with Z3 version 4.8.4, HoICE version 1.8.1, and Eldarica version 2.0.1 and JayHorn's Eldarica backend.
<TABLE>Results
The results of our experiments are shown in tab:jh-results. On the JayHorn benchmark
suite ConSORT performs competitively with JayHorn, correctly identifying 29 of the 32 safe programs
as such. For all 3 tests on which ConSORT timed out after 60 seconds, JayHorn also timed out
(column T/O).
For the unsafe programs, ConSORT correctly identified all programs as unsafe within 60 seconds;
JayHorn answered Unknown for 7 tests (column Imp.).
On our own benchmark set, ConSORT correctly verifies all safe versions
of the programs within 60 seconds. For the unsafe variants,
ConSORT was able to quickly and definitively determine these programs unsafe.
JayHorn times out on all tests except for Shuffle and ShuffleBUG (column JH).
We investigated the cause of time outs and discovered that after verification failed
with an unbounded heap model, JayHorn attempts verification on increasingly
larger bounded heaps. In every case, JayHorn exceeded the 60 second timeout
before reaching a preconfigured limit on the heap bound. This result suggests JayHorn struggles in the presence
of per-object invariants and unbounded allocations;
the only two tests JayHorn successfully analyzed contain just a single object allocation.
We do not believe
this struggle is indicative of a shortcoming in JayHorn's implementation,
but stems from the fundamental limitations of JayHorn's memory representation.
Like many verification tools (see sec:rw), JayHorn uses a single, unchanging
invariant to for every object allocated at the same syntactic location;
effectively, all objects allocated at the same location
are assumed to alias with one another.
This representation cannot, in general, handle programs with different
invariants for distinct objects that evolve over time.
We hypothesize other tools that adopt a similar approach will exhibit
the same difficulty.

Related Work
The difficulty in handling programs with mutable references and
aliasing has been well-studied. Like JayHorn, many approaches model the heap explicitly
at verification time, approximating concrete heap locations with allocation site
labels [1]}, [2]}, [6]}, [7]}, [8]};
each abstract location is also associated with a refinement.
As abstract locations summarize many concrete locations, this approach
does not in general admit strong updates and flow-sensitivity; in particular, the refinement
associated with an abstract location is fixed for the lifetime of the program.
The techniques cited above include various workarounds for this limitation. For
example, [7]}, [6]} temporarily allows
breaking these invariants through a distinguished program name
as long as the abstract location is not accessed through another name.
The programmer must therefore eventually bring the invariant back in sync with the summary location.
As a result, these systems ultimately cannot precisely handle programs that require
evolving invariants on mutable memory.
A similar approach was taken in
CQual [11]} by Aiken et al. [12]}.
They used an explicit restrict binding for pointers.
Strong updates are permitted through pointers bound
with restrict, but the program is forbidden from
using any pointers which share an allocation site while the restrict binding is live.
A related technique used in the field of object-oriented verification is
to declare object invariants at the class level and allow these
invariants on object fields to be broken during a limited period of time
[13]}, [14]}. In particular, the work on
Spec# [13]} uses an ownership system which tracks
whether object \(a\)  owns object \(b\) ; like ConSORT's ownership system,
these ownerships contain the effects of mutation. However, Spec#'s ownership
is quite strict and does not admit references to \(b\)  outside of the owning object \(a\) .
Viper [16]}, [17]}
(and its related projects [18]}, [19]}) uses
access annotations (expressed as permission predicates) to explicitly transfer access/mutation
permissions for references between static program names. Like ConSORT,
permissions may be fractionally transferred, allowing temporary shared, immutable
access to a mutable memory cell. However,
while ConSORT automatically infers many ownership transfers, Viper requires extensive
annotations for each transfer.
F*, a dependently typed dialect of ML, includes an update/select
theory of heaps and requires explicit annotations summarizing the heap
effects of a method
[20]}, [21]}, [22]}.
This approach enables modular reasoning and precise specification of
pre- and post-conditions with respect to the heap, but precludes full automation.
The work on rely–guarantee reference types by Gordon et
al. [23]}, [24]} uses refinement
types in a language mutable references and aliasing.
Their approach extends reference types with rely/guarantee predicates;
the rely predicate describes possible mutations via aliases,
and the guarantee predicate describes the admissible mutations through the current reference.
If two references may alias, then the guarantee predicate of one
reference implies the rely predicate of the other and vice versa.
This invariant is maintained with a splitting operation that
is similar to our \(+\)  operator.
Further, their type system allows strong updates to reference refinements
provided the new refinements are preserved by the rely predicate.
Thus, rely–guarantee refinement support multiple
mutable, aliased references with non-trivial refinement information. Unfortunately this
expressiveness comes at the cost of automated inference and verification; an embedding
of this system into Liquid Haskell [25]} described in
[24]} was forced to sacrifice strong updates.
Work by Degen et al. [27]} introduced linear state annotations to Java.
To effect strong updates in the presence of aliasing, like ConSORT,
their system requires annotated memory locations are mutated only through
a distinguished reference. Further, all aliases of this mutable reference give
no information about the state of the object much like our 0 ownership pointers.
However, their system cannot handle multiple, immutable aliases with non-trivial
annotation information; only the mutable reference may
have non-trivial annotation information.
The fractional ownerships in ConSORT and their counterparts in
[28]}, [29]} have a clear relation to
linear type systems. Many authors have explored the use of linear type
systems to reason in contexts with aliased mutable references
[30]}, [31]}, [32]}, and
in particular with the goal of supporting strong updates
[33]}. A closely related approach is RustHorn by
Matsushita et al. [34]}. Much like
ConSORT, RustHorn uses CHC and linear aliasing information for
the sound and—unlike ConSORT—complete verification of
programs with aliasing and mutability. However, their approach depends on Rust's
strict borrowing discipline, and cannot handle programs
where multiple aliased references are used
in the same lexical region. In contrast, ConSORT supports
fine-grained, per-statement changes in mutability and even further
control with alias annotations, which allows it to verify larger
classes of programs.
The ownerships of ConSORT also have
a connection to separation logic [35]};
the separating conjunction isolates write effects to local subheaps,
while ConSORT's ownership system isolates effects to local updates of pointer types.
Other researchers have used separation logic to precisely
support strong updates of abstract state.
For example, in work by Kloos et al. [36]}
resources are associated with static, abstract names; each
resource (represented by its static name) may be owned (and thus,
mutated) by exactly one thread. Unlike ConSORT, their ownership
system forbids even temporary immutable,
shared ownership, or transferring ownerships at arbitrary program points.
An approach proposed by Bakst and Jhala [37]}
uses a similar technique,
combining separation logic with refinement types. Their approach gives
allocated memory cells abstract names, and associates these names with
refinements in an abstract heap. Like the approach of Kloos et al.
and ConSORT's ownership 1 pointers, they
ensure these abstract locations are distinct
in all concrete heaps, enabling sound, strong updates.
The idea of using a rational number to express permissions to access a
reference dates back to the type system of fractional
permissions by Boyland [38]}. His work used
fractional permissions to verify race freedom of a concurrent program
without a may-alias analysis. Later,
Terauchi [39]} proposed a type-inference
algorithm that reduces typing constraints to a set of linear
inequalities over rational numbers. Boyland's idea also inspired a
variant of separation logic for a concurrent programming
language [40]} to express sharing of read
permissions among several threads. Our previous
work [28]}, [29]}, inspired by that
in [39]}, [40]}, proposed methods for type-based
verification of resource-leak freedom, in which a rational number
expresses an obligation to deallocate certain resource, not
just a permission.
The issue of context-sensitivity (sometimes called polyvariance)
is well-studied in the field of abstract interpretation
(e.g., [45]}, [46]}, [47]}, [48]}, [49]}, see [50]}
for a recent survey).
Polyvariance has also been used in type systems to assign
different behaviors to the same function depending on its call site
[51]}, [52]}, [53]}.
In the area of refinement type systems, Zhu and Jagannathan developed
a context-sensitive dependent type system for a functional language [54]}
that indexed function types by unique labels attached to call-sites. Our
context-sensitivity approach was inspired by this work.
In fact, we could have formalized context-polymorphism within the framework of full dependent
types, but chose the current presentation for simplicity.

Conclusion
We presented ConSORT, a novel type system for safety verification of imperative programs with mutability
and aliasing. ConSORT is built upon the novel combination of fractional ownership types and refinement
types. Ownership types flow-sensitively and precisely track the existence of mutable aliases. ConSORT admits sound strong updates by discarding refinement information on mutably-aliased references as
indicated by ownership types.
Our type system is amenable
to automatic type inference; we have implemented a prototype of this inference tool and found it can verify several
non-trivial programs and outperforms a state-of-the-art program verifier.
As an area of future work, we plan to investigate using fractional ownership types to soundly allow refinements that mention memory
locations.
Acknowledgments
The authors would like to the reviewers for their thoughtful
feedback and suggestions, and Yosuke Fukuda and Alex Potanin for their feedback on early drafts.
This work was supported in part by JSPS KAKENHI, grant numbers JP15H05706 and JP19H04084,
and in part by the JST ERATO MMSD Project.
Open Access This chapter is licensed under the terms of the Creative CommonsAttribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intendeduse is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
<FIGURE>
<FIGURE><FIGURE>
Proof of Type Soundness (thm:soundness)
We first define a typing relation for machine configurations \( \left\langle { \mathit {H} , \mathit {R} , \vec{F} , \mathit {e} }\right\rangle  \)  as shown in
fig:state-typing. The critical component of this typing relation is the consistency relation \(\mathbf {Cons}\) .
Intuitively, \(\mathbf {Cons}\)  expresses that the current heap and registers are consistent with the ownership
and refinement information implied by \(\Gamma \) . We say triple \(( \mathit {H},\mathit {R},\Gamma )\)  is consistent,
and write \(\mathbf {Cons} \, ( \mathit {H} , \mathit {R} , \Gamma )\) . In the definitions for \(\mathbf {own}\)  we write \(\lbrace  \mathit {a} \mapsto r \rbrace \)  to denote a function \(\textbf {Addr} \rightarrow [0,1]\) 
which returns \(r\)  for \(\mathit {a}\) , and 0 otherwise. We write \( \emptyset \)  to denote a constant
function \(\textbf {Addr} \rightarrow [0,1]\)  which always returns 0. We define the addition between
two functions \(\mathit {O_{{\mathrm {1}}}}, \mathit {O_{{\mathrm {2}}}}: \textbf {Addr} \rightarrow [0,1]\)  as: \(( \mathit {O_{{\mathrm {1}}}} + \mathit {O_{{\mathrm {2}}}} ) ( \mathit {a} ) = \mathit {O_{{\mathrm {1}}}} ( \mathit {a} ) + \mathit {O_{{\mathrm {2}}}} ( \mathit {a} )\) .
Finally, if a summation \( \Sigma \)  has no summands, we take its result to be \( \emptyset \) .
The proof of thm:soundness requires the following four key lemmas. These lemmas are stated
with respect to some well-typed program \( \left\langle { \mathit {D} , \mathit {e} }\right\rangle  \) , i.e. \(\vdash \left\langle { \mathit {D} , \mathit {e} }\right\rangle  \) .


\( \vdash _{\mathit {conf} }^D \left\langle { \emptyset , \emptyset , \cdot , \mathit {e} }\right\rangle  \) 


Trivial, taking \(\Gamma = \bullet \)  and by inversion on \(\vdash \left\langle { \mathit {D} , \mathit {e} }\right\rangle  \) .
\( \vdash _{\mathit {conf} }^D \mathbf {C} \)  implies \( \mathbf {C} \ne \mathbf {AssertFail} \) 


Simple proof by contradiction, as the \( \mathbf {AssertFail} \)  is not well-typed.
If \( \vdash _{\mathit {conf} }^D \left\langle { \mathit {H} , \mathit {R} , \vec{F} , \mathit {e} }\right\rangle  \)  and \( \left\langle { \mathit {H} , \mathit {R} , \vec{F} , \mathit {e} }\right\rangle  \longrightarrow _{ \mathit {D} } \mathbf {C} \) , then \( \vdash _{\mathit {conf} }^D \mathbf {C} \) 



If \( \vdash _{\mathit {conf} }^D \mathbf {C} \) , then, one of the following conditions hold:

\(\exists \mathbf {C}^{\prime }, \mathbf {C} \longrightarrow _{ \mathit {D} } \mathbf {C}^{\prime } \) , or

\(\mathbf {C} = \mathbf {AssertFail} \) , or

\(\mathbf {C} = \left\langle { \mathit {H} , \mathit {R} , \cdot , \mathit {x} }\right\rangle  \)

lem:preservation,lem:progress are the heart of proof effort, we give their proofs in sec:preservation-proof,sec:progress-proof
respectively.
We can now prove thm:soundness:
[thm:soundness: Soundness]
From lem:initial,lem:preservation and an inductive argument, any configuration
reachable from the initial state must be well-typed. Then, by lem:assertfail every
configuration reachable from the initial state cannot be \( \mathbf {AssertFail} \) , i.e., a well-typed
program never experiences an assertion failure. This completes the first part of the proof.
To prove the second portion of the theorem, it suffices to show that any configuration reachable
from the initial state can step or is a final configuration. Again from
lem:initial,lem:preservation and a simple inductive argument, we must have that
for any state \(\mathbf {C}\)  such that \( \left\langle { \emptyset , \emptyset , \cdot , \mathit {e} }\right\rangle  \longrightarrow ^* _{ \mathit {D} } \mathbf {C} \)  \( \vdash _{\mathit {conf} }^D \mathbf {C} \) .
Then by lem:progress we have the configuration may step or is one of the final configurations.
The remainder of this appendix proves lem:preservation,lem:progress. We introduce some auxiliary definitions and
lemmas in sec:aux-defn-lem, give the proof of lem:preservation in sec:preservation-proof, and prove
lem:progress in sec:progress-proof.

Auxiliary Lemmas and Definitions
<FIGURE>The well-formedness rules omitted from the main paper are found in fig:type-wf. We write
\( \mathcal {L} \vdash _{\mathit {WF}} \tau \operatorname{\Rightarrow }\Gamma \)  as shorthand for \( \mathcal {L} \vdash _{\mathit {WF}} \Gamma \)  and \( \mathcal {L} \mid \Gamma \vdash _{\mathit {WF}} \tau \) .
We first prove that the subtyping relations are transitive.

 If \(\Gamma \le \Gamma ^{\prime }\)  then \(\models \left.{ \Gamma }\right. \Rightarrow \left.{ \Gamma ^{\prime } }\right. \) .

 If \(\Gamma \vdash \tau _{{\mathrm {1}}} \le \tau _{{\mathrm {2}}}\)  and \(\Gamma \vdash \tau _{{\mathrm {2}}} \le \tau _{{\mathrm {3}}}\) , then \(\Gamma \vdash \tau _{{\mathrm {1}}} \le \tau _{{\mathrm {3}}}\)

 If \(\Gamma \le \Gamma ^{\prime }\)  and \(\Gamma ^{\prime } \vdash \tau _{{\mathrm {1}}} \le \tau _{{\mathrm {2}}}\) , then \(\Gamma \vdash \tau _{{\mathrm {1}}} \le \tau _{{\mathrm {2}}}\)

 If \(\Gamma \le \Gamma ^{\prime }\) , \(\Gamma \vdash \tau _{{\mathrm {1}}} \le \tau _{{\mathrm {2}}}\) , and \(\Gamma ^{\prime } \vdash \tau _{{\mathrm {2}}} \le \tau _{{\mathrm {3}}}\) , then \(\Gamma \vdash \tau _{{\mathrm {1}}} \le \tau _{{\mathrm {3}}}\) .

If \(\Gamma \le \Gamma ^{\prime }\)  and \(\Gamma ^{\prime } \le \Gamma ^{\prime \prime }\) , then \(\Gamma \le \Gamma ^{\prime \prime }\) .


It suffices to show that \(\models \left.{ \Gamma }\right. \Rightarrow [ \mathit {x} / \, \nu \, ] \, \varphi ^{\prime }\)  for any \( \mathit {x} \in \mathit {dom}( \Gamma ^{\prime } ) \)  where \(\Gamma ^{\prime } ( \mathit {x} ) = \left\lbrace { \nu \operatorname{:}\mathbf {int}\mid \varphi ^{\prime } }\right\rbrace  \) .
From \(\Gamma \le \Gamma ^{\prime }\)  we have \(\models \left.{ \Gamma }\right. \wedge \varphi \Rightarrow \varphi ^{\prime }\)  where \(\Gamma ( \mathit {x} ) = \left\lbrace { \nu \operatorname{:}\mathbf {int}\mid \varphi }\right\rbrace  \) .
We must then have \(\models \left.{ \Gamma }\right. \wedge [ \mathit {x} / \, \nu \, ] \, \varphi \Rightarrow [ \mathit {x} / \, \nu \, ] \, \varphi ^{\prime }\) . From the definition of \( \left.{ \Gamma }\right. \)  we have \( \left.{ \Gamma }\right. \wedge [ \mathit {x} / \, \nu \, ] \, \varphi \iff \left.{ \Gamma }\right. \) , giving the desired result.

By induction on \(\Gamma \vdash \tau _{{\mathrm {1}}} \le \tau _{{\mathrm {2}}}\) . We only consider the base case where \(\tau _{{\mathrm {1}}} = \left\lbrace { \nu \operatorname{:}\mathbf {int}\mid \varphi _{{\mathrm {1}}} }\right\rbrace  \)  and \(\tau _{{\mathrm {2}}} = \left\lbrace { \nu \operatorname{:}\mathbf {int}\mid \varphi _{{\mathrm {2}}} }\right\rbrace  \) ,
the case for reference types follows from the induction hypothesis.
By further inversion on \(\Gamma \vdash \tau _{{\mathrm {2}}} \le \tau _{{\mathrm {3}}}\)  we therefore have:
3 = { :int3 }
  1 2    2 3
From which it is immediate that we must have \(\models \left.{ \Gamma }\right. \wedge \varphi _{{\mathrm {1}}} \Rightarrow \varphi _{{\mathrm {3}}}\) , whereby S-Int gives \(\Gamma \vdash \tau _{{\mathrm {1}}} \le \tau _{{\mathrm {3}}}\) .

By induction on \(\Gamma ^{\prime } \vdash \tau _{{\mathrm {1}}} \le \tau _{{\mathrm {2}}}\) . The case for reference types is immediate from the inductive hypothesis, we focus
on the base case where \(\tau _{{\mathrm {1}}} = \left\lbrace { \nu \operatorname{:}\mathbf {int}\mid \varphi _{{\mathrm {1}}} }\right\rbrace  \)  and \(\tau _{{\mathrm {2}}} = \left\lbrace { \nu \operatorname{:}\mathbf {int}\mid \varphi _{{\mathrm {2}}} }\right\rbrace  \) , and where \(\models \left.{ \Gamma ^{\prime } }\right. \wedge \varphi _{{\mathrm {1}}} \Rightarrow \varphi _{{\mathrm {2}}}\) .
From \(\Gamma \le \Gamma ^{\prime }\)  and part:sub-env-impl above, we have \(\models \left.{ \Gamma }\right. \Rightarrow \left.{ \Gamma ^{\prime } }\right. \)  from which we can derive \( \left.{ \Gamma }\right. \wedge \varphi _{{\mathrm {1}}} \Rightarrow \varphi _{{\mathrm {2}}}\) , i.e.,
\(\Gamma \vdash \tau _{{\mathrm {1}}} \le \tau _{{\mathrm {2}}}\) .

Immediate from part:single-env-trans,part:env-sup-subtype.

Immediate corollary of part:env-sub-trans.

A value \(v\)  reaches an integer with \(n\)  dereferences in heap \(\mathit {H}\)  when it is in the relation \( \mathit {H} \vdash v \Downarrow n \) 
defined as the smallest relation closed under the following rules:

If \( v \in \mathbb {Z} \)  then \( \mathit {H} \vdash v \Downarrow 0 \)

If \( \mathit {H} \vdash v \Downarrow n \)  and \(\mathit {H} ( \mathit {a} ) \, = \, v\)  then \( \mathit {H} \vdash \mathit {a} \Downarrow n + 1 \)

We will write \( \mathit {H} \vdash v \Downarrow | \tau | \)  to indicate a value \(v\)  is shape consistent with \(\tau \)  in heap \(\mathit {H}\) , where
\( | \tau | \)  is the number of reference constructors in the type \(\tau \) .
We also prove a standard inversion lemma to
handle the fact our typing rules are not syntax directed.
[Inversion] 
If
\( \Theta \mid \mathcal {L} \mid \Gamma \vdash \mathit {e_{{\mathrm {0}}}} : \tau \operatorname{\Rightarrow }\Gamma ^{\prime } \) ,
then there exists some \(\Gamma _{\mathit {p}}\) , \(\tau _{\mathit {p}}\) , and \(\Gamma ^{\prime }_{\mathit {p}}\) 
such that \(\Gamma \le \Gamma _{\mathit {p}}\) , \( \vec{\ell } \vdash _{\mathit {WF}} \Gamma _{\mathit {p}} \) , \(\Gamma ^{\prime }_{\mathit {p}} , \tau _{\mathit {p}} \le \Gamma ^{\prime } , \tau \) , and:

If \(\mathit {e_{{\mathrm {0}}}} = \mathit {x}\)  then \(\Gamma _{\mathit {p}} ( \mathit {x} ) = \tau _{\mathit {p}} + \tau ^{\prime }\) , \(\Gamma ^{\prime }_{\mathit {p}} = \Gamma _{\mathit {p}} [ \mathit {x} \hookleftarrow \tau ^{\prime } ]\) .

If \(\mathit {e_{{\mathrm {0}}}} = \operatorname{\mathbf {let}}\mathit {x} = \mathit {y} \operatorname{\mathbf {in}}\mathit {e} \) , then
\( \Theta \mid \mathcal {L} \mid \Gamma _{\mathit {p}} [ \mathit {y} \hookleftarrow \tau _{{\mathrm {1}}} \wedge _{ \mathit {y} } \mathit {y} =_{ \tau _{{\mathrm {1}}} } \mathit {x} ] , \mathit {x} : ( \tau _{{\mathrm {2}}} \wedge _{ \mathit {x} } \mathit {x} =_{ \tau _{{\mathrm {2}}} } \mathit {y} ) \vdash \mathit {e} : \tau _{\mathit {p}} \operatorname{\Rightarrow }\Gamma ^{\prime }_{\mathit {p}} \) 
and \( \mathit {x} \notin \mathit {dom}( \Gamma ^{\prime }_{\mathit {p}} ) \)  where \(\Gamma _{\mathit {p}} ( \mathit {y} ) = \tau _{{\mathrm {1}}} + \tau _{{\mathrm {2}}}\) .

If \(\mathit {e_{{\mathrm {0}}}} = \operatorname{\mathbf {let}}\mathit {x} = n \operatorname{\mathbf {in}}\mathit {e} \)  then \( \Theta \mid \mathcal {L} \mid \Gamma _{\mathit {p}} , \mathit {x} : \left\lbrace { \nu \operatorname{:}\mathbf {int}\mid \nu \, = \, n }\right\rbrace  \vdash \mathit {e} : \tau _{\mathit {p}} \operatorname{\Rightarrow }\Gamma ^{\prime }_{\mathit {p}} \)  and \( \mathit {x} \notin \mathit {dom}( \Gamma ^{\prime }_{\mathit {p}} ) \) .

If \(\mathit {e_{{\mathrm {0}}}} = \operatorname{\mathbf {ifz}}\mathit {x} \operatorname{\mathbf {then}}\mathit {e_{{\mathrm {1}}}} \operatorname{\mathbf {else}}\mathit {e_{{\mathrm {2}}}} \)  then:

\(\Gamma _{\mathit {p}} ( \mathit {x} ) = \left\lbrace { \nu \operatorname{:}\mathbf {int}\mid \varphi }\right\rbrace  \)

\( \Theta \mid \mathcal {L} \mid \Gamma _{\mathit {p}} [ \mathit {x} \hookleftarrow \left\lbrace { \nu \operatorname{:}\mathbf {int}\mid \varphi \wedge \nu \, = \, 0 }\right\rbrace  ] \vdash \mathit {e_{{\mathrm {1}}}} : \tau _{\mathit {p}} \operatorname{\Rightarrow }\Gamma ^{\prime }_{\mathit {p}} \)

\( \Theta \mid \mathcal {L} \mid \Gamma _{\mathit {p}} [ \mathit {x} \hookleftarrow \left\lbrace { \nu \operatorname{:}\mathbf {int}\mid \varphi \wedge \nu \, \ne \, 0 }\right\rbrace  ] \vdash \mathit {e_{{\mathrm {2}}}} : \tau _{\mathit {p}} \operatorname{\Rightarrow }\Gamma ^{\prime }_{\mathit {p}} \)


If \(\mathit {e_{{\mathrm {0}}}} = \operatorname{\mathbf {let}}\mathit {x} = \operatorname{\mathbf {mkref}}\mathit {y} \operatorname{\mathbf {in}}\mathit {e} \) , then \(\Gamma _{\mathit {p}} ( \mathit {y} ) = \tau _{{\mathrm {1}}} + \tau _{{\mathrm {2}}}\) , \( \Theta \mid \mathcal {L} \mid \Gamma [ \mathit {y} \hookleftarrow \tau _{{\mathrm {1}}} ] , \mathit {x} : ( \tau _{{\mathrm {2}}} \wedge _{ \mathit {x} } \mathit {x} =_{ \tau _{{\mathrm {2}}} } \mathit {y} ) \operatorname{\mathbf {ref}}^{ 1 } \vdash \mathit {e} : \tau \operatorname{\Rightarrow }\Gamma ^{\prime }_{\mathit {p}} \) , and \( \mathit {x} \notin \mathit {dom}( \Gamma ^{\prime }_{\mathit {p}} ) \)

If \(\mathit {e_{{\mathrm {0}}}} = \operatorname{\mathbf {let}}\mathit {x} = * \mathit {y} \operatorname{\mathbf {in}}\mathit {e} \) , then:

\(\Gamma _{\mathit {p}} ( \mathit {y} ) = \tau _{{\mathrm {1}}} + \tau _{{\mathrm {2}}} \operatorname{\mathbf {ref}}^{ r } \)

\( \Theta \mid \mathcal {L} \mid \Gamma _{\mathit {p}} [ \mathit {y} \hookleftarrow \tau ^{\prime \prime } \operatorname{\mathbf {ref}}^{ r } ] , \mathit {x} : \tau _{{\mathrm {2}}} \vdash \mathit {e} : \tau _{\mathit {p}} \operatorname{\Rightarrow }\Gamma ^{\prime }_{\mathit {p}} \)

\( \mathit {x} \notin \mathit {dom}( \Gamma ^{\prime }_{\mathit {p}} ) \)


\(\tau ^{\prime \prime } = {\left\lbrace \begin{array}{ll}( \tau _{{\mathrm {1}}} \wedge _{ \mathit {y} } \mathit {y} =_{ \tau _{{\mathrm {1}}} } \mathit {x} ) & r > 0 \\\tau _{{\mathrm {1}}} & r = 0\end{array}\right.}\) 


If \(\mathit {e_{{\mathrm {0}}}} = \operatorname{\mathbf {let}}\mathit {x} = \mathit {f} ^ \ell ( \mathit {y_{{\mathrm {1}}}} ,\ldots , \mathit {y_{\mathit {n}}} ) \operatorname{\mathbf {in}}\mathit {e} \)  then:

\(\Gamma _{\mathit {p}} ( \mathit {y_{\mathit {i}}} ) = \sigma _{\alpha } \, \sigma _{x} \, \tau _{\mathit {i}}\)  for each \(i \in \left\lbrace {1,\ldots ,n}\right\rbrace \)

\( \Theta \mid \mathcal {L} \mid \Gamma _{\mathit {p}} [ \mathit {y_{\mathit {i}}} \hookleftarrow \sigma _{\alpha } \, \sigma _{x} \, \tau ^{\prime }_{\mathit {i}} ] , \mathit {x} : \sigma _{\alpha } \, \sigma _{x} \, \tau \vdash \mathit {e} : \tau _{\mathit {p}} \operatorname{\Rightarrow }\Gamma ^{\prime }_{\mathit {p}} \)

\(\Theta ( \mathit {f} ) = \forall \lambda .\left\langle { \mathit {x_{{\mathrm {1}}}} \operatorname{:}\tau _{{\mathrm {1}}} ,\dots , \mathit {x_{\mathit {n}}} \operatorname{:}\tau _{\mathit {n}} }\right\rangle \operatorname{\rightarrow }\left\langle { \mathit {x_{{\mathrm {1}}}} \operatorname{:}\tau ^{\prime }_{{\mathrm {1}}} ,\dots , \mathit {x_{\mathit {n}}} \operatorname{:}\tau ^{\prime }_{\mathit {n}} \mid \tau }\right\rangle  \)

\(\sigma _{\alpha } = [ \ell : \mathcal {L} / \lambda ]\)

\(\sigma _{x} = [ \mathit {y_{{\mathrm {1}}}} / \mathit {x_{{\mathrm {1}}}} ] \cdots [ \mathit {y_{\mathit {n}}} / \mathit {x_{\mathit {n}}} ] \)

\( \mathit {x} \notin \mathit {dom}( \Gamma ^{\prime }_{\mathit {p}} ) \)


If \(\mathit {e_{{\mathrm {0}}}} = \mathit {y} \operatorname{:=}\mathit {x} \operatorname{;}\mathit {e} \)  then:

\(\Gamma _{\mathit {p}} ( \mathit {x} ) = \tau _{{\mathrm {1}}} + \tau _{{\mathrm {2}}}\)

\(\Gamma _{\mathit {p}} ( \mathit {y} ) = \tau ^{\prime } \operatorname{\mathbf {ref}}^{ 1 } \)

\( \Theta \mid \mathcal {L} \mid \Gamma _{\mathit {p}} [ \mathit {x} \hookleftarrow \tau _{{\mathrm {1}}} ] [ \mathit {y} \hookleftarrow ( \tau _{{\mathrm {2}}} \wedge _{ \mathit {y} } \mathit {y} =_{ \tau _{{\mathrm {2}}} } \mathit {x} ) \operatorname{\mathbf {ref}}^{ 1 } ] \vdash \mathit {e} : \tau _{\mathit {p}} \operatorname{\Rightarrow }\Gamma ^{\prime }_{\mathit {p}} \)

The shapes of \(\tau ^{\prime }\)  and \(\tau _{{\mathrm {2}}}\)  are similar, i.e, \( | \tau ^{\prime } | \, = \, | \tau _{{\mathrm {2}}} | \) .


If \(\mathit {e_{{\mathrm {0}}}} = \mathbf {alias}( \mathit {x} = \mathit {y} ) \operatorname{;}\mathit {e} \)  then there exist some \(\tau _{{\mathrm {1}}}, \tau _{{\mathrm {2}}}, \tau ^{\prime }_{{\mathrm {1}}}, \tau ^{\prime }_{{\mathrm {2}}}, r_{{\mathrm {1}}}, r_{{\mathrm {2}}}, r^{\prime }_{{\mathrm {1}}}, r^{\prime }_{{\mathrm {2}}}\)  such that:

\( \tau _{{\mathrm {1}}} \operatorname{\mathbf {ref}}^{ r_{{\mathrm {1}}} } + \tau _{{\mathrm {2}}} \operatorname{\mathbf {ref}}^{ r_{{\mathrm {2}}} } \approx \tau ^{\prime }_{{\mathrm {1}}} \operatorname{\mathbf {ref}}^{ r^{\prime }_{{\mathrm {1}}} } + \tau ^{\prime }_{{\mathrm {2}}} \operatorname{\mathbf {ref}}^{ r^{\prime }_{{\mathrm {2}}} } \)

\(\Gamma _{\mathit {p}} ( \mathit {x} ) = \tau _{{\mathrm {1}}} \operatorname{\mathbf {ref}}^{ r_{{\mathrm {1}}} } \)  and \(\Gamma _{\mathit {p}} ( \mathit {y} ) = \tau _{{\mathrm {2}}} \operatorname{\mathbf {ref}}^{ r_{{\mathrm {2}}} } \)

\( \Theta \mid \mathcal {L} \mid \Gamma [ \mathit {x} \hookleftarrow \tau ^{\prime }_{{\mathrm {1}}} \operatorname{\mathbf {ref}}^{ r^{\prime }_{{\mathrm {1}}} } ] [ \mathit {y} \hookleftarrow \tau ^{\prime }_{{\mathrm {2}}} \operatorname{\mathbf {ref}}^{ r^{\prime }_{{\mathrm {2}}} } ] \vdash \mathit {e} : \tau _{\mathit {p}} \operatorname{\Rightarrow }\Gamma ^{\prime }_{\mathit {p}} \)


If \(\mathit {e_{{\mathrm {0}}}} = \mathbf {alias}( \mathit {x} = * \mathit {y} ) \operatorname{;}\mathit {e} \)  then there exist some \(\tau _{{\mathrm {1}}}, \tau _{{\mathrm {2}}}, \tau ^{\prime }_{{\mathrm {1}}}, \tau ^{\prime }_{{\mathrm {2}}}, r_{{\mathrm {1}}}, r_{{\mathrm {2}}}, r^{\prime }_{{\mathrm {1}}}, r^{\prime }_{{\mathrm {2}}}, r\) , such that:

\( \tau _{{\mathrm {1}}} \operatorname{\mathbf {ref}}^{ r_{{\mathrm {1}}} } + \tau _{{\mathrm {2}}} \operatorname{\mathbf {ref}}^{ r_{{\mathrm {2}}} } \approx \tau ^{\prime }_{{\mathrm {1}}} \operatorname{\mathbf {ref}}^{ r^{\prime }_{{\mathrm {1}}} } + \tau ^{\prime }_{{\mathrm {2}}} \operatorname{\mathbf {ref}}^{ r^{\prime }_{{\mathrm {2}}} } \)

\(\Gamma _{\mathit {p}} ( \mathit {x} ) = \tau _{{\mathrm {1}}} \operatorname{\mathbf {ref}}^{ r_{{\mathrm {1}}} } \)  and \(\Gamma _{\mathit {p}} ( \mathit {y} ) = ( \tau _{{\mathrm {2}}} \operatorname{\mathbf {ref}}^{ r_{{\mathrm {2}}} } ) \operatorname{\mathbf {ref}}^{ r } \)

\( \Theta \mid \mathcal {L} \mid \Gamma [ \mathit {x} \hookleftarrow \tau ^{\prime }_{{\mathrm {1}}} \operatorname{\mathbf {ref}}^{ r^{\prime }_{{\mathrm {1}}} } ] [ \mathit {y} \hookleftarrow ( \tau ^{\prime }_{{\mathrm {2}}} \operatorname{\mathbf {ref}}^{ r^{\prime }_{{\mathrm {2}}} } ) \operatorname{\mathbf {ref}}^{ r } ] \vdash \mathit {e} : \tau _{\mathit {p}} \operatorname{\Rightarrow }\Gamma ^{\prime }_{\mathit {p}} \)


If \( \mathit {e_{{\mathrm {0}}}} = \mathit {e_{{\mathrm {1}}}} \operatorname{;}\mathit {e_{{\mathrm {2}}}} \)  then \( \Theta \mid \mathcal {L} \mid \Gamma _{\mathit {p}} \vdash \mathit {e_{{\mathrm {1}}}} : \tau _{{\mathrm {1}}} \operatorname{\Rightarrow }\Gamma _{{\mathrm {1}}} \)  and \( \Theta \mid \mathcal {L} \mid \Gamma _{{\mathrm {1}}} \vdash \mathit {e_{{\mathrm {2}}}} : \tau _{\mathit {p}} \operatorname{\Rightarrow }\Gamma ^{\prime }_{\mathit {p}} \)

If \( \mathit {e_{{\mathrm {0}}}} = \mathit {x} \operatorname{;}\mathit {e^{\prime }} \)  then \( \Theta \mid \mathcal {L} \mid \Gamma _{\mathit {p}} [ \mathit {x} : \tau ^{\prime } + \tau _{{\mathrm {0}}} ] \vdash \mathit {x} : \tau _{{\mathrm {1}}} \operatorname{\Rightarrow }\Gamma _{\mathit {p}} [ \mathit {x} \hookleftarrow \tau _{{\mathrm {0}}} ] \)  and \( \Theta \mid \mathcal {L} \mid \Gamma _{\mathit {p}} [ \mathit {x} \hookleftarrow \tau _{{\mathrm {0}}} ] \vdash \mathit {e^{\prime }} : \tau _{\mathit {p}} \operatorname{\Rightarrow }\Gamma ^{\prime }_{\mathit {p}} \)

If \(\mathit {e_{{\mathrm {0}}}} = \mathbf {assert}( \varphi ) \operatorname{;}\mathit {e} \)  then \(\Gamma _{\mathit {p}} \models \varphi \)  and \( \Theta \mid \mathcal {L} \mid \Gamma _{\mathit {p}} \vdash \mathit {e} : \tau _{\mathit {p}} \operatorname{\Rightarrow }\Gamma ^{\prime }_{\mathit {p}} \)

By straightforward induction on the typing relation and
the transitivity of the subtyping relation lem:subtype-transitive.
The only case of note is the case for \( \mathit {e_{{\mathrm {0}}}} = \mathit {x} \operatorname{;}\mathit {e_{{\mathrm {2}}}} \) . If the subderivation for \(\mathit {x}\) 
has applications of T-Sub then the subtypings on the output environment can be pushed
into application subtyping on input environments when typing \(\mathit {e^{\prime }}\) . Similarly,
any input subtypings on the input environment of the derivation of \(\mathit {x}\)  can be pushed
into T-Sub rules such that \(\Gamma \le \Gamma _{\mathit {p}} [ \mathit {x} : \tau ^{\prime } + \tau _{{\mathrm {0}}} ]\) .
lem:stackvar,lem:ectxt-sub-well-typed prove some standard properties of execution contexts:
any decomposition of a well-typed expression into a execution context and redex can be well-typed,
and substituting a well-typed expression matching a context's hole type yields a well-typed expression
For any \(\mathit {E}\)  and \(\mathit {e^{\prime }}\)  such that \(\mathit {E} [ \mathit {e^{\prime }} ] = \mathit {e}\)  where
\( \Theta \mid \mathcal {L} \mid \Gamma \vdash \mathit {e} : \tau \operatorname{\Rightarrow }\Gamma ^{\prime } \)  there exists some \(\tau _{{\mathrm {0}}}\) , \(\Gamma _{{\mathrm {0}}}\)  such that
\(\Theta \mid []: \tau _{{\mathrm {0}}} \operatorname{\Rightarrow }\Gamma _{{\mathrm {0}}} \mid \mathcal {L} \vdash _{\mathit {ectx} } \mathit {E} : \tau \operatorname{\Rightarrow }\Gamma ^{\prime }\)  and
\( \Theta \mid \mathcal {L} \mid \Gamma \vdash \mathit {e^{\prime }} : \tau _{{\mathrm {0}}} \operatorname{\Rightarrow }\Gamma _{{\mathrm {0}}} \) .


By induction on the structure of \(\mathit {E}\) .
\(\mathit {E} = []\) 
Trivial, by taking \(\tau _{{\mathrm {0}}} = \tau \)  and \(\Gamma _{{\mathrm {0}}} = \Gamma ^{\prime }\) .

\( \mathit {E} = \mathit {E^{\prime }} \operatorname{;}\mathit {e^{\prime \prime }} \) 
Then \( \mathit {E} [ \mathit {e^{\prime }} ] = \mathit {E^{\prime }} [ \mathit {e^{\prime }} ] \operatorname{;}\mathit {e^{\prime \prime }} = \mathit {e}\) . By
lem:inversion we have
\(\begin{bcpcasearray}\Theta \mid \mathcal {L} \mid \Gamma _{\mathit {p}} \vdash \mathit {E^{\prime }} [ \mathit {e^{\prime }} ] : \tau _{{\mathrm {1}}} \operatorname{\Rightarrow }\Gamma _{{\mathrm {1}}} & \Theta \mid \mathcal {L} \mid \Gamma _{{\mathrm {1}}} \vdash \mathit {e^{\prime \prime }} : \tau _{\mathit {p}} \operatorname{\Rightarrow }\Gamma ^{\prime }_{\mathit {p}} \\\Gamma \le \Gamma _{\mathit {p}} & \Gamma ^{\prime }_{\mathit {p}} , \tau _{\mathit {p}} \le \Gamma ^{\prime } , \tau \end{bcpcasearray}\) 
for some \(\Gamma _{\mathit {p}}\) , \(\Gamma ^{\prime }_{\mathit {p}}\) , and \(\tau _{\mathit {p}}\) .
By the induction hypothesis
we then have \( \Theta \mid \mathcal {L} \mid \Gamma _{\mathit {p}} \vdash \mathit {e^{\prime }} : \tau _{{\mathrm {0}}} \operatorname{\Rightarrow }\Gamma _{{\mathrm {0}}} \)  and
\(\Theta \mid []: \tau _{{\mathrm {0}}} \operatorname{\Rightarrow }\Gamma _{{\mathrm {0}}} \mid \mathcal {L} \vdash _{\mathit {ectx} } \mathit {E^{\prime }} : \tau _{{\mathrm {1}}} \operatorname{\Rightarrow }\Gamma _{{\mathrm {1}}}\) . for some \(\tau _{{\mathrm {0}}}\)  and \(\Gamma _{{\mathrm {0}}}\) .
Next, as \(\Gamma ^{\prime }_{\mathit {p}} , \tau _{\mathit {p}} \le \Gamma ^{\prime } , \tau \)  by an application of T-Sub,
we have \( \Theta \mid \mathcal {L} \mid \Gamma _{{\mathrm {1}}} \vdash \mathit {e^{\prime \prime }} : \tau \operatorname{\Rightarrow }\Gamma ^{\prime } \) . By TE-Seq, we therefore
have: \(\Theta \mid []: \tau _{{\mathrm {0}}} \operatorname{\Rightarrow }\Gamma _{{\mathrm {0}}} \mid \mathcal {L} \vdash _{\mathit {ectx} } \mathit {E^{\prime }} \operatorname{;}\mathit {e^{\prime \prime }} : \tau \operatorname{\Rightarrow }\Gamma ^{\prime }\) .
Finally, from \(\Gamma \le \Gamma _{\mathit {p}}\)  and \( \Theta \mid \mathcal {L} \mid \Gamma _{\mathit {p}} \vdash \mathit {e^{\prime }} : \tau _{{\mathrm {0}}} \operatorname{\Rightarrow }\Gamma _{{\mathrm {0}}} \) ,
and application of T-Sub, we have \( \Theta \mid \mathcal {L} \mid \Gamma \vdash \mathit {e^{\prime }} : \tau _{{\mathrm {0}}} \operatorname{\Rightarrow }\Gamma _{{\mathrm {0}}} \) .
If \(\Theta \mid []: \tau \operatorname{\Rightarrow }\Gamma ^{\prime } \mid \mathcal {L} \vdash _{\mathit {ectx} } \mathit {E} : \tau ^{\prime \prime } \operatorname{\Rightarrow }\Gamma ^{\prime \prime }\)  and \( \Theta \mid \mathcal {L} \mid \Gamma \vdash \mathit {e} : \tau \operatorname{\Rightarrow }\Gamma ^{\prime } \)  for some \(\Gamma \) ,
then \( \Theta \mid \mathcal {L} \mid \Gamma \vdash \mathit {E} [ \mathit {e} ] : \tau ^{\prime \prime } \operatorname{\Rightarrow }\Gamma ^{\prime \prime } \) .


By induction on the typing derivation of \(\mathit {E}\) .
TE-Seq
E = E' ;e'
E [ e ] = E' [ e ] ;e'
[]: ' L ectx  E' : 0 0
L 0 e' : ” ”

By the induction hypothesis we have \( \Theta \mid \mathcal {L} \mid \Gamma \vdash \mathit {E^{\prime }} [ \mathit {e} ] : \tau _{{\mathrm {0}}} \operatorname{\Rightarrow }\Gamma _{{\mathrm {0}}} \) . We then
have our result via an application of T-Seq.

TE-Hole
Trivial, as \(\tau = \tau ^{\prime \prime }\)  and \(\Gamma ^{\prime } = \Gamma ^{\prime \prime }\)  and \(\mathit {E} [ \mathit {e} ] = \mathit {e}\) .
[Context Variable Substitution]

 If \(\tau _{{\mathrm {3}}} = \tau _{{\mathrm {1}}} + \tau _{{\mathrm {2}}}\)  then \([ \mathcal {L} / \lambda ] \, \tau _{{\mathrm {3}}} = [ \mathcal {L} / \lambda ] \, \tau _{{\mathrm {1}}} + [ \mathcal {L} / \lambda ] \, \tau _{{\mathrm {2}}}\)

For any \(\vec{\ell }\) :

If \( \lambda \vdash _{\mathit {WF}} \Gamma \)  then \( \vec{\ell } \vdash _{\mathit {WF}} [ \vec{\ell } / \lambda ] \Gamma \)

If \( \lambda \mid \Gamma \vdash _{\mathit {WF}} \tau \)  then \( \vec{\ell } \mid [ \vec{\ell } / \lambda ] \Gamma \vdash _{\mathit {WF}} [ \vec{\ell } / \lambda ] \, \tau \)

If \( \lambda \vdash _{\mathit {WF}} \tau \operatorname{\Rightarrow }\Gamma \)  then \( \vec{\ell } \vdash _{\mathit {WF}} [ \vec{\ell } / \lambda ] \, \tau \operatorname{\Rightarrow }[ \vec{\ell } / \lambda ] \Gamma \)


 For any \(\Gamma \) , \(\tau _{{\mathrm {1}}}\) , \(\tau _{{\mathrm {2}}}\) , \(\lambda \)  and \(\vec{\ell }\) , If \(\Gamma \vdash \tau _{{\mathrm {1}}} \le \tau _{{\mathrm {2}}}\) , then \([ \vec{\ell } / \lambda ] \Gamma \vdash [ \vec{\ell } / \lambda ] \, \tau _{{\mathrm {1}}} \le [ \vec{\ell } / \lambda ] \, \tau _{{\mathrm {2}}}\)

 If \(\Gamma \models \varphi \)  where \( \lambda \notin \mathbf {FCV} \, ( \varphi ) \)  then \([ \vec{\ell } / \lambda ] \Gamma \models \varphi \)

 If \( \Theta \mid \lambda \mid \Gamma \vdash \mathit {e} : \tau \operatorname{\Rightarrow }\Gamma ^{\prime } \)  then \( \Theta \mid \vec{\ell } \mid [ \vec{\ell } / \lambda ] \Gamma \vdash \mathit {e} : [ \vec{\ell } / \lambda ] \, \tau \operatorname{\Rightarrow }[ \vec{\ell } / \lambda ] \Gamma ^{\prime } \)


By straightforward induction on the definition of \(\tau _{{\mathrm {1}}} + \tau _{{\mathrm {2}}} = \tau _{{\mathrm {3}}}\) .

Observe that any substitution of context variables cannot change simple
types within \(\Gamma \)  and thus all types and refinements remain well-formed with respect
to integer variables in \(\Gamma \) .
It thus suffices to show that \(\mathbf {FCV} \, ( [ \vec{\ell } / \lambda ] \, \varphi ) \subseteq \mathbf {CV} \, ( \vec{\ell } ) = \emptyset \) 
for any refinement \(\varphi \)  appearing in \(\tau \)  or a type in \(\Gamma \) .
By the assumed well-formedness of \(\tau \)  with respect to context
variable \(\lambda \)  (resp. \(\Gamma \) ), after substitution all free
context variables in \(\tau \)  (resp. the types in \(\Gamma \) ) will be
replaced with \(\vec{\ell }\) . Thus, post-substitution no free context
variables appear in the refinement of \([ \vec{\ell } / \lambda ] \, \tau \)  (resp. refinements of
types in \([ \vec{\ell } / \lambda ] \Gamma \) ), trivially satisfying our requirements.

If \(\lambda \)  does not appear free in \(\tau _{{\mathrm {1}}}\) , \(\tau _{{\mathrm {2}}}\)  or \(\Gamma \) , then the result trivially holds. Let us then assume
\(\lambda \)  appears free. We prove the result by induction on the subtyping derivation.
S-Ref
1 = '1 ref r1   2 = '2 ref r2
[  / ]   1 = ( [  / ]   '1 ) ref r1   [  / ]   2 = ( [  / ]   '2 ) ref r2
'1 '2  r2 r1

We must show that \([ \vec{\ell } / \lambda ] \Gamma \vdash [ \vec{\ell } / \lambda ] \, \tau ^{\prime }_{{\mathrm {1}}} \le [ \vec{\ell } / \lambda ] \, \tau ^{\prime }_{{\mathrm {2}}}\) 
which holds immediately from the induction hypothesis.
S-Int
1 = { :int1 }  2 = { :int2 }
[  / ]   1 = { :int[  / ]   1 }  [  / ]   2 = { :int[  / ]   2 }
1 2

We must show that \([ \vec{\ell } / \lambda ] \Gamma \models [ \vec{\ell } / \lambda ] \, \varphi _{{\mathrm {1}}} \Rightarrow [ \vec{\ell } / \lambda ] \, \varphi _{{\mathrm {2}}}\) , i.e. \(\models \left.{ [ \vec{\ell } / \lambda ] \Gamma }\right. \wedge [ \vec{\ell } / \lambda ] \, \varphi _{{\mathrm {1}}} \Rightarrow [ \vec{\ell } / \lambda ] \, \varphi _{{\mathrm {2}}}\) .
From our assumption that \(\Gamma \models \varphi _{{\mathrm {1}}} \Rightarrow \varphi _{{\mathrm {2}}}\)  we have that \(\models \left.{ \Gamma }\right. \wedge \varphi _{{\mathrm {1}}} \Rightarrow \varphi _{{\mathrm {2}}}\)  is valid,
whereby the formula \( \left.{ \Gamma }\right. \wedge \varphi _{{\mathrm {1}}} \Rightarrow \varphi _{{\mathrm {2}}}\)  is true for any possible concrete valuation of the free context
variable \(\lambda \) . As \([ \vec{\ell } / \lambda ] \, \left.{ \Gamma }\right. \)  is equivalent to \( \left.{ [ \vec{\ell } / \lambda ] \Gamma }\right. \) 
we have the formula \( \left.{ [ \vec{\ell } / \lambda ] \Gamma }\right. \wedge [ \vec{\ell } / \lambda ] \, \varphi _{{\mathrm {1}}} \Rightarrow [ \vec{\ell } / \lambda ] \, \varphi _{{\mathrm {2}}}\)  must also be valid.

If \(\lambda \)  does not appear free in \( \left.{ \Gamma }\right. \) , then the result trivially holds. Otherwise
\(\models \left.{ \Gamma }\right. \Rightarrow \varphi \)  holds for any concrete valuation of the free context variable \(\lambda \) .
Then the formula \(\models \left.{ [ \vec{\ell } / \lambda ] \Gamma }\right. \Rightarrow \varphi \)  must be valid from the equivalence of \([ \vec{\ell } / \lambda ] \, \left.{ \Gamma }\right. \)  and \( \left.{ [ \vec{\ell } / \lambda ] \Gamma }\right. \) .

By induction on the typing derivation \( \Theta \mid \lambda \mid \Gamma \vdash \mathit {e} : \tau \operatorname{\Rightarrow }\Gamma ^{\prime } \) .
In every case, that \( \vec{\ell } \vdash _{\mathit {WF}} [ \vec{\ell } / \lambda ] \, \tau \operatorname{\Rightarrow }[ \vec{\ell } / \lambda ] \Gamma ^{\prime } \)  and \( \vec{\ell } \vdash _{\mathit {WF}} [ \vec{\ell } / \lambda ] \Gamma \) 
holds from itm:ctxt-sub-wf.
T-Var
e = x  = 2
= 0 [ x : 1 + 2 ]  ' = 0 [ x 2 ]

By application of itm:ctxt-sub-distribute.

T-LetInt
e = letx = n ine'  , x : { :int  =   n } e' : '
x dom( ' ) 

The induction hypothesis gives
\(\Theta \mid \vec{\ell } \mid [ \vec{\ell } / \lambda ] \Gamma , \mathit {x} : \left\lbrace { \nu \operatorname{:}\mathbf {int}\mid \nu \, = \, n }\right\rbrace  \vdash \mathit {e} : [ \vec{\ell } / \lambda ] \, \tau \operatorname{\Rightarrow }[ \vec{\ell } / \lambda ] \Gamma ^{\prime }\) 
We conclude \( \Theta \mid \vec{\ell } \mid [ \vec{\ell } / \lambda ] \Gamma \vdash \operatorname{\mathbf {let}}\mathit {x} = n \operatorname{\mathbf {in}}\mathit {e} : [ \vec{\ell } / \lambda ] \, \tau \operatorname{\Rightarrow }[ \vec{\ell } / \lambda ] \Gamma ^{\prime } \) 
as required.
T-Let
 e = letx = y ine'  x dom( ' )
 1 e' : '  1 = [ y ( 1  y  y = 1  x ) ] , x : ( 2  x  x = 2  y )
    ( y ) = y :1 + 2

By itm:ctxt-sub-distribute,
\(( [ \vec{\ell } / \lambda ] \Gamma ) ( \mathit {y} ) = [ \vec{\ell } / \lambda ] \, ( \tau _{{\mathrm {1}}} + \tau _{{\mathrm {2}}} ) = ( [ \vec{\ell } / \lambda ] \, \tau _{{\mathrm {1}}} + [ \vec{\ell } / \lambda ] \, \tau _{{\mathrm {2}}} )\) . We must then
show that \( \Theta \mid \vec{\ell } \mid \Gamma ^{\prime }_{{\mathrm {1}}} \vdash \mathit {e^{\prime }} : [ \vec{\ell } / \lambda ] \, \tau \operatorname{\Rightarrow }[ \vec{\ell } / \lambda ] \Gamma ^{\prime } \) 
where
\(\Gamma ^{\prime }_{{\mathrm {1}}} = ( [ \vec{\ell } / \lambda ] \Gamma ) [ \mathit {y} \hookleftarrow [ \vec{\ell } / \lambda ] \, \tau _{{\mathrm {1}}} \wedge _{ \mathit {y} } \mathit {y} \, = \, \mathit {x} ] , \mathit {x} : ( [ \vec{\ell } / \lambda ] \, \tau _{{\mathrm {2}}} \wedge _{ \mathit {x} } \mathit {x} \, = \, \mathit {y} )\) 
As \(\Gamma ^{\prime }_{{\mathrm {1}}} = [ \vec{\ell } / \lambda ] \Gamma _{{\mathrm {1}}}\)  the induction hypothesis gives the required typing judgment.
T-If,T-Seq
By trivial application of the inductive hypothesis.
T-MkRef,T-Deref
By reasoning similar to T-Let.
T-Call
e = letx = f  ( y1 ,..., yn ) ine'
x = [ y1 / x1 ] [ yn / xn ]
 = [ : / ' ]
1 e' : '
y dom( ' )
( f ) = ' . x1 :1 ,..., xn :n  x1 :'1 ,..., xn :'n '
1 = [ yi    x   'i ] , x :    x   '

We must first show that for \(\sigma _{\alpha }^{\prime } = [ \ell : \vec{\ell } / \lambda ^{\prime } ]\) :
\(\Theta \mid \vec{\ell } \mid \Gamma _{{\mathrm {3}}} \vdash \mathit {e^{\prime }} : [ \vec{\ell } / \lambda ] \, \tau \operatorname{\Rightarrow }[ \vec{\ell } / \lambda ] \Gamma ^{\prime }\) 
where \(\Gamma _{{\mathrm {3}}} = ( [ \vec{\ell } / \lambda ] \Gamma ) [ \mathit {y_{\mathit {i}}} \hookleftarrow \sigma _{\alpha }^{\prime } \, \sigma _{x} \, \tau ^{\prime }_{\mathit {i}} ] , \mathit {x} : \sigma _{\alpha }^{\prime } \, \sigma _{x} \, \tau ^{\prime }\) .
We first observe that \(\Gamma _{{\mathrm {3}}} = [ \vec{\ell } / \lambda ] \Gamma _{{\mathrm {1}}}\)  (this follows from the
equivalence of \([ \vec{\ell } / \lambda ] \, [ \ell : \lambda / \lambda ^{\prime } ]\)  and
\([ \ell : \vec{\ell } / \lambda ^{\prime } ]\) ) whereby the induction hypothesis
gives the required typing derivation.
We must also show that
\(\forall i \in \left\lbrace {1..n}\right\rbrace .( [ \ell : \vec{\ell } / \lambda ] \Gamma ) ( \mathit {y_{\mathit {i}}} ) = \sigma _{\alpha }^{\prime } \, \sigma _{x} \, \tau _{\mathit {i}}\) .
From the assumed well-typing of the term under \(\lambda \)  we have
that \(\forall i \in \left\lbrace {1..n}\right\rbrace .\Gamma ( \mathit {y_{\mathit {i}}} ) = \sigma _{\alpha } \, \sigma _{x} \, \tau _{\mathit {i}}\) . Recall
that \(\sigma _{\alpha }^{\prime }\)  is equivalent to \([ \vec{\ell } / \lambda ] \, \sigma _{\alpha }\) , whereby we have
\([ \vec{\ell } / \lambda ] \Gamma ( \mathit {y_{\mathit {i}}} ) = [ \vec{\ell } / \lambda ] \, \sigma _{\alpha } \, \sigma _{x} \, \tau _{\mathit {i}} = \sigma _{\alpha }^{\prime } \, \sigma _{x} \, \tau _{\mathit {i}}\)  for any \(\mathit {i}\)  as
equality is preserved by consistent substitution.
T-Assign
By the inductive hypothesis and application of itm:ctxt-sub-distribute.
T-Alias
[ x : 1 ref r1  ] [ y : 2 ref r2  ] alias( x = y ) ;e :
1 ref r1  + 2 ref r2  '1 ref r'1  + '2 ref r'2
[ x '1 ref r'1  ] [ y '2 ref r'2  ] e : 
From itm:ctxt-sub-distribute we have that \([ \vec{\ell } / \lambda ] \, ( \tau _{{\mathrm {1}}} \operatorname{\mathbf {ref}}^{ r_{{\mathrm {1}}} } ) + [ \vec{\ell } / \lambda ] \, ( \tau _{{\mathrm {2}}} \operatorname{\mathbf {ref}}^{ r_{{\mathrm {2}}} } ) = [ \vec{\ell } / \lambda ] \, ( \tau _{{\mathrm {1}}} \operatorname{\mathbf {ref}}^{ r_{{\mathrm {1}}} } + \tau _{{\mathrm {2}}} \operatorname{\mathbf {ref}}^{ r_{{\mathrm {2}}} } )\) 
and similarly for \( \tau ^{\prime }_{{\mathrm {1}}} \operatorname{\mathbf {ref}}^{ r^{\prime }_{{\mathrm {1}}} } + \tau ^{\prime }_{{\mathrm {2}}} \operatorname{\mathbf {ref}}^{ r^{\prime }_{{\mathrm {2}}} } \) . It therefore remains to show that:
\([ \vec{\ell } / \lambda ] \, ( \tau _{{\mathrm {1}}} \operatorname{\mathbf {ref}}^{ r_{{\mathrm {1}}} } + \tau _{{\mathrm {2}}} \operatorname{\mathbf {ref}}^{ r_{{\mathrm {2}}} } ) \approx [ \vec{\ell } / \lambda ] \, ( \tau ^{\prime }_{{\mathrm {1}}} \operatorname{\mathbf {ref}}^{ r^{\prime }_{{\mathrm {1}}} } + \tau ^{\prime }_{{\mathrm {2}}} \operatorname{\mathbf {ref}}^{ r^{\prime }_{{\mathrm {2}}} } )\) 
For which it suffices to show that \( \bullet \vdash [ \vec{\ell } / \lambda ] \, ( \tau _{{\mathrm {1}}} \operatorname{\mathbf {ref}}^{ r_{{\mathrm {1}}} } + \tau _{{\mathrm {2}}} \operatorname{\mathbf {ref}}^{ r_{{\mathrm {2}}} } ) \le [ \vec{\ell } / \lambda ] \, ( \tau ^{\prime }_{{\mathrm {1}}} \operatorname{\mathbf {ref}}^{ r^{\prime }_{{\mathrm {1}}} } + \tau ^{\prime }_{{\mathrm {2}}} \operatorname{\mathbf {ref}}^{ r^{\prime }_{{\mathrm {2}}} } )\) 
and \( \bullet \vdash [ \vec{\ell } / \lambda ] \, ( \tau ^{\prime }_{{\mathrm {1}}} \operatorname{\mathbf {ref}}^{ r^{\prime }_{{\mathrm {1}}} } + \tau ^{\prime }_{{\mathrm {2}}} \operatorname{\mathbf {ref}}^{ r^{\prime }_{{\mathrm {2}}} } ) \le [ \vec{\ell } / \lambda ] \, ( \tau _{{\mathrm {1}}} \operatorname{\mathbf {ref}}^{ r_{{\mathrm {1}}} } + \tau _{{\mathrm {2}}} \operatorname{\mathbf {ref}}^{ r_{{\mathrm {2}}} } )\) . From
\( \tau _{{\mathrm {1}}} \operatorname{\mathbf {ref}}^{ r_{{\mathrm {1}}} } + \tau _{{\mathrm {2}}} \operatorname{\mathbf {ref}}^{ r_{{\mathrm {2}}} } \approx \tau ^{\prime }_{{\mathrm {1}}} \operatorname{\mathbf {ref}}^{ r^{\prime }_{{\mathrm {1}}} } + \tau ^{\prime }_{{\mathrm {2}}} \operatorname{\mathbf {ref}}^{ r^{\prime }_{{\mathrm {2}}} } \)  these both follow from itm:ctxt-sub-subtype,
whereby the result follows from the inductive hypothesis.
T-AliasPtr
By similar reasoning to the T-Alias case.
T-Sub
1 e : 1 2  1
2 , 1 ' ,

By the induction hypothesis we have that: \( \Theta \mid \vec{\ell } \mid [ \vec{\ell } / \lambda ] \Gamma _{{\mathrm {1}}} \vdash \mathit {e} : [ \vec{\ell } / \lambda ] \, \tau _{{\mathrm {1}}} \operatorname{\Rightarrow }[ \vec{\ell } / \lambda ] \Gamma _{{\mathrm {2}}} \) .
If we show that \([ \vec{\ell } / \lambda ] \Gamma \le [ \vec{\ell } / \lambda ] \Gamma _{{\mathrm {1}}}\)  and \([ \vec{\ell } / \lambda ] \Gamma _{{\mathrm {2}}} , [ \vec{\ell } / \lambda ] \, \tau _{{\mathrm {1}}} \le [ \vec{\ell } / \lambda ] \Gamma ^{\prime } , [ \vec{\ell } / \lambda ] \, \tau \) 
we will have the required result. To show the first requirement, for any \( \mathit {x} \in \mathit {dom}( \Gamma ) \)  we have that
\([ \vec{\ell } / \lambda ] \Gamma \vdash [ \vec{\ell } / \lambda ] \Gamma ( \mathit {x} ) \le [ \vec{\ell } / \lambda ] \Gamma _{{\mathrm {1}}} ( \mathit {x} )\)  from itm:ctxt-sub-subtype so we have \([ \vec{\ell } / \lambda ] \Gamma \le [ \vec{\ell } / \lambda ] \Gamma _{{\mathrm {1}}}\) .
To show the latter requirement, we observe that \([ \vec{\ell } / \lambda ] \Gamma _{{\mathrm {2}}} , [ \vec{\ell } / \lambda ] \, \tau _{{\mathrm {1}}} \le [ \vec{\ell } / \lambda ] \Gamma ^{\prime } , [ \vec{\ell } / \lambda ] \, \tau \)  is equivalent to showing
\([ \vec{\ell } / \lambda ] ( \Gamma _{{\mathrm {2}}} , \mathit {x} : \tau _{{\mathrm {1}}} ) \le [ \vec{\ell } / \lambda ] ( \Gamma ^{\prime } , \mathit {x} : \tau )\)  for some \( \mathit {x} \notin \mathit {dom}( \Gamma _{{\mathrm {2}}} ) \) ,
whereby we have the required subtyping relationship from the application of itm:ctxt-sub-subtype.

T-Assert
assert( ) ;e : '
e : '  WF 
By induction hypothesis, the result holds if we can show \([ \vec{\ell } / \lambda ] \Gamma \models \varphi \)  which
follows from itm:ctxt-subst-assert (that \( \lambda \notin \mathbf {FCV} \, ( \varphi ) \)  follows
from the well-formedness of \(\varphi \)  with respect to \( \epsilon \) ).

[Substitution] 
If \( \Theta \mid \mathcal {L} \mid \Gamma \vdash \mathit {e} : \tau \operatorname{\Rightarrow }\Gamma ^{\prime } \)  and \( \mathit {x^{\prime }} \notin \mathit {dom}( \Gamma ) \) , then
\( \Theta \mid \mathcal {L} \mid [ \mathit {x^{\prime }} / \mathit {x} ] \, \Gamma \vdash \mathit {e} : [ \mathit {x^{\prime }} / \mathit {x} ] \, \tau \operatorname{\Rightarrow }[ \mathit {x^{\prime }} / \mathit {x} ] \, \Gamma ^{\prime } \) .


By straightforward induction of typing rules.
We now prove that if every variable satisfies its refinement in a type environment \(\Gamma \) ,
we must have \(\models [ \mathit {R} ] \, \left.{ \Gamma }\right. \) .
If \(\mathbf {SAT} \, ( \mathit {H} , \mathit {R} , \Gamma )\)  then \(\models [ \mathit {R} ] \, \left.{ \Gamma }\right. \) .


To show \(\models [ \mathit {R} ] \, \left.{ \Gamma }\right. \) , it suffices to show that for any \( \mathit {x} \in \mathit {dom}( \Gamma ) \)  where \(\Gamma ( \mathit {x} ) = \left\lbrace { \nu \operatorname{:}\mathbf {int}\mid \varphi }\right\rbrace  \) 
\(\models [ \mathit {R} ] \, [ \mathit {x} / \, \nu \, ] \, \varphi \)  holds. From \(\mathbf {SAT} \, ( \mathit {H} , \mathit {R} , \Gamma )\) , we must have \( \mathbf {SATv} ( \mathit {H} , \mathit {R} , \mathit {R} ( \mathit {x} ) , \Gamma ( \mathit {x} ) ) \) , whereby
we have \( \mathit {R} ( \mathit {x} ) \in \mathbb {Z} \)  and \([ \mathit {R} ] \, [ \mathit {R} ( \mathit {x} ) / \nu ] \varphi \) . As \([ \mathit {R} ] \, [ \mathit {x} / \, \nu \, ] \, \varphi \)  is equivalent to \([ \mathit {R} ] \, [ \mathit {R} ( \mathit {x} ) / \nu ] \varphi \) ,
and we have the desired result.
We prove that subtyping preserves the consistency relation in the following sense.
If \(\Gamma \le \Gamma ^{\prime }\)  and \(\mathbf {Cons} \, ( \mathit {H} , \mathit {R} , \Gamma )\)  then:

For any \( \mathit {x} \in \mathit {dom}( \Gamma ^{\prime } ) \) , \(\forall \, \mathit {a} \in \mathit {dom}( \mathit {H} ) . \mathbf {own} \, ( \mathit {H} , \mathit {R} ( \mathit {x} ) , \Gamma ( \mathit {x} ) ) ( \mathit {a} ) \le \mathbf {own} \, ( \mathit {H} , \mathit {R} ( \mathit {x} ) , \Gamma ^{\prime } ( \mathit {x} ) ) ( \mathit {a} )\)

\(\forall \, \mathit {a} \in \mathit {dom}( \mathit {H} ) . \mathbf {Own} \, ( \mathit {H} , \mathit {R} , \Gamma ^{\prime } ) ( \mathit {a} ) \le 1\)

If \(\Gamma \vdash \tau \le \tau ^{\prime }\)  and \( \mathbf {SATv} ( \mathit {H} , \mathit {R} , \mathit {v} , \tau ) \)  then \( \mathbf {SATv} ( \mathit {H} , \mathit {R} , \mathit {v} , \tau ^{\prime } ) \)

\(\mathbf {SAT} \, ( \mathit {H} , \mathit {R} , \Gamma ^{\prime } )\)

\(\mathbf {Cons} \, ( \mathit {H} , \mathit {R} , \Gamma ^{\prime } )\)


By induction on \(\Gamma \vdash \Gamma ( \mathit {x} ) \le \Gamma ^{\prime } ( \mathit {x} )\) .

Direct consequence of 1 and that \(\forall \, \mathit {a} \in \mathit {dom}( \mathit {H} ) . \mathbf {Own} \, ( \mathit {H} , \mathit {R} , \Gamma ) ( \mathit {a} ) \le 1\)  from \(\mathbf {Cons} \, ( \mathit {H} , \mathit {R} , \Gamma )\) .

From \(\mathbf {Cons} \, ( \mathit {H} , \mathit {R} , \Gamma )\)  we have \(\mathbf {SAT} \, ( \mathit {H} , \mathit {R} , \Gamma )\)  which by lem:sat-implies-gamma we have \(\models [ \mathit {R} ] \, \left.{ \Gamma }\right. \) .
We now proceed by induction on \(\Gamma \vdash \tau \le \tau ^{\prime }\) .

= { :int}  ' = { :int' }
  '

From \( \mathbf {SATv} ( \mathit {H} , \mathit {R} , \mathit {v} , \tau ) \)  we have \(\models [ \mathit {R} ] \, [ \mathit {v} / \nu ] \varphi \) .
We must show that \(\models [ \mathit {R} ] \, [ \mathit {v} / \nu ] \varphi ^{\prime }\) .
From \(\models \left.{ \Gamma }\right. \wedge \varphi \Rightarrow \varphi ^{\prime }\)  we must have
\(\models [ \mathit {R} ] \, [ \mathit {v} / \nu ] \left.{ \Gamma }\right. \wedge [ \mathit {R} ] \, [ \mathit {v} / \nu ] \varphi \Rightarrow [ \mathit {R} ] \, [ \mathit {v} / \nu ] \varphi ^{\prime }\)  is valid.
As \(\nu \)  does not appear free in \( \left.{ \Gamma }\right. \) , we have
\(\models [ \mathit {R} ] \, \left.{ \Gamma }\right. \wedge [ \mathit {R} ] \, [ \mathit {v} / \nu ] \varphi \Rightarrow [ \mathit {R} ] \, [ \mathit {v} / \nu ] \varphi ^{\prime }\)  is
valid whereby the result is immediate.
= p ref r1   ' = 'p ref r2
r2 r1

Immediate from the induction hypothesis.

Immediate consequence of 3 and that
\(\Gamma \le \Gamma ^{\prime }\)  implies that \(\Gamma \vdash \Gamma ( \mathit {x} ) \le \Gamma ^{\prime } ( \mathit {x} )\)  for any \( \mathit {x} \in \mathit {dom}( \Gamma ^{\prime } ) \) .

Immediate from 2 and 4.

To show consistency is preserved during evaluation, lem:sattosat,lem:ownequiv-preserv
show types equivalent according to \( \approx \)  are equivalent for the purposes
of \(\mathbf {own}\)  and \(\mathbf {SATv}\) . Then lem:ownadd,lem:satadd show that the
type addition operator \(+\)  “distributes” over \(\mathbf {SATv}\)  and \(\mathbf {own}\) .
[Type Equivalence Preserves Satisfiability] 
If \(\tau _{{\mathrm {1}}} \approx \tau _{{\mathrm {2}}}\) , then \( \mathbf {SATv} ( \mathit {H} , \mathit {R} , \mathit {v} , \tau _{{\mathrm {1}}} ) \iff \mathbf {SATv} ( \mathit {H} , \mathit {R} , \mathit {v} , \tau _{{\mathrm {2}}} ) \) .


We prove the forward case by induction on \( \bullet \vdash \tau _{{\mathrm {1}}} \le \tau _{{\mathrm {2}}}\)  as implied by
\(\tau _{{\mathrm {1}}} \approx \tau _{{\mathrm {2}}}\) . The inductive case follows from the IH. In the the base case
where \(\tau _{{\mathrm {1}}} = \left\lbrace { \nu \operatorname{:}\mathbf {int}\mid \varphi _{{\mathrm {1}}} }\right\rbrace  \)  and \(\tau _{{\mathrm {2}}} = \left\lbrace { \nu \operatorname{:}\mathbf {int}\mid \varphi _{{\mathrm {2}}} }\right\rbrace  \) , from \( \bullet \vdash \tau _{{\mathrm {1}}} \le \tau _{{\mathrm {2}}}\) 
we have that \(\models \varphi _{{\mathrm {1}}} \Rightarrow \varphi _{{\mathrm {2}}}\)  is valid, from which we must have \(\models [ \mathit {R} ] \, [ \mathit {v} / \nu ] \varphi _{{\mathrm {1}}} \Rightarrow [ \mathit {R} ] \, [ \mathit {v} / \nu ] \varphi _{{\mathrm {2}}}\) ,
where from the definition of \( \mathbf {SATv} ( \mathit {H} , \mathit {R} , \mathit {v} , \tau _{{\mathrm {1}}} ) \)  we must then have \( \mathbf {SATv} ( \mathit {H} , \mathit {R} , \mathit {v} , \tau _{{\mathrm {2}}} ) \) .
The backwards case follows similar reasoning by induction on \( \bullet \vdash \tau _{{\mathrm {2}}} \le \tau _{{\mathrm {1}}}\) .
If \(\tau _{{\mathrm {1}}} \approx \tau _{{\mathrm {2}}}\) , then \(\mathbf {own} \, ( \mathit {H} , \mathit {v} , \tau _{{\mathrm {1}}} ) = \mathbf {own} \, ( \mathit {H} , \mathit {v} , \tau _{{\mathrm {2}}} )\) .


By reasoning similar to that in lem:sattosat.
If \(\tau _{\mathit {p}} = \tau _{{\mathrm {1}}} + \tau _{{\mathrm {2}}}\) , then \(\mathbf {own} \, ( \mathit {H} , \mathit {v} , \tau _{\mathit {p}} ) = \mathbf {own} \, ( \mathit {H} , \mathit {v} , \tau _{{\mathrm {1}}} ) + \mathbf {own} \, ( \mathit {H} , \mathit {v} , \tau _{{\mathrm {2}}} )\) .


By induction on the rules used to derive \(\tau _{{\mathrm {1}}} + \tau _{{\mathrm {2}}} = \tau _{\mathit {p}}\) .
Tadd-Int
We have \(\mathbf {own} \, ( \mathit {H} , \mathit {v} , \tau _{\mathit {p}} ) = \mathbf {own} \, ( \mathit {H} , \mathit {v} , \tau _{{\mathrm {1}}} + \tau _{{\mathrm {2}}} )\) , where \(\tau _{{\mathrm {1}}} + \tau _{{\mathrm {2}}} = \left\lbrace { \nu \operatorname{:}\mathbf {int}\mid \varphi _{{\mathrm {1}}} \wedge \varphi _{{\mathrm {2}}} }\right\rbrace  \) ,
\(\mathbf {own} \, ( \mathit {H} , \mathit {v} , \tau _{{\mathrm {1}}} )\)  and \(\mathbf {own} \, ( \mathit {H} , \mathit {v} , \tau _{{\mathrm {2}}} )\) , where \(\tau _{{\mathrm {1}}} = \left\lbrace { \nu \operatorname{:}\mathbf {int}\mid \varphi _{{\mathrm {1}}} }\right\rbrace  , \tau _{{\mathrm {2}}} = \left\lbrace { \nu \operatorname{:}\mathbf {int}\mid \varphi _{{\mathrm {2}}} }\right\rbrace  \) .
From the definition of ownership, we have \(\mathbf {own} \, ( \mathit {H} , \mathit {v} , \tau _{\mathit {p}} ) = \mathbf {own} \, ( \mathit {H} , \mathit {v} , \tau _{{\mathrm {1}}} ) = \mathbf {own} \, ( \mathit {H} , \mathit {v} , \tau _{{\mathrm {2}}} ) = \emptyset \) .
It is thus trivial that \(\mathbf {own} \, ( \mathit {H} , \mathit {v} , \tau _{\mathit {p}} ) = \mathbf {own} \, ( \mathit {H} , \mathit {v} , \tau _{{\mathrm {1}}} ) + \mathbf {own} \, ( \mathit {H} , \mathit {v} , \tau _{{\mathrm {2}}} )\) .
Tadd-Ref
We assume \(\mathit {v} \, = \, \mathit {a}\)  and \( \mathit {a} \in \mathit {dom}( \mathit {H} ) \) , otherwise the result trivially holds.
We have \(\mathbf {own} \, ( \mathit {H} , \mathit {v} , \tau _{\mathit {p}} ) = \mathbf {own} \, ( \mathit {H} , \mathit {v} , \tau _{{\mathrm {1}}} + \tau _{{\mathrm {1}}} )\) , where \(\tau _{{\mathrm {1}}} + \tau _{{\mathrm {2}}} = ( \tau ^{\prime }_{{\mathrm {1}}} + \tau ^{\prime }_{{\mathrm {2}}} ) \operatorname{\mathbf {ref}}^{ r_{{\mathrm {1}}} + r_{{\mathrm {2}}} } \) ,
and \(\tau _{{\mathrm {1}}} = \tau ^{\prime }_{{\mathrm {1}}} \operatorname{\mathbf {ref}}^{ r_{{\mathrm {1}}} } \) , \(\tau _{{\mathrm {2}}} = \tau ^{\prime }_{{\mathrm {2}}} \operatorname{\mathbf {ref}}^{ r_{{\mathrm {2}}} } \) .
From the definition of ownership, we have \(\mathbf {own} \, ( \mathit {H} , \mathit {v} , \tau _{\mathit {p}} ) = \lbrace  \mathit {a} \mapsto r_{{\mathrm {1}}} + r_{{\mathrm {2}}} \rbrace  + \mathbf {own} \, ( \mathit {H} , \mathit {H} ( \mathit {v} ) , \tau ^{\prime }_{{\mathrm {1}}} + \tau ^{\prime }_{{\mathrm {2}}} )\)  and:
\(\mathbf {own} \, ( \mathit {H} , \mathit {v} , \tau _{{\mathrm {1}}} ) + \mathbf {own} \, ( \mathit {H} , \mathit {v} , \tau _{{\mathrm {2}}} ) & = \lbrace  \mathit {a} \mapsto r_{{\mathrm {1}}} \rbrace  + \mathbf {own} \, ( \mathit {H} , \mathit {H} ( \mathit {v} ) , \tau ^{\prime }_{{\mathrm {1}}} ) + \lbrace  \mathit {a} \mapsto r_{{\mathrm {2}}} \rbrace  + \mathbf {own} \, ( \mathit {H} , \mathit {H} ( \mathit {v} ) , \tau ^{\prime }_{{\mathrm {2}}} ) \\& = \lbrace  \mathit {a} \mapsto r_{{\mathrm {1}}} + r_{{\mathrm {2}}} \rbrace  + \mathbf {own} \, ( \mathit {H} , \mathit {H} ( \mathit {v} ) , \tau ^{\prime }_{{\mathrm {1}}} ) + \mathbf {own} \, ( \mathit {H} , \mathit {H} ( \mathit {v} ) , \tau ^{\prime }_{{\mathrm {2}}} )\) 

By the induction hypothesis, have that \(\mathbf {own} \, ( \mathit {H} , \mathit {H} ( \mathit {v} ) , \tau ^{\prime }_{{\mathrm {1}}} + \tau ^{\prime }_{{\mathrm {2}}} ) = \mathbf {own} \, ( \mathit {H} , \mathit {H} ( \mathit {v} ) , \tau ^{\prime }_{{\mathrm {1}}} ) + \mathbf {own} \, ( \mathit {H} , \mathit {H} ( \mathit {v} ) , \tau ^{\prime }_{{\mathrm {2}}} )\)  and can conclude that \(\mathbf {own} \, ( \mathit {H} , \mathit {v} , \tau _{\mathit {p}} ) = \mathbf {own} \, ( \mathit {H} , \mathit {v} , \tau _{{\mathrm {1}}} ) + \mathbf {own} \, ( \mathit {H} , \mathit {v} , \tau _{{\mathrm {2}}} )\) .
If \(\tau _{\mathit {p}} = \tau _{{\mathrm {1}}} + \tau _{{\mathrm {2}}}\) , we have
\( \mathbf {SATv} ( \mathit {H} , \mathit {R} , v , \tau _{\mathit {p}} ) \)  iff. \( \mathbf {SATv} ( \mathit {H} , \mathit {R} , v , \tau _{{\mathrm {1}}} ) \)  and \( \mathbf {SATv} ( \mathit {H} , \mathit {R} , v , \tau _{{\mathrm {2}}} ) \) 


By induction on the rules used to derive \(\tau _{{\mathrm {1}}} + \tau _{{\mathrm {2}}}\) . In the following
we only prove the forward direction of the implication; the backwards
direction is symmetric.
Tadd-Int
We have \( \mathbf {SATv} ( \mathit {H} , \mathit {R} , v , \tau _{{\mathrm {1}}} + \tau _{{\mathrm {2}}} ) \) , where \(\tau _{{\mathrm {1}}} + \tau _{{\mathrm {2}}} = \left\lbrace { \nu \operatorname{:}\mathbf {int}\mid \varphi _{{\mathrm {1}}} \wedge \varphi _{{\mathrm {2}}} }\right\rbrace  \) ,
we must show \( \mathbf {SATv} ( \mathit {H} , \mathit {R} , v , \tau _{{\mathrm {1}}} ) \)  and \( \mathbf {SATv} ( \mathit {H} , \mathit {R} , v , \tau _{{\mathrm {2}}} ) \) ,
where \(\tau _{{\mathrm {1}}} = \left\lbrace { \nu \operatorname{:}\mathbf {int}\mid \varphi _{{\mathrm {1}}} }\right\rbrace  , \tau _{{\mathrm {2}}} = \left\lbrace { \nu \operatorname{:}\mathbf {int}\mid \varphi _{{\mathrm {2}}} }\right\rbrace  \) .
From the definition of \(\mathbf {SATv}\) , we must show \([ \mathit {R} ] \, [ v / \nu ] \varphi _{{\mathrm {1}}}\)  and \([ \mathit {R} ] \, [ \mathit {v} / \nu ] \varphi _{{\mathrm {2}}}\) .
From \( \mathbf {SATv} ( \mathit {H} , \mathit {R} , v , \tau _{{\mathrm {1}}} + \tau _{{\mathrm {2}}} ) \)  we have \([ \mathit {R} ] \, [ \mathit {v} / \mathit {x} ] ( \varphi _{{\mathrm {1}}} \wedge \varphi _{{\mathrm {2}}} )\) .
It is immediate that for any value \(v\)  such that \([ \mathit {R} ] \, [ \mathit {v} / \nu ] ( \varphi _{{\mathrm {1}}} \wedge \varphi _{{\mathrm {2}}} )\) , we must have \([ \mathit {R} ] \, [ \mathit {v} / \nu ] \varphi _{{\mathrm {1}}}\)  and \([ \mathit {R} ] \, [ \mathit {v} / \nu ] \varphi _{{\mathrm {2}}}\) .
We then conclude \( \mathbf {SATv} ( \mathit {H} , \mathit {R} , v , \tau _{{\mathrm {1}}} + \tau _{{\mathrm {2}}} ) \)  implies \( \mathbf {SATv} ( \mathit {H} , \mathit {R} , v , \tau _{{\mathrm {1}}} ) \)  and \( \mathbf {SATv} ( \mathit {H} , \mathit {R} , v , \tau _{{\mathrm {2}}} ) \) .
Tadd-Ref
Immediate from the definition of \(\mathbf {SATv}\)  and the inductive hypothesis.
The valid substitution relation, written \( \mathit {R} \vdash _{vs} \tau \)  is the smallest relation closed
under the following rules:
[]
  x FPV   ( ) { } .   n . R ( x ) = n

R vs { :int}

[]
R vs 
R vs ref r
If \( \vec{\ell } \vdash _{\mathit {WF}} \Gamma \)  and \(\mathbf {Cons} \, ( \mathit {H} , \mathit {R} , \Gamma )\) , then \(\forall \, \mathit {x} \in \mathit {dom}( \Gamma ) . \mathit {R} \vdash _{vs} \Gamma ( \mathit {x} ) \) .


By \(\mathbf {Cons} \, ( \mathit {H} , \mathit {R} , \Gamma )\) , all integer variables in \(\Gamma \)  must be in
the domain of \(\mathit {R}\)  and must be an integer. From \( \vec{\ell } \vdash _{\mathit {WF}} \Gamma \) , any free variables
in any refinement of any type in \(\Gamma \)  must be an integer valued variable in \(\Gamma \) ,
which gives the required result.
We will write \( \mathit {R} \sqsubseteq \mathit {R^{\prime }} \)  to denote two register files such that:

\( \mathit {dom}( \mathit {R} ) \subseteq \mathit {dom}( \mathit {R^{\prime }} ) \) , and

\(\forall \, \mathit {x} \in \mathit {dom}( \mathit {R} ) . \mathit {R} ( \mathit {x} ) = \mathit {R^{\prime }} ( \mathit {x} )\)

Two heaps \(\mathit {H}\)  and \(\mathit {H^{\prime }}\)  are equivalent modulo \(\mathit {a}\), written \( \mathit {H} \approx _ \mathit {a} \mathit {H^{\prime }} \)  if:

\( \mathit {dom}( \mathit {H} ) = \mathit {dom}( \mathit {H^{\prime }} ) \)

\(\forall \, \mathit {a^{\prime }} \in \mathit {dom}( \mathit {H} ) . \mathit {a^{\prime }} \, \ne \, \mathit {a} \Rightarrow \mathit {H} ( \mathit {a} ) = \mathit {H} ( \mathit {a^{\prime }} )\)

For any \(n\) , \( \mathit {H} \vdash \mathit {a} \Downarrow n \)  iff \( \mathit {H^{\prime }} \vdash \mathit {a} \Downarrow n \)

For any type \(\tau = \top _{\mathit {n}}\) , \(\mathit {H}, \mathit {v}\) , \(\mathbf {own} \, ( \mathit {H} , \mathit {v} , \top _{\mathit {n}} ) = \emptyset \) .


By induction on \(\tau \) . In the base case, the result is trivial.
Then consider the case where \(\tau = \top _{{\mathit {n}-1}} \operatorname{\mathbf {ref}}^{ 0 } \) . If \( \mathit {v} \notin \textbf {Addr} \) ,
or if \(\mathit {v} \, = \, \mathit {a}\)  and \( \mathit {a} \notin \mathit {dom}( \mathit {H} ) \) , then the result trivially holds.
Otherwise the result holds from the inductive hypothesis, the definition of \(+\)  and \(\lbrace  \mathit {a} \mapsto 0 \rbrace \) .
[Heap Update Ownership Preservation] 
If \( \mathit {H} \approx _ \mathit {a} \mathit {H^{\prime }} \)  and \(\mathbf {own} \, ( \mathit {H} , \mathit {v} , \tau ) ( \mathit {a} ) = 0\) , then
\(\mathbf {own} \, ( \mathit {H} , \mathit {v} , \tau ) = \mathbf {own} \, ( \mathit {H^{\prime }} , \mathit {v} , \tau )\) .


By induction on the shape of \(\tau \) . If \(\tau = \left\lbrace { \nu \operatorname{:}\mathbf {int}\mid \varphi }\right\rbrace  \)  then
the result trivially holds. Otherwise, \(\tau = \tau ^{\prime } \operatorname{\mathbf {ref}}^{ r } \) . We assume
that \(\mathit {v} \, = \, \mathit {a^{\prime \prime }}\)  and \( \mathit {a^{\prime \prime }} \in \mathit {dom}( \mathit {H} ) \)  (otherwise the result
trivially holds, as \( \mathit {dom}( \mathit {H} ) = \mathit {dom}( \mathit {H^{\prime }} ) \)  by \( \mathit {H} \approx _ \mathit {a} \mathit {H^{\prime }} \) ).
Consider the case where \(\mathit {a^{\prime \prime }} \, = \, \mathit {a}\) . By definition
\(\mathbf {own} \, ( \mathit {H} , \mathit {a} , \tau ) = \lbrace  \mathit {a} \mapsto r \rbrace  + \mathbf {own} \, ( \mathit {H} , \mathit {H} ( \mathit {a} ) , \tau ^{\prime } )\) , and by the
assumption that \(\mathbf {own} \, ( \mathit {H} , \mathit {a} , \tau ) ( \mathit {a} ) = 0\)  we must have that
\(r = 0\) . Further, by the ownership well-formedness of types,
we must have \(\tau ^{\prime } = \top _{\mathit {n}}\)  for some \(n\) , thus by lem:top-type-empty-omap
we have \(\mathbf {own} \, ( \mathit {H} , \mathit {v} , \tau ) = \emptyset = \lbrace  \mathit {a} \mapsto 0 \rbrace  + \mathbf {own} \, ( \mathit {H^{\prime }} , \mathit {H^{\prime }} ( \mathit {a} ) , \top _{\mathit {n}} ) = \mathbf {own} \, ( \mathit {H^{\prime }} , \mathit {v} , \tau )\) .
Finally, consider the case where \(\mathit {a^{\prime \prime }} \, \ne \, \mathit {a}\) . Then from the
definition of \(\mathbf {own} \, ( \mathit {H} , \mathit {a^{\prime \prime }} , \tau )\)  and our assumption that
\(\mathbf {own} \, ( \mathit {H} , \mathit {a^{\prime \prime }} , \tau ) ( \mathit {a} ) = 0\) , we have \(\mathbf {own} \, ( \mathit {H} , \mathit {H} ( \mathit {a^{\prime \prime }} ) , \tau ^{\prime } ) ( \mathit {a} ) = 0\) ,
and the result holds from the inductive hypothesis and that \(\mathit {H} ( \mathit {a^{\prime \prime }} ) \, = \, \mathit {H^{\prime }} ( \mathit {a^{\prime \prime }} )\) .
For any \(\mathit {H}\) , \(\mathit {R}\) , \(\mathit {v}\) , and \(\tau \) , if \( \mathbf {SATv} ( \mathit {H} , \mathit {R} , \mathit {v} , \tau ) \)  then \( \mathit {H} \vdash \mathit {v} \Downarrow | \tau | \) 


By induction on \(\tau \)  and the definition of \(\mathbf {SATv}\) .
For any \(n\) , if \( \mathit {H} \vdash v \Downarrow n \)  then for any \(\mathit {R}\) , \( \mathbf {SATv} ( \mathit {H} , \mathit {R} , \mathit {v} , \top _{\mathit {n}} ) \) .


By induction on \(n\) . In the base case, by inversion on \( \mathit {H} \vdash \mathit {v} \Downarrow 0 \)  we have
\( \mathit {v} \in \mathbb {Z} \)  and as \([ \mathit {R} ] \, [ \mathit {v} / \nu ] \top \Rightarrow \top \) , we conclude \( \mathbf {SATv} ( \mathit {H} , \mathit {R} , \mathit {v} , \top _{{\mathrm {0}}} ) \) .
For \(n > 0\) , by inversion on \( \mathit {H} \vdash v \Downarrow n \)  we have that
\(\mathit {v} \, = \, \mathit {a}\) , \( \mathit {a} \in \mathit {dom}( \mathit {H} ) \) , and \( \mathit {H} \vdash \mathit {H} ( \mathit {a} ) \Downarrow n - 1 \) ,
whereby the result holds from the inductive hypothesis.
[Heap Update Consistency Preservation] 
If \( \mathit {H} \approx _ \mathit {a} \mathit {H^{\prime }} \)  and \(\mathbf {own} \, ( \mathit {H} , \mathit {v} , \tau ) ( \mathit {a} ) = 0\)  and \( \mathbf {SATv} ( \mathit {H} , \mathit {R} , \mathit {v} , \tau ) \) , then \( \mathbf {SATv} ( \mathit {H^{\prime }} , \mathit {R} , \mathit {v} , \tau ) \) .


By induction on the shape of \(\tau \) . The base case where
\(\tau = \left\lbrace { \nu \operatorname{:}\mathbf {int}\mid \varphi }\right\rbrace  \)  is trivial. We therefore consider the case
where \(\mathit {v} \, = \, \mathit {a^{\prime }}\)  and \(\tau = \tau ^{\prime } \operatorname{\mathbf {ref}}^{ r } \) .
We first consider the case where \(\mathit {a^{\prime }} \, = \, \mathit {a}\) , then by
our assumption that \(\mathbf {own} \, ( \mathit {H} , \mathit {a} , \tau ) ( \mathit {a} ) = 0\) , we must have that
\(\tau = \tau ^{\prime } \operatorname{\mathbf {ref}}^{ 0 } \) , whereby \(\tau = \top _{\mathit {n}}\)  for some \(\mathit {n}\) .
From \( \mathbf {SATv} ( \mathit {H} , \mathit {R} , \mathit {a} , \tau ) \)  and lem:sat-implies-shape-cons, we must have that
\( \mathit {H} \vdash \mathit {a} \Downarrow | \tau | \) ,
and from \( \mathit {H} \approx _ \mathit {a} \mathit {H^{\prime }} \) , we therefore have that \( \mathit {H^{\prime }} \vdash \mathit {a} \Downarrow | \tau | \) 
whereby the result holds from lem:top-type-sat-all.
Otherwise, we have that \(\mathit {a^{\prime }} \, \ne \, \mathit {a}\) , and by definition we must have that
\(\mathbf {own} \, ( \mathit {H} , \mathit {H} ( \mathit {a} ) , \tau ^{\prime } ) ( \mathit {a} ) = 0\)  and \(\mathit {H^{\prime }} ( \mathit {a} ) \, = \, \mathit {H} ( \mathit {a} )\)  hence the result follows
from the inductive hypothesis.
[Register Weakening] 
If \( \mathbf {SATv} ( \mathit {H} , \mathit {R} , v , \tau ) \)  and \( \mathit {R} \vdash _{vs} \tau \) ,
then for any \(\mathit {R^{\prime }}\)  such that \( \mathit {R} \sqsubseteq \mathit {R^{\prime }} \) , \( \mathbf {SATv} ( \mathit {H} , \mathit {R^{\prime }} , v , \tau ) \) .


By induction on the shape of \(\tau \) . If \(\tau = \tau ^{\prime } \operatorname{\mathbf {ref}}^{ r } \) , then
the result follows from the inductive hypothesis.
We therefore consider the case where
\(\tau = \left\lbrace { \nu \operatorname{:}\mathbf {int}\mid \varphi }\right\rbrace  \) . Without loss of generality, we consider
the case where \( \mathit {dom}( \mathit {R^{\prime }} ) \setminus \mathit {dom}( \mathit {R} ) = \left\lbrace {x}\right\rbrace \) ,
and \(\mathit {R^{\prime }} ( \mathit {x} ) \, = \, n\) . (If \(\mathit {R^{\prime }} ( \mathit {x} ) \, = \, \mathit {a}\) , the extra binding
also has no effect, and the case where more than one binding is
added follows from \(n\)  applications of the following argument.)
From \( \mathbf {SATv} ( \mathit {H} , \mathit {R} , v , \tau ) \) , we conclude that \( v \in \mathbb {Z} \)  and that
\([ \mathit {R} ] \, [ v / \nu ] \varphi \) . If \( \mathit {x} \notin \mathbf {FPV} \, ( \varphi ) \)  then \([ \mathit {R} ] \, [ v / \nu ] \varphi \iff [ \mathit {R^{\prime }} ] \, [ v / \nu ] \varphi \) 
and the result holds trivially. Otherwise, if \( \mathit {x} \in \mathbf {FPV} \, ( \varphi ) \)  and \( \mathit {x} \notin \mathit {dom}( \mathit {R} ) \) 
then \(\mathit {R}\)  is not a valid substitution, violating our assumption.
[Heap Extension Consistency Preservation] 
If we have heap \(H\) , such that \( \mathbf {SATv} ( \mathit {H} , \mathit {R} , \mathit {v} , \tau ) \) , for any heap
\(\mathit {H^{\prime }} = \mathit {H} \lbrace  \mathit {a} \mapsto \mathit {v^{\prime }} \rbrace , \mathit {a} \notin \mathit {dom}( \mathit {H} ) \) , then we have \( \mathbf {SATv} ( \mathit {H^{\prime }} , \mathit {R} , \mathit {v} , \tau ) \) .


By induction on the shape of \(\tau \) .
The base case where \(\tau = \left\lbrace { \nu \operatorname{:}\mathbf {int}\mid \varphi }\right\rbrace  \)  is trivial.
Next, we consider the case where \(\tau = \tau ^{\prime } \operatorname{\mathbf {ref}}^{ r } \) .
We must show that \( \mathit {v} \in \mathit {dom}( \mathit {H^{\prime }} ) \)  and \( \mathbf {SATv} ( \mathit {H^{\prime }} , \mathit {R} , \mathit {H^{\prime }} ( \mathit {v} ) , \tau ^{\prime } ) \) .
The first condition is immediately satisfied by inversion on \( \mathbf {SATv} ( \mathit {H} , \mathit {R} , \mathit {v} , \tau ^{\prime } ) \) ,
and from \( \mathit {a} \notin \mathit {dom}( \mathit {H} ) \) , we have \(v\ne a\) , which gives that \(H^{\prime }(v)=H(v)\) .
That is we must show \( \mathbf {SATv} ( \mathit {H^{\prime }} , \mathit {R} , \mathit {H} ( \mathit {v} ) , \tau ^{\prime } ) \) , which is follows from
the induction hypothesis.
[Heap Extension Ownership Preservation]

If \( \mathbf {SATv} ( \mathit {H} , \mathit {R} , \mathit {v} , \tau ) \) , then for any \( \mathit {a} \notin \mathit {dom}( \mathit {H} ) \) 
\(\mathbf {own} \, ( \mathit {H} , \mathit {v} , \tau ) = \mathbf {own} \, ( \mathit {H} \lbrace  \mathit {a} \mapsto \mathit {v^{\prime }} \rbrace  , \mathit {v} , \tau )\)  for any value \(\mathit {v^{\prime }}\) .


By induction on \(\tau \) . The base case is trivial as \(\mathbf {own} \, ( \mathit {H} , \mathit {v} , \left\lbrace { \nu \operatorname{:}\mathbf {int}\mid \varphi }\right\rbrace  ) = \emptyset = \mathbf {own} \, ( \mathit {H} \lbrace  \mathit {a} \mapsto \mathit {v} \rbrace  , \mathit {v} , \left\lbrace { \nu \operatorname{:}\mathbf {int}\mid \varphi }\right\rbrace  )\) .
We therefore consider the case where \(\tau = \tau ^{\prime } \operatorname{\mathbf {ref}}^{ r } \) .
From \( \mathbf {SATv} ( \mathit {H} , \mathit {R} , \mathit {v} , \tau ) \)  we must have that \(\mathit {v} \, = \, \mathit {a^{\prime }}\)  and
\( \mathit {a^{\prime }} \in \mathit {dom}( \mathit {H} ) \)  (and by extension \( \mathit {a^{\prime }} \in \mathit {dom}( \mathit {H} \lbrace  \mathit {a} \mapsto \mathit {v^{\prime }} \rbrace  ) \) ).
From the definition of the ownership function, we have that \(\mathbf {own} \, ( \mathit {H} , \mathit {v} , \tau ) = \mathbf {own} \, ( \mathit {H} , \mathit {H} ( \mathit {a} ) , \tau ^{\prime } ) + \lbrace  \mathit {a^{\prime }} \mapsto r \rbrace \) .
and \(\mathbf {own} \, ( \mathit {H} \lbrace  \mathit {a} \mapsto \mathit {v^{\prime }} \rbrace  , \mathit {v} , \tau ) = \mathbf {own} \, ( \mathit {H} \lbrace  \mathit {a} \mapsto \mathit {v^{\prime }} \rbrace  , \mathit {H} \lbrace  \mathit {a} \mapsto \mathit {v^{\prime }} \rbrace  ( \mathit {a^{\prime }} ) , \tau ^{\prime } ) + \lbrace  \mathit {a^{\prime }} \mapsto r \rbrace \) 
Then from our requirement that \( \mathit {a} \notin \mathit {dom}( \mathit {H} ) \) , we have \(\mathit {a} \, \ne \, \mathit {a^{\prime }}\)  and therefore
\(\mathit {H} ( \mathit {a^{\prime }} ) \, = \, \mathit {H} \lbrace  \mathit {a} \mapsto \mathit {v^{\prime }} \rbrace  ( \mathit {a^{\prime }} )\) , whereby the result holds from the inductive hypothesis.
[Environment Weakening] 
Define the partial operation \( \Gamma _{{\mathrm {1}}} \uplus \Gamma _{{\mathrm {2}}} \)  for two environments such \( \mathit {dom}( \Gamma _{{\mathrm {1}}} ) \cap \mathit {dom}( \Gamma _{{\mathrm {2}}} ) = \emptyset \) :
\(( \Gamma _{{\mathrm {1}}} \uplus \Gamma _{{\mathrm {2}}} ) \quad ( \mathit {x} ) = {\left\lbrace \begin{array}{ll}\Gamma _{{\mathrm {1}}} \quad ( \mathit {x} ) & \mathit {x} \in \mathit {dom}( \Gamma _{{\mathrm {1}}} ) \\\Gamma _{{\mathrm {2}}} \quad ( \mathit {x} ) & \mathit {x} \in \mathit {dom}( \Gamma _{{\mathrm {2}}} ) \\\textit {undef} & o.w.\end{array}\right.}\) 
Then, for any \(\Gamma \)  and \(\Gamma ^{\prime \prime }\)  where \( \mathit {dom}( \Gamma ) \cap \mathit {dom}( \Gamma ^{\prime \prime } ) = \emptyset \) :

\(\Gamma \vdash \tau _{{\mathrm {1}}} \le \tau _{{\mathrm {2}}}\)  implies \( \Gamma \uplus \Gamma ^{\prime \prime } \vdash \tau _{{\mathrm {1}}} \le \tau _{{\mathrm {2}}}\)

\(\Gamma \le \Gamma ^{\prime }\)  implies \( \Gamma \uplus \Gamma ^{\prime \prime } \le \Gamma ^{\prime } \uplus \Gamma ^{\prime \prime } \)

If \( \Theta \mid \mathcal {L} \mid \Gamma \vdash \mathit {e} : \tau \operatorname{\Rightarrow }\Gamma ^{\prime } \) , \( \mathcal {L} \vdash _{\mathit {WF}} \Gamma \uplus \Gamma ^{\prime \prime } \) , and \( \mathcal {L} \vdash _{\mathit {WF}} \Gamma ^{\prime } \uplus \Gamma ^{\prime \prime } \) , then \( \Theta \mid \mathcal {L} \mid \Gamma \uplus \Gamma ^{\prime \prime } \vdash \mathit {e} : \tau \operatorname{\Rightarrow }\Gamma ^{\prime \prime } \uplus \Gamma \)


As in the proof of lem:ctxt-substitution (part itm:ctxt-sub-subtype), at the root of
the subtyping derivation is a logical judgment of the form
\(\models \left.{ \Gamma }\right. \wedge \varphi _{{\mathrm {1}}} \Rightarrow \varphi _{{\mathrm {2}}}\)  which can be shown to be valid. We
must then show that \(\models \left.{ \Gamma \uplus \Gamma ^{\prime \prime } }\right. \wedge \varphi _{{\mathrm {1}}} \Rightarrow \varphi _{{\mathrm {2}}}\)  is valid. As
\( \left.{ \Gamma ^{\prime \prime } \uplus \Gamma }\right. \wedge \varphi _{{\mathrm {1}}} = \left.{ \Gamma ^{\prime \prime } }\right. \wedge \left.{ \Gamma }\right. \wedge \varphi \)  only strengthens the pre-condition
\( \left.{ \Gamma }\right. \wedge \varphi _{{\mathrm {1}}}\) , \(\models \left.{ \Gamma ^{\prime \prime } \uplus \Gamma }\right. \wedge \varphi _{{\mathrm {1}}} \Rightarrow \varphi _{{\mathrm {2}}}\)  must
also be valid.

It suffices to show that \( \Gamma \uplus \Gamma ^{\prime \prime } \vdash ( \Gamma \uplus \Gamma ^{\prime \prime } ) ( \mathit {x} ) \le ( \Gamma ^{\prime } \uplus \Gamma ^{\prime \prime } ) ( \mathit {x} )\)  for
any arbitrary \( \mathit {x} \in \mathit {dom}( \Gamma ^{\prime } \uplus \Gamma ^{\prime \prime } ) \) . If \( \mathit {x} \in \mathit {dom}( \Gamma ^{\prime } ) \)  then we must have
\(\Gamma \vdash \Gamma ( \mathit {x} ) \le \Gamma ^{\prime } ( \mathit {x} )\)  by inversion on \(\Gamma \le \Gamma ^{\prime }\) ,
whereby \( \Gamma \uplus \Gamma ^{\prime \prime } \vdash ( \Gamma \uplus \Gamma ^{\prime \prime } ) ( \mathit {x} ) = \Gamma ( \mathit {x} ) \le \Gamma ^{\prime } \uplus \Gamma ^{\prime \prime } ( \mathit {x} ) = \Gamma ^{\prime } ( \mathit {x} )\)  from part 1.
If \( \mathit {x} \notin \mathit {dom}( \Gamma ^{\prime } ) \) , then we must show \(( \Gamma \uplus \Gamma ^{\prime \prime } ) \vdash \Gamma ^{\prime \prime } ( \mathit {x} ) \le \Gamma ^{\prime \prime } ( \mathit {x} )\) , which trivially holds.

By induction on the typing derivation of
\( \Theta \mid \mathcal {L} \mid \Gamma \vdash \mathit {e} : \tau \operatorname{\Rightarrow }\Gamma ^{\prime } \) . We assume that the variables bound in
any let expressions that appear within \(\mathit {e}\)  are not in the domain
of \(\Gamma ^{\prime \prime }\) ; this requirement can be easily enforced with
consistent renaming and is preserved during evaluation. The only interesting cases are
T-Sub and T-Assert and the let bindings;
the other cases follow from the induction hypothesis.
We now prove the relevant cases.
T-Let
L letx = y ine : '
L [ y 1  y  y = 1  x ] , x : 2  x  x = 2  y e : '
( y ) = 1 + 2 x dom( ' )

Let \( \Gamma ^{\prime \prime \prime } = \Gamma ^{\prime \prime } \uplus \Gamma [ \mathit {y} \hookleftarrow \tau _{{\mathrm {1}}} \wedge _{ \mathit {y} } \mathit {y} =_{ \tau _{{\mathrm {1}}} } \mathit {x} ] , \mathit {x} : \tau _{{\mathrm {2}}} \wedge _{ \mathit {x} } \mathit {x} =_{ \tau _{{\mathrm {2}}} } \mathit {y} \) .
To use the inductive hypothesis, we must show that
\( \mathcal {L} \vdash _{\mathit {WF}} \Gamma ^{\prime \prime \prime } \)  and \( \mathcal {L} \vdash _{\mathit {WF}} \Gamma ^{\prime } \uplus \Gamma ^{\prime \prime } \) . The latter holds by assumption.
To show the former, it suffices
to show \( \mathcal {L} \mid \Gamma ^{\prime \prime \prime } \vdash _{\mathit {WF}} \tau _{{\mathrm {1}}} \wedge _{ \mathit {y} } \mathit {y} =_{ \tau _{{\mathrm {1}}} } \mathit {x} \)  and \( \mathcal {L} \mid \Gamma ^{\prime \prime \prime } \vdash _{\mathit {WF}} \tau _{{\mathrm {2}}} \wedge _{ \mathit {x} } \mathit {x} =_{ \tau _{{\mathrm {2}}} } \mathit {y} \) .
From the assumed well-formedness \( \mathcal {L} \vdash _{\mathit {WF}} \Gamma \uplus \Gamma ^{\prime \prime } \) , we must have \( \mathcal {L} \mid \Gamma \uplus \Gamma ^{\prime \prime } \vdash _{\mathit {WF}} \tau _{{\mathrm {1}}} + \tau _{{\mathrm {2}}} \) ,
and in particular \( \mathcal {L} \mid \Gamma \uplus \Gamma ^{\prime \prime } \vdash _{\mathit {WF}} \tau _{{\mathrm {1}}} \)  and \( \mathcal {L} \mid \Gamma \uplus \Gamma ^{\prime \prime } \vdash _{\mathit {WF}} \tau _{{\mathrm {2}}} \) . From this
we conclude both conditions hold. To show the well-typing of the overall let expression,
we must show \( \mathit {x} \notin \mathit {dom}( \Gamma ^{\prime } \uplus \Gamma ^{\prime \prime } ) \) , which follows from our assumption and \( \mathit {x} \notin \mathit {dom}( \Gamma ^{\prime } ) \) .
Finally, we must also show that \( \mathcal {L} \mid \Gamma ^{\prime } \uplus \Gamma ^{\prime \prime } \vdash _{\mathit {WF}} \tau \) . From \( \mathcal {L} \mid \Gamma ^{\prime } \vdash _{\mathit {WF}} \tau \) 
and the fact that\(\forall \, \mathit {x} \in \mathit {dom}( \Gamma ^{\prime } ) . \Gamma ^{\prime } ( \mathit {x} ) = \left\lbrace { \nu \operatorname{:}\mathbf {int}\mid \_ }\right\rbrace  \)  iff
\(( \Gamma ^{\prime } \uplus \Gamma ^{\prime \prime } ) ( \mathit {x} ) = \left\lbrace { \nu \operatorname{:}\mathbf {int}\mid \_ }\right\rbrace  \) , we must have \( \mathcal {L} \mid \Gamma ^{\prime } \uplus \Gamma ^{\prime \prime } \vdash _{\mathit {WF}} \tau \) .

Cases T-LetInt, T-Mkref, T-Mkref, T-Deref, T-Call: 
Similar to the reasoning in T-Let.
T-Sub
1  L 1 e : 2 2
2 , 2 ' ,

From the rules for subtyping, we must have
\( \mathit {dom}( \Gamma _{{\mathrm {1}}} ) \subseteq \mathit {dom}( \Gamma ) \)  and \( \mathit {dom}( \Gamma ^{\prime } ) \subseteq \mathit {dom}( \Gamma _{{\mathrm {2}}} ) \) . A simple inductive argument
gives that \( \mathit {dom}( \Gamma _{{\mathrm {2}}} ) \subseteq \mathit {dom}( \Gamma _{{\mathrm {1}}} ) \) , therefore we have \( \mathit {dom}( \Gamma ^{\prime } ) \subseteq \mathit {dom}( \Gamma _{{\mathrm {1}}} ) \) .
Let \(\mathcal {LV}\)  be the set of free variables in the refinements of \(\Gamma ^{\prime \prime }\) 
that are not in the domain of \(\Gamma ^{\prime \prime }\) . From the assumed well-formedness of
\( \mathcal {L} \vdash _{\mathit {WF}} \Gamma ^{\prime } \uplus \Gamma ^{\prime \prime } \) , we must have that
\(\forall x \in \mathcal {LV}. \mathit {x} \in \mathit {dom}( \Gamma ^{\prime } ) \wedge \Gamma ^{\prime } ( \mathit {x} ) = \left\lbrace { \nu \operatorname{:}\mathbf {int}\mid \_ }\right\rbrace  \) . Thus,
\(\mathcal {LV} \subseteq \Gamma _{{\mathrm {1}}}\)  and \(\mathcal {LV} \subseteq \Gamma _{{\mathrm {2}}}\) . Further, by definition,
for any \(\Gamma _{\mathit {p}} \le \Gamma _{\mathit {q}}\) , if \(\Gamma _{\mathit {q}} ( \mathit {x} ) = \left\lbrace { \nu \operatorname{:}\mathbf {int}\mid \_ }\right\rbrace  \)  then \(\Gamma _{\mathit {p}} ( \mathit {x} ) = \left\lbrace { \nu \operatorname{:}\mathbf {int}\mid \_ }\right\rbrace  \) ,
i.e. subtyping preserves simple types.
We conclude that \( \mathcal {L} \vdash _{\mathit {WF}} \Gamma _{{\mathrm {1}}} \uplus \Gamma ^{\prime \prime } \)  and
\( \mathcal {L} \vdash _{\mathit {WF}} \Gamma _{{\mathrm {2}}} \uplus \Gamma ^{\prime \prime } \) , whereby the inductive hypothesis gives
\( \Theta \mid \mathcal {L} \mid \Gamma _{{\mathrm {1}}} \uplus \Gamma ^{\prime \prime } \vdash \mathit {e} : \tau _{{\mathrm {2}}} \operatorname{\Rightarrow }\Gamma _{{\mathrm {2}}} \uplus \Gamma ^{\prime \prime } \) . To prove the overall result, we must
show that \( \Gamma \uplus \Gamma ^{\prime \prime } \le \Gamma _{{\mathrm {1}}} \uplus \Gamma ^{\prime \prime } \)  and \( \Gamma _{{\mathrm {2}}} \uplus \Gamma ^{\prime \prime } , \tau _{{\mathrm {2}}} \le \Gamma ^{\prime } \uplus \Gamma ^{\prime \prime } , \tau \) 
which follow from parts 1 and 2 above.
That \( \mathcal {L} \mid \Gamma _{{\mathrm {2}}} \uplus \Gamma ^{\prime \prime } \vdash _{\mathit {WF}} \tau _{{\mathrm {2}}} \)  follows by reasoning to the case for T-Let above.

T-Assert
We must show that \(\models \left.{ \Gamma ^{\prime \prime } \uplus \Gamma }\right. \Rightarrow \varphi \)  which is equivalent to
\(\models \left.{ \Gamma ^{\prime \prime } }\right. \wedge \left.{ \Gamma }\right. \Rightarrow \varphi \) . As the source term was well typed,
\(\models \left.{ \Gamma }\right. \Rightarrow \varphi \)  is valid, we must then have \(\models \left.{ \Gamma ^{\prime \prime } }\right. \wedge \left.{ \Gamma }\right. \Rightarrow \varphi \) 
whereby the inductive hypothesis gives the required result.


Proof of lem:preservation
We first prove two additional lemmas.
lem:stack-well-typed,lem:callfunc give key facts used in the return and
call cases respectively; we have separated them into separate lemmas for clarity.
For any \(\Gamma _{{\mathrm {0}}}\)  such that \( \Theta \mid \ell : \vec{\ell } \mid \Gamma _{{\mathrm {0}}} \vdash \mathit {x} : \tau _{{\mathrm {1}}} \operatorname{\Rightarrow }\Gamma _{{\mathrm {1}}} \)  and \(\Theta \mid []: \tau _{{\mathrm {1}}} \operatorname{\Rightarrow }\Gamma _{{\mathrm {1}}} \mid \vec{\ell } \vdash _{\mathit {ectx} } \mathit {E} [\operatorname{\mathbf {let}}\mathit {y} = []^ \ell \operatorname{\mathbf {in}}\mathit {e} ] : \tau _{{\mathrm {2}}} \operatorname{\Rightarrow }\Gamma _{{\mathrm {2}}}\)  then
\( \Theta \mid \vec{\ell } \mid \Gamma _{{\mathrm {0}}} \vdash \mathit {E} [\operatorname{\mathbf {let}}\mathit {y} = []^ \ell \operatorname{\mathbf {in}}\mathit {e} ] [ \mathit {x} ] : \tau _{{\mathrm {2}}} \operatorname{\Rightarrow }\Gamma _{{\mathrm {2}}} \) .


It suffices to show that \( \Theta \mid \vec{\ell } \mid \Gamma _{{\mathrm {0}}} \vdash \operatorname{\mathbf {let}}\mathit {y} = \mathit {x} \operatorname{\mathbf {in}}\mathit {e} : \tau ^{\prime }_{{\mathrm {1}}} \operatorname{\Rightarrow }\Gamma ^{\prime }_{{\mathrm {1}}} \) 
and \(\Theta \mid []: \tau ^{\prime }_{{\mathrm {1}}} \operatorname{\Rightarrow }\Gamma ^{\prime }_{{\mathrm {1}}} \mid \vec{\ell } \vdash _{\mathit {ectx} } \mathit {E} : \tau _{{\mathrm {2}}} \operatorname{\Rightarrow }\Gamma _{{\mathrm {2}}}\)  for some \(\tau ^{\prime }_{{\mathrm {1}}}\)  and \(\Gamma ^{\prime }_{{\mathrm {1}}}\) 
whereby the result will hold from lem:ectxt-sub-well-typed.
By inversion on
\(\Theta \mid []: \tau _{{\mathrm {1}}} \operatorname{\Rightarrow }\Gamma _{{\mathrm {1}}} \mid \vec{\ell } \vdash _{\mathit {ectx} } \mathit {E} [\operatorname{\mathbf {let}}\mathit {y} = []^ \ell \operatorname{\mathbf {in}}\mathit {e} ] : \tau _{{\mathrm {2}}} \operatorname{\Rightarrow }\Gamma _{{\mathrm {2}}}\)  we have
\(& \Theta \mid \vec{\ell } \mid \Gamma _{{\mathrm {1}}} , \mathit {y} : \tau _{{\mathrm {1}}} \vdash \mathit {e} : \tau ^{\prime \prime }_{{\mathrm {1}}} \operatorname{\Rightarrow }\Gamma ^{\prime \prime }_{{\mathrm {1}}}  \\& \Theta \mid []: \tau ^{\prime \prime }_{{\mathrm {1}}} \operatorname{\Rightarrow }\Gamma ^{\prime \prime }_{{\mathrm {1}}} \mid \mathcal {L} \vdash _{\mathit {ectx} } \mathit {E} : \tau _{{\mathrm {2}}} \operatorname{\Rightarrow }\Gamma _{{\mathrm {2}}}  \\& \mathit {y} \notin \mathit {dom}( \Gamma ^{\prime \prime }_{{\mathrm {1}}} ) \) 

We take \(\Gamma ^{\prime }_{{\mathrm {1}}} = \Gamma ^{\prime \prime }_{{\mathrm {1}}}\) , \(\tau ^{\prime }_{{\mathrm {1}}} = \tau ^{\prime \prime }_{{\mathrm {1}}}\) , and then eqn:ctxt-typed
gives the necessary typing for \(\mathit {E}\) .
It remains to to show that
\(\Theta \mid \vec{\ell } \mid \Gamma _{{\mathrm {0}}} \vdash \operatorname{\mathbf {let}}\mathit {y} = \mathit {x} \operatorname{\mathbf {in}}\mathit {e} : \tau ^{\prime }_{{\mathrm {1}}} \operatorname{\Rightarrow }\Gamma ^{\prime }_{{\mathrm {1}}}\) 
(That \( \vec{\ell } \vdash _{\mathit {WF}} \tau ^{\prime }_{{\mathrm {1}}} \operatorname{\Rightarrow }\Gamma ^{\prime }_{{\mathrm {1}}} \)  follows from eqn:let-body-ty)
By lem:inversion, from \( \Theta \mid \ell : \vec{\ell } \mid \Gamma _{{\mathrm {0}}} \vdash \mathit {x} : \tau _{{\mathrm {1}}} \operatorname{\Rightarrow }\Gamma _{{\mathrm {1}}} \)  we conclude there
exists some \(\Gamma _{\mathit {p}}\) , \(\tau _{\mathit {p}}\) , and \(\Gamma ^{\prime }_{\mathit {p}}\)  such:
\(& \Gamma _{{\mathrm {0}}} \le \Gamma _{\mathit {p}}  \\& \Gamma ^{\prime }_{\mathit {p}} , \tau _{\mathit {p}} \le \Gamma _{{\mathrm {1}}} , \tau _{{\mathrm {1}}}  \\& \Gamma ^{\prime }_{\mathit {p}} = \Gamma _{\mathit {p}} [ \mathit {x} \hookleftarrow \tau ^{\prime }_{\mathit {p}} ]  \\& \Gamma _{\mathit {p}} ( \mathit {x} ) = \tau _{\mathit {p}} + \tau ^{\prime }_{\mathit {p}}  \\& \vec{\ell } \vdash _{\mathit {WF}} \Gamma _{\mathit {p}} \) 
We first apply T-Sub with eqn:rin-sub,eqn:renv-sub-in-wf, so it remains to show
\(\Theta \mid \vec{\ell } \mid \Gamma _{\mathit {p}} [ \mathit {x} : \tau _{\mathit {p}} + \tau ^{\prime }_{\mathit {p}} ] \vdash \operatorname{\mathbf {let}}\mathit {y} = \mathit {x} \operatorname{\mathbf {in}}\mathit {e} : \tau ^{\prime }_{{\mathrm {1}}} \operatorname{\Rightarrow }\Gamma ^{\prime }_{{\mathrm {1}}}\) 
which, by T-Let holds if we show that:
\(\Theta \mid \vec{\ell } \mid \Gamma _{\mathit {p}} [ \mathit {x} \hookleftarrow \tau ^{\prime }_{\mathit {p}} \wedge _{ \mathit {x} } \mathit {x} =_{ \tau ^{\prime }_{\mathit {p}} } \mathit {y} ] , \mathit {y} : \tau _{\mathit {p}} \wedge _{ \mathit {y} } \mathit {y} =_{ \tau _{\mathit {p}} } \mathit {x} \vdash \mathit {e} : \tau ^{\prime }_{{\mathrm {1}}} \operatorname{\Rightarrow }\Gamma ^{\prime }_{{\mathrm {1}}}\) 
(\( \mathit {y} \notin \mathit {dom}( \Gamma ^{\prime }_{{\mathrm {1}}} ) \)  follows from eqn:y-not-free-var, and the well-formedness of
\(\Gamma _{\mathit {p}} [ \mathit {x} \hookleftarrow \tau ^{\prime }_{\mathit {p}} \wedge _{ \mathit {x} } \mathit {x} =_{ \tau ^{\prime }_{\mathit {p}} } \mathit {y} ] , \mathit {y} : \tau _{\mathit {p}} \wedge _{ \mathit {y} } \mathit {y} =_{ \tau _{\mathit {p}} } \mathit {x} \)  follows from the well-formedness of
\(\Gamma _{\mathit {p}}\) , \(\tau _{\mathit {p}}\)  and \(\tau ^{\prime }_{\mathit {p}}\)  and that \(\mathit {x}\)  and \(\mathit {y}\)  appear in the refinements
iff they are mapped to integer types in the new type environment.)
We can use T-Sub to weaken the type environment to:
\(\Theta \mid \vec{\ell } \mid \Gamma _{\mathit {p}} [ \mathit {x} \hookleftarrow \tau ^{\prime }_{\mathit {p}} ] , \mathit {y} : \tau _{\mathit {p}} \vdash \mathit {e} : \tau ^{\prime }_{{\mathrm {1}}} \operatorname{\Rightarrow }\Gamma ^{\prime }_{{\mathrm {1}}}\) 
From eqn:rout-sub above, we have that \(\Gamma _{\mathit {p}} [ \mathit {x} \hookleftarrow \tau ^{\prime }_{\mathit {p}} ] , \mathit {y} : \tau _{\mathit {p}} \le \Gamma _{{\mathrm {1}}} , \mathit {y} : \tau _{{\mathrm {1}}}\) ,
whereby one final application of T-Sub allows us to use to
eqn:let-body-ty above.
Let \(\mathit {E} [ \operatorname{\mathbf {let}}\mathit {x} = \mathit {f} ^ \ell ( \mathit {y_{{\mathrm {1}}}} ,\ldots , \mathit {y_{\mathit {n}}} ) \operatorname{\mathbf {in}}\mathit {e^{\prime }} ]\)  be a term such that:
0 letx = f  ( y1 ,..., yn ) ine' : 1 1   = [ :  / ]
[]: 1 1  ectx  E : 2 2  x = [ y1 / x1 ] [ yn / xn ]
f ( x1 ,   ..   , xn ) e D  f ( x1 ,   ..   , xn ) e
WF
where \(\Theta ( \mathit {f} ) = \forall \lambda .\left\langle { \mathit {x_{{\mathrm {1}}}} \operatorname{:}\tau _{{\mathrm {1}}} ,\dots , \mathit {x_{\mathit {n}}} \operatorname{:}\tau _{\mathit {n}} }\right\rangle \operatorname{\rightarrow }\left\langle { \mathit {x_{{\mathrm {1}}}} \operatorname{:}\tau ^{\prime }_{{\mathrm {1}}} ,\dots , \mathit {x_{\mathit {n}}} \operatorname{:}\tau ^{\prime }_{\mathit {n}} \mid \tau _{\mathit {q}} }\right\rangle  \) .
Then there exist some \(\tau _{{\mathrm {3}}}\)  and \(\Gamma _{{\mathrm {3}}}\) :
\(& \Theta \mid \ell : \vec{\ell } \mid \Gamma _{{\mathrm {0}}} \vdash \sigma _{x} \mathit {e} : \tau _{{\mathrm {3}}} \operatorname{\Rightarrow }\Gamma _{{\mathrm {3}}} \\& \Theta \mid []: \tau _{{\mathrm {3}}} \operatorname{\Rightarrow }\Gamma _{{\mathrm {3}}} \mid \vec{\ell } \vdash _{\mathit {ectx} } \mathit {E} [\operatorname{\mathbf {let}}\mathit {x} = []^ \ell \operatorname{\mathbf {in}}\mathit {e} ] : \tau _{{\mathrm {2}}} \operatorname{\Rightarrow }\Gamma _{{\mathrm {2}}}\) 



From lem:inversion on
\( \Theta \mid \vec{\ell } \mid \Gamma _{{\mathrm {0}}} \vdash \operatorname{\mathbf {let}}\mathit {x} = \mathit {f} ^ \ell ( \mathit {y_{{\mathrm {1}}}} ,\ldots , \mathit {y_{\mathit {n}}} ) \operatorname{\mathbf {in}}\mathit {e^{\prime }} : \tau _{{\mathrm {1}}} \operatorname{\Rightarrow }\Gamma _{{\mathrm {1}}} \)  we have, for some
\(\Gamma _{\mathit {p}}, \tau _{\mathit {p}}, \Gamma ^{\prime }_{\mathit {p}}\) , that:
\(& \Gamma _{{\mathrm {0}}} \le \Gamma _{\mathit {p}}  \\& \Gamma ^{\prime }_{\mathit {p}} , \tau _{\mathit {p}} \le \Gamma _{{\mathrm {1}}} , \tau _{{\mathrm {1}}}  \\& \Gamma _{\mathit {p}} ( \mathit {y_{\mathit {i}}} ) = \sigma _{\alpha } \, \sigma _{x} \, \tau _{\mathit {i}}  \\& \vec{\ell } \vdash _{\mathit {WF}} \Gamma _{\mathit {p}}  \\& \Theta \mid \vec{\ell } \mid \Gamma _{\mathit {p}} [ \mathit {y_{\mathit {i}}} \hookleftarrow \sigma _{\alpha } \, \sigma _{x} \, \tau ^{\prime }_{\mathit {i}} ] , \mathit {x} : \sigma _{\alpha } \, \sigma _{x} \, \tau _{\mathit {q}} \vdash \mathit {e^{\prime }} : \tau _{\mathit {p}} \operatorname{\Rightarrow }\Gamma ^{\prime }_{\mathit {p}}  \\& \mathit {x} \notin \mathit {dom}( \Gamma ^{\prime }_{\mathit {p}} ) \) 
To prove the first part, from the well-typing of the function body, we have
\( \Theta \mid \lambda \mid \mathit {x_{{\mathrm {1}}}} \operatorname{:}\tau _{{\mathrm {1}}} ,\ldots , \mathit {x_{\mathit {n}}} \operatorname{:}\tau _{\mathit {n}} \vdash \mathit {e} : \tau _{\mathit {q}} \operatorname{\Rightarrow }\mathit {x_{{\mathrm {1}}}} \operatorname{:}\tau ^{\prime }_{{\mathrm {1}}} ,\ldots , \mathit {x_{\mathit {n}}} \operatorname{:}\tau ^{\prime }_{\mathit {n}} \) .
From our assumption that all variable names are distinct,
by \(n\)  applications of the substitution lemma (lem:substitution) we have:
\( \Theta \mid \lambda \mid \mathit {y_{{\mathrm {1}}}} \operatorname{:}\sigma _{x} \, \tau _{{\mathrm {1}}} ,\ldots , \mathit {y_{\mathit {n}}} \operatorname{:}\sigma _{x} \, \tau _{\mathit {n}} \vdash \sigma _{x} \mathit {e} : \sigma _{x} \, \tau _{\mathit {q}} \operatorname{\Rightarrow }\mathit {y_{{\mathrm {1}}}} \operatorname{:}\sigma _{x} \, \tau ^{\prime }_{{\mathrm {1}}} ,\ldots , \mathit {y_{\mathit {n}}} \operatorname{:}\sigma _{x} \, \tau ^{\prime }_{\mathit {n}} \) .
By lem:ctxt-substitution (part itm:ctxt-subst-well-typed) we then have
\( \Theta \mid \ell : \vec{\ell } \mid \mathit {y_{{\mathrm {1}}}} \operatorname{:}\sigma _{\alpha } \, \sigma _{x} \, \tau _{{\mathrm {1}}} ,\ldots , \mathit {y_{\mathit {n}}} \operatorname{:}\sigma _{\alpha } \, \sigma _{x} \, \tau _{\mathit {n}} \vdash \sigma _{x} \mathit {e} : \sigma _{\alpha } \, \sigma _{x} \, \tau _{\mathit {q}} \operatorname{\Rightarrow }\mathit {y_{{\mathrm {1}}}} \operatorname{:}\sigma _{\alpha } \, \sigma _{x} \, \tau ^{\prime }_{{\mathrm {1}}} ,\ldots , \mathit {y_{\mathit {n}}} \operatorname{:}\sigma _{\alpha } \, \sigma _{x} \, \tau ^{\prime }_{\mathit {n}} \) .
We take \(\tau _{{\mathrm {3}}} = \sigma _{\alpha } \, \sigma _{x} \, \tau _{\mathit {q}}\)  and \(\Gamma _{{\mathrm {3}}} = \Gamma _{\mathit {p}} [ \mathit {y_{\mathit {i}}} \hookleftarrow \sigma _{\alpha } \, \sigma _{x} \, \tau ^{\prime }_{\mathit {i}} ]\) .
By the well-formedness of function types and well-formedness of \(\Gamma _{\mathit {p}}\) ,
we must have that \( \ell : \vec{\ell } \vdash _{\mathit {WF}} \Gamma _{{\mathrm {3}}} \) .
Then by eqn:arg-typed,eqn:sub-in-env-wf,lem:tyenv-weaken we have
\( \Theta \mid \ell : \vec{\ell } \mid \Gamma _{\mathit {p}} \vdash \sigma _{x} \mathit {e} : \tau _{{\mathrm {3}}} \operatorname{\Rightarrow }\Gamma _{{\mathrm {3}}} \) , whereby eqn:in-sub
and an application of T-Sub
gives \( \Theta \mid \ell : \vec{\ell } \mid \Gamma _{{\mathrm {0}}} \vdash \sigma _{x} \mathit {e} : \tau _{{\mathrm {3}}} \operatorname{\Rightarrow }\Gamma _{{\mathrm {3}}} \) , i.e., the first result.
To prove the second part, from the typing rule for TE-Stack we must show:
\(& \Theta \mid []: \tau _{{\mathrm {1}}} \operatorname{\Rightarrow }\Gamma _{{\mathrm {1}}} \mid \vec{\ell } \vdash _{\mathit {ectx} } \mathit {E} : \tau _{{\mathrm {2}}} \operatorname{\Rightarrow }\Gamma _{{\mathrm {2}}}  \\& \mathit {x} \notin \mathit {dom}( \Gamma _{{\mathrm {1}}} )  \\& \Theta \mid \vec{\ell } \mid \Gamma _{{\mathrm {3}}} , \mathit {x} : \tau _{{\mathrm {3}}} \vdash \mathit {e^{\prime }} : \tau _{{\mathrm {1}}} \operatorname{\Rightarrow }\Gamma _{{\mathrm {1}}} \) 

eqn:context-well-typed holds by assumption, and eqn:x-not-free follows from
eqn:cbind-erased and that \(\Gamma ^{\prime }_{\mathit {p}} \le \Gamma _{{\mathrm {1}}}\)  implies \( \mathit {dom}( \Gamma _{{\mathrm {1}}} ) \subseteq \mathit {dom}( \Gamma ^{\prime }_{\mathit {p}} ) \) .
\( \vec{\ell } \vdash _{\mathit {WF}} \tau _{{\mathrm {1}}} \operatorname{\Rightarrow }\Gamma _{{\mathrm {1}}} \)  follows from the well-typing of the function call term,
and \( \vec{\ell } \vdash _{\mathit {WF}} \Gamma _{{\mathrm {3}}} , \mathit {x} : \tau _{{\mathrm {3}}} \)  follows from eqn:let-body-well-typed.
From eqn:out-sub,eqn:let-body-well-typed we then have
eqn:let-body-sub-typed via an application of T-Sub.
[Preservation; lem:preservation]
The proof is organized by cases analysis on the transition rule used of \(\mathit {e}\) , and showing that the output configuration is well typed by
\( \vdash _{\mathit {conf} }^D \) . We must therefore find a \(\Gamma ^{\prime \prime }\)  that is consistent with \(\mathit {H^{\prime }}\)  and \(\mathit {R^{\prime }}\)  and also satisfies the other conditions imposed by
the definition of \( \vdash _{\mathit {conf} }^D \) . Here \(\Gamma ^{\prime \prime },\mathit {H^{\prime }}, \mathit {R^{\prime }}\)  represent the type environment, heap and register after the transition respectively.
We identify the heap and register file before transition with \(\mathit {H}\)  and \(\mathit {R}\)  respectively.
In order to show that the ownership invariant is preserved, we need to prove that \(\forall \, \mathit {a} \in \mathit {dom}( \mathit {H} ) . \mathbf {Own} \, ( \mathit {H} , \mathit {R} , \Gamma ^{\prime \prime } ) ( \mathit {a} ) \le 1\) .
In many cases, we will show that \(\mathbf {Own} \, ( \mathit {H} , \mathit {R} , \Gamma ) = \mathbf {Own} \, ( \mathit {H^{\prime }} , \mathit {R^{\prime }} , \Gamma ^{\prime \prime } )\) , whereby
from the assumption that \(\mathbf {Cons} \, ( \mathit {H} , \mathit {R} , \Gamma )\)  as implied by \( \vdash _{\mathit {conf} }^D \) 
we have \(\forall \, \mathit {a} \in \mathit {dom}( \mathit {H} ) . \mathbf {Own} \, ( \mathit {H} , \mathit {R} , \Gamma ) ( \mathit {a} ) \le 1\) , giving the desired result.
R-Var
conf D  H , R , Fn-1 : F , x  ,  H , R , Fn-1 : F , x   D   H , R , F , Fn-1 [ x ]

By inversion on configuration typing \( \vdash _{\mathit {conf} }^D \left\langle { \mathit {H} , \mathit {R} , F_{{\mathit {n}-1}} : \vec{F} , \mathit {x} }\right\rangle  \) , we have:
\(& \Theta \mid \vec{\ell } \mid \Gamma \vdash \mathit {x} : \tau _{\mathit {n}} \operatorname{\Rightarrow }\Gamma _{\mathit {n}} \\& \forall i\in \left\lbrace {1..n}\right\rbrace .\Theta \mid []: \tau _{\mathit {i}} \operatorname{\Rightarrow }\Gamma _{\mathit {i}} \mid \vec{\ell }_{{\mathit {i}-1}} \vdash _{\mathit {ectx} } F_{{\mathit {i}-1}} : \tau _{{\mathit {i}-1}} \operatorname{\Rightarrow }\Gamma _{{\mathit {i}-1}}\) 
Using lem:stack-well-typed, we can conclude that \( \Theta \mid \vec{\ell }_{{\mathit {n}-1}} \mid \Gamma \vdash F_{{\mathit {n}-1}} [ \mathit {x} ] : \tau _{{\mathit {n}-1}} \operatorname{\Rightarrow }\Gamma _{{\mathit {n}-1}} \) . We therefore take \(\Gamma ^{\prime \prime } = \Gamma \) .
It remains to show that \(\mathbf {Cons} \, ( \mathit {H} , \mathit {R} , \Gamma ^{\prime \prime } )\)  which follows immediately from
\(\mathbf {Cons} \, ( \mathit {H} , \mathit {R} , \Gamma )\) .
R-Deref
conf D  H , R , F , E [ letx = * y ine ]
 H , R , F , E [ letx = * y ine ]   D   H , R { x' v } , F , E [ [ x' / x ] e ]
H ( a )   =   v R ( y )   =   a R' = R { x' v }

By inversion on the configuration typing relationship, we have that:
\(\Theta \mid \vec{\ell } \mid \Gamma _{{\mathrm {0}}} \vdash \mathit {E} [ \operatorname{\mathbf {let}}\mathit {x} = * \mathit {y} \operatorname{\mathbf {in}}\mathit {e} ] : \tau _{\mathit {n}} \operatorname{\Rightarrow }\Gamma _{\mathit {n}} && \mathbf {Cons} \, ( \mathit {H} , \mathit {R} , \Gamma _{{\mathrm {0}}} )\) 

By lem:stackvar, we have some \(\tau , \Gamma ^{\prime }_{{\mathrm {0}}}\)  such that:
\(\Theta \mid []: \tau \operatorname{\Rightarrow }\Gamma ^{\prime }_{{\mathrm {0}}} \mid \vec{\ell } \vdash _{\mathit {ectx} } \mathit {E} : \tau _{\mathit {n}} \operatorname{\Rightarrow }\Gamma _{\mathit {n}} && \Theta \mid \vec{\ell } \mid \Gamma _{{\mathrm {0}}} \vdash \operatorname{\mathbf {let}}\mathit {x} = * \mathit {y} \operatorname{\mathbf {in}}\mathit {e} : \tau \operatorname{\Rightarrow }\Gamma ^{\prime }_{{\mathrm {0}}}\) 

Using lem:inversion, we have some \(\Gamma _{\mathit {p}}\) , \(\Gamma ^{\prime }_{\mathit {p}}\)  and \(\tau _{\mathit {p}}\)  such
that:
\(\Gamma _{{\mathrm {0}}} \le \Gamma _{\mathit {p}} \quad \quad \vec{\ell } \vdash _{\mathit {WF}} \Gamma _{\mathit {p}} \quad \quad \Gamma ^{\prime }_{\mathit {p}} , \tau _{\mathit {p}} \le \Gamma ^{\prime }_{{\mathrm {0}}} , \tau \\\Gamma _{\mathit {p}} ( \mathit {y} ) = ( \tau _{{\mathrm {1}}} + \tau _{{\mathrm {2}}} ) \operatorname{\mathbf {ref}}^{ r } \quad \quad \mathit {x} \notin \mathit {dom}( \Gamma ^{\prime }_{\mathit {p}} ) \\\tau ^{\prime \prime } = {\left\lbrace \begin{array}{ll}( \tau _{{\mathrm {1}}} \wedge _{ \mathit {y} } \mathit {y} =_{ \tau _{{\mathrm {1}}} } \mathit {x} ) & r > 0 \\\tau _{{\mathrm {1}}} & r = 0\end{array}\right.} \\\Theta \mid \vec{\ell } \mid \Gamma _{\mathit {p}} [ \mathit {y} \hookleftarrow \tau ^{\prime \prime } \operatorname{\mathbf {ref}}^{ r } ] , \mathit {x} : \tau _{{\mathrm {2}}} \vdash \mathit {e} : \tau _{\mathit {p}} \operatorname{\Rightarrow }\Gamma ^{\prime }_{\mathit {p}}\) 
From lem:subtyp-preserves-cons, we then have \(\mathbf {Cons} \, ( \mathit {H} , \mathit {R} , \Gamma _{\mathit {p}} )\) .
We will now show that:
\( & \mathbf {Cons} \, ( \mathit {H} , \mathit {R} \lbrace  \mathit {x^{\prime }} \mapsto \mathit {v} \rbrace  , \Gamma ^{\prime \prime } ) \\& \Theta \mid \vec{\ell } \mid \Gamma ^{\prime \prime } \vdash [ \mathit {x^{\prime }} / \mathit {x} ] \mathit {e} : [ \mathit {x^{\prime }} / \mathit {x} ] \, \tau _{\mathit {p}} \operatorname{\Rightarrow }[ \mathit {x^{\prime }} / \mathit {x} ] \, \Gamma ^{\prime }_{\mathit {p}}\) 

where \(\Gamma ^{\prime \prime } = \Gamma _{\mathit {p}} [ \mathit {y} \hookleftarrow ( [ \mathit {x^{\prime }} / \mathit {x} ] \, \tau ^{\prime \prime } ) \operatorname{\mathbf {ref}}^{ r } ] , \mathit {x^{\prime }} : \tau _{{\mathrm {2}}}\) .
Together these give our desired result. To see how,
from \( \Theta \mid \vec{\ell } \mid \Gamma _{\mathit {p}} [ \mathit {y} \hookleftarrow \tau ^{\prime \prime } \operatorname{\mathbf {ref}}^{ r } ] , \mathit {x} : \tau _{{\mathrm {2}}} \vdash \mathit {e} : \tau _{\mathit {p}} \operatorname{\Rightarrow }\Gamma ^{\prime }_{\mathit {p}} \)  above,
we must have that \( \vec{\ell } \vdash _{\mathit {WF}} \tau _{\mathit {p}} \operatorname{\Rightarrow }\Gamma ^{\prime }_{\mathit {p}} \) .
From \( \mathit {x} \notin \mathit {dom}( \Gamma ^{\prime }_{\mathit {p}} ) \)  we must therefore have that
\( [ \mathit {x^{\prime }} / \mathit {x} ] \, \tau _{\mathit {p}} = \tau _{\mathit {p}}\)  and \( [ \mathit {x^{\prime }} / \mathit {x} ] \, \Gamma ^{\prime }_{\mathit {p}} = \Gamma ^{\prime }_{\mathit {p}}\) . As \(\Gamma ^{\prime }_{\mathit {p}} , \tau _{\mathit {p}} \le \Gamma ^{\prime }_{{\mathrm {0}}} , \tau \) 
an application of T-Sub gives
\( \Theta \mid \vec{\ell } \mid \Gamma ^{\prime \prime } \vdash [ \mathit {x^{\prime }} / \mathit {x} ] \mathit {e} : \tau \operatorname{\Rightarrow }\Gamma ^{\prime }_{{\mathrm {0}}} \) . Then lem:ectxt-sub-well-typed
will give that \( \Theta \mid \vec{\ell } \mid \Gamma ^{\prime \prime } \vdash \mathit {E} [ [ \mathit {x^{\prime }} / \mathit {x} ] \mathit {e} ] : \tau _{\mathit {n}} \operatorname{\Rightarrow }\Gamma _{\mathit {n}} \) .
As \(\mathit {E}\)  and the stack \(\vec{F}\)  remained unchanged, combined with
eqn:new-tyenv-cons this gives
\( \vdash _{\mathit {conf} }^D \left\langle { \mathit {H} , \mathit {R} \lbrace  \mathit {x^{\prime }} \mapsto \mathit {v} \rbrace  , \vec{F} , \mathit {E} [ [ \mathit {x^{\prime }} / \mathit {x} ] \mathit {e} ] }\right\rangle  \)  as required.
As the above argument is used almost completely unchanged
in all of the following cases, we will invert the redex without regard
for the T-Sub rule, with the understanding that the subtyping rule
is handled with an argument identical to the above.
We now show that \( \Theta \mid \vec{\ell } \mid \Gamma ^{\prime \prime } \vdash [ \mathit {x^{\prime }} / \mathit {x} ] \mathit {e} : [ \mathit {x} / \mathit {x^{\prime }} ] \, \tau _{\mathit {p}} \operatorname{\Rightarrow }[ \mathit {x^{\prime }} / \mathit {x} ] \, \Gamma ^{\prime } \)  and
\(\mathbf {Cons} \, ( \mathit {H} , \mathit {R} \lbrace  \mathit {x^{\prime }} \mapsto \mathit {v} \rbrace  , \Gamma ^{\prime \prime } )\) .
The first is easy to obtain using lem:substitution; from \(\mathbf {Cons} \, ( \mathit {H} , \mathit {R} , \Gamma )\) ,
we have that \(\forall \, \mathit {x} \in \mathit {dom}( \Gamma ) . \mathit {x} \in \mathit {dom}( \mathit {R} ) \) , whereby from \( \mathit {x} \notin \mathit {dom}( \mathit {R} ) \)  we have
\( \mathit {x^{\prime }} \notin \mathit {dom}( \Gamma ) \) .
It therefore remains to show \(\mathbf {Cons} \, ( \mathit {H} , \mathit {R} \lbrace  \mathit {x^{\prime }} \mapsto \mathit {v} \rbrace  , \Gamma ^{\prime \prime } )\) .
To show \(\mathbf {SAT} \, ( \mathit {H} , \mathit {R} , \Gamma ^{\prime \prime } )\) , it suffices to
show that \( \mathbf {SATv} ( \mathit {H} , \mathit {R^{\prime }} , \mathit {R^{\prime }} ( \mathit {x^{\prime }} ) , \tau _{{\mathrm {2}}} ) \) 
and \( \mathbf {SATv} ( \mathit {H} , \mathit {R^{\prime }} , \mathit {H} ( \mathit {R^{\prime }} ( \mathit {y} ) ) , \tau ^{\prime \prime } ) \)  (that \(\mathbf {SATv}\)  holds for all other variables
\(\mathit {z}\)  follows from \(\Gamma ( \mathit {z} ) = \Gamma ^{\prime \prime } ( \mathit {z} )\)  and lem:r-valid-subst,lem:register).
If \(\tau _{{\mathrm {1}}}\)  is an integer type and \( r > 0 \) , then
by the definition of the strengthening operator, the latter is equivalent to show
that \( \mathbf {SATv} ( \mathit {H} , \mathit {R^{\prime }} , \mathit {H} ( \mathit {R^{\prime }} ( \mathit {y} ) ) , \tau _{{\mathrm {1}}} ) \) 
and that \(\mathit {R^{\prime }} ( \mathit {x^{\prime }} ) = \mathit {H} ( \mathit {R^{\prime }} ( \mathit {y} ) ) = \mathit {H} ( \mathit {R} ( \mathit {y} ) )\) , which is immediate from the definition of \({R-Deref}\) .
If \(\tau _{{\mathrm {1}}}\)  is not an integer or if \(r = 0\) ,
then we must only show that \( \mathbf {SATv} ( \mathit {H} , \mathit {R^{\prime }} , \mathit {H} ( \mathit {R^{\prime }} ( \mathit {y} ) ) , \tau _{{\mathrm {1}}} ) \) .
From \(\mathbf {Cons} \, ( \mathit {H} , \mathit {R} , \Gamma _{\mathit {p}} )\) , we know that \(\mathbf {SAT} \, ( \mathit {H} , \mathit {R} , \Gamma _{\mathit {p}} )\) , in particular, \( \mathbf {SATv} ( \mathit {H} , \mathit {R} , \mathit {R} ( \mathit {y} ) , \Gamma _{\mathit {p}} ( \mathit {y} ) ) \) .
Then by lem:satadd,lem:r-valid-subst,lem:register, from \( \mathit {R} \sqsubseteq \mathit {R^{\prime }} \) , \( \vec{\ell } \vdash _{\mathit {WF}} \Gamma _{\mathit {p}} \) , and \( \mathbf {SATv} ( \mathit {H} , \mathit {R} , \mathit {v} , \tau _{{\mathrm {1}}} + \tau _{{\mathrm {2}}} ) \)  we obtain
that \( \mathbf {SATv} ( \mathit {H} , \mathit {R^{\prime }} , \mathit {v} , \tau _{{\mathrm {1}}} ) \)  and \( \mathbf {SATv} ( \mathit {H} , \mathit {R^{\prime }} , \mathit {v} , \tau _{{\mathrm {2}}} ) \) , where \(\mathit {v} \, = \, \mathit {H} ( \mathit {R} ( \mathit {y} ) )\) .
We thus have that \( \mathbf {SATv} ( \mathit {H} , \mathit {R^{\prime }} , \mathit {R^{\prime }} ( \mathit {x^{\prime }} ) , \tau _{{\mathrm {2}}} ) \)  and \( \mathbf {SATv} ( \mathit {H} , \mathit {R^{\prime }} , \mathit {H} ( \mathit {R^{\prime }} ( \mathit {y} ) ) , \tau _{{\mathrm {1}}} ) \)  are satisfied.
We must also show that the ownership invariant is preserved.
Then, it's to show \(\forall \, \mathit {a} \in \mathit {dom}( \mathit {H} ) . \mathbf {Own} \, ( \mathit {H} , \mathit {R^{\prime }} , \Gamma ^{\prime \prime } ) ( \mathit {a} ) \le 1\) . Define \(\mathit {O^{\prime }_{{\mathrm {0}}}}\)  and \(\mathit {O^{\prime }_{{\mathrm {1}}}}\)  as follows:
\(\mathbf {Own} \, ( \mathit {H} , \mathit {R} , \Gamma _{\mathit {p}} ) & = \mathit {O^{\prime }_{{\mathrm {0}}}} + \mathbf {own} \, ( \mathit {H} , \mathit {R} ( \mathit {y} ) , \Gamma _{\mathit {p}} ( \mathit {y} ) ) \\\mathbf {Own} \, ( \mathit {H} , \mathit {R^{\prime }} , \Gamma ^{\prime \prime } ) & =\mathit {O^{\prime }_{{\mathrm {1}}}} + \mathbf {own} \, ( \mathit {H} , \mathit {R^{\prime }} ( \mathit {y} ) , \Gamma ^{\prime \prime } ( \mathit {y} ) ) + \mathbf {own} \, ( \mathit {H} , \mathit {R^{\prime }} ( \mathit {x^{\prime }} ) , \Gamma ^{\prime \prime } ( \mathit {x^{\prime }} ) ) \\\mathit {O^{\prime }_{{\mathrm {0}}}} & = \Sigma _{ \mathit {z} \in \mathit {dom}( \Gamma ) \setminus \left\lbrace { \mathit {y} }\right\rbrace  }\, \mathbf {own} \, ( \mathit {H} , \mathit {R} ( \mathit {z} ) , \Gamma _{\mathit {p}} ( \mathit {z} ) ) \\\mathit {O^{\prime }_{{\mathrm {1}}}} & = \Sigma _{ \mathit {z} \in \mathit {dom}( \Gamma ^{\prime \prime } ) \setminus \lbrace  \mathit {y} , \mathit {x^{\prime }} \rbrace  }\, \mathbf {own} \, ( \mathit {H} , \mathit {R^{\prime }} ( \mathit {z^{\prime }} ) , \Gamma ^{\prime \prime } ( \mathit {z^{\prime }} ) )\) 

By lem:heapop, \(\mathit {O^{\prime }_{{\mathrm {0}}}} = \mathit {O^{\prime }_{{\mathrm {1}}}}\)  holds. Then, it suffices to show that
\(\mathbf {own} \, ( \mathit {H} , \mathit {R} ( \mathit {y} ) , \Gamma _{\mathit {p}} ( \mathit {y} ) ) = \mathbf {own} \, ( \mathit {H} , \mathit {R^{\prime }} ( \mathit {y} ) , \Gamma ^{\prime \prime } ( \mathit {y} ) ) + \mathbf {own} \, ( \mathit {H} , \mathit {R^{\prime }} ( \mathit {x^{\prime }} ) , \Gamma ^{\prime \prime } ( \mathit {x^{\prime }} ) )\) .
As \(\mathit {R^{\prime }} ( \mathit {x^{\prime }} ) = \mathit {H} ( \mathit {R^{\prime }} ( \mathit {y} ) ) = \mathit {H} ( \mathit {R} ( \mathit {y} ) )\)  and from the definition of \(\Gamma ^{\prime \prime }\) , we have:
\(\mathbf {own} \, ( \mathit {H} , \mathit {R^{\prime }} ( \mathit {x^{\prime }} ) , \Gamma ^{\prime \prime } ( \mathit {x^{\prime }} ) ) & = \mathbf {own} \, ( \mathit {H} , \mathit {H} ( \mathit {R} ( \mathit {y} ) ) , \tau _{{\mathrm {2}}} ) \\\mathbf {own} \, ( \mathit {H} , \mathit {R^{\prime }} ( \mathit {y} ) , \Gamma ^{\prime \prime } ( \mathit {y} ) ) & = \lbrace  \mathit {a} \mapsto r \rbrace  + \mathbf {own} \, ( \mathit {H} , \mathit {H} ( \mathit {R} ( \mathit {y} ) ) , \tau _{{\mathrm {1}}} )\) 

From the definition of the ownership function, we have that
\(\mathbf {own} \, ( \mathit {H} , \mathit {R} ( \mathit {y} ) , \Gamma _{\mathit {p}} ( \mathit {y} ) ) = \lbrace  \mathit {a} \mapsto r \rbrace  + \mathbf {own} \, ( \mathit {H} , \mathit {H} ( \mathit {R} ( \mathit {y} ) ) , \tau _{{\mathrm {1}}} + \tau _{{\mathrm {2}}} )\) 
which, by lem:ownadd, is equivalent to:
\(\lbrace  \mathit {a} \mapsto r \rbrace  + \mathbf {own} \, ( \mathit {H} , \mathit {H} ( \mathit {R} ( \mathit {y} ) ) , \tau _{{\mathrm {1}}} ) + \mathbf {own} \, ( \mathit {H} , \mathit {H} ( \mathit {R} ( \mathit {y} ) ) , \tau _{{\mathrm {2}}} )\) 
We therefore have \(\mathbf {own} \, ( \mathit {H} , \mathit {R} ( \mathit {y} ) , \Gamma ( \mathit {y} ) ) = \mathbf {own} \, ( \mathit {H} , \mathit {R^{\prime }} ( \mathit {y} ) , \Gamma ^{\prime \prime } ( \mathit {y} ) ) + \mathbf {own} \, ( \mathit {H} , \mathit {R^{\prime }} ( \mathit {x^{\prime }} ) , \Gamma ^{\prime \prime } ( \mathit {x^{\prime }} ) )\) , and conclude that \(\mathbf {Own} \, ( \mathit {H} , \mathit {R} , \Gamma ) = \mathbf {Own} \, ( \mathit {H} , \mathit {R^{\prime }} , \Gamma ^{\prime \prime } )\) .
R-Seq
conf D  H , R , F , E [ x ;e ]
 H , R , F , E [ x ;e ]   D   H , R , F , E [ e ]

By inversion (see R-Deref) we have for some \(\Gamma \)  that:
\(& \Theta \mid \vec{\ell } \mid \Gamma [ \mathit {x} : \tau _{{\mathrm {0}}} + \tau _{{\mathrm {1}}} ] \vdash \mathit {x} : \tau _{{\mathrm {0}}} \operatorname{\Rightarrow }\Gamma [ \mathit {x} \hookleftarrow \tau _{{\mathrm {1}}} ] \\& \Theta \mid \vec{\ell } \mid \Gamma [ \mathit {x} \hookleftarrow \tau _{{\mathrm {1}}} ] \vdash \mathit {e} : \tau ^{\prime } \operatorname{\Rightarrow }\Gamma ^{\prime } \\& \mathbf {Cons} \, ( \mathit {H} , \mathit {R} , \Gamma )\) 

We take \(\Gamma ^{\prime \prime } = \Gamma [ \mathit {x} \hookleftarrow \tau _{{\mathrm {1}}} ]\) .
It suffices to show (see R-Deref)
that \( \Theta \mid \vec{\ell } \mid \Gamma ^{\prime \prime } \vdash \mathit {e} : \tau ^{\prime } \operatorname{\Rightarrow }\Gamma ^{\prime } \) ,
and \(\mathbf {Cons} \, ( \mathit {H} , \mathit {R} , \Gamma ^{\prime \prime } )\) .
The first is immediate from the inversion above, and
\(\mathbf {Cons} \, ( \mathit {H} , \mathit {R} , \Gamma ^{\prime \prime } )\)  follows from lem:ownadd,lem:satadd.
R-Let
conf D  H , R , F , E [ letx = y ine ]
 H , R , F , E [ letx = y ine ]   D   H , R { x' R ( y ) } , F , E [ [ x' / x ] e ]
x' dom( R ) R' = R { x' R ( y ) }

By inversion (see R-Deref) we have that for some \(\Gamma \)  that:
\(& \vec{\ell } \vdash _{\mathit {WF}} \Gamma \\& \Gamma ( \mathit {y} ) = \tau _{{\mathrm {1}}} + \tau _{{\mathrm {2}}} \\& \Theta \mid \vec{\ell } \mid \Gamma [ \mathit {y} \hookleftarrow \tau _{{\mathrm {1}}} \wedge _{ \mathit {y} } \mathit {y} =_{ \tau _{{\mathrm {1}}} } \mathit {x} ] , \mathit {x} : ( \tau _{{\mathrm {2}}} \wedge _{ \mathit {x} } \mathit {x} =_{ \tau _{{\mathrm {2}}} } \mathit {y} ) \vdash \mathit {e} : \tau \operatorname{\Rightarrow }\Gamma ^{\prime } \\& \mathbf {Cons} \, ( \mathit {H} , \mathit {R} , \Gamma ) \mathit {x} \notin \mathit {dom}( \Gamma ^{\prime } )\) 

We give \(\Gamma ^{\prime \prime } = \Gamma [ \mathit {y} \hookleftarrow \tau _{{\mathrm {1}}} \wedge _{ \mathit {y} } \mathit {y} =_{ \tau _{{\mathrm {1}}} } \mathit {x^{\prime }} ] , \mathit {x^{\prime }} : ( \tau _{{\mathrm {2}}} \wedge _{ \mathit {x^{\prime }} } \mathit {x^{\prime }} =_{ \tau _{{\mathrm {2}}} } \mathit {y} )\) .
It suffices to show (see R-Deref)
that \( \Theta \mid \vec{\ell } \mid \Gamma ^{\prime \prime } \vdash [ \mathit {x^{\prime }} / \mathit {x} ] \mathit {e} : \tau \operatorname{\Rightarrow }\Gamma ^{\prime } \) 
and \(\mathbf {Cons} \, ( \mathit {H} , \mathit {R} \lbrace  \mathit {x^{\prime }} \mapsto \mathit {R} ( \mathit {y} ) \rbrace  , \Gamma ^{\prime \prime } )\) .
The first is easy to obtain using reasoning as in the R-Deref case.
It therefore remains to show \(\mathbf {Cons} \, ( \mathit {H} , \mathit {R^{\prime }} , \Gamma ^{\prime \prime } )\) .
To show that the output environment is consistent, we must show that \( \mathbf {SATv} ( \mathit {H} , \mathit {R^{\prime }} , \mathit {R^{\prime }} ( \mathit {x^{\prime }} ) , \tau _{{\mathrm {2}}} \wedge _{ \mathit {x^{\prime }} } \mathit {x^{\prime }} \, = \, \mathit {y} ) \)  and \( \mathbf {SATv} ( \mathit {H} , \mathit {R^{\prime }} , \mathit {R^{\prime }} ( \mathit {y} ) , \tau _{{\mathrm {1}}} \wedge _{ \mathit {y} } \mathit {y} \, = \, \mathit {x^{\prime }} ) \) .
By reasoning similar to that in \({R-Deref}\) , it suffices to show that \( \mathbf {SATv} ( \mathit {H} , \mathit {R^{\prime }} , \mathit {R^{\prime }} ( \mathit {x^{\prime }} ) , \tau _{{\mathrm {2}}} ) \)  and \( \mathbf {SATv} ( \mathit {H} , \mathit {R^{\prime }} , \mathit {R^{\prime }} ( \mathit {y} ) , \tau _{{\mathrm {1}}} ) \) .
We know that \(\mathbf {Cons} \, ( \mathit {H} , \mathit {R} , \Gamma )\) , from which me have \(\mathbf {SAT} \, ( \mathit {H} , \mathit {R} , \Gamma )\) , in particular \( \mathit {y} \in \mathit {dom}( \mathit {R} ) \)  and \( \mathbf {SATv} ( \mathit {H} , \mathit {R} , \mathit {R} ( \mathit {y} ) , \Gamma ( \mathit {y} ) ) \) .
As \( \mathit {R} \sqsubseteq \mathit {R^{\prime }} \)  and \( \vec{\ell } \vdash _{\mathit {WF}} \Gamma \) , from lem:satadd,lem:r-valid-subst,lem:register, we obtain from \( \mathbf {SATv} ( \mathit {H} , \mathit {R} , \mathit {v} , \tau _{{\mathrm {1}}} + \tau _{{\mathrm {2}}} ) \)  that
\( \mathbf {SATv} ( \mathit {H} , \mathit {R^{\prime }} , \mathit {v} , \tau _{{\mathrm {1}}} ) \)  and \( \mathbf {SATv} ( \mathit {H} , \mathit {R^{\prime }} , \mathit {v} , \tau _{{\mathrm {2}}} ) \)  where \(v = R(y)\) .
We then have \( \mathbf {SATv} ( \mathit {H} , \mathit {R^{\prime }} , \mathit {R^{\prime }} ( \mathit {x^{\prime }} ) , \tau _{{\mathrm {2}}} ) \)  and \( \mathbf {SATv} ( \mathit {H} , \mathit {R^{\prime }} , \mathit {R^{\prime }} ( \mathit {y} ) , \tau _{{\mathrm {1}}} ) \)  are satisfied.
We must also show that the ownership invariant is preserved.
Then, it's to show \(\forall \, \mathit {a} \in \mathit {dom}( \mathit {H} ) . \mathbf {Own} \, ( \mathit {H} , \mathit {R^{\prime }} , \Gamma ^{\prime \prime } ) ( \mathit {a} ) \le 1\) . Define \(\mathit {O^{\prime }_{{\mathrm {0}}}}\)  and \(\mathit {O^{\prime }_{{\mathrm {1}}}}\)  as follows:
\(\mathbf {Own} \, ( \mathit {H} , \mathit {R} , \Gamma ) & = \mathit {O^{\prime }_{{\mathrm {0}}}} + \mathbf {own} \, ( \mathit {H} , \mathit {R} ( \mathit {y} ) , \Gamma ( \mathit {y} ) ) \\\mathbf {Own} \, ( \mathit {H} , \mathit {R^{\prime }} , \Gamma ^{\prime \prime } ) & = \mathit {O^{\prime }_{{\mathrm {1}}}} + \mathbf {own} \, ( \mathit {H} , \mathit {R^{\prime }} ( \mathit {y} ) , \Gamma ^{\prime \prime } ( \mathit {y} ) ) + \mathbf {own} \, ( \mathit {H} , \mathit {R^{\prime }} ( \mathit {x^{\prime }} ) , \Gamma ^{\prime \prime } ( \mathit {x^{\prime }} ) ) \\\mathit {O^{\prime }_{{\mathrm {0}}}} & = \Sigma _{ \mathit {z} \in \mathit {dom}( \Gamma ) \setminus \left\lbrace { \mathit {y} }\right\rbrace  }\, \mathbf {own} \, ( \mathit {H} , \mathit {R} ( \mathit {z} ) , \Gamma ( \mathit {z} ) ) \\\mathit {O^{\prime }_{{\mathrm {1}}}} & = \Sigma _{ \mathit {z} \in \mathit {dom}( \Gamma ^{\prime \prime } ) \setminus \lbrace  \mathit {y} , \mathit {x^{\prime }} \rbrace  }\, \mathbf {own} \, ( \mathit {H} , \mathit {R^{\prime }} ( \mathit {z^{\prime }} ) , \Gamma ^{\prime \prime } ( \mathit {z^{\prime }} ) )\) 

By lem:heapop, \(\mathit {O^{\prime }_{{\mathrm {0}}}} = \mathit {O^{\prime }_{{\mathrm {1}}}}\)  holds.
That \(\mathbf {own} \, ( \mathit {H} , \mathit {R^{\prime }} ( \mathit {x^{\prime }} ) , \tau _{{\mathrm {2}}} ) + \mathbf {own} \, ( \mathit {H} , \mathit {R^{\prime }} ( \mathit {y} ) , \tau _{{\mathrm {1}}} ) = \mathbf {own} \, ( \mathit {H} , \mathit {R} ( \mathit {y} ) , \tau _{{\mathrm {1}}} + \tau _{{\mathrm {2}}} )\)  follows immediately
from lem:ownadd and the condition \(\mathit {R} ( \mathit {y} ) = \mathit {R^{\prime }} ( \mathit {x^{\prime }} ) = \mathit {R^{\prime }} ( \mathit {y} )\) .
We therefore conclude that \(\mathbf {Own} \, ( \mathit {H} , \mathit {R} , \Gamma ) = \mathbf {Own} \, ( \mathit {H} , \mathit {R^{\prime }} , \Gamma ^{\prime \prime } )\) .
R-LetInt conf D  H , R , F , E [ letx = n ine ]
 H , R , F , E [ letx = n ine ]   D   H , R { x' n } , F , E [ [ x' / x ] e ] 

By inversion (see R-Deref) we have that, for some \(\Gamma \) :
\(& \Theta \mid \vec{\ell } \mid \Gamma , \mathit {x} : \left\lbrace { \nu \operatorname{:}\mathbf {int}\mid \nu \, = \, n }\right\rbrace  \vdash \mathit {e} : \tau \operatorname{\Rightarrow }\Gamma ^{\prime } \\& \mathbf {Cons} \, ( \mathit {H} , \mathit {R} , \Gamma ) \mathit {x} \notin \mathit {dom}( \Gamma ^{\prime } )\) 
We give that \(\Gamma ^{\prime \prime } = \Gamma , \mathit {x^{\prime }} : \left\lbrace { \nu \operatorname{:}\mathbf {int}\mid \nu \, = \, n }\right\rbrace  \) , and it thus suffices to show
that \( \Theta \mid \vec{\ell } \mid \Gamma ^{\prime \prime } \vdash [ \mathit {x^{\prime }} / \mathit {x} ] \mathit {e} : \tau \operatorname{\Rightarrow }\Gamma ^{\prime } \) 
and \(\mathbf {Cons} \, ( \mathit {H} , \mathit {R} \lbrace  \mathit {x^{\prime }} \mapsto n \rbrace  , \Gamma ^{\prime \prime } )\) .
The first one is easy to obtain using the lem:substitution (see R-Deref)
and the latter is trivial by similar reasoning to the T-Let and T-Deref cases.
R-IfTrue conf D  H , R , F , E [ ifzy thene1 elsee2 ]
 H , R , F , E [ ifzy thene1 elsee2 ]   D   H , R , F , E [ e1 ] 

By inversion (see R-Deref) we have that for some \(\Gamma \) :
\(& \Gamma ( \mathit {x} ) = \left\lbrace { \nu \operatorname{:}\mathbf {int}\mid \varphi }\right\rbrace  \\& \Theta \mid \vec{\ell } \mid \Gamma [ \mathit {x} \hookleftarrow \left\lbrace { \nu \operatorname{:}\mathbf {int}\mid \varphi \wedge \nu \, = \, 0 }\right\rbrace  ] \vdash \mathit {e_{{\mathrm {1}}}} : \tau \operatorname{\Rightarrow }\Gamma ^{\prime } \\& \mathbf {Cons} \, ( \mathit {H} , \mathit {R} , \Gamma )\) 

We take \(\Gamma ^{\prime \prime } = \Gamma [ \mathit {x} \hookleftarrow \left\lbrace { \nu \operatorname{:}\mathbf {int}\mid \varphi \wedge \nu \, = \, 0 }\right\rbrace  ]\) , and want to show that \(\mathbf {Cons} \, ( \mathit {H} , \mathit {R} , \Gamma ^{\prime \prime } )\)  (that \( \Theta \mid \vec{\ell } \mid \Gamma ^{\prime \prime } \vdash \mathit {e_{{\mathrm {1}}}} : \tau \operatorname{\Rightarrow }\Gamma ^{\prime } \)  is immediate).
By definition, from \(\mathbf {Cons} \, ( \mathit {H} , \mathit {R} , \Gamma )\)  we have \(\mathbf {SAT} \, ( \mathit {H} , \mathit {R} , \Gamma )\) , in particular \( \mathit {x} \in \mathit {dom}( \mathit {R} ) \) , \( \mathit {R} ( \mathit {x} ) \in \mathbb {Z} \)  and \([ \mathit {R} ] \, [ \mathit {R} ( \mathit {x} ) / \nu ] \varphi \) .
The refinement predicates \(\varphi \)  still holds in the output environment, since nothing changes in the register after transition.
Also from precondition of \({R-IfTrue}\) , we have \(\mathit {R} ( \mathit {x} ) \, = \, 0\) , thus \(\mathit {x}\)  satisfies the refinement that \(\nu \, = \, 0\) .
Thus \([ \mathit {R} ] \, [ \mathit {R} ( \mathit {x} ) / \nu ] ( \varphi \wedge \nu \, = \, 0 )\)  is trivially satisfied.
R-IfFalse Similar to the case for R-IfTrue.
R-MkRef
conf D  H , R , F , E [ letx = mkrefy ine ]
 H , R , F , E [ letx = mkrefy ine ]   D   H' , R' , F , E [ [ x' / x ] e ]
a dom( H ) x' dom( R )
H' = H { a R ( y ) } R' = R { x' a }

By inversion (see R-Deref) we have that for some \(\Gamma \) :
\(& \vec{\ell } \vdash _{\mathit {WF}} \Gamma \\& \Gamma ( \mathit {y} ) = \tau _{{\mathrm {1}}} + \tau _{{\mathrm {2}}} \\& \Theta \mid \vec{\ell } \mid \Gamma [ \mathit {y} \hookleftarrow \tau _{{\mathrm {1}}} ] , \mathit {x} : ( \tau _{{\mathrm {2}}} \wedge _{ \mathit {x} } \mathit {x} \, = \, \mathit {y} ) \operatorname{\mathbf {ref}}^{ 1 } \vdash \mathit {e} : \tau \operatorname{\Rightarrow }\Gamma ^{\prime } \\& \mathbf {Cons} \, ( \mathit {H} , \mathit {R} , \Gamma ) \mathit {x} \notin \mathit {dom}( \Gamma ^{\prime } )\) 

We give \(\Gamma ^{\prime \prime } = \Gamma [ \mathit {y} \hookleftarrow \tau _{{\mathrm {1}}} ] , \mathit {x^{\prime }} : ( \tau _{{\mathrm {2}}} \wedge _{ \mathit {x^{\prime }} } \mathit {x^{\prime }} \, = \, \mathit {y} ) \operatorname{\mathbf {ref}}^{ 1 } \) ,
and must show that \( \Theta \mid \vec{\ell } \mid \Gamma ^{\prime \prime } \vdash [ \mathit {x^{\prime }} / \mathit {x} ] \mathit {e} : \tau \operatorname{\Rightarrow }\Gamma ^{\prime } \)  and
\(\mathbf {Cons} \, ( \mathit {H^{\prime }} , \mathit {R^{\prime }} , \Gamma ^{\prime \prime } )\) . The first follows
from lem:substitution and the reasoning found in R-Deref,
and the second from the assumed well-formedness of \(\tau _{{\mathrm {1}}} + \tau _{{\mathrm {2}}}\) .
It remains to show \(\mathbf {Cons} \, ( \mathit {H^{\prime }} , \mathit {R^{\prime }} , \Gamma ^{\prime \prime } )\) .
To show that the output environment is consistent, we must show that \( \mathbf {SATv} ( \mathit {H^{\prime }} , \mathit {R^{\prime }} , \mathit {R^{\prime }} ( \mathit {x^{\prime }} ) , ( \tau _{{\mathrm {2}}} \wedge _{ \mathit {x^{\prime }} } \mathit {x^{\prime }} \, = \, \mathit {y} ) \operatorname{\mathbf {ref}}^{ 1 } ) \)  and \( \mathbf {SATv} ( \mathit {H^{\prime }} , \mathit {R^{\prime }} , \mathit {R^{\prime }} ( \mathit {y} ) , \tau _{{\mathrm {1}}} ) \) .
By reasoning similar to that in \({R-Deref}\) , it suffices to show that \( \mathbf {SATv} ( \mathit {H^{\prime }} , \mathit {R^{\prime }} , \mathit {R^{\prime }} ( \mathit {x^{\prime }} ) , \tau _{{\mathrm {2}}} \operatorname{\mathbf {ref}}^{ 1 } ) \)  and \( \mathbf {SATv} ( \mathit {H^{\prime }} , \mathit {R^{\prime }} , \mathit {R^{\prime }} ( \mathit {y} ) , \tau _{{\mathrm {1}}} ) \) .
We know that \(\mathbf {Cons} \, ( \mathit {H} , \mathit {R} , \Gamma )\) , from which we have \(\mathbf {SAT} \, ( \mathit {H} , \mathit {R} , \Gamma )\) , in particular \( \mathit {y} \in \mathit {dom}( \mathit {R} ) \)  and \( \mathbf {SATv} ( \mathit {H} , \mathit {R} , \mathit {R} ( \mathit {y} ) , \Gamma ( \mathit {y} ) ) \) .
As \( \mathit {R} \sqsubseteq \mathit {R^{\prime }} \)  and \( \vec{\ell } \vdash _{\mathit {WF}} \Gamma \) , from lem:register,lem:r-valid-subst, we have \( \mathbf {SATv} ( \mathit {H} , \mathit {R} , \mathit {R} ( \mathit {y} ) , \tau _{{\mathrm {1}}} + \tau _{{\mathrm {2}}} ) \)  implies \( \mathbf {SATv} ( \mathit {H} , \mathit {R^{\prime }} , \mathit {R^{\prime }} ( \mathit {y} ) , \tau _{{\mathrm {1}}} + \tau _{{\mathrm {2}}} ) \) .
By lem:newaddheap, we then have \( \mathbf {SATv} ( \mathit {H^{\prime }} , \mathit {R^{\prime }} , \mathit {R} ( \mathit {y} ) , \tau _{{\mathrm {1}}} + \tau _{{\mathrm {2}}} ) \) .
Then by lem:satadd, we have \( \mathbf {SATv} ( \mathit {H^{\prime }} , \mathit {R^{\prime }} , \mathit {v} , \tau _{{\mathrm {1}}} ) \)  and \( \mathbf {SATv} ( \mathit {H^{\prime }} , \mathit {R^{\prime }} , \mathit {v} , \tau _{{\mathrm {2}}} ) \)  where \(\mathit {v} \, = \, \mathit {R} ( \mathit {y} )\) .
We then have \( \mathbf {SATv} ( \mathit {H^{\prime }} , \mathit {R^{\prime }} , \mathit {R^{\prime }} ( \mathit {x^{\prime }} ) , \tau _{{\mathrm {2}}} \operatorname{\mathbf {ref}}^{ 1 } ) \)  and \( \mathbf {SATv} ( \mathit {H^{\prime }} , \mathit {R^{\prime }} , \mathit {R^{\prime }} ( \mathit {y} ) , \tau _{{\mathrm {1}}} ) \)  are satisfied.
We must also show that the ownership invariant is preserved.
Then, it's to show \(\forall \, \mathit {a^{\prime }} \in \mathit {dom}( \mathit {H} ) . \mathbf {Own} \, ( \mathit {H^{\prime }} , \mathit {R^{\prime }} , \Gamma ^{\prime \prime } ) ( \mathit {a^{\prime }} ) \le 1\) . From \(\mathbf {Cons} \, ( \mathit {H} , \mathit {R} , \Gamma )\)  and lem:ownaddheap,lem:ownadd we have:
\(\mathbf {Own} \, ( \mathit {H^{\prime }} , \mathit {R^{\prime }} , \Gamma ^{\prime \prime } ) & = \Sigma _{ \mathit {z} \in \mathit {dom}( \Gamma ^{\prime \prime } ) }\, \mathbf {own} \, ( \mathit {H^{\prime }} , \mathit {R^{\prime }} ( \mathit {z} ) , \Gamma ^{\prime \prime } ( \mathit {z} ) ) \\& = \Sigma _{ \mathit {z} \in \mathit {dom}( \Gamma ) }\, \mathbf {own} \, ( \mathit {H} , \mathit {R} ( \mathit {z} ) , \Gamma ( \mathit {z} ) ) + \lbrace  \mathit {a} \mapsto 1 \rbrace  \\& = \mathbf {Own} \, ( \mathit {H} , \mathit {R} , \Gamma ) + \lbrace  \mathit {a} \mapsto 1 \rbrace \) 
Since \( \mathit {a} \notin \mathit {dom}( \mathit {H} ) \)  and \(\forall \, \mathit {a^{\prime }} \in \mathit {dom}( \mathit {H} ) . \mathbf {Own} \, ( \mathit {H} , \mathit {R} , \Gamma ) ( \mathit {a^{\prime }} ) \le 1\) ,
we have \(\forall \, \mathit {a^{\prime }} \in \mathit {dom}( \mathit {H} ) . \mathbf {Own} \, ( \mathit {H^{\prime }} , \mathit {R^{\prime }} , \Gamma ^{\prime \prime } ) ( \mathit {a^{\prime }} ) \le 1\) .
R-Assign conf D  H , R , F , E [ y :=x ;e ]
 H , R , F , E [ y :=x ;e ]   D   H' , R' , F , E [ e ]
a   =   R ( y ) H' = H { a R ( x ) } R' = R

By inversion (see the R-Deref case) we have that
\(& \Theta \mid \vec{\ell } \mid \Gamma [ \mathit {x} : \tau _{{\mathrm {1}}} + \tau _{{\mathrm {2}}} ] [ \mathit {y} : \tau ^{\prime } \operatorname{\mathbf {ref}}^{ 1 } ] \vdash \mathit {y} \operatorname{:=}\mathit {x} \operatorname{;}\mathit {e} : \tau \operatorname{\Rightarrow }\Gamma ^{\prime } \\& \Theta \mid \vec{\ell } \mid \Gamma [ \mathit {x} \hookleftarrow \tau _{{\mathrm {1}}} ] [ \mathit {y} \hookleftarrow ( \tau _{{\mathrm {2}}} \wedge _{ \mathit {y} } \mathit {y} =_{ \tau _{{\mathrm {2}}} } \mathit {x} ) \operatorname{\mathbf {ref}}^{ 1 } ] \vdash \mathit {e} : \tau \operatorname{\Rightarrow }\Gamma ^{\prime } \\& \mathbf {Cons} \, ( \mathit {H} , \mathit {R} , \Gamma )\) 

We give \(\Gamma ^{\prime \prime } = \Gamma [ \mathit {x} \hookleftarrow \tau _{{\mathrm {1}}} ] [ \mathit {y} \hookleftarrow ( \tau _{{\mathrm {2}}} \wedge _{ \mathit {y} } \mathit {y} =_{ \tau _{{\mathrm {2}}} } \mathit {x} ) \operatorname{\mathbf {ref}}^{ 1 } ]\) . That
\( \Theta \mid \vec{\ell } \mid \Gamma ^{\prime \prime } \vdash \mathit {e} : \tau \operatorname{\Rightarrow }\Gamma ^{\prime } \)  is immediate.
We must therefore show that \(\mathbf {Cons} \, ( \mathit {H^{\prime }} , \mathit {R^{\prime }} , \Gamma ^{\prime \prime } )\) .
To show that the output environment is consistent, we must show that \( \mathbf {SATv} ( \mathit {H^{\prime }} , \mathit {R} , \mathit {R} ( \mathit {y} ) , ( \tau _{{\mathrm {2}}} \wedge _{ \mathit {y} } \mathit {y} \, = \, \mathit {x} ) \operatorname{\mathbf {ref}}^{ 1 } ) \)  and \( \mathbf {SATv} ( \mathit {H^{\prime }} , \mathit {R} , \mathit {R} ( \mathit {x} ) , \tau _{{\mathrm {1}}} ) \) .
By reasoning similar to that in \({R-Deref}\) , it suffices to show that \( \mathbf {SATv} ( \mathit {H^{\prime }} , \mathit {R} , \mathit {R} ( \mathit {y} ) , \tau _{{\mathrm {2}}} \operatorname{\mathbf {ref}}^{ 1 } ) \)  and \( \mathbf {SATv} ( \mathit {H^{\prime }} , \mathit {R} , \mathit {R} ( \mathit {x} ) , \tau _{{\mathrm {1}}} ) \) .
From \(\mathbf {Cons} \, ( \mathit {H} , \mathit {R} , \Gamma )\) , we know that \(\mathbf {SAT} \, ( \mathit {H} , \mathit {R} , \Gamma )\) , in particular, \( \mathbf {SATv} ( \mathit {H} , \mathit {R} , \mathit {R} ( \mathit {x} ) , \Gamma ( \mathit {x} ) ) \) .
If we show that \(\mathbf {own} \, ( \mathit {H} , \mathit {R} ( \mathit {x} ) , \tau _{{\mathrm {1}}} + \tau _{{\mathrm {2}}} ) ( \mathit {a} ) = 0\)  and \( \mathit {H} \approx _ \mathit {a} \mathit {H^{\prime }} \) ,
then, by lem:heapfor0, we will obtain \( \mathbf {SATv} ( \mathit {H^{\prime }} , \mathit {R} , \mathit {R} ( \mathit {x} ) , \tau _{{\mathrm {1}}} + \tau _{{\mathrm {2}}} ) \) ,
from which, by lem:satadd,
\( \mathbf {SATv} ( \mathit {H^{\prime }} , \mathit {R} , \mathit {R} ( \mathit {x} ) , \tau _{{\mathrm {1}}} ) \)  and \( \mathbf {SATv} ( \mathit {H^{\prime }} , \mathit {R} , \mathit {R} ( \mathit {x} ) , \tau _{{\mathrm {2}}} ) \)  follow.
We then have \( \mathbf {SATv} ( \mathit {H^{\prime }} , \mathit {R} , \mathit {R} ( \mathit {y} ) , \tau _{{\mathrm {2}}} \operatorname{\mathbf {ref}}^{ 1 } ) \)  and \( \mathbf {SATv} ( \mathit {H^{\prime }} , \mathit {R} , \mathit {R} ( \mathit {x} ) , \tau _{{\mathrm {1}}} ) \)  as \(\mathit {H^{\prime }} ( \mathit {R} ( \mathit {y} ) ) \, = \, \mathit {R} ( \mathit {x} )\) .
(That any other variables \(\mathit {z}\)  is consistent will follow from \(\mathbf {own} \, ( \mathit {H} , \mathit {R} ( \mathit {z} ) , \Gamma ( \mathit {z} ) ) ( \mathit {a} ) = 0\) 
as proved below and lem:heapfor0.)
To show \(\mathbf {own} \, ( \mathit {H} , \mathit {R} ( \mathit {x} ) , \tau _{{\mathrm {1}}} + \tau _{{\mathrm {2}}} ) ( \mathit {a} ) = 0\) ,
we define \(\mathit {O^{\prime }_{{\mathrm {0}}}}, \mathit {O^{\prime \prime }_{{\mathrm {0}}}}, \mathit {O^{\prime }_{{\mathrm {1}}}}\)  and \(\mathit {O^{\prime \prime }_{{\mathrm {1}}}}\)  as below:
\(\mathbf {Own} \, ( \mathit {H} , \mathit {R} , \Gamma ) & = \mathit {O^{\prime }_{{\mathrm {0}}}} + \mathit {O^{\prime \prime }_{{\mathrm {0}}}} \\\mathbf {Own} \, ( \mathit {H^{\prime }} , \mathit {R} , \Gamma ^{\prime \prime } ) & = \mathit {O^{\prime }_{{\mathrm {1}}}} + \mathit {O^{\prime \prime }_{{\mathrm {1}}}} \\\mathit {O^{\prime }_{{\mathrm {0}}}} & = \Sigma _{ \mathit {z} \in \mathit {dom}( \Gamma ) \setminus \lbrace  \mathit {y} , \mathit {x} \rbrace  }\, \mathbf {own} \, ( \mathit {H} , \mathit {R} ( \mathit {z} ) , \Gamma ( \mathit {z} ) ) \\\mathit {O^{\prime \prime }_{{\mathrm {0}}}} &= \mathbf {own} \, ( \mathit {H} , \mathit {R} ( \mathit {y} ) , \Gamma ( \mathit {y} ) ) + \mathbf {own} \, ( \mathit {H} , \mathit {R} ( \mathit {x} ) , \Gamma ( \mathit {x} ) ) \\\mathit {O^{\prime }_{{\mathrm {1}}}} & = \Sigma _{ \mathit {z} \in \mathit {dom}( \Gamma ^{\prime \prime } ) \setminus \lbrace  \mathit {y} , \mathit {x} \rbrace  }\, \mathbf {own} \, ( \mathit {H^{\prime }} , \mathit {R} ( \mathit {z} ) , \Gamma ^{\prime \prime } ( \mathit {z} ) ) \\\mathit {O^{\prime \prime }_{{\mathrm {1}}}} &= \mathbf {own} \, ( \mathit {H^{\prime }} , \mathit {R} ( \mathit {y} ) , \Gamma ^{\prime \prime } ( \mathit {y} ) ) + \mathbf {own} \, ( \mathit {H^{\prime }} , \mathit {R} ( \mathit {x} ) , \Gamma ^{\prime \prime } ( \mathit {x} ) )\) 

By the definition of the ownership function, \(\Gamma ( \mathit {y} ) = \tau ^{\prime } \operatorname{\mathbf {ref}}^{ 1 } \)  and \(\Gamma ( \mathit {x} ) = \tau _{{\mathrm {1}}} + \tau _{{\mathrm {2}}}\) , we have:
\(\mathit {O^{\prime \prime }_{{\mathrm {0}}}} & = \mathbf {own} \, ( \mathit {H} , \mathit {H} ( \mathit {R} ( \mathit {y} ) ) , \tau ^{\prime } ) + \lbrace  \mathit {a} \mapsto 1 \rbrace  + \mathbf {own} \, ( \mathit {H} , \mathit {R} ( \mathit {x} ) , \tau _{{\mathrm {1}}} + \tau _{{\mathrm {2}}} ) \\\mathit {O^{\prime \prime }_{{\mathrm {1}}}} & = \mathbf {own} \, ( \mathit {H^{\prime }} , \mathit {H^{\prime }} ( \mathit {R} ( \mathit {y} ) ) , \tau _{{\mathrm {2}}} ) + \lbrace  \mathit {a} \mapsto 1 \rbrace  + \mathbf {own} \, ( \mathit {H^{\prime }} , \mathit {R} ( \mathit {x} ) , \tau _{{\mathrm {1}}} )\) 

As \(\mathbf {Own} \, ( \mathit {H} , \mathit {R} , \Gamma ) ( \mathit {a} ) \le 1\)  (from \(\mathbf {Cons} \, ( \mathit {H} , \mathit {R} , \Gamma )\) ) and from
\(\mathbf {Own} \, ( \mathit {H} , \mathit {R} , \Gamma ) ( \mathit {a} ) & = \mathit {O^{\prime }_{{\mathrm {0}}}} ( \mathit {a} ) + \mathit {O^{\prime \prime }_{{\mathrm {0}}}} ( \mathit {a} ) \\& = \mathit {O^{\prime }_{{\mathrm {0}}}} ( \mathit {a} ) + \mathbf {own} \, ( \mathit {H} , \mathit {H} ( \mathit {R} ( \mathit {y} ) ) , \tau ^{\prime } ) ( \mathit {a} ) + 1 + \mathbf {own} \, ( \mathit {H} , \mathit {R} ( \mathit {x} ) , \tau _{{\mathrm {1}}} + \tau _{{\mathrm {2}}} ) ( \mathit {a} ) \\& = 1\) 

we have that:
\(\mathbf {own} \, ( \mathit {H} , \mathit {H} ( \mathit {R} ( \mathit {y} ) ) , \tau ^{\prime } ) ( \mathit {a} ) & = \mathbf {own} \, ( \mathit {H} , \mathit {R} ( \mathit {x} ) , \tau _{{\mathrm {1}}} + \tau _{{\mathrm {2}}} ) ( \mathit {a} ) \\& = \mathit {O^{\prime }_{{\mathrm {0}}}} ( \mathit {a} ) = 0\) 
We now show that \( \mathit {H} \approx _ \mathit {a} \mathit {H^{\prime }} \) . The first two conditions are clear, so it
remains to show that, for any \(n\) , \( \mathit {H} \vdash \mathit {a} \Downarrow n \)  iff \( \mathit {H^{\prime }} \vdash \mathit {a} \Downarrow n \) .
From lem:sat-implies-shape-cons, we have \( \mathit {H} \vdash \mathit {a} \Downarrow | \tau ^{\prime } \operatorname{\mathbf {ref}}^{ 1 } | \) , and
a proof by contradiction gives that \( | \tau ^{\prime } \operatorname{\mathbf {ref}}^{ 1 } | \)  is the only such \(n\) 
for which \( \mathit {H} \vdash \mathit {a} \Downarrow n \) . We now argue the forward case for the bi-implication,
the backwards case follows similar reasoning.
Given \( \mathit {H} \vdash \mathit {a} \Downarrow | \tau ^{\prime } \operatorname{\mathbf {ref}}^{ 1 } | \) , we must show \( \mathit {H} \lbrace  \mathit {a} \hookleftarrow \mathit {R} ( \mathit {x} ) \rbrace  \vdash \mathit {a} \Downarrow | \tau _{{\mathrm {2}}} \operatorname{\mathbf {ref}}^{ 1 } | \) , for which it suffices to show
\( \mathit {H} \lbrace  \mathit {a} \hookleftarrow \mathit {R} ( \mathit {x} ) \rbrace  \vdash \mathit {R} ( \mathit {x} ) \Downarrow | \tau _{{\mathrm {2}}} | \) .
From our requirement that \(\tau ^{\prime }\)  and \(\tau _{{\mathrm {2}}}\) 
(and therefore \(\tau _{{\mathrm {1}}} + \tau _{{\mathrm {2}}}\) ) have similar shapes, we have \( | \tau ^{\prime } | = | \tau _{{\mathrm {2}}} | = | \tau _{{\mathrm {1}}} + \tau _{{\mathrm {2}}} | \) .
By inverting the well-typing of the input configuration, we must have \( \mathbf {SATv} ( \mathit {H} , \mathit {R} , \mathit {R} ( \mathit {x} ) , \tau _{{\mathrm {1}}} + \tau _{{\mathrm {2}}} ) \) ,
thus by lem:sat-implies-shape-cons we must have \( \mathit {H} \vdash \mathit {R} ( \mathit {x} ) \Downarrow | \tau _{{\mathrm {2}}} | \) .
As \( | \tau _{{\mathrm {2}}} | \, = \, | \tau ^{\prime } | < | \tau ^{\prime } \operatorname{\mathbf {ref}}^{ 1 } | \) , \(\mathit {a}\)  cannot be reachable from \(\mathit {R} ( \mathit {x} )\)  in \(\mathit {H}\) 
(otherwise we would have \(\mathit {a}\)  reaches an integer along multiple heap paths of differing lengths,
a clear contradiction).
Then the value of \(\mathit {a}\)  in \(\mathit {H}\)  is irrelevant to the derivation of \( \mathit {H} \vdash \mathit {R} ( \mathit {x} ) \Downarrow | \tau _{{\mathrm {2}}} | \) ,
whereby \( \mathit {H} \lbrace  \mathit {a} \hookleftarrow \mathit {R} ( \mathit {x} ) \rbrace  \vdash \mathit {R} ( \mathit {x} ) \Downarrow | \tau _{{\mathrm {2}}} | \)  must hold.
Then, it's to show \(\forall \, \mathit {a^{\prime }} \in \mathit {dom}( \mathit {H^{\prime }} ) . \mathbf {Own} \, ( \mathit {H^{\prime }} , \mathit {R} , \Gamma ^{\prime \prime } ) ( \mathit {a^{\prime }} ) = ( \mathit {O^{\prime }_{{\mathrm {1}}}} + \mathit {O^{\prime \prime }_{{\mathrm {1}}}} ) ( \mathit {a^{\prime }} ) = \mathit {O^{\prime }_{{\mathrm {1}}}} ( \mathit {a^{\prime }} ) + \mathit {O^{\prime \prime }_{{\mathrm {1}}}} ( \mathit {a^{\prime }} ) \, \le \, 1\) .
For every \( \mathit {z} \in \mathit {dom}( \Gamma ) \setminus \lbrace  \mathit {y} , \mathit {x} \rbrace  \)  (and similarly for \(\Gamma ^{\prime \prime }\) ), we have
\(\Gamma ( \mathit {z} ) = \Gamma ^{\prime \prime } ( \mathit {z} )\) . Further, from \(\mathit {O^{\prime }_{{\mathrm {0}}}} ( \mathit {a} ) = 0\)  above, we must have \(\mathbf {own} \, ( \mathit {H} , \mathit {R} ( \mathit {z} ) , \Gamma ( \mathit {z} ) ) ( \mathit {a} ) = 0\) 
for all such \(\mathit {z}\) . As \( \mathit {H} \approx _ \mathit {a} \mathit {H^{\prime }} \) , by lem:heapop, we have that \(\mathit {O^{\prime }_{{\mathrm {0}}}} = \mathit {O^{\prime }_{{\mathrm {1}}}}\) .
Then, from \(\forall \, \mathit {a^{\prime }} \in \mathit {dom}( \mathit {H} ) . \mathbf {Own} \, ( \mathit {H} , \mathit {R} , \Gamma ) ( \mathit {a^{\prime }} ) = \mathit {O^{\prime }_{{\mathrm {0}}}} ( \mathit {a^{\prime }} ) + \mathit {O^{\prime \prime }_{{\mathrm {0}}}} ( \mathit {a^{\prime }} ) \, \le \, 1\) , it suffices to show
that \(\forall \, \mathit {a^{\prime }} \in \mathit {dom}( \mathit {H} ) . \mathit {O^{\prime \prime }_{{\mathrm {1}}}} ( \mathit {a^{\prime }} ) \le \mathit {O^{\prime \prime }_{{\mathrm {0}}}} ( \mathit {a^{\prime }} )\) .
We first consider the case for \(\mathit {a}\) :
\(\mathit {O^{\prime \prime }_{{\mathrm {1}}}} ( \mathit {a} ) & = \mathbf {own} \, ( \mathit {H^{\prime }} , \mathit {H^{\prime }} ( \mathit {R} ( \mathit {y} ) ) , \tau _{{\mathrm {2}}} ) ( \mathit {a} ) + \mathbf {own} \, ( \mathit {H^{\prime }} , \mathit {R} ( \mathit {x} ) , \tau _{{\mathrm {1}}} ) ( \mathit {a} ) + 1 \\\mathit {O^{\prime \prime }_{{\mathrm {0}}}} ( \mathit {a} ) & = \mathbf {own} \, ( \mathit {H} , \mathit {R} ( \mathit {x} ) , \tau _{{\mathrm {1}}} + \tau _{{\mathrm {2}}} ) ( \mathit {a} ) + \mathbf {own} \, ( \mathit {H} , \mathit {H} ( \mathit {R} ( \mathit {y} ) ) , \tau ^{\prime } ) ( \mathit {a} ) + 1\) 

From above, we have \(\mathbf {own} \, ( \mathit {H} , \mathit {R} ( \mathit {x} ) , \tau _{{\mathrm {2}}} + \tau _{{\mathrm {1}}} ) ( \mathit {a} ) = \mathbf {own} \, ( \mathit {H} , \mathit {H} ( \mathit {R} ( \mathit {y} ) ) , \tau ^{\prime } ) ( \mathit {a} ) = 0\) .
By lem:heapop and \( \mathit {H} \approx _ \mathit {a} \mathit {H^{\prime }} \) , we have \(\mathbf {own} \, ( \mathit {H} , \mathit {R} ( \mathit {x} ) , \tau _{{\mathrm {2}}} + \tau _{{\mathrm {1}}} ) = \mathbf {own} \, ( \mathit {H^{\prime }} , \mathit {R} ( \mathit {x} ) , \tau _{{\mathrm {2}}} + \tau _{{\mathrm {1}}} )\) .
Also by lem:ownadd, we have \(\mathbf {own} \, ( \mathit {H^{\prime }} , \mathit {R} ( \mathit {x} ) , \tau _{{\mathrm {2}}} + \tau _{{\mathrm {1}}} ) = \mathbf {own} \, ( \mathit {H^{\prime }} , \mathit {R} ( \mathit {x} ) , \tau _{{\mathrm {1}}} ) + \mathbf {own} \, ( \mathit {H^{\prime }} , \mathit {R} ( \mathit {x} ) , \tau _{{\mathrm {2}}} )\) .
From \(\mathit {H^{\prime }} ( \mathit {R} ( \mathit {y} ) ) \, = \, \mathit {R} ( \mathit {x} )\) , we therefore have \(\mathbf {own} \, ( \mathit {H^{\prime }} , \mathit {H^{\prime }} ( \mathit {R} ( \mathit {y} ) ) , \tau _{{\mathrm {2}}} ) ( \mathit {a} ) = \mathbf {own} \, ( \mathit {H^{\prime }} , \mathit {R} ( \mathit {x} ) , \tau _{{\mathrm {1}}} ) ( \mathit {a} ) = 0\) ,
and thus:
\(\mathit {O^{\prime \prime }_{{\mathrm {1}}}} ( \mathit {a} ) = \mathbf {own} \, ( \mathit {H^{\prime }} , \mathit {H^{\prime }} ( \mathit {R} ( \mathit {y} ) ) , \tau _{{\mathrm {2}}} ) ( \mathit {a} ) + \mathbf {own} \, ( \mathit {H^{\prime }} , \mathit {R} ( \mathit {x} ) , \tau _{{\mathrm {1}}} ) ( \mathit {a} ) + 1 = 1 = \mathit {O^{\prime \prime }_{{\mathrm {0}}}} ( \mathit {a} )\) 
Next, consider some \(\mathit {a} \, \ne \, \mathit {a^{\prime }}\) ;
\(\mathit {O^{\prime \prime }_{{\mathrm {1}}}} ( \mathit {a^{\prime }} ) & = \mathbf {own} \, ( \mathit {H^{\prime }} , \mathit {H^{\prime }} ( \mathit {R} ( \mathit {y} ) ) , \tau _{{\mathrm {2}}} ) ( \mathit {a^{\prime }} ) + \mathbf {own} \, ( \mathit {H^{\prime }} , \mathit {R} ( \mathit {x} ) , \tau _{{\mathrm {1}}} ) ( \mathit {a^{\prime }} ) \\\mathit {O^{\prime \prime }_{{\mathrm {0}}}} ( \mathit {a^{\prime }} ) & = \mathbf {own} \, ( \mathit {H} , \mathit {R} ( \mathit {x} ) , \tau _{{\mathrm {2}}} + \tau _{{\mathrm {1}}} ) ( \mathit {a^{\prime }} ) + \mathbf {own} \, ( \mathit {H} , \mathit {H} ( \mathit {R} ( \mathit {y} ) ) , \tau ^{\prime } ) ( \mathit {a^{\prime }} )\) 

By reasoning similar to the case for \(a = a^{\prime }\) , we have \(\mathit {O^{\prime \prime }_{{\mathrm {1}}}} ( \mathit {a^{\prime }} ) \le \mathbf {own} \, ( \mathit {H} , \mathit {R} ( \mathit {x} ) , \tau _{{\mathrm {2}}} + \tau _{{\mathrm {1}}} ) ( \mathit {a^{\prime }} ) \le \mathit {O^{\prime \prime }_{{\mathrm {0}}}} ( \mathit {a^{\prime }} )\) .
We therefore conclude that \(\forall \, \mathit {a^{\prime }} \in \mathit {dom}( \mathit {H^{\prime }} ) . \mathbf {Own} \, ( \mathit {H^{\prime }} , \mathit {R} , \Gamma ^{\prime \prime } ) ( \mathit {a^{\prime }} ) \le 1\) .
R-Alias
conf D  H , R , F , E [ alias( x = y ) ;e ]
 H , R , F , E [ alias( x = y ) ;e ]   D   H , R , F , E [ e ]
R ( x )   =   R ( y )

By inversion (see R-Deref) we have for some \(\Gamma \)  that:
\(& \Theta \mid \vec{\ell } \mid \Gamma [ \mathit {x} : \tau _{{\mathrm {1}}} \operatorname{\mathbf {ref}}^{ r_{{\mathrm {1}}} } ] [ \mathit {y} : \tau _{{\mathrm {2}}} \operatorname{\mathbf {ref}}^{ r_{{\mathrm {2}}} } ] \vdash \mathbf {alias}( \mathit {x} = \mathit {y} ) \operatorname{;}\mathit {e} : \tau \operatorname{\Rightarrow }\Gamma ^{\prime } \\& \Theta \mid \vec{\ell } \mid \Gamma [ \mathit {x} \hookleftarrow \tau ^{\prime }_{{\mathrm {1}}} \operatorname{\mathbf {ref}}^{ r^{\prime }_{{\mathrm {1}}} } ] [ \mathit {y} \hookleftarrow \tau ^{\prime }_{{\mathrm {2}}} \operatorname{\mathbf {ref}}^{ r^{\prime }_{{\mathrm {2}}} } ] \vdash \mathit {e} : \tau \operatorname{\Rightarrow }\Gamma ^{\prime } \\& \tau _{{\mathrm {1}}} \operatorname{\mathbf {ref}}^{ r_{{\mathrm {1}}} } + \tau _{{\mathrm {2}}} \operatorname{\mathbf {ref}}^{ r_{{\mathrm {2}}} } \approx \tau ^{\prime }_{{\mathrm {1}}} \operatorname{\mathbf {ref}}^{ r^{\prime }_{{\mathrm {1}}} } + \tau ^{\prime }_{{\mathrm {2}}} \operatorname{\mathbf {ref}}^{ r^{\prime }_{{\mathrm {2}}} } \\& \mathbf {Cons} \, ( \mathit {H} , \mathit {R} , \Gamma )\) 

We give \(\Gamma ^{\prime \prime } = \Gamma [ \mathit {x} \hookleftarrow \tau ^{\prime }_{{\mathrm {1}}} \operatorname{\mathbf {ref}}^{ r^{\prime }_{{\mathrm {1}}} } ] [ \mathit {y} \hookleftarrow \tau ^{\prime }_{{\mathrm {2}}} \operatorname{\mathbf {ref}}^{ r^{\prime }_{{\mathrm {2}}} } ]\) , and must show
\( \Theta \mid \vec{\ell } \mid \Gamma ^{\prime \prime } \vdash \mathit {e} : \tau \operatorname{\Rightarrow }\Gamma ^{\prime } \)  and \(\mathbf {Cons} \, ( \mathit {H} , \mathit {R} , \Gamma ^{\prime \prime } )\) .
The first is immediate.
To show \(\mathbf {Cons} \, ( \mathit {H} , \mathit {R} , \Gamma ^{\prime \prime } )\)  we first define:
\(\tau _{\mathit {p}\,{\mathrm {1}}} = & \tau _{{\mathrm {1}}} \operatorname{\mathbf {ref}}^{ r_{{\mathrm {1}}} } \\\tau _{\mathit {p}\,{\mathrm {2}}} = & \tau _{{\mathrm {2}}} \operatorname{\mathbf {ref}}^{ r_{{\mathrm {2}}} } \\\tau _{\mathit {q}\,{\mathrm {1}}} = & \tau ^{\prime }_{{\mathrm {1}}} \operatorname{\mathbf {ref}}^{ r^{\prime }_{{\mathrm {1}}} } \\\tau _{\mathit {q}\,{\mathrm {2}}} = & \tau ^{\prime }_{{\mathrm {2}}} \operatorname{\mathbf {ref}}^{ r^{\prime }_{{\mathrm {2}}} } \\\tau _{\mathit {q}} = & \tau _{\mathit {q}\,{\mathrm {1}}} + \tau _{\mathit {q}\,{\mathrm {2}}} \\\tau _{\mathit {p}} = & \tau _{\mathit {p}\,{\mathrm {1}}} + \tau _{\mathit {p}\,{\mathrm {2}}}\) 

We thus have \(\tau _{\mathit {q}} \approx \tau _{\mathit {p}}\) .
We know that \(\mathbf {Cons} \, ( \mathit {H} , \mathit {R} , \Gamma )\) , from which we have \(\mathbf {SAT} \, ( \mathit {H} , \mathit {R} , \Gamma )\) , in particular
\( \mathbf {SATv} ( \mathit {H} , \mathit {R} , \mathit {R} ( \mathit {y} ) , \Gamma ( \mathit {y} ) = \tau _{{\mathrm {2}}} \operatorname{\mathbf {ref}}^{ r_{{\mathrm {2}}} } ) \)  and \( \mathbf {SATv} ( \mathit {H} , \mathit {R} , \mathit {R} ( \mathit {x} ) , \Gamma ( \mathit {x} ) = \tau _{{\mathrm {1}}} \operatorname{\mathbf {ref}}^{ r_{{\mathrm {1}}} } ) \) .
From \(\tau _{\mathit {p}\,{\mathrm {1}}} + \tau _{\mathit {p}\,{\mathrm {2}}} = \tau _{\mathit {p}}\)  and lem:satadd, we have
\( \mathbf {SATv} ( \mathit {H} , \mathit {R} , \mathit {v} , \tau _{\mathit {p}\,{\mathrm {1}}} ) \)  and \( \mathbf {SATv} ( \mathit {H} , \mathit {R} , \mathit {v} , \tau _{\mathit {p}\,{\mathrm {2}}} ) \)  imply \( \mathbf {SATv} ( \mathit {H} , \mathit {R} , \mathit {v} , \tau _{\mathit {p}} ) \) , where \(\mathit {v} = \mathit {H} ( \mathit {R} ( \mathit {y} ) ) = \mathit {H} ( \mathit {R} ( \mathit {x} ) )\) .
From \(\tau _{\mathit {q}} \approx \tau _{\mathit {p}}\)  and lem:sattosat, we have that \( \mathbf {SATv} ( \mathit {H} , \mathit {R} , \mathit {v} , \tau _{\mathit {p}} ) \)  implies \( \mathbf {SATv} ( \mathit {H} , \mathit {R} , \mathit {v} , \tau _{\mathit {q}} ) \) .
From lem:satadd we also have that \( \mathbf {SATv} ( \mathit {H} , \mathit {R} , \mathit {v} , \tau _{\mathit {q}} ) \)  implies \( \mathbf {SATv} ( \mathit {H} , \mathit {R} , \mathit {v} , \tau _{\mathit {q}\,{\mathrm {1}}} ) \)  and \( \mathbf {SATv} ( \mathit {H} , \mathit {R} , \mathit {v} , \tau _{\mathit {q}\,{\mathrm {2}}} ) \) , where
again \(\mathit {v} = \mathit {H} ( \mathit {R} ( \mathit {y} ) ) = \mathit {H} ( \mathit {R} ( \mathit {x} ) )\) .
Then from the reasoning above, the refinements of \(\tau _{\mathit {q}\,{\mathrm {1}}}\)  and \(\tau _{\mathit {q}\,{\mathrm {2}}}\)  are valid and \(\mathbf {Cons} \, ( \mathit {H} , \mathit {R} , \Gamma ^{\prime \prime } )\)  holds.
Then, it's to show \(\forall \, \mathit {a} \in \mathit {dom}( \mathit {H} ) . \mathbf {Own} \, ( \mathit {H} , \mathit {R} , \Gamma ^{\prime \prime } ) ( \mathit {a} ) \le 1\) .
To prove that \(\mathbf {Own} \, ( \mathit {H} , \mathit {R} , \Gamma ) = \mathbf {Own} \, ( \mathit {H} , \mathit {R} , \Gamma ^{\prime \prime } )\)  follows from:
\(&\mathbf {own} \, ( \mathit {H} , \mathit {R} ( \mathit {x} ) , \tau _{{\mathrm {1}}} \operatorname{\mathbf {ref}}^{ r_{{\mathrm {1}}} } ) + \mathbf {own} \, ( \mathit {H} , \mathit {R} ( \mathit {y} ) , \tau _{{\mathrm {2}}} \operatorname{\mathbf {ref}}^{ r_{{\mathrm {2}}} } ) = \\&\,\,\,\,\mathbf {own} \, ( \mathit {H} , \mathit {R} ( \mathit {x} ) , \tau ^{\prime }_{{\mathrm {1}}} \operatorname{\mathbf {ref}}^{ r^{\prime }_{{\mathrm {1}}} } ) + \mathbf {own} \, ( \mathit {H} , \mathit {R} ( \mathit {y} ) , \tau ^{\prime }_{{\mathrm {2}}} \operatorname{\mathbf {ref}}^{ r^{\prime }_{{\mathrm {2}}} } )\) 

which follows immediately from the conditions \( \tau _{{\mathrm {1}}} \operatorname{\mathbf {ref}}^{ r_{{\mathrm {1}}} } + \tau _{{\mathrm {2}}} \operatorname{\mathbf {ref}}^{ r_{{\mathrm {2}}} } \approx \tau ^{\prime }_{{\mathrm {1}}} \operatorname{\mathbf {ref}}^{ r^{\prime }_{{\mathrm {1}}} } + \tau ^{\prime }_{{\mathrm {2}}} \operatorname{\mathbf {ref}}^{ r^{\prime }_{{\mathrm {2}}} } \) , \(\mathit {R} ( \mathit {x} ) \, = \, \mathit {R} ( \mathit {y} )\) , and lem:ownadd,lem:ownequiv-preserv.
R-AliasPtr
By reasoning similar to the R-Alias case.
R-AliasFail,R-AliasPtrFail The result configuration \( \mathbf {AliasFail} \)  is trivially well-typed.
R-Assert conf D  H , R , F , E [ assert( ) ;e ]  [ R ]  
 H , R , F , E [ assert( ) ;e ]   D   H , R , F , E [ e ]

By inversion (see R-Deref) we can obtain \( \Theta \mid \vec{\ell } \mid \Gamma \vdash \mathbf {assert}( \varphi ) \operatorname{;}\mathit {e} : \tau \operatorname{\Rightarrow }\Gamma ^{\prime }\)  and \( \Theta \mid \vec{\ell } \mid \Gamma \vdash \mathit {e} : \tau \operatorname{\Rightarrow }\Gamma ^{\prime } \) , and
the result follows immediately by taking \(\Gamma ^{\prime \prime } = \Gamma \) .
R-AssertFail conf D  H , R , F , E [ assert( ) ;e ]
 H , R , F , E [ assert( ) ;e ]   D  AssertFail
 assert( ) ;e : '

By inversion (see the R-Deref case) we have that
\(\Gamma \models \varphi \) , i.e., \(\models \left.{ \Gamma }\right. \Rightarrow \varphi \) ,
for some \(\Gamma \)  such that \(\mathbf {Cons} \, ( \mathit {H} , \mathit {R} , \Gamma )\) .
From lem:sat-implies-gamma we therefore have \(\models [ \mathit {R} ] \, \left.{ \Gamma }\right. \) .
From the precondition of R-AssertFail we have that
\(\lnot \models [ \mathit {R} ] \, \varphi \) . But from \(\models \left.{ \Gamma }\right. \Rightarrow \varphi \)  and \(\models [ \mathit {R} ] \, \left.{ \Gamma }\right. \) 
we can conclude that \(\models [ \mathit {R} ] \, \varphi \) , yielding a contradiction.
We therefore conclude that this case is impossible.
R-Call
conf D  H , R , F , E [ letx = f  ( y1 ,..., yn ) ine' ]
f ( x1 ,   ..   , xn ) e D
l  H , R , F , E [ letx = f  ( y1 ,..., yn ) ine' ]
    D   H , R , E [letx = [] ine' ] : F , [ y1 / x1 ] [ yn / xn ] e

We must show that
\( \vdash _{\mathit {conf} }^D \left\langle { \mathit {H} , \mathit {R} , \mathit {E} [\operatorname{\mathbf {let}}\mathit {x} = []^ \ell \operatorname{\mathbf {in}}\mathit {e^{\prime }} ] : \vec{F} , [ \mathit {y_{{\mathrm {1}}}} / \mathit {x_{{\mathrm {1}}}} ] \cdots [ \mathit {y_{\mathit {n}}} / \mathit {x_{\mathit {n}}} ] \mathit {e} }\right\rangle  \) 
for some \(\Gamma ^{\prime \prime }\) .
By inversion on the configuration typing, we have that, for some \(\Gamma \) :
\(\Theta \mid \vec{\ell } \mid \Gamma \vdash \mathit {E} [ \operatorname{\mathbf {let}}\mathit {x} = \mathit {f} ^ \ell ( \mathit {y_{{\mathrm {1}}}} ,\ldots , \mathit {y_{\mathit {n}}} ) \operatorname{\mathbf {in}}\mathit {e^{\prime }} ] : \tau _{\mathit {n}} \operatorname{\Rightarrow }\Gamma _{\mathit {n}} .\) 
By lem:stackvar, we then have for some \(\tau \) , and \(\Gamma ^{\prime }\)  that:
\(& \Theta \mid \vec{\ell } \mid \Gamma \vdash \operatorname{\mathbf {let}}\mathit {x} = \mathit {f} ^ \ell ( \mathit {y_{{\mathrm {1}}}} ,\ldots , \mathit {y_{\mathit {n}}} ) \operatorname{\mathbf {in}}\mathit {e^{\prime }} : \tau \operatorname{\Rightarrow }\Gamma ^{\prime } \\& \Theta \mid []: \tau \operatorname{\Rightarrow }\Gamma ^{\prime } \mid \vec{\ell } \vdash _{\mathit {ectx} } \mathit {E} : \tau _{\mathit {n}} \operatorname{\Rightarrow }\Gamma _{\mathit {n}}\) 

Taking \(\tau _{{\mathrm {1}}} = \tau , \Gamma _{{\mathrm {1}}} = \Gamma ^{\prime }, \Gamma _{{\mathrm {0}}} = \Gamma , \Gamma _{{\mathrm {2}}} = \Gamma _{\mathit {n}}, \tau _{{\mathrm {2}}} = \tau _{\mathit {n}}\) ,
by lem:callfunc we have, for some \(\tau ^{\prime \prime \prime }, \Gamma ^{\prime \prime \prime }\) :
\(& \Theta \mid \ell : \vec{\ell } \mid \Gamma \vdash \sigma _{x} \mathit {e} : \tau ^{\prime \prime \prime } \operatorname{\Rightarrow }\Gamma ^{\prime \prime \prime } \\& \Theta \mid []: \tau ^{\prime \prime \prime } \operatorname{\Rightarrow }\Gamma ^{\prime \prime \prime } \mid \vec{\ell } \vdash _{\mathit {ectx} } \mathit {E} [\operatorname{\mathbf {let}}\mathit {x} = []^ \ell \operatorname{\mathbf {in}}\mathit {e^{\prime }} ] : \tau _{\mathit {n}} \operatorname{\Rightarrow }\Gamma _{\mathit {n}}\) 

where:
\(\sigma _{x} & = [ \mathit {y_{{\mathrm {1}}}} / \mathit {x_{{\mathrm {1}}}} ] \cdots [ \mathit {y_{\mathit {n}}} / \mathit {x_{\mathit {n}}} ] \\\Theta ( \mathit {f} ) & = \forall \lambda .\left\langle { \mathit {x_{{\mathrm {1}}}} \operatorname{:}\tau _{\mathit {i}} ,\dots , \mathit {x_{\mathit {n}}} \operatorname{:}\tau _{\mathit {n}} }\right\rangle \operatorname{\rightarrow }\left\langle { \mathit {x_{{\mathrm {1}}}} \operatorname{:}\tau ^{\prime }_{{\mathrm {1}}} ,\dots , \mathit {x_{\mathit {n}}} \operatorname{:}\tau ^{\prime }_{\mathit {n}} \mid \tau _{\mathit {p}} }\right\rangle \) 

We therefore take \(\Gamma ^{\prime \prime } = \Gamma \) .
We must also prove that \(\forall i\in \left\lbrace {1..n+1}\right\rbrace .\Theta \mid []: \tau _{\mathit {i}} \operatorname{\Rightarrow }\Gamma _{\mathit {i}} \mid \vec{\ell }_{{\mathit {i}-1}} \vdash _{\mathit {ectx} } \mathit {E^{\prime }_{{\mathit {i}-1}}} : \tau _{{\mathit {i}-1}} \operatorname{\Rightarrow }\Gamma _{{\mathit {i}-1}}\)  where \(\mathit {E^{\prime }_{\mathit {n}}} = \mathit {E} [ \operatorname{\mathbf {let}}\mathit {x} = []^ \ell \operatorname{\mathbf {in}}\mathit {e^{\prime }} ]\)  and \(\mathit {E^{\prime }_{\mathit {i}}} = \mathit {E_{\mathit {i}}} (0 \le i < n)\) ,
which can be divided into proving
\(\forall i\in \left\lbrace {1..n}\right\rbrace .\Theta \mid []: \tau _{\mathit {i}} \operatorname{\Rightarrow }\Gamma _{\mathit {i}} \mid \vec{\ell }_{{\mathit {i}-1}} \vdash _{\mathit {ectx} } \mathit {E^{\prime }_{{\mathit {i}-1}}} : \tau _{{\mathit {i}-1}} \operatorname{\Rightarrow }\Gamma _{{\mathit {i}-1}}\)  and \(\Theta \mid []: \tau _{n+1} \operatorname{\Rightarrow }\Gamma _{n+1} \mid \vec{\ell }_{\mathit {n}} \vdash _{\mathit {ectx} } \mathit {E^{\prime }_{\mathit {n}}} : \tau _{\mathit {n}} \operatorname{\Rightarrow }\Gamma _{\mathit {n}}\) . The first follows by inversion on \( \vdash _{\mathit {conf} }^D \left\langle { \mathit {H} , \mathit {R} , \vec{F} , \mathit {E} [ \operatorname{\mathbf {let}}\mathit {x} = \mathit {f} ^ \ell ( \mathit {y_{{\mathrm {1}}}} ,\ldots , \mathit {y_{\mathit {n}}} ) \operatorname{\mathbf {in}}\mathit {e^{\prime }} ] }\right\rangle  \) .
To show the latter, we define \( \Gamma _{n+1} = \Gamma ^{\prime \prime \prime }\)  and \( \tau _{n+1} = \tau ^{\prime \prime \prime }\) , whereby the
well-typing holds from the result of applying lem:callfunc above.
Finally, \(\mathbf {Cons} \, ( \mathit {H} , \mathit {R} , \Gamma ^{\prime \prime } )\)  follows immediately from \(\mathbf {Cons} \, ( \mathit {H} , \mathit {R} , \Gamma )\)  and \(\Gamma ^{\prime \prime } = \Gamma \) .

Proof of Progress
We first state the standard decomposition lemma.
[Decomposition]

For any term \(\mathit {e}\) , either \(\mathit {e} = \mathit {x}\)  for some \(\mathit {x}\)  or there exists some \(\mathit {E}\)  and \(\mathit {e^{\prime }}\)  where \(\mathit {E} [ \mathit {e^{\prime }} ] = \mathit {e}\)  and one of the following
cases hold:

\(\mathit {e^{\prime }} = \operatorname{\mathbf {let}}\mathit {x} = \operatorname{\mathbf {mkref}}\mathit {y} \operatorname{\mathbf {in}}\mathit {e^{\prime \prime }} \)

\(\mathit {e^{\prime }} = \operatorname{\mathbf {let}}\mathit {x} = \mathit {y} \operatorname{\mathbf {in}}\mathit {e^{\prime \prime }} \)

\(\mathit {e^{\prime }} = \operatorname{\mathbf {let}}\mathit {x} = n \operatorname{\mathbf {in}}\mathit {e^{\prime \prime }} \)

\(\mathit {e^{\prime }} = \operatorname{\mathbf {let}}\mathit {x} = * \mathit {y} \operatorname{\mathbf {in}}\mathit {e^{\prime \prime }} \)

\(\mathit {e^{\prime }} = \operatorname{\mathbf {let}}\mathit {x} = \mathit {f} ^ \ell ( \mathit {y_{{\mathrm {1}}}} ,\ldots , \mathit {y_{\mathit {n}}} ) \operatorname{\mathbf {in}}\mathit {e^{\prime \prime }} \)

\( \mathit {e^{\prime }} = \mathit {x} \operatorname{;}\mathit {e^{\prime \prime }} \)

\(\mathit {e^{\prime }} = \mathbf {alias}( \mathit {x} = \mathit {y} ) \operatorname{;}\mathit {e^{\prime \prime }} \)

\(\mathit {e^{\prime }} = \mathbf {alias}( \mathit {x} = * \mathit {y} ) \operatorname{;}\mathit {e^{\prime \prime }} \)

\(\mathit {e^{\prime }} = \operatorname{\mathbf {ifz}}\mathit {x} \operatorname{\mathbf {then}}\mathit {e_{{\mathrm {1}}}} \operatorname{\mathbf {else}}\mathit {e_{{\mathrm {2}}}} \)

\(\mathit {e^{\prime }} = \mathbf {assert}( \varphi ) \operatorname{;}\mathit {e^{\prime \prime }} \)

\(\mathit {e^{\prime }} = \mathit {x} \operatorname{:=}\mathit {y} \operatorname{;}\mathit {e} \)

Straightforward induction on \(\mathit {e}\) .
[Progress; lem:progress]
By inversion on \( \vdash _{\mathit {conf} }^D \mathbf {C} \) , either \(\mathbf {C} = \mathbf {AliasFail} \)  or \(\mathbf {C} = \left\langle { \mathit {H} , \mathit {R} , \vec{F} , \mathit {e} }\right\rangle  \) .
In the former case the result is immediate. In the latter case we have
that \( \Theta \mid \vec{\ell } \mid \Gamma \vdash \mathit {e} : \tau \operatorname{\Rightarrow }\Gamma ^{\prime } \)  for some \(\tau , \Gamma \)  and \(\Gamma ^{\prime }\) ,
and further from lem:decomposition, we have that either \(\mathit {e} = \mathit {x}\)  for some \(\mathit {x}\)  or there exists
some \(\mathit {E}\)  or \(\mathit {e^{\prime }}\)  where \(\mathit {e} = \mathit {E} [ \mathit {e^{\prime }} ]\)  and \(\mathit {e^{\prime }}\)  meets one of the cases in
lem:decomposition.
In the case \(\mathit {e} = \mathit {x}\) , we further make case analysis on the form of \(\vec{F}\) .
The case where \(\vec{F} = \epsilon \)  is immediate;
In the other case where \(\vec{F} = F : \vec{F}^{\prime }\) , the configuration can step
to \( \left\langle { \mathit {H} , \mathit {R} , \vec{F} , F [ \mathit {x} ] }\right\rangle  \)  according to R-Var.
For the remaining cases where \(\mathit {e} = \mathit {E} [ \mathit {e^{\prime }} ]\) ,
by the well-typing of \(\mathit {e}\)  with respect to \(\Gamma \)  and lem:stackvar,
we have that \( \Theta \mid \mathcal {L} \mid \Gamma \vdash \mathit {e^{\prime }} : \tau _{{\mathrm {0}}} \operatorname{\Rightarrow }\Gamma _{{\mathrm {0}}} \)  some \(\tau _{{\mathrm {0}}}\)  and \(\Gamma _{{\mathrm {0}}}\) .
We now treat the remaining forms of \(\mathit {e^{\prime }}\) 

e' = letx = * y ine”

By inversion (lem:inversion) and lem:subtyp-preserves-cons we must have
that for some \(\Gamma _{\mathit {p}}\)  where \(\mathbf {Cons} \, ( \mathit {H} , \mathit {R} , \Gamma _{\mathit {p}} )\)  that \( \mathit {y} \in \mathit {dom}( \Gamma _{\mathit {p}} ) \)  and
\(\Gamma _{\mathit {p}} ( \mathit {y} ) = \tau ^{\prime } \operatorname{\mathbf {ref}}^{ r } \) . From \(\mathbf {Cons} \, ( \mathit {H} , \mathit {R} , \Gamma _{\mathit {p}} )\)  we must have \( \mathit {y} \in \mathit {dom}( \mathit {R} ) \) 
and further \( \mathbf {SATv} ( \mathit {H} , \mathit {R} , \mathit {R} ( \mathit {y} ) , \tau ^{\prime } \operatorname{\mathbf {ref}}^{ r^{\prime } } ) \) , from which we must have
\(\mathit {R} ( \mathit {y} ) \, = \, \mathit {a}\)  and \( \mathit {a} \in \mathit {dom}( \mathit {H} ) \) . Then \(\mathbf {C}\)  can step according to R-Deref.
e' = letx = y ine” 
Again, by lem:inversion,lem:subtyp-preserves-cons and the definition
of \(\mathbf {Cons}\) , we must have that \( \mathit {y} \in \mathit {dom}( \mathit {R} ) \) , and the system can step
according to R-LetVar.
e' = letx = mkrefy ine” 
Similar to the R-LetVar case above.
e' = letx = n ine”
e' = x ;e”
e' = assert( ) ;e”

The first two can trivially step according to R-LetInt and R-Seq respectively.
the last can step according to R-Assert or R-AssertFalse (although
by lem:preservation,lem:assertfail the latter is impossible).
e' = alias( x = y ) ;e”

Again by lem:inversion,lem:subtyp-preserves-cons and that
\(\mathbf {Cons} \, ( \mathit {H} , \mathit {R} , \Gamma _{\mathit {p}} )\)  implies \(\mathit {x}\)  and \(\mathit {y}\)  are bound to addresses
in the register file, we have that the configuration can step according to R-Alias
or R-AliasFail.
e' = alias( x = * y ) ;e”

Similar to the case above, we must have that \(\mathit {x}\)  is bound to an address
in the register file, and that \(\mathit {y}\)  is bound to an address that
is itself mapped to an address in the heap \(\mathit {H}\) . Then the configuration may
step according to R-AliasPtr or R-AliasPtrFail
e = ifzx thene1 elsee2

As above, from the well-typing we must have that \(\mathit {x}\)  is bound in \(\mathit {R}\) 
to some integer \(n\) . Then the configuration may step according to R-IfTrue
or R-IfFalse depending on whether
\(n \, = \, 0\)  or \(n \, \ne \, 0\) .
e' = x :=y ;e”

From the well-typing of \(\mathit {e^{\prime }}\) ,
lem:inversion,lem:subtyp-preserves-cons and the definition
of \(\mathbf {Cons}\) , we must have that \( \mathit {y} \in \mathit {dom}( \mathit {R} ) \) ,
\( \mathit {x} \in \mathit {dom}( \mathit {R} ) \) , \(\mathit {R} ( \mathit {x} ) \, = \, \mathit {a}\) , and \( \mathit {a} \in \mathit {dom}( \mathit {H} ) \) . Then
the configuration can step according R-Assign.
e' = letx = f  ( y1 ,..., yn ) ine”

From the well-typing of the function call we must have that \( \mathit {f} \in \mathit {dom}( \Theta ) \) .
From \(\Theta \vdash \mathit {D}\)  in the precondition of \( \vdash _{\mathit {conf} }^D \mathbf {C} \) , we must have that
\( \mathit {f} \mapsto ( \mathit {x_{{\mathrm {1}}}} , \, .. \, , \mathit {x_{\mathit {j}}} ) \mathit {e^{\prime \prime \prime }} \in \mathit {D} \) . Then from T-FunDef we must have that
\( j = n \)  whereby the configuration can step according to R-Call.
