feat!: add checked input cases and union member tracking

README.md

@@ -21,6 +21,17 @@ WeaveC itself is written in modern C++, which provides the most direct and compl
 
 > **Status:** early. Function bodies are analyzed by a bounded dataflow ([RFC 0002](docs/rfcs/0002-intraprocedural-checking.md)): use-after-free and double-free through any alias and across loops, use-after-move, conflicting borrows, and pointers that outlive what they point to. Calls are modelled by inferred signatures ([RFC 0003](docs/rfcs/0003-signature-inference.md)): every function in the translation unit gets a summary of what it frees, writes, stores and returns, so `node_free(n); n->v` is caught without annotations; the C standard library and POSIX are covered by a shipped table, and annotations are checked against the bodies that carry them. Unsafe code has a boundary ([RFC 0004](docs/rfcs/0004-unsafe-boundaries.md)): pointers cast from integers or declared `WEAVEC_RAW` are *raw* and may only be dereferenced or released inside a `WEAVEC_UNSAFE` region, which is analysed rather than skipped; calls through function pointers are checked from the pointer type's annotations or from the functions assigned to it. Programs are analysed whole ([RFC 0005](docs/rfcs/0005-whole-program-analysis.md)): every translation unit exports the summaries of what it defines, so `other_free(o); o->v` is caught when `other_free` lives in another file, callbacks registered in one file are checked in the file that calls them, and unresolved direct or indirect calls are reported as boundaries. `weavec-cc` is a drop-in `cc` that does this as part of a normal build. The checker is precise where C idioms need it ([RFC 0006](docs/rfcs/0006-precision.md)): a borrow ends at the pointer's last use, not at the end of its scope; `if (p == sentinel) return; free(p);` knows the two are distinct; proven distinct array elements retain independent release history; and a function that frees its argument only when it returns `0` (or `NULL`) is summarised per outcome, so `if (rc != 0) free(p);` is clean while `if (rc == 0) use(p);` is reported. The other half of the ownership contract is checked too ([RFC 0007](docs/rfcs/0007-resource-lifecycle.md)): a resource that is never released is a `leak`, reported where it is lost (`if (c) return -1;` after a `malloc`, an overwrite, a discarded `strdup`, a `free(b)` that drops an owned `b->data`), and releasing it with the wrong function (`free` on a `FILE *`, through any wrapper, across files) is a `mismatched-release`. Pointers are checked for validity, not only ownership ([RFC 0008](docs/rfcs/0008-pointer-validity.md)): dereferencing a `malloc` result, a `strchr` result or any other pointer that may be null without testing it is a `null-dereference` (through calls too: a function that dereferences its parameter requires callers to prove it non-null), a pointer used before it is assigned is a `use-of-uninitialized`, `free` of a stack object, a string literal or the middle of an allocation is an `invalid-release`, and a callee that frees a value and then reinitialises the place (`realloc` in place, `free` then `= NULL`) still kills every copy of the old value the caller kept. The checker also knows *why* ([RFC 0009](docs/rfcs/0009-value-conditional-behaviour.md)): it tracks what is known about integers, so `if (c) free(p); ... if (!c) use(p);` and `switch (op) { case FREE: free(p); }` followed by another `switch` on `op` are clean; a callee's behaviour is summarised *per argument* (`l_alloc(ud, p, n, 0)` frees `p` and returns null, `l_alloc(ud, p, n, 64)` does not; `if (!b->noalloc) free(b->data)` frees only for callers that did not set the flag); and a function whose every path ends in `abort`, `exit`, `longjmp` or another such function is inferred `noreturn`, so `if (bad) die(); use(p);` is checked on the good path only. Objects with more than one owner are understood ([RFC 0010](docs/rfcs/0010-shared-ownership.md)): a reference count is inferred from the `obj_ref`/`obj_unref` pair that keeps it (`o->rc++`; `if (--o->rc == 0) free(o)`, in any spelling from `o->rc--` to `__atomic_fetch_sub`), so `b = obj_ref(a); obj_unref(b); use(a)` is clean while one `obj_unref` too many is a `double-free`, a use after the last one is a `use-after-free`, and a reference taken and dropped is a `leak`; a callee that stores its argument only on success (`if (bag_put(b, s) < 0) free(s);`) is summarised per outcome, and one that keeps its argument in a node of its own (`table_set(t, o)`) is known to have kept it. Memory is checked spatially as well as temporally ([RFC 0011](docs/rfcs/0011-spatial-safety.md)): a pointer is an object and an offset into it, so `free(container_of(i, struct outer, in))` frees what `i` belongs to and a field pointer kept across `free(p)` is a `use-after-free`; objects have a size (`malloc(n)`, `char buf[8]`, a wrapper's `xmalloc(n)`, a `WEAVEC_SIZED_BY(len)` parameter) and every subscript, dereference and `memcpy`/`memset`/`fgets`/`read` length is checked against it, through what the path knows of the index (`i <= n` on `malloc(n)` may reach one past the end; `i < 8` on four bytes may reach `7`), so `buf[8]`, `for (i = 0; i <= n; i++) p[i]` and `memcpy(small, src, 16)` are `out-of-bounds`, and a callee that writes `b[7]` requires eight bytes of every caller. Strings and counted fields are sizes too ([RFC 0012](docs/rfcs/0012-spatial-safety-strings-and-fields.md)): the checker knows the length of what a buffer holds (`strlen(s)`, a literal, what `strcpy`/`strcat`/`sprintf` left) and whether it is NUL-terminated at all, so `strcpy(malloc(strlen(s)), s)`, `strcat(buf, "d")` on a full `buf` and `strlen(name)` after a `strncpy` that filled `name` are `out-of-bounds`; a pointer field is sized by a sibling count, declared (`char *WEAVEC_SIZED_BY(cap) data; size_t cap;`) or inferred from every store the program makes into it, so `b->data[b->cap]` is `out-of-bounds` and `b->data = malloc(4); b->cap = 8;` is an `annotation-mismatch`; `if (i <= n - 1) a[i + 1]` and `if (i >= 8) buf[i]` are decided; and `WEAVEC_ASSUME(len < cap)` states an invariant the function cannot see. A Juliet-style recall set (`test/recall`) tracks what fraction of each CWE the checker catches. Shipped summaries for libraries beyond libc and a Clang plugin packaging are next. See [docs/roadmap.md](docs/roadmap.md).
 
