Proofs directly about the checked size arithmetic.

theorem Miri.ABI.Verification.checkedAdd_success_below_bound {α : Type} [HasDataLayout α] (size offset : Size) (cx : α) (value : Size) : size.checkedAdd offset cx = some value → value.bytes < (HasDataLayout.dataLayout cx).objSizeBound

Every successful target-bounded addition is below the exclusive object-size bound.

theorem Miri.ABI.Verification.checkedAdd_rejects_obj_size_bound_16 : (Size.ofBytes 32767).checkedAdd (Size.ofBytes 1) { endian := Endian.little, pointerWidth := PointerWidth.w16 } = none

A 16-bit target rejects a result equal to its 2^15-byte exclusive bound.