---
name: property-taxonomy
user-invocable: false
description: The §5b property taxonomy — 16 property categories, cross-cutting modifiers, and the walk-the-scaffold procedure for enumerating candidate verifiable properties tagged (category, provenance CP|ICP|DP, difficulty 1-10). Load when generating properties from a spec (Verification Expert / CPs), from a design (Design Advisor / DPs), from existing code (Property Discovery / brownfield), or when classifying what kind of claim a property is.
---

# Property Taxonomy (§5b)

A **property** is a verifiable claim about a program or system. The taxonomy is an **enumeration scaffold**: walk the 16 categories against the artifact in front of you, ask per category "does this apply?", and emit candidate properties tagged `(category, provenance, difficulty)`. The difficulty rating selects the verification method via the **oracle ladder** (load the `oracle-ladder` skill).

## The 16 Categories

| # | Category | What it captures | Example properties |
|---|---|---|---|
| 1 | **Functional — mathematical** | Algebraic laws: commutativity, associativity, identity, distributivity | `a + b == b + a`; `parse(serialize(x)) == x` |
| 2 | **Functional — input-output** | Deterministic transformations, sorting invariants, formatting rules | sorted output is a permutation of input in non-decreasing order |
| 3 | **Functional — idempotence** | `f(f(x)) == f(x)` for retryable operations | database upsert, cache invalidation, API PUT |
| 4 | **Functional — purity** | Same inputs → same outputs, no side effects, no global state mutation | no I/O in pure-core functions; no mutation of input parameters |
| 5 | **Functional — state transitions** | Valid FSM transitions, precondition/postcondition, state invariants maintained | game phase transitions, order lifecycle |
| 6 | **Invariance — data structure** | Properties that must hold after every operation on a data structure | BST ordering, heap property, array bounds, no-duplicates-in-set |
| 7 | **Invariance — loop** | Properties maintained across iterations | accumulator bounds in a fold |
| 8 | **Invariance — representation** | Concrete data faithfully represents abstract ghost state | the glue between spec and implementation (P5 provenance bridge) |
| 9 | **Framing** | What the function is *allowed* to modify and what it must leave unchanged | "this function modifies only X; Y and Z are unchanged" |
| 10 | **Security & safety** | Input validation, access control, confidentiality, non-malleability of parsers | no buffer overflow; ownership-verified before data return; credentials never in logs |
| 11 | **Performance** | Time-complexity bounds, memory constraints, latency budgets | O(n log n) sort; response < 200ms at p99; allocation < 1MB |
| 12 | **Concurrency & thread-safety** | Race-freedom, proper locking, atomicity of operations | no data race on shared counter; lock ordering prevents deadlock |
| 13 | **Usability & interface** | API consistency, input validation, error-message quality | every public function validates arguments; error types are discriminated unions |
| 14 | **Refinement under composition** | Combined modules retain desired properties | separation-logic frame rule; rely/guarantee across component boundaries |
| 15 | **Integration & interoperability** | Contract compatibility across versions, loose coupling, schema evolution, service-boundary correctness | backward-compatible API; optional-field addition doesn't break consumers |
| 16 | **Temporal & distributed** | Safety ("bad things never happen"), liveness ("good things eventually happen"), fairness, consensus | mutual exclusion; eventual delivery; agreement + validity + termination |

## Cross-cutting modifiers

Every property additionally carries:

- **Boundary/edge-case flag** — special inputs (null, empty, max, min, adversarial). Tag whenever the property has a non-uniform behavior at extremes; these inputs become explicit PBT generators / SMT corner cases.
- **Determinism modifier** — deterministic vs non-deterministic. Non-deterministic properties cannot be checked by simple equality oracles; they need clustering, statistical bounds, or model-checking over the nondeterminism.
- **Sync/async modifier** — synchronous vs asynchronous evaluation context. Async shifts categories 12/16 up the difficulty ladder and changes the oracle (e.g., `loom`/`tokio::test` vs plain unit test).

## Provenance tag (P5)

Every property is tagged with its origin — provenance determines authority over who may change it:

- **CP — Contractual Property.** Traces to a stakeholder requirement (REQ-i.j). Only the stakeholder may modify/add/remove. Tested as black-box assertions on public interfaces.
- **ICP — Inherited Contractual Property.** Traces to an applicable norm (regulation, certification objective, corporate policy); cites authority by paragraph. The stakeholder confirms scope but cannot waive content. Carries an extra authority-citation column; `severity: exploitable` ICPs are non-waivable. 
- **DP — Design-induced Property.** Arises from implementation choices (data structures, algorithms, protocols, framings). Agents may modify DPs freely provided all CPs and ICPs remain satisfied. Tested as internal assertions and invariants.

## How to walk the taxonomy

For each category 1–16, against the artifact you are reasoning about:

1. Ask **"does this category apply to this component / requirement / data structure?"** Skip with a one-line note if not (the note is auditable evidence you considered it).
2. For each applicable category, write a candidate property in checkable form (a predicate, a Hoare triple, an algebraic law).
3. Tag it `(category #, provenance CP|ICP|DP, difficulty 1-10)` and set the three cross-cutting modifiers.
4. Route by difficulty through the oracle ladder. **Route conservatively**: when difficulty is ambiguous, pick the harder tier — a category-12 property looks easy until you realize it's shared-memory (difficulty 9), not actor-isolated (difficulty 5). Paradigm modulates difficulty; language modulates the method.
5. Difficulty-10 properties (emergent behavior, full info-flow, covert channels, crypto strength, halting) are **not skipped**: record them as monitored residual risk in `assumptions.md` with a runtime-monitor strategy (P12). Do not fake a test.

## Which agent walks it for what

- **Verification Expert** (requirement level): walks against the spec → candidate **CPs and ICPs** with difficulty, routed in `04-vnv-plan.md`.
- **Design Advisor** (design level): walks against `03-design.md` → candidate **DPs** tagged with the design choice they arise from and the CPs they support; enters them in `property_registry.md`.
- **Spec Extraction agent** (brownfield): walks against existing code via the CDCR protocol; generated properties are *candidates* until stakeholder confirmation.
- **Robustness Analysis Agent**: perturbation findings often surface categories 14–16 that weren't previously explicit.

## Notes on difficulty modulation

- A concurrency property (cat 12) in an **actor** zone (isolation is structural) may be difficulty-5 (check mailbox types); the same property in **shared memory** is difficulty-9 (model-check interleavings).
- A framing property (cat 9) in **reference-based Rust** is partially discharged free by the ownership/borrow checker (compiler is the oracle). (Load `language-profiles`.) **Exception — arena-allocated Rust:** when nodes are named by integer id rather than `&`/`&mut` (graphs, intrusive lists, cyclic rings), the borrow checker gives framing **nothing for free** — separation is deliberately outside the type system. Framing becomes an *explicit disjointness predicate* over a ghost id-set, and the "every other region unchanged" clause is proved in Verus, not borrow-checked (load `bi-abduction-arena`). So cat-9 difficulty for an aliased arena is *not* the easy compiler-discharged tier; it is a proof obligation.
- Representation invariance (cat 8) is the **provenance bridge**: it glues the concrete implementation state to the abstract ghost state the spec talks about, and is what lets a CP about abstract state be discharged against concrete code. For **arena structures** this is the central property: the executable indices (`head`/`next`/`tail`/`sparse`) are a *representation* of a ghost `Seq`/`Set` of ids, and the cat-8 invariant (shape clause) plus cat-6 disjointness/coverage *are* the `wf` of the structure. An aliased/cyclic structure is specified almost entirely in cats 6/8/9 over the ghost model — see `bi-abduction-arena`.
- **Refinement under composition (cat 14)** for arenas: when many sub-structures share one backing store, "combined regions retain disjointness" is the cat-14/frame obligation — the whole-arena partition holds because each operation frames the regions it doesn't touch (the disjointness clause), proved per-operation and composed. Not free from the type system; proved.

This skill is the canonical in-repo property taxonomy. Pair it with `oracle-ladder` to turn each tagged property into a verification-method assignment.