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 @@ -8,6 +8,7 @@ on:
paths:
- Cargo.toml
- Cargo.lock
- l64-symbolic/**
- l64-native/**
- l64-projection/**
- l64-cli/**
Expand Down Expand Up @@ -40,5 +41,5 @@ jobs:
- name: Test workspace
run: cargo test -q

- name: Lint native projection spine
run: cargo clippy -p l64-native -p l64-projection --all-targets -- -D warnings
- name: Lint native symbolic spine
run: cargo clippy -p l64-symbolic -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-symbolic",
"l64-projection",
"l64-core",
"l64-locus",
Expand Down
5 changes: 4 additions & 1 deletion LOCUS64_EXECUTION_COHERENCE_RAIL.athens
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,11 @@ ATHENS_DEVELOPMENT_RAIL v1
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=5
field=key=rail_version;value=6
field=key=schema_version;value=1
field=key=native_identity;value=exact_symbolic
field=key=native_compact_seal;value=non_authoritative
field=key=legacy_digest_boundary;value=blake3_l64_core_only
gate=id=incremental-closure-green
gate=id=legacy-authority-quarantine-green
gate=id=native-constraint-core-green
Expand Down
62 changes: 62 additions & 0 deletions LOCUS64_SYMBOLIC_COMMITMENT_CHANGE_CHAIN.athens
Original file line number Diff line number Diff line change
@@ -0,0 +1,62 @@
ATHENS_DEVELOPMENT_RAIL v1
field=key=compact_seal_authority;value=non_authoritative
field=key=exact_identity_authority;value=domain_plus_canonical_bytes
field=key=legacy_blake3_boundary;value=l64-core-only
field=key=rail_version;value=2
field=key=schema_version;value=1
gate=id=exact-identity-envelope-green
gate=id=seal-coordinate-algebra-green
gate=id=composition-grammar-green
gate=id=native-section-symbol-green
gate=id=dna-v2-symbolic-frame-green
gate=id=projection-symbol-binding-green
gate=id=developer-surface-green
gate=id=symbolic-commitment-green
stage=id=exact-identity-envelope
stage_field=stage=exact-identity-envelope;key=required_gates;value=exact-identity-envelope-green
stage_field=stage=exact-identity-envelope;key=status;value=complete
stage=id=seal-coordinate-algebra
stage_field=stage=seal-coordinate-algebra;key=depends_on;value=exact-identity-envelope
stage_field=stage=seal-coordinate-algebra;key=required_gates;value=seal-coordinate-algebra-green
stage_field=stage=seal-coordinate-algebra;key=status;value=complete
stage=id=composition-grammar
stage_field=stage=composition-grammar;key=depends_on;value=seal-coordinate-algebra
stage_field=stage=composition-grammar;key=required_gates;value=composition-grammar-green
stage_field=stage=composition-grammar;key=status;value=complete
stage=id=native-section-symbol
stage_field=stage=native-section-symbol;key=depends_on;value=composition-grammar
stage_field=stage=native-section-symbol;key=required_gates;value=native-section-symbol-green
stage_field=stage=native-section-symbol;key=status;value=complete
stage=id=dna-v2-symbolic-frame
stage_field=stage=dna-v2-symbolic-frame;key=depends_on;value=native-section-symbol
stage_field=stage=dna-v2-symbolic-frame;key=required_gates;value=dna-v2-symbolic-frame-green
stage_field=stage=dna-v2-symbolic-frame;key=status;value=complete
stage=id=projection-symbol-binding
stage_field=stage=projection-symbol-binding;key=depends_on;value=dna-v2-symbolic-frame
stage_field=stage=projection-symbol-binding;key=required_gates;value=projection-symbol-binding-green
stage_field=stage=projection-symbol-binding;key=status;value=complete
stage=id=developer-surface
stage_field=stage=developer-surface;key=depends_on;value=projection-symbol-binding
stage_field=stage=developer-surface;key=required_gates;value=developer-surface-green
stage_field=stage=developer-surface;key=status;value=complete
stage=id=symbolic-commitment-closure
stage_field=stage=symbolic-commitment-closure;key=depends_on;value=developer-surface
stage_field=stage=symbolic-commitment-closure;key=required_gates;value=symbolic-commitment-green
stage_field=stage=symbolic-commitment-closure;key=status;value=complete
history=from_status=current;gates=exact-identity-envelope-green;mode=linear_advance;stage_id=exact-identity-envelope;to_status=complete
history=evidence=local%3Al64s1-self-delimiting-domain-plus-canonical-bytes%2Bexact-roundtrip;kind=dogfood_promotion_receipt;stage_id=exact-identity-envelope
history=from_status=current;gates=seal-coordinate-algebra-green;mode=linear_advance;stage_id=seal-coordinate-algebra;to_status=complete
history=evidence=local%3Asigma-pi-delta-omega%2Bprime-field%2Btyped-axis-law%2Bmillion-sample-audit;kind=dogfood_promotion_receipt;stage_id=seal-coordinate-algebra
history=from_status=current;gates=composition-grammar-green;mode=linear_advance;stage_id=composition-grammar;to_status=complete
history=evidence=local%3Adomain-qualification%2Bordered%2Bcommutative%2Bderivation-composition;kind=dogfood_promotion_receipt;stage_id=composition-grammar
history=from_status=current;gates=native-section-symbol-green;mode=linear_advance;stage_id=native-section-symbol;to_status=complete
history=evidence=local%3Anodes-ports-contexts-routes-localization%2Bexact-state-identity;kind=dogfood_promotion_receipt;stage_id=native-section-symbol
history=from_status=current;gates=dna-v2-symbolic-frame-green;mode=linear_advance;stage_id=dna-v2-symbolic-frame;to_status=complete
history=evidence=local%3A44-byte-frame%2Bv1-explicit-rejection%2Bstale-seal-rejection%2Bexact-fixed-point;kind=dogfood_promotion_receipt;stage_id=dna-v2-symbolic-frame
history=from_status=current;gates=projection-symbol-binding-green;mode=linear_advance;stage_id=projection-symbol-binding;to_status=complete
history=evidence=local%3Aprojection-source-and-replay-bind-native-state-symbol%2Bstale-rejection;kind=dogfood_promotion_receipt;stage_id=projection-symbol-binding
history=from_status=current;gates=developer-surface-green;mode=linear_advance;stage_id=developer-surface;to_status=complete
history=evidence=local%3Aone-line-helpers%2Bparser-safe-ascii%2Breadable-unicode%2Baxis-change-explanations;kind=dogfood_promotion_receipt;stage_id=developer-surface
history=from_status=current;gates=symbolic-commitment-green;mode=linear_advance;stage_id=symbolic-commitment-closure;to_status=complete
history=evidence=github-66e09837ff96e2d10bee30232346e57f9bf7cec9-run-30146463330;kind=dogfood_promotion_receipt;stage_id=symbolic-commitment-closure
END
2 changes: 1 addition & 1 deletion l64-native/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -5,4 +5,4 @@ version.workspace = true
license.workspace = true

[dependencies]
blake3.workspace = true
l64-symbolic = { path = "../l64-symbolic" }
26 changes: 19 additions & 7 deletions l64-native/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ The second boundary adds a bounded native decoder. Canonical bytes must decode,

The third boundary makes primitive execution proof-carrying without adding a receipt schema. Every admitted operation receives a judgment type and kernel witness at routes deterministically composed from the operation route. Generic value insertion cannot construct a witness for a kernel-only judgment.

The fourth boundary adds a native DNA frame with a fixed 44-byte binary header, bounded canonical payload, embedded domain-separated BLAKE3 commitment, and exact DNA decode/re-encode fixed point. The frame contains no string metadata or legacy record payload.
The fourth boundary adds a native DNA frame with a fixed 44-byte binary header, bounded canonical payload, compact state field, and exact DNA decode/re-encode fixed point. The original frame used BLAKE3; the tenth boundary replaces that field with a composed symbolic seal while preserving the header width. The frame contains no string metadata or legacy record payload.

The fifth boundary adds a compact authored RNA ingress. `L64R1` uses one declared domain and strictly increasing numeric local slots; routes are composed as `(domain, slot)`. Its byte-oriented instructions lower directly through the existing graph and transaction APIs. Sequencing omits intrinsic evidence nodes because their routes and structure are deterministically derived.

Expand All @@ -37,8 +37,6 @@ 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;
Expand All @@ -53,7 +51,7 @@ The seventh boundary adds proof-producing congruence without promoting a union-f

`LOCUS64_PROOF_CONGRUENCE_CHANGE_CHAIN.athens` is complete on repository evidence. The parent execution rail has advanced to incremental dependency closure.

State identity is the domain-separated BLAKE3 commitment of canonical native bytes. No native name, claim identifier, theorem identifier, campaign identifier, JSON field name, or generic serialization schema participates.
Native authority identity is exact: the domain-qualified canonical byte sequence itself. A composed symbolic seal provides a fixed-width state reference and fast inequality check, but seal equality never substitutes for exact canonical comparison. No native name, claim identifier, theorem identifier, campaign identifier, JSON field name, or generic serialization schema participates.

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.

Expand All @@ -67,9 +65,9 @@ The eighth boundary adds incremental closure without turning invalidation into a
- 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.
- closure queries do not alter canonical bytes, state symbols, 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 derived reverse index is an in-memory accelerator only. It is excluded from RNA, DNA, state symbols, and authority identity.

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

Expand All @@ -79,8 +77,22 @@ The ninth boundary derives the first native upper views without turning any view
- 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;
- every view binds to the native state symbol, 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.

The tenth boundary removes BLAKE3 from the native execution and projection spine through a purpose-built symbolic identity system:

- `l64-symbolic` separates exact identity from compact sealing;
- exact identity is a self-delimiting `L64S1` envelope containing domain and canonical bytes, so authoritative equality is collision-free by representation;
- compact `SymbolicSeal` values expose `Σ`, `Π`, `Δ`, and `Ω` coordinates for aggregate content, ordered composition, adjacent transitions, and nonlinear boundary closure;
- ordered (`⊗`), commutative (`⊕`), derivational (`↦`), and domain-qualified (`∷`) composition are explicit operations rather than hidden byte concatenation;
- `StateSymbol` independently composes nodes, ports, contexts, and routes, allowing a changed state to identify the structural section that moved;
- journal events and projections carry symbolic seals, while `Graph::exact_state_identity()` remains the positive equality boundary;
- DNA v2 retains the 44-byte frame but stores the symbolic state seal; v1 is rejected instead of ambiguously reinterpreted;
- seal equality is only a fast-match signal. Canonical decoding, validation, and exact re-encoding remain mandatory before authority is accepted;
- the native and projection crates contain no BLAKE3 dependency.

Legacy `l64-core` still uses BLAKE3-backed string digests across its pre-native record, cache, receipt, and packet surfaces. That dependency is now confined to the legacy-authority-quarantine boundary; removing it requires retiring or exactly translating those roles, not substituting another opaque digest.
3 changes: 1 addition & 2 deletions l64-native/src/codec.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,7 @@ use std::collections::BTreeMap;
use crate::kernel::{EVIDENCE_LOCUS, EqualityRule, JUDGMENT_LOCUS};
use crate::{ContextDelta, Graph, LocusWord, Node, NodeId, OpCode, Port, PortRole, Route};

const CODEC_VERSION: u16 = 4;
const COMMITMENT_DOMAIN: &[u8] = b"l64-native-state-v4\0";
pub(crate) const CODEC_VERSION: u16 = 4;
const MAX_NODES: usize = 1 << 20;
const MAX_PORTS: usize = 1 << 22;
const MAX_CONTEXTS: usize = 1 << 20;
Expand Down
14 changes: 1 addition & 13 deletions l64-native/src/codec/io.rs
Original file line number Diff line number Diff line change
Expand Up @@ -119,8 +119,7 @@ pub fn decode_canonical(bytes: &[u8]) -> Result<Graph, DecodeError> {
}

validate_structure(&nodes, &ports, &contexts, &routes)?;
let commitment = commitment_bytes(bytes);
let graph = Graph::from_decoded_parts(nodes, ports, contexts, routes, commitment);
let graph = Graph::from_decoded_parts(nodes, ports, contexts, routes);
graph
.validate_decoded_authority()
.map_err(|_| DecodeError::InvalidAuthority)?;
Expand All @@ -129,14 +128,3 @@ pub fn decode_canonical(bytes: &[u8]) -> Result<Graph, DecodeError> {
}
Ok(graph)
}

pub(crate) fn state_commitment(graph: &Graph) -> [u8; 32] {
commitment_bytes(&canonical_bytes(graph))
}

fn commitment_bytes(bytes: &[u8]) -> [u8; 32] {
let mut hasher = blake3::Hasher::new();
hasher.update(COMMITMENT_DOMAIN);
hasher.update(bytes);
*hasher.finalize().as_bytes()
}
40 changes: 22 additions & 18 deletions l64-native/src/dna.rs
Original file line number Diff line number Diff line change
@@ -1,9 +1,10 @@
use crate::{DecodeError, Graph, canonical_bytes, decode_canonical};
use crate::{DecodeError, Graph, SymbolicSeal, canonical_bytes, decode_canonical};
use l64_symbolic::Composer;

const DNA_MAGIC: &[u8; 4] = b"L64D";
const DNA_VERSION: u16 = 1;
const DNA_VERSION: u16 = 2;
const DNA_FLAGS: u16 = 0;
const DNA_COMMITMENT_DOMAIN: &[u8] = b"l64-native-dna-v1\0";
const DNA_SYMBOL_DOMAIN: &str = "l64.native.dna.v2";
const DNA_HEADER_BYTES: usize = 44;
pub const MAX_NATIVE_DNA_PAYLOAD_BYTES: usize = 1 << 28;

Expand All @@ -15,7 +16,7 @@ pub enum DnaError {
UnsupportedVersion { version: u16 },
UnsupportedFlags { flags: u16 },
TrailingBytes,
CommitmentMismatch,
SealMismatch,
Canonical(DecodeError),
}

Expand All @@ -36,7 +37,7 @@ pub fn dna_bytes(graph: &Graph) -> Result<Vec<u8>, DnaError> {
out.extend_from_slice(&DNA_VERSION.to_le_bytes());
out.extend_from_slice(&DNA_FLAGS.to_le_bytes());
out.extend_from_slice(&(payload.len() as u32).to_le_bytes());
out.extend_from_slice(&dna_commitment(&payload));
out.extend_from_slice(&dna_seal(graph, payload.len()).to_bytes());
out.extend_from_slice(&payload);
Ok(out)
}
Expand Down Expand Up @@ -73,21 +74,24 @@ pub fn decode_dna(bytes: &[u8]) -> Result<Graph, DnaError> {
return Err(DnaError::TrailingBytes);
}

let stored_commitment: [u8; 32] = bytes[12..44]
.try_into()
.expect("fixed DNA commitment field");
let stored_seal = SymbolicSeal::from_bytes(
bytes[12..44]
.try_into()
.expect("fixed DNA symbolic seal field"),
);
let payload = &bytes[DNA_HEADER_BYTES..];
let computed_commitment = dna_commitment(payload);
if stored_commitment != computed_commitment {
return Err(DnaError::CommitmentMismatch);
let graph = decode_canonical(payload)?;
if stored_seal != dna_seal(&graph, payload.len()) {
return Err(DnaError::SealMismatch);
}

Ok(decode_canonical(payload)?)
Ok(graph)
}

fn dna_commitment(payload: &[u8]) -> [u8; 32] {
let mut hasher = blake3::Hasher::new();
hasher.update(DNA_COMMITMENT_DOMAIN);
hasher.update(payload);
*hasher.finalize().as_bytes()
fn dna_seal(graph: &Graph, payload_len: usize) -> SymbolicSeal {
let mut composer = Composer::new(DNA_SYMBOL_DOMAIN);
composer
.u16("version", DNA_VERSION)
.u64("payload-length", payload_len as u64)
.ordered("state", &[graph.state_symbol().root]);
composer.finish()
}
4 changes: 2 additions & 2 deletions l64-native/src/graph.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ use std::collections::BTreeMap;
use crate::kernel::{ConstraintState, EqualityRule, EvidencePlan};
use crate::{
ClosureState, ClosureTransition, ConstraintKind, ContextDelta, Dimension, JournalEvent,
LocusWord, Obstruction, OpCode, Port, PortRole, Route,
LocusWord, Obstruction, OpCode, Port, PortRole, Route, StateSymbol, SymbolicSeal,
};

pub type NodeId = u32;
Expand Down Expand Up @@ -80,7 +80,7 @@ pub struct Graph {
contexts: Vec<ContextDelta>,
routes: BTreeMap<Route, NodeId>,
journal: Vec<JournalEvent>,
commitment: [u8; 32],
symbol: StateSymbol,
derived: DerivedIndex,
}

Expand Down
Loading
Loading