jadephilipoom

Some informal notes on this proposal from a cryptographic perspective. No major issues, but a few thoughts/comments. Section 3.1 says: > Application Identifiers can be used for security policy decisions...

I'm not sure I understand why the semantics are different, and I don't remember discussing a change. @blaxill , would you mind elaborating a bit?

This is clearer to me now, thanks! I don't see a strong reason to change the setup to match cava1, personally, if it hasn't been a problem so far.

Another strategy I've found helpful, especially if you want to avoid the precondition, is to just truncate the number in the spec, e.g.: https://github.com/project-oak/silveroak/blob/db7486778505bcce4ad7824dfa0d6826efe1cd74/silveroak-opentitan/hmac/hw/Sha256Properties.v#L394-L397 Might be hard to read here...

I attempted to resolve this in some experiments [here](https://github.com/project-oak/silveroak/blob/eeec1483ab144b5552c8b74dfc50bd4122675ad4/investigations/ast/AST.v#L177) in case it's helpful; I used typeclasses to automatically find state-type-conversion functions (as opposed to proofs, to avoid issues with opaque...

> 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. There's already...

> Require minimised imports before acceptance? Yes -- maybe also absolutized and in alphabetical order. Essentially, I would want to have a `make` target that cleans up the imports, and...

This seems like a really good idea, especially for communication purposes; interaction is useful for papers and demos. We could also potentially (not as an immediate goal, since I assume...

Current build instructions: - install alectryon dependencies following their README - clone alectryon https://github.com/cpitclaudel/alectryon (I'm at 3b26ed522de533c0f158498c4a408d3825d68f0b but hopefully their main will also work) - set an enviroment variable ALECTRYON_PATH...

> I don't think we need the CI to automatically build the HTML (I am loathed to do anything to slow down the CI further). I believe it wouldn't slow...