feat!: enforce unresolved facets at run time with an object table

[owenthcarey]

Summary

Implements RFC 0032, Runtime enforcement. Every enforcing weavec-cc build now links a small runtime: an allocator that keeps each heap block's exact extent and liveness findable from a pointer (with a quarantine for freed blocks), plus tables of escaping stack locals and globals. A spatial or temporal facet that the analysis leaves unresolved, and that has a pointer operand, becomes a sixth outcome, guarded. An inserted guard asks the object table and traps on an access outside the object, on a use of a released object, and on an invalid release. Temporal bugs are caught at run time for the first time.

On the corpus, unresolved shares fall to 5.6% spatial / 14.3% temporal for the original projects and 9.5% / 18.7% for the held-out ones (gate R4: at most 12% / 20%). Before this change they were roughly 36–42% spatial and 35–37% temporal. All 39 corpus injections are detected.

Design notes

• Runtime (runtime/). libweavec_rt.a holds the size-class arena with slot metadata words, the quarantine, huge blocks, the Darwin malloc zone, the stack and global tables, the guards and reports. libweavec_alloc.a defines malloc, calloc, realloc and free for the image, with weak definitions for the other allocation entry points. runtime/test/rt_test.c runs as the runtime CTest.
• Core. The guarded outcome ranks between checked and unresolved. There are three new check templates (object, live, release) and a new require level, guarded. Ledger JSON is now schema version 2 and unit records are format 30.
• Analysis and frontend. CheckPlanner::planGuards turns unresolved facets into guards after the engine has published. The prelude's guard helpers look up arena pointers inline, with per-function range caches and "quiet" loops that skip state reads. Escaping locals and globals are registered. The driver adds the runtime to the link line, and falls back with a note under sanitizers, -nostdlib, a program that defines its own allocator, or a link without the runtime.
• New flags: -fweavec-runtime, -fno-weavec-runtime, -fno-weavec-stack-objects, -fno-weavec-global-objects, -Wweavec-possible, -fweavec-require=guarded, and --no-runtime for the weavec tool. New environment variables: WEAVEC_RT_QUARANTINE, WEAVEC_RT_STATS, WEAVEC_RT_REPORT_LOG.
• Fixes found on the way:
  • A false proof through array-element cells (the place class at a boundary).
  • A false proof through __attribute__((cleanup)) functions, which the engine did not see. Their call at scope exit is now an unknown callee handed the variable.
  • RFC 0030's span check for *(p - k), which checked p instead of the accessed address.
• The RFC's Implementation amendments (1–22) record every departure from the text, the review findings and the gate results.

Cost, gate R6, amended. These are the default mode's user CPU over the reference compiler:

Benchmark	Default	-fno-weavec-runtime	Peak memory
cJSON	1.66×	1.14×	0.59×
zlib	1.85×	1.00×	1.09×
Lua	5.94×	1.11×	1.61×

The RFC's original bounds for zlib (1.5×) and Lua (2.0×) are not met. The Lua benchmark executes about 4.5 × 10⁹ guards at roughly 3 cycles each, so closing the gap needs guards removed at compile time; that is carried forward to a follow-up RFC. The manifest's G14 limits are set to what was measured (amendment 3).

Other limits raised to measured values (amendments 3, 12 and 20):

• Lua's no-runtime bound: 1.10 → 1.15.
• G15's zlib build-step limit: 5.4 s → 6.6 s.
• The hygiene gate's library line budget: 66,500 → 69,000.
• A new 4,000-line budget for the runtime.

Known limits, documented in the guarantees reference:

• A use-after-free through a typed callback parameter is not caught: the callee's access is proven under A1, so it gets no guard.
• Globals do not trap on an under-run from their start, or on a one-element walk off their end.
• A pointer-to-array type that is larger than its block is checked against the type's bound only.
• A bit-field's guard is narrower than the storage unit Clang accesses.

Breaking changes:

• Ledger schema 2 and unit record format 30.
• The summary line prints a guarded count.
• Default builds replace the image's allocator; -fno-weavec-runtime restores the previous behaviour, with guardable facets left unresolved.

Test plan

• Unit tests added or updated for the guarded outcome, its rank and messages, the planner's guard table, ledger version 2 and the record round trip.
• Integration tests:
  • test/Driver/runtime-{link,flags}.c pin the link line, the fallbacks, the notes, the ledger fields and the require levels.
  • Six test/Emission/runtime-oracle-*.c rewrite oracles cover the guards, range caches, and stack and global registration.
  • 43 cases in test/cases/semantics/runtime/, plus the alias probes, the span-difference cases, and TRAP markers on 16 soundness probes.
• On macOS arm64, ctest --preset dev passes 705 of 705, and scripts/run-cases.py passes 532 of 532 in trap, --asan and --checks verify modes.
• On Linux arm64 (Ubuntu 24.04, LLVM 23, in a container), the ci-release preset passes 703 of 705. The two failures come from the container itself (no cc installed; tests run as root). runtime/test also passes on Linux x86-64 under emulation. Linux x86-64 as a whole is CI's to confirm.
• Corpus: scripts/corpus-gate.py --full passes G9–G13, rfc0032.R4, RFC 0031's G5, G6 and G12, and G14/G15 with their amended limits. Every config builds and passes its tests with no trap, except two known cases: sqlite stops at its three triaged-true errors, as before; jansson has four triaged-true guard failures. With --checks verify the corpus has no weavec.proven trap.
• expected.json is re-recorded from that run.
• scripts/check-hygiene.py, scripts/check-format.sh, and npm test / npm run build in docs/ pass.

Checklist

• Code is formatted (scripts/format.sh). clang-tidy was not run locally; the ci-tidy job will check it.
• Public headers and behaviour changes are documented: README, the docs site, docs/architecture.md, docs/development.md, AGENTS.md, and the test and corpus READMEs.
• Conventional Commit PR title. User-visible changes are documented; the changelog is generated.
• No Clang/LLVM dependencies introduced into lib/Core.