## D.2 Instantiation Rule Soundness

We prove the following technical lemma, which allows to extend an $\mathcal{E}$-interpretation $\rho$ into an $(\mathcal{E}, \text{module } x = \text{abs}_{\text{open}} : M_I)$-interpretation $\rho' = \rho$, $(x \mapsto m)$. This is possible whenever:

i) $m$ has type erase<sub>compl</sub>(M<sub>I</sub>);

ii) and we can show that $m$ verifies $M_I$'s complexity restriction by proving that:

$$ \forall f \in \text{procs}(M_I), \quad \mathcal{E}, \text{ module } \vec{x} = \text{abs}_{\text{open}} : \vec{M} \vdash \{\tau\} m(\vec{x}).f \{\tau \mid t_f\} $$

where $\vec{x}$ are $M_I$'s functor parameters, and $\vec{M}$ their types.

LEMMA D.3. Let $\mathcal{E}$ be a well-typed environment, $M_I$ be low-order module signature s.t.:

$$ M_I = \text{func}(\vec{x} : \vec{M}) \text{ sig\_restr } \theta \text{ end} $$

and $m$ be a module expression s.t. $\mathcal{E} \vdash_X m : \text{erase}_{\text{compl}}(M_I)$. Let $\mathcal{E}_a = \mathcal{E}$, module $x = \text{abs}_{\text{open}} : M_I$ and $\rho$ be an $\mathcal{E}$-interpretation. If, for every $f \in \text{procs}(M_I)$, we have:

$$ \mathcal{E}, \text{ module } \vec{x} = \text{abs}_{\text{open}} : \vec{M} \vdash \{\tau\} m(\vec{x}).f \{\tau \mid t_f\} \wedge t_f \leq_{\text{compl}} \theta[f] \quad (15) $$

then $\rho_a = \rho$, $(x \mapsto m)$ is an $\mathcal{E}_a$-interpretation. Moreover, for any $f \in \text{procs}(M_I)$:

$$ \text{compl}_{x.f}^{\mathcal{E}_a, \rho_a} \leq t_f[\text{conc}] + \sum_{\substack{\Lambda \in \text{abs}(\mathcal{E}) \\ h \in \text{procs}_{\mathcal{E}}(\Lambda)}} t_f[\Lambda.h] \cdot \text{compl}_{A.h}^{\mathcal{E}, \rho} \quad (16) $$

PROOF. Let $\vec{m}$ be an evaluation of $x$'s parameters s.t. for every $1 \le i \le |\vec{x}|$, if we let $x_i = \vec{x}[i]$, $m_i = \vec{m}[i]$ and $M_i = \vec{M}[i] = \text{sig\_restr } \lambda_c^i \wedge \text{end}$:

$$ \mathcal{E} \vdash (\text{module } x_i = m_i : \text{erase}_{\text{compl}}(M_i)) $$

and:

$$ \forall g \in \text{procs}(M_i), \text{cost}_{\nu}^{\mathcal{E}}(m_i.g) \le \lambda_c^i $$

Let $\mathcal{E}'_a = \mathcal{E}_a$; module $\vec{x} = \text{abs}_{\text{open}} : \vec{M}$ and $\rho'_a = \rho_a$, $(\vec{x} : \vec{m})$. Also, let $y \in \vec{x}$ and $g \in \text{procs}(\vec{M}[y])$. To prove that $\rho_a$ is an $\mathcal{E}_a$-interpretation, we only need to prove that:

$$ \#\text{calls}_{y.g}^{\mathcal{E}'_a, \rho'_a}(x(\vec{x}).f) \le \theta[f][y.g] \quad (17) $$

and that:

$$ \text{i-cost}^{\mathcal{E}'_a, \rho'_a, \vec{x}}(x(\vec{x}).f) \le \theta[f][\text{intr}] \quad (18) $$

Restriction to module structures. First, note that w.l.o.g. we can assume that $\vec{m}$ are all module structure (i.e. of the form struct \_end). Basically, we show that we can build another interpretation $\rho''_a$ extending $\rho_a$ which satisfies the same hypotheses than $\rho'_a$, and such that for every $z \in \vec{x}$, $\rho''_a(z)$ is a module structure such that, for every $g \in \text{procs}(\vec{M}[z])$:

