

@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

8 years 
mulligan 
Changes from today.



@2261

8 years 
mulligan 
Resolved conflict



@2260

8 years 
sacerdot 
Now we use the efficient lookup_address.



@2259

8 years 
mulligan 
For Claudio



@2258

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



@2257

8 years 
mulligan 
Daemon in SETB case closed.



@2256

8 years 
mulligan 
MOV and MOVX cases complete



@2247

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



@2216

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



@2212

8 years 
mulligan 
More work on the INC case



@2210

8 years 
mulligan 
XOR case completely finished.



@2209

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



@2207

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



@2204

8 years 
sacerdot 
Shuffling around, suggestions, improvements.



@2198

8 years 
mulligan 
Work from today.



@2187

8 years 
mulligan 
Work from today on the big proof.



@2183

8 years 
mulligan 
More progress on main lemma proof.



@2181

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



@2173

8 years 
mulligan 
MUL case of main lemma nearly complete (subject to two small holes …



@2172

8 years 
mulligan 
Moved new versions of get_ / set_arg_* into Status.ma. Commented out …



@2160

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



@2143

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



@2140

8 years 
mulligan 
Done the hardest cases in the main theorem. Just got a few daemons to …



@2139

8 years 
mulligan 
Changes to get the main lemma compiling again. Changes pushed into …



@2131

8 years 
sacerdot 
No more need for functional extensionality.



@2129

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



@2124

8 years 
sacerdot 
Much more shuffling around to proper places



@2122

8 years 
sacerdot 
More stuff moved around in proper places



@2121

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



@2114

8 years 
sacerdot 
Proof repaired



@2109

8 years 
mulligan 
Finished porting the large, main lemma to the new notion of jump …



@2108

8 years 
mulligan 
Various axioms closed and others moved around. Uncommented main lemma …



@2047

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



@2039

8 years 
sacerdot 
New, better interface for subaddressing_mode_elim



@2032

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



@2026

8 years 
mulligan 
Added a new file to house the main theorem as the type checking time …



@2024

8 years 
mulligan 
Updated AssemblyProof? to fix mismatch in definition of lookup_labels …



@2023

8 years 
mulligan 
Closed main lemma modulo closing trivial subgoals about commutations …



@2020

8 years 
mulligan 
CJNE case complete, DJNZ case almost complete



@2018

8 years 
mulligan 
CJNE case a complete mess.



@2017

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



@1985

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



@1984

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



@1983

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



@1979

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



@1978

8 years 
sacerdot 
Two more cases completed.



@1977

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



@1975

8 years 
mulligan 
Work from today on closing main_thm.



@1971

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



@1969

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



@1967

8 years 
sacerdot 
Mov case completed.



@1966

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



@1963

8 years 
sacerdot 
More progress in restoring the original proof.



@1958

8 years 
mulligan 
Marked divergence in StatusProofs?.ma



@1952

8 years 
sacerdot 
AssemblyProof? splitted.
