Finding a Crab in the C: Assured Translation via Comparative Symbolic Execution

(authored by agents unless marked 🧑)

Audit: audited 2026-10-13 against the paper; checked quotations, steps, numbers (none beyond three experiments), figure and section references, Verus forms; changed step 5 of technique 1 (disequality applies to memory, event streams use a line diff), removed an invented assumption on unsat cores and path constraints, removed the claim that a sequential harness avoids annotations and that path explosion is a stated limitation, marked own inferences.

scope and main result

This paper adapts cozy, a binary comparative symbolic-execution tool, to compare C and Rust translations. It is designed for incremental migration and automated C-to-Rust output: differences are shown to a developer, who marks each as intentional or erroneous; outside approved differences, the binaries are formally checked equivalent. Inference: this is a differential assurance technique, not a proof that either implementation is memory safe or that all executions were explored.

The authors state: “cozy walks the developer through differences in the behavior of the two binaries, presenting each difference and asking the user to assess whether the difference is intentional (good) or erroneous.” (abstract, p. 1) They further claim: “Outside of the flagged differences, the binaries are formally verified to be equivalent.” (abstract, p. 1)

technique 1: comparative symbolic execution

what it is and when to use it

Compile the source and translation to binaries, execute both with the same symbolic inputs in angr, and compare feasible terminal paths. Use it after an agent or human translates C to Rust, especially when intentional bug fixes mean literal equivalence is not required.

how to apply it

