Source-linked AI summary
A Trust Ledger and an Execution Check for CPG-Based C-to-Lean 4 Autoformalization: Separating Declined from Silently Incorrect Translations
Ishan K Singavarapu, Manish Bhatt
TL;DR
Autoformalization reports often combine code the translator declined with code it translated incorrectly in a single success rate. This paper pairs a structural trust ledger with execution checks, finding that SQLite’s reported coverage differs by 2.45× depending on whether call closure is required.
Problem
Autoformalization often reports a single success rate that conflates code declined by the translator with code translated incorrectly.
Source: §1 · pp. 1–2Method
The paper uses a per-construct ledger of declined translations alongside execution checks against a reference implementation to detect silent errors.
Source: §1 · p. 2Results
2.45×: the reported SQLite coverage figure differs depending on whether call closure is required.
Source: §1 · p. 2Takeaways & Limitations
The paper recommends executing translations against the language implementation rather than relying only on counts of attempted code.
Source: §8 · p. 9The findings establish that decoupling occurs, not how often; the observed cases are not a sample from a defined population.
Source: §6 · p. 8
Abstract
from arXiv · showhide
Verifying large C codebases requires translating them into formally checkable semantics, but most autoformalization work reports a single aggregate success rate that conflates two different failure modes: code the translator declined to handle and code the translator translated incorrectly. We present a deterministic code-property-graph (CPG)-based exporter that translates C source into a small Lean~4 core semantics under a three-tier correctness discipline: hole-free, call-closed, and dynamic-hole-risk, that keeps these modes distinct. Applied to a re-export of the SQLite source tree (8{,}602 functions, over 1.5~million AST nodes), the exporter translates 5{,}222 functions (60.7\%) hole-free, of which only 2{,}134 (24.8\%) are call-closed, a $2.4\times$ gap a single rate would hide. Both figures are reported in a full per-construct trust ledger rather than a single score. Our main contribution is methodological: a protocol for separating constructs that are fundamentally unresolvable by whole-program static analysis (such as public API boundaries) from constructs that only look that way. For example, we retracted our own ``impossible'' classification of function-pointer/vtable dispatch after tracing a concrete counterexample in the target codebase. Separately, a search for ``more holes closed'' surfaced a latent silent-wrong-answer bug: a translation that succeeded with an incorrect result rather than declining, a failure mode we argue is more dangerous than any hole, and one a hole-count-only evaluation would never surface.
1 Introduction
The paper separates declined translations from silently incorrect ones, showing that coverage can move independently of fidelity. Its protocol pairs a per-construct trust ledger with execution checks and reports structural measures without treating them as correctness claims.
1 Introduction
- Coverage counts declined constructs but misses well-typed translations that compute wrong answers, including errors involving character literals, do-while loops, and variadic signatures.Detecting silent errors requires executing the translation against a reference implementation.Source: §1 · p. 2
- A function is hole-free when its translated syntax has no placeholders, and call-closed when it also has no direct calls unresolved to exported functions.The paper reserves “verified” for properties checked by a proof assistant; none of its three structural measures qualifies.Source: §1 · p. 2
- The findings establish that decoupling occurs, not how often: the cases are not a sample from a defined population, and SQLite’s exported functions lack population-level oracle checks.The execution checks described here use hand-built fixtures.Source: §1 · p. 2
- Six cases separate metric movement from correctness: four correctness defects, one mostly relabeled movement, and one retracted impossibility claim changed 17 translations without moving coverage.The paper also finds that the number of hole causes is unstable because source-based labels partition the source.Source: §1 · p. 2
- The proposed discipline combines three structural measures, cause-itemized holes, and execution checks, while distinguishing statically unresolvable constructs from those that only appear so.A public API boundary is an example of a construct that whole-program static analysis cannot resolve.Source: §1 · p. 2
- 2.45×: the reported SQLite coverage figure differs depending on whether call closure is required.The authors describe this as a denominator effect, measured on one codebase.Source: §1 · p. 2
2 The pipeline and the metric
The pipeline converts C into terms of a Lean 4 interpreter and reports attempted translation through separate structural measures. Its coverage ledger excludes definitions the parser never emits.
2 The pipeline and the metric
- C code is mechanically transpiled into terms of a compact universal-language interpreter written in Lean 4, so translated programs can be run and compared with the language implementation.The interpreter is fuel-indexed and total, with no partial or sorry.Source: §2 · p. 3
- Joern’s code property graph supplies a shared node vocabulary for a deterministic CPG-to-JSON exporter and JSON-to-Lean printer, with unsupported constructs recorded as labeled holes.The pipeline uses no model on the translation path.Source: §2 · p. 3
- The three structural coverage measures are not correctness claims; call closure excludes unresolved direct calls but does not follow calls transitively or establish what resolved callees do.Dynamic-hole risk counts constructs that may still produce a hole on some input.Source: §2 · p. 3
- Because Joern parses C without running the preprocessor, signatures that defeat its parser can be absent from the ledger rather than counted as holes.Coverage therefore accounts for what was attempted, not everything the codebase contains.Source: §2 · p. 3
3 Coverage and fidelity move independently
The section documents six cases where translation behavior and coverage moved independently, plus a defect in the metric’s vocabulary. Its findings are organized around what changed in the translated program and what the coverage metric recorded.
3.1 Correctness changed and the metric did not move, or barely moved
- A1 fixed character literals that had silently produced wrong results, yet the hole count and every individual label stayed at 5,033 before and after on 3,560 functions.The corrected loop returned 3, 2, and 0 for n = 9, 3, and 1, matching compiled cc; digit literals remained wrong for a separate reason.Source: §3.1 · p. 4
- A2 and A3 silently mistranslated do-while loops and C variadic calls without holes, so coverage could not distinguish their incorrect translations from correct ones.The do-while repair changed seven C++ functions; the C vararg marker made surplus arguments bind as a tuple under Python’s convention.Source: §3.1 · pp. 4–5
- A4’s struct-address defect moved hole-free coverage by only 0.05 and 0.12 percentage points, while B1’s apparent 31-hole improvement was mostly relabeling rather than closure.In B1, 16 occurrences remained holes and 15 closed; hole-free increased by one across 14 changed functions.Source: §3.1 · p. 5, §3.2 · p. 5
3.3 A corrected claim, with no movement either way
- Function-pointer dispatch was analysis-recoverable, not fundamentally unresolvable: widening a scan closed 19 function-parameter pairs, changed 17 translations, and added zero hole-free functions.The paper distinguishes boundary-dependent limits, analysis-recoverable constructs, and representation-limited constructs; it does not claim the other classes are empty or that the ledger is free of misclassifications.Source: §3.3 · pp. 5–6
- The same change exposed a defect in its own fixed-point check: a lazy value cached an empty snapshot, so the mechanism showed zero effect until changed to a def.The authors caution that a check sharing an assumption with what it checks can flatter that system; here the shared assumption was a cache.Source: §3.3 · p. 6
3.4 The metric’s vocabulary is not stable either
- T1’s source-text-based labels made fragments appear to be separate causes; switching to parser-node types collapsed 15 labels to two, and the reported 70 causes are export-specific.The number of distinct hole causes cannot be compared across pipelines or corpora without knowing how labels are built.Source: §3.4 · p. 6
3.5 What surfaced them, and what did not
- None of the four correctness defects appeared in either the coverage rate or itemized inventory; only B1’s two relabelings were visible in the breakdown.The authors use this contrast to argue for itemizing declined constructs by cause rather than reporting only an aggregate rate.Source: §3.5 · p. 6
4 Read purely as coverage, the reported figure depends on the denominator
The SQLite export contains 8,602 functions and 1,513,464 AST nodes; its coverage figures differ substantially by denominator, while declined causes and dynamic-hole risk are reported at other units.
4 Read purely as coverage, the reported figure depends on the denominator
- 5,222 functions (60.7%) are hole-free, but only 2,134 (24.8%) are call-closed in the 8,602-function SQLite export.The export contains 1,513,464 AST nodes.Source: §4 · p. 6
- 14,260 residual holes are itemized under 70 causes, while dynamic-hole risk applies to 216,730 constructs rather than functions.The 70-cause total reflects the labeling scheme, not an intrinsic count of codebase categories.Source: §4 · pp. 6–7
- The figure’s dashed region represents silently incorrect translations, which may be hole-free and call-closed and are not excluded by either denominator.The figure is not to scale; only the three function sets are nested, while its right-hand column counts occurrences and constructs.Source: Figure 1 · p. 7
- 2.45× is the measured gap between hole-free and call-closed functions, reflecting direct calls that do not resolve inside the export.Those calls include calls into the C library; the authors do not claim the factor transfers to other codebases.Source: §4 · p. 7
- Declined constructs are dominated by C pointer and address semantics; the ten largest named causes total 9,101 occurrences, calculated from their listed counts.Another 5,159 occurrences are spread across 60 further causes.Source: §4 · p. 7
5 What we report instead, and why it is not sufficient
The paper proposes keeping three coverage tiers distinct, itemizing declined constructs by cause, and checking representative constructs through execution against the language implementation. These checks remain insufficient to establish population-level conformance for the SQLite export.
5 What we report instead, and why it is not sufficient
- Report three coverage tiers without collapsing them, itemize each declined construct by cause, and execute at least one fixture per construct family against the language implementation.The tiers make the denominator explicit; cause itemization also makes relabeling visible.Source: §5 · p. 7
- About 40 lines per fixture can record the correct value and retain the defective shape as a negative control, so a regression cannot present itself as progress.The specifications need no infrastructure beyond the proof assistant already in the pipeline.Source: §5 · p. 7
- Four independent checks support the execution step: runtime differential testing, a mutation gate, an axiom sweep with fresh-kernel replay, and an execution oracle for the claimed call-closed population.The assurance case tracks evidence kind separately from strength and caps population claims by coverage.Source: §5 · p. 8
- No SQLite export function has been checked by an oracle at population level; fixture execution supports existence claims, not how many further defects remain.Population checking requires a SQLite reference runtime, pointer and struct argument encoding, and an input policy.Source: §5 · p. 8
6 Limitations
The paper’s decoupling cases establish existence, not frequency, and come from one system and a single SQLite coverage export. Oracle checks are limited, and fidelity is tested rather than proved.
6 Limitations
- SQLite’s hole-free and call-closed functions have not been checked against an oracle at population level; the executed oracle checks use hand-built fixtures.The fixtures use defined-behavior C programs with int arithmetic and byte reads, not calling-convention details.Source: §6 · pp. 8–9
- No frequency claim follows from these cases: they are not a defined-population sample, and another large codebase could show hole-free and call-closed functions coinciding.The 2.45× denominator effect could therefore be specific to SQLite and its calls outside the export.Source: §6 · p. 8
- All seven findings come from one system, while the coverage measurement is one SQLite export; three findings were measured on a C++ corpus.The authors distinguish exporter defects from coverage figures, which are properties of their corpus.Source: §6 · p. 8
- The coverage artifact records no export command, parser version, source revision, or companion AST, so its correspondence to the exporter’s commit cannot be confirmed.The authors say the internally consistent tier ratio and per-cause distribution remain properties of an export of this codebase if it is stale.Source: §6 · p. 8
- No theorem relates the CPG, exported JSON, printed Lean, and source-program meaning; the evidence is execution against a compiler plus printer determinism.A4 also lacks a fixture and negative control.Source: §6 · pp. 8–9
7 Related work
Related work offers taxonomies for observable translation failures, verified compilation, differential testing, and functional translation. The paper positions its execution-based detection of silent mistranslations as complementary to artifact-level failure partitions.
7 Related work
- Signal-coverage matrices [1] and FormalRx’s 28-category taxonomy [9] classify observable statement-autoformalization failures, whereas silent mistranslations require execution to detect.The authors claim no novelty for distinguishing declined from incorrect outputs; their distinction is that artifact partitions cannot reveal these defects.Source: §7 · p. 9
- CompCert proves a realistic compiler correct end to end, while this paper leaves its translator unproved and treats fidelity as an empirical question.The authors describe this as an intentional trade.Source: §7 · p. 9
- Random differential testing has found compiler defects; A1 and A2 apply that technique to a translator, and mutation testing informs fixture negative controls.The authors add that the defects found this way are ones coverage metrics cannot see.Source: §7 · p. 9
- Unlike Aeneas’s shallow functional translation for Rust [4], this system uses a deep embedding driven by a language-agnostic CPG so translated programs can run against cc.The paper also describes LLM-based autoformalization [10] as motivating its closing observation.Source: §7 · p. 9
8 Conclusion
Coverage can remain unchanged while correctness changes, and it can move more than correctness does. The paper argues that translated artifacts should be executed and compared with the language implementation, rather than judged by attempted coverage alone.
8 Conclusion
- Coverage can stay still while correctness changes, and it can move further than correctness does.The same mismatch applies to a model that emits a well-typed wrong answer; the paper has not measured a model-based pipeline.Source: §8 · p. 9
- The argument transfers to model-based pipelines, but the paper does not measure the quantity there.Source: §8 · p. 9
- The proposed remedy is to execute the translated artifact and compare it against the language implementation, not just count what was attempted.Source: §8 · p. 9
9 Declaration of LLM usage
LLMs assisted with engineering the artifact and preparing the manuscript, but were excluded from translation and proof checking. The exporter and printer are deterministic, and the Lean kernel arbitrates what is proved.
9 Declaration of LLM usage
Reproducibility
The artifact records each finding and its deltas, and includes scripts to reproduce selected checks and recompute reported figures. Reproducing the SQLite export itself requires a source-tree parser run, while its command and revision were not recorded alongside the numbers.
Reproducibility
- Each finding is a dated artifact change, and the deltas quoted in §3 are recorded with those changes.Source: Reproducibility · p. 10
- A script reproduces A1–A3, builds their specifications, checks theorem axiom bases, and confirms that mutating an expected value fails the build.All three specifications build under the pinned toolchain with the guards matching; the first link needs a C compiler and the third needs the proof assistant.Source: Reproducibility · p. 10
- A second script recomputes every §4 figure from the export fields and checks internal consistency, including the sum of 70 per-label counts.The figures can be checked without running the pipeline, but reproducing the export requires the SQLite source tree and a parser run.Source: Reproducibility · p. 10
- The pinned dependencies are Joern 4.0.606, Lean v4.30.0-rc1, and cc -O0 for reference values; recorded values were reproduced on arm64 after measurement on x86-64.Source: Reproducibility · p. 11
NeurIPS Paper Checklist
The checklist records the paper's existential claims and scope limits, reports reproducibility and experimental settings, and documents released assets and safeguards. Appendix A links reported figures to artifact provenance.
NeurIPS Paper Checklist
- The paper reports existential decoupling claims and a denominator measurement, while disclaiming claims about frequency and transfer.The checklist states that each figure is traced in Appendix A.Source: NeurIPS Paper Checklist · p. 11
- The stated limitations include existential rather than frequency claims, a single pipeline, mixed-corpus cases, unrecorded export provenance, and fidelity tested rather than proved.Source: NeurIPS Paper Checklist · p. 11
- No new mathematical result is claimed; Appendix B's four machine-checked theorems concern concrete fixture programs, with their axiom basis reported.Source: NeurIPS Paper Checklist · p. 11
- The checklist says findings and §4 figures can be checked from recorded changes and a committed file, while the export itself cannot be rerun without missing provenance.The artifact is available with reproduction scripts as supplementary material, but the source AST behind the coverage export is not included.Source: NeurIPS Paper Checklist · p. 11
- The checklist locates corpora, dialect, parser and toolchain pins, and per-case corpus details in the paper, while treating deterministic counts and existence claims as not requiring error bars.Source: NeurIPS Paper Checklist · p. 11
- The largest reported export has 8,602 functions and 1,513,464 AST nodes; the checklist also records no GPU use or model training and no reported time or peak memory.It states that exact regeneration is blocked by the unrecorded command and source revision.Source: NeurIPS Paper Checklist · p. 11
- The checklist identifies selective quotation of the 2.45× gap as a foreseeable misuse: quoting only the hole-free figure overstates what the tiers establish.Source: NeurIPS Paper Checklist · p. 11
Appendix A Provenance of every reported figure
- The checklist records no high-risk model or dataset release, lists licenses and documented assets, and declares LLM use outside translation and proof checking; Appendix A maps figure provenance to artifact commits.P1 adds the coverage export, and P2–P8 are also on the default branch; Table 3 lists each reported figure with its artifact field or commit.Source: NeurIPS Paper Checklist · p. 11, Appendix A · p. 12, Table 3 · p. 12
Appendix B The three pinned fixtures
Appendix B pins three fixtures by checking both the correct outcome and the deliberately defective value, preserving the latter as a negative control. The checks share one axiom basis and reject mutated expected values, but several other cases remain unpinned or require whole-program analysis.
Appendix B The three pinned fixtures
- Each fixture pins its correct value and retained defective value at build time; A1 and A2 use compiler output, while A3’s correct value is refusal.The defective value is kept as a negative control.Source: Appendix B · p. 12, Table 4 · p. 12
- All four theorems across three fixtures use {propext, Classical.choice, Quot.sound}, and mutating each expected value fails the build.The checks use neither sorry, native decide, nor a compiler-trust escape.Source: Appendix B · p. 12
- The other three §3 cases and T1 are not pinned this way; A4 could be, but remains undone.B1 and T1 concern label counts rather than program behavior, while C1 needs whole-program call-closure analysis.Source: Appendix B · pp. 12–13