Module auto_trait 

Checkers for the Send/Sync marker-trait predicates.

These are intentionally structural/behavioural approximations (sound-incomplete): a full proof of “exclusive ownership” / “no cross-thread aliasing” needs an ownership + concurrency model (e.g. separation logic), which the current sequential VM does not have.

The vocabulary follows the Rust model: a raw pointer is !Send unless tamed — either the type has no raw pointers at all ([NoRawPtr]), or its raw-pointer field is Allocated/Owning (discharged via the struct’s #[rapx::invariant] annotations) and updated read-only ([NoInternalMut]), exclusively ([UniInternalMut]), or under synchronization / atomically ([AtomicUpdate]). The composition is declared in std-trait-ensures.json + std-compound-properties.rs; this module only implements the primitive type-level checks.

Enums

Contains 🔒

Three-valued structural verdict: a type definitely contains a negative (Yes), definitely does not (No), or contains an unresolved generic parameter so the answer is unknown (Maybe).

Functions

atomic_update_check 🔒

Type-level AtomicUpdate obligation check (no VM state required): Proved when aliased updates of the type’s raw pointers are safe without exclusive ownership. Two ways satisfy this:

contain_no_type_check 🔒

Type-level ContainNoType obligation check (no VM state required): returns Failed if ty structurally contains any named negative, Unknown if a generic parameter makes the answer unresolved, else Proved.

field_invariant_check 🔒

Type-level Allocated(ptr, T, n) / Owning(ptr) obligation check (no VM state required): Proved when T declares a matching #[rapx::invariant(Allocated(ptr))] / #[rapx::invariant(Owning(ptr))] annotation (optionally restricted to the field named in the property) and the already-run struct-invariant verification discharged it. invariant_results carries the per-struct verdict; when a struct’s invariants failed to verify, the check fails too.

find_raw_ptr 🔒

Structurally check whether ty (transitively) contains a raw pointer. A raw pointer may also appear as a pattern type (pattern_type!(*const T is ..)), so recurse into TyKind::Pat.

find_unsynchronized_mutation 🔒

Find an interior-mutability / raw-pointer field that is not guarded by a synchronization primitive. A raw pointer may also appear as a pattern type (pattern_type!(*const T is ..)), so recurse into TyKind::Pat.

has_atomic_ptr_updates 🔒

Whether any inherent method of ty performs an atomic update through an atomic intrinsic or an Atomic* method (fetch_add/store/…), e.g. an Arc-style fetch_add on a reference count reached via a raw pointer.

has_raw_ptr_writes 🔒

Whether any inherent method of ty writes through a raw pointer.

no_internal_mut_check 🔒

Type-level NoInternalMut obligation check (no VM state required): Failed if any inherent method writes through a raw pointer — either a plain *ptr = ... write or an atomic update (Atomic* intrinsic).

no_raw_ptr_check 🔒

Type-level NoRawPtr obligation check (no VM state required).

param_bound_is_satisfied 🔒

Whether a generic type parameter carries a Send/Sync bound on the impl, letting the checker treat it as satisfied instead of Unknown.

ref_send_check 🔒

Type-level RefSend obligation check (no VM state required).

type_implements_clone 🔒

Whether ty implements Clone (which copies any raw-pointer field, aliasing the pointee across a move).

type_structurally_contains 🔒

Structurally check whether ty (transitively) contains one of the negative types identified by negative_defs. A synchronization primitive (Mutex/ RwLock/Atomic*) guards its interior, so the scan stops there — a negative type nested inside one (e.g. Mutex<UnsafeCell>) is considered tamed.

uni_internal_mut_check 🔒

Type-level UniInternalMut obligation check (no VM state required): Proved if the type writes through a raw pointer (plain or atomic) but does not implement Clone (which would copy the pointer and alias the pointee).