libheif in Low*

Part of libheif's reading path, reimplemented in Low* and extracted to C by KaRaMeL. The box layer is complete and proved; the API over it covers 8% of libheif's surface. See What is not.

nix-shell --run 'make check'     # proofs, both corpora, and every test below

What is proved

Three theorems, machine-checked, for the box layer:

(1) spec_parse (spec_serialize v) == Some (v, |spec_serialize v|)   -- complete
(2) spec_parse b == Some (v, n)   ==> spec_serialize v == b[0..n)   -- non-malleable
(3) impl_parse b                  ==  spec_parse b                  -- refinement

(1) and (2) say the F* specification is the ISO/IEC 14496-12 byte format rather than some arbitrary function of bytes: every value has exactly one encoding, and every well-formed encoding parses back to the value that produced it. (3) says the extracted C computes exactly that — memory-safely and terminating, since it is Low*. Without (1) and (2), (3) would be vacuous.

On top of that:

• Nesting is bounded by construction. The box tree is validated to a depth index rather than a runtime counter, so a maliciously nested file cannot recurse — libheif checks the same bound (MAX_BOX_NESTING_LEVEL = 20) at run time to avoid stack exhaustion.
• Item extents cannot escape the file. resolve_extent is the only way to turn an iloc offset — an arbitrary 64-bit number from the input — into a readable range, and it returns one only if the range is inside the file.
• Colour conversion is bit-identical to libheif, checked over all 2²⁴ (y, cb, cr) triples, with no overflow and every plane access in bounds.
• Derived images terminate by construction. iden, grid and iovl are composited by a recursion whose bound is its decreases measure, so a file nesting them deeper than the limit is refused and a circular one terminates -- neither depending on a runtime counter being checked in the right place.
• A plane's sample width is part of its type. An 8-bit and a 16-bit plane are different types carrying different buffers, and a channel is a field rather than a list entry, so the shape of CVE-2026-84383 -- two Alpha planes of different depths, one allocation written at the other's width -- has no expression here. ISSUES.md works through which of its four steps that rules out and which it does not.

Trust base: the specification matching the ISO documents, plus F*, Z3, KaRaMeL and the C compiler. No assume val — the byte readers are built from LowStar.Buffer.index rather than the axiomatised LowStar.Endianness primitives, to keep it that way.

What is not

This is a subset of libheif's reading path, not a replacement for libheif. api/heif.h implements 38 of libheif's 464 public functions — about 8%. The metadata subset of those 38 that make compat exercises — opening a file, counting and listing top-level images, the primary item, size, alpha, thumbnails and bit depth — answers identically to libheif 1.23.3 on all 48 files of MPEG's conformance suite. The other 426 functions are not stubs; they are absent.

area	have / total
context (open, enumerate, primary item)	8 / 13
image handle (size, alpha, depth, thumbnails)	15 / 31
decoded image (planes, geometry)	12 / 31
library (init, version)	7 / 17
decoding (heif_decode_image + a decoder hook)	1 / 11
auxiliary images	1 / 14	alpha detection only
encoding and writing	0 / 45
colour profiles (ICC, NCLX) and conversion options	0 / 46
generic property read/write	0 / 43
component descriptions	0 / 39
region annotations	0 / 37
generic item read/write	0 / 23
ftyp brands	0 / 13
text, TAI timestamps	0 / 24
Exif and XMP metadata	0 / 10
tiling, unci API, OMAF, entity groups	0 / 20
security limits	0 / 5
encoder/decoder plugin registration	0 / 2	heifv_register_decoder instead
sequences and tracks	1 / 66

Two kinds of gap, and they are not the same size.

Missing API over parsing that already exists. The spec layer covers 44 box types including ftyp, taic, grpl, udes, ipco/ipma and mime, and heifv_item_get_data reaches any item's bytes. Brands, Exif/XMP extraction, TAI timestamps, entity groups and the generic property API are mostly a matter of exposing what is already parsed and proved.

Genuinely unbuilt. Encoding and writing — Heif.Impl.Write has the serialisation primitives and the round-trip theorem, but there is no whole-file writer and no encoder. Sequences and tracks: moov/trak/stbl are not parsed at all. Colour profiles: colr is not in the spec layer, so ICC and NCLX are new verified work, not plumbing. Regions (rgan) likewise.

Coded images are not decoded here. libheif delegates HEVC/AV1/JPEG/VVC to external codecs through a plugin interface, and so does this: heifv_register_decoder takes one, and heif_decode_image returns heif_error_Unsupported_feature without it. Two things are decoded natively — unci (uncompressed) items, which have no entropy coding to delegate, and the derived types grid, iovl and iden, which are composited from whatever the leaves decoded to.

PLAN.md has the phase breakdown and how much of each is trusted glue rather than verification; COMPAT.md lists the ten places the API deliberately differs from libheif, and nine more where libheif parses differently from the standard.

Results

MPEG HEIF conformance suite	48/48 parsed completely
libheif well-formed corpus	105/105 parsed completely
independent C walk vs. extracted proof	0 disagreements over 237 files
item extents resolved	239, 0 unreadable
colour conversion vs. libheif	2²⁴ triples, 0 mismatches
compat API vs. libheif 1.23.3	identical on 48/48 files (strict mode)
derived-image placement	5/5 grids and nested iden chains correct

