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

[Hendrik Boom]

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).

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 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. 

A brief glance suggests to me that this may not be structured in the 
same way. 

I will investigate further.  It is going to be interesting.

Unfortunately, I'm due for surgery next Tuesday, and a surgeon's idea of 
easy peasy is "You can walk as far as a taxi to teke you home" and not 
"When you get home you'll be able to do the usual there", 
so we'll have to wait and see...

-- hendrik

> 
> what about this?
> https://github.com/m-labs/nmigen/blob/master/nmigen/test/test_lib_fifo.py
> 
> ngggggh!
> 
> On Wed, May 1, 2019 at 8:54 PM <bugzilla-daemon at libre-riscv.org> wrote:
> >
> > http://bugs.libre-riscv.org/show_bug.cgi?id=61
> >
> > --- Comment #6 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
> > https://github.com/m-labs/nmigen/blob/master/nmigen/test/test_lib_fifo.py
> >
> > tracking through from there is something called FHDLTestCase.assertFormal
> > which calls the prerequisite sby proof, creating the sby config file
> > in the process.
> >
> > --
> > You are receiving this mail because:
> > You are on the CC list for the bug.
> > _______________________________________________
> > libre-riscv-dev mailing list
> > libre-riscv-dev at lists.libre-riscv.org
> > http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev
> 
> _______________________________________________
> libre-riscv-dev mailing list
> libre-riscv-dev at lists.libre-riscv.org
> http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev