Resource-Guided Program Synthesis

TL;DR

This paper introduces resource-guided synthesis, a type-based approach that efficiently generates recursive programs satisfying functional specifications and resource bounds, demonstrated by a tool that produces more efficient and secure code.

Contribution

It presents a novel type system combining polymorphic refinement types with amortized resource analysis for guiding program synthesis.

Findings

ReSyn synthesizes more efficient recursive programs.

ReSyn is faster than naive synthesis combined with resource analysis.

ReSyn can generate constant-resource implementations for security.

Abstract

This article presents resource-guided synthesis, a technique for synthesizing recursive programs that satisfy both a functional specification and a symbolic resource bound. The technique is type-directed and rests upon a novel type system that combines polymorphic refinement types with potential annotations of automatic amortized resource analysis. The type system enables efficient constraint-based type checking and can express precise refinement-based resource bounds. The proof of type soundness shows that synthesized programs are correct by construction. By tightly integrating program exploration and type checking, the synthesizer can leverage the user-provided resource bound to guide the search, eagerly rejecting incomplete programs that consume too many resources. An implementation in the resource-guided synthesizer ReSyn is used to evaluate the technique on a range of recursive data structure manipulations. The experiments show that ReSyn synthesizes programs that are asymptotically more efficient than those generated by a resource-agnostic synthesizer. Moreover, synthesis with ReSyn is faster than a naive combination of synthesis and resource analysis. ReSyn is also able to generate implementations that have a constant resource consumption for fixed input sizes, which can be used to mitigate side-channel attacks.

Tables

Table 1. Table 1. Comparison of ReSyn and Synquid . For each benchmark, we report the set of provided Components ; cumulative size of synthesized Code (in AST nodes) for all goals; as well as running times (in seconds) for ReSyn ( Time ) and Synquid ( TimeNR ).

Group	Description	Components	Code	Time	TimeNR
List	is empty	true, false	16	$0.20$	$0.16$
	member	true, false, $=$, $\ne$	41	$0.24$	$0.21$
	duplicate each element		39	$0.52$	$0.27$
	replicate	0, inc, dec, $\le$, $\ne$	31	$2.88$	$0.23$
	append two lists		38	$1.54$	$0.48$
	take first $n$ elements	0, inc, dec, $\le$, $\ne$	34	$2.42$	$0.17$
	drop first $n$ elements	0, inc, dec, $\le$, $\ne$	30	$20.37$	$0.32$
	concat list of lists	append	49	$3.34$	$0.81$
	delete value	$=$, $\ne$	49	$0.77$	$0.31$
	zip		32	$0.43$	$0.22$
	zip with		35	$0.45$	$0.24$
	$i$-th element	0, inc, dec, $\le$, $\ne$	30	$0.30$	$0.23$
	index of element	0, inc, dec, $=$, $\ne$	43	$0.54$	$0.29$
	insert at end		42	$0.43$	$0.32$
	balanced split	fst, snd, abs	64	$9.62$	$1.73$
	reverse	insert at end	35	$0.44$	$0.32$
	insert (sorted)	$\le$, $\ne$	57	$1.98$	$0.69$
	extract minimum	$\le$, $\ne$	71	$18.14$	$8.31$
	foldr		43	$1.78$	$0.60$
	length using fold	0, inc, dec	39	$0.27$	$0.21$
	append using fold		42	$0.32$	$0.26$
	map		27	$0.28$	$0.19$
Unique list	insert	$=$, $\ne$	49	$0.83$	$0.44$
	delete	$=$, $\ne$	45	$0.53$	$0.34$
	compress	$=$, $\ne$	64	$4.98$	$1.85$
	integer range	0, inc, dec, $\le$, $\ne$	46	$88.35$	$5.14$
	partition	$\le$	71	$13.04$	$5.46$
Sorted list	insert		64	$1.62$	$0.57$
	delete		52	$0.47$	$0.30$
	intersect		71	$17.01$	$0.76$
Tree	node count	0, 1, +	34	$3.84$	$0.52$
	preorder	append	45	$3.03$	$0.55$
	to list	append	45	$2.99$	$0.54$
	member	false, not, or, $=$	63	$2.17$	$0.60$
BST	member	true, false, $\le$, $\ne$	72	$0.50$	$0.32$
	insert	$\le$, $\ne$	90	$4.49$	$1.55$
	delete	$\le$, $\ne$	103	$26.77$	$9.25$
	BST sort	$\le$, $\ne$	191	$8.97$	$4.27$
Binary Heap	insert	$\le$, $\ne$	90	$3.21$	$1.03$
	member	false, not, or, $\le$, $\ne$	78	$2.34$	$0.84$
	1-element constructor	$\le$, $\ne$	44	$0.21$	$0.21$
	2-element constructor	$\le$, $\ne$	91	$0.67$	$0.34$
	3-element constructor	$\le$, $\ne$	274	$21.35$	$4.02$

Table 2. Table 2. Case Studies. For each synthesis problem, we report: the run time of ReSyn ( T ), Synquid ( T-NR ), naive combination of Synquid and resource analysis ( T-EAC ), ReSyn without incremental solving ( T-NInc ); as well as the tightest resource bound for the code generated by ReSyn ( B ) and by Synquid ( B-NR ). Here, S ​ L 𝑆 𝐿 SL is the type of sorted lists, and C ​ L 𝐶 𝐿 CL refers to the type of lists without adjacent duplicates. TO is 10 min; all benchmarks count recursive calls.

	Description	Type Signature	Components	T	T-NR	T-EAC	T-NInc	B	B-NR
1	triple	$\forall \alpha .xs:L\left({\alpha }^2\right)\to \{L\left(\alpha \right)\mid \text{len}\nu =\text{len}xs+\text{len}xs+\text{len}xs\}$	append	$0.88$	$0.36$	$0.42$	-	$\mid xs\mid$	$\mid xs\mid$
2	triple’	$\forall \alpha .xs:L\left({\alpha }^2\right)\to \{L\left(\alpha \right)\mid \text{len}\nu =\text{len}xs+\text{len}xs+\text{len}xs\}$	append’	$2.80$	$0.40$	$1.22$	-	$\mid xs\mid$	${\mid xs\mid }^2$
3	concat list of lists	$\forall \alpha .xxs:L\left(L\left({\alpha }^1\right)\right)\to acc:L\left(\alpha \right)\to \{L\left(\alpha \right)\mid \text{sumLen}xs=\text{len}\nu \}$	append	$3.21$	$0.86$	$1.10$	-	$\mid xxs\mid$	${\mid xxs\mid }^2$
4	compress	$\forall \alpha .xs:L\left({\alpha }^1\right)\to \{CL\left(\alpha \right)\mid \text{elems}xs=\text{elems}\nu \}$	$=$,$\ne$	$3.82$	$1.10$	$4.13$	-	$\mid xs\mid$	$2^{\mid xs\mid }$
5	common	$\forall \alpha .ys:SL\left({\alpha }^1\right)\to zs:SL\left({\alpha }^1\right)\to \{L\left(\alpha \right)\mid \text{elems}\nu =\text{elems}ys\cap \text{elems}zs\}$	, member	$30.79$	$1.07$	TO	-	$\mid ys\mid +\mid zs\mid$	$\mid ys\mid \mid zs\mid$
6	list difference	$\forall \alpha .ys:SL\left({\alpha }^1\right)\to zs:SL\left({\alpha }^1\right)\to \{L\left(\alpha \right)\mid \text{elems}\nu =\text{elems}ys-\text{elems}zs\}$	, member	$173.54$	$1.33$	TO	-	$\mid ys\mid +\mid zs\mid$	$\mid ys\mid \mid zs\mid$
7	insert	$\forall \alpha .x:\alpha \to xs:SL\left({\alpha }^1\right)\to \{SL\left(\alpha \right)\mid \text{elems}\nu =\left[x\right]\cup \text{elems}xs\}$		$1.30$	$0.43$	-	-	$\mid xs\mid$	$\mid xs\mid$
8	insert’	$\forall \alpha .x:\alpha \to xs:SL{\left(\alpha \right)}^{\mathrm{𝗇𝗎𝗆𝗀𝗍}(x,\nu )}\to \{SL\left(\alpha \right)\mid \text{elems}\nu =\left[x\right]\cup \text{elems}xs\}$		$49.59$	$0.67$	-	$102.23$	$\text{numgt}(x,xs)$	$\mid xs\mid$
9	insert”	$\forall \alpha .x:\alpha \to xs:SL\left({\alpha }^{\mathrm{𝗂𝗍𝖾}\left(x>\nu ,1,0\right)}\right)\to \{SL\left(\alpha \right)\mid \text{elems}\nu =\left[x\right]\cup \text{elems}xs\}$		$7.69$	$0.38$	-	$13.74$	$\text{numgt}(x,xs)$	$\mid xs\mid$
10	replicate	$\forall \alpha .n:\text{Nat}\to x:n\times {\alpha }^n\to \{L\left(\alpha \right)\mid \text{len}\nu =n\}$	zero, inc, dec	$1.43$	$0.15$	-	$2.67$	$n$	$n$
11	take	$\forall \alpha .n:\text{Nat}\to xs:{\{L\left(\alpha \right)\mid \text{len}\nu \ge n\}}^n\to \{L\left(\alpha \right)\mid \text{len}\nu =n\}$	zero, inc, dec	$1.22$	$0.11$	-	$2.42$	$n$	$n$
12	drop	$\forall \alpha .n:\text{Nat}\to xs:{\{L\left(\alpha \right)\mid \text{len}\nu \ge n\}}^n\to \{L\left(\alpha \right)\mid \text{len}\nu =\text{len}xs-n\}$	zero, inc, dec	$12.89$	$0.20$	-	$17.08$	$n$	$n$
13	range	$lo:\text{Int}\to hi:\{{\text{Int}}^{\nu -lo}\mid \nu \ge lo\}\to \{SL\left(\{\text{Int}\mid lo\le \nu \le hi\}\right)\mid \text{len}\nu =hi-lo\}$	inc,dec,$\ge$	$11.78$	$0.16$	-	-	$hi-lo$	-
14	CT insert	$\forall \alpha .x:\alpha \to xs:SL\left({\alpha }^1\right)\to \{SL\left(\alpha \right)\mid \text{elems}\nu =\left[x\right]\cup \text{elems}xs\}$		$2.24$	$0.63$	$0.79$	-	$\mid xs\mid$	$\mid xs\mid$
15	CT compare	$\forall \alpha .ys:L\left({\alpha }^1\right)\to zs:L\left(\alpha \right)\to \{\mathrm{𝖻𝗈𝗈𝗅}\mid \nu =(\text{len}ys=\text{len}zs)\}$	true, false, and	$14.25$	$0.54$	$9.14$	-	$\mid ys\mid$	$\mid ys\mid$
16	compare	$\forall \alpha .ys:L\left({\alpha }^1\right)\to zs:L\left(\alpha \right)\to \{\mathrm{𝖻𝗈𝗈𝗅}\mid \nu =(\text{len}ys=\text{len}zs)\}$	true, false, and	$1.01$	$0.34$	-	-	$\mid ys\mid$	$\mid ys\mid$

Equations

$$\begin{gathered} (\mathsf{elems}{l}_1=\{x\}\cup \mathsf{elems}xs)\wedge (x\notin \mathsf{elems}{l}_2)\wedge \\ (\mathsf{elems}\nu =\mathsf{elems}xs\cap \mathsf{elems}{l}_2)⟹\mathsf{elems}\nu =\mathsf{elems}{l}_1\cap \mathsf{elems}{l}_2 \end{gathered}$$

$$\begin{array}[]{r@{\hspace{0.2em}}c@{\hspace{0.2em}}l}a\hskip 1.99997pt&\Coloneqq\hfil\hskip 1.99997pt&x\mid\mathsf{true}\mid\mathsf{false}\mid\mathsf{nil}\mid\mathsf{cons}(\hat{a}_{h},a_{t})\\ \hat{a}\hskip 1.99997pt&\Coloneqq\hfil\hskip 1.99997pt&a\mid\lambda(x.e_{0})\mid\mathsf{fix}(f.x.e_{0})\\ e\hskip 1.99997pt&\Coloneqq\hfil\hskip 1.99997pt&\hat{a}\mid\mathsf{if}(a_{0},e_{1},e_{2})\mid\mathsf{matl}(a_{0},e_{1},x_{h}.x_{t}.e_{2})\mid\mathsf{app}(\hat{a}_{1},\hat{a}_{2})\\ \hskip 1.99997pt&\mid\hfil\hskip 1.99997pt&\mathsf{let}(e_{1},x.e_{2})\mid\mathsf{impossible}\mid\mathsf{tick}(c,e_{0})\\ v\hskip 1.99997pt&\Coloneqq\hfil\hskip 1.99997pt&\mathsf{true}\mid\mathsf{false}\mid\mathsf{nil}\mid\mathsf{cons}(v_{h},v_{t})\mid\lambda(x.e_{0})\mid\mathsf{fix}(f.x.e_{0})\end{array}$$

$$\begin{array}[]{r@{\hspace{0.2em}}c@{\hspace{0.2em}}l@{\hspace{0.6em}}r@{\hspace{0.2em}}c@{\hspace{0.2em}}l}\lx@intercol\framebox{\text{Refinement}}\hfil\lx@intercol\\ \psi,\phi\hskip 1.99997pt&\Coloneqq\hfil\hskip 1.99997pt&\hskip 1.00006pt\lx@intercol x\mid\top\mid\neg\psi\mid\psi_{1}\wedge\psi_{2}\mid n\mid\psi_{1}\leq\psi_{2}\mid\psi_{1}+\psi_{2}\mid\psi_{1}=\psi_{2}\hfil\lx@intercol\\ \lx@intercol\framebox{\text{Sort}}\hfil\lx@intercol\\ \Delta\hskip 1.99997pt&\Coloneqq\hfil\hskip 1.99997pt&\mathbb{B}\mid\mathbb{N}\mid\delta_{\alpha}\hfil\hskip 6.00006pt\\ \lx@intercol\framebox{\text{Base Type}}\hfil\lx@intercol&\lx@intercol\framebox{\text{Resource-Annotated Type}}\hfil\lx@intercol\\ B\hskip 1.99997pt&\Coloneqq\hfil\hskip 1.99997pt&\mathsf{bool}\mid L(T)\mid m\cdot\alpha\hfil\hskip 6.00006pt&\quad T\hskip 1.99997pt&\Coloneqq\hfil\hskip 1.99997pt&{R}^{\phi}\\ \lx@intercol\framebox{\text{Refinement Type}}\hfil\lx@intercol&\lx@intercol\framebox{\text{Type Schema}}\hfil\lx@intercol\\ R\hskip 1.99997pt&\Coloneqq\hfil\hskip 1.99997pt&\{B\mid\psi\}\mid{m}\cdot(x{\,:\,}T_{x}\rightarrow T)\hfil\hskip 6.00006pt&\quad S\hskip 1.99997pt&\Coloneqq\hfil\hskip 1.99997pt&T\mid\forall\alpha.S\end{array}$$

$$\begin{array}[]{r@{\hspace{0.6em}}c@{\hspace{0.6em}}l@{\hspace{3.0em}}r@{\hspace{0.6em}}c@{\hspace{0.6em}}l}\mathcal{I}(x)\hskip 6.00006pt&=\hfil\hskip 6.00006pt&x\hfil\hskip 30.00005pt\\ \mathcal{I}(\mathsf{true})\hskip 6.00006pt&=\hfil\hskip 6.00006pt&\top\hfil\hskip 30.00005pt&\mathcal{I}(\mathsf{nil})\hskip 6.00006pt&=\hfil\hskip 6.00006pt&0\\ \mathcal{I}(\mathsf{false})\hskip 6.00006pt&=\hfil\hskip 6.00006pt&\bot\hfil\hskip 30.00005pt&\mathcal{I}(\mathsf{cons}(\_,a_{t}))\hskip 6.00006pt&=\hfil\hskip 6.00006pt&\mathcal{I}(a_{t})+1\end{array}$$

$${{{{\begin{array}[]{r@{\hspace{0.5em}}c@{\hspace{0.5em}}l}\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{triple}}}}}}\hskip 5.0pt&\dblcolon\hfil\hskip 5.0pt&\ell{\,:\,}L({\mathsf{bool}}^{2})\rightarrow\{L(\mathsf{bool})\mid\nu=3\times\ell\}\\ \mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{triple}}}}}}\hskip 5.0pt&=\hfil\hskip 5.0pt&\lambda(\ell.\mathsf{let}(\mathsf{app}(\mathsf{app}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{append}}}}}},\ell),\ell),\ell^{\prime}.\\ \hskip 5.0pt&\hfil\hskip 5.0pt&\enskip\mathsf{app}(\mathsf{app}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{append}}}}}},\ell),\ell^{\prime}))\vspace{-1.2ex}\end{array}$$

$${\begin{array}[]{@{\hspace{0.2em}}r@{\hspace{0.2em}}c@{\hspace{0.2em}}l@{\hspace{0.2em}}}\hskip 1.99997pt\lx@intercol\hfil\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{append}}}}}}\hskip 1.99997pt&\dblcolon\hfil\hskip 1.99997pt&\forall\alpha.xs{\,:\,}L({\alpha}^{1})\rightarrow{1}\cdot(ys{\,:\,}L(\alpha)\rightarrow\{L(\alpha)\mid\nu=xs+ys\})\hfil\hskip 1.99997pt\end{array}$$

