#
# ChangeLog for src/ASM/AssemblyProof.ma
#
# Generated by Trac 1.2
# Dec 11, 2019, 11:55:53 AM

Mon, 21 May 2012 15:48:43 GMT mulligan [1975]
	* src/ASM/AssemblyProof.ma (modified)
	* src/ASM/AssemblyProofSplit.ma (modified)

	Work from today on closing main_thm.


Mon, 21 May 2012 08:33:26 GMT mulligan [1972]
	* src/ASM/AssemblyProof.ma (modified)

	Simple lemma with strangely complex proof complete.


Thu, 17 May 2012 15:45:21 GMT mulligan [1966]
	* src/ASM/AssemblyProof.ma (modified)
	* src/ASM/AssemblyProofSplit.ma (modified)

	Progress made on main_thm proof: trying to find a pattern to use ...


Wed, 16 May 2012 13:53:46 GMT mulligan [1957]
	* src/ASM/AssemblyProof.ma (modified)

	Stitching proofs back together after slight change in statement of ...


Wed, 16 May 2012 13:03:52 GMT mulligan [1955]
	* src/ASM/Arithmetic.ma (modified)
	* src/ASM/AssemblyProof.ma (modified)

	Completed proof of snd_assembly_1_pseudoinstruction_ok, modulo some ...


Wed, 16 May 2012 08:29:22 GMT mulligan [1953]
	* src/ASM/AssemblyProof.ma (modified)

	Commit to avoid conflicts.


Tue, 15 May 2012 23:29:17 GMT sacerdot [1952]
	* src/ASM/AssemblyProof.ma (modified)
	* src/ASM/AssemblyProofSplit.ma (added)

	AssemblyProof splitted.


Tue, 15 May 2012 09:13:14 GMT mulligan [1948]
	* src/ASM/Assembly.ma (modified)
	* src/ASM/AssemblyProof.ma (modified)
	* src/ASM/Interpret.ma (modified)

	Weakened statements of ASM/Assembly.ma and ASM/AssemblyProof.ma, so ...


Mon, 14 May 2012 22:30:13 GMT sacerdot [1947]
	* src/ASM/AssemblyProof.ma (modified)

	Failure of automation/demod investigated a little bit.


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 20:40:38 GMT sacerdot [1945]
	* src/ASM/AssemblyProof.ma (modified)

	All proof statements repaired.


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.


Mon, 14 May 2012 08:37:08 GMT mulligan [1939]
	* src/ASM/AbstractStatus.ma (added)
	* src/ASM/AssemblyProof.ma (modified)
	* src/ASM/Interpret.ma (modified)
	* src/common/StructuredTraces.ma (modified)

	Changes to get things to compile and to avoid the dependency ...


Fri, 11 May 2012 12:38:55 GMT mulligan [1936]
	* src/ASM/AssemblyProof.ma (modified)

	Some holes filled in AssemblyProof.ma.


Mon, 30 Jan 2012 10:41:08 GMT boender [1668]
	* src/ASM/Assembly.ma (modified)
	* src/ASM/AssemblyProof.ma (modified)

	- split build_maps into build_maps and build_maps_ok
	- work with CSC ...


Sun, 29 Jan 2012 21:25:57 GMT sacerdot [1667]
	* src/ASM/Assembly.ma (modified)
	* src/ASM/AssemblyProof.ma (modified)

	Main lemma for the main_thm of AssemblyProof re-declared as an axiom ...


Sat, 28 Jan 2012 12:42:15 GMT sacerdot [1666]
	* src/ASM/AssemblyProof.ma (modified)
	* src/ASM/Interpret.ma (modified)
	* src/ASM/Status.ma (modified)
	* src/ASM/StatusProofs.ma (modified)

	PreStatus datatype change: the code_memory field is not a left ...


Wed, 18 Jan 2012 17:17:37 GMT boender [1649]
	* src/ASM/Assembly.ma (modified)
	* src/ASM/AssemblyProof.ma (modified)

	- changes to Assembly for integration with Policy and easier use of ...


