Timeline


and

Mar 10, 2013:

1:21 PM Changeset [2838] by garnier
Closing some more cases

Mar 9, 2013:

12:19 PM Changeset [2837] by tranquil
* filled in evaluation of LTL/LIN's extended instrucitons

Mar 8, 2013:

11:55 PM Changeset [2836] by sacerdot
11:54 PM Changeset [2835] by sacerdot
Included Uses.ma which is required by the untrusted code. The …
11:45 PM Changeset [2834] by sacerdot
Execution integrated in the compiler, as it was in the prototype. …
11:40 PM Changeset [2833] by sacerdot
11:40 PM Changeset [2832] by sacerdot
Added abstraction in front of cases daemon for code extraction.
11:38 PM Changeset [2831] by sacerdot
11:37 PM Changeset [2830] by sacerdot
Added abstractions in front of cases daemon for code extraction.
11:18 PM Changeset [2829] by sacerdot
Semantics files committed.
11:17 PM Changeset [2828] by sacerdot
1. New semantics.ma file that puts together all semantics. It …
9:07 PM Changeset [2827] by sacerdot
Everything extracted again.
9:07 PM Changeset [2826] by sacerdot
New error messages.
8:36 PM Changeset [2825] by garnier
Progress, Clight to Cminor
5:37 PM Changeset [2824] by tranquil
* moved sum on lists notation to extranat * used sum on lists to …
3:51 PM Changeset [2823] by tranquil
* corrected bug in ERTL semantics (both delframe and newframe did the …
12:48 PM Changeset [2822] by garnier
A consitent proof state for Clight to Cminor, with some progress (and …
11:44 AM Changeset [2821] by tranquil
* implemented preclassified system for joint (in joint/joint_fullexec.ma)
12:26 AM Changeset [2820] by sacerdot
Proof obligation closed.
12:14 AM Changeset [2819] by sacerdot
Proof obligation closed.

Mar 7, 2013:

11:43 PM Changeset [2818] by sacerdot
"Repaired", using non computational daemons.
10:31 PM Changeset [2817] by sacerdot
Repaired after Paolo's commit.
10:20 PM Changeset [2816] by sacerdot
Repaired after Paolo's commit.
9:41 PM Changeset [2815] by sacerdot
exec superseded by exec_all
9:39 PM Changeset [2814] by sacerdot
frontend superseded by execute_all
9:34 PM Changeset [2813] by sacerdot
RTLabs now printed too
9:23 PM Changeset [2812] by sacerdot
Pre-classified system for RTLabs.
9:22 PM Changeset [2811] by sacerdot
Pre-classified system for RTLabs.
6:36 PM Changeset [2810] by sacerdot
Cminor semantics exported.
6:33 PM Changeset [2809] by sacerdot
6:03 PM Changeset [2808] by tranquil
added local_stacksize to joint internal functions to accomodate for …
5:43 PM Changeset [2807] by mckinna
Yet another ErrorMessage? Removed corresponding axiom in …
2:51 PM Changeset [2806] by tranquil
new b_graph_translate obligations
2:01 PM Changeset [2805] by sacerdot
Now also prints the trace for the labelled Clight.
1:55 PM Changeset [2804] by sacerdot
New executable exec_all. It contains a function to run and print all …
1:54 PM Changeset [2803] by sacerdot
More code extracted, used to debug the compiler.
1:53 PM Changeset [2802] by sacerdot
New file Clight_classified_system with the classified system for …
1:29 PM Changeset [2801] by piccolo
Partial commit not yet finished
1:07 PM Changeset [2800] by campbell
Tidy up Measurable.ma a little, get rid of obsolete comments.
1:04 PM Changeset [2799] by tranquil
* added taaf_to_taa, conversion from trace_any_any_free to …
12:56 PM Changeset [2798] by sacerdot
New error message.
12:55 PM Changeset [2797] by sacerdot
Extracted again after James's cleanup and the implementation of the …
12:10 PM Changeset [2796] by tranquil
* added global notation for existence in Type[1] (\exists[1] x.P) * in …
9:31 AM Changeset [2795] by sacerdot
Added new function Measurable.observe_all_in_measurable to be used to …
7:47 AM Changeset [2794] by mckinna
Minor tweaks/tidying up

Mar 6, 2013:

7:23 PM Changeset [2793] by campbell
Oops, gave fields wrong order during initialisation.
4:50 PM Changeset [2792] by campbell
Make instrumented output a little easier to read.
4:50 PM Changeset [2791] by campbell
Remove dead code in driver.
3:48 PM Changeset [2790] by campbell
Some null handling in conversion from CIL.
3:48 PM Changeset [2789] by campbell
Some changes to the driver to aid debugging.
3:48 PM Changeset [2788] by campbell
Report compiler error
3:48 PM Changeset [2787] by campbell
Output stack costs in driver.
2:59 PM Changeset [2786] by piccolo
Splitted ERTLtoERTLptrOK.ma and added new file with commutation lemmas
2:58 PM Changeset [2785] by piccolo
Traces.ma repaired
2:35 PM Changeset [2784] by sacerdot
Repaired after Mauro's commit.
12:09 PM Changeset [2783] by piccolo
modified joint_closed_internal_function definition (added condition on …
3:03 AM Changeset [2782] by sacerdot
1. Paolo's bv_of_nat/nat_of_bv in BitVector? used to work with the …
3:00 AM Changeset [2781] by sacerdot
One more computational daemon closed.
2:59 AM Changeset [2780] by sacerdot
Bug fixed: in BitVector?.ma the functions bv_to_nat and nat_to_bv were …

Mar 5, 2013:

11:50 PM Changeset [2779] by sacerdot
1. bug fixed in the use of vsplit 2. major speed up (avoid detour via …
11:34 PM Changeset [2778] by sacerdot
Code to pretty-print the IntelHex? output. At the moment the glue code …
10:03 PM Changeset [2777] by sacerdot
One computational daemon closed.
9:53 PM Changeset [2776] by sacerdot
The compiler now extracts also the stack cost model.
9:52 PM Changeset [2775] by sacerdot
The compiler now computes also the stack cost model.
6:15 PM Changeset [2774] by sacerdot
1. the compiler now outputs both the stack cost model and the max …

Mar 4, 2013:

10:03 AM Changeset [2773] by sacerdot
1. everything extracted again after all bugs in Matita's extraction …
9:55 AM Changeset [2772] by sacerdot
Useless code removed.

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