jadephilipoom
jadephilipoom
Similar to #639: now that we're exporting `Util/`, it would be nice to clean it up a bit. This issue tracks those efforts. - [ ] Remove experimental code and...
See discussion in #929 The previous cava library had two main files that library users would import, `Cava.Cava` (imports needed for circuit definitions and tests) and `Cava.CavaProperties` (imports needed for...
The AES s-box can be implemented in a wide variety of ways, with different timing properties and side-channel resistances. However, all of these implementations can easily be tested exhaustively, because...
Some relevant discussion in https://github.com/project-oak/silveroak/pull/910 Right now, we have a lot of code in `cava/Cava/Util` that is not specific to our project. That means our dependency structure is a little...
See discussion in https://github.com/project-oak/silveroak/issues/891 Sam had the idea to write the SHA-256 spec such that intermediate `N` values are allowed to be greater than `2^32`, and operations like `>>` and...
It's easy to accidentally downgrade a submodule; can we at least warn before push when a submodule is being downgraded? Maybe a git hook will work for this.
Currently, the workflow for the tutorial page is: 1. someone edits `tutorial.v` 2. when Jade next wants to edit the tutorial, she regenerates the HTML using her locally installed Alectryon...
See: https://github.com/project-oak/silveroak/pull/368#discussion_r597288464 https://github.com/JasonGross/coq-tools/issues/55 #373 #368 Currently we have some infrastructure using `coq-tools` to clean up imports: `minimize-requires` targets that try to get rid of unused imports, and `tools/absolutize_requires.sh` that absolutizes...
Let's say I'm trying to prove termination for a loop that looks like this: ``` done = 0 while (!done) { status = MMIOREAD (status_register_addr) ; done = status &...
More of a discussion than an issue. I was talking with @FiloSottile at HACS about the possibility of generating code for curve25519's scalar field using fiat-crypto. My first answer was...