aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/HTLgenspec.v
Commit message (Collapse)AuthorAgeFilesLines
* 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
| | | | | | | Necessary, as external calls are present in RTL, but we should not translate them. This will need to be added as a check into the HTL translation. Admitted in HTLgenspec for now.
* 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
| | | | Unnecessary
* Change tr_module to show registers are differentMichalis Pardalos2021-05-121-6/+6
| | | | Proof passed with no changes
* Fix added tr_code constructorsMichalis Pardalos2021-05-101-12/+19
| | | | | They did not indicate what instruction they cover. Now tr_code_call and tr_code_instr only apply to Icall and Ireturn respectively.
* 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
| | | | | Extracted the traversal of call args into a function and gave it a spec, so that it can be used to prove the overall spec for the Icall instruction.
* Solve easier branches of the transf_instr proofMichalis Pardalos2021-05-061-29/+64
| | | | What remains is the ones about the mapping of parameter registers.
* 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
| | | | | I am not yet convinced it is the right one, particularly around the way I've used existentials. I will be updating it as I progress with the proof.
* 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 ↵Yann Herklotz2021-02-161-13/+49
| | | | michalis-merge
* 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 22:53:00 +0000