ocaml-boundary

name

ocaml-boundary

description

The verified-library boundary — what OCaml is allowed to exist, the assume-val glue taxonomy, patch directories and their lifecycle, companion-file byte-layout rules, third-party vendoring policy, and the extraction targets (OCaml native, js_of_ocaml, wasm_of_ocaml, KaRaMeL C). Use when adding or reviewing any hand-written OCaml, when a patch in experimental_ocaml_glue or minimal_regrettable_glue is involved, when realising a new assume val, when writing a companion-file writer, or when someone proposes "just do it in OCaml for now". That proposal is how the project nearly lost its verification story once.

The OCaml boundary: what may exist outside F*

Iron Rule #11 in one line: inside the verified library boundary, OCaml is assume val realisations only — pure I/O, host-engine call-outs, vendored crypto. Everything that makes a semantic decision about RDF/SPARQL lives in F* and is extracted.

Why this is a hard rule (the disaster, briefly)

In April 2026, query-planning and access-method fast paths (the codenamed Yod6/Tet3/Lamed3/Mem5/Pe5/Bet7/Tav5/Heth3 patches) accreted as post-extraction OCaml. Each looked locally reasonable; cumulatively the verified core became dead code on the hot path, the "verified" claim collapsed, and every non-OCaml extraction target (KaRaMeL C, WASM-via-C, future Low*) became unreachable because the real logic no longer existed in F*. The recovery (docs/designissues/2026-05-07-query-planning-fstar-recovery.md, tracked in #200) rebuilt planning as F* modules and retired all eight violators. "Retirement is harder than accretion" — the cost of an OCaml shortcut is paid back with interest.

Named reflex to stop: "but this file is hand-written anyway, surely it's fine" — backend semantics, caching, timeout, and correctness decisions belong in F* even when they'd sit in a hand-written file.

The taxonomy (from the boundary audit)

Classify any OCaml you meet or write (docs/designissues/fstar-ocaml-boundary-audit.md):

Class	Meaning	Verdict
EXTRACTED	Generated by fstar.exe --codegen OCaml	never edit (anti-pattern #13; CI-enforced)
ASSUME-IO	Realises assume val for file/clock/socket I/O	acceptable
ASSUME-HOST	Host-engine call-out, e.g. regex (host-defined per SPARQL 1.1 — moving it into F* would be wrong)	acceptable
ASSUME-CRYPTO	Vendored/pure crypto primitive	acceptable; prefer HACL* long-term
CONSUMER	CLI, runners, HTTP entry points	fine, but lives in bin/<consumer>/, not ocaml-output/; not claimed verified
VIOLATION-SEM	Semantic logic in OCaml	migrate to F*. As of the 2026-07-06 audit, not zero: cottas_ondisk_runtime.sh, cottas_ondisk_z_lazy_open.sh, and ..._token_lookup_runtime.sh remain VIOLATION-SEM/MIXED. The production SPARQL query path no longer calls them (rewired to F* _tok on 2026-07-06), but three non-production consumers still do, so the patches can't be deleted yet (#118/#254).
MIXED	Both	split it

"Mirroring" a glue change into ocaml-output/ is not a loophole either (owner directive, 2026-07-04). When you edit a patch script in experimental_ocaml_glue/, the ONLY way the change reaches ocaml-output/ is re-running ./build-ocaml.sh extract — never by hand-applying the same edit to the patched .ml, even byte-for-byte identical. The extracted OCaml is ephemeral and derivative; you cannot impersonate the extractor+patch pipeline reliably, and CI diffs will catch you when you get it subtly wrong. With a warm .checked cache the re-extract costs minutes (see fast-verify-extract), so there is no time argument.

Companion-file writers are not a loophole. Byte layout belongs in F* (serialize : data -> Tot (list u8) plus parse and a roundtrip lemma); the OCaml side reduces to write_bytes/read_bytes. Every companion artifact gets a hash round-trip CI witness (unit test hashing F*-computed bytes against on-disk bytes) — pattern in docs/designissues/2026-05-07-io-verification-and-third-party.md.

The directories

• formal/fstar/ocaml-output/ — extracted .ml plus exactly two allowlisted hand-written modules: fstar_pure_hashes.ml (pure-OCaml MD5/SHA family realising the SPARQL11.Algebra hash assume-vals; pure so the same code runs on native, js_of_ocaml, AND wasm — the C-backed Digest/Digestif route crashed under wasm; must be linked before SPARQL11_Algebra.ml) and sparql_parser_stubs.ml (UTF-8 codepoint encoding + IRI escape realisations). Anything else hand-written here fails check-ocaml-output-cleanliness.yml.
• formal/fstar/minimal_regrettable_glue_code_each_with_an_open_issue/ — sanctioned build-time patches, one per assume val gap, named <issue>_<description>.sh. Currently 8; each maps to an open issue (Iron Rule #3).
• formal/fstar/experimental_ocaml_glue/ — runtime glue for the HDT/COTTAS/Parquet backends (18 scripts). This is the watchlist: additions here are restricted to the rule-#11 acceptable forms, and subagent prompts touching the backends must say so explicitly (subagent-prompting skill).
• bin/<consumer>/ — hand-written consumer sources (factoidal-cli, w3c-runner, factoidal-http, …). Outside the verified boundary by construction.

Patch lifecycle

ocaml-patches.sh applies the minimal dir (issue-number order) then the experimental dir; each patch is idempotent, keyed on grep markers.

• ./build-ocaml.sh extract runs the patches; compile does NOT (anti-pattern #11). After a fresh extraction without patches, every assume val silently regresses to failwith "Not yet implemented".
• Retirement is the goal state: implement the logic in F*, delete the patch, close the issue (many have retired this way: #53, #64, #65, #66, #67, #68, #95). When a patch dies, prune it from the glue dir's README table too — stale rows there have misled sessions before.
• Never sneak semantic logic into ocaml-patches.sh or a runner (anti-pattern #15). The glue-audit verdict taxonomy (ASSUME-OK / ASSUME-OK-PROVISIONAL / VIOLATION / NEEDS-AUDIT) is in docs/designissues/2026-05-08-glue-patches-audit.md.

CI enforcement

Workflow	Guards
check-derived-files.yml	blocks hand-edits to extracted .ml without a matching .fst/patch change
check-fstar-purity.yml	detects net-new semantic logic in the glue dirs + the two S-class consumer files
check-ocaml-output-cleanliness.yml	forbids non-allowlisted hand-written .ml in ocaml-output/
check-extraction.yml	extraction stays reproducible

Third-party and host-primitive policy

From 2026-05-07-io-verification-and-third-party.md:

• SHA-256 and friends: HACL* (opam dep now; vendored .fst if compliance demands). Until then, fstar_pure_hashes.ml.
• Verified binary parsers: EverParse when a format warrants it.
• UUID: RFC 4122 byte assembly in F* + assume val random_bytes.
• Randomness: two separate assume-vals (_csprng vs _weak) so a weak source can't silently serve a security context.
• Regex: stays assume val regex_match permanently (host-defined).
• Vendoring under formal/third_party/ (designated future home; create it with the first vendored dep): each dep in its own subdir with VERSION (commit pin) + LICENSE; never edit vendored code — record deviations in LOCAL_PATCHES.md.

Extraction targets (status and lessons)

Target	Status	Notes
OCaml native	production	build-ocaml.sh all/extract/compile; binaries committed per Iron Rule #9
js_of_ocaml	works	build-ocaml.sh js → docs/fstar-extracted/factoidal.js; powers the browser demos; debug variant via jsoo-debug-bundle
wasm_of_ocaml	works	build-ocaml.sh wasm; vendored zarith wasm runtime + wasm_stub_shims.py; the historical functions-suite hash crashes are why the pure-OCaml hash module exists
KaRaMeL C	pilot	--codegen krml clean on 5 pure modules; krml → .c blocked on karamel install (needs ocaml<4.13 switch, prebuilt binary, or newer wasm pin) — 2026-05-07-c-build-and-roaring-plan.md

The strategic point: every line of semantic OCaml narrows this table to one row. Keeping logic in F* is what keeps C, WASM-via-C, and Low* reachable. Established pipelines are F*→OCaml and F*→Low*→KaRaMeL→C; there is no good F*→Rust path, and asking a code assistant for one historically produced a hand-written Rust implementation (the pre-pivot mistake this repo deleted; see Iron Rules #1–#2).

What this skill does NOT cover

• F* module style and where definitions belong — fstar-module-style.
• Build mechanics — build-and-test.
• Prompting subagents with the boundary rules — subagent-prompting.