{"id":"a62a36fe-c575-429d-bc51-63147a25cec7","arxiv_id":"2412.14234","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":1,"one_line_summary":"A dual code-and-test generation pipeline with dynamic-analysis specifications translates the 3,000-line Zopfli C library into safe Rust, though the top-level validation compares compression ratios rather than exact outputs.","lead":"Syzygy is a pipeline that translates C libraries into safe Rust one function at a time, using an LLM for code and test generation and dynamic analysis to capture how pointers, aliases, and buffers behave at runtime. The authors report translating and test-validating Zopfli, a roughly 3,000-line compression library, which they say is the largest automated C to safe Rust translation to date.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Section 6.2.2's \"equivalence in compression ratios\" reduces to comparing compressed output sizes; because the input is identical, two different DEFLATE streams of equal length pass. The 1M-input validation therefore does not establish the claimed behavioral equivalence.","rationale":"I agree with the reader's weakest_assumption; it is the same load-bearing concern I identified. The ratio-based oracle is not a minor implementation detail: for fixed input size, equality of compression ratios is equivalent to equality of compressed output sizes, so the one-million-test suite validates only an output-length property. Different Huffman/block-splitting choices in a translated Zopfli can yield same-length streams with different content, and the paper's stated top-level check would not detect them. The per-function exact tests are a genuine strength, and I credit the paper for building I/O capture and per-function equivalence checks; however, they are generated from 26 semi-automatically collected top-level tests, use LLM-generated expected Rust values (which can introduce false positives), and still left a real bug (zopfli_block_split_lz77) that was repaired manually. Thus the final, broad validation via compression ratios carries most of the whole-program equivalence burden, and it is too weak. The concrete check I propose is direct and can reuse the existing harness. If exact byte equality holds on the 1M suite, the reader's concern is resolved and the paper's claim would be much better supported; if not, the abstract should be scoped to \"output-size-equivalent on tested inputs,\" which is materially weaker. The reader's CONDITIONAL verdict is appropriate until the authors run or release this comparison.","tokens_in":32406,"tokens_out":5773,"duration_ms":56098,"concrete_test":"Modify the EqTester used for the published one-million-input ZopfliDeflate validation so that, in addition to computing compression ratios, it compares the full output byte arrays produced by the C and safe-Rust implementations on the identical input and options. Report the number (or fraction) of inputs with differing bytes and, for the first divergence, the offset and byte values. Zero mismatches would settle the oracle concern and substantially strengthen the claim; any mismatch would require restricting the headline to output-size (ratio) equivalence.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The load-bearing validation step is in Section 6.2.2: \"We use these to check equivalence in compression ratios between the C and Rust programs.\" Since each test runs the C and Rust programs on the same input, compression-ratio equality is exactly compressed-length equality. It does not compare the values of the compressed byte arrays, so any two different DEFLATE streams of the same size pass. This conflicts with the Section 3 problem statement, which requires observational equivalence of outputs (P_C(t) ≃ P_R(t)). The per-function EqTester does compare serialized C/Rust values exactly, but that machinery is exercised on only 26 top-level inputs and relies on LLM-generated translateArgs and expected-value construction, plus manually specified structs and a manual repair (Figure 8). The abstract's phrase \"test-validated equivalence\" is therefore not supported by the broad one-million-input suite unless that suite compares exact outputs. The threat-to-valididity paragraph on test-based equivalence addresses coverage, not this oracle weakness.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper presents Syzygy, an LLM-driven pipeline that translates C codebases to safe Rust by decomposing the code into dependency-ordered translation units, mining dynamic specifications (types, bounds, nullability, aliasing, I/O examples) from instrumented C executions, and generating both Rust code and per-function equivalence tests whose expected outputs are obtained by translating real C I/O through LLM-generated translateArgs functions. The pipeline uses rejection sampling, compilation filtering, and test-failure feedback with multi-round repair. The main evaluation translates Zopfli, a compression library of roughly 3,000 lines and 98 functions, into safe Rust, and validates the result with a top-level suite of one million inputs. The paper claims this is the largest automated, test-validated C-to-safe-Rust translation to date.","tokens_in":32597,"tokens_out":3752,"duration_ms":38569,"significance":"If the translation is actually behaviorally equivalent on the tested inputs, this is a significant engineering and empirical contribution: it demonstrates a scalable recipe that combines dynamic analysis, LLM sampling, and incremental test-based equivalence checks, and it provides an ablation showing that test feedback is needed to go from merely compiling code to runnable code. The per-function EqTester design, which checks exact value equivalence against real C executions, is a genuine strength, as is the transparent reporting of cost, repair, and coverage. The central weakness is that the million-input top-level validation only compares compression ratios, not compressed byte streams, so the paper's headline equivalence claim is not supported by that suite. This issue is load-bearing and needs to be resolved before the main claim can be accepted.","major_comments":[{"comment":"The sentence \"We use these to check equivalence in compression ratios between the C and Rust programs\" defines the oracle for the one-million-input validation. Since the same input is compressed by both programs, compression-ratio equality is exactly compressed-length equality; two different DEFLATE streams of equal length would both pass. This does not establish the observational equivalence P_C(t) ≃ P_R(t) required by Section 3, and it does not justify the abstract's phrase \"test-validated equivalence.\" Please either compare exact compressed byte arrays and report how many inputs differ, or explicitly restrict the validation claim to compression-ratio equivalence and adjust the problem statement and abstract accordingly.","section":"Section 6.2.2"},{"comment":"The end-to-end pipeline is not fully automated as claimed. The paper reports manual specification of Rust structs (Section 4.3.1), manual verification of non-function translation units such as structs, globals, and macros (Section 6.2.1), and a manually strategized repair of zopfli_block_split_lz77 (Section 6.2.2). The exact per-function EqTester evidence is also seeded by only 26 top-level inputs (Section 6.2.1). The paper should state clearly which steps are automated and which require human intervention, and should quantify how many per-function I/O examples and exact equivalence tests were actually used, so that the \"largest automated and test-validated\" claim can be assessed accurately.","section":"Sections 4.3.1, 6.2.1, 6.2.2"},{"comment":"The test oracle itself is LLM-generated: translateArgs maps C inputs and expected outputs to Rust objects, and the equivalence test is generated by the LLM. If translateArgs or the generated assertions are incorrect, the commutative diagram in Section 4.4.3 can pass vacuously even when the Rust function is not equivalent. The paper transfers soundness to test reliability, but it provides no independent validation of translateArgs or of the generated assertions. Please add a concrete check, such as hand-validating translateArgs on a sample of per-function tests, reporting the number of failing per-function tests and repair rounds, or comparing against a mechanically constructed oracle for at least the 26 top-level inputs.","section":"Sections 4.4.1, 4.4.3, 5.4, 5.5"}],"minor_comments":[{"comment":"The caption says \"the a argument in sum points to a single int while that in sum points to an array of ints\"; the second mention of sum should likely be square, since square modifies a single int and sum iterates over an array.","section":"Figure 6 caption"},{"comment":"The table reports execution times without units; please state that the numbers are seconds (or another explicit unit).","section":"Table 3"},{"comment":"The text says GPT-4O can \"generate a correct translation for Zopfli\" but immediately adds that the translation \"crashes on some long test inputs\"; a translation that crashes on tests is not a correct translation, so this wording should be revised.","section":"Section 6.2.4"},{"comment":"The sampling diagram reuses K for both the translateArgs and EqTester sampling stages without defining it; please define K once or use distinct symbols.","section":"Figure 7"},{"comment":"The test-input description \"ranging between 1e1 and 1e7 characters\" should use explicit notation such as 10 to 10^7 characters for clarity.","section":"Section 6.2.2"},{"comment":"The phrase \"generated over 1000000 tests\" should be \"generate over 1,000,000 tests\" for readability.","section":"Section 8.2"}],"recommendation":"major_revision","confidential_remarks":"The core engineering result is credible and the per-function testing infrastructure is a useful contribution, but the weak top-level oracle is a load-bearing gap: as written, the million-input suite does not validate behavioral equivalence. The authors should be given the opportunity to either strengthen the oracle to exact output comparison or honestly downgrade the validation claim. If they cannot provide exact-output evidence, the paper's central claim should be reframed as compression-ratio-preserving translation rather than equivalence-preserving translation."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The real news is the scale: a 3,000-line, 98-function C library translated to safe Rust with per-function equivalence tests built from real C executions, plus a million-input top-level suite. That is a genuine advance over snippet-level LLM translation work. The integration of dynamic analysis for allocation sizes, aliasing, and nullability, and using that to drive both signature generation and intermediate test construction, is the actual contribution; I do not see it in the cited prior work. The per-function EqTester compares serialized C and Rust values exactly, and the suite reaches 95% line coverage; that is honest, checkable evidence.\n\nThe soft spot is exactly where the reader and the stress-test note land. Section 6.2.2 says the 1M-input validation checks \"equivalence in compression ratios.\" Since inputs are identical, that is just compressed-length equality. Two different DEFLATE streams of the same size pass. The paper's own problem statement (§3) requires observational equivalence of outputs, so the broad suite does not establish the claimed behavioral equivalence. The per-function tests are exact, but they are exercised on only 26 top-level inputs and depend on LLM-generated translateArgs and expected-value construction, plus manually written structs and a manual repair. The manual steps are disclosed, which I credit, but they are part of the method as described. The circularity burden is real but not fatal: the C source is the spec, and the per-function tests compare against actual C outputs, so this is not a closed loop by construction. The same-LLM-family concern is worth a sentence in the paper, not a rejection.\n\nThis paper is for people working on C-to-Rust migration, LLM-based code translation, and DARPA TRACTOR-style efforts. It deserves a serious referee. The engineering is solid and the scale-up is meaningful. What needs repair is the validation claim: either replace the compression-ratio oracle with exact output comparison on a meaningful subset, or explicitly scope the claim to ratio equivalence. The approach is sound; the headline overreaches.","headline":"Solid engineering scale-up with a genuine gap between the headline equivalence claim and the compression-ratio oracle.","tokens_in":33138,"tokens_out":1500,"would_cite":true,"duration_ms":16255,"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":"Syzygy claims that a 3,000-line C compression library can be translated into safe Rust automatically by pairing LLM code generation with dynamic-analysis-mined specifications and per-function equivalence tests, validated on one million…","keywords":["C-to-Rust translation","safe Rust","large language models","dynamic analysis","equivalence testing","rejection sampling","program synthesis","incremental translation"],"falsifier":"Take the translated and original C compression library and run a differential test that compares the exact compressed byte streams, or the decompressed outputs, on a large corpus of inputs sampled from the same length distribution. Any input for which the byte streams differ while the compression ratios match would show that the ratio-based oracle missed a behavioral difference; likewise, any crash the Rust version exhibits on inputs inside the tested range would do so.","tokens_in":32191,"feed_emoji":"🦀","tokens_out":6406,"duration_ms":57213,"temperature":0.7,"pith_summary":"Syzygy claims that C code can be translated to safe Rust automatically at the scale of a whole library by pairing LLM-driven generation with dynamic-analysis-derived information about memory, aliasing, nullability, and function input/output behavior. The approach translates one function (or type) at a time in dependency order, and for each unit it also generates an argument mapper and an equivalence test that compares the Rust behavior against the original C behavior on captured I/O examples. Translation candidates that compile and pass those per-function tests are committed, so each step preserves an invariant that previously translated code still works with the new addition. Applied to a 3,000-line, 98-function C compression library, the pipeline produced a safe-Rust version that passes a one-million-input equivalence suite achieving 95% line and 83% branch coverage; the authors claim this is the largest test-validated automated C-to-safe-Rust translation so far.","feed_headline":"LLM plus runtime checks turns a 3,000-line C library into safe Rust","feed_subtitle":"Pairs LLM generation with mined execution traces and per-function equivalence tests to scale C-to-Rust translation.","key_machinery":"The load-bearing mechanism is iterative aligned translation over a program dependency graph, with a dual code-and-test generation loop. A slicer decomposes the C codebase into functions, structs, typedefs, and macros and topologically sorts them. SpecMiner instruments and executes the C code to mine per-function specifications: types, allocation bounds, nullability, aliasing, and serialized input/output examples. CodeGenerator samples multiple LLM candidate translations, accepting only those that compile under a safe-Rust ban on unsafe blocks. ArgTranslator uses LLM-generated mapping functions plus an argument-construction API to translate C test inputs into Rust objects respecting aliasing and sizes, and EqTester generates equivalence tests that execute both versions and compare outputs. Rejection sampling at each stage filters candidates, and failing equivalence tests provide diff-based feedback for multi-round repair.","core_discovery":"On its own terms, the paper's central discovery is that the bottleneck in C-to-Rust translation is not the LLM's ability to write plausible code but the ability to know what the C code does at runtime and to test each piece in isolation. Syzygy mines execution traces of the top-level entry point to recover allocation sizes, pointer types, nullability, aliasing relations, and serialized I/O examples for every internal function; these specifications guide the LLM's signature choices and make possible reliable per-function equivalence tests. By looping over the dependency graph, translating bottom-up while generating both code and tests, the method filters out incorrect translations with execution feedback and repairs them with diff-based error messages. The result is a safe-Rust translation of the full library, validated end-to-end on one million compression tests; the paper claims this is the largest test-validated automated C-to-safe-Rust translation achieved so far.","pith_inferences":["Beyond the paper's claims: the ratio-based equivalence oracle could be upgraded to exact-output differential testing, which would turn the million-test pass from a compression-equality claim into an exact behavioral-equivalence claim for those inputs.","Beyond the paper's claims: the same recipe of fuzzing a documented entry point, mining internal function I/O, and letting equivalence tests drive incremental LLM translation could transfer to other C libraries, though cost and sampling rates remain open questions.","Beyond the paper's claims: because the paper reports that compiling alone leaves a long tail of functions with pass rates below 20%, a testable extension is to measure whether increased sampling or stronger dynamic analyses specifically rescue that tail."],"forward_implications":["Whole-library translation becomes tractable because the per-function equivalence invariant catches an error in one unit before dependent units are built, which is how the pipeline reaches 98 functions.","LLM output alone is not enough: without intermediate testing the pipeline still produces a compiling translation, but the ablation shows it crashes on trivial inputs, implying execution filtering is what makes the result usable.","Safe Rust can be produced end-to-end for a real library, but with a performance cost: optimized Rust is up to 3.67x slower than optimized C, largely from Vec allocations and bounds checks.","The approach carries practical constraints, including manual struct definitions and a current scope limited to acyclic data structures, single-threaded code, and no type punning."],"supporting_citations":[{"why":"The C compression library used as the main case-study translation target.","marker":"[15]"},{"why":"Prior LLM-based C-to-Rust translation approach on smaller programs whose lack of intermediate testing Syzygy addresses.","marker":"[54]"},{"why":"Closest prior LLM sampling-only translation approach without intermediate function tests, used as the main comparison.","marker":"[44]"},{"why":"User-study evidence of C-to-Rust translation difficulties that motivates dual code-and-test translation.","marker":"[31]"},{"why":"Rule-based translation baseline that produces unsafe Rust, contrasted with Syzygy's safe-Rust requirement.","marker":"[17]"},{"why":"Ownership-guided translation baseline that still leaves unsafe code, used for comparison.","marker":"[59]"},{"why":"Scaling inference compute via repeated sampling, which motivates the rejection-sampling strategy.","marker":"[5]"},{"why":"The concept of dynamic analysis that underlies the SpecMiner module.","marker":"[4]"}],"fun_headline_variants":["Runtime-guided LLMs convert 3K-line C library to safe Rust","LLMs + dynamic analysis achieve largest C-to-safe-Rust translation","Syzygy: runtime-guided LLM loop translates 3K-line C to safe Rust","Execution traces + LLM codegen: 3K-line C becomes safe Rust","Safe Rust from 3K-line C: Syzygy uses LLMs with runtime feedback"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that comparing compression ratios on the tested inputs is an adequate check of functional equivalence; if two implementations compress to the same ratio while producing different outputs, the validation suite would not catch the divergence.","fun_headline_variants_meta":{"raw":{"variants":["Runtime-guided LLMs convert 3K-line C library to safe Rust","LLMs + dynamic analysis achieve largest C-to-safe-Rust translation","Syzygy: runtime-guided LLM loop translates 3K-line C to safe Rust","Execution traces + LLM codegen: 3K-line C becomes safe Rust","Safe Rust from 3K-line C: Syzygy uses LLMs with runtime feedback"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000584,"raw_usage":{"total_tokens":2740,"prompt_tokens":931,"completion_tokens":1809,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":547,"completion_tokens_details":{"reasoning_tokens":1718}},"tokens_in":547,"tokens_out":1809,"duration_ms":10794,"temperature":1.0,"reasoning_tokens":1718,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-11T12:25:11.759030+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take the translated and original C compression library and run a differential test that compares the exact compressed byte streams, or the decompressed outputs, on a large corpus of inputs sampled from the same length distribution. Any input for which the byte streams differ while the compression ratios match would show that the ratio-based oracle missed a behavioral difference; likewise, any crash the Rust version exhibits on inputs inside the tested range would do so.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"The C compression library used as the main case-study translation target."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Rule-based translation baseline that produces unsafe Rust, contrasted with Syzygy's safe-Rust requirement."}],"review_version":1}