Graded Hoare Logic and Its Categorical Semantics