# # ChangeLog for src/ASM/Interpret.ma # # Generated by Trac 1.2 # Jan 21, 2020, 8:53:10 PM Wed, 23 Nov 2011 15:03:38 GMT mulligan [1540] * src/ASM/Interpret.ma (modified) changes to proof in interrupt.ma Wed, 23 Nov 2011 11:28:51 GMT mulligan [1538] * src/ASM/Interpret.ma (modified) changes to execute_1_0 proof Wed, 23 Nov 2011 09:36:34 GMT mulligan [1534] * src/ASM/CostsProof.ma (modified) * src/ASM/Interpret.ma (modified) committing my changes to interpret to prevent any further conflicts Tue, 22 Nov 2011 18:24:00 GMT sacerdot [1533] * src/ASM/Interpret.ma (modified) Proof of execute_1 with Russell completed (up to some daemon used ... Tue, 22 Nov 2011 10:50:15 GMT sacerdot [1527] * src/ASM/Interpret.ma (modified) More on Russell. Tue, 22 Nov 2011 09:43:47 GMT sacerdot [1526] * src/ASM/Interpret.ma (modified) * src/ASM/Status.ma (modified) Using Russell to prove some properties. Mon, 21 Nov 2011 14:49:04 GMT mulligan [1522] * src/ASM/ASM.ma (modified) * src/ASM/CostsProof.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/Status.ma (modified) * src/LIN/LINToASM.ma (modified) changes to preamble and lin to asm pass, resolved conflict in interpret Mon, 21 Nov 2011 11:10:57 GMT campbell [1519] * src/ASM/Interpret.ma (modified) * src/ASM/StatusProofs.ma (modified) More syntax updates. Fri, 18 Nov 2011 12:03:14 GMT campbell [1515] * src/ASM/ASM.ma (modified) * src/ASM/Erase.ma (modified) * src/ASM/I8051.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/Interpret2.ma (modified) * src/ASM/Status.ma (modified) * src/ASM/StatusProofs.ma (modified) * src/Clight/TypeComparison.ma (modified) * src/Clight/fresh.ma (modified) * src/Clight/label.ma (modified) * src/Clight/test/insertsort.test.ma (modified) * src/Clight/toCminor.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/ERTL/ERTLToLTL.ma (modified) * src/LIN/LINToASM.ma (modified) * src/LTL/LTLToLIN.ma (modified) * src/RTLabs/RTLabsToRTL.ma (modified) * src/common/Graphs.ma (modified) * src/common/Identifiers.ma (modified) * src/common/PositiveMap.ma (added) * src/common/PreIdentifiers.ma (modified) * src/joint/Erasure.ma (modified) * src/joint/SemanticUtils.ma (modified) * src/joint/TranslateUtils.ma (modified) * src/utilities/binary/positive.ma (modified) * src/utilities/extralib.ma (modified) * src/utilities/extranat.ma (modified) Add type of maps on positive binary numbers, and use them for ... Thu, 17 Nov 2011 16:41:08 GMT mulligan [1514] * src/ASM/CostsProof.ma (modified) * src/ASM/Interpret.ma (modified) changes from today. matita keeps dieing Wed, 16 Nov 2011 16:35:24 GMT mulligan [1511] * src/ASM/CostsProof.ma (modified) * src/ASM/Interpret.ma (modified) proofs, added, changes to execute_1_0 function therefore required to ... Mon, 07 Nov 2011 09:56:13 GMT mulligan [1494] * src/ASM/Interpret.ma (modified) * src/ASM/WellLabeled.ma (modified) changes to get everything compiling again Thu, 23 Jun 2011 00:56:20 GMT sacerdot [1037] * src/ASM/AssemblyProof.ma (modified) * src/ASM/Interpret.ma (modified) Main theorem: comments are working again. Thu, 16 Jun 2011 14:50:23 GMT sacerdot [985] * src/ASM/ASM.ma (modified) * src/ASM/Assembly.ma (modified) * src/ASM/AssemblyProof.ma (modified) * src/ASM/BitVector.ma (modified) * src/ASM/BitVectorTrie.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/Status.ma (modified) * src/ASM/Util.ma (modified) * src/common/AST.ma (modified) 1) Major refactoring: proofs moved where they should be. 2) New ... Fri, 10 Jun 2011 14:20:47 GMT sacerdot [936] * src/ASM/AssemblyProof.ma (modified) * src/ASM/Interpret.ma (modified) Ticks are now handled correctly everywhere and the main proof takes ... Thu, 09 Jun 2011 16:07:29 GMT sacerdot [928] * src/ASM/Interpret.ma (modified) Technical splitting. Thu, 09 Jun 2011 08:36:35 GMT mulligan [910] * src/ASM/Interpret.ma (modified) removed bug in execute_1_pseudoinstruction Tue, 31 May 2011 09:45:21 GMT sacerdot [865] * src/ASM/AssemblyProof.ma (modified) * src/ASM/Interpret.ma (modified) Renaming. 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 ... Wed, 25 May 2011 13:57:42 GMT sacerdot [843] * src/ASM/Interpret.ma (modified) * src/ASM/Status.ma (modified) Function moved from Interpret to Status. Tue, 24 May 2011 11:26:43 GMT sacerdot [827] * src/ASM/AssemblyProof.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/Status.ma (modified) The preamble is now part of the PseudoStatus. Mon, 23 May 2011 16:12:51 GMT mulligan [825] * src/ASM/Assembly.ma (modified) * src/ASM/AssemblyProof.ma (modified) * src/ASM/Interpret.ma (modified) lots of refactoring, finally got something to prove Mon, 23 May 2011 14:22:13 GMT mulligan [822] * src/ASM/Interpret.ma (modified) removed all axioms Mon, 23 May 2011 13:23:17 GMT mulligan [821] * src/ASM/Interpret.ma (modified) * src/ASM/Status.ma (modified) changes to introduce pseudostatus 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, 18 Apr 2011 10:30:53 GMT mulligan [757] * src/ASM/ASM.ma (modified) * src/ASM/Assembly.ma (modified) * src/ASM/I8051.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/Status.ma (modified) * src/ERTL/ERTLToLTL.ma (modified) * src/LIN/JointLTLLIN.ma (modified) * src/LIN/LIN.ma (modified) * src/LIN/LINToASM.ma (modified) * src/LTL/LTL.ma (modified) * src/LTL/LTLToLIN.ma (modified) * src/common/AST.ma (modified) * src/common/CostLabel.ma (modified) * src/common/Identifiers.ma (modified) * src/common/Registers.ma (modified) Lots more fixing to get both front and backends using same ... 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. 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.