owenthcarey · Oct 6, 2026 · Oct 5, 2026 · Oct 6, 2026 · Oct 6, 2026 · Oct 6, 2026
diff --git a/.clang-tidy b/.clang-tidy
@@ -11,6 +11,7 @@ Checks: >
   cert-*,
   -cert-err58-cpp,
   clang-analyzer-*,
+  -clang-analyzer-security.ArrayBound,
   cppcoreguidelines-*,
   -cppcoreguidelines-avoid-magic-numbers,
   -cppcoreguidelines-non-private-member-variables-in-classes,
@@ -55,6 +56,10 @@ Checks: >
 #   llvm-use-ranges: lib/Core must not depend on LLVM ADT.
 #   *-macro-to-enum: configuration macros live in generated headers.
 #   readability-trailing-comma: conflicts with clang-format's bin-packing.
+#   clang-analyzer-security.ArrayBound: reports every operand access of an
+#     LLVM instruction the analyzed function creates as an access before its
+#     region (LLVM keeps a User's operands in front of the object), in the
+#     LLVM headers, where no NOLINT in our code reaches (the guard passes).
 
 WarningsAsErrors: '*'
 HeaderFilterRegex: '(include|lib|tools|unittests)/.*'

diff --git a/AGENTS.md b/AGENTS.md
@@ -40,7 +40,11 @@ witness rule for definite errors, raw pointers only from `WEAVEC_RAW`, the
 library table's portability rule, guards on the accessed address, the link
 modes (`-fweavec-link=records|analyze|none`), the per-unit budget and unit
 record format 31; its *Implementation amendments* override its body too.
-There is no checked mode.
+Then `0034-fast-enforcement.md`: guards as declared calls the LLVM passes
+lower to inline shadow-memory checks, registration only where a guard can
+reach, definite errors confirmed by a replay, and the work budget; its
+*Implementation amendments* (the shadow encoding as built, among others)
+override its body. There is no checked mode.
 
 ## Before touching the model or the checker
 
@@ -123,7 +127,7 @@ cmake --preset dev && cmake --build --preset dev && ctest --preset dev
 | Change pointer kinds / how annotations become kinds | `lib/Core/PointerKind.cpp`, `lib/Analysis/AttributeReader.cpp`, `lib/Analysis/KindInference*.cpp`; what the engine takes from them: `lib/Analysis/EngineKinds.cpp` |
 | Change which checks are inserted     | `lib/Analysis/CheckPlanner.cpp` (plan), `lib/Frontend/CheckEmitter.cpp` and `Prelude.cpp` (emission) |
 | Change which facets get a guard      | `CheckPlanner::planGuards` in `lib/Analysis/CheckPlanner.cpp` (RFC 0032 §6); the need of a call argument's guard: `objectWitness` in `lib/Analysis/EngineLibrary.cpp`; possible findings dropped on guarded facets: `LedgerAdapter::dropGuardedPossible` |
-| Change the guard helpers / range caches | `lib/Frontend/Prelude.cpp` (`GuardHelpers`, `RuntimeHelpers`, `RuntimeDeclarations`), `lib/Frontend/CheckEmitter.cpp` (`planCache`, `declareCaches`, `isQuietLoop`); oracle tests `test/Emission/runtime-oracle-*.c` |
+| Change the guards' lowering / shadow checks | `lib/Frontend/GuardPasses.cpp` (`GuardCanonicalize`, `GuardMerge`, `GuardExpand`, `GlobalPadding`; RFC 0034 §1), the shadow encoding in `runtime/weavec_rt.h`, the prelude's declarations and stack helpers in `lib/Frontend/Prelude.cpp`; tests `test/Emission/guard-passes-*.c`, `runtime-oracle-*.c` |
 | Change stack / global object registration | `lib/Frontend/ObjectRegistration.cpp` (`planObjects`), `CheckEmitter::registerObjects` |
 | Change the runtime (allocator, object table, guards, reports) | `runtime/weavec_alloc.c`, `weavec_malloc.c`, `weavec_objects.c`, `weavec_report.c`, `weavec_rt.h` (the prelude declares the same entry points); its C test `runtime/test/rt_test.c` (CTest `runtime`); cases in `test/cases/semantics/runtime/` |
 | Change the runtime's link line and fallbacks | `lib/Frontend/Driver.cpp` (`addRuntimeLibraries`, `runtimeObstacle`, `allocatorDefinedBy`, `dropAllocatorIfDefined`); `test/Driver/runtime-*.c` |

diff --git a/README.md b/README.md
@@ -130,7 +130,7 @@ weavec-cc -c main.c -o main.o
 weavec-cc node.o main.o -o prog        # checks the records against each other, then links
 ```
 
-A bug inside one file is reported when that file is compiled. By default the link step only reads the records: it checks declarations against definitions and the requirements of each exported function at the calls other files make, and analyses no file again. A bug that needs two files, such as a use after free whose `free` is in another file, is caught by its guard at run time; to report it at build time, link with `-fweavec-link=analyze` (which analyses the units again, within a time budget) or run `weavec --whole-program`. Link inputs without a WeaveC record (archives, shared libraries, objects from another compiler) are named in one `unanalyzed-input` warning.
+A bug inside one file is reported when that file is compiled. By default the link step only reads the records: it checks declarations against definitions and the requirements of each exported function at the calls other files make, and analyses no file again. A bug that needs two files, such as a use after free whose `free` is in another file, is caught by its guard at run time; to report it at build time, link with `-fweavec-link=analyze` (which analyses the units again, within a time budget) or run `weavec --whole-program`. Link inputs without a WeaveC record (archives, shared libraries, objects from another compiler) are named in one `unanalyzed-input` warning; an archive whose objects `weavec-cc` built is named in a note instead.
 
 ### Checks
 
@@ -210,7 +210,7 @@ For a translation unit compiled by `weavec-cc` in an enforcing mode (the default
 - **(N) Null.** If its null facet is proven or checked, it does not dereference null, or the program traps first.
 - **(T) Temporal.** If its temporal facet is proven, the object is still alive, and a release releases a live allocation once.
 - **(G) Guards.** If a facet is guarded (the default; not with `-fno-weavec-runtime`) and the bytes it accesses start inside an object the runtime tracks (a heap block from the runtime's allocator, a local whose address escapes, a global), the object is live and the access stays inside it, or the program traps first. A guarded release is of null or the start of a live heap block, or the program traps.
-- **(V) Violations.** A definite violation never reaches the object unguarded: it fails the build, or, if lowered with `-Wno-error`, the site is guarded or checked, and traps unconditionally only where it can be neither.
+- **(V) Violations.** A definite violation, confirmed on a feasible path, fails the build; an unconfirmed one is a warning. If lowered with `-Wno-error`, its site is guarded or checked as a possible finding, so it traps only if it happens; nothing traps unconditionally.
 
 These hold under six assumptions:
 
@@ -230,22 +230,22 @@ If a memory-safety violation happens anyway, then a check trapped first, or the
 (G) is weaker than (S) and (T), which is why the ledger counts guarded facets separately from checked ones:
 
 - **Provenance is the address accessed.** A guard asks which object the bytes an access touches lie in *now*, at a subscript `p[i]` as at a dereference, so arithmetic that carries a pointer out of one tracked object and into another live one passes. (This is what lets a base formed outside a buffer, such as `base = src - start`, index back into it.) Two cases still trap: an index or field offset that reaches forwards from inside a live local or global into another one, since those lie next to each other with no gap, and an index or offset from a pointer into a live object that lands in memory nothing tracks. Between heap blocks there is always a byte that belongs to none, so a walk off a heap block traps at its first step.
-- **Freed memory is recycled.** A freed heap block is caught only while it is in the quarantine (64 MiB by default); once its storage is reused, the guard sees the new object.
+- **Freed memory is recycled.** A freed heap block is caught only while it is in the quarantine (16 MiB by default); once its storage is reused, the guard sees the new object.
 - **Untracked memory passes.** String literals, `alloca` blocks, and memory from other allocators or from code built without the runtime are not tracked; a guard passes on them unless an index carried the pointer there from a live tracked object.
 
 The full statement, including what is and is not caught, is in [the guarantees reference](docs/pages/reference/guarantees.md), [RFC 0030, *Soundness*](docs/rfcs/0030-prove-or-trap.md#soundness), [RFC 0032, *Soundness*](docs/rfcs/0032-runtime-enforcement.md#soundness) and [RFC 0033, *Soundness*](docs/rfcs/0033-drop-in-by-default.md#soundness).
 
 ## Performance
 
-Guards run on every execution of the operations they cover, and the runtime's allocator replaces the system's. Measured on the corpus benchmarks as user CPU time and peak memory, relative to the same program built by the reference Clang ([RFC 0032](docs/rfcs/0032-runtime-enforcement.md#implementation-amendments), amendment 3):
+Guards run on every execution of the operations they cover, and the runtime's allocator replaces the system's. A guard is an inline check of the runtime's shadow memory (one byte per 16 bytes) that the compiler merges and hoists like a load; only what the shadow cannot decide calls the runtime. Measured as user CPU time and peak memory, relative to the same program built by the reference Clang ([RFC 0034](docs/rfcs/0034-fast-enforcement.md#implementation-amendments), amendment 16):
 
 | Benchmark | Default (runtime) | `-fno-weavec-runtime` | Peak memory (default) |
 | --- | ---: | ---: | ---: |
-| cJSON parse/print | 1.66× | 1.14× | 0.59× |
-| zlib minigzip | 1.85× | 1.00× | 1.09× |
-| Lua bench | 5.94× | 1.11× | 1.61× |
+| cJSON parse/print | 1.59× | 1.15× | 0.37× |
+| zlib minigzip | 1.62× | 1.00× | 1.26× |
+| Lua bench | 2.43× | 1.09× | 1.54× |
 
-Interpreters and tight loops over pointers pay the most: Lua's dispatch loop executes roughly one guard for every two instructions of the unguarded program. Code that cannot afford this can build with `-fno-weavec-runtime`; facets that would have been guarded are then `unresolved` and not enforced, and a use of a freed object is not caught at run time.
+On ten more projects nobody tuned WeaveC on (QuickJS, LMDB, Janet, brotli, xz, libdeflate, zlib-ng, curl, cmark, libgit2), the default build runs their workloads at 1.5 to 4.0 times the reference compiler's CPU time, 2.55 on average (geometric mean), and every one of them builds and passes its own test suite. Interpreters and tight loops over pointers pay the most. Code that cannot afford this can build with `-fno-weavec-runtime`; facets that would have been guarded are then `unresolved` and not enforced, and a use of a freed object is not caught at run time.
 
 ## Building