aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/HTLgenspec.v
Commit message (Expand)AuthorAgeFilesLines
* Name the externctrl correctness clausesMichalis Pardalos2021-09-121-11/+18
* Guard join state with called module finishMichalis Pardalos2021-09-111-1/+2
* Get HTLgenspec compiling with RAM inferenceMichalis Pardalos2021-08-311-2/+2
* Move list lemmas to own fileMichalis Pardalos2021-08-221-21/+1
* Add length args = length params to Icall specMichalis Pardalos2021-08-211-44/+80
* Strengthen HTLgenspecMichalis Pardalos2021-08-201-9/+14
* Find called module in Icall proofMichalis Pardalos2021-08-191-1/+1
* Complete HTLspec (mostly)Michalis Pardalos2021-08-121-17/+66
* Correct lookup for called funcs, simplify tr_moduleMichalis Pardalos2021-08-041-15/+29
* Check whether callee is internal for IcallMichalis Pardalos2021-08-021-6/+0
* Add "join state is <=Int.max_unsigned" to HTLgenspecMichalis Pardalos2021-06-101-1/+2
* Add "internal calls only" into translation specMichalis Pardalos2021-05-181-20/+30
* Most of Ireturn proofMichalis Pardalos2021-05-161-1/+1
* 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-06-25 07:06:56 +0000