Pinned clock.rs. Host time is an explicit environment, never substituted with virtual time. Nanoseconds are exact integers; u128 saturation, Duration's u64 seconds bound, mixed-clock assertions and host checked-add fallback are preserved. No particular host clock trace is a proof over all environments.

structure Miri.Interpreter.Clock.Duration : Type

• seconds : UInt64
• nanos : UInt32
• nanosBound : self.nanos.toNat < 1000000000

def Miri.Interpreter.Clock.instReprDuration.repr : Duration → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Miri.Interpreter.Clock.instReprDuration : Repr Duration

Equations

• Miri.Interpreter.Clock.instReprDuration = { reprPrec := Miri.Interpreter.Clock.instReprDuration.repr }

def Miri.Interpreter.Clock.Duration.asNanos (d : Duration) : Nat

Equations

• d.asNanos = d.seconds.toNat * 1000000000 + d.nanos.toNat

def Miri.Interpreter.Clock.Duration.fromNanos (n : Nat) : Except StepError Duration

Equations

• One or more equations did not get rendered due to their size.

inductive Miri.Interpreter.Clock.Instant (Host : Type) : Type

• host {Host : Type} (value : Host) : Instant Host
• virtual {Host : Type} (nanoseconds : ABI.U128) : Instant Host

@[instance_reducible]

instance Miri.Interpreter.Clock.instReprInstant {Host✝ : Type} [Repr Host✝] : Repr (Instant Host✝)

Equations

• Miri.Interpreter.Clock.instReprInstant = { reprPrec := Miri.Interpreter.Clock.instReprInstant.repr }

def Miri.Interpreter.Clock.instReprInstant.repr {Host✝ : Type} [Repr Host✝] : Instant Host✝ → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

inductive Miri.Interpreter.Clock.Monotonic (Host : Type) : Type

• host {Host : Type} (epoch : Host) : Monotonic Host
• virtual {Host : Type} (nanoseconds : ABI.U128) : Monotonic Host

def Miri.Interpreter.Clock.instReprMonotonic.repr {Host✝ : Type} [Repr Host✝] : Monotonic Host✝ → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Miri.Interpreter.Clock.instReprMonotonic {Host✝ : Type} [Repr Host✝] : Repr (Monotonic Host✝)

Equations

• Miri.Interpreter.Clock.instReprMonotonic = { reprPrec := Miri.Interpreter.Clock.instReprMonotonic.repr }

inductive Miri.Interpreter.Clock.Deadline (Host System : Type) : Type

• monotonic {Host System : Type} (instant : Instant Host) : Deadline Host System
• realTime {Host System : Type} (time : System) : Deadline Host System

@[instance_reducible]

instance Miri.Interpreter.Clock.instReprDeadline {Host✝ System✝ : Type} [Repr Host✝] [Repr System✝] : Repr (Deadline Host✝ System✝)

Equations

• Miri.Interpreter.Clock.instReprDeadline = { reprPrec := Miri.Interpreter.Clock.instReprDeadline.repr }

def Miri.Interpreter.Clock.instReprDeadline.repr {Host✝ System✝ : Type} [Repr Host✝] [Repr System✝] : Deadline Host✝ System✝ → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

inductive Miri.Interpreter.Clock.TimeoutClock : Type

• monotonic : TimeoutClock
• realTime : TimeoutClock

@[instance_reducible]

instance Miri.Interpreter.Clock.instDecidableEqTimeoutClock : DecidableEq TimeoutClock

Equations

• Miri.Interpreter.Clock.instDecidableEqTimeoutClock x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Miri.Interpreter.Clock.instReprTimeoutClock.repr : TimeoutClock → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Miri.Interpreter.Clock.instReprTimeoutClock : Repr TimeoutClock

Equations

• Miri.Interpreter.Clock.instReprTimeoutClock = { reprPrec := Miri.Interpreter.Clock.instReprTimeoutClock.repr }

inductive Miri.Interpreter.Clock.TimeoutStyle : Type

• relative : TimeoutStyle
• absolute : TimeoutStyle

@[instance_reducible]

instance Miri.Interpreter.Clock.instDecidableEqTimeoutStyle : DecidableEq TimeoutStyle

Equations

• Miri.Interpreter.Clock.instDecidableEqTimeoutStyle x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Interpreter.Clock.instReprTimeoutStyle : Repr TimeoutStyle

Equations

• Miri.Interpreter.Clock.instReprTimeoutStyle = { reprPrec := Miri.Interpreter.Clock.instReprTimeoutStyle.repr }

