\Downarrow\leavevmode\nobreak\ \varsigma^{\prime},\sigma^{\prime},b$}\hskip
20.00003pt\hbox{\hskip-64.09695pt\hbox{\hbox{$\displaystyle\displaystyle\rho\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma^{\prime},\sigma^{\prime},l[b]\\!=\\!g\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\
\varsigma^{\prime\prime},\sigma^{\prime\prime},b^{\prime}$}}}}}\vbox{\hbox{\hskip-64.09695pt\hbox{\hbox{$\displaystyle\displaystyle\rho\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma^{\prime},\sigma^{\prime},l[b]\\!=\\!g\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\
\varsigma^{\prime\prime},\sigma^{\prime\prime},b^{\prime}$}}}\vbox{}}}}\over\hbox{\hskip
63.11949pt\vbox{\vbox{}\hbox{\hskip-63.11949pt\hbox{\hbox{$\displaystyle\displaystyle\rho\leavevmode\nobreak\
\vdash\leavevmode\nobreak\ \varsigma,\sigma,l[f]\\!=\\!g\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\
\varsigma^{\prime\prime},\sigma^{\prime\prime},b^{\prime}$}}}}}}$ Put-G
$\displaystyle\displaystyle{\hbox{\hskip
90.30359pt\vbox{\hbox{\hskip-90.30359pt\hbox{\hbox{$\displaystyle\displaystyle\rho\leavevmode\nobreak\
\vdash\leavevmode\nobreak\ \varsigma,\sigma,g\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\ \varsigma^{\prime},\sigma^{\prime},b$}\hskip
20.00003pt\hbox{\hskip-63.6965pt\hbox{\hbox{$\displaystyle\displaystyle\rho\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma^{\prime},\sigma^{\prime},l[c]\\!=\\!b\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\
\varsigma^{\prime\prime},\sigma^{\prime\prime},b^{\prime}$}}}}}\vbox{\hbox{\hskip-63.6965pt\hbox{\hbox{$\displaystyle\displaystyle\rho\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma^{\prime},\sigma^{\prime},l[c]\\!=\\!b\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\
\varsigma^{\prime\prime},\sigma^{\prime\prime},b^{\prime}$}}}\vbox{}}}}\over\hbox{\hskip
62.29715pt\vbox{\vbox{}\hbox{\hskip-62.29713pt\hbox{\hbox{$\displaystyle\displaystyle\rho\leavevmode\nobreak\
\vdash\leavevmode\nobreak\ \varsigma,\sigma,l[c]\\!=\\!g\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\
\varsigma^{\prime\prime},\sigma^{\prime\prime},b^{\prime}$}}}}}}$ Put
$\displaystyle\displaystyle{\hbox{\hskip
86.72704pt\vbox{\hbox{\hskip-86.72704pt\hbox{\hbox{$\displaystyle\displaystyle(d,f,v)=\sigma(l)$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\sigma^{\prime}=\sigma[l\mapsto(d[c\mapsto
v],f,v)]$}}}}\vbox{}}}\over\hbox{\hskip
59.7131pt\vbox{\vbox{}\hbox{\hskip-59.7131pt\hbox{\hbox{$\displaystyle\displaystyle\rho\leavevmode\nobreak\
\vdash\leavevmode\nobreak\ \varsigma,\sigma,l[c]\\!=\\!v\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\ \varsigma,\sigma^{\prime},v$}}}}}}$ Put-
NoContract $\displaystyle\displaystyle{\hbox{\hskip
114.7369pt\vbox{\hbox{\hskip-114.7369pt\hbox{\hbox{$\displaystyle\displaystyle(l^{\prime},\widehat{\rho},\flat,\mathcal{M})=\sigma(l)$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
c\not\in\textit{dom(}\mathcal{M}\textit{)}$}\hskip
20.00003pt\hbox{\hskip-61.2531pt\hbox{\hbox{$\displaystyle\displaystyle\rho\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma,\sigma,l^{\prime}[c]\\!=\\!v\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\
\varsigma^{\prime},\sigma^{\prime},v$}}}}}}\vbox{\hbox{\hskip-61.2531pt\hbox{\hbox{$\displaystyle\displaystyle\rho\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma,\sigma,l^{\prime}[c]\\!=\\!v\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\
\varsigma^{\prime},\sigma^{\prime},v$}}}\vbox{}}}}\over\hbox{\hskip
60.48311pt\vbox{\vbox{}\hbox{\hskip-60.4831pt\hbox{\hbox{$\displaystyle\displaystyle\rho\leavevmode\nobreak\
\vdash\leavevmode\nobreak\ \varsigma,\sigma,l[c]\\!=\\!v\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\ \varsigma^{\prime},\sigma^{\prime},v$}}}}}}$
Assert-E $\displaystyle\displaystyle{\hbox{\hskip
88.32242pt\vbox{\hbox{\hskip-88.32242pt\hbox{\hbox{$\displaystyle\displaystyle\rho\leavevmode\nobreak\
\vdash\leavevmode\nobreak\ \varsigma,\sigma,e\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\ \varsigma^{\prime},\sigma^{\prime},b$}\hskip
20.00003pt\hbox{\hskip-60.20638pt\hbox{\hbox{$\displaystyle\displaystyle\rho\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma^{\prime},\sigma^{\prime},b@^{\ell}f\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\
\varsigma^{\prime\prime},\sigma^{\prime\prime},b^{\prime}$}}}}}\vbox{\hbox{\hskip-60.20638pt\hbox{\hbox{$\displaystyle\displaystyle\rho\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma^{\prime},\sigma^{\prime},b@^{\ell}f\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\
\varsigma^{\prime\prime},\sigma^{\prime\prime},b^{\prime}$}}}\vbox{}}}}\over\hbox{\hskip
58.5709pt\vbox{\vbox{}\hbox{\hskip-58.5709pt\hbox{\hbox{$\displaystyle\displaystyle\rho\leavevmode\nobreak\
\vdash\leavevmode\nobreak\ \varsigma,\sigma,e@^{\ell}f\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\
\varsigma^{\prime\prime},\sigma^{\prime\prime},b^{\prime}$}}}}}}$ Assert-F
$\displaystyle\displaystyle{\hbox{\hskip
87.84222pt\vbox{\hbox{\hskip-87.84221pt\hbox{\hbox{$\displaystyle\displaystyle\rho\leavevmode\nobreak\
\vdash\leavevmode\nobreak\ \varsigma,\sigma,e\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\ \varsigma^{\prime},\sigma^{\prime},b$}\hskip
20.00003pt\hbox{\hskip-59.24596pt\hbox{\hbox{$\displaystyle\displaystyle\widehat{\emptyset}\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma,\sigma^{\prime},v@^{\ell}b\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\
\varsigma^{\prime\prime},\sigma^{\prime\prime},b^{\prime}$}}}}}\vbox{\hbox{\hskip-59.24596pt\hbox{\hbox{$\displaystyle\displaystyle\widehat{\emptyset}\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma,\sigma^{\prime},v@^{\ell}b\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\
\varsigma^{\prime\prime},\sigma^{\prime\prime},b^{\prime}$}}}\vbox{}}}}\over\hbox{\hskip
58.18779pt\vbox{\vbox{}\hbox{\hskip-58.18777pt\hbox{\hbox{$\displaystyle\displaystyle\rho\leavevmode\nobreak\
\vdash\leavevmode\nobreak\ \varsigma,\sigma,v@^{\ell}e\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\
\varsigma^{\prime\prime},\sigma^{\prime\prime},b^{\prime}$}}}}}}$ Construct-F
$\displaystyle\displaystyle{\hbox{\hskip
96.78856pt\vbox{\hbox{\hskip-96.78856pt\hbox{\hbox{$\displaystyle\displaystyle\rho\leavevmode\nobreak\
\vdash\leavevmode\nobreak\ \varsigma,\sigma,f\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\ \varsigma^{\prime},\sigma^{\prime},b$}\hskip
20.00003pt\hbox{\hskip-75.82266pt\hbox{\hbox{$\displaystyle\displaystyle\rho\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma^{\prime},\sigma^{\prime},(\widehat{\rho},\Lambda
x.e)(b)\leavevmode\nobreak\ \Downarrow\leavevmode\nobreak\
\varsigma^{\prime\prime},\sigma^{\prime\prime},b^{\prime}$}}}}}\vbox{\hbox{\hskip-75.82266pt\hbox{\hbox{$\displaystyle\displaystyle\rho\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma^{\prime},\sigma^{\prime},(\widehat{\rho},\Lambda
x.e)(b)\leavevmode\nobreak\ \Downarrow\leavevmode\nobreak\
\varsigma^{\prime\prime},\sigma^{\prime\prime},b^{\prime}$}}}\vbox{}}}}\over\hbox{\hskip
74.8452pt\vbox{\vbox{}\hbox{\hskip-74.84518pt\hbox{\hbox{$\displaystyle\displaystyle\rho\leavevmode\nobreak\
\vdash\leavevmode\nobreak\ \varsigma,\sigma,(\widehat{\rho},\Lambda
x.e)(f)\leavevmode\nobreak\ \Downarrow\leavevmode\nobreak\
\varsigma^{\prime\prime},\sigma^{\prime\prime},b^{\prime}$}}}}}}$ Wrap-E
$\displaystyle\displaystyle{\hbox{\hskip
91.25299pt\vbox{\hbox{\hskip-91.25298pt\hbox{\hbox{$\displaystyle\displaystyle\rho\leavevmode\nobreak\
\vdash\leavevmode\nobreak\ \varsigma,\sigma,e\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\ \varsigma^{\prime},\sigma^{\prime},b$}\hskip
20.00003pt\hbox{\hskip-66.0675pt\hbox{\hbox{$\displaystyle\displaystyle\rho\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma^{\prime},\sigma^{\prime},\textit{wrap}(b)\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\
\varsigma^{\prime\prime},\sigma^{\prime\prime},b^{\prime}$}}}}}\vbox{\hbox{\hskip-66.0675pt\hbox{\hbox{$\displaystyle\displaystyle\rho\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma^{\prime},\sigma^{\prime},\textit{wrap}(b)\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\
\varsigma^{\prime\prime},\sigma^{\prime\prime},b^{\prime}$}}}\vbox{}}}}\over\hbox{\hskip
64.43204pt\vbox{\vbox{}\hbox{\hskip-64.43204pt\hbox{\hbox{$\displaystyle\displaystyle\rho\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma,\sigma,\textit{wrap}(e)\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\
\varsigma^{\prime\prime},\sigma^{\prime\prime},b^{\prime}$}}}}}}$ Figure 10.
Inference rules for $\lambda_{J}^{\mathcal{C}on}$ (cont’d). Op-E-Error
$\displaystyle\displaystyle\rho\leavevmode\nobreak\ \vdash\leavevmode\nobreak\
\varsigma,\sigma,\textit{op}(\bullet,f)\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\ \varsigma,\sigma,\bullet$ Op-F-Error
$\displaystyle\displaystyle\rho\leavevmode\nobreak\ \vdash\leavevmode\nobreak\
\varsigma,\sigma,\textit{op}(v,\bullet)\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\ \varsigma,\sigma,\bullet$ App-E-Error
$\displaystyle\displaystyle\rho\leavevmode\nobreak\ \vdash\leavevmode\nobreak\
\varsigma,\sigma,\bullet(f)\leavevmode\nobreak\ \Downarrow\leavevmode\nobreak\
\varsigma,\sigma,\bullet$ App-F-Error
$\displaystyle\displaystyle\rho\leavevmode\nobreak\ \vdash\leavevmode\nobreak\
\varsigma,\sigma,l(\bullet)\leavevmode\nobreak\ \Downarrow\leavevmode\nobreak\
\varsigma,\sigma,\bullet$ New-E-Error
$\displaystyle\displaystyle\rho\leavevmode\nobreak\ \vdash\leavevmode\nobreak\
\varsigma,\sigma,\textit{new}\leavevmode\nobreak\ \bullet\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\ \varsigma,\sigma,\bullet$ Get-E-Error
$\displaystyle\displaystyle\rho\leavevmode\nobreak\ \vdash\leavevmode\nobreak\
\varsigma,\sigma,\bullet[f]\leavevmode\nobreak\ \Downarrow\leavevmode\nobreak\
\varsigma,\sigma,\bullet$ Get-F-Error
$\displaystyle\displaystyle\rho\leavevmode\nobreak\ \vdash\leavevmode\nobreak\
\varsigma,\sigma,l[\bullet]\leavevmode\nobreak\ \Downarrow\leavevmode\nobreak\
\varsigma,\sigma,\bullet$ Put-E-Error
$\displaystyle\displaystyle\rho\leavevmode\nobreak\ \vdash\leavevmode\nobreak\
\varsigma,\sigma,\bullet[f]\\!=\\!g\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\ \varsigma,\sigma,\bullet$ Put-F-Error
$\displaystyle\displaystyle\rho\leavevmode\nobreak\ \vdash\leavevmode\nobreak\
\varsigma,\sigma,l[\bullet]=g\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\ \varsigma,\sigma,\bullet$ Put-G-Error
$\displaystyle\displaystyle\rho\leavevmode\nobreak\ \vdash\leavevmode\nobreak\
\varsigma,\sigma,l[c]=\bullet\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\ \varsigma,\sigma,\bullet$ Assert-E-Error
$\displaystyle\displaystyle\rho\leavevmode\nobreak\ \vdash\leavevmode\nobreak\
\varsigma,\sigma,\bullet@f\leavevmode\nobreak\ \Downarrow\leavevmode\nobreak\
\varsigma,\sigma,\bullet$ Assert-F-Error
$\displaystyle\displaystyle\rho\leavevmode\nobreak\ \vdash\leavevmode\nobreak\
\varsigma,\sigma,v@\bullet\leavevmode\nobreak\ \Downarrow\leavevmode\nobreak\
\varsigma,\sigma,\bullet$ Wrap-E-Error
$\displaystyle\displaystyle\widehat{\rho}\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma,\sigma,\textit{wrap}(\bullet)\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\ \varsigma,\sigma,\bullet$ Construct-F-Error
$\displaystyle\displaystyle\widehat{\rho}\leavevmode\nobreak\
\vdash\leavevmode\nobreak\ \varsigma,\sigma,(\widehat{\rho},\Lambda
x.e)(\bullet)@v\leavevmode\nobreak\ \Downarrow_{\kappa}\leavevmode\nobreak\
\varsigma,\sigma,\bullet$ Figure 11. Inference rules for exception handling.

