source: src

Revision Log Mode:


Legend:

Added
Modified
Copied or renamed
Diff Rev Age Author Log Message
(edit) @2830   8 years sacerdot Added abstractions in front of cases daemon for code extraction.
(edit) @2828   8 years sacerdot 1. New semantics.ma file that puts together all semantics. It …
(edit) @2825   8 years garnier Progress, Clight to Cminor
(edit) @2824   8 years tranquil * moved sum on lists notation to extranat * used sum on lists to …
(edit) @2823   8 years tranquil * corrected bug in ERTL semantics (both delframe and newframe did the …
(edit) @2822   8 years garnier A consitent proof state for Clight to Cminor, with some progress (and …
(edit) @2821   8 years tranquil * implemented preclassified system for joint (in joint/joint_fullexec.ma)
(edit) @2820   8 years sacerdot Proof obligation closed.
(edit) @2819   8 years sacerdot Proof obligation closed.
(edit) @2818   8 years sacerdot "Repaired", using non computational daemons.
(edit) @2817   8 years sacerdot Repaired after Paolo's commit.
(edit) @2816   8 years sacerdot Repaired after Paolo's commit.
(edit) @2811   8 years sacerdot Pre-classified system for RTLabs.
(edit) @2809   8 years sacerdot …
(edit) @2808   8 years tranquil added local_stacksize to joint internal functions to accomodate for …
(edit) @2807   8 years mckinna Yet another ErrorMessage? Removed corresponding axiom in …
(edit) @2806   8 years tranquil new b_graph_translate obligations
(edit) @2802   8 years sacerdot New file Clight_classified_system with the classified system for …
(edit) @2801   8 years piccolo Partial commit not yet finished
(edit) @2800   8 years campbell Tidy up Measurable.ma a little, get rid of obsolete comments.
(edit) @2799   8 years tranquil * added taaf_to_taa, conversion from trace_any_any_free to …
(edit) @2796   8 years tranquil * added global notation for existence in Type[1] (\exists[1] x.P) * in …
(edit) @2795   8 years sacerdot Added new function Measurable.observe_all_in_measurable to be used to …
(edit) @2794   8 years mckinna Minor tweaks/tidying up
(edit) @2793   8 years campbell Oops, gave fields wrong order during initialisation.
(edit) @2786   8 years piccolo Splitted ERTLtoERTLptrOK.ma and added new file with commutation lemmas
(edit) @2785   8 years piccolo Traces.ma repaired
(edit) @2784   8 years sacerdot Repaired after Mauro's commit.
(edit) @2783   8 years piccolo modified joint_closed_internal_function definition (added condition on …
(edit) @2782   8 years sacerdot 1. Paolo's bv_of_nat/nat_of_bv in BitVector? used to work with the …
(edit) @2781   8 years sacerdot One more computational daemon closed.
(edit) @2774   8 years sacerdot 1. the compiler now outputs both the stack cost model and the max …
(edit) @2772   8 years sacerdot Useless code removed.
(edit) @2771   8 years sacerdot Some speed up in Policy.ma.
(edit) @2770   8 years mckinna WARNING: another big commit, touching many files in ASM/*.ma This …
(edit) @2769   8 years mckinna Mistakenly commented out both as_cost_get_label (needed; OK) as well …
(edit) @2768   8 years mckinna Nightmare: file no longer typechecks, because defn as_cost_get_labels …
(edit) @2767   8 years mckinna WARNING: BIG commit, which pushes code_size_opt check into …
(edit) @2766   8 years mckinna pruned redundant dependency on Clight/Cexec?.ma
(edit) @2765   8 years sacerdot 1. correctness.ma repaired 2. we used the OC_preclassified_system to …
(edit) @2764   8 years sacerdot preclassified_system for object code
(edit) @2763   8 years sacerdot All daemons in compiler.ma closed (i.e. proof obligations added to the …
(edit) @2762   8 years sacerdot All repaired up to compiler.ma. Note: one daemon is left for one …
(edit) @2761   8 years sacerdot Unused (but not useless) code commented out.
(edit) @2760   8 years sacerdot 1. Many files repaired. 2. 3 new daemons: 2 in Assembly.ma, 1 in …
(edit) @2757   8 years tranquil many things are still broken, but there is a partial backtrack on …
(edit) @2756   8 years sacerdot WARNING: this commit breaks things, sorry, Paolo is going to fix …
(edit) @2755   8 years tranquil * changed primitives of abstract status (with stuf that is probably …
(edit) @2754   8 years sacerdot 1. WARNING: I commented out one of James's function used in …
(edit) @2753   8 years mckinna Further tidying up thanks to Claudio's strong_decidable intervention; …
(edit) @2752   8 years mckinna Fixed TODO regarding length of list_instr Added ASM/CodeMemory.ma to …
(edit) @2751   8 years mckinna Added | AssemblyTooLarge? : ErrorMessage? to complete compiler.ma
(edit) @2750   8 years mckinna Miscellany on 216 bounds, memory, lemmas+definitions. Completes …
(edit) @2745   8 years sacerdot 1. Complexity of policy computation lowered from O(n2) to O(n) 2. …
(edit) @2741   8 years sacerdot File used only by untrusted code. Implemented in Matita to exploit …
(edit) @2739   8 years sacerdot The graph colouring algorithm takes in input also the function.
(edit) @2737   8 years garnier Commit of current proof state for Clight to Cminor translation.
(edit) @2734   8 years mckinna yet another puzzling automation failure, in the repaired case: "" …
(edit) @2732   8 years sacerdot Unused code removed.
(edit) @2728   8 years sacerdot listb.ma => listb_extra.ma for extraction
(edit) @2727   8 years campbell Remove a couple of redundant hypotheses.
(edit) @2726   8 years campbell Show max stack preserved in FEMeasurable.
(edit) @2725   8 years campbell Add observables to FEMeasurable proof; fix silly typo.
(edit) @2724   8 years campbell Add RTLabs cost labelling checks to compiler.ma.
(edit) @2723   8 years campbell Library name typo fixed.
(edit) @2722   8 years campbell It's easier to keep the real function identifier in front-end …
(edit) @2720   8 years tranquil implemented back end ops that were still axioms
(edit) @2716   8 years sacerdot utilities/deqsets.ma => utilities/deqsets_extra.ma for extraction
(edit) @2715   8 years sacerdot Policy.ma repaired
(edit) @2714   8 years sacerdot PolicyStep?.ma repaired
(edit) @2713   8 years sacerdot PolicyFront?.ma repaired
(edit) @2712   8 years tranquil changed some fields of joint_internal_function's invariant fixed linearise
(edit) @2711   8 years sacerdot …
(edit) @2710   8 years sacerdot ASMCosts.ma repaired
(edit) @2709   8 years sacerdot LINToAsm repaired
(edit) @2708   8 years tranquil fixed linearise and LINToASM LINToASM has now correct transformation …
(edit) @2707   8 years sacerdot Assembly repaired.
(edit) @2706   8 years mckinna repaired contentious broken automation at end of subgoal 9 of case (* …
(edit) @2705   8 years sacerdot More progress in ASM towards implementing the new pseudoinstructions.
(edit) @2704   8 years tranquil moved JMP from instructions to preinstructions, and added MovSuccessor? …
(edit) @2703   8 years mckinna now includes defn of costlabel_map
(edit) @2702   8 years sacerdot 1. proof closed in ASM/UtilBranch 2. more passes integrated in the …
(edit) @2701   8 years sacerdot Automation failure fixed by replacing with hand made proof.
(edit) @2700   8 years sacerdot 1. exponential function dropped in favour of standard library 2. …
(edit) @2699   8 years mckinna simplified dependencies somewhat
(edit) @2698   8 years mckinna simplified dependencies
(edit) @2697   8 years sacerdot Compiler fixed to include the ERTLptrToLTL pass.
(edit) @2696   8 years sacerdot I can't get this right... :-(
(edit) @2695   8 years sacerdot Renamed again.
(edit) @2694   8 years tranquil completed ERTLptrToLTL
(edit) @2693   8 years sacerdot 1. Stuff moved to correct places. 2. ERTLptr pass added
(edit) @2692   8 years garnier Add some more constraints in clight_cminor_data.
(edit) @2691   8 years sacerdot ERTLtoERTLptr* moved to the proper place
(edit) @2690   8 years campbell Most of the measurable subtrace preservation proof done.
(edit) @2689   8 years tranquil * fixed passes up to linearisation
(edit) @2688   8 years tranquil * in Arithmeticcs.ma: commented include that breaks script in latest …
(edit) @2687   8 years tranquil * polished some interfaces
(edit) @2686   8 years mckinna two minor modifications to assist disambiguation of "lookup" file …
(edit) @2685   8 years campbell Progress on measurable trace preservation: prefix preserves observable …
(edit) @2684   8 years sacerdot …
Note: See TracRevisionLog for help on using the revision log.