Timeline


and

Feb 26, 2013:

7:37 PM Changeset [2737] by garnier
Commit of current proof state for Clight to Cminor translation.
6:18 PM Changeset [2736] by sacerdot
Untrusted fixpoint computation branched in.
3:35 PM Changeset [2735] by campbell
Note about loose end in FEMeasurable.
3:31 PM Changeset [2734] by mckinna
yet another puzzling automation failure, in the repaired case: "" …

Feb 25, 2013:

11:04 PM Changeset [2733] by sacerdot
All axioms in set_adt implemented by hand.
11:03 PM Changeset [2732] by sacerdot
Unused code removed.
10:17 PM Changeset [2731] by sacerdot
Minimal set of axioms implemented to make the driver run.
9:54 PM Changeset [2730] by sacerdot
Exported again.
9:51 PM Changeset [2729] by sacerdot
More errors recognized
9:42 PM Changeset [2728] by sacerdot
listb.ma => listb_extra.ma for extraction
6:43 PM Changeset [2727] by campbell
Remove a couple of redundant hypotheses.
12:11 PM Changeset [2726] by campbell
Show max stack preserved in FEMeasurable.
11:45 AM Changeset [2725] by campbell
Add observables to FEMeasurable proof; fix silly typo.

Feb 24, 2013:

8:39 PM Changeset [2724] by campbell
Add RTLabs cost labelling checks to compiler.ma.

Feb 23, 2013:

5:05 PM Changeset [2723] by campbell
Library name typo fixed.
5:05 PM Changeset [2722] by campbell
It's easier to keep the real function identifier in front-end …
5:05 PM Changeset [2721] by campbell
Give the real error in the driver.
12:03 PM Changeset [2720] by tranquil
implemented back end ops that were still axioms
1:29 AM Changeset [2719] by sacerdot
More values manually abstracted to functions to avoid failwiths at …
1:19 AM Changeset [2718] by sacerdot
set_empty turned from a value to a function because it is not …
1:16 AM Changeset [2717] by sacerdot
Extracted code for the whole compiler. The space cost model is not …
1:03 AM Changeset [2716] by sacerdot
utilities/deqsets.ma => utilities/deqsets_extra.ma for extraction

Feb 22, 2013:

