theorem Miri.Concurrency.Verification.release_fence_preserves_metadata (before : ThreadClockSet) : have after := before.applyReleaseFence; after.fenceRelease = before.clock ∧ after.clock = before.clock ∧ after.fenceAcquire = before.fenceAcquire ∧ after.writeSeqCst = before.writeSeqCst ∧ after.readSeqCst = before.readSeqCst

The release-fence transition copies the current clock and preserves the remaining per-thread synchronization metadata.

theorem Miri.Concurrency.Verification.acquire_fence_preserves_metadata (before : ThreadClockSet) : have after := before.applyAcquireFence; after.clock = before.clock.join before.fenceAcquire ∧ after.fenceAcquire = before.fenceAcquire ∧ after.fenceRelease = before.fenceRelease

The acquire-fence transition joins its pending clock and preserves the other synchronization metadata.

theorem Miri.Concurrency.Verification.atomic_access_rejects_incompatible_write (cell : MemoryCellClocks) (thread : ThreadClockSet) (oldAtomic : AtomicMemoryCellClocks) (newSize : ByteSize) (hOldSize : oldAtomic.size ≠ some newSize) (hReads : oldAtomic.readVector.le thread.clock = false) (hWrites : oldAtomic.writeVector.le thread.clock = false) (hCell : cell.atomicOps = some oldAtomic) : cell.atomicAccess thread newSize true = Except.error DataRaceResult.race

Incompatible concurrent atomic sizes reject a write access.