{"id":"7c124d12-1f11-4d37-8026-0e3da85ee897","arxiv_id":"2501.13262","paper_version":1,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"ASDF compiles the basis-oriented Qwerty language into OpenQASM 3 and QIR, with resource estimates comparable to circuits produced by Qiskit, Quipper, and Q# for five benchmark algorithms.","lead":"ASDF is the first compiler for Qwerty, a quantum programming language that expresses algorithms through basis changes rather than gate circuits. It converts those basis-level programs into OpenQASM 3 and QIR, with fault-tolerant circuit costs roughly matching hand-written circuits from Qiskit, Quipper, and Q#.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Predication cleanup (§5.3) is the load-bearing unproven step: a missed renaming swap silently corrupts the orthogonal subspace, and the benchmark evaluation does not exercise predicated functions.","rationale":"The reader's weakest-assumption analysis correctly identifies predication cleanup as the most load-bearing unproven step. The paper's resource comparison is credible and reproducible, but a compiler contribution rests on semantic correctness of its transformations, and §5.3 provides neither a theorem nor systematic simulation-backed evidence. The swap-unswap trick is plausible for a single swap with a single computational-basis predicate, but the extension to arbitrary predicate bases and composed renaming permutations is only asserted. A wrong predicated function would not change the reported resource estimates, so the evaluation cannot catch it. For these reasons the concern is real, but it is a missing-proof/missing-validation concern rather than evidence of an actual bug; the appropriate verdict remains CONDITIONAL, requiring a correctness argument or extensive equivalence testing before acceptance.","tokens_in":27104,"tokens_out":19162,"duration_ms":202137,"concrete_test":"Run a randomized equivalence harness in the artifact: generate random reversible Qwerty basic blocks (n ≤ 4) built from qbunpack/qbpack reorderings, basis translations, and phase operations; for random predicate bases b chosen from single-vector, multi-vector, and primitive bases such as pm[1], compile b & f and ~f with ASDF; simulate the emitted OpenQASM/QIR with qir-runner or a dense simulator on all computational basis states; compare against a NumPy reference implementing Qwerty's basis-translation semantics. Repeat for at least 1000 random cases. Any mismatch falsifies §5.3; if none, the residual risk is confined to unsampled programs.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim is that ASDF compiles Qwerty's basis-oriented programs into circuits with costs comparable to circuit-oriented compilers. That claim has two implicit parts: the generated circuits must be semantically correct, and their costs must be competitive. The cost comparison is supported by the artifact and §8.3, but semantic correctness is not established. The weakest point is predication cleanup in §5.3. ASDF predicates a basic block by adding predicate bases to each operation and then, to undo renaming-based swaps in the space orthogonal to the predicate, emits for every logical swap an uncontrolled SWAP followed by a controlled SWAP, based on an intraprocedural index analysis. The paper gives a single worked example and a verbal cancellation argument, but no invariant or proof that (a) the index analysis is a bijection that captures every qbunpack/qbpack/renaming permutation, (b) the generated predicated SWAP sequence realizes the predicate projector for multi-vector or non-std predicate bases, and (c) the swap decomposition cancels as required. A missed swap or incorrect index mapping produces a unitary that is not diag(U, I) on the predicate/orthogonal decomposition, while resource counts remain essentially unchanged. The §8.3 benchmarks (BV, DJ, Grover, Simon, period finding) are oracle-based and, as described, do not exercise b & f or ~f in a way that would detect such a bug, so the evaluation cannot rule it out.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper presents ASDF, an MLIR-based compiler for Qwerty, a basis-oriented quantum programming language. The compiler type-checks and lowers Qwerty programs to OpenQASM 3 or QIR by synthesizing circuits from basis translations, automatically generating adjoint and predicated function specializations, and applying gate-level optimizations. The empirical evaluation compares the fault-tolerant resource estimates of ASDF-generated circuits with handwritten circuits in Qiskit, Quipper, and Q# across five benchmarks (Bernstein-Vazirani, Deutsch-Jozsa, Grover, Simon, and period finding), reporting comparable costs. A publicly available Docker artifact reproduces the experiments.","tokens_in":27320,"tokens_out":5872,"duration_ms":61650,"significance":"If the correctness gaps identified below are closed, this is a significant systems contribution: ASDF is, to the authors' knowledge, the first compiler for the basis-oriented paradigm, and it demonstrates that a high-level basis-oriented language can be compiled to circuits with fault-tolerant resource costs competitive with handwritten circuit-oriented code. The paper's strengths include a reproducible Docker artifact (DOI provided), open-source code, a polynomial-time span-equivalence checker with a complexity proof, and a multi-compiler empirical comparison over standard algorithms. The main weaknesses are the absence of a correctness proof for the predication-cleanup mechanism and the lack of any benchmark exercising predicated functions, leaving a load-bearing part of the claimed 'full generally' specialization support unvalidated.","major_comments":[{"comment":"The predication cleanup is not proven correct. The text describes an intraprocedural index analysis and a swap-unswap sequence, but gives no invariant or theorem showing that (a) the index map is a bijection that captures every renaming-based swap in the basic block, and (b) the emitted pair of one uncontrolled SWAP followed by one controlled SWAP realizes the intended predicate projector (the function on the predicate subspace and the identity on the orthogonal subspace). A missed swap or an incorrect index mapping would silently corrupt the orthogonal subspace while leaving resource counts unchanged. The evaluation in §8.3 does not include any benchmark that uses `b & f`, so this code path is not empirically validated by the reported experiments. Please add a formal invariant and correctness proof for the cleanup, or provide a systematic test harness that runs a variety of predicated Qwerty functions on a simulator and checks equivalence against the expected unitary.","section":"§5.3, Fig. 5"},{"comment":"The span-equivalence check is given only a complexity proof. Theorem B.6 establishes the O(k^2 log k) runtime, but no theorem states that Algorithm B1 accepts exactly those basis translations for which the two bases have equal span. The text says correctness 'can be proved inductively' but the proof is not supplied. Because this check guards every basis translation, a false positive would allow invalid translations to be synthesized and a false negative would reject valid programs. Please provide the correctness theorem and its proof (or a detailed invariant and induction argument) for Algorithm B1.","section":"§4.1, Appendix B"},{"comment":"The function-specialization analysis lacks a correctness proof. Algorithm D5 is claimed to terminate because cyclic call graphs cannot be constructed in Qwerty, but this fact is not proven, and no theorem asserts that the computed set of specializations contains exactly the specializations required by the program. A missing specialization would cause a compilation or linking failure rather than a wrong circuit, but the paper's claim that ASDF handles adjoints and predication 'in full generality' (Section 5) needs a supporting argument or an alternative empirical demonstration that all predicating and adjointing patterns in the test suite are correctly specialized.","section":"§6.2, Appendix D"}],"minor_comments":[{"comment":"The red label 'UNSWAP' in the figure is a fragment and is potentially confusing; the caption correctly says the red gates are SWAP gates, so the label should be clarified or removed.","section":"§5.3, Fig. 5"},{"comment":"The capitalization of the compiler name is inconsistent: 'ASDF' appears in the title and abstract while the body uses 'Asdf'. Please pick one form and use it consistently.","section":"Throughout"},{"comment":"The phrase 'assigning fresh indices to each non-stationary argument to the basic block' is unclear; the figure shows indices on non-stationary value edges, not on arguments. Please clarify what indices are assigned to what.","section":"§5.3"},{"comment":"The algorithm does not explain the distinct roles of 'smallstd' and 'bigstd' inside the loop; a sentence or two of intuition would substantially improve readability.","section":"Appendix E, Algorithm E6"},{"comment":"The Deutsch-Jozsa results are said to be 'virtually identical' to Bernstein-Vazirani and therefore omitted from the figures; please state this explicitly in the figure captions or provide the omitted data in an appendix so the reader does not wonder about the missing benchmark.","section":"§8.3"},{"comment":"Reference [2] cites only the arXiv preprint of the Qwerty paper; if a published version exists, please cite it as well.","section":"References"}],"recommendation":"major_revision","confidential_remarks":"The paper is a strong systems contribution with a reproducible artifact and a convincing empirical cost comparison. The load-bearing weakness is the unproven predication cleanup in §5.3, which is not exercised by the benchmark suite. I would be willing to accept after the authors either provide a rigorous correctness proof for the cleanup (or a precise invariant plus convincing argument) or add comprehensive simulation-based tests for predicated functions that would catch the plausible failure modes. The span-checking correctness theorem is also needed if the authors want the type checker to be a guaranteed part of the contribution. The specialization-analysis proof is less critical but should be addressed if the contribution is framed as 'full generality'."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"You should know this paper is the first compiler for Qwerty and makes a credible case that basis-oriented programming need not cost you circuit quality. The artifact is real: Docker images, scripts, and resource estimates are all there, and the comparison against Qiskit, Quipper, and Q# across five benchmarks shows cost parity, which is what the abstract actually claims.\n\nWhat is genuinely new: a basis-level MLIR dialect, polynomial span-equivalence checking with proofs in the appendix, circuit synthesis for basis translations via standardize/permute/destandardize, and an interprocedural analysis for adjoint/predicated specializations. The span-checking proof looks right, and the synthesis approach is clearly distinct from gate-level IRs like QIRO, QSSA, or Quake. The engineering is serious and the evaluation is reproducible.\n\nThe soft spot is Section 5.3, predication cleanup. When a block swaps qubits by renaming, ASDF undoes that swap in the orthogonal subspace by emitting an uncontrolled SWAP followed by a controlled SWAP, relying on an intraprocedural index analysis. The paper gives a worked example and a verbal cancellation argument, but no invariant or proof that the index analysis is a bijection that captures every qbunpack/qbpack/renaming permutation, and no proof that the generated SWAP sequence realizes the intended projector for arbitrary predicate bases. A missed swap would silently corrupt the orthogonal subspace while leaving resource counts unchanged. The five benchmarks are oracle-based and do not exercise b & f or ~f in a way that would detect such a bug. This is a real gap, but it is a gap in proof coverage, not evidence that the transform is wrong. The paper would be stronger with a correctness theorem or simulation-backed equivalence tests for predicated and adjointed functions.\n\nOne smaller issue: the contributions list says compiled code is of \"equal quality\" to handwritten circuits. That overstates what a resource estimate on five benchmarks can show. The abstract's \"comparable cost\" is the right claim. The citation pattern is appropriate; self-citation to the Qwerty paper is proper context. No fitted constants, no invented entities.\n\nI would send this to peer review. It is a substantive systems contribution with a reproducible evaluation. The reviewers should push on Section 5.3 and ask for predication-focused tests. If the authors cannot supply a proof, conditional acceptance with a strengthened evaluation is still reasonable.","headline":"First real compiler for a basis-oriented quantum language, with a reproducible artifact and credible cost parity; the predication cleanup is the one unproven load-bearing step.","tokens_in":27905,"tokens_out":1654,"would_cite":true,"duration_ms":18164,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"ASDF, the first compiler for the basis-oriented Qwerty language, synthesizes quantum circuits whose fault-tolerant qubit and runtime costs match handwritten circuits from circuit-oriented compilers.","keywords":["quantum programming language","basis-oriented programming","basis translation","circuit synthesis","function specialization","adjoint functions","predicated functions","fault-tolerant resource estimation"],"falsifier":"Compile a reversible Qwerty function that performs a non-trivial qubit permutation through renaming, write it in predicated form, and compare ideal-state-vector simulation of the predicated function against the generated circuit on many random inputs orthogonal to the predicate; any deviation there would refute the predication cleanup.","tokens_in":26896,"feed_emoji":"⚛️","tokens_out":11668,"duration_ms":111053,"temperature":0.7,"pith_summary":"The paper argues that a quantum programming language built on basis translations rather than gates can be compiled into efficient circuits, removing the assumed tax of high-level abstraction. It introduces ASDF, the first compiler for the Qwerty language, and demonstrates on Bernstein-Vazirani, Deutsch-Jozsa, Grover's search, Simon's problem, and period finding that the generated circuits use comparable physical qubits and estimated runtimes on fault-tolerant hardware to handwritten circuits produced by established circuit-oriented compilers. The central objects are basis translations, operations that rewrite a state's amplitudes from one orthonormal basis to another while preserving them, and the compiler's treatment of adjoint and predicated forms of functions. If the claim holds, quantum programmers can reason in bases and reusable reversible functions without sacrificing resource efficiency.","feed_headline":"High-level basis-based quantum code now matches handwritten circuits","feed_subtitle":"Qwerty's basis-and-function style yields fault-tolerant qubit and time costs on par with hand-built circuits.","key_machinery":"The load-bearing object is Qwerty IR, a quantum static-single-assignment dialect in a general extensible multi-level compiler-infrastructure framework, whose operations carry basis-translation, preparation, measurement, and function-adjoint or predication structure. It matters because it lets ASDF lower basis translations through a four-part pipeline: standardize, apply vector phases, permute standard-basis vectors, and destandardize. The second load-bearing mechanism is the predication cleanup, in which every renaming-based swap is recognized by a dataflow index analysis and then undone by one uncontrolled swap followed by one predicated swap, so the renaming is reversed exactly in the subspace orthogonal to the predicate.","core_discovery":"The discovery is that the basis translation, Qwerty's core primitive, is not an obstacle to compilation: any well-typed translation can be factored into a standardization step, a phase-adjustment step on standard-basis vectors, a permutation implemented by reversible-logic synthesis, and a destandardization step, with conditional versions used exactly where the two sides of the translation change primitive basis. Around this synthesis, ASDF builds a compiler with a quantum static-single-assignment IR that represents qubits flowing through basis-translation and measurement operations, so adjoint and predicated calls become structural rewrites rather than special cases. The result, the paper claims, is that a family of well-known algorithms written without any hand-composed gates compiles to circuits whose fault-tolerant resource estimates match those of handwritten circuits from the comparison compilers.","pith_inferences":["Editorial inference: if the resource parity holds beyond the five benchmarks, basis-oriented languages could let domain experts delegate circuit design entirely to the compiler, much as high-level synthesis did for classical hardware.","Editorial inference: the uncontrolled-swap-then-controlled-swap cleanup is a general way to make SSA-style renaming safe under predicates and could be extracted as a reusable pass for any quantum IR with renaming-based swaps.","Editorial inference: the factoring-based span-equivalence checker is a candidate algorithmic primitive for type systems of other basis-oriented quantum languages, since it avoids enumerating exponentially many basis vectors.","Editorial inference: a direct stress test of the predication cleanup, using random reversible functions composed with non-trivial predicates and ideal simulation of orthogonal input states, would harden the empirical case beyond the paper's benchmarks."],"forward_implications":["Fault-tolerant resource estimates show Qwerty programs can target surface-code hardware at qubit and time costs comparable to hand-coded circuits, so the abstraction layer does not add a practical premium.","Aggressive inlining removes all callable intrinsics from the generated low-level representation on the five benchmarks, producing straight-line code suitable for restricted hardware profiles.","Basis translations with programmer-supplied phase factors synthesize directly to multi-controlled phase gates, making constructs such as diffuser steps one-line basis translations.","The span-equivalence type checker verifies basis translations in polynomial time, so exponential-sized bases such as 64-qubit tensor products remain checkable.","Adjoint and predicated function specializations are generated transitively through the call graph, so reusable reversible functions can be invoked backwards or under predicates without manual gate-level rewriting."],"supporting_citations":[{"why":"Defines Qwerty's basis-translation, adjoint, and predication semantics that ASDF must compile.","marker":"[2]"},{"why":"Supplies the reversible-logic synthesis routines that turn permutations and classical functions into gate circuits.","marker":"[40]"},{"why":"Provides the T-depth-one decomposition of multi-controlled gates that keeps fault-tolerant costs low.","marker":"[42]"},{"why":"Gives the surface-code resource estimates used to compare qubit counts and runtimes.","marker":"[57]"},{"why":"Supplies the circuit-optimization pass and one set of benchmark implementations used as the comparison baseline.","marker":"[38]"},{"why":"Provides one of the circuit-oriented compiler baselines and benchmark implementations used in the comparison.","marker":"[16]"},{"why":"Provides the other circuit-oriented compiler baseline and the callable-intrinsic comparison for the generated low-level representation.","marker":"[53]"},{"why":"Supplies the quantum SSA IR design from which Qwerty IR's dataflow semantics are adapted.","marker":"[36]"},{"why":"Provides the multi-level compiler infrastructure used to implement the custom dialect, inlining, and canonicalization.","marker":"[26]"},{"why":"Supplies the relaxed peephole optimizations that simplify multi-controlled gates and reduce output cost.","marker":"[27]"}],"fun_headline_variants":["Basis-based quantum code now matches handwritten circuits","Compiler turns basis abstractions into circuits on par with manual","Automated basis translation yields circuits as good as hand-coded","ASDF compiler: basis-driven quantum code, manual-grade circuits"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The predication cleanup assumes the intraprocedural dataflow index analysis finds every renaming-based swap in every predicated block; if it misses one, the compiled function will modify states outside the predicate's span.","fun_headline_variants_meta":{"raw":{"variants":["Basis-based quantum code now matches handwritten circuits","Compiler turns basis abstractions into circuits on par with manual","Automated basis translation yields circuits as good as hand-coded","ASDF compiler: basis-driven quantum code, manual-grade circuits"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000326,"raw_usage":{"total_tokens":1767,"prompt_tokens":826,"completion_tokens":941,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":442,"completion_tokens_details":{"reasoning_tokens":874}},"tokens_in":442,"tokens_out":941,"duration_ms":10323,"temperature":1.0,"reasoning_tokens":874,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-10T16:19:17.596427+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Compile a reversible Qwerty function that performs a non-trivial qubit permutation through renaming, write it in predicated form, and compare ideal-state-vector simulation of the predicated function against the generated circuit on many random inputs orthogonal to the predicate; any deviation there would refute the predication cleanup.","supporting_citations":[{"cited_title":"Adams, Sharjeel Khan, Jeffrey S","cited_arxiv_id":null,"evidence_quote":"Defines Qwerty's basis-translation, adjoint, and predication semantics that ASDF must compile."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Provides the other circuit-oriented compiler baseline and the callable-intrinsic comparison for the generated low-level representation."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the relaxed peephole optimizations that simplify multi-controlled gates and reduce output cost."}],"review_version":1}