aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls
Commit message (Expand)AuthorAgeFilesLines
...
* | Move HTL renaming pass to own fileMichalis Pardalos2021-06-063-240/+230
* | Add explanations for axiomsMichalis Pardalos2021-05-181-11/+13
* | Add axiom that only the main contains storesMichalis Pardalos2021-05-181-4/+10
* | Qed on top-level correctness lemmaMichalis Pardalos2021-05-181-2/+2
* | Update lemmata broken by changes to semanticsMichalis Pardalos2021-05-181-42/+35
* | Get Icall translation lemma *statement* passingMichalis Pardalos2021-05-181-15/+17
* | Add "internal calls only" into translation specMichalis Pardalos2021-05-182-70/+94
* | Get Ireturn proof to pass againMichalis Pardalos2021-05-181-11/+8
* | Callstate proof with holes regarding stackMichalis Pardalos2021-05-181-129/+97
* | Complete Returnstate proofsMichalis Pardalos2021-05-181-19/+3
* | Complete Returnstate proofsMichalis Pardalos2021-05-172-78/+173
* | Elaborate how stackframes match (match_frames)Michalis Pardalos2021-05-171-3/+29
* | Add module idents to the semanticsMichalis Pardalos2021-05-172-51/+66
* | Most of Ireturn proofMichalis Pardalos2021-05-164-17/+80
* | Update HTL proof for resource sharing (WIP)Michalis Pardalos2021-05-142-242/+307
* | Give new semantics for HTLMichalis Pardalos2021-05-131-15/+41
* | Get HTLgenproof passing again (with admits)Michalis Pardalos2021-05-131-230/+172
* | Remove "active_call" from HTL semanticsMichalis Pardalos2021-05-132-28/+24
* | 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-062-43/+123
* | Solve easier branches of the transf_instr proofMichalis Pardalos2021-05-061-29/+64
* | Define map_incr to clarify st_incrMichalis Pardalos2021-05-051-9/+13
* | 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
* | Rewrite transf_instr, move complicated part upMichalis Pardalos2021-05-031-6/+6
* | 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
* | Add externctrl props to HTLgen's st_propMichalis Pardalos2021-05-031-41/+44
* | Use ltac:() instead of Program in HTLgenMichalis Pardalos2021-05-031-140/+116
* | Use Defined for obligations in Program DefinitionsMichalis Pardalos2021-05-021-12/+12
* | Give a (questionable) translation spec for HTLgenMichalis Pardalos2021-05-022-39/+61
* | Simplify some HTLgenspec proofsMichalis Pardalos2021-05-021-2/+2
* | Handle declarations of externctrl regs in VerilogMichalis Pardalos2021-05-011-24/+41
* | Remove some dead code from VeriloggenMichalis Pardalos2021-05-011-17/+0
* | Fix HTLgen using wrong register in call wait stateMichalis Pardalos2021-05-011-2/+3
* | Fix typo bug in applying externctrlMichalis Pardalos2021-05-011-2/+2
* | Print externctrl in HTL debug outputMichalis Pardalos2021-05-012-6/+31
* | Apply externctrl mapping in HTL->Verilog stageMichalis Pardalos2021-04-301-22/+147
* | Tie all modules' clock to mainMichalis Pardalos2021-04-304-16/+47
* | Fix map_externctrl double-incrementing freshregMichalis Pardalos2021-04-301-3/+2
* | Delete unused get_main_clk function from HTLgenMichalis Pardalos2021-04-301-11/+0
generated by cgit (git 2.34.1) at 2024-06-30 20:39:30 +0000