**diff options**

Diffstat (limited to 'site/posts/StronglySpecifiedFunctionsProgram.v')

-rw-r--r-- | site/posts/StronglySpecifiedFunctionsProgram.v | 533 |

1 files changed, 533 insertions, 0 deletions

diff --git a/site/posts/StronglySpecifiedFunctionsProgram.v b/site/posts/StronglySpecifiedFunctionsProgram.v new file mode 100644 index 0000000..34496b6 --- /dev/null +++ b/site/posts/StronglySpecifiedFunctionsProgram.v @@ -0,0 +1,533 @@ +(** # +<h1>Strongly-Specified Functions in Coq with the <code>Program</code> Framework</h1> + +<p> +This blogpost was initially published on <time +datetime="2017-01-14">2017-01-14</time>, and as later been heavily rewritten in +late 2019. +</p> + # *) + +(** #<div id="generate-toc"></div># *) + +(** For the past few weeks, I have been playing around with <<Program>>. *) + +(** ** The Theory *) + +(** If I had to explain `Program`, I would say `Program` is the heir + of the `refine` tactic. It gives you a convenient way to embed + proofs within functional programs that are supposed to fade away + during code extraction. But what do I mean when I say "embed + proofs" within functional programs? I found two ways to do it. *) + +(** *** Invariants *) + +(** First, we can define a record with one or more fields of type + [Prop]. By doing so, we can constrain the values of other fields. Put + another way, we can specify invariant for our type. For instance, in + SpecCert, I have defined the memory controller's SMRAMC register + as follows: *) + +Record SmramcRegister := { + d_open: bool; + d_lock: bool; + lock_is_close: d_lock = true -> d_open = false; +}. + +(** So [lock_is_closed] is an invariant I know each instance of + `SmramcRegister` will have to comply with, because every time I + will construct a new instance, I will have to prove + [lock_is_closed] holds true. For instance: *) + +Definition lock + (reg: SmramcRegister) + : SmramcRegister. + refine ({| d_open := false; d_lock := true |}). + +(** Coq leaves us this goal to prove. + +<< +reg : SmramcRegister + ============================ +true = true -> false = false +>> + + This sound reasonable enough. *) + +Proof. + trivial. +Defined. + +(** We have witness in my previous article about strongly-specified + functions that mixing proofs and regular terms may leads to + cumbersome code. + + From that perspective, [Program] helps. Indeed, the [lock] + function can also be defined as follows: *) + +From Coq Require Import Program. + +Program Definition lock' + (reg: SmramcRegister) + : SmramcRegister := + {| d_open := false + ; d_lock := true + |}. + +(** *** Pre and Post Conditions *) + +(** Another way to "embed proofs in a program" is by specifying pre- + and post-conditions for its component. In Coq, this is done using + sigma-types. *) + +(** On the one hand, a precondition is a proposition a function input + has to satisfy in order for the function to be applied. For + instance, a precondition for [head : forall {a}, list a -> a] the + function that returns the first element of a list [l] requires [l] + to contain at least one element. We can write that using a + sigma-type. The type of [head] then becomes [forall {a} (l: list a + | l <> []) : a] + + On the other hand, a post condition is a proposition a function + output has to satisfy in order for the function to be correctly + implemented. In this way, `head` should in fact return the first + element of [l] and not something else. + + <<Program>> makes writing this specification straightforward. *) + +(* begin hide *) +From Coq Require Import List. +Import ListNotations. +(* end hide *) +#[program] +Definition head {a} (l : list a | l <> []) : { x : a | exists l', x :: l' = l }. +(* begin hide *) +Abort. +(* end hide *) + +(** We recall that because `{ l: list a | l <> [] }` is not the same + as [list a], in theory we cannot just compare [l] with [x :: + l'] (we need to use [proj1_sig]). One benefit on <<Program>> is to + deal with it using an implicit coercion. + + Note that for the type inference to work as expected, the + unwrapped value (here, [x :: l']) needs to be the left operand of + [=]. + + Now that [head] have been specified, we have to implement it. *) + +#[program] +Definition head {a} (l: list a | l <> []) : { x : a | exists l', cons x l' = l } := + match l with + | x :: l' => x + | [] => ! + end. + +Next Obligation. + exists l'. + reflexivity. +Qed. + +(** I want to highlight several things here: + + - We return [x] (of type [a]) rather than a gigma-type, then <<Program>> is smart + enough to wrap it. To do so, it tries to prove the post condition and because + it fails, we have to do it ourselves (this is the Obligation we solve after + the function definition.) + - The [[]] case is absurd regarding the precondition, we tell Coq that using + the bang (`!`) symbol. + + We can have a look at the extracted code: + +<< +(** val head : 'a1 list -> 'a1 **) +let head = function +| Nil -> assert false (* absurd case *) +| Cons (a, _) -> a +>> + + The implementation is pretty straightforward, but the pre- and + post conditions have faded away. Also, the absurd case is + discarded using an assertion. This means one thing: [head] should + not be used directly from the Ocaml world. "Interface" functions + have to be total. *) + +(** ** The Practice *) + +From Coq Require Import Lia. + +(** I have challenged myself to build a strongly specified library. My goal was to + define a type [vector : nat -> Type -> Type] such as [vector a n] is a list of + [n] instance of [a]. *) + +Inductive vector (a : Type) : nat -> Type := +| vcons {n} : a -> vector a n -> vector a (S n) +| vnil : vector a O. + +Arguments vcons [a n] _ _. +Arguments vnil {a}. + +(** I had three functions in mind: [take], [drop] and [extract]. I + learned few lessons. My main take-away remains: do not use + gigma-types, <<Program>> and dependent-types together. From my + point of view, Coq is not yet ready for this. Maybe it is possible + to make those three work together, but I have to admit I did not + find out how. As a consequence, my preconditions are defined as + extra arguments. + + To be able to specify the post conditions my three functions and + some others, I first defined [nth] to get the _nth_ element of a + vector. + + My first attempt to write [nth] was a failure. + +<< +#[program] +Fixpoint nth {a n} (v : vector a n) (i : nat) {struct v} : option a := + match v, i with + | vcons x _, O => Some x + | vcons x r, S i => nth r i + | vnil, _ => None + end. +>> + + raises an anomaly. *) + +#[program] +Fixpoint nth {a n} (v : vector a n) (i : nat) {struct v} : option a := + match v with + | vcons x r => + match i with + | O => Some x + | S i => nth r i + end + | vnil => None + end. + +(** With [nth], it is possible to give a very precise definition of [take]: *) + +#[program] +Fixpoint take {a n} (v : vector a n) (e : nat | e <= n) + : { v': vector a e | forall i : nat, i < e -> nth v' i = nth v i } := + match e with + | S e' => match v with + | vcons x r => vcons x (take r e') + | vnil => ! + end + | O => vnil + end. + +Next Obligation. + now apply le_S_n. +Defined. + +Next Obligation. + induction i. + + reflexivity. + + apply e0. + now apply Lt.lt_S_n. +Defined. + +Next Obligation. + now apply PeanoNat.Nat.nle_succ_0 in H. +Defined. + +Next Obligation. + now apply PeanoNat.Nat.nlt_0_r in H. +Defined. + +(** As a side note, I wanted to define the post condition as follows: + [{ v': vector A e | forall (i : nat | i < e), nth v' i = nth v i + }]. However, this made the goals and hypotheses become very hard + to read and to use. Sigma-types in sigma-types: not a good + idea. *) + +From Coq Require Import Extraction. + +Extraction Implicit take [a n]. +Extraction take. + +(** +<< +(** val take : 'a1 vector -> nat -> 'a1 vector **) + +let rec take v = function +| O -> Vnil +| S e' -> + (match v with + | Vcons (_, x, r) -> Vcons (e', x, (take r e')) + | Vnil -> assert false (* absurd case *)) +>> + + Then I could tackle `drop` in a very similar manner: *) + +#[program] +Fixpoint drop {a n} (v : vector a n) (b : nat | b <= n) + : { v': vector a (n - b) | forall i, i < n - b -> nth v' i = nth v (b + i) } := + match b with + | 0 => v + | S n => (match v with + | vcons _ r => (drop r n) + | vnil => ! + end) + end. + +Next Obligation. + now rewrite <- Minus.minus_n_O. +Defined. + +Next Obligation. + induction n; + rewrite <- eq_rect_eq; + reflexivity. +Defined. + +Next Obligation. + now apply le_S_n. +Defined. + +Next Obligation. + now apply PeanoNat.Nat.nle_succ_0 in H. +Defined. + +(*begin hide *) +Extraction Implicit drop [a n]. +Extraction drop. +(* end hide *) +(** The proofs are easy to write, and the extracted code is exactly what one might + want it to be: *) +(** +<< +(** val drop : 'a1 vector -> nat -> 'a1 vector **) +let rec drop v = function +| O -> v +| S n -> + (match v with + | Vcons (_, _, r) -> drop r n + | Vnil -> assert false (* absurd case *)) +>> + + But <<Program>> really shone when it comes to implementing extract. I just + had to combine [take] and [drop]. *) + +#[program] +Definition extract {a n} (v : vector a n) (e : nat | e <= n) (b : nat | b <= e) + : { v': vector a (e - b) | forall i, i < (e - b) -> nth v' i = nth v (b + i) } := + take (drop v b) (e - b). + + +Next Obligation. + transitivity e; auto. +Defined. + +Next Obligation. + now apply PeanoNat.Nat.sub_le_mono_r. +Defined. + +Next Obligation. + destruct drop; cbn in *. + destruct take; cbn in *. + rewrite e1; auto. + rewrite <- e0; auto. + lia. +Defined. + +(*begin hide *) +Extraction Implicit extract [a n]. +Extraction extract. +(* end hide *) +(** The proofs are straightforward because the specifications of [drop] and + [take] are precise enough, and we do not need to have a look at their + implementations. The extracted version of [extract] is as clean as we can + anticipate. + +<< +(** val extract : 'a1 vector -> nat -> nat -> 'a1 vector **) +let extract v e b = + take (drop v b) (sub e b) +>> *) + +(** I was pretty happy, so I tried some more. Each time, using [nth], I managed + to write a precise post condition and to prove it holds true. For instance, + given [map] to apply a function [f] to each element of a vector [v]: *) + +#[program] +Fixpoint map {a b n} (v : vector a n) (f : a -> b) + : { v': vector b n | forall i, nth v' i = option_map f (nth v i) } := + match v with + | vnil => vnil + | vcons a v => vcons (f a) (map v f) + end. + +Next Obligation. + induction i. + + reflexivity. + + apply e. +Defined. + +(** I also managed to specify and write [append]: *) + +Program Fixpoint append {a n m} (v : vector a n) (u : vector a m) + : { w : vector a (n + m) | forall i, (i < n -> nth w i = nth v i) /\ + (n <= i -> nth w i = nth u (i - n)) } := + match v with + | vnil => u + | vcons a v => vcons a (append v u) + end. + +Next Obligation. + split. + + now intro. + + intros _. + now rewrite PeanoNat.Nat.sub_0_r. +Defined. + +Next Obligation. + rename wildcard' into n. + destruct (Compare_dec.lt_dec i (S n)); split. + + intros _. + destruct i. + ++ reflexivity. + ++ cbn. + specialize (a1 i). + destruct a1 as [a1 _]. + apply a1. + auto with arith. + + intros false. + lia. + + now intros. + + intros ord. + destruct i. + ++ lia. + ++ cbn. + specialize (a1 i). + destruct a1 as [_ a1]. + apply a1. + auto with arith. +Defined. + +(** Finally, I tried to implement [map2] that takes a vector of [a], a vector of + [b] (both of the same size) and a function [f : a -> b -> c] and returns a + vector of [c]. + + First, we need to provide a precise specification for [map2]. To do that, we + introduce [option_app], a function that Haskellers know all to well as being + part of the <<Applicative>> type class. *) + +Definition option_app + {A B: Type} + (opf: option (A -> B)) + (opx: option A) + : option B := + match opf, opx with + | Some f, Some x => Some (f x) + | _, _ => None +end. + +(** We thereafter use [<$>] as an infix operator for [option_map] and [<*>] as + an infix operator for [option_app]. *) + +Infix "<$>" := option_map (at level 50). +Infix "<*>" := option_app (at level 55). + +(** Given two vectors [v] and [u] of the same size and a function [f], and given + [w] the result computed by [map2], then we can propose the following + specification for [map2]: + + [forall (i : nat), nth w i = f <$> nth v i <*> nth u i] + + This reads as follows: the [i]th element of [w] is the result of applying + the [i]th elements of [v] and [u] to [f]. + + It turns out implementing [map2] with the <<Program>> framework has proven + to be harder than I originally expected. My initial attempt was the + following: + +<< +#[program] +Fixpoint map2 + {A B C: Type} + {n: nat} + (v: vector A n) + (u: vector B n) + (f: A -> B -> C) + {struct v} + : { w: vector C n | forall i, nth w i = f <$> nth v i <*> nth u i } := + match v, u with + | vcons x rst, vcons x' rst' => vcons (f x x') (map2 rst rst' f) + | vnil, vnil => vnil + | _, _ => ! + end. +>> + +<< +Error: Illegal application: +The term "@eq" of type "forall A : Type, A -> A -> Prop" +cannot be applied to the terms + "nat" : "Set" + "S wildcard'" : "nat" + "B" : "Type" +The 3rd term has type "Type" which should be coercible to "nat". +>> *) + +#[program] +Fixpoint map2 + {A B C: Type} + {n: nat} + (v: vector A n) + (u: vector B n) + (f: A -> B -> C) + {struct v} + : { w: vector C n | forall i, nth w i = f <$> nth v i <*> nth u i } := _. + +Next Obligation. + dependent induction v; dependent induction u. + + remember (IHv u f) as u'. + inversion u'. + refine (exist _ (vcons (f a a0) x) _). + intros i. + induction i. + * cbv. + reflexivity. + * simpl. + apply (H i). + + refine (exist _ vnil _). + cbv. + reflexivity. +Qed. + +(** ** Is It Usable? *) + +(** This post mostly gives the "happy ends" for each function. I think I tried + to hard for what I got in return and therefore I am convinced <<Program>> is + not ready (at least for a dependent type, I cannot tell for the rest). For + instance, I found at least one bug in Program logic (I still have to report + it). Have a look at the following code: *) + +#[program] +Fixpoint map2 + {A B C: Type} + {n: nat} + (v: vector A n) + (v': vector B n) + (f: A -> B -> C) + {struct v} + : vector C n := + match v with + | _ => vnil + end. + +(** It gives the following error: + +<< +Error: Illegal application: +The term "@eq" of type "forall A : Type, A -> A -> Prop" +cannot be applied to the terms + "nat" : "Set" + "0" : "nat" + "wildcard'" : "vector A n'" +The 3rd term has type "vector A n'" which should be coercible to "nat". +>> *) +(* begin hide *) +Reset map2. +(* end hide *) |