Abstraction Functions as Types

TL;DR

The paper presents a synthetic, phase-based framework for modular verification that encodes abstraction functions as types via a phase distinction between concrete and abstract data. By introducing fracture and gluing, along with abstract, concrete, and behavioral modalities, it achieves noninterference guarantees that support modular substitution of implementations while preserving abstract behavior. It extends the framework to cost-aware verification through Calf and Decalf, introducing sealing to obtain cost upper bounds within abstract specifications. The approach is demonstrated with concrete data structures (batched queues and red-black trees) and is positioned within related work on phased type theory, representation independence, and ghost code. This work enables scalable, cost-aware, modular verification in dependently typed languages while hiding private details from clients.

Abstract

Software development depends on the use of libraries whose public specifications inform client code and impose obligations on private implementations; it follows that verification at scale must also be modular, preserving such abstraction. Hoare's influential methodology uses abstraction functions to demonstrate the coherence between such concrete implementations and their abstract specifications. However, the Hoare methodology relies on a conventional separation between implementation and specification, providing no linguistic support for ensuring that this convention is obeyed. This paper proposes a synthetic account of Hoare's methodology within univalent dependent type theory by encoding the data of abstraction functions within types themselves. This is achieved via a phase distinction, which gives rise to a gluing construction that renders an abstraction function as a type and a pair of modalities that fracture a type into its concrete and abstract parts. A noninterference theorem governing the phase distinction characterizes the modularity guarantees provided by the theory. This approach scales to verification of cost, allowing the analysis of client cost relative to a cost-aware specification. A monadic sealing effect facilitates modularity of cost, permitting an implementation to be upper-bounded by its specification in cases where private details influence observable cost. The resulting theory supports modular development of programs and proofs in a manner that hides private details of no concern to clients while permitting precise specifications of both the cost and behavior of programs.

Figures (4)

• Figure 1: Type representing invariant-preserving red-black trees.
• Figure 2: Type representing batched queues, instrumented with an abstract-phase quotient to allow data to flow implicitly from the inbox list to the outbox list.
• Figure 3: Type representing invariant-preserving red-black trees, instrumented with the concrete modality and abstract quotients to annihilate red-black coloring and tree shape in the abstract phase.
• Figure 4: List reverse implemented using a queue, $\Impl{qreverse}$, and a direct list reversal function, $\Impl{reverse}$.

Theorems & Definitions (25)

• definition 1
• definition 2
• lemma 1
• definition 3
• theorem 1: Fracture and Gluing
• remark 1: Semantics
• remark 2: Representation Invariants
• remark 3
• remark 4
• remark 5: Smart Constructors