[Agda-dev] More efficient handling of TopLevelModuleNames

[Nicolas Pouillard]

I would avoid the temptation of proving bottom through the use of some 
conflict in the hash function.

On 12/04/2014 07:38 AM, Dominique Devriese wrote:
> I may still be missing something, but are we sure that *cryptographic*
> hashes are needed?  Why not a simpler (and probably faster),
> non-cryptographic hash function, like
>
>    http://en.wikipedia.org/wiki/Java_hashCode()#The_java.lang.String_hash_function
> ?
>
> Regards,
> Dominique
>
>
> 2014-12-03 21:18 GMT+01:00 Guilhem Moulin <guilhem.moulin at chalmers.se>:
>> On Wed, 03 Dec 2014 at 10:11:02 +0100, Nicolas Pouillard wrote:
>>> On 12/02/2014 11:15 PM, Andreas Abel wrote:
>>>> A 128bit hash seems to be an alternative to a String representation of
>>>> TopLevelModuleNames which could lead to a significant speed up of
>>>> serialization.
>>> I support the choice of 128bit hash. As much as one can experiment with
>>> different hash functions to test performances. I would recommend choosing
>>> SHA256 truncated to 128bits. Another option would be to look at SHA3 which
>>> is faster (if I recall well) and secure as well.
>> Actually SHA-512 can be faster than SHA-256 on 64 bits platforms [1],
>> essentially because the word size is larger.  But anyway, the common
>> cryptographic hash functions (MD5 and SHA-{1,2,3}) were optimized for
>> large messages, while I guess a typical QId will hardly be longer than,
>> say 128 bytes.
>>
>> I'm unsure how significant the overhead would be, but one may want to
>> benchmark BLAKE2 (derived of BLAKE, a SHA-3 finalist) which
>>
>>    “is extremely fast both when hashing a single large file and when
>>     hashing many small files. For example, BLAKE2s hashes 64-byte files
>>     quicker than SHA-1, MD5, and even MD4.” — https://blake2.net/
>>
>> --
>> Guilhem.
>>
>> [1] https://community.emc.com/community/edn/rsashare/blog/2010/11/01/sha-2-algorithms-when-sha-512-is-more-secure-and-faster
>>
>> _______________________________________________
>> Agda-dev mailing list
>> Agda-dev at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda-dev
>>
> _______________________________________________
> Agda-dev mailing list
> Agda-dev at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda-dev

-- 
Best regards,
-- NP