{"id":"d3b48b63-f44c-4e7f-994a-3eb4dad086f1","arxiv_id":"2510.08889","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Scala 3 extension that lets capabilities be revoked and returned flow-sensitively, turning each capability into a typestate token checked by the compiler.","lead":"This paper extends Scala 3 with 'revocable capabilities' so a program can hand out, revoke, and hand back capabilities in order, letting the compiler check stateful operations such as file open/close, lock hand-over-hand, DOM building, and session protocols. The idea is that you get the safety of scoped resources without being forced into nested lifetimes.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The safety claim rests on an unverified Sigma/ANF transform that the paper itself says is outside the reachability-types formalism; a use-after-close through the unpacked Sigma pair is a concrete way this could break.","rationale":"The reader's weakest assumption — that soundness is imported from a same-author formalization and that the paper's adaptations (especially Sigma and the ANF transform) are asserted without proof — is exactly the load-bearing concern I find. I sharpen it to the Sigma/ANF mechanism because that is the part the manuscript itself admits lies outside reachability types, and because it is load-bearing for all the return-capability patterns in the case studies (file open/close, lock transitions, DOM brackets, session operations). If a killed capability can be revived through the original Sigma pair after ANF unpacking, then the prototype is unsound even for the simplest file example. Conversely, if the counterexample is rejected, the concern is mitigated for that path, but the absence of a formal connection between the ANF transform and the CPS translation means the general claim would still be conditional. The footnote inconsistency about omitted explicit capability bindings weakens the empirical 'all code compiles' evidence but is secondary. The approach is plausible and the design is coherent, so the right verdict remains CONDITIONAL rather than REJECT: the authors should provide the compiler fork with a commit hash, a counterexample test, or a proof that the Sigma/ANF transform preserves the imported soundness result.","tokens_in":22493,"tokens_out":10908,"duration_ms":99335,"concrete_test":"Run the released prototype on this program:\n\nval s = newFileSigma(\"a.txt\")\nval f: s.a.type = s.a\nimplicit val c = s.b\nopenImp(f)(using c)\ncloseImp(f)\nopenImp(f)(using s.b)\n\nIf this type-checks, the ANF/Sigma transform fails to track that s.b was killed, and the safety claim is false for the implemented subset. If it is rejected, test the analogous program that captures `s` in a closure after unpacking; rejection in both cases would indicate the transient-wrapper discipline holds, though a soundness proof would still be needed.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim is that the prototype statically rejects stale or illegal capability uses. The paper's only soundness anchor is Deng et al. [2025], but the mechanism that makes the case studies work — returning capabilities via Sigma and unpacking them with the type-directed ANF transform — is explicitly outside that formalism. Section 4 states: \"Sigma is not directly expressible using reachability types\" and says functions returning Sigma \"should be transformed in continuation-passing style,\" yet no theorem connects the implemented ANF transform to that CPS translation, and no proof shows that the transient-wrapper discipline prevents the original Sigma pair or its fields from being used after the extracted capability is killed. The destructive effect checker also covers only \"a core subset of Scala 3\" (Section 5), omitting destructive effects on mutable variables and object fields. Thus the \"statically safe\" headline is not established for the actual implementation. Separately, Section 2.5's footnote 1 says the implicit capability parameter \"must be explicitly bound and passed\" and is omitted in later examples, so Section 3's claim that \"All code in this section can be compiled by our prototype\" is not independently reproducible from the printed code.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes a design for flow-sensitive typestate tracking in Scala 3 by extending flow-insensitive capability mechanisms. The central mechanism is a destructive effect arrow (=!>), an implicit-return arrow (?<=) implemented via a type-directed ANF transformation over transient Sigma pairs, and path-dependent capabilities to preserve resource identity. The paper claims that these minimal extensions make imperative typestate programming statically safe and ergonomic, and it supports this with several case studies: file operations, hand-over-hand locking, DOM construction, and binary session types. A prototype compiler extension and a brief informal account of the underlying formal model are presented, with the soundness argument delegated to the same-group formalization of Deng et al. [2025].","tokens_in":22905,"tokens_out":3908,"duration_ms":37938,"significance":"If the claims were fully established, the paper would make a useful practical contribution: it would show that a small, mostly library-level extension to an existing mainstream language can express a wide range of typestate patterns without the explicit annotations of earlier typestate systems. The breadth of the case studies (locks, DOM, sessions) and the fact that the prototype is evaluated against the Scala capture-checker test suite (Section 5) are genuine strengths. However, the paper's central safety guarantee is not proved or even precisely stated for the actual implementation. The formal model of Deng et al. [2025] is imported, while the paper's own novel device—Sigma-guided implicit return via ANF—is explicitly admitted to fall outside that formalism. The implementation also restricts itself to a core subset of Scala and uses unchecked `asInstanceOf` casts. As it stands, the paper does not deliver a self-contained, verifiable argument that the prototype is statically safe, and the printed case-study code is not independently reproducible. The contribution is promising, but the validation is incomplete.","major_comments":[{"comment":"The paper states that \"Sigma is not directly expressible using reachability types\" and that \"functions returning Sigma should be transformed in continuation-passing style,\" yet the actual implementation uses a type-directed ANF transform. No theorem, lemma, or even precise statement connects the implemented transform to the CPS translation, and no argument shows that the transient-wrapper discipline prevents the original Sigma pair or its fields from being used after an extracted capability is killed. Since the implicit-return arrow ?<= is implemented through this transform, the central claim of statically safe returning of capabilities is unsupported. A formal statement of the CPS translation and its relationship to the ANF transform, together with a proof or at least a precise soundness conjecture with a testable invariant, is needed.","section":"Section 4, \"Sigma\" paragraph"},{"comment":"The checker \"supports a core subset of Scala 3\" and \"the most relevant omissions are destructive effects on mutable variables and object fields.\" This is a load-bearing limitation, not a footnote: the case studies in Section 3 are imperative and rely on mutable state—for instance, the Table and Row classes in Figure 2 have mutable lock fields, and the DOM example has internal state implied by \"more fields\" in Figure 4. The paper's abstract and introduction claim \"static safety reasoning for expressive imperative code,\" but the implementation cannot track destructive effects on exactly the mutable fields that these examples use. The limitations need to be stated in the abstract/introduction and their impact on the case-study claims must be analyzed.","section":"Section 5, \"Destructive Effect Checker\""},{"comment":"Section 3 states: \"All code in this section can be compiled by our prototype.\" But §2.5 footnote 1 says that, due to a Scala limitation, \"the implicit parameter c must be explicitly bound and passed\" and that \"for clarity, we omit them in subsequent examples.\" Therefore the printed code is not complete as shown and the claim is not independently checkable from the paper. Please provide a complete artifact, or show all code snippets in compilable form (even if verbose), and mark which portions are elided.","section":"Section 3 vs. §2.5 footnote 1"},{"comment":"The paper introduces a static marker FUN to denote \"the self-reference at the innermost (most recent) level,\" deviating from Deng et al. [2025], who use explicit naming for multiple levels of self-reference. This extension is used in Section 3.3.1 for `cFuture`, where a callback must be allowed to kill free variables. No soundness argument shows that the innermost-level self-reference is equivalent to the original multi-level mechanism, or that the interaction of FUN with the destructive effect checker preserves the imported soundness result. This is another adaptation that needs either a formal account or an explicit reduction to the existing formalism.","section":"Section 4, \"One-Shot Functions\""}],"minor_comments":[{"comment":"There are several typos: \"posesses\" (§3.3), \"chanenl\" (§3.3.1), \"protcool\" (§3.3), and inconsistent use of \"Section 3.2\" where a figure reference is intended for `open`/`close` (§3.2). A pass for terminology consistency would help.","section":"Throughout"},{"comment":"The presentation of path-dependent capabilities would benefit from an explicit comparison of the `^` tracking notation with the `q` freshness marker used in the formal model; the two notations are mixed in Section 2.1.2 and later, which can mislead readers about which formal system is being followed.","section":"Section 2.4"},{"comment":"The definition of `Dual` via match types is only sketched (`typeDual[P <: Session] <: Session = Pmatch`). Since the session-type case study relies on duality being type-level and sound, please clarify the omitted match cases and any bounds needed for `Var[N <: Int]`.","section":"Section 3.3, Figure 8"},{"comment":"The paper says the prototype can also be implemented as a compiler plugin, but no artifact or repository is provided. For a paper whose main evidence is a working prototype, making the code available would substantially strengthen the evaluation and reproducibility.","section":"Section 5"}],"recommendation":"major_revision","confidential_remarks":"The paper's dependence on a same-group formalization (Deng et al. 2025) is not in itself disqualifying, but the present manuscript does not state precisely which claims are inherited, which are new, and which are conjectured. The reviewer requests either a full soundness theorem for the Sigma/ANF device and FUN marker, or a clearly scoped claim that does not assert global static safety for the implemented prototype. A complete artifact would also help. I would consider reject if no formal connection is supplied, because the central safety claim is currently unverified; I recommend major_revision to give the authors the opportunity to supply it."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The thing to know first: this paper has a real idea. It combines flow-sensitive kill effects with path-dependent capabilities and an implicit-return mechanism (?<= / Sigma-guided ANF) to get typestate without lexical scopes. The case studies are substantive — hand-over-hand locking, DOM stack, session types — and they give a good feel for the design. The genuinely new piece is the returning mechanism; prior reachability/capturing types work is scoped, and this is a credible next step.\n\nWhat it does well: the API is ergonomic, revocation is opt-in, and the ANF transform resolves implicit ambiguity without burdening the programmer. The related-work section is broad and honest. Crucially, the paper itself concedes in Section 4 that Sigma is not directly expressible in reachability types and should be CPS-transformed, and Section 5 states the implementation covers only a core subset of Scala 3. The authors are not hiding the gaps.\n\nThe soft spots are in the safety story. There is no soundness theorem. The guarantee is imported from Deng et al. 2025, a same-group arXiv paper with no artifact link or independent formalization we can point to, and the paper's own modifications — omitting use effects, adding the FUN marker, the Sigma transient pair, and the type-directed ANF transform — are asserted rather than proved. Section 4 says functions returning Sigma should be transformed in CPS, but no theorem connects the implemented ANF transform to that CPS translation. That is load-bearing. The stress-test worry about unpacking a Sigma pair and then using the original pair after the extracted capability is killed is not demonstrated here, but it is exactly the kind of case the missing proof would need to cover. Also, the destructive effect checker omits mutable variables and fields, and the API implementations rely on Unit-typed capability casts defended only by the opacity of type members outside factory methods — that's a discipline, not an enforced invariant. Finally, footnote 1 says the implicit parameter must be explicitly bound and passed but is omitted in later examples, so the claim that all Section 3 code compiles cannot be checked from the printed text.\n\nNone of this means the design is wrong. It means the paper currently establishes plausibility, not soundness. The fix is cheap in principle: release the compiler fork with a commit hash, add a soundness statement or say which properties are only empirically tested, and make the relationship between the ANF transform and the CPS formalization precise.\n\nWho it is for: PL people working on capabilities, typestate, or Scala capture checking. It deserves a serious referee; the right outcome is probably conditional acceptance after the proof/artifact gap is addressed.\n\nRecommendation: send it to peer review.","headline":"A genuinely ergonomic typestate design with nice case studies, whose headline safety claim currently rests on an unpublished same-group formalization and an unproved Sigma/ANF bridge.","tokens_in":23294,"tokens_out":3914,"would_cite":false,"duration_ms":34485,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"Flow-sensitive typestate tracking rides on revocable capabilities, letting a Scala 3 extension reject stale state uses at compile time.","keywords":["typestate","revocable capabilities","destructive effects","reachability types","path-dependent types","implicit resolution","ANF transformation","session types"],"falsifier":"Compile a program that stores an open-file capability in a mutable variable, closes the file through the original variable, then reads through the stored capability. The paper's Section 5 openly omits destructive effects on mutable variables and object fields, so if this program type-checks and throws a file error at runtime, the claimed static safety does not extend to ordinary imperative code; similarly, any accepted program that performs a write-after-close via an alias or escape would falsify the central claim.","tokens_in":22432,"feed_emoji":"🔒","tokens_out":6732,"duration_ms":85261,"temperature":0.7,"pith_summary":"Flow-sensitive typestate tracking can be built on top of flow-insensitive capability mechanisms, rather than requiring a bespoke typestate analysis. The central trick is to decouple capability lifetimes from lexical scopes, so functions can receive, revoke, and return capabilities in a flow-sensitive way; a destructive effect system kills stale capabilities and any reachable aliases, path-dependent types tie each capability to a specific object's identity, and a type-directed ANF transformation returns fresh capabilities into implicit scope. The paper implements this as a Scala 3 compiler prototype and demonstrates it on file operations, hand-over-hand locking, DOM construction with context-free bracket states, and binary session types. If the claim holds, ordinary imperative code gets compile-time rejection of write-after-close and similar illegal state uses without explicit state annotations.","feed_headline":"Scala 3 prototype stops write-after-close at compile time","feed_subtitle":"Capabilities leave lexical scopes: functions revoke and return them, tracking file, lock, DOM, and session state implicitly.","key_machinery":"The central mechanism is the revocable capability: a token whose type is path-dependent on a specific resource (e.g., f.IsOpen) and whose lifetime is governed by a destructive effect system. The arrows ?=> (capability received implicitly), =!> (capability revoked/killed), and ?<= (capability returned implicitly) are combined as ?=!>? to express a complete typestate transition in a function type. A transient Σ-pair bundles a resource with a fresh capability for return, and a type-directed ANF transformation immediately unpacks it, placing the capability into implicit scope with highest precedence so that implicit resolution automatically finds the current state and not a stale one. This machi","core_discovery":"The paper shows that stateful resource safety can be enforced by turning capabilities into first-class, revocable witnesses of an object's current state. Each resource (file, lock, DOM node, channel) carries abstract type members for its states, and a capability is a path-dependent value of one of those state types. Operations consume and reissue capabilities: an open-file capability is killed by close, and a fresh closed-file capability is returned; because the new capability is numerically tied to the same object via its path prefix, capabilities for different objects can never be confused. The system's three arrows — implicit receive (?=>), destructive revoke (=!>), and implicit return (?","pith_inferences":["If the omitted destructive effects on mutable variables and object fields are added, the same mechanism could plausibly subsume ownership and borrow checking for a broader class of imperative Scala code, not just resource protocols.","The transient Σ-pair plus ANF unpacking is a reusable pattern: any capability-based language with path-dependent types and implicit resolution could adopt flow-sensitive typestate without a bespoke whole-program analysis.","A natural stress test would apply the prototype to existing Scala code that uses synchronized and resource-handling libraries, measuring how many idioms require new annotations and how often the checker's conservative qualifier tests reject safe code.","A mechanized proof of soundness for the prototype's actual core subset — including the FUN self-reference and CPS-transformed Sigma — would convert the imported guarantee from an assumption into a theorem; until then the safety result is contingent."],"forward_implications":["Programs that use a resource after a state transition — writing to a closed file, unlocking a lock that was never acquired, closing a DOM element twice — fail to type-check.","Capabilities can be released out of LIFO order, so patterns like hand-over-hand locking compile and are statically verified.","The same framework covers finite-state resources and context-free typestate such as balanced DOM bracket stacks, by parameterizing a type member over a compile-time list.","Binary session types become typestate capabilities: protocol violations on channel endpoints, including sending after the channel is closed or selecting an unavailable branch, are caught statically.","Because capabilities are resolved implicitly, user code stays concise and aliasing is handled by qualifier/disjointness checks rather than explicit permission annotations."],"fun_headline_variants":["Capabilities as state witnesses: revoke and reissue in Scala 3","Scala 3's revocable capabilities kill typestate analysis","First-class capabilities: close a file, get a new capability","Flow-sensitive capabilities without flow-sensitive analysis","Compile-time state tracking via revocable path-dependent types"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"Safety rests on the assumption that the prototype's adaptations to the formally proved effect system — omitting the separate tracking of use versus mention, adding the FUN self-reference marker, and translating Sigma-pairs in continuation-passing style — preserve that system's soundness; the paper states but does not prove this.","fun_headline_variants_meta":{"raw":{"variants":["Capabilities as state witnesses: revoke and reissue in Scala 3","Scala 3's revocable capabilities kill typestate analysis","First-class capabilities: close a file, get a new capability","Flow-sensitive capabilities without flow-sensitive analysis","Compile-time state tracking via revocable path-dependent types"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000193,"raw_usage":{"total_tokens":1190,"prompt_tokens":749,"completion_tokens":441,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":493,"completion_tokens_details":{"reasoning_tokens":355}},"tokens_in":493,"tokens_out":441,"duration_ms":22010,"temperature":1.0,"reasoning_tokens":355,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-04T10:40:56.957273+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Compile a program that stores an open-file capability in a mutable variable, closes the file through the original variable, then reads through the stored capability. The paper's Section 5 openly omits destructive effects on mutable variables and object fields, so if this program type-checks and throws a file error at runtime, the claimed static safety does not extend to ordinary imperative code; similarly, any accepted program that performs a write-after-close via an alias or escape would falsify the central claim.","supporting_citations":[],"review_version":1}