[TUHS] Formal Specification and Verification (was Re: TUHS Digest, Vol 33, Issue 5)

[George Michaelson]

Witness to this, the interest in *trying* to apply Coq to Ethereum
smart contracts...

I say "try" because as a complete skeptic, I think the attempt is
doomed except in very small sense. But the reason they are trying is
the importance to FinTech of formally verified state in the expression
of financial transactions. These are serious people. A bunch from
french academic research institutions, a bunch from the CSIRO in
Australia.

I think Perry wrote something of long term value. I encourage you to
write this up somewhere you'd be willing to have published like a tech
blog.

-G

On Sun, Aug 19, 2018 at 5:57 AM, Perry E. Metzger <perry at piermont.com> wrote:
> Sorry for the thread necromancy, but this is a _very_ important
> topic. Perhaps it doesn't belong on tuhs but rather on coff.
>
> This is a pretty long posting. If you don't care to read it, the TL;DR
> is that formal specification and verification is now a real
> discipline, which it wasn't in the old days, and there are systems to
> do it in, and it's well understood.
>
> On 2018-08-06 at 08:52 -0700, Bakul Shah wrote:
>>
>> What counts as a "formal spec"? Is it like Justice Potter
>> Stewart's "I know it when I see it" definition or something
>> better?
>
> At this point, we have a good definition. A formal specification is a
> description of the behavior of a program or piece of hardware in a
> precise machine-readable form that may be used as the basis for fully
> formal verification of the behavior of an implementation. Often these
> days, the specification is given in a formal logic, such as the
> predicative calculus of inductive constructions, which is the logic
> underlying the Coq system.
>
> Isabelle/HOL is another popular system for this sort of work. ACL2 is
> (from what I can tell) of more historical interest but it has
> apparently been used for things like the formal verification of
> floating point and cache control units for real hardware. (It is my
> understanding that it has been many years since Intel would dare
> release a system where the cache unit wasn't verified, and the only
> time in decades it tried to release a non-verified FPU, it got the
> FDIV bug and has never tried that again.) There are some others out
> there, like F*, Lean, etc.
>
> Formal specifications good enough for full formal verification have
> been made for a variety of artifacts along with proofs that the
> artifacts follow the specification. There's a fully formally verified
> C compiler called CompCert for example, based on an operational
> semantics written in Coq. There's another formal semantics for C
> written in K, which is a rather different formal system. There's a
> verified microkernel, seL4, whose specification is written in
> Isabelle/HOL. There's a fully formal specification of the RISC V, and
> an associated verified RTL implementation.
>
> Generally speaking, a formal specification:
>
> 1) Must be machine readable
> 2) The semantics of the underlying specification language must
>    themselves be extremely precisely described. You can't prove the
>    consistency and completeness of the underlying system (see Gödel)
>    but you _can_ still strongly specify the language.
> 3) Must be usable for formal (that is, machine checkable) proofs that
>    implementations comply with the spec, so it has to be sufficiently
>    powerful. Typical systems are now equivalent to higher order logic.
>
> From: "Hellwig Geisse" <hellwig.geisse at mni.thm.de>
> Sent:Mon, 06 Aug 2018 18:30:30 +0200
>>
>>  For me, a "formal spec" should serve two goals:
>>  1) You can reason about the thing that is specified.
>
> Yes.
>
> 2) The spec can be "executed" (i.e., there is an
>>  interpreting mechanism, which lets the spec behave
>>  like the real thing).
>
> Not always reasonable.
>
> First, it is often the case that a spec does not describe execution at
> all. See, for example, the specification of a sorting function I give
> at the end of this message: it simply says "a sorting function is a
> function such that, for all inputs, the return is a non-decreasing
> permutation of the input". This is not executable. It is a purely
> descriptive property, and you cannot extract an executable algorithm
> from the spec.
>
> Second, even when a spec amounts to a description of execution, a
> proof assistant often cannot actually execute it. For example,
> although you can reason about non-terminating execution in pCiC (and
> thus Coq), programs written in a strongly normalizing lambda calculus
> that can be used as a logic must terminate, or functions that did not
> terminate would be inhabitants of all types and the logic would be
> inconsistent. Thus, you cannot execute a program with infinite loops
> inside Coq, although you can reason about them (and indeed, you can
> reason about coinductively defined objects like infinite execution
> traces.)
>
> On Mon, 06 Aug 2018 14:19:31 -0700 "Steve Johnson" <scj at yaccman.com>
> wrote:
>> I take a somewhat more relaxed view of what a spec should be:
>> It should describe a program with enough completeness that a
>> competent programmer could write it from the spec alone.
>
> I think this is a bit more relaxed than is currently accepted.
>
>> The formal systems I have seen would roll over and die when
>> presented with even a simple compiler.__
>
> I don't know what this means. If it is that there aren't
> implementations of languages like pCiC, that's not true, see Coq. If
> it means no one can formally specify a compiler, given that formally
> verified compilers exist, that's also not true.
>
> The "final theorem" proving the correctness of CompCert depends on
> having an operational semantics of both C and the target architecture,
> and says (more or less) that the observed behavior of the input
> program in C is the same as the observed behavior of the output
> program (say in ARM machine language). This is a serious piece of
> work, but it is also something that has actually been done -- the
> tools are capable of the task.
>
>> Additionally, being able to specify that a particular function be
>> carried out by a heapsort, for example, would require that the
>> formalism could describe the heapsort and prove it correct.__ These
>> don't grow on trees...
>
> Formally verifying a couple of sorting algorithms described in Coq is
> a exercise for an intro level class on formal verification. I've done
> it. Once you have the proper primitives described, the specification
> for a sorting algorithm in Coq looks like this:
>
> Definition is_a_sorting_algorithm (f: list nat -> list nat) :=
>   forall al, Permutation al (f al) /\ sorted (f al).
>
> That says "the property "is_a_sorting_algorithm" over a function from
> lists of natural numbers to lists of natural numbers is that the
> output is a permutation of the input in which all the elements are in
> non-decreasing order." The definitions in question are very
> precise. For example, one definition of sorted (the property of being
> a non-decreasing list) is:
>
> Definition sorted (al: list nat) :=
>  forall i j, i < j < length al -> nth i al 0 <= nth j al 0.
>
> and the property of being a permutation, which is relatively
> complicated inductively defined property, is:
>
> Inductive Permutation {A : Type} : list A -> list A -> Prop :=
>     perm_nil : Permutation
>   | perm_skip : forall (x : A) (l l' : list A),
>                 Permutation l l' ->
>                 Permutation (x :: l) (x :: l')
>   | perm_swap : forall (x y : A) (l : list A),
>                 Permutation (y :: x :: l) (x :: y :: l)
>   | perm_trans : forall l l' l'' : list A,
>                  Permutation l l' ->
>                  Permutation l' l'' ->
>                  Permutation l l''.
>
> Coq starts out with basically nothing defined, by the way. Notions
> such as "natural number" and "list" are not built in. Peano naturals
> are defined in the system thusly:
>
> Inductive nat : Type :=
>   | O : nat
>   | S : nat -> nat.
>
> The underlying basis of Coq (i.e. the Predicative Calculus of
> Inductive Constructions) is a dependently typed lambda calculus that's
> astonishingly simple, and the checker for proofs in the system is only
> a few hundred lines long -- the checker is the only portion of the
> system which needs to be trusted.
>
> In recent years, I've noted that "old timers" (such as many of us,
> myself included) seem to be unaware of the fact that systems like Coq
> exist, or that it is now relatively (I emphasize _relatively_) routine
> for substantial systems to be fully formally specified and then fully
> formally verified.
>
>
> Perry
> --
> Perry E. Metzger                perry at piermont.com