def Miri.Interpreter.Clock.instReprTimeoutStyle.repr : TimeoutStyle → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Miri.Interpreter.Clock.M (S A : Type) : Type

Equations

• Miri.Interpreter.Clock.M S A = EStateM Miri.Interpreter.StepError S A

structure Miri.Interpreter.Clock.HostHooks (Host System S : Type) : Type

• monotonicNow : M S Host
• systemNow : M S System
• unixEpoch : System
• checkedAddMonotonic : Host → Duration → M S (Option Host)
• checkedAddSystem : System → Duration → M S (Option System)
• durationSince : Host → Host → M S Duration
• sleep : Duration → M S Unit

def Miri.Interpreter.Clock.addHostLossy {H S : Type} (checkedAdd : H → Duration → M S (Option H)) (time : H) (duration : Duration) : M S H

On host overflow the source retries exactly one hour, then asserts that this succeeds. It does not clamp to a fabricated maximum host timestamp.

Equations

• One or more equations did not get rendered due to their size.

def Miri.Interpreter.Clock.Instant.addLossy {Host System S : Type} (h : HostHooks Host System S) (instant : Instant Host) (duration : Duration) : M S (Instant Host)

Equations

• One or more equations did not get rendered due to their size.

def Miri.Interpreter.Clock.Instant.durationSince {Host System S : Type} (h : HostHooks Host System S) (instant earlier : Instant Host) : M S Duration

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.Clock.Instant.durationSince h (Miri.Interpreter.Clock.Instant.host instant_2) (Miri.Interpreter.Clock.Instant.host earlier_2) = h.durationSince instant_2 earlier_2
• Miri.Interpreter.Clock.Instant.durationSince h instant earlier = throw (Miri.Interpreter.StepError.invalidProgram "all clock instants must be of the same kind")

def Miri.Interpreter.Clock.Monotonic.new {Host System S : Type} (h : HostHooks Host System S) (communicate : Bool) : M S (Monotonic Host)

Equations

• One or more equations did not get rendered due to their size.

def Miri.Interpreter.Clock.Monotonic.tick {Host : Type} (checkedArithmetic : Bool) (clock : Monotonic Host) : Except StepError (Monotonic Host)

Rust's virtual tick uses ordinary u128 addition. The source build's arithmetic overflow-check setting is explicit, rather than silently saturating.

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.Clock.Monotonic.tick checkedArithmetic (Miri.Interpreter.Clock.Monotonic.host a) = pure (Miri.Interpreter.Clock.Monotonic.host a)

def Miri.Interpreter.Clock.Monotonic.sleep {Host System S : Type} (h : HostHooks Host System S) (clock : Monotonic Host) (duration : Duration) : M S (Monotonic Host)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Interpreter.Clock.Monotonic.sleep h (Miri.Interpreter.Clock.Monotonic.host a) duration = do h.sleep duration pure (Miri.Interpreter.Clock.Monotonic.host a)

def Miri.Interpreter.Clock.Monotonic.epoch {Host : Type} : Monotonic Host → Instant Host

Equations

• (Miri.Interpreter.Clock.Monotonic.host a).epoch = Miri.Interpreter.Clock.Instant.host a
• (Miri.Interpreter.Clock.Monotonic.virtual a).epoch = Miri.Interpreter.Clock.Instant.virtual 0

def Miri.Interpreter.Clock.Monotonic.now {Host System S : Type} (h : HostHooks Host System S) (clock : Monotonic Host) : M S (Instant Host)

Equations

• Miri.Interpreter.Clock.Monotonic.now h (Miri.Interpreter.Clock.Monotonic.host a) = do let __do_lift ← h.monotonicNow pure (Miri.Interpreter.Clock.Instant.host __do_lift)
• Miri.Interpreter.Clock.Monotonic.now h (Miri.Interpreter.Clock.Monotonic.virtual a) = pure (Miri.Interpreter.Clock.Instant.virtual a)

def Miri.Interpreter.Clock.Deadline.addLossy {Host System S : Type} (h : HostHooks Host System S) (deadline : Deadline Host System) (duration : Duration) : M S (Deadline Host System)

Equations

• One or more equations did not get rendered due to their size.

def Miri.Interpreter.Clock.timeout {Host System S : Type} (h : HostHooks Host System S) (clock : Monotonic Host) (communicate : Bool) (kind : TimeoutClock) (style : TimeoutStyle) (duration : Duration) : M S (Deadline Host System)

Preserve source effect ordering: RealTime checks communication before reading the host; Absolute monotonic uses epoch without reading now.

Equations

• One or more equations did not get rendered due to their size.