bmb-query

Understand a million lines with a single question.

Query interface for BMB codebases — ask questions, get answers grounded in contracts.

---

Philosophy

You don't need to read AI-generated code. You need to understand what it guarantees.

$ bmb query "what does the auth module guarantee?"

The auth module provides 3 public functions with these guarantees:

  login(user, pass) -> Session?
    post: ret.is_some() implies valid_credentials(user, pass)
    post: ret.is_some() implies session_store.contains(ret)

  logout(session)
    post: not session_store.contains(session)

  verify(session) -> bool
    post: ret == session_store.contains(session)

Contracts are the documentation. This tool makes them accessible.

---

Features

Natural Language Queries

Ask in plain English. Get answers from contracts.

bmb query "can this function ever return null?"
bmb query "what preconditions does payment.charge require?"
bmb query "show me all functions that modify user state"

Failure Case Generation

Understand boundaries through counterexamples.

$ bmb query "when does binary_search fail?"

binary_search fails when:
  1. Precondition violated: arr is not sorted
     Example: binary_search([3, 1, 2], 1)
  
  2. Returns None: target not in array
     Example: binary_search([1, 2, 3], 5)

Dependency Analysis

Trace how contracts flow through your codebase.

$ bmb query "what depends on is_sorted?"

is_sorted is used in:
  ├── binary_search (precondition)
  ├── merge (postcondition)
  ├── SortedVec.insert (invariant)
  └── quick_sort (postcondition)

Changes to is_sorted affect 4 contracts.

Module Summaries

Get the big picture instantly.

$ bmb query "summarize the payment module"

payment (src/payment.bmb)
├── 5 public functions
├── 2 types with invariants
└── Key guarantees:
    - All charges require valid_card(card)
    - Refunds never exceed original charge
    - Transaction log is append-only

---

Usage

CLI

# Interactive mode
bmb query

# Single question
bmb query "what does this function do?"

# Query specific file
bmb query --file src/auth.bmb "list all preconditions"

# Output as JSON (for tooling)
bmb query --json "module dependencies"

LSP Integration

Works with vscode-bmb:

• Hover over function → see contract summary
• Right-click → "Explain this code"
• Command palette → "BMB: Ask about codebase"

REPL

$ bmb query --repl
bmb> what modules modify the database?
bmb> show the contract for user.create
bmb> why does transfer require sender != receiver?

---

Query Types

Query	Example
Guarantees	"what does X guarantee?"
Requirements	"what does X require?"
Failures	"when does X fail?"
Dependencies	"what depends on X?"
Modifications	"what modifies X?"
Comparison	"difference between X and Y?"
Search	"functions that return Option"

---

How It Works

Query → Parse → Contract Analysis → LLM Grounding → Response
                     ↓
              Actual contracts,
              not hallucination

Responses are grounded in real contracts from your codebase. The LLM explains; it doesn't invent.

---

Configuration

# bmb-query.toml
[query]
default_scope = "src/"
max_depth = 5

[llm]
provider = "anthropic"  # or "openai", "local"
model = "claude-sonnet"

---

Integration

With CI

# Generate contract documentation
- run: bmb query --json "summarize all modules" > contracts.json

With bmb-test

# Find untested contracts
bmb query "contracts with no test coverage"

---

License

MIT