|
|
@2281
|
7 years |
sacerdot |
…
|
|
|
@2280
|
7 years |
sacerdot |
Proof repaired.
|
|
|
@2279
|
7 years |
sacerdot |
1. Bug fixed in the semantics of PUSH (no indirection performed)
2. …
|
|
|
@2278
|
7 years |
mulligan |
Half of JC case complete
|
|
|
@2277
|
7 years |
tranquil |
* replaced incorrect use of subvector_with
|
|
|
@2276
|
7 years |
sacerdot |
…
|
|
|
@2275
|
7 years |
tranquil |
* moved around some code (I8051.ma does not depend on ByteValues?.ma …
|
|
|
@2274
|
7 years |
sacerdot |
Dead code commented out and code out of place moved to Test.ma.
|
|
|
@2273
|
7 years |
sacerdot |
1. lemmas moved from all files to Test.ma
2. most of the lemmas in …
|
|
|
@2272
|
7 years |
mulligan |
Changed proof strategy for main lemma after noticed that the current …
|
|
|
@2271
|
7 years |
garnier |
Proof of correction for the semantics of expressions under memory …
|
|
|
@2270
|
7 years |
mulligan |
Bug spotted and fixed in write_at_stack_pointer
|
|
|
@2269
|
7 years |
sacerdot |
Proof completely repaired up to …
|
|
|
@2268
|
7 years |
mulligan |
Bug spotted in instruction_size (lookup_datalabels cannot just be a …
|
|
|
@2267
|
7 years |
sacerdot |
Call is now proved using the new strategy.
|
|
|
@2266
|
7 years |
sacerdot |
All daemons closed in Jmp case.
|
|
|
@2265
|
7 years |
sacerdot |
Commented out code removed.
|
|
|
@2264
|
7 years |
sacerdot |
1) Major change: we now always use the efficient way of resolving …
|
|
|
@2263
|
7 years |
garnier |
Finished proving semantics preservation under memory injections for …
|
|
|
@2262
|
7 years |
mulligan |
Changes from today.
|
|
|
@2261
|
7 years |
mulligan |
Resolved conflict
|
|
|
@2260
|
7 years |
sacerdot |
Now we use the efficient lookup_address.
|
|
|
@2259
|
7 years |
mulligan |
For Claudio
|
|
|
@2258
|
7 years |
sacerdot |
1. lemma generalized
2. automation replaced with expansion to make …
|
|
|
@2257
|
7 years |
mulligan |
Daemon in SETB case closed.
|
|
|
@2256
|
7 years |
mulligan |
MOV and MOVX cases complete
|
|
|
@2255
|
7 years |
garnier |
Had to modify the definition of memory injections to prove that …
|
|
|
@2254
|
7 years |
campbell |
Fix up invariants in Cminor semantics.
|
|
|
@2253
|
7 years |
campbell |
Cminor to RTLabs is now a total function.
|
|
|
@2252
|
7 years |
campbell |
Use the return statement invariant. Restructure the invariants for …
|
|
|
@2251
|
7 years |
campbell |
Add new invariant to Cminor that return typs should be respected.
|
|
|
@2250
|
7 years |
campbell |
Tidy up Clight to Cminor pass a bit.
|
|
|
@2249
|
7 years |
campbell |
Tweak Cminor invariant to be slightly more readable/extendable.
|
|
|
@2248
|
7 years |
sacerdot |
Final changes. All daemons removed, but the real one (open goal).
|
|
|
@2247
|
7 years |
mulligan |
Work on the MOV instruction from today and bug fixes in set_arg_1.
|
|
|
@2246
|
7 years |
sacerdot |
Final technical lemma streamlined. Maybe it can be streamlined even more.
|
|
|
@2245
|
7 years |
sacerdot |
Temporary commit to have a backtracking point. Yes, I know this breaks …
|
|
|
@2244
|
7 years |
sacerdot |
Technical lemma used.
|
|
|
@2243
|
7 years |
sacerdot |
One more lemma streamlined, one to go + one to be completed.
|
|
|
@2242
|
7 years |
sacerdot |
jump_expansion_step3 streamlined
|
|
|
@2241
|
7 years |
boender |
- merged changes by Claudio
|
|
|
@2240
|
7 years |
sacerdot |
All "interesting" technical lemmas singled out, proofs to be uncommented.
|
|
|
@2239
|
7 years |
sacerdot |
One more lemma polished.
|
|
|
@2238
|
7 years |
sacerdot |
Taken out lemma integrated.
|
|
|
@2237
|
7 years |
sacerdot |
Even shorter version.
|
|
|
@2236
|
7 years |
sacerdot |
One subproof made shorter.
|
|
|
@2235
|
7 years |
sacerdot |
Towards smaller proofs.
|
|
|
@2234
|
7 years |
garnier |
Progress on proving semantics preservation under memory injections.
|
|
|
@2233
|
7 years |
tranquil |
* completed update of ERTL semantics
* some minor changes in joint …
|
|
|
@2232
|
7 years |
campbell |
Remove unused block structure in Cminor.
|
|
|
@2231
|
7 years |
garnier |
Various tiny lemmas used in at least two files in the fornt-end.
|
|
|
@2230
|
7 years |
sacerdot |
Glue proof maximally simplified or sort of.
|
|
|
@2229
|
7 years |
sacerdot |
More cleaning up, ready for more aggressive factorization.
|
|
|
@2228
|
7 years |
sacerdot |
Further proof reduction.
|
|
|
@2227
|
7 years |
garnier |
* New version of the switch removal algorithm, described at the top of …
|
|
|
@2226
|
7 years |
campbell |
Whole program proof.
|
|
|
@2225
|
7 years |
sacerdot |
Minor and major improvements everywhere, shortened proofs.
|
|
|
@2224
|
7 years |
campbell |
Proper whole program result in RTLabs/Traces
|
|
|
@2223
|
7 years |
campbell |
Simplify RTLabs structure traces proofs by getting rid of wrong …
|
|
|
@2222
|
7 years |
sacerdot |
More robust to possible future changes to the "in match" semantics …
|
|
|
@2221
|
7 years |
boender |
- removed cases daemon from PolicyFront?
|
|
|
@2220
|
7 years |
sacerdot |
Some minor speed up and daemon-uncommenting.
|
|
|
@2219
|
7 years |
campbell |
Speed up cast simplification proof checking a bit.
|
|
|
@2218
|
7 years |
campbell |
Separate out cost properties required of RTLabs programs from the …
|
|
|
@2217
|
7 years |
tranquil |
* collapsed step_params, unserialized_params, funct_params and …
|
|
|
@2216
|
7 years |
mulligan |
More work on the big lemma. Nearly there now.
|
|
|
@2215
|
7 years |
sacerdot |
Some speed up.
|
|
|
@2214
|
7 years |
tranquil |
* changed order of parameters of joint_internal_function and genv in …
|
|
|
@2213
|
7 years |
boender |
- removed one cases daemon
|
|
|
@2212
|
7 years |
mulligan |
More work on the INC case
|
|
|
@2211
|
7 years |
boender |
- finished proof of sigma specification
- added some stuff to Util, as …
|
|
|
@2210
|
7 years |
mulligan |
XOR case completely finished.
|
|
|
@2209
|
7 years |
mulligan |
Closed major daemons in the supporting lemmas of the main lemma.
|
|
|
@2208
|
7 years |
tranquil |
* moving some code around
* changed immediates to hold beval in …
|
|
|
@2207
|
7 years |
mulligan |
Improvements and corrections to the main lemma proof in …
|
|
|
@2206
|
7 years |
campbell |
Add note about cost maps to simulation definition.
|
|
|
@2205
|
7 years |
campbell |
Get correctness.ma type checking again.
|
|
|
@2204
|
7 years |
sacerdot |
Shuffling around, suggestions, improvements.
|
|
|
@2203
|
7 years |
campbell |
A general result about simulations of executions.
|
|
|
@2202
|
7 years |
campbell |
Start defining equivalent executions.
|
|
|
@2201
|
7 years |
campbell |
Forgotten comment update.
|
|
|
@2200
|
7 years |
tranquil |
* updated joint semantics: generation of linear and graph semantics
* …
|
|
|
@2199
|
7 years |
sacerdot |
No longer used lemma containing the last daemon removed.
The proof is …
|
|
|
@2198
|
7 years |
mulligan |
Work from today.
|
|
|
@2197
|
7 years |
sacerdot |
Main lemmas all closed.
|
|
|
@2196
|
7 years |
sacerdot |
Speed up using patterns.
|
|
|
@2195
|
7 years |
mulligan |
Got AssemblyProof?.ma compiling again using daemons.
|
|
|
@2194
|
7 years |
sacerdot |
1. monotone moved to Assembly
2. some easier daemons, one shows an …
|
|
|
@2193
|
7 years |
sacerdot |
Statement clean-up.
|
|
|
@2192
|
7 years |
sacerdot |
Shuffling around.
|
|
|
@2191
|
7 years |
sacerdot |
Only one daemon left.
|
|
|
@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
|
|
|