|
|
@1029
|
10 years |
sacerdot |
…
|
|
|
@1028
|
10 years |
sacerdot |
One more sentence restored and fitted in.
|
|
|
@1027
|
10 years |
sacerdot |
Bug fixed in figure.
|
|
|
@1026
|
10 years |
mulligan |
final version? under 16 pages
|
|
|
@1025
|
10 years |
mulligan |
removing stray single words to reduce page usage
|
|
|
@1024
|
10 years |
mulligan |
tidied explanation of proof
|
|
|
@1023
|
10 years |
mulligan |
changes to english in matita section, shrunk diagrams in introduction …
|
|
|
@1022
|
10 years |
sacerdot |
…
|
|
|
@1021
|
10 years |
mulligan |
tidied english in sect 3
|
|
|
@1020
|
10 years |
sacerdot |
More on Matita.
|
|
|
@1019
|
10 years |
sacerdot |
Finished rewriting of Section 3.
|
|
|
@1018
|
10 years |
mulligan |
tidying
|
|
|
@1017
|
10 years |
mulligan |
complete, just under 16 pages
|
|
|
@1016
|
10 years |
sacerdot |
Many fixes to the code snippets.
|
|
|
@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).
|
|
|
@1013
|
10 years |
mulligan |
more added
|
|
|
@1012
|
10 years |
mulligan |
just a few things left to change
|
|
|
@1011
|
10 years |
mulligan |
…
|
|
|
@1010
|
10 years |
mulligan |
more added, finished up to end of subsect 3.2
|
|
|
@1009
|
10 years |
mulligan |
added line number counts, etc.
|
|
|
@1008
|
10 years |
mulligan |
…
|
|
|
@1007
|
10 years |
mulligan |
added explanation of sdcc
|
|
|
@1006
|
10 years |
boender |
- added fold + lemmas on fold
|
|
|
@1005
|
10 years |
sacerdot |
…
|
|
|
@1004
|
10 years |
mulligan |
changes to typesetting
|
|
|
@1003
|
10 years |
sacerdot |
…
|
|
|
@1002
|
10 years |
sacerdot |
…
|
|
|
@1001
|
10 years |
mulligan |
reworded intro
|
|
|
@1000
|
10 years |
sacerdot |
…
|
|
|
@999
|
10 years |
mulligan |
conclusions
|
|
|
@998
|
10 years |
sacerdot |
Half repaired, half broken. Most functions no longer return option …
|
|
|
@997
|
10 years |
mulligan |
minor linguistic polishing
|
|
|
@996
|
10 years |
sacerdot |
Minor fixes.
|
|
|
@995
|
10 years |
mulligan |
changes
|
|
|
@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
|
|
|
@990
|
10 years |
sacerdot |
Do no longer use the daemon automatically :-)
|
|
|
@989
|
10 years |
sacerdot |
Type of build_maps strengthened.
|
|
|
@988
|
10 years |
sacerdot |
Proof restored.
|
|
|
@987
|
10 years |
sacerdot |
Real parameterization over the policy.
|
|
|
@986
|
10 years |
mulligan |
changes to paper
|
|
|
@985
|
10 years |
sacerdot |
1) Major refactoring: proofs moved where they should be.
2) New …
|
|
|
@984
|
10 years |
mulligan |
updates
|
|
|
@983
|
10 years |
mulligan |
more work added
|
|
|
@982
|
10 years |
boender |
- this should work (see previous commit)
|
|
|
@981
|
10 years |
mulligan |
added more, worked on conclusions and related work. need just to …
|
|
|
@980
|
10 years |
boender |
- displaced some lemmas (jmeq) from AssemblyProof?
|
|
|
@979
|
10 years |
sacerdot |
…
|
|
|
@978
|
10 years |
campbell |
Update remaining Clight examples.
|
|
|
@977
|
10 years |
sacerdot |
#$%@#$@#$
|
|
|
@976
|
10 years |
mulligan |
more changes, rearranged paper to put lemmas/defns in correct order, …
|
|
|
@975
|
10 years |
sacerdot |
…
|
|
|
@974
|
10 years |
mulligan |
more added
|
|
|
@973
|
10 years |
mulligan |
work from yesterday that could not be committed
|
|
|
@972
|
10 years |
sacerdot |
…
|
|
|
@971
|
10 years |
sacerdot |
…
|
|
|
@970
|
10 years |
mulligan |
commit as i need some money for the communists
|
|
|
@969
|
10 years |
mulligan |
more work on paper, nearly finished policy discussion
|
|
|
@968
|
10 years |
mulligan |
work on paper
|
|
|
@967
|
10 years |
campbell |
Update RTLabs pretty printer and examples.
|
|
|
@966
|
10 years |
campbell |
Update Cminor pretty printer and some examples.
|
|
|
@965
|
10 years |
campbell |
Update some Clight examples.
|
|
|
@964
|
10 years |
campbell |
Rest of cast fix.
|
|
|
@963
|
10 years |
campbell |
Extra debugging aid for animation of semantics.
|
|
|
@962
|
10 years |
campbell |
Casts should use source type's signedness, not the target's.
|
|
|
@961
|
10 years |
campbell |
Use precise bitvector sizes throughout the front end, rather than …
|
|
|
@960
|
10 years |
mulligan |
more work on paper
|
|
|
@959
|
10 years |
sacerdot |
…
|
|
|
@958
|
10 years |
sacerdot |
…
|
|
|
@957
|
10 years |
sacerdot |
…
|
|
|
@956
|
10 years |
mulligan |
changes prior to claudio's editing
|
|
|
@955
|
10 years |
mulligan |
more work on conclusions
|
|
|
@954
|
10 years |
mulligan |
more changes to introduction
|
|
|
@953
|
10 years |
mulligan |
more changes, including additions to the bibliography, and tightening …
|
|
|
@952
|
10 years |
mulligan |
work from yesterday
|
|
|
@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.
|
|
|
@947
|
10 years |
sacerdot |
…
|
|
|
@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.
|
|
|