diff --git a/LOCUS64_EXECUTION_COHERENCE_RAIL.athens b/LOCUS64_EXECUTION_COHERENCE_RAIL.athens index 7f1b3ed..c191c09 100644 --- a/LOCUS64_EXECUTION_COHERENCE_RAIL.athens +++ b/LOCUS64_EXECUTION_COHERENCE_RAIL.athens @@ -1,8 +1,8 @@ ATHENS_DEVELOPMENT_RAIL v1 -field=key=current_stage;value=incremental-closure -field=key=next_stage;value=native-upper-projection +field=key=current_stage;value=native-upper-projection +field=key=next_stage;value=legacy-authority-quarantine field=key=projection_authority;value=non_authoritative -field=key=rail_version;value=3 +field=key=rail_version;value=4 field=key=schema_version;value=1 gate=id=incremental-closure-green gate=id=legacy-authority-quarantine-green @@ -19,17 +19,19 @@ stage_field=stage=proof-producing-congruence;key=status;value=complete stage=id=incremental-closure stage_field=stage=incremental-closure;key=depends_on;value=proof-producing-congruence stage_field=stage=incremental-closure;key=required_gates;value=incremental-closure-green -stage_field=stage=incremental-closure;key=status;value=current +stage_field=stage=incremental-closure;key=status;value=complete stage=id=native-upper-projection stage_field=stage=native-upper-projection;key=depends_on;value=incremental-closure stage_field=stage=native-upper-projection;key=required_gates;value=native-upper-projection-green -stage_field=stage=native-upper-projection;key=status;value=next +stage_field=stage=native-upper-projection;key=status;value=current stage=id=legacy-authority-quarantine stage_field=stage=legacy-authority-quarantine;key=depends_on;value=native-upper-projection stage_field=stage=legacy-authority-quarantine;key=required_gates;value=legacy-authority-quarantine-green -stage_field=stage=legacy-authority-quarantine;key=status;value=planned +stage_field=stage=legacy-authority-quarantine;key=status;value=next history=from_status=current;gates=native-constraint-core-green;mode=linear_advance;stage_id=native-constraint-core;to_status=complete history=evidence=github-cbcbfe5d9c4f34baf0ca54306c77a85ac970bd26-run-29990484222;kind=dogfood_promotion_receipt;stage_id=native-constraint-core history=from_status=current;gates=proof-producing-congruence-green;mode=linear_advance;stage_id=proof-producing-congruence;to_status=complete history=evidence=github-0a84bdd3dc232a0db1b79009c3bf99cfd4fb40cd-run-29997066639;kind=dogfood_promotion_receipt;stage_id=proof-producing-congruence +history=from_status=current;gates=incremental-closure-green;mode=linear_advance;stage_id=incremental-closure;to_status=complete +history=evidence=github-fd90966af2191e6d9ca5e14e17f0bcaca431c260-run-30009891592;kind=dogfood_promotion_receipt;stage_id=incremental-closure END diff --git a/LOCUS64_INCREMENTAL_CLOSURE_CHANGE_CHAIN.athens b/LOCUS64_INCREMENTAL_CLOSURE_CHANGE_CHAIN.athens new file mode 100644 index 0000000..0e6cd16 --- /dev/null +++ b/LOCUS64_INCREMENTAL_CLOSURE_CHANGE_CHAIN.athens @@ -0,0 +1,46 @@ +ATHENS_DEVELOPMENT_RAIL v1 +field=key=projection_authority;value=non_authoritative +field=key=rail_version;value=7 +field=key=schema_version;value=1 +gate=id=closure-state-evaluator-green +gate=id=context-refinement-impact-green +gate=id=exact-affected-recompute-green +gate=id=incremental-closure-green +gate=id=local-global-closure-green +gate=id=reverse-incidence-green +stage=id=reverse-incidence +stage_field=stage=reverse-incidence;key=required_gates;value=reverse-incidence-green +stage_field=stage=reverse-incidence;key=status;value=complete +stage=id=closure-state-evaluator +stage_field=stage=closure-state-evaluator;key=depends_on;value=reverse-incidence +stage_field=stage=closure-state-evaluator;key=required_gates;value=closure-state-evaluator-green +stage_field=stage=closure-state-evaluator;key=status;value=complete +stage=id=context-refinement-impact +stage_field=stage=context-refinement-impact;key=depends_on;value=closure-state-evaluator +stage_field=stage=context-refinement-impact;key=required_gates;value=context-refinement-impact-green +stage_field=stage=context-refinement-impact;key=status;value=complete +stage=id=exact-affected-recompute +stage_field=stage=exact-affected-recompute;key=depends_on;value=context-refinement-impact +stage_field=stage=exact-affected-recompute;key=required_gates;value=exact-affected-recompute-green +stage_field=stage=exact-affected-recompute;key=status;value=complete +stage=id=local-global-closure +stage_field=stage=local-global-closure;key=depends_on;value=exact-affected-recompute +stage_field=stage=local-global-closure;key=required_gates;value=local-global-closure-green +stage_field=stage=local-global-closure;key=status;value=complete +stage=id=incremental-closure-closure +stage_field=stage=incremental-closure-closure;key=depends_on;value=local-global-closure +stage_field=stage=incremental-closure-closure;key=required_gates;value=incremental-closure-green +stage_field=stage=incremental-closure-closure;key=status;value=complete +history=from_status=current;gates=reverse-incidence-green;mode=linear_advance;stage_id=reverse-incidence;to_status=complete +history=evidence=local%3A43-tests%2Breverse-index%2Bdecode-rebuild%2Bexact-independent-exclusion;kind=dogfood_promotion_receipt;stage_id=reverse-incidence +history=from_status=current;gates=closure-state-evaluator-green;mode=linear_advance;stage_id=closure-state-evaluator;to_status=complete +history=evidence=local%3Aclosure-closed-open-invalid%2Bevidence-propagation%2Bclippy;kind=dogfood_promotion_receipt;stage_id=closure-state-evaluator +history=from_status=current;gates=context-refinement-impact-green;mode=linear_advance;stage_id=context-refinement-impact;to_status=complete +history=evidence=local%3Adirect-child-constraint-refinement%2Bpositive-discharge%2Bnegative-refusal;kind=dogfood_promotion_receipt;stage_id=context-refinement-impact +history=from_status=current;gates=exact-affected-recompute-green;mode=linear_advance;stage_id=exact-affected-recompute;to_status=complete +history=evidence=local%3Areverse-reachable-only%2Bdownstream-equality%2Bindependent-stability;kind=dogfood_promotion_receipt;stage_id=exact-affected-recompute +history=from_status=current;gates=local-global-closure-green;mode=linear_advance;stage_id=local-global-closure;to_status=complete +history=evidence=local%3Aroot-open%2Bchild-closed-or-invalid%2Bglobal-aggregate;kind=dogfood_promotion_receipt;stage_id=local-global-closure +history=from_status=current;gates=incremental-closure-green;mode=linear_advance;stage_id=incremental-closure-closure;to_status=complete +history=evidence=github-fd90966af2191e6d9ca5e14e17f0bcaca431c260-run-30009891592;kind=dogfood_promotion_receipt;stage_id=incremental-closure-closure +END diff --git a/l64-native/README.md b/l64-native/README.md index 8fbcb47..5294fa3 100644 --- a/l64-native/README.md +++ b/l64-native/README.md @@ -37,6 +37,8 @@ The sixth boundary adds the first native constraint core without creating a para The larger implementation files are factored only at existing item boundaries into construction, typing, transaction, validation, codec, and RNA concerns. This changes review locality without introducing another authority layer or altering canonical bytes. + + The seventh boundary adds proof-producing congruence without promoting a union-find table into authority: - equality is a native type judgment with a deterministically attached equality witness; @@ -55,4 +57,16 @@ State identity is the domain-separated BLAKE3 commitment of canonical native byt The existing `l64-cli` command names now route `L64R1` and `L64D` directly through this native path. Legacy RNA/DNA behavior is classified as compatibility/forensic ingress and is available explicitly through `l64-cli legacy ...`; ambient fallback remains temporarily available with a mandatory deprecation warning. -This remains additive. It does not yet implement incremental dependency closure, native upper-stack projections, or replacement of the legacy runtime, registry, certification, and old packet implementation internally. +This remains additive. It does not yet implement native upper-stack projections or replacement of the legacy runtime, registry, certification, and old packet implementation internally. + +The eighth boundary adds incremental closure without turning invalidation into a second authority database: + +- reverse dependencies and context-local node lists are derived from canonical type/port incidence and rebuilt after decode; +- assumption change is represented by an immutable direct child-context refinement, preserving prior authority in its original scope; +- guarded operations, their judgments, evidence, downstream operations, and equality proofs receive context-relative `Closed`, `Open`, or `Invalid` closure states; +- closure transitions identify the exact reverse-reachable subgraph whose state changed and carry the constraint binding that caused the transition; +- independent structure remains outside the affected set; +- local and global closure are distinguishable; +- closure queries do not alter canonical bytes, commitments, routes, contexts, or journal history. + +The derived reverse index is an in-memory accelerator only. It is excluded from RNA, DNA, state commitments, and authority identity. diff --git a/l64-native/src/closure.rs b/l64-native/src/closure.rs new file mode 100644 index 0000000..a1d0a9a --- /dev/null +++ b/l64-native/src/closure.rs @@ -0,0 +1,63 @@ +use crate::{ContextId, NodeId}; + +#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord)] +pub enum ClosureState { + Closed, + Open, + Invalid, +} + +impl ClosureState { + pub(crate) fn combine(self, other: Self) -> Self { + self.max(other) + } +} + +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub struct ClosureTransition { + node: NodeId, + before: ClosureState, + after: ClosureState, + cause: NodeId, + from_context: ContextId, + to_context: ContextId, +} + +impl ClosureTransition { + pub(crate) fn new( + node: NodeId, + before: ClosureState, + after: ClosureState, + cause: NodeId, + from_context: ContextId, + to_context: ContextId, + ) -> Self { + Self { + node, + before, + after, + cause, + from_context, + to_context, + } + } + + pub fn node(&self) -> NodeId { + self.node + } + pub fn before(&self) -> ClosureState { + self.before + } + pub fn after(&self) -> ClosureState { + self.after + } + pub fn cause(&self) -> NodeId { + self.cause + } + pub fn from_context(&self) -> ContextId { + self.from_context + } + pub fn to_context(&self) -> ContextId { + self.to_context + } +} diff --git a/l64-native/src/graph.rs b/l64-native/src/graph.rs index 2ff6af9..1039764 100644 --- a/l64-native/src/graph.rs +++ b/l64-native/src/graph.rs @@ -2,8 +2,8 @@ use std::collections::BTreeMap; use crate::kernel::{ConstraintState, EqualityRule, EvidencePlan}; use crate::{ - ConstraintKind, ContextDelta, Dimension, JournalEvent, LocusWord, Obstruction, OpCode, Port, - PortRole, Route, + ClosureState, ClosureTransition, ConstraintKind, ContextDelta, Dimension, JournalEvent, + LocusWord, Obstruction, OpCode, Port, PortRole, Route, }; pub type NodeId = u32; @@ -67,6 +67,12 @@ impl Node { } } +#[derive(Debug, Clone, Default)] +struct DerivedIndex { + reverse: Vec>, + by_context: Vec>, +} + #[derive(Debug, Clone)] pub struct Graph { nodes: Vec, @@ -75,6 +81,7 @@ pub struct Graph { routes: BTreeMap, journal: Vec, commitment: [u8; 32], + derived: DerivedIndex, } impl Default for Graph { @@ -87,3 +94,5 @@ include!("graph/construction.rs"); include!("graph/typing.rs"); include!("graph/storage.rs"); include!("graph/context.rs"); +include!("graph/derived.rs"); +include!("graph/closure.rs"); diff --git a/l64-native/src/graph/closure.rs b/l64-native/src/graph/closure.rs new file mode 100644 index 0000000..ea819e7 --- /dev/null +++ b/l64-native/src/graph/closure.rs @@ -0,0 +1,191 @@ +impl Graph { + pub fn closure_state( + &self, + context: ContextId, + node: NodeId, + ) -> Result { + self.ensure_context(context)?; + self.ensure_node(node)?; + let mut memo = vec![None; self.node_count()]; + self.closure_state_inner(context, node, &mut memo) + } + + pub fn context_closure(&self, context: ContextId) -> Result { + let nodes = self.visible_nodes(context)?; + let mut memo = vec![None; self.node_count()]; + let mut state = ClosureState::Closed; + for node in nodes { + state = state.combine(self.closure_state_inner(context, node, &mut memo)?); + if state == ClosureState::Invalid { + break; + } + } + Ok(state) + } + + pub fn global_closure(&self) -> Result { + let mut state = ClosureState::Closed; + for context in 0..self.context_count() as ContextId { + state = state.combine(self.context_closure(context)?); + if state == ClosureState::Invalid { + break; + } + } + Ok(state) + } + + pub fn closure_transitions( + &self, + from_context: ContextId, + to_context: ContextId, + ) -> Result, Obstruction> { + self.ensure_context(from_context)?; + let refinement = self.ensure_context(to_context)?; + if refinement.parent() != from_context { + return Err(Obstruction::ContextNotDirectRefinement { + parent: from_context, + child: to_context, + }); + } + let cause = refinement.binding().ok_or(Obstruction::UnknownContext { + context: to_context, + })?; + let (subject, _, _) = self.constraint_parts(cause).map_err(|_| { + Obstruction::RefinementBindingNotConstraint { + context: to_context, + binding: cause, + } + })?; + let affected = self.affected_nodes(subject)?; + let mut before_memo = vec![None; self.node_count()]; + let mut after_memo = vec![None; self.node_count()]; + let mut transitions = Vec::new(); + for node in affected { + let record = self.ensure_node(node)?; + if !self.context_visible(record.context(), from_context) { + continue; + } + let before = self.closure_state_inner(from_context, node, &mut before_memo)?; + let after = self.closure_state_inner(to_context, node, &mut after_memo)?; + if before != after { + transitions.push(ClosureTransition::new( + node, + before, + after, + cause, + from_context, + to_context, + )); + } + } + Ok(transitions) + } + + fn closure_state_inner( + &self, + context: ContextId, + node: NodeId, + memo: &mut [Option], + ) -> Result { + if let Some(state) = memo[node as usize] { + return Ok(state); + } + let record = self.ensure_node(node)?; + if !self.context_visible(record.context(), context) { + memo[node as usize] = Some(ClosureState::Invalid); + return Ok(ClosureState::Invalid); + } + + let state = match record.opcode() { + opcode if opcode.is_executable() => { + self.executable_closure_state(context, node, memo)? + } + OpCode::TypeJudgment => { + let subject = self + .ports(node) + .and_then(|ports| ports.first()) + .map(Port::target) + .ok_or(Obstruction::MalformedEvidence { node })?; + self.closure_state_inner(context, subject, memo)? + } + OpCode::KernelWitness | OpCode::Obligation => { + let judgment = record + .ty() + .ok_or(Obstruction::MalformedEvidence { node })?; + self.closure_state_inner(context, judgment, memo)? + } + OpCode::TypeEquality => self.equality_closure_state(context, node, memo)?, + OpCode::EqualityWitness => { + let judgment = record + .ty() + .ok_or(Obstruction::MalformedEquality { node })?; + self.closure_state_inner(context, judgment, memo)? + } + _ => ClosureState::Closed, + }; + memo[node as usize] = Some(state); + Ok(state) + } + + fn executable_closure_state( + &self, + context: ContextId, + node: NodeId, + memo: &mut [Option], + ) -> Result { + let record = self.ensure_node(node)?; + let ports = self + .ports(node) + .ok_or(Obstruction::UnknownNode { node })?; + let inputs = ports.iter().map(Port::target).collect::>(); + let mut state = ClosureState::Closed; + for input in &inputs { + state = state.combine(self.closure_state_inner(context, *input, memo)?); + } + if state == ClosureState::Invalid { + return Ok(state); + } + let output_type = record.ty().ok_or(Obstruction::ExpectedType { node })?; + let own = match self.validate_operation(context, record.opcode(), &inputs, output_type) { + Ok(EvidencePlan::Witness) => ClosureState::Closed, + Ok(EvidencePlan::Obligation { .. }) => ClosureState::Open, + Err(_) => ClosureState::Invalid, + }; + Ok(state.combine(own)) + } + + fn equality_closure_state( + &self, + context: ContextId, + judgment: NodeId, + memo: &mut [Option], + ) -> Result { + let (left, right) = self.equality_parts(judgment)?; + let mut state = self + .closure_state_inner(context, left, memo)? + .combine(self.closure_state_inner(context, right, memo)?); + if state == ClosureState::Invalid { + return Ok(state); + } + let witness = self + .equality_witness_for(judgment) + .ok_or(Obstruction::MalformedEquality { node: judgment })?; + let witness_node = self.ensure_node(witness)?; + let rule = EqualityRule::from_raw(witness_node.payload() as u8) + .ok_or(Obstruction::MalformedEquality { node: witness })?; + let premise_ports = self + .ports(witness) + .ok_or(Obstruction::MalformedEquality { node: witness })?; + let premises = premise_ports.iter().map(Port::target).collect::>(); + for premise in &premises { + state = state.combine(self.closure_state_inner(context, *premise, memo)?); + } + if state == ClosureState::Invalid { + return Ok(state); + } + match self.validate_equality_rule(context, left, right, rule, &premises) { + Ok(()) => Ok(state), + Err(_) => Ok(ClosureState::Invalid), + } + } +} diff --git a/l64-native/src/graph/construction.rs b/l64-native/src/graph/construction.rs index 9b8f7e8..e401956 100644 --- a/l64-native/src/graph/construction.rs +++ b/l64-native/src/graph/construction.rs @@ -6,14 +6,17 @@ impl Graph { routes: BTreeMap, commitment: [u8; 32], ) -> Self { - Self { + let mut graph = Self { nodes, ports, contexts, routes, journal: Vec::new(), commitment, - } + derived: DerivedIndex::default(), + }; + graph.rebuild_derived_index(); + graph } pub fn new() -> Self { @@ -24,6 +27,7 @@ impl Graph { routes: BTreeMap::new(), journal: Vec::new(), commitment: [0; 32], + derived: DerivedIndex::empty(1), }; graph.commitment = crate::codec::state_commitment(&graph); graph @@ -77,6 +81,7 @@ impl Graph { let before = self.commitment; let id = self.contexts.len() as ContextId; self.contexts.push(ContextDelta { parent, binding }); + self.derived.by_context.push(Vec::new()); let after = crate::codec::state_commitment(self); self.push_event(OpCode::ExtendContext, binding, before, after); self.commitment = after; @@ -263,6 +268,9 @@ impl Graph { self.routes.insert(route, operation); self.routes.insert(judgment_route, judgment); self.routes.insert(evidence_route, evidence); + self.register_derived_node(operation); + self.register_derived_node(judgment); + self.register_derived_node(evidence); let after = crate::codec::state_commitment(self); self.push_event(opcode, operation, before, after); @@ -319,6 +327,8 @@ impl Graph { self.routes.insert(route, judgment); self.routes.insert(evidence_route, evidence); + self.register_derived_node(judgment); + self.register_derived_node(evidence); let after = crate::codec::state_commitment(self); self.push_event(OpCode::EqualityWitness, judgment, before, after); self.commitment = after; @@ -329,4 +339,5 @@ impl Graph { commitment: after, } } + } diff --git a/l64-native/src/graph/derived.rs b/l64-native/src/graph/derived.rs new file mode 100644 index 0000000..560c39b --- /dev/null +++ b/l64-native/src/graph/derived.rs @@ -0,0 +1,79 @@ +impl DerivedIndex { + fn empty(context_count: usize) -> Self { + Self { + reverse: Vec::new(), + by_context: vec![Vec::new(); context_count], + } + } +} + +impl Graph { + fn rebuild_derived_index(&mut self) { + self.derived = DerivedIndex::empty(self.contexts.len()); + self.derived.reverse.resize_with(self.nodes.len(), Vec::new); + for node in 0..self.nodes.len() as NodeId { + self.register_derived_node(node); + } + } + + fn register_derived_node(&mut self, node: NodeId) { + let record = self.nodes[node as usize]; + while self.derived.reverse.len() <= node as usize { + self.derived.reverse.push(Vec::new()); + } + while self.derived.by_context.len() <= record.context() as usize { + self.derived.by_context.push(Vec::new()); + } + self.derived.by_context[record.context() as usize].push(node); + + let mut dependencies = Vec::new(); + if let Some(ty) = record.ty() { + dependencies.push(ty); + } + dependencies.extend(self.ports[record.port_range()].iter().map(Port::target)); + dependencies.sort_unstable(); + dependencies.dedup(); + for dependency in dependencies { + self.derived.reverse[dependency as usize].push(node); + } + } + + pub fn direct_dependents(&self, node: NodeId) -> Result<&[NodeId], Obstruction> { + self.ensure_node(node)?; + Ok(&self.derived.reverse[node as usize]) + } + + pub fn affected_nodes(&self, seed: NodeId) -> Result, Obstruction> { + self.ensure_node(seed)?; + let mut affected = std::collections::BTreeSet::from([seed]); + let mut queue = std::collections::VecDeque::from([seed]); + while let Some(current) = queue.pop_front() { + for dependent in &self.derived.reverse[current as usize] { + if affected.insert(*dependent) { + queue.push_back(*dependent); + } + } + } + Ok(affected.into_iter().collect()) + } + + fn visible_nodes(&self, context: ContextId) -> Result, Obstruction> { + self.ensure_context(context)?; + let mut contexts = Vec::new(); + let mut cursor = context; + loop { + contexts.push(cursor); + if cursor == ROOT_CONTEXT { + break; + } + cursor = self.ensure_context(cursor)?.parent(); + } + contexts.reverse(); + let mut nodes = Vec::new(); + for context in contexts { + nodes.extend_from_slice(&self.derived.by_context[context as usize]); + } + nodes.sort_unstable(); + Ok(nodes) + } +} diff --git a/l64-native/src/graph/storage.rs b/l64-native/src/graph/storage.rs index b6ba2d2..0383f9a 100644 --- a/l64-native/src/graph/storage.rs +++ b/l64-native/src/graph/storage.rs @@ -81,6 +81,7 @@ impl Graph { port_count: ports.len() as u16, }); self.routes.insert(route, node); + self.register_derived_node(node); let after = crate::codec::state_commitment(self); self.push_event(opcode, node, before, after); self.commitment = after; diff --git a/l64-native/src/kernel/equality/validation.rs b/l64-native/src/kernel/equality/validation.rs index dbd8286..4f612d2 100644 --- a/l64-native/src/kernel/equality/validation.rs +++ b/l64-native/src/kernel/equality/validation.rs @@ -47,7 +47,8 @@ impl Graph { Ok(()) } - fn validate_equality_rule( + + pub(crate) fn validate_equality_rule( &self, context: ContextId, left: NodeId, @@ -183,7 +184,7 @@ impl Graph { self.equality_parts(premise) } - fn equality_witness_for(&self, judgment: NodeId) -> Option { + pub(crate) fn equality_witness_for(&self, judgment: NodeId) -> Option { let route = self.route_for_node(judgment)?; self.resolve(&route.composed(EVIDENCE_LOCUS)) } @@ -194,7 +195,7 @@ impl Graph { .find_map(|(route, candidate)| (*candidate == node).then_some(route)) } - fn context_visible(&self, ancestor: ContextId, mut context: ContextId) -> bool { + pub(crate) fn context_visible(&self, ancestor: ContextId, mut context: ContextId) -> bool { loop { if ancestor == context { return true; diff --git a/l64-native/src/kernel/proposal.rs b/l64-native/src/kernel/proposal.rs index e0a0764..6e584ab 100644 --- a/l64-native/src/kernel/proposal.rs +++ b/l64-native/src/kernel/proposal.rs @@ -216,4 +216,13 @@ pub enum Obstruction { left: NodeId, right: NodeId, }, + ContextNotDirectRefinement { + parent: ContextId, + child: ContextId, + }, + RefinementBindingNotConstraint { + context: ContextId, + binding: NodeId, + }, } + diff --git a/l64-native/src/lib.rs b/l64-native/src/lib.rs index 8e31bcc..0cfefb3 100644 --- a/l64-native/src/lib.rs +++ b/l64-native/src/lib.rs @@ -1,5 +1,6 @@ #![forbid(unsafe_code)] +mod closure; mod codec; mod context; mod dimension; @@ -10,6 +11,7 @@ mod kernel; mod rna; mod route; +pub use closure::{ClosureState, ClosureTransition}; pub use codec::{DecodeError, canonical_bytes, decode_canonical}; pub use context::ContextDelta; pub use dimension::Dimension; diff --git a/l64-native/tests/architecture.rs b/l64-native/tests/architecture.rs index fd0ff69..860c283 100644 --- a/l64-native/tests/architecture.rs +++ b/l64-native/tests/architecture.rs @@ -1,7 +1,7 @@ use core::mem::size_of; use std::{fs, path::Path}; -use l64_native::{Dimension, Node, Port}; +use l64_native::{ClosureTransition, Dimension, Node, Port}; #[test] fn compact_layout_budgets_hold() { @@ -15,6 +15,11 @@ fn compact_layout_budgets_hold() { "Port grew to {} bytes", size_of::() ); + assert!( + size_of::() <= 24, + "ClosureTransition grew to {} bytes", + size_of::() + ); assert!( size_of::() <= 8, "Dimension grew to {} bytes", diff --git a/l64-native/tests/closure.rs b/l64-native/tests/closure.rs new file mode 100644 index 0000000..cb2fe05 --- /dev/null +++ b/l64-native/tests/closure.rs @@ -0,0 +1,330 @@ +use l64_native::{ + ClosureState, ConstraintKind, Dimension, Graph, LocusWord, Obstruction, Proposal, ROOT_CONTEXT, + Route, canonical_bytes, decode_canonical, +}; + +fn route(index: u64) -> Route { + Route::root(LocusWord(0x434c4f5355524539)).composed(LocusWord(index)) +} + +struct GuardedFixture { + graph: Graph, + subject: u32, + sqrt: u32, + sqrt_evidence: u32, + downstream: u32, + independent: u32, +} + +fn guarded_fixture() -> GuardedFixture { + let mut graph = Graph::new(); + let scalar = graph.declare_atom_type(route(1), LocusWord(0x52)).unwrap(); + let dimensionless = Dimension::new([0, 0, 0, 0, 0, 0, 0]); + let quantity = graph + .declare_quantity_type(route(2), scalar, dimensionless) + .unwrap(); + let subject = graph + .insert_value(route(3), ROOT_CONTEXT, quantity) + .unwrap(); + let peer = graph + .insert_value(route(4), ROOT_CONTEXT, quantity) + .unwrap(); + let sqrt_result = graph + .transact(Proposal::square_root( + route(5), + ROOT_CONTEXT, + subject, + quantity, + )) + .unwrap(); + let downstream = graph + .transact(Proposal::multiply( + route(6), + ROOT_CONTEXT, + sqrt_result.node, + peer, + quantity, + )) + .unwrap() + .node; + + let independent_left = graph + .insert_value(route(7), ROOT_CONTEXT, quantity) + .unwrap(); + let independent_right = graph + .insert_value(route(8), ROOT_CONTEXT, quantity) + .unwrap(); + let independent = graph + .transact(Proposal::add( + route(9), + ROOT_CONTEXT, + independent_left, + independent_right, + quantity, + )) + .unwrap() + .node; + + GuardedFixture { + graph, + subject, + sqrt: sqrt_result.node, + sqrt_evidence: sqrt_result.evidence, + downstream, + independent, + } +} + +#[test] +fn reverse_incidence_is_exact_and_rebuilt_from_canonical_graph() { + let fixture = guarded_fixture(); + let affected = fixture.graph.affected_nodes(fixture.subject).unwrap(); + assert!(affected.contains(&fixture.sqrt)); + assert!(affected.contains(&fixture.sqrt_evidence)); + assert!(affected.contains(&fixture.downstream)); + assert!(!affected.contains(&fixture.independent)); + + let bytes = canonical_bytes(&fixture.graph); + let decoded = decode_canonical(&bytes).unwrap(); + assert_eq!(decoded.affected_nodes(fixture.subject).unwrap(), affected); + assert_eq!(canonical_bytes(&decoded), bytes); +} + +#[test] +fn positive_refinement_discharges_only_the_dependent_obligation_chain() { + let mut fixture = guarded_fixture(); + assert_eq!( + fixture + .graph + .closure_state(ROOT_CONTEXT, fixture.sqrt) + .unwrap(), + ClosureState::Open + ); + assert_eq!( + fixture.graph.context_closure(ROOT_CONTEXT).unwrap(), + ClosureState::Open + ); + + let cause = fixture + .graph + .declare_constraint( + route(20), + ROOT_CONTEXT, + fixture.subject, + ConstraintKind::NonNegative, + true, + ) + .unwrap(); + let child = fixture.graph.extend_context(ROOT_CONTEXT, cause).unwrap(); + let transitions = fixture + .graph + .closure_transitions(ROOT_CONTEXT, child) + .unwrap(); + + assert!(transitions.iter().any(|transition| { + transition.node() == fixture.sqrt + && transition.before() == ClosureState::Open + && transition.after() == ClosureState::Closed + && transition.cause() == cause + })); + assert!(transitions.iter().any(|transition| { + transition.node() == fixture.sqrt_evidence + && transition.before() == ClosureState::Open + && transition.after() == ClosureState::Closed + })); + assert!( + !transitions + .iter() + .any(|transition| transition.node() == fixture.independent) + ); + assert_eq!( + fixture.graph.context_closure(child).unwrap(), + ClosureState::Closed + ); + assert_eq!( + fixture.graph.global_closure().unwrap(), + ClosureState::Open, + "the original open context remains valid and independently visible" + ); +} + +#[test] +fn negative_refinement_invalidates_exactly_the_reverse_reachable_subgraph() { + let mut fixture = guarded_fixture(); + let independent_before = fixture + .graph + .closure_state(ROOT_CONTEXT, fixture.independent) + .unwrap(); + let cause = fixture + .graph + .declare_constraint( + route(30), + ROOT_CONTEXT, + fixture.subject, + ConstraintKind::NonNegative, + false, + ) + .unwrap(); + let child = fixture.graph.extend_context(ROOT_CONTEXT, cause).unwrap(); + let transitions = fixture + .graph + .closure_transitions(ROOT_CONTEXT, child) + .unwrap(); + + for dependent in [fixture.sqrt, fixture.sqrt_evidence, fixture.downstream] { + assert!(transitions.iter().any(|transition| { + transition.node() == dependent && transition.after() == ClosureState::Invalid + })); + } + assert!( + !transitions + .iter() + .any(|transition| transition.node() == fixture.independent) + ); + assert_eq!( + fixture + .graph + .closure_state(child, fixture.independent) + .unwrap(), + independent_before + ); + assert_eq!( + fixture.graph.context_closure(child).unwrap(), + ClosureState::Invalid + ); + assert_eq!( + fixture.graph.global_closure().unwrap(), + ClosureState::Invalid + ); +} + +#[test] +fn equality_provenance_is_invalidated_when_its_endpoint_closure_fails() { + let mut fixture = guarded_fixture(); + let equality = fixture + .graph + .prove_reflexive_equality(route(40), ROOT_CONTEXT, fixture.sqrt) + .unwrap(); + let cause = fixture + .graph + .declare_constraint( + route(41), + ROOT_CONTEXT, + fixture.subject, + ConstraintKind::NonNegative, + false, + ) + .unwrap(); + let child = fixture.graph.extend_context(ROOT_CONTEXT, cause).unwrap(); + let transitions = fixture + .graph + .closure_transitions(ROOT_CONTEXT, child) + .unwrap(); + + assert!(transitions.iter().any(|transition| { + transition.node() == equality.node && transition.after() == ClosureState::Invalid + })); + assert!(transitions.iter().any(|transition| { + transition.node() == equality.evidence && transition.after() == ClosureState::Invalid + })); +} + +#[test] +fn closure_transition_requires_one_direct_constraint_refinement() { + let mut fixture = guarded_fixture(); + let first_binding = fixture + .graph + .declare_constraint( + route(50), + ROOT_CONTEXT, + fixture.subject, + ConstraintKind::NonNegative, + true, + ) + .unwrap(); + let child = fixture + .graph + .extend_context(ROOT_CONTEXT, first_binding) + .unwrap(); + let second_subject = fixture + .graph + .insert_value( + route(51), + child, + fixture.graph.node(fixture.subject).unwrap().ty().unwrap(), + ) + .unwrap(); + let second_binding = fixture + .graph + .declare_constraint( + route(52), + child, + second_subject, + ConstraintKind::NonNegative, + true, + ) + .unwrap(); + let grandchild = fixture.graph.extend_context(child, second_binding).unwrap(); + + assert_eq!( + fixture.graph.closure_transitions(ROOT_CONTEXT, grandchild), + Err(Obstruction::ContextNotDirectRefinement { + parent: ROOT_CONTEXT, + child: grandchild, + }) + ); + + let value_binding = fixture + .graph + .insert_value( + route(53), + ROOT_CONTEXT, + fixture.graph.node(fixture.subject).unwrap().ty().unwrap(), + ) + .unwrap(); + let non_constraint_child = fixture + .graph + .extend_context(ROOT_CONTEXT, value_binding) + .unwrap(); + assert_eq!( + fixture + .graph + .closure_transitions(ROOT_CONTEXT, non_constraint_child), + Err(Obstruction::RefinementBindingNotConstraint { + context: non_constraint_child, + binding: value_binding, + }) + ); +} + +#[test] +fn closure_queries_do_not_mutate_authority_or_canonical_bytes() { + let mut fixture = guarded_fixture(); + let cause = fixture + .graph + .declare_constraint( + route(60), + ROOT_CONTEXT, + fixture.subject, + ConstraintKind::NonNegative, + true, + ) + .unwrap(); + let child = fixture.graph.extend_context(ROOT_CONTEXT, cause).unwrap(); + let before = canonical_bytes(&fixture.graph); + let commitment = fixture.graph.state_commitment(); + let journal = fixture.graph.journal_len(); + + let _ = fixture.graph.direct_dependents(fixture.subject).unwrap(); + let _ = fixture.graph.affected_nodes(fixture.subject).unwrap(); + let _ = fixture + .graph + .closure_transitions(ROOT_CONTEXT, child) + .unwrap(); + let _ = fixture.graph.context_closure(child).unwrap(); + let _ = fixture.graph.global_closure().unwrap(); + + assert_eq!(canonical_bytes(&fixture.graph), before); + assert_eq!(fixture.graph.state_commitment(), commitment); + assert_eq!(fixture.graph.journal_len(), journal); +}