[libre-riscv-dev] [Bug 61] Formal Mathematical Proofs needed

[Hendrik Boom]

On Wed, May 01, 2019 at 11:28:01PM +0100, Luke Kenneth Casson Leighton wrote:
> ---
> crowd-funded eco-conscious hardware: https://www.crowdsupply.com/eoma68
> 
> On Wed, May 1, 2019 at 11:08 PM Hendrik Boom <hendrik at topoi.pooq.com> wrote:
> >
> > On Wed, May 01, 2019 at 08:59:02PM +0100, Luke Kenneth Casson Leighton wrote:
> > > hendrik: does the demo at the end (bounded proof) mean *anything* to you?
> > > https://symbiyosys.readthedocs.io/en/latest/quickstart.html
> >
> > I'm going to have to read it in much more detail, but it looks as if
> > they use a proof system to prove that there are no failures within
> > a fixed number of "cycles".  I suspect this is done by some kind of
> > cross between a simulator and a theorem prover, propagating safety
> > assertions cycle by cycle, either forward (which is intuitive) or
> > backward (which seems to have nicer theory).
> 
>  http://bugs.libre-riscv.org/show_bug.cgi?id=61#c8
> 
>  i did a dumb-conversion of samuel falvo's formal proof of the
> MStatus.py that he wrote (i'm good at dumb conversions...) and it
> looks really quite straightforward (the BMC mode, at least).
> 
>  prove mode also worked...
> 
> > Why bounded?  Well, to prove it is safe forever you have to prove that
> > some sufficiently inclusive safety conditions in any step logically
> > imply the sae safty comditions in the next step.  Then by indiction the
> > result follows.  Unfortunately it is difficult to mechanically produce
> > such a set conditions that can, as it were, reproduce themselves into
> > the future.
> >
> > The automated proof assistants I am familiar with all involve in some
> > sense writing computer programs to guide the proof process.  These
> > programs are usually specific to the theorem being proved
> 
>  these seem to be more like... conditions-checking that you'd see in
> any unit test.  although, from what i gather, the more complex "proof"
> engines can actually auto-generate FSMs and full logic tables and
> stuff.
> 
>  "AnyConst" from nmigen looks to be quite useful as a way to represent
> "any value" rather than having to run a hundred billion cycles of all
> possible 48-bit permutations on just *one* input...
> 
> 
> > and there is
> > a rigorous separation between the code driving the proof process and
> > the code actually performing the proof steps so that the driver cannot
> > interfere with the validity of the proof steps.
> 
>  yes, test_mstatus.py seems to be structured that way, as is the
> nmigen FIFO formal proof unit test, all these instantiate a "dut"
> instance which is then tested.
> 
>  you don't "interfere" with the device under test (dut)

You not only don't interfere with the device under test, you also don't 
let the proof strategy interfere with the statements in the proof.
Which is why the original ML (MetaLanguage) was a type-secure language 
with one data type for "theorem" and another for "formula" (i.e., 
something that might or might not ever be proved.  It was not originally 
intended as a general purpose programming language.

The available operations on 'Theorems" were nothing but the formal rules 
for deduction of the logic being used.  The rules for "formula" allowed 
a lot of tinkering so you could write code to try and figure out a proof 
for the thing.

This ancient proof engine was what has later morphed into the ML family 
of general-purpose, mostly-functional programming languages, such aas 
SML, CAML, OCaml, all of them type-safe by design.

-- hendrik