# # ChangeLog for src/ASM/BitVectorTrie.ma # # Generated by Trac 1.2 # Dec 12, 2019, 7:41:35 PM Sun, 03 Mar 2013 13:03:58 GMT mckinna [2767] * src/ASM/ASM.ma (modified) * src/ASM/BitVectorTrie.ma (modified) * src/ASM/CodeMemory.ma (modified) * src/LIN/LINToASM.ma (modified) * src/common/AST.ma (modified) * src/common/CostLabel.ma (modified) * src/common/LabelledObjects.ma (modified) * src/compiler.ma (modified) * src/utilities/extranat.ma (modified) * src/utilities/option.ma (modified) WARNING: BIG commit, which pushes code_size_opt check into ... Thu, 07 Jun 2012 15:58:26 GMT boender [2028] * src/ASM/Arithmetic.ma (modified) * src/ASM/Assembly.ma (modified) * src/ASM/BitVectorTrie.ma (modified) - bugfix to Assembly (forgotten sigma) - added ... Wed, 09 May 2012 17:23:37 GMT boender [1931] * src/ASM/BitVectorTrie.ma (modified) * src/ASM/Policy.ma (modified) - added latest bvt alias - temporary "cases daemon" commit of new ... Tue, 20 Dec 2011 13:38:50 GMT boender [1632] * src/ASM/BitVectorTrie.ma (modified) - strengthened insert_lookup_opt Wed, 14 Dec 2011 13:44:42 GMT boender [1609] * src/ASM/Assembly.ma (modified) * src/ASM/BitVectorTrie.ma (modified) * src/common/Errors.ma (modified) - added alias to ASM/BitVectorTrie - removed double include from ... 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 Thu, 24 Nov 2011 11:26:30 GMT boender [1553] * src/ASM/BitVectorTrie.ma (modified) - added lookup_opt_lookup lemma Mon, 21 Nov 2011 16:51:20 GMT boender [1524] * src/ASM/BitVectorTrie.ma (modified) * src/ASM/Vector.ma (modified) - adapted files to new Matita syntax Mon, 21 Nov 2011 12:06:01 GMT sacerdot [1521] * src/ASM/BitVector.ma (modified) * src/ASM/BitVectorTrie.ma (modified) * src/ASM/Status.ma (modified) * src/Clight/CexecComplete.ma (modified) * src/Clight/CexecEquiv.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/RTLabs/RTLabsToRTL.ma (modified) * src/joint/TranslateUtils.ma (modified) * src/utilities/binary/Z.ma (modified) Syntax change in Matita: change what where => change where what. Fri, 18 Nov 2011 23:38:20 GMT sacerdot [1516] * src/ASM/BitVector.ma (modified) * src/ASM/BitVectorTrie.ma (modified) * src/ASM/BitVectorZ.ma (modified) * src/ASM/Status.ma (modified) * src/ASM/Util.ma (modified) * src/ASM/Vector.ma (modified) * src/Clight/Cexec.ma (modified) * src/Clight/CexecComplete.ma (modified) * src/Clight/CexecEquiv.ma (modified) * src/Clight/CexecSound.ma (modified) * src/Clight/casts.ma (modified) * src/Clight/toCminor.ma (modified) * src/Cminor/initialisation.ma (modified) * src/Cminor/semantics.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/RTL/RTLToERTL.ma (modified) * src/common/AST.ma (modified) * src/common/Events.ma (modified) * src/common/FrontEndOps.ma (modified) * src/common/GenMem.ma (modified) * src/common/Identifiers.ma (modified) * src/common/Integers.ma (modified) * src/common/Mem.ma (modified) * src/common/Pointers.ma (modified) * src/common/PositiveMap.ma (modified) * src/joint/BEValues.ma (modified) * src/joint/TranslateUtils.ma (modified) * src/utilities/extralib.ma (modified) * src/utilities/extranat.ma (modified) * src/utilities/lists.ma (modified) Ported to syntax of Matita 0.99.1. Wed, 02 Nov 2011 07:27:30 GMT boender [1479] * src/ASM/Assembly.ma (modified) * src/ASM/BitVectorTrie.ma (modified) - added insert_lookup_opt - assembly compiles now Mon, 31 Oct 2011 09:18:29 GMT mulligan [1474] * src/ASM/ASMCosts.ma (added) * src/ASM/BitVectorTrie.ma (modified) adding missing asmcosts file for computing the costs of an assembly ... Wed, 19 Oct 2011 17:17:04 GMT sacerdot [1424] * src/ASM/BitVectorTrie.ma (modified) * src/ERTL/ERTLToLTL.ma (modified) 1. fold function over BitVectorTries moved from ERTLToLTL to ... Mon, 17 Oct 2011 13:50:50 GMT boender [1393] * src/ASM/Assembly.ma (modified) * src/ASM/BitVectorTrie.ma (modified) * src/ASM/Status.ma (modified) - added invariant for policy trie to assembly - change (syntax only) ... Fri, 07 Oct 2011 10:26:39 GMT campbell [1316] * src (modified) * src/ASM (modified) * src/ASM/BitVectorTrie.ma (modified) * src/Clight/toCminor.ma (modified) * src/Cminor/initialisation.ma (modified) * src/Cminor/semantics.ma (modified) * src/Cminor/syntax.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/RTLabs/syntax.ma (modified) * src/common/Errors.ma (modified) * src/common/Identifiers.ma (modified) * src/utilities/deppair.ma (copied) * src/utilities/extralib.ma (modified) * src/utilities/lists.ma (modified) * src/utilities/option.ma (modified) * src/utilities/pair.ma (copied) Merge in id-lookup-branch to trunk. Mon, 18 Jul 2011 10:44:31 GMT boender [1074] * src/ASM/BitVectorTrie.ma (modified) - added lookup lemma Fri, 15 Jul 2011 10:56:48 GMT campbell [1070] * src/ASM/BitVectorTrie.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/RTLabs/syntax.ma (modified) * src/common/Identifiers.ma (modified) Show that entry and exit labels are in the RTLabs graph. Mon, 04 Jul 2011 13:31:18 GMT mulligan [1052] * src/ASM/BitVectorTrie.ma (modified) * src/RTLabs/RTLAbstoRTL.ma (modified) * src/common/AST.ma (modified) * src/utilities/HMap.ma (modified) removed offsets after reading cerco mailing list Mon, 27 Jun 2011 12:17:25 GMT boender [1044] * src/ASM/BitVectorTrie.ma (modified) - more fold/forall stuff Thu, 23 Jun 2011 15:40:43 GMT boender [1038] * src/ASM/BitVectorTrie.ma (modified) - some more BVT improvements Wed, 22 Jun 2011 14:03:33 GMT boender [1034] * src/ASM/BitVectorTrie.ma (modified) various & sundry fold/forall lemmas Mon, 20 Jun 2011 15:51:51 GMT boender [1006] * src/ASM/BitVectorTrie.ma (modified) - added fold + lemmas on fold Fri, 17 Jun 2011 11:30:01 GMT sacerdot [990] * src/ASM/BitVector.ma (modified) * src/ASM/BitVectorTrie.ma (modified) * src/ASM/FoldStuff.ma (modified) * src/ASM/Status.ma (modified) * src/ASM/Util.ma (modified) Do no longer use the daemon automatically :-) 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 ... Thu, 28 Apr 2011 15:36:33 GMT mulligan [782] * src/ASM/BitVectorTrie.ma (modified) * src/ASM/Util.ma (modified) * src/ERTL/ERTL.ma (modified) * src/RTL/RTL.ma (modified) * src/RTL/RTLtoERTL.ma (modified) * src/common/Identifiers.ma (modified) * src/utilities/RegisterSet.ma (modified) More work on rtl-ertl pass from today, plus resolved conflict. Thu, 28 Apr 2011 08:55:47 GMT campbell [779] * src/ASM/BitVectorTrie.ma (modified) * src/common/Identifiers.ma (modified) Add merging of tries and identifier sets (based on Dominic's earlier ... Tue, 19 Apr 2011 10:22:32 GMT campbell [761] * src/ASM/BitVectorTrie.ma (modified) * src/Cminor/semantics.ma (modified) * src/Cminor/test/sum-bad.ma (added) * src/RTLabs/RTLabs-sem.ma (modified) * src/common/Identifiers.ma (modified) * src/utilities/Coqlib.ma (modified) * src/utilities/option.ma (added) Enforce the use of declared identifiers/registers in Cminor/RTLabs. Wed, 30 Mar 2011 16:47:35 GMT campbell [726] * src/ASM/BitVector.ma (modified) * src/ASM/BitVectorTrie.ma (modified) * src/ASM/Vector.ma (modified) * src/Clight/AST.ma (modified) * src/Clight/CexecComplete.ma (modified) * src/Clight/test/duff.ma (modified) * src/Clight/test/factorial.ma (modified) * src/Clight/test/insertsort.ma (modified) * src/Clight/test/io.ma (modified) * src/Clight/test/io2.ma (modified) * src/Clight/test/search.ma (modified) * src/RTLabs/import.ma (modified) * src/common/Graphs.ma (modified) * src/common/Registers.ma (modified) Change identifiers to Words in Clight and RTLabs semantics. 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 12:28:33 GMT campbell [697] * src/ASM (modified) * src/ASM/Arithmetic.ma (modified) * src/ASM/BitVector.ma (modified) * src/ASM/BitVectorTrie.ma (modified) * src/ASM/BitVectorZ.ma (copied) * src/ASM/Char.ma (modified) * src/ASM/Util.ma (modified) * src/ASM/Vector.ma (modified) * src/common/Integers.ma (modified) * src/utilities/Coqlib.ma (modified) * src/utilities/binary/Z.ma (modified) * src/utilities/binary/positive.ma (modified) * src/utilities/extralib.ma (modified) * src/utilities/oldlib (moved) Merge Clight branch of vectors and friends. Start making stuff build. 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.