$$ \#\text{calls}_{z.g}^{\mathcal{E}'_a, \rho'_a}(x(\vec{x}).f) = \#\text{calls}_{z.g}^{\mathcal{E}'_a, \rho''_a}(x(\vec{x}).f) $$

and:

$$ \text{i-cost}^{\mathcal{E}'_a, \rho'_a, \vec{x}}(x(\vec{x}).f) = \text{i-cost}^{\mathcal{E}'_a, \rho''_a, \vec{x}}(x(\vec{x}).f) $$

Indeed, assume that there exists some $y \in \vec{x}$ such that $\vec{m}[y]$ is not a module structure in $\rho'_a$. If $\vec{m}[y]$ is a module path p in $\rho'_a$, then we resolve it in $\mathcal{E}$, $\rho$ (which is always possible, since $\vec{m}[y]$ is well-typed in $\mathcal{E}$ and $\rho$ is an $\mathcal{E}$-interpretation) until we get a module structure struct st end, and replace y by struct st end in $\rho''_a$. Finally, $\vec{m}[y]$ cannot be a functor (by typing hypothesis) in $\rho'_a$. We repeat the steps above until $(\rho'_a)[\vec{x}]$ are all module structures.
Proof of Equ. (17). Since $\rho'_a(x) = m$ and $m$ is well-typed in $\mathcal{E}$, and since the module expressions $\vec{m}$ are well-typed in $\mathcal{E}$, we can remove $x$ from the environment and the interpretation while keeping the semantics unchanged. That is, we have:

$$ \#\text{calls}_{\vec{y},g}^{\mathcal{E}'_a, \rho'_a}(\vec{x}).f) = \#\text{calls}_{\vec{y},g}^{\mathcal{E}', \rho'}(\vec{m}).f) \quad (19) $$

where:

$\mathcal{E}' = \mathcal{E}$; module $\vec{x} = \text{abs}_{\text{open}} : \vec{M}$ and $\rho' = \rho, (\vec{x} : \vec{m})$

Since $\mathcal{E}$ is well-typed, and $\vec{m}$ have types $\vec{M}$ in $\mathcal{E}$, and since $\vec{M}$ is not a functor type, we can check that $\mathcal{E}'$ is well-typed, and $\rho'$ is an $\mathcal{E}'$-interpretation. Using Equ. (15), we get:

$$ \forall v, \text{cost}_{\vec{v}}^{\mathcal{E}', \rho'}(\vec{m}).f) \le t_f[\text{conc}] + \sum_{\substack{A \in \text{abs}(\mathcal{E}') \\ h \in \text{procs}_{\mathcal{E}'}(A)}} t_f[\text{A.h}] \cdot \text{compl}_{A.h}^{\mathcal{E}', \rho'} \quad (20) $$

Let $N > 0$ be an non-zero positive integer. We are going to change the interpretation of $y$ in $\rho'$ by adding some code doing nothing and taking time $N$. Let $\text{st}_y$ be such that $\rho'(y) = \text{struct st}_y$ end. By typing hypothesis, we know that $\text{st}_y$ is of the shape:

$$ \text{st}_y = \text{st}_1; \text{proc } g(\vec{v} : \vec{\tau}) \to \tau_r = \{ \text{var } (\vec{v}_1 : \vec{\tau}_1); s_g; \text{return } e_g \}; \text{st}_2 $$

Then, we let $\text{st}_y^N$ be the module structure:

$$ \text{st}_1; \text{proc } g(\vec{v} : \vec{\tau}) \to \tau_r = \{ \text{var } (\vec{v}_1 : \vec{\tau}_1); (\text{tic}^N; s_g); \text{return } e_g \}; \text{st}_2 $$

and let $\rho'_N$ be the interpretation with the same domain as $\rho'$ s.t.:

