aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/HTLgenproof.v
Commit message (Expand)AuthorAgeFilesLines
* Merge branch 'master' into dev/michalisdev/michalisYann Herklotz2021-10-181-22/+21
|\
| * Remove warnings of attributesYann Herklotz2021-10-081-23/+23
* | Check that only main has a stacksizeMichalis Pardalos2021-10-111-11/+22
* | Get all call and return proofs passing againMichalis Pardalos2021-10-081-4/+25
* | Maintain that initial call does not have argumentsMichalis Pardalos2021-10-071-0/+1
* | [WIP] Handle empty stack case for empty stack caseMichalis Pardalos2021-10-071-39/+65
* | Clarify ireturn proofMichalis Pardalos2021-09-301-5/+5
* | Prove match_arrs_emptyMichalis Pardalos2021-09-301-1/+19
* | Complete alloc/free zero proofsMichalis Pardalos2021-09-301-8/+15
* | Complete call/return proofsMichalis Pardalos2021-09-301-68/+122
* | [WIP] Updating proof for new state matchingMichalis Pardalos2021-09-291-39/+69
* | Update match_states. Pointers based on main's spMichalis Pardalos2021-09-291-21/+27
* | Add assumptions about externctrl finish registersMichalis Pardalos2021-09-211-21/+131
* | [WIP] Reset finish register after returningMichalis Pardalos2021-09-201-8/+56
* | Merge remote-tracking branch 'upstream/dev-michalis' into dev-michalisMichalis Pardalos2021-09-191-3/+3
|\ \
| * | Fix infinite loop in proofdev-michalisYann Herklotz2021-09-191-3/+3
* | | [WIP] Fix usage of externctrl property in proofMichalis Pardalos2021-09-191-6/+6
* | | Address admits relating to externctrl paramsMichalis Pardalos2021-09-161-8/+35
|/ /
* | Complete callstate proofMichalis Pardalos2021-09-161-6/+43
* | Progress with callstate proofMichalis Pardalos2021-09-151-8/+11
* | Progress with icall proofMichalis Pardalos2021-09-151-16/+106
* | Progress with mem_alloc_zeroMichalis Pardalos2021-09-151-3/+85
* | Prove mem_free_stack_matchMichalis Pardalos2021-09-141-6/+86
* | Add hammer tacticsMichalis Pardalos2021-09-131-0/+3
* | Icall proof progressMichalis Pardalos2021-09-131-35/+85
* | Guard join state with called module finishMichalis Pardalos2021-09-111-2/+8
* | Progress with stackframe matching for IcallMichalis Pardalos2021-09-101-1/+8
* | Prove that called module exists for IcallMichalis Pardalos2021-09-101-2/+26
* | Get HTLgenproof to compile with RAM inferenceMichalis Pardalos2021-08-311-2/+9
* | Merge branch 'oopsla21' into sharing-mergeMichalis Pardalos2021-08-261-18/+82
|\|
| * Basically done with proofYann Herklotz2021-04-071-2/+2
| * Add negative edge reasoning to HTLgenproofYann Herklotz2021-03-091-12/+76
| * Add RAM semantics to HTL and fix proofYann Herklotz2021-03-031-6/+8
| * Add implementationYann Herklotz2021-03-021-1/+1
* | Use new HTLgenspec in proofMichalis Pardalos2021-08-221-3/+27
* | More progress in Icall proofMichalis Pardalos2021-08-191-14/+16
* | Find called module in Icall proofMichalis Pardalos2021-08-191-13/+33
* | Get HTLgenproof passing with updated specMichalis Pardalos2021-08-061-3/+3
* | Correct lookup for called funcs, simplify tr_moduleMichalis Pardalos2021-08-041-9/+8
* | Remove all Admitted from top-level Compiler.vMichalis Pardalos2021-06-101-23/+199
* | 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-181-50/+64
* | 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-171-78/+165
generated by cgit (git 2.34.1) at 2024-06-08 21:06:21 +0000