uor-foundation 0.3.0

UOR Foundation — typed Rust traits for the complete ontology. Import and implement.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150

// @generated by uor-crate from uor-ontology — do not edit manually

//! `derivation/` namespace — Computation witnesses recording term rewriting sequences from original terms to their canonical forms..
//!
//! Space: Bridge

use crate::enums::RewriteRule;
use crate::HostTypes;

/// A complete term rewriting witness: the full sequence of rewrite steps transforming an original term into its canonical form.
pub trait Derivation<H: HostTypes> {
    /// Associated type for `Term`.
    type Term: crate::kernel::schema::Term<H>;
    /// The term at the start of the derivation, before any rewriting.
    fn original_term(&self) -> &Self::Term;
    /// The canonical form produced at the end of the derivation.
    fn canonical_term(&self) -> &Self::Term;
    /// Associated type for `Datum`.
    type Datum: crate::kernel::schema::Datum<H>;
    /// The datum value obtained by evaluating the canonical term.
    fn result(&self) -> &Self::Datum;
    /// Associated type for `RewriteStep`.
    type RewriteStep: RewriteStep<H>;
    /// A rewrite step in this derivation.
    fn step(&self) -> &[Self::RewriteStep];
    /// Associated type for `TermMetrics`.
    type TermMetrics: TermMetrics<H>;
    /// Metrics for the canonical term produced by this derivation.
    fn term_metrics(&self) -> &Self::TermMetrics;
}

/// An abstract step in a derivation. Concrete subclasses are RewriteStep (term-level rewriting) and RefinementStep (type-level refinement).
pub trait DerivationStep<H: HostTypes> {}

/// A single rewrite step in a derivation: the application of one rewrite rule to transform a term.
pub trait RewriteStep<H: HostTypes>: DerivationStep<H> {
    /// Associated type for `Term`.
    type Term: crate::kernel::schema::Term<H>;
    /// The term before this rewrite step.
    fn from(&self) -> &Self::Term;
    /// The term after this rewrite step.
    fn to(&self) -> &Self::Term;
    /// The typed rewrite rule applied in this step. Provides a structured reference to a named RewriteRule individual, complementing the string-valued derivation:rule property.
    fn has_rewrite_rule(&self) -> RewriteRule;
}

/// A type-level refinement step: the application of a constraint to narrow a type, pinning additional site coordinates. Complements RewriteStep (term-level) in the derivation hierarchy.
pub trait RefinementStep<H: HostTypes>: DerivationStep<H> {
    /// Associated type for `TypeDefinition`.
    type TypeDefinition: crate::user::type_::TypeDefinition<H>;
    /// The type before this refinement step was applied.
    fn previous_type(&self) -> &Self::TypeDefinition;
    /// Associated type for `Constraint`.
    type Constraint: crate::user::type_::Constraint<H>;
    /// The constraint that was applied in this refinement step.
    fn applied_constraint(&self) -> &Self::Constraint;
    /// The type after this refinement step was applied.
    fn refined_type(&self) -> &Self::TypeDefinition;
    /// The number of site coordinates pinned by this refinement step.
    fn sites_closed(&self) -> u64;
}

/// Metrics describing the size and complexity of a term.
pub trait TermMetrics<H: HostTypes> {
    /// The total number of rewrite steps in this derivation.
    fn step_count(&self) -> u64;
    /// The number of nodes in the canonical term's syntax tree.
    fn term_size(&self) -> u64;
}

/// A single step in the construction of a SynthesizedType: one constraint added to the synthesis candidate and the resulting change in the constraint nerve's topological signature. Ordered by derivation:stepIndex. Analogous to derivation:RewriteStep in the forward pipeline.
pub trait SynthesisStep<H: HostTypes> {
    /// Zero-based sequential index of this step within the synthesis derivation.
    fn step_index(&self) -> u64;
    /// Associated type for `Constraint`.
    type Constraint: crate::user::type_::Constraint<H>;
    /// The constraint added in this synthesis step.
    fn added_constraint(&self) -> &Self::Constraint;
    /// Associated type for `SynthesisSignature`.
    type SynthesisSignature: crate::bridge::observable::SynthesisSignature<H>;
    /// The constraint nerve signature before this synthesis step.
    fn signature_before(&self) -> &Self::SynthesisSignature;
    /// The constraint nerve signature after this synthesis step.
    fn signature_after(&self) -> &Self::SynthesisSignature;
}

