1use crate::{ABSTRACT_VALUE_CASCADE_FAMILY_CLAIM_LEVEL_V0, AbstractPropertyValueV0};
2use serde::Serialize;
3use std::collections::{BTreeMap, BTreeSet};
4
5#[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(¤t)
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(¤t) 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}