Untangling mechanized proofs

An introduction to Alectryon

Alectryon (named after the Greek god of chicken) is a collection of tools for writing technical documents that mix Coq code and prose, in a style sometimes called literate programming.

Coq proofs are hard to understand in isolation: unlike pen-and-paper proofs, proof scripts only record the steps to take (induct on x, apply a theorem, …), not the states (goals) that these steps lead to. As a result, plain proof scripts are essentially incomprehensible without the assistance of an interactive interface like CoqIDE or Proof General.

The most common approach these days for sharing proofs with readers without forcing them to run Coq is to manually copy Coq's output into source code comments — a tedious, error-prone, and brittle process. Any text that accompanies the proof is also embedded in comments, making for a painful editing experience.

Alectryon does better: it automatically captures Coq's output and interleaves it with proof scripts to produce interactive webpages, and it lets you toggle between prose- and code-oriented perspectives on the same document so that you can use your favorite text editing mode for writing prose and your favorite Coq IDE for writing proofs.

Continue reading

A brief introduction to Iris

Introduction to concurrency reasoning in the Iris framework, using a bank as an example program.

Iris is a powerful framework for doing concurrency reasoning. In the PDOS group we've been using it to verify concurrent storage systems, including reasoning about code implemented in Go. Iris stands out among concurrency frameworks in my mind for two reasons: it is extremely modular, allowing us to adapt it to a setting quite different from its original purposes; and it is extremely well-engineered, allowing us to work with it as a library rather than re-implement it. Iris stands out, especially among Coq frameworks, for how usable it is.

Iris is also, unfortunately, a beast to learn. It can be hard to tell where to start, hard to figure out what Iris even is, and hard to appreciate why Iris is such a good framework. In this post we'll work through a sort of "hello, world" example of concurrency verification, proving it correct in Iris. My goal is to convince you that the underlying ideas are approachable and get you excited about Iris; if I succeed then you'll walk away appreciating Iris a bit more and maybe be curious enough to dive deeper into other material.

Continue reading

Recording and editing a talk for an online conference

A step-by-step guide on using guvcview, ffmpeg, and aegisub to assemble a talk video.

Most PL conferences moved online this year, and many are asking authors to pre-record talks to avoid livestreaming difficulties. Here are the steps we followed to record and edit our Kôika talk at PLDI 2020 and our extraction talk at IJCAR 2020. This posts covers preparing and recording the talk, adding the slides, and captioning the final video.

Continue reading

How to write a type-safe unwrap (aka fromJust)

Tips and tricks for writing functions that take proofs as arguments.

Let's say you've written a programming language in Coq. You have nice inductives for your ASTs; one for untyped terms (UntypedAST) and one for typed terms (TypedAST). You wrote a simple typechecker, and maybe an interpreter, too!

typecheck : UntypedAST -> option TypedAST
interp : TypedAST -> Value

You write a few programs…

Example well_typed := UAdd (UNat 1) (UNat 1).
Example ill_typed := UAdd (UNat 1) (UBool true).

… typecheck them:

Definition tc_good := typecheck well_typed.
= Some {| tau := Nat; ast := TAdd (TNat 1) (TNat 1) |} : option TypedAST
Definition tc_bad := typecheck ill_typed.
= None : option TypedAST

… and attempt to run them:

The term "tc_good" has type "option TypedAST" while it is expected to have type "TypedAST".

D'oh! interp takes a TypedAST, but typecheck returns an option. What do we do?

Continue reading

Computing with opaque proofs

Computations with dependent types often get stuck on rewrites that use opaque lemmas. When the corresponding equality is decidable, these lemmas don't need to be made transparent to unblock computation.

A fairly common occurrence when working with dependent types in Coq is to call Compute on a benign expression and get back a giant, partially-reduced term, like this:

Import EqNotations Vector.VectorNotations.
= match match Nat.add_1_r 3 in (_ = H) return (Vector.t nat H) with | eq_refl => [1; 2; 3; 4] end as c in (Vector.t _ H) return (match H as c0 return (Vector.t nat c0 -> Type) with | 0 => fun _ : Vector.t nat 0 => False -> forall x1 : Prop, x1 -> x1 | S x => fun _ : Vector.t nat (S x) => nat end c) with | [] => fun x : False => match x return (forall x0 : Prop, x0 -> x0) with end | h :: _ => h end : (fun (n : nat) (_ : Vector.t nat (S n)) => nat) 3 (rew [Vector.t nat] Nat.add_1_r 3 in ([1; 2; 3] ++ [4]))

This post shows how to work around this issue.

Continue reading