provable_contracts/query/
types.rs

1//! Types for the contract query engine.
2
3use crate::schema::ContractKind;
4use serde::{Deserialize, Serialize};
5
6/// How to interpret the query string.
7#[derive(Debug, Clone, PartialEq, Eq)]
8pub enum SearchMode {
9    /// BM25 semantic ranking over corpus (default).
10    Semantic,
11    /// Regex match against all string fields.
12    Regex,
13    /// Exact substring match (case-insensitive by default).
14    Literal,
15}
16
17/// A single entry in the contract index.
18#[derive(Debug, Clone, Serialize, Deserialize)]
19pub struct ContractEntry {
20    pub stem: String,
21    pub path: String,
22    pub description: String,
23    pub equations: Vec<String>,
24    pub obligation_types: Vec<String>,
25    pub properties: Vec<String>,
26    pub references: Vec<String>,
27    pub depends_on: Vec<String>,
28    pub is_registry: bool,
29    #[serde(default)]
30    pub kind: ContractKind,
31    pub obligation_count: usize,
32    pub falsification_count: usize,
33    pub kani_count: usize,
34    /// Concatenated searchable text for BM25.
35    pub corpus_text: String,
36}
37
38/// Parameters controlling a query.
39#[derive(Debug, Clone)]
40#[allow(clippy::struct_excessive_bools)]
41pub struct QueryParams {
42    pub query: String,
43    pub mode: SearchMode,
44    pub case_sensitive: bool,
45    pub limit: usize,
46    pub obligation_filter: Option<String>,
47    pub min_score: Option<f64>,
48    pub depends_on: Option<String>,
49    pub depended_by: Option<String>,
50    pub unproven_only: bool,
51    pub show_score: bool,
52    pub show_graph: bool,
53    pub show_paper: bool,
54    pub show_proof_status: bool,
55    pub show_binding: bool,
56    pub binding_path: Option<String>,
57    pub binding_gaps_only: bool,
58    pub show_diff: bool,
59    pub show_pagerank: bool,
60    pub show_call_sites: bool,
61    pub show_violations: bool,
62    pub show_coverage_map: bool,
63    pub min_level: Option<String>,
64    /// Filter cross-project results to a named project (e.g., "aprender").
65    pub project_filter: Option<String>,
66    /// Explicit additional project path to include in cross-project scan.
67    pub include_project: Option<String>,
68    /// Force cross-project scan even when no cross-project flags are set.
69    pub all_projects: bool,
70    /// Filter by contract tier (1-7).
71    pub tier_filter: Option<u8>,
72    /// Filter by kernel equivalence class (A-E).
73    pub class_filter: Option<char>,
74    /// Filter by contract kind (kernel, registry, model-family, pattern, schema).
75    pub kind_filter: Option<ContractKind>,
76}
77
78impl Default for QueryParams {
79    fn default() -> Self {
80        Self {
81            query: String::new(),
82            mode: SearchMode::Semantic,
83            case_sensitive: false,
84            limit: 10,
85            obligation_filter: None,
86            min_score: None,
87            depends_on: None,
88            depended_by: None,
89            unproven_only: false,
90            show_score: false,
91            show_graph: false,
92            show_paper: false,
93            show_proof_status: false,
94            show_binding: false,
95            binding_path: None,
96            binding_gaps_only: false,
97            show_diff: false,
98            show_pagerank: false,
99            show_call_sites: false,
100            show_violations: false,
101            show_coverage_map: false,
102            min_level: None,
103            project_filter: None,
104            include_project: None,
105            all_projects: false,
106            tier_filter: None,
107            class_filter: None,
108            kind_filter: None,
109        }
110    }
111}
112
113/// A single query result with relevance score and optional enrichment.
114#[derive(Debug, Clone, Serialize)]
115pub struct QueryResult {
116    pub rank: usize,
117    pub stem: String,
118    pub path: String,
119    pub relevance: f64,
120    pub description: String,
121    pub kind: ContractKind,
122    pub equations: Vec<String>,
123    pub obligation_count: usize,
124    pub references: Vec<String>,
125    pub depends_on: Vec<String>,
126    #[serde(skip_serializing_if = "Vec::is_empty")]
127    pub depended_by: Vec<String>,
128    #[serde(skip_serializing_if = "Option::is_none")]
129    pub score: Option<ScoreInfo>,
130    #[serde(skip_serializing_if = "Option::is_none")]
131    pub proof_status: Option<ProofStatusInfo>,
132    #[serde(skip_serializing_if = "Vec::is_empty")]
133    pub bindings: Vec<EquationBinding>,
134    #[serde(skip_serializing_if = "Option::is_none")]
135    pub diff: Option<DiffInfo>,
136    #[serde(skip_serializing_if = "Option::is_none")]
137    pub pagerank: Option<f64>,
138    #[serde(skip_serializing_if = "Vec::is_empty")]
139    pub call_sites: Vec<CallSiteInfo>,
140    #[serde(skip_serializing_if = "Vec::is_empty")]
141    pub violations: Vec<ViolationInfo>,
142    #[serde(skip_serializing_if = "Vec::is_empty")]
143    pub coverage_map: Vec<ProjectCoverage>,
144}
145
146/// Cross-project call site for a contract.
147#[derive(Debug, Clone, Serialize)]
148pub struct CallSiteInfo {
149    pub project: String,
150    pub file: String,
151    pub line: u32,
152    pub equation: Option<String>,
153}
154
155/// A contract violation detected in a consumer project.
156#[derive(Debug, Clone, Serialize)]
157pub struct ViolationInfo {
158    pub project: String,
159    pub kind: String,
160    pub detail: String,
161}
162
163/// Per-project coverage summary for a contract.
164#[derive(Debug, Clone, Serialize)]
165pub struct ProjectCoverage {
166    pub project: String,
167    pub call_sites: usize,
168    pub binding_refs: usize,
169    pub binding_implemented: usize,
170    pub binding_total: usize,
171}
172
173/// Inline score info for enrichment.
174#[derive(Debug, Clone, Serialize)]
175pub struct ScoreInfo {
176    pub composite: f64,
177    pub grade: String,
178    pub spec_depth: f64,
179    pub falsification: f64,
180    pub kani: f64,
181    pub lean: f64,
182    pub binding: f64,
183}
184
185/// Inline proof status info for enrichment.
186#[derive(Debug, Clone, Serialize)]
187pub struct ProofStatusInfo {
188    pub level: String,
189    pub obligations: u32,
190    pub falsification_tests: u32,
191    pub kani_harnesses: u32,
192    pub lean_proved: u32,
193}
194
195/// Git diff summary for a contract.
196#[derive(Debug, Clone, Serialize)]
197pub struct DiffInfo {
198    pub last_modified: String,
199    pub days_ago: u64,
200    pub commit_hash: String,
201}
202
203/// Binding status for a single equation.
204#[derive(Debug, Clone, Serialize)]
205pub struct EquationBinding {
206    pub equation: String,
207    pub status: String,
208    #[serde(skip_serializing_if = "Option::is_none")]
209    pub module_path: Option<String>,
210}
211
212/// Output of a query execution.
213#[derive(Debug, Clone, Serialize)]
214pub struct QueryOutput {
215    pub query: String,
216    pub total_matches: usize,
217    pub results: Vec<QueryResult>,
218}
provable_contracts/query/types.rs

provable_contracts/query/
types.rs
