Design decisions: - absolute time? - what time synchronization guarantees we have at verification time? Probably best to push those decisions to the concrete implementation, and just write support for this opcode