Wed, 14 Dec 2011 16:57:08 GMT sacerdot [1616]
	* src/ASM/AssemblyProof.ma (modified)

	Partially ported to new Matita syntax.
	Because of some changes in ...


Wed, 14 Dec 2011 12:50:23 GMT sacerdot [1607]
	* src/ASM/Assembly.ma (modified)
	* src/ASM/AssemblyProof.ma (modified)

	Porting to new library.


Wed, 02 Nov 2011 13:46:59 GMT sacerdot [1484]
	* src/ASM/AssemblyProof.ma (modified)

	...


Mon, 10 Oct 2011 10:53:43 GMT sacerdot [1333]
	* src/ASM/AssemblyProof.ma (modified)

	Avoid using the name of the construction of jmeq.


Wed, 29 Jun 2011 08:47:39 GMT mulligan [1045]
	* src/ASM/AssemblyProof.ma (modified)
	* src/RTLabs/RTLAbstoRTL.ma (modified)
	* src/RTLabs/syntax.ma (modified)
	* src/common/AST.ma (modified)

	resolved conflict in rtlabs


Sat, 25 Jun 2011 00:32:53 GMT sacerdot [1043]
	* src/ASM/AssemblyProof.ma (modified)

	Axiom commented out.


Sat, 25 Jun 2011 00:30:07 GMT sacerdot [1042]
	* src/ASM/AssemblyProof.ma (modified)

	Dead code removed.
	Slow code uncommented.


Fri, 24 Jun 2011 15:05:21 GMT sacerdot [1041]
	* src/ASM/AssemblyProof.ma (modified)

	fetch_assembly is still working after bug fix


Fri, 24 Jun 2011 12:11:08 GMT sacerdot [1039]
	* src/ASM/AssemblyProof.ma (modified)

	fetch_assembly_pseudo2 repaired from dependent type madness


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.


Wed, 22 Jun 2011 21:38:55 GMT sacerdot [1036]
	* src/ASM/AssemblyProof.ma (modified)

	...


Wed, 22 Jun 2011 21:06:43 GMT sacerdot [1035]
	* src/ASM/AssemblyProof.ma (modified)

	Main theorem (broken because of dependent types) almost restored.


Tue, 21 Jun 2011 02:27:06 GMT sacerdot [1015]
	* src/ASM/AssemblyProof.ma (modified)

	One intermediate version of main_thm0 close to be repaired.


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:42:02 GMT mulligan [994]
	* src/ASM/AssemblyProof.ma (modified)

	small changes


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 16:05:05 GMT mulligan [992]
	* src/ASM/AssemblyProof.ma (modified)
	* src/ASM/CPP2011/cpp-2011.tex (modified)

	a few more axioms closed


Fri, 17 Jun 2011 15:17:43 GMT mulligan [991]
	* src/ASM/AssemblyProof.ma (modified)

	loads of axioms related to equality on instructions closed


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 21:27:48 GMT sacerdot [988]
	* src/ASM/AssemblyProof.ma (modified)

	Proof restored.


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)


Thu, 16 Jun 2011 12:26:47 GMT sacerdot [979]
	* src/ASM/AssemblyProof.ma (modified)

	...


Thu, 16 Jun 2011 10:12:59 GMT sacerdot [977]
	* src/ASM/AssemblyProof.ma (modified)

	#$%@#$@#$


Thu, 16 Jun 2011 09:34:26 GMT sacerdot [975]
	* src/ASM/AssemblyProof.ma (modified)

	...


Wed, 15 Jun 2011 22:22:57 GMT sacerdot [972]
	* src/ASM/AssemblyProof.ma (modified)

	...


Wed, 15 Jun 2011 22:07:20 GMT sacerdot [971]
	* src/ASM/AssemblyProof.ma (modified)

	...


Wed, 15 Jun 2011 12:22:59 GMT sacerdot [959]
	* src/ASM/AssemblyProof.ma (modified)

	...


Tue, 14 Jun 2011 23:35:27 GMT sacerdot [951]
	* src/ASM/AssemblyProof.ma (modified)

	long call case completed


Tue, 14 Jun 2011 15:46:15 GMT sacerdot [950]
	* src/ASM/AssemblyProof.ma (modified)

	Horrible sub-proof finished :-)