$$xs:L({\mathsf{bool}}^1)\to 1\cdot (ys:L({\mathsf{bool}}^0)\to \{L({\mathsf{bool}}^0)\mid \nu =xs+ys\})\text{vspace}-.8ex$$

$$\Gamma ,\ell :L({\mathsf{bool}}^1)⊢e_1::\{L({\mathsf{bool}}^0)\mid \nu =\ell +\ell \}.\text{vspace}-.8ex$$

$$\Gamma ,\ell :L({\mathsf{bool}}^1),{\ell }^{\prime }:T_1⊢e_2::\{L({\mathsf{bool}}^0)\mid \nu =xs+(xs+xs)\}.$$

$$\Gamma ,\ell :L({\mathsf{bool}}^2),\nu :L({\mathsf{bool}}^0)\models \nu =\ell +(\ell +\ell )⟹\nu =3\times \ell ,$$

$$\begin{array}[]{r@{\hspace{0.2em}}c@{\hspace{0.2em}}l}D\hskip 1.99997pt&\Coloneqq\hfil\hskip 1.99997pt&\cdot\mid D;x\leftarrow e\\ \mathring{e}\hskip 1.99997pt&\Coloneqq\hfil\hskip 1.99997pt&e\mid\circ\mid\mathsf{app}(x,\circ)\mid\mathsf{if}(x,\circ,\circ)\mid\mathsf{matl}(x,\circ,x_{h}.x_{t}.\circ)\mid\mathsf{lets}(D.\mathring{e})\\ T\hskip 1.99997pt&\Coloneqq\hfil\hskip 1.99997pt&{R}^{\phi}\mid\mathsf{?}\end{array}$$

$$\mathbb{C}(\Gamma ⊢m_1\cdot \alpha <:m_2\cdot \alpha )=\{\Gamma \models m_1-m_2\ge 0\}$$

$$\mathbb{C}(\Gamma ⊢\{B_1\mid {\psi }_1\}<:\{B_2\mid {\psi }_2\})=\{\Gamma ,\nu :B_1\models {\psi }_1⟹{\psi }_2\}\cup \mathbb{C}(\Gamma ⊢B_1<:B_2)$$

$$\mathbb{C}(\Gamma ⊢{R_1}^{{\varphi }_1}<:{R_2}^{{\varphi }_2})=\{\Gamma ,\nu :R_1\models {\varphi }_1-{\varphi }_2\ge 0\}\cup \mathbb{C}(\Gamma ⊢R_1<:R_2)$$

$$\mathbb{C}(\Gamma ⊢m\cdot \alpha \text{curlyveedownarrow}{m}_1\cdot \alpha \mid m_2\cdot \alpha )=\{\Gamma \models m-(m_1+m_2)\ge 0,$$

$$\Gamma \models m_1+m_2-m\ge 0\}$$

$$\mathbb{C}(\Gamma ⊢R^{\varphi }\text{curlyveedownarrow}{R_1}^{{\varphi }_1}\mid {R_2}^{{\varphi }_2})=\{\Gamma \models \varphi -({\varphi }_1+{\varphi }_2)\ge 0,\Gamma \models {\varphi }_1+{\varphi }_2-\varphi \ge 0\}$$

$$\cup \mathbb{C}(\Gamma ⊢R\text{curlyveedownarrow}{R}_1\mid R_2)$$

$$\mathbb{C}(\Phi (\Gamma )=\Phi ({\Gamma }^{\prime }))=\{\Gamma \models \Phi (\Gamma )-\Phi ({\Gamma }^{\prime })\ge 0,\Phi ({\Gamma }^{\prime })-\Phi (\Gamma )\ge 0\}$$

$$\overrightarrow{\exists C_i}.\overrightarrow{\forall x}.\underset{r\in R}{\bigwedge }r(\overrightarrow{C_i},\overrightarrow{x})$$

$$\exists C_0\dots C_3.\forall a,b,\nu .$$

$$(\neg (a\ge b)\wedge \nu =b)⟹(C_0+1)\cdot a+C_1\cdot b+(C_2-1)\cdot \nu +C_3\ge 0$$

$$(\neg (a\ge b)\wedge \nu =b)⟹C_0\cdot a+C_1\cdot b+C_2\cdot \nu +C_3\ge 0$$

$$\Phi (\cdot )$$

$$\Phi (\Gamma ,x:{\{B\mid \psi \}}^{\varphi })$$

$$\Phi (\Gamma ,x:{(m\cdot (y:T_y\to T))}^{\varphi })$$

$$\Phi (\Gamma ,x:\forall \alpha .S)$$

$$[U/\alpha ]\mathsf{bool}$$

$$[U/\alpha ]L(T)$$

$$[U/\alpha ]m\cdot \beta$$

$$[{\{B\mid \psi \}}^{\varphi }/\alpha ]m\cdot \alpha$$

$$[U/\alpha ]\{B\mid \psi \}$$

$$\text{where}[U/\alpha ]B={\{B^{\prime }\mid {\psi }^{\prime }\}}^{{\varphi }^{\prime }}$$

$$[U/\alpha ]m\cdot (x:T_x\to T)$$

$$[U/\alpha ]R^{\varphi }$$

$$\text{where}[U/\alpha ]R=R^{\prime {\varphi }^{\prime }}$$

$$[U/\alpha ]\forall \beta .S$$

$$m\times \mathsf{bool}$$

$$m\times L(T)$$

$$m_1\times (m_2\cdot \alpha )$$

$$\text{llparenthesis}\mathbb{B}\text{rrparenthesis}$$

$$\text{llparenthesis}\mathbb{N}\text{rrparenthesis}$$

$${\mathcal{T}}_E(\mathsf{bool})$$

Full text

Program Synthesis, Automated Amortized Resource Analysis, Refinement Types

††ccs: Software and its engineering Automatic programming††ccs: Theory of computation Automated reasoning††journalyear: 2019††copyright: acmlicensed††conference: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation; June 22–26, 2019; Phoenix, AZ, USA††booktitle: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’19), June 22–26, 2019, Phoenix, AZ, USA††price: 15.00††doi: 10.1145/3314221.3314602††isbn: 978-1-4503-6712-7/19/06

1. Introduction

In recent years, program synthesis has emerged as a promising technique for automating low-level aspects of programming (Gulwani et al., 2012; Solar-Lezama, 2013; Torlak and Bodík, 2014). Synthesis technology enables users to create programs by describing desired behavior with input-output examples (Osera and Zdancewic, 2015; Feser et al., 2015; Smith and Albarghouthi, 2016; Feng et al., 2017a; Feng et al., 2017b, 2018; Wang et al., 2018, 2017), natural language (Yaghmazadeh et al., 2017), and partial or complete formal specifications (Srivastava et al., 2010; Kneuss et al., 2013; Polikarpova et al., 2016; Inala et al., 2017; Qiu and Solar-Lezama, 2017). If the input is a formal specification, synthesis algorithms can not only create a program but also a proof that the program meets the given specification  (Srivastava et al., 2010; Kneuss et al., 2013; Polikarpova et al., 2016; Qiu and Solar-Lezama, 2017).

One of the greatest challenges in software development is to write programs that are not only correct but also efficient with respect to memory usage, execution time, or domain specific resource metrics. For this reason, automatically optimizing program performance has long been a goal of synthesis, and several existing techniques tackle this problem for low-level straight-line code (Schkufza et al., 2013; Phothilimthana et al., 2014; Sharma et al., 2015; Phothilimthana et al., 2016; Bornholt et al., 2016) or add efficient synchronization to concurrent programs (Cerný et al., 2011; Gupta et al., 2015; Cerný et al., 2015a; Ferles et al., 2018). However, the developed techniques are not applicable to recent advances in the synthesis of high-level looping or recursive programs manipulating custom data structures  (Kneuss et al., 2013; Osera and Zdancewic, 2015; Feser et al., 2015; Polikarpova et al., 2016; Inala et al., 2017; Qiu and Solar-Lezama, 2017). These techniques lack the means to analyze and understand the resource usage of the synthesized programs. Consequently, they cannot take into account the program’s efficiency and simply return the first program that arises during the search and satisfies the functional specification.

In this work, we study the problem of synthesizing high-level recursive programs given both a functional specification of a program and a bound on its resource usage. A naive solution would be to first generate a program using conventional program synthesis and then use existing automatic static resource analyses (Hoffmann et al., 2012; Peng Wang, 2017; Cicek et al., 2017) to check whether its resource usage satisfies the bound. Note, however, that for recursive programs, both synthesis and resource analysis are undecidable in theory and expensive in practice. Instead, in this paper we propose resource-guided synthesis: an approach that tightly integrates program synthesis and resource analysis, and uses the resource bound to guide the synthesis process, generating programs that are efficient by construction.

Type-Driven Synthesis

In a nutshell, the idea of this work is to combine type-driven program synthesis, pioneered in the work on Synquid (Polikarpova et al., 2016), with type-based automatic amortized resource analysis (AARA) (Hofmann and Jost, 2003; Jost et al., 2010; Hoffmann et al., 2011, 2017) as implemented in Resource Aware ML (RaML) (Hoffmann, 2018). Type-driven synthesis and AARA are a perfect match because they are both based on decidable, constraint-based type systems that can be easily checked with off-the-shelf constraint solvers.

In Synquid, program specifications are written as refinement types (Vazou et al., 2013; Knowles and Flanagan, 2009). The key to efficient synthesis is round-trip type checking, which uses an SMT solver to aggressively prune the search space by rejecting partial programs that do not meet the specification (see Sec. 2.1). Until now, types have only been used in the context of synthesis to specify functional properties.

AARA is a type-based technique for automatically deriving symbolic resource bounds for functional programs. The idea is to add resource annotations to data types, in order to specify a potential function that maps values of that type to non-negative numbers. The type system ensures that the initial potential is sufficient to cover the cost of the evaluation. By a priori fixing the shape of the potential functions, type inference can be reduced to linear programming (see Sec. 2.2).

The  $\mathrm{Re}^{2}$ Type System

The first contribution of this paper is a new type system, which we dub $\mathrm{Re}^{2}$—for refinements and resources—that combines polymorphic refinement types with AARA (Sec. 3). $\mathrm{Re}^{2}$ is a conservative extension of Synquid’s refinement type system and RaML’s affine type system with linear potential annotations. As a result, $\mathrm{Re}^{2}$ can express logical assertions that are required for effectively specifying program synthesis problems. In addition, the type system features annotations of numeric sort in the same refinement language to express potential functions. Using such annotations, programmers can express precise resource bounds that go beyond the template potential functions of RaML.

The features that distinguish $\mathrm{Re}^{2}$ from other refinement-based type systems for resource analysis (Peng Wang, 2017; Cicek et al., 2017; Radicek et al., 2018) are

(1) the combination of logical and quantitative refinements and

(2) the use of AARA, which simplifies resource constraints and naturally applies to non-monotone resources like memory that can become available during the execution.

These features also pose nontrivial technical challenges: the interaction between substructural and dependent types is known to be tricky (Krishnaswami et al., 2015; Lago and Gaboardi, 2011), while polymorphism and higher-order functions are challenging for AARA (one solution is proposed in (Jost et al., 2010), but their treatment of polymorphism is not fully formalized).

In addition to the design of $\mathrm{Re}^{2}$, we prove the soundness of the type system with respect to a small-step cost semantics. In the formal development, we focus on a simple call-by-value functional language with Booleans and lists, where type refinements are restricted to linear inequalities over lengths of lists. However, we structure the formal development to emphasize that $\mathrm{Re}^{2}$ can be extended with user-defined data types, more expressive refinements, or non-linear potential annotations. The proof strategy itself is a contribution of this paper. The type soundness of the logical refinement part of the system is inspired by TiML (Peng Wang, 2017). The main novelty is the soundness proof of the potential annotations using a small-step cost semantics instead of RaML’s big-step evaluation semantics.

Type-Driven Synthesis with $\mathrm{Re}^{2}$

The second contribution of this paper is a resource-guided synthesis algorithm based on $\mathrm{Re}^{2}$. In Sec. 4, we first develop a system of synthesis rules that prescribe how to derive well-typed programs from $\mathrm{Re}^{2}$ types, and prove its soundness wrt. the $\mathrm{Re}^{2}$ type system. We then show how to algorithmically derive programs using a combination of backtracking search and constraint solving. In particular this requires solving a new form of constraints we call resource constraints, which are constrained linear inequalities over unknown numeric refinement terms. To solve resource constraints, we develop a custom solver based on counter-example guided inductive synthesis (Solar-Lezama et al., 2006) and SMT (de Moura and Bjørner, 2008).

The ReSyn Synthesizer

The third contribution of this paper is the implementation and experimental evaluation of the first resource-aware synthesizer for recursive programs. We implemented our synthesis algorithm in a tool called ReSyn, which takes as input

(1) a goal type that specifies the logical refinements and resource requirements of the program, and

(2) types of components (i.e. library functions that the program may call).

ReSyn then synthesizes a program that provably meets the specification (assuming the soundness of components).

To evaluate the scalability of the synthesis algorithm and the quality of the synthesized programs, we compare ReSyn with baseline Synquid on a variety of general-purpose data structure operations, such as eliminating duplicates from a list or computing common elements between two lists. The evaluation (Sec. 5) shows that ReSyn is able to synthesize programs that are asymptotically more efficient than those generated by Synquid. Moreover, the tool scales better than a naive combination of synthesis and resource analysis.

2. Background and Overview

This section provides the necessary background on type-driven program synthesis (Sec. 2.1) and automatic resource analysis (Sec. 2.2). We then describe and motivate their combination in $\mathrm{Re}^{2}$ and showcase novel features of the type system (Sec. 2.3). Finally, we demonstrate how $\mathrm{Re}^{2}$ can be used for resource-guided synthesis (Sec. 2.4).

2.1. Type-Driven Program Synthesis

Type-driven program synthesis (Polikarpova et al., 2016) is a technique for automatically generating functional programs from their high-level specifications expressed as refinement types (Knowles and Flanagan, 2009; Rondon et al., 2008). For example, a programmer might describe a function that computes the common elements between two lists using the following type signature:

⬇

$\rightarrow$ {\nu$$\colonList a$\mid$elems $\nu$ $=$ elems l1 $\cap$ elems l2}

Here, the return type of common is refined with the predicate elems $\nu$ $=$ elems l1 $\cap$ elems l2, which restricts the set of elements of the output list $\nu$111Hereafter the bound variable of the refinement is always called $\nu$ and the binding is omitted. to be the intersection of the sets of elements of the two arguments. Here elems is a user-defined logic-level function, also called measure (Kawaguchi et al., 2009; Vazou et al., 2013). In addition to the synthesis goal above, the synthesizer takes as input a component library: signatures of data constructors and functions it can use. In our example, the library includes the list constructors Nil and Cons and the function

which determines whether a given value is in the list. Given this goal and components, the type-driven synthesizer Synquid (Polikarpova et al., 2016) produces an implementation of common in Fig. 1.

The Synthesis Mechanism

Type-driven synthesis works by systematically exploring the space of programs that can be built from the component library and validating candidate programs against the goal type using a variant of liquid type inference (Rondon et al., 2008). To validate a program against a refinement type, liquid type inference generates a system of subtyping constraints over refinement types. The subtyping constraints are then reduced to implications between refinement predicates. For example, checking common xs l2 in line 3 of Fig. 1 against the goal type reduces to validating the following implication:

[TABLE]

Since this formula belongs to a decidable theory of uninterpreted functions and arrays, its validity can be checked by an SMT solver (de Moura and Bjørner, 2008). In general, the generated implications may contain unknown predicates. In this case, type inference reduces to a system of constrained horn clauses (Bjørner et al., 2015), which can be solved via predicate abstraction.

Synthesis and Program Efficiency

The program in Fig. 1 is correct, but not particularly efficient: it runs roughly in time $n{\cdot}m$, where $m$ is the length of l1 and $n$ is the length of l2, since it calls the member function (a linear scan) for every element of l1. The programmer might realize that keeping the input lists sorted would enable computing common elements in linear time by scanning the two lists in parallel. To communicate this intent to the synthesizer, they can define the type of (strictly) sorted lists by augmenting a traditional list definition with a simple refinement:

⬇

SCons$::$x$\colon$a $\rightarrow$ xs$\colon$SList {a$\mid$x $<$ $\nu$} $\rightarrow$ SList a

This definition says that a sorted list is either empty, or is constructed from a head element x and a tail list xs, as long as xs is sorted and all its elements are larger than x.222Following Synquid, our language imposes an implicit constraint on all type variables to support equality and ordering. Hence, they cannot be instantiated with arrow types. This could be lifted by adding type classes. Given an updated synthesis goal (where selems is a version of elems for SList)

⬇

$\rightarrow$ {\nu$$\colonList a$\mid$elems $\nu$ $=$ selems l1 $\cap$ selems l2}

and a component library that includes List, SList, and $<$ (but not member!), Synquid can synthesize an efficient program shown in in Fig. 2.

However, if the programmer leaves the function member in the library, Synquid will synthesize the inefficient implementation in Fig. 1. In general, Synquid explores candidate programs in the order of size and returns the first one that satisfies the goal refinement type. This can lead to suboptimal solutions, especially as the component library grows larger and allows for many functionally correct programs. To avoid inefficient solutions, the synthesizer has to be aware of the resource usage of the candidate programs.

