{"id":"903f38da-8b92-4097-9098-5290abed9f7c","arxiv_id":"2607.10314","paper_version":1,"verdict":"ACCEPT","confidence":"HIGH","novelty_score":7.5,"correctness_risk":"low","formal_verification":"full","parameter_count":0,"one_line_summary":"Under physical separation, every finite Rowhammer execution projects to the Dirac distribution of the ordinary deterministic run on protected memory, control and access traces, fully mechanised in Lean.","lead":"This paper builds a fully Lean-checked probabilistic operational semantics for programs under Rowhammer bit-flips, abstracting away DRAM physics. It proves that physically separating variables collapses the faulty semantics to ordinary deterministic behaviour on protected state and preserves non-interference for every admissible fault model.","discovery_kind":"new_method","skeptic_critique":{"model":"grok-4.5","headline":"No significant objection identified","rationale":"The reader correctly identifies Theorem 6.1 as the strongest claim and F3–F4 as the weakest modelling assumption. That assumption is stated openly (§5.1, §9) as a genuine restriction that excludes charge accumulation and refresh-cycle effects; the theorems are therefore conditional on the abstract contract, not on a claim of physical completeness. Because the development is fully machine-checked, the usual soundness doubts that accompany pen-and-paper operational semantics do not arise. The concrete verification step above is the natural residual check rather than a test of a suspected error. Consequently the ACCEPT verdict stands without adjustment.","tokens_in":30613,"tokens_out":393,"duration_ms":4705,"concrete_test":"Independently re-check the Lean statement of physical_separation_sound (and its supporting lemmas stepRHHat_agree / runRHTrace_protected) against the paper’s informal statement of Theorem 6.1; confirm that the axiom audit reports only propext, Classical.choice and Quot.sound, and that the no-fault embedding (runRHTrace_noFlip) holds without safety or well-formedness assumptions.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim (Theorem 6.1) is a fully mechanised, distribution-independent collapse result under an explicitly stated abstract fault contract. The history-freeness/stationarity restriction (F3–F4) is the modelling boundary the paper itself flags; it does not create an internal inconsistency or a hidden gap in the proved statement. The protected-view projection, frame-locality, well-formedness and safe_disjoint hypotheses are necessary and sufficient for the Dirac equality, and the non-interference results are direct corollaries of that equality rather than a second simulation. No load-bearing flaw in the argument as formulated was found.","agreement_with_reader":"agree"},"referee_report":{"model":"grok-4.5","summary":"The paper gives a probabilistic small-step operational semantics for a WHILE language under Rowhammer-style faults. Faults are isolated at the read/write interface via an abstract, history-free, frame-local probability kernel; the rest of the semantics is lifted monadically. The main result (Theorem 6.1) is a distribution-independent collapse: under physical separation and program well-formedness, the protected projection of every finite n-step Rowhammer run is exactly the Dirac distribution of the ordinary deterministic run (residual program, protected memory, access trace). Observation-parametric non-interference is then shown to be preserved and reflected by the same collapse. The entire development is mechanised in Lean 4/mathlib with an explicit axiom audit (only propext, Classical.choice, Quot.sound).","tokens_in":30736,"tokens_out":748,"duration_ms":6100,"significance":"This is a genuine bridge between DRAM disturbance research and programming-language security. The collapse theorem is distribution-free, covers terminating and non-terminating prefixes, and is fully machine-checked; the non-interference results are direct corollaries rather than a second simulation. The small fault-kernel interface is language-parametric in principle and recovers ordinary semantics by the no-fault embedding (Theorem 6.4). For a venue that values mechanised semantics and hyperproperties, the contribution is substantial and the artefact is a clear strength.","major_comments":[],"minor_comments":[{"comment":"Section 5.1, clauses (F3)–(F4): history-freeness and stationarity are correctly flagged as modelling restrictions that exclude charge accumulation and refresh effects. A short forward pointer in the introduction or abstract to the future-work discussion in Section 10 would help readers who expect a device-level model.","section":"§5.1"},{"comment":"Section 5.6: mixed termination is illustrated but limiting probabilities of divergence are not mechanised. The finite-step approach is sufficient for the proved theorems; a one-sentence clarification that the paper makes no claim about eventual termination probabilities would avoid over-reading.","section":"§5.6"},{"comment":"Section 8.1: the four concrete observers are useful, but the text already notes that the fourth is not classical termination-insensitive NI. Making that caveat slightly more prominent (e.g., in the definition list) would prevent mis-citation.","section":"§8.1"},{"comment":"Figures 2–4 and the distance-based SeparationModel instance are clear; a brief remark that numerical address distance is only a witness, not a claim about physical DRAM geometry, already appears but could be repeated near the first use of the concrete instance.","section":"§5.3"},{"comment":"A few typographical nits (e.g., spacing around ‘i.e.’, occasional long lines in Lean excerpts) do not affect readability but could be cleaned in production.","section":null}],"recommendation":"accept","confidential_remarks":"The reader’s and skeptic’s assessments match my own: the central claim is sound, mechanised, and free of load-bearing gaps. History-freeness is a deliberate modelling boundary, not a hidden flaw. Fit for a PL/formal-methods venue is excellent; the paper is ready for acceptance with only light copy-editing."},"author_rebuttal":null,"desk_editor":{"model":"grok-4.5","letter":"This is the first reusable operational interface that lets standard PL tools talk about Rowhammer without modelling DRAM physics. The real payload is Theorem 6.1: under frame-locality, physical separation and well-formedness, the protected view of every finite probabilistic run is exactly the Dirac of the ordinary deterministic run (residual program, protected memory, access trace). Non-interference then falls out as a corollary of that collapse rather than a second simulation. That is clean engineering.\n\nWhat they did well: the fault kernel is a small monadic reinterpretation of read/write, the SeparationModel is abstract enough to cover more than linear distance, and the Lean development ships with an axiom audit that uses only the three foundational axioms. No sorries, no problem-specific axioms. The no-fault embedding recovers ordinary semantics by computation, which is the right sanity check. The observation-parametric NI story is also well judged; they do not over-claim termination-insensitivity.\n\nSoft spots are real but proportionate. History-freeness and stationarity (F3–F4) exclude charge accumulation and refresh effects; the paper flags this itself and treats it as future work. The abstract geometry is deliberately coarser than real bank/row remapping, so the theorem is a conditional guarantee once you have measured br and a safe layout. Neither gap creates an internal contradiction or a hidden free parameter. The temporary anonymity of the repo is a minor practical annoyance, not a scientific one.\n\nThis is for people who care about mechanised semantics, information-flow hyperproperties, or formal justification of placement defences. Hardware people who want quantitative flip rates will find it too abstract; PL people who want a reusable fault interface will find it useful. The math is solid, the citations are appropriate, and the central argument holds under the stated contract. I would send it to referees without hesitation.","headline":"Clean, fully mechanised PL semantics for Rowhammer with a distribution-independent collapse theorem for physical separation; the modelling restrictions are stated honestly and do not break the proved claims.","tokens_in":31356,"tokens_out":462,"would_cite":true,"duration_ms":5671,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"grok-4.5","headline":"Physical separation makes Rowhammer disappear from the protected view of every finite program run, for every admissible fault model.","keywords":["Rowhammer","operational semantics","probabilistic fault models","physical separation","non-interference","information flow","mechanised verification","Lean"],"falsifier":"Exhibit a well-formed program on a safe layout together with a frame-local kernel for which some finite step count yields a protected residual program, protected memory value, or access trace different from the deterministic run; or show that real DRAM faults that depend on charge accumulation produce such a divergence under an otherwise faithful instantiation of the model.","tokens_in":31468,"feed_emoji":"💾","tokens_out":597,"duration_ms":5149,"temperature":0.7,"pith_summary":"Conventional programming-language semantics assume that reading or writing one memory location leaves every other location alone. Rowhammer breaks that assumption: hammering one DRAM row can flip bits in nearby rows that the program never touched. This paper supplies a compositional operational semantics that treats those faults as a small probabilistic effect on the ordinary read and write operations of an idealised imperative language, without modelling DRAM physics. The key result is a distribution-independent collapse theorem: if every location a well-formed program uses is placed outside every other such location's blast radius, then the residual program, the protected memory contents, and the access trace after any finite number of steps are exactly those of the ordinary fault-free run, as a Dirac distribution. The same collapse transfers ordinary non-interference into a probability-sensitive Rowhammer setting and reflects every Rowhammer leak back to a leak already present without faults. The whole development is mechanised in Lean.","feed_headline":"Physical separation erases Rowhammer from every finite run","feed_subtitle":"Protected program state matches the fault-free semantics for every admissible fault model","key_machinery":"The semantic-collapse theorem (Theorem 6.1 / physical_separation_sound): a probabilistic simulation whose invariant is parametric in a kept region of memory, instantiated by physical separation so that every supported fault outcome leaves protected locations and control flow untouched.","core_discovery":"Under an abstract frame-local fault kernel, a safe physical layout, and program well-formedness, the protected projection of every finite probabilistic Rowhammer execution is identical to the corresponding deterministic execution: residual program, memory restricted to protected locations, and access trace coincide as a point mass, independently of the concrete flip probabilities.","pith_inferences":[],"forward_implications":[],"fun_headline_variants":["Safe layouts collapse Rowhammer to fault-free finite runs","Physical separation erases faults from protected projections","Protected state matches deterministic semantics for every model","Frame-local faults vanish under safe variable placement","Separation yields Dirac mass of every finite Rowhammer-free run"],"cache_read_input_tokens":16512,"weakest_assumption_plain":"Faults are history-free and stationary: the chance of a flip depends only on the current victim set and the current memory, never on activation history, refresh state, or time.","fun_headline_variants_meta":{"raw":{"variants":["Safe layouts collapse Rowhammer to fault-free finite runs","Physical separation erases faults from protected projections","Protected state matches deterministic semantics for every model","Frame-local faults vanish under safe variable placement","Separation yields Dirac mass of every finite Rowhammer-free run"]},"model":"grok-4.5","effort":"low","cost_usd":0.004076,"raw_usage":{"total_tokens":1256,"prompt_tokens":817,"num_sources_used":0,"completion_tokens":76,"cost_in_usd_ticks":40760000,"prompt_tokens_details":{"text_tokens":817,"audio_tokens":0,"image_tokens":0,"cached_tokens":128},"completion_tokens_details":{"audio_tokens":0,"reasoning_tokens":363,"accepted_prediction_tokens":0,"rejected_prediction_tokens":0}},"tokens_in":817,"tokens_out":76,"duration_ms":3596,"temperature":1.0,"reasoning_tokens":363,"cache_read_input_tokens":128,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-07-14T12:41:22.285547+00:00","model_set":{"reader":"grok-4.5"},"falsifier":"Exhibit a well-formed program on a safe layout together with a frame-local kernel for which some finite step count yields a protected residual program, protected memory value, or access trace different from the deterministic run; or show that real DRAM faults that depend on charge accumulation produce such a divergence under an otherwise faithful instantiation of the model.","supporting_citations":[],"review_version":1}