hacspec-python

hacspec-python copied to clipboard

chris-wood

chris-wood

chris-wood

implement contract

1

The `contract` speclib ins't actually checking the contract yet.

franziskuskiefer

Function `_F` in blake2b expects a `uint128_t` as third argument but gets `uint64_t` depending on `to_double_word`. @denismerigoux can you look into this?

franziskuskiefer

Add support for running [wycheproof test vectors](https://github.com/google/wycheproof/tree/master/testvectors).

franziskuskiefer

`ctr.py` should be either used or removed.

franziskuskiefer

Type checker

3

To make sure that hacspecs are properly typed we need a way to type check specs. We started out using [mypy](https://github.com/python/mypy) but it turns out it doesn't support everything we...

franziskuskiefer

ocaml parser

2

I'd like to merge the ocaml parser to master if it's working. But I tried to use it and failed 😢 Or am I using it wrong @strub ? ./main.native...

franziskuskiefer

Tracking progress on the spec checker. There are currently three separate efforts - haskell checker in [spec-checker](../tree/master/spec-checker) - python checker in [spec-checker/spec-checker.py](../tree/master/spec-checker/spec-checker.py) - ocaml checker in [spec-checker-ocaml](../tree/ocaml-parser/spec-checker-ocaml) (branch)

franziskuskiefer