Let me expand on a couple of these points. There's a bit of history.

The C version of the kernel was originally written by rapidly transcribing the Haskell prototype into C. A number of comments persist in the C source which explain the relationship to the Haskell source, or which refer to the documentation available in the Haskell prototype.

For instance, sendAsyncIPC in C
  ( https://github.com/seL4/seL4/blob/master/src/object/asyncendpoint.c )
was written by transcribing sendAsyncIPC from Haskell
  ( https://github.com/seL4/seL4/blob/master/haskell/src/SEL4/Object/AsyncEndpoint.lhs )

The line-to-line conversion is pretty obvious.

The comment about "WaitingAEP AEP must have non-empty queue" references the matching fail line in the Haskell sources. This is significant because we had, by that stage, proven that the Haskell specification executed without any of the errors/failures occuring, so these failures were actually a golden reference for what should and should not happen.

Someting to clarify: Gerwin claims that the assertions will be proven. He means the *Haskell* assertions. We don't prove anything about the C assertions, which are stripped out by the C preprocessor in the verification target. We did discover once, after verification, that one of the C assertions was wrongly transcribed from its Haskell counterpart, so the debug build of the kernel could panic in a situation where nothing was actually wrong.

On a related note, you asked earlier whether the halt () semantics are baked into the proofs. The C-parser doesn't assign any special meaning to halt () as opposed to any other hidden function. However the C-parser outputs are currently plumbed through a conversion in a theory called Substitute
( https://github.com/seL4/l4v/blob/master/spec/cspec/Substitute.thy )
which happens to wrap calls to the halt procedure in "DontReach" assertions. So we do directly prove that the halt/fail calls that remain in the kernel after preprocessing aren't reached. Gerwin doesn't know about this, because I added this conversion recently and it didn't change any of the proofs.

The substituted definitions are proven to be an anti-refinement of the C-parser's definitions in the theory CToCRefine
( https://github.com/seL4/l4v/blob/master/lib/clib/CToCRefine.thy )
which seems to have ended up in an odd place.

Well, that's probably more details than you ever wanted to know.

Cheers,
    Thomas.

On 28/01/15 08:45, Gerwin Klein wrote: