aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/Asmblockgenproof1.v
Commit message (Expand)AuthorAgeFilesLines
* proof clarificationDavid Monniaux2020-03-201-3/+5
* more understandabe proofsDavid Monniaux2020-03-201-38/+38
* progress in RA invariantsDavid Monniaux2020-03-201-23/+24
* removing more coq8.10 warningsSylvain Boulmé2020-03-091-0/+2
* removing warnings on hints in coreSylvain Boulmé2020-03-071-2/+2
* Removing from Asmblockgenproof0 architecture specific definitionsCyril SIX2020-02-101-1/+1
* more proofs on notrap2David Monniaux2019-09-081-9/+53
* more proofs on notrapDavid Monniaux2019-09-081-6/+124
* moving forward on K1CDavid Monniaux2019-09-071-35/+19
* more on notrapDavid Monniaux2019-09-051-8/+26
* (#156) - Un peu de cleaning et de docCyril SIX2019-07-301-242/+4
* osel immDavid Monniaux2019-06-041-0/+48
* added immediate cmoveDavid Monniaux2019-06-041-0/+3
* shortcuts for cmoveDavid Monniaux2019-06-041-16/+36
* Osel -> assembleurDavid Monniaux2019-06-041-0/+57
* rm old select/selectl/selectf/selectfsDavid Monniaux2019-06-031-244/+0
* Asmblockgen prologue is now 1 basicblock (instead of 3)Cyril SIX2019-05-101-25/+22
* Exploiting immediate comparisonsCyril SIX2019-05-091-30/+131
* little fixDavid Monniaux2019-05-041-1/+1
* rm Ofslow (résidu du Risc-V, inutilisé et complique les preuves)David Monniaux2019-05-031-14/+14
* does not yet work, arity mismatchDavid Monniaux2019-05-011-0/+1
* it compilesDavid Monniaux2019-05-011-10/+89
* ça avanceDavid Monniaux2019-05-011-5/+78
* pass one proofDavid Monniaux2019-05-011-7/+2
* translate load.xsDavid Monniaux2019-05-011-1/+6
* indexed2XS beginDavid Monniaux2019-05-011-0/+4
* srsdDavid Monniaux2019-04-291-11/+9
* begin using shrxDavid Monniaux2019-04-291-24/+9
* Merge remote-tracking branch 'origin/mppa-work' into mppa-refactorCyril SIX2019-04-081-63/+264
|\
| * Oselectf, Oselectfs with conditionDavid Monniaux2019-04-051-17/+111
| * selectl with conditionDavid Monniaux2019-04-051-9/+56
| * Select cmpluDavid Monniaux2019-04-051-0/+18
| * select cmpuDavid Monniaux2019-04-051-3/+23
| * factor out some proofsDavid Monniaux2019-04-051-6/+3
| * some more Oselect comparisonsDavid Monniaux2019-04-041-1/+12
| * OselectDavid Monniaux2019-04-041-4/+5
| * prepare for conditions in cmoveDavid Monniaux2019-04-041-4/+4
| * ternary ops for float/doubleDavid Monniaux2019-04-031-0/+28
| * ternary ops in AES and TEADavid Monniaux2019-04-031-2/+2
| * Merge remote-tracking branch 'origin/mppa-work' into mppa-ternaryDavid Monniaux2019-04-031-74/+232
| |\
| * | selectl generationDavid Monniaux2019-03-261-3/+13
| * | selectlDavid Monniaux2019-03-251-0/+14
| * | more on cmoveDavid Monniaux2019-03-251-63/+24
* | | Merge remote-tracking branch 'origin/mppa-refactor-reviewed' into mppa-refactorCyril SIX2019-04-081-6/+6
|\ \ \
| * | | relecture sylvainSylvain Boulmé2019-04-051-6/+6
| | |/ | |/|
* / | #91 Removed completely the duplicated semantics in AsmblockCyril SIX2019-04-051-16/+13
|/ /
* | Preuve des load/store registre registre. Reste des modifs mineures dans les p...Cyril SIX2019-04-031-29/+157
* | Preuve du transl_load et transl_store registre offsetCyril SIX2019-04-031-25/+84
* | We now generate load/store with 3 registers (ld rd rs1[rs2]), proofs admittedCyril SIX2019-04-031-34/+6
* | Added definition of PLoadRRR and PStoreRRR - no Asmblockgen generation yetCyril SIX2019-04-021-13/+12
|/
generated by cgit (git 2.34.1) at 2024-07-12 04:53:29 +0000