Mon, 13 Jun 2011 16:42:14 GMT mulligan [949]
	* src/ASM/Arithmetic.ma (modified)
	* src/ASM/AssemblyProof.ma (modified)
	* src/ASM/Status.ma (modified)

	resolved conflict, work from today


Mon, 13 Jun 2011 13:28:26 GMT sacerdot [948]
	* src/ASM/AssemblyProof.ma (modified)

	Some progress on the Call case.


Mon, 13 Jun 2011 09:37:46 GMT sacerdot [946]
	* src/ASM/AssemblyProof.ma (modified)

	Jmp case repaired after addition of MAP hypothesis.


Mon, 13 Jun 2011 09:15:31 GMT mulligan [945]
	* src/ASM/AssemblyProof.ma (modified)

	more small changes to proof of main thrm


Mon, 13 Jun 2011 08:54:58 GMT mulligan [944]
	* src/ASM/AssemblyProof.ma (modified)

	split definition


Sun, 12 Jun 2011 23:46:41 GMT sacerdot [943]
	* src/ASM/AssemblyProof.ma (modified)

	...


Sun, 12 Jun 2011 23:14:38 GMT sacerdot [942]
	* src/ASM/AssemblyProof.ma (modified)

	New invariant for the main theorem.
	The new invariant is much more ...


Sat, 11 Jun 2011 21:37:20 GMT sacerdot [941]
	* src/ASM/AssemblyProof.ma (modified)

	Jmp case finished up to arithmetical properties.


Fri, 10 Jun 2011 16:49:00 GMT mulligan [940]
	* src/ASM/AssemblyProof.ma (modified)

	more changes to inc case of main theorem


Fri, 10 Jun 2011 16:42:41 GMT sacerdot [939]
	* src/ASM/AssemblyProof.ma (modified)

	Long Jmp case finished.


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

	...


Fri, 10 Jun 2011 14:48:45 GMT mulligan [937]
	* src/ASM/AssemblyProof.ma (modified)

	resolved conflict in assembly_proof, more lemmas added


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


Fri, 10 Jun 2011 11:15:11 GMT mulligan [935]
	* src/ASM/AssemblyProof.ma (modified)
	* src/ASM/Status.ma (modified)

	changes to status and assembly proof


Fri, 10 Jun 2011 01:25:09 GMT sacerdot [934]
	* src/ASM/AssemblyProof.ma (modified)

	...


Fri, 10 Jun 2011 01:20:34 GMT sacerdot [933]
	* src/ASM/AssemblyProof.ma (modified)

	New proof strategy.


Fri, 10 Jun 2011 01:10:27 GMT sacerdot [932]
	* src/ASM/AssemblyProof.ma (modified)

	...


Fri, 10 Jun 2011 00:53:49 GMT sacerdot [931]
	* src/ASM/AssemblyProof.ma (modified)

	...


Fri, 10 Jun 2011 00:19:09 GMT sacerdot [930]
	* src/ASM/AssemblyProof.ma (modified)

	Comment, Cost, ADD, ADC cases done.


Thu, 09 Jun 2011 16:40:44 GMT mulligan [929]
	* src/ASM/AssemblyProof.ma (modified)

	added ticks_of function


