Module types 

The contract IR: places, expressions, predicates, and the property model.

Property is a DNF form (only Atom and Or; conjunction is a list), with a PropertyKind vocabulary of safety tags. All contract front-ends (attributes, JSON, compound-property macros, pest DSL) produce this IR.

Structs

AndProperty 🔒

A conjunction: every conjuncts member must hold.

AtomProperty 🔒

ContractOrigin 🔒

Display metadata for a property expanded from a compound property (pred!-style macro). Purely presentational: it lets reports render a macro-expanded contract as a single name(args) entry with its doc-derived meaning, instead of the underlying primitives it expanded into.

ContractPlace 🔒

A place a contract refers to: a PlaceBase root plus a sequence of ContractProjection steps into it (e.g. self.next.value, head.iter()).

NumericPredicate 🔒

OrProperty 🔒

A disjunction: at least one disjuncts member must hold.

Enums

ContractExpr 🔒

ContractKind 🔒

ContractProjection 🔒

A step into a place, from the base down to the value a contract talks about (written as .field, .unwrap_some(), or .iter() in the DSL).

NumericBinOp 🔒

NumericUnaryOp 🔒

PlaceBase 🔒

The root of a contract place: a function’s return value, an argument, or a raw MIR local. Return ⇔ Local(0); Arg(n) ⇔ Local(n + 1).

Property 🔒

A safety property: a boolean formula over atomic predicates.

PropertyArg 🔒

One argument of a predicate call — what the property is applied to.

PropertyKind 🔒

The vocabulary of safety predicates a contract can assert.

RelOp 🔒