$$ \forall w \in \text{dom}(\rho'), \rho'_N(w) = \begin{cases} \rho'(w) & \text{if } w \neq y \\ \text{struct st}_y^N \text{ end} & \text{if } w = y \end{cases} $$

Let $v$ be some arbitrary memory. Since $\rho'$ is an $\mathcal{E}'$-interpretation, then so is $\rho'_N$. Using Equ. (15), we get:

$$ \text{cost}_{\vec{v}}^{\mathcal{E}', \rho'_N}(\vec{m}).f) \le t_f[\text{conc}] + \sum_{\substack{A \in \text{abs}(\mathcal{E}') \\ h \in \text{procs}_{\mathcal{E}'}(A)}} t_f[\text{A.h}] \cdot \text{compl}_{A.h}^{\mathcal{E}', \rho'_N} \quad (21) $$

Moreover, we can easily check that:

$$ \#\text{calls}_{\vec{y},g}^{\mathcal{E}', \rho'}(\vec{m}).f) = \#\text{calls}_{\vec{y},g}^{\mathcal{E}', \rho'_N}(\vec{m}).f) $$

and:

$$ \text{cost}_{\vec{v}}^{\mathcal{E}', \rho'_N}(\vec{m}).f) = \text{cost}_{\vec{v}}^{\mathcal{E}', \rho'}(\vec{m}).f) + N \cdot \#\text{calls}_{\vec{y},g}^{\mathcal{E}', \rho'}(\vec{m}).f) $$

From Equ. (21), we have:

$$ \text{cost}_{\vec{v}}^{\mathcal{E}', \rho'}(\vec{m}).f) + N \cdot \#\text{calls}_{\vec{y},g}^{\mathcal{E}', \rho'}(\vec{m}).f) \le t_f[\text{conc}] + \sum_{\substack{A \in \text{abs}(\mathcal{E}') \\ h \in \text{procs}_{\mathcal{E}'}(A)}} t_f[\text{A.h}] \cdot \text{compl}_{A.h}^{\mathcal{E}', \rho'_N} $$
Using the inequality above, and Equ. (20), we have:

$$
\begin{align*}
& N \cdot \#\text{calls}_{y.g}^{\mathcal{E}', \rho'}(m(\vec{x}).f) \\
\le {} & \sum_{\substack{A \in \text{abs}(\mathcal{E}') \\ h \in \text{procs}_{\mathcal{E}'}(A)}} t_f[A.h] \cdot (\text{compl}_{A.h}^{\mathcal{E}', \rho'_N} - \text{compl}_{A.h}^{\mathcal{E}', \rho'}) \\
\le {} & t_f[y.g] \cdot (\text{compl}_{y.g}^{\mathcal{E}', \rho'_N} - \text{compl}_{y.g}^{\mathcal{E}', \rho'}) \quad (\text{Since } \forall z \neq y, \rho'_N(z) = \rho'(z)) \\
\le {} & t_f[y.g] \cdot N
\end{align*}
$$

We deduce that $\#\text{calls}_{y.g}^{\mathcal{E}', \rho'}(m(\vec{x}).f) \le t_f[y.g]$. From Equ. (15), we get that:

$$
\#\text{calls}_{y.g}^{\mathcal{E}', \rho'}(m(\vec{x}).f) \le \theta[f][y.g]
$$

This, together with Equ. (19), proves Equ. (17)

Finally, to prove that Equ. (18) and Equ. 16 hold we do the exactly the same reasoning, this time
by adding to the interpretation of x some code doing nothing and taking time N.
□

We also prove the following weakening lemma for the intrinsic complexity of a procedure.

LEMMA D.4. For every well-typed environment $\mathcal{E}$, if:

$$
\mathcal{E} = \mathcal{E}_1; \mathcal{E}_2 \quad \text{where} \quad \mathcal{E}_1 = \mathcal{E}_0; \text{module } x = \text{abs}_{\text{open}} : \mathcal{M}_1
$$

and $\mathcal{E}_2$ contains only module declarations. Then for every $f \in \text{procs}(\mathcal{M}_1)$ and $\mathcal{E}$-interpretation $\rho$, we
have $\text{compl}_{x.f}^{\mathcal{E}, \rho} = \text{compl}_{x.f}^{\mathcal{E}_1, \rho_1}$ where $\rho_1$ is the restriction of $\rho$ to $\mathcal{E}_1$'s abstract modules.

