Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 3 additions & 2 deletions .github/workflows/native-core.yml
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ on:
- Cargo.toml
- Cargo.lock
- l64-native/**
- l64-projection/**
- l64-cli/**
- LOCUS64_*_RAIL.athens
- LOCUS64_*_CHANGE_CHAIN.athens
Expand Down Expand Up @@ -39,5 +40,5 @@ jobs:
- name: Test workspace
run: cargo test -q

- name: Lint native core
run: cargo clippy -p l64-native --all-targets -- -D warnings
- name: Lint native projection spine
run: cargo clippy -p l64-native -p l64-projection --all-targets -- -D warnings
1 change: 1 addition & 0 deletions Cargo.toml
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
[workspace]
members = [
"l64-native",
"l64-projection",
"l64-core",
"l64-locus",
"l64-research",
Expand Down
12 changes: 7 additions & 5 deletions LOCUS64_EXECUTION_COHERENCE_RAIL.athens
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
ATHENS_DEVELOPMENT_RAIL v1
field=key=current_stage;value=native-upper-projection
field=key=next_stage;value=legacy-authority-quarantine
field=key=current_stage;value=legacy-authority-quarantine
field=key=next_stage;value=complete
field=key=projection_authority;value=non_authoritative
field=key=rail_version;value=4
field=key=rail_version;value=5
field=key=schema_version;value=1
gate=id=incremental-closure-green
gate=id=legacy-authority-quarantine-green
Expand All @@ -23,15 +23,17 @@ 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=current
stage_field=stage=native-upper-projection;key=status;value=complete
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=next
stage_field=stage=legacy-authority-quarantine;key=status;value=current
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
history=from_status=current;gates=native-upper-projection-green;mode=linear_advance;stage_id=native-upper-projection;to_status=complete
history=evidence=github-0ad8acc52f35362262c383efd02cc455e6778489-run-30139859138;kind=dogfood_promotion_receipt;stage_id=native-upper-projection
END
60 changes: 60 additions & 0 deletions LOCUS64_NATIVE_UPPER_PROJECTION_CHANGE_CHAIN.athens
Original file line number Diff line number Diff line change
@@ -0,0 +1,60 @@
ATHENS_DEVELOPMENT_RAIL v1
field=key=projection_authority;value=non_authoritative
field=key=rail_version;value=2
field=key=schema_version;value=1
gate=id=projection-contract-green
gate=id=read-only-query-green
gate=id=atlas-view-green
gate=id=certification-view-green
gate=id=replay-view-green
gate=id=report-research-view-green
gate=id=deterministic-regeneration-green
gate=id=native-upper-projection-green
stage=id=projection-contract
stage_field=stage=projection-contract;key=required_gates;value=projection-contract-green
stage_field=stage=projection-contract;key=status;value=complete
stage=id=read-only-native-query
stage_field=stage=read-only-native-query;key=depends_on;value=projection-contract
stage_field=stage=read-only-native-query;key=required_gates;value=read-only-query-green
stage_field=stage=read-only-native-query;key=status;value=complete
stage=id=atlas-candidate-view
stage_field=stage=atlas-candidate-view;key=depends_on;value=read-only-native-query
stage_field=stage=atlas-candidate-view;key=required_gates;value=atlas-view-green
stage_field=stage=atlas-candidate-view;key=status;value=complete
stage=id=certification-burden-view
stage_field=stage=certification-burden-view;key=depends_on;value=atlas-candidate-view
stage_field=stage=certification-burden-view;key=required_gates;value=certification-view-green
stage_field=stage=certification-burden-view;key=status;value=complete
stage=id=replay-causal-view
stage_field=stage=replay-causal-view;key=depends_on;value=certification-burden-view
stage_field=stage=replay-causal-view;key=required_gates;value=replay-view-green
stage_field=stage=replay-causal-view;key=status;value=complete
stage=id=report-research-view
stage_field=stage=report-research-view;key=depends_on;value=replay-causal-view
stage_field=stage=report-research-view;key=required_gates;value=report-research-view-green
stage_field=stage=report-research-view;key=status;value=complete
stage=id=deterministic-regeneration
stage_field=stage=deterministic-regeneration;key=depends_on;value=report-research-view
stage_field=stage=deterministic-regeneration;key=required_gates;value=deterministic-regeneration-green
stage_field=stage=deterministic-regeneration;key=status;value=complete
stage=id=native-upper-projection-closure
stage_field=stage=native-upper-projection-closure;key=depends_on;value=deterministic-regeneration
stage_field=stage=native-upper-projection-closure;key=required_gates;value=native-upper-projection-green
stage_field=stage=native-upper-projection-closure;key=status;value=complete
history=from_status=current;gates=projection-contract-green;mode=linear_advance;stage_id=projection-contract;to_status=complete
history=evidence=local%3Aprojection-source-binding%2Bnonmutation%2Bno-storage%2Bsingle-native-dependency;kind=dogfood_promotion_receipt;stage_id=projection-contract
history=from_status=current;gates=read-only-query-green;mode=linear_advance;stage_id=read-only-native-query;to_status=complete
history=evidence=local%3Acontext%2Bvisible-node%2Broute%2Bequality-evidence-read-surface;kind=dogfood_promotion_receipt;stage_id=read-only-native-query
history=from_status=current;gates=atlas-view-green;mode=linear_advance;stage_id=atlas-candidate-view;to_status=complete
history=evidence=local%3Atyped-operation-and-equality-candidates%2Bnative-route-resolution;kind=dogfood_promotion_receipt;stage_id=atlas-candidate-view
history=from_status=current;gates=certification-view-green;mode=linear_advance;stage_id=certification-burden-view;to_status=complete
history=evidence=local%3Aclosed-open-invalid%2Bcontext-discharge-without-authority-rewrite;kind=dogfood_promotion_receipt;stage_id=certification-burden-view
history=from_status=current;gates=replay-view-green;mode=linear_advance;stage_id=replay-causal-view;to_status=complete
history=evidence=local%3Ajournal-bound-replay%2Bsource-route-causality%2Bjournal-divergence-rejection;kind=dogfood_promotion_receipt;stage_id=replay-causal-view
history=from_status=current;gates=report-research-view-green;mode=linear_advance;stage_id=report-research-view;to_status=complete
history=evidence=local%3Adeterministic-counts%2Bobligation-and-invalid-routes%2Baffected-set-ranking;kind=dogfood_promotion_receipt;stage_id=report-research-view
history=from_status=current;gates=deterministic-regeneration-green;mode=linear_advance;stage_id=deterministic-regeneration;to_status=complete
history=evidence=local%3A56-tests%2Bstrict-clippy%2Bformat%2Blive-projection-execution%2Bforged-and-stale-rejection;kind=dogfood_promotion_receipt;stage_id=deterministic-regeneration
history=from_status=current;gates=native-upper-projection-green;mode=linear_advance;stage_id=native-upper-projection-closure;to_status=complete
history=evidence=github-0ad8acc52f35362262c383efd02cc455e6778489-run-30139859138;kind=dogfood_promotion_receipt;stage_id=native-upper-projection-closure
END
16 changes: 15 additions & 1 deletion l64-native/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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 native upper-stack projections or replacement of the legacy runtime, registry, certification, and old packet implementation internally.
This remains additive. Native upper projections now exist as read-only derivations in `l64-projection`; replacement and quarantine of the legacy runtime, registry, certification, and old packet implementation remain incomplete.

The eighth boundary adds incremental closure without turning invalidation into a second authority database:

Expand All @@ -70,3 +70,17 @@ The eighth boundary adds incremental closure without turning invalidation into a
- 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.

The ninth boundary derives the first native upper views without turning any view into authority:

- `l64-projection` depends only on `l64-native`;
- atlas candidates are reconstructed from executable operations, equalities, ports, routes, closure, and native evidence;
- certification burdens distinguish discharged, open, invalid, and missing-evidence states without rewriting obligation nodes;
- replay is a deterministic view of the native journal and rejects a canonical decode that lacks that runtime history;
- reporting counts visible native structure and exposes obligation and invalid routes;
- research ranking follows open, invalid, and high-impact reverse-reachable structure;
- every view binds to the native commitment, context, structural counts, journal length, and projection version;
- verification rebuilds the complete view and requires exact equality;
- the projection crate contains no storage, registry, cache, alternate graph, import, promotion, serialization, or hash authority.

`LOCUS64_NATIVE_UPPER_PROJECTION_CHANGE_CHAIN.athens` is complete on repository evidence. The parent execution rail has advanced to legacy authority quarantine.
5 changes: 4 additions & 1 deletion l64-native/src/graph/construction.rs
Original file line number Diff line number Diff line change
Expand Up @@ -58,6 +58,10 @@ impl Graph {
self.contexts.len()
}

pub fn context(&self, id: ContextId) -> Option<&ContextDelta> {
self.contexts.get(id as usize)
}

pub fn journal_len(&self) -> usize {
self.journal.len()
}
Expand Down Expand Up @@ -339,5 +343,4 @@ impl Graph {
commitment: after,
}
}

}
2 changes: 1 addition & 1 deletion l64-native/src/graph/derived.rs
Original file line number Diff line number Diff line change
Expand Up @@ -57,7 +57,7 @@ impl Graph {
Ok(affected.into_iter().collect())
}

fn visible_nodes(&self, context: ContextId) -> Result<Vec<NodeId>, Obstruction> {
pub fn visible_nodes(&self, context: ContextId) -> Result<Vec<NodeId>, Obstruction> {
self.ensure_context(context)?;
let mut contexts = Vec::new();
let mut cursor = context;
Expand Down
9 changes: 5 additions & 4 deletions l64-native/src/kernel/equality/validation.rs
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,6 @@ impl Graph {
Ok(())
}


pub(crate) fn validate_equality_rule(
&self,
context: ContextId,
Expand Down Expand Up @@ -184,12 +183,12 @@ impl Graph {
self.equality_parts(premise)
}

pub(crate) fn equality_witness_for(&self, judgment: NodeId) -> Option<NodeId> {
pub fn equality_witness_for(&self, judgment: NodeId) -> Option<NodeId> {
let route = self.route_for_node(judgment)?;
self.resolve(&route.composed(EVIDENCE_LOCUS))
}

fn route_for_node(&self, node: NodeId) -> Option<&Route> {
pub fn route_for_node(&self, node: NodeId) -> Option<&Route> {
self.routes_raw()
.iter()
.find_map(|(route, candidate)| (*candidate == node).then_some(route))
Expand All @@ -213,7 +212,9 @@ impl Graph {
fn same_equality_sort(&self, left: &crate::Node, right: &crate::Node) -> bool {
match (left.ty(), right.ty()) {
(Some(left_ty), Some(right_ty)) => left_ty == right_ty,
(None, None) => self.equality_endpoint_allowed(left) && self.equality_endpoint_allowed(right),
(None, None) => {
self.equality_endpoint_allowed(left) && self.equality_endpoint_allowed(right)
}
_ => false,
}
}
Expand Down
8 changes: 8 additions & 0 deletions l64-projection/Cargo.toml
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
[package]
name = "l64-projection"
edition.workspace = true
version.workspace = true
license.workspace = true

[dependencies]
l64-native = { path = "../l64-native" }
15 changes: 15 additions & 0 deletions l64-projection/README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
# l64-projection

`l64-projection` derives read-only upper views from `l64-native::Graph` authority.

It provides five coordinated views over one native state and context:

- atlas candidates from executable operation and equality nodes;
- certification burdens from context-relative closure and native evidence;
- replay steps from the native journal;
- deterministic aggregate reporting;
- ranked research candidates from open and invalid reverse-reachable structure.

Every projection carries its native state commitment, context, structural counts, journal length, and projection version. Verification rebuilds the complete view from the graph and requires exact equality. The crate has no storage, registry, cache, import, promotion, serialization, hashing, or alternate graph dependency.

Projection records are expendable. Native authority remains canonical.
29 changes: 29 additions & 0 deletions l64-projection/examples/native_projection.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,29 @@
use l64_native::{Dimension, Graph, LocusWord, Proposal, ROOT_CONTEXT, Route};
use l64_projection::ProjectionSet;

fn route(index: u64) -> Route {
Route::root(LocusWord(0x50524f4a45435431)).composed(LocusWord(index))
}

fn main() {
let mut graph = Graph::new();
let scalar = graph.declare_atom_type(route(1), LocusWord(0x52)).unwrap();
let quantity = graph
.declare_quantity_type(route(2), scalar, Dimension::new([0, 0, 0, 0, 0, 0, 0]))
.unwrap();
let value = graph
.insert_value(route(3), ROOT_CONTEXT, quantity)
.unwrap();
graph
.transact(Proposal::square_root(
route(4),
ROOT_CONTEXT,
value,
quantity,
))
.unwrap();

let projection = ProjectionSet::derive(&graph, ROOT_CONTEXT, 8).unwrap();
projection.verify(&graph).unwrap();
print!("{}", projection.render_text());
}
101 changes: 101 additions & 0 deletions l64-projection/src/atlas.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,101 @@
use crate::{
EvidenceRef, PortRef, ProjectionError, ProjectionSource, SourceRef, closure_rank, evidence_ref,
source_ref,
};
use l64_native::{ClosureState, ContextId, Graph, OpCode, Route};

#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord)]
pub enum AtlasCandidateKind {
Operation,
Equality,
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct AtlasCandidate {
pub kind: AtlasCandidateKind,
pub source: SourceRef,
pub opcode: OpCode,
pub closure: ClosureState,
pub output_type: Option<SourceRef>,
pub ports: Vec<PortRef>,
pub direct_dependents: Vec<SourceRef>,
pub canonical_route: Option<Route>,
pub evidence: Option<EvidenceRef>,
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct AtlasView {
pub source: ProjectionSource,
pub candidates: Vec<AtlasCandidate>,
}

impl AtlasView {
pub fn derive(graph: &Graph, context: ContextId) -> Result<Self, ProjectionError> {
let source = ProjectionSource::capture(graph, context)?;
let mut candidates = Vec::new();
for node in graph.visible_nodes(context)? {
let record = graph.node(node).ok_or(ProjectionError::UnknownNode(node))?;
let kind = match record.opcode() {
OpCode::Compose
| OpCode::MatMul
| OpCode::Add
| OpCode::Multiply
| OpCode::Divide
| OpCode::Sqrt => AtlasCandidateKind::Operation,
OpCode::TypeEquality => AtlasCandidateKind::Equality,
_ => continue,
};
let source = source_ref(graph, node)?;
let output_type = record.ty().map(|id| source_ref(graph, id)).transpose()?;
let ports = graph
.ports(node)
.ok_or(ProjectionError::UnknownNode(node))?
.iter()
.map(|port| {
Ok(PortRef {
role: port.role(),
ordinal: port.ordinal(),
target: source_ref(graph, port.target())?,
})
})
.collect::<Result<Vec<_>, ProjectionError>>()?;
let mut direct_dependents = graph
.direct_dependents(node)?
.iter()
.copied()
.map(|id| source_ref(graph, id))
.collect::<Result<Vec<_>, ProjectionError>>()?;
direct_dependents.sort();
let canonical_route = graph.canonical_representative_route(context, node).ok();
let evidence = evidence_ref(graph, context, node)?;
candidates.push(AtlasCandidate {
kind,
source,
opcode: record.opcode(),
closure: graph.closure_state(context, node)?,
output_type,
ports,
direct_dependents,
canonical_route,
evidence,
});
}
candidates.sort_by(|left, right| {
closure_rank(left.closure)
.cmp(&closure_rank(right.closure))
.then_with(|| left.kind.cmp(&right.kind))
.then_with(|| left.source.route.cmp(&right.source.route))
});
Ok(Self { source, candidates })
}

pub fn verify(&self, graph: &Graph) -> Result<(), ProjectionError> {
self.source.verify(graph)?;
let rebuilt = Self::derive(graph, self.source.context)?;
if &rebuilt == self {
Ok(())
} else {
Err(ProjectionError::ProjectionMismatch)
}
}
}
Loading
Loading