+Checked helpers can be rechecked under established input cases, including
+read-only helpers and forwarded callbacks
+([RFC 0025](docs/rfcs/0025-case-sensitive-checked-contracts.md)). Named unions
+with scalar or pointer members carry independent member evidence: a tag selects
+a branch, while actual writes establish its payload. Complete compatible copies
+preserve that evidence, and overlapping writes invalidate old values. Reports
+retain each case's premises and result alongside the generic definition. See
+the [case and union guide](docs/checked-code.md#check-input-cases-and-union-members)
+and [validation record](docs/validation-rfc0025.md) for supported cases,
+remaining limits and measured coverage and cost.
+
 Common C runtime operations now carry checked contracts
 ([RFC 0024](docs/rfcs/0024-checked-runtime-contracts.md)). Comparison and search
 check initialized input; descriptor and stream reads establish only their

docs/annotations.md

@@ -759,3 +759,11 @@ a non-null pointer`. No annotation or warning suppression grants runtime safety.
 Implicit output also requires a live standard stream, including through
 helpers that do not spell the stream argument.
 See [C runtime contracts](checked-code.md#c-runtime-contracts).
+
+RFC 0025 adds the `checking-incomplete` reason
+`read requires an initialized compatible union member`. This requirement is
+independent of pointee lifetime, initialized bytes, bounds and ownership. A tag
+comparison cannot establish it. Unrepresented union storage reports
+`union storage cannot be represented`; a call whose input member path cannot
+be resolved reports `union member requirement cannot be instantiated`.
+No new annotation spelling or diagnostic identifier is introduced.

docs/architecture.md

@@ -51,7 +51,7 @@ dispatch. `DataflowRuntime.cpp` checks memory and stream preconditions,
 They use the existing checked call, callback, output and summary machinery.
 Source definitions retain priority over library spellings. Ordinary summaries
 alone never authorize a checked runtime contract. Portable records use checked
-encoding 6, summary format 19 and sidecar format 20.
+encoding 7, summary format 20 and sidecar format 21 (RFC 0025).
 
 | Header             | Purpose                                                                                        |
 | ------------------ | ---------------------------------------------------------------------------------------------- |
@@ -454,7 +454,7 @@ checks by source operation. `--dump-analysis` prints
 These counts are independent of unsafe-region reporting and warning controls.
 A caller requirement is an obligation, not a proof that all callers satisfy it.
 
-`SummaryFormatVersion` is **19** and `SidecarFormatVersion` is **20**. Numeric
+`SummaryFormatVersion` is **20** and `SidecarFormatVersion` is **21**. Numeric
 outputs use `numeric <path> value ...` records; `requires-extent` retains
 optional `start` intervals and typed guards. Core validates types, operators,
 paths, shapes and limits. Comparison, global remapping and dependency
@@ -746,3 +746,25 @@ descriptor. Hitting a limit loses proof. Native inference initially supports
 null-ended singly linked chains; Core also checks endpoint-exclusive explicit
 segments. General graphs, cyclic ownership, tagged unions, volatile/atomic links
 and doubly linked mutation remain outside this predicate.
+
+### Input cases and overlapping member storage (RFC 0025)
+
+`DataflowCases.cpp` discovers bounded scalar/pointer input paths and forwards
+those candidates across calls. `DataflowCallContext.cpp` captures established
+values for read-only helpers as well as memory-changing helpers. Each canonical
+context retains a separately checked summary; generic definition reports and
+selection remain independent. Unsupported CFG operations are accounted for
+where they execute, while unrepresented operations remain conservative.
+
+`Core/Union.h` stores member descriptors and bounded guarded witnesses without
+Clang dependencies. `DataflowUnions.cpp` supplies target layouts, checks member
+reads and invalidates overlapping values on writes. Independently captured
+pointer positions may survive a guarded member join, but the member witness
+never supplies initialized pointee bytes. Consumption, unknown writes and lost
+scalar dependencies retire the corresponding evidence. Record copies project
+holder identities before installing copied pointer facts.
+
+Checked encoding 7 carries optional `caseInputs` and `union-member` requirements
+and postconditions. Sidecars and checkpoints retain the existing canonical
+context-to-summary association. Expanded and compact reports include every
+retained case premise and ledger under the generic function's `cases` field.

docs/checked-code.md

@@ -155,6 +155,40 @@ A potentially overlapping write must preserve the witness, establish a new
 zero, or lose the termination evidence. Separating pointer holders does not
 separate the arrays they reference.
 
+## Check input cases and union members
+
+RFC 0025 rechecks helpers under bounded facts established by a caller,
+including read-only helpers. For example, `read_if(0, 0)` can be checked when
+`read_if` returns immediately for a zero selector, even if its other branch
+has unresolved arithmetic or memory accesses. Forwarding helpers and resolved
+callbacks retain the case premises. Every evaluated selector still needs
+initialized storage; a tag value supplies no payload or pointee permission.
+
+Named, complete unions with scalar or pointer members can be checked directly:
+
+```c
+union value { int number; int *pointer; };
+int main(void) {
+    int n = 7;
+    union value v = {.pointer = &n};
+    return *v.pointer;
+}
+```
+
+Reading a member requires evidence that this member was initialized. Reading
+another member, or changing an enclosing tag without establishing the selected
+payload, leaves checking incomplete. A pointer member independently needs live
+storage, sufficient bounds and initialized pointee bytes. Compatible complete
+record copies preserve member evidence; partial byte writes and unknown writes
+invalidate overlapping values. Guarded branch joins retain only evidence
+justified on every applicable incoming path.
+
+A helper can require an input member or establish a member through an output
+parameter or a returned record. The `union-member` requirement is separate
+from initialized byte ranges. Unsupported aggregate/array members, anonymous
+member promotion, bit-fields, volatile/atomic union storage and representation
+punning remain incomplete. There is no union or tag annotation.
+
 ## Read a report
 
 `--checked-report=path` computes contracts and writes JSON without selecting
@@ -167,7 +201,14 @@ units with source, target and function records. Each function records:
 - `status`: proven, conditional, trusted, or incomplete;
 - sufficient `requirements` and guaranteed `establishes`, including `when`
   input guards and optional `on` returning outcomes;
-- `obligations` with property, outcome, source location, reason and call origins.
+- `obligations` with property, outcome, source location, reason and call origins;
+- `case_inputs`, the optional candidate input paths, and `cases`, each with
+  canonical `premises` and its own complete contract and obligation ledger.
+
+Case results do not change the generic function's status or the totals of
+selected definitions. Selecting both a successful caller and its incomplete
+generic helper still fails the invocation. Compact reports preserve the same
+case records when expanded with `scripts/checked-report.py`.
 
 Obligation outcomes distinguish proven facts, entry requirements, explicit
 trust, unresolved coverage and violations. A complete conditional helper still
@@ -433,6 +474,6 @@ establish the exact written prefix. If `0 <= n && n < sizeof buffer`, `buffer[n]
 is the written terminator. If `n >= sizeof buffer`, truncation initializes the
 capacity and its final NUL. A negative or overwritten result establishes neither.
 
-Runtime records use checked encoding 6, summary format 19 and sidecar format 20.
+Runtime records use checked encoding 7, summary format 20 and sidecar format 21.
 Rebuild objects carrying older sidecars. The cache validates the executable and
 source dependencies before reusing these records.