Inductive containers (RFC 0023)

Core/Container.h keeps the portable chain descriptor, explicit graph prover, capability entailment and bounded must-fact lattice independent of Clang. ContainerShape describes the canonical record layout, its successor field, initialized fields, optional terminal head and read/write/release capability. A release shape also describes owned payload fields and allocation families. The graph prover checks every explicit node and endpoint; it never treats an unknown edge as null. A folded fact represents any finite runtime length.

DataflowContainers.cpp discovers candidate links from actual field operations, establishes predicates from checked storage, and exports sufficient entry premises for generic functions. Candidate discovery supplies no closed proof. Immutable entry witnesses retain their original descriptors when a cursor or output shape changes. DataflowContainerTransfer.cpp handles field mutation, folding, saved successors, separated regions, release and call invalidation. DataflowContainerContracts.cpp transports the resulting output predicates. These components use the existing evaluated CFG and loop fixed point; ordinary integer, lifetime, byte-memory, unsupported-call and leak checks still apply.

The fact’s member set is a conservative invalidation dependency, not evidence of separation. Separation comes from concrete disjoint storage, a sufficient entry premise, a saved head/tail relation, or fresh allocation. An unknown write retires affected evidence and prevents the same input from being assumed again. Pointer replacement also retires saved relations to its former value. Joins intersect established facts and separation while combining invalidation sets. Quantified release also retires native byte-pointer evidence into the consumed footprint, including owned payloads. SafetyState::invalidatedPointers prevents an old input snapshot or allocation record from reestablishing checked lifetime after consumption. The mark survives joins and pointer copies until a new value is installed; ordinary resource records remain available for leak checking.

Checked encoding 5 adds container, container-separated, container-derived, container-fresh and container-tail. Derived outputs retain up to three conjunctive entry sources, all remapped through the existing path machinery. They describe a subset plus freshly added nodes; they do not promise full input consumption. Fresh outputs require actual allocation evidence. Tail outputs are imported across read-only calls. A terminal output can establish a detached node’s null successor. Descriptors, source premises and capability combinations are validated during decoding. Summary format 23 and sidecar format 24 prevent older metadata from silently discarding these records.

Limits are 32 fields, 64 explicit nodes, 64 active facts and 16 KiB per encoded 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.

Recursive ownership and footprint conservation (RFC 0027)

ContainerShape adds multiple recursive fields, initialized-scalar ownership conditions, and head-only refinements for known null links/payloads and scalar values. Descendant projection drops head refinements. The explicit graph prover checks acyclicity, initialized nodes, active ownership edges and disjoint owned payloads; inactive edges grant no pointee capability. Partial head facts retain which children or payloads have already been released and cannot be exported as intact whole objects.

Core/Footprint.h supplies a separate sparse domain of exact equalities over formal allocation identities. Fraction-free elimination detects arithmetic overflow. Forget is existential projection; join intersects row spaces, including equalities represented by different bases. Both variables and relations are capped at 64. These equations cannot create structural validity or separation.

DataflowFootprints.cpp maintains entry snapshots, head/payload allocations, conditional field contributions, current root footprints, acquired allocations and accumulated release. Replacement and mutation retire current-value equations while retaining historical allocation identities. A complete output requires both the structural predicate and its proved conservation relation. Calls capture inputs before effects, then install only established output relations. Indirect targets contribute only their common guaranteed outputs.

Direct recursive cleanup uses private proper-child induction hypotheses. Every returning path must establish complete input consumption before an inferred contract is published. Active recursion alone supplies no output. The ordinary may-effect fixed point continues independently. Mutual recursion remains conservative. Complete preservation, consumption, partition and combination outputs use checked encoding 9; strict decoding requires their source predicates and separation premises. Summary format 23 and sidecar format 24 carry these records across program databases, object metadata and validated checkpoints.

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

Contiguous buffer invariants (RFC 0026)

Core/Buffer.h separates layout, initialized prefix, optional termination, backing release permission and pointer-element sequence ownership. Its must facts intersect at joins. Guarded posts carry immutable call results and lose their authority on dependent writes. Bounded sequence refinements distinguish preserving entry elements from appending a separately represented pointer.

DataflowBuffers.cpp discovers candidate records and establishes the current predicate from allocation, byte, count and lifetime facts. It materializes relational bounds without equating successive backing allocations. DataflowBufferContracts.cpp checks caller premises, activates result-guarded posts, projects interfaces and accounts for element release obligations. DataflowTraversalRelations.cpp proves bounded min/max and nonwrapping sum relations on each predecessor. Compound count updates carry only bounds and initialized prefixes proved for their evaluated right-hand side.

SummaryStore memoizes immutable layout discovery, including rejected shapes, for one AST lifetime. Its 256-entry cache recomputes on saturation and never stores flow facts or proof results. Discovery avoids interning places for records with no buffer subobjects. Buffer-specific range snapshots and numeric reasoning run only in functions with registered buffer candidates.

Checked encoding 9 carries validated buffer, buffer-preserved and buffer-appended requirements and outputs to the existing interface codec. Summary format 23 and sidecar format 24 reject older encodings. Ordinary warnings remain independent from checked completeness.