Search:
Login
Preferences
Help/Guide
About Trac
Wiki
Timeline
Roadmap
Browse Source
View Tickets
Search
Context Navigation
View Latest Revision
Older Revisions
→
source:
src
/
ASM
Revision Log Mode:
Stop on copy
Follow copies
Show only adds and deletes
View log starting at
and back to
Show at most
revisions per page.
Show full log messages
Legend:
Added
Modified
Copied or renamed
Diff
Rev
Age
Author
Log Message
(edit)
@2108
8 years
mulligan
Various axioms closed and others moved around. Uncommented main lemma …
Diff
Rev
Age
Author
Log Message
(edit)
@2102
8 years
boender
- some small changes
(edit)
@2101
8 years
boender
- renamed medium to absolute jump - revised proofs of policy, some …
Diff
Rev
Age
Author
Log Message
(edit)
@2099
8 years
boender
- added reference to Intel dev manual
(edit)
@2098
8 years
boender
- updates & changes
(edit)
@2097
8 years
mulligan
Consistency change (institution)
(edit)
@2096
8 years
mulligan
Changes to the English for Jaap, and some tidying up and making …
(edit)
@2095
8 years
mulligan
Added reference to
CompCert?
and CompCertTSO.
(edit)
@2094
8 years
boender
- oops
(edit)
@2093
8 years
boender
- added reference to CompCertTSO
(edit)
@2092
8 years
mulligan
Jaap noticed it's Randall Hyde not Holmes.
(edit)
@2091
8 years
boender
- systematically changed 'jump' to 'branch'
(edit)
@2090
8 years
mulligan
Fixed mistaken reference to RISC instead of CISC architectures.
(edit)
@2089
8 years
mulligan
Harmonised institution name to that used by Jaap
(edit)
@2088
8 years
mulligan
Added list of keywords as is required. Other minor changes.
(edit)
@2087
8 years
mulligan
Tidied up the paper, added a few more things, tidied and expanded …
(edit)
@2086
8 years
boender
- spell-check
(edit)
@2085
8 years
boender
- rewrote introduction - changed 'medium' to 'absolute' - added a bit …
(edit)
@2084
8 years
boender
- changed bibliography style - added
CerCo?
thanks - some words of …
(edit)
@2083
8 years
mulligan
More work on paper from today.
(edit)
@2082
8 years
boender
- reworked and extended presentation of invariants
(edit)
@2081
8 years
sacerdot
Type of assembly fixed to be compatible with the old one and to take …
(edit)
@2080
8 years
boender
- added references to SDCC and gcc (thanks, Dominic) - updated sigma …
(edit)
@2079
8 years
sacerdot
sigma_policy_specification restyled
(edit)
@2078
8 years
sacerdot
sigma_policy_specification has been 1) strengthened 2) made nicer to …
(edit)
@2077
8 years
boender
- committed actual file instead of link
Diff
Rev
Age
Author
Log Message
(edit)
@2075
8 years
mulligan
Solved conflict in
AssemblyProof?
Diff
Rev
Age
Author
Log Message
(edit)
@2073
8 years
sacerdot
All false daemons removed.
(edit)
@2072
8 years
sacerdot
We need to import Jaap's invariants now.
(edit)
@2071
8 years
sacerdot
More daemons closed, but one is suspect now.
(edit)
@2070
8 years
sacerdot
More daemons closed.
(edit)
@2069
8 years
sacerdot
…
(edit)
@2068
8 years
sacerdot
…
(edit)
@2067
8 years
sacerdot
…
(edit)
@2066
8 years
mulligan
Finished for the day.
(edit)
@2065
8 years
boender
- committed another draft
(edit)
@2064
8 years
boender
- more progress
(edit)
@2063
8 years
mulligan
Minor fixes
(edit)
@2062
8 years
sacerdot
Everything repaired (broken because of new proof obligation for fetch).
(edit)
@2061
8 years
mulligan
Added Randall Holmes' Usenet post on branch displacement optimisation …
(edit)
@2060
8 years
mulligan
More work on paper.
(edit)
@2059
8 years
boender
- updated Policy to work better
(edit)
@2058
8 years
mulligan
First draft of changes to main sections (i.e. those describing the …
(edit)
@2057
8 years
sacerdot
Repaired (was broken by fetch_pseudo_instruction now taking a proof …
(edit)
@2056
8 years
sacerdot
Repaired, ported to new fetch_pseudo_assembly. The execute_n is …
(edit)
@2055
8 years
sacerdot
Warning: this commit adds an hypothesis that breaks all of assembly stuff.
(edit)
@2054
8 years
boender
- progress
(edit)
@2053
8 years
mulligan
Introduction changed, with many paragraphs deleted.
(edit)
@2052
8 years
mulligan
Initial commit of proposed CPP 2012 paper on the proof of correctness …
(edit)
@2051
8 years
mulligan
Finished the Jmp case in the main theorem.
Diff
Rev
Age
Author
Log Message
(edit)
@2049
8 years
boender
- progress
(edit)
@2048
8 years
boender
- factorised jump decisions
(edit)
@2047
8 years
mulligan
Big bugs in policy calculations found. Waiting for Jaap's commit.
(edit)
@2046
8 years
boender
- removed old paper directory
(edit)
@2045
8 years
boender
- renamed paper directory
Diff
Rev
Age
Author
Log Message
(edit)
@2040
8 years
sacerdot
Repaired using new /demod/ that allows to specify the rules to be used.
(edit)
@2039
8 years
sacerdot
New, better interface for subaddressing_mode_elim
(edit)
@2038
8 years
sacerdot
split => vsplit
(edit)
@2037
8 years
sacerdot
flatten is now part of stdlib
(edit)
@2036
8 years
sacerdot
New daemon inserted because /demod/ got worst :-(
Diff
Rev
Age
Author
Log Message
(edit)
@2034
8 years
boender
- split Policy into three separate files for ease (and indeed …
Diff
Rev
Age
Author
Log Message
(edit)
@2032
8 years
sacerdot
!! BEWARE: major commit !! 1) [affects everybody] split for …
Diff
Rev
Age
Author
Log Message
(edit)
@2028
8 years
boender
- bugfix to Assembly (forgotten sigma) - added …
(edit)
@2027
8 years
mulligan
Got the main lemma to apply in the proof of main theorem again and …
(edit)
@2026
8 years
mulligan
Added a new file to house the main theorem as the type checking time …
Diff
Rev
Age
Author
Log Message
(edit)
@2024
8 years
mulligan
Updated
AssemblyProof?
to fix mismatch in definition of lookup_labels …
(edit)
@2023
8 years
mulligan
Closed main lemma modulo closing trivial subgoals about commutations …
(edit)
@2022
8 years
boender
- corrected jump calculation algorithm
(edit)
@2021
8 years
sacerdot
Proof skeleton in place. Several daemons to be closed adding invariants.
(edit)
@2020
8 years
mulligan
CJNE case complete, DJNZ case almost complete
Diff
Rev
Age
Author
Log Message
(edit)
@2018
8 years
mulligan
CJNE case a complete mess.
(edit)
@2017
8 years
mulligan
Large swathes of proof of main lemma added.
Diff
Rev
Age
Author
Log Message
(edit)
@2015
8 years
mulligan
Changes following a conversation with Jaap: as it stands computation …
(edit)
@2014
8 years
mulligan
Fixed problem in James' email message.
Diff
Rev
Age
Author
Log Message
(edit)
@2008
8 years
boender
- substantial closing of holes in proof
Diff
Rev
Age
Author
Log Message
(edit)
@2006
8 years
boender
- added alias for bitvector zero - changed extralib bounded …
(edit)
@2005
8 years
boender
- minor changes to make things compile with a clean checkout
Diff
Rev
Age
Author
Log Message
(edit)
@2001
8 years
campbell
Get the compiler to output more.
Diff
Rev
Age
Author
Log Message
(edit)
@1996
8 years
campbell
Work on correctness from yesterday.
Diff
Rev
Age
Author
Log Message
(edit)
@1987
8 years
campbell
Move BEValues to common to reflect their use in the memory model for …
Diff
Rev
Age
Author
Log Message
(edit)
@1985
8 years
mulligan
A single `false' case for unconditional jumps completed.
(edit)
@1984
8 years
mulligan
Most proof obligations closed in main_lemma apart from those of the …
(edit)
@1983
8 years
mulligan
Changes to simplify the simpler cases of the main_lemma.
Diff
Rev
Age
Author
Log Message
(edit)
@1979
8 years
sacerdot
Very very very tricky lemma closed. A dreadful mix of JM equality …
(edit)
@1978
8 years
sacerdot
Two more cases completed.
(edit)
@1977
8 years
sacerdot
Unblocked: let ... as hides two different terms, one that uses Leibniz …
(edit)
@1976
8 years
tranquil
* monads: just changed some defs, which had to be propagated in some …
(edit)
@1975
8 years
mulligan
Work from today on closing main_thm.
Diff
Rev
Age
Author
Log Message
(edit)
@1973
8 years
boender
- removed superfluous match - displaced 'cases daemon'
(edit)
@1972
8 years
mulligan
Simple lemma with strangely complex proof complete.
(edit)
@1971
8 years
sacerdot
1. Interpret.ma: we need to prove \sigma (execute_preinstruction …
Diff
Rev
Age
Author
Log Message
(edit)
@1969
8 years
sacerdot
Some more progress, but now we must prove something on a Russell …
Diff
Rev
Age
Author
Log Message
(edit)
@1967
8 years
sacerdot
Mov case completed.
(edit)
@1966
8 years
mulligan
Progress made on main_thm proof: trying to find a pattern to use …
(edit)
@1965
8 years
boender
- further completed proof, changed jump_expansion' to reflect new type …
(edit)
@1964
8 years
tranquil
introduced as_label_of_cost and adapted accordingly. Equality of cost …
(edit)
@1963
8 years
sacerdot
More progress in restoring the original proof.
(edit)
@1962
8 years
sacerdot
More examples are now indexed.
(edit)
@1961
8 years
sacerdot
No more interaction required.
Diff
Rev
Age
Author
Log Message
(edit)
@1959
8 years
mulligan
Commented out diverging application of demodulation and closed goals …
Note:
See
TracRevisionLog
for help on using the revision log.
Download in other formats:
RSS Feed
ChangeLog