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

feat(formal): grow P-3 to a real borrow graph (loan edges + move-loca… #905