Abstract. Rowhammer is a hardware vulnerability in dynamic random-access memory (DRAM) in which repeated accesses to one or more aggressor rows can induce bit-flips in nearby victim rows. This phenomenon violates a core assumption of conventional programming language semantics: that reading from or writing to one memory location does not modify others. Despite the security importance of this phenomenon, there is no widely established formal framework connecting Rowhammer faults with program behaviour. This makes it difficult to reason rigorously about the efficacy of proposed Rowhammer defences and the program-level guarantees they provide. To address this gap, we present a probabilistic small-step operational semantics for an idealised imperative language subject to Rowhammer-style faults. The semantics is high-level in that it abstracts from DRAM internals and semiconductor physics. A general probabilistic fault model parameterises the semantics, representing Rowhammer-style faults by assigning probabilities to bit-flips during read or write operations within a specified victim region. The resulting distributions are propagated through programs using the standard monadic structure of probabilistic computation. As a case study, we formalise physical separation, a well-known defence that places program variables sufficiently far apart in physical memory that an access to one variable cannot disturb another. We prove a distribution-independent semantic collapse theorem: for every finite execution, including prefixes of terminating and non-terminating executions, the protected projection of the probabilistic Rowhammer semantics is the Dirac distribution of the corresponding Rowhammer-free execution. Furthermore, we develop an observation-parametric account of secure information flow. Non-interference is expressed as a hyperproperty comparing the distributions of low observations from low-equivalent initial memories. Under physical separation, ordinary non-interference and probability-sensitive Rowhammer non-interference coincide for every observer of protected behaviour. Consequently, physical separation preserves non-interference for every admissible fault model, while every Rowhammer non-interference violation reflects a violation already present in the Rowhammer-free semantics. The development is fully mechanised in Lean using mathlib, relying on no unfinished proofs or problem-specific axioms.