aboutsummaryrefslogtreecommitdiffstats
path: root/src
Commit message (Expand)AuthorAgeFilesLines
...
| * Add Verilog generation for ramsYann Herklotz2021-03-021-18/+47
| * Admit VeriloggenproofYann Herklotz2021-03-021-2/+3
| * Finish initial implementation of memory genYann Herklotz2021-03-012-2/+89
| * Change lists in case statements to stmnt_listYann Herklotz2021-03-016-12/+30
| * Add initial memory generationYann Herklotz2021-03-011-0/+17
* | Use new HTLgenspec in proofMichalis Pardalos2021-08-221-3/+27
* | Move list lemmas to own fileMichalis Pardalos2021-08-222-21/+28
* | Add length args = length params to Icall specMichalis Pardalos2021-08-211-44/+80
* | Strengthen HTLgenspecMichalis Pardalos2021-08-201-9/+14
* | More progress in Icall proofMichalis Pardalos2021-08-191-14/+16
* | Find called module in Icall proofMichalis Pardalos2021-08-194-29/+39
* | Complete HTLspec (mostly)Michalis Pardalos2021-08-123-52/+133
* | Tie clocks in the ApplyExternctrl passMichalis Pardalos2021-08-122-2/+7
* | Get HTLgenproof passing with updated specMichalis Pardalos2021-08-061-3/+3
* | Correct lookup for called funcs, simplify tr_moduleMichalis Pardalos2021-08-043-32/+61
* | Check whether callee is internal for IcallMichalis Pardalos2021-08-022-25/+24
* | Add "join state is <=Int.max_unsigned" to HTLgenspecMichalis Pardalos2021-06-102-10/+13
* | Remove all Admitted from top-level Compiler.vMichalis Pardalos2021-06-107-425/+618
* | Get top-level (Compiler) proof closer to QedMichalis Pardalos2021-06-081-3/+27
* | Make externctrl application its own HTL passMichalis Pardalos2021-06-064-185/+229
* | Move HTL renaming pass to own fileMichalis Pardalos2021-06-065-242/+249
* | 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-102-14/+36
* | Progress on tr_module proofMichalis Pardalos2021-05-082-52/+82
* | Fully clean up the iter_expand_instr_spec proofMichalis Pardalos2021-05-072-146/+80
* | Complete iter_expand_instr_spec proofMichalis Pardalos2021-05-071-14/+23
* | Prove a spec for the mapping of function paramsMichalis Pardalos2021-05-063-49/+128
* | Solve easier branches of the transf_instr proofMichalis Pardalos2021-05-061-29/+64
generated by cgit (git 2.34.1) at 2024-06-30 20:48:20 +0000