Unsafe and Raw Pointers

What unsafe Means

An unsafe operation is an operation whose safety depends on facts that ordinary static analysis cannot completely establish at that source location.

Examples include:

• raw-pointer dereference;
• raw-pointer write;
• raw-pointer arithmetic;
• raw-to-safe reference construction;
• slice construction from raw parts;
• calling an unsafe fn;
• calling an unsafe foreign function;
• inline assembly;
• unchecked representation construction;
• unchecked enum or union construction;
• interpreting an unverified numeric address;
• adopting ownership from raw or foreign storage.

The explicit unsafe marker records that the remaining proof obligations have been reviewed outside ordinary compiler proof.

What unsafe Does Not Disable

The compiler continues every analysis that remains applicable.

unsafe does not mean:

• stop type checking;
• stop ownership checking;
• stop borrow checking;
• stop lifetime analysis;
• stop effect analysis;
• ignore moves or invalidation;
• ignore cleanup rules;
• ignore target or platform rules;
• permit arbitrary backend undefined behavior.

If the compiler can prove an unsafe obligation false, the operation is rejected even when it is written inside an unsafe context.

// Conceptual example:
// if the compiler proves that `pointer` is null here,
// unsafe does not make this read legal.

let value := unsafe pointer.Read()

Unsafe Operations Are Operation-Specific

The language does not have one universal “trust everything in this file” mode.

Each compiler-known unsafe operation has its own required obligations. For example, a raw read may require:

• non-null address;
• correct alignment;
• readable storage;
• a valid initialized representation;
• sufficient lifetime;
• compatible aliasing;
• correct address space;
• permission under the active platform contract.

An unrelated unsafe operation may have a different set of obligations.

Single-Operation unsafe

A single unsafe expression can be marked directly:

let value := unsafe pointer.Read()

A single unsafe statement can also be marked directly:

unsafe pointer.Write(value)

This is the narrowest form and is preferred when only one operation requires trust.

unsafe Blocks

Several related operations may be grouped into an unsafe block:

let value := unsafe {
    Validate(pointer)
    pointer.Read()
}

The block follows ordinary Sec block and evaluation rules.

Safe operations inside the block remain ordinary safe operations. The block does not remove their normal checks.

Unsafe Blocks Can Produce Values

Because the block follows normal block-expression semantics, it may produce a value:

let result := unsafe {
    Prepare(pointer)
    pointer.Read()
}

The resulting type is determined by the ordinary block-expression rules.

unsafe does not create a special “unsafe value” type.

Unsafe Scope Is Lexically Explicit

The marker applies only to the operation or block it introduces.

unsafe {
    pointer.Write(value)
}

pointer.Write(value)    // still requires unsafe here

A parent scope does not become implicitly unsafe.

Nested unsafe contexts are permitted, although tooling may report a nested marker as redundant when it adds no useful boundary clarity.

Empty and Redundant Unsafe Contexts

An empty unsafe block is valid syntax:

unsafe {
}

An unsafe context containing no operation that requires unsafe is also valid.

By default, these cases should produce informational diagnostics rather than hard errors.

Project policy may promote redundant-unsafe diagnostics to warnings.

unsafe fn

An unsafe function or method exposes proof obligations to its caller:

unsafe fn FromRawParts(
    pointer: RawPtr[byte],
    length: int,
) Buffer {
    // ...
}

Calling it requires an unsafe context:

let buffer := unsafe Buffer.FromRawParts(pointer, length)

Unsafe status is part of the callable safety contract.

It is not the same thing as panic behavior, allocation behavior, blocking behavior or any other effect.

The Body of unsafe fn Is Still Explicit

Declaring a function unsafe does not make its body implicitly unsafe.

unsafe fn ReadRaw(pointer: RawPtr[byte]) byte {
    return unsafe pointer.Read()
}

Each actual unsafe operation remains marked.

This keeps the exact implementation trust boundary visible during review.

An unsafe fn may contain only safe operations when the caller obligation exists for contractual reasons.

Caller Proof Obligations

Every unsafe callable must define what the caller promises.

Obligations may include:

• pointer is non-null;
• pointer is correctly aligned;
• address range is valid;
• storage remains live for the required lifetime;
• storage contains initialized valid representation;
• mutable access is exclusive;
• no conflicting aliases exist;
• the allocator/deallocator pair is correct;
• address space is valid;
• hardware context is valid;
• foreign ABI is correct;
• callback or thread affinity is satisfied;
• concurrent invalidation cannot occur;
• length/capacity relationships are valid.

The compiler may prove some obligations itself. Only the remaining unproven obligations are accepted by the explicit unsafe boundary.

A compiler-proven contradiction remains an error.

Safety Documentation

Public unsafe APIs should document their caller obligations.

Sec 0.1 treats this as strongly recommended rather than a universal hard language requirement.

Project or tooling policy may require safety documentation for exported unsafe APIs.

Compiler-known unsafe operations must not rely solely on comments: their obligations must also exist in compiler-readable metadata.

Safe Wrappers

A safe function may use unsafe operations internally when it establishes every obligation before crossing the boundary.

Conceptually:

fn CreateBuffer(
    pointer: RawPtr[byte],
    length: int,
) Result[Buffer, BufferError] {
    if length < 0 {
        return Err(BufferError.InvalidLength)
    }

    // Additional pointer/storage validation belongs here.

    let buffer := unsafe Buffer.FromRawParts(pointer, length)
    return Ok(buffer)
}

A safe wrapper must not leave hidden obligations that the safe API cannot express or enforce.

Recoverable validation failure should use normal Sec error handling where appropriate.

Trust Provenance

Encapsulating an unsafe operation in a safe wrapper removes the caller's unsafe obligation only when the wrapper discharges it.

It does not erase the fact that the implementation ultimately depends on trusted behavior.

The compiler/tooling may retain facts such as:

caller-facing safety: safe
implementation provenance: depends on unsafe foreign call

Trust provenance is useful for:

• security audits;
• whole-program trust reports;
• ISR analysis;
• LSP navigation;
• certification profiles;
• invalidating assumptions when a platform or FFI contract changes.

Effects Remain Active Inside Unsafe Code

Unsafe status and effect analysis are independent semantic dimensions.

An unsafe operation may still carry effects such as:

MayPanic
MayAllocate
MayBlock
MaySuspend
MaySpawn
MayIO
MayAccessVolatile
MayMutateExternalState
MayUseNondeterministicInput

Therefore @noPanic, @noAlloc, @noBlock, ISR restrictions and other verified contracts continue to apply.

Unsafe Does Not Suppress Panic Rules

Panic-capable code does not become compatible with a no-panic context merely because it appears inside unsafe.

Trusted foreign no-panic claims are accepted only when the foreign contract explicitly provides that fact.

Cleanup code that must remain panic-free remains subject to its normal no-panic restrictions.

Unsafe Does Not Authorize Hidden Allocation

Raw-pointer conversion, raw-to-safe reference construction, ownership adoption and escaping lifetime relationships do not gain permission to allocate merely because the code is unsafe.

Allocation-capable unsafe operations retain their ordinary allocation effects.

@noAlloc and ISR allocation restrictions remain enforced.

Unsafe Does Not Authorize Blocking or Suspension

An unsafe foreign, assembly or platform operation that may block or suspend must publish that effect or be treated conservatively.

An ISR cannot call a blocking operation merely by wrapping the call in unsafe.

RawPtr[T]

RawPtr[T] is Sec's unchecked typed raw-address value.

let address: RawPtr[byte]
let itemAddress: RawPtr[Item]

A raw pointer is not a safe reference.

It does not inherently carry:

• non-nullness;
• lifetime;
• ownership;
• destruction responsibility;
• bounds;
• borrow authority;
• exclusive access;
• generation validity;
• hardware privilege;
• proof that the address contains a valid T.

RawPtr[void]

RawPtr[void] represents an untyped raw address:

let handle: RawPtr[void]

It does not directly support typed:

• Read();
• Write(value);
• VolatileRead();
• VolatileWrite(value);
• Offset(elements).

A concrete compatible raw-pointer interpretation must first be established under the applicable conversion and unsafe rules.

Raw Pointers Are Ordinary Address Values

RawPtr[T] itself is copyable.

let first: RawPtr[byte] := pointer
let second := first

Copying the pointer copies the raw address value. It does not copy, retain, borrow, own or move the pointee.

Moving a raw-pointer holder moves only that raw-pointer value. It does not move the memory addressed by the pointer.

Destroying a raw-pointer value never destroys or deallocates its pointee.

Operations on Raw Pointer Values That Are Not Inherently Unsafe

Merely handling a raw address as a value does not require unsafe.

Examples include:

• storing a raw pointer;
• copying it;
• moving it;
• returning it;
• passing it through a compatible FFI boundary;
• comparing compatible raw pointers for equality;
• testing raw-pointer null state under the canonical raw/FFI rules;
• formatting or inspecting an address for diagnostics where permitted;
• representation-compatible raw-pointer conversion explicitly defined as safe.

None of these operations asserts that the pointee is valid.

Raw-Pointer Operations That Require Unsafe

Unless a specialized compiler-verified adapter says otherwise, unsafe is required for:

• Read();
• Write(value);
• VolatileRead();
• VolatileWrite(value);
• pointer arithmetic;
• integer-to-raw-pointer conversion;
• constructing ref T from raw storage;
• constructing ref mut T from raw storage;
• constructing a slice/view from raw pointer plus extent;
• assuming alignment;
• assuming initialized representation;
• adopting ownership from a raw address;
• constructing a callable function pointer from a raw address;
• reinterpreting unrelated pointer representations without compiler proof.

Null Is Part of the Raw-Pointer Value Domain

Every RawPtr[T] may represent a null address.

A raw pointer may become null through:

• a foreign return;
• an unsafe conversion;
• a platform operation;
• an allocator or operating-system operation;
• another raw-pointer-producing operation.

Storing, moving, returning, passing, comparing or testing a null raw pointer is permitted when the surrounding operation is otherwise valid.

Dereferencing null is invalid.

Safe references remain non-null. Safe APIs should normally translate nullable foreign outcomes into explicit Option, Result or validated wrapper types.

Raw-Pointer Construction Is Explicit

A RawPtr[T] may originate from:

• a foreign function result;
• an explicit unsafe safe-reference conversion;
• an explicit unsafe integer/address conversion;
• a platform or hardware address primitive;
• an allocator/runtime primitive;
• another compatible raw-pointer conversion.

A raw pointer is never created implicitly from:

• a safe reference;
• an integer;
• an owning collection;
• a string;
• a slice;
• an unrelated pointer representation.

The exact source syntax for general RawPtr ↔ ref/ref mut conversion is intentionally not specified here because that spelling is not yet canonically locked.

Raw-Pointer Read

Canonical typed raw read:

let value := unsafe pointer.Read()

For pointer: RawPtr[T], Read() produces a T.

Before reading, the accepted proof obligations include at least:

• the pointer is non-null;
• the address is aligned for T;
• the address is readable in the active address space;
• storage covers at least one T;
• the storage contains a valid initialized T representation;
• the storage remains live for the complete read;
• ownership/aliasing rules permit the access;
• the target/platform policy permits the read.

Reading does not create ownership of the pointee merely because a T value is produced.

RawPtr[void].Read() is invalid.

Raw-Pointer Write

Canonical typed raw write:

unsafe pointer.Write(value)

Before writing, the accepted obligations include at least:

• the pointer is non-null;
• the address is aligned for T;
• the address is writable in the active address space;
• storage covers at least one T;
• the incoming representation is valid;
• required mutable/exclusive authority exists;
• no conflicting safe reference or foreign access violates the contract;
• the write does not bypass required destruction of a live object;
• the target/platform policy permits the write.

Write() does not grant ownership of destination storage.

It also must not silently overwrite a live non-trivial object while bypassing its required lifecycle semantics.

Volatile Raw-Pointer Access

Volatile access uses separate compiler-known operations:

let value := unsafe pointer.VolatileRead()

unsafe pointer.VolatileWrite(value)

Volatile access is distinct from ordinary Read() and Write().

It does not:

• make RawPtr[T] a volatile-qualified type;
• create ownership;
• establish synchronization;
• grant hardware privilege;
• establish mapping authority;
• establish DMA ownership;
• establish cache coherence;
• provide atomicity.

Exact volatile access width and ordering are defined by the platform/volatile rules.

Raw-Pointer Arithmetic

Pointer arithmetic requires unsafe.

Sec does not use ordinary numeric pointer arithmetic:

pointer + 1       // invalid raw-pointer arithmetic
pointer - 1       // invalid raw-pointer arithmetic
pointer++         // invalid
pointer--         // invalid

Canonical operations are:

pointer.Offset(elements)
pointer.AddBytes(bytes)
pointer.Difference(other)

These operations compute raw addresses only. They do not establish that the result is dereferenceable.

Offset(elements)

Offset(elements: int) computes an address offset measured in elements of the pointee type.

let next := unsafe pointer.Offset(1)

The byte scaling depends on the selected target layout for T.

Offset() is invalid for RawPtr[void].

The operation does not prove that the result remains within the same allocation, mapped region, hardware window or live object.

AddBytes(bytes)

Byte-oriented pointer arithmetic uses RawPtr[byte]:

let next := unsafe bytes.AddBytes(offset)

This keeps byte arithmetic explicit instead of silently reinterpreting element sizes.

AddBytes() is defined for RawPtr[byte].

Difference(other)

Two compatible raw pointers with the same element type may compute an element difference:

let distance := unsafe end.Difference(begin)

The result is an int where the operation is valid for the selected target and address domain.

Difference does not create a safe range and does not prove common allocation origin.

Raw-Pointer Comparison

Compatible raw pointers may be compared for equality.

Equality compares raw address identity according to the selected target representation.

Equality does not prove that either pointer is:

• non-null;
• live;
• aligned;
• dereferenceable;
• owned;
• within the same allocation.

Raw-pointer equality is different from safe-reference equality, which may include live storage identity and generation semantics.

Ordering comparisons are not generally meaningful unless a target-specific API defines them.

Integer and Address Conversion

Interpreting an arbitrary integer as a raw pointer requires unsafe.

Converting a raw pointer to a target-sized unsigned integer representation requires the applicable explicit low-level conversion.

Such conversion proves no storage validity.

The compiler must respect:

• selected target pointer width;
• address-space representation;
• capability/tag requirements;
• non-flat pointer models;
• overflow and truncation rules.

The implementation must never use the compiler host's pointer width as a substitute for the selected target's pointer model.

Safe Reference to Raw Pointer

Converting ref T or ref mut T into raw-address semantics crosses out of the safe-reference model and requires unsafe unless a specialized compiler-verified adapter defines the operation as safe.

The resulting raw pointer does not keep the referenced value alive.

It also does not preserve safe-reference guarantees after the source reference or source storage lifetime ends.

Raw-pointer use cannot be used to evade an active borrow conflict and later recreate a conflicting safe reference.

The exact source syntax for this conversion is intentionally not specified until the canonical conversion grammar is locked.

Raw Pointer to Safe Reference

Constructing ref T from raw storage requires unsafe unless a trusted adapter proves the complete contract.

A shared safe reference requires at least:

• non-null address;
• correct alignment;
• valid initialized T;
• readable storage;
• lifetime covering the reference;
• canonical provenance;
• no conflicting mutable access;
• foreign/hardware mutation compatible with shared semantics;
• address-space/platform compatibility.

Constructing ref mut T additionally requires writable storage and exclusive mutable authority for the complete borrow live range.

The exact source spelling for raw-to-safe conversion is intentionally not invented by this manual until the language grammar is canonically locked.

Slice Construction from Raw Parts

Constructing a safe slice or view from a raw pointer plus extent is unsafe unless a trusted wrapper establishes the complete slice contract.

Required facts include:

• valid range;
• nonnegative and representable extent;
• no length × element-size overflow;
• correct alignment;
• initialized element representations;
• sufficient storage lifetime;
• compatible aliasing and mutability;
• one compatible storage region where required;
• valid target address space.

Constructing a slice from raw parts must not allocate merely to make the conversion work.

A zero-length slice does not justify fabricating an arbitrary valid scalar safe reference.

Unchecked Representation Construction

Constructing a typed value directly from raw bits or raw storage without ordinary constructors is unsafe unless a compiler-verified representation operation proves validity.

Unsafe does not make every bit pattern a valid Sec value.

Validity obligations may include:

• enum discriminant validity;
• union active variant;
• bool validity;
• rune validity;
• named-type contracts;
• reference invariants;
• ownership state;
• alignment;
• padding rules;
• FFI layout.

A compiler-proven invalid representation is rejected even inside unsafe.

Ownership Adoption from Raw or Foreign Storage

Turning a raw/foreign resource into an owned Sec resource is unsafe unless a safe wrapper proves the complete ownership contract.

Obligations include:

