|
|
@2190
|
7 years |
sacerdot |
Two daemons left.
|
|
|
@2189
|
7 years |
sacerdot |
Proof very close to completion.
|
|
|
@2188
|
7 years |
sacerdot |
1. Policy specification generalized
2. All invariants but the main one …
|
|
|
@2187
|
7 years |
mulligan |
Work from today on the big proof.
|
|
|
@2186
|
7 years |
tranquil |
updated joint semantics
|
|
|
@2185
|
7 years |
campbell |
Use bitvectors for offsets.
|
|
|
@2184
|
7 years |
campbell |
Minor fix ups.
|
|
|
@2183
|
7 years |
mulligan |
More progress on main lemma proof.
|
|
|
@2182
|
7 years |
tranquil |
updated linearisation pass
|
|
|
@2181
|
7 years |
mulligan |
Work from the last week on the new formulation of the main lemma for …
|
|
|
@2180
|
7 years |
campbell |
Fix off-by-one error in GenMem?.ma.
|
|
|
@2179
|
7 years |
campbell |
Dependent pair monad binding notation.
|
|
|
@2178
|
7 years |
campbell |
Shift some notation into utilities.
|
|
|
@2177
|
7 years |
campbell |
Tidy up multiplication.
|
|
|
@2176
|
7 years |
campbell |
Remove memory spaces other than XData and Code; simplify pointers as a …
|
|
|
@2175
|
7 years |
tranquil |
corrected small bug
|
|
|
@2174
|
7 years |
tranquil |
* factored out script for (axiomatised) fixpoint computation
* ERTL → …
|
|
|
@2173
|
7 years |
mulligan |
MUL case of main lemma nearly complete (subject to two small holes …
|
|
|
@2172
|
7 years |
mulligan |
Moved new versions of get_ / set_arg_* into Status.ma. Commented out …
|
|
|
@2171
|
7 years |
mulligan |
Finished the commutations
|
|
|
@2170
|
7 years |
sacerdot |
Splitted from AssemblyProofSplit?.ma
|
|
|
@2169
|
7 years |
tranquil |
corrected bug where definition of carry bit by MUL and DIV (which …
|
|
|
@2168
|
7 years |
sacerdot |
No more daemons left! All axioms are real axioms.
|
|
|
@2167
|
7 years |
sacerdot |
Only one daemon left.
|
|
|
@2166
|
7 years |
sacerdot |
1. less daemons
2. more easily usable statement
|
|
|
@2165
|
7 years |
sacerdot |
Only three daemons left.
|
|
|
@2164
|
7 years |
sacerdot |
More steady progress.
|
|
|
@2163
|
7 years |
sacerdot |
Steady progress.
|
|
|
@2162
|
7 years |
tranquil |
* yet another correction to joint
* added functions adding prologues …
|
|
|
@2161
|
7 years |
sacerdot |
Most of the old proof restored.
|
|
|
@2160
|
7 years |
mulligan |
Added a new scratch file Test.ma for working on lemmas that are needed …
|
|
|
@2159
|
7 years |
sacerdot |
One daemon left, back to original proof.
|
|
|
@2158
|
7 years |
sacerdot |
One less daemon.
|
|
|
@2157
|
7 years |
sacerdot |
Anticipating a proof needed before.
|
|
|
@2156
|
7 years |
sacerdot |
One more invariant, one less daemon.
|
|
|
@2155
|
7 years |
tranquil |
updates to blocks and RTLabs to RTL translation (which sidesteps …
|
|
|
@2154
|
7 years |
sacerdot |
Code shuffled around.
|
|
|
@2153
|
7 years |
boender |
- updated the proof some more
|
|
|
@2152
|
7 years |
boender |
- this should compile
|
|
|
@2151
|
7 years |
sacerdot |
1. Lemmas from AssemblyProof? anticipated to Assembly.ma
2. Jaap's …
|
|
|
@2150
|
7 years |
campbell |
Add labelling result to the correctness file.
|
|
|
@2149
|
7 years |
sacerdot |
Code shuffling to proper places.
|
|
|
@2148
|
7 years |
sacerdot |
1. specification made more user-friendly for AssemblyProof?
2. no more …
|
|
|
@2147
|
7 years |
sacerdot |
Theorem closed (up to one more lemma on overflow), but new proof …
|
|
|
@2146
|
7 years |
sacerdot |
1. specification fixed again
2. the proof in AssemblyProof? is now …
|
|
|
@2145
|
7 years |
campbell |
Cost labelling doesn't affect interaction.
|
|
|
@2144
|
7 years |
sacerdot |
1. Policy specification fixed
2. Proof of monotonicity of sigma
|
|
|
@2143
|
7 years |
mulligan |
Changes to the subaddressing mode elim functions moved into their …
|
|
|
@2142
|
7 years |
sacerdot |
Down to one daemon that requires one lemma (monotonicity of sigma).
|
|
|
@2141
|
7 years |
boender |
- committed working version
|
|
|
@2140
|
7 years |
mulligan |
Done the hardest cases in the main theorem. Just got a few daemons to …
|
|
|
@2139
|
7 years |
mulligan |
Changes to get the main lemma compiling again. Changes pushed into …
|
|
|
@2138
|
7 years |
sacerdot |
Invariant exported from proof of assembly_ok.
|
|
|
@2137
|
7 years |
sacerdot |
Bug fixed in specification.
|
|
|
@2136
|
7 years |
sacerdot |
…
|
|
|
@2135
|
7 years |
sacerdot |
One complex daemon changed to two simpler ones.
|
|
|
@2134
|
7 years |
campbell |
Split out behavioural equivalence spec for labelling.
|
|
|
@2133
|
7 years |
boender |
- moved does_not_occur_occur_absurd
|
|
|
@2132
|
7 years |
sacerdot |
Two more daemons closed, one left.
|
|
|
@2131
|
7 years |
sacerdot |
No more need for functional extensionality.
|
|
|
@2130
|
7 years |
sacerdot |
Proof repaired after Dominic's bug fix.
|
|
|
@2129
|
7 years |
mulligan |
Large changes from today trying to complete the main theorem. Again :(
|
|
|
@2128
|
7 years |
sacerdot |
Final shuffling around
|
|
|
@2127
|
7 years |
sacerdot |
Last daemon closed
|
|
|
@2126
|
7 years |
sacerdot |
Proof improved (for case 3) + new proof (for case 11)
|
|
|
@2125
|
7 years |
boender |
- some more displacement from Policy to Util
|
|
|
@2124
|
7 years |
sacerdot |
Much more shuffling around to proper places
|
|
|
@2123
|
7 years |
boender |
- moved is_well_labeled_p to Status and instruction_is_label to ASM
…
|
|
|
@2122
|
7 years |
sacerdot |
More stuff moved around in proper places
|
|
|
@2121
|
7 years |
sacerdot |
More functions moved to the places they belong to
|
|
|
@2120
|
7 years |
campbell |
Fix victim of alloc unfolding.
|
|
|
@2119
|
7 years |
sacerdot |
load_code_memory moved to Fetch.ma and proved correct w.r.t. next …
|
|
|
@2118
|
7 years |
campbell |
Labelling preserves behaviour.
|
|
|
@2117
|
7 years |
campbell |
Workaround for bug in Matita.
|
|
|
@2116
|
7 years |
sacerdot |
load_code_memory will be moved into Fetch.ma in the next commit.
This …
|
|
|
@2115
|
7 years |
sacerdot |
Old commented out code removed
|
|
|
@2114
|
7 years |
sacerdot |
Proof repaired
|
|
|
@2113
|
7 years |
sacerdot |
Proof by cases repaired; dead code removed.
|
|
|
@2112
|
7 years |
sacerdot |
WARNING: this commit may break some code.
- dead/useless code removed
|
|
|
@2111
|
7 years |
sacerdot |
Cleanup: lemmas/theorems/axioms moved to the right places.
|
|
|
@2110
|
7 years |
sacerdot |
…
|
|
|
@2109
|
7 years |
mulligan |
Finished porting the large, main lemma to the new notion of jump …
|
|
|
@2108
|
7 years |
mulligan |
Various axioms closed and others moved around. Uncommented main lemma …
|
|
|
@2107
|
7 years |
campbell |
Memory initialisation and program transformations.
|
|
|
@2106
|
7 years |
campbell |
Fix up a couple of proofs broken by recent changes.
|
|
|
@2105
|
7 years |
campbell |
Show some results about globalenvs and program transformations.
|
|
|
@2104
|
7 years |
campbell |
Fill in misc axiom.
|
|
|
@2103
|
7 years |
campbell |
Make transform_*program take a more general transformation to make …
|
|
|
@2102
|
7 years |
boender |
- some small changes
|
|
|
@2101
|
7 years |
boender |
- renamed medium to absolute jump
- revised proofs of policy, some …
|
|
|
@2100
|
7 years |
tranquil |
temporary solution to a bug where operations on spilled registers …
|
|
|
@2099
|
7 years |
boender |
- added reference to Intel dev manual
|
|
|
@2098
|
7 years |
boender |
- updates & changes
|
|
|
@2097
|
7 years |
mulligan |
Consistency change (institution)
|
|
|
@2096
|
7 years |
mulligan |
Changes to the English for Jaap, and some tidying up and making …
|
|
|
@2095
|
7 years |
mulligan |
Added reference to CompCert? and CompCertTSO.
|
|
|
@2094
|
7 years |
boender |
- oops
|
|
|
@2093
|
7 years |
boender |
- added reference to CompCertTSO
|
|
|
@2092
|
7 years |
mulligan |
Jaap noticed it's Randall Hyde not Holmes.
|
|
|
@2091
|
7 years |
boender |
- systematically changed 'jump' to 'branch'
|
|
|