Module Wire_3dSource

everparse_name name returns the C identifier EverParse derives from a struct name: underscores are stripped and the _-separated segments are joined in CamelCase. Each segment is capitalized and any internal run of two or more consecutive uppercase letters collapses to a single one. E.g. Grpc_message becomes GrpcMessage, EP_Header becomes EpHeader, CLCW becomes Clcw, and TMFrame becomes Tmframe.

pascal_case s is EverParse's own identifier mangling, transcribed from pascal_case in EverParse's src/3d/Target.fst. It drops underscores and CamelCases, lowercasing every character that follows an uppercase letter or a digit until the next lower-case one. EverParse names a validator wrapper pascal_case (module ^ "_check_" ^ codec), so use this (not everparse_name) to predict a wrapper symbol exactly: e.g. pascal_case "tpm_check_TPM2B" is "TpmCheckTpm2b" and pascal_case "virtio_check_Virtq_desc" is "VirtioCheckVirtqDesc".

generate_3d ~outdir schemas generates .3d files from Wire modules.

generate_dune ~outdir ~package schemas writes dune.inc listing the build, runtest, and install rules for the generated C artifacts.

run_everparse ?quiet ~outdir schemas invokes EverParse on .3d files in outdir.

If quiet is true (the default), EverParse output is suppressed. If quiet is false, EverParse stdout/stderr are left visible.

Requires 3d.exe in PATH.

parse_3d ~outdir file runs 3d.exe on a single .3d file in outdir. Returns Ok () when 3D accepts the file, or Error stderr with the captured error message otherwise.

With ~batch:false (the default) it stops after the 3D type-checker, before F* and KaRaMeL: fast, but it does not catch kind errors that only fail F* verification (e.g. a list over a possibly-empty element). With ~batch:true it runs the full --batch verification (F* and C extraction), catching those, and discarding the generated C. Unlike run_everparse it does no endianness-header copy, so it works on a bare output directory. Intended for projection coverage tests.

Requires 3d.exe in PATH.

fork_pool ~max_jobs jobs runs each job in its own process, at most max_jobs at a time, returning each job's success (exit 0 with no exception) in input order. Used to overlap the per-module EverParse runs, whose cost is dominated by F* verification. Each job that invokes 3d.exe must use a private working directory, as concurrent runs race on EverParse's shared intermediate files.

rm_rf dir removes dir and its files (a flat output directory), ignoring errors. A cleanup helper for the private per-run directories used with fork_pool.

batch_check ~outdir schemas verifies every schema through EverParse (one .3d module each, accepted iff F* verifies it), the way EverParse's own corpus is tested. The cost is dominated by per-module F* verification (CPU-bound, several seconds each) with negligible startup, so the schemas are verified concurrently in a fork_pool (at most max_jobs at once, default a small multiple of the cores) rather than serially in one 3d.exe --batch. Each run uses a private directory. Returns Ok () iff EverParse accepts every schema, else Error naming the offending schema(s) with their captured diagnostics. Schemas must have distinct names (one .3d module each). Requires 3d.exe in PATH.

write_external_typedefs ~outdir schemas writes the default <Name>_ExternalTypedefs.h for each schema that uses the WireCtx contract, declaring WIRECTX as a forward reference to the matching <Name>Fields plug struct.

write_fields ~outdir schemas writes the default <Name>_Fields.{c,h} plug for each schema that uses the WireCtx contract: a typed struct (one member per named field) and the <Name>Set* switch dispatchers that populate it.

generate_c ?quiet ~outdir schemas invokes EverParse on existing .3d files to produce C parsers and generates test.c.

The EverParse-emitted <Name>Check<Codec> wrapper is hardened after generation: it returns FALSE unless the validator consumed the whole buffer, so a valid record followed by trailing bytes is rejected. The raw <Name>Validate<Codec> function keeps EverParse's prefix semantics and returns the consumed position.

If quiet is true (the default), EverParse output is suppressed. If quiet is false, EverParse stdout/stderr are left visible.

Requires 3d.exe (EverParse) in PATH.

run ?quiet ~outdir schemas runs the full pipeline: writes .3d files, invokes EverParse, and produces C validators. The quiet flag is passed through to EverParse execution.

A codec with its type erased, so codecs of different record types share one list. Build with pack. main and the standalone helpers take these rather than an already-projected Wire.Everparse.t, so the `Ffi-vs- `Standalone projection mode is chosen by main, not at the call site.

pack codec erases codec's type for a packed list.