• correct allocator or provider;
• matching reclamation operation;
• correct extent and alignment;
• uniqueness where exclusive ownership is required;
• initialized object state;
• destruction responsibility;
• foreign lifetime and retention rules.

Numeric address alone never proves ownership.

Double adoption of the same exclusive resource is invalid.

Unsafe does not permit double destruction or double free.

Releasing Ownership to Foreign Code

Passing a raw address to foreign code does not by itself transfer Sec ownership.

Ownership transfer across FFI requires an explicit foreign ownership contract.

After a committed consuming foreign transfer, the Sec source Place becomes unavailable under the ordinary ownership rules.

Failure and non-commit behavior must be specified by the foreign wrapper contract.

Unsafe Does Not Disable Borrow Checking

Safe references continue to follow normal borrow rules inside unsafe code.

Raw aliases may exist outside the safe-reference borrow model, but using them in a way that violates a live safe-reference guarantee is invalid.

Reconstructing a safe reference from raw storage must re-establish borrow compatibility.

Known overlap or alias conflict is rejected.

Unsafe Does Not Extend Lifetime

A raw pointer may physically outlive the storage it once addressed.

That does not make dereference after storage lifetime end valid.

Safe wrappers must not return references that depend on ended local storage.

Unsafe also does not trigger hidden heap or Arena promotion to repair an invalid lifetime.

A known use-after-domain-end is rejected even inside unsafe code.

Unsafe Does Not Disable Destruction Rules

Deterministic destruction remains active.

A raw write must not overwrite a live non-trivial object while silently bypassing required destruction unless a dedicated low-level replacement/adoption contract proves that lifecycle transition.

Unsafe operations inside defer, free or another cleanup body remain explicitly marked where such operations are otherwise permitted.

Unsafe does not make panic-capable required cleanup legal.

Unsafe Does Not Legalize Concurrency Violations

unsafe does not:

• make a non-transferable value transferable;
• legalize a data race;
• waive thread affinity;
• waive task-migration restrictions;
• waive process-boundary rules;
• waive ISR restrictions;
• waive destruction-context restrictions.

Volatile access is not synchronization.

Foreign/raw concurrent access requires explicit synchronization and ownership contracts.

Address Spaces and Target Dependence

RawPtr[T] uses the selected target's pointer and address-space model.

The compiler must not assume:

• one flat address space;
• host pointer width;
• integer-only pointer representation;
• interchangeability of all address spaces.

A target may use tagged, capability or otherwise richer pointer representations.

A target may reject conversions between incompatible address spaces.

Hardware and Fixed Addresses

Hardware knowledge is not automatically unsafe merely because it refers to physical addresses.

Compiler/platform-verified fixed-address declarations may remain safe:

@address(Platform.GPIOA)
let mut gpio: GpioRegisters

Raw numeric address interpretation requires unsafe when the compiler cannot prove the complete storage/access contract.

Raw-pointer MMIO access remains subject to:

• exact access width;
• volatile ordering;
• mapping validity;
• device availability;
• privilege rules;
• ISR restrictions.

Hardware signal polarity remains application/driver semantics.

Runtime Mappings

Creating and destroying mapped regions follows the platform mapping/resource model.

Unsafe access through a raw pointer into a mapping still requires:

• mapping lifetime;
• valid extent;
• correct address space;
• appropriate access mode.

A raw pointer does not keep the mapping alive.

Remap or unmap may invalidate both raw and safe views.

Safe mapping wrappers may encapsulate the raw platform operations when they preserve the complete contract.

Interrupt Contexts

Unsafe code reachable from an ISR remains subject to all interrupt safety restrictions.

unsafe does not waive:

• @isr or @interruptSafe requirements;
• no-panic rules;
• no-allocation rules;
• no-blocking rules;
• bounded-work requirements;
• synchronization requirements;
• hardware-access restrictions.

Named compiler-known interrupt vectors may be safe when the platform contract verifies them. Raw numeric vector/address interpretation may require an unsafe trust boundary.

Unsafe and the FFI Boundary

Foreign code is a trust boundary because Sec cannot verify its implementation.

A useful FFI contract may need to define:

• ABI and linkage;
• nullability;
• ownership transfer;
• borrowing and retention;
• lifetime;
• thread/callback affinity;
• allocation and deallocation;
• panic/abort/unwind behavior;
• blocking or suspension;
• I/O and external mutation;
• layout, alignment and extent.

