DESIGN RECORDS
The RFC library
Every major design decision has a written record: the problem, the proposed semantics, the tradeoffs, and the evidence required. These RFCs are the authoritative design references for WeaveC.
Accepted records specify the design. Implemented records have completed their defined implementation and test criteria. Superseded records are kept as history; the record that replaced them says what changed. RFC 0035 defines the guards and RFC 0036 the current guarantee. Earlier records that specify the ownership analysis RFC 0036 deleted are kept as history. A status is not a guarantee about arbitrary C programs; consult each RFC’s scope and validation.
36 design records
- RFC 0001Ownership, borrowing and lifetimes for CSuperseded
- RFC 0002Sound intra-procedural checkingSuperseded
- RFC 0003Signature inferenceSuperseded
- RFC 0004Unsafe boundaries: raw pointers, unsafe regions and indirect callsSuperseded
- RFC 0005Whole-program analysis: cross-translation-unit summaries and the compiler driverSuperseded
- RFC 0006Precision: non-lexical loans, condition facts, element places and outcome-conditional summariesSuperseded
- RFC 0007Resource lifecycle: leaks, release families and owned fieldsSuperseded
- RFC 0008Pointer validity: null dereferences, uninitialised pointers, invalid releases and replaced valuesSuperseded
- RFC 0009Value-conditional behaviour: scalar facts, guarded effects and inferred noreturnSuperseded
- RFC 0010Shared ownership: reference counts, ownership by outcome and per-outcome factsSuperseded
- RFC 0011Spatial safety: derived pointers, extents and boundsSuperseded
- RFC 0012Spatial safety II: strings, sized fields, offset relations and assumptionsSuperseded
- RFC 0013Interprocedural heap state and value identitySuperseded
- RFC 0014Pointer identity and precise call effectsSuperseded
- RFC 0015Array elements, range operations, and container ownershipSuperseded
- RFC 0016Compositional call checking under caller alias relationshipsSuperseded
- RFC 0017C integer semantics and compositional spatial safetySuperseded
- RFC 0018Compositional safety contracts and checked codeSuperseded
- RFC 0019Practical checked memory contracts for buffers and heap objectsSuperseded
- RFC 0020Scalable modular checked analysisSuperseded
- RFC 0021Practical C traversal and inductive buffer contractsSuperseded
- RFC 0022Compositional checked interfaces for opaque pointers and callbacksSuperseded
- RFC 0023Inductive ownership contracts for linked containersSuperseded
- RFC 0024Checked C runtime contracts and variadic interfacesSuperseded
- RFC 0025Case-sensitive checked contracts and discriminated C objectsSuperseded
- RFC 0026Inferred relational contracts for growable buffers and vectorsSuperseded
- RFC 0027Recursive object ownership and complete cleanup contractsSuperseded
- RFC 0028Inferred contracts for opaque objects and private library stateSuperseded
- RFC 0029Compositional invariants for recursive C workflowsSuperseded
- RFC 0030Prove or trap — one safety semantics with compiler-enforced checksImplemented (as amended by [RFC 0031](0031-object-engine.md), which replaced its engine, took over its gates G10, G14 and G15, and amended G10's limit to 65; and by [RFC 0032](0032-runtime-enforcement.md), which adds the outcome `guarded`, a runtime in every enforcing build, guards for temporal facets, the require level `guarded` and ledger version 2. Where this text says "RFC 0032" for records in object sections, baselines and archives, it means the adoption RFC, which is now planned as RFC 0033. Its analysis (§2–§9) is superseded by [RFC 0036](0036-deterministic-heap-reuse.md), which deletes it)
- RFC 0031The object engine — a sound heap abstraction behind the engine seamSuperseded
- RFC 0032Runtime enforcement — an object table, guarded facets and a temporal backstopImplemented (its cost gate R6 as amended by *Implementation amendments* 3; the original bound for zlib and Lua is carried forward)
- RFC 0033Drop-in by default — no false stops on code WeaveC was never tuned onImplemented (its build-cost gate D5 not met and carried forward, *Implementation amendments* 13)
- RFC 0034Fast enforcement, confirmed errors and a bounded analysisImplemented (gates F5 and F7, and F2's build time for opus,
- RFC 0035Guard by defaultImplemented (gates G7 and G9 carried forward as measured;
- RFC 0036Deterministic heap reuseAccepted
No matching records. Try a shorter title or choose all statuses.
Propose a change
Section titled “Propose a change”Read the RFC process for when a proposal is required, how to draft one, and how statuses change.