|
|
|
@2680
|
8 years |
mckinna |
proofs which previously succeeded fail, thanks to fold on positive_map …
|
|
|
|
@2679
|
8 years |
mckinna |
Further tweak to Brian's changes: no normalization reqd at all!
|
|
|
|
@2678
|
8 years |
campbell |
Switch to single source step simulations for front-end measurable …
|
|
|
|
@2677
|
8 years |
campbell |
Retain the pointer for the function called in front-end call states
so …
|
|
|
|
@2676
|
8 years |
campbell |
Less aggressive normalisation in ASMCosts to prevent memory blowup.
|
|
|
|
@2675
|
8 years |
tranquil |
* a generic graph program transformation
|
|
|
|
@2674
|
8 years |
tranquil |
* another change in block definition
* RTLabs -> RTL and ERTL -> …
|
|
|
|
@2673
|
8 years |
tranquil |
corrected some compilation errors (that might depend on some matita update)
|
|
|
|
@2672
|
8 years |
sacerdot |
One less axiom on bitvectors.
|
|
|
|
@2671
|
8 years |
sacerdot |
simplification
|
|
|
|
@2670
|
8 years |
campbell |
Clean up from recent commits.
|
|
|
|
@2669
|
8 years |
campbell |
Tweak exec_steps output; show that simulations extend to measurable …
|
|
|
|
@2668
|
8 years |
campbell |
Intermediate measurable proof check-in before I change its traces again.
|
|
|
|
@2667
|
8 years |
garnier |
Clight to Cminor, statements: some cases down. Subset of the …
|
|
|
|
@2666
|
8 years |
piccolo |
bug fixed in blocks.ma
|
|
|
|
@2665
|
8 years |
sacerdot |
…
|
|
|
|
@2664
|
8 years |
sacerdot |
Tailcall case implemented (it does not happen ATM).
|
|
|
|
@2663
|
8 years |
piccolo |
some minor modifications to ERTLtoERTLptr
|
|
|
|
@2662
|
8 years |
piccolo |
Towards a very generalized lemma that summarizes all of Paolo's results.
|
|
|
|
@2661
|
8 years |
sacerdot |
stacksize "repaired" by "considering" tailcalls
Some daemons added …
|
|
|
|
@2660
|
8 years |
sacerdot |
…
|
|
|
|
@2659
|
8 years |
sacerdot |
Tailcall elimination no longer necessary:
1. the back-end is almost …
|
|
|
|
@2658
|
8 years |
sacerdot |
…
|
|
|
|
@2657
|
8 years |
sacerdot |
Cost proof fully repaired. It was broken by the definitions used in …
|
|
|
|
@2656
|
8 years |
sacerdot |
Ported to tailcalls (currently nothing is classified as a tailcall).
|
|
|
|
@2655
|
8 years |
tranquil |
new step in code semantic lemma
|
|
|
|
@2654
|
8 years |
garnier |
Memory injections in a coherent state.
|
|
|
|
@2653
|
8 years |
sacerdot |
…
|
|
|
|
@2652
|
8 years |
sacerdot |
String type changed definition.
|
|
|
|
@2651
|
8 years |
sacerdot |
Type String changed.
|
|
|
|
@2650
|
8 years |
regisgia |
* Final version of the untrusted software.
|
|
|
|
@2649
|
8 years |
sacerdot |
…
|
|
|
|
@2648
|
8 years |
sacerdot |
Back in sync with the extracted code.
|
|
|
|
@2647
|
8 years |
sacerdot |
Stupid typo fixed.
|
|
|
|
@2646
|
8 years |
sacerdot |
A tag was classified as an error message. Fixed.
|
|
|
|
@2645
|
8 years |
sacerdot |
1. some broken back-end files repaires, several still to go
2. the …
|
|
|
|
@2644
|
8 years |
campbell |
Commit some work on FEMeasurable before trying to do something nicer …
|
|
|
|
@2643
|
8 years |
sacerdot |
We are not proving erasure, so this is dead code.
|
|
|
|
@2642
|
8 years |
piccolo |
fixed joint/Traces after having posed block 0 to be Code
|
|
|
|
@2641
|
8 years |
piccolo |
defined dummy block code equals to 0
|
|
|
|
@2640
|
8 years |
tranquil |
updated RTL and RTLabs to RTL translation
|
|
|
|
@2639
|
8 years |
sacerdot |
We are not going to prove erasure. Thus this becomes dead code.
|
|
|
|
@2638
|
8 years |
piccolo |
Back-end fixes for last Garnier's commit that removes the regions from …
|
|
|
|
@2637
|
8 years |
sacerdot |
…
|
|
|
|
@2636
|
8 years |
campbell |
Extracted front-end.
|
|
|
|
@2635
|
8 years |
sacerdot |
…
|
|
|
|
@2634
|
8 years |
sacerdot |
…
|
|
|
|
@2633
|
8 years |
sacerdot |
…
|
|
|
|
@2632
|
8 years |
sacerdot |
…
|
|
|
|
@2631
|
8 years |
sacerdot |
…
|
|
|
|
@2630
|
8 years |
sacerdot |
…
|
|
|
|
@2629
|
8 years |
sacerdot |
…
|
|
|
|
@2628
|
8 years |
sacerdot |
…
|
|
|
|
@2627
|
8 years |
sacerdot |
…
|
|
|
|
@2626
|
8 years |
sacerdot |
…
|
|
|
|
@2625
|
8 years |
sacerdot |
…
|
|
|
|
@2624
|
8 years |
campbell |
Properly evict unused and axiomatised Floats.
|
|
|
|
@2623
|
8 years |
campbell |
Name change update.
|
|
|
|
@2622
|
8 years |
sacerdot |
…
|
|
|
|
@2621
|
8 years |
sacerdot |
…
|
|
|
|
@2620
|
8 years |
campbell |
Sufficient hacking to run the extracted Clight semantics.
|
|
|
|
@2619
|
8 years |
campbell |
Update some test cases.
|
|
|
|
@2618
|
8 years |
campbell |
Tidy up measurable a little.
|
|
|
|
@2617
|
8 years |
campbell |
Trivial simplification on split_trace.
|
|
|
|
@2616
|
8 years |
sacerdot |
…
|
|
|
|
@2615
|
8 years |
sacerdot |
…
|
|
|
|
@2614
|
8 years |
sacerdot |
…
|
|
|
|
@2613
|
8 years |
sacerdot |
…
|
|
|
|
@2612
|
8 years |
sacerdot |
…
|
|
|
|
@2611
|
8 years |
sacerdot |
…
|
|
|
|
@2610
|
8 years |
sacerdot |
…
|
|
|
|
@2609
|
8 years |
sacerdot |
Bibliography in place.
|
|
|
|
@2608
|
8 years |
garnier |
Regions are no more stored in blocks. block_region now tests the id, …
|
|
|
|
@2607
|
8 years |
sacerdot |
authors fixed
|
|
|
|
@2606
|
8 years |
sacerdot |
conclusions
|
|
|
|
@2605
|
8 years |
sacerdot |
A tentative submission to itp-2013.
We will probably not submit the …
|
|
|
|
@2604
|
8 years |
piccolo |
ERTLtoERTLptr in place.
|
|
|
|
@2603
|
8 years |
piccolo |
Dead code commented out.
|
|
|
|
@2602
|
8 years |
piccolo |
Dead code commented out.
|
|
|
|
@2601
|
8 years |
sacerdot |
Extraction to ocaml is now working, with a couple of bugs left.
One …
|
|
|
|
@2600
|
8 years |
garnier |
Memory injections are now only defined relatively to block ids, not …
|
|
|
|
@2599
|
8 years |
tranquil |
* map_opt and map on positive maps are now clean (erase empty …
|
|
|
|
@2598
|
8 years |
garnier |
Tentative, partial draft for the definition of Clight-Cminor …
|
|
|
|
@2597
|
8 years |
campbell |
Some work in progress on measurable subtrace preservation.
|
|
|
|
@2596
|
8 years |
campbell |
Use a simpler stack cost map, and then specialise to each semantics.
|
|
|
|
@2595
|
8 years |
tranquil |
* dropped locals and exit from definition of joint_if_function
* new …
|
|
|
|
@2594
|
8 years |
garnier |
Some fixes in memory injections, and some holes filled.
|
|
|
|
@2593
|
8 years |
mckinna |
Finally chased down wicked failure to close case 1.1: of …
|
|
|
|
@2592
|
8 years |
piccolo |
main lemma of ERTLptr in place
|
|
|
|
@2591
|
8 years |
garnier |
Moved simulation proof for expressions in toCminorCorrectnessExpr.ma, …
|
|
|
|
@2590
|
8 years |
piccolo |
added monad machineary for ERTL to ERTLptr translation
eval_seq_no_pc …
|
|
|
|
@2589
|
8 years |
campbell |
Add one of the simulation diagrams
|
|
|
|
@2588
|
8 years |
garnier |
modified Cexec/Csem? semantics:
. force andbool and orbool types to be …
|
|
|
|
@2587
|
8 years |
campbell |
Tweak talk a little.
|
|
|
|
@2586
|
8 years |
amadio |
r
|
|
|
|
@2585
|
8 years |
campbell |
Many improvements to proof/structured traces talk.
|
|
|
|
@2584
|
8 years |
regisgia |
* Update slides.
|
|
|
|
@2583
|
8 years |
campbell |
Structured traces talk with most of the content; not quite final.
|
|
|
|
@2582
|
8 years |
garnier |
Some progress on CL to CM.
|
|
|
|
@2581
|
8 years |
mckinna |
commented out back end entirely until knock-on effects of changes to …
|
|
|
|
