Unsound axiom found for mmio

[hiroki-chen]

/// ostd/specs/mm/frame/meta_owners.rs#L67-L72
pub broadcast axiom fn axiom_mmio_usage_iff_mmio_paddr(slot: MetaSlotOwner)
    ensures
        (#[trigger] slot.usage == PageUsage::MMIO) <==> is_mmio_paddr(
            meta_to_frame(slot.slot_vaddr),
        ),
;

slot.usage == MMIO
          ↓ axiom_mmio_usage_iff_mmio_paddr
  is_mmio_paddr(pa)

  Frame::from_unused(pa, ...)
          ↓ REF_COUNT_UNUSED
  slot.usage = Frame
          ↓ axiom
  !is_mmio_paddr(pa)

So if you construct a page following the above path then you obtain is_mmio_paddr(pa) &&!is_mmio_paddr(pa) ==> false and via ex falso quodlibet we can prove anything!!!

@rikosellic

[hiroki-chen]

As is_mmio_paddr only tracks if a page is not amenable to refcounting.

[rikosellic]

This is indeed unsound. The MetaSlot design needs an overhaul.