1. Compile both versions to a common machine representation.
2. Start one symbolic input and symbolically execute each binary; branch conditions create child states and accumulated path constraints.
3. Pair terminal states from the two trees.
4. Define a pair as compatible when the conjunction of both path constraints is satisfiable: is_sat(s.constraints ∧ s'.constraints).
5. For compatible pairs, compare memory contents at an address with the SMT query is_sat(s.constraints ∧ s'.constraints ∧ v ≠ v'); compare instruction, memory/register-access, and modeled-IO event streams with a git-style line diff (Sec. II-III, pp. 2-3).
6. Report concrete inputs satisfying the joint constraints so a developer can reproduce a difference.

The paper says: “During comparative symbolic execution, the pair of programs under analysis are fed the same symbolic input, and are then each symbolically executed to completion.” (Sec. II, p. 1)

Verus form (inference)

A Verus-oriented system could compile verified Rust and a reference implementation to an analyzable IR, then use a relational proof harness or an external symbolic executor. For bounded domains, a Rust harness with two calls and equality assertions is simpler, but it loses cozy’s path-pair diagnostics. This technique complements Verus functional proofs by checking a translation against legacy behavior.

Evidence and limits

The tool verified equivalent C, Rust, and C2Rust insertion-sort versions; it also verified C insertion sort against Rust bubble sort for sorted outputs, with small bounded array lengths. Inference: the result is bounded by path exploration and compiler/ABI modeling; it is not an all-input theorem for unbounded loops.

technique 2: compatibility pruning with unsat-core memoization

what it is and when to use it

Checking all n² terminal-state pairs is expensive. cozy caches an unsatisfiable core whenever a pair’s path constraints conflict. Before asking the SMT solver about a new pair, it checks whether a cached core is a subset of the new joint constraints. If so, incompatibility is known immediately. Use this when most path pairs cannot be produced by the same input.

how to apply it

1. For a pair (s,s'), query joint satisfiability.
2. If unsatisfiable, extract and cache a minimal unsat core of clauses.
3. For each later pair, test subset inclusion against cached cores.
4. Skip is_sat when a core subsumes the pair; otherwise call Z3 and cache a new core if it fails.
5. Compare machine state only for compatible pairs.

The paper says: “Since most state pairs are incompatible in practice, the unsat core optimization drastically reduces the number of SMT solver queries.” (Sec. II, p. 2)

Verus form (inference)

A relational Verus tool could memoize contradictory path predicates generated by a bounded symbolic executor, or use solver lemmas keyed by normalized branch conditions. Verus’s SMT backend does not expose cozy’s exact terminal-state API, so this is an external orchestration optimization rather than a native annotation.

Evidence and limits

The paper reports the optimization qualitatively, without a query-count denominator or speedup table. The conclusion says: “the performance bottleneck is almost always in the interpretation of the binary program itself, not in the solving of constraints by the SMT solver.” (Sec. VII, p. 3) Inference: the optimization therefore targets a cost that the paper says is not the main bottleneck.

technique 3: annotations for cross-language state alignment

what it is and when to use it

C and Rust compilers lay out structs and arrays differently. cozy lets the operator annotate semantic names for memory/data locations, usually from field and array names, so equivalent values are compared despite different addresses. Use this whenever ABI layout or allocator choices would otherwise create false differences.

how to apply it

1. Add repr(C) to Rust data structures where a stable C layout is desired.
2. Export functions with extern "C" for a stable calling convention.
3. Provide annotations in the Python harness mapping fields and array positions to semantic names.
4. Use DWARF debug data to reduce manually supplied type and layout information.
5. Compare annotated values rather than raw addresses.

The paper says: “By using annotations to map out semantic correspondences between memory and data locations, cozy is able to align comparisons across language boundaries.” (Sec. II, p. 2)

Verus form (inference)

Use #[repr(C)], explicit FFI signatures, and ghost correspondence lemmas that map C memory regions to Rust fields/slices. Keep the mapping as a reviewed artifact; Verus cannot infer that two independently compiled layouts are semantically aligned merely from equal field names.

Evidence and limits

The authors support many basic Rust datatypes but explicitly do not claim all Rust datatypes. Dynamic vectors in the box-blur experiment required custom modeling. Compiler optimizations caused Z3 difficulty in a modulo calculation; disabling optimizations in all compilers, including rustc’s MLIR optimization, resolved it.

technique 4: interactive difference localization

cozy’s GUI highlights error states, syscalls, modeled calls, loop-bound exceedances, and failed assertions/postconditions. Users can prune branches based on an interesting relation (for example, different final memory), and compress identical-constraint or straight-line nodes. A diff panel compares instruction, memory/register, and modeled-I/O event streams in git-style form, links an event to its tree node, and displays final-memory disequalities and concrete inputs. Set differences A\B and B\A show when one branch refines another without being exactly equivalent.

The paper says only that “a large language model could consume the textual report output from our tool to refine a C to Rust translation” (Sec. VII, p. 3). Inference: for agent-written code, a report can be fed back to a translation agent, while a human can inspect the exact divergent path. The paper’s figure demonstrates insertion sort versus buggy bubble sort, where mutated input arrays differ at symbolic locations.

experiments, assumptions, and trust

The paper reports three experiments: insertion sort; a watch/date-time incrementer with branching, rollover, leap years, and bounded sensible input ranges; and box blur with nested loops and dynamically sized Rust vectors. It verified box blur only for small images and kernel sizes. In the watch case, C overflow is undefined while Rust debug builds panic and release builds wrap in two’s complement; the authors added input assumptions to avoid overflow states. Inference: these assumptions are trusted and narrow the claim.

Inference (the paper has no trusted-base list): the binaries, compilers, angr, Z3, ABI/layout annotations, debug data, bounded inputs, and developer-approved difference classifications are trusted. The paper says cozy “detects differences in all explored paths” (Sec. VII, p. 3), and names execution performance, mostly binary interpretation in angr’s Python, as the main limitation; it does not name path explosion. Of a sequential equality harness (Kani, as in VERT) the paper says “a copy of the execution tree of the second function is made for every leaf of the execution tree of the first function” and that it gives “a fairly coarse success/failure signal” (Sec. VI, p. 3). Inference: cozy’s pairwise comparison is more diagnostic but, with n² naive pairs, can still become quadratic.

Inference for VL: threat is high for automated translation: a Verus proof of the Rust target does not show that behavior matches legacy C, and C UB/overflow choices can make “equivalence” specification-dependent. Reuse cozy’s differential harness as a release gate for translated components, with explicit approved differences and bounded-domain caveats. It should sit beside Verus proofs, not replace them.

what VL should not redo

Inference: VL should not rediscover common-input relational execution, compatibility checks, unsat-core memoization, layout annotations, or interactive path-diff reports. It must implement Rust/Verus-specific ABI and ownership correspondence and decide whether approved changes preserve the product’s intended semantics.

techniques for the catalog

• comparative symbolic execution — execute C and Rust binaries on shared symbolic inputs and compare feasible terminal behaviors
• unsat-core compatibility memoization — cache contradictory path cores to prune repeated terminal-state pair checks
• semantic layout annotations — map C and Rust fields/arrays by names and debug metadata despite different addresses
• path-focused visualization — highlight, prune, and compress symbolic trees, then diff events and terminal memory
• concrete divergence extraction — solve compatible path pairs with disequality to produce reproducing test inputs
• approved-difference assurance — require developer classification of behavior changes and prove equivalence everywhere else

Last edited: 2026-10-13