Closed hjorthjort closed 3 years ago
DEXTER-ADDLIQUIDITY-NEGATIVE-SPEC doesn't cover:
DEXTER-ADDLIQUIDITY-NEGATIVE-SPEC
notBool (Amount *Int TokenAmount) %Int XtzAmount =/=Int 0
DEXTER-REMOVELIQUIDITY-NEGATIVE-SPEC doesn't cover:
DEXTER-REMOVELIQUIDITY-NEGATIVE-SPEC
notBool (MinTokensWithdrawn <=Int (LqtBurned *Int TokenAmount) /Int OldLqt)
These are covered because it occurs only when OldLqt < LqtBurned
notBool #IsLegalMutezValue((LqtBurned *Int XtzAmount) /Int OldLqt)
notBool TokenAmount >=Int (LqtBurned *Int TokenAmount) /Int OldLqt
notBool XtzAmount >=Int (LqtBurned *Int XtzAmount) /Int OldLqt
The following specs don't deal with target entrypoint not existing
DEXTER-ADDLIQUIDITY-POSITIVE-SPEC
DEXTER-TOKENTOXTZ-FA*-NEGATIVE-*-SPEC
DEXTER-XTZTOTOKEN-FA*-NEGATIVE-*-SPEC
DEXTER-TOKENTOTOKEN-POSITIVE-SPEC
DEXTER-ADDLIQUIDITY-NEGATIVE-SPECdoesn't cover:notBool (Amount *Int TokenAmount) %Int XtzAmount =/=Int 0DEXTER-REMOVELIQUIDITY-NEGATIVE-SPECdoesn't cover:notBool (MinTokensWithdrawn <=Int (LqtBurned *Int TokenAmount) /Int OldLqt)These are covered because it occurs only when OldLqt < LqtBurned
notBool #IsLegalMutezValue((LqtBurned *Int XtzAmount) /Int OldLqt)notBool TokenAmount >=Int (LqtBurned *Int TokenAmount) /Int OldLqtnotBool XtzAmount >=Int (LqtBurned *Int XtzAmount) /Int OldLqtThe following specs don't deal with target entrypoint not existing
DEXTER-ADDLIQUIDITY-POSITIVE-SPECDEXTER-REMOVELIQUIDITY-NEGATIVE-SPECDEXTER-TOKENTOXTZ-FA*-NEGATIVE-*-SPECDEXTER-XTZTOTOKEN-FA*-NEGATIVE-*-SPECDEXTER-TOKENTOTOKEN-POSITIVE-SPEC