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

[Luke Kenneth Casson Leighton]

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


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

 yeh, looks that way

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

 :)