Timeline
Dec 7, 2012:
- 8:37 PM Changeset [2547] by
- going on in proof of linearise simplified by use of monadic functional …
- 6:49 PM Changeset [2546] by
- Some more progress.
- 6:39 PM Changeset [2545] by
- Comitting current progress of CL to CM
- 5:52 PM Changeset [2544] by
- More added, painful crash course in learning Agda. Seem to have the …
- 11:35 AM Changeset [2543] by
- finished stmt_at_sigma_commute
- 11:13 AM Changeset [2542] by
- Trying an Agda port of the polymorphic variants implementation to see …
Dec 6, 2012:
- 4:02 PM Changeset [2541] by
- adapted size notation to last matita lib update (01/12/2012) that …
- 3:17 PM Changeset [2540] by
- cl_jump case now provides a proof of costedness of the following state
- 2:48 PM Changeset [2539] by
- added cl_jump case to trace_any_any_free
- 1:39 PM Changeset [2538] by
- fixed Traces.ma after changes in joint/semantics.ma
- 1:24 PM Changeset [2537] by
- rolled back changes on calls in joint. Now the save_frame parameter …
- 1:18 PM Changeset [2536] by
- finished eval_seq_no_pc_sigma_commute lemma
Dec 5, 2012:
- 7:20 PM Changeset [2535] by
- Add the trivial C program with check that there's a measurable subtrace.
- 7:20 PM Changeset [2534] by
- Tweak measurable definition to stop at the return from a function.
- 7:20 PM Changeset [2533] by
- Some fall out from removing floats.
- 6:57 PM Changeset [2532] by
- added FCOND in LIN, and rewritten linearise so that it never adds a …
- 1:28 PM Changeset [2531] by
- Trivial tweaks.
Dec 4, 2012:
- 6:29 PM Changeset [2530] by
- temporary switch to cl_jump treated as cl_other fixed script for new …
- 6:16 PM Changeset [2529] by
- rewritten function handling in joint swapped call_rel with ret_rel in …
- 9:05 AM Changeset [2528] by
- added cases PUSH, C_ADDRESS and COPACCS
Dec 3, 2012:
- 6:22 PM Changeset [2527] by
- Progress on CL to CM.
- 5:48 PM Changeset [2526] by
- …
- 5:39 PM Changeset [2525] by
- …
- 4:41 PM Changeset [2524] by
- Avoiding conflicts
- 4:30 PM Changeset [2523] by
- …
- 4:15 PM Changeset [2522] by
- Generic stuff moved to infrastructure.
- 4:10 PM Changeset [2521] by
- ..
- 4:07 PM Changeset [2520] by
- Now it is nice!
- 12:29 PM Changeset [2519] by
- To prevent conflicts
- 12:28 PM Changeset [2518] by
- …
- 11:51 AM Changeset [2517] by
- …
Dec 2, 2012:
- 5:45 PM Changeset [2516] by
- removed typedefs; restored older versions; moved typedefs to …
- 5:20 PM Changeset [2515] by
- …
- 4:40 PM Changeset [2514] by
- All .ma files committed: some of them are just in-progress.
Dec 1, 2012:
- 9:01 PM Changeset [2513] by
- Minor tweaks. Simplified dependencies again.
- 8:36 PM Changeset [2512] by
- Simplified dependencies on ASM, to allow rollback to when …
Nov 30, 2012:
- 6:31 PM Changeset [2511] by
- Conjecture main Cminor/RTLabs simulation results. Add a few notes …
- 4:40 PM Changeset [2510] by
- Some progress on the Cl -> Cm front
- 1:15 PM Changeset [2509] by
- misc note
Nov 29, 2012:
- 8:12 PM Changeset [2508] by
- more tweaks. compiler and correctness still build.
- 7:14 PM Changeset [2507] by
- finished pop case in commutation eval_Seq_no_pc
- 6:38 PM Changeset [2506] by
- Use common definition of measurable.
- 3:37 PM Changeset [2505] by
- Cleaned up compiler.ma; some refactoring/additional code needed in …
- 3:33 PM Changeset [2504] by
- More refactoring to support the tidied up compiler.ma
- 3:32 PM Changeset [2503] by
- tidied up, with new auxiliary defns, some refactoring, some code …
- 11:59 AM Changeset [2502] by
- Sketch a little about how measurable traces might work with RTLabs and …
- 10:12 AM Changeset [2501] by
- working on lineariseProof. Not yet finished.
Nov 28, 2012:
- 5:57 PM Changeset [2500] by
- Continuing work on simulation in Clight/Cminor?
- 12:52 PM Changeset [2499] by
- Separate out the RTLabs abstract status record from the proofs about …
Nov 27, 2012:
- 6:01 PM Changeset [2498] by
- Refactor: Typedefs object_code and costlabel_map lifted out from …
- 5:59 PM Changeset [2497] by
- Simplified dependencies on ASM; knock-on from changes in ASM/*.ma
- 5:50 PM Changeset [2496] by
- Some tentative work on the simulation proof for expressions, in order …
- 5:17 PM Changeset [2495] by
- continuing lineariseProof
Nov 26, 2012:
- 6:24 PM Changeset [2494] by
- Removed BJC's axiomatisation of rtlabs_to_rtl, now that …
- 6:00 PM Changeset [2493] by
- Change in cst_well_defd to fix previously broken defn of …
- 11:52 AM Changeset [2492] by
- Reduce axiomatisation in compiler.ma.
- 11:30 AM Changeset [2491] by
- fixed wrt change of list member definition
Nov 25, 2012:
- 1:33 PM Changeset [2490] by
- switched back to Byte immediate (instead of beval ones) propagated …
Nov 23, 2012:
- 5:28 PM Changeset [2489] by
- Conjecture some Clight/Cminor? simulation results.
- 4:29 PM Changeset [2488] by
- glitch fixed
- 3:47 PM Changeset [2487] by
- Set up "after_n_steps" to enforce an invariant on states.
- 12:18 PM Changeset [2486] by
- First go at a generalised version of measurable.
- 11:22 AM Changeset [2485] by
- Sketch of Clight/Cminor? callstate simulation
Nov 22, 2012:
- 6:40 PM Changeset [2484] by
- fixed Traces and semantics added commutation record (not yet finished) …
- 5:05 PM Changeset [2483] by
- Memory injections for Clight to Cminor, partially axiomatized.
- 3:49 PM Changeset [2482] by
- Note about front-end simulations
- 10:09 AM HiPEAC13 edited by
- (diff)
Nov 21, 2012:
Nov 20, 2012:
- 6:40 PM Changeset [2481] by
- corrected some inconsistencies fixed some of lineariseProof
- 6:39 PM Changeset [2480] by
- Some more changes.
- 5:12 PM Changeset [2479] by
- A small amount of rewriting as i didn't like the original introduction …
- 2:28 PM Changeset [2478] by
- unified is_internal_function_of_program and is_internal_function
- 1:41 PM Changeset [2477] by
- status_simulation reformulated definition of joint_classify split up …
Nov 19, 2012:
- 6:04 PM Changeset [2476] by
- fixed commutation lemmas in lineariseProof started proof of main …
- 5:13 PM Changeset [2475] by
- Get compiler.ma and correctness.ma checking again. Note that the …
- 10:57 AM Changeset [2474] by
- changed form of a statement
Nov 16, 2012:
- 6:59 PM Changeset [2473] by
- put some generic stuff we need in the back end in extraGlobalenvs …
- 6:41 PM Changeset [2472] by
- Misc clight->cminor notes.
- 6:41 PM Changeset [2471] by
- Tame global environments a little.
Nov 15, 2012:
- 7:06 PM Changeset [2470] by
- completely separated program counters from code pointers in joint …
- 6:33 PM Changeset [2469] by
- Fix up opaque type errors from recent changes.
- 6:12 PM Changeset [2468] by
- Floats are gone from the front-end. Some trace amount might remain in …
- 4:43 PM Changeset [2467] by
- LINEARISE PROOF MODIFIED NOT YED FIXED
Nov 14, 2012:
- 7:17 PM Changeset [2466] by
- Show how global environments in clight to cminor pass match up.
- 7:17 PM Changeset [2465] by
- Remove obsolete comment (runtime functions should be implemented later …
- 5:38 PM Changeset [2464] by
- adapted lineariseProof to new semantics
- 1:20 PM Changeset [2463] by
- swapped back call_rel and ret_rel…
- 10:31 AM Changeset [2462] by
- separated in back end values program counters from code pointers …
Nov 13, 2012:
- 7:06 PM Changeset [2461] by
- First cut of inductive structured traces diagrams.
- 6:30 PM Changeset [2460] by
- Rest of variable characterisation.
- 6:30 PM Changeset [2459] by
- Syntax update
- 11:38 AM Changeset [2458] by
- Clight to Cminor allocates stack variables to disjoint regions within …
- 11:30 AM Changeset [2457] by
- rewritten function handling in joint swapped call_rel with ret_rel in …
- 11:28 AM Changeset [2456] by
- - added simple proof
Nov 12, 2012:
- 4:39 PM Changeset [2455] by
- Dump rough notes on RTLabs structured traces existence proof.
- 4:39 PM Changeset [2454] by
- More misc notes on clight->cminor.
- 4:30 PM Changeset [2453] by
- come changes in monad notation to * avoid pretty printed monsters * …
- 12:50 PM Changeset [2452] by
- Completed commutation lemmas of fetch_statement
Nov 10, 2012:
- 5:31 PM Changeset [2451] by
- Structured traces paper for Brian as per e-mail conversation yesterday.
Nov 9, 2012:
- 6:04 PM Changeset [2450] by
- Minor typo
- 6:01 PM Changeset [2449] by
- Documentation added.
- 4:38 PM Changeset [2448] by
- Comitting current state of switch removal.
- 4:01 PM Changeset [2447] by
- All axioms opened so far and that must be closed here have been closed.
- 1:21 PM Changeset [2446] by
- Fetch commutation proof reduced to one simple (?) lemma.
- 11:47 AM Changeset [2445] by
- 1. sigma function axiomatically defined (together with its spec). …
Nov 8, 2012:
- 6:47 PM Changeset [2444] by
- Some inversion lemmas for after_n_steps for dealing with >1 source …
- 2:27 PM Changeset [2443] by
- changed joint's stack pointer and internal stack
Note: See TracTimeline
for information about the timeline view.
