Skip to content

Latest commit

 

History

History
217 lines (174 loc) · 17.4 KB

README.md

File metadata and controls

217 lines (174 loc) · 17.4 KB
Raw

This is a fork of calf for demonstrating our work on verified cost analysis of joinable red black trees.

A verified cost analysis of joinable red black trees

We present our mechanization of correctness and cost verification of joinable red black trees in calf, which is embedded in Agda.

Dependency

To type-check the code, we require Agda version 2.6.3. Moreover, we make use of the latest (unreleased) Agda standard library. The commit hash for the version we have tested with is here.

File location

calf: A Cost-Aware Logical Framework

The calf language is a cost-aware logical framework for studying quantitative aspects of functional programs.

This repository contains the Agda implementation of calf, as well as some case studies of varying complexity.

HTML Browsing

The source code may be viewed interactively with (semantic) syntax highlighting in the browser using the HTML files in the ./html directory. These files were generated by running:

agda --html --html-dir=html src/index.agda

You may want to start by opening html/index.html.

To view a specific module M, open html/M.html in a web browser. For example, open html/Examples.Sorting.Parallel.html to view the module Examples.Sorting.Parallel.

Installation

This implementation of calf has been tested using:

  • Agda v2.6.3, with agda-stdlib v1.7.1 (preferred)
  • Agda v2.6.2, with agda-stdlib v1.7
  • Agda v2.6.1.3, with agda-stdlib v1.6

Installation instructions may be found in INSTALL.md.

Language Implementation

Cost Monoid Parameterization

calf is parameterized by a cost monoid (ℂ, +, zero, ≤). The formal definition, CostMonoid, is given in Calf.CostMonoid. The definition of a parallel cost monoid (ℂ, ⊕, 𝟘, ⊗, 𝟙, ≤) is given, as well, as ParCostMonoid.

Some common cost monoids and parallel cost monoids are given in Calf.CostMonoids; for example, ℕ-CostMonoid simply tracks sequential cost. Note that every ParCostMonoid induces a CostMonoid via the additive substructure (ℂ, ⊕, 𝟘, ≤).

Core Language

The language itself is implemented via the following files, which are given in a dependency-respecting order.

The following modules are not parameterized:

  • Calf.Prelude contains commonly-used definitions.
  • Calf.Metalanguage defines the basic dependent Call-By-Push-Value (CBPV) language, using Agda postulates and rewrite rules.
  • Calf.PhaseDistinction defines the phase distinction of extension and intension, including the extensional phase ext, the open/extensional modality ◯, and the closed/intensional modality ●.
  • Calf.Noninterference contains theorems related to the phase distinction/noninterference.

The following modules are parameterized by a CostMonoid:

  • Calf.Step defines the computational effect step and the associated coherence laws via rewrite rules.

The following modules are parameterized by a ParCostMonoid:

  • Calf.ParMetalanguage defines the parallel pairing operation _&_ whose cost structure is given by the product operation of a ParCostMonoid (i.e., _⊗_).

Types

In src/Calf/Types, we provide commonly-used types.

The following modules are not parameterized:

