# # ChangeLog for src/ASM/Fetch.ma # # Generated by Trac 1.2 # Mar 5, 2021, 9:22:22 AM 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 ... Wed, 27 Jun 2012 14:23:54 GMT sacerdot [2124] * src/ASM/ASM.ma (modified) * src/ASM/Arithmetic.ma (modified) * src/ASM/AssemblyProof.ma (modified) * src/ASM/AssemblyProofSplit.ma (modified) * src/ASM/BitVector.ma (modified) * src/ASM/Fetch.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/StatusProofs.ma (modified) * src/ASM/Util.ma (modified) * src/ASM/Vector.ma (modified) Much more shuffling around to proper places Wed, 27 Jun 2012 10:09:25 GMT sacerdot [2119] * src/ASM/AssemblyProof.ma (modified) * src/ASM/Fetch.ma (modified) * src/ASM/Status.ma (modified) load_code_memory moved to Fetch.ma and proved correct w.r.t. next ... Wed, 16 May 2012 19:12:23 GMT sacerdot [1961] * src/ASM/Fetch.ma (modified) No more interaction required. Mon, 14 May 2012 22:01:30 GMT sacerdot [1946] * src/ASM/ASMCostsSplit.ma (modified) * src/ASM/Arithmetic.ma (modified) * src/ASM/Assembly.ma (modified) * src/ASM/AssemblyProof.ma (modified) * src/ASM/Fetch.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/Status.ma (modified) * src/ASM/UtilBranch.ma (modified) \snd half_add => add everywhere Mon, 14 May 2012 14:33:20 GMT mulligan [1941] * src/ASM/AssemblyProof.ma (modified) * src/ASM/Fetch.ma (modified) Changes to the AssemblyProof with a few more (large) axioms closed. Thu, 12 Jan 2012 17:16:50 GMT mulligan [1642] * src/ASM/ASMCosts.ma (modified) * src/ASM/Fetch.ma (modified) finished big proof in all but two cases Wed, 14 Dec 2011 10:52:28 GMT mulligan [1604] * src/ASM/Fetch.ma (modified) for jaap Tue, 13 Dec 2011 15:23:40 GMT mulligan [1602] * src/ASM/Fetch.ma (modified) * src/ASM/Util.ma (modified) giving up on fetch proofs for time being Tue, 13 Dec 2011 12:41:08 GMT sacerdot [1600] * src/ASM/BitVectorTrie.ma (modified) * src/ASM/Erase.ma (modified) * src/ASM/Fetch.ma (modified) * src/ASM/FoldStuff.ma (modified) * src/ASM/I8051.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/JMCoercions.ma (deleted) * src/ASM/Status.ma (modified) * src/ASM/Util.ma (modified) * src/utilities/Compare.ma (deleted) * src/utilities/Coqlib.ma (modified) * src/utilities/deppair.ma (deleted) * src/utilities/lists.ma (deleted) * src/utilities/option.ma (deleted) * src/utilities/sigma.ma (deleted) utilities and ASM ported to the new standard library Mon, 12 Dec 2011 16:53:36 GMT mulligan [1598] * src/ASM/Fetch.ma (modified) * src/ASM/FoldStuff.ma (modified) * src/ASM/Util.ma (modified) * src/ASM/Vector.ma (modified) * src/common/Errors.ma (modified) * src/utilities/pair.ma (modified) changes over the last couple of days Mon, 12 Dec 2011 08:51:21 GMT mulligan [1597] * src/ASM/ASMCosts.ma (modified) * src/ASM/Fetch.ma (modified) fixed fetch for jaap Tue, 06 Dec 2011 16:24:45 GMT mulligan [1591] * src/ASM/ASMCosts.ma (modified) * src/ASM/Fetch.ma (modified) work from today Thu, 24 Nov 2011 16:19:30 GMT boender [1555] * src/ASM/Assembly.ma (modified) * src/ASM/Fetch.ma (modified) * src/common/PositiveMap.ma (modified) - changes to assembly - added lookup to PositiveMap - lightly ... Wed, 08 Jun 2011 08:30:27 GMT sacerdot [895] * src/ASM/Fetch.ma (modified) Fetch function fixed: alla AJMPS were ACALL (and the other way ... Fri, 03 Jun 2011 14:03:00 GMT sacerdot [876] * src/ASM/AssemblyProof.ma (modified) * src/ASM/Fetch.ma (modified) ... Mon, 30 May 2011 11:44:45 GMT sacerdot [856] * src/ASM/AssemblyProof.ma (modified) * src/ASM/Fetch.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/Util.ma (modified) 1. if_then_else is now a notation for match with (to allow Russell to ... Fri, 20 May 2011 16:09:00 GMT mulligan [820] * src/ASM/ASM.ma (modified) * src/ASM/Assembly.ma (modified) * src/ASM/Fetch.ma (modified) * src/ASM/Interpret.ma (modified) changes to get the semantics of pseudoassembly working Mon, 28 Mar 2011 15:40:51 GMT mulligan [712] * src/ASM/Arithmetic.ma (modified) * src/ASM/Fetch.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/Util.ma (modified) Changes to get things to typecheck. Wed, 23 Mar 2011 01:24:11 GMT sacerdot [706] * src/ASM/Fetch.ma (modified) Fixed (reference to basics/pairs was dandling). Fri, 18 Mar 2011 12:47:53 GMT mulligan [698] * src/ASM/ASM.ma (modified) * src/ASM/Arithmetic.ma (modified) * src/ASM/BitVector.ma (modified) * src/ASM/BitVectorTrie.ma (modified) * src/ASM/Fetch.ma (modified) * src/ASM/I8051.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/Status.ma (modified) * src/ASM/String.ma (modified) * src/ASM/Util.ma (modified) * src/ASM/Vector.ma (modified) * src/LIN/LIN.ma (modified) * src/LIN/LINToASM.ma (modified) * src/common/AST.ma (modified) * src/common/CostLabel.ma (modified) * src/utilities/BitVectorTrieSet.ma (modified) * src/utilities/StringTools.ma (modified) Commit with changes to files to get our files to typecheck. Fri, 18 Mar 2011 10:34:13 GMT mulligan [690] * src/ASM/ASM.ma (copied) * src/ASM/Arithmetic.ma (copied) * src/ASM/BitVector.ma (copied) * src/ASM/BitVectorTrie.ma (copied) * src/ASM/Char.ma (copied) * src/ASM/Fetch.ma (copied) * src/ASM/Interpret.ma (copied) * src/ASM/Status.ma (copied) * src/ASM/String.ma (copied) * src/ASM/Util.ma (copied) * src/ASM/Vector.ma (copied) * src/ASM/new-matita-development (deleted) Moved new matita files into correct place. Fri, 18 Mar 2011 10:31:32 GMT mulligan [688] * Deliverables/D4.1/Demo-March-2011 (deleted) * Deliverables/D4.2-4.3/LIN/LinToAsm.ma (deleted) * src (added) * src/ASM (moved) * src/LIN (moved) * src/LIN/LIN.ma (copied) Fixed local conflicts. Restructured svn repository.