|
|
|
@2991
|
7 years |
piccolo |
Fixed cond and seq case in StatusSimulationHelper?
Added cost case in …
|
|
|
|
@2990
|
7 years |
campbell |
Replace dodgy hypothesis by nice ones, clean up a little.
|
|
|
|
@2989
|
7 years |
campbell |
Make front-end measurability preservation proof cope with moving the …
|
|
|
|
@2975
|
7 years |
tranquil |
* RTL premain fixed
* fixed bug in back end ops (subtracting to a …
|
|
|
|
@2959
|
7 years |
sacerdot |
Typo
|
|
|
|
@2958
|
7 years |
sacerdot |
Error message implemented.
|
|
|
|
@2953
|
7 years |
campbell |
Fix silly label handling bug I realised was there during my talk…
|
|
|
|
@2927
|
7 years |
tranquil |
stupid bug in bool_of_beval
|
|
|
|
@2926
|
7 years |
tranquil |
corrected bug in executing Sub
|
|
|
|
@2914
|
7 years |
campbell |
Use single definition for stack measurement.
|
|
|
|
@2896
|
7 years |
campbell |
Complete part of measurable to structured subtraces proof that
shows …
|
|
|
|
@2895
|
7 years |
campbell |
Match up function id from RTLabs Callstate with shadow stack,
use in …
|
|
|
|
@2871
|
7 years |
tranquil |
op2 evaluation on beval's rendered oblivious to carry bit when …
|
|
|
|
@2870
|
7 years |
sacerdot |
Proof fixed.
|
|
|
|
@2869
|
7 years |
tranquil |
some reorganization of definitions, and a new taaf_append_taaf
|
|
|
|
@2843
|
7 years |
piccolo |
1) Fixed a litte bug in Joint.ma
2) ERTL to ERTLptr correctness proof …
|
|
|
|
@2824
|
7 years |
tranquil |
* moved sum on lists notation to extranat
* used sum on lists to …
|
|
|
|
@2807
|
7 years |
mckinna |
Yet another ErrorMessage?
Removed corresponding axiom in …
|
|
|
|
@2801
|
7 years |
piccolo |
Partial commit not yet finished
|
|
|
|
@2800
|
7 years |
campbell |
Tidy up Measurable.ma a little, get rid of obsolete comments.
|
|
|
|
@2799
|
7 years |
tranquil |
* added taaf_to_taa, conversion from trace_any_any_free to …
|
|
|
|
@2796
|
7 years |
tranquil |
* added global notation for existence in Type[1] (\exists[1] x.P)
* in …
|
|
|
|
@2795
|
7 years |
sacerdot |
Added new function Measurable.observe_all_in_measurable to be used to …
|
|
|
|
@2783
|
7 years |
piccolo |
modified joint_closed_internal_function definition (added condition on …
|
|
|
|
@2769
|
7 years |
mckinna |
Mistakenly commented out
both as_cost_get_label (needed; OK)
as well …
|
|
|
|
@2768
|
7 years |
mckinna |
Nightmare: file no longer typechecks,
because defn as_cost_get_labels …
|
|
|
|
@2767
|
7 years |
mckinna |
WARNING: BIG commit, which pushes code_size_opt check into …
|
|
|
|
@2760
|
7 years |
sacerdot |
1. Many files repaired.
2. 3 new daemons: 2 in Assembly.ma, 1 in …
|
|
|
|
@2757
|
7 years |
tranquil |
many things are still broken, but there is a partial backtrack on …
|
|
|
|
@2756
|
7 years |
sacerdot |
WARNING: this commit breaks things, sorry, Paolo is going to fix …
|
|
|
|
@2755
|
7 years |
tranquil |
* changed primitives of abstract status (with stuf that is probably …
|
|
|
|
@2751
|
7 years |
mckinna |
Added
| AssemblyTooLarge? : ErrorMessage?
to complete compiler.ma
|
|
|
|
@2727
|
7 years |
campbell |
Remove a couple of redundant hypotheses.
|
|
|
|
@2726
|
7 years |
campbell |
Show max stack preserved in FEMeasurable.
|
|
|
|
@2725
|
7 years |
campbell |
Add observables to FEMeasurable proof; fix silly typo.
|
|
|
|
@2724
|
7 years |
campbell |
Add RTLabs cost labelling checks to compiler.ma.
|
|
|
|
@2722
|
7 years |
campbell |
It's easier to keep the real function identifier in front-end …
|
|
|
|
@2720
|
7 years |
tranquil |
implemented back end ops that were still axioms
|
|
|
|
@2703
|
7 years |
mckinna |
now includes defn of costlabel_map
|
|
|
|
@2690
|
7 years |
campbell |
Most of the measurable subtrace preservation proof done.
|
|
|
|
@2685
|
7 years |
campbell |
Progress on measurable trace preservation: prefix preserves observable …
|
|
|
|
@2682
|
7 years |
campbell |
Don't apply inv in after_n_steps to last state.
|
|
|
|
@2678
|
7 years |
campbell |
Switch to single source step simulations for front-end measurable …
|
|
|
|
@2673
|
7 years |
tranquil |
corrected some compilation errors (that might depend on some matita update)
|
|
|
|
@2670
|
7 years |
campbell |
Clean up from recent commits.
|
|
|
|
@2669
|
7 years |
campbell |
Tweak exec_steps output; show that simulations extend to measurable …
|
|
|
|
@2668
|
7 years |
campbell |
Intermediate measurable proof check-in before I change its traces again.
|
|
|
|
@2646
|
7 years |
sacerdot |
A tag was classified as an error message. Fixed.
|
|
|
|
@2645
|
7 years |
sacerdot |
1. some broken back-end files repaires, several still to go
2. the …
|
|
|
|
@2644
|
7 years |
campbell |
Commit some work on FEMeasurable before trying to do something nicer …
|
|
|
|
@2641
|
7 years |
piccolo |
defined dummy block code equals to 0
|
|
|
|
@2624
|
7 years |
campbell |
Properly evict unused and axiomatised Floats.
|
|
|
|
@2618
|
7 years |
campbell |
Tidy up measurable a little.
|
|
|
|
@2617
|
7 years |
campbell |
Trivial simplification on split_trace.
|
|
|
|
@2608
|
7 years |
garnier |
Regions are no more stored in blocks. block_region now tests the id, …
|
|
|
|
@2604
|
7 years |
piccolo |
ERTLtoERTLptr in place.
|
|
|
|
@2603
|
7 years |
piccolo |
Dead code commented out.
|
|
|
|
@2601
|
7 years |
sacerdot |
Extraction to ocaml is now working, with a couple of bugs left.
One …
|
|
|
|
@2599
|
7 years |
tranquil |
* map_opt and map on positive maps are now clean (erase empty …
|
|
|
|
@2597
|
7 years |
campbell |
Some work in progress on measurable subtrace preservation.
|
|
|
|
@2596
|
7 years |
campbell |
Use a simpler stack cost map, and then specialise to each semantics.
|
|
|
|
@2590
|
7 years |
piccolo |
added monad machineary for ERTL to ERTLptr translation
eval_seq_no_pc …
|
|
|
|
@2582
|
7 years |
garnier |
Some progress on CL to CM.
|
|
|
|
@2570
|
7 years |
piccolo |
ERTLtoERTLptr in place
|
|
|
|
@2569
|
7 years |
campbell |
Fix Clight semantics for ptr + char. (Compiler works anyway.)
|
|
|
|
@2553
|
7 years |
tranquil |
as_classify changed to a partial function
added a status for tailcalls
|
|
|
|
@2548
|
7 years |
tranquil |
in BackEndOps?, cleaner def of be_op2
new statement of …
|
|
|
|
@2541
|
7 years |
tranquil |
adapted size notation to last matita lib update (01/12/2012)
that …
|
|
|
|
@2540
|
7 years |
tranquil |
cl_jump case now provides a proof of costedness of the following state
|
|
|
|
@2539
|
7 years |
tranquil |
added cl_jump case to trace_any_any_free
|
|
|
|
@2534
|
7 years |
campbell |
Tweak measurable definition to stop at the return from a function.
|
|
|
|
@2533
|
7 years |
campbell |
Some fall out from removing floats.
|
|
|
|
@2531
|
7 years |
mckinna |
Trivial tweaks.
|
|
|
|
@2530
|
7 years |
tranquil |
temporary switch to cl_jump treated as cl_other
fixed script for new …
|
|
|
|
@2511
|
7 years |
campbell |
Conjecture main Cminor/RTLabs simulation results.
Add a few notes …
|
|
|
|
@2508
|
7 years |
mckinna |
more tweaks. compiler and correctness still build.
|
|
|
|
@2503
|
7 years |
mckinna |
tidied up, with new auxiliary defns, some refactoring, some code …
|
|
|
|
@2502
|
7 years |
campbell |
Sketch a little about how measurable traces might work with RTLabs and …
|
|
|
|
@2500
|
7 years |
garnier |
Continuing work on simulation in Clight/Cminor?
|
|
|
|
@2496
|
7 years |
garnier |
Some tentative work on the simulation proof for expressions, in order …
|
|
|
|
@2487
|
7 years |
campbell |
Set up "after_n_steps" to enforce an invariant on states.
|
|
|
|
@2486
|
7 years |
campbell |
First go at a generalised version of measurable.
|
|
|
|
@2478
|
7 years |
tranquil |
unified is_internal_function_of_program and is_internal_function
|
|
|
|
@2477
|
7 years |
tranquil |
status_simulation reformulated
definition of joint_classify split up …
|
|
|
|
@2476
|
7 years |
piccolo |
fixed commutation lemmas in lineariseProof
started proof of main …
|
|
|
|
@2474
|
7 years |
tranquil |
changed form of a statement
|
|
|
|
@2473
|
7 years |
tranquil |
put some generic stuff we need in the back end in extraGlobalenvs …
|
|
|
|
@2471
|
7 years |
campbell |
Tame global environments a little.
|
|
|
|
@2470
|
7 years |
tranquil |
completely separated program counters from code pointers in joint …
|
|
|
|
@2468
|
7 years |
garnier |
Floats are gone from the front-end. Some trace amount might remain in …
|
|
|
|
@2463
|
7 years |
tranquil |
swapped back call_rel and ret_rel…
|
|
|
|
@2462
|
7 years |
tranquil |
separated in back end values program counters from code pointers …
|
|
|
|
@2459
|
7 years |
campbell |
Syntax update
|
|
|
|
@2457
|
7 years |
tranquil |
rewritten function handling in joint
swapped call_rel with ret_rel in …
|
|
|
|
@2453
|
7 years |
tranquil |
come changes in monad notation to
* avoid pretty printed monsters
* …
|
|
|
|
@2444
|
7 years |
campbell |
Some inversion lemmas for after_n_steps for dealing with >1 source …
|
|
|
|
@2443
|
7 years |
tranquil |
changed joint's stack pointer and internal stack
|
|
|
|
@2439
|
7 years |
campbell |
Get a proper reverse mapping of function blocks to identifiers by …
|
|
|
|
@2436
|
7 years |
tranquil |
small changes
|
|
|
|
@2435
|
7 years |
tranquil |
new back end operations
|
|
|
|
