Proof-Carrying Code Generator

Requirements
    ↓
Formal Specification
    ↓
Verified Implementation
    ↓
Proof Obligations
    ↓
Certified Code + Proofs
    ↓
Code Extraction

(* Specification *)
definition sorted_spec :: "nat list ⇒ nat list ⇒ bool" where
  "sorted_spec input output ≡ sorted output ∧ mset output = mset input"

(* Implementation *)
fun insertion_sort :: "nat list ⇒ nat list" where
  "insertion_sort [] = []" |
  "insertion_sort (x # xs) = insert x (insertion_sort xs)"

(* Correctness theorem *)
theorem insertion_sort_correct:
  "sorted_spec input (insertion_sort input)"
proof (induction input)
  case Nil
  then show ?case by (simp add: sorted_spec_def)
next
  case (Cons x xs)
  then show ?case
    using insert_sorted mset_insert
    by (auto simp: sorted_spec_def)
qed

(* Extract code *)
export_code insertion_sort in SML file "sort.sml"

(* Abstract specification *)
Definition find_spec {A} (P : A → bool) (l : list A) : option A :=
  (* Nondeterministic: any element satisfying P *)
  ...

(* Concrete implementation *)
Fixpoint find {A} (P : A → bool) (l : list A) : option A :=
  match l with
  | [] => None
  | x :: xs => if P x then Some x else find P xs
  end.

(* Refinement proof *)
Theorem find_refines : forall A P l,
  find P l = find_spec P l.
Proof.
  (* Proof that concrete refines abstract *)
Qed.

(* Extract *)
Extraction "find.ml" find.

Require Import Program.

Program Definition safe_div (a b : nat) (H : b ≠ 0) : nat :=
  a / b.

(* Proof obligation automatically generated *)
Next Obligation.
  (* Prove division is safe *)
Qed.

lemma array_access_safe:
  "⟦ i < length arr ⟧ ⟹ ∃v. arr ! i = v"
  by auto

fun safe_get :: "'a list ⇒ nat ⇒ 'a option" where
  "safe_get [] _ = None" |
  "safe_get (x # xs) 0 = Some x" |
  "safe_get (x # xs) (Suc n) = safe_get xs n"

lemma safe_get_bounds:
  "safe_get xs i = Some v ⟹ i < length xs"
  by (induction xs i rule: safe_get.induct) auto

Definition safe_head {A} (l : list A) (H : l ≠ []) : A :=
  match l with
  | [] => match H eq_refl with end
  | x :: _ => x
  end.

Lemma safe_head_correct : forall A (l : list A) H,
  l ≠ [] → safe_head l H = hd_error l.
Proof.
  intros. destruct l; auto. contradiction.
Qed.

definition bounded_access :: "'a array ⇒ nat ⇒ 'a option" where
  "bounded_access arr i = (if i < array_length arr
                           then Some (array_get arr i)
                           else None)"

lemma bounded_access_safe:
  "bounded_access arr i = Some v ⟹ i < array_length arr"
  by (simp add: bounded_access_def split: if_splits)

fun factorial :: "nat ⇒ nat" where
  "factorial 0 = 1" |
  "factorial (Suc n) = Suc n * factorial n"

function fact_spec :: "nat ⇒ nat" where
  "fact_spec 0 = 1" |
  "fact_spec n = n * fact_spec (n - 1)"
  by auto

theorem factorial_correct:
  "factorial n = fact_spec n"
  by (induction n) auto

Inductive BST : tree → Prop :=
  | BST_leaf : BST Leaf
  | BST_node : forall l x r,
      BST l → BST r →
      (forall y, In y l → y < x) →
      (forall y, In y r → x < y) →
      BST (Node l x r).

Fixpoint insert (x : nat) (t : tree) : tree :=
  match t with
  | Leaf => Node Leaf x Leaf
  | Node l y r =>
      if x <? y then Node (insert x l) y r
      else if y <? x then Node l y (insert x r)
      else t
  end.

Theorem insert_preserves_BST : forall x t,
  BST t → BST (insert x t).
Proof.
  induction t; intros; simpl.
  - constructor; constructor.
  - inversion H; subst.
    destruct (x <? n) eqn:E1.
    + (* Insert left *)
    + destruct (n <? x) eqn:E2.
      * (* Insert right *)
      * (* Equal, no change *)
Qed.

function gcd :: "nat ⇒ nat ⇒ nat" where
  "gcd a 0 = a" |
  "gcd a b = gcd b (a mod b)"
  by auto
termination
  by (relation "measure (λ(a, b). b)") auto

lemma gcd_terminates:
  "∃result. gcd a b = result"
  by auto

definition binary_search_spec :: "nat list ⇒ nat ⇒ nat option" where
  "binary_search_spec xs target = (
    if sorted xs ∧ target ∈ set xs
    then Some (THE i. i < length xs ∧ xs ! i = target)
    else None)"

fun binary_search :: "nat list ⇒ nat ⇒ nat option" where
  "binary_search xs target = bs_aux xs target 0 (length xs)"

fun bs_aux :: "nat list ⇒ nat ⇒ nat ⇒ nat ⇒ nat option" where
  "bs_aux xs target low high = (
    if low ≥ high then None
    else let mid = (low + high) div 2 in
         if xs ! mid = target then Some mid
         else if xs ! mid < target then bs_aux xs target (mid + 1) high
         else bs_aux xs target low mid)"

lemma bs_aux_bounds:
  "⟦ bs_aux xs target low high = Some i; low ≤ high; high ≤ length xs ⟧
   ⟹ low ≤ i ∧ i < high"
proof (induction xs target low high rule: bs_aux.induct)
  case (1 xs target low high)
  then show ?case
    by (auto simp: Let_def split: if_splits)
qed

lemma bs_aux_no_overflow:
  "⟦ low ≤ high; high ≤ length xs ⟧
   ⟹ (low + high) div 2 < length xs"
  by auto

theorem binary_search_correct:
  "sorted xs ⟹ binary_search xs target = binary_search_spec xs target"
proof -
  assume "sorted xs"
  show ?thesis
  proof (cases "target ∈ set xs")
    case True
    then show ?thesis
      using binary_search_finds_target[OF `sorted xs` True]
      by (simp add: binary_search_spec_def)
  next
    case False
    then show ?thesis
      using binary_search_not_found[OF `sorted xs` False]
      by (simp add: binary_search_spec_def)
  qed
qed

export_code binary_search in SML file "binary_search.sml"
export_code binary_search in OCaml file "binary_search.ml"

(* Verified core *)
definition verified_sort :: "nat list ⇒ nat list" where
  "verified_sort = insertion_sort"

theorem verified_sort_correct:
  "sorted (verified_sort xs) ∧ mset (verified_sort xs) = mset xs"
  by (simp add: verified_sort_def insertion_sort_correct)

(* Export for use in larger system *)
export_code verified_sort in OCaml file "verified_sort.ml"

Module VerifiedList.
  (* Verified operations *)
  Definition safe_nth := ...
  Definition safe_update := ...
  Definition verified_map := ...

  (* Correctness theorems *)
  Theorem safe_nth_correct : ...
  Theorem safe_update_correct : ...
  Theorem verified_map_correct : ...
End VerifiedList.

(* Extract entire module *)
Extraction "verified_list.ml" VerifiedList.