onomyprotocol / market-audit Goto Github PK

This expression will evaluate to false when attempting to fire Close() action over an already existing stop position. I.e. given an existing stop position P, in TLA+ terms, action Close(P) is not enabled ( = cannot become part of a valid behaviour).

This means that a DEX implementation following this market model will not support cancelling of stop orders.

This is caused by line 152, where a new stop order is added to orders collection attached to <bidCoin, askCoin> pair, while here we attempt to remove it from a orders collection attached to <askCoin, bidCoin> pair.

Following #9, we've noticed that the behavior of Close is likely underspecified. Specifically, it appears that Close merely removes a position from limits/stops, but does not perform any account balance update. According to our understanding, closing a position should decrease the balance associated with bidCoin and increase the balance associated with askCoin (across different accounts).