## Diagram: Verification Framework for Linked Lists ### Overview This diagram illustrates a formal verification framework that connects abstract, pure mathematical representations of a linked list with its concrete, real-world implementation. It shows how specifications written in a pure language (Pearllite) are systematically encoded into assertions for a real-world implementation language (Gilsonite) to enable formal verification using tools like Creusot and Gillian-Rust. ### Components/Axes The diagram is divided into two primary horizontal regions, representing two conceptual "worlds," and includes associated verification tools on the right. **1. Top Region: "World of pure representations" (Green Outline)** * **Label:** `World of pure representations` (Top-left, green text). * **Primary Component:** A dashed green box labeled `Seq<[T]>` (Sequence of lists of T). * **Contents:** Three solid green boxes inside the dashed box, representing elements of the sequence: * `r₀ : [T]` * `r₁ : [T]` * `r₂ : [T]` * **Associated Specification:** To the right, a solid green box labeled `Pearllite` containing the text: `ensures: *self = ^self`. * **Associated Tool:** Far right, a green clipboard icon labeled `Creusot`. **2. Bottom Region: "Real world" (Red Outline)** * **Label:** `Real world` (Left, red text). * **Primary Component:** A dashed red box labeled `LinkedList<T>`. * **Contents:** Three solid red boxes representing nodes in a linked list. Each node has three fields: * **Node 1 (Left):** Top field: `v₀ : T`. Middle field: Empty. Bottom field: `Ø` (null symbol). * **Node 2 (Center):** Top field: `v₁ : T`. Middle field: Empty. Bottom field: Empty. * **Node 3 (Right):** Top field: `v₂ : T`. Middle field: Empty. Bottom field: `Ø`. * **Connections:** Red arrows point from the middle field of Node 1 to Node 2, and from the middle field of Node 2 to Node 3, indicating the `next` pointers. The bottom `Ø` in Node 1 and Node 3 likely represents the `prev` pointer being null (for a singly-linked list or the head/tail of a doubly-linked list). * **Associated Specification:** To the right, a solid red box labeled `Gilsonite` containing two lines of text: * `requires: ⟦LinkedList<T>⟧ (self, (c, f))` * `ensures: ⟨ c = f ⟩` * **Associated Tool:** Far right, a red clipboard icon labeled `Gillian-Rust`. **3. Connecting Arrows (Blue)** * **Mapping Arrow:** A thick, double-lined blue arrow labeled `⟦LinkedList<T>⟧` points from the `LinkedList<T>` dashed box up to the `Seq<[T]>` dashed box. This represents the abstraction function mapping the concrete list to its pure sequence model. * **Individual Mappings:** Three thin blue arrows point from each concrete node (`v₀`, `v₁`, `v₂`) up to the corresponding pure sequence element (`r₀`, `r₁`, `r₂`). Each is labeled `⟦T⟧`, indicating the valuation of the element's value. * **Encoding Arrow:** A thick, double-lined blue arrow labeled `systematic encoding` points down from the `Pearllite` specification box to the `Gilsonite` specification box. This represents the translation of the pure specification into a form usable for the concrete implementation. ### Detailed Analysis * **Data Flow:** The diagram shows a bidirectional relationship. The concrete `LinkedList<T>` in the "Real world" is abstracted into a pure `Seq<[T]>` via the `⟦LinkedList<T>⟧` mapping. Conversely, a pure specification (`ensures: *self = ^self`) is systematically encoded into a concrete specification (`requires`/`ensures` clauses) for the implementation. * **Specification Details:** * **Pearllite (Pure):** `ensures: *self = ^self`. This is a postcondition stating that the value of `self` after execution (`^self`) is equal to its value before execution (`*self`). This typically denotes a pure function that does not mutate its input. * **Gilsonite (Concrete):** * `requires: ⟦LinkedList<T>⟧ (self, (c, f))`: A precondition stating that the concrete `self` (the linked list) must correspond to a pure sequence model defined by the pair `(c, f)`. * `ensures: ⟨ c = f ⟩`: A postcondition stating that the sequence model `(c, f)` remains unchanged after execution. This mirrors the pure `ensures` clause, translated into the context of the abstraction function. * **Tool Association:** `Creusot` is associated with the pure Pearllite world, while `Gillian-Rust` is associated with the concrete Gilsonite/Rust world. This suggests Creusot is used for verifying pure specifications, and Gillian-Rust is used for verifying the concrete implementation against its encoded specifications. ### Key Observations 1. **Clear Separation of Concerns:** The diagram strictly separates the abstract, mathematical model (green) from the concrete, imperative implementation (red). 2. **Formal Notation:** It uses formal verification notation (`⟦ ⟧` for valuation/abstraction, `*`/`^` for pre/post-state, `requires`/`ensures` clauses). 3. **Linked List Structure:** The "Real world" diagram depicts a singly-linked list of three elements (`v₀`, `v₁`, `v₂`). The `Ø` symbols in the first and last nodes' bottom fields suggest they are the head and tail, with null previous pointers. 4. **Systematic Encoding:** The central blue arrow highlights that the connection between the two worlds is not ad-hoc but follows a defined, systematic process. ### Interpretation This diagram is a conceptual map for a **formal verification pipeline** for low-level data structures. It demonstrates how to bridge the gap between high-level, human-readable specifications (in a pure language like Pearllite) and the messy reality of mutable memory and pointers (in a language like Rust, modeled here by Gilsonite). The core idea is to: 1. **Model:** Define a pure, mathematical model (`Seq<[T]>`) for the data structure. 2. **Specify:** Write functional correctness properties (`ensures`) in the pure language. 3. **Abstract:** Formally define an abstraction function (`⟦LinkedList<T>⟧`) that maps concrete memory states to pure models. 4. **Encode:** Systematically translate the pure specifications into verification conditions (`requires`/`ensures`) for the concrete code, using the abstraction function. 5. **Verify:** Use specialized tools (Creusot for the pure logic, Gillian-Rust for the separation logic of the concrete heap) to prove that the implementation satisfies the encoded specifications. The diagram argues that by maintaining this rigorous connection between the "World of pure representations" and the "Real world," one can achieve high-assurance software where the implementation is proven to match its abstract specification. The presence of two different tools (Creusot, Gillian-Rust) suggests a toolchain where different verifiers handle different layers of abstraction.