Apples to Apples: Getting Type Mappings Right in LLM-Based Code Translation

What Makes a Type Mapping Correct

Deciding how types should map across languages is difficult because a choice made for one type affects how values flow through function bodies and across call sites. The right target type often depends not only on the source type itself, but also on how the program uses values of that type. A C function that takes a char * may use it to read text, write into a buffer, or access a sequence of raw bytes. Rust gives each of these uses a different type, and the C signature alone does not say which one is meant.

On the target language side, a type checker or compiler can validate that the generated code uses the chosen types consistently, but it cannot establish a correspondence between source and target values. A correctness claim about such a correspondence must begin by identifying the values for which conversion is expected to succeed. Some mappings may cover every value of the source type. Others may support only a subset and report an error for values outside it. A mapping from Python’s unbounded integers to C’s fixed-width integers, for example, cannot convert every source value.

To make this concept a little more precise, let σ be a source type in language S and τ a target type in language T, and write ⟦σ⟧ and ⟦τ⟧ for the sets of values admitted by those types. A value conversion function C_S→T takes a value in ⟦σ⟧ and either returns ok(w) for some value w in the target language or reports an error. The value conversion function C_T→S operates in the opposite direction. If σ is Python’s integer type and τ is C’s int, the value conversion function C_Python→C returns the same integer when it fits in a C int and reports an error otherwise. The reverse value conversion function always succeeds because every C int has a corresponding Python integer.

For the values a conversion function supports, conversion soundness is the key requirement: every successful result must be admitted by the target type. In symbols,

The value conversion function in the opposite direction must satisfy the same property. Note that conversion soundness guarantees that a successful conversion produces a valid target value, but it does not guarantee that the value conversion function in the opposite direction recovers the original source value.

We say a mapping is lossless for a set of source values when converting any of those values to the target representation and back recovers the original source value. In our Python-to-C example, conversion is lossless for every Python integer that fits in a C int: converting the integer to C and then back to Python recovers the original value. Python integers outside that range cannot be converted to a C int, so they are not included in the set of values for which lossless conversion is promised.

More generally, this property, called round-trip preservation, is stronger than conversion soundness. Let lossless_S ⊆ ⟦σ⟧ denote the source values for which lossless conversion is promised. Then

Thus, every value in lossless_S must convert successfully and be recovered by the reverse value conversion function. Round-trip preservation rules out value conversion functions that map different supported source values to the same target value, since the reverse value conversion function could not recover the original source value.

Taken together, the two types, the two value conversion functions, and the set of lossless values form a type mapping, which we write

A type mapping is correct when both value conversion functions are sound and the mapping is round-trip preserving on lossless_S.

Both properties come into play when a source function is compared with the translated function on the same inputs. To compare a Python function with a C translation, a test harness has to convert every Python integer argument into a C int and convert every result back into Python. If these value conversion functions are sound but not round-trip preserving, an argument or result may change during conversion and introduce a disagreement between the two functions that is not a failure of the translation.

Now that we know what makes a type mapping correct, we need to figure out how to find one. The first step is choosing a target type for each occurrence of a source type, and the earlier char * example showed that this step is harder than it looks: the same C type can represent data used in several different ways, so the declared source type alone may not determine its Rust counterpart. We begin there.

How a Program Uses Values Guides Type Translation

When the declared source type does not determine the target type, how the program uses values of that type can. We call this information program context. To see how context guides the choice of a target type, consider the following C function, adapted from Hong and Ryu’s paper on Tymcrat, an LLM-based tool for translating C programs into Rust. The function increments an integer through a pointer:

void inc(int *p) {
  *p += 1;
}

A direct translation of the function inc maps the type of the C pointer p to the Rust raw pointer type *mut i32. Dereferencing a raw pointer requires unsafe Rust, but the way the source C function uses p suggests a more idiomatic Rust type. Because inc reads and updates only a single integer at the address supplied by the caller, the type of p can be expressed in Rust as &mut i32, a mutable reference to an integer:

fn inc(p: &mut i32) {
  *p += 1;
}

The Rust compiler accepts this signature together with the translated body, but rejects one that declares p as an immutable reference, since the body writes through it.

Hong and Ryu built Tymcrat around the observation that choosing an idiomatic Rust signature can depend on how the source function uses its parameters. Before generating the body translation, Tymcrat uses the source function body to generate candidate Rust signatures and discards signatures containing type errors. It then generates a Rust function for each remaining signature, uses compiler feedback to reduce type errors, and selects a translation. This process happens in dependency order, so that the signature selected for each callee can be included in the prompt when generating callers.

