spec_execution/
lib.rs

1//! Typed spec and proof surface crate for generated artifact families.
2//!
3//! The crate keeps the historical compatibility name, but it does not claim
4//! a full execution runtime. It publishes spec/proof schemas and bounded
5//! evaluation artifacts for later admission elsewhere.
6
7use schemars::JsonSchema;
8use serde::{Deserialize, Serialize};
9use stack_ids::{
10    ContentDigest, GeneratedConformanceCorpusId, GeneratedInterpreterBundleId,
11    GeneratedMigrationPlanId, GeneratedSchemaBundleId, HumanVetoBundleId, MetaChallengeBundleId,
12    NormativeAstId, ProofEvaluationReceiptId, ProofObligationSetId, SelfHostingBuildReceiptId,
13    SpecBundleId,
14};
15
16pub use stack_ids::SurfaceStatus;
17
18pub const SPEC_BUNDLE_V1_SCHEMA: &str = "spec_bundle_v1";
19pub const NORMATIVE_AST_V1_SCHEMA: &str = "normative_ast_v1";
20pub const GENERATED_SCHEMA_BUNDLE_V1_SCHEMA: &str = "generated_schema_bundle_v1";
21pub const GENERATED_INTERPRETER_BUNDLE_V1_SCHEMA: &str = "generated_interpreter_bundle_v1";
22pub const GENERATED_CONFORMANCE_CORPUS_V1_SCHEMA: &str = "generated_conformance_corpus_v1";
23pub const GENERATED_MIGRATION_PLAN_V1_SCHEMA: &str = "generated_migration_plan_v1";
24pub const PROOF_OBLIGATION_SET_V1_SCHEMA: &str = "proof_obligation_set_v1";
25pub const PROOF_EVALUATION_RECEIPT_V1_SCHEMA: &str = "proof_evaluation_receipt_v1";
26pub const HUMAN_VETO_BUNDLE_V1_SCHEMA: &str = "human_veto_bundle_v1";
27pub const META_CHALLENGE_BUNDLE_V1_SCHEMA: &str = "meta_challenge_bundle_v1";
28pub const SELF_HOSTING_BUILD_RECEIPT_V1_SCHEMA: &str = "self_hosting_build_receipt_v1";
29
30#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, JsonSchema)]
31pub struct SpecBundleV1 {
32    pub schema_version: String,
33    pub spec_bundle_id: SpecBundleId,
34    pub spec_name: String,
35    pub canonical_owner: String,
36    pub publication_status: SurfaceStatus,
37}
38
39#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, JsonSchema)]
40pub struct NormativeAstNodeV1 {
41    pub node_id: String,
42    pub kind: String,
43    pub normative_text: String,
44}
45
46#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, JsonSchema)]
47pub struct NormativeASTV1 {
48    pub schema_version: String,
49    pub normative_ast_id: NormativeAstId,
50    pub spec_bundle_id: SpecBundleId,
51    #[serde(default)]
52    pub nodes: Vec<NormativeAstNodeV1>,
53    pub publication_status: SurfaceStatus,
54}
55
56#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, JsonSchema)]
57pub struct GeneratedSchemaFileV1 {
58    pub path: String,
59    pub digest: ContentDigest,
60    #[serde(default)]
61    pub source_node_ids: Vec<String>,
62}
63
64#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize, JsonSchema)]
65#[serde(rename_all = "snake_case")]
66pub enum GeneratedAdmissionState {
67    AdvisoryOnly,
68    NonAdmitted,
69    HumanVetoed,
70}
71
72#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, JsonSchema)]
73pub struct GeneratedSchemaBundleV1 {
74    pub schema_version: String,
75    pub generated_schema_bundle_id: GeneratedSchemaBundleId,
76    pub spec_bundle_id: SpecBundleId,
77    pub normative_ast_id: NormativeAstId,
78    pub proof_obligation_set_id: ProofObligationSetId,
79    pub schema_family: String,
80    #[serde(default)]
81    pub generated_files: Vec<GeneratedSchemaFileV1>,
82    pub admission_state: GeneratedAdmissionState,
83    pub advisory_only: bool,
84    pub generated_at: String,
85}
86
87#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, JsonSchema)]
88pub struct GeneratedInterpreterBundleV1 {
89    pub schema_version: String,
90    pub generated_interpreter_bundle_id: GeneratedInterpreterBundleId,
91    pub spec_bundle_id: SpecBundleId,
92    pub normative_ast_id: NormativeAstId,
93    pub proof_obligation_set_id: ProofObligationSetId,
94    pub generated_schema_bundle_id: GeneratedSchemaBundleId,
95    pub horizon_only: bool,
96    pub generated_at: String,
97}
98
99#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, JsonSchema)]
100pub struct GeneratedConformanceCorpusV1 {
101    pub schema_version: String,
102    pub generated_conformance_corpus_id: GeneratedConformanceCorpusId,
103    pub spec_bundle_id: SpecBundleId,
104    pub normative_ast_id: NormativeAstId,
105    pub proof_obligation_set_id: ProofObligationSetId,
106    pub generated_schema_bundle_id: GeneratedSchemaBundleId,
107    pub horizon_only: bool,
108    pub generated_at: String,
109}
110
111#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, JsonSchema)]
112pub struct GeneratedMigrationPlanV1 {
113    pub schema_version: String,
114    pub generated_migration_plan_id: GeneratedMigrationPlanId,
115    pub spec_bundle_id: SpecBundleId,
116    pub normative_ast_id: NormativeAstId,
117    pub proof_obligation_set_id: ProofObligationSetId,
118    pub generated_schema_bundle_id: GeneratedSchemaBundleId,
119    pub horizon_only: bool,
120    pub generated_at: String,
121}
122
123#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, JsonSchema)]
124pub struct ProofObligationV1 {
125    pub obligation_id: String,
126    pub description: String,
127    pub satisfied: bool,
128    pub blocking: bool,
129}
130
131#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, JsonSchema)]
132pub struct ProofObligationSetV1 {
133    pub schema_version: String,
134    pub proof_obligation_set_id: ProofObligationSetId,
135    pub spec_bundle_id: SpecBundleId,
136    pub normative_ast_id: NormativeAstId,
137    #[serde(default)]
138    pub obligations: Vec<ProofObligationV1>,
139}
140
141#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, JsonSchema)]
142pub struct ProofEvaluationReceiptV1 {
143    pub schema_version: String,
144    pub proof_evaluation_receipt_id: ProofEvaluationReceiptId,
145    pub proof_obligation_set_id: ProofObligationSetId,
146    #[serde(default, skip_serializing_if = "Option::is_none")]
147    pub generated_schema_bundle_id: Option<GeneratedSchemaBundleId>,
148    pub satisfied_count: usize,
149    #[serde(default)]
150    pub unsatisfied_blocking_obligations: Vec<String>,
151    pub admission_allowed: bool,
152    pub advisory_only: bool,
153    pub evaluated_at: String,
154}
155
156#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, JsonSchema)]
157pub struct HumanVetoBundleV1 {
158    pub schema_version: String,
159    pub human_veto_bundle_id: HumanVetoBundleId,
160    pub generated_schema_bundle_id: GeneratedSchemaBundleId,
161    pub reason: String,
162}
163
164#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, JsonSchema)]
165pub struct MetaChallengeBundleV1 {
166    pub schema_version: String,
167    pub meta_challenge_bundle_id: MetaChallengeBundleId,
168    pub generated_schema_bundle_id: GeneratedSchemaBundleId,
169    pub challenge_summary: String,
170    pub horizon_only: bool,
171}
172
173#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize, JsonSchema)]
174#[serde(rename_all = "snake_case")]
175pub enum GeneratedSurfaceGovernanceState {
176    AdvisoryBaseline,
177    ChallengePending,
178    HumanVetoed,
179}
180
181#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, JsonSchema)]
182pub struct SelfHostingBuildReceiptV1 {
183    pub schema_version: String,
184    pub self_hosting_build_receipt_id: SelfHostingBuildReceiptId,
185    pub spec_bundle_id: SpecBundleId,
186    pub generated_schema_bundle_id: GeneratedSchemaBundleId,
187    pub generated_interpreter_bundle_id: GeneratedInterpreterBundleId,
188    pub generated_conformance_corpus_id: GeneratedConformanceCorpusId,
189    pub generated_migration_plan_id: GeneratedMigrationPlanId,
190    pub proof_evaluation_receipt_id: ProofEvaluationReceiptId,
191    #[serde(default, skip_serializing_if = "Option::is_none")]
192    pub human_veto_bundle_id: Option<HumanVetoBundleId>,
193    #[serde(default, skip_serializing_if = "Option::is_none")]
194    pub meta_challenge_bundle_id: Option<MetaChallengeBundleId>,
195    pub governance_state: GeneratedSurfaceGovernanceState,
196    pub rollback_required: bool,
197    pub admission_allowed: bool,
198    pub advisory_only: bool,
199    #[serde(default)]
200    pub notes: Vec<String>,
201    pub generated_at: String,
202}
203
204#[derive(Debug, Clone, PartialEq, Eq)]
205pub struct GeneratedCompanionBundles {
206    pub schema_bundle: GeneratedSchemaBundleV1,
207    pub interpreter_bundle: GeneratedInterpreterBundleV1,
208    pub conformance_corpus: GeneratedConformanceCorpusV1,
209    pub migration_plan: GeneratedMigrationPlanV1,
210    pub proof_evaluation_receipt: ProofEvaluationReceiptV1,
211    pub self_hosting_build_receipt: SelfHostingBuildReceiptV1,
212}
213
214pub fn generate_schema_bundle(
215    spec: &SpecBundleV1,
216    ast: &NormativeASTV1,
217    obligations: &ProofObligationSetV1,
218    schema_family: impl Into<String>,
219    generated_at: impl Into<String>,
220) -> (GeneratedSchemaBundleV1, ProofEvaluationReceiptV1) {
221    let generated_at = generated_at.into();
222    let evaluated_at = generated_at.clone();
223    let schema_family = schema_family.into();
224    let blocking = obligations
225        .obligations
226        .iter()
227        .filter(|obligation| obligation.blocking && !obligation.satisfied)
228        .map(|obligation| obligation.obligation_id.clone())
229        .collect::<Vec<_>>();
230    let file_payload = serde_json::json!({
231        "spec_bundle_id": spec.spec_bundle_id,
232        "normative_ast_id": ast.normative_ast_id,
233        "source_node_ids": ast.nodes.iter().map(|node| node.node_id.clone()).collect::<Vec<_>>(),
234    });
235    let file = GeneratedSchemaFileV1 {
236        path: format!("generated/{schema_family}/schema.json"),
237        digest: ContentDigest::compute_json(&file_payload)
238            .unwrap_or_else(|e| {
239                tracing::warn!(error = %e, "schema file payload digest failed; using empty-digest fallback");
240                ContentDigest::compute_str("")
241            }),
242        source_node_ids: ast.nodes.iter().map(|node| node.node_id.clone()).collect(),
243    };
244
245    let bundle = GeneratedSchemaBundleV1 {
246        schema_version: GENERATED_SCHEMA_BUNDLE_V1_SCHEMA.into(),
247        generated_schema_bundle_id: GeneratedSchemaBundleId::generate(),
248        spec_bundle_id: spec.spec_bundle_id.clone(),
249        normative_ast_id: ast.normative_ast_id.clone(),
250        proof_obligation_set_id: obligations.proof_obligation_set_id.clone(),
251        schema_family,
252        generated_files: vec![file],
253        admission_state: GeneratedAdmissionState::AdvisoryOnly,
254        advisory_only: true,
255        generated_at,
256    };
257
258    let receipt = ProofEvaluationReceiptV1 {
259        schema_version: PROOF_EVALUATION_RECEIPT_V1_SCHEMA.into(),
260        proof_evaluation_receipt_id: ProofEvaluationReceiptId::generate(),
261        proof_obligation_set_id: obligations.proof_obligation_set_id.clone(),
262        generated_schema_bundle_id: Some(bundle.generated_schema_bundle_id.clone()),
263        satisfied_count: obligations
264            .obligations
265            .iter()
266            .filter(|obligation| obligation.satisfied)
267            .count(),
268        unsatisfied_blocking_obligations: blocking.clone(),
269        admission_allowed: blocking.is_empty(),
270        advisory_only: true,
271        evaluated_at,
272    };
273
274    (bundle, receipt)
275}
276
277pub fn generate_companion_bundles(
278    spec: &SpecBundleV1,
279    ast: &NormativeASTV1,
280    obligations: &ProofObligationSetV1,
281    schema_family: impl Into<String>,
282    generated_at: impl Into<String>,
283) -> GeneratedCompanionBundles {
284    let generated_at = generated_at.into();
285    let (schema_bundle, proof_evaluation_receipt) =
286        generate_schema_bundle(spec, ast, obligations, schema_family, generated_at.clone());
287    let interpreter_bundle = GeneratedInterpreterBundleV1 {
288        schema_version: GENERATED_INTERPRETER_BUNDLE_V1_SCHEMA.into(),
289        generated_interpreter_bundle_id: GeneratedInterpreterBundleId::generate(),
290        spec_bundle_id: spec.spec_bundle_id.clone(),
291        normative_ast_id: ast.normative_ast_id.clone(),
292        proof_obligation_set_id: obligations.proof_obligation_set_id.clone(),
293        generated_schema_bundle_id: schema_bundle.generated_schema_bundle_id.clone(),
294        horizon_only: true,
295        generated_at: generated_at.clone(),
296    };
297    let conformance_corpus = GeneratedConformanceCorpusV1 {
298        schema_version: GENERATED_CONFORMANCE_CORPUS_V1_SCHEMA.into(),
299        generated_conformance_corpus_id: GeneratedConformanceCorpusId::generate(),
300        spec_bundle_id: spec.spec_bundle_id.clone(),
301        normative_ast_id: ast.normative_ast_id.clone(),
302        proof_obligation_set_id: obligations.proof_obligation_set_id.clone(),
303        generated_schema_bundle_id: schema_bundle.generated_schema_bundle_id.clone(),
304        horizon_only: true,
305        generated_at: generated_at.clone(),
306    };
307    let migration_plan = GeneratedMigrationPlanV1 {
308        schema_version: GENERATED_MIGRATION_PLAN_V1_SCHEMA.into(),
309        generated_migration_plan_id: GeneratedMigrationPlanId::generate(),
310        spec_bundle_id: spec.spec_bundle_id.clone(),
311        normative_ast_id: ast.normative_ast_id.clone(),
312        proof_obligation_set_id: obligations.proof_obligation_set_id.clone(),
313        generated_schema_bundle_id: schema_bundle.generated_schema_bundle_id.clone(),
314        horizon_only: true,
315        generated_at: generated_at.clone(),
316    };
317    let self_hosting_build_receipt = establish_veto_challenge_baseline(
318        spec,
319        &schema_bundle,
320        &interpreter_bundle,
321        &conformance_corpus,
322        &migration_plan,
323        &proof_evaluation_receipt,
324        None,
325        None,
326        generated_at.clone(),
327    );
328
329    GeneratedCompanionBundles {
330        schema_bundle,
331        interpreter_bundle,
332        conformance_corpus,
333        migration_plan,
334        proof_evaluation_receipt,
335        self_hosting_build_receipt,
336    }
337}
338
339#[allow(clippy::too_many_arguments)]
340pub fn establish_veto_challenge_baseline(
341    spec: &SpecBundleV1,
342    schema_bundle: &GeneratedSchemaBundleV1,
343    interpreter_bundle: &GeneratedInterpreterBundleV1,
344    conformance_corpus: &GeneratedConformanceCorpusV1,
345    migration_plan: &GeneratedMigrationPlanV1,
346    proof_evaluation_receipt: &ProofEvaluationReceiptV1,
347    human_veto: Option<&HumanVetoBundleV1>,
348    meta_challenge: Option<&MetaChallengeBundleV1>,
349    generated_at: impl Into<String>,
350) -> SelfHostingBuildReceiptV1 {
351    let governance_state = if human_veto.is_some() {
352        GeneratedSurfaceGovernanceState::HumanVetoed
353    } else if meta_challenge.is_some() {
354        GeneratedSurfaceGovernanceState::ChallengePending
355    } else {
356        GeneratedSurfaceGovernanceState::AdvisoryBaseline
357    };
358    let admission_allowed = proof_evaluation_receipt.admission_allowed && human_veto.is_none();
359
360    SelfHostingBuildReceiptV1 {
361        schema_version: SELF_HOSTING_BUILD_RECEIPT_V1_SCHEMA.into(),
362        self_hosting_build_receipt_id: SelfHostingBuildReceiptId::generate(),
363        spec_bundle_id: spec.spec_bundle_id.clone(),
364        generated_schema_bundle_id: schema_bundle.generated_schema_bundle_id.clone(),
365        generated_interpreter_bundle_id: interpreter_bundle.generated_interpreter_bundle_id.clone(),
366        generated_conformance_corpus_id: conformance_corpus.generated_conformance_corpus_id.clone(),
367        generated_migration_plan_id: migration_plan.generated_migration_plan_id.clone(),
368        proof_evaluation_receipt_id: proof_evaluation_receipt.proof_evaluation_receipt_id.clone(),
369        human_veto_bundle_id: human_veto.map(|bundle| bundle.human_veto_bundle_id.clone()),
370        meta_challenge_bundle_id: meta_challenge
371            .map(|bundle| bundle.meta_challenge_bundle_id.clone()),
372        governance_state,
373        rollback_required: human_veto.is_some() || meta_challenge.is_some(),
374        admission_allowed,
375        advisory_only: true,
376        notes: vec![
377            "generated surfaces remain non-admitted until proof obligations pass and a human lane accepts them".into(),
378            "self-hosting status does not override veto, challenge, or rollback obligations".into(),
379        ],
380        generated_at: generated_at.into(),
381    }
382}
spec_execution/lib.rs

spec_execution/
lib.rs
