Skip to content

Define memory-safety models and evidence - #5226

Merged
richlander merged 25 commits into
mainfrom
docs/memory-safety-models
Aug 31, 2026
Merged

richlander merged 25 commits into
mainfrom
docs/memory-safety-models

Conversation

@richlander

@richlander richlander commented Aug 30, 2026 •

Copy link
Copy Markdown
Owner

The focused memory-safety composition design distinguishes the legacy v1 model
from the currently recognized v2 binary marker and defines how project policy,
binary contracts, method-body evidence, and provenance compose.

The PR owns only vocabulary, evidence-plane boundaries, and typed handoffs.
Implementation findings discovered during review were split into focused
owner issues: #5252, #5253, #5254, #5255, #5256, #5257, #5258, #5259,
#5260, #5262, and #5270.

The claims are grounded in the public .NET Blog overview and pinned
dotnet/designs, dotnet/roslyn, dotnet/csharplang, and dotnet/runtime
sources. The blog supplies explanatory adoption context rather than normative
compiler semantics. Egor Bogatov's dotnet/runtime#131002 migration analyzers
and dotnet/runtime#131484 source-audit work are treated as external audit
models, not a dotnet-inspect evidence plane or binary/IL-body proof.

The v2 auditing scenario explicitly requires a completeness-qualified census
of inner-unsafe methods, identification of safe boundaries as the highest
burden unsafe users, and bounded caller/callee paths in both directions across
assemblies. #5270 owns that focused DotnetInspector.ResearchQueries
composition over the existing Analysis and call-graph substrates.

Decompiler reconstruction now has an explicit runtime oracle: use
unsafe(expr) when one expression can be isolated, otherwise use the smallest
dependency-correct block and keep semantically safe statements outside. This is
synthesized placement because IL cannot recover the original block/expression
choice. #5255 and #2021 own the focused implementation and compile-back gate.

Demo

An actual .NET 11 Preview 7 throwaway class library containing only
public sealed class C { }, built with updated enforcement and
AllowUnsafeBlocks=false, produces these memory-safety rows:

Area Signal Value Evidence
Memory safety Memory safety model Updated (v2) module MemorySafetyRulesAttribute
Memory safety RequiresUnsafe members 0 RequiresUnsafeAttribute
Memory safety Disable runtime marshalling No DisableRuntimeMarshallingAttribute
Memory safety Unsafe public signatures 0 public pointer signatures

The design's composed-report mockup keeps project policy, binary facts, and
project-to-binary provenance separate, including an explicit Unverified
provenance row.

Validation

  • npx markdownlint-cli docs/design/memory-safety-models.md docs/design/memory-safety-modes.md docs/overview.md docs/README.md
  • git diff --check origin/main...HEAD

richlander and others added 2 commits August 30, 2026 07:40
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
@richlander richlander added the documentation Improvements or additions to documentation label Aug 30, 2026
@richlander

Copy link
Copy Markdown
Owner Author

Round 1 review of 51c5b05b7c5b9d29cb97ccca6d1df54001a028b8
returned three accepted findings:

  1. The mixed-model section made the callee model the sole control. Roslyn
    classifies the callee contract as implicit or explicit, but the caller model
    also controls enforcement: implicit legacy pointer compatibility is enforced
    for both caller models, while an explicit v2 contract is enforced only for
    an updated-rules caller.
  2. The Analysis gap inventory omitted call-target contracts.
    MethodSafetyAnalysis currently recognizes calls from pointer signatures or
    selected API types, so it misses pointerless RequiresUnsafe calls and
    misclassifies pointer-bearing v2 members without that contract.
  3. The demo showed abbreviated output as a shell transcript. It will be
    replaced with the full four-column, four-row output from the actual
    v2/no-unsafe throwaway probe and will identify the probe inputs.

The locked head is superseded. The replacement will keep the scope
documentation-only and will be re-reviewed as round 1.

richlander and others added 2 commits August 30, 2026 07:52
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
@richlander

Copy link
Copy Markdown
Owner Author

Round 1 replacement review of
144201b0cf191061f8471719939d2df92fe3d527 returned three accepted findings:

  1. Decompiler call reconstruction has the same missing callee-model dimension
    as Analysis. Same- and cross-assembly call handling must distinguish legacy
    pointer compatibility from v2 RequiresUnsafeAttribute contracts.
  2. The model discussed propagating "members" but described only callable
    signatures. Pointer-bearing legacy fields and attributed v2 fields also
    carry caller-unsafe contracts and must be included explicitly.
  3. Unsupported or malformed module markers do not become v2, but Roslyn still
    applies legacy pointer compatibility while also reporting the unrecognized
    marker. The design must preserve and present both facts rather than calling
    the contract judgment unavailable.

