|
|
@2242
|
9 years |
sacerdot |
jump_expansion_step3 streamlined
|
|
|
@2241
|
9 years |
boender |
- merged changes by Claudio
|
|
|
@2240
|
9 years |
sacerdot |
All "interesting" technical lemmas singled out, proofs to be uncommented.
|
|
|
@2239
|
9 years |
sacerdot |
One more lemma polished.
|
|
|
@2238
|
9 years |
sacerdot |
Taken out lemma integrated.
|
|
|
@2237
|
9 years |
sacerdot |
Even shorter version.
|
|
|
@2236
|
9 years |
sacerdot |
One subproof made shorter.
|
|
|
@2235
|
9 years |
sacerdot |
Towards smaller proofs.
|
|
|
@2234
|
9 years |
garnier |
Progress on proving semantics preservation under memory injections.
|
|
|
@2233
|
9 years |
tranquil |
* completed update of ERTL semantics
* some minor changes in joint …
|
|
|
@2232
|
9 years |
campbell |
Remove unused block structure in Cminor.
|
|
|
@2231
|
9 years |
garnier |
Various tiny lemmas used in at least two files in the fornt-end.
|
|
|
@2230
|
9 years |
sacerdot |
Glue proof maximally simplified or sort of.
|
|
|
@2229
|
9 years |
sacerdot |
More cleaning up, ready for more aggressive factorization.
|
|
|
@2228
|
9 years |
sacerdot |
Further proof reduction.
|
|
|
@2227
|
9 years |
garnier |
* New version of the switch removal algorithm, described at the top of …
|
|
|
@2226
|
9 years |
campbell |
Whole program proof.
|
|
|
@2225
|
9 years |
sacerdot |
Minor and major improvements everywhere, shortened proofs.
|
|
|
@2224
|
9 years |
campbell |
Proper whole program result in RTLabs/Traces
|
|
|
@2223
|
9 years |
campbell |
Simplify RTLabs structure traces proofs by getting rid of wrong …
|
|
|
@2222
|
9 years |
sacerdot |
More robust to possible future changes to the "in match" semantics …
|
|
|
@2221
|
9 years |
boender |
- removed cases daemon from PolicyFront?
|
|
|
@2220
|
9 years |
sacerdot |
Some minor speed up and daemon-uncommenting.
|
|
|
@2219
|
9 years |
campbell |
Speed up cast simplification proof checking a bit.
|
|
|
@2218
|
9 years |
campbell |
Separate out cost properties required of RTLabs programs from the …
|
|
|
@2217
|
9 years |
tranquil |
* collapsed step_params, unserialized_params, funct_params and …
|
|
|
@2216
|
9 years |
mulligan |
More work on the big lemma. Nearly there now.
|
|
|
@2215
|
9 years |
sacerdot |
Some speed up.
|
|
|
@2214
|
9 years |
tranquil |
* changed order of parameters of joint_internal_function and genv in …
|
|
|
@2213
|
9 years |
boender |
- removed one cases daemon
|
|
|
@2212
|
9 years |
mulligan |
More work on the INC case
|
|
|
@2211
|
9 years |
boender |
- finished proof of sigma specification
- added some stuff to Util, as …
|
|
|
@2210
|
9 years |
mulligan |
XOR case completely finished.
|
|
|
@2209
|
9 years |
mulligan |
Closed major daemons in the supporting lemmas of the main lemma.
|
|
|
@2208
|
9 years |
tranquil |
* moving some code around
* changed immediates to hold beval in …
|
|
|
@2207
|
9 years |
mulligan |
Improvements and corrections to the main lemma proof in …
|
|
|
@2206
|
9 years |
campbell |
Add note about cost maps to simulation definition.
|
|
|
@2205
|
9 years |
campbell |
Get correctness.ma type checking again.
|
|
|
@2204
|
9 years |
sacerdot |
Shuffling around, suggestions, improvements.
|
|
|
@2203
|
9 years |
campbell |
A general result about simulations of executions.
|
|
|
@2202
|
9 years |
campbell |
Start defining equivalent executions.
|
|
|
@2201
|
9 years |
campbell |
Forgotten comment update.
|
|
|
@2200
|
9 years |
tranquil |
* updated joint semantics: generation of linear and graph semantics
* …
|
|
|
@2199
|
9 years |
sacerdot |
No longer used lemma containing the last daemon removed.
The proof is …
|
|
|
@2198
|
9 years |
mulligan |
Work from today.
|
|
|
@2197
|
9 years |
sacerdot |
Main lemmas all closed.
|
|
|
@2196
|
9 years |
sacerdot |
Speed up using patterns.
|
|
|
@2195
|
9 years |
mulligan |
Got AssemblyProof?.ma compiling again using daemons.
|
|
|
@2194
|
9 years |
sacerdot |
1. monotone moved to Assembly
2. some easier daemons, one shows an …
|
|
|
@2193
|
9 years |
sacerdot |
Statement clean-up.
|
|
|
@2192
|
9 years |
sacerdot |
Shuffling around.
|
|
|
@2191
|
9 years |
sacerdot |
Only one daemon left.
|
|
|
@2190
|
9 years |
sacerdot |
Two daemons left.
|
|
|
@2189
|
9 years |
sacerdot |
Proof very close to completion.
|
|
|
@2188
|
9 years |
sacerdot |
1. Policy specification generalized
2. All invariants but the main one …
|
|
|
@2187
|
9 years |
mulligan |
Work from today on the big proof.
|
|
|
@2186
|
9 years |
tranquil |
updated joint semantics
|
|
|
@2185
|
9 years |
campbell |
Use bitvectors for offsets.
|
|
|
@2184
|
9 years |
campbell |
Minor fix ups.
|
|
|
@2183
|
9 years |
mulligan |
More progress on main lemma proof.
|
|
|
@2182
|
9 years |
tranquil |
updated linearisation pass
|
|
|
@2181
|
9 years |
mulligan |
Work from the last week on the new formulation of the main lemma for …
|
|
|
@2180
|
9 years |
campbell |
Fix off-by-one error in GenMem?.ma.
|
|
|
@2179
|
9 years |
campbell |
Dependent pair monad binding notation.
|
|
|
@2178
|
9 years |
campbell |
Shift some notation into utilities.
|
|
|
@2177
|
9 years |
campbell |
Tidy up multiplication.
|
|
|
@2176
|
9 years |
campbell |
Remove memory spaces other than XData and Code; simplify pointers as a …
|
|
|
@2175
|
9 years |
tranquil |
corrected small bug
|
|
|
@2174
|
9 years |
tranquil |
* factored out script for (axiomatised) fixpoint computation
* ERTL → …
|
|
|
@2173
|
9 years |
mulligan |
MUL case of main lemma nearly complete (subject to two small holes …
|
|
|
@2172
|
9 years |
mulligan |
Moved new versions of get_ / set_arg_* into Status.ma. Commented out …
|
|
|
@2171
|
9 years |
mulligan |
Finished the commutations
|
|
|
@2170
|
9 years |
sacerdot |
Splitted from AssemblyProofSplit?.ma
|
|
|
@2168
|
9 years |
sacerdot |
No more daemons left! All axioms are real axioms.
|
|
|
@2167
|
9 years |
sacerdot |
Only one daemon left.
|
|
|
@2166
|
9 years |
sacerdot |
1. less daemons
2. more easily usable statement
|
|
|
@2165
|
9 years |
sacerdot |
Only three daemons left.
|
|
|
@2164
|
9 years |
sacerdot |
More steady progress.
|
|
|
@2163
|
9 years |
sacerdot |
Steady progress.
|
|
|
@2162
|
9 years |
tranquil |
* yet another correction to joint
* added functions adding prologues …
|
|
|
@2161
|
9 years |
sacerdot |
Most of the old proof restored.
|
|
|
@2160
|
9 years |
mulligan |
Added a new scratch file Test.ma for working on lemmas that are needed …
|
|
|
@2159
|
9 years |
sacerdot |
One daemon left, back to original proof.
|
|
|
@2158
|
9 years |
sacerdot |
One less daemon.
|
|
|
@2157
|
9 years |
sacerdot |
Anticipating a proof needed before.
|
|
|
@2156
|
9 years |
sacerdot |
One more invariant, one less daemon.
|
|
|
@2155
|
9 years |
tranquil |
updates to blocks and RTLabs to RTL translation (which sidesteps …
|
|
|
@2154
|
9 years |
sacerdot |
Code shuffled around.
|
|
|
@2153
|
9 years |
boender |
- updated the proof some more
|
|
|
@2152
|
9 years |
boender |
- this should compile
|
|
|
@2151
|
9 years |
sacerdot |
1. Lemmas from AssemblyProof? anticipated to Assembly.ma
2. Jaap's …
|
|
|
@2150
|
9 years |
campbell |
Add labelling result to the correctness file.
|
|
|
@2149
|
9 years |
sacerdot |
Code shuffling to proper places.
|
|
|
@2148
|
9 years |
sacerdot |
1. specification made more user-friendly for AssemblyProof?
2. no more …
|
|
|
@2147
|
9 years |
sacerdot |
Theorem closed (up to one more lemma on overflow), but new proof …
|
|
|
@2146
|
9 years |
sacerdot |
1. specification fixed again
2. the proof in AssemblyProof? is now …
|
|
|
@2145
|
9 years |
campbell |
Cost labelling doesn't affect interaction.
|
|
|
@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).
|
|
|