feat(formal): grow P-3 to a real borrow graph (loan edges + move-locality)

feat(formal): grow P-3 to a real borrow graph (loan edges + move-locality) #1202