wrap-vs-specify

wrap-vs-specify is a cursor rule for Cursor from briangmilnes/APAS-VERUS. It costs 0 tokens per session (630 once invoked), scanned A, original, MIT.

A set of rules for deciding whether to add Verus specifications directly to an existing Rust type or place that type inside a new wrapper structure. Verus specifications describe properties used to prove code correct.

In plain words
What is it for?
It is for designing and modifying Verus specifications for Rust types, including choosing between direct specifications and wrapper structs.
Why use it?
It prevents choosing the wrong design when adding formal specifications to standard library types such as sets or maps.

Cursor rule for Cursor

Install

Getting it into your agent

One page per mod, every tool's command on it. A separate URL per tool would split the same page into five that compete with each other.

agentmods
npx agentmods add rules/briangmilnes/apas-verus/wrap-vs-specify
Clone the repo
git clone --depth 1 https://github.com/briangmilnes/APAS-VERUS

Made for: Cursor.

Wrote this? Show the measurements

A badge with what this costs and how it scanned, read live from this page, so it follows the numbers instead of freezing them. Markdown for a README, HTML for a documentation site or a project page.

agentmods badge for wrap-vs-specify

README.md
[![agentmods](https://agentmods.dev/badge/rules/briangmilnes/apas-verus/wrap-vs-specify.svg)](https://agentmods.dev/rules/briangmilnes/apas-verus/wrap-vs-specify)
Your own site
<a href="https://agentmods.dev/rules/briangmilnes/apas-verus/wrap-vs-specify"><img src="https://agentmods.dev/badge/rules/briangmilnes/apas-verus/wrap-vs-specify.svg" alt="Measured on agentmods" height="20"></a>
Per session 0 Nothing until a file matches its globs; then the whole rule loads.
When invoked 630 The whole file, excluding the scripts and references it only reads on demand.
Security scan A 0 findings. Scan, not verified.
Origin original No closer match found in the catalogue.
Token cost

What it costs to keep this loaded

Counted locally with the o200k_base tokenizer, which is exact for GPT models; Claude uses its own tokenizer and its counts differ. Treat this as one consistent yardstick across the catalogue rather than a bill. Prices are per million input tokens.

ModelPer sessionOnce invoked
Fable 5 $0.00000 $0.00630
Opus 5 $0.00000 $0.00315
Sonnet 5 $0.00000 $0.00126
Haiku 4.5 $0.00000 $0.00063

Measured yesterday against content hash 40ba5eeea828, method: parsed. Prices are Anthropic first-party input rates as of 2026-08-30, from the pricing page.

Security

Grade A, and why

wrap-vs-specify scanned grade A with 0 findings against 26 rules in 11 categories — prompt injection, anti-refusal, data exfiltration, privilege escalation, supply chain, agent snooping, system-prompt leakage, SSRF and excessive agency — measured yesterday.

A static scan of the body, not an audit. Every finding is printed with the line that produced it so you can judge whether it matters here. A mod is markdown that instructs an agent; that is exactly why what it instructs is worth reading.

Nothing flagged

None of the 26 patterns this scan looks for appear in this file: no shell pipes, no recursive deletes, no credential paths, no hidden text, no instruction-override or anti-refusal phrasing, no agent-config snooping. That is not a guarantee, it is the absence of the things that are checkable.

.cursor/rules/verus/wrap-vs-specify.mdc · 78 lines

How it starts

The opening of the file, as written. The whole thing — 78 lines — stays where its author put it; the contents beside it link to each section on GitHub.

Wrap vs Specify

Two approaches for adding Verus specifications to Rust types:

SPECIFY (external_type_specification / assume_specification)

Adds specs directly to an existing Rust type WITHOUT creating a new struct.

// The std type IS the type you use
#[verifier::external_type_specification]
pub struct ExHashSet<K, S>(HashSet<K, S>);

// Users write:
let s: HashSet<u64> = HashSet::new();
assert(s@ == Set::empty());  // Specs available on std type

Characteristics:

  • No new struct created
  • User uses the original std type directly
  • View type matches the std type's generic params (e.g., Set<K> not Set<K::V>)
  • Cannot add new methods, only specs to existing methods

WRAP (new struct containing the std type)

Creates a NEW struct that contains the std type as a field.

// New struct wrapping the std type
pub struct HashSetWithView<K: View + Eq + Hash> {
    m: HashSet<K>,  // the wrapped std type
}

// Users write:
let s: HashSetWithView<MyKey> = HashSetWithView::new();
assert(s@ == Set::empty());  // View can differ from inner type's view

Characteristics:

  • New struct created
  • User uses the wrapper type, not std type directly
  • View type can be transformed (e.g., Set<K::V> mapped from keys)
  • Can add new methods beyond what std provides
  • Can enforce additional invariants in preconditions

When to Use Which

Situation Use
Simple types, no View mapping needed SPECIFY
Need K::V instead of K in view WRAP
Need to add methods std doesn't have WRAP
Need to enforce coherence properties (e.g., obeys_feq_full) WRAP
Want users to use familiar std types SPECIFY

Examples in vstd

std Type SPECIFY WRAP
Vec<T> ExVec
HashSet<K> ExHashSet HashSetWithView
HashMap<K,V> ExHashMap HashMapWithView
hash_set::Iter<K> ExSetIter

Examples in vstdplus/APAS

std Type SPECIFY WRAP
HashSet<K> HashSetWithViewPlus (adds iter())
hash_set::Iter<K> SetStEphIter (closed spec view)

Read the full file on GitHub · 78 lines

Changes

What this file has done since we first saw it

Hashed on every crawl. A supply-chain change to an agent config is a question of when, not whether, so the history is kept rather than the latest state alone.

  1. yesterday First seen · 78 lines · 0 tokens per session scan A 40ba5eeea828

Subscribe to this mod's changes

wrap-vs-specify is a cursor rule published in the GitHub repository briangmilnes/APAS-VERUS (10 stars, last pushed 1mo ago), licensed MIT. It costs nothing until one of its globs matches a file; then it loads 630 tokens. A static security scan graded it A with 0 findings. No closer match exists in the catalogue, so it is treated as the original; first seen 2026-09-03.