11:41 PM Changeset [2715] by sacerdot
Policy.ma repaired
11:20 PM Changeset [2714] by sacerdot
PolicyStep?.ma repaired
10:39 PM Changeset [2713] by sacerdot
PolicyFront?.ma repaired
8:04 PM Changeset [2712] by tranquil
changed some fields of joint_internal_function's invariant fixed linearise
7:23 PM Changeset [2711] by sacerdot
7:20 PM Changeset [2710] by sacerdot
ASMCosts.ma repaired
7:17 PM Changeset [2709] by sacerdot
LINToAsm repaired
7:11 PM Changeset [2708] by tranquil
fixed linearise and LINToASM LINToASM has now correct transformation …
6:45 PM Changeset [2707] by sacerdot
Assembly repaired.
6:23 PM Changeset [2706] by mckinna
repaired contentious broken automation at end of subgoal 9 of case (* …
5:56 PM Changeset [2705] by sacerdot
More progress in ASM towards implementing the new pseudoinstructions.
3:53 PM Changeset [2704] by tranquil
moved JMP from instructions to preinstructions, and added MovSuccessor?
3:31 PM Changeset [2703] by mckinna
now includes defn of costlabel_map
3:27 PM Changeset [2702] by sacerdot
1. proof closed in ASM/UtilBranch 2. more passes integrated in the …
2:30 PM Changeset [2701] by sacerdot
Automation failure fixed by replacing with hand made proof.
2:12 PM Changeset [2700] by sacerdot
1. exponential function dropped in favour of standard library 2. …
2:11 PM Changeset [2699] by mckinna
simplified dependencies somewhat
1:11 PM Changeset [2698] by mckinna
simplified dependencies
12:13 PM Changeset [2697] by sacerdot
Compiler fixed to include the ERTLptrToLTL pass.
12:12 PM Changeset [2696] by sacerdot
I can't get this right... :-(
12:06 PM Changeset [2695] by sacerdot
Renamed again.
11:53 AM Changeset [2694] by tranquil
completed ERTLptrToLTL
11:39 AM Changeset [2693] by sacerdot
1. Stuff moved to correct places. 2. ERTLptr pass added
11:27 AM Changeset [2692] by garnier
Add some more constraints in clight_cminor_data.
11:10 AM Changeset [2691] by sacerdot
ERTLtoERTLptr* moved to the proper place

Feb 21, 2013:

7:24 PM Changeset [2690] by campbell
Most of the measurable subtrace preservation proof done.
7:23 PM Changeset [2689] by tranquil
* fixed passes up to linearisation
6:03 PM Changeset [2688] by tranquil
* in Arithmeticcs.ma: commented include that breaks script in latest …
4:20 PM Changeset [2687] by tranquil
* polished some interfaces
3:34 PM Changeset [2686] by mckinna
two minor modifications to assist disambiguation of "lookup" file …
11:38 AM Changeset [2685] by campbell
Progress on measurable trace preservation: prefix preserves observable …
10:32 AM Changeset [2684] by sacerdot

Feb 20, 2013:

6:41 PM Changeset [2683] by tranquil
proof of properties of b_graph_program_transform (with an open axiom)

Feb 19, 2013:

7:24 PM Changeset [2682] by campbell
Don't apply inv in after_n_steps to last state.
6:48 PM Changeset [2681] by tranquil
* improvements to the graph translation function * fixed passes up to LTL
4:36 PM Changeset [2680] by mckinna
proofs which previously succeeded fail, thanks to fold on positive_map …
3:15 PM Changeset [2679] by mckinna
Further tweak to Brian's changes: no normalization reqd at all!
12:23 PM Changeset [2678] by campbell
Switch to single source step simulations for front-end measurable …
12:23 PM Changeset [2677] by campbell
Retain the pointer for the function called in front-end call states so …
12:23 PM Changeset [2676] by campbell
Less aggressive normalisation in ASMCosts to prevent memory blowup.

Feb 18, 2013:

6:26 PM Changeset [2675] by tranquil
* a generic graph program transformation
5:48 PM Changeset [2674] by tranquil
* another change in block definition * RTLabs -> RTL and ERTL -> …
1:18 PM Changeset [2673] by tranquil
corrected some compilation errors (that might depend on some matita update)

Feb 16, 2013:

6:49 PM Changeset [2672] by sacerdot
One less axiom on bitvectors.
5:12 PM Changeset [2671] by sacerdot
simplification

Feb 15, 2013:

11:27 AM Changeset [2670] by campbell
Clean up from recent commits.
11:27 AM Changeset [2669] by campbell
Tweak exec_steps output; show that simulations extend to measurable …
11:27 AM Changeset [2668] by campbell
Intermediate measurable proof check-in before I change its traces again.

Feb 14, 2013:

7:10 PM Changeset [2667] by garnier
Clight to Cminor, statements: some cases down. Subset of the …
11:49 AM Changeset [2666] by piccolo
bug fixed in blocks.ma
10:01 AM Changeset [2665] by sacerdot
12:01 AM Changeset [2664] by sacerdot
Tailcall case implemented (it does not happen ATM).

Feb 12, 2013:

7:40 PM Changeset [2663] by piccolo
some minor modifications to ERTLtoERTLptr
6:56 PM Changeset [2662] by piccolo
Towards a very generalized lemma that summarizes all of Paolo's results.
3:26 AM Changeset [2661] by sacerdot
stacksize "repaired" by "considering" tailcalls Some daemons added …
3:06 AM Changeset [2660] by sacerdot
2:47 AM Changeset [2659] by sacerdot
Tailcall elimination no longer necessary: 1. the back-end is almost …
2:43 AM Changeset [2658] by sacerdot
2:41 AM Changeset [2657] by sacerdot
Cost proof fully repaired. It was broken by the definitions used in …

Feb 11, 2013:

6:58 PM Changeset [2656] by sacerdot
Ported to tailcalls (currently nothing is classified as a tailcall).
4:52 PM Changeset [2655] by tranquil
new step in code semantic lemma

Feb 8, 2013:

8:54 PM Changeset [2654] by garnier
Memory injections in a coherent state.
1:45 PM Changeset [2653] by sacerdot
11:49 AM Changeset [2652] by sacerdot
String type changed definition.
11:13 AM Changeset [2651] by sacerdot
Type String changed.
8:46 AM Changeset [2650] by regisgia
* Final version of the untrusted software.

Feb 7, 2013:

10:43 PM Changeset [2649] by sacerdot
10:43 PM Changeset [2648] by sacerdot
Back in sync with the extracted code.
10:10 PM Changeset [2647] by sacerdot
Stupid typo fixed.
9:44 PM Changeset [2646] by sacerdot
A tag was classified as an error message. Fixed.
9:22 PM Changeset [2645] by sacerdot
1. some broken back-end files repaires, several still to go 2. the …
4:42 PM Changeset [2644] by campbell
Commit some work on FEMeasurable before trying to do something nicer …
4:03 PM Changeset [2643] by sacerdot
We are not proving erasure, so this is dead code.
3:24 PM Changeset [2642] by piccolo
fixed joint/Traces after having posed block 0 to be Code
3:15 PM Changeset [2641] by piccolo
defined dummy block code equals to 0
3:13 PM Changeset [2640] by tranquil
updated RTL and RTLabs to RTL translation
3:07 PM Changeset [2639] by sacerdot
We are not going to prove erasure. Thus this becomes dead code.
2:15 PM Changeset [2638] by piccolo
Back-end fixes for last Garnier's commit that removes the regions from …

Feb 6, 2013:

11:51 PM Changeset [2637] by sacerdot
11:43 PM Changeset [2636] by campbell
Extracted front-end.
11:28 PM Changeset [2635] by sacerdot
11:23 PM Changeset [2634] by sacerdot
11:16 PM Changeset [2633] by sacerdot
11:11 PM Changeset [2632] by sacerdot
10:28 PM Changeset [2631] by sacerdot
10:19 PM Changeset [2630] by sacerdot
10:19 PM Changeset [2629] by sacerdot
10:18 PM Changeset [2628] by sacerdot
10:06 PM Changeset [2627] by sacerdot
9:32 PM Changeset [2626] by sacerdot
8:14 PM Changeset [2625] by sacerdot
6:39 PM Changeset [2624] by campbell
Properly evict unused and axiomatised Floats.
6:39 PM Changeset [2623] by campbell
Name change update.
6:11 PM Changeset [2622] by sacerdot
5:53 PM Changeset [2621] by sacerdot
5:03 PM Changeset [2620] by campbell
Sufficient hacking to run the extracted Clight semantics.
5:03 PM Changeset [2619] by campbell
Update some test cases.
5:03 PM Changeset [2618] by campbell
Tidy up measurable a little.
5:03 PM Changeset [2617] by campbell
Trivial simplification on split_trace.
4:07 PM Changeset [2616] by sacerdot
3:51 PM Changeset [2615] by sacerdot
3:39 PM Changeset [2614] by sacerdot
3:30 PM Changeset [2613] by sacerdot
3:15 PM Changeset [2612] by sacerdot
2:21 PM Changeset [2611] by sacerdot
2:00 PM Changeset [2610] by sacerdot
1:56 PM Changeset [2609] by sacerdot
Bibliography in place.
1:01 PM Changeset [2608] by garnier
Regions are no more stored in blocks. block_region now tests the id, …
12:15 PM Changeset [2607] by sacerdot
authors fixed
12:13 PM Changeset [2606] by sacerdot
conclusions
10:30 AM Changeset [2605] by sacerdot
A tentative submission to itp-2013. We will probably not submit the …

Feb 5, 2013:

10:49 PM Changeset [2604] by piccolo
ERTLtoERTLptr in place.
1:54 PM Changeset [2603] by piccolo
Dead code commented out.
1:54 PM Changeset [2602] by piccolo
Dead code commented out.
1:36 PM Changeset [2601] by sacerdot
Extraction to ocaml is now working, with a couple of bugs left. One …

Feb 1, 2013:

12:13 PM Changeset [2600] by garnier
Memory injections are now only defined relatively to block ids, not …

Jan 31, 2013:

5:15 PM Changeset [2599] by tranquil
* map_opt and map on positive maps are now clean (erase empty …
12:56 PM Changeset [2598] by garnier
Tentative, partial draft for the definition of Clight-Cminor …
12:07 PM Changeset [2597] by campbell
Some work in progress on measurable subtrace preservation.
12:06 PM Changeset [2596] by campbell
Use a simpler stack cost map, and then specialise to each semantics.

Jan 30, 2013:

7:25 PM Changeset [2595] by tranquil
* dropped locals and exit from definition of joint_if_function * new …

Jan 29, 2013:

8:28 PM Changeset [2594] by garnier
Some fixes in memory injections, and some holes filled.
12:13 PM Changeset [2593] by mckinna
Finally chased down wicked failure to close case 1.1: of …
11:20 AM Changeset [2592] by piccolo
main lemma of ERTLptr in place

Jan 28, 2013:

11:43 AM Changeset [2591] by garnier
Moved simulation proof for expressions in toCminorCorrectnessExpr.ma, …
Note: See TracTimeline for information about the timeline view.