{"id":"d91bf218-51c5-49c9-8e64-e286c22efb5d","arxiv_id":"2607.15877","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"From separation-logic specifications for database operations, the authors derive, without extra assumptions, that any verified implementation correctly implements its weak isolation level.","lead":"By adding erasable ghost instrumentation and a trace invariant, the paper shows that any database implementation satisfying specific separation-logic specifications automatically satisfies its advertised isolation level. The proof is machine-checked in Rocq and covers every possible client workload, not just predefined tests.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"State-based model amendment: NoConf's snapshot index is unconstrained by start time, so two blind-write txns to same key can both commit; equivalence to Adya is cited, not proven.","rationale":"The reader's CONDITIONAL verdict is reasonable, but I would rank the unproved amended-model equivalence ahead of the inherited correctness of [3]'s specifications. The paper's headline claim is that the separation-logic specifications imply the database community's dependency-graph isolation levels. The chain of implications relies on Crooks et al.'s equivalence between the state-based and dependency-graph models. Section 3 explicitly amends the state-based model, so the cited equivalence no longer applies without a new proof. The NoConf commit test, as written, leaves the snapshot index existentially free except for constraints from no-prior-write reads. For blind-write transactions, this freedom can hide write-write conflicts by choosing a snapshot after the conflicting transaction. If that is right, the amended model admits executions that Adya's snapshot isolation forbids, so the final step of the central claim is unsupported. This is not an attack on the machine-checked proof: Theorem 6.2 may be fully correct for the amended model. The issue is that the amended model may be strictly weaker than the intended isolation level. The reader's primary concern about [3]'s specs is also valid, but that is inherited from prior work; the equivalence gap is introduced by this paper. A positive proof of equivalence or a counterexample would settle the matter, so CONDITIONAL remains the appropriate verdict.","tokens_in":30707,"tokens_out":27823,"duration_ms":310147,"concrete_test":"Formalize or enumerate both the amended Section 3 state-based model and an accepted dependency-graph formalization of snapshot isolation with explicit start times. Minimal case: two transactions, both {W(k,v_i), C(true)}, with T2's start linearization point before T1's commit linearization point in the trace. Check whether CT_SI admits E = [T1,T2] with snapshot(T2) after T1 while Adya SI rejects it. This can be done by brute-force search over small instances in Alloy/TLA+, or by a Rocq formalization of the two models and an equivalence theorem. If a witness exists, the equivalence claim is false; if none exists, close Section 3 by proving the equivalence for the amended NoConf.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The advertised conclusion is not merely ValidTrace(I,t) for the paper's own Section 3 model, but that this model is equivalent to Crooks et al. [16] and hence to Adya's dependency-graph model. Section 3 amends the Crooks model (removing unique values and at-most-one-write-per-key, and reformulating NoConf), yet the equivalence proof is only cited, not re-proven for the amendment. The amendment has a concrete soft spot. In Definition 3.3/Figure 5, NoConf(E,T,i) forbids only transactions at indices i' with i < i' < j, where j is T's position in E and i is an existentially chosen snapshot index. Complete(E,T,s,i) constrains i only through reads R(id,k,ov) with NoPriorWrite; for a transaction with no such reads, i can be chosen arbitrarily close to j. Hence an execution with T1 = {W(k,1), C} at index 1 and T2 = {W(k,2), C} at index 2 is admitted: give T2 snapshot index 1, so no transaction lies strictly between i and j. Under Adya's snapshot isolation (and standard first-committer-wins), two concurrent transactions that both write k cannot both commit, regardless of whether they read. If this counterexample is valid, the amended state-based model is strictly weaker than the dependency-graph model, and the conclusion 'in the Adya model' does not follow from the cited equivalence. The proof of Theorem 6.2 may construct E using start linearization points, but that does not repair the model-level equivalence claim: Definition 3.5 and Theorem 5.1 quantify over the amended model as stated. This is a missing proof obligation, not a demonstrated error in the machine-checked core.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper presents a method for proving that any database implementation satisfying the separation-logic specifications of Alnor Mathiasen et al. [3] implements the corresponding isolation level in the state-based model of Crooks et al. [16]. The method instruments database operations with ghost pre/post events, enforces a global trace invariant ValidTrace(I,t), extracts linearization points and transactions, and proves a free theorem (Theorem 5.1): for any verified clients, all reachable traces satisfy the commit test of I. Proofs are mechanized in Rocq/Iris/Aneris (13,000+ lines). The paper covers read uncommitted, read committed, and snapshot isolation, with a detailed proof sketch for snapshot isolation.","tokens_in":31058,"tokens_out":11335,"duration_ms":115834,"significance":"If the central claims hold, this is a significant step: it avoids workload-specific model checking and gives a modular, machine-checked bridge from executable code to abstract consistency models. The paper is commendable for shipping a large Rocq formalization and for stating the theorem parametrically in the prior specifications, making the result a genuine free theorem. However, the significance depends on the amended Section 3 model preserving the Crooks--Adya equivalence; this is currently asserted rather than proved.","major_comments":[{"comment":"The amended NoConf leaves the snapshot index i unconstrained for blind writes. A transaction T with no NoPriorWrite read of k may set i = j-1, so an execution [T1={W(k,1),C} at index 1, T2={W(k,2),C} at index 2] is accepted. If T1 and T2 overlap in the source execution, Adya's write-write conflict rule forbids both commits. The paper cites Crooks et al. [16] for equivalence but explicitly states that this model has been amended (removed unique-value and one-write-per-key assumptions, changed NoConf). No proof is supplied that the amended model remains equivalent to the dependency-graph model. This is load-bearing: Theorem 5.1 is stated for the amended model and the intro/conclusion claim Adya as the endpoint. Please either prove the equivalence for the amended model or scope the claims to the amended model and state which standard guarantees are lost.","section":"§3, Definition 3.3 and Figure 5"},{"comment":"The Adequacy theorem inherits the separation-logic specifications specI from the authors' own prior work [3]. ValidTrace(I,t) establishes the amended state-based commit test, but nothing in the paper proves that specI captures the intended isolation level beyond the write-skew example in Section A. Since the headline claim is that isolation levels are derived from the structure of specifications, an explicit statement that the result is only as strong as specI -- together with a summary of the phenomena checked for each level in [3] -- would make the dependency visible. This is a premise concern, not an internal inconsistency, but it is central to the advertised guarantee.","section":"Theorem 5.1 / §4–§5"}],"minor_comments":[{"comment":"CT_SI(T,E) is written with NoConf(E,T,s), while Definition 3.3 defines NoConf(E,T,i). The third argument should be an index, not a state; the notation should be made consistent.","section":"§3, Figure 5"},{"comment":"The second transaction's read is rendered as R((τ2,c2),y,x0); from the trace in Figure 9 it should be y,y0.","section":"§5.3, Figure 13"},{"comment":"Definition 3.5 and the text around it refer to 'Theorem 3.5'; it is a definition. Similarly, the commit tests in Figure 5 are called 'Theorem 3.3/3.4' but are definitions.","section":"§3, §5.4"},{"comment":"The same symbol t is used for the event trace and for the linearization-point sequence. This is easy to confuse; distinct symbols (e.g., t and ℓ) would improve readability.","section":"§5, The Global Proof Invariant"},{"comment":"The paper claims that all proofs are mechanized but gives no artifact description (location of the Rocq development, key theorem names). A short reproducibility note would help readers and reviewers.","section":"Mechanization"}],"recommendation":"major_revision","confidential_remarks":"The main risk is the unproved equivalence of the amended Section 3 model to Adya's dependency-graph model. If the authors can supply that equivalence (ideally mechanized), the paper is publishable; otherwise the claims must be scoped to the amended state-based model. The reliance on the authors' own prior specifications is a premise, not misconduct, but it should be stated clearly."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"My read: the free theorem is the real thing. If you accept the specs from Alnor Mathiasen et al. 2025, the paper shows that any implementation satisfying those specs yields traces satisfying the Crooks-style state-based model, for arbitrary client programs. That is a genuine bridge from executable, separation-logic-verified database implementations to accepted transactional consistency models, and it is the first I have seen. Extending the trace-invariant technique from Birkedal et al. is non-trivial, and the claimed 13k-line Rocq mechanization is exactly the kind of evidence that makes a result credible. The ghost-invariant with linearization points is a sound and elegant way to lift Hoare-style specs to a global trace property.\n\nThe main soft spot is the amended Crooks model. Section 3 removes the unique-values and single-write-per-key assumptions and reformulates NoConf, then the paper simply cites Crooks et al. for equivalence to the Adya dependency-graph model. That equivalence was proved for the original model, not this amended one. The stress-test note proposes a blind-write counterexample, but I think that example does not actually break the model: a transaction with no reads can choose a snapshot index immediately before itself, which serializes it after any conflicting writer. So two blind-write transactions can both commit in the model, but they are then sequentially ordered, which Adya's SI allows. The specific counterexample does not land. The underlying point still stands: there is a missing proof obligation to show the amended commit test accepts exactly the executions accepted by the dependency-graph model. Maybe the equivalence is true and lives in the Rocq development, but the paper does not provide it, and the claim of deriving the Adya model rests on that citation.\n\nOther soft spots are minor. The artifact is not linked or hashed, so verification is not immediately reproducible. And the central premise is the authors' own prior specifications; that is a premise, not a circular step, but it means the theorem inherits any gap in those specs.\n\nThis paper is for verification researchers and database systems people working on formal guarantees. It deserves a serious referee, and the referee should push on the model equivalence and, if possible, inspect the Rocq artifact. I would send it to review.","headline":"Genuinely new free theorem connecting separation-logic specs to a Crooks-style consistency model, but the paper owes the reader a proof that its amended model is still equivalent to the dependency-graph model.","tokens_in":31631,"tokens_out":7840,"would_cite":true,"duration_ms":74048,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q60","68P15"],"pacs":[],"model":"deepseek-v4-flash","headline":"For three weak isolation levels, any database implementation that satisfies a given set of separation-logic per-operation specifications automatically implements that isolation level, for every possible client, with a machine-checked proof.","keywords":["isolation levels","separation logic","free theorem","transactional consistency","state-based model","ghost code","linearizability","formal verification"],"falsifier":"One disqualifying observation would be a database implementation that provably satisfies the snapshot-isolation separation-logic specification yet has a committed execution whose transactions cannot be ordered into any state-based execution satisfying the snapshot-isolation commit test. A second would be an execution accepted by the amended state-based commit test but rejected by the dependency-graph definition of the same isolation level, which would refute the claimed equivalence between the two models.","tokens_in":30523,"feed_emoji":"🗄️","tokens_out":5471,"duration_ms":48800,"temperature":0.7,"pith_summary":"The paper's central thesis is that isolation-level correctness can be read off the structure of separation-logic specifications: verify the individual database operations against the appropriate Hoare-style specification, and the database automatically satisfies the corresponding isolation level in a state-based transactional consistency model. The proof works for read uncommitted, read committed, and snapshot isolation, covers arbitrary client programs and arbitrary transaction workloads, and is fully machine-checked. The mechanism is a trace-based extraction: operations are instrumented with ghost code that records start and end events, linearization points are inserted logically, operations are grouped into transactions, and an invariant guarantees those transactions admit an execution passing the isolation level's commit test. The result is a free theorem, meaning the model-level guarantee needs no additional proof for each concrete database implementation once its operations meet the specifications.","feed_headline":"Verified databases get their isolation level for free","feed_subtitle":"Machine-checked proof: meeting the per-operation specs guarantees the consistency model for all clients.","key_machinery":"The load-bearing mechanism is a four-level trace extraction. Level 0 is instrumented executable code; ghost operations emit pre and post events into a global trace with fresh tags (level 1). From that trace, a sequence of linearization points is constructed (level 2), constrained to be coherent with the trace in the standard linearizability sense. The linearization points are chopped into transactions per connection (level 3), requiring each transaction to read its own most recent write, have ordered operations, and end with a single commit. At the top, the transactions must admit an execution of the state-based model whose commit test holds. The global proof invariant ValidTrace(I,t) packag","core_discovery":"The paper proves an adequacy theorem: for an isolation level I with its separation-logic specification specI, any implementation libI satisfying specI, wrapped with the ghost instrumentation, produces only valid traces under arbitrary verified clients, and no thread crashes. A valid trace is one for which a sequence of linearization points, a set of transactions, and a state-based execution exist such that the isolation level's commit test holds for all committed transactions. This is exactly implementation correctness in the state-based consistency model, and, via the model's established equivalence, in the dependency-graph formulation used by the database community. The proof is uniform: i","pith_inferences":["Editorial inference: the same extraction pipeline should extend to stronger and additional isolation levels (such as serializability or parallel snapshot isolation) once separation-logic specifications exist; the main friction is designing the per-level commit test and the corresponding resource wrapping, not the trace machinery.","Editorial inference: the method's practical power depends on the cost of proving the underlying per-operation specifications for a real database; for high-performance engines this is a substantial verification effort, though it is paid once per implementation rather than per workload.","Editorial inference: a testable extension would be to instantiate the pipeline for a small distributed database and show that the extracted transactions satisfy the commit test on all interleavings, providing a concrete end-to-end case against which this paper's machinery can be checked.","Editorial inference: because the equivalence between the amended state-based model and the dependency-graph model is cited rather than proven in this paper, a rigorous independent check of that equivalence for the modified NoConf test would close the only remaining semantic gap."],"forward_implications":["Verifying a database's isolation level reduces to proving per-operation separation-logic specifications; the consistency-model guarantee follows automatically for all possible client programs.","The guarantee holds for every transaction workload, not just a fixed workload, so it is strictly stronger than model-checking approaches that enumerate interleavings.","The result is a free theorem: new database implementations acquire the model-level guarantee without re-proving the connection, as long as they satisfy the specifications.","Clients can be verified against the same modular per-operation specifications, so correctness composes with other libraries and verified components.","Because the proof is machine-checked, the link between executable code and the isolation-level model is mechanized end to end."],"fun_headline_variants":["Free theorem: separation logic specs guarantee isolation levels","Database isolation levels verified for free with separation logic","Separation logic proof: specs imply isolation levels for all clients","Machine-checked proof: spec compliance ensures isolation level","Isolation levels fall out of separation logic specs for free"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"The result inherits correctness of the separation-logic specifications: if those specifications permit a behavior that violates the intended isolation guarantee, the free theorem still holds formally but offers no real guarantee.","fun_headline_variants_meta":{"raw":{"variants":["Free theorem: separation logic specs guarantee isolation levels","Database isolation levels verified for free with separation logic","Separation logic proof: specs imply isolation levels for all clients","Machine-checked proof: spec compliance ensures isolation level","Isolation levels fall out of separation logic specs for free"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000199,"raw_usage":{"total_tokens":1200,"prompt_tokens":730,"completion_tokens":470,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":474,"completion_tokens_details":{"reasoning_tokens":393}},"tokens_in":474,"tokens_out":470,"duration_ms":4103,"temperature":1.0,"reasoning_tokens":393,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-01T22:04:16.588499+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"One disqualifying observation would be a database implementation that provably satisfies the snapshot-isolation separation-logic specification yet has a committed execution whose transactions cannot be ordered into any state-based execution satisfying the snapshot-isolation commit test. A second would be an execution accepted by the amended state-based commit test but rejected by the dependency-graph definition of the same isolation level, which would refute the claimed equivalence between the two models.","supporting_citations":[],"review_version":1}