Re: needing an fpga...

[Camm Maguire]

Greetings!  Just a followup on this old thread.

Debian axiom builds and is installed on riscv64:

https://buildd.debian.org/status/fetch.php?pkg=axiom&arch=riscv64&ver=20170501-12&stamp=1676291249&raw=0

There is no 'relaxation' implemented in the linker at the moment.  I
have no idea on what performance penalty if any this incurs.

Take care,

Camm Maguire <camm@maguirefamily.org> writes:

> Greetings!  Doubtless there are many lisp-oriented optimizations
> possible with the instruction set.  GCL, once ported, of course will
> still go through gcc, so the assembler will by default be somewhat
> 'generic'.  GCL can handle special builtin instructions on a platform
> specific basis.
>
> Take care,
>
>
> Tim Daly <axiomcas@gmail.com> writes:
>
>> Camm,
>>
>> Greetings, as you say...
>>
>> That would save me a lot of effort. At the moment I've been
>> targeting FORTH because I have a verilog implementation.
>>
>> I'm hoping for a "Lisp all the way to the metal". That way I can
>> move freely between Axiom's SANE implementation, to the RISC-V
>> hard processor and the soft processor running on the FPGA. Coding
>> the proof checker in a primitive lisp that compiles directly to RISC-V
>> would be sweet.
>>
>> The lower level Lisps only need to be enough to support the
>> compiled forms, such as goto, rather than full lisp with macros.
>> Essentially it only needs to support a thin layer over the RISC-V
>> instruction set.
>>
>> I hadn't thought of it until now but I'm expecting to develop a
>> special set of extended instructions for RISC-V (an "L" extension?)
>> that will support the "side-loading" of proofs into the FPGA from
>> the main CPU. It might be interesting to think about having some
>> of those instructions support primitive Lisp operations, such as
>> CONS, CAR, CDR, etc.
>>
>> I've never heard of porterbox before. I'll have to look at it.
>>
>> Hope you and the family are well.
>>
>> Tim
>>
>> On 6/17/21, Camm Maguire <camm@maguirefamily.org> wrote:
>>> Greetings!  I take it this discussion pertains to the same platform as
>>> Debian's 'riscv64'.  There are virtual machine images which can be run
>>> in emulation, but I have been waiting for a porterbox to become
>>> available to port gcl.  I anticipate the linker will just take a few
>>> days.
>>>
>>> Take care,
>>>
>>> Tim Daly <axiomcas@gmail.com> writes:
>>>
>>>> Program bugs won't go away until we change a few things.
>>>>
>>>> There is a 25 year old effort in proof technology but it is
>>>> divorced from the lower layers.
>>>>
>>>> Since Axiom is a collection of mathematical algorithms
>>>> it, unlike other software, is well specified. That makes it
>>>> ideal for proof technology. It is also well-factored so the
>>>> various definitions and axioms in proofs can be built up
>>>> in an orderly manner.
>>>>
>>>> Compilers and operating systems lie between the code
>>>> and the metal so what the compiler outputs might still
>>>> fail by violating the proof.
>>>>
>>>> Ideally the proof would be carried down to the metal
>>>> and checked by a proof checker so that even if the
>>>> compiler failed, due to perhaps an optimization, the
>>>> failure would be caught during execution before it
>>>> got too damaging.
>>>>
>>>> Proofs also ensure that various "standard" attacks
>>>> like buffer over-runs can't exist.
>>>>
>>>> Schools like CMU are teaching proof techniques in
>>>> their CS classes so the next generation will be well
>>>> aware of when, how, and why to use them.
>>>>
>>>> The gap is between the software and the hardware.
>>>> I'm doing research to cross that gap. That's where
>>>> RISC-V and FPGAs come into play. It allows proofs
>>>> "down to the metal".
>>>>
>>>> RISC-V allows me to extend the instruction set to
>>>> support proofs and FPGA interactions.  I can
>>>> run RISC-V in both hard core (for the code) and
>>>> soft-core (for the FPGA) so I'm able to have a common
>>>> Instruction Set Architecture that "knows" about proofs.
>>>>
>>>> FPGAs allow me to have a hardware implementation
>>>> of proof technology that can't be manipulated by an
>>>> attacker. It also allows the proofs to be checked in
>>>> parallel with the execution so there is minimal impact
>>>> on performance but still have high assurance code.
>>>>
>>>> There is still a long way to go. I have to implement
>>>> the proof checker in the FPGA, for example. I have
>>>> to figure out what the extended ISA needs to be to
>>>> "cross-talk" from the hard IP to the soft IP, etc.
>>>>
>>>> If I'm not chosen for one of the free FPGAs, at least
>>>> let me know when they are generally available.
>>>>
>>>> Tim
>>>>
>>>>
>>>>
>>>> On 6/14/21, Jeff Scheel <jeff@riscv.org> wrote:
>>>>> Thanks for the detailed explanation, Tim.  That's very helpful.
>>>>> -Jeff
>>>>>
>>>>> --
>>>>> Jeff Scheel (he/him/his)
>>>>> Linux Foundation, RISC-V Technical Program Manager
>>>>>
>>>>>
>>>>> On Thu, Jun 10, 2021 at 7:25 PM Tim Daly <axiomcas@gmail.com> wrote:
>>>>>
>>>>>> I'm the lead developer on Axiom, a computer algebra system.
>>>>>> https://en.wikipedia.org/wiki/Axiom_(computer_algebra_system)
>>>>>>
>>>>>> The current effort involves proving mathematical algorithms
>>>>>> "down to the metal". The "metal" target is an FPGA. The
>>>>>> proof system is LEAN (open source from Microsoft):
>>>>>> https://leanprover.github.io/
>>>>>>
>>>>>> The basic idea is to develop a proof of an algorithm.
>>>>>> Once a proof exists there is a "proof checker" that can
>>>>>> check the proof. It is much easier than creating the proof.
>>>>>>
>>>>>> Next, the algorithm and the proof are packaged together
>>>>>> in the ELF (aka proof-carrying code). The bundle is wrapped
>>>>>> in AES to ensure integrity.
>>>>>>
>>>>>> When the algorithm is run in the CPU, the proof is
>>>>>> side-loaded into the FPGA. While the algorithm runs
>>>>>> the proof checker algorithm checks the proof.
>>>>>>
>>>>>> State information from the proofs of algorithms in the
>>>>>> program get "flowed" thru the execution so that the
>>>>>> whole program is proof-checked.
>>>>>>
>>>>>> The current effort is focused on several things: (1) creating
>>>>>> a soft core RISC-V process (it needs to be a verified soft
>>>>>> core),  (2) implementing the proof checker in RISC-V,
>>>>>> (3) figuring out how to communicate between the main
>>>>>> CPU and the RISC-V soft core, and (4) figuring out how
>>>>>> to side-load the proof to run in parallel.
>>>>>>
>>>>>> The proof instructions implementing things like side-load
>>>>>> and communication are currently expected to be an
>>>>>> extended RISCV instruction set.
>>>>>>
>>>>>> I have the open source tool chain set up. I've been learning
>>>>>> how to use them on an icebreaker fpga. The icebreaker is
>>>>>> too small for the whole task but I can construct pieces in
>>>>>> verilog for test purposes.
>>>>>>
>>>>>> Tim Daly
>>>>>> http://axiom-developer.org/~daly
>>>>>>
>>>>>
>>>>
>>>>
>>>>
>>>>
>>>
>>> Jeff Scheel <jeff@riscv.org> writes:
>>>
>>>> Tim, I think the board you want is the PolarFire SoC Icicle board.  You
>>>> can find them on the RISC-V Exchange website:  RISC-V Exchange - RISC-V
>>>> International (riscv.org)
>>>>
>>>> We will be offering these as our next round of boards that go out. Your
>>>> project is a great one so it's simply a matter of when, not if I'll get a
>>>> board for you.  But, I can rest assured that you're "on my list".  ;-)
>>>> -Jeff
>>>>
>>>> --
>>>> Jeff Scheel (he/him/his)
>>>> Linux Foundation, RISC-V Technical Program Manager
>>>>
>>>> On Mon, Jun 14, 2021 at 2:29 PM Tim Daly <axiomcas@gmail.com> wrote:
>>>>
>>>>  Program bugs won't go away until we change a few things.
>>>>
>>>>  There is a 25 year old effort in proof technology but it is
>>>>  divorced from the lower layers.
>>>>
>>>>  Since Axiom is a collection of mathematical algorithms
>>>>  it, unlike other software, is well specified. That makes it
>>>>  ideal for proof technology. It is also well-factored so the
>>>>  various definitions and axioms in proofs can be built up
>>>>  in an orderly manner.
>>>>
>>>>  Compilers and operating systems lie between the code
>>>>  and the metal so what the compiler outputs might still
>>>>  fail by violating the proof.
>>>>
>>>>  Ideally the proof would be carried down to the metal
>>>>  and checked by a proof checker so that even if the
>>>>  compiler failed, due to perhaps an optimization, the
>>>>  failure would be caught during execution before it
>>>>  got too damaging.
>>>>
>>>>  Proofs also ensure that various "standard" attacks
>>>>  like buffer over-runs can't exist.
>>>>
>>>>  Schools like CMU are teaching proof techniques in
>>>>  their CS classes so the next generation will be well
>>>>  aware of when, how, and why to use them.
>>>>
>>>>  The gap is between the software and the hardware.
>>>>  I'm doing research to cross that gap. That's where
>>>>  RISC-V and FPGAs come into play. It allows proofs
>>>>  "down to the metal".
>>>>
>>>>  RISC-V allows me to extend the instruction set to
>>>>  support proofs and FPGA interactions.  I can
>>>>  run RISC-V in both hard core (for the code) and
>>>>  soft-core (for the FPGA) so I'm able to have a common
>>>>  Instruction Set Architecture that "knows" about proofs.
>>>>
>>>>  FPGAs allow me to have a hardware implementation
>>>>  of proof technology that can't be manipulated by an
>>>>  attacker. It also allows the proofs to be checked in
>>>>  parallel with the execution so there is minimal impact
>>>>  on performance but still have high assurance code.
>>>>
>>>>  There is still a long way to go. I have to implement
>>>>  the proof checker in the FPGA, for example. I have
>>>>  to figure out what the extended ISA needs to be to
>>>>  "cross-talk" from the hard IP to the soft IP, etc.
>>>>
>>>>  If I'm not chosen for one of the free FPGAs, at least
>>>>  let me know when they are generally available.
>>>>
>>>>  Tim
>>>>
>>>>  On 6/14/21, Jeff Scheel <jeff@riscv.org> wrote:
>>>>  > Thanks for the detailed explanation, Tim.  That's very helpful.
>>>>  > -Jeff
>>>>  >
>>>>  > --
>>>>  > Jeff Scheel (he/him/his)
>>>>  > Linux Foundation, RISC-V Technical Program Manager
>>>>  >
>>>>  >
>>>>  > On Thu, Jun 10, 2021 at 7:25 PM Tim Daly <axiomcas@gmail.com> wrote:
>>>>  >
>>>>  >> I'm the lead developer on Axiom, a computer algebra system.
>>>>  >> https://en.wikipedia.org/wiki/Axiom_(computer_algebra_system)
>>>>  >>
>>>>  >> The current effort involves proving mathematical algorithms
>>>>  >> "down to the metal". The "metal" target is an FPGA. The
>>>>  >> proof system is LEAN (open source from Microsoft):
>>>>  >> https://leanprover.github.io/
>>>>  >>
>>>>  >> The basic idea is to develop a proof of an algorithm.
>>>>  >> Once a proof exists there is a "proof checker" that can
>>>>  >> check the proof. It is much easier than creating the proof.
>>>>  >>
>>>>  >> Next, the algorithm and the proof are packaged together
>>>>  >> in the ELF (aka proof-carrying code). The bundle is wrapped
>>>>  >> in AES to ensure integrity.
>>>>  >>
>>>>  >> When the algorithm is run in the CPU, the proof is
>>>>  >> side-loaded into the FPGA. While the algorithm runs
>>>>  >> the proof checker algorithm checks the proof.
>>>>  >>
>>>>  >> State information from the proofs of algorithms in the
>>>>  >> program get "flowed" thru the execution so that the
>>>>  >> whole program is proof-checked.
>>>>  >>
>>>>  >> The current effort is focused on several things: (1) creating
>>>>  >> a soft core RISC-V process (it needs to be a verified soft
>>>>  >> core),  (2) implementing the proof checker in RISC-V,
>>>>  >> (3) figuring out how to communicate between the main
>>>>  >> CPU and the RISC-V soft core, and (4) figuring out how
>>>>  >> to side-load the proof to run in parallel.
>>>>  >>
>>>>  >> The proof instructions implementing things like side-load
>>>>  >> and communication are currently expected to be an
>>>>  >> extended RISCV instruction set.
>>>>  >>
>>>>  >> I have the open source tool chain set up. I've been learning
>>>>  >> how to use them on an icebreaker fpga. The icebreaker is
>>>>  >> too small for the whole task but I can construct pieces in
>>>>  >> verilog for test purposes.
>>>>  >>
>>>>  >> Tim Daly
>>>>  >> http://axiom-developer.org/~daly
>>>>  >>
>>>>  >
>>>>
>>>
>>> --
>>> Camm Maguire                                            
>>> camm@maguirefamily.org
>>> ==========================================================================
>>> "The earth is but one country, and mankind its citizens."  --  Baha'u'llah
>>>
>>
>>
>>
>>

-- 
Camm Maguire                                        camm@maguirefamily.org
==========================================================================
"The earth is but one country, and mankind its citizens."  --  Baha'u'llah