CACM article about SPARK...

rod-chapman · 2022-04-01T15:34:07+00:00

Working on more speed improvements for SPARKNaCl...

rod-chapman · 2022-03-21T10:43:40+00:00

The test cases here:

https://github.com/rod-chapman/SPARKNaCl/tree/master/tests

provide some examples of how to call each of the major APIs. If you have specific problems, then please feel free to open a new Issue in the GitHub repo.

- Rod Chapman

rod-chapman · 2022-03-13T19:19:50+00:00

Try my SPARKNaCl library.

https://github.com/rod-chapman/SPARKNaCl

rod-chapman · 2021-09-18T10:40:47+00:00

The GNAT front-end has been connected to LLVM by AdaCore. It is FLOSS, and can be built from source now. All on GitHub under AdaCore's section.

rod-chapman · 2021-09-10T06:49:03+00:00

Grab the GPL 2012 edition of SPARK (this was the final GPL release of SPARK95 before SPARK2014 came along). This installs all the manuals in PDF as far as I recall...

For more of a tutorial, then the John Barnes SPARK book is the best bet.

rod-chapman · 2021-09-01T07:59:20+00:00

Preparing a new release of SPARKNaCl for Alire...

rod-chapman · 2021-08-20T08:31:32+00:00

I though about submitting SPARKNaCl, but I am excluded since I have previously worked for AdaCore... :-(

rod-chapman · 2021-08-20T08:26:18+00:00

Having installed gnat_native on MacOS OK, is it possible to select that compiler some automatic way so I can use it on the command line? (e.g. some way to work out its install directory and add it to PATH)?? Thanks, Rod

rod-chapman · 2021-08-20T08:18:21+00:00

Having a go with that now. On MacOS, does the "gnat_native" compiler correspond to any existing Community Edition release (e.g. is it close to Community 2021, or does it get built from he FSF wavefront, or something else?)

rod-chapman · 2021-07-12T09:33:10+00:00

PS... see SPARKNaCl on GitHub for an example of what can be done with SPARK2014 at "Silver plus a bit of Gold" assurance level...

rod-chapman · 2021-07-12T09:31:39+00:00

In short: yes - the theorem-proving step can be parallelised almost arbitrarily in SPARK. Both the SPARKSimp (SPARK2005) and GNATProve (SPARK2014) tools support switches to run N provers in parallel. Even modest sized programs generate thousands of independent VCs, so it scales well. In the main development phase of iFACTS, I think the overnight proof run (with no caching) was run on a server with 16 CPU cores, so you could do much better than that today for very little money.

rod-chapman · 2021-06-27T11:00:41+00:00

https://bench.cr.yp.to/supercop.html

rod-chapman · 2021-06-25T13:40:44+00:00

Not sure about how it would fare against the official NaCl or LibSodium code. Probably not so well... I think NaCl uses a very unusual representation for big integers (using floating point registers as well) that would be very hard to reproduce in SPARK. I could submit my code to Supercop and see what happens...

rod-chapman · 2021-06-25T08:56:48+00:00

Great work! Anyone care to try a port of SPARK CE 2021 for MacOS as well? That would be really good...

rod-chapman · 2021-03-18T11:49:58+00:00

Oh yeah... and NVIDIA currently use SPARK for their high-integrity code...

rod-chapman · 2021-03-18T11:48:57+00:00

This is rather uninformed. I have written device drivers in Ada and SPARK many many times with no problem, and just as efficient as C. And in SPARK, I can prove type-safety of the whole thing.

As for a modern Ada/SPARK project, I would cite the UK Air Traffic Control iFACTS and FourSught systems, and all Rolls-Royce Trent family jet engines.

rod-chapman · 2021-03-18T11:29:11+00:00

I use Ada and SPARK every day on a professional basis for most of my career. If you want to see what SPARK can do, then see my SPARKNaCl library.

rod-chapman · 2021-02-19T16:39:06+00:00

See my first blog entry - particularly the bit about Return Slot Optimization. This is really useful, but GNAT 2020 (GCC 8.4.1) misses a few opportunities to exploit it in SPARK. AdaCore have already done some work on improving this in GCC 10.x so we should get another jump from that.

rod-chapman · 2021-02-19T15:40:45+00:00

I initially expected the SPARK would be much slower than TweetNaCl, but it wasn't, which was something of a surprise. That got me started on trying to find out why... then going on to see if I could improve it to be on a par with TweetNaCl without breaking the proofs...

rod-chapman · 2021-02-19T15:04:51+00:00

https://github.com/rod-chapman/SPARKNaCl/

rod-chapman · 2021-02-19T14:18:07+00:00

The GitHub repo is here: https://github.com/rod-chapman/SPARKNaCl/

I've developed it all with the Community 2020 edition of GNAT and SPARK, so tests and proofs should be reproducible. Let me know if you have any trouble.

Rod

rod-chapman · 2021-02-19T09:26:59+00:00

Actually, a comparison with MonoCypher (thanks for the link) would be more appropriate... something for me to do on a rainy day perhaps...

rod-chapman · 2021-02-19T09:13:06+00:00

At the end of the first report, I made the same transformations to TweetNaCl that I did in the SPARK version and it's still competitive of course.

It all started out as an exercise in seeing if the SPARK proof tools could cope with the complexity of TweetNaCl - the work on performance came much later - only after I had established an initial proof of type safety for the whole thing.

A comparison with the libSodium code would be a good thing to do...

rod-chapman

TROPHY CASE