Sounds a lot like group borrowing from Valen, but that one still has annotations like `entity in world.entities[] mut`. Are you tracking the same things implicitly with post conditions?