2.2. Automatic Amortized Resource Analysis

To reason about the resource usage of programs we take inspiration from automatic amortized resource analysis (AARA) (Hofmann and Jost, 2003; Jost et al., 2010; Hoffmann et al., 2011, 2017). AARA is a state-of-the-art technique for automatically deriving symbolic resource bounds on functional programs, and is implemented for a subset of OCaml in Resource Aware ML (RaML) (Hoffmann et al., 2017; Hoffmann, 2018). For example, RaML is able to automatically derive the worst-case bound $2m+n{\cdot}m$ on the number of recursive calls for the function common and $m+n$ for common’  333In this section we assume for simplicity that the resource of interest is the number of recursive calls. Both AARA and our type system support user-defined cost metrics (see Sec. 3 for details)..

Potential Annotations

AARA is inspired by the potential method for manually analyzing the worst-case cost of a sequence of operations (Tarjan, 1985a). It uses annotated types to introduce potential functions that map program states to non-negative numbers. To derive a bound, we have to statically ensure that the potential at every program state is sufficient to cover the cost of the next transition and the potential of the following state. In this way, we ensure that the initial potential is an upper bound on the total cost.

The key to making this approach effective is to closely integrate the potential functions with data structures (Hofmann and Jost, 2003; Jost et al., 2010). For instance, in RaML the type ${L^{1}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{int}}}}}})$ stands for a list that contains one unit of potential for every element. This type defines the potential function ${\phi(\ell{:}L^{1}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{int}}}}}}))=1\cdot|\ell|$. The potential can be used to pay for a recursive call (or, in general, cover resource usage) or to assign potential to other data structures.

Bound Inference

Potential annotations can be derived automatically by starting with a symbolic type derivation that contains fresh variables for the potential annotations of each type, and applying syntax directed type rules that impose local constraints on the annotations. The integration of data structures and potential ensures that these constraints are linear even for polynomial potential annotations.

2.3. Bounding Resources with $\mathrm{Re}^{2}$

To reason about resource usage in type-driven synthesis, we integrate AARA’s potential annotations and refinement types into a novel type system that we call $\mathrm{Re}^{2}$. In $\mathrm{Re}^{2}$, a refinement type can be annotated with a potential term $\phi$ of numeric sort, which is drawn from the same logic as refinements. Intuitively, the type ${R}^{\phi}$ denotes values of refinement type $R$ with $\phi$ units of potential. In the rest of this section we illustrate features of $\mathrm{Re}^{2}$ on a series of examples, and delay formal treatment to Sec. 3.

With potential annotations, users can specify that common’ must run in time at most $m+n$, by giving it the following type signature:

⬇

$\rightarrow$ {\nu$$\colonList a$\mid$elems $\nu$ $=$ selems l1 $\cap$ selems l2}

This type assigns one unit of potential to every element of the arguments l1 and l2, and hence only allows making one recursive call per element of each list. Whenever resource annotations are omitted, the potential is implicitly zero: for example, the elements of the result carry no potential.

Our type checker uses the following reasoning to argue that this potential is sufficient to cover the efficient implementation in Fig. 2. Consider the recursive call in line 4, which has a cost of one. Pattern-matching l1 against SCons x xs transfers the potential from l1 to the binders, resulting in types ${\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{x}}}}}}:{a}^{1}$ and ${{{\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{xs}}}}}}:\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{SList}}}}}}\ ({\{a\mid\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{x}}}}}}<\nu\}}^{1})$. The unit of potential associated with x can now be used to pay for the recursive call. Moreover, the types of the arguments, xs and l2, match the required type ${\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{SList}}}}}}\ {a}^{1}$, which guarantees that the potential stored in the tail and the second list are sufficient to cover the rest of the evaluation. Other recursive calls are checked in a similar manner.

Importantly, the inefficient implementation in Fig. 1 would not type-check against this signature. Assuming that member is soundly annotated with

(requiring a unit of potential per element of l), the guard in line 2 consumes all the potential stored in l2; hence the occurrence of l2 in line 3 has the type ${\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{List}}}}}}\ {a}^{0}$, which is not a subtype of ${\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{List}}}}}}\ {a}^{1}$.

Dependent Potential Annotations

In combination with logical refinements and parametric polymorphism, this simple extension to the Synquid’s type system turns out to be surprisingly powerful. Unlike in RaML, potential annotations in $\mathrm{Re}^{2}$ can be dependent, i.e. mention program variables and the special variable $\nu$. Dependent annotations can encode fine-grained bounds, which are out of reach for RaML. As one example, consider function range a b that builds a list of all integers between $a$ and $b$; we can express that it takes at most $b-a$ steps by giving the argument $b$ a type ${{\{\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{Int}}}}}}\mid\nu\geq a\}}^{\nu-a}$. As another example, consider insertion into a sorted list insert x xs; we can express that it takes at most as many steps as there are elements in $xs$ that are smaller than $x$, by giving $xs$ the type ${\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{SList}}}}}}\ {\alpha}^{\mathsf{ite}(\nu<x,1,0)}$ (i.e. only assigning potential to elements that are smaller than $x$). These fine-grained bounds are checked completely automatically in our system, by reduction to constraints in SMT-decidable theories.

Polymorphism

Another source of expressiveness in $\mathrm{Re}^{2}$ is parametric polymorphism: since potential annotations are attached to types, type polymorphism gives us resource polymorphism for free. Consider two functions in Fig. 3, triple and tripleSlow, which implement two different ways to append a list l to two copies of itself. Both of them make use of a component function append, whose type indicates that it makes a linear traversal of its first argument. Intuitively, triple is more efficient that tripleSlow because in the former both calls to append traverse a list of length $n$, whereas in the latter the outer call traverses a list of length $2{\cdot}n$. This difference is reflected in the signatures of the two functions: tripleSlow requires three units of potential per list element, while triple only requires two.

Checking that tripleSlow satisfies this bound is somewhat nontrivial because the two applications of append must have different types: the outer application must return List Int, while the inner application must return ${{\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{List}}}}}}\ \mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{Int}}}}}}^{1}$ (i.e. carry enough potential to be traversed by append). RaML’s monomorphic type system is unable to assign a single general type to append, which can be used at both call sites. So the function has be reanalyzed at every (monomorphic) call site. $\mathrm{Re}^{2}$, on the other hand, handles this example out of the box, since the type variable a in the type of append can be instantiated with Int for the outer occurrence and with ${\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{Int}}}}}}^{1}$ for the inner occurrence, yielding the type

As a final example, consider the standard map function:

Although this type has no potential annotations, it implicitly tells us something about the resource behavior of map: namely, that map applies a function to each list element at most once. This is because a can be instantiated with a type with an arbitrary amount of potential, and the only way to pay for this potential is with a list element (which also has type a).

2.4. Resource-guided Synthesis with ReSyn

We have extended Synquid with support for $\mathrm{Re}^{2}$ types in a new program synthesizer ReSyn. Given a resource-annotated signature for common’ from Sec. 2.3 and a component library that includes member, ReSyn is able to synthesize the efficient implementation in Fig. 2. The key to efficient synthesis is type-checking each program candidate incrementally as it is being constructed, and discarding an ill-typed program prefix as early as possible. For example, while enumerating candidates for the function common’, we can safely discard the inefficient version from Fig. 1 even before constructing the second branch of the conditional (because the first branch together with the guard use up too many resources). Hence, as we explain in more detail in Sec. 4, a key technical challenge in ReSyn has been a tight integration of resources into Synquid’s round-trip type checking mechanism, which aggressively propagates type information top-down from the goal and solves constraints incrementally as they arise.

Termination Checking

In addition to making the synthesizer resource-aware, $\mathrm{Re}^{2}$ types also subsume and generalize Synquid’s termination checking mechanism. To avoid generating diverging functions, Synquid uses a simple termination metric (the tuple of function’s arguments), and checks that this metric decreases at every recursive call. Using this metric, Synquid is not able to synthesize the function range from Sec. 2.3, because it requires a recursive call that decreases the difference between the arguments, $b-a$. In contrast, ReSyn need not reason explicitly about termination, since potential annotations already encode an upper bound on the number of recursive calls. Moreover, the flexibility of these annotations enables ReSyn to synthesize programs that require nontrivial termination metrics, such as range.

3. The $\mathrm{Re}^{2}$ Type System

In this section, we define a subset of $\mathrm{Re}^{2}$ as a formal calculus to prove type soundness. This subset includes Booleans that are refined by their values, and lists that are refined by their lengths. The programs in Sec. 1 and Sec. 2 use Synquid’s surface syntax. The gap from the surface language to the core calculus involves inductive types and refinement-level measures. The restriction to this subset in the technical development is only for brevity and proofs carry over to all the features of Synquid.

Syntax

Fig. 4 presents the grammar of terms in $\mathrm{Re}^{2}$ via abstract binding trees (Harper, 2016). The core language is basically the standard lambda calculus augmented with Booleans and lists. A value $v\in\mathsf{Val}$ is either a boolean constant, a list of values, or a function. Expressions in $\mathrm{Re}^{2}$ are in a-normal-form (Sabry and Felleisen, 1992), which means that syntactic forms occurring in non-tail position allow only atoms $\hat{a}\in\mathsf{Atom}$, i.e., variables and values; this restriction simplifies typing rules for applications, as we explain below. We identify a subset $\mathsf{SimpAtom}$ of $\mathsf{Atom}$ that contains atoms interpretable in the refinement logic. Intuitively, the value of an $a\in\mathsf{SimpAtom}$ should be either a Boolean or a list. The syntactic form $\mathsf{impossible}$ is introduced as a placeholder for unreachable code, e.g., the else-branch of a conditional whose predicate is always true.

The syntactic form $\mathsf{tick}(c,e_{0})$ is used to specify resource usage, and it is intended to cost $c\in\mathbb{Z}$ units of resource and then reduce to $e_{0}$. If the cost $c$ is negative, then $-c$ units of resource will become available in the system. $\mathsf{tick}$ terms support flexible user-defined cost metrics: for example, to count recursive calls, the programmer may wrap every such call in $\mathsf{tick}(1,\cdot)$; to keep track of memory consumption, they might wrap every data constructor in $\mathsf{tick}(c,\cdot)$, where $c$ is the amount of memory that constructor allocates.

Operational Semantics

The resource usage of a program is determined by a small-step operational cost semantics. The semantics is a standard one augmented with a resource parameter. A step in the evaluation judgment has the form $\langle e,q\rangle\mapsto\langle e^{\prime},q^{\prime}\rangle$ where $e$ and $e^{\prime}$ are expressions and $q,q^{\prime}\in\mathbb{Z}^{+}_{0}$ are nonnegative integers. For example, the following is the rule for $\mathsf{tick}(c,e_{0})$.

{mathpar}\inferrule $\langle\mathsf{tick}(c,e_{0}),q\rangle\mapsto\langle e_{0},q-c\rangle$

The multi-step evaluation relation $\mapsto^{*}$ is the reflexive transitive closure of $\mapsto$. The judgment $\langle e,q\rangle\mapsto^{*}\langle e^{\prime},q^{\prime}\rangle$ expresses that with $q$ units of available resources, $e$ evaluates to $e^{\prime}$ without running out of resources and $q^{\prime}$ resources are left. Intuitively, the high-water mark resource usage of an evaluation of $e$ to $e^{\prime}$ is the minimal $q$ such that $\langle e,q\rangle\mapsto^{*}\langle e^{\prime},q^{\prime}\rangle$. For monotone resources like time, the cost is the sum of costs of all the evaluated $\mathsf{tick}$ expressions. In general, this net cost is invariant, that is, $p-p^{\prime}=q-q^{\prime}$ if $\langle e,p\rangle\mapsto^{n}\langle e^{\prime},p^{\prime}\rangle$ and $\langle e,q\rangle\mapsto^{n}\langle e^{\prime},q^{\prime}\rangle$, where $\mapsto^{n}$ is the relation obtained by self-composing $\mapsto$ for $n$ times.

Refinements

We now combine Synquid’s type system with AARA to reason about resource usage. Fig. 5 shows the syntax of the $\mathrm{Re}^{2}$ type system. Refinements $\psi$ are distinct from program terms and classified by sorts $\Delta$. $\mathrm{Re}^{2}$’s sorts include Booleans $\mathbb{B}$, natural numbers $\mathbb{N}$, and uninterpreted symbols $\delta_{\alpha}$. Refinements can be logical formulas and linear expressions, which may reference program variables. Logical refinements $\psi$ have sort $\mathbb{B}$, while potential annotations $\phi$ have sort $\mathbb{N}$. $\mathrm{Re}^{2}$ interprets a variable of Boolean type as its value, list type as its length, and type variable $\alpha$ as an uninterpreted symbol with a corresponding sort $\delta_{\alpha}$. We use the following interpretation $\mathcal{I}(\cdot)$ to reflect interpretable atoms $a\in\mathsf{SimpAtom}$ in the refinement logic:

[TABLE]

Types

We classify types into four categories. Base types $B$ include Booleans, lists and type variables. Type variables $\alpha$ are annotated with a multiplicity $m\in\mathbb{Z}^{+}_{0}\cup\{\infty\}$, which denotes an upper bound on the number of usages of a variable like in bounded linear logic (Girard et al., 1992). For example, $L(2\cdot\alpha)$ denotes a universal list whose elements can be used at most twice.

Refinement types are subset types and dependent arrow types. The inhabitants of the subset type $\{B\mid\psi\}$ are values of type $B$ that satisfy the refinement $\psi$. The refinement $\psi$ is a logical predicate over program variables and a special value variable $\nu$, which does not appear in the program and stands for the inhabitant itself. For example, $\{\mathsf{bool}\mid\nu\}$ is a type of $\mathsf{true}$, and $\{L(\mathsf{bool})\mid\nu\leq 5\}$ represents Boolean lists of length at most 5. Dependent arrow types $x{\,:\,}T_{x}\rightarrow T$ are function types whose return type may reference the formal argument $x$. As type variables, these function types are also annotated with a multiplicity $m\in\mathbb{Z}^{+}_{0}\cup\{\infty\}$ restricting the number of times the function may be applied.

To apply the potential method of amortized analysis (Tarjan, 1985b), we need to define potentials with respect to the data structures in the program. We introduce resource-annotated types as a refinement type augmented with a potential annotation, written ${R}^{\phi}$. Intuitively, ${R}^{\phi}$ assigns $\phi$ units of potential to values of the refinement type $R$. The potential annotation $\phi$ may also reference the value variable $\nu$. For example, ${L(\mathsf{bool})}^{5\times\nu}$ describes Boolean lists $\ell$ with $5|\ell|$ units of potential where $|\ell|$ is the length of $\ell$. The same potential can be expressed by assigning $5$ units of potential to every element using the type $L({\mathsf{bool}}^{5})$.

Type schemas represent (possibly) polymorphic types. Note that the type quantifier ${\forall}$ can only appear outermost in a type.

Similar to Synquid, we introduce a notion of scalar types, which are resource-annotated base types refined by logical constraints. Intuitively, interpretable atoms are scalars and $\mathrm{Re}^{2}$ only allows the refinement-level logic to reason about values of scalar types. We will abbreviate $1\cdot\alpha$ as $\alpha$, $\{B\mid\top\}$ as $B$, ${\infty}\cdot(x{\,:\,}T_{x}\rightarrow T)$ as $x{\,:\,}T_{x}\rightarrow T$, and ${R}^{0}$ as $R$.

Typing Rules

In $\mathrm{Re}^{2}$, the typing context $\Gamma$ is a sequence of variable bindings $x:S$, type variables $\alpha$, path conditions $\psi$, and free potentials $\phi$. Our type system consists of five judgments: sorting, well-formedness, subtyping, sharing, and typing. We omit sorting and well-formedness rules and include them in Appendix A. The sorting judgment $\Gamma\vdash\psi\in\Delta$ states that a refinement $\psi$ has a sort $\Delta$ under a context $\Gamma$. A type $S$ is said to be well-formed under a context $\Gamma$, written $\Gamma\vdash S~{}\mathsf{type}$, if every referenced variable in it is in the correct scope.

Fig. 6 presents selected typing rules for $\mathrm{Re}^{2}$. The typing judgment $\Gamma\vdash e\dblcolon S$ states that the expression $e$ has type $S$ in context $\Gamma$. The intuitive meaning is that if there is at least the amount resources as indicated by the potential in the context $\Gamma$ then this suffices to evaluate $e$ to a value $v$, and after the evaluation there are at least as many resources available as indicated by the potential in $S$. The auxiliary typing judgment $\Gamma\vdash a:B$ assigns base types to interpretable atoms. Atomic typing is useful in the rule (T-SimpAtom), which uses the interpretation $\mathcal{I}(\cdot)$ to derive a most precise refinement type for interpretable atoms.

The subtyping judgment $\Gamma\vdash T_{1}<:T_{2}$ is defined in a standard way, with the extra requirement that the potential in $T_{1}$ should be greater than or equal to that in $T_{2}$. Subtyping is often used to “forget” some program variables in the type to ensure the result type does not reference any locally introduced variable, e.g., the result type of $\mathsf{let}(e_{1},x.e_{2})$ cannot have $x$ in it and the result type of $\mathsf{matl}(a_{0},e_{1},x_{h}.x_{t}.e_{2})$ cannot reference $x_{h}$ or $x_{t}$.

