Correctness proof of a log-based semantics for software transactional memory using Agda.