An approach for implementing TUNES

[June Kerby]

> [Specifying a PC]
> > Yes... would it be possible to do it in Coq or ACL2?
> [Problems with Coq and ACL2]

Hmm... well it sounds like we're going to have to make our own logic system
then from scratch probably.

> >> For instance, proving the correctness of the persistent store requires
> >> a model of the hard-disk system (well specified with SCSI; not so with
> >> IDE).
> > It certainly does, but that does not mean we have to specify useless
> > extensions to the IDE standard. We only have to specify enough so that a
> > working TUNES system with a persistent store can be found by the logic
> > system.
> Well, the problem with IDE is precisely that, by lack of specification
> on the way buffers are flushed, failsafe persistence is not implementable
> (contrarily to what is the case with SCSI), unless you're ready to make
> a lot of blind assumptions (hopefully correct guesses) that bring you in
> the safe zone. Of course, even if you don't formally specify the standard
> and your additional assumptions, you're still using it and making them.

Well, if the proof system is unable to come up with a good enough working
TUNES based on specifications that all IDE drives share, then the solution
to me is to add more specifications until it does work (possible breaking
compatibility with other systems that "follow the IDE standard"), but then
limit the resulting TUNES image to only the systems with IDE drives that
share the added specifications. In other words, we may need two (or more)
different TUNES images for ibm-pcs based on what flavor of IDE (or other
hardware they have), just like we will need different images for ibm-pcs
and Macs.

> 
> My point is that specification is a difficult task that cannot be done
> correctly outright; programming proven-correct things with evolving
> specifications is an even more daunting task. These tasks require tools
> that just do not exist currently. It is also the goal of Tunes to bring
> those tools. But we might have to rely not on these tools to bootstrap
> Tunes.
>

Yes, but we don't have to worry about evolving with the specifications yet.
We could bootstrap TUNES on a PC without worrying about extensions that will
come out in later versions of the hardware. Once we have a working TUNES, then
it would be easy to evolve... I guess my point again is that specifying
the PC could be done, and is fairly practical...

> 
> >> Proving the correctness of drawing routines requires a model of the video
> >> (beware that things are often not exactly the same when done by the video
> >> hardware, and that discrepancies should "leak" into a security breach
> >> when misspecifying what happens with video or other inexact I/O).
> > 
> > That is true... If we specify that operation FOO only puts a pixel on the 
> > screen, when it actually makes the monitor blow up, then anyone who the 
> > security privilege to put a pixel on the screen will be able to perform 
> > operation FOO and thus make the monitor blow up.
> >
> The problem is much more subtle: if you formally define "drawing a line"
> by a given routine, but the actual hardware or library routine will
> draw the line in a different way (displacing a few pixels,
> doing anti-aliasing in a different way, etc), then there will be
> a discrepancy between your assumptions and the reality,
> and an ill-intentionned user or a ill-driven program
> might use this discrepancy to prove an absurdity in your system,
> whence to be able to have the system admit any inconsistent axiom.

That's true. If a user can get the system to derive a contradiction, then
he could probably get the system to derive any proposition at all. This is
more serious than i thought... However, in this specific case with the video
drawing, if it is only an error in the hardware, then an contradiction will
not be able to be derived because the system will not know about the 
discrepancy. We will need to be careful not to specify things inconsistently.
Is there is a way to prove that a deductive system is consistent?

> 
> Specifying operations as conceptually "simple" as "drawing a line"
> in a way that be both correct and useful is _quite_ challenging!

Yes, we would need to be lenient enough to allow the system to make "lines"
out of square pixels, yet strict enough that it still looks like a line. 

> > [proving by changing point of view]
> 
> A very well-known example of a theorem people use to demonstrate their
> favorite proof system is REVERSE-REVERSE: to reverse a list (structure
> inductively defined from cons and nil) is an involutive operation.
> Well, the elegant and interesting way to do this (I think) is to
> prove that the free inductive presentation of lists with cons and nil
> is isomorphic to the presentation of lists as either the empty list,
> or a non-empty one, with non-empty lists being inductively defined
> from atom and append, with the equations making append associative.
> Once you have this equivalence between two points of views,
> the non-trivial theorem REVERSE-REVERSE among cons-nil lists
> becomes a trivial theorem about (recursively) commuting the arguments
> to append among nil-atom-append lists.

Although I don't quite follow this example (can't figure out what "involutive"
means used here), I do understand what you're saying. This might be a good
technique to put into our deductive system, whenever we make one.

> >> Of course, when we begin massively specifying things,
> >> we may have to completely reimplement "dirty" parts of the system
> >> so as to be able to achieve provable code.
> >
> > Yes, we would. But I am still wondering if we can escape writing any 
> > "dirty" code at all, by finding or writing a logic system to find a TUNES,
> > giving the TUNES definition, and the definition of our target.
> >
> You seem to ignore that writing a logic system, or adapting one so it
> be reflective, _does_ include a lot of dirty work!

That's true. The question is, which would require more "dirty" code
(hand-coded code that is not proven correct), and which would be easier:
1) Writing a deductive system to find TUNES, or 
2) Writing a mini-TUNES using (maybe including orthogonal persistence, and a
   nicer overall development environment than what we have now), and then
   writing a deductive system to find TUNES?

Retro and Brix seem to be attempts at #2 (are there others?). I'm not sure
which would be easier, but I tend to favor #1.

Anyone else have any more thoughts on this?

- Brent Kerby ("Iepos")