This artifact contains an Isabelle/HOL formalisation of an extension of Probabilistic Separation Logic and its soundness proof corresponding to Section 3.2, Section 4, and Appendix A of the paper "Combining Classical and Probabilistic Independence Reasoning to Verify the Security of Oblivious Algorithms". We have tested it with Isabelle2022 on Windows and MacOS. We also provide a Linux VM including all the codes and dependency.