feat!: prove or trap every memory-safety operation

.github/workflows/ci.yml

@@ -77,6 +77,9 @@ jobs:
           - name: Linux / Clang / Debug + ASan/UBSan
             os: ubuntu-24.04
             preset: ci-debug
+            # RFC 0030 (gate H1): the test/cases suites build, diagnose and
+            # write ledgers under ASan, without running the case programs.
+            configure-args: -DWEAVEC_CASES_ARGS=--no-run
           - name: Linux / Clang / Release
             os: ubuntu-24.04
             preset: ci-release
@@ -125,41 +128,55 @@ jobs:
           max-size: ${{ env.CCACHE_MAXSIZE }}
 
       - name: Configure
-        run: cmake --preset "${{ matrix.preset }}"
+        run: cmake --preset "${{ matrix.preset }}" ${{ matrix.configure-args }}
 
       - name: Build
         run: cmake --build --preset "${{ matrix.preset }}"
 
+      # Unit, lit and the test/cases suites (one cases-<suite> test per
+      # directory of test/cases, RFC 0030 section 17.4), in parallel.
       - name: Test
         env:
           ASAN_OPTIONS: detect_leaks=0:strict_string_checks=1
           UBSAN_OPTIONS: print_stacktrace=1:halt_on_error=1
-        run: ctest --preset "${{ matrix.preset }}"
+        run: ctest --preset "${{ matrix.preset }}" -j "$(getconf _NPROCESSORS_ONLN)"
 
       - name: Documentation examples
-        run: python3 docs/scripts/check-examples.py --weavec "build/${{ matrix.preset }}/bin/weavec"
+        env:
+          ASAN_OPTIONS: detect_leaks=0
+        run: |
+          python3 docs/scripts/check-examples.py \
+            --weavec "build/${{ matrix.preset }}/bin/weavec" \
+            --weavec-cc "build/${{ matrix.preset }}/bin/weavec-cc"
 
-      # ctest already ran the recall set; run it once more here so the
-      # per-CWE table is in the log (RFC 0011, *Recall check*).
-      - name: Recall
-        run: python3 scripts/recall.py --weavec "build/${{ matrix.preset }}/bin/weavec"
+      # RFC 0030 gate H2: no checked-mode residue, no library names compared
+      # outside the LibrarySpec table, no corpus project names in lib/, the
+      # engine seam, and the Dataflow and library line budgets.
+      - name: Repository hygiene
+        if: runner.os == 'Linux' && matrix.preset == 'ci-release'
+        run: |
+          python3 scripts/test_check_hygiene.py
+          python3 scripts/check-hygiene.py
 
-      # RFC 0014: fixed source revisions exercise real callback-heavy code.
-      # Counts are retained for review; parse errors, crashes, timeouts and
-      # nonconvergence fail the gate on both release platforms.
+      # RFC 0030 (section 17.5): per-file compiles and whole-program analyses of
+      # the pinned corpus configurations in test/corpus/, checked against the
+      # ratchet in test/corpus/expected.json and the triage in
+      # test/corpus/triage.json. The weekly Corpus workflow runs --full.
       - name: Pinned corpus
         if: matrix.preset == 'ci-release'
         run: |
-          python3 scripts/corpus.py --weavec "build/${{ matrix.preset }}/bin/weavec" \
-            --manifest scripts/corpus/rfc0014.json --timeout 120 \
-            --measure-memory --json corpus-rfc0014.json
+          python3 scripts/corpus-gate.py --quick \
+            --weavec "build/${{ matrix.preset }}/bin/weavec" \
+            --weavec-cc "build/${{ matrix.preset }}/bin/weavec-cc" \
+            --only log.c --only cJSON-program --only linenoise-program \
+            --only jansson --json corpus-gate-quick.json
 
       - name: Upload pinned corpus results
         if: always() && matrix.preset == 'ci-release'
         uses: actions/upload-artifact@v7
         with:
-          name: corpus-rfc0014-${{ matrix.os }}
-          path: corpus-rfc0014.json
+          name: corpus-gate-quick-${{ matrix.os }}
+          path: corpus-gate-quick.json
           if-no-files-found: ignore
 
       - name: Smoke-test install
@@ -181,6 +198,7 @@ jobs:
           path: |
             build/${{ matrix.preset }}/Testing/Temporary/LastTest.log
             build/${{ matrix.preset }}/test/**/Output/**
+            build/${{ matrix.preset }}/test/cases/cases-*.json
           if-no-files-found: ignore
 
   # ---------------------------------------------------------------------------

.github/workflows/corpus.yml

@@ -1,8 +1,10 @@
 name: Corpus
 
-# Runs weavec over the real-world projects in scripts/corpus/projects.json
-# and compares diagnostic counts with scripts/corpus/baseline.json. Not part of
-# the PR gate: the projects track branches and can change under us.
+# Runs the full corpus gate (RFC 0030, section 17.5) over the projects pinned
+# by SHA in test/corpus/manifest.json: per-file compiles, whole-program
+# analyses, project builds, test suites, injections and benchmarks, checked
+# against test/corpus/expected.json and test/corpus/triage.json. The gate
+# clones the projects into build/corpus. Pull requests run --quick in CI.
 on:
   schedule:
     - cron: "17 6 * * 1"
@@ -18,7 +20,9 @@ jobs:
   corpus:
     name: Corpus regression
     runs-on: ubuntu-24.04
-    timeout-minutes: 45
+    # --full builds and tests every project, applies each injection and runs
+    # the benchmarks, so it needs more time than the analysis-only run did.
+    timeout-minutes: 120
     steps:
       - uses: actions/checkout@v7
 
@@ -49,15 +53,17 @@ jobs:
           cmake --preset ci-release -DWEAVEC_BUILD_TESTS=OFF
           cmake --build --preset ci-release
 
-      - name: Run corpus
+      - name: Run corpus gate
         run: |
-          scripts/corpus.py --weavec build/ci-release/bin/weavec \
-            --json corpus-results.json \
-            --baseline scripts/corpus/baseline.json
+          python3 scripts/corpus-gate.py --full \
+            --weavec build/ci-release/bin/weavec \
+            --weavec-cc build/ci-release/bin/weavec-cc \
+            --json corpus-gate-full.json
 
       - name: Upload results
         if: always()
         uses: actions/upload-artifact@v7
         with:
-          name: corpus-results
-          path: corpus-results.json
+          name: corpus-gate-full
+          path: corpus-gate-full.json
+          if-no-files-found: ignore

AGENTS.md

@@ -5,28 +5,40 @@ most and where to find the rest.
 
 ## Project in one paragraph
 
-WeaveC is a Clang/LLVM-based tool that adds inferred ownership and borrowing
-checks to C. Three C++ libraries: `weavec::Core` (the ownership model, **no
-Clang/LLVM includes allowed**), `weavec::Analysis` (Clang AST → core facts;
-the only layer that includes both), `weavec::Frontend` (Clang
-`FrontendAction`, whole-program orchestration, sidecars, the compiler
-driver, diagnostics bridging). `tools/weavec` is a libTooling CLI;
-`tools/weavec-cc` is a drop-in C compiler (Clang's driver with WeaveC
-inside) that analyses the whole program at link time (RFC 0005).
-Full picture: `docs/architecture.md`; model semantics and the reasoning
-behind them: `docs/rfcs/` (start with `0001-ownership-model.md`).
+WeaveC is a Clang/LLVM-based C compiler and analysis tool that adds inferred
+ownership and borrowing to C. For every safety facet (spatial, null,
+temporal) of every memory operation it records one outcome in a *ledger*:
+proven, checked by a runtime check it inserts, a definite violation (an
+error), or unresolved or trusted with a reason. Three C++ libraries:
+`weavec::Core` (the model, the ledger, pointer kinds, the library table;
+**no Clang/LLVM includes allowed**), `weavec::Analysis` (Clang AST → core
+facts: sites, kinds, the engine behind the `SafetyEngine` seam, the check
+planner; the only layer that includes both), `weavec::Frontend` (deferred
+CodeGen, check emission, zero-initialisation, ledger writers, unit records,
+whole-program orchestration, the compiler driver, diagnostics bridging).
+`runtime/` holds the small C runtime for report mode and precompiled
+headers. `tools/weavec` is a libTooling CLI; `tools/weavec-cc` is a drop-in C
+compiler (Clang's driver with WeaveC inside) that inserts the checks and
+analyses the whole program at link time. Full picture:
+`docs/architecture.md`. Model semantics and the reasoning behind them:
+`docs/rfcs/`. Read `0001-ownership-model.md` first, then
+`0030-prove-or-trap.md`, which is the current model: it replaces RFC 0001's
+guarantee, amends RFCs 0002–0017 where they say so, and supersedes RFCs
+0018–0029. There is no checked mode.
 
 ## Before touching the model or the checker
 
-Design decisions for `Core`, `lib/Analysis/Dataflow.cpp` (the checker),
-`weavec.h`, diagnostic ids, and what crosses translation units (exports,
-the program database, the sidecar) are recorded as RFCs in
-`docs/rfcs/`. **Read the relevant RFC before changing any of these**, and
-treat it as authoritative over comments in the code. If the change you are
-about to make is not covered by an Accepted RFC, or contradicts one, stop and
-write or amend an RFC first (`docs/rfcs/README.md` explains when one is
-required and the process); do not encode a new design decision in code
-alone. Bug fixes that bring code in line with an RFC need no RFC.
+Design decisions for `Core`, the checker (the engine behind `SafetyEngine`,
+today `FunctionDataflow` in `lib/Analysis/Dataflow*.cpp`), the ledger and
+its outcomes and reasons, `LibrarySpec.txt`, `weavec.h`, diagnostic ids,
+the inserted checks, and what crosses translation units (exports, the
+program database, the unit record) are recorded as RFCs in `docs/rfcs/`.
+**Read the relevant RFC before changing any of these**, and treat it as
+authoritative over comments in the code. If the change you are about to
+make is not covered by an Accepted RFC, or contradicts one, stop and write
+or amend an RFC first (`docs/rfcs/README.md` explains when one is required
+and the process); do not encode a new design decision in code alone. Bug
+fixes that bring code in line with an RFC need no RFC.
 
 ## Build and test
 
@@ -38,15 +50,20 @@ cmake --preset dev && cmake --build --preset dev && ctest --preset dev
 - Unit tests: `build/dev/unittests/WeaveC{Core,Analysis,Frontend}Tests`.
 - Integration tests: `lit -v build/dev/test` (FileCheck-based; see
   `test/README.md`).
+- Test cases: `scripts/run-cases.py [--filter 'soundness/**']` (see
+  `test/cases/README.md`); CTest runs them as `cases-<suite>`.
+- Corpus gate: `scripts/corpus-gate.py --quick` (see `test/corpus/README.md`).
+- Hygiene gate: `scripts/check-hygiene.py`.
 - Format: `scripts/format.sh`; check: `scripts/check-format.sh`.
 
 ## Rules that reviewers will enforce
 
 1. Never add `clang/` or `llvm/` includes under `include/weavec/Core` or
    `lib/Core`.
 2. Every new diagnostic gets a stable id in `weavec::core::diag`
-   (`include/weavec/Core/Diagnostic.h`), an entry in `docs/annotations.md`,
-   a unit test, and a lit test that pins the exact message.
+   (`include/weavec/Core/Diagnostic.h`), an entry in `docs/annotations.md`
+   and `docs/data/diagnostic-remedies.json`, a unit test, and a lit test that
+   pins the exact message.
 3. Annotation spellings live in exactly two places that must agree:
    `include/weavec/Analysis/Annotations.h` (`spelling::`) and
    `resources/include/weavec.h`.
@@ -57,31 +74,48 @@ cmake --preset dev && cmake --build --preset dev && ctest --preset dev
    than anonymous namespaces); `.clang-tidy` enforces it.
 6. Use Conventional Commit PR titles and document user-visible changes in the
    relevant guides. `CHANGELOG.md` is generated solely by semantic-release;
-   do not edit it manually. Pre-0.1.0 notes are archived in
-   `docs/development-history.md`.
+   do not edit it manually.
 7. Do not commit generated files (`build/`, `compile_commands.json`).
 8. Changes to `Core`, checker rules, annotations or diagnostic ids reference
-   the RFC that specifies them (in the PR and, for lit tests, in the
-   filename: `test/Analysis/rfc0002-*.c`).
+   the RFC that specifies them in the PR. New tests are named by feature
+   (`test/cases/<area>/…`, `test/Emission/<feature>-*.c`); existing
+   `rfcNNNN-` names may stay.
+9. Keep the engine seam and the library table clean (gate H2,
+   `scripts/check-hygiene.py`): only `DataflowEngine.cpp`,
+   `FunctionAnalysis.cpp`, `CallbackSummaries.cpp`,
+   `CallContextSummaries.cpp`, `KindSeeding.cpp` and the `Dataflow*.cpp`
+   files include `Dataflow.h`; `FunctionDataflow` publishes only through `LedgerAdapter`
+   and never receives a `DiagnosticSink`; library behaviour goes in
+   `lib/Core/LibrarySpec.txt`, never in `name == "…"` tests; nothing under
+   `lib/` names a corpus project; library code stays within its line
+   budget.
 
 ## Where things are
 
 | Task                                 | Look at                                                |
 | ------------------------------------ | ------------------------------------------------------ |
 | Propose a model / checker change     | `docs/rfcs/README.md`, `docs/rfcs/0000-template.md`    |
-| Add a checker rule                   | `lib/Analysis/Dataflow.cpp` (after an RFC)             |
+| Add a checker rule                   | After an RFC, behind the seam: the engine (`lib/Analysis/Dataflow*.cpp`, run by `DataflowEngine`) publishes only through `LedgerAdapter` (`include/weavec/Analysis/LedgerAdapter.h`, `SafetyEngine.h`) |
+| Change outcomes, reasons, the summary line | `lib/Core/Ledger.cpp`, `lib/Analysis/LedgerAdapter.cpp` (defaults, rollup) |
+| Change which sites exist             | `lib/Analysis/SiteCollector.cpp`                       |
+| 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/KindSeeding.cpp` |
+| Change which checks are inserted     | `lib/Analysis/CheckPlanner.cpp` (plan), `lib/Frontend/CheckEmitter.cpp` and `Prelude.cpp` (emission), `runtime/` |
+| Change zero-initialisation           | `lib/Frontend/ZeroInit.cpp`                            |
 | Map an expression to a place         | `lib/Analysis/PlaceBuilder.cpp`                        |
-| Recognise an allocator / releaser    | `lib/Analysis/Allocators.cpp`, `lib/Analysis/Builtins.cpp` (libc table) |
+| Model a C library function / allocator / releaser | `lib/Core/LibrarySpec.txt` (one unit test per row in `unittests/Core/LibrarySpecTest.cpp`), `lib/Analysis/Allocators.cpp` |
+| Change function-pointer slots        | `lib/Core/FnSlots.cpp`, `lib/Analysis/SlotCollector.cpp` |
 | Change how a callee's summary is found | `lib/Analysis/Summaries.cpp` (`SummaryStore`, RFC 0003/0005) |
-| Change the TU driver / call graph    | `lib/Analysis/TranslationUnitAnalysis.cpp`             |
+| Change the TU driver / call graph    | `lib/Analysis/TranslationUnitAnalysis.cpp`, `lib/Analysis/UnitPipeline.cpp` |
 | Change what a unit exports / the program database | `lib/Analysis/ProgramDatabase.cpp` (RFC 0005) |
 | Change the summary text format       | `lib/Core/SummaryIO.cpp` (versioned; round-trip tests) |
-| Change the whole-program algorithm   | `lib/Frontend/ProgramAnalysis.cpp`                     |
-| Change the sidecar file (`foo.o.weavec`) | `lib/Frontend/Sidecar.cpp` (bump `SidecarFormatVersion`) |
+| Change the whole-program algorithm / link step | `lib/Frontend/ProgramAnalysis.cpp`, `lib/Frontend/Driver.cpp` |
+| Change the unit record (`foo.o.weavec`) | `lib/Frontend/UnitRecord.cpp` (format 28; the schema fingerprint follows the codec's field table), `lib/Frontend/Sidecar.cpp` |
+| Change the ledger JSON / SARIF       | `lib/Frontend/LedgerWriter.cpp`, `lib/Frontend/LedgerOutput.cpp` |
 | Change `weavec-cc` (driver, cc1 wrapping, link step) | `lib/Frontend/Driver.cpp`, `tools/weavec-cc/main.cpp` |
 | Change `-W` / `-fweavec-*` handling  | `lib/Frontend/DiagnosticControl.cpp`, `DriverOptions` in `Driver.h` |
-| Debug what the checker inferred      | `weavec --dump-analysis file.c --`; `weavec --whole-program --dump-analysis a.c b.c --` |
-| Measure precision on real code       | `scripts/corpus.py`, `scripts/corpus/README.md`        |
+| Debug what the checker inferred      | `weavec --dump-analysis file.c --`; `weavec --dump-kinds file.c --`; `weavec --ledger=out.json file.c --`; `weavec --whole-program --dump-analysis a.c b.c --` |
+| Add or run a test case               | `test/cases/README.md`, `scripts/run-cases.py`         |
+| Measure precision on real code       | `scripts/corpus-gate.py`, `test/corpus/` (README, manifest, expected ratchet, triage) |
 | Change how diagnostics are rendered  | `lib/Frontend/ClangDiagnosticSink.cpp`                 |
 | Add a CLI flag                       | `tools/weavec/main.cpp`, `FrontendOptions`; driver flags in `Driver.h` |
 | Add an annotation                    | `Annotations.h`, `weavec.h`, `docs/annotations.md`     |

CMakeLists.txt

@@ -104,6 +104,9 @@ add_subdirectory(lib)
 
 if(WEAVEC_BUILD_TOOLS)
   add_subdirectory(tools)
+  # RFC 0030: libweavec_rt.a and libweavec_chk.a (the latter generated with
+  # `weavec-cc -fweavec-print-prelude=out-of-line`).
+  add_subdirectory(runtime)
 endif()
 
 if(WEAVEC_BUILD_TESTS)

CMakePresets.json

@@ -121,6 +121,7 @@
     {
       "name": "test-base",
       "hidden": true,
+      "environment": { "CTEST_PARALLEL_LEVEL": "" },
       "output": { "outputOnFailure": true },
       "execution": { "noTestsAction": "error", "stopOnFailure": false }
     },

CONTRIBUTING.md

@@ -93,11 +93,13 @@ Additional rules:
 - **Warnings** are errors in CI. Do not suppress warnings without a comment
   explaining why.
 - **Tests.** New checker behaviour needs both a unit test (in `unittests/`)
-  exercising the core logic and a lit test (in `test/`) exercising the
-  end-to-end diagnostic. Lit tests that pin behaviour specified by an RFC
-  carry its number in the filename (`test/Analysis/rfc0002-*.c`).
-  False-positive fixes need a regression test in `test/Analysis/clean.c` or a
-  new file.
+  exercising the core logic and an end-to-end test: a lit test (in `test/`)
+  when the exact diagnostic text matters, or a case under `test/cases/`
+  whose markers pin what must be reported, checked or left unproven (see
+  `test/cases/README.md`). New tests are named by feature
+  (`test/cases/<area>/…`, `test/Emission/<feature>-*.c`), not by RFC number;
+  existing `rfcNNNN-` names may stay. False-positive fixes need a regression
+  case under `test/cases/` (a `// CLEAN` file).
 
 ## Commit messages
 
@@ -121,8 +123,7 @@ and `chore` normally do not trigger a release. Optional scopes include `core`,
 
 Python Semantic Release generates `CHANGELOG.md` from the commit history;
 do not edit it manually. Document behavior and migration guidance in the
-relevant guides and commit/PR descriptions. The earlier hand-written notes
-are preserved in [the development history](docs/development-history.md).
+relevant guides and commit/PR descriptions.
 
 ## Reporting bugs