rapx/verify/contract/
spec.rs

1//! Declaration table mapping tag names to their property specs.
2//!
3//! This is the single source of truth for every safety tag `rapx` understands:
4//! its `PropertyKind`, the argument shapes it accepts (for variable-arity tags
5//! there is more than one form), its default `ContractKind`, and the assembly
6//! strategy used to build the final `Property` from raw `syn::Expr` arguments.
7//!
8//! `PropertyKind` orthogonalisation lives on `PropertyKind` in `types.rs`.
9
10use super::types::*;
11
12#[derive(Clone, Copy, Debug, PartialEq, Eq)]
13pub(crate) enum ArgKind { Target, Ty, Expr, Ident }
14
15/// How a tag's arguments are assembled into a `Property`.
16#[derive(Clone, Copy, Debug, PartialEq, Eq)]
17pub(crate) enum BuildKind {
18    /// Positional resolution over a matched `forms` entry (common case).
19    Uniform,
20    /// `Size(T, sized | unsized | const)` — second arg is an ident or a const.
21    Size,
22    /// `Allocated(target[, T, n[, allocator]])` — 1/3/4-argument forms.
23    Allocated,
24    /// `InBound(index | target,index | target,T,n)` — index + for_each variants.
25    InBound,
26    /// `NonOverlap(indices | a,b,T,count)` — 1/4-argument forms.
27    NonOverlap,
28    /// `ValidNum(predicate | value, interval)`.
29    ValidNum,
30    /// `Pinned(ptr, lifetime)` — lifetime is optional.
31    Pinned,
32    /// `SplitTransmute([T], [U])` — array element types.
33    SplitTransmute,
34    /// One-or-more target places (`Alias`, `Alive`).
35    Targets,
36    /// Placeholder accepting any args; always yields `Unknown`.
37    TobeSpecified,
38}
39
40pub(crate) struct PropertySpec {
41    pub tag: &'static str,
42    pub kind: PropertyKind,
43    /// Accepted argument shapes. For `BuildKind::Targets` the single entry is
44    /// a marker and the tag accepts one or more `Target` args.
45    pub forms: &'static [&'static [ArgKind]],
46    pub contract_kind: ContractKind,
47    pub build: BuildKind,
48    /// Human-readable explanation template, with `{0}`, `{1}`, `{2}`
49    /// placeholders bound to the rendered positional arguments.  This keeps the
50    /// display text co-located with the tag declaration instead of hardcoded in
51    /// the renderer.  A few argument-dependent kinds (`InBound`, `Size`,
52    /// `ValidNum`, `Alive`, `Allocated`, `NonOverlap`) override this template
53    /// structurally at render time.
54    pub meaning: &'static str,
55}
56
57const fn ps(
58    tag: &'static str,
59    kind: PropertyKind,
60    forms: &'static [&'static [ArgKind]],
61    contract_kind: ContractKind,
62    build: BuildKind,
63    meaning: &'static str,
64) -> PropertySpec {
65    PropertySpec { tag, kind, forms, contract_kind, build, meaning }
66}
67
68use ArgKind::{Expr, Ident, Target, Ty};
69
70// ── Table ────────────────────────────────────────────────────────────
71
72static SPECS: &[PropertySpec] = &[
73    // Uniform single-form primitives.
74    ps("NonNull",       PropertyKind::NonNull,       &[&[Target]],               ContractKind::Precond, BuildKind::Uniform, "{0} as usize != 0"),
75    ps("Owning",        PropertyKind::Owning,        &[&[Target]],               ContractKind::Precond, BuildKind::Uniform, "ownership(*{0}) = none: no live owner aliases the pointee"),
76    ps("Opened",        PropertyKind::Opened,        &[&[Target]],               ContractKind::Precond, BuildKind::Uniform, "{0} is a valid open file descriptor"),
77    ps("Unreachable",   PropertyKind::Unreachable,   &[&[]],                     ContractKind::Precond, BuildKind::Uniform, "not Reachable()"),
78    ps("Align",         PropertyKind::Align,         &[&[Target, Ty]],           ContractKind::Precond, BuildKind::Uniform, "({0} as usize) % align_of::<{1}>() == 0"),
79    ps("Typed",         PropertyKind::Typed,         &[&[Target, Ty]],           ContractKind::Precond, BuildKind::Uniform, "*{0} holds TypeInvariant({1})"),
80    ps("Init",          PropertyKind::Init,          &[&[Target, Ty, Expr]],     ContractKind::Precond, BuildKind::Uniform, "forall i in 0..{2}: *({0} + i*sizeof({1})) |= type_invariant({1}), and the {2} value(s) are initialized"),
81    ps("ValidString",   PropertyKind::ValidString,   &[&[Target, Ty, Expr]],     ContractKind::Precond, BuildKind::Uniform, "{0} is valid UTF-8"),
82    ps("NonVolatile",   PropertyKind::NonVolatile,   &[&[Target, Ty, Expr]],     ContractKind::Precond, BuildKind::Uniform, "{0} does not reference volatile memory"),
83    ps("ValidTransmute", PropertyKind::ValidTransmute, &[&[Ty, Ty]],             ContractKind::Precond, BuildKind::Uniform, "bytes_of({1}) within bytes_of({0})"),
84    ps("Trait",         PropertyKind::Trait,         &[&[Ty, Ident]],            ContractKind::Precond, BuildKind::Uniform, "{0} satisfies the trait bound {1}"),
85    ps("NoPadding",     PropertyKind::NoPadding,     &[&[Ty]],                   ContractKind::Precond, BuildKind::Uniform, "{0} has no padding bytes between fields"),
86    ps("ValidCStr",     PropertyKind::ValidCStr,     &[&[Target, Expr]],         ContractKind::Precond, BuildKind::Uniform, "{0} is a null-terminated valid UTF-8 byte sequence"),
87    ps("Unwrap",        PropertyKind::Unwrap,        &[&[Target, Ident]],        ContractKind::Precond, BuildKind::Uniform, "unwrap({0}) = {1}"),
88    // Variable-arity / special-build primitives.
89    ps("Size",          PropertyKind::Size,          &[&[Ty, Ident], &[Ty, Expr]], ContractKind::Precond, BuildKind::Size, "sizeof({0}) = {1}"),
90    ps("NonSize",       PropertyKind::Size,          &[&[Ty, Ident], &[Ty, Expr]], ContractKind::Precond, BuildKind::Size, "sizeof({0}) = {1}"),
91    ps("Allocated",     PropertyKind::Allocated,     &[&[Target], &[Target, Ty, Expr], &[Target, Ty, Expr, Ident]], ContractKind::Precond, BuildKind::Allocated, "{0} points to a live allocation of size: size_of({1}) * {2}"),
92    ps("InBound",       PropertyKind::InBound,       &[&[Expr], &[Target, Expr], &[Target, Ty, Expr]], ContractKind::Precond, BuildKind::InBound, "same_alloc([{0}, {0} + sizeof({1})*{2}])"),
93    ps("InBounded",     PropertyKind::InBound,       &[&[Expr], &[Target, Expr], &[Target, Ty, Expr]], ContractKind::Precond, BuildKind::InBound, "same_alloc([{0}, {0} + sizeof({1})*{2}])"),
94    ps("NonOverlap",    PropertyKind::NonOverlap,    &[&[Target], &[Target, Target, Ty, Expr]], ContractKind::Precond, BuildKind::NonOverlap, "[{0}] are pairwise disjoint memory ranges"),
95    ps("ValidNum",      PropertyKind::ValidNum,      &[&[Expr], &[Expr, Expr]],   ContractKind::Precond, BuildKind::ValidNum, "{0}"),
96    ps("Alias",         PropertyKind::Alias,         &[&[Target, Target]],       ContractKind::Hazard,  BuildKind::Targets, "{0} and {1} alias each other (hazard)"),
97    ps("Alive",         PropertyKind::Alive,         &[&[Target, Target]],       ContractKind::Precond, BuildKind::Targets, "*{0} outlives '{1}"),
98    ps("Pinned",        PropertyKind::Pinned,        &[&[Target, Ident]],        ContractKind::Precond, BuildKind::Pinned, "{0} will not be moved"),
99    ps("SplitTransmute", PropertyKind::SplitTransmute, &[&[Ty, Ty]],             ContractKind::Precond, BuildKind::SplitTransmute, "[{0}] as [{1}]: every size_of({1})-byte contiguous chunk of [{0}] is a valid bit-pattern of {1} (type_invariant satisfied, alignment not required)\nforall w subset bytes([{0}]), |w| == |{1}|: reinterpret_as_{1}(w) |= type_invariant({1}) \\ align_of({1})"),
100    ps("TobeSpecified", PropertyKind::Unknown,       &[],                        ContractKind::Precond, BuildKind::TobeSpecified, "(unresolved contract)"),
101];
102
103pub(crate) fn find_spec(name: &str) -> Option<&'static PropertySpec> {
104    SPECS.iter().find(|s| s.tag == name)
105}
106
107/// The canonical meaning template for a property kind (the first tag that maps
108/// to `kind`).  Argument-dependent kinds override this at render time.
109pub(crate) fn kind_meaning(kind: PropertyKind) -> &'static str {
110    SPECS.iter()
111        .find(|s| s.kind == kind)
112        .map(|s| s.meaning)
113        .unwrap_or("(unresolved contract)")
114}
rapx/verify/contract/spec.rs

rapx/verify/contract/
spec.rs
