Get the current timestamp as a natural number, specifically the number of seconds since 00:00 January 1, 1900 GMT. Note well that this is not the Unix epoch.
In the logic this function reads from the ACL2 oracle, so there is no logical guarantee that it will return successive times. (Indeed, the user could likely change their computer's clock so that it would report earlier times.)
In the execution, we use Common Lisp's
This is, for whatever reason, a different starting date than the Unix epoch (which records time since the start of 1970). You should therefore be careful if you need to compare this timestamp against those produced by external tools.
(defun universal-time-fn (state) (declare (xargs :stobjs (state))) (declare (xargs :guard t)) (let ((__function__ 'universal-time)) (declare (ignorable __function__)) (b* ((- (raise "Raw Lisp definition not installed?")) ((mv err val state) (read-acl2-oracle state))) (if (and (not err) (natp val)) (mv val state) (mv 0 state)))))
(defthm natp-of-universal-time.seconds (b* (((mv ?seconds acl2::?state) (universal-time-fn state))) (natp seconds)) :rule-classes :type-prescription)
(defthm state-p1-of-universal-time.state (implies (force (state-p1 state)) (b* (((mv ?seconds acl2::?state) (universal-time-fn state))) (state-p1 state))) :rule-classes :rewrite)