#
# ChangeLog for src/ASM/Assembly.ma
#
# Generated by Trac 1.2
# Apr 15, 2021, 8:28:50 PM

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) ...


Wed, 12 Oct 2011 19:11:07 GMT boender [1363]
	* src/ASM/Assembly.ma (modified)

	- done stuff with create_label_trie


Thu, 06 Oct 2011 16:09:18 GMT boender [1309]
	* src/ASM/Assembly.ma (modified)

	- refounded JEP


Fri, 05 Aug 2011 11:47:34 GMT boender [1103]
	* src/ASM/Assembly.ma (modified)

	- reverted to old policy


Tue, 05 Jul 2011 07:51:31 GMT boender [1054]
	* src/ASM/Assembly.ma (modified)

	- proven policy safe


Fri, 24 Jun 2011 14:54:33 GMT sacerdot [1040]
	* src/ASM/Assembly.ma (modified)

	Bug fixed in assembly.


Tue, 21 Jun 2011 00:02:37 GMT sacerdot [1014]
	* src/ASM/Assembly.ma (modified)
	* src/ASM/AssemblyProof.ma (modified)
	* src/ASM/FoldStuff.ma (modified)
	* src/ASM/StatusProofs.ma (added)

	The main theorem is completely broken (again).


Mon, 20 Jun 2011 15:05:23 GMT sacerdot [998]
	* src/ASM/Assembly.ma (modified)
	* src/ASM/AssemblyProof.ma (modified)
	* src/ASM/Util.ma (modified)
	* src/ASM/Vector.ma (modified)

	Half repaired, half broken. Most functions no longer return option ...


Fri, 17 Jun 2011 16:28:49 GMT sacerdot [993]
	* src/ASM/Assembly.ma (modified)
	* src/ASM/AssemblyProof.ma (modified)
	* src/ASM/Status.ma (modified)
	* src/ASM/Util.ma (modified)

	More Russell everywhere; getting closer to the goal.


Fri, 17 Jun 2011 08:28:19 GMT sacerdot [989]
	* src/ASM/Assembly.ma (modified)
	* src/ASM/AssemblyProof.ma (modified)

	Type of build_maps strengthened.


Thu, 16 Jun 2011 16:08:12 GMT sacerdot [987]
	* src/ASM/Assembly.ma (modified)
	* src/ASM/AssemblyProof.ma (modified)

	Real parameterization over the policy.


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, 16 Jun 2011 12:39:53 GMT boender [982]
	* src/ASM/Assembly.ma (modified)
	* src/ASM/AssemblyProof.ma (modified)

	- this should work (see previous commit)


Fri, 10 Jun 2011 16:36:55 GMT sacerdot [938]
	* src/ASM/Assembly.ma (modified)
	* src/ASM/AssemblyProof.ma (modified)

	...


Thu, 09 Jun 2011 13:38:47 GMT mulligan [922]
	* src/ASM/Assembly.ma (modified)

	changes to get assemblyproof to compile


Thu, 09 Jun 2011 12:52:38 GMT boender [920]
	* src/ASM/Assembly.ma (modified)

	- corrected mov instruction


Thu, 09 Jun 2011 09:10:16 GMT boender [914]
	* src/ASM/Assembly.ma (modified)

	- complete.


Thu, 09 Jun 2011 08:50:05 GMT boender [913]
	* src/ASM/Assembly.ma (modified)

	- temporary commit s.t. Assembly compiles


Wed, 08 Jun 2011 16:15:26 GMT boender [907]
	* src/ASM/Assembly.ma (modified)
	* src/ASM/Util.ma (modified)

	- added quadruples to Util
	- start of implementation of new jump ...


Wed, 25 May 2011 16:10:04 GMT mulligan [846]
	* src/ASM/Assembly.ma (modified)
	* src/ASM/AssemblyProof.ma (modified)

	changes


Wed, 25 May 2011 14:26:17 GMT sacerdot [844]
	* src/ASM/Assembly.ma (modified)

	Useless code removed.


Wed, 25 May 2011 13:57:03 GMT sacerdot [842]
	* src/ASM/Assembly.ma (modified)

	Bug fixed.


Wed, 25 May 2011 11:57:55 GMT sacerdot [840]
	* src/ASM/Assembly.ma (modified)
	* src/ASM/AssemblyProof.ma (modified)

	sigma defined


Wed, 25 May 2011 09:49:10 GMT mulligan [837]
	* src/ASM/Assembly.ma (modified)

	changes complete


Wed, 25 May 2011 09:43:42 GMT mulligan [836]
	* src/ASM/Assembly.ma (modified)

	changes to assembly functions


Tue, 24 May 2011 21:19:53 GMT sacerdot [833]
	* src/ASM/Assembly.ma (modified)
	* src/ASM/AssemblyProof.ma (modified)

	Bug fixed to make the file compile.
	But the type of the assembly ...


Tue, 24 May 2011 16:40:13 GMT mulligan [832]
	* src/ASM/ASM.ma (modified)
	* src/ASM/Assembly.ma (modified)
	* src/ASM/AssemblyProof.ma (modified)

	work from today


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


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 ...


Tue, 29 Mar 2011 16:17:57 GMT mulligan [719]
	* src/ASM/Assembly.ma (added)

	Added missing assembly file ported to matita.