Figure 9 and 10 defines the standard evaluation rules for expressions $e$ in
$\lambda_{J}^{\mathcal{C}on}$. The inference rules for expressions are mostly
standard. Each rule for a composite expression evaluates exactly one
subexpression and then recursively invokes the evaluation judgment to
continue. Once all subexpressions are evaluated, the respective rule performs
the desired operation.

The corresponding straightforward error propagation rules are disjoint to the
remaining rules because they fire only if an intermediate term contains an
exception. The rules set in Figure 11 defines error handling.

####  C.2.1. Contract Construction

Contract-Fresh $\displaystyle\displaystyle\rho\leavevmode\nobreak\
\vdash\leavevmode\nobreak\ \varsigma,\sigma,\mathcal{C}\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\ \varsigma,\sigma,(\emptyset,\mathcal{C})$
Contract-Sandbox $\displaystyle\displaystyle\widehat{\rho}\leavevmode\nobreak\
\vdash\leavevmode\nobreak\ \varsigma,\sigma,\mathcal{C}\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\ \varsigma,\sigma,(\widehat{\rho},\mathcal{C})$
Constructor-Fresh $\displaystyle\displaystyle\rho\leavevmode\nobreak\
\vdash\leavevmode\nobreak\ \varsigma,\sigma,\mathcal{A}\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\ \varsigma,\sigma,(\emptyset,\mathcal{A})$
Constructor-Sandbox
$\displaystyle\displaystyle\widehat{\rho}\leavevmode\nobreak\
\vdash\leavevmode\nobreak\ \varsigma,\sigma,\mathcal{A}\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\ \varsigma,\sigma,(\widehat{\rho},\mathcal{A})$
Construct $\displaystyle\displaystyle{\hbox{\hskip
133.78815pt\vbox{\hbox{\hskip-133.78813pt\hbox{\hbox{$\displaystyle\displaystyle\rho\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma,\sigma,\textit{wrap}(w)\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\
\varsigma^{\prime},\sigma^{\prime},\widehat{w}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\widehat{\rho}[x\mapsto\widehat{w}]\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma^{\prime},\sigma^{\prime},\mathcal{C}\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\
\varsigma^{\prime},\sigma^{\prime},b$}}}}\vbox{}}}\over\hbox{\hskip
73.71288pt\vbox{\vbox{}\hbox{\hskip-73.71286pt\hbox{\hbox{$\displaystyle\displaystyle\rho\leavevmode\nobreak\
\vdash\leavevmode\nobreak\ \varsigma,\sigma,(\widehat{\rho},\Lambda
x.\mathcal{C})(w)\leavevmode\nobreak\ \Downarrow\leavevmode\nobreak\
\varsigma^{\prime},\sigma^{\prime},b$}}}}}}$ Figure 12. Contract Construction
rules for $\lambda_{J}^{\mathcal{C}on}$.

