What the kernel does not establish
9e785de585c0e313 · Source at the matching commit ↗The kernel checks a proof against its Lean statement. Applying that result to the selected C source also depends on the items below. These dependencies are reviewed, locked and tested; they are not discharged merely by compiling the proofs. See safety, verification policy and progress for the claim, acceptance rules and current status.
1. Kernel and permitted axioms
The Lean kernel and propext, Classical.choice and Quot.sound are trusted.
The declaration audit permits only those axioms. Fresh kernel replay checks the compiled
proof closure; execution tests do not replace it.
2. Runtime and object schema
ZlibF/Runtime/ defines what a translated run means. Space.lean supplies object references
and updates. Monad.lean supplies faults, sequencing and loops. Ptr.lean supplies pointer
arithmetic, loads, stores and comparisons. Libc.lean models the required library operations;
Alloc.lean imports it. Schema.lean, Tables.lean and LibcTables.lean supply generated
records, constants, heap tables and operations for each struct kind. Their generator and
runtime schema are part of this dependency.
A no-fault theorem concerns these definitions. The intended correspondence is that reachable
C undefined behaviour becomes Fault.ub, subject to the limits below. Unsigned arithmetic is
modular. Each translation must check signed arithmetic, shifts and conversions. Loops have
fuel 2^64; exhausting it is Fault.outOfFuel, which termination proofs must exclude.
Memory and library operations
The heap has separate tables for object kinds. Freed block numbers are never reused. Allocators
write at nextBlk only if that identity is unused there; otherwise they fault. Fresh protects
future identities. The initial heap must also have unique block identities across tables below
nextBlk; Fresh alone does not express that condition.
| Operation | Model behaviour requiring review |
|---|---|
memcpy, zmemcpy |
Reject null pointers even for zero length, overlapping ranges and read-only destinations. Whole-record copies use copyK, which rejects copying an object onto itself. A bare load/store record pair does not check overlap. |
memmove |
Checks the same ranges and writability, but permits overlap and copies from the original source. |
memset, zmemzero |
Ptr.fill counts elements and assigns a value; it represents byte memset or zero filling only in the stated uses. Ptr.memset replicates a byte. Whole-record zeroing stores the explicit zero record. |
strlen |
Requires a NUL inside the represented block. |
| Allocation | Fresh integers come from the arbitrary garbage function; fresh pointer fields are NULL. The allocOk oracle determines failure. Automatic local objects bypass that oracle and do not consume an allocator attempt. |
free |
NULL is a no-op. Otherwise the argument must be the start of a live writable allocation of the represented kind. There is no allocation-origin tag. |
| String literals | strLitRef denotes a static read-only NUL-terminated entry in the generated closed strTable. It is always live, has stable identity and is never freed. Unknown literal text faults. Other external strings use a different allocation path. |
The runtime does not provide general models of calloc, realloc, formatting, errno,
abs or strerror. Translations provide the particular behaviours they need. These definitions
also require review; their placement outside Runtime/ does not reduce their semantic role.
Representation gaps and proof obligations
| Choice or gap | Consequence for a C claim |
|---|---|
| Uninitialised pointers become NULL | Equality, copying and freeing NULL can succeed without a prior write. Every pointer read needs a write-before-read argument. The init translations explicitly zero the two allocated stream-state records; this is not a general property of fresh records or automatic z_stream storage. Closing the gap requires initialisation tracking or a distinct uninitialised value for all pointer forms, with checked operations and corresponding translation changes. |
| One garbage value per cell | Integer theorems quantify over every Heap.garbage, indexed by allocation attempt and cell position. Repeated reads of a cell nevertheless agree. Proofs must not rely on that agreement where C permits unstable unspecified values. |
| Array extents are predicates | WellFormed, Heap.RecordsWellFormed and Statics.WellFormed must establish C lengths. Generated preservation lemmas retain them. Static contents must match the defining C translation; the runtime does not compare them with C. |
| Pointer equality is structural | Different objects compare unequal; equality of dangling pointers does not fault. Proofs must not rely on outcomes that C does not guarantee, including equality at adjacent object boundaries. Relational comparison requires the same live array. |
| Null arithmetic is partly permitted | Ptr.add NULL 0 returns NULL. Ptr.diff rejects null arguments, but Compress.ptrDiff returns zero for two nulls. These choices require a separate definedness argument for the corresponding C calls. The Ptr.diff comment's C23 attribution is inaccurate; see the operation and language comparison. |
| Address and layout model is partial | There is no general ABI address, effective-type or record-byte-view model. CRC observes low address bits: heap byte blocks retain aligned origins; static and embedded byte origins have arbitrary stable residues. The metadata can be configured without changing any existing storage. Byte-assembled word loads do not settle the C cast's aliasing semantics. Scalar-cell adapters may omit aliases. See deviations. |
| Read-only marking is partial | Byte blocks, named static tables and instances can be read-only. Word blocks and records in tables cannot represent that qualifier. |
| Pointer construction checks are partial | Ptr.add checks its result, not whether a manually constructed starting offset was valid. Translation review must exclude invalid uses of the public Ptr.ref constructor. |
| Object origin is not tracked | A caller block created by allocBytes can be freed by translated code. Frame and ownership clauses must prevent this where the API forbids it. A wrong-kind state cast faults earlier than the corresponding C access. |
These are limits of the model, not permission to narrow a public theorem silently. The runtime review is historical evidence about these choices, not independent approval of the current baseline.
Table updates
Tbl wraps an array and reads as a total function of block identity. Missing entries return
the default (none or false). upd has proved same-key, different-key and repeated-update
rules from Tbl.get_set.
Writing primitives use Space.modify to remove, modify and replace an array without retaining
a chain of previous arrays. Space.modify_eq states equality with the simpler functional
put operation. The trusted review must cover Tbl.get_set, Tbl.modify_eq and every generated
Space instance's modify and modify_eq. The operation lemmas reason with put; execution
performance does not establish their correspondence. See the
table-update review.
3. Manual translation
The translation in ZlibF/Zlib/ is written statement by statement. The kernel does not check
its correspondence to C. Review must check evaluation order, checks, arithmetic, storage
lifetime and effects. A mismatch is a translation bug; it must be corrected with a differential
regression, never hidden by changing a theorem. The translation rules
require evidence for each function. The test inventory is tests/list.txt.
Differential tests compare finite executions against the real C. They are evidence of fidelity, not proof. In particular, agreement and a silent sanitizer do not establish that a C expression has defined semantics.
4. Selected source
The verified source is the pinned zlib/ submodule plus patches/*.patch in name order.
The submodule is never edited. A patch is permitted only for a confirmed upstream bug blocking
a proof; it must be minimal and match a submitted upstream fix. It is removed after the fix is
merged and the pin moves past it.
There are currently no patches. The patch register records the selected-source policy. Historical proposals are not part of the verified source merely because notes mention them.
5. Configuration and external world
The first target is the default x86_64 Linux/LP64 static build with the default allocator.
The accepted platform scope requires each represented byte
object to have fewer than 2^63 bytes. This is an environment premise; zlib
proofs establish that their operations preserve it.
Allocation failure remains in scope. Other upstream configurations and custom allocators
require their own correspondence arguments; the full project goal includes them.
The gz file world and formatting model are additional trusted semantics. Their supported file kinds, errors, conversions and external string allocation do not represent every operating-system or library behaviour. Callback correctness relies on the explicit returning protocol, finite input bound and window-preservation assumptions. Deviations records the consequences for the public adapters. Compiler, operating-system and hardware correctness are outside the proof.
6. Statements and authority
A proof can establish an incomplete or wrong specification. Reviewers must compare the target, its preconditions and named specification identifiers with the API, format and selected C. They must also confirm that init establishes the invariant and that the caller domain has not been reduced.
Locks preserve definitions and theorem types; they do not approve their meaning. Independent baseline review and enforced repository protections supply that authority boundary. The verification policy explains it. Current checked results and unresolved obligations belong in progress.