The four extents reported as outside the file all come from pclr_zero_columns.heic, which is 3,173 bytes and declares extents ending at 718,098. Refusing them is the point.

Performance

make bench, against libheif 1.23.3 from nixpkgs, same machine, same flags, alternating order, best of N trials. Minimum rather than mean: both sides do the same work on the same bytes, so every difference between trials is interference, and interference only ever adds time.

	verified	reference	ratio
opening a file (48-file corpus)	0.73 µs/file	0.73 µs/file (libheif)	1.00x
YCbCr 4:2:0 → RGBA, 1920×1080	4.68 ns/px	4.66 ns/px (libheif's integer path)	1.005x
compositing a 2×2 grid of 1280×720 tiles	53 Gpx/s	49 Gpx/s (row-wise memcpy)	~1.0x

Three things are worth saying about those numbers rather than leaving them to be read off.

Opening a file costs the same, but this does more. 65% of the open here is validating the entire box tree to the nesting limit against the format specification -- that is what heif_context_read_from_memory means in this library. libheif parses the boxes it needs. Neither reads the payload: a box header carries its own size, so mdat is stepped over, and the cost tracks the number of boxes rather than the size of the file. C025 is 19 KiB and C007 is 535 KiB, and both open in about a microsecond.

The colour converter is bit-identical, not merely close -- all 2²⁴ input triples agree with libheif's integer path -- and getting it to parity took two codegen fixes rather than any change to the algorithm. The rounding divide is done unsigned so gcc emits a shift instead of the sign-correction sequence a signed divide by a power of two needs, and the loops are C.Loops.for so KaRaMeL emits a real for that gcc can hoist the row bases out of. Both are commented in Heif.Impl.Color with the measurement that motivated them.

The blit was 13x slower before it was measured. It was a per-sample loop: correct, proved, and pointless, because the bound it establishes is the same one a row-wise copy needs. B.blit is verified and extracts to memcpy, so the fix cost nothing in assurance. That is the general shape of the three results -- where this is slower than libheif it has been a code-generation or loop-shape problem, not the proofs.

Layout

path	contents
spec/Heif.Spec.Format	valid laws; uintbe, lbytes, map, filter, bind
spec/Heif.Spec.Exact	evalid; exact, exactly, all, list, nlist, region
spec/Heif.Spec.BE, .Cstring	big-endian bridge; NUL-terminated strings
spec/Heif.Spec.Box	box header (§4.2), fmt_box, fmt_boxes
spec/Heif.Spec.Body, .Codec	all 44 box payloads; hvcC, av1C
spec/Heif.Spec.Dispatch, .Tree	fourcc → format; depth-bounded tree
src/Heif.Impl.Slice, .Validate	input view; validator/reader combinators
src/Heif.Impl.Body, .Box, .Dispatch, .Tree	validators for every format above
src/Heif.Impl.Item	iloc extent resolution
src/Heif.Impl.Meta	readers for pitm, iinf, ipma/ipco, iref, ispe
src/Heif.Impl.Props	irot, clap, grid, iovl; depth from hvcC/av1C
src/Heif.Impl.Image	planes, allocation, scaling, the clipping blit
src/Heif.Impl.Compose	tile placement; sub-plane views
src/Heif.Impl.Render	iden/grid/iovl; multi-extent and idat items
src/Heif.Impl.Unci	uncompressed frames (ISO/IEC 23001-17)
src/Heif.Impl.Color	YCbCr → RGBA
src/Heif.Impl.Write	serialisation primitives
api/heifv.h, api/heifv.c	the native API: ranges, extents, planes
api/heif.h, api/heif_compat.c	the libheif-compatible API
test/	box walk, item dump, exhaustive colour check, libheif diff, placement
bench/	open, colour conversion, compositing — each against a reference

Building

krml is built once from the karamel/ checkout; nixpkgs has no karamel derivation. karamel/flake.nix is more hermetic but rebuilds F* from source, whereas the nixpkgs F* is binary-cached and was checked compatible with this krml. make conformance fetches MPEG's suite over git-lfs.

Conformance

COMPAT.md lists every place libheif parses differently from the standard — nine cases, all of them libheif accepting two byte strings as the same value, which property (2) forbids — and ten more where api/heif.h deliberately differs from libheif, four of which heifv_set_libheif_strict switches off.

ISSUES.md records memory-safety findings. In libheif: none so far, which is a real result given the 132 fuzzer crash inputs in its corpus. It also records what CVE-2026-84383 would and would not have been caught by, one defect found in this code by the placement test — a base offset added twice, silently wrong but never unsafe, because resolve_extent refused every doubled offset that fell outside the file — and the layers still out of scope.

Grounding is MPEG's machine-readable box syntax (300 definitions across 14496-12 and 23008-12) and its HEIF conformance suite, both freely available; the normative prose is paywalled and is not used. Cross-checking against it found two places where libheif's non-normative behaviour had been copied into this parser, and one design bug: box semantics are container-dependent, and inside iref a child's fourcc is a reference type rather than a box type.