type_bridge_schema/
safety_condition.rs

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

type_bridge_schema/
safety_condition.rs
