Re: SPARKSkein released

["Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>]

Le Mon, 16 Aug 2010 09:37:59 +0200, Rod Chapman  
<roderick.chapman@googlemail.com> a écrit:

> Altran Praxis and AdaCore have released SPARKSkein - a new reference
> implementation of Skein-512 written and verified using the SPARK
> language and toolset. In particular, this release includes a complete
> proof of type-safety for the implementation, test cases for structural
> coverage, performance, and the reference test vectors from the Skein
> specification. Performance is very close to that of the C reference
> implementation.
>
> Check it out at www.skein-hash.info
>
> There's also a technical paper describing the implementation and
> results, available from
> the same place.
>
>  - Rod Chapman, SPARK Team, Altran Praxis

Was useful:
http://www.skein-hash.info/sites/default/files/SPARKSkein.pdf
says
> [...]
> 4.1.1 Prover says no…a bug is discovered
> The subprogram Skein_512_Final caused someproblems, and led to the  
> discovery of a subtle
> corner-case bug.
> [...]