From 722c74d1dab29ec3b538206ec5b9dfe2e90372ce Mon Sep 17 00:00:00 2001 From: FreshSoftware4 <99464939+FreshSoftware4@users.noreply.github.com> Date: Thu, 23 Jul 2026 05:49:34 -0700 Subject: [PATCH 1/8] Add incremental closure state --- l64-native/src/closure.rs | 63 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 63 insertions(+) create mode 100644 l64-native/src/closure.rs 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 + } +} From 4997768d8d049cef99af6899775704a0eefa79f8 Mon Sep 17 00:00:00 2001 From: FreshSoftware4 <99464939+FreshSoftware4@users.noreply.github.com> Date: Thu, 23 Jul 2026 05:50:08 -0700 Subject: [PATCH 2/8] Derive reverse dependency index --- l64-native/src/graph/derived.rs | 79 +++++++++++++++++++++++++++++++++ 1 file changed, 79 insertions(+) create mode 100644 l64-native/src/graph/derived.rs 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) + } +} From 04da39f916d9d4b1ec0c9ca9d3b6ddc9491690a2 Mon Sep 17 00:00:00 2001 From: FreshSoftware4 <99464939+FreshSoftware4@users.noreply.github.com> Date: Thu, 23 Jul 2026 05:50:45 -0700 Subject: [PATCH 3/8] Evaluate incremental closure --- l64-native/src/graph/closure.rs | 191 ++++++++++++++++++++++++++++++++ 1 file changed, 191 insertions(+) create mode 100644 l64-native/src/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), + } + } +} From 6731ed34d39ae8a5d9c61cc922bd96646c90c763 Mon Sep 17 00:00:00 2001 From: FreshSoftware4 <99464939+FreshSoftware4@users.noreply.github.com> Date: Thu, 23 Jul 2026 05:51:26 -0700 Subject: [PATCH 4/8] Add incremental closure rail --- ...64_INCREMENTAL_CLOSURE_CHANGE_CHAIN.athens | 45 +++++++++++++++++++ 1 file changed, 45 insertions(+) create mode 100644 LOCUS64_INCREMENTAL_CLOSURE_CHANGE_CHAIN.athens diff --git a/LOCUS64_INCREMENTAL_CLOSURE_CHANGE_CHAIN.athens b/LOCUS64_INCREMENTAL_CLOSURE_CHANGE_CHAIN.athens new file mode 100644 index 0000000..fd9cb4b --- /dev/null +++ b/LOCUS64_INCREMENTAL_CLOSURE_CHANGE_CHAIN.athens @@ -0,0 +1,45 @@ +ATHENS_DEVELOPMENT_RAIL v1 +field=key=current_stage;value=incremental-closure-closure +field=key=projection_authority;value=non_authoritative +field=key=rail_version;value=6 +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=current +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 +END From 756a95cbdcb4fe3d976bd66aea0e4570eb699773 Mon Sep 17 00:00:00 2001 From: FreshSoftware4 <99464939+FreshSoftware4@users.noreply.github.com> Date: Thu, 23 Jul 2026 05:52:16 -0700 Subject: [PATCH 5/8] Test exact incremental closure --- l64-native/tests/closure.rs | 330 ++++++++++++++++++++++++++++++++++++ 1 file changed, 330 insertions(+) create mode 100644 l64-native/tests/closure.rs 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); +} From fd90966af2191e6d9ca5e14e17f0bcaca431c260 Mon Sep 17 00:00:00 2001 From: FreshSoftware4 <99464939+FreshSoftware4@users.noreply.github.com> Date: Thu, 23 Jul 2026 06:07:14 -0700 Subject: [PATCH 6/8] Add exact incremental closure --- l64-native/README.md | 14 ++++++++++++++ l64-native/src/graph.rs | 13 +++++++++++-- l64-native/src/graph/construction.rs | 15 +++++++++++++-- l64-native/src/graph/storage.rs | 1 + l64-native/src/kernel/equality/validation.rs | 7 ++++--- l64-native/src/kernel/proposal.rs | 9 +++++++++ l64-native/src/lib.rs | 2 ++ l64-native/tests/architecture.rs | 7 ++++++- 8 files changed, 60 insertions(+), 8 deletions(-) diff --git a/l64-native/README.md b/l64-native/README.md index 8fbcb47..e352a71 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; @@ -56,3 +58,15 @@ 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. + +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/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/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/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", From f2999ba52c43cb70abe165c488f8f214e4e98b1d Mon Sep 17 00:00:00 2001 From: FreshSoftware4 <99464939+FreshSoftware4@users.noreply.github.com> Date: Thu, 23 Jul 2026 06:12:05 -0700 Subject: [PATCH 7/8] Advance incremental closure rail --- LOCUS64_EXECUTION_COHERENCE_RAIL.athens | 14 ++++++++------ LOCUS64_INCREMENTAL_CLOSURE_CHANGE_CHAIN.athens | 7 ++++--- 2 files changed, 12 insertions(+), 9 deletions(-) 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 index fd9cb4b..0e6cd16 100644 --- a/LOCUS64_INCREMENTAL_CLOSURE_CHANGE_CHAIN.athens +++ b/LOCUS64_INCREMENTAL_CLOSURE_CHANGE_CHAIN.athens @@ -1,7 +1,6 @@ ATHENS_DEVELOPMENT_RAIL v1 -field=key=current_stage;value=incremental-closure-closure field=key=projection_authority;value=non_authoritative -field=key=rail_version;value=6 +field=key=rail_version;value=7 field=key=schema_version;value=1 gate=id=closure-state-evaluator-green gate=id=context-refinement-impact-green @@ -31,7 +30,7 @@ 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=current +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 @@ -42,4 +41,6 @@ history=from_status=current;gates=exact-affected-recompute-green;mode=linear_adv 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 From 291e72ceae72a0d5bf40e971cb5e7c052762a793 Mon Sep 17 00:00:00 2001 From: FreshSoftware4 <99464939+FreshSoftware4@users.noreply.github.com> Date: Thu, 23 Jul 2026 06:13:45 -0700 Subject: [PATCH 8/8] Close incremental closure contract --- l64-native/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/l64-native/README.md b/l64-native/README.md index e352a71..5294fa3 100644 --- a/l64-native/README.md +++ b/l64-native/README.md @@ -57,7 +57,7 @@ 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: