HAI Experiments with Relational Specification of Hardware This is just a sketch repository. All files should be single-file Coq code right now.