

@2301

8 years 
mulligan 
Trying to get the big proof working again



@2285

8 years 
sacerdot 
1. duplicated code erased
2. POP case finished up to lemmas on …



@2284

8 years 
sacerdot 
PUSH finished



@2283

8 years 
mulligan 
Work from today.



@2282

8 years 
sacerdot 
PUSH case almost finished



@2279

8 years 
sacerdot 
1. Bug fixed in the semantics of PUSH (no indirection performed)
2. …



@2278

8 years 
mulligan 
Half of JC case complete



@2276

8 years 
sacerdot 
…



@2273

8 years 
sacerdot 
1. lemmas moved from all files to Test.ma
2. most of the lemmas in …



@2272

8 years 
mulligan 
Changed proof strategy for main lemma after noticed that the current …



@2265

8 years 
sacerdot 
Commented out code removed.



@2262

9 years 
mulligan 
Changes from today.



@2261

9 years 
mulligan 
Resolved conflict



@2260

9 years 
sacerdot 
Now we use the efficient lookup_address.



@2259

9 years 
mulligan 
For Claudio



@2258

9 years 
sacerdot 
1. lemma generalized
2. automation replaced with expansion to make …



@2257

9 years 
mulligan 
Daemon in SETB case closed.



@2256

9 years 
mulligan 
MOV and MOVX cases complete



@2247

9 years 
mulligan 
Work on the MOV instruction from today and bug fixes in set_arg_1.



@2216

9 years 
mulligan 
More work on the big lemma. Nearly there now.



@2212

9 years 
mulligan 
More work on the INC case



@2210

9 years 
mulligan 
XOR case completely finished.



@2209

9 years 
mulligan 
Closed major daemons in the supporting lemmas of the main lemma.



@2207

9 years 
mulligan 
Improvements and corrections to the main lemma proof in …



@2204

9 years 
sacerdot 
Shuffling around, suggestions, improvements.



@2198

9 years 
mulligan 
Work from today.



@2187

9 years 
mulligan 
Work from today on the big proof.



@2183

9 years 
mulligan 
More progress on main lemma proof.



@2181

9 years 
mulligan 
Work from the last week on the new formulation of the main lemma for …



@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 …



@2160

9 years 
mulligan 
Added a new scratch file Test.ma for working on lemmas that are needed …



@2143

9 years 
mulligan 
Changes to the subaddressing mode elim functions moved into their …



@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 …



@2131

9 years 
sacerdot 
No more need for functional extensionality.



@2129

9 years 
mulligan 
Large changes from today trying to complete the main theorem. Again :(



@2124

9 years 
sacerdot 
Much more shuffling around to proper places



@2122

9 years 
sacerdot 
More stuff moved around in proper places



@2121

9 years 
sacerdot 
More functions moved to the places they belong to



@2114

9 years 
sacerdot 
Proof repaired



@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 …



@2047

9 years 
mulligan 
Big bugs in policy calculations found. Waiting for Jaap's commit.



@2039

9 years 
sacerdot 
New, better interface for subaddressing_mode_elim



@2032

9 years 
sacerdot 
!! BEWARE: major commit !!
1) [affects everybody]
split for …



@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 …



@2020

9 years 
mulligan 
CJNE case complete, DJNZ case almost complete



@2018

9 years 
mulligan 
CJNE case a complete mess.



@2017

9 years 
mulligan 
Large swathes of proof of main lemma added.



@1985

9 years 
mulligan 
A single `false' case for unconditional jumps completed.



@1984

9 years 
mulligan 
Most proof obligations closed in main_lemma apart from those of the …



@1983

9 years 
mulligan 
Changes to simplify the simpler cases of the main_lemma.



@1979

9 years 
sacerdot 
Very very very tricky lemma closed. A dreadful mix of JM equality …



@1978

9 years 
sacerdot 
Two more cases completed.



@1977

9 years 
sacerdot 
Unblocked: let ... as hides two different terms, one that uses Leibniz …



@1975

9 years 
mulligan 
Work from today on closing main_thm.



@1971

9 years 
sacerdot 
1. Interpret.ma:
we need to prove
\sigma (execute_preinstruction …



@1969

9 years 
sacerdot 
Some more progress, but now we must prove something on a Russell …



@1967

9 years 
sacerdot 
Mov case completed.



@1966

9 years 
mulligan 
Progress made on main_thm proof: trying to find a pattern to use …



@1963

9 years 
sacerdot 
More progress in restoring the original proof.



@1958

9 years 
mulligan 
Marked divergence in StatusProofs?.ma



@1952

9 years 
sacerdot 
AssemblyProof? splitted.