Contract monitoring happens in the context of a secure sandbox environment to
preserve noninterference. So a contract definition (contract abstraction) will
evaluate to a contract closure containing the contract (the abstraction)
together with an empty environment or together with an sandbox environment
$\widehat{\rho}$ when defining the contract (the abstraction) inside of a
sandbox environment. Figure 12 contains its inference rules.

Constructor application (Rule Construct) starts after the first expression
evaluates to a contract closure and the second expression evaluates to a
value. It wraps the given value and evaluates the contract $\mathcal{C}$ in
the sandbox environment after binding the sandboxed value $\widehat{w}$.

####  C.2.2. Contract Assertion

Assert $\displaystyle\displaystyle{\hbox{\hskip
57.27571pt\vbox{\hbox{\hskip-57.2757pt\hbox{\hbox{$\displaystyle\displaystyle\widehat{\rho}\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma,\sigma,v@^{\flat}\mathcal{C}\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\
\varsigma^{\prime},\sigma^{\prime},b$}}}\vbox{}}}\over\hbox{\hskip
65.13858pt\vbox{\vbox{}\hbox{\hskip-65.13857pt\hbox{\hbox{$\displaystyle\displaystyle\rho\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma,\sigma,v@^{\flat}(\widehat{\rho},\mathcal{C})\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\ \varsigma^{\prime},\sigma^{\prime},b$}}}}}}$

Assert-BaseContract $\displaystyle\displaystyle{\hbox{\hskip
134.07697pt\vbox{\hbox{\hskip-134.07697pt\hbox{\hbox{$\displaystyle\displaystyle\widehat{\rho}\leavevmode\nobreak\
\vdash\leavevmode\nobreak\ \varsigma,\sigma,(\lambda
x.e)(\textit{wrap}(v))\leavevmode\nobreak\ \Downarrow\leavevmode\nobreak\
\varsigma^{\prime},\sigma^{\prime},b$}\hskip
20.00003pt\hbox{\hskip-85.10309pt\hbox{\hbox{$\displaystyle\displaystyle\widehat{\rho}\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma^{\prime}\cup\\{\flat\blacktriangleleft\tau(b)\\},\sigma^{\prime},v@^{\flat}b\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\
\varsigma^{\prime\prime},\sigma^{\prime\prime},b^{\prime}$}}}}}\vbox{\hbox{\hskip-85.10309pt\hbox{\hbox{$\displaystyle\displaystyle\widehat{\rho}\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma^{\prime}\cup\\{\flat\blacktriangleleft\tau(b)\\},\sigma^{\prime},v@^{\flat}b\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\
\varsigma^{\prime\prime},\sigma^{\prime\prime},b^{\prime}$}}}\vbox{}}}}\over\hbox{\hskip
66.29924pt\vbox{\vbox{}\hbox{\hskip-66.29922pt\hbox{\hbox{$\displaystyle\displaystyle\widehat{\rho}\leavevmode\nobreak\
\vdash\leavevmode\nobreak\ \varsigma,\sigma,v@^{\flat}\lambda
x.e\leavevmode\nobreak\ \Downarrow\leavevmode\nobreak\
\varsigma^{\prime\prime},\sigma^{\prime\prime},b^{\prime}$}}}}}}$ Assert-
DelayedContract $\displaystyle\displaystyle{\hbox{\hskip
69.67987pt\vbox{\hbox{\hskip-69.67986pt\hbox{\hbox{$\displaystyle\displaystyle
l^{\prime}\notin\textit{dom(}\sigma\textit{)}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\sigma^{\prime}=\sigma[l^{\prime}\mapsto(l,\widehat{\rho},\flat,\mathcal{Q})]$}}}}\vbox{}}}\over\hbox{\hskip
55.98523pt\vbox{\vbox{}\hbox{\hskip-55.98523pt\hbox{\hbox{$\displaystyle\displaystyle\widehat{\rho}\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma,\sigma,l@^{\flat}\mathcal{Q}\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\ \varsigma,\sigma^{\prime},l^{\prime}$}}}}}}$
Assert-IntersectionContract $\displaystyle\displaystyle{\hbox{\hskip
140.37292pt\vbox{\hbox{\hskip-140.37292pt\hbox{\hbox{$\displaystyle\displaystyle\iota_{1},\iota_{2}\not\in\textit{dom(}\varsigma\textit{)}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\widehat{\rho}\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma\cup\\{\flat\blacktriangleleft\iota_{1}\cap\iota_{2}\\},\sigma,(v@^{\iota_{1}}\mathcal{I})@^{\iota_{2}}\mathcal{C}\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\
\varsigma^{\prime},\sigma^{\prime},b$}}}}\vbox{}}}\over\hbox{\hskip
66.30351pt\vbox{\vbox{}\hbox{\hskip-66.3035pt\hbox{\hbox{$\displaystyle\displaystyle\widehat{\rho}\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma,\sigma,v@^{\flat}(\mathcal{I}\cap\mathcal{C})\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\ \varsigma^{\prime},\sigma^{\prime},b$}}}}}}$
Assert-UnionContract $\displaystyle\displaystyle{\hbox{\hskip
142.38683pt\vbox{\hbox{\hskip-142.38681pt\hbox{\hbox{$\displaystyle\displaystyle\iota_{1},\iota_{2}\not\in\textit{dom(}\varsigma\textit{)}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\widehat{\rho}\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma\cup\\{\flat\blacktriangleleft\iota_{1}\cup\iota_{2}\\},\sigma,(v@^{\iota_{1}}\mathcal{C})@^{\iota_{2}}\mathcal{D}\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\
\varsigma^{\prime},\sigma^{\prime},b$}}}}\vbox{}}}\over\hbox{\hskip
68.3174pt\vbox{\vbox{}\hbox{\hskip-68.3174pt\hbox{\hbox{$\displaystyle\displaystyle\widehat{\rho}\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma,\sigma,v@^{\flat}(\mathcal{C}\cup\mathcal{D})\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\ \varsigma^{\prime},\sigma^{\prime},b$}}}}}}$
Assert-AndContract $\displaystyle\displaystyle{\hbox{\hskip
142.38683pt\vbox{\hbox{\hskip-142.38681pt\hbox{\hbox{$\displaystyle\displaystyle\iota_{1},\iota_{2}\not\in\textit{dom(}\varsigma\textit{)}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\widehat{\rho}\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma\cup\\{\flat\blacktriangleleft\iota_{1}\wedge\iota_{2}\\},\sigma,(v@^{\iota_{1}}\mathcal{C})@^{\iota_{2}}\mathcal{D}\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\
\varsigma^{\prime},\sigma^{\prime},b$}}}}\vbox{}}}\over\hbox{\hskip
68.3174pt\vbox{\vbox{}\hbox{\hskip-68.3174pt\hbox{\hbox{$\displaystyle\displaystyle\widehat{\rho}\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma,\sigma,v@^{\flat}(\mathcal{C}\wedge\mathcal{D})\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\ \varsigma^{\prime},\sigma^{\prime},b$}}}}}}$
Assert-OrContract $\displaystyle\displaystyle{\hbox{\hskip
140.37292pt\vbox{\hbox{\hskip-140.37292pt\hbox{\hbox{$\displaystyle\displaystyle\iota_{1},\iota_{2}\not\in\textit{dom(}\varsigma\textit{)}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\widehat{\rho}\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma\cup\\{\flat\blacktriangleleft\iota_{1}\vee\iota_{2}\\},\sigma,(v@^{\iota_{1}}\mathcal{I})@^{\iota_{2}}\mathcal{C}\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\
\varsigma^{\prime},\sigma^{\prime},b$}}}}\vbox{}}}\over\hbox{\hskip
66.30351pt\vbox{\vbox{}\hbox{\hskip-66.3035pt\hbox{\hbox{$\displaystyle\displaystyle\widehat{\rho}\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma,\sigma,v@^{\flat}(\mathcal{I}\vee\mathcal{C})\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\ \varsigma^{\prime},\sigma^{\prime},b$}}}}}}$
Assert-NotContract $\displaystyle\displaystyle{\hbox{\hskip
114.75363pt\vbox{\hbox{\hskip-114.75363pt\hbox{\hbox{$\displaystyle\displaystyle\iota\not\in\textit{dom(}\varsigma\textit{)}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\widehat{\rho}\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma\cup\\{\flat\blacktriangleleft\neg\iota\\},\sigma,v@^{\iota}\mathcal{I}\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\
\varsigma^{\prime},\sigma^{\prime},b$}}}}\vbox{}}}\over\hbox{\hskip
62.6924pt\vbox{\vbox{}\hbox{\hskip-62.69238pt\hbox{\hbox{$\displaystyle\displaystyle\widehat{\rho}\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma,\sigma,v@^{\flat}(\neg\mathcal{I})\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\ \varsigma^{\prime},\sigma^{\prime},b$}}}}}}$

