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)
@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
9 years
mulligan
CJNE case a complete mess.
(edit)
@2017
9 years
mulligan
Large swathes of proof of main lemma added.
Diff
Rev
Age
Author
Log Message
(edit)
@2015
9 years
mulligan
Changes following a conversation with Jaap: as it stands computation …
(edit)
@2014
9 years
mulligan
Fixed problem in James' email message.
Diff
Rev
Age
Author
Log Message
(edit)
@2008
9 years
boender
- substantial closing of holes in proof
Diff
Rev
Age
Author
Log Message
(edit)
@2006
9 years
boender
- added alias for bitvector zero - changed extralib bounded …
(edit)
@2005
9 years
boender
- minor changes to make things compile with a clean checkout
Diff
Rev
Age
Author
Log Message
(edit)
@2001
9 years
campbell
Get the compiler to output more.
Diff
Rev
Age
Author
Log Message
(edit)
@1996
9 years
campbell
Work on correctness from yesterday.
Diff
Rev
Age
Author
Log Message
(edit)
@1987
9 years
campbell
Move BEValues to common to reflect their use in the memory model for …
Diff
Rev
Age
Author
Log Message
(edit)
@1985
9 years
mulligan
A single `false' case for unconditional jumps completed.
(edit)
@1984
9 years
mulligan
Most proof obligations closed in main_lemma apart from those of the …
(edit)
@1983
9 years
mulligan
Changes to simplify the simpler cases of the main_lemma.
Diff
Rev
Age
Author
Log Message
(edit)
@1979
9 years
sacerdot
Very very very tricky lemma closed. A dreadful mix of JM equality …
(edit)
@1978
9 years
sacerdot
Two more cases completed.
(edit)
@1977
9 years
sacerdot
Unblocked: let ... as hides two different terms, one that uses Leibniz …
(edit)
@1976
9 years
tranquil
* monads: just changed some defs, which had to be propagated in some …
(edit)
@1975
9 years
mulligan
Work from today on closing main_thm.
Diff
Rev
Age
Author
Log Message
(edit)
@1973
9 years
boender
- removed superfluous match - displaced 'cases daemon'
(edit)
@1972
9 years
mulligan
Simple lemma with strangely complex proof complete.
(edit)
@1971
9 years
sacerdot
1. Interpret.ma: we need to prove \sigma (execute_preinstruction …
Diff
Rev
Age
Author
Log Message
(edit)
@1969
9 years
sacerdot
Some more progress, but now we must prove something on a Russell …
Diff
Rev
Age
Author
Log Message
(edit)
@1967
9 years
sacerdot
Mov case completed.
(edit)
@1966
9 years
mulligan
Progress made on main_thm proof: trying to find a pattern to use …
(edit)
@1965
9 years
boender
- further completed proof, changed jump_expansion' to reflect new type …
(edit)
@1964
9 years
tranquil
introduced as_label_of_cost and adapted accordingly. Equality of cost …
(edit)
@1963
9 years
sacerdot
More progress in restoring the original proof.
(edit)
@1962
9 years
sacerdot
More examples are now indexed.
(edit)
@1961
9 years
sacerdot
No more interaction required.
Diff
Rev
Age
Author
Log Message
(edit)
@1959
9 years
mulligan
Commented out diverging application of demodulation and closed goals …
(edit)
@1958
9 years
mulligan
Marked divergence in
StatusProofs?
.ma
(edit)
@1957
9 years
mulligan
Stitching proofs back together after slight change in statement of …
(edit)
@1956
9 years
boender
- finished proof of lemma (where auto does strange things again)
(edit)
@1955
9 years
mulligan
Completed proof of snd_assembly_1_pseudoinstruction_ok, modulo some …
Diff
Rev
Age
Author
Log Message
(edit)
@1953
9 years
mulligan
Commit to avoid conflicts.
(edit)
@1952
9 years
sacerdot
AssemblyProof?
splitted.
(edit)
@1951
9 years
sacerdot
Bug with overloaded names in the context.
(edit)
@1950
9 years
boender
- advances in policy
Diff
Rev
Age
Author
Log Message
(edit)
@1948
9 years
mulligan
Weakened statements of ASM/Assembly.ma and ASM/AssemblyProof.ma, so …
(edit)
@1947
9 years
sacerdot
Failure of automation/demod investigated a little bit.
(edit)
@1946
9 years
sacerdot
\snd half_add => add everywhere
(edit)
@1945
9 years
sacerdot
All proof statements repaired.
(edit)
@1944
9 years
sacerdot
common/StructuredTraces no longer depends on ASM/AbstractStatus (again)
(edit)
@1943
9 years
boender
- changed 'labels okay' part of create_label_cost_map
(edit)
@1942
9 years
mulligan
Work on showing the equivalence of two methods of looking up from the maps.
(edit)
@1941
9 years
mulligan
Changes to the
AssemblyProof?
with a few more (large) axioms closed.
(edit)
@1940
9 years
boender
- committed new version of final invariant
(edit)
@1939
9 years
mulligan
Changes to get things to compile and to avoid the dependency …
(edit)
@1938
9 years
sacerdot
Definitions moved to the right places, now everything compiles again.
(edit)
@1937
9 years
boender
- filled in some of the gaps in the proof of Policy - reverted …
(edit)
@1936
9 years
mulligan
Some holes filled in
AssemblyProof?
.ma.
(edit)
@1935
9 years
mulligan
Generalized some lemma in ASM/CostsProof.ma to work on abstract …
(edit)
@1934
9 years
boender
- various & sundry moves of lemmas to better places - integrated …
Note:
See
TracRevisionLog
for help on using the revision log.
Download in other formats:
RSS Feed
ChangeLog