Liquid Resource Types

TL;DR

Liquid resource types provide an automated, precise method for verifying resource bounds in functional programs by combining logical refinements with potential annotations, enabling expressive and automatic resource analysis.

Contribution

This work introduces liquid resource types, a novel type system that automatically verifies resource bounds with expressive potential annotations, bridging automation and flexibility.

Findings

Successfully verifies resource bounds automatically

Supports polynomial and exponential bounds

Reduces manual proof effort

Abstract

This article presents liquid resource types, a technique for automatically verifying the resource consumption of functional programs. Existing resource analysis techniques trade automation for flexibility -- automated techniques are restricted to relatively constrained families of resource bounds, while more expressive proof techniques admitting value-dependent bounds rely on handwritten proofs. Liquid resource types combine the best of these approaches, using logical refinements to automatically prove precise bounds on a program's resource consumption. The type system augments refinement types with potential annotations to conduct an amortized resource analysis. Importantly, users can annotate data structure declarations to indicate how potential is allocated within the type, allowing the system to express bounds with polynomials and exponentials, as well as more precise expressions depending on program values. We prove the soundness of the type system, provide a library of flexible and reusable data structures for conducting resource analysis, and use our prototype implementation to automatically verify resource bounds that previously required a manual proof.