Predictable Verification using Intrinsic Definitions

TL;DR

The paper addresses the challenge of verifying data-structure maintenance without relying on recursive definitions by introducing intrinsic definitions that augment locations with ghost monadic maps under a local condition $LC$. It then presents the Fix-What-You-Break (FWYB) methodology, a three-stage process that converts high-level intrinsic specifications into decidable, quantifier-free verification conditions, using ghost code and a broken-set $Br$ to manage local-condition violations. The authors implement IDS/FWYB in Boogie and demonstrate scalable verification across diverse structures, including overlaid data structures like a List over a BST, with benchmarks showing rapid verification and minimal reliance on programmer lemmas. This approach promises practical, predictable verification for mutable data structures and suggests avenues for integration with higher-level languages to broaden adoption.

Abstract

We propose a novel mechanism of defining data structures using intrinsic definitions that avoids recursion and instead utilizes monadic maps satisfying local conditions. We show that intrinsic definitions are a powerful mechanism that can capture a variety of data structures naturally. We show that they also enable a predictable verification methodology that allows engineers to write ghost code to update monadic maps and perform verification using reduction to decidable logics. We evaluate our methodology using Boogie and prove a suite of data structure manipulating programs correct.

Figures (12)

• Figure 1: Grammar of while programs with recursion. $x,y$ are variables denoting objects of class $C?$ (i.e., $C$ objects or $\mathit{nil}$), $v, w$ are a background sort(s) variables, $r, t$ denote variables of any sort, $f$ is a pointer field, $d$ is a data field, and $be$ is a expression of the background sort(s).
• Figure 2: Rules for constructing well-behaved programs. Local condition formula instantiated at $x$ is denoted by $\mathit{LC}(x)$. The statement $(\mathsf{if}\, \mathit{cond}\, \mathsf{then}\, S)$ is sugar for $(\mathsf{if}\, \mathit{cond}\, \mathsf{then}\, S\, \mathsf{else}\, \mathsf{skip})$.
• Figure 3: Reasoning about the set of objects broken by x.next := z. The dashed arrow represents the old $\mathit{next}$ pointer before the mutation. The grey nodes denote objects where local conditions can be broken by the mutation. We see that only $x$ and $y$ may violate $\mathit{next}$ and $\mathit{prev}$ being inverses.
• Figure 4: Operational Semantics
• Figure 5: Grammar of programs with ghost code. $x,y, z$ are user variables $\mathit{Var}_U$, $a,b$ are ghost variables $\mathit{Var}_G$, $f \in \mathcal{F}$ is a user field, and $g \in \mathcal{G}$ is a ghost map. Notation $\mathit{Expr}[\mathit{Vars},\mathit{Maps}]$ denotes expressions over the vocabulary given by variables $\mathit{Vars}$ and maps $\mathit{Maps}$, similarly $\mathit{BoolExpr}[\mathit{Vars},\mathit{Maps}]$ denotes boolean expressions. Termination for ghost loops and functions can be established in any way.

Theorems & Definitions (14)

• definition 1: Data Structure
• definition 2: Intrinsic Definition
• definition 3: Data Structures defined by Intrinsic Definitions
• definition 4: Validity of Intrinsic Hoare Triples
• definition 5: Projection of Ghost-Augmented Code to User Code
• Proposition 3.1
• Proposition 3.2
• Proposition 3.3
• Theorem 3.4: FWYB Soundness
• definition 6: Projection of Ghost-Augmented Code to User Code