In this paper, we address the reentrancy vulnerabilities in smart contracts by two program logics. We first propose a coarse-grained logic that extends standard Hoare logic by a proof rule for reentry trigger command. We prove this logic is sound and complete. We propose another fine-grained logic that considers reentry triggers as entry and exit points of a function. For verifying coarse-grained specifications, these two logics have the same expressiveness, and we can derive coarse-grained judgments from fine-grained ones. In comparison, the fine-grained logic is more useful for fine-grained specifications. We use a toy language to demonstrate our results and formalize all definitions and proofs in Coq.