/// A persistent snapshot of a ConstraintSearchState at a specific SynthesisStep, allowing a TypeSynthesisResolver to resume exploration after interruption. Essential at Q1+ scale where exhaustive synthesis is computationally significant.
pub trait SynthesisCheckpoint<H: HostTypes> {
    /// Associated type for `SynthesisStep`.
    type SynthesisStep: SynthesisStep<H>;
    /// The SynthesisStep at which this checkpoint was taken.
    fn checkpoint_step(&self) -> &Self::SynthesisStep;
    /// Associated type for `ConstraintSearchState`.
    type ConstraintSearchState: crate::bridge::resolver::ConstraintSearchState<H>;
    /// The ConstraintSearchState snapshot captured by this checkpoint.
    fn checkpoint_state(&self) -> &Self::ConstraintSearchState;
}

/// A peer of derivation:SynthesisStep specialised to inhabitance search. Each step represents one navigation in the constraint nerve, either pinning a site to a value or confirming that a predicate evaluates true on the current partial assignment.
pub trait InhabitanceStep<H: HostTypes>: SynthesisStep<H> {
    /// Associated type for `ConstraintSearchState`.
    type ConstraintSearchState: crate::bridge::resolver::ConstraintSearchState<H>;
    /// The ConstraintSearchState before this InhabitanceStep was taken.
    fn prior_state(&self) -> &Self::ConstraintSearchState;
    /// The ConstraintSearchState after this InhabitanceStep was taken.
    fn successor_state(&self) -> &Self::ConstraintSearchState;
    /// Associated type for `DispatchRule`.
    type DispatchRule: crate::kernel::predicate::DispatchRule<H>;
    /// The predicate:DispatchRule whose evaluation drove this InhabitanceStep.
    fn rule(&self) -> &Self::DispatchRule;
}

/// A peer of derivation:SynthesisCheckpoint specialised to inhabitance search. Marks an audit point where the resolver state can be restored if the search backtracks.
pub trait InhabitanceCheckpoint<H: HostTypes>: SynthesisCheckpoint<H> {
    /// Ordinal index of this checkpoint within the InhabitanceSearchTrace's checkpoint sequence.
    fn checkpoint_index(&self) -> i64;
}

/// Observes the derivation depth of a Datum, computed as the maximum nesting level of derivation:RewriteStep applications producing it. Used as the bound observable for the depthConstraintKind BoundConstraint.
pub trait DerivationDepthObservable<H: HostTypes>:
    crate::bridge::observable::Observable<H>
{
}

/// An ordered sequence of derivation:RewriteStep events produced by replaying a Derivation. Used by uor-foundation-verify to re-derive a certificate from a content-addressed trace without running the deciders. The traceEventCount property records the trace length.
pub trait DerivationTrace<H: HostTypes> {
    /// Number of RewriteStep events recorded in this DerivationTrace. Used by Derivation::replay() to size the fixed-capacity event arena without allocation.
    fn trace_event_count(&self) -> u64;
}

/// The rewrite rule applying the critical identity: neg(bnot(x)) → succ(x). Grounded in op:criticalIdentity.
pub mod critical_identity_rule {
    /// `groundedIn` -> `criticalIdentity`
    pub const GROUNDED_IN: &str = "https://uor.foundation/op/criticalIdentity";
}

/// The rewrite rule applying involution cancellation: f(f(x)) → x for any involution f.
pub mod involution_rule {}

/// The rewrite rule applying associativity to re-bracket nested binary operations.
pub mod associativity_rule {}

/// The rewrite rule applying commutativity to reorder operands of commutative operations.
pub mod commutativity_rule {}

/// The rewrite rule eliminating identity elements: add(x, 0) → x, mul(x, 1) → x, xor(x, 0) → x.
pub mod identity_element_rule {}

/// The rewrite rule normalizing compound expressions to canonical ordering (e.g., sorting operands by address).
pub mod normalization_rule {}