Tymcrat reduced the number of type errors by 71.5 percent across 39 GNU programs, but Hong and Ryu emphasize that the absence of type errors does not establish correctness: their manual review found functions with no type errors whose translations did not preserve the original program behavior. These results show how program context can address one part of defining a type mapping: choosing target types that reflect how the source program uses values. The other part, showing that the chosen types make the mapping correct, remains open, since neither conversion soundness nor round-trip preservation follows from successful target compilation alone.

Good Type Mappings Leave No Value Behind

Once a target type has been chosen, the next question is whether source values survive the trip into the target language and back. Two types may look equivalent, and code that uses them may compile, while the target type still fails to distinguish values that the source type keeps apart. When that happens, round-trip preservation is out of reach: two different source values are forced onto the same target value, and the reverse value conversion function cannot tell them apart any longer. The authors of Oxidizer, an LLM-based tool for translating Go programs into Rust, give a concrete example. Consider the following Go structure with a field of type []int:

type EntryDetail struct {
  Addenda05 []int
}

A plausible Rust translation gives the field Addenda05 the type Vec<i64>:

struct EntryDetail {
  addenda05: Vec<i64>,
}

Both the types []int and Vec<i64> contain sequences of integers, but a Go []int value can be either nil or an empty sequence, while a Rust Vec<i64> value has only one empty representation. These two distinct Go values must therefore be mapped to the same Rust value. The Rust structure is well typed, and functions that use it may compile, but a value conversion function into Vec<i64> cannot be round-trip preserving for both Go values.

To detect this mismatch, Oxidizer introduces a notion of type compatibility. A target type is compatible with a source type when the source values being considered can be converted to the target type and back, with each round trip recovering the original source value. In the terminology of this post, a target type is compatible with a source type when there exists a type mapping between the two types that is lossless for a selected set of source values.

More concretely, Oxidizer instruments the source project and runs the project’s tests to collect input and output values for functions — i.e., the lossless_S set of the mapping. Oxidizer then implements the two value conversion functions between Go and Rust through JSON. The value conversion function C_Go→Rust serializes a Go value as JSON and deserializes the result into the proposed Rust type, and C_Rust→Go serializes the Rust value and deserializes it back into Go. Using slightly abused notation, the recorded value v satisfies round-trip preservation when C_Rust→Go(C_Go→Rust(v)) = v.

In the example above, the nil value of type []int has no distinct counterpart in Vec<i64>: either C_Go→Rust fails on it, or it produces the empty vector, which C_Rust→Go maps back to an empty, non-nil sequence rather than to nil. Either way, round-trip preservation fails for that value. Because the recorded values come from the project test suite, Oxidizer establishes round-trip preservation only for values observed while running the tests. It does not explicitly define a type mapping or otherwise characterize the values for which the mapping is correct beyond those reached by the tests. To move beyond this limited guarantee, we need a type mapping whose supported values are specified independently of a project’s tests and whose correctness can be established for all of those values.

Interface Generators to the Rescue

At Code Metal, we translate between many source and target languages, and we want to avoid writing, and proving, the same value conversion functions once for every pair of languages. A language-independent specification of values, shared by all languages, lets each language connect to the specification once instead of to every other language. Schema-based interface generators provide such a construction: they are commonly built around an interface definition language, or IDL, in which a schema describes structured values, paired with a serialization format that defines how the values described by that schema are represented as bytes. Together, the schema and the format form a language-independent specification of structured values and their valid serialized representations. A generator then produces language-specific data types, serializers, and deserializers that implement this specification.

Our approach, schema-based type mappings, uses the components of schema-based interface generators to construct a type mapping. It starts with a source type and its corresponding schema in the IDL; that is, a description of the structure of the type’s values, such as the fields of a record, the type of each field, and which fields are optional or repeated. From this schema, the generator for each supported language produces a type representing the schema values, together with serializers and deserializers for that type. For a particular source and target language, the generated types provide the two types in a mapping. The source serializer followed by the target deserializer provides the value conversion function in one direction, while the target serializer followed by the source deserializer provides the conversion in the other direction. The values described by the schema determine the source values for which round-trip preservation is promised. One possible gap remains between the generated source type and the type used in the source program, but their equivalence can be validated separately.

