Skip to content

[Certora] Properties about markets in MorphoMarketV1AdapterV2 #959

Description

@QGarchery

Property: show that markets with supply shares > 0, or some allocation, have the same loanToken as the vault, and have the adaptiveCurveIrm.
Similar to vault v1 where this is the invariant enabledHasConsistentAsset.

This property is useful for the vault exit bundles, since it allows to show that markets that you interact with are consistent. This is because markets such that shares converted to assets are 0 are skipped in that bundles contract. So if it's not skipped, then we know that shares are not 0, so we have the property above

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions