higher_graphen_core/extension/
derivation.rs

1use super::common::LifecycleStatus;
2use crate::text::normalize_required_text;
3use crate::{CoreError, Id, Provenance, Result, ReviewStatus};
4use serde::{Deserialize, Serialize};
5
6/// Inference verifier category for a derivation.
7#[derive(Clone, Copy, Debug, Deserialize, Eq, Hash, PartialEq, Serialize)]
8#[serde(rename_all = "snake_case")]
9pub enum VerifierKind {
10    /// Human review validated the inference.
11    HumanReview,
12    /// Schema validation checked the inference.
13    SchemaValidator,
14    /// A proof checker validated the inference.
15    ProofChecker,
16    /// A test run checked the inference.
17    TestRun,
18    /// Static analysis checked the inference.
19    StaticAnalysis,
20    /// A custom engine checked the inference.
21    CustomEngine,
22}
23
24/// Verifier used by a derivation.
25#[derive(Clone, Debug, Deserialize, PartialEq, Serialize)]
26#[serde(deny_unknown_fields)]
27pub struct Verifier {
28    /// Verifier kind.
29    pub kind: VerifierKind,
30    /// Verifier reference, command, URL, or engine id.
31    pub reference: String,
32}
33
34impl Verifier {
35    /// Creates a verifier with a validated reference.
36    pub fn new(kind: VerifierKind, reference: impl Into<String>) -> Result<Self> {
37        Ok(Self {
38            kind,
39            reference: normalize_required_text("verifier.reference", reference)?,
40        })
41    }
42}
43
44/// Status of derivation verification.
45#[derive(Clone, Copy, Debug, Deserialize, Eq, Hash, PartialEq, Serialize)]
46#[serde(rename_all = "snake_case")]
47pub enum VerificationStatus {
48    /// No verifier or review has checked the inference.
49    Unverified,
50    /// Machine verification succeeded.
51    MachineChecked,
52    /// Human review succeeded.
53    HumanReviewed,
54    /// Verification failed.
55    Failed,
56    /// Replaced by a later derivation.
57    Superseded,
58}
59
60/// Derivation failure mode.
61#[derive(Clone, Copy, Debug, Deserialize, Eq, Hash, PartialEq, Serialize)]
62#[serde(rename_all = "snake_case")]
63pub enum DerivationFailureMode {
64    /// A required premise is missing.
65    MissingPremise,
66    /// The inference rule is invalid.
67    InvalidRule,
68    /// The rule is applied outside its scope.
69    OutOfScopeRule,
70    /// A witness contradicts the derivation.
71    ContradictedByWitness,
72    /// The derivation is circular.
73    CircularDerivation,
74    /// The conclusion jumps beyond the premises and rule.
75    UnsupportedJump,
76    /// The verifier could not be run.
77    VerifierUnavailable,
78    /// No failure is known.
79    None,
80}
81
82/// Inference rule applied by a derivation.
83#[derive(Clone, Debug, Deserialize, PartialEq, Serialize)]
84#[serde(deny_unknown_fields)]
85pub struct InferenceRule {
86    /// Rule identifier.
87    pub id: Id,
88    /// Rule name.
89    pub name: String,
90    /// Contexts where the rule may be applied.
91    #[serde(default, skip_serializing_if = "Vec::is_empty")]
92    pub rule_scope_contexts: Vec<Id>,
93    /// Interpretation package that owns the rule.
94    #[serde(skip_serializing_if = "Option::is_none")]
95    pub interpretation_package: Option<Id>,
96}
97
98impl InferenceRule {
99    /// Creates an inference rule with a validated name.
100    pub fn new(id: Id, name: impl Into<String>) -> Result<Self> {
101        Ok(Self {
102            id,
103            name: normalize_required_text("inference_rule.name", name)?,
104            rule_scope_contexts: Vec::new(),
105            interpretation_package: None,
106        })
107    }
108
109    fn has_scope(&self) -> bool {
110        !self.rule_scope_contexts.is_empty() || self.interpretation_package.is_some()
111    }
112}
113
114/// Structured inference from premises to a conclusion.
115#[derive(Clone, Debug, Deserialize, PartialEq, Serialize)]
116#[serde(deny_unknown_fields)]
117pub struct Derivation {
118    /// Derivation identifier.
119    pub id: Id,
120    /// Derived conclusion cell.
121    pub conclusion: Id,
122    /// Premise cells.
123    #[serde(default, skip_serializing_if = "Vec::is_empty")]
124    pub premises: Vec<Id>,
125    /// Inference rule applied.
126    pub inference_rule: InferenceRule,
127    /// Supporting warrants.
128    #[serde(default, skip_serializing_if = "Vec::is_empty")]
129    pub warrants: Vec<Id>,
130    /// Premises explicitly excluded from the derivation.
131    #[serde(default, skip_serializing_if = "Vec::is_empty")]
132    pub excluded_premises: Vec<Id>,
133    /// Counterexample witnesses.
134    #[serde(default, skip_serializing_if = "Vec::is_empty")]
135    pub counterexamples: Vec<Id>,
136    /// Verifier used to check the derivation.
137    #[serde(skip_serializing_if = "Option::is_none")]
138    pub verifier: Option<Verifier>,
139    /// Verification state.
140    pub verification_status: VerificationStatus,
141    /// Known failure mode.
142    pub failure_mode: DerivationFailureMode,
143    /// Derivation provenance.
144    pub provenance: Provenance,
145    /// Review lifecycle state.
146    pub review_status: LifecycleStatus,
147}
148
149impl Derivation {
150    /// Creates an unverified derivation candidate.
151    pub fn candidate(
152        id: Id,
153        conclusion: Id,
154        premises: Vec<Id>,
155        inference_rule: InferenceRule,
156        provenance: Provenance,
157    ) -> Self {
158        Self {
159            id,
160            conclusion,
161            premises,
162            inference_rule,
163            warrants: Vec::new(),
164            excluded_premises: Vec::new(),
165            counterexamples: Vec::new(),
166            verifier: None,
167            verification_status: VerificationStatus::Unverified,
168            failure_mode: DerivationFailureMode::None,
169            provenance,
170            review_status: LifecycleStatus::Candidate,
171        }
172    }
173
174    /// Validates conditions required before treating the derivation as accepted.
175    pub fn validate_acceptance(&self) -> Result<()> {
176        if self
177            .premises
178            .iter()
179            .all(|premise| premise == &self.conclusion)
180        {
181            return Err(CoreError::malformed_field(
182                "premises",
183                "derivation cannot be circular over only the conclusion",
184            ));
185        }
186        if !self.inference_rule.has_scope() {
187            return Err(CoreError::malformed_field(
188                "inference_rule.rule_scope",
189                "accepted derivation requires a scoped inference rule",
190            ));
191        }
192        if self.failure_mode != DerivationFailureMode::None {
193            return Err(CoreError::malformed_field(
194                "failure_mode",
195                "accepted derivation requires no unresolved failure mode",
196            ));
197        }
198        if !self.counterexamples.is_empty() {
199            return Err(CoreError::malformed_field(
200                "counterexamples",
201                "accepted derivation cannot have unresolved counterexamples",
202            ));
203        }
204        match self.verification_status {
205            VerificationStatus::MachineChecked | VerificationStatus::HumanReviewed => {}
206            _ => {
207                return Err(CoreError::malformed_field(
208                    "verification_status",
209                    "accepted derivation requires machine_checked or human_reviewed status",
210                ));
211            }
212        }
213        if self.verifier.is_none() && self.provenance.review_status != ReviewStatus::Accepted {
214            return Err(CoreError::malformed_field(
215                "verifier",
216                "accepted derivation requires verifier or explicit accepted review",
217            ));
218        }
219        Ok(())
220    }
221}
higher_graphen_core/extension/derivation.rs

higher_graphen_core/extension/
derivation.rs
