From C to a checked theorem

A theorem is about a Lean computation. Applying it to zlib requires two reviewed connections: the runtime must represent the relevant C operations, and the translation must match the selected C source. The kernel checks the proof after those choices. It does not check either connection to C. Trusted base records that boundary.

The layers

flowchart TD
    C["Pinned zlib source + ordered patches"] --> T["Statement-by-statement translation"]
    R["Runtime: objects, pointers, arithmetic, faults, loops"] --> T
    T --> P["Execution proofs: no fault, termination, frame, ownership"]
    T --> F["Refinement proofs"]
    M["Heap-free algorithm and API models"] --> F
    S["Independent format specification"] --> M
    S --> F
    P --> A["Public calls and legal call sequences"]
    F --> A

Safety and functional correctness use the same concrete states. Heap-free mathematics belongs in ZlibF/Math/; it should not acquire heap dependencies merely because a memory proof uses it. An intermediate algorithm model is useful when it separates mathematics from memory reasoning. It still needs a refinement proof connecting it to the translated function.

Selected source and module layout

The first target is the default x86_64 Linux static build with LP64 widths and the default allocator. Allocation failure is in scope. Other build configurations and custom allocator implementations are separate scope, recorded in representation limits. The source submodule is never edited. A patch is permitted only for a confirmed upstream bug, under the rules in the repository's AGENTS.md and patches/README.md.

Large C-file modules may have supporting submodules. Function names remain the C names. A function's docstring begins with its C signature. The translation rules describe the correspondence in detail.

Why an object heap

A C struct is represented by a Lean record. A heap has separate tables for records, byte arrays, word arrays and other element kinds. A pointer names an object or an embedded/static array, plus an element index. It does not contain a machine address.

flowchart LR
    P["Pointer: null, or reference + index"] --> B["Heap byte/word block"]
    P --> E["Array embedded in a record"]
    P --> S["Static array"]
    H["Heap"] --> B
    H --> K["Record tables: stream, inflate state, deflate state, …"]
    K --> E
    H --> O["Allocation oracle, fresh block counter, garbage values"]

This makes field updates and framing direct. A record field is a projection; changing it is a record update. Updating bytes cannot change a record in another table. Copying a whole record also copies its embedded arrays. The generated runtime schema gives the complete fields, pointer constructors and type choices.

The representation deliberately avoids ABI byte offsets. It therefore cannot give a byte view of an arbitrary struct, or represent every possible alias between a scalar cell and a buffer. Array field lengths are not enforced by the record type. WellFormed, Heap.RecordsWellFormed and Statics.WellFormed supply those facts where needed. A proof must carry them or derive them from its representation invariant.

Execution and faults

The runtime exposes a return value and final heap, or a fault. Fault.ub represents the undefined operations covered by the model. Fault.outOfFuel represents an exhausted loop bound; a termination proof excludes it. The safety definition gives the full obligation.

The language operations live in Space.lean, Monad.lean and Ptr.lean. Modelled C library operations live in Libc.lean and generated LibcTables.lean. The generated schema and record access operations are in Schema.lean and Tables.lean.

Semantic differences that proofs must respect

These are design limits, not extra claims about C. The authoritative details are in trusted base and representation limits.

Automatic storage must retain its C lifetime and must not consume a default-allocator failure index. Locals whose addresses escape into a call still need represented storage and cleanup. No proof may repair a representation gap by silently restricting the public domain.

Design decisions

These identifiers keep earlier design discussions traceable. They describe the chosen approach; their soundness obligations remain in the trusted-base and proof guides.

Composing calls without assuming their answers

A helper theorem proves a property of the actual translated helper. Its caller establishes the helper's precondition and then uses that theorem. A helper contract is never an assumption that replaces execution. Internal obligations names the conditions that callers must establish.

One representation invariant per state record carries bounds, ownership and the history needed for correctness. Initialisation establishes it; later calls preserve it; end functions release the owned storage. This establishes that the invariant is reachable. Whole-sequence proofs then compose those function theorems, including refusals and failed allocations. See the proof guide for the method and checking guide for what counts as an accepted result.

Design guide · Documentation home