GAUNT-COMPILER-ASSUMPTION-LEDGER: receipt unsafe/cast/layout hazards beyond the bvisor basement

[heyoub]

Why

The current BatPak posture already has the right instinct: do not let raw bytes quietly become “truth.” transmute, raw layout assumptions, unchecked pointer moves, and narrowing casts are not ordinary code style concerns. They are places where we ask the compiler, allocator, OS, or layout model to believe an invariant it cannot prove.

The repo already has strong partial coverage:

• crates/core/build.rs::check_no_banned_patterns bans transmute, mem::read, and pointer_cast in core src, with the existing doctrine that repr(C) is not a wire format and serialization goes through MessagePack.
• tools/integrity/src/unsafe_ledger.rs reconciles sanctioned bvisor basement unsafe sites against traceability/unsafe_ledger.yaml using stable LEDGER:<id> anchors.
• The unsafe-ledger gate already catches both unsafe { ... } blocks and unsafe fn declarations, which is the right AST-level shape.

But this is still narrower than the real hazard class. BatPak has legitimate compiler-assumption sites outside the bvisor basement, such as admitted mmap mapping and feature-gated global allocator shims. Those have SAFETY comments, but they are not currently part of the same repo-wide anchored ledger model.

Proposal

Add a generalized compiler-assumption ledger/gate:

GAUNT-COMPILER-ASSUMPTION-LEDGER

This should not mean “ban all danger.” It should mean: any place that relies on a compiler/layout/allocator/OS invariant that Rust cannot prove must either be rejected or receipted.

Suggested new file:

traceability/compiler_assumption_ledger.yaml

Suggested entry shape:

entries:
  - file: crates/core/src/store/platform/mmap.rs
    anchor: core-platform-mmap-index-map
    kind: unsafe-fn
    hazard: file-backed mmap assumes semantic immutability/admission token validity
    invariant: >-
      The caller holds MmapIndexAdmission proving platform mmap admissibility and separately owns
      the store semantic proof that the mapped file will not be mutated in a way that invalidates
      the index reader.
    safer_alternative_considered: safe buffered read path exists / mmap is admitted only by evidence token
    requirement: PlatformEvidence
    tests:
      - crates/core/tests/platform_backend.rs::platform_profile_match_allows_open_and_mismatch_fails_before_lifecycle

Initial detector surface

Start strict and practical. Prefer AST over raw grep where possible.

Track/reconcile:

• unsafe { ... }
• unsafe fn
• unsafe impl
• std::mem::transmute
• std::mem::transmute_copy
• std::mem::read
• std::mem::zeroed
• MaybeUninit::assume_init
• from_raw_fd, from_raw_handle, from_raw_parts, from_raw_parts_mut
• raw pointer deref/read/write/copy
• unchecked indexing/slicing APIs
• pointer casts and suspicious as casts involving raw pointers, function pointers, or integer-pointer boundaries

Do not initially ban every numeric as cast repo-wide. That will turn the gate into lint confetti. Instead:

1. hard-reject pointer-ish as casts unless receipted;
2. warn/collect narrowing numeric casts first;
3. prefer TryFrom, named truncation helpers, or domain-specific saturating helpers for intentional numeric boundaries.

Relationship to existing gates

This should complement, not replace, the bvisor unsafe ledger.

Possible migration path:

1. Keep traceability/unsafe_ledger.yaml as the specialized bvisor basement control.
2. Add compiler_assumption_ledger.yaml for non-basement assumptions.
3. Optionally later unify the two ledgers under one schema once the new gate proves stable.

Acceptance criteria

• New integrity subcommand or structural-check arm reconciles compiler-assumption sites fail-closed.
• Each live receipted site requires a stable comment anchor immediately above the hazardous site, similar to LEDGER:<id>.
• Gate fails for:
  • unanchored hazardous site;
  • duplicate anchor;
  • unregistered anchored site;
  • stale ledger entry;
  • malformed ledger entry;
  • ledger entry outside allowed source roots unless explicitly whitelisted.
• Detector is AST-based for Rust syntax hazards where feasible.
• Existing known legitimate sites are either moved into the new ledger or explicitly proven out of scope.
• Red-fixture tests prove the gate catches at least:
  • planted transmute;
  • planted unsafe fn outside sanctioned coverage;
  • planted unsafe impl;
  • planted raw pointer cast;
  • stale ledger entry;
  • duplicated anchor.

Non-goals

• Do not turn BatPak into “no unsafe ever” theater.
• Do not force every harmless widening cast into paperwork.
• Do not rely on comments alone. The comment is the anchor; the ledger plus gate is the law.

BatPak flavor

Danger may enter, but it signs the ledger, empties its pockets, and sits under fluorescent lights.

[heyoub]

Rust 1.97 qualification tie-in

#183 should use this ledger issue as the owner for one specific compatibility audit: Rust 1.97 changed encoding choices for some ordinary enums whose layout was never guaranteed.

That does not mean ordinary enums are unsafe or need paperwork. It means the detector/audit should specifically look for places where an un-repr(...) enum is treated as any of:

• wire/storage representation;
• FFI ABI;
• raw bytes or mapped layout;
• integer/discriminant identity outside normal Rust matching;
• hash/content identity derived from memory representation.

Any real site belongs in this ledger or should be rewritten through explicit canonical encoding. A clean audit result is valid evidence too.

Keep edition-2024 unsafe_op_in_unsafe_fn migration out of #183; that is a separate edition decision. No new crate is needed for either side.