Skip to content

[Certora] side effect of calling settlementFee in a rule #932

Description

@MathisGD

P2 Badge Cover market-creating takes in fee spread proof

When take is the first interaction with an uncreated market, this pre-call to settlementFee reverts because marketState[id].tickSpacing == 0; in CVL, a plain reverting call prunes the path, so settlementFeeSpreadBounds never checks market-creating takes that initialize and charge the default settlement fee. Consider touching/creating the market in the rule before reading the fee, or otherwise adding a separate rule for the first-take path.

Useful? React with 👍 / 👎.

Originally posted by @chatgpt-codex-connector[bot] in #931

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type
    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions