silveroak

silveroak copied to clipboard

Bumps [nokogiri](https://github.com/sparklemotion/nokogiri) from 1.11.5 to 1.13.6. Release notes Sourced from nokogiri's releases. 1.13.6 / 2022-05-08 Security [CRuby] Address CVE-2022-29181, improper handling of unexpected data types, related to untrusted inputs to...

dependabot[bot]

express `device_implements_state_machine` using only `run1`, without `runUntilResp` (on top of #959)

2

I'm trying to work top-down from `device_implements_state_machine` towards Cava Hmac, and the first too-high-level item that I encountered was that the read/write steps in `device_implements_state_machine` talk about several device steps...

samuelgruetter

Not intended to be merged, just to show generated SystemVerilog

blaxill

Polish contents of Util

2

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...

jadephilipoom

Currently `native_compute` cannot find the ocaml compiler. Either the CI path needs updating or the nix definitions need ocaml adding.

blaxill

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...

jadephilipoom

I need to know that BitVec's are bounded by 2^n.

2

I need the following information about the representation of BitVec. ```coq Axiom denote_bv_max : forall (n : N) (m : denote_type (BitVec (N.to_nat n))), m < 2 ^ n. ```...

fshaked

Parameterize AES proof over s-box

1

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...

jadephilipoom

Combine Uart and SHA256 proofs

2

Compared to the lightbulb's end-to-end theorem, ours currently does not involve any I/O with the external world, but it might actually be quite easy to add that. More concretely, I'm...

samuelgruetter

Separate/upstream Util directory

6

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...

jadephilipoom