Skip to main content

provable_contracts/query/
mod.rs

1//! Contract query engine with BM25 semantic search.
2//!
3//! Provides fast lookup across all contracts with semantic ranking,
4//! regex/literal search, and structured filters.
5//!
6//! Spec: `docs/specifications/sub/query.md`
7
8pub mod cross_project;
9mod index;
10mod persist;
11mod query_enrich;
12pub mod registry;
13mod types;
14mod types_render;
15
16pub use cross_project::CrossProjectIndex;
17pub use index::ContractIndex;
18pub use types::{
19    DiffInfo, EquationBinding, ProjectCoverage, ProofStatusInfo, QueryOutput, QueryParams,
20    QueryResult, ScoreInfo, SearchMode, ViolationInfo,
21};
22
23use crate::binding::BindingRegistry;
24use query_enrich::{
25    build_call_sites, build_coverage_map, build_violations, filter_by_project, filter_coverage,
26    filter_violations,
27};
28
29/// Execute a query against a contract index.
30pub fn execute(index: &ContractIndex, params: &QueryParams) -> QueryOutput {
31    let scored_indices = match params.mode {
32        SearchMode::Semantic => index.bm25_search(&params.query),
33        SearchMode::Regex => {
34            match index.regex_search(&params.query) {
35                Ok(idxs) => idxs.into_iter().map(|i| (i, 1.0)).collect(),
36                Err(_) => Vec::new(), // Invalid regex yields empty results
37            }
38        }
39        SearchMode::Literal => index
40            .literal_search(&params.query, params.case_sensitive)
41            .into_iter()
42            .map(|i| (i, 1.0))
43            .collect(),
44    };
45
46    let binding = params.binding_path.as_ref().and_then(|p| {
47        let content = std::fs::read_to_string(p).ok()?;
48        serde_yaml::from_str::<BindingRegistry>(&content).ok()
49    });
50
51    let filtered = apply_filters(index, scored_indices, params, binding.as_ref());
52    let total_matches = filtered.len();
53    let limited: Vec<_> = filtered.into_iter().take(params.limit).collect();
54
55    // Build cross-project index lazily when any cross-project flag is set
56    let needs_xp = params.show_call_sites
57        || params.show_violations
58        || params.show_coverage_map
59        || params.all_projects;
60    let xp_index = if needs_xp {
61        index.entries.first().map(|e| {
62            let p = std::path::Path::new(&e.path);
63            // Go up from contracts/foo.yaml to the repo root
64            let contracts_dir = p.parent().unwrap_or(p);
65            let repo_root = if contracts_dir
66                .parent()
67                .is_none_or(|p| p.as_os_str().is_empty())
68            {
69                std::path::Path::new(".")
70            } else {
71                contracts_dir.parent().unwrap()
72            };
73            let extra = params.include_project.as_ref().map(std::path::Path::new);
74            cross_project::CrossProjectIndex::build_with_extra(repo_root, extra)
75        })
76    } else {
77        None
78    };
79
80    let project_filter = params.project_filter.as_deref();
81    let results: Vec<QueryResult> = limited
82        .into_iter()
83        .enumerate()
84        .map(|(rank, (idx, relevance))| {
85            build_result(
86                index,
87                params,
88                binding.as_ref(),
89                xp_index.as_ref(),
90                project_filter,
91                rank,
92                idx,
93                relevance,
94            )
95        })
96        .collect();
97
98    QueryOutput {
99        query: params.query.clone(),
100        total_matches,
101        results,
102    }
103}
104
105#[allow(clippy::too_many_arguments)]
106fn build_result(
107    index: &ContractIndex,
108    params: &QueryParams,
109    binding: Option<&BindingRegistry>,
110    xp_index: Option<&cross_project::CrossProjectIndex>,
111    project_filter: Option<&str>,
112    rank: usize,
113    idx: usize,
114    relevance: f64,
115) -> QueryResult {
116    let entry = &index.entries[idx];
117    let (depends_on, depended_by) = graph_fields(index, entry, params.show_graph);
118    QueryResult {
119        rank: rank + 1,
120        stem: entry.stem.clone(),
121        path: clean_path(&entry.path),
122        relevance,
123        description: entry.description.clone(),
124        kind: entry.kind,
125        equations: entry.equations.clone(),
126        obligation_count: entry.obligation_count,
127        references: opt_vec(&entry.references, params.show_paper),
128        depends_on,
129        depended_by,
130        score: params
131            .show_score
132            .then(|| query_enrich::build_score_info(entry))
133            .flatten(),
134        proof_status: params
135            .show_proof_status
136            .then(|| query_enrich::build_proof_status_info(entry))
137            .flatten(),
138        bindings: opt_binding(entry, binding, params.show_binding),
139        diff: params
140            .show_diff
141            .then(|| query_enrich::build_diff_info(entry))
142            .flatten(),
143        pagerank: if params.show_pagerank {
144            index.cached_pagerank(&entry.stem)
145        } else {
146            None
147        },
148        call_sites: filter_by_project(build_call_sites(&entry.stem, xp_index), project_filter),
149        violations: filter_violations(
150            build_violations(entry, xp_index, params.show_violations),
151            project_filter,
152        ),
153        coverage_map: filter_coverage(
154            build_coverage_map(&entry.stem, xp_index, params.show_coverage_map),
155            project_filter,
156        ),
157    }
158}
159
160/// Clean a contract path for display: strip to `contracts/...` relative form.
161fn clean_path(raw: &str) -> String {
162    // Use the last occurrence of "contracts/" to handle paths like
163    // /foo/contracts/crates/.../../../contracts/softmax-kernel-v1.yaml
164    if let Some(idx) = raw.rfind("contracts/") {
165        raw[idx..].to_string()
166    } else {
167        raw.to_string()
168    }
169}
170
171fn opt_vec(source: &[String], include: bool) -> Vec<String> {
172    if include {
173        source.to_vec()
174    } else {
175        Vec::new()
176    }
177}
178
179fn graph_fields(
180    index: &ContractIndex,
181    entry: &types::ContractEntry,
182    show: bool,
183) -> (Vec<String>, Vec<String>) {
184    if !show {
185        return (Vec::new(), Vec::new());
186    }
187    let deps = entry.depends_on.clone();
188    let rev = index
189        .depended_by(&entry.stem)
190        .into_iter()
191        .map(String::from)
192        .collect();
193    (deps, rev)
194}
195
196fn opt_binding(
197    entry: &types::ContractEntry,
198    binding: Option<&BindingRegistry>,
199    show: bool,
200) -> Vec<EquationBinding> {
201    if show {
202        query_enrich::build_binding_info(entry, binding)
203    } else {
204        Vec::new()
205    }
206}
207
208fn apply_filters(
209    index: &ContractIndex,
210    results: Vec<(usize, f64)>,
211    params: &QueryParams,
212    binding: Option<&BindingRegistry>,
213) -> Vec<(usize, f64)> {
214    results
215        .into_iter()
216        .filter(|(idx, _)| {
217            let entry = &index.entries[*idx];
218            filter_obligation(entry, params.obligation_filter.as_ref())
219                && filter_depends_on(entry, params.depends_on.as_ref())
220                && filter_depended_by(index, entry, params.depended_by.as_ref())
221                && filter_unproven(entry, params.unproven_only)
222                && filter_min_score(index, entry, params.min_score)
223                && filter_binding_gaps(entry, params.binding_gaps_only, binding)
224                && filter_min_level(entry, params.min_level.as_deref())
225                && filter_tier(entry, params.tier_filter)
226                && filter_class(entry, params.class_filter)
227                && filter_kind(entry, params.kind_filter)
228        })
229        .collect()
230}
231
232fn filter_kind(entry: &types::ContractEntry, kind: Option<crate::schema::ContractKind>) -> bool {
233    match kind {
234        Some(k) => entry.kind == k,
235        None => true,
236    }
237}
238
239fn filter_obligation(entry: &types::ContractEntry, obligation: Option<&String>) -> bool {
240    match obligation {
241        Some(ot) => entry.obligation_types.iter().any(|t| t == ot),
242        None => true,
243    }
244}
245
246fn filter_depends_on(entry: &types::ContractEntry, depends_on: Option<&String>) -> bool {
247    match depends_on {
248        Some(dep) => entry.depends_on.iter().any(|d| d == dep),
249        None => true,
250    }
251}
252
253fn filter_depended_by(
254    index: &ContractIndex,
255    entry: &types::ContractEntry,
256    depended_by: Option<&String>,
257) -> bool {
258    match depended_by {
259        Some(target) => index
260            .get_by_stem(target)
261            .is_some_and(|t| t.depends_on.contains(&entry.stem)),
262        None => true,
263    }
264}
265
266fn filter_min_score(
267    index: &ContractIndex,
268    entry: &types::ContractEntry,
269    min_score: Option<f64>,
270) -> bool {
271    let Some(threshold) = min_score else {
272        return true;
273    };
274    if let Some(cached) = index.cached_score(&entry.stem) {
275        return cached >= threshold;
276    }
277    query_enrich::build_score_info(entry).is_some_and(|s| s.composite >= threshold)
278}
279
280fn filter_binding_gaps(
281    entry: &types::ContractEntry,
282    gaps_only: bool,
283    binding: Option<&BindingRegistry>,
284) -> bool {
285    if !gaps_only {
286        return true;
287    }
288    let Some(binding) = binding else {
289        return false;
290    };
291    binding.bindings_for(&entry.stem).iter().any(|b| {
292        b.status == crate::binding::ImplStatus::NotImplemented
293            || b.status == crate::binding::ImplStatus::Partial
294    })
295}
296
297fn filter_unproven(entry: &types::ContractEntry, unproven_only: bool) -> bool {
298    if !unproven_only {
299        return true;
300    }
301    entry.obligation_count > entry.kani_count
302}
303
304fn filter_tier(entry: &types::ContractEntry, tier: Option<u8>) -> bool {
305    let Some(t) = tier else { return true };
306    registry::tier_of(&entry.stem) == t
307}
308
309fn filter_class(entry: &types::ContractEntry, class: Option<char>) -> bool {
310    let Some(c) = class else { return true };
311    registry::classes_of(&entry.stem).contains(&c)
312}
313
314fn filter_min_level(entry: &types::ContractEntry, min_level: Option<&str>) -> bool {
315    let Some(min) = min_level else { return true };
316    let threshold = query_enrich::parse_proof_level(min);
317    let path = std::path::Path::new(&entry.path);
318    let Ok(contract) = crate::schema::parse_contract(path) else {
319        return false;
320    };
321    let level = crate::proof_status::compute_proof_level(&contract, None);
322    level >= threshold
323}
324
325#[cfg(test)]
326mod tests {
327    include!("query_tests.rs");
328}
329#[cfg(test)]
330mod coverage_tests {
331    include!("query_tests_coverage.rs");
332}
333#[cfg(test)]
334mod render_tests {
335    include!("query_tests_render.rs");
336}