aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls
Commit message (Collapse)AuthorAgeFilesLines
...
* | 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-122-51/+130
| |
* | 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-105-383/+588
| |
* | Make externctrl application its own HTL passMichalis Pardalos2021-06-063-184/+225
| |
* | 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
| | | | | | | | | | This is true due to the inlining pass. It should be checked in the translation and be added in the translation spec.
* | Qed on top-level correctness lemmaMichalis Pardalos2021-05-181-2/+2
| |
* | Update lemmata broken by changes to semanticsMichalis Pardalos2021-05-181-42/+35
| | | | | | | | | | | | * Removed calls to match_externctrl_tac. Carried forward without need for the tactic * Admitted match_frames goals. They should be easy enough to fix
* | Get Icall translation lemma *statement* passingMichalis Pardalos2021-05-181-15/+17
| |
* | Add "internal calls only" into translation specMichalis Pardalos2021-05-182-70/+94
| | | | | | | | | | | | | | 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.
* | 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
| | | | | | | | Necessary because they are used as pointers in externctrl
* | 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
| | | | | | | | There is still some questions about the use of module identifiers in the semantics.
* | Get HTLgenproof passing again (with admits)Michalis Pardalos2021-05-131-230/+172
| |
* | Remove "active_call" from HTL semanticsMichalis Pardalos2021-05-132-28/+24
| | | | | | | | | | added previously to support the fork/wait/join HTL instructions which have since been removed
* | 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-062-43/+123
| | | | | | | | | | 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.
* | 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
| | | | | | | | | | Mapping the externctrl for the parameters requires a traversal on a list. Moved it up to the top of the branch to make it stand out in the proof.
* | 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
| | | | | | | | Program rewrites match statements, making proofs much harder.
* | Use Defined for obligations in Program DefinitionsMichalis Pardalos2021-05-021-12/+12
| | | | | | | | The created terms might need to be inspected.
generated by cgit (git 2.34.1) at 2024-07-02 19:32:12 +0000