  In program synthesis there is a well-known trade-off between concise and
strong specifications: if a specification is too verbose, it might be harder to
write than the program; if it is too weak, the synthesised program might not
match the user's intent. In this work we explore the use of annotations for
restricting memory access permissions in program synthesis, and show that they
can make specifications much stronger while remaining surprisingly concise.
Specifically, we enhance Synthetic Separation Logic (SSL), a framework for
synthesis of heap-manipulating programs, with the logical mechanism of
read-only borrows. We observe that this minimalistic and conservative SSL
extension benefits the synthesis in several ways, making it more (a) expressive
(stronger correctness guarantees are achieved with a modest annotation
overhead), (b) effective (it produces more concise and easier-to-read
programs), (c) efficient (faster synthesis), and (d) robust (synthesis
efficiency is less affected by the choice of the search heuristic). We explain
the intuition and provide formal treatment for read-only borrows. We
substantiate the claims (a)--(d) by describing our quantitative evaluation of
the borrowing-aware synthesis implementation on a series of standard benchmark
specifications for various heap-manipulating programs.
