site/posts/StronglySpecifiedFunctionsProgram.v

# *)
(** ** 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.
<