Unknown foreign behavior is treated conservatively where proof is required.

The next chapter covers FFI declarations and contracts in detail.

unsafe extern

Unsafe foreign functions combine separate safety and ABI/linkage concepts:

unsafe extern "system" fn rawSysCall(
    number: int,
    argument1: uint64,
) int64

Here:

• unsafe defines caller proof obligations;
• extern "system" defines foreign linkage/ABI selection;
• fn declares the callable.

Calling an unsafe extern function requires an unsafe context:

let result := unsafe rawSysCall(number, argument)

The marker does not prove that the arguments, pointers, ownership or ABI declaration are correct.

Inline Assembly

Inline assembly is an unsafe operation and trust boundary.

Exact assembly syntax belongs to the inline-assembly rules, but the assembly contract must describe enough behavior for compiler correctness.

Relevant facts include:

• register inputs and outputs;
• clobbers;
• memory reads and writes;
• volatile behavior;
• control flow;
• stack behavior;
• possible trap or abort;
• blocking;
• I/O;
• external mutation.

Assembly effects remain active inside unsafe.

Unsafe Function Values

Unsafe status is part of callable compatibility.

An unsafe function cannot implicitly become a safe function value.

Calling through an unsafe function value requires unsafe context.

A safe wrapper may produce a safe callable only after discharging the caller obligations.

Effects and trust provenance remain attached to the callable target set.

Unsafe and Interfaces

Interface method safety contracts are preserved by implementations.

A safe interface method cannot be implemented by a callable that requires additional unsafe caller obligations.

An unsafe interface method may have an internally safe implementation while remaining unsafe to call through the interface contract.

Dynamic dispatch must not erase unsafe status.

Unsafe and Generics

Generic code preserves the unsafe requirements of operations on concrete instantiated types and callable values.

A generic constraint must not assume an operation is safe when the callable safety contract is unknown.

Specialization may prove a previously unnecessary unsafe boundary redundant only when canonical semantics permit that conclusion.

Trust provenance from generic dependencies remains available to analysis and tooling.

Closures and Raw Pointers

A closure may capture a RawPtr[T] as an ordinary copyable address value.

That does not make later pointer interpretation safe.

Dereferencing the captured raw pointer still requires explicit unsafe context and complete validity obligations at the use site.

Closure lifetime and transferability rules remain active normally.

Compile-Time Evaluation

Ordinary compile-time evaluation rejects unsafe operations.

The compiler does not normally execute operations such as:

• raw-pointer dereference;
• foreign calls;
• inline assembly;
• addressed-storage access;
• raw target-memory access;
• unsafe ownership adoption.

A compiler-known intrinsic may be compile-time evaluable only when explicitly defined as such.

Writing an unsafe context does not force or authorize compile-time execution.

Unsafe Is Not a General Backend-UB Switch

Sec should minimize backend undefined behavior even for unsafe operations.

Where practical, unsafe operations should lower to:

• defined target instructions;
• explicit traps;
• validated intrinsics;
• well-specified foreign ABI operations;
• carefully bounded backend assumptions.

Backend assumptions must never be stronger than the obligations or trusted facts accepted at the Sec/Semantic IR boundary.

When violating an unsafe obligation necessarily violates backend assumptions, tooling and documentation should describe that risk accurately.

Unsafe Requires No Mandatory Runtime

Unsafe is primarily a compile-time language and analysis feature.

It requires no mandatory:

• runtime unsafe flag;
• dynamic trust checker;
• pointer metadata;
• provenance object;
• generational reference representation;
• exception machinery;
• general Sec runtime.

A selected target profile may independently use runtime checks for other safety models.

Trust metadata may be erased from release binaries when the selected tooling or certification profile does not require it.

Diagnostics

Unsafe diagnostics should distinguish a missing unsafe context from an operation that is already known to be invalid.

Missing unsafe context

raw-pointer read requires an unsafe context

    pointer.Read()

help: write `unsafe pointer.Read()` when the required safety obligations are established

Known invalid operation

this raw-pointer read is known to use a null address

`unsafe` can accept obligations that the compiler cannot prove,
but it does not make a proven null dereference valid

help: validate the raw pointer before reading it

Unsafe function body remains explicit

raw-pointer dereference still requires an explicit unsafe operation

this function is declared `unsafe fn`, but its body is not implicitly unsafe

