Timeline



Mar 3, 2013:

11:46 PM Changeset [2771] by sacerdot
Some speed up in Policy.ma.
9:58 PM Changeset [2770] by mckinna
WARNING: another big commit, touching many files in ASM/*.ma This …
2:59 PM Changeset [2769] by mckinna
Mistakenly commented out both as_cost_get_label (needed; OK) as well …
2:44 PM Changeset [2768] by mckinna
Nightmare: file no longer typechecks, because defn as_cost_get_labels …
2:03 PM Changeset [2767] by mckinna
WARNING: BIG commit, which pushes code_size_opt check into …
10:39 AM Changeset [2766] by mckinna
pruned redundant dependency on Clight/Cexec?.ma
12:23 AM Changeset [2765] by sacerdot
1. correctness.ma repaired 2. we used the OC_preclassified_system to …

Mar 2, 2013:

11:59 PM Changeset [2764] by sacerdot
preclassified_system for object code
11:42 AM Changeset [2763] by sacerdot
All daemons in compiler.ma closed (i.e. proof obligations added to the …
2:37 AM Changeset [2762] by sacerdot
All repaired up to compiler.ma. Note: one daemon is left for one …
1:50 AM Changeset [2761] by sacerdot
Unused (but not useless) code commented out.
1:29 AM Changeset [2760] by sacerdot
1. Many files repaired. 2. 3 new daemons: 2 in Assembly.ma, 1 in …

Mar 1, 2013:

7:56 PM Changeset [2759] by campbell
Print out costs, with choice of style. Note small anti-assertion patch …
7:55 PM Changeset [2758] by campbell
Adapt prototype's Clight printer. Doesn't use cost map yet.
7:13 PM Changeset [2757] by tranquil
many things are still broken, but there is a partial backtrack on …
1:05 PM Changeset [2756] by sacerdot
WARNING: this commit breaks things, sorry, Paolo is going to fix …
11:06 AM Changeset [2755] by tranquil
* changed primitives of abstract status (with stuf that is probably …
10:26 AM Changeset [2754] by sacerdot
1. WARNING: I commented out one of James's function used in …

Feb 28, 2013:

5:56 PM Changeset [2753] by mckinna
Further tidying up thanks to Claudio's strong_decidable intervention; …
2:36 PM Changeset [2752] by mckinna
Fixed TODO regarding length of list_instr Added ASM/CodeMemory.ma to …
2:29 PM Changeset [2751] by mckinna
Added | AssemblyTooLarge? : ErrorMessage? to complete compiler.ma
2:27 PM Changeset [2750] by mckinna
Miscellany on 216 bounds, memory, lemmas+definitions. Completes …
2:12 PM Changeset [2749] by regisgia
* Updated version of the Frama-C plugin.
2:12 PM Changeset [2748] by regisgia
* Remove the old version of the plugin.

Feb 27, 2013:

10:48 PM Changeset [2747] by sacerdot
The compiler (frontend + backend)
10:46 PM Changeset [2746] by sacerdot
1. debugging code in glue 2. updated version
10:46 PM Changeset [2745] by sacerdot
1. Complexity of policy computation lowered from O(n2) to O(n) 2. …
10:45 PM Changeset [2744] by sacerdot
Build no longer fails.
9:27 PM Changeset [2743] by sacerdot
Latest version of the compiler, extracted with the latest version of …
5:42 PM Changeset [2742] by sacerdot
Untrusted register colouring fully branched.
5:16 PM Changeset [2741] by sacerdot
File used only by untrusted code. Implemented in Matita to exploit …
4:59 PM Changeset [2740] by sacerdot
Graph colouring terminated up to Uses that will be implemented in Matita.
4:37 PM Changeset [2739] by sacerdot
The graph colouring algorithm takes in input also the function.
2:03 PM Changeset [2738] by sacerdot
Porting the graph colouring stuff from the untrusted prototype to the …

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 …
Note: See TracTimeline for information about the timeline view.