axiom-developer
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Down to the metal...


From: Tim Daly
Subject: Down to the metal...
Date: Wed, 26 May 2021 05:36:00 -0400

I'm working on circuit construction and found the tool nMigen
https://m-labs.hk/gateware/nmigen/

nMigen is a Python toolbox for building complex digital hardware.

nMigen offers Bounded Model Checking and formal
verification tool checkers for circuits.

You can, for example, guarantee that a certain signal
state is always true (definitions) or that some combination
of circuit signals never occur (logic checks). Thus you can
formally verify the circuits.

While it seems crazy to think about proofs and Lean
checking "to the metal" level I think you'll be surprised at
how fast the industry is changing. Truly complex hardware,
such as full circuit boards faster than most laptops, has
hit the under-100 dollar range. There are several people
working on RISC-V processors in open source:

https://hackaday.io/project/178826-pineapple-one

https://www.youtube.com/watch?v=YgXJf8c5PLo&list=PLEeZWGE3PwbZTypHq00G-yEX8TEI95lw4

RISC-V is an open source instruction set that allows
user-extensible instructions (e.g. a check-proof instruction
that side-loads proof-check code for an algorithm into the
FPGA). The RISC-V instruction set is MUCH simpler than
the x86, making it easier to write and verify the semantics.

I now have 2 boards that each have both a CPU and an
FPGA on the same board. I can "reprogram the FPGA"
directly from the CPU, thus I can "side load a proof" based
on the algorithm the CPU is running.

So the circuits are correct that implement the proof checker
and the RISC-V instruction set. The proof checker from LEAN
checks the proof for the current algorithm while the algorithm
executes. The algorithm and proof are packaged together in
an AES module so they can't be tampered with. The "proof
state" can be maintained so it can be input as an axiom to
the next algorithm, "chaining" the proofs thru the program.

One of these years I hope to have a "down to the metal"
real-time proof-checked GCD algorithm running in Axiom.
Longer term, as each Axiom algorithm is proven, LEAN
can use Axiom's mathematics "at a higher level".

There is still a long way to go, of course. This is about as
hard are research gets I think, even PhD research. But it
has the long-term potential of eliminating bugs at all levels
which I think will change the industry.

Tim



reply via email to

[Prev in Thread] Current Thread [Next in Thread]