Protocol Buffers provide a familiar example of schema-based interface generators. Returning to the earlier EntryDetail example shows the value of this approach: the Go field has type []int, which admits both a nil slice and a non-nil empty slice, while the proposed Rust type Vec<i64> has only one empty-vector value. Converting both Go values to Rust would therefore lose a distinction that the source program can observe, while a correct type mapping must preserve this distinction.

A schema-based approach can preserve this distinction. To see how, consider the following Protocol Buffers schema, which represents the sequence inside an IntList message:

syntax = "proto3";

message IntList {
  repeated int64 values = 1;
}

message EntryDetail {
  IntList addenda05 = 1;
}

In this schema, addenda05 may be absent or may contain an IntList. When it is present, the values field may be empty or may contain elements. The schema therefore distinguishes the three cases needed to represent a nil Go slice, a non-nil empty slice, and a nonempty slice. For each supported language, a generator uses this schema to produce an EntryDetail type and serializers and deserializers for that type. The generated type must represent all three possibilities for addenda05. For Rust, a bare Vec<i64> therefore remains insufficient.

To describe this construction for arbitrary schemas and supported languages, let Σ denote a schema. In the example above, Σ is the Protocol Buffers description of EntryDetail and IntList. We write σ^Σ and τ^Σ to denote the types generated from the schema Σ for the source language S and target language T, respectively. Let W^Σ denote the valid byte representations determined by Σ and the serialization format. In the Protocol Buffers example, these are the valid binary representations of messages described by the schema. Finally, we write EΣS and DΣS for the serializer and deserializer generated for the source language S, and EΣT and DΣT for those generated for the target language T. Conversion from the representation in language S to the representation in language T proceeds as follows:

In the terminology of the first section, this construction yields the type mapping

where losslessΣS contains the generated source-language values corresponding to values described by Σ. For the mapping MΣS,T to be correct, each serializer must produce a valid encoding of the structured value represented by its input, and each deserializer must reconstruct that same structured value from any valid encoding of it. When these requirements are satisfied by the serializers and deserializers generated for S and T, they establish conversion soundness. For every value in losslessΣS, they also establish round-trip preservation: conversion to another language and back recovers the original value. These guarantees apply to values described by Σ, rather than to arbitrary values of native types.

Schema-based interface generators have also appeared as a solution to a related problem in LLM-based translation systems. CrossCrate, an LLM-based tool for translating Go programs into Rust, uses them to validate translations involving opaque library types. CrossCrate uses an LLM to synthesize a Protocol Buffers schema for source types that may contain opaque library types, as well as adapters connecting the source Go type and translated Rust type to types generated from that schema. It states a universal round-trip property requiring every value of the source Go type to survive conversion to Rust and back, and checks this property on values observed while running tests. CrossCrate demonstrates the practical value of a shared schema when source and target library types cannot be compared directly.

Verified Type Mappings at Code Metal

At Code Metal, we embrace schema-based type mappings as a general component of our translation systems. Our system makes each mapping explicit and separate from the code generated by a language model. It consists of a language-independent data description language and a generator for each supported language. These generators produce corresponding types, serializers, and deserializers for C, C++, Rust, Python, TypeScript, CUDA, OpenCL, Octave, and VHDL. The same mapping can therefore be used throughout the translation and validation of a large code base, including whenever source and translated functions are compared on corresponding inputs.

While schema-based interface generators are a major strength of our approach, they also pose a potential risk. For each supported language, one generator produces types, serializers, and deserializers for every supported schema. This means that a defect in a single generator can affect every mapping involving the language. The fact that every such mapping uses code produced by the same generator also lets us address this risk in one place. A single machine-checked proof can establish, once and for all, that for every supported schema the generator produces serializers and deserializers whose conversions are sound and recover every value promised to be lossless after a round trip. Ye and Delaware demonstrate the fundamentals of this approach in A Verified Protocol Buffer Compiler, using Rocq to verify a generator that produces serializers and deserializers for a supported subset of Protocol Buffers.

More broadly, this reflects how we build translation systems at Code Metal. We use language models to generate idiomatic code from program context while carving out core components that can be statically generated and formally verified. Type mappings and conversion code form one such crucial component. Without them, we can check that the translated code compiles, but we cannot compare its behavior with the source program on corresponding inputs. Getting type mappings right is what turns the comparison between a program and its translation into an apples-to-apples comparison: only when values are known to correspond across languages can we conclude that the translation preserves the behavior of the source program.