The locked replacement head is superseded. These documentation corrections
remain within the existing design scope and will receive another round 1
replacement review.

richlander and others added 2 commits August 30, 2026 08:03
@richlander

Copy link
Copy Markdown
Owner Author

Round 1 replacement review of
3dd61a6bf7952e0bd852ffc764f51aad1df939a3 returned three accepted findings:

  1. Pointer shapes determine v1 compatibility propagation, but they no longer
    prove that source established an unsafe context. Pointer relaxations are
    language-feature-gated independently of the module rules marker, so
    binary-only unsafe-user classification must keep pointer shape separate from
    positive context-requiring operations.
  2. Roslyn's unrecognized-version use-site diagnostic is implemented for
    methods/accessors, not every member kind. The design will narrow that claim
    while requiring dotnet-inspect to surface the invalid module marker
    independently for fields.
  3. The Analysis inventory omitted the shipped OpaqueUnsafeMethods() and
    HollowUnsafeMethods() classifications. Correcting CallerUnsafeMode
    changes their v2 populations, so their owning design and tests must be
    updated as part of that Analysis stage.

The locked replacement head is superseded. These remain documentation-only
corrections within round 1.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
@richlander

Copy link
Copy Markdown
Owner Author

Round 1 replacement review of
24dd38f739e5c72ba0a936a857e912460420369d returned three accepted findings:

  1. Operation evidence also needs language-feature-aware interpretation.
    Analysis currently treats every localloc as unsafe, while Decompiler
    currently wraps relaxed pointer stack allocation, arithmetic, and comparison
    operations that the unsafe-evolution language permits in safe contexts.
  2. Property and event contracts live on PropertyDef/EventDef and are inherited
    by their accessor MethodDefs. The current Analysis and Decompiler paths check
    MethodDef plus invalid TypeDef lookalikes, so the design must require
    association-aware contract resolution.
  3. Metadata already exposes a user-visible ApiMember.IsUnsafe classification
    used by api --unsafe and API diff. It combines pointer shape and method
    attributes without the module model, omits v2 property contracts, and does
    not classify fields; it must consume the shared Metadata-owned contract
    model too.

The locked replacement head is superseded. The corrections remain within the
same owner map and round 1.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
@richlander

Copy link
Copy Markdown
Owner Author

Round 1 replacement review of
695084f292d647168ee08ab7a558b86cc2962b77 produced one clean review and four
accepted findings from the other seat:

  1. Signature facts and version-aware member contracts belong to Metadata;
    Analysis owns IL-body evidence and composed method judgments.
  2. A v2 unsafe instance constructor establishes an unsafe context for its
    base(...) or this(...) initializer, but not for its body.
  3. The relaxed-declaration gap also covers ordinary fixed headers and
    pointer-bearing lambda parameters, which current Decompiler paths can wrap
    unnecessarily.
  4. Roslyn synthesizes v2 field contracts onto FieldDef even though the current
    runtime RequiresUnsafeAttribute.AttributeUsage omits fields. The design
    must follow emitted compiler metadata rather than rejecting that carrier
    from runtime reflection policy.

The locked head is superseded. The clean review does not transfer to the
replacement; both seats will review the next exact head.

richlander and others added 2 commits August 30, 2026 08:43
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
@richlander

Copy link
Copy Markdown
Owner Author

Round 1 replacement review of
b0e083be6414f2be6ffbbca7b660af8dd780ed45 returned four accepted findings:

  1. Roslyn excludes fixed-size-buffer fields from v1 implicit field contracts;
    the design's field rule needs that exception.
  2. Conflicting module markers need an explicit unavailable member-contract
    result. They cannot silently select compatibility or v2 interpretation.
  3. memory-safety-modes.md still normatively described presence-only
    Decompiler selection and must instead name recognized-v2 Metadata state as
    the contract while labeling the current presence test as an implementation
    gap.
  4. ApiMember.IsUnsafe feeds C# declaration spelling, Decompiler shells,
    Research summaries, and JS-export admission in addition to API filtering
    and diff. Its current conflation of pointer shape and caller contract needs
    a typed consumer migration so changing the contract does not silently change
    unrelated pointer-shape policy.

