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//!
10//! Some tags are declared but not fully supported: `Unwrap`, `Pinned`,
11//! `Opened` and `Unreachable` are parsed but the checker returns `Unknown`;
12//! `NonVolatile` is assumed satisfied (the VM does not model volatile access).
13
14use super::types::*;
15
16#[derive(Clone, Copy, Debug, PartialEq, Eq)]
17pub(crate) enum ArgKind {
18    Target,
19    Ty,
20    Expr,
21    Ident,
22}
23
24/// How a tag's arguments are assembled into a `Property`.
25#[derive(Clone, Copy, Debug, PartialEq, Eq)]
26pub(crate) enum BuildKind {
27    /// Positional resolution over a matched `forms` entry (common case).
28    Uniform,
29    /// `Size(T, sized | unsized | const)` — second arg is an ident or a const.
30    Size,
31    /// `Allocated(target[, T, n[, allocator]])` — 1/3/4-argument forms.
32    Allocated,
33    /// `InBound(index | target,index | target,T,n)` — index + for_each variants.
34    InBound,
35    /// `NonOverlap(indices | a,b,T,count)` — 1/4-argument forms.
36    NonOverlap,
37    /// `ValidNum(predicate | value, interval)`.
38    ValidNum,
39    /// `Pinned(ptr, lifetime)` — exactly two args; lifetime is required.
40    Pinned,
41    /// `SplitTransmute([T], [U])` — array element types.
42    SplitTransmute,
43    /// One-or-more target places (`Alias`, `Alive`).
44    Targets,
45    /// `ContainNoType(T, bad1, bad2, ...)` — first arg is a type, the rest are
46    /// negative type names (one or more).
47    ContainNoType,
48    /// Placeholder accepting any args; always yields `Unknown`.
49    TobeSpecified,
50}
51
52pub(crate) struct PropertySpec {
53    pub tag: &'static str,
54    pub kind: PropertyKind,
55    /// Accepted argument shapes. Authoritative for [`BuildKind::Uniform`]
56    /// only: the other build kinds validate arity in their `build_*`
57    /// function, so keep the two in sync. For `BuildKind::Targets` the single
58    /// entry is a marker and the tag accepts one or more `Target` args.
59    pub forms: &'static [&'static [ArgKind]],
60    pub contract_kind: ContractKind,
61    pub build: BuildKind,
62    /// Human-readable explanation template, with `{0}`, `{1}`, `{2}`
63    /// placeholders bound to the rendered positional arguments.  This keeps the
64    /// display text co-located with the tag declaration instead of hardcoded in
65    /// the renderer.  A few argument-dependent kinds (`InBound`, `Size`,
66    /// `ValidNum`, `Alive`, `Allocated`, `NonOverlap`, `Alias`) override this
67    /// template structurally at render time.
68    pub meaning: &'static str,
69}
70
71const fn ps(
72    tag: &'static str,
73    kind: PropertyKind,
74    forms: &'static [&'static [ArgKind]],
75    contract_kind: ContractKind,
76    build: BuildKind,
77    meaning: &'static str,
78) -> PropertySpec {
79    PropertySpec {
80        tag,
81        kind,
82        forms,
83        contract_kind,
84        build,
85        meaning,
86    }
87}
88
89use ArgKind::{Expr, Ident, Target, Ty};
90
91// ── Table ────────────────────────────────────────────────────────────
92
93static SPECS: &[PropertySpec] = &[
94    // Uniform single-form primitives.
95    ps(
96        "NonNull",
97        PropertyKind::NonNull,
98        &[&[Target]],
99        ContractKind::Precond,
100        BuildKind::Uniform,
101        "{0} as usize != 0",
102    ),
103    ps(
104        "Null",
105        PropertyKind::Null,
106        &[&[Target]],
107        ContractKind::Precond,
108        BuildKind::Uniform,
109        "{0} is the null pointer",
110    ),
111    ps(
112        "Owning",
113        PropertyKind::Owning,
114        &[&[Target]],
115        ContractKind::Precond,
116        BuildKind::Uniform,
117        "ownership(*{0}) = none: no live owner aliases the pointee",
118    ),
119    // Unverified: the checker returns `Unknown` (no implementation yet).
120    ps(
121        "Opened",
122        PropertyKind::Opened,
123        &[&[Target]],
124        ContractKind::Precond,
125        BuildKind::Uniform,
126        "{0} is a valid open file descriptor",
127    ),
128    // Unverified: the checker returns `Unknown` (no implementation yet).
129    ps(
130        "Unreachable",
131        PropertyKind::Unreachable,
132        &[&[]],
133        ContractKind::Precond,
134        BuildKind::Uniform,
135        "this branch is unreachable",
136    ),
137    ps(
138        "Align",
139        PropertyKind::Align,
140        &[&[Target, Ty]],
141        ContractKind::Precond,
142        BuildKind::Uniform,
143        "({0} as usize) % align_of::<{1}>() == 0",
144    ),
145    ps(
146        "Typed",
147        PropertyKind::Typed,
148        &[&[Target, Ty]],
149        ContractKind::Precond,
150        BuildKind::Uniform,
151        "*{0} holds TypeInvariant({1})",
152    ),
153    ps(
154        "Init",
155        PropertyKind::Init,
156        &[&[Target, Ty, Expr], &[Target, Expr]],
157        ContractKind::Precond,
158        BuildKind::Uniform,
159        "forall i in 0..{2}: *({0} + i*sizeof({1})) |= type_invariant({1}), and the {2} value(s) are initialized",
160    ),
161    ps(
162        "ValidString",
163        PropertyKind::ValidString,
164        &[&[Target, Ty, Expr], &[Target]],
165        ContractKind::Precond,
166        BuildKind::Uniform,
167        "{0} is valid UTF-8",
168    ),
169    // Assumed satisfied: the VM does not model volatile access.
170    ps(
171        "NonVolatile",
172        PropertyKind::NonVolatile,
173        &[&[Target, Ty, Expr]],
174        ContractKind::Precond,
175        BuildKind::Uniform,
176        "{0} does not reference volatile memory",
177    ),
178    ps(
179        "ValidTransmute",
180        PropertyKind::ValidTransmute,
181        &[&[Ty, Ty]],
182        ContractKind::Precond,
183        BuildKind::Uniform,
184        "bytes_of({1}) within bytes_of({0})",
185    ),
186    ps(
187        "Trait",
188        PropertyKind::Trait,
189        &[&[Ty, Ident]],
190        ContractKind::Precond,
191        BuildKind::Uniform,
192        "{0} satisfies the trait bound {1}",
193    ),
194    // Variable-arity negative type predicate: first arg is the target type,
195    // the rest are negative type names the target must not (structurally)
196    // contain.  Arity is validated by `build_contain_no_type`.
197    ps(
198        "ContainNoType",
199        PropertyKind::ContainNoType,
200        &[&[Ty, Ident]],
201        ContractKind::Precond,
202        BuildKind::ContainNoType,
203        "{0} does not structurally contain {1}",
204    ),
205    // `&T: Send` — the type can be shared across threads: every
206    // interior-mutability / raw-pointer field of {0} is guarded by a
207    // synchronization primitive (mutex/rwlock/atomic).
208    ps(
209        "RefSend",
210        PropertyKind::RefSend,
211        &[&[Ty]],
212        ContractKind::Precond,
213        BuildKind::Uniform,
214        "&{0} is Send: all shared mutations of {0} go through a synchronization primitive",
215    ),
216    // Interior-mutability predicates for taming raw pointers in `Send`/`Sync`.
217    ps(
218        "NoRawPtr",
219        PropertyKind::NoRawPtr,
220        &[&[Ty]],
221        ContractKind::Precond,
222        BuildKind::Uniform,
223        "{0} has no raw pointers",
224    ),
225    ps(
226        "NoInternalMut",
227        PropertyKind::NoInternalMut,
228        &[&[Ty]],
229        ContractKind::Precond,
230        BuildKind::Uniform,
231        "{0} has no interior mutation through raw pointers",
232    ),
233    ps(
234        "UniInternalMut",
235        PropertyKind::UniInternalMut,
236        &[&[Ty]],
237        ContractKind::Precond,
238        BuildKind::Uniform,
239        "{0} has unique interior mutation (exclusive owner, no aliasing Clone)",
240    ),
241    ps(
242        "AtomicUpdate",
243        PropertyKind::AtomicUpdate,
244        &[&[Ty]],
245        ContractKind::Precond,
246        BuildKind::Uniform,
247        "{0} updates its raw pointers under synchronization or atomically",
248    ),
249    ps(
250        "NoPadding",
251        PropertyKind::NoPadding,
252        &[&[Ty]],
253        ContractKind::Precond,
254        BuildKind::Uniform,
255        "{0} has no padding bytes between fields",
256    ),
257    ps(
258        "ValidCStr",
259        PropertyKind::ValidCStr,
260        &[&[Target, Expr]],
261        ContractKind::Precond,
262        BuildKind::Uniform,
263        "{0} is a null-terminated valid UTF-8 byte sequence",
264    ),
265    // Unverified: the checker returns `Unknown` (no implementation yet).
266    ps(
267        "Unwrap",
268        PropertyKind::Unwrap,
269        &[&[Target, Ident]],
270        ContractKind::Precond,
271        BuildKind::Uniform,
272        "unwrap({0}) = {1}",
273    ),
274    // Variable-arity / special-build primitives.
275    ps(
276        "Size",
277        PropertyKind::Size,
278        &[&[Ty, Ident], &[Ty, Expr]],
279        ContractKind::Precond,
280        BuildKind::Size,
281        "sizeof({0}) = {1}",
282    ),
283    ps(
284        "Allocated",
285        PropertyKind::Allocated,
286        &[&[Target], &[Target, Ty, Expr], &[Target, Ty, Expr, Ident]],
287        ContractKind::Precond,
288        BuildKind::Allocated,
289        "{0} points to a live allocation of size: size_of({1}) * {2}",
290    ),
291    ps(
292        "InBound",
293        PropertyKind::InBound,
294        &[&[Expr], &[Target, Expr], &[Target, Ty, Expr]],
295        ContractKind::Precond,
296        BuildKind::InBound,
297        "same_alloc([{0}, {0} + sizeof({1})*{2}])",
298    ),
299    ps(
300        "NonOverlap",
301        PropertyKind::NonOverlap,
302        &[&[Target], &[Target, Target, Ty, Expr]],
303        ContractKind::Precond,
304        BuildKind::NonOverlap,
305        "[{0}] are pairwise disjoint memory ranges",
306    ),
307    ps(
308        "ValidNum",
309        PropertyKind::ValidNum,
310        &[&[Expr], &[Expr, Expr]],
311        ContractKind::Precond,
312        BuildKind::ValidNum,
313        "{0}",
314    ),
315    ps(
316        "Alias",
317        PropertyKind::Alias,
318        &[&[Target, Target]],
319        ContractKind::Hazard,
320        BuildKind::Targets,
321        "{0} and {1} alias each other (hazard)",
322    ),
323    ps(
324        "Alive",
325        PropertyKind::Alive,
326        &[&[Target, Target]],
327        ContractKind::Precond,
328        BuildKind::Targets,
329        "*{0} outlives '{1}",
330    ),
331    // Unverified: the checker returns `Unknown` (no implementation yet).
332    ps(
333        "Pinned",
334        PropertyKind::Pinned,
335        &[&[Target, Ident]],
336        ContractKind::Precond,
337        BuildKind::Pinned,
338        "{0} will not be moved",
339    ),
340    ps(
341        "SplitTransmute",
342        PropertyKind::SplitTransmute,
343        &[&[Ty, Ty]],
344        ContractKind::Precond,
345        BuildKind::SplitTransmute,
346        "[{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})",
347    ),
348    ps(
349        "TobeSpecified",
350        PropertyKind::Unknown,
351        &[],
352        ContractKind::Precond,
353        BuildKind::TobeSpecified,
354        "(unresolved contract)",
355    ),
356];
357
358pub(crate) fn find_spec(name: &str) -> Option<&'static PropertySpec> {
359    SPECS.iter().find(|s| s.tag == name)
360}
361
362/// The first tag name that maps to `kind` (the inverse of [`find_spec`]).
363pub(crate) fn tag_name_for_kind(kind: PropertyKind) -> Option<&'static str> {
364    SPECS.iter().find(|s| s.kind == kind).map(|s| s.tag)
365}
366
367/// The canonical meaning template for a property kind (the first tag that maps
368/// to `kind`).  Argument-dependent kinds override this at render time.
369pub(crate) fn kind_meaning(kind: PropertyKind) -> &'static str {
370    SPECS
371        .iter()
372        .find(|s| s.kind == kind)
373        .map(|s| s.meaning)
374        .unwrap_or("(unresolved contract)")
375}
rapx/verify/contract/spec.rs

rapx/verify/contract/
spec.rs