To reason about logical refinements, we introduce validity checking, written $\Gamma\models\psi$, to state that a logical refinement $\psi$ is always true under any instance of the context $\Gamma$. The validity checking relation is established upon a denotational semantics for refinements. Validity checking in $\mathrm{Re}^{2}$ is decidable because it can be reduced to Presburger arithmetic. The full development of validity checking is included in Appendix B.

We reason about inductive invariants for lists in rule (T-MatL), using interpretation $\mathcal{I}(\cdot)$. In our formalization, lists are refined by their length thus the invariants are: (i) $\mathsf{nil}$ has length [math], and (ii) the length of $\mathsf{cons}(\_,a_{t})$ is the length of $a_{t}$ plus one. The type system can be easily enriched with more refinements and data types (e.g., the elements of a list are the union of its head and those of its tail) by updating the interpretation $\mathcal{I}(\cdot)$ as well as the premises of rule (T-MatL).

Finally, notable are the two typing rules for applications: (T-App) and (T-App-SimpAtom). In the former case, the function return type $T$ does not mention $x$, and hence can be directly used as the type of the application (this is the case e.g. for all higher-order applications, since our well-formedness rules prevent functions from appearing in refinements). In the latter case, $T$ mentions $x$, but luckily any argument of a scalar type must be a simple atom $a$, so we can substitute $x$ with its interpretation $\mathcal{I}(a)$. The ability to derive precise types for dependent applications motivates the use of a-normal-form in $\mathrm{Re}^{2}$.

Resources

The rule (T-Consume-P) states that an expression $\mathsf{tick}(c,e_{0})$ is only well-typed in a context that contains a free potential term $c$. To transform the context into this form, we can use the rule (S-Transfer) to transfer potential within the context between variable types and free potential terms, as long as we can prove that the total amount of potential remains the same. For example, the combination of (S-Transfer) and (S-Relax) allows us to derive both $x:{\mathsf{bool}}^{1}\vdash x\dblcolon{\mathsf{bool}}^{1}$ and $x:{\mathsf{bool}}^{1}\vdash\mathsf{tick}(1,x)\dblcolon\mathsf{bool}$ (but not $x:{\mathsf{bool}}^{1}\vdash\mathsf{tick}(1,x)\dblcolon{\mathsf{bool}}^{1}$).

The typing rules of $\mathrm{Re}^{2}$ form an affine type system (Walker, 2002). To use a program variable multiple times, we have to introduce explicit sharing to ensure that the program cannot gain potential. The sharing judgment $\Gamma\vdash S\mathrel{\curlyveedownarrow}S_{1}\mid S_{2}$ means that in the context $\Gamma$, the potential indicated by $S$ is apportioned into two parts to be associated with $S_{1}$ and $S_{2}$. We extend this notion to context sharing, written $\vdash\Gamma\mathrel{\curlyveedownarrow}\Gamma_{1}\mid\Gamma_{2}$, which states that $\Gamma_{1},\Gamma_{2}$ has the same sequence of bindings as $\Gamma$, but the potentials of type bindings in $\Gamma$ are shared point-wise, and the free potentials in the $\Gamma$ are also split. A special context sharing $\vdash\Gamma\mathrel{\curlyveedownarrow}\Gamma\mid\Gamma$ is used in the typing rules (T-Abs) and (T-Fix) for functions. The self-sharing indicates that the function can only reference potential-free free variables in the context. This is also used to ensure that the program cannot gain more potential through free variables by applying the same function multiple times.

Restricting functions to be defined under potential-free contexts is undesirable in some situations. For example, a curried function of type $x{\,:\,}T_{x}\rightarrow y{\,:\,}T_{y}\rightarrow T$ might require nonzero units of potential on its first argument $x$, which is not allowed by rule (T-Abs) or (T-Fix) on the inner function type $y{\,:\,}T_{y}\rightarrow T$. We introduce another rule (T-Abs-Lin) to relax the restriction. The rule associates a multiplicity $m$ with the function type, which denotes the number of times that the function could be applied. Instead of context self-sharing, we require the potential in the context to be enough for $m$ function applications. Note that in ReSyn’s surface syntax used in the Sec. 2, every curried function type implicitly has multiplicity 1 on the inner function: $x{\,:\,}T_{x}\rightarrow{1}\cdot(y{\,:\,}T_{y}\rightarrow T)$.

Example

Recall the function triple from Fig. 3, which can be written as follows in $\mathrm{Re}^{2}$ core syntax:

[TABLE]

Next, we illustrate how $\mathrm{Re}^{2}$ uses the signature of append:

[TABLE]

to justify the resource bound $2|\ell|$ on triple. Suppose $\Gamma$ is a typing context that contains the signature of append. The argument $\ell$ is used three times, so we need to use sharing relations to apportion the potential of $\ell$. We have $\Gamma\vdash L({\mathsf{bool}}^{2})\mathrel{\curlyveedownarrow}L({\mathsf{bool}}^{1})\mid L({\mathsf{bool}}^{1})$, $\Gamma\vdash L({\mathsf{bool}}^{1})\mathrel{\curlyveedownarrow}L({\mathsf{bool}}^{1})\mid L({\mathsf{bool}}^{0})$, and we assign $L({\mathsf{bool}}^{1})$, $L({\mathsf{bool}}^{0})$, and $L({\mathsf{bool}}^{1})$ to the three occurrences of $\ell$ respectively in the order they appear in the program. To reason about ${e_{1}=\mathsf{app}(\mathsf{app}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{append}}}}}},\ell),\ell)$, we instantiate append with $\alpha\mapsto{\mathsf{bool}}^{0}$, inferring its type as

[TABLE]

We then can typecheck ${e_{2}=\mathsf{app}(\mathsf{app}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{append}}}}}},\ell),\ell^{\prime})$ with the same instantiation of append:

[TABLE]

(where $T_{1}$ is the type of $e_{1}$). Finally, by subtyping and the following valid judgment in the refinement logic

[TABLE]

we conclude ${\Gamma\vdash\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{triple}}}}}}\dblcolon\ell{\,:\,}L({\mathsf{bool}}^{2})\rightarrow\{L(\mathsf{bool})\mid\nu=3\times\ell\}$.

Soundness

The type soundness for $\mathrm{Re}^{2}$ is based on progress and preservation. The progress theorem states that if we derive a bound $q$ for an expression $e$ with the type system and $p\geq q$ resources are available, then $\langle e,p\rangle$ can make a step if $e$ is not a value. In this way, progress shows that resource bounds are indeed bounds on the high-water mark of the resource usage since states $\langle e,p\rangle$ in the small step semantics can be stuck based on resource usage if, for instance, $p=0$ and $e=\mathsf{tick}(1,e^{\prime})$.

Theorem 1 (Progress).

If $q\vdash e\dblcolon S$ and $p\geq q$, then either $e\in\mathsf{Val}$ or there exist $e^{\prime}$ and $p^{\prime}$ such that $\langle e,p\rangle\mapsto\langle e^{\prime},p^{\prime}\rangle$.

Proof.

By strengthening the assumption to $\Gamma\vdash e\dblcolon S$ where $\Gamma$ is a sequence of type variables and free potentials, and then induction on $\Gamma\vdash e\dblcolon S$. ∎

The preservation theorem accounts for resource consumption by relating the left over resources after a computation to the type judgment of the new term.

Theorem 2 (Preservation).

If $q\vdash e\dblcolon S$, $p\geq q$ and $\langle e,p\rangle\mapsto\langle e^{\prime},p^{\prime}\rangle$, then $p^{\prime}\vdash e^{\prime}\dblcolon S$.

Proof.

By strengthening the assumption to $\Gamma\vdash e\dblcolon S$ where $\Gamma$ is a sequence of free potentials, and then induction on $\Gamma\vdash e\dblcolon S$, followed by inversion on the evaluation judgment $\langle e,p\rangle\mapsto\langle e^{\prime},p^{\prime}\rangle$. ∎

The proof of preservation makes use of the following crucial substitution lemma.

Lemma 0 (Substitution).

If $\Gamma_{1},x:{\{B\mid\psi\}}^{\phi},\Gamma^{\prime}\vdash e\dblcolon S$, $\Gamma_{2}\vdash t\dblcolon{\{B\mid\psi\}}^{\phi}$, $t\in\mathsf{Val}$ and $\vdash\Gamma\mathrel{\curlyveedownarrow}\Gamma_{1}\mid\Gamma_{2}$, then $\Gamma,[\mathcal{I}(t)/x]\Gamma^{\prime}\vdash[t/x]e\dblcolon[\mathcal{I}(t)/x]S$.

Proof.

By induction on $\Gamma_{1},x:{\{B\mid\psi\}}^{\phi},\Gamma^{\prime}\vdash e\dblcolon S$. ∎

Since we found the purely syntactic soundness statement about results of computations (they are well-typed values) somewhat unsatisfactory, we also introduced a denotational notation of consistency. For example, a list of values $\ell=[v_{1},\cdots,v_{n}]$ is consistent with $q\vdash\ell\dblcolon{L(\{\mathsf{bool}\mid\neg\nu\})}^{\nu+5}$, if $q\geq n+5$ and each value $v_{i}$ of the list is $\mathsf{false}$. We then show that well-typed values are consistent with their typing judgement.

Lemma 0 (Consistency).

If $q\vdash v\dblcolon S$, then $v$ satisfies the conditions indicated by $S$ and $q$ is greater than or equal to the potential stored in $v$ with respect to $S$.

As a result, we derive the following theorem.

Theorem 5 (Soundness).

If $q\vdash e\dblcolon S$ and $p\geq q$ the either

• •

$\langle e,p\rangle\mapsto^{*}\langle v,p^{\prime}\rangle$ and $v$ is consistent with $p^{\prime}\vdash v\dblcolon S$ or

• •

for every $n$ there is $\langle e^{\prime},p^{\prime}\rangle$ such that $\langle e,p\rangle\mapsto^{n}\langle e^{\prime},p^{\prime}\rangle$.

Complete proofs can be found in Appendix D.

Inductive Datatypes and Measures

We can generalize our development of list types for inductive types $\mu X.\overrightarrow{C:T\times X^{k}}$, where $C$ is the constructor name, $T$ is the element type that does not contain $X$, and $X^{k}$ is the $k$-element product type $X\times X\times\cdots\times X$. The introduction rules and elimination rules are almost the same as (T-Nil), (T-Cons) and (T-MatL), respectively, except that we need to capture inductive invariants for each constructor $C$ in the rules correspondingly. In Synquid, these invariants are specified by inductive measures that map values to refinements. We can introduce new sorting rules for inductive types to embed values as their related measures in the refinement logic.

Constant Resource

Our type system infers upper bounds on resource usage. Recently, AARA has been generalized to verify constant-resource behavior (Ngo et al., 2017). A program is said to be constant-resource if its executions on inputs of the same size consume the same amount of resource. We can adapt the technique in (Ngo et al., 2017) to $\mathrm{Re}^{2}$ by

(i) changing the subtyping rules to keep potentials invariant (i.e. replacing $\geq$ with $=$ in (Sub-TVar), (Sub-Arrow), (Sub-Pot)), and

(ii) changing the rule (Simp-Atom-Var) to require $\phi=0$.

Based on the modified type system, our synthesis algorithm can also synthesize constant-time implementations (see Sec. 5.2 for more details).

4. Type-Driven Synthesis with $\mathrm{Re}^{2}$

In this section, we first show how to turn the type checking rules of $\mathrm{Re}^{2}$ into synthesis rules, and then leverage these rules to develop a synthesis algorithm.

4.1. Synthesis Rules

Extended Syntax

To express synthesis rules, we extend $\mathrm{Re}^{2}$ with a new syntactic form $\mathring{e}$ for expression templates. As shown in Fig. 7, templates are expressions that can contain holes $\circ$ in certain positions. The flat let form $\mathsf{lets}(D.\mathring{e})$, where $D$ is a sequence of bindings, is a shortcut for a nest of let-expressions $\mathsf{let}(x_{1},d_{1}.\ldots\mathsf{let}(x_{n},d_{n}.\mathring{e}))$; we write $\mathsf{fold}(\mathsf{lets}(D.e))$ to convert a flat let (without holes) back to the original syntax. We also extend the language of types with an unknown type $\mathsf{?}$, which is used to build partially defined goal types, as explained below.

Synthesis for A-Normal-Form

Our synthesis relation consists of two mutually recursive judgments: the synthesis judgment $\Gamma\vdash\mathring{e}\dblcolon S\rightsquigarrow e$ intuitively means that the template $\mathring{e}$ can be completed into an expression $e$ such that $\Gamma\vdash e\dblcolon S$; the purpose of the auxiliary atomic synthesis judgment is explained below. Selected rules for both judgments are given in Fig. 8; the full technical development can be found in Appendix E.

The synthesis rule (Syn-Gen) handles polymorphic goal types. The rules (Syn-Fix) and (Syn-Abs) handle arrow types and derive either a fixpoint term or an abstraction. The rule (Syn-Imp) derives $\mathsf{impossible}$ in an inconsistent context (which may arise e.g. in a dead branch of a pattern match). The rest of the rules handle the common case when the goal type $T$ is scalar and the context is consistent; in this case the target expression can be either a conditional, a match, or an E-term (Polikarpova et al., 2016), i.e. a term made of variables, applications, and constructors. Special care must be taken to ensure that these expressions are in a-normal-form: generally, a-normalizing an expression requires introducing fresh variables and let-bindings for them. To retain completeness, our synthesis rules need to do the same: intuitively, in addition to an expression $e$, a rule might also need to produce a sequence of let-bindings $D$ that define fresh variables in $e$. To this end, we introduce the atomic synthesis judgment $\Gamma\vdash\mathring{e}\dblcolon T\overset{a}{\rightsquigarrow}\mathsf{lets}(D.a)$, which synthesizes normalized E-terms, where $a$ is an atom and each definition in $D$ is an application or a constructor in a-normal-form.

As an example, consider the rule (Syn-Cond) for synthesizing conditionals: ideally, we would like to synthesize a guard $e$ of type $\mathsf{bool}$, and then synthesize the two branches under the assumptions that $e$ evaluates to $\mathsf{true}$ and $\mathsf{false}$, respectively. Recall, however, that the guard must be atomic; hence, to synthesize a well-formed conditional, we use atomic synthesis to produce a guard $\mathsf{lets}(D.x)$. Now to get a well-scoped program we must place the whole conditional inside the bindings $D$; to that end, the second premise of (Syn-Cond) uses a nontrivial template $\mathsf{lets}(D.\mathsf{if}(x,\circ,\circ))$. The rules (Fill-Let) and (Fill-Cond) handle this template by integrating it into the typing context and exposing the hole; along the way (Fill-Let) takes care of context sharing, which accounts for the potential consumed by the definitions in $D$. Synthesis of matches works similarly using (Syn-MatL) and (Fill-MatL).

Atomic Synthesis

The first four rules of atomic synthesis generate a simple atom if its type matches the goal; the rest of the rules deal with the hardest part: normalized applications. Consider the rule (ASyn-App): given a goal type $T$ for the application $\mathsf{app}(e_{1},e_{2})$, we need to construct goal types for $e_{1}$ and $e_{2}$, to avoid enumerating them blindly. Following Synquid’s round-trip type checking idea, we use the type $\_{\,:\,}\mathsf{?}\rightarrow T$ as the goal for $e_{1}$ (i.e. a function from unknown type to $T$). The subtyping rules for $\mathsf{?}$ are such that $\Gamma\vdash(y{\,:\,}T_{1}\rightarrow T_{2})<:(\_{\,:\,}\mathsf{?}\rightarrow T)$ holds if $T_{2}$ and $T$ agree in shape and those refinements that do not mention $y$; hence this goal type filters out those functions $e_{1}$ that cannot fulfill the desired goal type $T$, independently of the choice of $e_{2}$. One difference with Synquid is that the goal type for $e_{1}$ is linear, reflecting that we intend to use $e_{1}$ only once and allowing it to capture positive potential.

Similarly to the conditional case explained above, the synthesized left-hand side of the application, $e_{1}$, has the form $\mathsf{lets}(D_{1}.x)$, and the argument $e_{2}$ must be synthesized inside the bindings $D_{1}$. These bindings are processed by (AFill-Let), and the actual argument synthesis happens in either (AFill-App) or (AFill-SimpAtom), depending on whether the argument type is a scalar. The former corresponds to a higher-order application: here $T_{1}$ is an arrow type, and hence the argument cannot occur in the function’s return type; in this case, synthesizing an expression of type $T_{1}$ must yield an abstraction or fixpoint (since $T_{1}$ is an arrow), both of which are atoms. The latter corresponds to a first-order application: here the return type $T^{\prime}$ can mention $y$, so after synthesizing an argument of type $T_{y}$, we still need to check whether the resulting application $\mathsf{lets}(D.\mathsf{app}(x,a))$ has the right type $T$. Note how both (AFill-App) or (AFill-SimpAtom) return normalized E-terms by generating a fresh variable and binding it to an application.

Cost Metrics

In the context of synthesis we cannot rely on programmer-written $\mathsf{tick}$ terms to model cost. Instead in our formalization we use a simple cost metric where each function application consumes one unit of resource; hence every application generated by (AFill-App) or (AFill-SimpAtom) is wrapped in $\mathsf{tick}(1,\cdot)$. Our implementation provides more flexibility and allows the programmer to annotate any arrow type with a non-negative cost $c$ to denote that applying a function of this type should incur cost $c$.

