Ben Blaxill

Unfortunately coq-ext-lib has not had a release since our patch and is included in Coq Platform. If we are looking for more standard Coq dependency management, I think it would...

FWIW this is the intended semantics for cava2, using moore machines for control logic would be difficult.

They are equivalent but the recent version doesn't require a binder for "output" to already be present. Technically cava1 is also a mealy machine as its output is dependent on...

I'm happy to change this (how "G" is represented), the choice is mostly syntactical- apart from the false state duplication.

> if all the Cava state was duplicated. I didn't need to duplicate any state for the more realistic SHA256, which includes serialisation, padding, etc., so I don't expect to...

This is not currently derivable, but it should be fine to require this as a precondition: https://github.com/project-oak/silveroak/commit/72a0eb76a9b36eec7ae73ef6fd3ef280c6bf90a0 All the primitive operations effectively have such implicit preconditions and should be closed...

Dune is used by a few of our dependencies and is slated as the future build tool a lot of Ocaml & Coq projects to use. After a bit of...

I've been leaving the states unreduced e.g. ``` Definition Delay'{x : type}(init: denote_type x): Circuit _ [x] x := ``` I don't see this as an issue, but perhaps you...

Another alternative could be to bifurcate the state and variable types, so that state-unit absorbs and the variable-unit doesn't. Since the state of an expression is created from these known...

At this point we have `cava2` succeeding `cava` but depending on it for `Cava/Util`. AFAIK `Cava/Util` has no dependencies and could be made into a standalone library.