CONSTANTS
    G1 = g1
    G2 = g2
    A1 = a1
    NoArtifact = noArtifact
    Generations <- GenerationsFixture
    Artifact = a1

SPECIFICATION Spec
CHECK_DEADLOCK FALSE

INVARIANTS
    TypeOK
    LeaseBindingConsistent
    MountedGenerationLeased
    LeasedArtifactPublished
    GCExcludesLeases
    ReplacementOnlyDuringGC
    ForeignStagePreserved
    OwnedStageRequiresIntent