Initial work on representing HDL and formal verification in Rocq. #56

Merged

programmerjake merged 3 commits from cesar/fayalite:rocq_hdl into master

2025-12-09 16:34:36 +00:00

Author	SHA1	Message	Date
Cesar Strauss	e4210a672f	Check copyright header in Rocq files. All checks were successful / test (pull_request) Successful in 4m4s Details / test (push) Successful in 4m39s Details If we ever add Verilog files, we can "or" both results, I guess.	2025-12-09 07:45:35 -03:00
Cesar Strauss	e54558d848	Demonstrates state with multiple variables and hidden state. Some checks failed / test (pull_request) Failing after 22s Details	2025-12-08 22:00:49 -03:00
Cesar Strauss	46f3519c76	Demonstrate a preliminary mapping from HDL to Rocq. Starts with a very simple example, including a proof by induction.	2025-12-08 19:32:05 -03:00