Figure 13. Inference rules for contract assertion.

It remains to define contract assertion (Figure 13).

Rule Assert applies after the first subexpression evaluates to a value and the
second subexpression evaluates to a contract-value. It triggers the evaluation
of contract $\mathcal{C}$ in an sandbox environment $\widehat{\rho}$.

Asserting a base contract to any value wraps the value to avoid interference
and evaluates the predicate after binding the wrapped value. Finally, a new
constraint is attached with the result of the predicate.

Once a base contract evaluates to a value (Figure 14) the constraint state is
checked whether a violation can be signaled.

Rule Assert-DelayedContract asserts a delayed contract to an object. It wraps
its location in a proxy together with the current sandbox environment, the
associated blame identifier, and the contract itself. It is an error to assert
a delayed contract to a primitive value.

Asserting an intersection-contract, an union-contract, or an boolean
combination asserts the first subcontract to the value before it asserts the
second subcontract to the resulting behavior. These contract evaluations
create a new constraint that contains thecorresponding operator, respectively.

NoBlame $\displaystyle\displaystyle{\hbox{\hskip
46.86987pt\vbox{\hbox{\hskip-46.86986pt\hbox{\hbox{$\displaystyle\displaystyle\varsigma\textit{
is not a blame state}$}}}\vbox{}}}\over\hbox{\hskip
54.44983pt\vbox{\vbox{}\hbox{\hskip-54.44983pt\hbox{\hbox{$\displaystyle\displaystyle\widehat{\rho}\leavevmode\nobreak\
\vdash\leavevmode\nobreak\ \varsigma,\sigma,v@^{\flat}b\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\ \varsigma,\sigma,v$}}}}}}$ Blame
$\displaystyle\displaystyle{\hbox{\hskip
37.98096pt\vbox{\hbox{\hskip-37.98096pt\hbox{\hbox{$\displaystyle\displaystyle\varsigma\textit{
is a blame state}$}}}\vbox{}}}\over\hbox{\hskip
53.51352pt\vbox{\vbox{}\hbox{\hskip-53.51352pt\hbox{\hbox{$\displaystyle\displaystyle\widehat{\rho}\leavevmode\nobreak\
\vdash\leavevmode\nobreak\ \varsigma,\sigma,v@^{\flat}b\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\ \varsigma,\sigma,\bullet$}}}}}}$ Figure 14.
Inference rules for blame calculation.

####  C.2.3. Application, Read, and Assignment

Function application, property read, and property assignment distinguish two
cases: either the operation applies directly to a non-proxy object or it
applies to a proxy. If the target of the operation is not a proxy object, then
the usual rules apply.

Figure 15 contains the inference rules for function application and property
access for the non-standard cases.

