modelvet engineering guide

August 4, 2026 ยท View on GitHub

This guide is the repository's public engineering standard. The security contract depends on these rules being mechanically enforced, not merely on reviewer intent.

Architecture

mvet_gguf_verify validates one caller-owned, whole-file buffer in file order:

  1. gguf_header.c validates magic, version, counts, and allocates bounded span indexes.
  2. gguf_kv.c validates metadata keys, values, aggregate budget, uniqueness, and general.alignment.
  3. gguf_tensors.c validates tensor records, dtype geometry, dense offsets, data extent, and the exact end of file.

The supporting modules each own one concern: cursor.c is the only input reader, checked.c owns hostile arithmetic, arena.c owns working-memory carves, utf8.c owns strict UTF-8, span.c owns deterministic duplicate detection, and report.c is the only violation writer.

The safetensors validator follows the same shape over the same supporting modules: st.c owns the public entry, st_json.c the bounded header-JSON lexical layer, st_header.c the frame, key walks, and duplicate checks, and st_tensors.c tensor entries, the pinned dtype table, and the sorted-extent layout proof.

The library is freestanding. Code under src/ does not use allocation, stdio, filesystem APIs, errno, hosted assertions, or hidden writable global state. Hosted dependencies are confined to tests and tools, including the modelvet(1) CLI (tools/modelvet_cli.c), which maps one file read-only and exits with the verdict: 0 verified ACCEPT, 1 verified REJECT, 2 no verdict. The Python binding (bindings/python/) is ctypes over the shared library; it contains no parsing logic of its own.

C rules

  • Compile as C11 with -Wall -Wextra -Werror -Wconversion -Wshadow -fno-builtin; library objects also use -ffreestanding.
  • Use fixed-width integers for wire fields and size_t for object sizes and indexes. Initialize every object and prefer designated struct initializers.
  • Validate public arguments at the boundary. State already-proven internal invariants with MVET_ASSERT; release behavior must remain correct with MVET_NO_ASSERT.
  • Send overflow-capable arithmetic on hostile values through mvet_checked_*. Direct cursor arithmetic is allowed only after mvet_cursor_require proves the range.
  • Validate a hostile count against a named MVET_MAX_* cap before iteration. Do not add recursion or data-dependent unbounded retry loops.
  • Keep functions at one abstraction level, at most 40 lines and four parameters, with guard clauses and no more than two levels of nesting.
  • Use four spaces, no tabs, a 100-column limit, and the mvet_/MVET_ namespace. Function braces start on their own line; control-flow braces stay attached. Names describe roles and units; single-letter abbreviations are reserved for conventional local mathematics.
  • Check every fallible call. Use MVET_TRY only when early return cannot skip cleanup or another obligation.

tools/check_style.sh enforces formatting, whitespace, line length, function size, parameter count, and the configured static-analysis checks.

Reports and ABI

Malformed bytes are not API errors. A structural failure returns MVET_OK with MVET_VERDICT_REJECT. MVET_ERR_ARG and MVET_ERR_ARENA describe only caller-contract failures.

Reports preserve the first violation. mvet_violation is the sole writer, and each producible MVET_V_* value has exactly one source producer. Violation numbers are append-only. Each public enum comment defines the byte offset and both detail fields; tests/test_codes.c asserts that complete tuple.

Public symbols, public struct fields, and violation values are ABI. Pre-1.0 changes are permitted only when deliberate, documented, and covered by public API and amalgamation behavior tests.

The input buffer, report, arena object, and arena storage are distinct borrowed regions for the duration of a verification call. The library does not retain their addresses after it returns.

Arena proof

The verifier allocates one mvet_span_t per metadata key and tensor name. A span is two size_t words. Both arrays are multiples of the eight-byte arena alignment on supported targets, so at most the first non-empty carve needs padding. The exact bound is therefore:

sizeof(size_t) * 2 * (MVET_MAX_KV_COUNT + MVET_MAX_TENSORS)
+ (any index exists ? MVET_ARENA_ALIGN - 1 : 0)

The public MVET_GGUF_ARENA_WORST_BYTES macro expresses that formula. Tests exercise all possible base-address residues, prove exact-fit success, and prove that one byte less fails at the worst residue. Default 64-bit caps require 147,463 bytes. Defining MVET_MAX_TENSORS=2048u gives the documented 49,159 byte profile, below 64 KiB.

Any change to an arena allocation, cap, span representation, or alignment must update this formula and its exact-bound tests in the same change.

The safetensors verifier carves three arrays: one span per root key (tensor names plus one __metadata__ key), one span per metadata key, and one u64 start/end extent pair per tensor. Carve counts derive from the validated header length through per-entry byte minimums (the smallest spellable root, metadata, and tensor entries are 17, 5, and 50 bytes), so demand is proportional for small inputs while the worst case stays closed-form:

sizeof(size_t) * 2 * (MVET_MAX_ST_TENSORS + 1 + MVET_MAX_ST_METADATA_ENTRIES)
+ sizeof(uint64_t) * 2 * MVET_MAX_ST_TENSORS
+ (MVET_ARENA_ALIGN - 1)

