{"id":"7d382925-e30a-4994-a75b-06421312ebf4","arxiv_id":"2607.00563","paper_version":1,"verdict":"ACCEPT","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"low","formal_verification":"full","parameter_count":0,"one_line_summary":"A certificate-carrying rewriting system for Scratch-like languages uses a trusted checker to verify optimizer rewrites by recomputing preservation conditions, with a Lean-mechanized cooperative-frame refinement theorem covering multiple state families and 94.3% acceptance on 300 projects.","lead":"The paper introduces certificate-carrying source-to-source rewriting for event-driven block languages like Scratch, where an untrusted optimizer proposes rewrites and a trusted checker verifies them by recomputing all side conditions under an explicit observation lens. This yields behavior-preservation guarantees with a small trusted base, supported by a Lean-mechanized theorem and evaluation on 300 real projects.","discovery_kind":"new_method","skeptic_critique":{"model":"grok-4.3","headline":"Mechanized theorem covers only two of six rewrite families","rationale":"The reader's weakest assumption correctly identifies the model-to-VM gap as the primary external risk. The partial coverage of the mechanized theorem is an additional internal scoping limitation on the formal guarantee that is not reflected in the reader's \"formal_verification: full\" rating. The approach remains sound where the theorem applies, but the headline claim for the six-family checker requires the unmechanized families to be justified separately. This moves the verdict from unconditional ACCEPT to CONDITIONAL.","tokens_in":1877,"tokens_out":321,"duration_ms":29858,"concrete_test":"For each of the four non-mechanized families, list the exact side conditions checked by its implementation and determine whether they are instances of the parametric cooperative-frame theorem; if any side condition fails to follow from the mechanized statement, the soundness claim for that family lacks mechanized support.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"The central soundness argument is the cooperative-frame refinement theorem, which the paper mechanizes in Lean and shows covers two concrete rewrite families (variable state and renderer state). A checker is built for six families total, with evaluation and adversarial testing performed on all six. For the remaining four families the claim that recomputed side conditions suffice for behavior preservation therefore rests on unmechanized arguments. An error in those arguments would let the checker accept unsound rewrites, so the \"given a correct checker\" guarantee does not extend to the full set of families used in the reported results.","agreement_with_reader":"partial"},"referee_report":{"model":"grok-4.3","summary":"The paper presents certificate-carrying source-to-source rewriting for optimizing event-driven block programs in languages such as Scratch. An untrusted optimizer proposes rewrites that a trusted fail-closed checker accepts only after recomputing all side conditions under an explicit observation lens. The central soundness argument is a cooperative-frame refinement theorem mechanized in Lean, shown to cover two rewrite families (variable state and renderer state); a checker is implemented for six families total. Evaluation on 300 real projects reports 94.3% acceptance of behavior-preserving rewrites, sub-0.1s certification time, and zero false accepts across 4,278 adversarial perturbations. An ablation and audit further support the approach.","tokens_in":1999,"tokens_out":391,"duration_ms":19008,"significance":"If the result holds, the work shows how to obtain behavior-preservation guarantees for concurrent event-driven end-user languages while keeping the trusted base small. Strengths include the Lean-mechanized theorem, explicit model-to-VM assumptions, an adversarial test suite with zero false accepts, and an ablation demonstrating that semantic side conditions are necessary. The result is relevant to verified compilation and optimization for block-based languages.","major_comments":[{"comment":"The cooperative-frame refinement theorem is mechanized in Lean and shown to cover only two of the six rewrite families for which the checker is built and on which the evaluation and adversarial campaign (4,278 rewrites) are performed. For the remaining four families the claim that recomputed side conditions suffice for behavior preservation therefore rests on unmechanized arguments; an error in those arguments would allow the checker to accept unsound rewrites, so the \"given a correct checker\" guarantee does not extend to the full set of families used in the reported results.","section":"abstract and sections describing the theorem and checker implementation"}],"minor_comments":[],"recommendation":"major_revision","confidential_remarks":null},"author_rebuttal":{"model":"grok-4.3","summary":"We thank the referee for the careful and constructive review. The observation about the scope of the mechanized theorem is accurate, and we address it directly below.","responses":[{"response":"We agree with the referee's assessment. The Lean mechanization establishes the cooperative-frame refinement theorem parametrically and instantiates it only for the variable-state and renderer-state families. The checker for the remaining four families (and the reported evaluation results) relies on pen-and-paper arguments that the same frame condition, once the side conditions are re-checked, suffices for those state models. An error in those arguments would indeed weaken the end-to-end guarantee for those families. In the revised manuscript we will add an explicit table enumerating the mechanization status of each of the six families, qualify the abstract and introduction to distinguish the mechanized core from the manually justified families, and note that the adversarial campaign and ablation still supply empirical evidence even for the unmechanized cases. We do not claim that the mechanized theorem alone covers all six families.","revision_made":"yes","referee_comment":"[abstract and sections describing the theorem and checker implementation] The cooperative-frame refinement theorem is mechanized in Lean and shown to cover only two of the six rewrite families for which the checker is built and on which the evaluation and adversarial campaign (4,278 rewrites) are performed. For the remaining four families the claim that recomputed side conditions suffice for behavior preservation therefore rests on unmechanized arguments; an error in those arguments would allow the checker to accept unsound rewrites, so the \"given a correct checker\" guarantee does not extend to the full set of families used in the reported results."}],"tokens_in":1500,"tokens_out":362,"duration_ms":28705,"standing_objections":[]},"desk_editor":{"model":"grok-4.3","letter":"The paper's main result is a Lean-mechanized parametric cooperative-frame refinement theorem that justifies two concrete rewrite families (variable state and renderer state) under an explicit observation lens. They build a checker around it that recomputes every side condition for six families total, then test on 300 real Scratch projects where it accepts behavior-preserving rewrites on 283 of them at under 0.1 seconds each.\n\nThe design keeps the trusted base small by making the checker the only authority and stating the model-to-VM assumptions explicitly. The adversarial campaign of 4278 perturbed rewrites produced zero false accepts, the ablation without semantic conditions let behavior-changing rewrites through, and an audit caught eight additional cases the per-family suites missed. These are concrete, useful numbers.\n\nThe new element is the certificate-carrying architecture with recomputation instead of optimizer trust, plus the single mechanized theorem that covers multiple instantiations. The evaluation and the separation of checker from optimizer are the parts that hold up cleanly.\n\nThe soft spot is the coverage gap. The mechanized theorem applies directly to only two of the six families used in the checker and the reported results. The other four rely on unmechanized arguments, so the guarantee that a correct checker prevents unsound acceptances does not extend uniformly to the full evaluation. The observation lens and VM assumptions remain load-bearing and unverified beyond the stated model.\n\nThis is for programming-languages people working on verified transformations in concurrent or event-driven end-user languages. Readers who want to see how to certify rewrites with a small trusted base will find the design and the numbers worth their time.\n\nIt deserves a serious referee because the mechanized core and the testing are substantive enough to review, even with the partial mechanization.","headline":"Mechanized theorem covers two rewrite families with a practical checker for six and clean evaluation numbers, but the soundness for the full set rests partly on unmechanized arguments.","tokens_in":2517,"tokens_out":436,"would_cite":true,"duration_ms":24932,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"grok-4.3","headline":"A trusted checker recomputes every side condition of a proposed rewrite, ensuring an optimizer bug cannot mint an unsound acceptance under stated model-to-VM assumptions.","keywords":["block-based languages","source-to-source rewriting","behavior preservation","certificate-carrying transformation","event-driven programs","optimization verification","Scratch"],"falsifier":"A rewrite that the checker accepts but that the virtual machine confirms changes observable behavior under the stated observation lens would falsify the central claim.","tokens_in":2754,"feed_emoji":"🛡️","tokens_out":716,"duration_ms":37952,"temperature":0.7,"pith_summary":"The paper establishes that optimization of event-driven block programs can be turned into certificate-carrying source-to-source rewriting. An untrusted optimizer proposes a rewrite while a trusted fail-closed checker accepts it only after recomputing all required side conditions under an explicit observation lens. This approach keeps the trusted computing base small because the checker alone decides acceptance. The central soundness result is a cooperative-frame refinement theorem, mechanized in Lean, that justifies when a write can be removed without changing observable behavior. Evaluation on 300 Scratch projects shows the checker accepts valid rewrites on 94.3 percent of cases, runs in under a tenth of a second, and rejects all 4,278 adversarial perturbations tested.","feed_headline":"Trusted checker blocks optimizer bugs from accepting unsafe rewrites","feed_subtitle":"For Scratch programs, recomputing every side condition ensures behavior preservation even if the optimizer is buggy.","key_machinery":"The cooperative-frame refinement theorem under a parametric observation lens, which justifies removing a write that is overwritten before observation within a non-yielding window.","core_discovery":"We turn optimization into certificate-carrying source-to-source rewriting. An untrusted optimizer proposes a rewrite; a trusted, fail-closed checker accepts it only after recomputing every side condition that the rewrite's behavior preservation depends on under an explicit observation lens. The checker is the sole authority: given a correct checker and a small, explicitly stated set of model-to-VM assumptions, an optimizer bug cannot mint an unsound acceptance. The observation lens is a parameter, and the central soundness argument is a cooperative-frame refinement theorem: a write overwritten before any thread observes it, within a window in which no thread yields, can be removed. We mechan","pith_inferences":["The same parametric theorem structure could be instantiated for additional rewrite families beyond the six evaluated.","The approach may transfer to other concurrent event-driven languages that share similar observation models.","Small trusted checkers of this form could support verified transformations in other end-user programming environments."],"forward_implications":["The checker accepts a behavior-preserving rewrite on 94.3% of 300 real Scratch projects.","Certification costs under one tenth of a second per project.","A cross-family adversarial campaign of 4,278 perturbed rewrites produces zero false accepts.","An ablation that removes semantic side conditions ships rewrites the virtual machine confirms change behavior, while the full checker rejects every one."],"fun_headline_variants":["Checker verifies every side condition before accepting rewrite","Trusted checker prevents unsafe rewrites from optimizer bugs","Recompute conditions to certify behavior-preserving rewrites","Cooperative frame refinement secures block program optimizations","Observation lens certifies Scratch rewrites via explicit checks"],"cache_read_input_tokens":2112,"weakest_assumption_plain":"The model-to-VM assumptions accurately capture the observable semantics of the target virtual machine and the chosen observation lens detects all behavior changes relevant to the rewrite families.","fun_headline_variants_meta":{"raw":{"variants":["Checker verifies every side condition before accepting rewrite","Trusted checker prevents unsafe rewrites from optimizer bugs","Recompute conditions to certify behavior-preserving rewrites","Cooperative frame refinement secures block program optimizations","Observation lens certifies Scratch rewrites via explicit checks"]},"model":"grok-4.3","cost_usd":0.003305,"raw_usage":{"total_tokens":1752,"prompt_tokens":806,"num_sources_used":0,"completion_tokens":68,"cost_in_usd_ticks":33053000,"prompt_tokens_details":{"text_tokens":806,"audio_tokens":0,"image_tokens":0,"cached_tokens":64},"completion_tokens_details":{"audio_tokens":0,"reasoning_tokens":878,"accepted_prediction_tokens":0,"rejected_prediction_tokens":0}},"tokens_in":806,"tokens_out":68,"duration_ms":13784,"temperature":1.0,"reasoning_tokens":878,"cache_read_input_tokens":64,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-07-02T02:17:52.828646+00:00","model_set":{"reader":"grok-4.3"},"falsifier":"A rewrite that the checker accepts but that the virtual machine confirms changes observable behavior under the stated observation lens would falsify the central claim.","supporting_citations":[],"review_version":1}