# 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.

## Key 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.