|
|
@1945
|
9 years |
sacerdot |
All proof statements repaired.
|
|
|
@1941
|
9 years |
mulligan |
Changes to the AssemblyProof? with a few more (large) axioms closed.
|
|
|
@1939
|
9 years |
mulligan |
Changes to get things to compile and to avoid the dependency …
|
|
|
@1936
|
9 years |
mulligan |
Some holes filled in AssemblyProof?.ma.
|
|
|
@1668
|
9 years |
boender |
- split build_maps into build_maps and build_maps_ok
- work with CSC …
|
|
|
@1667
|
9 years |
sacerdot |
Main lemma for the main_thm of AssemblyProof? re-declared as an axiom …
|
|
|
@1666
|
9 years |
sacerdot |
PreStatus? datatype change: the code_memory field is not a left …
|
|
|
@1649
|
9 years |
boender |
- changes to Assembly for integration with Policy and easier use of …
|
|
|
@1616
|
9 years |
sacerdot |
Partially ported to new Matita syntax.
Because of some changes in …
|
|
|
@1607
|
9 years |
sacerdot |
Porting to new library.
|
|
|
@1484
|
9 years |
sacerdot |
…
|
|
|
@1333
|
9 years |
sacerdot |
Avoid using the name of the construction of jmeq.
|
|
|
@1045
|
10 years |
mulligan |
resolved conflict in rtlabs
|
|
|
@1043
|
10 years |
sacerdot |
Axiom commented out.
|
|
|
@1042
|
10 years |
sacerdot |
Dead code removed.
Slow code uncommented.
|
|
|
@1041
|
10 years |
sacerdot |
fetch_assembly is still working after bug fix
|
|
|
@1039
|
10 years |
sacerdot |
fetch_assembly_pseudo2 repaired from dependent type madness
|
|
|
@1037
|
10 years |
sacerdot |
Main theorem: comments are working again.
|
|
|
@1036
|
10 years |
sacerdot |
…
|
|
|
@1035
|
10 years |
sacerdot |
Main theorem (broken because of dependent types) almost restored.
|
|
|
@1015
|
10 years |
sacerdot |
One intermediate version of main_thm0 close to be repaired.
|
|
|
@1014
|
10 years |
sacerdot |
The main theorem is completely broken (again).
|
|
|
@998
|
10 years |
sacerdot |
Half repaired, half broken. Most functions no longer return option …
|
|
|
@994
|
10 years |
mulligan |
small changes
|
|
|
@993
|
10 years |
sacerdot |
More Russell everywhere; getting closer to the goal.
|
|
|
@992
|
10 years |
mulligan |
a few more axioms closed
|
|
|
@991
|
10 years |
mulligan |
loads of axioms related to equality on instructions closed
|
|
|
@989
|
10 years |
sacerdot |
Type of build_maps strengthened.
|
|
|
@988
|
10 years |
sacerdot |
Proof restored.
|
|
|
@987
|
10 years |
sacerdot |
Real parameterization over the policy.
|
|
|
@985
|
10 years |
sacerdot |
1) Major refactoring: proofs moved where they should be.
2) New …
|
|
|
@982
|
10 years |
boender |
- this should work (see previous commit)
|
|
|
@979
|
10 years |
sacerdot |
…
|
|
|
@977
|
10 years |
sacerdot |
#$%@#$@#$
|
|
|
@975
|
10 years |
sacerdot |
…
|
|
|
@972
|
10 years |
sacerdot |
…
|
|
|
@971
|
10 years |
sacerdot |
…
|
|
|
@959
|
10 years |
sacerdot |
…
|
|
|
@951
|
10 years |
sacerdot |
long call case completed
|
|
|
@950
|
10 years |
sacerdot |
Horrible sub-proof finished :-)
|
|
|
@949
|
10 years |
mulligan |
resolved conflict, work from today
|
|
|
@948
|
10 years |
sacerdot |
Some progress on the Call case.
|
|
|
@946
|
10 years |
sacerdot |
Jmp case repaired after addition of MAP hypothesis.
|
|
|
@945
|
10 years |
mulligan |
more small changes to proof of main thrm
|
|
|
@944
|
10 years |
mulligan |
split definition
|
|
|
@943
|
10 years |
sacerdot |
…
|
|
|
@942
|
10 years |
sacerdot |
New invariant for the main theorem.
The new invariant is much more …
|
|
|
@941
|
10 years |
sacerdot |
Jmp case finished up to arithmetical properties.
|
|
|
@940
|
10 years |
mulligan |
more changes to inc case of main theorem
|
|
|
@939
|
10 years |
sacerdot |
Long Jmp case finished.
|
|
|
@938
|
10 years |
sacerdot |
…
|
|
|
@937
|
10 years |
mulligan |
resolved conflict in assembly_proof, more lemmas added
|
|
|
@936
|
10 years |
sacerdot |
Ticks are now handled correctly everywhere and the main proof takes …
|
|
|
@935
|
10 years |
mulligan |
changes to status and assembly proof
|
|
|
@934
|
10 years |
sacerdot |
…
|
|
|
@933
|
10 years |
sacerdot |
New proof strategy.
|
|
|
@932
|
10 years |
sacerdot |
…
|
|
|
@931
|
10 years |
sacerdot |
…
|
|
|
@930
|
10 years |
sacerdot |
Comment, Cost, ADD, ADC cases done.
|
|
|
@929
|
10 years |
mulligan |
added ticks_of function
|
|
|
@926
|
10 years |
sacerdot |
Main theorem false because of ticks :-(
|
|
|
@925
|
10 years |
sacerdot |
…
|
|
|
@924
|
10 years |
sacerdot |
…
|
|
|
@923
|
10 years |
sacerdot |
Main theorem made nice... but unprovable at the moment.
|
|
|
@921
|
10 years |
mulligan |
resolved conflict, fixed bugs
|
|
|
@919
|
10 years |
sacerdot |
Back to a readable statement.
|
|
|
@916
|
10 years |
sacerdot |
Fix for jump_expansion_policy.
|
|
|
@915
|
10 years |
mulligan |
finished changes to fetch_assembly_pseudo2
|
|
|
@912
|
10 years |
sacerdot |
Readable main theorem statement.
|
|
|
@911
|
10 years |
sacerdot |
Type of set_code_memory generalized.
|
|
|
@909
|
10 years |
sacerdot |
Back to the main theorem.
|
|
|
@908
|
10 years |
sacerdot |
Next big lemma proved!
|
|
|
@906
|
10 years |
sacerdot |
…
|
|
|
@905
|
10 years |
mulligan |
work from today
|
|
|
@904
|
10 years |
sacerdot |
Cleanup.
|
|
|
@903
|
10 years |
sacerdot |
Statement of new main lemma (as axiom).
|
|
|
@902
|
10 years |
sacerdot |
Cleanup.
|
|
|
@901
|
10 years |
sacerdot |
Second main lemma proved.
|
|
|
@897
|
10 years |
sacerdot |
Proof completed, fetch and assembly are mutual inverses.
|
|
|
@896
|
10 years |
sacerdot |
Proof finished (but ugly) :-)
|
|
|
@894
|
10 years |
sacerdot |
Bug more evident.
|
|
|
@893
|
10 years |
sacerdot |
Cleanup.
|
|
|
@892
|
10 years |
sacerdot |
First fundamental lemma almost finished.
|
|
|
@890
|
10 years |
sacerdot |
Better statement, begin of uniform proof.
|
|
|
@889
|
10 years |
sacerdot |
Minor changes because of the new, weaker (but much faster) delift.
|
|
|
@885
|
10 years |
sacerdot |
Proof almost finished, but rewritings are extremely slow.
|
|
|
@884
|
10 years |
sacerdot |
…
|
|
|
@883
|
10 years |
sacerdot |
Merged done well.
|
|
|
@877
|
10 years |
mulligan |
work from today
|