Thu, 09 Jun 2011 15:06:26 GMT sacerdot [926]
	* src/ASM/AssemblyProof.ma (modified)

	Main theorem false because of ticks :-(


Thu, 09 Jun 2011 14:42:50 GMT sacerdot [925]
	* src/ASM/AssemblyProof.ma (modified)

	...


Thu, 09 Jun 2011 14:14:54 GMT sacerdot [924]
	* src/ASM/AssemblyProof.ma (modified)

	...


Thu, 09 Jun 2011 13:51:07 GMT sacerdot [923]
	* src/ASM/AssemblyProof.ma (modified)

	Main theorem made nice... but unprovable at the moment.


Thu, 09 Jun 2011 13:21:27 GMT mulligan [921]
	* src/ASM/AssemblyProof.ma (modified)

	resolved conflict, fixed bugs


Thu, 09 Jun 2011 12:15:32 GMT sacerdot [919]
	* src/ASM/AssemblyProof.ma (modified)

	Back to a readable statement.


Thu, 09 Jun 2011 09:56:49 GMT sacerdot [916]
	* src/ASM/AssemblyProof.ma (modified)

	Fix for jump_expansion_policy.


Thu, 09 Jun 2011 09:30:59 GMT mulligan [915]
	* src/ASM/AssemblyProof.ma (modified)

	finished changes to fetch_assembly_pseudo2


Thu, 09 Jun 2011 08:45:16 GMT sacerdot [912]
	* src/ASM/AssemblyProof.ma (modified)

	Readable main theorem statement.


Thu, 09 Jun 2011 08:38:21 GMT sacerdot [911]
	* src/ASM/AssemblyProof.ma (modified)
	* src/ASM/Status.ma (modified)

	Type of set_code_memory generalized.


Wed, 08 Jun 2011 23:27:57 GMT sacerdot [909]
	* src/ASM/AssemblyProof.ma (modified)

	Back to the main theorem.


Wed, 08 Jun 2011 23:22:15 GMT sacerdot [908]
	* src/ASM/AssemblyProof.ma (modified)

	Next big lemma proved!


Wed, 08 Jun 2011 16:12:15 GMT sacerdot [906]
	* src/ASM/AssemblyProof.ma (modified)

	...


Wed, 08 Jun 2011 16:07:20 GMT mulligan [905]
	* src/ASM/AssemblyProof.ma (modified)

	work from today


Wed, 08 Jun 2011 15:53:32 GMT sacerdot [904]
	* src/ASM/AssemblyProof.ma (modified)

	Cleanup.


Wed, 08 Jun 2011 15:53:18 GMT sacerdot [903]
	* src/ASM/AssemblyProof.ma (modified)

	Statement of new main lemma (as axiom).


Wed, 08 Jun 2011 15:28:12 GMT sacerdot [902]
	* src/ASM/AssemblyProof.ma (modified)

	Cleanup.


Wed, 08 Jun 2011 15:27:35 GMT sacerdot [901]
	* src/ASM/AssemblyProof.ma (modified)

	Second main lemma proved.


Wed, 08 Jun 2011 08:59:01 GMT sacerdot [897]
	* src/ASM/AssemblyProof.ma (modified)

	Proof completed, fetch and assembly are mutual inverses.


Wed, 08 Jun 2011 08:38:31 GMT sacerdot [896]
	* src/ASM/AssemblyProof.ma (modified)

	Proof finished (but ugly) :-)


Wed, 08 Jun 2011 08:09:06 GMT sacerdot [894]
	* src/ASM/AssemblyProof.ma (modified)

	Bug more evident.


Tue, 07 Jun 2011 15:32:30 GMT sacerdot [893]
	* src/ASM/AssemblyProof.ma (modified)

	Cleanup.


Tue, 07 Jun 2011 15:28:57 GMT sacerdot [892]
	* src/ASM/AssemblyProof.ma (modified)

	First fundamental lemma almost finished.


Tue, 07 Jun 2011 00:56:39 GMT sacerdot [890]
	* src/ASM/AssemblyProof.ma (modified)

	Better statement, begin of uniform proof.


Mon, 06 Jun 2011 21:07:24 GMT sacerdot [889]
	* src/ASM/AssemblyProof.ma (modified)
	* src/ASM/Vector.ma (modified)
	* src/common/Integers.ma (modified)

	Minor changes because of the new, weaker (but much faster) delift.


Sun, 05 Jun 2011 00:04:22 GMT sacerdot [885]
	* src/ASM/AssemblyProof.ma (modified)

	Proof almost finished, but rewritings are extremely slow.


Sat, 04 Jun 2011 16:16:08 GMT sacerdot [884]
	* src/ASM/AssemblyProof.ma (modified)

	...


Fri, 03 Jun 2011 16:36:00 GMT sacerdot [883]
	* src/ASM/AssemblyProof.ma (modified)

	Merged done well.


Fri, 03 Jun 2011 14:11:24 GMT mulligan [877]
	* src/ASM/AssemblyProof.ma (added)

	work from today