aristo_core/index/
enums.rs

1//! Enum types for `.aristo/index.toml`.
2
3use schemars::JsonSchema;
4use serde::{Deserialize, Serialize};
5
6/// Annotation kind: `intent` (verifiable claim about code) or `assume`
7/// (external invariant the code relies on, taken as given).
8#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize, JsonSchema)]
9#[serde(rename_all = "lowercase")]
10pub enum AnnotationKind {
11    Intent,
12    Assume,
13}
14
15/// Current verification state. The wire form uses kebab-case to keep
16/// `pending-deepen` readable on disk.
17#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize, JsonSchema)]
18#[serde(rename_all = "kebab-case")]
19pub enum Status {
20    /// Verified at the strongest method available; signature is current.
21    Verified,
22    /// Verified via assertion-style testing (mined assertions, free or paid).
23    Tested,
24    /// Verified via neural reasoning (LLM-based).
25    Neural,
26    /// Was verified at a prior code state; current `body_hash` differs from
27    /// the signed outcome. Sig still valid; only the code drifted.
28    Stale,
29    /// `verified_outcome.commit_hash` is not in this repository's history.
30    /// Most likely cause: index entry copied from another repo (B5b).
31    Orphan,
32    /// `verified_outcome` does not verify against any bundled public key —
33    /// either tampered or signed by a revoked/unknown key (B5b).
34    Forged,
35    /// Has not yet been verified, or was reverted to unknown after a rename
36    /// or rebind operation invalidated the prior signature.
37    Unknown,
38    /// Sig is valid but commit ancestry could not be confirmed because the
39    /// outcome's commit falls outside a shallow checkout's window (B5b).
40    PendingDeepen,
41    /// Verification produced a counterexample — the property does NOT
42    /// hold under the cited code/text version. Terminal state: stays
43    /// Counterexample until either `body_hash` drifts (→ Stale) or the
44    /// intent text is rewritten to exclude the refuted case. There is
45    /// NO accept-counterexample flow; counterexamples are loud and
46    /// surface on every `aristo stamp` until the user fixes them.
47    Counterexample,
48    /// Verification was inconclusive — the verifier could not discharge
49    /// the proof's gap and queued one or more suggested annotations the
50    /// user could add to close it. Distinct from Unknown (which means
51    /// "never attempted") so the skip logic can tell "we tried and got
52    /// stuck" from "we haven't tried yet." Stays Inconclusive until
53    /// either the source drifts (→ Stale via the body-drift rule), the
54    /// user adopts a queued suggestion (→ re-verify), or the user
55    /// explicitly re-runs with `--rerun`.
56    Inconclusive,
57}
58
59/// `verify` field value. Mixed-type per design (G1):
60///
61/// - `false` (TOML bool): documentation only; no check ever runs.
62/// - `true` (TOML bool): resolves to project default in `aristo.toml [verify] default_method`.
63/// - one of `"neural"`, `"test"`, `"full"` (TOML string): named method.
64#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize, JsonSchema)]
65#[serde(untagged)]
66pub enum VerifyLevel {
67    Bool(bool),
68    Method(VerifyMethod),
69}
70
71/// Named verification methods (the string form of [`VerifyLevel`]).
72#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize, JsonSchema)]
73#[serde(rename_all = "lowercase")]
74pub enum VerifyMethod {
75    Neural,
76    Test,
77    Full,
78}
79
80/// What syntactic region an annotation covers. Determines the body region
81/// hashed for staleness detection (per B3) and the scope a `"test"`-mode
82/// assertion is injected over.
83#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize, JsonSchema)]
84#[serde(rename_all = "snake_case")]
85pub enum CoveredRegion {
86    /// Whole function body (most common; α-form attribute on a fn).
87    Function,
88    /// A single statement (β-form macro before a stmt or loop).
89    Statement,
90    /// Every method in an `impl` block.
91    ImplMethods,
92    /// The inline body of a module item.
93    ModuleInlineBody,
94    /// A struct or enum item.
95    Type,
96    /// A struct field or enum variant.
97    Field,
98    /// The crate root.
99    Crate,
100    /// A trait declaration.
101    Trait,
102}
103
104#[cfg(test)]
105mod tests {
106    use super::*;
107
108    #[test]
109    fn annotation_kind_round_trips_lowercase() {
110        let v = serde_json::to_value(AnnotationKind::Intent).unwrap();
111        assert_eq!(v, serde_json::json!("intent"));
112        let back: AnnotationKind = serde_json::from_value(v).unwrap();
113        assert_eq!(back, AnnotationKind::Intent);
114    }
115
116    #[test]
117    fn status_pending_deepen_is_kebab_case() {
118        let v = serde_json::to_value(Status::PendingDeepen).unwrap();
119        assert_eq!(v, serde_json::json!("pending-deepen"));
120        let back: Status = serde_json::from_value(serde_json::json!("pending-deepen")).unwrap();
121        assert_eq!(back, Status::PendingDeepen);
122    }
123
124    #[test]
125    fn verify_level_accepts_bool_form() {
126        let level: VerifyLevel = serde_json::from_value(serde_json::json!(false)).unwrap();
127        assert_eq!(level, VerifyLevel::Bool(false));
128        let level: VerifyLevel = serde_json::from_value(serde_json::json!(true)).unwrap();
129        assert_eq!(level, VerifyLevel::Bool(true));
130    }
131
132    #[test]
133    fn verify_level_accepts_named_method_form() {
134        let level: VerifyLevel = serde_json::from_value(serde_json::json!("full")).unwrap();
135        assert_eq!(level, VerifyLevel::Method(VerifyMethod::Full));
136    }
137
138    #[test]
139    fn verify_level_rejects_unknown_string() {
140        let result: Result<VerifyLevel, _> = serde_json::from_value(serde_json::json!("partial"));
141        assert!(result.is_err());
142    }
143
144    #[test]
145    fn covered_region_uses_snake_case() {
146        let v = serde_json::to_value(CoveredRegion::ImplMethods).unwrap();
147        assert_eq!(v, serde_json::json!("impl_methods"));
148        let v = serde_json::to_value(CoveredRegion::ModuleInlineBody).unwrap();
149        assert_eq!(v, serde_json::json!("module_inline_body"));
150    }
151
152    #[test]
153    fn unknown_status_value_is_rejected() {
154        let result: Result<Status, _> = serde_json::from_value(serde_json::json!("partial"));
155        assert!(result.is_err());
156    }
157}
aristo_core/index/enums.rs

aristo_core/index/
enums.rs