MVET_ST_ARENA_WORST_BYTES expresses that formula: 278,551 bytes at 64-bit defaults, 57,367 under the documented 64 KiB profile (-DMVET_MAX_ST_TENSORS=1536u -DMVET_MAX_ST_METADATA_ENTRIES=512u). tests/test_st_arena.c proves the bound exact the same three ways.

Upstream GGML contract

GGUF has a de facto implementation contract in GGML. The dtype enum, quant block widths, and stored block sizes are audited against the exact llama.cpp commit in tools/ggml-pin.env. tools/check_ggml.c compiles against those upstream headers and compares all wire slots, including intentionally dead ones.

CI checks the pinned commit on every change. A scheduled workflow also checks the current upstream branch and fails visibly when a new slot or layout change requires review. Drift is never accepted by silently updating the pin: inspect the upstream change, update parser behavior and focused tests, then advance the commit deliberately.

safetensors has a canonical Rust implementation instead of GGML. The mirrored contract (frame checks, validate() tiling rules, dtype bit widths including the sub-byte types, and the whitespace policy) is derived from the exact commit in tools/st-pin.env. Deliberate strictness beyond canonical behavior (duplicate keys, escapes in keys, unknown tensor fields, the caps) is marked "policy" on its violation codes in the public header; everything else must track the pin, under the same deliberate-drift rule as GGML. A scheduled workflow diffs the audited tensor.rs against current upstream main and fails on any change, and the differential shim's Cargo rev is held equal to the pin by make check-st-pin, so the pin can only advance deliberately and in both places at once.

Verification matrix

Run the smallest relevant checks while editing and the complete matrix before handoff of parser, bounds, ABI, or dtype changes:

make clean && make test CC=gcc
make clean && make test CC=clang
make check CC=clang
make test-profile-64k CC=clang
make test-no-assert CC=clang
make clean && make test CC=clang \
  EXTRA_CFLAGS="-fsanitize=address,undefined -fno-sanitize-recover=all"
make fuzz && ./build/smoke_fuzz -runs=100000
make check-ggml GGML_DIR=/path/to/llama.cpp
git diff --check

CI additionally runs MemorySanitizer, a 32-bit build, a static AArch64 build under QEMU, the generated amalgamation behavior tests, and the Python binding contract (make check-python). Real-model burn-in is local-only (make test-real GGUF_DIR=/path/to/ggufs) and complements rather than replaces deterministic fixtures.

Hardening gates

  • CVE corpus. tests/corpus/ holds one file per advisory, generated by tools/make_corpus.c and described by tests/corpus/MANIFEST. make check-corpus requires each file to be rejected with its exact recorded violation code; rejection for the wrong reason is a failure, because it means the invariant that kills that advisory stopped working. make check-corpus-stable regenerates into a scratch directory and diffs, so a corpus file can never drift from the generator that documents its shape. Never point a fuzzer at tests/corpus/: libFuzzer writes new inputs into its first positional directory. Use a scratch corpus and pass the seed directory second.
  • Arena discipline. make check-arena-64k runs the whole corpus plus the GGUF and safetensors worst-case carve forcers through one fixed 64 KiB arena under the reduced-cap profile, asserting no exhaustion and a high-water mark inside the closed-form bound.
  • Bounded work. make check-work builds with MVET_WORK_PROFILE, which makes cursor.c, utf8.c, and span.c charge a counter for every step that scales with input, then asserts total work against a linear term plus the deterministic n log n sorting term, and separately asserts that doubling the tensor count does not more than triple the work. The counter is absent from every shipping build.
  • Fuzzing. Per-PR smoke in ci.yml; per-format targets (gguf_fuzz, st_fuzz) with a nightly long run seeded from the corpus in fuzz-nightly.yml; make afl builds the same targets under AFL++. tools/oss-fuzz-build.sh is the entry point for OSS-Fuzz registration.
  • Differential parity. make diff-gguf GGML_DIR=... GGML_LIB=... buckets inputs against a real upstream loader. Upstream runs in a forked child because it can abort on hostile input, so "they crash" is a recorded bucket. Results and triage live in docs/PARITY.md. For safetensors, make diff-st links the canonical Rust implementation at the exact audited commit through a C-ABI shim (tools/st_diff_shim/, rev held equal to tools/st-pin.env by check-st-pin); its exit code is the acceptance bar (never more permissive than canonical, no canonical panics), it runs nightly in CI, and its report is docs/PARITY-ST.md.
  • Amalgamation parity. make check-amalg links the entire default test sweep, including the CVE-corpus gate, against the amalgamated translation unit instead of the static library, so the vendorable pair can never behaviorally drift from the src/ build it was generated from.
  • CLI contract. make check-cli asserts the exit-code mapping, the JSON report shape (including hostile file-name escaping), format routing, and the whole CVE corpus with exact violation names through modelvet(1). tools/check_codes.sh also requires every violation code to appear in the CLI's name table, so output can never fall behind the enum.