SPARK GPL 2011 and SPARKSkein 2011

SPARK GPL 2011 and SPARKSkein 2011

[Rod Chapman]

SPARK GPL 2011 is now up on libre.adacore.com.

We've also updated the SPARKSkein release to meet
v1.3 of the Skein specification, and reproduced all
analyses and proofs with the GPL 2011 toolset.
This is at www.skein-hash.info.

 - Rod

Re: SPARK GPL 2011 and SPARKSkein 2011

[Stephen Leake]

Rod Chapman <roderick.chapman@googlemail.com> writes:

> SPARK GPL 2011 is now up on libre.adacore.com.
>
> We've also updated the SPARKSkein release to meet
> v1.3 of the Skein specification, and reproduced all
> analyses and proofs with the GPL 2011 toolset.
> This is at www.skein-hash.info.

Very interesting!

However, I think www.skein-hash.info could use a bit more propaganda
about what SPARKskein is, and why people should care about it.

For example, here is the abstract from the paper about SPARKskein:

(http://www.skein-hash.info/sites/default/files/SPARKSkein.pdf)

    This paper describes SPARKSkein – a new reference implementation of
    the Skein algorithm, written and verified using the SPARK language
    and toolset. This paper is aimed at readers familiar with the Skein
    algorithm and its existing reference implementation, but who might
    not be familiar with SPARK. The new implementation is readable,
    completely portable to a wide-variety of machines of differing
    word-sizes and endian-ness, and “formal” in that it is subject to a
    proof of type safety. This proof also identified a subtle bug in the
    implementation which persists in the C version of the code. The new
    code offers similar performance to the existing reference
    implementation. As a further result of this work, we have identified
    several opportunities to improve both the SPARK tools and GCC.

Just getting this on the web page somewhere (perhaps on
http://www.skein-hash.info/downloads) would be very good. _Especially_
the parts about being completely portable (I'm assuming the C version is
not?), finding a bug in the C version, and "similar performance".

This is an excellent opportunity to advertise the benefits of Ada and
SPARK.

Hmm. That info is available at
http://www.altran-praxis.com/news/SPARKskein_16_Aug_10.aspx, which is
probably a more appropriate place for such things. Pardon my enthusiasm :)


Any update on the 'future work' section of the paper (improvements for
gnat, spark)?

-- 
-- Stephe