generate_standalone ?quiet ?name ~outdir ~package codecs runs the documentation pipeline: project each codec with Wire.Everparse.doc, merge them into one <Name>.3d, and (when 3d.exe is available) compile it to a single validator-only <Name>.c (no _Fields plug, no FFI). The file base is name when given, else package, normalised to a CamelCase identifier ("my-pkg" becomes MyPkg); package always names the opam package. The generated <Name>Check<Codec> wrappers validate the whole buffer, rejecting trailing bytes (see generate_c). Only the checked wrapper header <Name>Wrapper.h is installed as the public C API; the raw <Name>Validate* entrypoints (which take an unguarded StartPosition) stay build-internal, linked into the archive but not shipped as a header.

generate_dune_standalone ?name ~outdir ~package codecs writes a dune.inc for the single-file documentation build: rules that emit <Name>.3d and compile it to <Name>.c, a rule that builds the validator into an installed lib<name>.a archive, a runtest rule that runs the differential self-check (see generate_corpus / generate_agree), and an install stanza (under opam package) for the spec, parser, and archive. name defaults to package; see generate_standalone.

The c/ archive builds and installs in every dune context through that context's own toolchain (%{ocaml-config:c_compiler}, the ocaml-config partial linker, and the binutils that compiler resolves), so a cross build produces and installs a target-native archive rather than the host's. Only the host-side steps are gated on (= %{context_name} default): regenerating the committed .3d/C from 3d.exe, and the agree differential test, which runs a built validator on the build machine.

wrapper_symbols base codecs is the <Base>Check<Codec> wrapper C symbol for each codec, computed exactly as EverParse names them. These are the only symbols a standalone archive exports; the raw <Base>Validate* validators are localized (see archive_link_steps).

archive_link_steps ~macos ~pack_linker ~objcopy ~ar ~archive ~base ~wrappers is the post-compile shell commands that fold <base>.o and <base>Wrapper.o into archive exporting only wrappers and localizing the raw validators. Platform specific (macos localizes during the partial link with pack_linker, elsewhere objcopy does it after). The tool commands are parameters so the emitted dune rule can pass the build context's toolchain (cross tools in a cross context) while the symbol-hiding test passes the host's; both share this one definition of the localize logic.

generate_corpus ?count ppf codecs prints, for each codec, count fuzzed inputs as <codec> <hex> <verdict> lines, where verdict is 1 when the OCaml codec accepts the bytes (decodes, validates, and the record spans the whole input -- matching the hardened Check wrapper's whole-buffer contract) and 0 otherwise, and <hex> is - for the empty input. Lengths are biased around each codec's minimum size so the corpus straddles the accept/reject boundary. This is the oracle half of the doc pipeline's differential self-check; main's corpus subcommand calls it on stdout.

generate_agree ?name ~outdir ~package codecs writes agree.c into outdir: a C program that replays a generate_corpus corpus through the EverParse-generated validators and exits nonzero on any input where the validator's accept/reject decision differs from the recorded verdict. It reads the <Name>Check<Codec> helper names from the generated <Name>Wrapper.h, so generate_c_standalone (or 3d.exe) must have run first.

main ?name ~mode ~package codecs dispatches based on Sys.argv:

• 3d writes the .3d file(s)
• c produces the C parser(s)
• dune generates dune.inc with build rules, test, and install stanzas
• otherwise runs the full pipeline.

mode is mandatory, so every gen.ml states what it emits. With ~mode:`Ffi it projects each codec with Wire.Everparse.project in `Ffi mode and drives the multi-file FFI pipeline, one set per codec. With ~mode:`Standalone it projects in `Standalone mode and drives the single-file pipeline, one <Name>.3d and <Name>.c standalone parser for the whole family. The codecs are the same either way; only the mode changes.

name overrides the standalone file base (see generate_standalone); it has no effect in `Ffi mode, whose file names come from the individual codecs.

has_3d_exe () returns true if 3d.exe is available in PATH or ~/.local/everparse/bin/.

ensure_dir path creates the directory path if it does not exist.

The strict-C11 cc flags the generated dune rule compiles the EverParse C with (and the e2e test mirrors), so the generated validators are checked under the same standard a downstream caller would use.

everparse_type_defines are the preprocessor -D flags mapping each 3D integer type (UINT16BE, ...) to its host-order C type, needed to compile the wrapper of a parameterized validator (whose parameters EverParse types with the 3D names). Harmless for non-parameterized wrappers.