# # ChangeLog for src/ASM/AssemblyProofSplitSplit.ma # # Generated by Trac 1.2 # Apr 20, 2021, 12:25:13 PM Mon, 30 Jul 2012 16:33:11 GMT mulligan [2278] * src/ASM/AssemblyProofSplit.ma (modified) * src/ASM/AssemblyProofSplitSplit.ma (modified) Half of JC case complete Sun, 29 Jul 2012 22:46:19 GMT sacerdot [2273] * src/ASM/AssemblyProofSplit.ma (modified) * src/ASM/AssemblyProofSplitSplit.ma (modified) * src/ASM/PolicyFront.ma (modified) * src/ASM/Test.ma (modified) 1. lemmas moved from all files to Test.ma 2. most of the lemmas in ... Thu, 26 Jul 2012 13:29:15 GMT sacerdot [2269] * src/ASM/AssemblyProofSplitSplit.ma (modified) Proof completely repaired up to ... Thu, 26 Jul 2012 10:05:58 GMT sacerdot [2267] * src/ASM/AssemblyProofSplitSplit.ma (modified) Call is now proved using the new strategy. Thu, 26 Jul 2012 08:43:55 GMT sacerdot [2266] * src/ASM/AssemblyProofSplitSplit.ma (modified) All daemons closed in Jmp case. Wed, 25 Jul 2012 22:38:42 GMT sacerdot [2264] * src/ASM/Assembly.ma (modified) * src/ASM/AssemblyProofSplitSplit.ma (modified) * src/ASM/Fetch.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/Policy.ma (modified) * src/ASM/PolicyFront.ma (modified) * src/ASM/PolicyStep.ma (modified) * src/ASM/Status.ma (modified) 1) Major change: we now always use the efficient way of resolving ... Thu, 28 Jun 2012 16:47:26 GMT mulligan [2140] * src/ASM/AssemblyProofSplit.ma (modified) * src/ASM/AssemblyProofSplitSplit.ma (modified) Done the hardest cases in the main theorem. Just got a few daemons ... Thu, 28 Jun 2012 15:42:22 GMT mulligan [2139] * src/ASM/ASM.ma (modified) * src/ASM/AssemblyProofSplit.ma (modified) * src/ASM/AssemblyProofSplitSplit.ma (modified) * src/ASM/Status.ma (modified) Changes to get the main lemma compiling again. Changes pushed into ... Wed, 27 Jun 2012 22:55:05 GMT sacerdot [2131] * src/ASM/AssemblyProof.ma (modified) * src/ASM/AssemblyProofSplit.ma (modified) * src/ASM/AssemblyProofSplitSplit.ma (modified) No more need for functional extensionality. Wed, 27 Jun 2012 17:14:32 GMT mulligan [2129] * src/ASM/AssemblyProof.ma (modified) * src/ASM/AssemblyProofSplit.ma (modified) * src/ASM/AssemblyProofSplitSplit.ma (modified) * src/ASM/Interpret.ma (modified) * src/common/StructuredTraces.ma (modified) Large changes from today trying to complete the main theorem. Again :( Wed, 27 Jun 2012 14:59:10 GMT sacerdot [2127] * src/ASM/AssemblyProofSplitSplit.ma (modified) Last daemon closed Wed, 27 Jun 2012 14:04:14 GMT boender [2123] * src/ASM/ASM.ma (modified) * src/ASM/AssemblyProofSplitSplit.ma (modified) * src/ASM/Status.ma (modified) * src/ASM/Util.ma (modified) - moved is_well_labeled_p to Status and instruction_is_label to ASM ... Wed, 27 Jun 2012 13:36:54 GMT sacerdot [2122] * src/ASM/AssemblyProof.ma (modified) * src/ASM/AssemblyProofSplit.ma (modified) * src/ASM/AssemblyProofSplitSplit.ma (modified) * src/ASM/BitVector.ma (modified) * src/ASM/Vector.ma (modified) More stuff moved around in proper places Tue, 26 Jun 2012 14:05:15 GMT sacerdot [2110] * src/ASM/Assembly.ma (modified) * src/ASM/AssemblyProof.ma (modified) * src/ASM/AssemblyProofSplitSplit.ma (modified) ... Wed, 13 Jun 2012 15:00:35 GMT sacerdot [2062] * src/ASM/AssemblyProofSplitSplit.ma (modified) * src/ASM/Interpret.ma (modified) Everything repaired (broken because of new proof obligation for fetch). Tue, 12 Jun 2012 15:49:02 GMT mulligan [2051] * src/ASM/Assembly.ma (modified) * src/ASM/AssemblyProofSplitSplit.ma (modified) * src/ASM/Interpret.ma (modified) Finished the Jmp case in the main theorem. Tue, 12 Jun 2012 12:18:16 GMT mulligan [2047] * src/ASM/Assembly.ma (modified) * src/ASM/AssemblyProofSplit.ma (modified) * src/ASM/AssemblyProofSplitSplit.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/PolicyFront.ma (modified) Big bugs in policy calculations found. Waiting for Jaap's commit. Thu, 07 Jun 2012 15:53:27 GMT mulligan [2027] * src/ASM/AssemblyProofSplitSplit.ma (modified) Got the main lemma to apply in the proof of main theorem again and ... Thu, 07 Jun 2012 14:37:42 GMT mulligan [2026] * src/ASM/AssemblyProofSplit.ma (modified) * src/ASM/AssemblyProofSplitSplit.ma (added) Added a new file to house the main theorem as the type checking time ...