help: mark the exact operation:
    return unsafe pointer.Read()

Important diagnostic categories include:

• missing unsafe context;
• unnecessary or redundant unsafe;
• unsafe callable invoked outside context;
• interface/function-value safety mismatch;
• unknown generic callable safety;
• unknown foreign ownership or effects;
• known raw-pointer null;
• known alignment violation;
• known lifetime violation;
• known alias conflict;
• invalid raw-pointer range;
• uninitialized read;
• invalid representation;
• unverified target address;
• unsafe cleanup effect;
• compile-time-forbidden unsafe operation.

Formatter, LSP and Analysis

The formatter preserves canonical forms:

let value := unsafe pointer.Read()

unsafe pointer.Write(value)

let result := unsafe {
    Prepare(pointer)
    pointer.Read()
}

unsafe fn FromRawParts(...) Buffer {
}

unsafe extern "system" fn rawSysCall(number: int) int64

The formatter must not invent:

• C-style pointer syntax;
• unsafe struct;
• unsafe type;
• unlocked raw/reference conversion syntax.

LSP and analysis tooling may expose:

• unsafe operation identity;
• caller obligations;
• unsafe callable status;
• foreign trust facts;
• effects;
• trust provenance;
• nearest unsafe context;
• safe-wrapper boundary;
• raw address-space/null/alignment/range facts;
• safe alternatives where available.

Tooling must never imply that wrapping a compiler-proven-invalid operation in unsafe will fix the program.

Best Practices

• Keep unsafe regions as narrow as practical.
• Prefer single-operation unsafe when one operation carries the trust boundary.
• Document the exact caller obligations of public unsafe fn APIs.
• Build small safe wrappers that validate all obligations before entering unsafe code.
• Do not use unsafe as a way to bypass ownership, borrowing or lifetime errors.
• Use RawPtr[T] only when safe references or platform abstractions cannot express the required operation.
• Remember that a raw pointer does not keep storage alive.
• Remember that copying a raw pointer does not copy or own the pointee.
• Use Read/Write and volatile operations intentionally; they have different semantics.
• Use Offset, AddBytes and Difference rather than numeric pointer operators.
• Do not create safe references from raw storage until every reference guarantee is re-established.
• Do not infer ownership from an address.
• Prefer compiler/platform-known hardware bindings such as @address over unverified numeric addresses.
• Treat foreign code, inline assembly and unverified target facts as explicit trust boundaries.
• Keep effects such as panic, allocation, blocking and volatile I/O visible even inside unsafe code.

Summary

