Miri's vector-clock value operations

This module ports the timestamp and vector-clock operations from the pinned upstream/miri-source/src/concurrency/vector_clock.rs (Miri revision 7fa591d7d4dd9af8154becbc8332f8096f8323b1, blob 723dfd29651525198b7590553f1ef5e72b952eba). The stored representation keeps the complete packed 32-bit timestamp word, including the low read/retag bit. Clock comparisons and timestamp equality intentionally inspect time only, as the Rust PartialEq/Ord implementations do.

The source's Span field is omitted. In this file it affects debug output and diagnostic attribution only: increment copies a non-dummy span, join and set_at_index choose a non-dummy span, and none of those span choices affects timestamp time, read type, ordering, clock equality, or update success. The surrounding data-race detector uses spans when rendering diagnostics, which is outside this value-operation port. SmallVec's inline capacity is likewise a storage optimization; this module preserves the logical vector length and trailing-zero invariant, not allocation strategy.

This does not model thread scheduling, synchronization, data-race reports, atomic operations, memory, or full Miri concurrency semantics.

inductive Miri.Concurrency.NaReadType : Type

The non-atomic read category packed into a vector timestamp.

• Read : NaReadType
• Retag : NaReadType

@[instance_reducible]

instance Miri.Concurrency.instDecidableEqNaReadType : DecidableEq NaReadType

Equations

• Miri.Concurrency.instDecidableEqNaReadType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Concurrency.instReprNaReadType : Repr NaReadType

Equations

• Miri.Concurrency.instReprNaReadType = { reprPrec := Miri.Concurrency.instReprNaReadType.repr }

def Miri.Concurrency.instReprNaReadType.repr : NaReadType → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instInhabitedNaReadType : Inhabited NaReadType

Equations

• Miri.Concurrency.instInhabitedNaReadType = { default := Miri.Concurrency.instInhabitedNaReadType.default }

inductive Miri.Concurrency.ClockError : Type

Errors corresponding to Rust conversion failures, checked timestamp overflow, and assertions/panics in the selected value operations.

• timestampOverflow : ClockError
• vectorIndexOverflow : ClockError
• setAtIndexWouldDecrease : ClockError
• mutableIndexOutOfBounds : ClockError

@[instance_reducible]

instance Miri.Concurrency.instDecidableEqClockError : DecidableEq ClockError

Equations

• Miri.Concurrency.instDecidableEqClockError x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Concurrency.instReprClockError : Repr ClockError

Equations

• Miri.Concurrency.instReprClockError = { reprPrec := Miri.Concurrency.instReprClockError.repr }

def Miri.Concurrency.instReprClockError.repr : ClockError → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instInhabitedClockError : Inhabited ClockError

Equations

• Miri.Concurrency.instInhabitedClockError = { default := Miri.Concurrency.instInhabitedClockError.default }

structure Miri.Concurrency.VectorIdx : Type

A clock index is exactly a Rust u32 value.

• value : Fin 4294967296

def Miri.Concurrency.instDecidableEqVectorIdx.decEq (x✝ x✝¹ : VectorIdx) : Decidable (x✝ = x✝¹)

Equations

