theorem Miri.Concurrency.WeakMemoryVerification.store_impl_preserves_limit (buffer : StoreBuffer Nat) (value : Nat) (index : VectorIdx) (clock : VClock) (isSeqCst : Bool) (syncClock : VClock) : (buffer.storeImpl value index clock isSeqCst syncClock).newer.length < STORE_BUFFER_LIMIT

Every store transition retains the pinned implementation's capacity bound.

theorem Miri.Concurrency.WeakMemoryVerification.source_fetch_has_candidate (buffer : StoreBuffer Nat) (isSeqCst : Bool) (clocks : ThreadClockSet) : buffer.fetchChoices isSeqCst clocks ≠ []

The source choice relation never gets stuck: the initial/latest entry is included even when it is the first element that closes the inclusive prefix.