type_bridge_schema/
safety_condition.rs

1//! Verifier-derived safety conditions for exact schema transitions.
2
3use std::cmp::Ordering;
4
5use serde::Serialize;
6use type_bridge_contract::codec::to_canonical_json;
7use type_bridge_contract::diagnostic::{Diagnostic, DiagnosticCategory, DiagnosticCode};
8use type_bridge_contract::fingerprint::{CanonicalizationVersion, Fingerprint, FingerprintDomain};
9use type_bridge_contract::id::{AttributeId, TypeId, TypeKind};
10use type_bridge_contract::managed_scope::SemanticProfileBinding;
11use type_bridge_contract::schema::{
12    AnnotationFact, AnnotationKindId, AnnotationSubjectId, CanonicalValueRange, CanonicalValueSet,
13    DeclaredIdentityFingerprint, DeclaredSchema, OwnsFactId, SchemaAnnotationValue, SchemaFact,
14    SchemaFactId, SchemaOperation, SchemaOperationKind, ValueFactId,
15};
16use type_bridge_contract::schema_lowering::SchemaLoweringProfileBinding;
17use type_bridge_contract::semantic_profile::{InterfaceKind, SemanticProfile};
18use type_bridge_contract::value::{CanonicalValue, Cardinality};
19
20use crate::{SafetyClass, classify_schema_operation_safety};
21
22/// Fingerprint domain for verifier-derived safety-condition identities.
23pub const SAFETY_CONDITION_FINGERPRINT_DOMAIN: &str = "typebridge.schema.safety-condition";
24/// Canonicalization identifier for verifier-derived safety conditions.
25pub const SAFETY_CONDITION_CANONICALIZATION: &str = "typebridge.safety-condition/v1";
26
27/// Registry-owned profiles which affect safety derivation and lowering identity.
28#[derive(Clone, Debug, Eq, PartialEq, Serialize)]
29pub struct SafetyDerivationProfile {
30    semantic: SemanticProfileBinding,
31    lowering: SchemaLoweringProfileBinding,
32}
33
34impl SafetyDerivationProfile {
35    /// Bind already registry-resolved semantic and lowering profiles.
36    pub fn new(
37        semantic: SemanticProfileBinding,
38        lowering: SchemaLoweringProfileBinding,
39    ) -> Result<Self, Diagnostic> {
40        SemanticProfile::resolve(semantic.id())?;
41        Ok(Self { semantic, lowering })
42    }
43
44    /// Return the exact semantic-profile binding.
45    pub const fn semantic(&self) -> &SemanticProfileBinding {
46        &self.semantic
47    }
48
49    /// Return the exact schema-lowering-profile binding.
50    pub const fn lowering(&self) -> &SchemaLoweringProfileBinding {
51        &self.lowering
52    }
53}
54
55/// Stable identity of canonical verifier-derived condition bytes.
56#[derive(Clone, Debug, Eq, PartialEq, Serialize)]
57#[serde(transparent)]
58pub struct SafetyConditionId(Fingerprint);
59
60impl SafetyConditionId {
61    fn compute(bytes: &[u8]) -> Result<Self, Diagnostic> {
62        Ok(Self(Fingerprint::compute(
63            FingerprintDomain::new(SAFETY_CONDITION_FINGERPRINT_DOMAIN)?,
64            CanonicalizationVersion::new(SAFETY_CONDITION_CANONICALIZATION)?,
65            None,
66            bytes,
67        )))
68    }
69
70    /// Return the generic domain-separated fingerprint.
71    pub const fn as_fingerprint(&self) -> &Fingerprint {
72        &self.0
73    }
74}
75
76/// Scalar annotation subject that can be represented by the assertion algebra.
77#[derive(Clone, Debug, Eq, PartialEq, Serialize)]
78#[serde(tag = "kind", content = "value", rename_all = "snake_case")]
79pub enum ScalarSafetySubject {
80    /// Every instance of one attribute value declaration.
81    Value(ValueFactId),
82    /// Values reached through one exact effective ownership.
83    Owns(OwnsFactId),
84}
85
86/// Missing feature or workflow required to express a safety condition honestly.
87#[derive(Clone, Copy, Debug, Eq, PartialEq, Serialize)]
88#[serde(rename_all = "snake_case")]
89pub enum SafetyConditionUnlock {
90    /// Canonical inequality over two thing bindings.
91    BindingDistinct,
92    /// Canonical regular-expression predicate over an attribute value.
93    ValueRegex,
94    /// An explicit data backfill or owner-approved transformation.
95    Backfill,
96}
97
98impl SafetyConditionUnlock {
99    /// Return the stable diagnostic spelling.
100    pub const fn as_str(self) -> &'static str {
101        match self {
102            Self::BindingDistinct => "binding_distinct",
103            Self::ValueRegex => "value_regex",
104            Self::Backfill => "backfill",
105        }
106    }
107}
108
109/// Closed reason vocabulary for conditions the current query algebra cannot express.
110#[derive(Clone, Copy, Debug, Eq, PartialEq, Serialize)]
111#[serde(rename_all = "snake_case")]
112pub enum UnresolvableSafetyReason {
113    /// `@key` needs distinct owner-thing comparison.
114    KeyRequiresDistinctOwners,
115    /// `@unique` needs distinct owner-thing comparison.
116    UniqueRequiresDistinctOwners,
117    /// Relates cardinality needs distinct player-thing comparison.
118    RelatesCardinalityRequiresDistinctPlayers,
119    /// Plays cardinality needs distinct relation-thing comparison.
120    PlaysCardinalityRequiresDistinctRelations,
121    /// A minimum greater than one needs distinct attribute-thing comparison.
122    OwnsMinimumRequiresDistinctAttributes,
123    /// Regex narrowing needs a canonical regex value predicate.
124    RegexNarrowingRequiresValueRegex,
125    /// Value-domain conversion requires an explicit backfill.
126    ValueTypeConversionRequiresBackfill,
127    /// Subtype-edge changes require an explicit data-policy decision.
128    SubtypeTransitionRequiresBackfill,
129    /// Role-specialization changes require an explicit data-policy decision.
130    RoleSpecializationRequiresBackfill,
131    /// A future conditional transition has no assertion-algebra representation.
132    ConditionalTransitionRequiresBackfill,
133}
134
135impl UnresolvableSafetyReason {
136    /// Return the stable diagnostic spelling.
137    pub const fn as_str(self) -> &'static str {
138        match self {
139            Self::KeyRequiresDistinctOwners => "key_requires_distinct_owners",
140            Self::UniqueRequiresDistinctOwners => "unique_requires_distinct_owners",
141            Self::RelatesCardinalityRequiresDistinctPlayers => {
142                "relates_cardinality_requires_distinct_players"
143            }
144            Self::PlaysCardinalityRequiresDistinctRelations => {
145                "plays_cardinality_requires_distinct_relations"
146            }
147            Self::OwnsMinimumRequiresDistinctAttributes => {
148                "owns_minimum_requires_distinct_attributes"
149            }
150            Self::RegexNarrowingRequiresValueRegex => "regex_narrowing_requires_value_regex",
151            Self::ValueTypeConversionRequiresBackfill => "value_type_conversion_requires_backfill",
152            Self::SubtypeTransitionRequiresBackfill => "subtype_transition_requires_backfill",
153            Self::RoleSpecializationRequiresBackfill => "role_specialization_requires_backfill",
154            Self::ConditionalTransitionRequiresBackfill => {
155                "conditional_transition_requires_backfill"
156            }
157        }
158    }
159}
160
161/// Closed verifier-derived safety-condition vocabulary.
162#[derive(Clone, Debug, Eq, PartialEq, Serialize)]
163#[serde(tag = "kind", rename_all = "snake_case")]
164pub enum SafetyCondition {
165    /// No instance of a type may exist.
166    NoInstances {
167        /// Type whose instances would violate the transition.
168        type_id: TypeId,
169        /// Whether instances of subtypes also violate the transition.
170        include_subtypes: bool,
171    },
172    /// Every owner must have at least the target number of attributes.
173    OwnsMinimum {
174        /// Exact effective ownership being tightened.
175        owns: OwnsFactId,
176        /// Target minimum. Revision one can lower only the value one.
177        minimum: u64,
178    },
179    /// No owner may have more than the target number of distinct attribute values.
180    OwnsMaximum {
181        /// Exact effective ownership being tightened.
182        owns: OwnsFactId,
183        /// Finite target maximum.
184        maximum: u64,
185    },
186    /// Existing values must not be below a target lower bound.
187    RangeLower {
188        /// Exact scalar subject being constrained.
189        subject: ScalarSafetySubject,
190        /// Inclusive target lower bound.
191        lower: CanonicalValue,
192    },
193    /// Existing values must not be above a target upper bound.
194    RangeUpper {
195        /// Exact scalar subject being constrained.
196        subject: ScalarSafetySubject,
197        /// Inclusive target upper bound.
198        upper: CanonicalValue,
199    },
200    /// Existing values must belong to the target allowed-value set.
201    ValuesNarrowed {
202        /// Exact scalar subject being constrained.
203        subject: ScalarSafetySubject,
204        /// Canonically ordered, non-empty target allowed values.
205        allowed: Vec<CanonicalValue>,
206    },
207    /// No attribute instance may be orphaned when `@independent` is removed.
208    NoOrphanAttributes {
209        /// Attribute type losing independent existence.
210        attribute: AttributeId,
211    },
212    /// The verifier identified a requirement that cannot be silently weakened.
213    Unresolvable {
214        /// Stable explanation of the missing representation.
215        reason: UnresolvableSafetyReason,
216        /// Feature or workflow which can unlock the transition.
217        unlock: SafetyConditionUnlock,
218    },
219}
220
221impl SafetyCondition {
222    /// Return whether the current assertion algebra can lower this condition.
223    pub const fn is_resolvable(&self) -> bool {
224        !matches!(self, Self::Unresolvable { .. })
225    }
226
227    /// Return an explicit missing feature or workflow, when gated.
228    pub const fn unlock(&self) -> Option<SafetyConditionUnlock> {
229        match self {
230            Self::Unresolvable { unlock, .. } => Some(*unlock),
231            _ => None,
232        }
233    }
234}
235
236#[derive(Serialize)]
237struct SafetyConditionIdentityMaterial<'a> {
238    canonicalization: &'static str,
239    condition: &'a SafetyCondition,
240    lowering_profile: &'a SchemaLoweringProfileBinding,
241    operation_index: u32,
242    policy: SafetyClass,
243    semantic_profile: &'a SemanticProfileBinding,
244    source_declared: &'a DeclaredIdentityFingerprint,
245    target_declared: &'a DeclaredIdentityFingerprint,
246}
247
248/// One exact verifier-derived requirement bound to its transition and profiles.
249#[derive(Clone, Debug, Eq, PartialEq, Serialize)]
250pub struct RequiredSafetyCondition {
251    condition: SafetyCondition,
252    id: SafetyConditionId,
253    lowering_profile: SchemaLoweringProfileBinding,
254    operation_index: u32,
255    policy: SafetyClass,
256    semantic_profile: SemanticProfileBinding,
257    source_declared: DeclaredIdentityFingerprint,
258    target_declared: DeclaredIdentityFingerprint,
259}
260
261impl RequiredSafetyCondition {
262    fn derive(
263        operation_index: u32,
264        policy: SafetyClass,
265        condition: SafetyCondition,
266        source_declared: &DeclaredSchema,
267        target_declared: &DeclaredSchema,
268        profile: &SafetyDerivationProfile,
269    ) -> Result<Self, Diagnostic> {
270        let source_declared = source_declared.declared_identity_fingerprint().clone();
271        let target_declared = target_declared.declared_identity_fingerprint().clone();
272        let identity = SafetyConditionIdentityMaterial {
273            canonicalization: SAFETY_CONDITION_CANONICALIZATION,
274            condition: &condition,
275            lowering_profile: profile.lowering(),
276            operation_index,
277            policy,
278            semantic_profile: profile.semantic(),
279            source_declared: &source_declared,
280            target_declared: &target_declared,
281        };
282        let id = SafetyConditionId::compute(&to_canonical_json(&identity)?)?;
283        Ok(Self {
284            condition,
285            id,
286            lowering_profile: profile.lowering().clone(),
287            operation_index,
288            policy,
289            semantic_profile: profile.semantic().clone(),
290            source_declared,
291            target_declared,
292        })
293    }
294
295    /// Return the stable canonical condition identity.
296    pub const fn id(&self) -> &SafetyConditionId {
297        &self.id
298    }
299
300    /// Return the operation ordinal that produced this requirement.
301    pub const fn operation_index(&self) -> u32 {
302        self.operation_index
303    }
304
305    /// Return the original eight-class policy; guards never rewrite it.
306    pub const fn policy(&self) -> SafetyClass {
307        self.policy
308    }
309
310    /// Return the closed derived condition.
311    pub const fn condition(&self) -> &SafetyCondition {
312        &self.condition
313    }
314
315    /// Return the exact source declaration identity.
316    pub const fn source_declared_identity(&self) -> &DeclaredIdentityFingerprint {
317        &self.source_declared
318    }
319
320    /// Return the exact target declaration identity.
321    pub const fn target_declared_identity(&self) -> &DeclaredIdentityFingerprint {
322        &self.target_declared
323    }
324
325    /// Return the exact semantic-profile binding used by the verifier.
326    pub const fn semantic_profile(&self) -> &SemanticProfileBinding {
327        &self.semantic_profile
328    }
329
330    /// Return the exact lowering-profile binding used by the verifier.
331    pub const fn lowering_profile(&self) -> &SchemaLoweringProfileBinding {
332        &self.lowering_profile
333    }
334
335    /// Return whether this assertion can resolve a Conditional requirement.
336    pub fn resolves_conditional_requirement(&self) -> bool {
337        self.policy == SafetyClass::Conditional && self.condition.is_resolvable()
338    }
339
340    /// Encode identity material without the self-referential identity field.
341    pub fn canonical_identity_bytes(&self) -> Result<Vec<u8>, Diagnostic> {
342        to_canonical_json(&SafetyConditionIdentityMaterial {
343            canonicalization: SAFETY_CONDITION_CANONICALIZATION,
344            condition: &self.condition,
345            lowering_profile: &self.lowering_profile,
346            operation_index: self.operation_index,
347            policy: self.policy,
348            semantic_profile: &self.semantic_profile,
349            source_declared: &self.source_declared,
350            target_declared: &self.target_declared,
351        })
352    }
353
354    /// Encode the complete trusted condition as canonical JSON.
355    pub fn canonical_bytes(&self) -> Result<Vec<u8>, Diagnostic> {
356        to_canonical_json(self)
357    }
358}
359
360/// Ordered verifier output for one schema operation.
361#[derive(Clone, Debug, Eq, PartialEq, Serialize)]
362pub struct DerivedSafetyConditions {
363    conditions: Vec<RequiredSafetyCondition>,
364    operation_index: u32,
365    policy: SafetyClass,
366}
367
368impl DerivedSafetyConditions {
369    /// Return the operation ordinal shared by every condition.
370    pub const fn operation_index(&self) -> u32 {
371        self.operation_index
372    }
373
374    /// Return the unchanged eight-class operation policy.
375    pub const fn policy(&self) -> SafetyClass {
376        self.policy
377    }
378
379    /// Return conditions in deterministic fact and bound order.
380    pub fn conditions(&self) -> &[RequiredSafetyCondition] {
381        &self.conditions
382    }
383
384    /// Return whether every Conditional requirement has an expressible assertion.
385    pub fn resolves_conditional_requirements(&self) -> bool {
386        self.policy == SafetyClass::Conditional
387            && !self.conditions.is_empty()
388            && self
389                .conditions
390                .iter()
391                .all(RequiredSafetyCondition::resolves_conditional_requirement)
392    }
393}
394
395/// Derive safety conditions from an exact trusted source/operation/target transition.
396pub fn derive_safety_conditions(
397    operation_index: usize,
398    operation: &SchemaOperation,
399    source_declared: &DeclaredSchema,
400    target_declared: &DeclaredSchema,
401    profile: &SafetyDerivationProfile,
402) -> Result<DerivedSafetyConditions, Diagnostic> {
403    let operation_index = u32::try_from(operation_index).map_err(|_| {
404        failure(
405            DiagnosticCategory::ResourceLimit,
406            "safety_condition_operation_index_limit",
407            "operation index exceeds the canonical safety-condition range",
408        )
409    })?;
410    validate_exact_transition(operation, source_declared, target_declared)?;
411    let semantic = SemanticProfile::resolve(profile.semantic().id())?;
412    let policy = classify_schema_operation_safety(operation);
413    let mut conditions = Vec::new();
414
415    match operation.kind() {
416        SchemaOperationKind::Define => {
417            for fact in operation.defined_facts().expect("define exposes facts") {
418                derive_defined_fact(
419                    fact,
420                    operation_index,
421                    policy,
422                    source_declared,
423                    target_declared,
424                    profile,
425                    &semantic,
426                    &mut conditions,
427                )?;
428            }
429        }
430        SchemaOperationKind::Redefine => derive_redefinition(
431            operation
432                .expected_fact()
433                .expect("redefine exposes expected fact"),
434            operation
435                .replacement_fact()
436                .expect("redefine exposes replacement fact"),
437            operation_index,
438            policy,
439            source_declared,
440            target_declared,
441            profile,
442            &semantic,
443            &mut conditions,
444        )?,
445        SchemaOperationKind::Undefine => derive_undefined_fact(
446            operation.undefined_fact().expect("undefine exposes fact"),
447            operation_index,
448            policy,
449            source_declared,
450            target_declared,
451            profile,
452            &semantic,
453            &mut conditions,
454        )?,
455    }
456
457    if policy == SafetyClass::Conditional
458        && conditions.is_empty()
459        && !is_proven_condition_free_constraint_transition(operation, source_declared)?
460    {
461        push_condition(
462            &mut conditions,
463            operation_index,
464            policy,
465            SafetyCondition::Unresolvable {
466                reason: UnresolvableSafetyReason::ConditionalTransitionRequiresBackfill,
467                unlock: SafetyConditionUnlock::Backfill,
468            },
469            source_declared,
470            target_declared,
471            profile,
472        )?;
473    }
474
475    Ok(DerivedSafetyConditions {
476        conditions,
477        operation_index,
478        policy,
479    })
480}
481
482#[allow(clippy::too_many_arguments)]
483fn derive_defined_fact(
484    fact: &SchemaFact,
485    operation_index: u32,
486    policy: SafetyClass,
487    source: &DeclaredSchema,
488    target: &DeclaredSchema,
489    profile: &SafetyDerivationProfile,
490    semantic: &SemanticProfile,
491    conditions: &mut Vec<RequiredSafetyCondition>,
492) -> Result<(), Diagnostic> {
493    match fact {
494        SchemaFact::Annotation(annotation) => derive_annotation_transition(
495            None,
496            Some(annotation),
497            operation_index,
498            policy,
499            source,
500            target,
501            profile,
502            semantic,
503            conditions,
504        ),
505        // A supertype gained by a type that already exists in the committed
506        // source may carry instances whose data placement is a policy
507        // decision. A subtype introduced by this same transition cannot have
508        // instances — the exactly-observed source lacks the type and the
509        // introducing delta commits in one transaction group — so its `sub`
510        // edge is provably condition-free.
511        SchemaFact::Sub(sub)
512            if source
513                .fact(&SchemaFactId::Type(sub.id().subtype().clone()))
514                .is_some() =>
515        {
516            push_unresolvable(
517                conditions,
518                operation_index,
519                policy,
520                UnresolvableSafetyReason::SubtypeTransitionRequiresBackfill,
521                SafetyConditionUnlock::Backfill,
522                source,
523                target,
524                profile,
525            )
526        }
527        SchemaFact::Sub(_) => Ok(()),
528        SchemaFact::Relates(relates) if relates.specializes().is_some() => push_unresolvable(
529            conditions,
530            operation_index,
531            policy,
532            UnresolvableSafetyReason::RoleSpecializationRequiresBackfill,
533            SafetyConditionUnlock::Backfill,
534            source,
535            target,
536            profile,
537        ),
538        _ => Ok(()),
539    }
540}
541
542#[allow(clippy::too_many_arguments)]
543fn derive_redefinition(
544    old: &SchemaFact,
545    new: &SchemaFact,
546    operation_index: u32,
547    policy: SafetyClass,
548    source: &DeclaredSchema,
549    target: &DeclaredSchema,
550    profile: &SafetyDerivationProfile,
551    semantic: &SemanticProfile,
552    conditions: &mut Vec<RequiredSafetyCondition>,
553) -> Result<(), Diagnostic> {
554    match (old, new) {
555        (SchemaFact::Annotation(old), SchemaFact::Annotation(new)) => derive_annotation_transition(
556            Some(old),
557            Some(new),
558            operation_index,
559            policy,
560            source,
561            target,
562            profile,
563            semantic,
564            conditions,
565        ),
566        (SchemaFact::Value(old), SchemaFact::Value(new))
567            if old.value_type() != new.value_type() =>
568        {
569            push_unresolvable(
570                conditions,
571                operation_index,
572                policy,
573                UnresolvableSafetyReason::ValueTypeConversionRequiresBackfill,
574                SafetyConditionUnlock::Backfill,
575                source,
576                target,
577                profile,
578            )
579        }
580        (SchemaFact::Sub(_), SchemaFact::Sub(_)) => push_unresolvable(
581            conditions,
582            operation_index,
583            policy,
584            UnresolvableSafetyReason::SubtypeTransitionRequiresBackfill,
585            SafetyConditionUnlock::Backfill,
586            source,
587            target,
588            profile,
589        ),
590        (SchemaFact::Relates(_), SchemaFact::Relates(_)) => push_unresolvable(
591            conditions,
592            operation_index,
593            policy,
594            UnresolvableSafetyReason::RoleSpecializationRequiresBackfill,
595            SafetyConditionUnlock::Backfill,
596            source,
597            target,
598            profile,
599        ),
600        _ => Ok(()),
601    }
602}
603
604#[allow(clippy::too_many_arguments)]
605fn derive_undefined_fact(
606    fact: &SchemaFact,
607    operation_index: u32,
608    policy: SafetyClass,
609    source: &DeclaredSchema,
610    target: &DeclaredSchema,
611    profile: &SafetyDerivationProfile,
612    semantic: &SemanticProfile,
613    conditions: &mut Vec<RequiredSafetyCondition>,
614) -> Result<(), Diagnostic> {
615    match fact {
616        SchemaFact::Type(type_fact) => push_condition(
617            conditions,
618            operation_index,
619            policy,
620            SafetyCondition::NoInstances {
621                type_id: type_fact.id().clone(),
622                include_subtypes: true,
623            },
624            source,
625            target,
626            profile,
627        ),
628        SchemaFact::Annotation(annotation) => derive_annotation_transition(
629            Some(annotation),
630            None,
631            operation_index,
632            policy,
633            source,
634            target,
635            profile,
636            semantic,
637            conditions,
638        ),
639        SchemaFact::Relates(relates) if relates.specializes().is_some() => push_unresolvable(
640            conditions,
641            operation_index,
642            policy,
643            UnresolvableSafetyReason::RoleSpecializationRequiresBackfill,
644            SafetyConditionUnlock::Backfill,
645            source,
646            target,
647            profile,
648        ),
649        _ => Ok(()),
650    }
651}
652
653#[allow(clippy::too_many_arguments)]
654fn derive_annotation_transition(
655    old: Option<&AnnotationFact>,
656    new: Option<&AnnotationFact>,
657    operation_index: u32,
658    policy: SafetyClass,
659    source: &DeclaredSchema,
660    target: &DeclaredSchema,
661    profile: &SafetyDerivationProfile,
662    semantic: &SemanticProfile,
663    conditions: &mut Vec<RequiredSafetyCondition>,
664) -> Result<(), Diagnostic> {
665    let annotation = new.or(old).expect("an annotation transition has one side");
666    let subject = annotation.id().subject();
667    match annotation.id().kind() {
668        AnnotationKindId::Abstract if old.is_none() => {
669            if let AnnotationSubjectId::Type(type_id) = subject {
670                push_condition(
671                    conditions,
672                    operation_index,
673                    policy,
674                    SafetyCondition::NoInstances {
675                        type_id: type_id.clone(),
676                        include_subtypes: false,
677                    },
678                    source,
679                    target,
680                    profile,
681                )?;
682            }
683            // Abstract-on-relates intentionally reaches the operation-level explicit
684            // Backfill/unresolvable fallback until a live-pinned condition exists.
685        }
686        AnnotationKindId::Independent if new.is_none() => {
687            if let AnnotationSubjectId::Type(type_id) = subject
688                && type_id.kind() == TypeKind::Attribute
689            {
690                push_condition(
691                    conditions,
692                    operation_index,
693                    policy,
694                    SafetyCondition::NoOrphanAttributes {
695                        attribute: AttributeId::new(type_id.label().as_str())?,
696                    },
697                    source,
698                    target,
699                    profile,
700                )?;
701            }
702        }
703        AnnotationKindId::Key if old.is_none() => push_unresolvable(
704            conditions,
705            operation_index,
706            policy,
707            UnresolvableSafetyReason::KeyRequiresDistinctOwners,
708            SafetyConditionUnlock::BindingDistinct,
709            source,
710            target,
711            profile,
712        )?,
713        AnnotationKindId::Unique if old.is_none() => push_unresolvable(
714            conditions,
715            operation_index,
716            policy,
717            UnresolvableSafetyReason::UniqueRequiresDistinctOwners,
718            SafetyConditionUnlock::BindingDistinct,
719            source,
720            target,
721            profile,
722        )?,
723        AnnotationKindId::Card => derive_cardinality_conditions(
724            subject,
725            operation_index,
726            policy,
727            source,
728            target,
729            profile,
730            semantic,
731            conditions,
732        )?,
733        AnnotationKindId::Range => {
734            if let Some(new) = new {
735                let range = range_payload(new)?;
736                let old_range = old.map(range_payload).transpose()?;
737                let (lower_narrows, upper_narrows) = range_narrowing(old_range, range)?;
738                let subject = scalar_subject(subject)?;
739                if lower_narrows {
740                    let lower = range.lower().expect("a narrowing lower bound is present");
741                    push_condition(
742                        conditions,
743                        operation_index,
744                        policy,
745                        SafetyCondition::RangeLower {
746                            subject: subject.clone(),
747                            lower: lower.clone(),
748                        },
749                        source,
750                        target,
751                        profile,
752                    )?;
753                }
754                if upper_narrows {
755                    let upper = range.upper().expect("a narrowing upper bound is present");
756                    push_condition(
757                        conditions,
758                        operation_index,
759                        policy,
760                        SafetyCondition::RangeUpper {
761                            subject,
762                            upper: upper.clone(),
763                        },
764                        source,
765                        target,
766                        profile,
767                    )?;
768                }
769            }
770        }
771        AnnotationKindId::Values => {
772            if let Some(new) = new {
773                let values = values_payload(new)?;
774                let old_values = old.map(values_payload).transpose()?;
775                if values_narrow(old_values, values)? {
776                    push_condition(
777                        conditions,
778                        operation_index,
779                        policy,
780                        SafetyCondition::ValuesNarrowed {
781                            subject: scalar_subject(subject)?,
782                            allowed: values.iter().cloned().collect(),
783                        },
784                        source,
785                        target,
786                        profile,
787                    )?;
788                }
789            }
790        }
791        AnnotationKindId::Regex if new.is_some() => push_unresolvable(
792            conditions,
793            operation_index,
794            policy,
795            UnresolvableSafetyReason::RegexNarrowingRequiresValueRegex,
796            SafetyConditionUnlock::ValueRegex,
797            source,
798            target,
799            profile,
800        )?,
801        _ => {}
802    }
803    Ok(())
804}
805
806fn is_proven_condition_free_constraint_transition(
807    operation: &SchemaOperation,
808    source: &DeclaredSchema,
809) -> Result<bool, Diagnostic> {
810    if operation.kind() == SchemaOperationKind::Define {
811        return Ok(is_proven_condition_free_define(operation, source));
812    }
813    if operation.kind() != SchemaOperationKind::Redefine {
814        return Ok(false);
815    }
816    let (SchemaFact::Annotation(old), SchemaFact::Annotation(new)) = (
817        operation
818            .expected_fact()
819            .expect("redefine exposes expected fact"),
820        operation
821            .replacement_fact()
822            .expect("redefine exposes replacement fact"),
823    ) else {
824        return Ok(false);
825    };
826    match new.id().kind() {
827        AnnotationKindId::Range => {
828            let (lower_narrows, upper_narrows) =
829                range_narrowing(Some(range_payload(old)?), range_payload(new)?)?;
830            Ok(!lower_narrows && !upper_narrows)
831        }
832        AnnotationKindId::Values => Ok(!values_narrow(
833            Some(values_payload(old)?),
834            values_payload(new)?,
835        )?),
836        _ => Ok(false),
837    }
838}
839
840/// Prove a conditional define carries only condition-free work.
841///
842/// The only proven shape is a `sub` edge whose subtype is absent from the
843/// exactly-observed source: the type is introduced by this same transition and
844/// cannot have instances when the introducing transaction group runs. Any
845/// annotation, struct, or specializing-relates fact deliberately fails the
846/// proof — those keep the conservative backfill catch-all even when their own
847/// derivation produced no condition.
848fn is_proven_condition_free_define(operation: &SchemaOperation, source: &DeclaredSchema) -> bool {
849    let Some(facts) = operation.defined_facts() else {
850        return false;
851    };
852    let mut proven_sub = false;
853    for fact in facts {
854        match fact {
855            SchemaFact::Sub(sub) => {
856                if source
857                    .fact(&SchemaFactId::Type(sub.id().subtype().clone()))
858                    .is_some()
859                {
860                    return false;
861                }
862                proven_sub = true;
863            }
864            SchemaFact::Relates(relates) if relates.specializes().is_some() => {
865                return false;
866            }
867            SchemaFact::Annotation(_) | SchemaFact::Struct(_) => return false,
868            SchemaFact::Type(_)
869            | SchemaFact::Value(_)
870            | SchemaFact::Owns(_)
871            | SchemaFact::Relates(_)
872            | SchemaFact::Plays(_)
873            | SchemaFact::Function(_) => {}
874        }
875    }
876    proven_sub
877}
878
879fn range_payload(annotation: &AnnotationFact) -> Result<&CanonicalValueRange, Diagnostic> {
880    match annotation.value() {
881        SchemaAnnotationValue::Range(range) => Ok(range),
882        _ => Err(failure(
883            DiagnosticCategory::InvalidContract,
884            "safety_condition_malformed_range_transition",
885            "range transition does not contain range payloads on both sides",
886        )),
887    }
888}
889
890fn range_narrowing(
891    old: Option<&CanonicalValueRange>,
892    new: &CanonicalValueRange,
893) -> Result<(bool, bool), Diagnostic> {
894    if let Some(old) = old {
895        let old_domain = old
896            .lower()
897            .or_else(|| old.upper())
898            .expect("canonical ranges are non-empty")
899            .value_type();
900        let new_domain = new
901            .lower()
902            .or_else(|| new.upper())
903            .expect("canonical ranges are non-empty")
904            .value_type();
905        if old_domain != new_domain {
906            return Err(failure(
907                DiagnosticCategory::InvalidContract,
908                "safety_condition_incomparable_range_domain",
909                "range transition bounds use incomparable scalar domains",
910            ));
911        }
912    }
913
914    let lower_narrows = match (old.and_then(CanonicalValueRange::lower), new.lower()) {
915        (_, None) => false,
916        (None, Some(_)) => true,
917        (Some(old), Some(new)) => compare_same_domain(new, old)? == Ordering::Greater,
918    };
919    let upper_narrows = match (old.and_then(CanonicalValueRange::upper), new.upper()) {
920        (_, None) => false,
921        (None, Some(_)) => true,
922        (Some(old), Some(new)) => compare_same_domain(new, old)? == Ordering::Less,
923    };
924    Ok((lower_narrows, upper_narrows))
925}
926
927fn values_payload(annotation: &AnnotationFact) -> Result<&CanonicalValueSet, Diagnostic> {
928    match annotation.value() {
929        SchemaAnnotationValue::Values(values) => Ok(values),
930        _ => Err(failure(
931            DiagnosticCategory::InvalidContract,
932            "safety_condition_malformed_values_transition",
933            "values transition does not contain values payloads on both sides",
934        )),
935    }
936}
937
938fn values_narrow(
939    old: Option<&CanonicalValueSet>,
940    new: &CanonicalValueSet,
941) -> Result<bool, Diagnostic> {
942    let Some(old) = old else {
943        return Ok(true);
944    };
945    let old_domain = old
946        .iter()
947        .next()
948        .expect("canonical value sets are non-empty")
949        .value_type();
950    let new_domain = new
951        .iter()
952        .next()
953        .expect("canonical value sets are non-empty")
954        .value_type();
955    if old_domain != new_domain {
956        return Err(failure(
957            DiagnosticCategory::InvalidContract,
958            "safety_condition_incomparable_values_domain",
959            "values transition members use incomparable scalar domains",
960        ));
961    }
962    Ok(old
963        .iter()
964        .any(|old_value| !new.iter().any(|new_value| new_value == old_value)))
965}
966
967fn compare_same_domain(
968    left: &CanonicalValue,
969    right: &CanonicalValue,
970) -> Result<Ordering, Diagnostic> {
971    left.semantic_cmp_same_domain(right).ok_or_else(|| {
972        failure(
973            DiagnosticCategory::InvalidContract,
974            "safety_condition_incomparable_range_domain",
975            "range transition bounds use incomparable scalar domains",
976        )
977    })
978}
979
980#[allow(clippy::too_many_arguments)]
981fn derive_cardinality_conditions(
982    subject: &AnnotationSubjectId,
983    operation_index: u32,
984    policy: SafetyClass,
985    source: &DeclaredSchema,
986    target: &DeclaredSchema,
987    profile: &SafetyDerivationProfile,
988    semantic: &SemanticProfile,
989    conditions: &mut Vec<RequiredSafetyCondition>,
990) -> Result<(), Diagnostic> {
991    let old = effective_cardinality(source, subject, semantic)?;
992    let new = effective_cardinality(target, subject, semantic)?;
993    let minimum_narrows = new.min() > old.min();
994    let maximum_narrows = match (old.max(), new.max()) {
995        (_, None) => false,
996        (None, Some(_)) => true,
997        (Some(old), Some(new)) => new < old,
998    };
999    if !minimum_narrows && !maximum_narrows {
1000        return Ok(());
1001    }
1002
1003    match subject {
1004        AnnotationSubjectId::Owns(owns) => {
1005            if minimum_narrows {
1006                if new.min() == 1 {
1007                    push_condition(
1008                        conditions,
1009                        operation_index,
1010                        policy,
1011                        SafetyCondition::OwnsMinimum {
1012                            owns: owns.clone(),
1013                            minimum: 1,
1014                        },
1015                        source,
1016                        target,
1017                        profile,
1018                    )?;
1019                } else {
1020                    push_unresolvable(
1021                        conditions,
1022                        operation_index,
1023                        policy,
1024                        UnresolvableSafetyReason::OwnsMinimumRequiresDistinctAttributes,
1025                        SafetyConditionUnlock::BindingDistinct,
1026                        source,
1027                        target,
1028                        profile,
1029                    )?;
1030                }
1031            }
1032            if maximum_narrows {
1033                push_condition(
1034                    conditions,
1035                    operation_index,
1036                    policy,
1037                    SafetyCondition::OwnsMaximum {
1038                        owns: owns.clone(),
1039                        maximum: new.max().expect("a narrowing maximum is finite"),
1040                    },
1041                    source,
1042                    target,
1043                    profile,
1044                )?;
1045            }
1046        }
1047        AnnotationSubjectId::Relates(_) => push_unresolvable(
1048            conditions,
1049            operation_index,
1050            policy,
1051            UnresolvableSafetyReason::RelatesCardinalityRequiresDistinctPlayers,
1052            SafetyConditionUnlock::BindingDistinct,
1053            source,
1054            target,
1055            profile,
1056        )?,
1057        AnnotationSubjectId::Plays(_) => push_unresolvable(
1058            conditions,
1059            operation_index,
1060            policy,
1061            UnresolvableSafetyReason::PlaysCardinalityRequiresDistinctRelations,
1062            SafetyConditionUnlock::BindingDistinct,
1063            source,
1064            target,
1065            profile,
1066        )?,
1067        _ => {
1068            return Err(failure(
1069                DiagnosticCategory::InvalidContract,
1070                "safety_condition_invalid_cardinality_subject",
1071                "cardinality safety derivation requires an interface subject",
1072            ));
1073        }
1074    }
1075    Ok(())
1076}
1077
1078fn effective_cardinality(
1079    declared: &DeclaredSchema,
1080    subject: &AnnotationSubjectId,
1081    semantic: &SemanticProfile,
1082) -> Result<Cardinality, Diagnostic> {
1083    let kind = match subject {
1084        AnnotationSubjectId::Owns(_) => InterfaceKind::Owns,
1085        AnnotationSubjectId::Relates(_) => InterfaceKind::Relates,
1086        AnnotationSubjectId::Plays(_) => InterfaceKind::Plays,
1087        _ => {
1088            return Err(failure(
1089                DiagnosticCategory::InvalidContract,
1090                "safety_condition_invalid_cardinality_subject",
1091                "cardinality safety derivation requires an interface subject",
1092            ));
1093        }
1094    };
1095    let explicit = annotation(declared, subject, &AnnotationKindId::Card).and_then(|annotation| {
1096        match annotation.value() {
1097            SchemaAnnotationValue::Cardinality(cardinality) => Some(*cardinality),
1098            _ => None,
1099        }
1100    });
1101    let key = matches!(subject, AnnotationSubjectId::Owns(_))
1102        && annotation(declared, subject, &AnnotationKindId::Key).is_some();
1103    Ok(semantic.effective_cardinality(kind, explicit, key))
1104}
1105
1106fn annotation<'a>(
1107    declared: &'a DeclaredSchema,
1108    subject: &AnnotationSubjectId,
1109    kind: &AnnotationKindId,
1110) -> Option<&'a AnnotationFact> {
1111    declared.facts().find_map(|fact| match fact {
1112        SchemaFact::Annotation(annotation)
1113            if annotation.id().subject() == subject && annotation.id().kind() == kind =>
1114        {
1115            Some(annotation)
1116        }
1117        _ => None,
1118    })
1119}
1120
1121fn scalar_subject(subject: &AnnotationSubjectId) -> Result<ScalarSafetySubject, Diagnostic> {
1122    match subject {
1123        AnnotationSubjectId::Value(value) => Ok(ScalarSafetySubject::Value(value.clone())),
1124        AnnotationSubjectId::Owns(owns) => Ok(ScalarSafetySubject::Owns(owns.clone())),
1125        _ => Err(failure(
1126            DiagnosticCategory::InvalidContract,
1127            "safety_condition_invalid_scalar_subject",
1128            "value safety derivation requires a value or ownership subject",
1129        )),
1130    }
1131}
1132
1133#[allow(clippy::too_many_arguments)]
1134fn push_unresolvable(
1135    conditions: &mut Vec<RequiredSafetyCondition>,
1136    operation_index: u32,
1137    policy: SafetyClass,
1138    reason: UnresolvableSafetyReason,
1139    unlock: SafetyConditionUnlock,
1140    source: &DeclaredSchema,
1141    target: &DeclaredSchema,
1142    profile: &SafetyDerivationProfile,
1143) -> Result<(), Diagnostic> {
1144    push_condition(
1145        conditions,
1146        operation_index,
1147        policy,
1148        SafetyCondition::Unresolvable { reason, unlock },
1149        source,
1150        target,
1151        profile,
1152    )
1153}
1154
1155fn push_condition(
1156    conditions: &mut Vec<RequiredSafetyCondition>,
1157    operation_index: u32,
1158    policy: SafetyClass,
1159    condition: SafetyCondition,
1160    source: &DeclaredSchema,
1161    target: &DeclaredSchema,
1162    profile: &SafetyDerivationProfile,
1163) -> Result<(), Diagnostic> {
1164    conditions.push(RequiredSafetyCondition::derive(
1165        operation_index,
1166        policy,
1167        condition,
1168        source,
1169        target,
1170        profile,
1171    )?);
1172    Ok(())
1173}
1174
1175fn validate_exact_transition(
1176    operation: &SchemaOperation,
1177    source: &DeclaredSchema,
1178    target: &DeclaredSchema,
1179) -> Result<(), Diagnostic> {
1180    match operation.kind() {
1181        SchemaOperationKind::Define => {
1182            for fact in operation.defined_facts().expect("define exposes facts") {
1183                let id = fact.id();
1184                if find_fact(source, &id).is_some() {
1185                    return Err(transition_failure(
1186                        "safety_condition_source_define_conflict",
1187                        "defined fact already exists in the declared source",
1188                    ));
1189                }
1190                if find_fact(target, &id) != Some(fact) {
1191                    return Err(transition_failure(
1192                        "safety_condition_target_define_mismatch",
1193                        "defined fact does not exactly match the declared target",
1194                    ));
1195                }
1196            }
1197        }
1198        SchemaOperationKind::Redefine => {
1199            let expected = operation
1200                .expected_fact()
1201                .expect("redefine exposes expected fact");
1202            let replacement = operation
1203                .replacement_fact()
1204                .expect("redefine exposes replacement fact");
1205            let id = expected.id();
1206            if find_fact(source, &id) != Some(expected) {
1207                return Err(transition_failure(
1208                    "safety_condition_source_redefine_mismatch",
1209                    "expected fact does not exactly match the declared source",
1210                ));
1211            }
1212            if find_fact(target, &id) != Some(replacement) {
1213                return Err(transition_failure(
1214                    "safety_condition_target_redefine_mismatch",
1215                    "replacement fact does not exactly match the declared target",
1216                ));
1217            }
1218        }
1219        SchemaOperationKind::Undefine => {
1220            let fact = operation.undefined_fact().expect("undefine exposes fact");
1221            let id = fact.id();
1222            if find_fact(source, &id) != Some(fact) {
1223                return Err(transition_failure(
1224                    "safety_condition_source_undefine_mismatch",
1225                    "removed fact does not exactly match the declared source",
1226                ));
1227            }
1228            if find_fact(target, &id).is_some() {
1229                return Err(transition_failure(
1230                    "safety_condition_target_undefine_conflict",
1231                    "removed fact is still present in the declared target",
1232                ));
1233            }
1234        }
1235    }
1236    Ok(())
1237}
1238
1239fn find_fact<'a>(declared: &'a DeclaredSchema, id: &SchemaFactId) -> Option<&'a SchemaFact> {
1240    declared.facts().find(|fact| fact.id() == id.clone())
1241}
1242
1243fn transition_failure(code: &'static str, message: &'static str) -> Diagnostic {
1244    failure(DiagnosticCategory::Integrity, code, message)
1245}
1246
1247fn failure(category: DiagnosticCategory, code: &'static str, message: &'static str) -> Diagnostic {
1248    Diagnostic::new(
1249        category,
1250        DiagnosticCode::new(code).expect("static safety-condition diagnostic code is canonical"),
1251        message,
1252    )
1253}
1254
1255#[cfg(test)]
1256mod tests {
1257    use type_bridge_contract::capability::CapabilitySet;
1258    use type_bridge_contract::codec::FormatVersion;
1259    use type_bridge_contract::id::TypeKind;
1260    use type_bridge_contract::managed_scope::SemanticProfileBinding;
1261    use type_bridge_contract::schema::{
1262        AnnotationFactId, CanonicalValueRange, CanonicalValueSet, DocumentId, OwnsFact, SourceSpan,
1263        SourcedSchemaFact, TypeFact, ValueFact,
1264    };
1265    use type_bridge_contract::schema_lowering::SchemaLoweringProfileBinding;
1266    use type_bridge_contract::value::ValueTypeTag;
1267
1268    use super::*;
1269
1270    fn test_safety_profile() -> SafetyDerivationProfile {
1271        SafetyDerivationProfile::new(
1272            SemanticProfileBinding::typedb_3_12_1().expect("semantic profile"),
1273            SchemaLoweringProfileBinding::from_canonical_profile_bytes(
1274                br#"{"id":"typedb-3.12.1-schema-lowering/v1","test_fixture":"safety-condition"}"#,
1275            )
1276            .expect("test lowering profile"),
1277        )
1278        .expect("test safety profile")
1279    }
1280
1281    fn type_id(kind: TypeKind, label: &str) -> TypeId {
1282        TypeId::new(kind, label).expect("fixture type")
1283    }
1284
1285    fn declared(facts: Vec<SchemaFact>) -> DeclaredSchema {
1286        let facts = facts.into_iter().enumerate().map(|(index, fact)| {
1287            let offset = u64::try_from(index).expect("fixture offset");
1288            let line = u32::try_from(index + 1).expect("fixture line");
1289            SourcedSchemaFact::new(
1290                fact,
1291                SourceSpan::new(
1292                    DocumentId::new("safety-condition-test").expect("document"),
1293                    offset,
1294                    offset + 1,
1295                    line,
1296                    1,
1297                    line,
1298                    2,
1299                )
1300                .expect("span"),
1301            )
1302        });
1303        DeclaredSchema::from_facts(FormatVersion::V1, CapabilitySet::new(), facts)
1304            .expect("declared fixture")
1305    }
1306
1307    fn annotation_fact(
1308        subject: AnnotationSubjectId,
1309        kind: AnnotationKindId,
1310        value: SchemaAnnotationValue,
1311    ) -> SchemaFact {
1312        SchemaFact::Annotation(
1313            AnnotationFact::new(AnnotationFactId::new(subject, kind), value)
1314                .expect("annotation fixture"),
1315        )
1316    }
1317
1318    fn owns_fixture() -> (Vec<SchemaFact>, OwnsFactId) {
1319        let person = type_id(TypeKind::Entity, "person");
1320        let age = AttributeId::new("age").expect("attribute");
1321        let owns = OwnsFactId::new(person.clone(), age.clone()).expect("owns");
1322        (
1323            vec![
1324                SchemaFact::Type(TypeFact::new(person).expect("type")),
1325                SchemaFact::Type(TypeFact::new(type_id(TypeKind::Attribute, "age")).expect("type")),
1326                SchemaFact::Value(ValueFact::new(ValueFactId::new(age), ValueTypeTag::Long)),
1327                SchemaFact::Owns(OwnsFact::new(owns.clone())),
1328            ],
1329            owns,
1330        )
1331    }
1332
1333    #[test]
1334    fn condition_identity_order_and_transition_tamper_are_pinned() {
1335        let profile = test_safety_profile();
1336        let (base, owns) = owns_fixture();
1337        let subject = AnnotationSubjectId::Owns(owns.clone());
1338        let old = annotation_fact(
1339            subject.clone(),
1340            AnnotationKindId::Card,
1341            SchemaAnnotationValue::Cardinality(Cardinality::new(0, Some(3)).expect("old card")),
1342        );
1343        let new = annotation_fact(
1344            subject,
1345            AnnotationKindId::Card,
1346            SchemaAnnotationValue::Cardinality(Cardinality::new(1, Some(1)).expect("new card")),
1347        );
1348        let source = declared(base.iter().cloned().chain([old.clone()]).collect());
1349        let target = declared(base.iter().cloned().chain([new.clone()]).collect());
1350        let operation = SchemaOperation::redefine(old, new).expect("operation");
1351
1352        let first = derive_safety_conditions(7, &operation, &source, &target, &profile)
1353            .expect("conditions");
1354        let second = derive_safety_conditions(7, &operation, &source, &target, &profile)
1355            .expect("conditions");
1356        assert_eq!(first, second);
1357        assert_eq!(first.conditions().len(), 2);
1358        assert!(matches!(
1359            first.conditions()[0].condition(),
1360            SafetyCondition::OwnsMinimum { minimum: 1, .. }
1361        ));
1362        assert!(matches!(
1363            first.conditions()[1].condition(),
1364            SafetyCondition::OwnsMaximum { maximum: 1, .. }
1365        ));
1366        assert_eq!(first.conditions()[0].id(), second.conditions()[0].id());
1367        assert_eq!(
1368            first.conditions()[0]
1369                .canonical_identity_bytes()
1370                .expect("identity bytes"),
1371            second.conditions()[0]
1372                .canonical_identity_bytes()
1373                .expect("identity bytes")
1374        );
1375        let moved = derive_safety_conditions(8, &operation, &source, &target, &profile)
1376            .expect("moved condition");
1377        assert_ne!(first.conditions()[0].id(), moved.conditions()[0].id());
1378        assert_eq!(
1379            derive_safety_conditions(7, &operation, &source, &source, &profile)
1380                .expect_err("target tamper")
1381                .code()
1382                .as_str(),
1383            "safety_condition_target_redefine_mismatch"
1384        );
1385    }
1386
1387    #[test]
1388    fn expressible_and_gated_families_preserve_original_policy() {
1389        let profile = test_safety_profile();
1390        let person = type_id(TypeKind::Entity, "person");
1391        let base = vec![SchemaFact::Type(
1392            TypeFact::new(person.clone()).expect("type"),
1393        )];
1394        let abstract_fact = annotation_fact(
1395            AnnotationSubjectId::Type(person.clone()),
1396            AnnotationKindId::Abstract,
1397            SchemaAnnotationValue::Presence,
1398        );
1399        let source = declared(base.clone());
1400        let target = declared(
1401            base.iter()
1402                .cloned()
1403                .chain([abstract_fact.clone()])
1404                .collect(),
1405        );
1406        let abstract_conditions = derive_safety_conditions(
1407            0,
1408            &SchemaOperation::define(vec![abstract_fact]).expect("abstract operation"),
1409            &source,
1410            &target,
1411            &profile,
1412        )
1413        .expect("abstract condition");
1414        assert_eq!(abstract_conditions.policy(), SafetyClass::Conditional);
1415        assert!(abstract_conditions.resolves_conditional_requirements());
1416        assert!(matches!(
1417            abstract_conditions.conditions()[0].condition(),
1418            SafetyCondition::NoInstances {
1419                include_subtypes: false,
1420                ..
1421            }
1422        ));
1423
1424        let (owns_base, owns) = owns_fixture();
1425        let key = annotation_fact(
1426            AnnotationSubjectId::Owns(owns),
1427            AnnotationKindId::Key,
1428            SchemaAnnotationValue::Presence,
1429        );
1430        let key_source = declared(owns_base.clone());
1431        let key_target = declared(owns_base.into_iter().chain([key.clone()]).collect());
1432        let key_conditions = derive_safety_conditions(
1433            1,
1434            &SchemaOperation::define(vec![key]).expect("key operation"),
1435            &key_source,
1436            &key_target,
1437            &profile,
1438        )
1439        .expect("key condition");
1440        assert_eq!(key_conditions.policy(), SafetyClass::BackfillRequired);
1441        assert!(matches!(
1442            key_conditions.conditions()[0].condition(),
1443            SafetyCondition::Unresolvable {
1444                reason: UnresolvableSafetyReason::KeyRequiresDistinctOwners,
1445                unlock: SafetyConditionUnlock::BindingDistinct,
1446            }
1447        ));
1448
1449        let age = AttributeId::new("age").expect("attribute");
1450        let scalar_base = vec![
1451            SchemaFact::Type(TypeFact::new(type_id(TypeKind::Attribute, "age")).expect("type")),
1452            SchemaFact::Value(ValueFact::new(
1453                ValueFactId::new(age.clone()),
1454                ValueTypeTag::Long,
1455            )),
1456        ];
1457        let range = annotation_fact(
1458            AnnotationSubjectId::Value(ValueFactId::new(age.clone())),
1459            AnnotationKindId::Range,
1460            SchemaAnnotationValue::Range(
1461                CanonicalValueRange::new(
1462                    Some(CanonicalValue::Long(1)),
1463                    Some(CanonicalValue::Long(9)),
1464                )
1465                .expect("range"),
1466            ),
1467        );
1468        let range_source = declared(scalar_base.clone());
1469        let range_target = declared(scalar_base.iter().cloned().chain([range.clone()]).collect());
1470        let range_conditions = derive_safety_conditions(
1471            2,
1472            &SchemaOperation::define(vec![range]).expect("range operation"),
1473            &range_source,
1474            &range_target,
1475            &profile,
1476        )
1477        .expect("range conditions");
1478        assert_eq!(range_conditions.conditions().len(), 2);
1479        assert!(range_conditions.resolves_conditional_requirements());
1480
1481        let values = annotation_fact(
1482            AnnotationSubjectId::Value(ValueFactId::new(age.clone())),
1483            AnnotationKindId::Values,
1484            SchemaAnnotationValue::Values(
1485                CanonicalValueSet::new([CanonicalValue::Long(2), CanonicalValue::Long(4)])
1486                    .expect("values"),
1487            ),
1488        );
1489        let values_target = declared(
1490            scalar_base
1491                .iter()
1492                .cloned()
1493                .chain([values.clone()])
1494                .collect(),
1495        );
1496        let values_conditions = derive_safety_conditions(
1497            3,
1498            &SchemaOperation::define(vec![values]).expect("values operation"),
1499            &range_source,
1500            &values_target,
1501            &profile,
1502        )
1503        .expect("values condition");
1504        assert!(matches!(
1505            values_conditions.conditions()[0].condition(),
1506            SafetyCondition::ValuesNarrowed { allowed, .. } if allowed.len() == 2
1507        ));
1508
1509        let code = AttributeId::new("code").expect("attribute");
1510        let regex_base = vec![
1511            SchemaFact::Type(TypeFact::new(type_id(TypeKind::Attribute, "code")).expect("type")),
1512            SchemaFact::Value(ValueFact::new(
1513                ValueFactId::new(code.clone()),
1514                ValueTypeTag::String,
1515            )),
1516        ];
1517        let regex = annotation_fact(
1518            AnnotationSubjectId::Value(ValueFactId::new(code)),
1519            AnnotationKindId::Regex,
1520            SchemaAnnotationValue::Regex(
1521                type_bridge_contract::schema::RegexPattern::new("[0-9]+").expect("regex"),
1522            ),
1523        );
1524        let regex_source = declared(regex_base.clone());
1525        let regex_target = declared(regex_base.into_iter().chain([regex.clone()]).collect());
1526        let regex_conditions = derive_safety_conditions(
1527            4,
1528            &SchemaOperation::define(vec![regex]).expect("regex operation"),
1529            &regex_source,
1530            &regex_target,
1531            &profile,
1532        )
1533        .expect("regex gate");
1534        assert!(matches!(
1535            regex_conditions.conditions()[0].condition(),
1536            SafetyCondition::Unresolvable {
1537                reason: UnresolvableSafetyReason::RegexNarrowingRequiresValueRegex,
1538                unlock: SafetyConditionUnlock::ValueRegex,
1539            }
1540        ));
1541    }
1542
1543    #[test]
1544    fn destructive_guards_do_not_reclassify_policy() {
1545        let profile = test_safety_profile();
1546        let person = type_id(TypeKind::Entity, "person");
1547        let type_fact = SchemaFact::Type(TypeFact::new(person).expect("type"));
1548        let source = declared(vec![type_fact.clone()]);
1549        let target = declared(Vec::new());
1550        let conditions = derive_safety_conditions(
1551            0,
1552            &SchemaOperation::undefine(type_fact),
1553            &source,
1554            &target,
1555            &profile,
1556        )
1557        .expect("undefine guard");
1558        assert_eq!(conditions.policy(), SafetyClass::Destructive);
1559        assert!(!conditions.resolves_conditional_requirements());
1560        assert_eq!(
1561            conditions.conditions()[0].policy(),
1562            SafetyClass::Destructive
1563        );
1564        assert!(matches!(
1565            conditions.conditions()[0].condition(),
1566            SafetyCondition::NoInstances {
1567                include_subtypes: true,
1568                ..
1569            }
1570        ));
1571    }
1572
1573    #[test]
1574    fn range_and_values_emit_only_for_actual_narrowing() {
1575        let profile = test_safety_profile();
1576        let age = AttributeId::new("age").expect("attribute");
1577        let subject = AnnotationSubjectId::Value(ValueFactId::new(age.clone()));
1578        let base = [
1579            SchemaFact::Type(TypeFact::new(type_id(TypeKind::Attribute, "age")).expect("type")),
1580            SchemaFact::Value(ValueFact::new(ValueFactId::new(age), ValueTypeTag::Long)),
1581        ];
1582        let range = |lower: Option<i64>, upper: Option<i64>| {
1583            annotation_fact(
1584                subject.clone(),
1585                AnnotationKindId::Range,
1586                SchemaAnnotationValue::Range(
1587                    CanonicalValueRange::new(
1588                        lower.map(CanonicalValue::Long),
1589                        upper.map(CanonicalValue::Long),
1590                    )
1591                    .expect("range"),
1592                ),
1593            )
1594        };
1595        let derive_range = |old: SchemaFact, new: SchemaFact| {
1596            let source = declared(base.iter().cloned().chain([old.clone()]).collect());
1597            let target = declared(base.iter().cloned().chain([new.clone()]).collect());
1598            derive_safety_conditions(
1599                9,
1600                &SchemaOperation::redefine(old, new).expect("range operation"),
1601                &source,
1602                &target,
1603                &profile,
1604            )
1605            .expect("range derivation")
1606        };
1607
1608        let widening = derive_range(range(Some(2), Some(8)), range(Some(1), Some(9)));
1609        assert_eq!(widening.policy(), SafetyClass::Conditional);
1610        assert!(widening.conditions().is_empty());
1611
1612        let narrowing = derive_range(range(Some(1), Some(9)), range(Some(2), Some(8)));
1613        assert_eq!(narrowing.conditions().len(), 2);
1614        assert!(matches!(
1615            narrowing.conditions()[0].condition(),
1616            SafetyCondition::RangeLower {
1617                lower: CanonicalValue::Long(2),
1618                ..
1619            }
1620        ));
1621        assert!(matches!(
1622            narrowing.conditions()[1].condition(),
1623            SafetyCondition::RangeUpper {
1624                upper: CanonicalValue::Long(8),
1625                ..
1626            }
1627        ));
1628        let repeated = derive_range(range(Some(1), Some(9)), range(Some(2), Some(8)));
1629        assert_eq!(
1630            narrowing.conditions()[0].id(),
1631            repeated.conditions()[0].id()
1632        );
1633
1634        let mixed = derive_range(range(Some(2), None), range(None, Some(8)));
1635        assert_eq!(mixed.conditions().len(), 1);
1636        assert!(matches!(
1637            mixed.conditions()[0].condition(),
1638            SafetyCondition::RangeUpper {
1639                upper: CanonicalValue::Long(8),
1640                ..
1641            }
1642        ));
1643
1644        let values = |members: &[i64]| {
1645            annotation_fact(
1646                subject.clone(),
1647                AnnotationKindId::Values,
1648                SchemaAnnotationValue::Values(
1649                    CanonicalValueSet::new(members.iter().copied().map(CanonicalValue::Long))
1650                        .expect("values"),
1651                ),
1652            )
1653        };
1654        let derive_values = |old: SchemaFact, new: SchemaFact| {
1655            let source = declared(base.iter().cloned().chain([old.clone()]).collect());
1656            let target = declared(base.iter().cloned().chain([new.clone()]).collect());
1657            derive_safety_conditions(
1658                10,
1659                &SchemaOperation::redefine(old, new).expect("values operation"),
1660                &source,
1661                &target,
1662                &profile,
1663            )
1664            .expect("values derivation")
1665        };
1666
1667        let superset = derive_values(values(&[2, 4]), values(&[2, 4, 6]));
1668        assert!(superset.conditions().is_empty());
1669        let subset = derive_values(values(&[2, 4, 6]), values(&[2, 4]));
1670        assert_eq!(subset.conditions().len(), 1);
1671        assert!(matches!(
1672            subset.conditions()[0].condition(),
1673            SafetyCondition::ValuesNarrowed { allowed, .. } if allowed == &vec![
1674                CanonicalValue::Long(2),
1675                CanonicalValue::Long(4),
1676            ]
1677        ));
1678        let partial = derive_values(values(&[2, 4]), values(&[4, 6]));
1679        assert_eq!(partial.conditions().len(), 1);
1680    }
1681}
type_bridge_schema/safety_condition.rs

type_bridge_schema/
safety_condition.rs
