aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/HTLgenspec.v
Commit message (Expand)AuthorAgeFilesLines
* Update HTL proof for resource sharing (WIP)Michalis Pardalos2021-05-141-1/+3
* Remove reverse matching from monad_crushMichalis Pardalos2021-05-121-2/+2
* Change tr_module to show registers are differentMichalis Pardalos2021-05-121-6/+6
* Fix added tr_code constructorsMichalis Pardalos2021-05-101-12/+19
* Clean up HTLgenspecMichalis Pardalos2021-05-101-127/+130
* Remove unused lemmas in HTLgenspecMichalis Pardalos2021-05-101-414/+33
* Delete inv_incr tactic (unused)Michalis Pardalos2021-05-101-51/+0
* Get entire HTLgenspec proof passingMichalis Pardalos2021-05-101-14/+26
* Progress on tr_module proofMichalis Pardalos2021-05-081-52/+80
* Fully clean up the iter_expand_instr_spec proofMichalis Pardalos2021-05-071-146/+67
* Complete iter_expand_instr_spec proofMichalis Pardalos2021-05-071-14/+23
* Prove a spec for the mapping of function paramsMichalis Pardalos2021-05-061-38/+111
* Solve easier branches of the transf_instr proofMichalis Pardalos2021-05-061-29/+64
* Clean up iter_expand_instr_spec proofMichalis Pardalos2021-05-051-21/+10
* Solve iter_expand_instr_spec by tactic (not Icall)Michalis Pardalos2021-05-051-105/+179
* Add lemmas relating to new HTLgen operationsMichalis Pardalos2021-05-031-49/+71
* Add some statements about externctrl to tr_codeMichalis Pardalos2021-05-031-9/+13
* Give a (questionable) translation spec for HTLgenMichalis Pardalos2021-05-021-12/+24
* Simplify some HTLgenspec proofsMichalis Pardalos2021-05-021-2/+2
* Tie all modules' clock to mainMichalis Pardalos2021-04-301-4/+33
* Get HTLgenproof to compileMichalis Pardalos2021-04-201-86/+87
* [WIP] HTLgenspec proofMichalis Pardalos2021-04-171-46/+34
* Add idle state after returnMichalis Pardalos2021-03-011-27/+30
* Merge branch 'michalis' of https://github.com/mpardalos/vericert into michali...Yann Herklotz2021-02-161-13/+49
* Fix imports to remove warnings when compilingYann Herklotz2021-01-221-4/+14
* Add correct copyright notices in filesYann Herklotz2021-01-101-0/+1
* Add RTLBlock intermediate languageYann Herklotz2020-08-301-0/+641
generated by cgit (git 2.34.1) at 2024-07-04 20:53:38 +0000