# A verification challenge

Hillel Wayne posted a challenge
to find out whether functional programs are really easier to verify than
imperative ones, as some claim. There were three problems, and I am posting Coq
solutions here (two of them by myself).
The first challenge was to prove the correctness of a padding function. Given a
padding character c, a length n and a sequence s, left_pad c n s should
pad s with c on the left until its size reaches n. If the original string
is larger than n, the function should do nothing. My implementation is
similar to other solutions on the web, and reuses functions and lemmas available
in the Math Comp libraries.

## Padding

Implicit Types (c : char) (i n : nat) (s : seq char).

Definition left_pad c n s := nseq (n - size s) c ++ s.

Definition left_pad c n s := nseq (n - size s) c ++ s.

The call to nseq creates a constant sequence with the number of cs that
needs to be added, and appends that sequence to s. Note that subtraction is
truncated: n - size s is equal to 0 when n <= size s.
As the specification for left_pad, I am taking the properties that were
verified in the original
solution in Hillel's post, which was written in Dafny. My proofs are not
automated like in Dafny, but still fairly easy. (The statements are slightly
different because they use the nth function to index into a sequence, which
requires a default element to return when the index overflows.)

Lemma left_pad1 c n s : size (left_pad c n s) = maxn n (size s).

Proof.

by rewrite /left_pad size_cat size_nseq maxnC maxnE [RHS]addnC.

Qed.

Lemma left_pad2 c n s i :

i < n - size s ->

nth c (left_pad c n s) i = c.

Proof.

move=> bound.

by rewrite /left_pad nth_cat size_nseq bound nth_nseq bound.

Qed.

Lemma left_pad3 c n s i :

nth c (left_pad c n s) (n - size s + i) = nth c s i.

Proof.

by rewrite /left_pad nth_cat size_nseq ltnNge leq_addr /= addKn.

Qed.

Interestingly, these properties completely characterize the result of
left_pad: any function f that satisfies the same specification must produce
the same output.

Lemma left_padP f :

(forall c n s, size (f c n s) = maxn n (size s)) ->

(forall c n s i, i < n - size s -> nth c (f c n s) i = c) ->

(forall c n s i, nth c (f c n s) (n - size s + i) = nth c s i) ->

forall c n s, f c n s = left_pad c n s.

Some fans of functional programming claim that it obviates the need for
verification, since the code serves as its own specification. Though exaggerate
(as we will see in the last problem), the claim does have a certain appeal: the
definition of left_pad is shorter and more direct than the specification that
we proved.

## Unique

## Fulcrum

*fulcrum*of a sequence of integers s, which is defined as the index i that minimizes the quantity fv s i shown below in absolute value.

Implicit Types (s : seq int) (n : int).

Definition fv s i :=

\sum_(0 <= l < i) s`_l - \sum_(i <= l < size s) s`_l.

Definition is_fulcrum s i := forall j, `|fv s i| <= `|fv s j|.

Definition fv s i :=

\sum_(0 <= l < i) s`_l - \sum_(i <= l < size s) s`_l.

Definition is_fulcrum s i := forall j, `|fv s i| <= `|fv s j|.

The simplest way out would be to compute fv s i for all indices i and
return the index that yields the smallest value. Instead of writing this
program ourselves, we can just reuse the arg min function available in Math
Comp.

Definition fulcrum_naive s :=

[arg min_(i < ord0 : 'I_(size s).+1) `|fv s i|]%O.

Lemma fvE s i :

fv s i = (\sum_(0 <= l < i) s`_l) *+ 2 - \sum_(0 <= l < size s) s`_l.

Lemma fv_overflow s i : fv s i = fv s (minn i (size s)).

Lemma fulcrum_naiveP s : is_fulcrum s (fulcrum_naive s).

Proof.

rewrite /fulcrum_naive; case: Order.TotalTheory.arg_minP=> //= i _ iP j.

move/(_ (inord (minn j (size s))) erefl): iP.

rewrite (_ : fv s (inord _) = fv s j) //= [RHS]fv_overflow.

by rewrite inordK ?ltnS ?geq_minr //.

Qed.

Unfortunately, this naive implementation runs in quadratic time, and the
problem asked for a

*linear*solution. We can do better by folding over s and computing the values of fv s i incrementally. With a left fold, we can compute the fulcrum with four auxiliary variables defined in the state type below, without the need for extra stack space. (This is a bit more efficient than the original solution, which had to store two sequences of partial sums.)Record state := State {

curr_i : nat; (* The current position in the list *)

best_i : nat; (* The best fulcrum found so far *)

curr : int; (* = fv s curr_i *)

best : int; (* = fv s best_i *)

}.

On each iteration, the fulcrum_body function updates the state st given
n, the current element of the sequence. The main function, fulcrum, just
needs to provide a suitable initial state and return the final value of
best_i.

Definition fulcrum_body st n :=

let curr' := n *+ 2 + st.(curr) in

let curr_i' := st.(curr_i).+1 in

let best' := if `|curr'| < `|st.(best)| then curr' else st.(best) in

let best_i' := if `|curr'| < `|st.(best)| then curr_i' else st.(best_i) in

State curr_i' best_i' curr' best'.

Definition fulcrum s :=

let k := - foldl +%R 0 s in

(foldl fulcrum_body (State 0 0 k k) s).(best_i).

To verify fulcrum, we first prove a lemma about foldl. It says that we
can prove that some property I holds of the final loop state by showing that
it holds of the initial state x0 and that it is preserved on every iteration
in other words, that I is a

*loop invariant*. The property is parameterized by a "ghost variable" i, which counts the number of iterations performed.Lemma foldlP T S f (s : seq T) x0 (I : nat -> S -> Prop) :

I 0%N x0 ->

(forall i x a, (i < size s)%N -> I i x -> I i.+1 (f x (nth a s i))) ->

I (size s) (foldl f x0 s).

We complete the proof by instantiating foldlP with the fulcrum_inv
predicate below. This predicate ensures, among other things, that best_i
holds the fulcrum for the first i positions of the sequence s. Hence, when
the loop terminates, we know that best_i is the fulcrum for all of s.

Variant fulcrum_inv s i st : Prop :=

| FlucrumInv of

(st.(best_i) <= i)%N &

st.(curr_i) = i &

st.(best) = fv s st.(best_i) &

st.(curr) = fv s i &

(forall j, (j <= i)%N -> `|fv s st.(best_i)| <= `|fv s j|).

Lemma fulcrumP s : is_fulcrum s (fulcrum s).

Proof.

rewrite /fulcrum; have ->: - foldl +%R 0 s = fv s 0.

by rewrite /fv big_geq // (foldl_idx [law of +%R]) (big_nth 0) add0r.

set st := foldl _ _ _; suff: fulcrum_inv s (size s) st.

case=> ???? iP j; rewrite [fv s j]fv_overflow; apply: iP.

exact: geq_minr.

apply: foldlP=> {st}; first by split=> //=; case.

move=> i [_ best_i _ _] a iP [/= bP -> -> -> inv].

rewrite (set_nth_default 0 a iP) {a}.

have e: fv s i.+1 = s`_i *+ 2 + fv s i.

by rewrite !fvE big_nat_recr //= [_ + s`_i]addrC mulrnDl addrA.

split=> //=; do 1?[by case: ifP; rewrite // -ltnS ltnW].

move=> j; case: ltngtP => // [j_i|->] _.

case: ifP=> [|_]; last exact: inv.

rewrite -e => /Order.POrderTheory.ltW {}iP.

apply: Order.POrderTheory.le_trans iP _; exact: inv.

by case: Order.TotalTheory.leP => //; rewrite -e.

Qed.