gremlin.c

gremlin.c is a C99 protobuf implementation with the compiler, code generator, and wire runtime in this repository. It does not call protoc, does not link third-party libraries, and generated code writes to caller-owned buffers.

The project is still pre-1.0. APIs and generated header shapes may change; pin a commit if you depend on it.

What You Get

• gremlinc-gen: a CLI and CMake helper that turn .proto files into C headers.
• gremlin.h: a header-only protobuf wire runtime used by generated code.
• Lazy readers over caller-owned buffers. Strings, bytes, and nested messages are zero-copy views.
• Two-pass encoding: generated _size() computes the exact byte count, then generated _encode() fills a struct gremlin_writer.
• In-tree parser and descriptor resolver, so consumers need only a C99 compiler and CMake.

Supported generated-field families include scalar numeric fields, strings/bytes, enums, nested messages, repeated fields, packed repeated fields, maps, and unknown-field skipping.

Verification

Formal verification is a machine-checked proof about code behavior. Instead of running examples and hoping they cover the interesting cases, the C functions are annotated with ACSL contracts and Frama-C WP proves that the implementation satisfies those contracts for all inputs allowed by the preconditions.

This is useful for the protobuf wire runtime because the important bugs are low-level and easy to miss with tests: out-of-bounds reads or writes, offset arithmetic overflow, non-canonical varint bytes, incorrect fixed32/fixed64 layout, or malformed input that should return a defined error. Tests still exist, but the proof gives stronger coverage for these small shared primitives than any practical test corpus can.

The main proof target is verify-runtime. It runs Frama-C WP over runtime/include/gremlin.h through runtime/tests/verify.c, which references the static-inline functions so WP checks their bodies.

Current runtime proof: 719 / 719 WP obligations. The exact function set is RUNTIME_WP_FCTS in runtime/CMakeLists.txt: writer setup, varint/fixed size helpers, _encode_at writers, varint/fixed/bytes decoders, gremlin_skip_data, zigzag conversions, and float/double bit casts.

Run from the build directory:

cmake --build . --target verify-runtime

The repository also contains other proofs, such as descriptor arena allocation and selected code-generator helpers. Parser proofs are useful for the compiler itself, but they are not the proof surface generated protobuf code relies on at runtime.

Quick Start

include(FetchContent)
FetchContent_Declare(gremlin
    GIT_REPOSITORY https://github.com/norma-core/gremlin.c.git
    GIT_TAG        main)
FetchContent_MakeAvailable(gremlin)

gremlinc_generate(
    TARGET       my_protos
    IMPORTS_ROOT ${CMAKE_SOURCE_DIR}/protos
    PROTOS       foo.proto nested/bar.proto)

add_executable(my_app main.c)
target_link_libraries(my_app PRIVATE my_protos)

my_protos is an INTERFACE target that puts the generated headers and runtime include path on your executable. A complete consumer project is in example/.

From this repo:

mkdir build && cd build
cmake ..
make
ctest

Runtime API Shape

Generated messages use plain C structs and inline functions:

size_t need = example_Person_size(&person);
uint8_t *buf = malloc(need);

struct gremlin_writer w;
gremlin_writer_init(&w, buf, need);
example_Person_encode(&person, &w);

example_Person_reader r;
enum gremlin_error err = example_Person_reader_init(&r, buf, w.offset);

See example/main.c for a full encode/decode path.

Benchmarks

integration-test/benchmark.c is a C port of the gremlin.zig benchmark corpus. On the current development machine, the generated C path is about 2x faster than the Zig reference on the aggregate benchmark sum.

Reproduce locally:

cmake -S integration-test -B integration-test/build
cmake --build integration-test/build --target benchmark
./integration-test/build/benchmark 20000000

Benchmark builds use -O3 -DNDEBUG -march=native -flto, so results are machine- and compiler-dependent.

Repository Layout

parser/           protobuf syntax parser used by the compiler
descriptors/      descriptor pool and resolution pipeline
runtime/          verified header-only wire primitives
gremlinc/         C code generator library
gremlinc-gen/     CLI driver and gremlinc_generate() CMake helper
example/          standalone consumer example
integration-test/ generated-code tests and benchmark corpus

Related

This is a C99 port of gremlin.zig with the same encode/decode model and benchmark corpus.