# # ChangeLog for src/ASM/Policy.ma # # Generated by Trac 1.2 # Dec 11, 2019, 6:42:22 PM Sun, 03 Mar 2013 22:46:51 GMT sacerdot [2771] * src/ASM/Policy.ma (modified) Some speed up in Policy.ma. Sat, 02 Mar 2013 10:42:16 GMT sacerdot [2763] * src/ASM/ASM.ma (modified) * src/ASM/Policy.ma (modified) * src/LIN/LINToASM.ma (modified) * src/compiler.ma (modified) All daemons in compiler.ma closed (i.e. proof obligations added to ... Sat, 02 Mar 2013 01:37:43 GMT sacerdot [2762] * src/ASM/Policy.ma (modified) * src/compiler.ma (modified) All repaired up to compiler.ma. Note: one daemon is left for one ... Wed, 27 Feb 2013 21:46:05 GMT sacerdot [2745] * src/ASM/Policy.ma (modified) * src/compiler.ma (modified) 1. Complexity of policy computation lowered from O(n^2) to O(n) 2. ... Fri, 22 Feb 2013 13:12:24 GMT sacerdot [2700] * src/ASM/Arithmetic.ma (modified) * src/ASM/Policy.ma (modified) * src/ASM/Util.ma (modified) * src/ERTLptr/ERTLptrToLTL.ma (modified) * src/ERTLptr/Interference.ma (modified) * src/ERTLptr/liveness.ma (modified) * src/compiler.ma (modified) * src/utilities/fixpoints.ma (modified) 1. exponential function dropped in favour of standard library 2. ... Fri, 08 Feb 2013 12:45:22 GMT sacerdot [2653] * src/ASM/Policy.ma (modified) * src/ASM/PolicyFront.ma (modified) ... Fri, 08 Feb 2013 10:49:55 GMT sacerdot [2652] * src/ASM/Policy.ma (modified) * src/ASM/PolicyFront.ma (modified) * src/ASM/PolicyStep.ma (modified) String type changed definition. Mon, 03 Sep 2012 10:42:47 GMT boender [2318] * src/ASM/Policy.ma (modified) * src/ASM/PolicyFront.ma (modified) - now it compiles Mon, 03 Sep 2012 09:36:43 GMT boender [2317] * src/ASM/Policy.ma (modified) * src/ASM/PolicyStep.ma (modified) - small changes to make things compile Mon, 03 Sep 2012 07:03:24 GMT boender [2316] * src/ASM/ASM.ma (modified) * src/ASM/Assembly.ma (modified) * src/ASM/Policy.ma (modified) * src/ASM/PolicyFront.ma (modified) * src/ASM/PolicyStep.ma (modified) * src/ASM/Status.ma (modified) - committed temporary version: true version has to wait until I ... 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 ... Mon, 23 Jul 2012 08:35:43 GMT sacerdot [2230] * src/ASM/Policy.ma (modified) Glue proof maximally simplified or sort of. Fri, 20 Jul 2012 19:38:04 GMT sacerdot [2229] * src/ASM/Policy.ma (modified) More cleaning up, ready for more aggressive factorization. Fri, 20 Jul 2012 19:10:21 GMT sacerdot [2228] * src/ASM/Policy.ma (modified) Further proof reduction. Fri, 20 Jul 2012 16:15:40 GMT sacerdot [2225] * src/ASM/Policy.ma (modified) * src/ASM/PolicyFront.ma (modified) * src/ASM/PolicyStep.ma (modified) Minor and major improvements everywhere, shortened proofs. Wed, 18 Jul 2012 13:57:09 GMT boender [2211] * src/ASM/Policy.ma (modified) * src/ASM/PolicyFront.ma (modified) * src/ASM/PolicyStep.ma (modified) * src/ASM/Util.ma (modified) - finished proof of sigma specification - added some stuff to Util, ... Wed, 04 Jul 2012 13:38:52 GMT boender [2153] * src/ASM/Policy.ma (modified) - updated the proof some more Wed, 04 Jul 2012 11:23:00 GMT boender [2152] * src/ASM/Policy.ma (modified) * src/ASM/PolicyFront.ma (modified) * src/ASM/PolicyStep.ma (modified) - this should compile Thu, 28 Jun 2012 18:08:58 GMT boender [2141] * src/ASM/Policy.ma (modified) * src/ASM/PolicyFront.ma (modified) * src/ASM/PolicyStep.ma (modified) - committed working version Tue, 19 Jun 2012 14:43:50 GMT boender [2101] * src/ASM/Assembly.ma (modified) * src/ASM/Policy.ma (modified) * src/ASM/PolicyFront.ma (modified) * src/ASM/PolicyStep.ma (modified) * src/utilities/extralib.ma (modified) - renamed medium to absolute jump - revised proofs of policy, some ... Thu, 14 Jun 2012 09:44:46 GMT sacerdot [2078] * src/ASM/Assembly.ma (modified) * src/ASM/AssemblyProof.ma (modified) * src/ASM/Policy.ma (modified) sigma_policy_specification has been 1) strengthened 2) made nicer ... Wed, 13 Jun 2012 13:44:20 GMT boender [2059] * src/ASM/Policy.ma (modified) * src/ASM/PolicyFront.ma (modified) * src/ASM/PolicyStep.ma (modified) - updated Policy to work better Wed, 13 Jun 2012 10:11:21 GMT sacerdot [2055] * src/ASM/Assembly.ma (modified) * src/ASM/CostsProof.ma (modified) * src/ASM/Policy.ma (modified) * src/ASM/Status.ma (modified) * src/ASM/Util.ma (modified) Warning: this commit adds an hypothesis that breaks all of assembly ... Fri, 08 Jun 2012 15:16:22 GMT boender [2034] * src/ASM/Policy.ma (modified) * src/ASM/PolicyFront.ma (added) * src/ASM/PolicyStep.ma (added) - split Policy into three separate files for ease (and indeed ... Fri, 08 Jun 2012 14:32:03 GMT sacerdot [2032] * src/ASM/ASM.ma (modified) * src/ASM/Arithmetic.ma (modified) * src/ASM/Assembly.ma (modified) * src/ASM/AssemblyProof.ma (modified) * src/ASM/AssemblyProofSplit.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/Policy.ma (modified) * src/ASM/Status.ma (modified) * src/ASM/StatusProofs.ma (modified) * src/ASM/Util.ma (modified) * src/ASM/Vector.ma (modified) * src/ASM/WellLabeled.ma (modified) * src/Clight/Csem.ma (modified) * src/Clight/SimplifyCasts.ma (modified) * src/Clight/casts.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/RTL/RTLToERTL.ma (modified) * src/RTLabs/RTLabsToRTL.ma (modified) * src/RTLabs/RTLabsToRTL_paolo.ma (modified) * src/common/FrontEndOps.ma (modified) * src/common/FrontEndVal.ma (modified) * src/common/Integers.ma (modified) * src/common/Values.ma (modified) !! BEWARE: major commit !! 1) [affects everybody] split for ... Tue, 05 Jun 2012 15:49:09 GMT mulligan [2018] * src/ASM/AssemblyProofSplit.ma (modified) * src/ASM/Policy.ma (modified) CJNE case a complete mess. Wed, 30 May 2012 17:22:05 GMT boender [2008] * src/ASM/Policy.ma (modified) - substantial closing of holes in proof Mon, 21 May 2012 14:57:23 GMT boender [1973] * src/ASM/Policy.ma (modified) - removed superfluous match - displaced 'cases daemon' Thu, 17 May 2012 10:42:14 GMT boender [1965] * src/ASM/Policy.ma (modified) - further completed proof, changed jump_expansion' to reflect new ... Wed, 16 May 2012 13:10:58 GMT boender [1956] * src/ASM/Policy.ma (modified) - finished proof of lemma (where auto does strange things again) Tue, 15 May 2012 16:20:31 GMT boender [1950] * src/ASM/Policy.ma (modified) - advances in policy Mon, 14 May 2012 16:02:20 GMT mulligan [1942] * src/ASM/Assembly.ma (modified) * src/ASM/Policy.ma (modified) Work on showing the equivalence of two methods of looking up from the ... Mon, 14 May 2012 14:05:55 GMT boender [1940] * src/ASM/Policy.ma (modified) - committed new version of final invariant Fri, 11 May 2012 13:06:15 GMT boender [1937] * src/ASM/Policy.ma (modified) * src/ASM/Util.ma (modified) - filled in some of the gaps in the proof of Policy - reverted ... Thu, 10 May 2012 13:37:07 GMT boender [1934] * src/ASM/Arithmetic.ma (modified) * src/ASM/Assembly.ma (modified) * src/ASM/Policy.ma (modified) * src/ASM/Util.ma (modified) - various & sundry moves of lemmas to better places - integrated ... Thu, 10 May 2012 10:00:21 GMT boender [1933] * src/ASM/Policy.ma (modified) - slight revamp Thu, 10 May 2012 08:35:18 GMT boender [1932] * src/ASM/Policy.ma (modified) - added some more dependent types (we love 'em) 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 ... Wed, 11 Apr 2012 12:36:47 GMT boender [1886] * src/ASM/Policy.ma (modified) - improvements for disambiguation and quick(er) typing Thu, 05 Apr 2012 16:13:26 GMT boender [1879] * src/ASM/Policy.ma (modified) - Policy compiles until the end, still some (fairly trivial) cases ... Wed, 07 Mar 2012 18:16:55 GMT boender [1810] * src/ASM/Policy.ma (modified) - new version of policy that compiles up to the final glue Wed, 07 Mar 2012 12:27:17 GMT boender [1809] * src/ASM/Policy.ma (modified) - committed partially compiling version of policy (up until ... Wed, 14 Dec 2011 16:28:11 GMT sacerdot [1615] * src/ASM/Assembly.ma (modified) * src/ASM/Policy.ma (modified) Policy now depends on Assembly and not the other way around. Wed, 14 Dec 2011 16:00:45 GMT boender [1614] * src/ASM/Assembly.ma (modified) * src/ASM/Policy.ma (added) - split policy from assembly