| 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.