PROOF SKETCH. Assume $M_I = (\text{func}(\vec{x} : \vec{M}) \ \text{sig} \ \text{end})$. Let $\mathcal{E}' = (\mathcal{E}, \text{module } \vec{x} = \text{abs}_{\text{open}} : \vec{M})$ and $\mathcal{E}'_1 = (\mathcal{E}_1, \text{module } \vec{x} = \text{abs}_{\text{open}} : \vec{M})$, we prove that $\text{compl}_{x.f}^{\mathcal{E}, \rho} \le \text{compl}_{x.f}^{\mathcal{E}_1, \rho_1}$ and $\text{compl}_{x.f}^{\mathcal{E}, \rho} \ge \text{compl}_{x.f}^{\mathcal{E}_1, \rho_1}$.

The latter inequality is straightforward to show, since any $\mathcal{E}'_1$-interpretation $\rho_1$ can be extended
into an $\mathcal{E}'$-interpretation $\rho$ that leaves the intrinsic cost of x unchanged, i.e. such that for any $v$:

$$
\text{i-cost}_{v}^{\mathcal{E}', \rho', \vec{x}}(x(\vec{x}).f) = \text{i-cost}_{v}^{\mathcal{E}', \rho', \vec{x}}(x(\vec{x}).f)
$$

To prove the former inequality, we show that any $\mathcal{E}'$-interpretation $\rho$ can be transformed into an
$\mathcal{E}'_1$-interpretation $\rho'$ such that Equ. (D.2) holds, by inlining all modules of $\mathcal{E}_2$ in $\rho$. We omit the
details.
\hfill $\square$

LEMMA D.5. The rule INSTANTIATION given in Fig. 13 is sound.

PROOF. We consider an instance of the rule INSTANTIATION. We want to prove that:

$$
\mathcal{E}, \text{module } x = m : M_I \vdash \{\phi\} s \{\psi \mid T_{\text{ins}}\}
$$

Let $\mathcal{E}_c = (\mathcal{E}, \text{module } x = m : M_I)$ and $\mathcal{E}_a = (\mathcal{E}, \text{module } x = \text{abs}_{\text{open}} : M_I)$. We know that:

$$
M_I = \text{func}(\vec{y} : \vec{M}) \ \text{sig} \ S_I \ \text{restr} \ \theta \ \text{end} \qquad \mathcal{E} \vdash_x m : \text{erase}_{\text{compl}}(M_I)
$$

Let $\rho$ be an $\mathcal{E}_c$-interpretation and $v \in \phi$, we need to show that for every memory $v$:

$$
\mathrm{supp}(\pi_1^{\#}(\llbracket s \rrbracket_{v}^{\mathcal{E}_c, \rho})) \subseteq \psi \qquad (22)
$$

$$
\text{cost}_{v}^{\mathcal{E}_c, \rho}(s) \le T_{\text{ins}}[\text{conc}] + \sum_{\substack{A \in \text{abs}(\mathcal{E}_c) \\ g \in \text{procs}_{\mathcal{E}_c}(A)}} T_{\text{ins}}[A.g] \cdot \text{compl}_{A.g}^{\mathcal{E}_c, \rho} \quad (23)
$$
We know that $M_I = \text{func}(\vec{y} : \vec{M}) \text{ sig } S_I \text{ restr } \theta$ end and:

$$ \mathcal{E}_a \vdash \{\phi\} s \{\psi \mid t_s\} \qquad (24) $$

Using Lemma D.3, we know that $\rho_a = \rho$, $(x \mapsto m)$ is an $\mathcal{E}_a$-interpretation. Hence, using Equ. (24), we deduce that:

$$ \text{supp}(\pi_1^{\#}(\llbracket s \rrbracket_{\nu}^{\mathcal{E}_a, \rho_a})) \subseteq \psi \qquad (25) $$

$$ \text{cost}_{\nu}^{\mathcal{E}_a, \rho_a}(s) \le t_s[\text{conc}] + \sum_{\substack{A \in \text{abs}(\mathcal{E}_a) \\ g \in \text{procs}_{\mathcal{E}_a}(A)}} t_s[\text{A.g}] \cdot \text{compl}_{A.g}^{\mathcal{E}_a, \rho_a} \qquad (26) $$

Using the fact that $\rho_a(x) = m$, we can check (by induction over $\#\text{size}_{\mathcal{E}_a}^{\rho_a}(s)$) that:

$$ \llbracket s \rrbracket_{\nu}^{\mathcal{E}_a, \rho_a} = \llbracket s \rrbracket_{\nu}^{\mathcal{E}_c, \rho} \quad \text{and} \quad \text{cost}_{\nu}^{\mathcal{E}_a, \rho_a}(s) = \text{cost}_{\nu}^{\mathcal{E}_c, \rho}(s) $$

From the left equality above and Equ. (25), we know that Equ. (22) holds. It remains to prove Equ. (23).

From the right equality above and Equ. (26):

$$ \begin{aligned} \text{cost}_{\nu}^{\mathcal{E}_c, \rho}(s) &\le t_s[\text{conc}] + \sum_{\substack{A \in \text{abs}(\mathcal{E}_a) \\ g \in \text{procs}_{\mathcal{E}_a}(A)}} t_s[\text{A.g}] \cdot \text{compl}_{A.g}^{\mathcal{E}_a, \rho_a} \\ &\le t_s[\text{conc}] + \sum_{f \in \text{procs}(S_I)} t_s[\text{x.f}] \cdot \text{compl}_{\text{x.f}}^{\mathcal{E}_a, \rho_a} \\ &\quad + \sum_{\substack{A \in \text{abs}(\mathcal{E}_c) \\ g \in \text{procs}_{\mathcal{E}_c}(A)}} t_s[\text{A.g}] \cdot \text{compl}_{A.g}^{\mathcal{E}_a, \rho_a} \end{aligned} $$

We replace $\text{compl}_{A.g}^{\mathcal{E}_a, \rho_a}$ by $\text{compl}_{A.g}^{\mathcal{E}_c, \rho}$ for every $A \in \text{abs}(\mathcal{E}_c)$ and $g \in \text{procs}_{\mathcal{E}_c}(A)$ using Lemma D.4:

$$ \text{cost}_{\nu}^{\mathcal{E}_c, \rho}(s) \le t_s[\text{conc}] + \sum_{f \in \text{procs}(S_I)} t_s[\text{x.f}] \cdot \text{compl}_{\text{x.f}}^{\mathcal{E}_a, \rho_a} + \sum_{\substack{A \in \text{abs}(\mathcal{E}_c) \\ g \in \text{procs}_{\mathcal{E}_c}(A)}} t_s[\text{A.g}] \cdot \text{compl}_{A.g}^{\mathcal{E}_c, \rho} \qquad (27) $$

Using Lemma D.3, we upper-bound $\text{compl}_{\text{x.f}}^{\mathcal{E}_a, \rho_a}$ for every $f \in \text{procs}(S_I)$:

$$ \text{compl}_{\text{x.f}}^{\mathcal{E}_a, \rho_a} \le t_f[\text{conc}] + \sum_{\substack{A \in \text{abs}(\mathcal{E}_c) \\ g \in \text{procs}_{\mathcal{E}_c}(A)}} t_f[\text{A.g}] \cdot \text{compl}_{A.g}^{\mathcal{E}_a, \rho} $$

We check that the quantities above are identical when evaluated in $\mathcal{E}_c$, hence:

$$ \text{compl}_{\text{x.f}}^{\mathcal{E}_a, \rho_a} \le t_f[\text{conc}] + \sum_{\substack{A \in \text{abs}(\mathcal{E}_c) \\ g \in \text{procs}_{\mathcal{E}_c}(A)}} t_f[\text{A.g}] \cdot \text{compl}_{A.g}^{\mathcal{E}_a, \rho} $$

Hence, re-organizing the terms in the sum in Equ. (27):

$$ \text{cost}_{\nu}^{\mathcal{E}_c, \rho}(s) \le t_s[\text{conc}] + \sum_{f \in \text{procs}(S_I)} t_s[\text{x.f}] \cdot t_f[\text{conc}] + \sum_{\substack{A \in \text{abs}(\mathcal{E}_c) \\ g \in \text{procs}_{\mathcal{E}_c}(A)}} (t_s[\text{A.g}] + \sum_{f \in \text{procs}(S_I)} t_s[\text{x.f}] \cdot t_f[\text{A.g}]) \cdot \text{compl}_{A.g}^{\mathcal{E}_c, \rho} $$

Which, by definition of $T_{\text{ins}}$, is exactly Equ. (23). □