|
|
@2146
|
9 years |
sacerdot |
1. specification fixed again
2. the proof in AssemblyProof? is now …
|
|
|
@2144
|
9 years |
sacerdot |
1. Policy specification fixed
2. Proof of monotonicity of sigma
|
|
|
@2143
|
9 years |
mulligan |
Changes to the subaddressing mode elim functions moved into their …
|
|
|
@2142
|
9 years |
sacerdot |
Down to one daemon that requires one lemma (monotonicity of sigma).
|
|
|
@2141
|
9 years |
boender |
- committed working version
|
|
|
@2140
|
9 years |
mulligan |
Done the hardest cases in the main theorem. Just got a few daemons to …
|
|
|
@2139
|
9 years |
mulligan |
Changes to get the main lemma compiling again. Changes pushed into …
|
|
|
@2138
|
9 years |
sacerdot |
Invariant exported from proof of assembly_ok.
|
|
|
@2137
|
9 years |
sacerdot |
Bug fixed in specification.
|
|
|
@2136
|
9 years |
sacerdot |
…
|
|
|
@2135
|
9 years |
sacerdot |
One complex daemon changed to two simpler ones.
|
|
|
@2132
|
9 years |
sacerdot |
Two more daemons closed, one left.
|
|
|
@2131
|
9 years |
sacerdot |
No more need for functional extensionality.
|
|
|
@2130
|
9 years |
sacerdot |
Proof repaired after Dominic's bug fix.
|
|
|
@2129
|
9 years |
mulligan |
Large changes from today trying to complete the main theorem. Again :(
|
|
|
@2128
|
9 years |
sacerdot |
Final shuffling around
|
|
|
@2127
|
9 years |
sacerdot |
Last daemon closed
|
|
|
@2126
|
9 years |
sacerdot |
Proof improved (for case 3) + new proof (for case 11)
|
|
|
@2125
|
9 years |
boender |
- some more displacement from Policy to Util
|
|
|
@2124
|
9 years |
sacerdot |
Much more shuffling around to proper places
|
|
|
@2123
|
9 years |
boender |
- moved is_well_labeled_p to Status and instruction_is_label to ASM
…
|
|
|
@2122
|
9 years |
sacerdot |
More stuff moved around in proper places
|
|
|
@2121
|
9 years |
sacerdot |
More functions moved to the places they belong to
|
|
|
@2119
|
9 years |
sacerdot |
load_code_memory moved to Fetch.ma and proved correct w.r.t. next …
|
|
|
@2115
|
9 years |
sacerdot |
Old commented out code removed
|
|
|
@2114
|
9 years |
sacerdot |
Proof repaired
|
|
|
@2113
|
9 years |
sacerdot |
Proof by cases repaired; dead code removed.
|
|
|
@2112
|
9 years |
sacerdot |
WARNING: this commit may break some code.
- dead/useless code removed
|
|
|
@2111
|
9 years |
sacerdot |
Cleanup: lemmas/theorems/axioms moved to the right places.
|
|
|
@2110
|
9 years |
sacerdot |
…
|
|
|
@2109
|
9 years |
mulligan |
Finished porting the large, main lemma to the new notion of jump …
|
|
|
@2108
|
9 years |
mulligan |
Various axioms closed and others moved around. Uncommented main lemma …
|
|
|
@2102
|
9 years |
boender |
- some small changes
|
|
|
@2101
|
9 years |
boender |
- renamed medium to absolute jump
- revised proofs of policy, some …
|
|
|
@2099
|
9 years |
boender |
- added reference to Intel dev manual
|
|
|
@2098
|
9 years |
boender |
- updates & changes
|
|
|
@2097
|
9 years |
mulligan |
Consistency change (institution)
|
|
|
@2096
|
9 years |
mulligan |
Changes to the English for Jaap, and some tidying up and making …
|
|
|
@2095
|
9 years |
mulligan |
Added reference to CompCert? and CompCertTSO.
|
|
|
@2094
|
9 years |
boender |
- oops
|
|
|
@2093
|
9 years |
boender |
- added reference to CompCertTSO
|
|
|
@2092
|
9 years |
mulligan |
Jaap noticed it's Randall Hyde not Holmes.
|
|
|
@2091
|
9 years |
boender |
- systematically changed 'jump' to 'branch'
|
|
|
@2090
|
9 years |
mulligan |
Fixed mistaken reference to RISC instead of CISC architectures.
|
|
|
@2089
|
9 years |
mulligan |
Harmonised institution name to that used by Jaap
|
|
|
@2088
|
9 years |
mulligan |
Added list of keywords as is required. Other minor changes.
|
|
|
@2087
|
9 years |
mulligan |
Tidied up the paper, added a few more things, tidied and expanded …
|
|
|
@2086
|
9 years |
boender |
- spell-check
|
|
|
@2085
|
9 years |
boender |
- rewrote introduction
- changed 'medium' to 'absolute'
- added a bit …
|
|
|
@2084
|
9 years |
boender |
- changed bibliography style
- added CerCo? thanks
- some words of …
|
|
|
@2083
|
9 years |
mulligan |
More work on paper from today.
|
|
|
@2082
|
9 years |
boender |
- reworked and extended presentation of invariants
|
|
|
@2081
|
9 years |
sacerdot |
Type of assembly fixed to be compatible with the old one and to take …
|
|
|
@2080
|
9 years |
boender |
- added references to SDCC and gcc (thanks, Dominic)
- updated sigma …
|
|
|
@2079
|
9 years |
sacerdot |
sigma_policy_specification restyled
|
|
|
@2078
|
9 years |
sacerdot |
sigma_policy_specification has been
1) strengthened
2) made nicer to …
|
|
|
@2077
|
9 years |
boender |
- committed actual file instead of link
|
|
|
@2075
|
9 years |
mulligan |
Solved conflict in AssemblyProof?
|
|
|
@2073
|
9 years |
sacerdot |
All false daemons removed.
|
|
|
@2072
|
9 years |
sacerdot |
We need to import Jaap's invariants now.
|
|
|
@2071
|
9 years |
sacerdot |
More daemons closed, but one is suspect now.
|
|
|
@2070
|
9 years |
sacerdot |
More daemons closed.
|
|
|
@2069
|
9 years |
sacerdot |
…
|
|
|
@2068
|
9 years |
sacerdot |
…
|
|
|
@2067
|
9 years |
sacerdot |
…
|
|
|
@2066
|
9 years |
mulligan |
Finished for the day.
|
|
|
@2065
|
9 years |
boender |
- committed another draft
|
|
|
@2064
|
9 years |
boender |
- more progress
|
|
|
@2063
|
9 years |
mulligan |
Minor fixes
|
|
|
@2062
|
9 years |
sacerdot |
Everything repaired (broken because of new proof obligation for fetch).
|
|
|
@2061
|
9 years |
mulligan |
Added Randall Holmes' Usenet post on branch displacement optimisation …
|
|
|
@2060
|
9 years |
mulligan |
More work on paper.
|
|
|
@2059
|
9 years |
boender |
- updated Policy to work better
|
|
|
@2058
|
9 years |
mulligan |
First draft of changes to main sections (i.e. those describing the …
|
|
|
@2057
|
9 years |
sacerdot |
Repaired (was broken by fetch_pseudo_instruction now taking a proof …
|
|
|
@2056
|
9 years |
sacerdot |
Repaired, ported to new fetch_pseudo_assembly.
The execute_n is …
|
|
|
@2055
|
9 years |
sacerdot |
Warning: this commit adds an hypothesis that breaks all of assembly stuff.
|
|
|
@2054
|
9 years |
boender |
- progress
|
|
|
@2053
|
9 years |
mulligan |
Introduction changed, with many paragraphs deleted.
|
|
|
@2052
|
9 years |
mulligan |
Initial commit of proposed CPP 2012 paper on the proof of correctness …
|
|
|
@2051
|
9 years |
mulligan |
Finished the Jmp case in the main theorem.
|
|
|
@2049
|
9 years |
boender |
- progress
|
|
|
@2048
|
9 years |
boender |
- factorised jump decisions
|
|
|
@2047
|
9 years |
mulligan |
Big bugs in policy calculations found. Waiting for Jaap's commit.
|
|
|
@2046
|
9 years |
boender |
- removed old paper directory
|
|
|
@2045
|
9 years |
boender |
- renamed paper directory
|
|
|
@2040
|
9 years |
sacerdot |
Repaired using new /demod/ that allows to specify the rules to be used.
|
|
|
@2039
|
9 years |
sacerdot |
New, better interface for subaddressing_mode_elim
|
|
|
@2038
|
9 years |
sacerdot |
split => vsplit
|
|
|
@2037
|
9 years |
sacerdot |
flatten is now part of stdlib
|
|
|
@2036
|
9 years |
sacerdot |
New daemon inserted because /demod/ got worst :-(
|
|
|
@2034
|
9 years |
boender |
- split Policy into three separate files for ease (and indeed …
|
|
|
@2032
|
9 years |
sacerdot |
!! BEWARE: major commit !!
1) [affects everybody]
split for …
|
|
|
@2028
|
9 years |
boender |
- bugfix to Assembly (forgotten sigma)
- added …
|
|
|
@2027
|
9 years |
mulligan |
Got the main lemma to apply in the proof of main theorem again and …
|
|
|
@2026
|
9 years |
mulligan |
Added a new file to house the main theorem as the type checking time …
|
|
|
@2024
|
9 years |
mulligan |
Updated AssemblyProof? to fix mismatch in definition of lookup_labels …
|
|
|
@2023
|
9 years |
mulligan |
Closed main lemma modulo closing trivial subgoals about commutations …
|
|
|
@2022
|
9 years |
boender |
- corrected jump calculation algorithm
|
|
|
@2021
|
9 years |
sacerdot |
Proof skeleton in place. Several daemons to be closed adding invariants.
|
|
|