Soundness

The synthesis rules always produce a well-typed expression (proof can be found in Appendix F).

Theorem 1 (Soundness of Synthesis).

If $\Gamma\vdash\circ\dblcolon S\rightsquigarrow e$ then $\Gamma\vdash e\dblcolon S$.

4.2. Synthesis Algorithm

In this section we discuss how to turn the declarative synthesis rules of Sec. 4.1 into a synthesis algorithm, which takes as input a goal type $S$, a context $\Gamma$, and a bound $k$ on the program depth, and either returns a program $e$ of depth at most $k$ such that $\Gamma\vdash e\dblcolon S$, or determines that no such program exists. The core algorithm follows the recipe from prior work on type-driven synthesis (Polikarpova et al., 2016; Osera and Zdancewic, 2015) and performs a fairly standard goal-directed backtracking proof search with $\Gamma\vdash\circ\dblcolon e\rightsquigarrow S$ as the top-level goal. In the rest of this section, we explain how to make such proof search feasible by reducing the core sources of non-determinism to constraint solving.

Typing constraints

The main sources of non-determinism in a synthesis derivation stem from the following premises of synthesis and typing rules:

(1) whenever a given context $\Gamma$ is shared as $\Gamma\vdash\Gamma\mathrel{\curlyveedownarrow}\Gamma_{1}\mid\Gamma_{2}$, we need to guess how to apportion potential annotations in $\Gamma$;

(2) whenever potential in a given context $\Gamma$ is transfered, we need to guess potential annotations in $\Gamma^{\prime}$ such that $\Phi(\Gamma)=\Phi(\Gamma^{\prime})$; and finally

(3) whenever ${\{B\mid\psi\}}^{\phi}$ is used to instantiate a type variable, we need to guess both $\phi$ and $\psi$.

All three amount to inference of unknown refinement terms of either Boolean or numeric sort. To infer these terms efficiently, we use the following constraint-based approach. First, we build a symbolic synthesis derivation, which may contain unknown refinement terms $U^{\Delta}_{\Gamma}$, and collect all subtyping, sharing, and transfer premises from the derivation into a system of typing constraints. Here $\Delta$ records the desired sort of the unknown refinement term, and $\Gamma$ records the context in which it must be well-formed. A solution to a system of typing constraints, is a map $\mathcal{L}:U\to\psi$ such that for every unknown $U^{\Delta}_{\Gamma}$, $\Gamma\vdash\mathcal{L}(U)\in\Delta$ and substituting $\mathcal{L}(U)$ for $U$ within the typing constraints yields valid subtyping, sharing, and transfer judgments.

Constraint Solving

To solve typing constraints, the algorithm first transforms them into validity constraints of one of two forms: $\Gamma\models\psi\implies\psi^{\prime}$ or $\Gamma\models\phi\geq 0$; the interesting cases of this translation are shown in Fig. 9. Then, using the definition of validity (Appendix B), we further reduce these into a system of:

1. (1)

Horn constraints of the form $\psi_{1}\wedge\ldots\wedge\psi_{n}\implies\psi_{0}$, and 2. (2)

resource constraints of the form $\psi_{1}\wedge\ldots\wedge\psi_{n}\implies\phi\geq 0$.

Here any $\psi_{i}$ can be either a Boolean unknown $U^{\mathbb{B}}_{\Gamma}$ or a known refinement term, and $\phi$ is a sum of zero or more numeric unknowns $U^{\mathbb{N}}_{\Gamma}$ and a known (linear) refinement term. While prior work has shown how to efficiently solve Horn constraints using predicate abstraction (Rondon et al., 2008; Polikarpova et al., 2016), resource constraints present a new challenge, since they contain unknown terms of both Boolean and numeric sorts. In the interest of efficiency, our synthesis algorithm does not attempt to solve for both Boolean and numeric terms at the same time. Instead, it uses existing techniques to find a solution for the Horn constraints, and then plugs this solution into the resource constraints. Note that this approach does not sacrifice completeness, as long as the Horn solver returns the least-fixpoint (i.e. strongest) solution for each $U^{\mathbb{B}}_{\Gamma}$, since Boolean unknowns only appear negatively in resource constraints444Our implementation uses Synquid’s default greatest-fixpoint Horn solver, which technically renders this technique incomplete, however we observed that it works well in practice..

Resource Constraints

The main new challenge then is to solve a system of resource constraints of the form $\psi\implies\phi\geq 0$, where $\psi$ is now a known formula of the refinement logic. Since potential annotations in $\mathrm{Re}^{2}$ are restricted to linear terms over program variables, we can replace each unknown term $U^{\mathbb{N}}_{\Gamma}$ in $\phi$ with a linear template $\sum_{x\in X}C_{i}\cdot x$, where each $C_{i}$ is an unknown integer coefficient and $X$ is the set of all variables in $\Gamma$ such that $\Gamma\vdash x\in\mathbb{N}$. After normalization, the system of resource constraints is reduced to the following doubly-quantified system of linear inequalities:

[TABLE]

where each clause $r$ is of the form $\psi(\overrightarrow{x})\implies\sum f(\overrightarrow{C_{i}})\cdot x\geq 0$, $\psi$ is a known formula over the program variables $\overrightarrow{x}$, and each $f$ is a linear function over unknown integer coefficients $\overrightarrow{C_{i}}$.

Note a crucial difference between these constraints and those generated by RaML: since RaML’s potential annotations are not dependent—i.e. $r$ cannot mention program variables $\overrightarrow{x}$—its resource constraints reduce to plain linear inequalities: $\overrightarrow{\exists C_{i}}.\bigwedge\sum C_{i}\geq c$ (where $c$ is a known constant), which can be handled by an LP solver. In our case, the challenge stems both from the double quantification and the fact that individual clauses $r$ are bounded by formulas $\psi$, which are often nontrivial. For example, synthesizing the function range from Sec. 2 gives rise to the following (simplified) resource constraints:

[TABLE]

where a solution only exists if the bounds are taken into account. One solution is $[C_{0}\mapsto-1,C_{1}\mapsto 0,C_{2}\mapsto 1,C_{3}\mapsto 0]$, which stands for the potential term $\nu-a$.

Incremental Solving

Constraints of this form can be solved using counter-example guided synthesis (CEGIS) (Solar-Lezama et al., 2006), which is, however, relatively expensive. We observe that in the context of synthesis we have to repeatedly solve similar systems of resource constraints because a program candidate is type-checked incrementally as it is being constructed, which corresponds to an incrementally growing set of clauses $R$. Moreover, we observe that as new clauses are added, only a few existing coefficients $C_{i}$ are typically invalidated, so we can avoid solving for all the coefficients from scratch. To this end, we develop an incremental version of the CEGIS algorithm, shown in Algorithm 1.

The goal of the algorithm is to find a solution $\mathcal{C}:C_{i}\to\mathbb{Z}$ that maps unknown coefficients to integers such that $\overrightarrow{\forall x}.R(\mathcal{C},\overrightarrow{x})$ holds (we write $R(\mathcal{C},\overrightarrow{x})$ as a shorthand for $\bigwedge_{r\in R}r(\mathcal{C},\overrightarrow{x})$). The algorithm takes as input a set of clauses $R$ (which includes both old and new clauses), the current solution $\mathcal{C}$ (new coefficients $C_{i}$ are mapped to 0) and the current set of examples $\mathcal{E}$, where an example $e\in\mathcal{E}$ is a partial assignment to universally-quantified variables $e:X\to\mathbb{N}$.

The algorithm first queries the SMT solver for a counter-example $e$ to the current solution. If no such counter-example exists, the solution is still valid (this happens surprisingly often, since many resource constraints are trivial). Otherwise, the current solution needs to be updated. To this end, a traditional CEGIS algorithm would query the SMT solver with the following synthesis constraint: $\exists\overrightarrow{C_{i}}.\bigwedge_{e\in\mathcal{E}^{\prime}}\ R(\overrightarrow{C_{i}},e)$, which enforces that all clauses are satisfied on the extended set of examples. Instead, our incremental algorithm picks out only those clauses $R^{\prime}$ that are actually violated by the new counter-example; since in our setting $R^{\prime}$ is typically small, this optimization significantly reduces the size of the synthesis constraint and synthesis times for programs with dependent annotations (as we demonstrate in Sec. 5).

4.3. Implementation

We implemented the resource-guided synthesis algorithm in ReSyn, which extends Synquid with support for resource-annotated types and a resource constraint solver. Note that while our formalization is restricted to Booleans and length-indexed lists, our implementation supports the full expressiveness of Synquid’s types: types include integers and user-defined algebraic datatypes, and refinement formulas support sets and can mention arbitrary user-defined measures. More importantly, resource terms in ReSyn can mention integer variables and use subtraction, multiplication, conditional expressions, and numeric measures; finally, multiplicities on type variables can be dependent (mention variables). These changes have the following implications:

(1) resource terms are not syntactically guaranteed to be non-negative, so we emit additional well-formedness constraints to enforce this;

(2) resource terms are not syntactically restricted to be linear; our implementation is incomplete, and simply rejects the program if a nonlinear term arises;

(3) subtyping and sharing constraints with conditional resource terms are decomposed into unconditional ones by moving the guard to the context, so the search space for all numeric unknowns remains unconditional;

(4) to handle measure applications in resource constraints, we replace them with fresh integer variables, and avoid spurious counter-examples by explicitly instantiating the congruence axiom with all applications in the constraint.

5. Evaluation

We evaluated ReSyn using the following criteria:

**: **

Relative performance: How do ReSyn’s synthesis times compare to Synquid’s? How much does the additional burden of solving resource constraints affect its performance?

**: **

Efficacy of resource analysis: Can ReSyn discover more efficient programs than Synquid?

**: **

Value of round-trip type checking: Does round-trip type checking afforded by the tight integration of resource analysis into Synquid effective at pruning the search space? How does it compare to the naive combination of synthesis and resource analysis?

**: **

Value of incremental solving: To what extent does incremental solving of resource constraints improve ReSyn’s performance?

5.1. Relative Performance

To evaluate ReSyn’s performance relative to Synquid, we selected 43 problems from Synquid’s original suite, annotated them with resource bounds, and re-synthesized them with ReSyn. The rest of the original 64 benchmarks require non-linear bounds, and thus are out of scope of $\mathrm{Re}^{2}$. The details of this experiment are shown in Tab. 1, which compares ReSyn’s synthesis times against Synquid’s on these linear-bounded benchmarks.

Unsurprisingly, due to the additional constraint-solving, ReSyn generally performs worse than Synquid: the median synthesis time is about $2.5\times$ higher. Note, however, that in return it provides provable guarantees about the performance of generated code. ReSyn was able to discover a more efficient implementation for only one of the original Synquid benchmarks (compress, discussed below). In general, these benchmarks contain only the minimal set of components required to produce a valid implementation, which makes it hard for Synquid to find a non-optimal version. Four of the benchmarks in Tab. 1 use advanced features of $\mathrm{Re}^{2}$: for example, any function using natural numbers to index or construct a data structure requires dependent potential annotations.

5.2. Case Studies

The value of resource-guided synthesis becomes clear when the library of components grows. To confirm this intuition, we assembled a suite of 16 case studies shown in Tab. 2, each exemplifying some feature of ReSyn.

Optimization

The first six benchmarks showcase ReSyn’s ability to generate faster code than Synquid (the cost metric in each case is the number of recursive calls). Benchmark 1 is triple from Sec. 2.3, where both Synquid and ReSyn generate the same efficient solution; benchmark 2 is slight modification of this example: it uses a component append’, which traverses its second argument (unlike append, which traverses its first). In this case, ReSyn generates the efficient solution, associating the two calls to append’ to the left, while Synquid still generates the same—now inefficient—solution, associating these calls to the right. In benchmark 3 ReSyn makes the optimal choice of accumulator to avoid a quadratic-time implementation. Benchmark 4 is compress from Tab. 1: the task is to remove adjacent duplicated from a list. Here Synquid makes an unnecessary recursive call, resulting in a solution that is slightly shorter but runs in exponential time!

In other cases, ReSyn drastically changes the structure of the program to find an optimal implementation. Benchmark 5 is common from Sec. 2.1, where ReSyn must find an implementation that does not call member. Benchmark 6 works similarly, but computes the difference between two lists instead of their intersection. On these benchmarks, the performance disparity between ReSyn and Synquid is much worse, as ReSyn must reject many more programs before it finds an appropriate implementation. On the other hand, these benchmarks also showcase the value of round-trip type checking: the column T-EAC reports synthesis times for a naive combination of synthesis and resource analysis, where we simply ask Synquid to enumerate functionally correct programs until one type-checks under $\mathrm{Re}^{2}$. As you can see, for benchmarks 5 and 6 this naive version times out after ten minutes.

Dependent Potentials

Benchmarks 7–13 showcase fine-grained bounds that leverage dependent potential annotations. The first three of those synthesize a function insert that inserts an element into a sorted list. In benchmark 7 we use a simple linear bound (the length of the list), while benchmarks 8 and 9 specify a tighter bound: insert x xs can only make one recursive call per element of xs larger than x. These two examples showcase two different styles of specifying precise bounds: in 8 we define a custom measure numgt that counts list elements greater than a certain value; in 9, we instead annotate each list element with a conditional term indicating that it carries potential only if its value is larger than x. As discussed in Sec. 2, benchmark 13 (range) cannot be synthesized by Synquid at all, because of restrictions on its termination checking mechanism, while ReSyn handles this benchmark out of the box.

For benchmarks 8–13, which make use of dependent potential annotations, we also report the synthesis times without incremental solving of resource constraints (T-NInc), which are up to $2\times$ higher.

Constant Resource

As discussed in Sec. 3, a simple extension to $\mathrm{Re}^{2}$ enables it to verify constant-resource implementations. We showcase this feature in benchmarks 14–16. Benchmark 15 is an example from (Ngo et al., 2017), which compares a public list $ys$ with a secret list $zs$. By allotting potential only to $ys$, we guarantee that the resource consumption of the generated program is independent of the length of $zs$. If this requirement is relaxed (as in benchmark 16), the generated program indeed terminates early, potentially revealing the length of $zs$ to an adversary (in case $zs$ is the shorter of the two lists). Benchmark 14 is a constant-time version of benchmark 7 (insert), which is forced to make extra recursive calls so as not to reveal the length of the list.

6. Related Work

Resource Analysis

Automatic static resource analysis has been extensively studied and is an active area of research. Many advanced techniques for imperative integer programs apply abstract interpretation to generate numerical invariants. The obtained size-change information forms the basis for the computation of actual bounds on loop iterations and recursion depths; using counter instrumentation (Gulwani et al., 2009), ranking functions (Alias et al., 2010; Albert et al., 2011; Brockschmidt et al., 2014; Sinn et al., 2014), recurrence relations (Albert et al., 2012b, a), and abstract interpretation itself (Zuleger et al., 2011; Cerný et al., 2015b). Automatic resource analysis techniques for functional programs are based on sized types (Vasconcelos, 2008), recurrence relations (Danner et al., 2012), term-rewriting (Avanzini et al., 2012), and amortized resource analysis (Hofmann and Jost, 2003; Jost et al., 2010; Hoffmann et al., 2011; Simões et al., 2012). There exist several tools that can automatically derive loop and recursion bounds for imperative programs including SPEED (Gulwani et al., 2009; Gulwani and Zuleger, 2010), KoAT (Brockschmidt et al., 2014), PUBS (Albert et al., 2012a), Rank (Alias et al., 2010), ABC (Blanc et al., 2010) and LOOPUS (Zuleger et al., 2011; Sinn et al., 2014). These techniques are passive in the sense that they provide feedback about a program without actively synthesizing or repairing programs.

Domain-Specific Program Synthesis

Most program synthesis techniques (Osera and Zdancewic, 2015; Feser et al., 2015; Smith and Albarghouthi, 2016; Feng et al., 2017a; Feng et al., 2017b, 2018; Wang et al., 2018, 2017; Srivastava et al., 2010; Kneuss et al., 2013; Polikarpova et al., 2016; Inala et al., 2017; Qiu and Solar-Lezama, 2017) do not explicitly take resource usage into account during synthesis. Many of them, however, leverage domain knowledge to restrict the search space to only include efficient programs (Gulwani et al., 2011; Cheung et al., 2013) or to encode domain-specific performance considerations as part of the functional specification (Inala et al., 2016; Loncaric et al., 2016, 2018).

Synthesis with Quantitative Objectives

Two lines of prior work on synthesis are explicitly concerned with optimizing resource usage. One is quantitative automata-theoretic synthesis, which has been used to synthesize optimal Mealy machines (Bloem et al., 2009) and place synchronization in concurrent programs (Cerný et al., 2011; Gupta et al., 2015; Cerný et al., 2015a). In contrast, we focus on synthesis of high-level programs that can manipulate custom data structures, which are out of reach for automata-theoretic synthesis.

The second relevant line of work is synthesis-aided compilation (Schkufza et al., 2013; Phothilimthana et al., 2014; Sharma et al., 2015; Phothilimthana et al., 2016). This work is limited to generating low-level straight-line code, which is an easy target for correctness validation and cost estimation. Perhaps the closest work to ours is the Synapse tool (Bornholt et al., 2016), which supports a richer space of programs, but requires extensive guidance from the user (in the form of meta-sketches), and relies on bounded reasoning, which can only provide correctness and optimality guarantees for a finite set of inputs. In contrast, we use type-based verification and resource analysis techniques, which enable ReSyn to handle high-level recursive programs and provide guarantees for an unbounded set of inputs.