The locked head is superseded. Both reviewers will inspect the replacement
head; no prior clean result transfers.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
richlander and others added 2 commits August 30, 2026 10:09
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
@richlander

Copy link
Copy Markdown
Owner Author

Scope recovery completed by user direction: split into focused successors.

The broad head was superseded. Replacement head
1dbc0376d7edcca36883d6cd65f955d2c4b7e22c retains only:

  • v1/v2 vocabulary and marker semantics;
  • propagation, unsafe-user, safe-boundary, permission, and mixed-model rules;
  • project, binary, body, and provenance evidence boundaries;
  • the high-level product answer map and demo; and
  • a thin owner/dependency map.

Owner-internal findings are preserved in #5252, #5253, #5254, #5255, #5256,
#5257, #5258, #5259, and #5260. Each successor names its owner, owning
document, evidence, dependency, and non-claims.

Round 1 restarts on the focused replacement head; no review result from the
broad candidate transfers.

@richlander

Copy link
Copy Markdown
Owner Author

Round 4 replacement 2\n\nSuperseded head: f881e2963ace676e6b8466e41265662592105a04\nReplacement head: 8e33cd51b2803753b3fda1e552878ff58f1a3d56\nEffective base: 39afbe459c14d30bcc64415d8859c2b27c775704\n\nGPT-5.6 Sol found that an unsafe instance-constructor modifier supplies the base(...)/this(...) initializer context, so initializer IL cannot universally prove inner unsafe. Claude Opus 5 found that #5262 remained owned by ILInspector.Research even though it now consumes #5270 from DotnetInspector.ResearchQueries. The replacement makes positive inner-unsafe evidence context-aware, explicitly excluding initializer operations whose context is supplied by an unsafe-constructor contract and preserving missing/origin-ambiguous evidence as unknown. #5254 now owns initializer-versus-body evidence. #5262 now joins #5270 in DotnetInspector.ResearchQueries, and #5256 must expose typed policy facts from a layer that companion can consume without a CLI dependency or layering reversal.

@richlander richlander added the review-clean PR has met the adversarial review standard per AGENTS.md. label Aug 30, 2026
@richlander

Copy link
Copy Markdown
Owner Author

Round 4 is review-clean at 8e33cd51b2803753b3fda1e552878ff58f1a3d56: GPT-5.6 Sol and Claude Opus 5 both returned CLEAN on that exact head. Current-head ci-required and markdownlint are successful, and GitHub reports the PR mergeable with clean merge state.

@richlander richlander removed the review-clean PR has met the adversarial review standard per AGENTS.md. label Aug 31, 2026
@richlander

Copy link
Copy Markdown
Owner Author

Round 5 start\n\nCandidate head: 8e33cd51b2803753b3fda1e552878ff58f1a3d56\nEffective base: 39afbe459c14d30bcc64415d8859c2b27c775704\n\nThe user requested more feedback after round 4 became review-clean. The head and base are unchanged. GPT-5.6 Sol remains the fixed seat; Gemini 3.1 Pro replaces Claude Opus 5 to add a different reviewer family and a fresh reading of the complete composition and successor-owner map.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
@richlander

Copy link
Copy Markdown
Owner Author

Round 5 replacement\n\nSuperseded head: 8e33cd51b2803753b3fda1e552878ff58f1a3d56\nReplacement head: 645649796772a9730e760d536b772e0105fd655f\nEffective base: 39afbe459c14d30bcc64415d8859c2b27c775704\n\nThe user identified the subsystem-by-subsystem non-ownership inventory as unhelpful; it is replaced by a concise composition-only boundary. GPT-5.6 Sol found that v2 declarations which require explicit safe spelling had no product owner, so the shared model now records that derived requirement and #5255/#5257 own reconstruction and declaration spelling. Gemini found ambiguity between producing method roles and collecting them into an audit census; #5254 now produces separate typed propagation, inner-unsafe, and safe-boundary roles, while #5270 only filters/projects those roles onto the census and paths. The #5256 typed project-policy handoff required by #5262 is now explicit in both the issue and successor table.

@richlander

Copy link
Copy Markdown
Owner Author

