Track the kit and lqt checker owns on the ledger

[gkaracha]

This includes kit stored in the cfmm, kit from winning bids for liquidation auctions, and liquidity tokens stored in the cfmm.

This change allows us to check more invariants:

1. total_kit_on_the_ledger = state.parameters.circulating_kit
2. checker's_kit_on_the_ledger + 1mukit >= state.cfmm.kit
3. checker's_lqt_on_the_ledger + 1n = state.cfmm.lqt

NOTE 1: The +1s are needed because the cfmm keeps 1 phantom token per category so that it never has to divide by zero.)

NOTE 2: The second assertion is an inequality because checker also stores kit from bids.

This PR

• Extends assert_checker_invariants to additionally check the above three invariants.
• Adds a call to assert_checker_invariants at the beginning and end of every entrypoint (strict or lazy) and view.
• Adds extra assertions in the cfmm-related entrypoints when we know that the total amount of kit and/or lqt on the fa2 ledger should be preserved or change by a fixed amount.

Because of the additional strictness I had to change several tests; until now we'd frequently create input states that violate some or all of these invariants.

[purcell]

This is nice, and makes sense to me! I read the notes in the other issue and agree it's better if we can track everything in the ledgers.

Tangentially related: are there any dexter-like re-entrancy cases possible now? Do we need to do a pass to check for that?

Separately, don't worry about manually adding [skip ci] notes in commit messages. They're a pain to clean up later and not really necessary now IMO: we have essentially unmetered Actions now, and cachix caching for the nix parts.

[purcell]

Unsure whether to merge this, because it's mostly marked "wip". 😄

[gkaracha]

Tangentially related: are there any dexter-like re-entrancy cases possible now? Do we need to do a pass to check for that?

Ah, that's a good question. I did a pass for that some time ago and I couldn't think of any cases like that being possible for checker. Checker almost always interacts directly with Tezos.sender so it's difficult to trick it. However, I said almost because for example when we deactivate a burrow we ask for an address to send the tez to, and one could maliciously pass checker's. Let's do a pass to check for weaknesses, still, I'd say, I am not yet convinced we are secure in that respect.

Separately, don't worry about manually adding [skip ci] notes in commit messages. They're a pain to clean up later and not really necessary now IMO: we have essentially unmetered Actions now, and cachix caching for the nix parts.

Good to know! :+1: The reason I used to many in this PR is because by changing the assertion first many places broke, so most of the commits were incremental patches, in which the tests would fail. My plan was to use the squash-and-merge when done.

Unsure whether to merge this, because it's mostly marked "wip".

Ha, it's not WIP anymore :smile: I'll squash it and merge it myself, thanks for having a look!