App-FunctionContract $\displaystyle\displaystyle{\hbox{\hskip
158.71722pt\vbox{\hbox{\hskip-158.71722pt\hbox{\hbox{$\displaystyle\displaystyle(l^{\prime},\widehat{\rho},\flat,(\mathcal{C}\rightarrow\mathcal{D}))=\sigma(l)$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\iota_{1},\iota_{2}\not\in\textit{dom(}\varsigma\textit{)}$}\hskip
20.00003pt\hbox{\hskip-121.81747pt\hbox{\hbox{$\displaystyle\displaystyle\rho\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma\cup\\{\flat\blacktriangleleft\iota_{1}\rightarrow\iota_{2}\\},\sigma,(l^{\prime}(v@^{\iota_{1}}(\widehat{\rho},\mathcal{C})))@^{\iota_{2}}(\widehat{\rho},\mathcal{D})\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\
\varsigma^{\prime},\sigma^{\prime},b$}}}}}}\vbox{\hbox{\hskip-121.81747pt\hbox{\hbox{$\displaystyle\displaystyle\rho\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma\cup\\{\flat\blacktriangleleft\iota_{1}\rightarrow\iota_{2}\\},\sigma,(l^{\prime}(v@^{\iota_{1}}(\widehat{\rho},\mathcal{C})))@^{\iota_{2}}(\widehat{\rho},\mathcal{D})\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\
\varsigma^{\prime},\sigma^{\prime},b$}}}\vbox{}}}}\over\hbox{\hskip
53.97328pt\vbox{\vbox{}\hbox{\hskip-53.97327pt\hbox{\hbox{$\displaystyle\displaystyle\rho\leavevmode\nobreak\
\vdash\leavevmode\nobreak\ \varsigma,\sigma,l(v)\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\ \varsigma^{\prime},\sigma^{\prime},b$}}}}}}$
App-DependentContract $\displaystyle\displaystyle{\hbox{\hskip
141.79141pt\vbox{\hbox{\hskip-141.79141pt\hbox{\hbox{$\displaystyle\displaystyle(l^{\prime},\widehat{\rho},\flat,(x\rightarrow\mathcal{A}\,x))=\sigma(l)$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\rho\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma,\sigma,(l^{\prime}(v))@^{\flat}(\widehat{\rho},\mathcal{A})(v)\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\
\varsigma^{\prime},\sigma^{\prime},b$}}}}\vbox{}}}\over\hbox{\hskip
53.97328pt\vbox{\vbox{}\hbox{\hskip-53.97327pt\hbox{\hbox{$\displaystyle\displaystyle\rho\leavevmode\nobreak\
\vdash\leavevmode\nobreak\ \varsigma,\sigma,l(v)\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\ \varsigma^{\prime},\sigma^{\prime},b$}}}}}}$
App-IntersectionContract $\displaystyle\displaystyle{\hbox{\hskip
162.3978pt\vbox{\hbox{\hskip-162.39778pt\hbox{\hbox{$\displaystyle\displaystyle(l^{\prime},\widehat{\rho},\flat,(\mathcal{Q}\cap\mathcal{R}))=\sigma(l)$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\iota_{1},\iota_{2}\not\in\textit{dom(}\varsigma\textit{)}$}\hskip
20.00003pt\hbox{\hskip-127.23415pt\hbox{\hbox{$\displaystyle\displaystyle\rho\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma\cup\\{\flat\blacktriangleleft\iota_{1}\cap\iota_{2}\\},\sigma,((l^{\prime}@^{\iota_{1}}(\widehat{\rho},\mathcal{Q}))@^{\iota_{2}}(\widehat{\rho},\mathcal{R}))\,(v)\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\
\varsigma^{\prime},\sigma^{\prime},b$}}}}}}\vbox{\hbox{\hskip-127.23415pt\hbox{\hbox{$\displaystyle\displaystyle\rho\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma\cup\\{\flat\blacktriangleleft\iota_{1}\cap\iota_{2}\\},\sigma,((l^{\prime}@^{\iota_{1}}(\widehat{\rho},\mathcal{Q}))@^{\iota_{2}}(\widehat{\rho},\mathcal{R}))\,(v)\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\
\varsigma^{\prime},\sigma^{\prime},b$}}}\vbox{}}}}\over\hbox{\hskip
53.97328pt\vbox{\vbox{}\hbox{\hskip-53.97327pt\hbox{\hbox{$\displaystyle\displaystyle\rho\leavevmode\nobreak\
\vdash\leavevmode\nobreak\ \varsigma,\sigma,l(v)\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\ \varsigma^{\prime},\sigma^{\prime},b$}}}}}}$
App-OrContarct $\displaystyle\displaystyle{\hbox{\hskip
162.3978pt\vbox{\hbox{\hskip-162.39778pt\hbox{\hbox{$\displaystyle\displaystyle(l^{\prime},\widehat{\rho},\flat,(\mathcal{Q}\vee\mathcal{R}))=\sigma(l)$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\iota_{1},\iota_{2}\not\in\textit{dom(}\varsigma\textit{)}$}\hskip
20.00003pt\hbox{\hskip-127.23415pt\hbox{\hbox{$\displaystyle\displaystyle\rho\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma\cup\\{\flat\blacktriangleleft\iota_{1}\vee\iota_{2}\\},\sigma,((l^{\prime}@^{\iota_{1}}(\widehat{\rho},\mathcal{Q}))@^{\iota_{2}}(\widehat{\rho},\mathcal{R}))\,(v)\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\
\varsigma^{\prime},\sigma^{\prime},b$}}}}}}\vbox{\hbox{\hskip-127.23415pt\hbox{\hbox{$\displaystyle\displaystyle\rho\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma\cup\\{\flat\blacktriangleleft\iota_{1}\vee\iota_{2}\\},\sigma,((l^{\prime}@^{\iota_{1}}(\widehat{\rho},\mathcal{Q}))@^{\iota_{2}}(\widehat{\rho},\mathcal{R}))\,(v)\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\
\varsigma^{\prime},\sigma^{\prime},b$}}}\vbox{}}}}\over\hbox{\hskip
53.97328pt\vbox{\vbox{}\hbox{\hskip-53.97327pt\hbox{\hbox{$\displaystyle\displaystyle\rho\leavevmode\nobreak\
\vdash\leavevmode\nobreak\ \varsigma,\sigma,l(v)\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\ \varsigma^{\prime},\sigma^{\prime},b$}}}}}}$
App-NotContarct $\displaystyle\displaystyle{\hbox{\hskip
138.44913pt\vbox{\hbox{\hskip-138.44913pt\hbox{\hbox{$\displaystyle\displaystyle(l^{\prime},\widehat{\rho},\flat,(\neg\mathcal{Q}))=\sigma(l)$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\iota\not\in\textit{dom(}\varsigma\textit{)}$}\hskip
20.00003pt\hbox{\hskip-100.28172pt\hbox{\hbox{$\displaystyle\displaystyle\rho\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma\cup\\{\flat\blacktriangleleft\neg\iota\\},\sigma,(l^{\prime}@^{\iota}(\widehat{\rho},\mathcal{Q}))\,(v)\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\
\varsigma^{\prime},\sigma^{\prime},b$}}}}}}\vbox{\hbox{\hskip-100.28172pt\hbox{\hbox{$\displaystyle\displaystyle\rho\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma\cup\\{\flat\blacktriangleleft\neg\iota\\},\sigma,(l^{\prime}@^{\iota}(\widehat{\rho},\mathcal{Q}))\,(v)\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\
\varsigma^{\prime},\sigma^{\prime},b$}}}\vbox{}}}}\over\hbox{\hskip
53.97328pt\vbox{\vbox{}\hbox{\hskip-53.97327pt\hbox{\hbox{$\displaystyle\displaystyle\rho\leavevmode\nobreak\
\vdash\leavevmode\nobreak\ \varsigma,\sigma,l(v)\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\ \varsigma^{\prime},\sigma^{\prime},b$}}}}}}$
Get-Contract $\displaystyle\displaystyle{\hbox{\hskip
157.1683pt\vbox{\hbox{\hskip-157.16829pt\hbox{\hbox{$\displaystyle\displaystyle(l^{\prime},\widehat{\rho},\flat,\mathcal{M})=\sigma(l)$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
c\in\textit{dom(}\mathcal{M}\textit{)}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\iota\not\in\textit{dom(}\sigma\textit{)}$}\hskip
20.00003pt\hbox{\hskip-80.75122pt\hbox{\hbox{$\displaystyle\displaystyle\rho\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma,\sigma,(l^{\prime}[c])@^{\flat}(\widehat{\rho},\mathcal{M}(c))\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\
\varsigma^{\prime},\sigma^{\prime},b$}}}}}}}\vbox{\hbox{\hskip-80.75122pt\hbox{\hbox{$\displaystyle\displaystyle\rho\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma,\sigma,(l^{\prime}[c])@^{\flat}(\widehat{\rho},\mathcal{M}(c))\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\
\varsigma^{\prime},\sigma^{\prime},b$}}}\vbox{}}}}\over\hbox{\hskip
52.42294pt\vbox{\vbox{}\hbox{\hskip-52.42293pt\hbox{\hbox{$\displaystyle\displaystyle\rho\leavevmode\nobreak\
\vdash\leavevmode\nobreak\ \varsigma,\sigma,l[c]\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\ \varsigma^{\prime},\sigma^{\prime},b$}}}}}}$
Put-Contract $\displaystyle\displaystyle{\hbox{\hskip
170.42332pt\vbox{\hbox{\hskip-170.42332pt\hbox{\hbox{$\displaystyle\displaystyle(l^{\prime},\widehat{\rho},\flat,\mathcal{M})=\sigma(l)$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
c\in\textit{dom(}\mathcal{M}\textit{)}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\iota\not\in\textit{dom(}\sigma\textit{)}$}\hskip
20.00003pt\hbox{\hskip-107.26128pt\hbox{\hbox{$\displaystyle\displaystyle\rho\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma\cup\\{\flat\blacktriangleleft\tilde{\iota}\\},\sigma^{\prime},l^{\prime}[c]\\!=\\!(v@^{\iota}(\widehat{\rho},\mathcal{M}(c))\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\
\varsigma^{\prime},\sigma^{\prime},v$}}}}}}}\vbox{\hbox{\hskip-107.26128pt\hbox{\hbox{$\displaystyle\displaystyle\rho\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma\cup\\{\flat\blacktriangleleft\tilde{\iota}\\},\sigma^{\prime},l^{\prime}[c]\\!=\\!(v@^{\iota}(\widehat{\rho},\mathcal{M}(c))\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\
\varsigma^{\prime},\sigma^{\prime},v$}}}\vbox{}}}}\over\hbox{\hskip
60.48311pt\vbox{\vbox{}\hbox{\hskip-60.4831pt\hbox{\hbox{$\displaystyle\displaystyle\rho\leavevmode\nobreak\
\vdash\leavevmode\nobreak\ \varsigma,\sigma,l[c]\\!=\\!v\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\ \varsigma^{\prime},\sigma^{\prime},v$}}}}}}$
Figure 15. Inference rules for function application, property read, and
property assignment.

If the target object is a proxy that carries a function contract, then the
domain contract $\mathcal{C}$ is attached to the argument. Next, function
application continues by passing the input value to the proxy’s target
location $l^{\prime}$. After completion, the range contract $\mathcal{D}$ is
applied to the function’s result.

The assertion of both contracts takes place inside the sandbox environment
$\widehat{\rho}$ stored in the proxy. A new constraint with two fresh
variables indicates that both parts have to hold.

In case of a dependent contract attached to a function, function application
proceeds by passing the input value to the proxy’s target location. Next, the
original function argument gets passed to the contract constructor where the
value gets wrapped to be acceptable in the sandbox environment. Finally, the
wrapped input is bound in the sandbox environment and the contract assertion
proceeds on the function’s result.

A property read on a contracted object has two cases depending on the presence
of a contract for the accessed property. If a contract exists, then the
contract is attached to the value after reading it from the target
$l^{\prime}$ of the proxy. Otherwise, the value is simply read from the
target. The assertion of a contract happens in the context of the included
constraint.

A property write on a contracted object continues with the operation on the
target location $l^{\prime}$ after the contract is attached to the value.
Therefore, the adherence to a contract is also checked on assignments, but the
check happens in the context of a fresh constraint that inverts the
responsibilities.

####  C.2.4. Sandbox Encapsulation

Wrap-Constant $\displaystyle\displaystyle\widehat{\rho}\leavevmode\nobreak\
\vdash\leavevmode\nobreak\ \varsigma,\sigma,c\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\ \varsigma,\sigma,c$ Wrap-Contract
$\displaystyle\displaystyle\widehat{\rho}\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma,\sigma,(\widehat{\rho}^{\prime},\mathcal{C})\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\
\varsigma,\sigma,(\widehat{\rho}^{\prime},\mathcal{C})$ Wrap-Constructor
$\displaystyle\displaystyle\widehat{\rho}\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma,\sigma,(\widehat{\rho}^{\prime},\mathcal{A})\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\
\varsigma,\sigma,(\widehat{\rho}^{\prime},\mathcal{A})$ Wrap-NonProxyObject
$\displaystyle\displaystyle{\hbox{\hskip
99.33788pt\vbox{\hbox{\hskip-99.33788pt\hbox{\hbox{$\displaystyle\displaystyle
l^{\prime}\not\in\textit{dom(}\sigma\textit{)}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\not\exists
l^{\prime\prime}\in\textit{dom(}\sigma\textit{)}:\leavevmode\nobreak\
(l,\widehat{\rho})=\sigma(l^{\prime\prime})$}}}}\vbox{}}}\over\hbox{\hskip
81.38235pt\vbox{\vbox{}\hbox{\hskip-81.38234pt\hbox{\hbox{$\displaystyle\displaystyle\widehat{\rho}\leavevmode\nobreak\
\vdash\leavevmode\nobreak\ \varsigma,\sigma[l\mapsto o],l\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\ \varsigma,\sigma[l\mapsto
o,l^{\prime}\mapsto(l,\widehat{\rho})],l^{\prime}$}}}}}}$ Wrap-Existing
$\displaystyle\displaystyle\widehat{\rho}\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma,\sigma[l^{\prime}\mapsto(l,\widehat{\rho})],l\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\ \varsigma,\sigma,l^{\prime}$ Wrap-Proxy
$\displaystyle\displaystyle\widehat{\rho}\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma,\sigma[l^{\prime}\mapsto(l,\widehat{\rho})],l^{\prime}\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\ \varsigma,\sigma,l^{\prime}$ Wrap-Contract
$\displaystyle\displaystyle{\hbox{\hskip
75.94241pt\vbox{\hbox{\hskip-75.94241pt\hbox{\hbox{$\displaystyle\displaystyle\widehat{\rho}\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma,\sigma[l\mapsto(l^{\prime},\widehat{\rho},\flat,\mathcal{Q})],l^{\prime}\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\
\varsigma,\sigma^{\prime},l^{\prime\prime}$}}}\vbox{}}}\over\hbox{\hskip
103.86964pt\vbox{\vbox{}\hbox{\hskip-103.86964pt\hbox{\hbox{$\displaystyle\displaystyle\widehat{\rho}\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma,\sigma[l\mapsto(l^{\prime},\widehat{\rho},\flat,\mathcal{Q})],l\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\
\varsigma,\sigma^{\prime}[l^{\prime\prime\prime}\mapsto(l^{\prime\prime},\widehat{\rho},\flat,\mathcal{Q})],l^{\prime\prime}$}}}}}}$
App-Sandbox $\displaystyle\displaystyle{\hbox{\hskip
136.0539pt\vbox{\hbox{\hskip-136.0539pt\hbox{\hbox{$\displaystyle\displaystyle(l^{\prime},\widehat{\rho})=\sigma(l)$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle(d,(\rho^{\prime},\lambda
x.e),v^{\prime})=\sigma(l^{\prime})$}\hskip
20.00003pt\hbox{\hskip-81.52539pt\hbox{\hbox{$\displaystyle\displaystyle\widehat{\rho}\leavevmode\nobreak\
\vdash\leavevmode\nobreak\ \varsigma,\sigma,(\lambda
x.e)(\textit{wrap}(v))\leavevmode\nobreak\ \Downarrow\leavevmode\nobreak\
\varsigma^{\prime},\sigma^{\prime},b$}}}}}}\vbox{\hbox{\hskip-81.52539pt\hbox{\hbox{$\displaystyle\displaystyle\widehat{\rho}\leavevmode\nobreak\
\vdash\leavevmode\nobreak\ \varsigma,\sigma,(\lambda
x.e)(\textit{wrap}(v))\leavevmode\nobreak\ \Downarrow\leavevmode\nobreak\
\varsigma^{\prime},\sigma^{\prime},b$}}}\vbox{}}}}\over\hbox{\hskip
53.97328pt\vbox{\vbox{}\hbox{\hskip-53.97327pt\hbox{\hbox{$\displaystyle\displaystyle\rho\leavevmode\nobreak\
\vdash\leavevmode\nobreak\ \varsigma,\sigma,l(v)\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\ \varsigma^{\prime},\sigma^{\prime},b$}}}}}}$
Get-Sandbox $\displaystyle\displaystyle{\hbox{\hskip
66.51848pt\vbox{\hbox{\hskip-66.51848pt\hbox{\hbox{$\displaystyle\displaystyle\widehat{\rho}\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma,\sigma,\textit{wrap}(l^{\prime}[c])\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\
\varsigma,\sigma^{\prime},b$}}}\vbox{}}}\over\hbox{\hskip
71.03236pt\vbox{\vbox{}\hbox{\hskip-71.03236pt\hbox{\hbox{$\displaystyle\displaystyle\rho\leavevmode\nobreak\
\vdash\leavevmode\nobreak\
\varsigma,\sigma[l\mapsto(l^{\prime},\widehat{\rho})],l[c]\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\
\varsigma,\sigma^{\prime\prime},b^{\prime}$}}}}}}$ Put-Sandbox
$\displaystyle\displaystyle\rho\leavevmode\nobreak\ \vdash\leavevmode\nobreak\
\varsigma,\sigma[l\mapsto(l^{\prime},\widehat{\rho})],l[c]\\!=\\!v\leavevmode\nobreak\
\Downarrow\leavevmode\nobreak\
\varsigma,\sigma[l\mapsto(l^{\prime},\widehat{\rho})],\bullet$ Figure 16.
Inference rules for sandbox encapsulation.

