# # ChangeLog for / # # Generated by Trac 1.2 # Dec 12, 2019, 3:46:34 AM Thu, 16 Aug 2012 17:01:18 GMT garnier [2298] * src/Clight/switchRemoval.ma (modified) WIP: converting switch removal from Z to bitvectors. Does not ... Thu, 16 Aug 2012 16:03:21 GMT campbell [2297] * src/RTLabs/CostSpec.ma (modified) * src/RTLabs/Traces.ma (modified) Nicer form of steps until cost label bound in RTLabs. Mon, 13 Aug 2012 12:18:31 GMT campbell [2296] * src/RTLabs/Traces.ma (modified) * src/RTLabs/semantics.ma (modified) * src/common/Pointers.ma (modified) * src/utilities/deqsets.ma (added) Tidy up some ill-placed definitions. Mon, 13 Aug 2012 10:21:30 GMT campbell [2295] * src/RTLabs/Traces.ma (modified) * src/RTLabs/semantics.ma (modified) Start on showing unrepeating property of RTLabs structured traces: ... Mon, 13 Aug 2012 10:21:29 GMT campbell [2294] * src/RTLabs/CostSpec.ma (modified) Make RTLabs cost spec deterministic. Mon, 13 Aug 2012 10:21:28 GMT campbell [2293] * src/RTLabs/Traces.ma (modified) Add instruction pointer for call states in RTLabs. Thu, 02 Aug 2012 16:40:15 GMT campbell [2292] * src/Cminor/toRTLabs.ma (modified) * src/RTLabs/syntax.ma (modified) * src/utilities/lists.ma (modified) More RTLabs invariants. Thu, 02 Aug 2012 15:04:38 GMT campbell [2291] * src/compiler.ma (modified) Disable switch removal in compiler.ma for now. Thu, 02 Aug 2012 15:04:37 GMT campbell [2290] * src/RTLabs/RTLabsToRTL.ma (modified) Remove jump tables from RTLabs -> RTL. Thu, 02 Aug 2012 15:04:37 GMT campbell [2289] * src/Cminor/toRTLabs.ma (modified) Update alias Thu, 02 Aug 2012 15:04:36 GMT campbell [2288] * src/RTLabs/CostSpec.ma (modified) * src/RTLabs/Traces.ma (modified) * src/RTLabs/semantics.ma (modified) * src/RTLabs/syntax.ma (modified) Remove jumptables from RTLabs. :( Thu, 02 Aug 2012 15:04:35 GMT campbell [2287] * src/Cminor/toRTLabs.ma (modified) * src/RTLabs/syntax.ma (modified) RTLabs typing for loads and stores. Thu, 02 Aug 2012 13:18:11 GMT tranquil [2286] * src/ASM/I8051.ma (modified) * src/ASM/Util.ma (modified) * src/ASM/Vector.ma (modified) * src/ERTL/ERTL.ma (modified) * src/ERTL/ERTLToLTL.ma (modified) * src/ERTL/ERTLToLTL_paolo.ma (deleted) * src/ERTL/ERTL_paolo.ma (deleted) * src/ERTL/Interference.ma (modified) * src/ERTL/Interference_paolo.ma (deleted) * src/ERTL/liveness.ma (modified) * src/ERTL/liveness_paolo.ma (deleted) * src/ERTL/semantics.ma (modified) * src/ERTL/semantics_paolo.ma (deleted) * src/LIN/LIN.ma (modified) * src/LIN/LINToASM.ma (modified) * src/LIN/LIN_paolo.ma (deleted) * src/LIN/joint_LTL_LIN.ma (modified) * src/LIN/joint_LTL_LIN_paolo.ma (deleted) * src/LIN/joint_LTL_LIN_semantics.ma (modified) * src/LIN/joint_LTL_LIN_semantics_paolo.ma (deleted) * src/LIN/semantics.ma (modified) * src/LIN/semantics_paolo.ma (deleted) * src/LTL/LTL.ma (modified) * src/LTL/LTLToLIN.ma (modified) * src/LTL/LTLToLIN_paolo.ma (deleted) * src/LTL/LTL_paolo.ma (deleted) * src/LTL/semantics.ma (modified) * src/LTL/semantics_paolo.ma (deleted) * src/RTL/RTL.ma (modified) * src/RTL/RTLTailcall.ma (modified) * src/RTL/RTLTailcall_paolo.ma (deleted) * src/RTL/RTLToERTL.ma (modified) * src/RTL/RTLToERTL_paolo.ma (deleted) * src/RTL/RTL_paolo.ma (deleted) * src/RTL/semantics.ma (modified) * src/RTL/semantics_paolo.ma (deleted) * src/RTLabs/RTLabsToRTL.ma (modified) * src/RTLabs/RTLabsToRTL_paolo.ma (deleted) * src/common/AST.ma (modified) * src/common/BackEndOps.ma (added) * src/common/ByteValues.ma (modified) * src/common/ByteValues_paolo.ma (deleted) * src/common/FrontEndVal.ma (modified) * src/common/Registers.ma (modified) * src/compiler.ma (modified) * src/joint/BEMem.ma (modified) * src/joint/Joint.ma (modified) * src/joint/Joint_paolo.ma (deleted) * src/joint/SemanticUtils.ma (modified) * src/joint/Traces.ma (modified) * src/joint/TranslateUtils.ma (modified) * src/joint/TranslateUtils_paolo.ma (deleted) * src/joint/blocks.ma (modified) * src/joint/linearise.ma (modified) * src/joint/semantics.ma (modified) * src/joint/semanticsUtils_paolo.ma (deleted) * src/joint/semantics_paolo.ma (deleted) * src/utilities/extranat.ma (modified) Big update! * merge of all _paolo variants * reorganised some ... Thu, 02 Aug 2012 11:58:14 GMT sacerdot [2285] * src/ASM/AssemblyProofSplit.ma (modified) * src/ASM/StatusProofs.ma (modified) * src/ASM/StatusProofsSplit.ma (modified) 1. duplicated code erased 2. POP case finished up to lemmas on ... Wed, 01 Aug 2012 14:56:20 GMT sacerdot [2284] * src/ASM/AssemblyProof.ma (modified) * src/ASM/AssemblyProofSplit.ma (modified) * src/ASM/Test.ma (modified) PUSH finished Tue, 31 Jul 2012 16:11:27 GMT mulligan [2283] * src/ASM/AssemblyProofSplit.ma (modified) * src/ASM/Interpret.ma (modified) Work from today. Tue, 31 Jul 2012 16:08:00 GMT sacerdot [2282] * src/ASM/AssemblyProof.ma (modified) * src/ASM/AssemblyProofSplit.ma (modified) * src/ASM/Test.ma (modified) PUSH case almost finished Tue, 31 Jul 2012 00:22:35 GMT sacerdot [2281] * src/ASM/Test.ma (modified) ... Mon, 30 Jul 2012 22:10:59 GMT sacerdot [2280] * src/ASM/Interpret.ma (modified) Proof repaired. Mon, 30 Jul 2012 21:44:50 GMT sacerdot [2279] * src/ASM/AssemblyProof.ma (modified) * src/ASM/AssemblyProofSplit.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/Test.ma (modified) 1. Bug fixed in the semantics of PUSH (no indirection performed) 2. ... Mon, 30 Jul 2012 16:33:11 GMT mulligan [2278] * src/ASM/AssemblyProofSplit.ma (modified) * src/ASM/AssemblyProofSplitSplit.ma (modified) Half of JC case complete Mon, 30 Jul 2012 14:54:33 GMT tranquil [2277] * src/common/ByteValues_paolo.ma (modified) * replaced incorrect use of subvector_with Mon, 30 Jul 2012 12:36:41 GMT sacerdot [2276] * src/ASM/AssemblyProof.ma (modified) * src/ASM/AssemblyProofSplit.ma (modified) * src/ASM/Test.ma (modified) ... Mon, 30 Jul 2012 11:05:55 GMT tranquil [2275] * src/ASM/I8051.ma (modified) * src/common/ByteValues.ma (modified) * src/common/ByteValues_paolo.ma (copied) * moved around some code (I8051.ma does not depend on ByteValues.ma ... Sun, 29 Jul 2012 23:14:40 GMT sacerdot [2274] * src/ASM/StatusProofsSplit.ma (modified) * src/ASM/Test.ma (modified) Dead code commented out and code out of place moved to Test.ma. Sun, 29 Jul 2012 22:46:19 GMT sacerdot [2273] * src/ASM/AssemblyProofSplit.ma (modified) * src/ASM/AssemblyProofSplitSplit.ma (modified) * src/ASM/PolicyFront.ma (modified) * src/ASM/Test.ma (modified) 1. lemmas moved from all files to Test.ma 2. most of the lemmas in ... Fri, 27 Jul 2012 15:53:25 GMT mulligan [2272] * src/ASM/AssemblyProof.ma (modified) * src/ASM/AssemblyProofSplit.ma (modified) * src/ASM/Interpret.ma (modified) * src/ASM/Status.ma (modified) * src/ASM/StatusProofs.ma (modified) * src/ASM/StatusProofsSplit.ma (modified) * src/ASM/Test.ma (modified) Changed proof strategy for main lemma after noticed that the current ... Thu, 26 Jul 2012 15:02:52 GMT garnier [2271] * src/Clight/switchRemoval.ma (modified) Proof of correction for the semantics of expressions under memory ... Thu, 26 Jul 2012 13:57:30 GMT mulligan [2270] * src/ASM/Status.ma (modified) Bug spotted and fixed in write_at_stack_pointer Thu, 26 Jul 2012 13:29:15 GMT sacerdot [2269] * src/ASM/AssemblyProofSplitSplit.ma (modified) Proof completely repaired up to ... Thu, 26 Jul 2012 12:56:58 GMT mulligan [2268] * src/ASM/Assembly.ma (modified) Bug spotted in instruction_size (lookup_datalabels cannot just be a ... Thu, 26 Jul 2012 10:05:58 GMT sacerdot [2267] * src/ASM/AssemblyProofSplitSplit.ma (modified) Call is now proved using the new strategy. Thu, 26 Jul 2012 08:43:55 GMT sacerdot [2266] * src/ASM/AssemblyProofSplitSplit.ma (modified) All daemons closed in Jmp case. Thu, 26 Jul 2012 01:48:31 GMT sacerdot [2265] * src/ASM/AssemblyProofSplit.ma (modified) Commented out code removed. 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 ... Wed, 25 Jul 2012 16:55:36 GMT garnier [2263] * src/Clight/Csem.ma (modified) * src/Clight/switchRemoval.ma (modified) Finished proving semantics preservation under memory injections for ... Wed, 25 Jul 2012 15:54:59 GMT mulligan [2262] * src/ASM/AssemblyProofSplit.ma (modified) Changes from today. Wed, 25 Jul 2012 15:04:33 GMT mulligan [2261] * src/ASM/AssemblyProofSplit.ma (modified) Resolved conflict Wed, 25 Jul 2012 14:52:44 GMT sacerdot [2260] * src/ASM/AssemblyProofSplit.ma (modified) Now we use the efficient lookup_address. Wed, 25 Jul 2012 14:37:34 GMT mulligan [2259] * src/ASM/AssemblyProofSplit.ma (modified) For Claudio Wed, 25 Jul 2012 11:47:01 GMT sacerdot [2258] * src/ASM/AssemblyProofSplit.ma (modified) * src/ASM/Test.ma (modified) 1. lemma generalized 2. automation replaced with expansion to make ... Wed, 25 Jul 2012 11:13:52 GMT mulligan [2257] * src/ASM/AssemblyProofSplit.ma (modified) Daemon in SETB case closed. Wed, 25 Jul 2012 10:12:57 GMT mulligan [2256] * src/ASM/AssemblyProof.ma (modified) * src/ASM/AssemblyProofSplit.ma (modified) MOV and MOVX cases complete Tue, 24 Jul 2012 18:12:00 GMT garnier [2255] * src/Clight/switchRemoval.ma (modified) Had to modify the definition of memory injections to prove that ... Tue, 24 Jul 2012 17:40:23 GMT campbell [2254] * src/Cminor/semantics.ma (modified) Fix up invariants in Cminor semantics. Tue, 24 Jul 2012 17:40:22 GMT campbell [2253] * src/Clight/test/goto-if.test.ma (modified) * src/Clight/test/sum.test.ma (modified) * src/Cminor/toRTLabs.ma (modified) * src/compiler.ma (modified) Cminor to RTLabs is now a total function. Tue, 24 Jul 2012 17:40:21 GMT campbell [2252] * src/Clight/toCminor.ma (modified) * src/Cminor/initialisation.ma (modified) * src/Cminor/syntax.ma (modified) * src/Cminor/toRTLabs.ma (modified) Use the return statement invariant. Restructure the invariants for ... Tue, 24 Jul 2012 17:40:21 GMT campbell [2251] * 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) Add new invariant to Cminor that return typs should be respected. Tue, 24 Jul 2012 17:40:20 GMT campbell [2250] * src/Clight/toCminor.ma (modified) Tidy up Clight to Cminor pass a bit. Tue, 24 Jul 2012 17:40:13 GMT campbell [2249] * src/Clight/toCminor.ma (modified) * src/Cminor/initialisation.ma (modified) * src/Cminor/syntax.ma (modified) Tweak Cminor invariant to be slightly more readable/extendable. Tue, 24 Jul 2012 17:15:24 GMT sacerdot [2248] * src/ASM/PolicyStep.ma (modified) Final changes. All daemons removed, but the real one (open goal). Tue, 24 Jul 2012 16:00:48 GMT mulligan [2247] * src/ASM/AssemblyProof.ma (modified) * src/ASM/AssemblyProofSplit.ma (modified) * src/ASM/Status.ma (modified) * src/ASM/Test.ma (modified) Work on the MOV instruction from today and bug fixes in set_arg_1. Tue, 24 Jul 2012 15:51:11 GMT sacerdot [2246] * src/ASM/PolicyStep.ma (modified) Final technical lemma streamlined. Maybe it can be streamlined even more. Tue, 24 Jul 2012 14:50:20 GMT sacerdot [2245] * src/ASM/PolicyStep.ma (modified) Temporary commit to have a backtracking point. Yes, I know this ... Tue, 24 Jul 2012 12:47:26 GMT sacerdot [2244] * src/ASM/PolicyStep.ma (modified) Technical lemma used. Tue, 24 Jul 2012 12:31:25 GMT sacerdot [2243] * src/ASM/PolicyStep.ma (modified) One more lemma streamlined, one to go + one to be completed. Tue, 24 Jul 2012 11:01:55 GMT sacerdot [2242] * src/ASM/PolicyStep.ma (modified) jump_expansion_step3 streamlined Tue, 24 Jul 2012 09:51:49 GMT boender [2241] * src/ASM/PolicyStep.ma (modified) - merged changes by Claudio Tue, 24 Jul 2012 09:40:43 GMT sacerdot [2240] * src/ASM/PolicyStep.ma (modified) All "interesting" technical lemmas singled out, proofs to be uncommented. Tue, 24 Jul 2012 09:09:29 GMT sacerdot [2239] * src/ASM/PolicyStep.ma (modified) One more lemma polished. Mon, 23 Jul 2012 21:31:57 GMT sacerdot [2238] * src/ASM/PolicyStep.ma (modified) Taken out lemma integrated. Mon, 23 Jul 2012 21:11:27 GMT sacerdot [2237] * src/ASM/PolicyStep.ma (modified) Even shorter version. Mon, 23 Jul 2012 20:46:06 GMT sacerdot [2236] * src/ASM/PolicyStep.ma (modified) One subproof made shorter. Mon, 23 Jul 2012 19:22:02 GMT sacerdot [2235] * src/ASM/PolicyFront.ma (modified) Towards smaller proofs. Mon, 23 Jul 2012 17:31:11 GMT garnier [2234] * src/Clight/frontend_misc.ma (modified) * src/Clight/switchRemoval.ma (modified) Progress on proving semantics preservation under memory injections. Mon, 23 Jul 2012 14:51:51 GMT tranquil [2233] * src/ERTL/semantics_paolo.ma (modified) * src/LIN/joint_LTL_LIN_semantics_paolo.ma (modified) * src/RTL/semantics_paolo.ma (modified) * src/joint/semantics_paolo.ma (modified) * completed update of ERTL semantics * some minor changes in joint ... Mon, 23 Jul 2012 12:05:10 GMT campbell [2232] * 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) Remove unused block structure in Cminor. Mon, 23 Jul 2012 10:44:36 GMT garnier [2231] * src/Clight/frontend_misc.ma (added) Various tiny lemmas used in at least two files in the fornt-end. 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 18:28:57 GMT garnier [2227] * src/Clight/switchRemoval.ma (modified) * New version of the switch removal algorithm, described at the top ... Fri, 20 Jul 2012 16:36:34 GMT campbell [2226] * src/RTLabs/CostSpec.ma (modified) * src/RTLabs/Traces.ma (modified) * src/common/Globalenvs.ma (modified) Whole program proof. 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. Fri, 20 Jul 2012 14:29:31 GMT campbell [2224] * src/RTLabs/Traces.ma (modified) Proper whole program result in RTLabs/Traces Fri, 20 Jul 2012 14:29:29 GMT campbell [2223] * src/RTLabs/Traces.ma (modified) Simplify RTLabs structure traces proofs by getting rid of wrong ... Fri, 20 Jul 2012 08:58:15 GMT sacerdot [2222] * src/ASM/PolicyFront.ma (modified) * src/common/Identifiers.ma (modified) More robust to possible future changes to the "in match" semantics ... Fri, 20 Jul 2012 08:46:29 GMT boender [2221] * src/ASM/Assembly.ma (modified) * src/ASM/PolicyFront.ma (modified) - removed cases daemon from PolicyFront Fri, 20 Jul 2012 00:05:56 GMT sacerdot [2220] * src/ASM/PolicyStep.ma (modified) Some minor speed up and daemon-uncommenting. Thu, 19 Jul 2012 16:45:52 GMT campbell [2219] * src/Clight/SimplifyCasts.ma (modified) Speed up cast simplification proof checking a bit. Thu, 19 Jul 2012 16:45:49 GMT campbell [2218] * src/RTLabs/CostSpec.ma (added) * src/RTLabs/Traces.ma (modified) * src/common/Pointers.ma (modified) Separate out cost properties required of RTLabs programs from the ... Thu, 19 Jul 2012 16:13:54 GMT tranquil [2217] * src/ERTL/ERTL_paolo.ma (modified) * src/LIN/joint_LTL_LIN_paolo.ma (modified) * src/LIN/joint_LTL_LIN_semantics_paolo.ma (added) * src/LIN/semantics_paolo.ma (added) * src/LTL/semantics_paolo.ma (added) * src/RTL/RTLToERTL_paolo.ma (modified) * src/RTL/RTL_paolo.ma (modified) * src/RTL/semantics_paolo.ma (modified) * src/RTLabs/RTLabsToRTL_paolo.ma (modified) * src/joint/Joint_paolo.ma (modified) * src/joint/TranslateUtils_paolo.ma (modified) * src/joint/semantics_paolo.ma (modified) * collapsed step_params, unserialized_params, funct_params and ... Thu, 19 Jul 2012 15:33:54 GMT mulligan [2216] * src/ASM/AssemblyProofSplit.ma (modified) More work on the big lemma. Nearly there now. Thu, 19 Jul 2012 15:12:50 GMT sacerdot [2215] * src/ASM/PolicyStep.ma (modified) Some speed up. Thu, 19 Jul 2012 12:42:02 GMT tranquil [2214] * src/ERTL/ERTLToLTL_paolo.ma (modified) * src/ERTL/ERTL_paolo.ma (modified) * src/ERTL/liveness_paolo.ma (modified) * src/LIN/LIN_paolo.ma (modified) * src/LIN/joint_LTL_LIN_paolo.ma (modified) * src/LTL/LTL_paolo.ma (modified) * src/RTL/RTLTailcall_paolo.ma (modified) * src/RTL/RTLToERTL_paolo.ma (modified) * src/RTL/RTL_paolo.ma (modified) * src/RTLabs/RTLabsToRTL_paolo.ma (modified) * src/joint/Joint_paolo.ma (modified) * src/joint/TranslateUtils_paolo.ma (modified) * src/joint/blocks.ma (modified) * src/joint/linearise.ma (modified) * src/joint/semanticsUtils_paolo.ma (modified) * src/joint/semantics_paolo.ma (modified) * changed order of parameters of joint_internal_function and genv in ... Wed, 18 Jul 2012 15:57:26 GMT boender [2213] * src/ASM/PolicyFront.ma (modified) - removed one cases daemon Wed, 18 Jul 2012 15:30:26 GMT mulligan [2212] * src/ASM/AssemblyProofSplit.ma (modified) * src/ASM/Interpret.ma (modified) More work on the INC case 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, 18 Jul 2012 13:03:59 GMT mulligan [2210] * src/ASM/AssemblyProofSplit.ma (modified) XOR case completely finished. Wed, 18 Jul 2012 12:56:12 GMT mulligan [2209] * src/ASM/AssemblyProof.ma (modified) * src/ASM/AssemblyProofSplit.ma (modified) Closed major daemons in the supporting lemmas of the main lemma. Wed, 18 Jul 2012 11:26:43 GMT tranquil [2208] * src/ERTL/ERTLToLTL_paolo.ma (modified) * src/ERTL/ERTL_paolo.ma (modified) * src/ERTL/liveness_paolo.ma (modified) * src/ERTL/semantics_paolo.ma (added) * src/LIN/joint_LTL_LIN_paolo.ma (modified) * src/LTL/LTL_paolo.ma (modified) * src/RTL/RTLToERTL_paolo.ma (modified) * src/RTL/RTL_paolo.ma (modified) * src/RTLabs/RTLabsToRTL_paolo.ma (modified) * src/joint/Joint_paolo.ma (modified) * src/joint/semanticsUtils_paolo.ma (modified) * moving some code around * changed immediates to hold beval in ... Wed, 18 Jul 2012 10:29:14 GMT mulligan [2207] * src/ASM/AssemblyProofSplit.ma (modified) * src/ASM/Test.ma (modified) Improvements and corrections to the main lemma proof in ... Wed, 18 Jul 2012 10:27:02 GMT campbell [2206] * src/common/Executions.ma (modified) Add note about cost maps to simulation definition. Wed, 18 Jul 2012 10:27:01 GMT campbell [2205] * src/LTL/LTLToLIN.ma (modified) * src/compiler.ma (modified) * src/correctness.ma (modified) Get correctness.ma type checking again. Wed, 18 Jul 2012 08:08:37 GMT sacerdot [2204] * src/ASM/AssemblyProofSplit.ma (modified) * src/ASM/Test.ma (modified) Shuffling around, suggestions, improvements. Tue, 17 Jul 2012 16:57:40 GMT campbell [2203] * src/Clight/Cexec.ma (modified) * src/Clight/labelSimulation.ma (modified) * src/common/Executions.ma (modified) * src/common/SmallstepExec.ma (modified) A general result about simulations of executions. Tue, 17 Jul 2012 16:57:39 GMT campbell [2202] * src/Clight/labelSimulation.ma (modified) * src/Clight/labelSpecification.ma (modified) * src/common/Executions.ma (added) * src/common/SmallstepExec.ma (modified) Start defining equivalent executions. Tue, 17 Jul 2012 16:57:38 GMT campbell [2201] * src/Clight/labelSpecification.ma (modified) Forgotten comment update. Tue, 17 Jul 2012 16:00:03 GMT tranquil [2200] * src/ASM/BitVectorZ.ma (modified) * src/joint/linearise.ma (modified) * src/joint/semanticsUtils_paolo.ma (modified) * src/joint/semantics_paolo.ma (modified) * src/utilities/hide.ma (added) * updated joint semantics: generation of linear and graph semantics ... Tue, 17 Jul 2012 15:40:00 GMT sacerdot [2199] * src/ASM/Assembly.ma (modified) No longer used lemma containing the last daemon removed. The proof ...