-- allium: 2
-- vecgrep.allium
--
-- Scope: User-visible behaviour of vecgrep.
-- Includes:
-- - one project root per invocation
-- - path admission against that root
-- - config resolution from CLI/project/global/defaults
-- - index lifecycle for CLI, TUI, and server modes
-- - search lifecycle and result/output behaviour
-- Excludes:
-- - embedding internals, storage details, threading, terminal layout
-- - exact chunking/tokenization algorithms
-- - HTTP transport details (method validation, status codes, URL parsing)
external entity Operator {
id: String
}
external entity Client {
id: String
}
enum RootMarker { git | hg | jj | vecgrep | none }
enum Mode { cli | interactive | serve }
enum OutputFormat { pretty | json | files | count }
enum PathKind { file | directory }
enum PathStatus { admitted | skipped | rejected }
enum EmbedderSource { local | remote }
enum IndexStatus { empty | indexing | ready | aborted }
enum SearchSource { cli | interactive | http }
enum SearchStatus { pending | completed | failed }
enum StaleCleanupScope { walked_directory_prefix | none }
config {
precedence: cli > project > global
top_k: Integer = 10
threshold: Decimal = 0.2
chunk_size: Integer = 256
chunk_overlap: Integer = 64
full_index: Boolean = false
quiet: Boolean = false
index_warn_threshold: Integer = 1000
embedder_source: EmbedderSource = local
embedder_model: String = "all-MiniLM-L6-v2"
}
value IndexStats {
files: Integer
chunks: Integer
holes: Integer
db_size_bytes: Integer
}
entity ProjectRoot {
path: Path
marker: RootMarker
index_status: IndexStatus
model_name: String?
chunk_size: Integer?
chunk_overlap: Integer?
file_count: Integer
chunk_count: Integer
hole_count: Integer
}
entity Invocation {
operator: Operator
cwd: Path
mode: Mode
output_format: OutputFormat
query: String? -- from positional or --query flag
query_flag: String? -- explicit --query flag; requires interactive or serve mode
-- when set, all positionals become paths (no filesystem checks)
-- if clap assigned a positional to query, it is moved to paths
show_stats: Boolean
show_root: Boolean
index_only: Boolean
reindex_requested: Boolean
clear_cache_requested: Boolean
skip_outside_root: Boolean
no_scope: Boolean -- when true, search entire project index ignoring path scopes
-- conflicts with explicit paths
open_cmd: String? -- template for opening files from TUI
-- placeholders: {file}, {line}, {end_line}
-- falls back to $PAGER or less
selected_root: ProjectRoot?
paths: SearchPath with invocation = this
admitted_paths: paths where status = admitted
searches: Search with invocation = this
}
entity SearchPath {
invocation: Invocation
path: Path
kind: PathKind
status: PathStatus
}
entity IndexRun {
invocation: Invocation
root: ProjectRoot
blocking: Boolean
stale_cleanup_scope: StaleCleanupScope
status: pending | completed | aborted
}
entity Search {
invocation: Invocation?
request_id: String
root: ProjectRoot
source: SearchSource
query: String
top_k: Integer
threshold: Decimal
status: SearchStatus
results: SearchResult with search = this
}
entity SearchResult {
search: Search
file: Path
start_line: Integer
end_line: Integer
score: Decimal
text: String
}
-- Root selection ----------------------------------------------------------
--
-- Priority: cwd marker > single-directory argument marker > cwd fallback.
-- Expressed as a single rule with conditionals rather than three mutually-
-- exclusive rules with guard chains on intermediate candidate fields.
rule SelectRoot {
when: invocation: Invocation.created
let cwd_root = FindMarkerAbove(invocation.cwd)
let path_root =
if invocation.paths.count = 1 and invocation.paths[0].kind = directory:
FindMarkerAbove(invocation.paths[0].path)
else:
null
ensures: invocation.selected_root =
if cwd_root != null:
cwd_root
else if path_root != null:
path_root
else:
ProjectRoot.created(
path: invocation.cwd,
marker: none,
index_status: empty,
file_count: 0,
chunk_count: 0,
hole_count: 0
)
}
-- Path admission ----------------------------------------------------------
rule AdmitOrRejectPaths {
when: path: SearchPath.created
requires: path.invocation.selected_root != null
ensures:
if not PathOutsideRoot(path.path, path.invocation.selected_root.path):
path.status = admitted
else if path.invocation.skip_outside_root:
path.status = skipped
else:
path.status = rejected
InvocationFailed(invocation: path.invocation, reason: outside_selected_root)
}
rule FailIfNoPathsAdmitted {
when: invocation: Invocation.created
requires: invocation.paths.count > 0
requires: invocation.admitted_paths.count = 0
ensures: InvocationFailed(invocation: invocation, reason: all_paths_outside_selected_root)
}
-- Cache management --------------------------------------------------------
rule ClearCacheResetsIndex {
when: invocation: Invocation.clear_cache_requested becomes true
requires: invocation.selected_root != null
ensures: invocation.selected_root.index_status = empty
ensures: invocation.selected_root.model_name = null
ensures: invocation.selected_root.chunk_size = null
ensures: invocation.selected_root.chunk_overlap = null
ensures: invocation.selected_root.file_count = 0
ensures: invocation.selected_root.chunk_count = 0
ensures: invocation.selected_root.hole_count = 0
}
rule ReindexOrConfigChangeRebuildsIndex {
when: invocation: Invocation.selected_root becomes not null
requires:
invocation.reindex_requested
or invocation.selected_root.model_name != null and (
invocation.selected_root.model_name != config.embedder_model
or invocation.selected_root.chunk_size != config.chunk_size
or invocation.selected_root.chunk_overlap != config.chunk_overlap
)
ensures: invocation.selected_root.index_status = indexing
ensures: invocation.selected_root.file_count = 0
ensures: invocation.selected_root.chunk_count = 0
ensures: invocation.selected_root.hole_count = 0
}
-- Indexing lifecycle ------------------------------------------------------
--
-- CLI and --index-only always block until indexing completes before
-- searching. TUI and serve index progressively: searches may return
-- partial results from whatever has been indexed so far.
rule BlockingIndexRun {
when: invocation: Invocation.selected_root becomes not null
requires:
invocation.mode = cli
or invocation.index_only
or config.full_index
ensures: IndexRun.created(
invocation: invocation,
root: invocation.selected_root,
blocking: true,
stale_cleanup_scope:
if invocation.admitted_paths.count = 1
and invocation.admitted_paths[0].kind = directory:
walked_directory_prefix
else:
none,
status: pending
)
ensures: invocation.selected_root.index_status = indexing
}
rule BlockingIndexCompletes {
when: run: IndexRun.created
requires: run.blocking
ensures:
if config.index_warn_threshold > 0
and UserDeclinesLargeIndex(run.invocation):
run.status = aborted
run.root.index_status = aborted
else:
run.status = completed
run.root.index_status = ready
}
rule StaleEntriesRemovedAfterIndexing {
when: run: IndexRun.status becomes completed
requires: run.stale_cleanup_scope = walked_directory_prefix
ensures: StaleEntriesRemoved(run.root, scope: walked_directory_prefix)
ensures: ExplicitFlagCleared(run.root, walked_paths: run.walked_paths)
@guidance
-- When the walk covers a single subdirectory, only non-explicit
-- stale entries under that prefix are removed. Entries outside
-- the walked prefix are intentionally preserved so that narrow
-- searches don't force project-wide cleanup.
--
-- Explicit files (from file paths, not directory walks) are never
-- deleted — they stay cached for fast re-search. Files seen in
-- the walk have their explicit flag cleared so they become normal
-- cached entries (even if their content hash matched and they
-- were not re-embedded).
}
-- Search lifecycle --------------------------------------------------------
rule CliSearchStartsAfterIndexing {
when: run: IndexRun.status becomes completed
requires: run.invocation.mode = cli
requires: run.invocation.query != null
requires: not run.invocation.index_only
ensures: Search.created(
invocation: run.invocation,
request_id: NewRequestId(run.invocation),
root: run.root,
source: cli,
query: run.invocation.query,
top_k: config.top_k,
threshold: config.threshold,
status: pending
)
}
rule InteractiveSearchStartsOnQuery {
when: invocation: Invocation.query becomes not null
requires: invocation.mode = interactive
ensures: Search.created(
invocation: invocation,
request_id: NewRequestId(invocation),
root: invocation.selected_root,
source: interactive,
query: invocation.query,
top_k: config.top_k,
threshold: config.threshold,
status: pending
)
}
rule SearchCompletesOrFails {
when: search: Search.created
ensures:
if EmbeddingFails(search):
search.status = failed
else:
search.status = completed
SearchResultsReady(search: search)
}
-- Index-only and info operations ------------------------------------------
rule IndexOnlyStopsAfterIndexing {
when: run: IndexRun.status becomes completed
requires: run.invocation.index_only
ensures: IndexBuilt(invocation: run.invocation)
}
rule ShowStats {
when: invocation: Invocation.show_stats becomes true
requires: invocation.selected_root != null
invocation.query = null -- standalone action, no query allowed
ensures: StatsRendered(
invocation: invocation,
stats: IndexStats(
files: invocation.selected_root.file_count,
chunks: invocation.selected_root.chunk_count,
holes: invocation.selected_root.hole_count,
db_size_bytes: CacheSizeBytes(invocation.selected_root)
)
)
}
rule ShowRoot {
when: invocation: Invocation.show_root becomes true
requires: invocation.selected_root != null
ensures: RootPrinted(invocation: invocation, root: invocation.selected_root.path)
}
-- Surfaces ----------------------------------------------------------------
surface CommandLine {
facing operator: Operator
context invocation: Invocation where mode = cli
exposes:
invocation.selected_root.path
invocation.output_format
config.top_k
config.threshold
invocation.selected_root.index_status
invocation.selected_root.chunk_count
provides:
RunSearch(operator, invocation)
when invocation.query != null
and not invocation.index_only
and not invocation.show_root
and not invocation.show_stats
BuildIndex(operator, invocation)
when invocation.index_only
ShowStats(operator, invocation)
when invocation.show_stats
ShowRoot(operator, invocation)
when invocation.show_root
Reindex(operator, invocation)
when invocation.reindex_requested
ClearCache(operator, invocation)
when invocation.clear_cache_requested
@guarantee SearchResultsScopedToRequestedPaths
-- Search results are post-filtered to only include files under
-- the requested directory paths or matching requested file paths.
-- Searching "src/" only returns results from src/, not the entire
-- index. Running from a subdirectory without explicit paths scopes
-- results to that subdirectory (the default "." is resolved to the
-- cwd suffix relative to the project root). Consistent with ripgrep
-- path scoping. Applies across CLI, TUI, and serve.
@guarantee ExplicitFilesAreCachedButFiltered
-- Paths with kind = file are indexed with an explicit flag and
-- stay cached permanently for fast re-search. Only the specific
-- explicit files passed in the invocation appear in results, not
-- all explicit files from prior invocations. Directory-only
-- searches exclude all explicit files. When a directory walk
-- rediscovers an explicit file, its flag is cleared and it
-- becomes a normal cached entry.
@guarantee JsonOutputUsesRootRelativePaths
-- When output_format = json, file paths are relative to the project
-- root and each JSONL line includes a "root" field.
@guarantee TerminalOutputUsesCwdRelativePaths
-- When output_format in {pretty, files, count}, file paths are
-- displayed relative to the operator's working directory.
}
surface InteractiveSearch {
facing operator: Operator
context invocation: Invocation where mode = interactive
exposes:
invocation.query
invocation.selected_root.path
invocation.selected_root.index_status
invocation.selected_root.chunk_count
invocation.searches
provides:
UpdateQuery(operator, invocation, query)
MoveSelection(operator, invocation)
TogglePreview(operator, invocation)
OpenSelectedResult(operator, invocation)
}
surface SearchServer {
facing client: Client
context root: ProjectRoot
exposes:
root.path
root.index_status
root.chunk_count
provides:
SearchRequest(client, root, query, top_k?, threshold?)
StatusRequest(client, root)
@guarantee ProgressiveIndexing
-- Searches may return results from a partial index while
-- background indexing is still in progress.
@guarantee SearchDefaults
-- When top_k or threshold are omitted, the server uses the
-- resolved config values (config.top_k, config.threshold).
@guarantee PipelineStatusEndpoint
-- GET /status returns the current PipelineStatus as JSON.
-- During indexing: {"status":"indexing","indexed":N,"total":M|null,"chunks":C}
-- When ready: {"status":"ready","files":N,"chunks":C}
-- Ready state reports full index counts from the database,
-- not just the current indexing pass.
}
rule ServerSearchStarts {
when: SearchRequest(client, root, query, top_k, threshold)
requires: query != null and query != ""
ensures: Search.created(
request_id: NewRequestId(client),
root: root,
source: http,
query: query,
top_k: top_k ?? config.top_k,
threshold: threshold ?? config.threshold,
status: pending
)
}