Checked Lean model of the pinned rustc allocation initialization mask.

@[reducible, inline]

abbrev Miri.Memory.InitMaskError : Type

Equations

• Miri.Memory.InitMaskError = Miri.Memory.MemoryError

structure Miri.Memory.InitMaskMaterialized : Type

• blocks : Array UInt64

def Miri.Memory.instDecidableEqInitMaskMaterialized.decEq (x✝ x✝¹ : InitMaskMaterialized) : Decidable (x✝ = x✝¹)

Equations

• Miri.Memory.instDecidableEqInitMaskMaterialized.decEq { blocks := a } { blocks := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Memory.instDecidableEqInitMaskMaterialized : DecidableEq InitMaskMaterialized

Equations

• Miri.Memory.instDecidableEqInitMaskMaterialized = Miri.Memory.instDecidableEqInitMaskMaterialized.decEq

def Miri.Memory.instReprInitMaskMaterialized.repr : InitMaskMaterialized → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Memory.instReprInitMaskMaterialized : Repr InitMaskMaterialized

Equations

• Miri.Memory.instReprInitMaskMaterialized = { reprPrec := Miri.Memory.instReprInitMaskMaterialized.repr }

inductive Miri.Memory.InitMaskBlocks : Type

• Lazy (state : Bool) : InitMaskBlocks
• Materialized (blocks : InitMaskMaterialized) : InitMaskBlocks

def Miri.Memory.instDecidableEqInitMaskBlocks.decEq (x✝ x✝¹ : InitMaskBlocks) : Decidable (x✝ = x✝¹)

Equations

• Miri.Memory.instDecidableEqInitMaskBlocks.decEq (Miri.Memory.InitMaskBlocks.Lazy a) (Miri.Memory.InitMaskBlocks.Lazy b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Miri.Memory.instDecidableEqInitMaskBlocks.decEq (Miri.Memory.InitMaskBlocks.Lazy state) (Miri.Memory.InitMaskBlocks.Materialized blocks) = isFalse ⋯
• Miri.Memory.instDecidableEqInitMaskBlocks.decEq (Miri.Memory.InitMaskBlocks.Materialized blocks) (Miri.Memory.InitMaskBlocks.Lazy state) = isFalse ⋯
• Miri.Memory.instDecidableEqInitMaskBlocks.decEq (Miri.Memory.InitMaskBlocks.Materialized a) (Miri.Memory.InitMaskBlocks.Materialized b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Memory.instDecidableEqInitMaskBlocks : DecidableEq InitMaskBlocks

Equations

• Miri.Memory.instDecidableEqInitMaskBlocks = Miri.Memory.instDecidableEqInitMaskBlocks.decEq

@[instance_reducible]

instance Miri.Memory.instReprInitMaskBlocks : Repr InitMaskBlocks

Equations

• Miri.Memory.instReprInitMaskBlocks = { reprPrec := Miri.Memory.instReprInitMaskBlocks.repr }

def Miri.Memory.instReprInitMaskBlocks.repr : InitMaskBlocks → Nat → Std.Format

Equations

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

structure Miri.Memory.InitMask : Type

• blocks : InitMaskBlocks
• len : ABI.Size

def Miri.Memory.instDecidableEqInitMask.decEq (x✝ x✝¹ : InitMask) : Decidable (x✝ = x✝¹)

Equations

• Miri.Memory.instDecidableEqInitMask.decEq { blocks := a, len := a_1 } { blocks := b, len := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Memory.instDecidableEqInitMask : DecidableEq InitMask

Equations

• Miri.Memory.instDecidableEqInitMask = Miri.Memory.instDecidableEqInitMask.decEq

def Miri.Memory.instReprInitMask.repr : InitMask → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Memory.instReprInitMask : Repr InitMask

Equations

• Miri.Memory.instReprInitMask = { reprPrec := Miri.Memory.instReprInitMask.repr }

inductive Miri.Memory.InitChunk : Type

• Init (start finish : ABI.Size) : InitChunk
• Uninit (start finish : ABI.Size) : InitChunk

@[instance_reducible]

instance Miri.Memory.instDecidableEqInitChunk : DecidableEq InitChunk

Equations

• Miri.Memory.instDecidableEqInitChunk = Miri.Memory.instDecidableEqInitChunk.decEq

def Miri.Memory.instDecidableEqInitChunk.decEq (x✝ x✝¹ : InitChunk) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Memory.instDecidableEqInitChunk.decEq (Miri.Memory.InitChunk.Init start finish) (Miri.Memory.InitChunk.Uninit start_1 finish_1) = isFalse ⋯
• Miri.Memory.instDecidableEqInitChunk.decEq (Miri.Memory.InitChunk.Uninit start finish) (Miri.Memory.InitChunk.Init start_1 finish_1) = isFalse ⋯

@[instance_reducible]

instance Miri.Memory.instReprInitChunk : Repr InitChunk

Equations

• Miri.Memory.instReprInitChunk = { reprPrec := Miri.Memory.instReprInitChunk.repr }

def Miri.Memory.instReprInitChunk.repr : InitChunk → Nat → Std.Format

Equations

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

structure Miri.Memory.InitChunkIter : Type

• initMask : InitMask
• isInit : Bool
• start : ABI.Size
• finish : ABI.Size

structure Miri.Memory.InitCopy : Type

• initial : Bool
• ranges : Array UInt64

def Miri.Memory.instDecidableEqInitCopy.decEq (x✝ x✝¹ : InitCopy) : Decidable (x✝ = x✝¹)

Equations

• Miri.Memory.instDecidableEqInitCopy.decEq { initial := a, ranges := a_1 } { initial := b, ranges := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Miri.Memory.instDecidableEqInitCopy : DecidableEq InitCopy

Equations

• Miri.Memory.instDecidableEqInitCopy = Miri.Memory.instDecidableEqInitCopy.decEq

@[instance_reducible]

instance Miri.Memory.instReprInitCopy : Repr InitCopy

Equations

• Miri.Memory.instReprInitCopy = { reprPrec := Miri.Memory.instReprInitCopy.repr }

def Miri.Memory.instReprInitCopy.repr : InitCopy → Nat → Std.Format

Equations

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

def Miri.Memory.InitMaskMaterialized.bitIndex (offset : ABI.Size) : Nat × Nat

Equations

• Miri.Memory.InitMaskMaterialized.bitIndex offset = (Miri.Memory.sizeBytes✝ offset / Miri.Memory.blockSize✝, Miri.Memory.sizeBytes✝ offset % Miri.Memory.blockSize✝)

def Miri.Memory.InitChunk.isInit : InitChunk → Bool

Equations

• (Miri.Memory.InitChunk.Init a a_1).isInit = true
• (Miri.Memory.InitChunk.Uninit a a_1).isInit = false

def Miri.Memory.InitChunk.range (chunk : InitChunk) : Except InitMaskError AllocRange

Equations

• (Miri.Memory.InitChunk.Init a a_1).range = Miri.Memory.AllocRange.fromEndpoints a a_1
• (Miri.Memory.InitChunk.Uninit a a_1).range = Miri.Memory.AllocRange.fromEndpoints a a_1

def Miri.Memory.InitChunkIter.next? (iter : InitChunkIter) : Except InitMaskError (Option (InitChunk × InitChunkIter))

Equations

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

def Miri.Memory.InitCopy.noBytesInit (defined : InitCopy) : Bool

Equations

• defined.noBytesInit = (!defined.initial && defined.ranges.size == 1)

def Miri.Memory.InitMask.new (size : ABI.Size) (state : Bool) : InitMask

Equations

• Miri.Memory.InitMask.new size state = { blocks := Miri.Memory.InitMaskBlocks.Lazy state, len := size }

def Miri.Memory.InitMask.materializedBlockCount (self : InitMask) : Nat

Equations

• self.materializedBlockCount = match self.blocks with | Miri.Memory.InitMaskBlocks.Lazy state => 0 | Miri.Memory.InitMaskBlocks.Materialized blocks => blocks.blocks.size

def Miri.Memory.InitMask.materializedWords (self : InitMask) : Option (Array UInt64)

Equations

• self.materializedWords = match self.blocks with | Miri.Memory.InitMaskBlocks.Lazy state => none | Miri.Memory.InitMaskBlocks.Materialized blocks => some blocks.blocks

def Miri.Memory.InitMask.get (self : InitMask) (index : ABI.Size) : Except InitMaskError Bool

Equations

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

def Miri.Memory.InitMask.isRangeInitialized (self : InitMask) (range : AllocRange) : Except InitMaskError (Except AllocRange Unit)

Equations

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

def Miri.Memory.InitMask.setRange (self : InitMask) (range : AllocRange) (newState : Bool) : Except InitMaskError InitMask

Equations

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

def Miri.Memory.InitMask.rangeAsInitChunks (self : InitMask) (range : AllocRange) : Except InitMaskError InitChunkIter

Equations

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

def Miri.Memory.InitMask.collectChunks (iter : InitChunkIter) : Except InitMaskError (Array InitChunk)

Equations

• Miri.Memory.InitMask.collectChunks iter = Miri.Memory.InitMask.collectChunksAux✝ iter (Miri.Memory.sizeBytes✝ iter.finish - Miri.Memory.sizeBytes✝ iter.start + 1)

def Miri.Memory.InitMask.prepareCopy (self : InitMask) (range : AllocRange) : Except InitMaskError InitCopy

Equations

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

def Miri.Memory.InitMask.applyCopy (self : InitMask) (defined : InitCopy) (range : AllocRange) (repeatCount : UInt64) : Except InitMaskError InitMask

Equations

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

theorem Miri.Memory.InitMask.new_has_no_materialized_blocks (size : ABI.Size) (state : Bool) : (new size state).materializedBlockCount = 0

theorem Miri.Memory.InitMask.lazy_get (size index : ABI.Size) (state : Bool) : (new size state).get index = Except.ok state

theorem Miri.Memory.InitMask.lazy_initialized_query (size : ABI.Size) (range : AllocRange) (finish : ABI.Size) (hEnd : range.endExclusive = Except.ok finish) (hInBounds : finish.bytes ≤ size.bytes) : (new size true).isRangeInitialized range = Except.ok (Except.ok ())

theorem Miri.Memory.InitMask.lazy_uninitialized_query (size : ABI.Size) (range : AllocRange) (finish : ABI.Size) (hEnd : range.endExclusive = Except.ok finish) (hInBounds : finish.bytes ≤ size.bytes) : (new size false).isRangeInitialized range = Except.ok (Except.error range)

theorem Miri.Memory.InitMask.full_overwrite_stays_lazy (size finish : ABI.Size) (oldState newState : Bool) (range : AllocRange) (hEnd : range.endExclusive = Except.ok finish) (hStart : range.start.bytes = 0) (hFull : size.bytes ≤ finish.bytes) : (new size oldState).setRange range newState = Except.ok (new finish newState)

def Miri.Memory.InitMask.WriteProof.WellFormed (mask : InitMask) : Prop

Equations

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

theorem Miri.Memory.InitMask.WriteProof.set_range_exists (mask : InitMask) (range : AllocRange) (finish : ABI.Size) (state : Bool) (valid : WellFormed mask) (endpoint : range.endExclusive = Except.ok finish) (nonempty : range.start.bytes.toNat < finish.bytes.toNat) (inBounds : finish.bytes.toNat ≤ mask.len.bytes.toNat) : ∃ (updated : InitMask), mask.setRange range state = Except.ok updated ∧ updated.len = mask.len ∧ WellFormed updated