Skip to main content

omena_abstract_value/
cascade_family.rs

1use crate::{ABSTRACT_VALUE_CASCADE_FAMILY_CLAIM_LEVEL_V0, AbstractPropertyValueV0};
2use serde::Serialize;
3use std::collections::{BTreeMap, BTreeSet};
4
5/// Research-staged cascade-family substrate for M6 positioning.
6///
7/// This is intentionally framing-neutral: it records context-indexed value
8/// families and restriction morphisms without claiming a categorical gluing
9/// theorem or committing paper-stage terminology.
10#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
11#[serde(rename_all = "camelCase")]
12pub struct CascadeValueFamilyV0 {
13    pub schema_version: &'static str,
14    pub product: &'static str,
15    pub framing: &'static str,
16    pub claim_level: &'static str,
17    pub property_name: String,
18    pub supported_readings: Vec<&'static str>,
19    pub context_value_count: usize,
20    pub restriction_map_count: usize,
21    pub property_consistent: bool,
22    pub dangling_restriction_count: usize,
23    pub theorem_claimed: bool,
24    pub members: Vec<CascadeValueFamilyMemberV0>,
25    pub restriction_maps: Vec<CascadeRestrictionMapV0>,
26}
27
28#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Serialize)]
29#[serde(rename_all = "camelCase")]
30pub struct CascadeContextV0 {
31    pub id: String,
32    #[serde(skip_serializing_if = "Option::is_none")]
33    pub parent_id: Option<String>,
34    pub selectors: Vec<String>,
35    pub conditions: Vec<String>,
36    pub layers: Vec<String>,
37}
38
39#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
40#[serde(rename_all = "camelCase")]
41pub struct CascadeValueFamilyMemberV0 {
42    pub context: CascadeContextV0,
43    pub value: AbstractPropertyValueV0,
44}
45
46#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Serialize)]
47#[serde(rename_all = "camelCase")]
48pub struct CascadeRestrictionMapV0 {
49    pub parent_context_id: String,
50    pub child_context_id: String,
51    pub morphism: CascadeMorphismV0,
52}
53
54#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Serialize)]
55#[serde(rename_all = "camelCase")]
56pub struct CascadeMorphismV0 {
57    pub kind: &'static str,
58    pub direction: &'static str,
59    pub preserves_property_name: bool,
60    pub evidence: Vec<&'static str>,
61}
62
63#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
64#[serde(rename_all = "camelCase")]
65pub struct CascadeStalkEvaluationV0 {
66    pub schema_version: &'static str,
67    pub product: &'static str,
68    pub claim_level: &'static str,
69    pub property_name: String,
70    pub requested_context_id: String,
71    pub requested_context_exists: bool,
72    #[serde(skip_serializing_if = "Option::is_none")]
73    pub resolved_context_id: Option<String>,
74    pub restriction_path: Vec<String>,
75    pub used_restriction_map_count: usize,
76    pub bounded_by_context_count: usize,
77    pub bounded_resolution_ready: bool,
78    pub theorem_claimed: bool,
79    #[serde(skip_serializing_if = "Option::is_none")]
80    pub value: Option<AbstractPropertyValueV0>,
81    pub resolved: bool,
82    #[serde(skip_serializing_if = "Option::is_none")]
83    pub blocked_reason: Option<&'static str>,
84}
85
86#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
87#[serde(rename_all = "camelCase")]
88pub struct CascadeRestrictionCycleSummaryV0 {
89    pub schema_version: &'static str,
90    pub product: &'static str,
91    pub claim_level: &'static str,
92    pub cycle_detection_model: &'static str,
93    pub context_count: usize,
94    pub restriction_map_count: usize,
95    pub cycle_count: usize,
96    pub cycles: Vec<CascadeRestrictionCycleV0>,
97    pub theorem_claimed: bool,
98}
99
100#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Serialize)]
101#[serde(rename_all = "camelCase")]
102pub struct CascadeRestrictionCycleV0 {
103    pub path: Vec<String>,
104}
105
106pub fn summarize_context_indexed_cascade_value_family_v0(
107    property_name: impl Into<String>,
108    members: Vec<CascadeValueFamilyMemberV0>,
109    restriction_maps: Vec<CascadeRestrictionMapV0>,
110) -> CascadeValueFamilyV0 {
111    let property_name = property_name.into();
112    let mut members = members;
113    members.sort_by(|left, right| left.context.id.cmp(&right.context.id));
114    members.dedup_by(|left, right| left.context.id == right.context.id);
115
116    let mut restriction_maps = restriction_maps;
117    restriction_maps.sort();
118    restriction_maps.dedup();
119
120    let context_ids = members
121        .iter()
122        .map(|member| member.context.id.as_str())
123        .collect::<BTreeSet<_>>();
124    let property_consistent = members
125        .iter()
126        .all(|member| property_value_name(&member.value) == property_name);
127    let dangling_restriction_count = restriction_maps
128        .iter()
129        .filter(|restriction| {
130            !context_ids.contains(restriction.parent_context_id.as_str())
131                || !context_ids.contains(restriction.child_context_id.as_str())
132        })
133        .count();
134    let restriction_map_count = restriction_maps.len();
135
136    CascadeValueFamilyV0 {
137        schema_version: "0",
138        product: "omena-abstract-value.cascade-value-family",
139        framing: "framingNeutralCascadeFamily",
140        claim_level: ABSTRACT_VALUE_CASCADE_FAMILY_CLAIM_LEVEL_V0,
141        property_name,
142        supported_readings: vec!["restrictionMapCompatible", "aggregationCompatible"],
143        context_value_count: members.len(),
144        restriction_map_count,
145        property_consistent,
146        dangling_restriction_count,
147        theorem_claimed: false,
148        members,
149        restriction_maps,
150    }
151}
152
153#[deprecated(
154    since = "0.4.0",
155    note = "use summarize_context_indexed_cascade_value_family_v0; removal is not before 1.0 and requires downstream migration plus zero audited non-compatibility uses"
156)]
157pub fn summarize_cascade_value_family_v0(
158    property_name: impl Into<String>,
159    members: Vec<CascadeValueFamilyMemberV0>,
160    restriction_maps: Vec<CascadeRestrictionMapV0>,
161) -> CascadeValueFamilyV0 {
162    let mut family =
163        summarize_context_indexed_cascade_value_family_v0(property_name, members, restriction_maps);
164    family.supported_readings = vec!["presheafCompatible", "cosheafCompatible"];
165    family
166}
167
168pub fn derive_context_indexed_cascade_restriction_maps_v0(
169    members: &[CascadeValueFamilyMemberV0],
170) -> Vec<CascadeRestrictionMapV0> {
171    let context_ids = members
172        .iter()
173        .map(|member| member.context.id.as_str())
174        .collect::<BTreeSet<_>>();
175    let mut maps = members
176        .iter()
177        .filter_map(|member| {
178            let parent_id = member.context.parent_id.as_deref()?;
179            context_ids
180                .contains(parent_id)
181                .then(|| CascadeRestrictionMapV0 {
182                    parent_context_id: parent_id.to_string(),
183                    child_context_id: member.context.id.clone(),
184                    morphism: context_indexed_cascade_refinement_morphism_v0(),
185                })
186        })
187        .collect::<Vec<_>>();
188    maps.sort();
189    maps.dedup();
190    maps
191}
192
193#[deprecated(
194    since = "0.4.0",
195    note = "use derive_context_indexed_cascade_restriction_maps_v0; removal is not before 1.0 and requires downstream migration plus zero audited non-compatibility uses"
196)]
197pub fn derive_cascade_restriction_maps_v0(
198    members: &[CascadeValueFamilyMemberV0],
199) -> Vec<CascadeRestrictionMapV0> {
200    derive_context_indexed_cascade_restriction_maps_v0(members)
201        .into_iter()
202        .map(|mut restriction| {
203            restriction.morphism.evidence = vec![
204                "contextIndexedValueFamily",
205                "parentChildCascadeContext",
206                "noSheafTheoremClaim",
207            ];
208            restriction
209        })
210        .collect()
211}
212
213pub fn context_indexed_cascade_refinement_morphism_v0() -> CascadeMorphismV0 {
214    CascadeMorphismV0 {
215        kind: "contextRefinement",
216        direction: "parentToChildRestriction",
217        preserves_property_name: true,
218        evidence: vec![
219            "contextIndexedValueFamily",
220            "parentChildCascadeContext",
221            "noCategoricalGluingTheoremClaim",
222        ],
223    }
224}
225
226#[deprecated(
227    since = "0.4.0",
228    note = "use context_indexed_cascade_refinement_morphism_v0; removal is not before 1.0 and requires downstream migration plus zero audited non-compatibility uses"
229)]
230pub fn cascade_context_refinement_morphism_v0() -> CascadeMorphismV0 {
231    let mut morphism = context_indexed_cascade_refinement_morphism_v0();
232    morphism.evidence = vec![
233        "contextIndexedValueFamily",
234        "parentChildCascadeContext",
235        "noSheafTheoremClaim",
236    ];
237    morphism
238}
239
240pub fn cascade_value_for_context<'a>(
241    family: &'a CascadeValueFamilyV0,
242    context_id: &str,
243) -> Option<&'a AbstractPropertyValueV0> {
244    family
245        .members
246        .iter()
247        .find(|member| member.context.id == context_id)
248        .map(|member| &member.value)
249}
250
251pub fn cascade_family_context_values(
252    family: &CascadeValueFamilyV0,
253) -> BTreeMap<String, AbstractPropertyValueV0> {
254    family
255        .members
256        .iter()
257        .map(|member| (member.context.id.clone(), member.value.clone()))
258        .collect()
259}
260
261pub fn evaluate_cascade_stalk_v0(
262    family: &CascadeValueFamilyV0,
263    context_id: &str,
264) -> CascadeStalkEvaluationV0 {
265    let values = cascade_family_context_values(family);
266    let requested_context_exists = values.contains_key(context_id);
267    let parent_by_child = family
268        .restriction_maps
269        .iter()
270        .map(|restriction| {
271            (
272                restriction.child_context_id.clone(),
273                restriction.parent_context_id.clone(),
274            )
275        })
276        .collect::<BTreeMap<_, _>>();
277    let mut restriction_path = Vec::new();
278    let mut current = context_id.to_string();
279    let bound = family.context_value_count.max(1);
280
281    for _ in 0..=bound {
282        restriction_path.push(current.clone());
283        if let Some(value) = values.get(&current)
284            && !property_value_is_bottom(value)
285        {
286            return CascadeStalkEvaluationV0 {
287                schema_version: "0",
288                product: "omena-abstract-value.cascade-stalk-evaluation",
289                claim_level: "fixtureWitnessBoundedCascadeStalkEvaluation",
290                property_name: family.property_name.clone(),
291                requested_context_id: context_id.to_string(),
292                requested_context_exists,
293                resolved_context_id: Some(current),
294                used_restriction_map_count: restriction_path.len().saturating_sub(1),
295                bounded_by_context_count: bound,
296                bounded_resolution_ready: true,
297                theorem_claimed: false,
298                value: Some(value.clone()),
299                resolved: true,
300                blocked_reason: None,
301                restriction_path,
302            };
303        }
304        let Some(parent) = parent_by_child.get(&current) else {
305            break;
306        };
307        current = parent.clone();
308    }
309
310    CascadeStalkEvaluationV0 {
311        schema_version: "0",
312        product: "omena-abstract-value.cascade-stalk-evaluation",
313        claim_level: "fixtureWitnessBoundedCascadeStalkEvaluation",
314        property_name: family.property_name.clone(),
315        requested_context_id: context_id.to_string(),
316        requested_context_exists,
317        resolved_context_id: None,
318        restriction_path,
319        used_restriction_map_count: 0,
320        bounded_by_context_count: bound,
321        bounded_resolution_ready: true,
322        theorem_claimed: false,
323        value: None,
324        resolved: false,
325        blocked_reason: Some("no non-bottom value found along bounded restriction path"),
326    }
327}
328
329pub fn summarize_cascade_restriction_cycles_v0(
330    family: &CascadeValueFamilyV0,
331) -> CascadeRestrictionCycleSummaryV0 {
332    let context_ids = family
333        .members
334        .iter()
335        .map(|member| member.context.id.clone())
336        .collect::<BTreeSet<_>>();
337    let mut adjacency = BTreeMap::<String, Vec<String>>::new();
338    for restriction in &family.restriction_maps {
339        adjacency
340            .entry(restriction.parent_context_id.clone())
341            .or_default()
342            .push(restriction.child_context_id.clone());
343    }
344    for targets in adjacency.values_mut() {
345        targets.sort();
346        targets.dedup();
347    }
348
349    let mut cycles = BTreeSet::<CascadeRestrictionCycleV0>::new();
350    for start in &context_ids {
351        collect_restriction_cycles_from(
352            start,
353            start,
354            &adjacency,
355            &mut Vec::new(),
356            &mut cycles,
357            family.context_value_count.max(1),
358        );
359    }
360    let cycles = cycles.into_iter().collect::<Vec<_>>();
361    CascadeRestrictionCycleSummaryV0 {
362        schema_version: "0",
363        product: "omena-abstract-value.cascade-restriction-cycle-summary",
364        claim_level: "fixtureWitnessBoundedRestrictionCycleDetection",
365        cycle_detection_model: "boundedRestrictionCycleWitnessNotCohomologyTheorem",
366        context_count: family.context_value_count,
367        restriction_map_count: family.restriction_map_count,
368        cycle_count: cycles.len(),
369        cycles,
370        theorem_claimed: false,
371    }
372}
373
374fn collect_restriction_cycles_from(
375    start: &str,
376    current: &str,
377    adjacency: &BTreeMap<String, Vec<String>>,
378    path: &mut Vec<String>,
379    cycles: &mut BTreeSet<CascadeRestrictionCycleV0>,
380    bound: usize,
381) {
382    if path.len() > bound {
383        return;
384    }
385    path.push(current.to_string());
386    if let Some(children) = adjacency.get(current) {
387        for child in children {
388            if child == start && path.len() > 1 {
389                let mut cycle = path.clone();
390                cycle.push(start.to_string());
391                cycles.insert(CascadeRestrictionCycleV0 {
392                    path: canonical_restriction_cycle(cycle),
393                });
394            } else if !path.contains(child) {
395                collect_restriction_cycles_from(start, child, adjacency, path, cycles, bound);
396            }
397        }
398    }
399    path.pop();
400}
401
402fn canonical_restriction_cycle(mut cycle: Vec<String>) -> Vec<String> {
403    if cycle.len() <= 2 {
404        return cycle;
405    }
406    cycle.pop();
407    let Some((start_index, _)) = cycle
408        .iter()
409        .enumerate()
410        .min_by(|left, right| left.1.cmp(right.1))
411    else {
412        return cycle;
413    };
414    let mut canonical = (0..cycle.len())
415        .map(|offset| cycle[(start_index + offset) % cycle.len()].clone())
416        .collect::<Vec<_>>();
417    canonical.push(canonical[0].clone());
418    canonical
419}
420
421fn property_value_is_bottom(value: &AbstractPropertyValueV0) -> bool {
422    matches!(value, AbstractPropertyValueV0::Bottom { .. })
423}
424
425fn property_value_name(value: &AbstractPropertyValueV0) -> &str {
426    match value {
427        AbstractPropertyValueV0::Bottom { property_name }
428        | AbstractPropertyValueV0::Exact { property_name, .. }
429        | AbstractPropertyValueV0::FiniteSet { property_name, .. }
430        | AbstractPropertyValueV0::CustomPropertyReference { property_name, .. }
431        | AbstractPropertyValueV0::Top { property_name } => property_name,
432    }
433}