Module compound 

User-defined compound-contract layer.

Users (downloading a prebuilt rapx binary) can define new named safety contracts as boolean combinations of the primitive safety properties, and reference them from #[rapx::requires(MyTag(...))] — without recompiling rapx.

A compound property is a DNF macro over primitive property calls:

MySafeRead(p: Ptr, T: Ty, n: Expr) {
    NonNull(p) && Align(p, T) && Allocated(p, T, n)
}

StrOrBytes(s: Ptr, T: Ty, n: Expr) {
    ValidCStr(s, n) || (Allocated(s, T, n) && Init(s, T, n))
}

The DSL only composes existing primitives; it cannot invent new primitive semantics (those live in property_checker.rs). Expansion is a pure front-end that produces ordinary Property values consumed by the existing checker.

Structs

CompoundSpec 🔒

A parsed compound-property declaration.

Subst 🔒

Substitute compound formal parameters with the concrete call-site arguments inside a literal expression (e.g. turn size_of(T) * n into size_of(u32) * len, or p.unwrap_some() into head.unwrap_some()).

Enums

CompoundArg 🔒

A single argument in a compound body: a reference to a formal parameter, or a literal (kept as source text, re-parsed as syn::Expr at expansion time).

CompoundBody 🔒

The body of a compound property: a boolean tree over primitive-property calls (Call leaves), freely nested via And/Or. The DSL &&/|| grammar permits arbitrary nesting (an And may contain an Or and vice versa), so this is not constrained to DNF; expand_compound_body recurses over whatever shape was parsed.

Functions

builtin_compounds 🔒

Builtin compounds shipped with rapx: the standard compound safety properties (std-compound-properties.rs) plus user extensions (user-compound-properties.rs).

builtin_compounds_map 🔒

Cached, shared builtin compound map (see builtin_compounds).

builtin_subsumptions_map 🔒

Cached builtin subsumption map (see subsumption_closure).

collect_compound_refs 🔒

compound_param_ty_matches_arg_kind 🔒

Whether a compound parameter annotation matches a primitive argument role.

compound_refs 🔒

Collect the tag names referenced by a CompoundBody, in left-to-right order.

expand_compound 🔒

Expand a named compound against concrete argument expressions.

expand_compound_body 🔒

Expand a CompoundBody into the property list it denotes.

extract_def_property_string 🔒

Extract the string literal from a #[rapx::def_property("compound ...")] attribute’s textual representation.

find_compound 🔒

Look up a compound property by name, in the given crate’s namespace first, then the builtin namespace.

find_compound_cycle 🔒

Return a cycle path (e.g. ["A", "B", "A"]) if expanding start can reach itself again through compound-to-compound references, None otherwise.

find_cycle_in 🔒

flatten_subsumption_body 🔒

Flatten a subsumption body (a pure conjunction of primitive calls) into a list of (tag, args) pairs.

is_def_property_attr 🔒

Whether an attribute path is rapx::def_property (or the bare form with the tool prefix stripped).

parse_compounds 🔒

Parse a source fragment containing block-shaped contract definitions (Name(params) { body }) into a list of CompoundSpecs.

parse_equation_params 🔒

parse_one_compound_block 🔒

Parse a single leading Name(p: Ptr, T: Ty, ...) { body } block from s. Returns the CompoundSpec (without doc) and the number of bytes consumed through the closing }.

register_compound_properties 🔒

Scan the local crate for #[rapx::def_property("...")] tool attributes (emitted by the rapx_macros::pred proc-macro) and register each embedded compound-property string. Returns the number of compounds registered.

register_compounds_from_source 🔒

Parse compound-property declarations from source and insert them into the given crate’s namespace. Returns the number of compounds registered.

render_expr_src 🔒

Render a syn::Expr back to source-like text. proc_macro2 stringifies tokens space-separated (self . 0, size_of (T)), so collapse the spaces around punctuation for a readable form.

resolve_arg_string 🔒

Resolve a call-site argument expression to its display form, following the compound parameter’s declared role so internal placeholders (e.g. Arg_0 from a JSON contract) render as the actual parameter name.

resolve_subsumption_args 🔒

Resolve a subsumption body’s (tag, args) — whose args are Param(i) indices into atom’s own arguments — into concrete PropertyArgs.

subsumption_closure 🔒

Apply the builtin subsumption rules to an asserted fact: a stronger primitive also asserts its weaker consequences — a one-way weakening, unlike the ≡ compound equivalences above. The rules are declared declaratively in std-subsumption.rs with the same Name(params) { body } syntax; the head is an existing primitive tag and the body a pure conjunction of weaker primitive calls whose parameters map positionally to the head’s arguments (e.g. Init(p, T, n) ⇒ Typed(p, T)). Pointer-validity primitives (NonNull/Allocated/InBound) are deliberately not implied: they are orthogonal requirements stated explicitly by contracts.

unknown_property 🔒

user_compounds_map 🔒

Per-crate user compounds, registered from #[rapx::def_property] attributes.