Explain all invariants in BCP, provide some formal proofs why BPC works. Also TON Core rewrited this a lot, and we need to check that and document