formal-verification

Deflate is a lossless data compression file format that zip and gzip are based on.

The deflate algorithm would be a nice formalisation and verification exercise in HOL. The result of the formalisation effort could be used to con

Prusti uses collections such as HashSet and HashMap, which use a high quality hasher that provides high protection against collisions. However, that hasher is relatively slow and we don't care about HashDoS attacks. So, replacing those collections with FxHashSet and FxHashMap should always be better.

Collections: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_data_structures/fx/i