The following modules are parameterized by a CostMonoid:

  • Calf.Types.Bounded defines a record IsBounded A e c that contains a proof that the cost of e (of type A) is bounded by c : ℂ. Additionally, it provides lemmas for proving the boundedness of common forms of computations.
  • Calf.Types.BoundedFunction defines cost-bounded functions using IsBounded.
  • Calf.Types.BigO gives a definition of "big-O" asymptotic bounds as a relaxation of IsBounded. In particular, an element of the type given A measured-via size , f ∈𝓞(g) (i.e., "given an input of type A and a size measure size on A, f is in 𝓞(g)) is a lower bound on input sizes n' and a constant multiplier k along with a proof h that for all inputs x with n' ≤ size x, f x is bounded by k multiples of g (size x), denoted n' ≤n⇒f[n]≤ k g[n]via h.

Examples

We provide a variety of case studies in src/Examples.

Sequential

Examples.Id

  • module Easy
    • Definition of the program id which trivially returns its input.
    • Theorem id/correct stating the (trivially true) correctness of id.
    • Theorem id≤id/cost stating that the cost of id n is bounded by id/cost n = 0.
    • Theorem id/asymptotic : given nat measured-via (λ n → n) , id ∈𝓞(λ n → 0) stating that id is in 𝓞(0).
  • module Hard
    • Definition of the program id which reconstructs its input via induction.
    • Theorem id/correct stating the correctness of id.
    • Theorem id≤id/cost/closed stating that the cost of id n is bounded by n.
    • Theorem id/asymptotic : given nat measured-via (λ n → n) , id ∈𝓞(λ n → n) stating that id is in 𝓞(n), where n is the input number.
  • A proof that Easy.id and Hard.id are extensionally equivalent, easy≡hard : ◯ (Easy.id ≡ Hard.id).

Examples.Gcd

  • A calf implementation of Euclid's algorithm for gcd.
  • Examples.Gcd.Euclid
    • Specification of the cost model via the instrumented operation mod.
    • Definition of the type gcd/i, which specifies that inputs to Euclid's algorithm should be ordered (first is greater than second).
    • Definition of the program gcd/depth that computes the recursion depth of Euclid's algorithm.
  • Examples.Gcd.Clocked
    • The clocked version of Euclid's algorithm gcd/clocked in which the first parameter is used to justify recursive calls.
    • The actual algorithm gcd, obtained by instantiating the clock parameter by gcd/depth.
    • The theorem gcd≤gcd/depth stating that the cost of Euclid's algorithm is bounded by the recursion depth gcd/depth.
  • Examples.Gcd.Spec
    • Theorems gcd≡spec/zero and gcd≡spec/suc stating the behavioral correctness of gcd in terms of the defining equations of Euclid's algorithm.
  • Examples.Gcd.Refine
    • Refinement of the bound gcd/depth -- the theorem gcd/depth≤gcd/depth/closed states that the cost of gcd is bounded by suc ∘ fib⁻¹.

Examples.Queue

  • A calf implementation of Batched queues.
  • Specification of the cost model as the number of list iterations via the axiom list/ind/cons.
  • Upper bounds on the cost of individual enqueue and dequeue operations:
    • The theorem enq≤enq/cost stating that enqueue has zero cost.
    • The theorem deq≤deq/cost stating that dequeue has linear cost.
  • Amortized analysis of sequences of enqueue and dequeue operations:
    • The theorem acost≤2*|l| stating that the amortized cost of a sequence of queue operations is at most twice the length of the sequence.

Parallel

Examples.TreeSum

  • Definition of the program sum which sums the elements of a tree, incurring unit cost when performing each addition operation. At each node, the recursive calls are computed in parallel.
  • Theorem sum≤sum/cost/closed stating that the cost of sum t is bounded by sum/cost/closed t = size t , depth t.

Examples.Exp2

  • module Slow
    • Definition of the program exp₂ which computes the exponentation of two by its input by performing two identical recursive calls.
    • Theorem exp₂/correct stating the correctness of exp₂.
    • Theorem exp₂≤exp₂/cost/closed stating that the cost of exp₂ n is bounded by exp₂/cost/closed n = (pred[2^ n ] , n), where pred[2^ n ] = (2 ^ n) - 1. Since two identical recursive calls are made, the work is exponential, but the span is still linear.
  • module Fast
    • Definition of the program exp₂ which computes the exponentation of two by its input via a standard recursive algorithm.
    • Theorem exp₂/correct stating the correctness of exp₂.
    • Theorem exp₂≤exp₂/cost/closed stating that the cost of exp₂ n is bounded by exp₂/cost/closed n = (n , n).
  • A proof that Slow.exp₂ and Fast.exp₂ are extensionally equivalent, slow≡fast : ◯ (Slow.exp₂ ≡ Fast.exp₂).

Hybrid

Examples.Sorting

First, we develop a common collection of definitions and theorems used in both sequential and parallel sorting.

  • Examples.Sorting.Comparable
    • Record Comparable describing the requirements for a type to be comparable, including h-cost, a hypothesis that each comparison is bounded by unit cost. This serves as the cost model for sorting.
  • Examples.Sorting.Core
    • Predicates for correctness of sorting, based on Sorted and the permutation relation ↭ from agda-stdlib. The predicate IsSort sort states that sort is a correct sorting algorithm.
    • Theorem IsSort⇒≡, which states that any two correct sorting algorithms are extensionally equivalent.

Examples.Sorting.Sequential

Here, we use cost monoid ℕ-CostMonoid, tracking the total number of sequential steps incurred.

  • Examples.Sorting.Sequential.InsertionSort
    • Definition of the program sort implementing insertion sort.
    • Theorem sort/correct : IsSort sort verifying the correctness of sort.
    • Theorem sort≤sort/cost/closed stating that the cost of sort l is bounded by sort/cost/closed l = length l ².
    • Theorem sort/asymptotic : given (list A) measured-via length , sort ∈𝓞(λ n → n ²) stating that sort is in 𝓞(n ²), where n is the length of the input list.
  • Examples.Sorting.Sequential.MergeSort
    • Examples.Sorting.Sequential.MergeSort.Split
      • Definition of the program split, which splits a list in halves.
      • Theorem split/correct verifying correctness properties of split.
      • Theorem split≤split/cost stating that the cost of split l is bounded by zero, since splitting a list into halves requires no comparisons.
    • Examples.Sorting.Sequential.MergeSort.Merge
      • Definition of the program merge, which merges a pair of sorted lists.
      • Theorem merge/correct verifying correctness properties of merge.
      • Theorem merge≤merge/cost/closed stating that the cost of merge (l₁ , l₂) is bounded by length l₁ + length l₂.
    • Definition of the program sort implementing merge sort.
    • Theorem sort/correct : IsSort sort verifying the correctness of sort.
    • Theorem sort≤sort/cost/closed stating that the cost of sort l is bounded by sort/cost/closed l = ⌈log₂ length l ⌉ * length l.
    • Theorem sort/asymptotic : given (list A) measured-via length , sort ∈𝓞(λ n → n * ⌈log₂ n ⌉) stating that sort is in 𝓞(n * ⌈log₂ n ⌉), where n is the length of the input list.

Theorem isort≡msort : ◯ (ISort.sort ≡ MSort.sort) states that InsertionSort.sort and MergeSort.sort are extensionally equivalent.

Examples.Sorting.Parallel

Here, we use parallel cost monoid ℕ²-ParCostMonoid, tracking a pair of natural numbers corresponding to the work (sequential cost) and span (idealized parallel cost), respectively.

  • Examples.Sorting.Parallel.InsertionSort
    • Definition of the program sort implementing insertion sort.
    • Theorem sort/correct : IsSort sort verifying the correctness of sort.
    • Theorem sort≤sort/cost/closed stating that the cost of sort l is bounded by sort/cost/closed l = (length l ² , length l ²).
    • Theorem sort/asymptotic : given (list A) measured-via length , sort ∈𝓞(λ n → n ² , n ²) stating that sort is in 𝓞(n ²) work and 𝓞(n ²) span, where n is the length of the input list.
  • Examples.Sorting.Parallel.MergeSort
    • Examples.Sorting.Parallel.MergeSort.Split
      • Definition of the program split, which splits a list in halves.
      • Theorem split/correct verifying correctness properties of split.
      • Theorem split≤split/cost stating that the cost of split l is bounded by 𝟘 = (zero , zero), since splitting a list into halves requires no comparisons.
    • Examples.Sorting.Parallel.MergeSort.Merge
      • Definition of the program merge, which sequentially merges a pair of sorted lists.
      • Theorem merge/correct verifying correctness properties of merge.
      • Theorem merge≤merge/cost/closed stating that the cost of merge (l₁ , l₂) is bounded by (length l₁ + length l₂ , length l₁ + length l₂), since this implementation of merge is sequential.
    • Definition of the program sort implementing merge sort, where both recursive calls to sort are performed in parallel (via the parallel pairing operation _&_).
    • Theorem sort/correct : IsSort sort verifying the correctness of sort.
    • Theorem sort≤sort/cost/closed stating that the cost of sort l is bounded by sort/cost/closed l = (⌈log₂ length l ⌉ * length l , 2 * length l + ⌈log₂ length l ⌉).
    • Theorem sort/asymptotic : given (list A) measured-via length , sort ∈𝓞(λ n → n * ⌈log₂ n ⌉ , n) stating that sort is in 𝓞(n * ⌈log₂ n ⌉) work and 𝓞(n) span, where n is the length of the input list.
  • Examples.Sorting.Parallel.MergeSortPar
    • Examples.Sorting.Parallel.MergeSortPar.Merge
      • Definition of the program merge, which merges a pair of sorted lists in parallel using auxiliary functions splitMid and splitBy.
      • Theorem merge/correct verifying correctness properties of merge.
      • Theorem merge≤merge/cost/closed stating that the cost of merge (l₁ , l₂) is bounded by (pred[2^ ⌈log₂ suc (length l₁) ⌉ ] * ⌈log₂ suc (length l₂) ⌉ , ⌈log₂ suc (length l₁) ⌉ * ⌈log₂ suc (length l₂) ⌉), where pred[2^ n ] = (2 ^ n) - 1.
    • Definition of the program sort implementing merge sort, where both recursive calls to sort are performed in parallel. This is identical to MergeSort.sort, but using the parallel merge operation MergeSortPar.Merge.Merge.
    • Theorem sort/correct : IsSort sort verifying the correctness of sort.
    • Theorem sort≤sort/cost/closed stating that the cost of sort l is bounded by sort/cost/closed l = (⌈log₂ length l ⌉ * length l * ⌈log₂ suc ⌈ length l /2⌉ ⌉ , ⌈log₂ length l ⌉ * ⌈log₂ suc ⌈ length l /2⌉ ⌉ ²).
    • Theorem sort/asymptotic : given (list A) measured-via length , sort ∈𝓞(λ n → n * ⌈log₂ n ⌉ ² , ⌈log₂ n ⌉ ^ 3) stating that sort is in 𝓞(n * ⌈log₂ n ⌉ ²) work and 𝓞(⌈log₂ n ⌉ ^ 3) span, where n is the length of the input list.

Theorem isort≡msort : ◯ (ISort.sort ≡ MSort.sort) states that InsertionSort.sort and MergeSort.sort are extensionally equivalent. Similarly, msort≡psort : ◯ (MSort.sort ≡ PSort.sort) states that MergeSort.sort and MergeSortPar.sort are extensionally equivalent.