• unsafe permits operations whose complete safety obligations are not automatically proven.
• unsafe disables no compiler analysis.
• A compiler-proven false safety obligation is rejected even inside unsafe.
• Sec supports single-operation unsafe operation and block-form unsafe { ... }.
• Unsafe blocks follow normal block-expression result semantics.
• Unsafe scope is lexical and does not propagate to parent or sibling scopes.
• Empty or redundant unsafe contexts are valid and normally diagnosed informationally.
• Sec supports unsafe fn and unsafe methods.
• Calling an unsafe callable requires an unsafe context.
• The body of unsafe fn is not implicitly unsafe.
• Every actual unsafe operation inside an unsafe function remains explicitly marked.
• Unsafe callable contracts define caller proof obligations.
• Caller obligations may include non-nullness, alignment, lifetime, aliasing, ownership, address-space, ABI and concurrency facts.
• The compiler may prove some obligations and reject obligations known to be false.
• Public unsafe APIs should document their caller obligations.
• Compiler-known unsafe operations carry machine-readable obligation metadata.
• A safe wrapper may encapsulate unsafe code only after establishing every caller obligation.
• Unsafe does not transitively mark callers through a correct safe wrapper.
• Trust provenance may remain available internally even when the wrapper is caller-safe.
• Unsafe status and effects are separate semantic dimensions.
• Unsafe does not waive panic, allocation, blocking, suspension, volatile, I/O or external-mutation effects.
• @noPanic, @noAlloc, @noBlock and ISR restrictions remain active.
• Unsafe does not authorize hidden allocation.
• Unsafe does not authorize blocking or suspension in contexts that forbid them.
• RawPtr[T] is an unchecked typed address value.
• RawPtr[T] is not a safe reference.
• RawPtr[T] is copyable and non-owning.
• Copying or moving a raw-pointer value does not copy, move, retain or own its pointee.
• Destroying a raw pointer does not destroy or deallocate the pointee.
• RawPtr[void] represents an untyped raw address.
• RawPtr[void] cannot directly perform typed reads, writes, volatile access or element offsets.
• Storing, copying, moving, returning, passing, equality-testing and null-testing raw pointers are not inherently unsafe.
• Raw reads, writes, volatile access, pointer arithmetic, integer-address construction, raw-to-safe conversion, raw slice construction and ownership adoption require unsafe unless a specialized verified operation says otherwise.
• Null is part of the value domain of every RawPtr[T].
• Dereferencing a null raw pointer is invalid.
• Unsafe does not make a known null dereference valid.
• Safe references remain non-null.
• Raw-pointer construction from safe references, integers and unrelated pointer representations is never implicit.
• The exact source spelling for general RawPtr ↔ ref/ref mut conversion is intentionally not specified until canonically locked.
• pointer.Read() performs a typed raw read under explicit unsafe obligations.
• pointer.Write(value) performs a typed raw write under explicit unsafe obligations.
• Raw writes must not bypass required destruction of a live non-trivial object.
• VolatileRead() and VolatileWrite() are distinct from ordinary raw access.
• Volatile access does not imply synchronization, atomicity, ownership or hardware privilege.
• Raw-pointer arithmetic uses Offset, AddBytes and Difference.
• Ordinary numeric operators are not raw-pointer arithmetic.
• Offset scales by target sizeof(T) and is invalid for RawPtr[void].
• AddBytes is byte-oriented and defined for RawPtr[byte].
• Difference requires compatible same-element-type raw pointers.
• Pointer arithmetic does not prove bounds or common allocation identity.
• Raw-pointer equality compares raw address identity and does not imply dereferenceability.
• Raw-pointer equality is distinct from safe-reference identity.
• Integer/address conversion must use the selected target pointer representation, never compiler-host assumptions.
• A raw pointer derived from a safe reference does not keep the referent alive.
• Raw-to-safe reference construction must re-establish non-nullness, alignment, representation, lifetime, provenance and borrow authority.
• Constructing ref mut T from raw storage additionally requires writable storage and exclusive mutable authority.
• Constructing a safe slice from raw parts requires valid extent, alignment, initialization, lifetime, aliasing and address-space proof.
• Unsafe does not make every raw bit pattern a valid typed value.
• Unchecked enum/union/representation construction remains subject to type validity and lifecycle rules.
• Adopting ownership from raw or foreign storage requires the correct provider, reclamation, uniqueness, initialization and lifetime contract.
• Numeric address alone never proves ownership.
• Unsafe does not permit double adoption, double destruction or double free.
• Passing a raw pointer to foreign code does not by itself transfer ownership.
• Committed foreign ownership transfer makes the Sec source unavailable according to ordinary ownership rules.
• Unsafe does not disable safe-reference borrow checking.
• Raw aliases cannot be used to manufacture conflicting safe borrows.
• Unsafe does not extend storage, object or reference lifetime.
• Known use-after-lifetime-end remains invalid inside unsafe.
• Unsafe does not disable deterministic destruction.
• Unsafe does not legalize data races or waive thread/task/process/ISR restrictions.
• Raw-pointer address spaces and representation are selected-target facts.
• The compiler must not assume one flat address space or compiler-host pointer width.
• Compiler/platform-verified hardware addresses may be safe without raw numeric address interpretation.
• @address is not automatically an unsafe operation.
• Raw-pointer MMIO access remains subject to volatile, mapping, privilege and ISR rules.
• Raw pointers do not keep runtime mappings alive.
• Unsafe foreign functions use separate unsafe, extern "<abi>" and fn semantics.
• Foreign undefined behavior is not repaired by Sec's unsafe marker.
• Inline assembly is an unsafe trust boundary and must publish enough behavior for compiler correctness.
• Unsafe status is part of function-value and interface callable compatibility.
• Generic specialization preserves unsafe requirements.
• A closure may safely store a raw-pointer value while later dereference remains unsafe.
• Ordinary compile-time evaluation rejects unsafe operations unless a specific compiler-known intrinsic says otherwise.
• Unsafe is not permission for unrestricted backend undefined behavior.
• Unsafe requires no mandatory Sec runtime or dynamic borrow/trust machinery.