Acknowledgements.

This article is based on research supported by the United States Air Force under DARPA AA Contract FA8750-18-C-0092 and DARPA STAC Contract FA8750-15-C-0082, and by the National Science Foundation under SaTC Award 1801369, SHF Award 1812876, and CAREER Award 1845514. Any opinions, findings, and conclusions contained in this document are those of the authors and do not necessarily reflect the views of the sponsoring organizations.

Appendix A The $\mathrm{Re}^{2}$ Type System

A.1. Scalar Types: $S~{}\mathsf{scalar}$

In $\mathrm{Re}^{2}$, we define scalar types to be annotated subset types.Neither arrow types nor type schemas are scalar.

{mathpar}\inferrule

${\{B\mid\psi\}}^{\phi}~{}\mathsf{scalar}$

A.2. Sorting: $\Gamma\vdash\psi\in\Delta$

Refinements are classified by sorts. The sorting judgment $\Gamma\vdash\psi\in\Delta$ states that a refinement $\psi$ has a sort $\Delta$ under a context $\Gamma$. The typing context is needed because refinements can reference program variables. To reflect types of program variables in the refinement level, we define a relation $S\rightsquigarrow\Delta$ as follows. The relation $\rightsquigarrow$ defines a partial function from types to sorts.

{mathpar}\inferrule

${\{\mathsf{bool}\mid\psi\}}^{\phi}$ ↝$\mathbb{B}$ \inferrule ${\{L(T)\mid\psi\}}^{\phi}$ ↝$\mathbb{N}$ \inferrule ${\{m\cdot\alpha\mid\psi\}}^{\phi}$ ↝δ_α

Fig. 11 presents the sorting rules.

A.3. Type Wellformedness: $\Gamma\vdash S~{}\mathsf{type}$

A type $S$ is said to be wellformed under a context $\Gamma$ if the following three properties hold:

• •

every referenced program variables in $S$ is in the correct scope, and

• •

polymorphic types can never carry positive potential.

Fig. 12 presents the type wellformedness rules.

Recall that when we defined sorting rules we proposed a relation $S\rightsquigarrow\Delta$ that is a partial function from types to sorts. With wellformed types, we can interpret $\rightsquigarrow$ as a better-behaved map.

Proposition 1.

The relation $S\rightsquigarrow\Delta$ defines a total map from wellformed scalar types into sorts, i.e., if $\Gamma\vdash S~{}\mathsf{type}$ and $S~{}\mathsf{scalar}$, then there exists a unique $\Delta$ such that $S\rightsquigarrow\Delta$.

Proof.

By induction on $\Gamma\vdash S~{}\mathsf{type}$. ∎

A.4. Context Wellformedness: $\vdash\Gamma~{}\mathsf{context}$

A context $\Gamma$ is said to be wellformed if every binding in $\Gamma$ is wellformed under a “prefix” context before it. Recall that the context is a sequence of variable bindings, type variables, path conditions, and free potentials. Fig. 13 shows these rules.

A.5. Context Sharing: $\vdash\Gamma\mathrel{\curlyveedownarrow}\Gamma_{1}\mid\Gamma_{2}$

We have already presented type sharing rules. To apportion the associated potential of $\Gamma$ properly to two contexts $\Gamma_{1},\Gamma_{2}$ with the same sequence of bindings, we introduce context sharing relations. The rules are summarized in Fig. 14.

A.6. Total Free Potential: $\Phi(\Gamma)$

The free potentials of a context $\Gamma$, written $\Phi(\Gamma)$, include all the potential bindings, as well as outermost annotated potentials of variable bindings.

[TABLE]

A.7. Type Substitution: $[{\{B\mid\psi\}}^{\phi}/\alpha]S$

In $\mathrm{Re}^{2}$, type substitution is restricted to resource-annotated subset types. The substitution $[{\{B\mid\psi\}}^{\phi}/\alpha]S$ should take care of logical refinements and potential annotations from both $S$ and ${\{B\mid\psi\}}^{\phi}$. Following gives the definition.

[TABLE]

Type multiplication is defined as follows.

[TABLE]

Appendix B Validity Checking in $\mathrm{Re}^{2}$

In this section, we define the validity checking judgment $\Gamma\models\psi$ where $\Gamma$ is a wellformed context and $\psi$ is a Boolean-sorted refinement. Intuitively, the judgment states that the formula $\psi$ is always true under any instance of $\Gamma$. Our approach is to define a set-based denotational semantics for refinements and then reduce the validity checking in $\mathrm{Re}^{2}$ to Presburger arithmetic.

Semantics of Sorts

A sort $\Delta$ represents a set $\llparenthesis\Delta\rrparenthesis$ of $\Delta$-sorted refinements. The following gives the definition of $\llparenthesis\Delta\rrparenthesis$. Note that we only define the semantics for sorts that do not contain uninterpreted sorts. We denote such sorts by $\Delta_{o}$, defined as $\{\mathbb{B},\mathbb{N}\}$.

[TABLE]

Semantics of Types

As we have already done in the sorting rules, scalar types are reflected in the refinement level. To interpret a wellformed scalar type as a sort without uninterpreted sorts, we define a transformation $\mathcal{T}_{E}(\cdot)$ from types to sorts, parametrized by an environment that resolves uninterpreted sorts $\delta_{\alpha}$.

[TABLE]

Semantics of Contexts

To give a meaning to a context $\Gamma$, we need to assign an instance for each variable binding with a scalar type, as well as type variables. Intuitively, a context $\Gamma$ represents a set of environments that resolves both program variables and uninterpreted sorts. Making use of semantics for sorts and types defined above, we can define $\llparenthesis\Gamma\rrparenthesis$ inductively as follows.

[TABLE]

Semantics of Refinements

The meaning of a refinement $\psi$ is defined with respect to its sorting judgment $\Gamma\vdash\psi\in\Delta$. The following defines an evaluation map $\llbracket\psi\rrbracket:\llparenthesis\Gamma\rrparenthesis\to\llparenthesis\Delta\rrparenthesis$, by induction on the derivation of the sorting judgment, or essentially structural induction on $\psi$.

[TABLE]

Validity Checking

Now we show how to assign meanings to contexts and refinements, then the last step to define $\Gamma\models\psi$ is to collect all the refinement constraints mentioned in $\Gamma$.

We first define how to extract constraints from a type binding. Note that only scalar types (i.e., subset types) can carry logical refinements.

[TABLE]

Then we define $\mathscr{B}(\Gamma)$ to collect all the constraints from variable bindings and path conditions in $\Gamma$. It is defined inductively on $\Gamma$.

[TABLE]

Now we can define the validity checking judgment $\Gamma\models\psi$.

[TABLE]

Further, we can embed our denotational semantics for refinements in Presburger arithmetic, so we can also write the validity checking as the following formula

[TABLE]

where $\models$ is interpreted in Presburger arithmetic.

Appendix C Definition of Consistency for $\mathrm{Re}^{2}$

To describe soundness of $\mathrm{Re}^{2}$, we will need a notion of consistency. Basically, given a typing judgment $\Gamma\vdash v\dblcolon S$ of a value, we want to know that under the context $\Gamma$, $v$ satisfies the logical conditions indicated by $S$, as well as $\Gamma$ has sufficient amount of potential to be stored in $v$ with respect to $S$.

To start with, we need an interpretation $\mathcal{I}(\cdot)$ that maps interpretable values into refinements. The following gives an interpretation of our core calculus for $\mathrm{Re}^{2}$.

[TABLE]

Note that $\mathcal{I}(\cdot)$ is only defined on values of scalar types.

Then we can use $\mathcal{I}(\cdot)$ to transform a value stack $V$ to a refinement environment $E$ with respect to a context $\Gamma$. The stack $V$ maps type variables to concrete types and program variables to values. The environment $E$ is used to define validity checking in former sections. The following defines the transformation $\mathcal{I}_{V}(\Gamma)$ by induction on $\Gamma$.

[TABLE]

Now we define how to extract constraints from a value with respect to its type. It is similar to how we extract constraints from a typing binding in the refinement level. The differences are that (i) we need to use the interpretation $\mathcal{I}(\cdot)$ to map values to refinements, (ii) we need to take care of list elements and pair components, (iii) we need to substitute type variables with concrete types, and (iv) for polymorphic type schemas, we assert that the constraints hold for all instantiations.

[TABLE]

The following defines how to collect path conditions of a stack $V$ with respect to its typing context $\Gamma$, written $\Psi_{V}(\Gamma)$.

[TABLE]

Similar to logical refinements, we can also collect potential annotations. The following defines $\Phi_{V}(v:S)$ as the potential stored in the value $v$ with respect to the type $S$ under the stack $V$.

[TABLE]

Also we have a stack version for potentials $\Phi_{V}(\Gamma)$.

[TABLE]

Finally, we are able to define two notions of consistency for values and stacks, respectively.

Definition 1 (Value consistency).

A value $v\in\mathsf{Val}$ is said to be consistent with $\Gamma\vdash v\dblcolon S$, if for all $\cdot\vdash V\dblcolon\Gamma$, $E=\mathcal{I}_{V}(\Gamma)$ such that $E\models\Psi_{V}(\Gamma)$, we have $E\models\Psi_{V}(v:S)\wedge\Phi_{V}(\Gamma)\geq\Phi_{V}(v:S)$.

Definition 2 (Stack consistency).

An environment $V^{\prime}$ is said to be consistent with $\Gamma\vdash V^{\prime}\dblcolon\Gamma^{\prime}$, if for for all $\cdot\vdash V\dblcolon\Gamma$, $E=\mathcal{I}_{V}(\Gamma)$ such that $E\models\Psi_{V}(\Gamma)$, we have $E^{\prime}\models\Psi_{V,V^{\prime}}(\Gamma^{\prime})\wedge\Phi_{V}(\Gamma)\geq\Phi_{V,V^{\prime}}(\Gamma^{\prime})$ where $E^{\prime}\overset{\underset{\text{def}}{}}{=}\mathcal{I}_{V,V^{\prime}}(\Gamma,\Gamma^{\prime})$.

Appendix D Proofs for Soundness

D.1. Progress

Lemma 0.

Let $\Gamma=\overline{q\mid\alpha}$.

1. (1)

If $\Gamma\vdash T~{}\mathsf{type}$, then $\mathsf{nil}$ is consistent with $\Gamma\vdash\mathsf{nil}\dblcolon\{L(T)\mid\nu=\mathcal{I}(\mathsf{nil})\}$. 2. (2)

If $\vdash\Gamma\mathrel{\curlyveedownarrow}\Gamma_{1}\mid\Gamma_{2}$, $v_{h}$ is consistent with $\Gamma_{1}\vdash v_{h}\dblcolon T$, and $v_{t}$ is consistent with $\Gamma_{2}\vdash v_{t}\dblcolon\{L(T)\mid\nu=\mathcal{I}(v_{t})\}$, then $\mathsf{cons}(v_{h},v_{t})$ is consistent with $\Gamma\vdash\mathsf{cons}(v_{h},v_{t})\dblcolon\{L(T)\mid\nu=\mathcal{I}(\mathsf{cons}(v_{h},v_{t}))\}$.

Proof of (1).

[TABLE]

∎

Proof of (2).

[TABLE]

∎

Proposition 2.

If $\langle e,p\rangle\mapsto\langle e^{\prime},p^{\prime}\rangle$ and $c\geq 0$, then $\langle e,p+c\rangle\mapsto\langle e^{\prime},p^{\prime}+c\rangle$.

Proof.

By induction on $\langle e,p\rangle\mapsto\langle e^{\prime},p^{\prime}\rangle$. ∎

Proposition 3.

If $v\in\mathsf{Val}$, $\Gamma\vdash v\dblcolon T_{1}$, $\Gamma\vdash T_{1}<:T_{2}$, $\cdot\vdash V\dblcolon\Gamma$ and $E=\mathcal{I}_{V}(\Gamma)$ such that $E\models\Psi_{V}(\Gamma)$, then $E\models\Psi_{V}(v:T_{1})\implies(\Psi_{V}(v:T_{2})\wedge\Phi_{V}(v:T_{1})\geq\Phi_{V}(v:T_{2}))$.

Proof.

By induction on $\Gamma\vdash T_{1}<:T_{2}$. ∎

Proposition 4.

If $v\in\mathsf{Val}$, $\Gamma\vdash v\dblcolon S$, $\Gamma\vdash S\mathrel{\curlyveedownarrow}S_{1}\mid S_{2}$, $\cdot\vdash V\dblcolon\Gamma$ and $E=\mathcal{I}_{V}(\Gamma)$ such that $E\models\Psi_{V}(\Gamma)$, then $E\models\Phi_{V}(v:S)=\Phi_{V}(v:S_{1})+\Phi_{V}(v:S_{2})$.

Proof.

By induction on $\Gamma\vdash S\mathrel{\curlyveedownarrow}S_{1}\mid S_{2}$. ∎

Lemma 0.

If $\Gamma=\overline{q\mid\alpha}$, $\Gamma\vdash a:B$, $\cdot\vdash V\dblcolon\Gamma$ and $p\geq\Phi_{V}(\Gamma)$, then $a\in\mathsf{Val}$ and $a$ is consistent with $\Gamma\vdash a\dblcolon\{B\mid\nu=\mathcal{I}(a)\}$.

Proof.

By induction on $\Gamma\vdash a:B$:

[TABLE]

∎

Theorem 6 (Progress).

If $\Gamma=\overline{q\mid\alpha}$, $\Gamma\vdash e\dblcolon S$, $\cdot\vdash V\dblcolon\Gamma$ and $p\geq\Phi_{V}(\Gamma)$, then either $e\in\mathsf{Val}$ and $e$ is consistent with $\Gamma\vdash e\dblcolon S$, or there exist $e^{\prime}$ and $p^{\prime}$ such that $\langle e,p\rangle\mapsto\langle e^{\prime},p^{\prime}\rangle$.

Proof.

By induction on $\Gamma\vdash e\dblcolon S$:

[TABLE]

∎

D.2. Substitution

Proposition 7.

If $\Gamma\vdash e\dblcolon S$ and $\vdash\Gamma,\Gamma^{\prime}~{}\mathsf{context}$, then $\Gamma,\Gamma^{\prime}\vdash e\dblcolon S$.

Proof.

By induction on $\Gamma\vdash e\dblcolon S$. ∎

Proposition 8.

If $\Gamma_{1}\vdash e\dblcolon S$ and $\vdash\Gamma\mathrel{\curlyveedownarrow}\Gamma_{1}\mid\Gamma_{2}$, then $\Gamma\vdash e\dblcolon S$.

Proof.

By induction on $\Gamma_{1}\vdash e\dblcolon S$. ∎

Proposition 9.

If $\Gamma\vdash v\dblcolon{\{B\mid\psi\}}^{\phi}$ and $v\in\mathsf{Val}$, then $\Gamma\vdash v\dblcolon{\{B\mid\nu=\mathcal{I}(v)\}}^{\phi}$.

Proof.

By induction on $\Gamma\vdash v\dblcolon{\{B\mid\psi\}}^{\phi}$. ∎

Proposition 10.

If $\Gamma\vdash v\dblcolon{R}^{\phi}$ and $v\in\mathsf{Val}$, then $\Gamma\models\Phi(\Gamma)\geq[\mathcal{I}(v)/\nu]\phi$.

Proof.

By induction on $\Gamma\vdash v\dblcolon{R}^{\phi}$. ∎

Proposition 11.

If $\Gamma\vdash v\dblcolon S$, $\Gamma\vdash S\mathrel{\curlyveedownarrow}S_{1}\mid S_{2}$ and $v\in\mathsf{Val}$, then there exist $\Gamma_{1}$ and $\Gamma_{2}$ such that $\vdash\Gamma\mathrel{\curlyveedownarrow}\Gamma_{1}\mid\Gamma_{2}$, and $\Gamma_{1}\vdash v\dblcolon S_{1}$, $\Gamma_{2}\vdash v\dblcolon S_{2}$.

Proof.

By induction on $\Gamma\vdash v\dblcolon S$. ∎

Proposition 12.

If $\Gamma\vdash v\dblcolon S$, $\Gamma\vdash S\mathrel{\curlyveedownarrow}S\mid S$ and $v\in\mathsf{Val}$, then there exists $\Gamma^{\prime}$ such that $\vdash\Gamma\mathrel{\curlyveedownarrow}\Gamma\mid\Gamma^{\prime}$ (so $\vdash\Gamma^{\prime}\mathrel{\curlyveedownarrow}\Gamma^{\prime}\mid\Gamma^{\prime}$), and $\Gamma^{\prime}\vdash v\dblcolon S$.

Proof.

By induction on $\Gamma\vdash v\dblcolon S$. ∎

Lemma 0.

If $\Gamma,\psi,\Gamma^{\prime}\vdash\mathcal{J}$ and $\Gamma\models\psi$, then $\Gamma,\Gamma^{\prime}\vdash\mathcal{J}$.

Proof.

By induction on $\Gamma,\psi,\Gamma^{\prime}\vdash\mathcal{J}$. ∎

Lemma 0.

Suppose $\mathcal{J}$ is a judgment other than typing.

1. (1)

If $\Gamma_{1},x:{\{B\mid\psi\}}^{\phi},\Gamma^{\prime}\vdash\mathcal{J}$, $\Gamma_{2}\vdash t\dblcolon{\{B\mid\psi\}}^{\phi}$, $t\in\mathsf{Val}$ and $\vdash\Gamma\mathrel{\curlyveedownarrow}\Gamma_{1}\mid\Gamma_{2}$, then $\Gamma,[\mathcal{I}(t)/x]\Gamma^{\prime}\vdash[\mathcal{I}(t)/x]\mathcal{J}$. 2. (2)

If $\Gamma_{1},x:S_{x},\Gamma^{\prime}\vdash\mathcal{J}$, $S_{x}$ is non-scalar/poly, $\Gamma_{2}\vdash t\dblcolon S_{x}$, $t\in\mathsf{Val}$ and $\vdash\Gamma\mathrel{\curlyveedownarrow}\Gamma_{1}\mid\Gamma_{2}$, then $\Gamma,\Gamma^{\prime}\vdash\mathcal{J}$.

Proof.

By induction on $\Gamma,x:S_{x},\Gamma^{\prime}\vdash\mathcal{J}$. ∎

Lemma 0.

1. (1)

If $\Gamma_{1},x:{\{B_{x}\mid\psi\}}^{\phi},\Gamma^{\prime}\vdash e:B$, $\Gamma_{2}\vdash t\dblcolon{\{B_{x}\mid\psi\}}^{\phi}$, $t\in\mathsf{Val}$ and $\vdash\Gamma\mathrel{\curlyveedownarrow}\Gamma_{1}\mid\Gamma_{2}$, then $\Gamma,[\mathcal{I}(t)/x]\Gamma^{\prime}\vdash[t/x]a:[\mathcal{I}(t)/x]B$. 2. (2)

If $\Gamma_{1},x:S_{x},\Gamma^{\prime}\vdash a:B$, $S_{x}$ is non-scalar/poly, $\Gamma_{2}\vdash t\dblcolon S_{x}$, $t\in\mathsf{Val}$ and $\vdash\Gamma\mathrel{\curlyveedownarrow}\Gamma_{1}\mid\Gamma_{2}$, then $\Gamma,\Gamma^{\prime}\vdash[t/x]a:B$.

Proof of (1).

By induction on $\Gamma_{1},x:{\{B_{x}\mid\psi\}}^{\phi},\Gamma^{\prime}\vdash a:B$:

[TABLE]

∎

Theorem 16 (Substitution).

1. (1)

If $\Gamma_{1},x:{\{B\mid\psi\}}^{\phi},\Gamma^{\prime}\vdash e\dblcolon S$, $\Gamma_{2}\vdash t\dblcolon{\{B\mid\psi\}}^{\phi}$, $t\in\mathsf{Val}$ and $\vdash\Gamma\mathrel{\curlyveedownarrow}\Gamma_{1}\mid\Gamma_{2}$, then $\Gamma,[\mathcal{I}(t)/x]\Gamma^{\prime}\vdash[t/x]e\dblcolon[\mathcal{I}(t)/x]S$. 2. (2)

If $\Gamma_{1},x:S_{x},\Gamma^{\prime}\vdash e\dblcolon S$, $S_{x}$ is non-scalar/poly, $\Gamma_{2}\vdash t\dblcolon S_{x}$, $t\in\mathsf{Val}$ and $\vdash\Gamma\mathrel{\curlyveedownarrow}\Gamma_{1}\mid\Gamma_{2}$, then $\Gamma,\Gamma^{\prime}\vdash[t/x]e\dblcolon S$.

Proof of (1).

By induction on $\Gamma_{1},x:{\{B\mid\psi\}}^{\phi},\Gamma^{\prime}\vdash e\dblcolon S$:

[TABLE]

∎

D.3. Preservation

Proposition 17.

If $\langle e,p\rangle\mapsto\langle e^{\prime},p^{\prime}\rangle$ and $\langle e,q\rangle\mapsto\langle e^{\prime\prime},q^{\prime}\rangle$, then $e^{\prime}=e^{\prime\prime}$ and $q-p=q^{\prime}-p^{\prime}$.

Proof.

By induction on $\langle e,p\rangle\mapsto\langle e^{\prime},p^{\prime}\rangle$ and then inversion on $\langle e,q\rangle\mapsto\langle e^{\prime\prime},q^{\prime}\rangle$. ∎

Theorem 18 (Preservation).

If $\Gamma=\overline{q}$, $\Gamma\vdash e\dblcolon S$, $p\geq\Phi_{\emptyset}(\Gamma)$ and $\langle e,p\rangle\mapsto\langle e^{\prime},p^{\prime}\rangle$, then $p^{\prime}\vdash e^{\prime}\dblcolon S$.

Proof.

By induction on $\Gamma\vdash e\dblcolon S$:

[TABLE]

∎

Appendix E Synthesis Rules

E.1. Program Templates

[TABLE]

E.2. Types

[TABLE]

E.3. Type Wellformedness: $\Gamma\vdash T~{}\mathsf{type}$

{mathpar}\inferrule

[Wf-TUnk]

$\Gamma\vdash\mathsf{?}~{}\mathsf{type}$

E.4. Restricted denotation $\Gamma\models_{X}\psi$

[TABLE]

[TABLE]

E.5. Subtyping: $\Gamma\vdash T<:T$

{mathpar}\inferrule

[Sub-TBot]

$\Gamma\vdash\mathsf{?}<:T$ \inferrule[Sub-Refined] $\Gamma\vdash B_{1}<:B_{2}$

$\Gamma,\nu:B_{1}\models_{\mathsf{fv}(\psi_{1}\implies\psi_{2})}\psi_{1}\implies\psi_{2}$ $\Gamma\vdash\{B_{1}\mid\psi_{1}\}<:\{B_{2}\mid\psi_{2}\}$

E.6. Atomic synthesis: $\Gamma\vdash\mathring{e}\dblcolon T\overset{a}{\rightsquigarrow}\mathsf{lets}(D.a)$

{mathpar}\inferrule

[ASyn-Var] $\Gamma\vdash x\dblcolon T$ $\Gamma\vdash\circ\dblcolon T\overset{a}{\rightsquigarrow}\mathsf{lets}(\cdot.x)$ \inferrule[ASyn-True] $\Gamma\vdash\mathsf{true}\dblcolon T$ $\Gamma\vdash\circ\dblcolon T\overset{a}{\rightsquigarrow}\mathsf{lets}(\cdot.\mathsf{true})$ \inferrule[ASyn-False] $\Gamma\vdash\mathsf{false}\dblcolon T$ $\Gamma\vdash\circ\dblcolon T\overset{a}{\rightsquigarrow}\mathsf{lets}(\cdot.\mathsf{false})$ \inferrule[ASyn-Nil] $\Gamma\vdash\mathsf{nil}\dblcolon T$ $\Gamma\vdash\circ\dblcolon T\overset{a}{\rightsquigarrow}\mathsf{lets}(\cdot.\mathsf{nil})$ \inferrule[ASyn-Cons] $\Gamma\vdash\circ\dblcolon T\overset{a}{\rightsquigarrow}\mathsf{lets}(D_{h}.a_{h})$

$\Gamma\vdash\mathsf{lets}(D_{h}.\mathsf{cons}(a_{h},\circ))\dblcolon{\{L(T)\mid\psi\}}^{\phi}\overset{a}{\rightsquigarrow}\mathsf{lets}(D.a)$ $\Gamma\vdash\circ\dblcolon{\{L(T)\mid\psi\}}^{\phi}\overset{a}{\rightsquigarrow}\mathsf{lets}(D.a)$ \inferrule[ASyn-App]

$\Gamma\vdash\circ\dblcolon{1}\cdot(\_{\,:\,}\mathsf{?}\rightarrow T)\overset{a}{\rightsquigarrow}\mathsf{lets}(D_{1}.x)$

$\Gamma\vdash\mathsf{lets}(D_{1}.\mathsf{app}(x,\circ))\dblcolon T\overset{a}{\rightsquigarrow}\mathsf{lets}(D.x^{\prime})$

$\Gamma\vdash\circ\dblcolon T\overset{a}{\rightsquigarrow}\mathsf{lets}(D.x^{\prime})$ \inferrule[AFill-Cons] $\Gamma\vdash a_{h}:T$

$\Gamma\vdash\circ\dblcolon{\{L(T)\mid\psi^{\prime}\}}^{\phi^{\prime}}\overset{a}{\rightsquigarrow}\mathsf{lets}(D.a_{t})$

$\Gamma\vdash\mathsf{fold}(\mathsf{lets}(D.\mathsf{cons}(a_{h},a_{t})))\dblcolon{\{L(T)\mid\psi\}}^{\phi}$

ψ’ = $[\nu+1/\nu]\psi$

ϕ’ = $[\nu+1/\nu]\phi$ $\Gamma\vdash\mathsf{cons}(a_{h},\circ)\dblcolon{\{L(T)\mid\psi\}}^{\phi}\overset{a}{\rightsquigarrow}\mathsf{lets}(D.\mathsf{cons}(a_{h},a_{t}))$

\inferrule

[AFill-App-SimpAtom] $\Gamma\vdash x\dblcolon{1}\cdot(y{\,:\,}T_{1}\rightarrow T^{\prime})$

T_1 scalar

$\Gamma\vdash\circ\dblcolon T_{1}\overset{a}{\rightsquigarrow}\mathsf{lets}(D.a)$

$\Gamma\vdash\mathsf{fold}(\mathsf{lets}(D.\mathsf{app}(x,a)))\dblcolon T$ $\Gamma,1\vdash\mathsf{app}(x,\circ)\dblcolon T\overset{a}{\rightsquigarrow}\mathsf{lets}(D;x^{\prime}\leftarrow\mathsf{tick}(1,\mathsf{app}(x,a)).x^{\prime})$ \inferrule[AFill-App] $\Gamma\vdash x\dblcolon{1}\cdot(\_{\,:\,}T_{1}\rightarrow T)$

T_1 non-scalar

$\Gamma\vdash\circ\dblcolon T_{1}\rightsquigarrow\hat{a}$

$\Gamma\vdash\mathsf{app}(x,\hat{a})\dblcolon T$ $\Gamma,1\vdash\mathsf{app}(x,\circ)\dblcolon T\overset{a}{\rightsquigarrow}\mathsf{lets}(x^{\prime}\leftarrow\mathsf{tick}(1,\mathsf{app}(x,\hat{a})).x^{\prime})$ \inferrule[AFill-Let] $\vdash\Gamma\mathrel{\curlyveedownarrow}\Gamma_{1}\mid\Gamma_{2}$

$\Gamma_{1}\vdash e_{1}\dblcolon S_{1}$

$\Gamma_{2},x:S_{1}\vdash\mathsf{lets}(D.\mathring{e}_{2})\dblcolon T\overset{a}{\rightsquigarrow}\mathsf{lets}(D_{2}.a)$ $\Gamma\vdash\mathsf{lets}(x\leftarrow e_{1};D.\mathring{e}_{2})\dblcolon T\overset{a}{\rightsquigarrow}\mathsf{lets}(x\leftarrow e_{1};D_{2}.a)$ \inferrule[AFill-Let-Emp] $\Gamma\vdash\mathring{e}\dblcolon T\overset{a}{\rightsquigarrow}\mathsf{lets}(D.a)$ $\Gamma\vdash\mathsf{lets}(\cdot.\mathring{e})\dblcolon T\overset{a}{\rightsquigarrow}\mathsf{lets}(D.a)$ \inferrule[AFill-Transfer] $\Gamma\models\Phi(\Gamma)=\Phi(\Gamma^{\prime})$

$\Gamma^{\prime}\vdash\mathring{e}\dblcolon T\overset{a}{\rightsquigarrow}\mathsf{lets}(D.a)$ $\Gamma\vdash\mathring{e}\dblcolon T\overset{a}{\rightsquigarrow}\mathsf{lets}(D.a)$

E.7. Synthesis: $\Gamma\vdash\mathring{e}\dblcolon S\rightsquigarrow e$

{mathpar}\inferrule

[Syn-Imp] $\Gamma\models\bot$ $\Gamma\vdash\circ\dblcolon T\rightsquigarrow\mathsf{impossible}$ \inferrule[Syn-Cond]

$\Gamma\vdash\circ\dblcolon\mathsf{bool}\overset{a}{\rightsquigarrow}\mathsf{lets}(D.x)$

$\Gamma\vdash\mathsf{lets}(D.\mathsf{if}(x,\circ,\circ))\dblcolon T\rightsquigarrow e$ $\Gamma\vdash\circ\dblcolon T\rightsquigarrow e$ \inferrule[Syn-MatL]

$\Gamma\vdash T~{}\mathsf{type}$

$\Gamma\vdash\circ\dblcolon L(T)\overset{a}{\rightsquigarrow}\mathsf{lets}(D.x)$

$\Gamma\vdash\mathsf{lets}(D.\mathsf{matl}(x,\circ,x_{h}.x_{t}.\circ))\dblcolon T\rightsquigarrow e$ $\Gamma\vdash\circ\dblcolon T\rightsquigarrow e$ \inferrule[Syn-Fix] $\Gamma,f:(x{\,:\,}T_{x}\rightarrow T),x:T_{x}\vdash\circ\dblcolon T\rightsquigarrow e$

$\vdash\Gamma\mathrel{\curlyveedownarrow}\Gamma\mid\Gamma$

$\Gamma\vdash(x{\,:\,}T_{x}\rightarrow T)~{}\mathsf{type}$ $\Gamma\vdash\circ\dblcolon(x{\,:\,}T_{x}\rightarrow T)\rightsquigarrow\mathsf{fix}(f.x.e)$ \inferrule[Syn-Abs-Lin] $\Gamma,x:T_{x}\vdash\circ\dblcolon T\rightsquigarrow e$

$\Gamma\vdash T_{x}~{}\mathsf{type}$ $\Gamma\vdash\circ\dblcolon({1}\cdot(x{\,:\,}T_{x}\rightarrow T))\rightsquigarrow\lambda(x.e)$ \inferrule[Syn-Gen] $\Gamma,\alpha\vdash S\mathrel{\curlyveedownarrow}S\mid S$

$\Gamma,\alpha\vdash\circ\dblcolon S\rightsquigarrow e$

$e\in\mathsf{Val}$ $\Gamma\vdash\circ\dblcolon\forall\alpha.S\rightsquigarrow e$ \inferrule[Fill-Cond] $\Gamma\vdash x:\mathsf{bool}$

$\Gamma,x\vdash\circ\dblcolon T\rightsquigarrow e_{1}$

$\Gamma,\neg x\vdash\circ\dblcolon T\rightsquigarrow e_{2}$ $\Gamma\vdash\mathsf{if}(x,\circ,\circ)\dblcolon T\rightsquigarrow\mathsf{if}(x,e_{1},e_{2})$ \inferrule[Fill-MatL] $\vdash\Gamma\mathrel{\curlyveedownarrow}\Gamma_{1}\mid\Gamma_{2}$

$\Gamma_{1}\vdash x:L(T)$

$\Gamma_{2},x=0\vdash\circ\dblcolon T\rightsquigarrow e_{1}$

$\Gamma_{2},x_{h}:T,x_{t}:L(T),x=x_{t}+1\vdash\circ\dblcolon T\rightsquigarrow e_{2}$ $\Gamma\vdash\mathsf{matl}(x,\circ,x_{h}.x_{t}.\circ)\dblcolon T\rightsquigarrow\mathsf{matl}(x,e_{1},x_{h}.x_{t}.e_{2})$ \inferrule[Fill-Let] $\vdash\Gamma\mathrel{\curlyveedownarrow}\Gamma_{1}\mid\Gamma_{2}$

$\Gamma_{1}\vdash e_{1}\dblcolon S_{1}$

$\Gamma_{2},x:S_{1}\vdash\mathsf{lets}(D.\mathring{e}_{2})\dblcolon T\rightsquigarrow e_{2}$

$\Gamma\vdash T~{}\mathsf{type}$ $\Gamma\vdash\mathsf{lets}(D;x\leftarrow e_{1}.\mathring{e}_{2})\dblcolon T\rightsquigarrow\mathsf{let}(e_{1},x.e_{2})$ \inferrule[Fill-Let-Emp] $\Gamma\vdash\mathring{e}\dblcolon T\rightsquigarrow e$ $\Gamma\vdash\mathsf{lets}(\cdot.\mathring{e})\dblcolon T\rightsquigarrow e$ \inferrule[Syn-Atom] $\Gamma\vdash\circ\dblcolon T\overset{a}{\rightsquigarrow}\mathsf{lets}(D.a)$ $\Gamma\vdash\circ\dblcolon T\rightsquigarrow\mathsf{fold}(\mathsf{lets}(D.a))$

Appendix F Soundness of Synthesis

Proposition 1.

If $\Gamma\vdash\mathsf{fold}(\mathsf{lets}(D.e))\dblcolon T$, then $\Gamma,c\vdash\mathsf{fold}(\mathsf{lets}(D;x^{\prime}\leftarrow\mathsf{tick}(c,e).x^{\prime}))\dblcolon T$ for $c\geq 0$.

Proof.

By induction on the length of $D$.

• •

