search

project-oak / silveroak

Formal specification and verification of hardware, especially for security and privacy.
Apache License 2.0
124 stars 20 forks source link

Make use of tvar typeclass #929

Closed jadephilipoom closed 3 years ago

jadephilipoom commented 3 years ago

Currently, we have a tvar typeclass that should help us infer type denotation definitions, but no instances of the typeclass are ever constructed (although they do exist inside sections). Making denote_type an instance of tvar means we can remove a lot of (var:=denote_type) clauses, which seems like an improvement.

samuelgruetter commented 3 years ago

Does that mean that in a Section with a Context {var: tvar} where cava2.Types is also imported, there are two available tvar instances (denote_type and var)? IIUC, it's not specified which of them Coq's typeclass search will pick. Is that a "risk" you're willing to take? (It might well be worth it, just asking because I'd like to have some understanding of the codebase).

jadephilipoom commented 3 years ago

it's not specified which of them Coq's typeclass search will pick.

Really? I thought in this case the more "local" instance was always preferred. I can always add a | 10 to the denote_type instance to deprioritize it, so it would only be selected if other instances are not available. Does that sound reasonable to you?

jadephilipoom commented 3 years ago

Another option would be to put the denote_type instance in a file like Semantics.v or something that you would only import when doing proofs, not defining circuits. In the previous version of Cava we had two files that exported various core-library components: one for defining circuits, and the other for proofs, so you didn't have to import a bunch of (slow) proof files in order to just write down a circuit. We could introduce a similar structure and have denote_type only declared as an instance for the proofs version.

samuelgruetter commented 3 years ago

I thought in this case the more "local" instance was always preferred.

That seems to be true in my experience, I'm just not sure how much one should rely on it.

We could introduce a similar structure and have denote_type only declared as an instance for the proofs version.

That would be nice, but I'd only do it if it requires very little additional effort. I think this PR could also be merged as is.

jadephilipoom commented 3 years ago

That would be nice, but I'd only do it if it requires very little additional effort. I think this PR could also be merged as is.

It's probably a good idea to re-introduce that structure at some point anyway, so I'll maybe make an issue for it and note in the issue that we should properly handle tvar instances (which will be especially important once we also have a netlist-generation instance).