Checked contracts (RFCs 0018–0019)

Core/Safety owns the obligation ledger, object identities, guarded initialized and zeroed ranges, and bounded branch premises. Pointer holders and pointee storage have separate identities; initialization cannot establish provenance. Core/CheckedContract implements sufficient precondition union and postcondition intersection; Core/CheckedIO provides bounded portable serialization. FunctionSummary::checked is deliberately separate from witness-based requiresExtent, and survives global remapping and joins.

The Analysis layer attaches operation accounting to the existing CFG transfer and reporting passes. DataflowSafety inventories supported semantics, initialization and diagnostics; DataflowSafetyMemory resolves byte intervals and entry requirements; DataflowSafetyCalls discharges requirements and models library effects; DataflowSafetyContracts captures call-entry dependencies and applies conditional output facts; DataflowSafetyLoops projects sufficient counted-loop bounds and proves complete supported fills/copies on normal exits. PendingOutcome carries memory and numeric output facts until an outcome is selected, with invalidation when output storage or dependencies change. The additional state is enabled by checked selection or a report request.

RFC 0021 adds stable same-array positions and terminated-prefix witnesses to the checked state. Core/Traversal provides bounded difference constraints and target pointer-difference arithmetic; Core/Relation joins both sides of a difference interval and widens changing bounds through a finite zero threshold. These components contain no Clang or LLVM dependencies.

CheckedRequirements shares ordered entry/output sets between copied contracts. Its public iterators are immutable; insertion and intersection detach shared storage before modifying it. Duplicate joins preserve storage, the original requirement cap and exact portable contents. This avoids copying large conditional guards while rebuilding whole-program databases. RFC 0024 reuses canonical call ledgers in the bounded explanation-preparation cache. The key includes the live source projection, callee, caller, call site and trust/unsafe modes. Ordered merging applies when the obligation cap cannot be reached. Near the cap, prepared rows retain the original origin order and capacity decisions. Retained rows, strings and call-path capacity count against the existing cache byte bound; cache eviction changes reuse only. Global remapping retains shared checked sets when none of their paths, affine expressions or guard predicates references a global. Path projection caches immutable local/synthetic failures as well as stable interface paths; array selectors remain dependent on the current state. RFC 0028 stores summary-path steps in SummarySteps: copies and shortened prefixes share read-only bytes, while explicit edits detach before mutation. An atomic reference count and trailing element array share one aligned allocation; the path handle retains only the backing pointer and visible length. Allocation arithmetic and object lifetimes are checked. The uniqueness check acquires other handles’ releases before reusing their backing bytes for an edit. Call-input footprints stop with an explicit over-limit result after the existing 64-fact bound. Each function can reuse up to 64 preparations under live immutable summary owners. Caller values, aliases and checked-case additions are always computed from the current state. Element views remain const, and self-append retains its source during growth. The common dereference step has one immutable backing value. This changes no path ordering, selector, serialized spelling or proof premise. PlaceTable uses owned hashed keys with non-owning lookup probes; dense IDs and descendant order still follow creation order. Sorted effect maps merge with a moving insertion position while preserving each existing per-path join. Generic and specialized unit exports use ExportedSummary to retain an immutable publication. Unit copies, database indexes and checkpoint inputs reuse it when global numbering agrees. Its const value view supports exact comparison and transport; replacement and widening publish independent values. Remapping retains the input publication only when the projected value and all proof explanations remain identical. Context keys remap independently. Memory specializations retain the original join and normalization; report invalidation replaces its own publication without changing earlier readers. At unit export, a sufficient entry requirement may omit antecedent predicates on known private globals. This strengthens its caller obligation while keeping the native contract precise. Required object/interval references and every public output premise still undergo strict global remapping. DataflowCursors captures and updates byte coordinates; DataflowPointerOperations validates same-array comparisons and differences; DataflowTraversalRelations verifies common incoming facts and sufficient buffer envelopes; DataflowStringTraversal maintains initialized termination witnesses. Dataflow.cpp retains all CFG edges, including direct gotos, and can partition eligible small loops by completed back edges before falling back to widening. Every final obligation is checked on converged states.

position, progress and explicit terminator quantities cross interfaces through checked-record encoding 9. Call-entry snapshots precede ordinary effects, with output positions installed afterward. Portable call contexts can additionally contain directed same-array byte-pointer orders (o: records); these neither equate addresses nor invent ownership shares. They participate in context equality, global remapping, validation and the existing context budgets. Interacting writes must preserve the witness byte or require separation of the actual referents. AnalysisState stores it in an optional domain, so ordinary analysis skips constructing, copying and joining the proof containers.

Every computed definition, including main and private helpers, has a record in UnitExports::checkedDefinitions. This does not change externally visible function lookup. Frontend/CheckedReport collects reporting passes and writes JSON atomically. Frontend/CheckedArtifacts fingerprints build inputs and objects for compiler-sidecar validation before replay. Compilation may defer an unavailable external contract; the link pass must resolve it. Checked failure reaches Clang independently of the diagnostic filtering policy.

Summary format 23 and sidecar format 24 carry guarded/outcome-qualified contracts, numeric outputs and RFC 0021 traversal records. Checked record encoding uses version 9; report JSON uses expanded version 2 or compact version 3. Strict parsing and global remapping reject missing premises. Explanation depth is bounded independently of semantic contract limits; truncating a call chain does not change the obligation it explains.

The unit exporter preserves supported private roots and their postconditions with RFC 0028 interface metadata. Entry requirements and private premises of public/result output facts retain strict remapping; exporting a contract cannot silently forget something its proof needs. Unsupported private storage retains the conservative exclusion rules.