• Miri.Concurrency.instDecidableEqVectorIdx.decEq { value := a } { value := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Concurrency.instDecidableEqVectorIdx : DecidableEq VectorIdx

Equations

• Miri.Concurrency.instDecidableEqVectorIdx = Miri.Concurrency.instDecidableEqVectorIdx.decEq

@[instance_reducible]

instance Miri.Concurrency.instReprVectorIdx : Repr VectorIdx

Equations

• Miri.Concurrency.instReprVectorIdx = { reprPrec := Miri.Concurrency.instReprVectorIdx.repr }

def Miri.Concurrency.instReprVectorIdx.repr : VectorIdx → Nat → Std.Format

Equations

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

def Miri.Concurrency.VectorIdx.ofU32 (value : Nat) (h : value < 4294967296) : VectorIdx

Construct the index associated with a Rust u32.

Equations

• Miri.Concurrency.VectorIdx.ofU32 value h = { value := ⟨value, h⟩ }

def Miri.Concurrency.VectorIdx.ofNat (value : Nat) : Except ClockError VectorIdx

Model Idx::new: converting a host index above u32::MAX panics upstream.

Equations

• Miri.Concurrency.VectorIdx.ofNat value = if h : value < 4294967296 then Except.ok { value := ⟨value, h⟩ } else Except.error Miri.Concurrency.ClockError.vectorIndexOverflow

def Miri.Concurrency.VectorIdx.toNat (index : VectorIdx) : Nat

Convert the index to its mathematical value.

Equations

• index.toNat = ↑index.value

@[simp]

theorem Miri.Concurrency.VectorIdx.toNat_ofU32 (value : Nat) (h : value < 4294967296) : (ofU32 value h).toNat = value

def Miri.Concurrency.maxTimestamp : Nat

The largest time encodable above a one-bit read type in a packed u32.

Equations

• Miri.Concurrency.maxTimestamp = 2147483647

structure Miri.Concurrency.VTimestamp : Type

A timestamp stores the exact unsigned 32-bit word 2 * time + readBit.

The Fin bound models the raw u32 range without truncating or dropping its retag bit. Rust equality and ordering compare time, not this whole word.

• packed : Fin 4294967296

@[instance_reducible]

instance Miri.Concurrency.instReprVTimestamp : Repr VTimestamp

Equations

• Miri.Concurrency.instReprVTimestamp = { reprPrec := Miri.Concurrency.instReprVTimestamp.repr }

def Miri.Concurrency.instReprVTimestamp.repr : VTimestamp → Nat → Std.Format

Equations

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

def Miri.Concurrency.VTimestamp.ZERO : VTimestamp

The all-zero timestamp.

Equations

• Miri.Concurrency.VTimestamp.ZERO = { packed := ⟨0, Miri.Concurrency.VTimestamp.ZERO._proof_1⟩ }

def Miri.Concurrency.VTimestamp.packedValue (timestamp : VTimestamp) : Nat

The raw packed u32 value as a natural number.

Equations

• timestamp.packedValue = ↑timestamp.packed

def Miri.Concurrency.VTimestamp.time (timestamp : VTimestamp) : Nat

Decode the timestamp by shifting away the low read-type bit.

Equations

• timestamp.time = ↑timestamp.packed / 2

def Miri.Concurrency.VTimestamp.readType (timestamp : VTimestamp) : NaReadType

Decode the low bit as a regular read or retag read.

Equations

• timestamp.readType = if ↑timestamp.packed % 2 = 0 then Miri.Concurrency.NaReadType.Read else Miri.Concurrency.NaReadType.Retag

def Miri.Concurrency.VTimestamp.encode (time : Nat) (readType : NaReadType) : Except ClockError VTimestamp

Encode time and read type, preserving the source's checked-multiply overflow.

Equations

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

def Miri.Concurrency.VTimestamp.ofTime (time : Nat) : Except ClockError VTimestamp

Encode a timestamp, returning overflow instead of wrapping its packed word.

Equations

• Miri.Concurrency.VTimestamp.ofTime time = Miri.Concurrency.VTimestamp.encode time Miri.Concurrency.NaReadType.Read

def Miri.Concurrency.VTimestamp.ofPacked (packed : Nat) (h : packed < 4294967296) : VTimestamp

The packed-word constructor, useful for faithful decoding of existing u32 values.

Equations

• Miri.Concurrency.VTimestamp.ofPacked packed h = { packed := ⟨packed, h⟩ }

def Miri.Concurrency.VTimestamp.sameTime (left right : VTimestamp) : Bool

Equality corresponding to Rust PartialEq: the packed read/retag bit is ignored.

Equations

• left.sameTime right = (left.time == right.time)

def Miri.Concurrency.VTimestamp.compare (left right : VTimestamp) : Ordering

Ordering corresponding to Rust Ord: only the decoded timestamp is compared.

Equations

• left.compare right = if left.time < right.time then Ordering.lt else if left.time > right.time then Ordering.gt else Ordering.eq

def Miri.Concurrency.VTimestamp.setTime (timestamp : VTimestamp) (time : Nat) : Except ClockError VTimestamp

Preserve the read type while replacing time; encoding overflow is an upstream panic.

Equations

• timestamp.setTime time = Miri.Concurrency.VTimestamp.encode time timestamp.readType

def Miri.Concurrency.VTimestamp.setReadType (timestamp : VTimestamp) (readType : NaReadType) : VTimestamp

Preserve time while replacing the packed read/retag bit.

Equations

• timestamp.setReadType Miri.Concurrency.NaReadType.Read = { packed := ⟨2 * timestamp.time, ⋯⟩ }
• timestamp.setReadType Miri.Concurrency.NaReadType.Retag = { packed := ⟨2 * timestamp.time + 1, ⋯⟩ }

def Miri.Concurrency.VTimestamp.maxForJoin (left right : VTimestamp) : VTimestamp

Rust r.max(l): the receiver is the other clock's timestamp, and Rust's Ord::max returns its second argument on ties, so the left/self timestamp wins.

Equations

• left.maxForJoin right = if right.time ≤ left.time then left else right

@[simp]

theorem Miri.Concurrency.VTimestamp.maxForJoin_left_on_time_tie (left right : VTimestamp) (sameTime : left.time = right.time) : left.maxForJoin right = left

@[simp]

theorem Miri.Concurrency.VTimestamp.time_setReadType (timestamp : VTimestamp) (readType : NaReadType) : (timestamp.setReadType readType).time = timestamp.time

@[simp]

theorem Miri.Concurrency.VTimestamp.sameTime_refl (timestamp : VTimestamp) : timestamp.sameTime timestamp = true

@[instance_reducible]

instance Miri.Concurrency.instBEqVTimestamp : BEq VTimestamp

Equations

• Miri.Concurrency.instBEqVTimestamp = { beq := Miri.Concurrency.VTimestamp.sameTime }

inductive Miri.Concurrency.VClock : Type

A vector clock is either empty or ends in a timestamp whose time is nonzero.

Its prefix may contain zero timestamps, including timestamp-zero retag reads. This representation enforces Miri's unique trailing-zero-free clock shape.

• zero : VClock

  The all-zero vector is represented only by the empty clock.

• nonzero (earlier : List VTimestamp) (last : VTimestamp) (last_time_nonzero : last.time ≠ 0) : VClock

  A canonical clock with arbitrary prefix and a nonzero final time.

def Miri.Concurrency.instReprVClock.repr : VClock → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Concurrency.instReprVClock : Repr VClock

Equations

• Miri.Concurrency.instReprVClock = { reprPrec := Miri.Concurrency.instReprVClock.repr }

@[instance_reducible]

instance Miri.Concurrency.instInhabitedVClock : Inhabited VClock

Equations

• Miri.Concurrency.instInhabitedVClock = { default := Miri.Concurrency.instInhabitedVClock.default }

def Miri.Concurrency.VClock.asList : VClock → List VTimestamp

The logical timestamp slice corresponding to the internal vector.

Equations

• Miri.Concurrency.VClock.zero.asList = []
• (Miri.Concurrency.VClock.nonzero a a_1 a_2).asList = a ++ [a_1]

def Miri.Concurrency.VClock.length (clock : VClock) : Nat

The logical number of stored entries.

Equations

• clock.length = clock.asList.length

def Miri.Concurrency.VClock.default : VClock

The all-zero vector clock.

Equations

• Miri.Concurrency.VClock.default = Miri.Concurrency.VClock.zero

def Miri.Concurrency.VClock.ofList (values : List VTimestamp) : VClock

Build a clock from a logical timestamp list, removing trailing time-zero values.

Equations

• Miri.Concurrency.VClock.ofList values = Miri.Concurrency.VClock.ofReversedList✝ values.reverse

def Miri.Concurrency.VClock.last? : VClock → Option VTimestamp

The last stored timestamp, when the clock is nonempty.

Equations

• Miri.Concurrency.VClock.zero.last? = none
• (Miri.Concurrency.VClock.nonzero a a_1 a_2).last? = some a_1

theorem Miri.Concurrency.VClock.last_time_nonzero (clock : VClock) : match clock.last? with | none => True | some timestamp => timestamp.time ≠ 0

The canonical last-entry invariant follows from the representation.

def Miri.Concurrency.VClock.index (clock : VClock) (index : VectorIdx) : VTimestamp

Read a clock entry; absent vector indices denote VTimestamp::ZERO.

Equations

• clock.index index = (Miri.Concurrency.VClock.listIndex?✝ clock.asList index.toNat).getD Miri.Concurrency.VTimestamp.ZERO

def Miri.Concurrency.VClock.newWithIndex (index : VectorIdx) (timestamp : VTimestamp) : VClock

Construct a clock containing only the supplied timestamp at one index. As upstream, any timestamp whose time is zero produces the empty vector, even a retag read.

Equations

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

def Miri.Concurrency.VClock.incrementIndex (clock : VClock) (index : VectorIdx) : Except ClockError VClock

Increment the timestamp at a known vector index. Packed-time overflow is returned explicitly instead of wrapping.

Equations

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

def Miri.Concurrency.VClock.join (left right : VClock) : VClock

Pointwise join, with the source's left/self raw timestamp chosen on equal times.

Equations

• left.join right = Miri.Concurrency.VClock.ofList (Miri.Concurrency.VClock.joinLists✝ left.asList right.asList)

def Miri.Concurrency.VClock.setAtIndex (clock other : VClock) (index : VectorIdx) : Except ClockError VClock

Replace one coordinate by the corresponding timestamp of other. This models the source assertion that the coordinate may only increase; the assertion failure is represented explicitly as setAtIndexWouldDecrease.

Equations

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

def Miri.Concurrency.VClock.setZeroVector (_clock : VClock) : VClock

Clear all clock entries.

Equations

• _clock.setZeroVector = Miri.Concurrency.VClock.zero

def Miri.Concurrency.VClock.applyReadType (clock : VClock) (index : VectorIdx) (readType : NaReadType) : Except ClockError VClock

Read the packed read type at an existing coordinate and preserve its time.

Equations

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

def Miri.Concurrency.VClock.clone (clock : VClock) : VClock

Clone a clock, including every raw read-type bit.

Equations

• clock.clone = clock

def Miri.Concurrency.VClock.cloneFrom (_clock source : VClock) : VClock

Clone-from has the same logical behavior as replacing the value.

Equations

• _clock.cloneFrom source = source

def Miri.Concurrency.VClock.equalLists : List VTimestamp → List VTimestamp → Bool

Clock equality corresponding to Rust's derived VClock equality and timestamp PartialEq: length and every decoded time must agree; read/retag bits are ignored.

Equations

• Miri.Concurrency.VClock.equalLists [] [] = true
• Miri.Concurrency.VClock.equalLists (left :: leftRest) (right :: rightRest) = (left.sameTime right && Miri.Concurrency.VClock.equalLists leftRest rightRest)
• Miri.Concurrency.VClock.equalLists x✝¹ x✝ = false

@[irreducible]

def Miri.Concurrency.VClock.compareCommon (order : Ordering) : List VTimestamp → List VTimestamp → Option Ordering

Compare the common vector prefix using Miri's partial-order accumulation rule.

Equations

• Miri.Concurrency.VClock.compareCommon Ordering.eq (left :: leftRest) (right :: rightRest) = Miri.Concurrency.VClock.compareCommon (left.compare right) leftRest rightRest
• Miri.Concurrency.VClock.compareCommon Ordering.lt (left :: leftRest) (right :: rightRest) = none
• Miri.Concurrency.VClock.compareCommon Ordering.lt (left :: leftRest) (right :: rightRest) = Miri.Concurrency.VClock.compareCommon Ordering.lt leftRest rightRest
• Miri.Concurrency.VClock.compareCommon Ordering.gt (left :: leftRest) (right :: rightRest) = none
• Miri.Concurrency.VClock.compareCommon Ordering.gt (left :: leftRest) (right :: rightRest) = Miri.Concurrency.VClock.compareCommon Ordering.gt leftRest rightRest
• Miri.Concurrency.VClock.compareCommon order x✝¹ x✝ = some order

def Miri.Concurrency.VClock.partialCompare (left right : VClock) : Option Ordering

Partial componentwise vector-clock comparison.

Equations

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

def Miri.Concurrency.VClock.lt (left right : VClock) : Bool

Rust's optimized strict-less-than comparison.

Equations

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

def Miri.Concurrency.VClock.le (left right : VClock) : Bool

Rust's optimized less-than-or-equal comparison.

Equations

• left.le right = (decide (left.length ≤ right.length) && Miri.Concurrency.VClock.allLE✝ left.asList right.asList)

def Miri.Concurrency.VClock.gt (left right : VClock) : Bool

Rust's optimized strict-greater-than comparison.

Equations

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

def Miri.Concurrency.VClock.ge (left right : VClock) : Bool

Rust's optimized greater-than-or-equal comparison.

Equations

• left.ge right = (decide (left.length ≥ right.length) && Miri.Concurrency.VClock.allGE✝ left.asList right.asList)

def Miri.Concurrency.VClock.fromTimestamps (timestamps : List VTimestamp) : VClock

Build a read-only clock from timestamps, canonicalizing only trailing time-zero entries.

Equations

• Miri.Concurrency.VClock.fromTimestamps timestamps = Miri.Concurrency.VClock.ofList timestamps

@[simp]

theorem Miri.Concurrency.VClock.length_zero : default.length = 0

theorem Miri.Concurrency.VClock.increment_keeps_canonical (clock : VClock) (index : VectorIdx) (next : VClock) (_h : clock.incrementIndex index = Except.ok next) : match next.last? with | none => True | some timestamp => timestamp.time ≠ 0

theorem Miri.Concurrency.VClock.join_keeps_canonical (left right : VClock) : match (left.join right).last? with | none => True | some timestamp => timestamp.time ≠ 0

@[instance_reducible]

instance Miri.Concurrency.instBEqVClock : BEq VClock

Equations

• Miri.Concurrency.instBEqVClock = { beq := fun (left right : Miri.Concurrency.VClock) => Miri.Concurrency.VClock.equalLists left.asList right.asList }