The sandbox encapsulation (Figure 16) distinguishes several cases. A primitive
value, a contract value, and a contract abstraction value is not wrapped.

To wrap a location that points to a non-proxy object, the location is packed
in a fresh proxy along with the current sandbox environment. This packaging
ensures that each further access to the wrapped location has to use the
current environment.

In case the location is already wrapped by a sandbox proxy or the location of
a sandbox proxy gets wrapped then the location to the existing proxy is
returned. This rule ensures that an object is wrapped at most once and thus
preserves object identity inside the sandbox.

If the location points to a contracted object, the wrap operation continues
with the target $l^{\prime}$, before adding all contract from the contracted
object.

The application of a wrapped function proceeds by unwrapping the function and
evaluating it in the sandbox environment contained in the proxy. The function
argument and its result are known to be wrapped in this case.

A property read on a sandboxed location continues the operation on the target
and wraps the resulting behavior. An assignment to a sandboxed object is not
allowed, thus it signals a sandbox violation.

## References

  * [1] Parker Abercrombie and Murat Karaorman.  jContractor: Design by contract for Java.  http://jcontractor.sourceforge.net/, 2003.
  * [2] Amal Ahmed, Robert Bruce Findler, Jeremy G. Siek, and Philip Wadler.  Blame for all.  In Thomas Ball and Mooly Sagiv, editors, Proceedings 38th Annual ACM Symposium on Principles of Programming Languages, pages 201–214, Austin, TX, USA, January 2011. ACM Press.
  * [3] Jean-Baptiste Arnaud, Marcus Denker, Stéphane Ducasse, Damien Pollet, Alexandre Bergel, and Mathieu Suen.  Read-only execution for dynamic languages.  In Jan Vitek, editor, Objects, Models, Components, Patterns, 48th International Conference, TOOLS 2010, Málaga, Spain, June 28 - July 2, 2010. Proceedings, volume 6141 of Lecture Notes in Computer Science, pages 117–136, Málaga, Spain, June 2010. Springer.
  * [4] Thomas H. Austin, Tim Disney, and Cormac Flanagan.  Virtual values for language extension.  In Cristina Videira Lopes and Kathleen Fisher, editors, OOPSLA, pages 921–938, Portland, OR, USA, 2011. ACM.
  * [5] Thomas Ball and Mooly Sagiv, editors.  Proceedings 38th Annual ACM Symposium on Principles of Programming Languages, Austin, TX, USA, January 2011. ACM Press.
  * [6] Franco Barbanera, Mariangiola Dezani-Ciancaglini, and Ugo de’ Liguoro.  Intersection and union types: Syntax and semantics.  Information and Computation, 119(2):202–230, 1995.
  * [7] Nuel Belnap.  A useful four-valued logic.  In J. Michael Dunn and George Epstein, editors, Modern Uses of Multiple-Valued Logic, volume 2 of Episteme, pages 5–37. Springer Netherlands, 1977.
  * [8] João Filipe Belo, Michael Greenberg, Atsushi Igarashi, and Benjamin C. Pierce.  Polymorphic contracts.  In Gilles Barthe, editor, Proceedings of the 20th European Symposium on Programming, volume 6602 of Lecture Notes in Computer Science, pages 18–37, Saarbrücken, Germany, March 2011. Springer-Verlag.
  * [9] Matthias Blume and David McAllester.  Sound and complete models of contracts.  Journal of Functional Programming, 16:375–414, July 2006.
  * [10] Gilad Bracha and David Ungar.  Mirrors: Design principles for meta-level facilities of object-oriented programming languages.  In John M. Vlissides and Douglas C. Schmidt, editors, OOPSLA, pages 331–344. ACM, 2004.
  * [11] Lorenzo Caminiti.  Contract++, contract programming library for C++.  http://sourceforge.net/projects/contractpp/, August 2012.
  * [12] Giuseppe Castagna, Nils Gesbert, and Luca Padovani.  A theory of contracts for Web services.  ACM Transactions on Programming Languages and Systems, 31(5), 2009\.
  * [13] Arthur Charguéraud.  Pretty-big-step semantics.  In Matthias Felleisen and Philippa Gardner, editors, ESOP, volume 7792 of Lecture Notes in Computer Science, pages 41–60, Rome, Italy, March 2013. Springer.
  * [14] Olaf Chitil.  Practical typed lazy contracts.  In Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming (ICFP 2012). ACM, September 2012.
  * [15] Mario Coppo and M. Dezani-Ciancaglini.  A new type-assignment for $\lambda$-terms.  Archiv. Math. Logik, 19(139-156), 1978.
  * [16] Christos Dimoulas and Matthias Felleisen.  On contract satisfaction in a higher-order world.  ACM Transactions on Programming Languages and Systems, 33(5):16, 2011.
  * [17] Christos Dimoulas, Robert Bruce Findler, Cormac Flanagan, and Matthias Felleisen.  Correct blame for contracts: No more scapegoating.  In Thomas Ball and Mooly Sagiv, editors, Proceedings 38th Annual ACM Symposium on Principles of Programming Languages, pages 215–226, Austin, TX, USA, January 2011. ACM Press.
  * [18] Christos Dimoulas, Riccardo Pucella, and Matthias Felleisen.  Future contracts.  In António Porto and Francisco J. López-Fraguas, editors, Principles and Practice of Declarative Programming, PPDP 2009, pages 195–206, Coimbra, Portugal, September 2009. ACM.
  * [19] Christos Dimoulas, Sam Tobin-Hochstadt, and Matthias Felleisen.  Complete monitors for behavioral contracts.  In European Symposium on Programming, volume 7211 of Lecture Notes in Computer Science, Tallinn, Estland, April 2012. Springer-Verlag.
  * [20] Tim Disney.  contracts.js.  https://github.com/disnet/contracts.js, April 2013.
  * [21] Tim Disney, Nathan Faubion, David Herman, and Cormac Flanagan.  Sweeten your JavaScript: Hygienic macros for ES5.  In Andrew P. Black and Laurence Tratt, editors, DLS, pages 35–44, Portland, OR, USA, October 2014. ACM.
  * [22] Tim Disney, Cormac Flanagan, and Jay McCarthy.  Temporal higher-order contracts.  In Olivier Danvy, editor, Proceedings International Conference on Functional Programming 2011, pages 176–188, Tokyo, Japan, September 2011\. ACM Press, New York.
  * [23] ECMAScript Language Specification, December 2009.  ECMA International, ECMA-262, 5th edition.
  * [24] Manuel Fähndrich, Michael Barnett, and Francesco Logozzo.  Embedded contract languages.  In Sung Y. Shin, Sascha Ossowski, Michael Schumacher, Mathew J. Palakal, and Chih-Cheng Hung, editors, Proceedings of the 2010 ACM Symposium on Applied Computing, pages 2103–2110, Sierre, Switzerland, 2010. ACM.
  * [25] Matthias Felleisen and Philippa Gardner, editors.  Programming Languages and Systems - 22nd European Symposium on Programming, ESOP 2013, volume 7792 of Lecture Notes in Computer Science, Rome, Italy, March 2013. Springer.
  * [26] Robert Bruce Findler and Matthias Blume.  Contracts as pairs of projections.  In Philip Wadler and Masami Hagiya, editors, Proceedings of the 8th International Symposium on Functional and Logic Programming FLOPS 2006, pages 226–241, Fuji Susono, Japan, April 2006. Springer-Verlag.
  * [27] Robert Bruce Findler and Matthias Felleisen.  Contracts for higher-order functions.  In Simon Peyton-Jones, editor, Proceedings International Conference on Functional Programming 2002, pages 48–59, Pittsburgh, PA, USA, October 2002. ACM Press, New York.
  * [28] Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, and Raymie Stata.  Extended static checking for Java.  In Proceedings of the 2002 Conference on Programming Language Design and Implementation, pages 234–245, Berlin, Germany, June 2002. ACM Press.
  * [29] Matthew Flatt, Robert Bruce Findler, and PLT.  The Racket Guide, v.6.0 edition, March 2014.  http://docs.racket-lang.org/guide/index.html.
  * [30] Joseph A. Goguen and José Meseguer.  Security policies and security models.  In IEEE Symposium on Security and Privacy, pages 11–20, 1982.
  * [31] google-caja: A source-to-source translator for securing JavaScript-based web content.  http://code.google.com/p/google-caja/, (as of 2011).
  * [32] Michael Greenberg, Benjamin C. Pierce, and Stephanie Weirich.  Contracts made manifest.  In Proceedings 37th Annual ACM Symposium on Principles of Programming Languages, pages 353–364, Madrid, Spain, January 2010. ACM Press.
  * [33] Arjun Guha, Claudiu Saftoiu, and Shriram Krishnamurthi.  The essence of javascript.  In Theo D’Hondt, editor, ECOOP, volume 6183 of Lecture Notes in Computer Science, pages 126–150, Maribor, Slovenia, June 2010. Springer.
  * [34] David R. Hanson and Todd A. Proebsting.  Dynamic variables.  In Proceedings of the 2001 Conference on Programming Language Design and Implementation, pages 264–273, Snowbird, UT, USA, June 2001. ACM Press, New York, USA.
  * [35] Phillip Heidegger, Annette Bieniusa, and Peter Thiemann.  Access permission contracts for scripting languages.  In John Field and Michael Hicks, editors, Proceedings 39th Annual ACM Symposium on Principles of Programming Languages, pages 111–122, Philadelphia, USA, January 2012. ACM Press.
  * [36] Richard Helm, Ian M. Holland, and Dipayan Gangopadhyay.  Contracts: specifying behavioral compositions in object-oriented systems.  In Norman K. Meyrowitz, editor, Conference Object Oriented Programming, Systems, Languages, and Applications / European Conference on Object-Oriented Programming, pages 169–180, Ottawa, Canada, October 1990.
  * [37] Ralf Hinze, Johan Jeuring, and Andres Löh.  Typed contracts for functional programming.  In Philip Wadler and Masami Hagiya, editors, Proceedings of the 8th International Symposium on Functional and Logic Programming FLOPS 2006, pages 208–225, Fuji Susono, Japan, April 2006. Springer-Verlag.
  * [38] Matthias Keil, Sankha Narayan Guria, Andreas Schlegel, Manuel Geffken, and Peter Thiemann.  Transparent object proxies for JavaScript.  In John Boyland, editor, ECOOP, volume ? of Lecture Notes in Computer Science, Prague, Czech Repulic, July 2015. Springer.  to appear.
  * [39] Matthias Keil and Peter Thiemann.  Efficient dynamic access analysis using JavaScript proxies.  In Proceedings of the 9th Symposium on Dynamic Languages, DLS ’13, pages 49–60, New York, NY, USA, 2013. ACM.
  * [40] Reto Kramer.  iContract — the Java design by contract tool.  In Proceedings of the Technology of Object-Oriented Languages and Systems, pages 295–307, Santa Barbara, CA, USA, 1998. IEEE Computer Society.
  * [41] Gary T. Leavens, Albert L. Baker, and Clyde Ruby.  JML: A notation for detailed design.  In Haim Kilov, Bernhard Rumpe, and Ian Simmonds, editors, Behavioral Specifications of Businesses and Systems, pages 175–188, Norwell, MA, USA, 1999. Kluwer Academic Publishers.
  * [42] Gary T. Leavens and Matthew B. Dwyer, editors.  Proceedings of the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2012, part of SPLASH 2012, Tucson, AZ, USA, October 21-25, 2012. ACM, 2012.
  * [43] Zoran Majkic.  Many-valued intuitionistic implication and inference closure in a bilattice-based logic.  In ISMVL, pages 214–220. IEEE Computer Society, 2005.
  * [44] Bertrand Meyer.  Object-Oriented Software Construction.  Prentice-Hall, 1988.
  * [45] Mark S. Miller, Tom Van Cutsem, and Bill Tulloh.  Distributed electronic rights in JavaScript.  In Matthias Felleisen and Philippa Gardner, editors, ESOP, volume 7792 of Lecture Notes in Computer Science, pages 1–20, Rome, Italy, March 2013. Springer.
  * [46] Mark S. Miller, Mike Samuel, Ben Laurie, Ihab Awad, and Mike Stay.  Caja: Safe active content in sanitized JavaScript.  http://google-caja.googlecode.com, 2008.  Google White Paper.
  * [47] Mark Samuel Miller.  Robust Composition: Towards a Unified Approach to Access Control and Concurrency Control.  PhD thesis, Johns Hopkins University, Baltimore, MD, USA, 2006.  AAI3245526.
  * [48] John C. Reynolds.  Gedanken - a simple typeless language based on the principle of completeness and the reference concept.  Commun. ACM, 13(5):308–319, 1970.
  * [49] T. Stephen Strickland, Sam Tobin-Hochstadt, Robert Bruce Findler, and Matthew Flatt.  Chaperones and impersonators: Run-time support for reasonable interposition.  In Gary T. Leavens and Matthew B. Dwyer, editors, OOPSLA, pages 943–962. ACM, 2012.
  * [50] Sam Tobin-Hochstadt and David Van Horn.  Higher-order symbolic execution via contracts.  In Gary T. Leavens and Matthew B. Dwyer, editors, OOPSLA, pages 537–554. ACM, 2012.
  * [51] Jesse A. Tov and Riccardo Pucella.  Stateful contracts for affine types.  In Andrew D. Gordon, editor, ESOP 2010, volume 6012 of Lecture Notes in Computer Science, pages 550–569. Springer-Verlag, 2010.
  * [52] Tom Van Cutsem and Mark S. Miller.  Proxies: Design principles for robust object-oriented intercession APIs.  In William D. Clinger, editor, DLS, pages 59–72. ACM, 2010.
  * [53] Tom Van Cutsem and Mark S. Miller.  Trustworthy proxies - virtualizing objects with invariants.  In Giuseppe Castagna, editor, ECOOP, volume 7920 of Lecture Notes in Computer Science, pages 154–178, Montpellier, France, July 2013\. Springer.
  * [54] Philip Wadler and Robert Bruce Findler.  Well-typed programs can’t be blamed.  In Proceedings 18th European Symposium on Programming, volume 5502 of Lecture Notes in Computer Science, pages 1–16, York, UK, March 2009\. Springer.
  * [55] Philip Wadler and Masami Hagiya, editors.  Proceedings of the 8th International Symposium on Functional and Logic Programming FLOPS 2006, Fuji Susono, Japan, April 2006. Springer-Verlag.
  * [56] Dana N. Xu, Simon L. Peyton Jones, and Koen Claessen.  Static contract checking for Haskell.  In Benjamin Pierce, editor, Proceedings 36th Annual ACM Symposium on Principles of Programming Languages, pages 41–52, Savannah, GA, USA, January 2009. ACM Press.