$D=\cdot$: We have $\mathsf{fold}(\mathsf{lets}(\cdot.e))=e$ and $\mathsf{fold}(\mathsf{lets}(x^{\prime}\leftarrow\mathsf{tick}(c,e).x^{\prime}))=\mathsf{let}(\mathsf{tick}(c,e),x^{\prime}.x^{\prime})$. By $\Gamma\vdash e\dblcolon T$ we know $\Gamma,c\vdash\mathsf{tick}(c,e)\dblcolon T$ by (T-Consume-P). Therefore by (T-Let) we derive $\Gamma,c\vdash\mathsf{let}(\mathsf{tick}(c,e),x^{\prime}.x^{\prime})\dblcolon T$.

• •

$D=x_{1}\leftarrow e_{1};D^{\prime}$: We have $\mathsf{fold}(\mathsf{lets}(x_{1}\leftarrow e_{1};D^{\prime}.e))=\mathsf{let}(e_{1},x_{1}.\mathsf{fold}(\mathsf{lets}(D^{\prime}.e)))$. By inversion on

[TABLE]

we know there exist $\Gamma_{1},\Gamma_{2},S_{1}$ such that $\vdash\Gamma\mathrel{\curlyveedownarrow}\Gamma_{1}\mid\Gamma_{2}$, $\Gamma_{1}\vdash e_{1}\dblcolon S_{1}$ and $\Gamma_{2},x_{1}:S_{1}\vdash\mathsf{fold}(\mathsf{lets}(D^{\prime}.e))\dblcolon T$. Thus by I.H. we have $\Gamma_{2},x_{1}:S_{1},c\vdash\mathsf{fold}(\mathsf{lets}(D^{\prime};x^{\prime}\leftarrow\mathsf{tick}(c,e).x^{\prime}))\dblcolon T$. Again by (T-Let) and (T-Transfer) we derive $\Gamma,c\vdash\mathsf{let}(e_{1},x_{1}.\mathsf{fold}(\mathsf{lets}(D^{\prime};x^{\prime}\leftarrow\mathsf{tick}(c,e).x^{\prime})))\dblcolon T$, i.e., $\Gamma,c\vdash\mathsf{fold}(\mathsf{lets}(D;x^{\prime}\leftarrow\mathsf{tick}(c,e).x^{\prime}))\dblcolon T$.

∎

Lemma 0.

If $\Gamma\vdash\mathring{e}\dblcolon T\overset{a}{\rightsquigarrow}\mathsf{lets}(D.a)$, then $\Gamma\vdash\mathsf{fold}(\mathsf{lets}(D.a))\dblcolon T$.

Proof.

By induction on the derivation of $\Gamma\vdash\mathring{e}\dblcolon T\overset{a}{\rightsquigarrow}\mathsf{lets}(D.a)$.

• •

$\footnotesize\inferrule*[lab={\footnotesize{(ASyn-Var)}},]{\Gamma\vdash x\dblcolon T}{\Gamma\vdash\circ\dblcolon T\overset{a}{\rightsquigarrow}\mathsf{lets}(\cdot.x)}$

We have $\mathsf{fold}(\mathsf{lets}(\cdot.x))=x$ and thus conclude $\Gamma\vdash x\dblcolon T$ by the premise.

Cases (ASyn-True), (ASyn-False), (ASyn-Nil) are similar to this case.

• •

$\footnotesize\inferrule*[lab={\footnotesize{(ASyn-Cons)}},]{\Gamma\vdash\circ\dblcolon T\overset{a}{\rightsquigarrow}\mathsf{lets}(D_{h}.a_{h})\\ \Gamma\vdash\mathsf{lets}(D_{h}.\mathsf{cons}(a_{h},\circ))\dblcolon{\{L(T)\mid\psi\}}^{\phi}\overset{a}{\rightsquigarrow}\mathsf{lets}(D.a)}{\Gamma\vdash\circ\dblcolon{\{L(T)\mid\psi\}}^{\phi}\overset{a}{\rightsquigarrow}\mathsf{lets}(D.a)}$

By I.H. on the second premise.

• •

$\footnotesize\inferrule*[lab={\footnotesize{(ASyn-App)}},]{\Gamma\vdash\circ\dblcolon{1}\cdot(\_{\,:\,}?\rightarrow T)\overset{a}{\rightsquigarrow}\mathsf{lets}(D_{1}.x)\\ \Gamma\vdash\mathsf{lets}(D_{1}.\mathsf{app}(x,\circ))\dblcolon T\overset{a}{\rightsquigarrow}\mathsf{lets}(D.x^{\prime})}{\Gamma\vdash\circ\dblcolon T\overset{a}{\rightsquigarrow}\mathsf{lets}(D.x^{\prime})}$

By I.H. on the second premise.

• •

$\footnotesize\inferrule*[lab={\footnotesize{(AFill-Cons)}},]{\Gamma\vdash a_{h}:T\\ \Gamma\vdash\circ\dblcolon{\{L(T)\mid\psi^{\prime}\}}^{\phi^{\prime}}\overset{a}{\rightsquigarrow}\mathsf{lets}(D.a_{t})\\ \Gamma\vdash\mathsf{fold}(\mathsf{lets}(D.\mathsf{cons}(a_{h},a_{t})))\dblcolon{\{L(T)\mid\psi\}}^{\phi}\\ \psi^{\prime}=[\nu+1/\nu]\psi\\ \phi^{\prime}=[\nu+1/\nu]\phi}{\Gamma\vdash\mathsf{cons}(a_{h},\circ)\dblcolon{\{L(T)\mid\psi\}}^{\phi}\overset{a}{\rightsquigarrow}\mathsf{lets}(D.\mathsf{cons}(a_{h},a_{t}))}$

By the third premise.

• •

$\footnotesize\inferrule*[lab={\footnotesize{(AFill-App-SimpAtom)}},]{\Gamma\vdash x\dblcolon{1}\cdot(y{\,:\,}T_{1}\rightarrow T^{\prime})\\ T_{1}~{}\mathsf{scalar}\\ \Gamma\vdash\circ\dblcolon T_{1}\overset{a}{\rightsquigarrow}\mathsf{lets}(D.a)\\ \Gamma\vdash\mathsf{fold}(\mathsf{lets}(D.\mathsf{app}(x,a)))\dblcolon T}{\Gamma,1\vdash\mathsf{app}(x,\circ)\dblcolon T\overset{a}{\rightsquigarrow}\mathsf{lets}(D;x^{\prime}\leftarrow\mathsf{tick}(1,\mathsf{app}(x,a)).x^{\prime})}$

Appeal to Prop. 1.

• •

$\footnotesize\inferrule*[lab={\footnotesize{(AFill-App)}},]{\Gamma\vdash x\dblcolon{1}\cdot(\_{\,:\,}T_{1}\rightarrow T)\\ T_{1}~{}\text{non-scalar}\\ \Gamma\vdash\circ\dblcolon T_{1}\rightsquigarrow\hat{a}\\ \Gamma\vdash\mathsf{app}(x,\hat{a})\dblcolon T}{\Gamma,1\vdash\mathsf{app}(x,\circ)\dblcolon T\overset{a}{\rightsquigarrow}\mathsf{lets}(x^{\prime}\leftarrow\mathsf{tick}(1,\mathsf{app}(x,\hat{a})).x^{\prime})}$

Appeal to Prop. 1.

• •

$\footnotesize\inferrule*[lab={\footnotesize{(AFill-Let)}},]{\vdash\Gamma\mathrel{\curlyveedownarrow}\Gamma_{1}\mid\Gamma_{2}\\ \Gamma_{1}\vdash e_{1}\dblcolon S_{1}\\ \Gamma_{2},x:S_{1}\vdash\mathsf{lets}(D.\mathring{e_{2}})\dblcolon T\overset{a}{\rightsquigarrow}\mathsf{lets}(D_{2}.a)}{\Gamma\vdash\mathsf{lets}(x\leftarrow e_{1};D.\mathring{e_{2}})\dblcolon T\overset{a}{\rightsquigarrow}\mathsf{lets}(x\leftarrow e_{1};D_{2}.a)}$

By I.H. on the third premise, we have

[TABLE]

Since $\mathsf{fold}(\mathsf{lets}(x\leftarrow e_{1};D_{2}.a))=\mathsf{let}(e_{1},x.\mathsf{fold}(\mathsf{lets}(D_{2}.a)))$, we conclude by (T-Let).

• •

$\footnotesize\inferrule*[lab={\footnotesize{(AFill-Let-Emp)}},]{\Gamma\vdash\mathring{e}\dblcolon T\overset{a}{\rightsquigarrow}\mathsf{lets}(D.a)}{\Gamma\vdash\mathsf{lets}(\cdot.\mathring{e})\dblcolon T\overset{a}{\rightsquigarrow}\mathsf{lets}(D.a)}$

By I.H. on the premise.

• •

$\footnotesize\inferrule*[lab={\footnotesize{(AFill-Transfer)}},]{\Gamma\models\Phi(\Gamma)=\Phi(\Gamma^{\prime})\\ \Gamma^{\prime}\vdash\mathring{e}\dblcolon T\overset{a}{\rightsquigarrow}\mathsf{lets}(D.a)}{\Gamma\vdash\mathring{e}\dblcolon T\overset{a}{\rightsquigarrow}\mathsf{lets}(D.a)}$

By I.H. on the second premise, we have $\Gamma^{\prime}\vdash\mathsf{fold}(\mathsf{lets}(D.a))\dblcolon T$.

Thus we derive $\Gamma\vdash\mathsf{fold}(\mathsf{lets}(D.a))\dblcolon T$ by (S-Transfer).

∎

Lemma 0.

If $\Gamma\vdash\mathring{e}\dblcolon S\rightsquigarrow e$, then $\Gamma\vdash e\dblcolon S$.

Proof.

By induction on the derivation of $\Gamma\vdash\mathring{e}\dblcolon S\rightsquigarrow e$.

• •

$\footnotesize\inferrule*[lab={\footnotesize{(Syn-Imp)}},]{\Gamma\models\bot}{\Gamma\vdash\circ\dblcolon T\rightsquigarrow\mathsf{impossible}}$

We derive $\Gamma\vdash\mathsf{impossible}\dblcolon T$ by (T-Imp).

• •

$\footnotesize\inferrule*[lab={\footnotesize{(Syn-Cond)}},]{\Gamma\vdash\circ\dblcolon\mathsf{bool}\overset{a}{\rightsquigarrow}\mathsf{lets}(D.x)\\ \Gamma\vdash\mathsf{lets}(D.\mathsf{if}(x,\circ,\circ))\dblcolon T\rightsquigarrow e}{\Gamma\vdash\circ\dblcolon T\rightsquigarrow e}$

By I.H. on the second premise.

• •

$\footnotesize\inferrule*[lab={\footnotesize{(Syn-MatL)}},]{\Gamma\vdash T~{}\mathsf{type}\\ \Gamma\vdash\circ\dblcolon L(T)\overset{a}{\rightsquigarrow}\mathsf{lets}(D.x)\\ \Gamma\vdash\mathsf{lets}(D.\mathsf{matl}(x,\circ,x_{h}.x_{t}.\circ))\dblcolon T\rightsquigarrow e}{\Gamma\vdash\circ\dblcolon T\rightsquigarrow e}$

By I.H. on the third premise.

• •

$\footnotesize\inferrule*[lab={\footnotesize{(Syn-Fix)}},]{\Gamma,f:(x{\,:\,}T_{x}\rightarrow T),x:T_{x}\vdash\circ\dblcolon T\rightsquigarrow e\\ \vdash\Gamma\mathrel{\curlyveedownarrow}\Gamma\mid\Gamma\\ \Gamma\vdash(x{\,:\,}T_{x}\rightarrow T)~{}\mathsf{type}}{\Gamma\vdash\circ\dblcolon(x{\,:\,}T_{x}\rightarrow T)\rightsquigarrow\mathsf{fix}(f.x.e)}$

By I.H. on the first premise, we have $\Gamma,f:(x{\,:\,}T_{x}\rightarrow T),x:T_{x}\vdash e\dblcolon T$.

Thus we derive $\Gamma\vdash\mathsf{fix}(f.x.e)\dblcolon(x{\,:\,}T_{x}\rightarrow T)$.

• •

$\footnotesize\inferrule*[lab={\footnotesize{(Syn-Abs-Lin)}},]{\Gamma,x:T_{x}\vdash\circ\dblcolon T\rightsquigarrow e\\ \Gamma\vdash T_{x}~{}\mathsf{type}}{\Gamma\vdash\circ\dblcolon({1}\cdot(x{\,:\,}T_{x}\rightarrow T))\rightsquigarrow\lambda(x.e)}$

By I.H. on the first premise, we have $\Gamma,x:T_{x}\vdash e\dblcolon T$.

Thus we derive $\Gamma\vdash\lambda(x.e)\dblcolon{1}\cdot(x{\,:\,}T_{x}\rightarrow T)$ by (T-Abs-Lin).

• •

$\footnotesize\inferrule*[lab={\footnotesize{(Syn-Gen)}},]{\Gamma,\alpha\vdash S\mathrel{\curlyveedownarrow}S\mid S\\ \Gamma,\alpha\vdash\circ\dblcolon S\rightsquigarrow e\\ e\in\mathsf{Val}}{\Gamma\vdash\circ\dblcolon\forall\alpha.S\rightsquigarrow e}$

By I.H. on the second premise, we have $\Gamma,\alpha\vdash e\dblcolon S$.

Thus we derive $\Gamma\vdash e\dblcolon\forall\alpha.S$ by (S-Gen).

• •

$\footnotesize\inferrule*[lab={\footnotesize{(Fill-Cond)}},]{\Gamma\vdash x:\mathsf{bool}\\ \Gamma,x\vdash\circ\dblcolon T\rightsquigarrow e_{1}\\ \Gamma,\neg x\vdash\circ\dblcolon T\rightsquigarrow e_{2}}{\Gamma\vdash\mathsf{if}(x,\circ,\circ)\dblcolon T\rightsquigarrow\mathsf{if}(x,e_{1},e_{2})}$

By I.H. on the second premise, we have $\Gamma,x\vdash e_{1}\dblcolon T$.

By I.H. on the third premise, we have $\Gamma,\neg x\vdash e_{2}\dblcolon T$.

Thus we derive $\Gamma\vdash\mathsf{if}(x,e_{1},e_{2})\dblcolon T$ by (T-Cond).

• •

$\footnotesize\inferrule*[lab={\footnotesize{(Fill-MatL)}},]{\vdash\Gamma\mathrel{\curlyveedownarrow}\Gamma_{1}\mid\Gamma_{2}\\ \Gamma_{1}\vdash x:L(T)\\ \Gamma_{2},x=0\vdash\circ\dblcolon T\rightsquigarrow e_{1}\\ \Gamma_{2},x_{h}:T,x_{t}:L(T),x=x_{t}+1\vdash\circ\dblcolon T\rightsquigarrow e_{2}}{\Gamma\vdash\mathsf{matl}(x,\circ,x_{h}.x_{t}.\circ)\dblcolon T\rightsquigarrow\mathsf{matl}(x,e_{1},x_{h}.x_{t}.e_{2})}$

By I.H. on the third premise, we have $\Gamma_{2},x=0\vdash e_{1}\dblcolon T$.

By I.H. on the fourth premise, we have $\Gamma_{2},x_{h}:T,x_{t}:L(T),x=x_{t}+1\vdash e_{2}\dblcolon T$.

Thus we derive $\Gamma\vdash\mathsf{matl}(x,e_{1},x_{h}.x_{t}.e_{2})\dblcolon T$.

• •

$\footnotesize\inferrule*[lab={\footnotesize{(Fill-Let)}},]{\vdash\Gamma\mathrel{\curlyveedownarrow}\Gamma_{1}\mid\Gamma_{2}\\ \Gamma_{1}\vdash e_{1}\dblcolon S_{1}\\ \Gamma_{2},x:S_{1}\vdash\mathsf{lets}(D.\mathring{e_{2}})\dblcolon T\rightsquigarrow e_{2}\\ \Gamma\vdash T~{}\mathsf{type}}{\Gamma\vdash\mathsf{lets}(D;x\leftarrow e_{1}.\mathring{e_{2}})\dblcolon T\rightsquigarrow\mathsf{let}(e_{1},x.e_{2})}$

By I.H. on the third premise, we have $\Gamma_{2},x:S_{1}\vdash e_{2}\dblcolon T$.

Thus we derive $\Gamma\vdash\mathsf{let}(e_{1},x.e_{2})\dblcolon T$ by (T-Let).

• •

$\footnotesize\inferrule*[lab={\footnotesize{(Fill-Let-Emp)}},]{\Gamma\vdash\mathring{e}\dblcolon T\rightsquigarrow e}{\Gamma\vdash\mathsf{lets}(\cdot.\mathring{e})\dblcolon T\rightsquigarrow e}$

By I.H. on the premise.

• •

$\footnotesize\inferrule*[lab={\footnotesize{(Syn-Atom)}},]{\Gamma\vdash\circ\dblcolon T\overset{a}{\rightsquigarrow}\mathsf{lets}(D.a)}{\Gamma\vdash\circ\dblcolon T\rightsquigarrow\mathsf{fold}(\mathsf{lets}(D.a))}$

Appeal to Lem. 2.

∎

Theorem 4 (Soundness of Synthesis).

If $\Gamma\vdash\circ\dblcolon S\rightsquigarrow e$, then $\Gamma\vdash e\dblcolon S$.

Proof.

By Lemma 3. ∎