Lasse Letager Hansen

The `examples/coverage` crate is only partially tested. Enable more tests, e.g. add support / enable tests for closures.

Bignum library

3

There seem to be a couple of bignum implementations, with relations to Hax. - Hacl bignum - hax-lib bigint - Old Hacspec library - Specification of ~nat~ in the annotated...

It should be possible to make a git diff binary, that has a strategy for resolving conflicts, which tries to run an existing proof, otherwise adds a manual conflict resolution...

Phase setup hard to use

1

The errors for misalignment between phases and/or features results in an error, printing a comparison between the two module definitions. This is hard to read, and figuring out what is...

`#[hax_lib::lemma]` in traits

3

Currently the `#[hax_lib::lemma]` attribute is not supported on items in traits.

Overview of old project and dead branches

2

Playing around with writing specifications in Hacspec: - Introducing the group trait (`zkgroup`) into hacspec [group_trait](https://github.com/cmester0/specs/tree/group_trait). - The OVN implementation for adding smart contract support (ConCert) to implementations [OVN](https://github.com/cmester0/specs/tree/ovn). -...

When having large maps updating values gets very slow. The following code: ```prolog pred map_test_fold i:int, i:V, i:V, o:std.map int V. map_test_fold I V U M :- std.fold {std.iota I}...

Close to working tabled type class

10

I have tried to implement tabled type classes to solve possible exponential time type class resolution exemplified by the diamond problem. Any feedback or input is very welcome.