Bluebell: An Alliance of Relational Lifting and Independence For Probabilistic Reasoning
summary
Bluebell is a program logic that unifies unary and relational proofs by adding a joint conditioning modality that encodes conditional independence and relational liftings. It recovers standard probabilistic separation logic rules (including the probabilistic separation star frame) and PRHL-style coupling proofs, lets one combine two different alignments of samples using independence, and removes ad hoc XOR axioms used in past work. The prototype yields the expected relational liftings on textbook examples like one-time-pad and paired-sample programs.
AI-written summary · about