Round 5 supporting-contract replacement\n\nCandidate head remains 645649796772a9730e760d536b772e0105fd655f; effective base remains 39afbe459c14d30bcc64415d8859c2b27c775704.\n\nGemini 3.1 Pro found that #5257 could not derive required safe spelling for field-backed properties and events from caller-contract absence alone. The repository document already names declaration shape as required evidence; the supporting issue handoff was incomplete. #5253 now explicitly produces typed containing-type layout and property/event backing-storage association facts, preserving unknown associations. #5257 now explicitly consumes those facts. No repository-head change was needed.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
@richlander

Copy link
Copy Markdown
Owner Author

Round 5 replacement 2\n\nSuperseded head: 645649796772a9730e760d536b772e0105fd655f\nReplacement head: 794c6a18615f3f07ccb49d6cdeb2f829567ea4f4\nEffective base: 39afbe459c14d30bcc64415d8859c2b27c775704\n\nGPT-5.6 Sol found overlapping ownership for derived v2 safe declaration spelling between #5255 and #5257. The answer map now separates CSharp declaration contract spelling from Decompiler body/context rendering. #5255 no longer owns safe modifiers and explicitly consumes CSharp declaration shells; #5257 remains the sole declaration-spelling owner over #5253 typed layout, backing-association, and caller-contract facts.

richlander and others added 2 commits August 30, 2026 21:55
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
@richlander

Copy link
Copy Markdown
Owner Author

Round 5 replacement 3\n\nSuperseded head: 794c6a18615f3f07ccb49d6cdeb2f829567ea4f4\nReplacement head: fb9d2e77029644b8dc58c4165c75d853375acc2e\nEffective base: 39afbe459c14d30bcc64415d8859c2b27c775704\n\nThe user added the Decompiler expectation for C# unsafe(expr): IL proves a context requirement but cannot recover whether source used a block or expression. The replacement defines dotnet/runtime migrated source plus its analyzer/fixer as the placement oracle: isolate one expression when possible, otherwise use the smallest dependency-correct block and exclude semantically safe statements. Current block output remains until the pinned compile-back Roslyn supports the expression form; #2021 and #5255 now record the implementation target.\n\nCarried review findings were also resolved: memory-safety-modes.md now owns body-context placement only and no longer contains Analysis-owned Opaque/Hollow classifications or declaration-modifier ownership; #5255 supplies primary-constructor fallback shape when a parameter cannot carry a required storage modifier; #5257 owns the resulting declaration spelling; and #5262 now directly depends on #5252 for the recognized binary model.

@richlander richlander added the review-clean PR has met the adversarial review standard per AGENTS.md. label Aug 31, 2026
@richlander

Copy link
Copy Markdown
Owner Author

Round 5 is review-clean at fb9d2e77029644b8dc58c4165c75d853375acc2e: GPT-5.6 Sol and Gemini 3.1 Pro both returned clean on the exact replacement head. Current-head ci-required and markdownlint are successful, and GitHub reports a clean merge state.

@richlander
richlander merged commit d645f2b into main Aug 31, 2026
11 checks passed
@richlander
richlander deleted the docs/memory-safety-models branch August 31, 2026 05:07
@richlander

Copy link
Copy Markdown
Owner Author

Production-host adoption path for the Metadata API-fact successor #5253: 3 stages. (1) #5253 publishes version-aware caller contracts, independent signature-pointer facts, module layout/rules, and conventional backing-storage evidence in the shared API models. (2) #5257 adopts those facts in the shared CSharp declaration producer, with #5255 supplying its separately owned primary-constructor fallback. (3) #5257 exercises that producer through both CLI and browser/Wasm declaration surfaces. #5253 completes stage 1 only and leaves current IsUnsafe behavior unchanged. JS-export policy #5258 and Research summaries #5259 remain independent adoption branches. Retirement/narrowing of IsUnsafe follows explicit consumer migration rather than silently changing its meaning in the producer.

@richlander

Copy link
Copy Markdown
Owner Author

Counted production-host adoption path for the declaration-spelling slice: (1) Metadata facts, including the focused layout prerequisite #6144; (2) shared CSharp declaration spelling and unchanged-product-output compiler evidence in #6105 under #5257; (3) CLI and browser/Wasm declaration/source enablement through the shared producer. Total: three stages. #6144 supplies typed evidence independently; it does not enable C# layout replay or either host. The CSharp WIP remains parked until that prerequisite lands.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

documentation Improvements or additions to documentation review-clean PR has met the adversarial review standard per AGENTS.md.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant