lesson_4

Lesson 4: Program Verification

From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Definition sorry {T} : T. Admitted.

Brief recap:

We have seen so far:

What is a Coq proof, its justification of truth.
How does the kernel work, typing judgments Γ ⊢ p : T
Syntax of proofs and types, vernacular commands
Basic inductive types
Library built-ins for logic and data types (nat, bool, list)
Tension of computation vs equality
Interfaces vs implementations (using Records with "axioms")
Interpretation of "AST" into Coq's logic
Tactics are program synthesis algoritms
Tacticals ⇒, : and context management
Tactics have rewrite, move, apply, case, elim, simpl, ∃
Intro patterns // and /=
Proof by computation vs by tactics, A ∧ B vs A ∧ B
The reflect predicate , data vs functions
Proof of decidability of equality
Mathematical structures eq, choice, count, fin Type.
Mathematical libraries (math-comp, mathlib)
Infinitude of primes
Extensionality in maths vs in programming / proving. Its trade-offs
Basic structures (abelian groups, rings, commutative rings) Proofs mostly by rewriting
Advanced inference of instances
Matrices (proofs by extensionality / pointwise)
Big operators, indexing on types vs operators / functionsa
Equivalences on types (briefly)
Ring morphisms (briefly)
Polynomials (briefly)
key point: do exercises! Scrach your own itch.
It is harder to model / write theorem statements than to prove them

Program verification

While mathematical proofs are often about equivalences, containement, completions, and generalizations, proofs about programs are quite often about behavior and structure.

Relating the two is a fascinating and ongoing topic, but as of today the tool used are quite different.

While in math we work a lot with abstract structures, It is a rare occurence that the specification of a micro-processor or a programming language will generalize to one.

This has deep implications as developing reusable theories become harder, and we must rely more on tactics and complex automation to achieve an effective proof style.

Moreover, low content of abstract structures means that we will have to encode a lot of information about our objects as data, which can be cumbersome to handle as opposed to more computational encodings.

Fortunately, Coq's inductives excel at that, and that's one of the reasons it has become an incredible popular tool in the PL research community (the other likely being that indeed it is very hard to prove a computer system correct by hand).

A great example is the CompCert Compiler, which related a high-level specification of the C programming language to the result of C compilation, targetting several architectures. CompCert has won the ACM System and Software Award in 2022, and remains a Coq showcase.

More on Inductive Data Types: Indexed Data Types

We will start this lesson by revisiting Coq's inductive data types. We have seen that we can use them in a functional programming style, to define datatypes, abstract syntax trees, and generally different styles of cases and containers. Let's define here a simple lambda calculus:

So far so good, but how can we define the typing relation Γ ⊢ p : T in Coq?

Indexed Inductives

A capability of Coq's inductives that we have not exploited is that their type is not restricted to a Prop/Type kind, but can be any arbitrary well-formed type, and constructors can indeed return instances of that type. That means that an inductive can work as a very general (n-ary!) relation over values of different types, where constructors encode the rules.

Let's see an example:

Inductive relation1 : nat → nat → Prop :=
| Even_step : ∀ n, 0 < n → ~~ odd n → relation1 n (n %/ 2)
| Odd_step : ∀ n, 0 < n → odd n → relation1 n (3 × n + 1).

What are the elements of this relation?

Let's try to state a little theorem, but first we need define some helpers as to make our life easier:

Inductive closure (T : Type) (R : T → T → Prop) : T → T → Prop :=
  | Base : ∀ x y, R x y → closure R x y
  | Trans : ∀ x y z, R x z → closure R z y → closure R x y.

Notation estep n := (@Even_step n erefl erefl).
Notation ostep n := (@Odd_step n erefl erefl).

Lemma some_other_theorem : closure relation1 12 1.
Proof.
apply: (Trans (estep 12)).
apply: (Trans (estep 6)).
apply: (Trans (ostep 3)).
apply: (Trans (estep 10)).
apply: (Trans (ostep 5)).
apply: (Trans (estep 16)).
apply: (Trans (estep 8)).
apply: (Trans (estep 4)).
exact: (Base (estep 2)).
Qed.

Lemma some_theorem : ∀ x, closure relation1 x 1.
Proof. Admitted.

Inductive has_type : list ty → term → ty → Prop :=
| T_Var : ∀ n Γ ty,
           n < size Γ →
        nth t_nat Γ n = ty →

        has_type Γ (var n) ty
| T_Lam :
  ∀ Γ ta tr t,
        has_type [:: ta & Γ] t tr →

    has_type Γ (lam t) (t_arr (ta, tr))
| T_App :
  ∀ Γ tya tyr tf ta,
     has_type Γ tf (t_arr(tya,tyr)) →
     has_type Γ ta tya →

     has_type Γ (app (tf, ta)) tyr.

Example term_id : has_type [::] (lam (var 0)) (t_arr (t_nat,t_nat)).
Proof. by repeat constructor. Qed.

Inductive msg := A | B.

Variables (n_nodes : nat).
Variables (min_delay : nat).
Variables (node : 'I_n_nodes → msg → option ('I_n_nodes × msg)).

Definition msg_queue := 'I_n_nodes → list msg.
Record net :=
  { timestamp : nat
  ; queue : msg_queue
  }.

Implicit Types (nid : 'I_n_nodes).
Implicit Types (q : msg_queue).

Definition update queue nid msg_ : msg_queue :=
  fun m ⇒
    if nid == m
    then queue nid ++ [:: msg_]
    else queue nid.

Definition remove st nid : option (msg_queue × msg) :=
  match st.(queue) nid with
  | [::] ⇒ None
  | [:: msg & l] ⇒ None
  end.

Definition process timestamp q nid (msg : msg) : net :=
  match node nid msg with
  | None ⇒ {| timestamp := timestamp; queue := q |}
  | Some (nid', msg') ⇒
      let timestamp := timestamp + min_delay in
      let q := update q nid' msg' in
      {| timestamp := timestamp; queue := q |}
  end.

Inductive net_step : net → net → Prop :=
  | Send : ∀ nid st msg delta_,
      min_delay < delta_ →
      let timestamp := st.(timestamp) + delta_ in
      let queue := update st.(queue) nid msg in
      let st' := {| timestamp := timestamp
                  ; queue := queue |} in
      net_step st st'
  | Recv :
    ∀ nid st msg delta_ queue',
      0 < delta_ →
      let timestamp := st.(timestamp) + delta_ in
      remove st nid = Some (queue', msg) →
      let st' := process timestamp queue' nid msg in
      net_step st st'
.

Inductive lang :=
  | Var of nat
  | Const of nat
  | Add of lang × lang.

Fixpoint eval (env : list nat) l : nat :=
  match l with
  | Var n ⇒ nth 0 env n
  | Const n ⇒ n
  | Add (e1, e2) ⇒ eval env e1 + eval env e2
  end.

Inductive sop :=
  | Push of nat
  | Swap of nat × nat
  | SAdd.

Definition swap (l : list nat) (i j : nat) : list nat. Admitted.

Inductive s_m : list nat → sop → list nat → Prop :=
  | Op_push : ∀ l n ,
      s_m l (Push n) [:: n & l]
  | Op_swap : ∀ l i j,
      s_m l (Swap (i,j)) (swap l i j)
  | Op_add : ∀ x y l,
      s_m [:: x, y & l] SAdd [:: x + y & l].

Variable (comp : lang → list sop).

Inductive labelled_closure : Type := .
Theorem comp_correct : Type.

Definition jug := Type.