diff --git a/.github/workflows/native-core.yml b/.github/workflows/native-core.yml index aa0c6cc..cf66d52 100644 --- a/.github/workflows/native-core.yml +++ b/.github/workflows/native-core.yml @@ -1,23 +1,15 @@ name: Native core gate on: - push: - branches: - - 'chatgpt/**' - paths: - - Cargo.toml - - Cargo.lock - - l64-native/** - - LOCUS64_*_RAIL.athens - - LOCUS64_*_CHANGE_CHAIN.athens - - .github/workflows/native-core.yml pull_request: branches: - main + - 'chatgpt/**' paths: - Cargo.toml - Cargo.lock - l64-native/** + - l64-cli/** - LOCUS64_*_RAIL.athens - LOCUS64_*_CHANGE_CHAIN.athens - .github/workflows/native-core.yml @@ -28,7 +20,6 @@ permissions: jobs: verify: - if: github.event_name == 'push' || github.event.pull_request.head.repo.full_name != github.repository runs-on: ubuntu-latest steps: - name: Checkout diff --git a/LOCUS64_EXECUTION_COHERENCE_RAIL.athens b/LOCUS64_EXECUTION_COHERENCE_RAIL.athens index 95053a1..7f1b3ed 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=proof-producing-congruence -field=key=next_stage;value=incremental-closure +field=key=current_stage;value=incremental-closure +field=key=next_stage;value=native-upper-projection field=key=projection_authority;value=non_authoritative -field=key=rail_version;value=2 +field=key=rail_version;value=3 field=key=schema_version;value=1 gate=id=incremental-closure-green gate=id=legacy-authority-quarantine-green @@ -15,19 +15,21 @@ stage_field=stage=native-constraint-core;key=status;value=complete stage=id=proof-producing-congruence stage_field=stage=proof-producing-congruence;key=depends_on;value=native-constraint-core stage_field=stage=proof-producing-congruence;key=required_gates;value=proof-producing-congruence-green -stage_field=stage=proof-producing-congruence;key=status;value=current +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=next +stage_field=stage=incremental-closure;key=status;value=current 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=planned +stage_field=stage=native-upper-projection;key=status;value=next 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 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 END diff --git a/LOCUS64_PROOF_CONGRUENCE_CHANGE_CHAIN.athens b/LOCUS64_PROOF_CONGRUENCE_CHANGE_CHAIN.athens new file mode 100644 index 0000000..5447b02 --- /dev/null +++ b/LOCUS64_PROOF_CONGRUENCE_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=canonical-representative-green +gate=id=congruence-lifting-green +gate=id=equality-judgment-green +gate=id=evidence-path-validation-green +gate=id=forged-merge-closure-green +gate=id=primitive-equality-witness-green +stage=id=equality-judgment +stage_field=stage=equality-judgment;key=required_gates;value=equality-judgment-green +stage_field=stage=equality-judgment;key=status;value=complete +stage=id=primitive-equality-witness +stage_field=stage=primitive-equality-witness;key=depends_on;value=equality-judgment +stage_field=stage=primitive-equality-witness;key=required_gates;value=primitive-equality-witness-green +stage_field=stage=primitive-equality-witness;key=status;value=complete +stage=id=congruence-lifting +stage_field=stage=congruence-lifting;key=depends_on;value=primitive-equality-witness +stage_field=stage=congruence-lifting;key=required_gates;value=congruence-lifting-green +stage_field=stage=congruence-lifting;key=status;value=complete +stage=id=evidence-path-validation +stage_field=stage=evidence-path-validation;key=depends_on;value=congruence-lifting +stage_field=stage=evidence-path-validation;key=required_gates;value=evidence-path-validation-green +stage_field=stage=evidence-path-validation;key=status;value=complete +stage=id=canonical-representative +stage_field=stage=canonical-representative;key=depends_on;value=evidence-path-validation +stage_field=stage=canonical-representative;key=required_gates;value=canonical-representative-green +stage_field=stage=canonical-representative;key=status;value=complete +stage=id=forged-merge-closure +stage_field=stage=forged-merge-closure;key=depends_on;value=canonical-representative +stage_field=stage=forged-merge-closure;key=required_gates;value=forged-merge-closure-green +stage_field=stage=forged-merge-closure;key=status;value=complete +history=from_status=current;gates=equality-judgment-green;mode=linear_advance;stage_id=equality-judgment;to_status=complete +history=evidence=local%3A41-tests%3Btyped-equality-judgment%2Battached-witness;kind=dogfood_promotion_receipt;stage_id=equality-judgment +history=from_status=current;gates=primitive-equality-witness-green;mode=linear_advance;stage_id=primitive-equality-witness;to_status=complete +history=evidence=local%3A41-tests%3Breflexive%2Bstructural%2Bsymmetry%2Btransitivity;kind=dogfood_promotion_receipt;stage_id=primitive-equality-witness +history=from_status=current;gates=congruence-lifting-green;mode=linear_advance;stage_id=congruence-lifting;to_status=complete +history=evidence=local%3A41-tests%3Bconstructor%2Boperation-congruence;kind=dogfood_promotion_receipt;stage_id=congruence-lifting +history=from_status=current;gates=evidence-path-validation-green;mode=linear_advance;stage_id=evidence-path-validation;to_status=complete +history=evidence=local%3A41-tests%3Bdeterministic-path%2Bcontext-scope%2Bdecode-recheck;kind=dogfood_promotion_receipt;stage_id=evidence-path-validation +history=from_status=current;gates=canonical-representative-green;mode=linear_advance;stage_id=canonical-representative;to_status=complete +history=evidence=local%3A41-tests%3Broute-minimal-representative-no-persisted-index;kind=dogfood_promotion_receipt;stage_id=canonical-representative +history=from_status=current;gates=forged-merge-closure-green;mode=linear_advance;stage_id=forged-merge-closure;to_status=complete +history=evidence=github-0a84bdd3dc232a0db1b79009c3bf99cfd4fb40cd-run-29997066639;kind=dogfood_promotion_receipt;stage_id=forged-merge-closure +END diff --git a/l64-cli/tests/native_cli.rs b/l64-cli/tests/native_cli.rs index c4d6866..cc5af92 100644 --- a/l64-cli/tests/native_cli.rs +++ b/l64-cli/tests/native_cli.rs @@ -6,6 +6,8 @@ use std::{ }; const SOURCE: &[u8] = b"L64R1 0x4c36344e41544956\na 1 0x41\na 2 0x42\na 3 0x43\nf 4 1 2\nf 5 2 3\nf 6 1 3\nv 7 4\nv 8 5\nc 9 7 8 6\n"; +const EQUALITY_SOURCE: &[u8] = + b"L64R1 0x4551\na 1 0x41\na 2 0x41\ne 3 2 1 2 0\ne 4 3 2 1 0 3\ne 5 4 1 1 0 3 4\n"; fn fixture(name: &str, bytes: &[u8]) -> PathBuf { let dir = std::env::temp_dir().join(format!( @@ -47,6 +49,31 @@ fn native_compile_and_sequence_use_existing_commands() { assert_eq!(output.stdout, SOURCE); } +#[test] +fn native_cli_preserves_equality_proof_fixed_point() { + let rna = fixture("equality.rna", EQUALITY_SOURCE); + let dna = rna.with_extension("dna"); + + Command::cargo_bin("l64-cli") + .unwrap() + .args([ + "compile-rna", + rna.to_str().unwrap(), + "--out", + dna.to_str().unwrap(), + ]) + .assert() + .success(); + + let output = Command::cargo_bin("l64-cli") + .unwrap() + .args(["sequence-dna", dna.to_str().unwrap()]) + .output() + .unwrap(); + assert!(output.status.success()); + assert_eq!(output.stdout, EQUALITY_SOURCE); +} + #[test] fn invalid_native_operation_cannot_create_dna() { let source = b"L64R1 0x1\na 1 0x52\nm 2 1 2 3\nm 3 1 4 2\nm 4 1 2 2\nv 5 2\nv 6 3\nx 7 5 6 4\n"; diff --git a/l64-native/README.md b/l64-native/README.md index cdbf54b..8fbcb47 100644 --- a/l64-native/README.md +++ b/l64-native/README.md @@ -37,8 +37,22 @@ 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; +- primitive rules cover reflexivity, exact structural identity, symmetry, and transitivity; +- congruence lifts checked equalities through type constructors and executable operations; +- every premise points to an earlier equality judgment with its own checked witness; +- proof paths are returned deterministically and remain context-scoped; +- canonical representatives are selected by minimum composed route over the validated equality component; +- no equivalence class, representative cache, or merge table is persisted; +- decoder-side rule re-execution rejects forged rules, missing provenance, scope escape, and mismatched congruence premises; +- equality-bearing `L64R1` reaches the exact `L64D → L64R1 → L64D` fixed point. + +`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. 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 proof-producing congruence, 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 incremental dependency closure, native upper-stack projections, or replacement of the legacy runtime, registry, certification, and old packet implementation internally. diff --git a/l64-native/src/codec.rs b/l64-native/src/codec.rs index 8b3b6cf..49418bf 100644 --- a/l64-native/src/codec.rs +++ b/l64-native/src/codec.rs @@ -1,10 +1,10 @@ use std::collections::BTreeMap; -use crate::kernel::{EVIDENCE_LOCUS, JUDGMENT_LOCUS}; +use crate::kernel::{EVIDENCE_LOCUS, EqualityRule, JUDGMENT_LOCUS}; use crate::{ContextDelta, Graph, LocusWord, Node, NodeId, OpCode, Port, PortRole, Route}; -const CODEC_VERSION: u16 = 3; -const COMMITMENT_DOMAIN: &[u8] = b"l64-native-state-v3\0"; +const CODEC_VERSION: u16 = 4; +const COMMITMENT_DOMAIN: &[u8] = b"l64-native-state-v4\0"; const MAX_NODES: usize = 1 << 20; const MAX_PORTS: usize = 1 << 22; const MAX_CONTEXTS: usize = 1 << 20; diff --git a/l64-native/src/codec/validation.rs b/l64-native/src/codec/validation.rs index 1ae5755..7cfebe9 100644 --- a/l64-native/src/codec/validation.rs +++ b/l64-native/src/codec/validation.rs @@ -79,7 +79,10 @@ fn validate_node_semantics( match node.opcode() { OpCode::Value => { let ty = node.ty().ok_or(DecodeError::InvalidNode)?; - if nodes[ty as usize].opcode() == OpCode::TypeJudgment { + if matches!( + nodes[ty as usize].opcode(), + OpCode::TypeJudgment | OpCode::TypeEquality + ) { return Err(DecodeError::InvalidNode); } } @@ -94,6 +97,20 @@ fn validate_node_semantics( return Err(DecodeError::InvalidNode); } } + OpCode::TypeEquality => { + if node.payload() != 0 { + return Err(DecodeError::InvalidNode); + } + } + OpCode::EqualityWitness => { + let ty = node.ty().ok_or(DecodeError::InvalidNode)?; + if nodes[ty as usize].opcode() != OpCode::TypeEquality + || node.payload() > u8::MAX as u64 + || EqualityRule::from_raw(node.payload() as u8).is_none() + { + return Err(DecodeError::InvalidNode); + } + } OpCode::TypeQuantity => { if crate::Dimension::from_bits(node.payload()).is_none() { return Err(DecodeError::InvalidNode); @@ -165,10 +182,29 @@ fn validate_evidence_routes( attached[judgment as usize] = true; attached[witness as usize] = true; } + for (route, judgment) in routes { + if nodes[*judgment as usize].opcode() != OpCode::TypeEquality { + continue; + } + let witness = *routes + .get(&route.composed(EVIDENCE_LOCUS)) + .ok_or(DecodeError::InvalidRoute)?; + if nodes[witness as usize].opcode() != OpCode::EqualityWitness + || nodes[witness as usize].ty() != Some(*judgment) + { + return Err(DecodeError::InvalidRoute); + } + attached[*judgment as usize] = true; + attached[witness as usize] = true; + } for (index, node) in nodes.iter().enumerate() { if matches!( node.opcode(), - OpCode::TypeJudgment | OpCode::KernelWitness | OpCode::Obligation + OpCode::TypeJudgment + | OpCode::KernelWitness + | OpCode::Obligation + | OpCode::TypeEquality + | OpCode::EqualityWitness ) && !attached[index] { return Err(DecodeError::InvalidRoute); @@ -213,6 +249,15 @@ fn validate_port_law(opcode: OpCode, ports: &[Port], has_type: bool) -> Result<( } OpCode::KernelWitness => ports.is_empty() && has_type, OpCode::Obligation => ports.len() == 1 && ports[0].role() == PortRole::Premise && has_type, + OpCode::TypeEquality => { + ports.len() == 2 + && ports[0].role() == PortRole::Left + && ports[1].role() == PortRole::Right + && !has_type + } + OpCode::EqualityWitness => { + ports.iter().all(|port| port.role() == PortRole::Premise) && has_type + } OpCode::ExtendContext => false, }; valid.then_some(()).ok_or(DecodeError::InvalidPortLaw) diff --git a/l64-native/src/graph.rs b/l64-native/src/graph.rs index 7ca66d3..2ff6af9 100644 --- a/l64-native/src/graph.rs +++ b/l64-native/src/graph.rs @@ -1,6 +1,6 @@ use std::collections::BTreeMap; -use crate::kernel::{ConstraintState, EvidencePlan}; +use crate::kernel::{ConstraintState, EqualityRule, EvidencePlan}; use crate::{ ConstraintKind, ContextDelta, Dimension, JournalEvent, LocusWord, Obstruction, OpCode, Port, PortRole, Route, diff --git a/l64-native/src/graph/construction.rs b/l64-native/src/graph/construction.rs index 1a99d5c..9b8f7e8 100644 --- a/l64-native/src/graph/construction.rs +++ b/l64-native/src/graph/construction.rs @@ -187,7 +187,7 @@ impl Graph { ) -> Result { self.ensure_context(context)?; let type_node = self.ensure_type(ty)?; - if type_node.opcode() == OpCode::TypeJudgment { + if matches!(type_node.opcode(), OpCode::TypeJudgment | OpCode::TypeEquality) { return Err(Obstruction::EvidenceOnlyType { node: ty }); } self.insert_committed_node(route, context, ty, OpCode::Value, 0, &[]) @@ -274,4 +274,59 @@ impl Graph { commitment: after, } } + + pub(crate) fn insert_admitted_equality( + &mut self, + routes: [Route; 2], + context: ContextId, + left: NodeId, + right: NodeId, + rule: EqualityRule, + premises: &[NodeId], + ) -> crate::CommitResult { + let [route, evidence_route] = routes; + let before = self.commitment; + + let judgment = self.nodes.len() as NodeId; + let judgment_first_port = self.ports.len() as u32; + self.ports.push(Port::new(left, PortRole::Left, 0)); + self.ports.push(Port::new(right, PortRole::Right, 1)); + self.nodes.push(Node { + payload: 0, + context, + ty: META_TYPE, + first_port: judgment_first_port, + opcode: OpCode::TypeEquality as u16, + port_count: 2, + }); + + let evidence = self.nodes.len() as NodeId; + let evidence_first_port = self.ports.len() as u32; + self.ports.extend( + premises + .iter() + .enumerate() + .map(|(ordinal, target)| Port::new(*target, PortRole::Premise, ordinal as u16)), + ); + self.nodes.push(Node { + payload: rule as u64, + context, + ty: judgment, + first_port: evidence_first_port, + opcode: OpCode::EqualityWitness as u16, + port_count: premises.len() as u16, + }); + + self.routes.insert(route, judgment); + self.routes.insert(evidence_route, evidence); + let after = crate::codec::state_commitment(self); + self.push_event(OpCode::EqualityWitness, judgment, before, after); + self.commitment = after; + crate::CommitResult { + node: judgment, + evidence, + event: self.journal.len().saturating_sub(1) as EventId, + commitment: after, + } + } } diff --git a/l64-native/src/kernel.rs b/l64-native/src/kernel.rs index 1d7d8b9..38d59e2 100644 --- a/l64-native/src/kernel.rs +++ b/l64-native/src/kernel.rs @@ -1,6 +1,7 @@ -use crate::{ContextId, Dimension, Graph, LocusWord, NodeId, Route}; +use crate::{ContextId, Dimension, Graph, LocusWord, NodeId, ROOT_CONTEXT, Route}; include!("kernel/types.rs"); include!("kernel/proposal.rs"); include!("kernel/transaction.rs"); include!("kernel/validation.rs"); +include!("kernel/equality.rs"); diff --git a/l64-native/src/kernel/equality.rs b/l64-native/src/kernel/equality.rs new file mode 100644 index 0000000..efadfc4 --- /dev/null +++ b/l64-native/src/kernel/equality.rs @@ -0,0 +1,3 @@ +include!("equality/proof.rs"); +include!("equality/validation.rs"); +include!("equality/canonical.rs"); diff --git a/l64-native/src/kernel/equality/canonical.rs b/l64-native/src/kernel/equality/canonical.rs new file mode 100644 index 0000000..a4a0bb4 --- /dev/null +++ b/l64-native/src/kernel/equality/canonical.rs @@ -0,0 +1,120 @@ +impl Graph { + pub fn equality_path( + &self, + context: ContextId, + left: NodeId, + right: NodeId, + ) -> Result, Obstruction> { + self.ensure_context(context)?; + let left_node = self.ensure_node(left)?; + let right_node = self.ensure_node(right)?; + if !self.equality_endpoint_allowed(left_node) + || !self.equality_endpoint_allowed(right_node) + || !self.context_visible(left_node.context(), context) + || !self.context_visible(right_node.context(), context) + { + return Err(Obstruction::NoEqualityPath { left, right }); + } + self.validate_equality_authority()?; + if left == right { + return Ok(Vec::new()); + } + + let mut queue = std::collections::VecDeque::from([left]); + let mut parent = std::collections::BTreeMap::::new(); + parent.insert(left, (left, u32::MAX)); + while let Some(current) = queue.pop_front() { + for judgment in self.routes_raw().values() { + let equality = self + .node(*judgment) + .ok_or(Obstruction::UnknownNode { node: *judgment })?; + if equality.opcode() != OpCode::TypeEquality + || !self.context_visible(equality.context(), context) + { + continue; + } + let (edge_left, edge_right) = self.equality_parts(*judgment)?; + let next = if edge_left == current { + Some(edge_right) + } else if edge_right == current { + Some(edge_left) + } else { + None + }; + let Some(next) = next else { continue }; + if parent.contains_key(&next) { + continue; + } + parent.insert(next, (current, *judgment)); + if next == right { + let mut path = Vec::new(); + let mut cursor = right; + while cursor != left { + let (previous, proof) = parent[&cursor]; + path.push(proof); + cursor = previous; + } + path.reverse(); + return Ok(path); + } + queue.push_back(next); + } + } + Err(Obstruction::NoEqualityPath { left, right }) + } + + pub fn canonical_representative( + &self, + context: ContextId, + node: NodeId, + ) -> Result { + self.ensure_context(context)?; + let subject = self.ensure_node(node)?; + if !self.equality_endpoint_allowed(subject) || !self.context_visible(subject.context(), context) + { + return Err(Obstruction::UncanonicalizableNode { node }); + } + self.validate_equality_authority()?; + + let mut members = std::collections::BTreeSet::from([node]); + loop { + let before = members.len(); + for candidate in 0..self.node_count() as NodeId { + let equality = self + .node(candidate) + .ok_or(Obstruction::UnknownNode { node: candidate })?; + if equality.opcode() != OpCode::TypeEquality + || !self.context_visible(equality.context(), context) + { + continue; + } + let (left, right) = self.equality_parts(candidate)?; + if members.contains(&left) || members.contains(&right) { + members.insert(left); + members.insert(right); + } + } + if members.len() == before { + break; + } + } + + self.routes_raw() + .iter() + .find_map(|(_, candidate)| members.contains(candidate).then_some(*candidate)) + .ok_or(Obstruction::UncanonicalizableNode { node }) + } + + pub fn canonical_representative_route( + &self, + context: ContextId, + node: NodeId, + ) -> Result { + let representative = self.canonical_representative(context, node)?; + self.route_for_node(representative) + .cloned() + .ok_or(Obstruction::UncanonicalizableNode { + node: representative, + }) + } +} diff --git a/l64-native/src/kernel/equality/proof.rs b/l64-native/src/kernel/equality/proof.rs new file mode 100644 index 0000000..f3ceaf1 --- /dev/null +++ b/l64-native/src/kernel/equality/proof.rs @@ -0,0 +1,158 @@ +impl Graph { + pub fn prove_reflexive_equality( + &mut self, + route: Route, + context: ContextId, + subject: NodeId, + ) -> Result { + self.prove_equality( + route, + context, + subject, + subject, + EqualityRule::Reflexive, + &[], + ) + } + + pub fn prove_structural_equality( + &mut self, + route: Route, + context: ContextId, + left: NodeId, + right: NodeId, + ) -> Result { + self.prove_equality( + route, + context, + left, + right, + EqualityRule::Structural, + &[], + ) + } + + pub fn prove_symmetric_equality( + &mut self, + route: Route, + context: ContextId, + premise: NodeId, + ) -> Result { + let (left, right) = self.equality_parts(premise)?; + self.prove_equality( + route, + context, + right, + left, + EqualityRule::Symmetry, + &[premise], + ) + } + + pub fn prove_transitive_equality( + &mut self, + route: Route, + context: ContextId, + first: NodeId, + second: NodeId, + ) -> Result { + let (left, middle) = self.equality_parts(first)?; + let (second_middle, right) = self.equality_parts(second)?; + if middle != second_middle { + return Err(Obstruction::EqualityPremiseMismatch { premise: second }); + } + self.prove_equality( + route, + context, + left, + right, + EqualityRule::Transitive, + &[first, second], + ) + } + + pub fn prove_congruent_equality( + &mut self, + route: Route, + context: ContextId, + left: NodeId, + right: NodeId, + premises: &[NodeId], + ) -> Result { + self.prove_equality( + route, + context, + left, + right, + EqualityRule::Congruence, + premises, + ) + } + + pub(crate) fn prove_equality( + &mut self, + route: Route, + context: ContextId, + left: NodeId, + right: NodeId, + rule: EqualityRule, + premises: &[NodeId], + ) -> Result { + let evidence_route = route.composed(EVIDENCE_LOCUS); + if self.resolve(&route).is_some() || self.resolve(&evidence_route).is_some() { + return Err(Obstruction::RouteOccupied); + } + self.validate_equality_rule(context, left, right, rule, premises)?; + Ok(self.insert_admitted_equality( + [route, evidence_route], + context, + left, + right, + rule, + premises, + )) + } + + pub(crate) fn equality_parts( + &self, + judgment: NodeId, + ) -> Result<(NodeId, NodeId), Obstruction> { + let node = self.ensure_node(judgment)?; + let ports = self + .ports(judgment) + .ok_or(Obstruction::MalformedEquality { node: judgment })?; + if node.opcode() != OpCode::TypeEquality + || ports.len() != 2 + || ports[0].role() != PortRole::Left + || ports[1].role() != PortRole::Right + { + return Err(Obstruction::MalformedEquality { node: judgment }); + } + Ok((ports[0].target(), ports[1].target())) + } + + pub(crate) fn equality_evidence_parts( + &self, + judgment: NodeId, + ) -> Result<(EqualityRule, Vec), Obstruction> { + let evidence = self + .equality_witness_for(judgment) + .ok_or(Obstruction::MalformedEquality { node: judgment })?; + let node = self + .node(evidence) + .ok_or(Obstruction::MalformedEquality { node: evidence })?; + let ports = self + .ports(evidence) + .ok_or(Obstruction::MalformedEquality { node: evidence })?; + let rule = EqualityRule::from_raw(node.payload() as u8) + .filter(|_| node.payload() <= u8::MAX as u64) + .ok_or(Obstruction::MalformedEquality { node: evidence })?; + if node.opcode() != OpCode::EqualityWitness + || node.ty() != Some(judgment) + || ports.iter().any(|port| port.role() != PortRole::Premise) + { + return Err(Obstruction::MalformedEquality { node: evidence }); + } + Ok((rule, ports.iter().map(Port::target).collect())) + } +} diff --git a/l64-native/src/kernel/equality/validation.rs b/l64-native/src/kernel/equality/validation.rs new file mode 100644 index 0000000..dbd8286 --- /dev/null +++ b/l64-native/src/kernel/equality/validation.rs @@ -0,0 +1,288 @@ +impl Graph { + pub(crate) fn validate_equality_authority(&self) -> Result<(), Obstruction> { + let mut attached = vec![false; self.node_count()]; + for (route, judgment) in self.routes_raw() { + let node = self + .node(*judgment) + .ok_or(Obstruction::UnknownNode { node: *judgment })?; + if node.opcode() != OpCode::TypeEquality { + continue; + } + let evidence = self + .resolve(&route.composed(EVIDENCE_LOCUS)) + .ok_or(Obstruction::MalformedEquality { node: *judgment })?; + let evidence_node = self + .node(evidence) + .ok_or(Obstruction::MalformedEquality { node: evidence })?; + let evidence_ports = self + .ports(evidence) + .ok_or(Obstruction::MalformedEquality { node: evidence })?; + let rule = EqualityRule::from_raw(evidence_node.payload() as u8) + .filter(|_| evidence_node.payload() <= u8::MAX as u64) + .ok_or(Obstruction::MalformedEquality { node: evidence })?; + if evidence_node.opcode() != OpCode::EqualityWitness + || evidence_node.ty() != Some(*judgment) + || evidence_node.context() != node.context() + || evidence_ports + .iter() + .any(|port| port.role() != PortRole::Premise) + { + return Err(Obstruction::MalformedEquality { node: evidence }); + } + let premises = evidence_ports.iter().map(Port::target).collect::>(); + let (left, right) = self.equality_parts(*judgment)?; + self.validate_equality_rule(node.context(), left, right, rule, &premises)?; + attached[*judgment as usize] = true; + attached[evidence as usize] = true; + } + for (index, node) in self.nodes_raw().iter().enumerate() { + if matches!(node.opcode(), OpCode::TypeEquality | OpCode::EqualityWitness) + && !attached[index] + { + return Err(Obstruction::MalformedEquality { + node: index as NodeId, + }); + } + } + Ok(()) + } + + fn validate_equality_rule( + &self, + context: ContextId, + left: NodeId, + right: NodeId, + rule: EqualityRule, + premises: &[NodeId], + ) -> Result<(), Obstruction> { + self.ensure_context(context)?; + let left_node = self.ensure_node(left)?; + let right_node = self.ensure_node(right)?; + if !self.context_visible(left_node.context(), context) + || !self.context_visible(right_node.context(), context) + { + return Err(Obstruction::EqualityContextEscape { + premise: if !self.context_visible(left_node.context(), context) { + left + } else { + right + }, + context, + }); + } + if !self.equality_endpoint_allowed(left_node) + || !self.equality_endpoint_allowed(right_node) + || !self.same_equality_sort(left_node, right_node) + { + return Err(Obstruction::EqualitySortMismatch { left, right }); + } + + let premise_pairs = premises + .iter() + .map(|premise| self.checked_premise(context, *premise)) + .collect::, _>>()?; + + match rule { + EqualityRule::Reflexive => { + if left != right || !premises.is_empty() { + return Err(Obstruction::InvalidEqualityRule); + } + } + EqualityRule::Structural => { + if !premises.is_empty() || !self.structurally_equal(left, right)? { + return Err(Obstruction::InvalidEqualityRule); + } + } + EqualityRule::Symmetry => { + if premise_pairs.as_slice() != [(right, left)] { + return Err(Obstruction::InvalidEqualityRule); + } + } + EqualityRule::Transitive => { + if premise_pairs.len() != 2 + || premise_pairs[0].0 != left + || premise_pairs[0].1 != premise_pairs[1].0 + || premise_pairs[1].1 != right + { + return Err(Obstruction::InvalidEqualityRule); + } + } + EqualityRule::Congruence => { + self.validate_congruence(left, right, &premise_pairs)?; + } + } + Ok(()) + } + + fn validate_congruence( + &self, + left: NodeId, + right: NodeId, + premise_pairs: &[(NodeId, NodeId)], + ) -> Result<(), Obstruction> { + let left_node = self.ensure_node(left)?; + let right_node = self.ensure_node(right)?; + if !self.congruence_subject_allowed(left_node.opcode()) + || left_node.opcode() != right_node.opcode() + || left_node.payload() != right_node.payload() + || left_node.context() != right_node.context() + || left_node.ty() != right_node.ty() + { + return Err(Obstruction::InvalidEqualityRule); + } + let left_ports = self + .ports(left) + .ok_or(Obstruction::MalformedEquality { node: left })?; + let right_ports = self + .ports(right) + .ok_or(Obstruction::MalformedEquality { node: right })?; + if left_ports.is_empty() + || left_ports.len() != right_ports.len() + || left_ports.len() != premise_pairs.len() + { + return Err(Obstruction::InvalidEqualityRule); + } + for ((left_port, right_port), pair) in left_ports + .iter() + .zip(right_ports) + .zip(premise_pairs) + { + if left_port.role() != right_port.role() + || left_port.flags() != right_port.flags() + || left_port.ordinal() != right_port.ordinal() + || *pair != (left_port.target(), right_port.target()) + { + return Err(Obstruction::InvalidEqualityRule); + } + } + Ok(()) + } + + fn checked_premise( + &self, + context: ContextId, + premise: NodeId, + ) -> Result<(NodeId, NodeId), Obstruction> { + let node = self.ensure_node(premise)?; + if node.opcode() != OpCode::TypeEquality { + return Err(Obstruction::EqualityPremiseMismatch { premise }); + } + if !self.context_visible(node.context(), context) { + return Err(Obstruction::EqualityContextEscape { premise, context }); + } + let witness = self + .equality_witness_for(premise) + .ok_or(Obstruction::EqualityPremiseMismatch { premise })?; + let witness_node = self.ensure_node(witness)?; + if witness_node.opcode() != OpCode::EqualityWitness + || witness_node.ty() != Some(premise) + || witness_node.context() != node.context() + { + return Err(Obstruction::EqualityPremiseMismatch { premise }); + } + self.equality_parts(premise) + } + + fn equality_witness_for(&self, judgment: NodeId) -> Option { + let route = self.route_for_node(judgment)?; + self.resolve(&route.composed(EVIDENCE_LOCUS)) + } + + fn route_for_node(&self, node: NodeId) -> Option<&Route> { + self.routes_raw() + .iter() + .find_map(|(route, candidate)| (*candidate == node).then_some(route)) + } + + fn context_visible(&self, ancestor: ContextId, mut context: ContextId) -> bool { + loop { + if ancestor == context { + return true; + } + if context == ROOT_CONTEXT { + return false; + } + let Some(delta) = self.contexts_raw().get(context as usize) else { + return false; + }; + context = delta.parent(); + } + } + + 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), + _ => false, + } + } + + fn equality_endpoint_allowed(&self, node: &crate::Node) -> bool { + matches!( + node.opcode(), + OpCode::TypeAtom + | OpCode::TypeMatrix + | OpCode::TypeFunction + | OpCode::TypeQuantity + | OpCode::Value + | OpCode::Compose + | OpCode::MatMul + | OpCode::Add + | OpCode::Multiply + | OpCode::Divide + | OpCode::Sqrt + ) + } + + fn congruence_subject_allowed(&self, opcode: OpCode) -> bool { + matches!( + opcode, + OpCode::TypeMatrix + | OpCode::TypeFunction + | OpCode::TypeQuantity + | OpCode::Compose + | OpCode::MatMul + | OpCode::Add + | OpCode::Multiply + | OpCode::Divide + | OpCode::Sqrt + ) + } + + fn structurally_equal(&self, left: NodeId, right: NodeId) -> Result { + let left_node = self.ensure_node(left)?; + let right_node = self.ensure_node(right)?; + if !matches!( + left_node.opcode(), + OpCode::TypeAtom + | OpCode::TypeMatrix + | OpCode::TypeFunction + | OpCode::TypeQuantity + | OpCode::Compose + | OpCode::MatMul + | OpCode::Add + | OpCode::Multiply + | OpCode::Divide + | OpCode::Sqrt + ) || left_node.opcode() != right_node.opcode() + || left_node.payload() != right_node.payload() + || left_node.context() != right_node.context() + || left_node.ty() != right_node.ty() + { + return Ok(false); + } + let left_ports = self + .ports(left) + .ok_or(Obstruction::MalformedEquality { node: left })?; + let right_ports = self + .ports(right) + .ok_or(Obstruction::MalformedEquality { node: right })?; + Ok(left_ports.len() == right_ports.len() + && left_ports.iter().zip(right_ports).all(|(left, right)| { + left.target() == right.target() + && left.role() == right.role() + && left.flags() == right.flags() + && left.ordinal() == right.ordinal() + })) + } +} diff --git a/l64-native/src/kernel/proposal.rs b/l64-native/src/kernel/proposal.rs index 63f820b..e0a0764 100644 --- a/l64-native/src/kernel/proposal.rs +++ b/l64-native/src/kernel/proposal.rs @@ -194,4 +194,26 @@ pub enum Obstruction { MalformedEvidence { node: NodeId, }, + EqualitySortMismatch { + left: NodeId, + right: NodeId, + }, + InvalidEqualityRule, + MalformedEquality { + node: NodeId, + }, + EqualityPremiseMismatch { + premise: NodeId, + }, + EqualityContextEscape { + premise: NodeId, + context: ContextId, + }, + UncanonicalizableNode { + node: NodeId, + }, + NoEqualityPath { + left: NodeId, + right: NodeId, + }, } diff --git a/l64-native/src/kernel/types.rs b/l64-native/src/kernel/types.rs index 28b8f4f..c26b2af 100644 --- a/l64-native/src/kernel/types.rs +++ b/l64-native/src/kernel/types.rs @@ -20,6 +20,8 @@ pub enum OpCode { Constraint = 14, Sqrt = 15, Obligation = 16, + TypeEquality = 17, + EqualityWitness = 18, } impl OpCode { @@ -41,6 +43,8 @@ impl OpCode { 14 => Some(Self::Constraint), 15 => Some(Self::Sqrt), 16 => Some(Self::Obligation), + 17 => Some(Self::TypeEquality), + 18 => Some(Self::EqualityWitness), _ => None, } } @@ -53,6 +57,7 @@ impl OpCode { | Self::TypeFunction | Self::TypeJudgment | Self::TypeQuantity + | Self::TypeEquality ) } @@ -124,6 +129,29 @@ pub(crate) enum EvidencePlan { }, } +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +#[repr(u8)] +pub(crate) enum EqualityRule { + Reflexive = 1, + Structural = 2, + Symmetry = 3, + Transitive = 4, + Congruence = 5, +} + +impl EqualityRule { + pub(crate) fn from_raw(value: u8) -> Option { + match value { + 1 => Some(Self::Reflexive), + 2 => Some(Self::Structural), + 3 => Some(Self::Symmetry), + 4 => Some(Self::Transitive), + 5 => Some(Self::Congruence), + _ => None, + } + } +} + #[derive(Debug, Clone, Copy, PartialEq, Eq)] #[repr(u8)] pub enum PortRole { @@ -134,6 +162,8 @@ pub enum PortRole { Subject = 5, Premise = 6, Conclusion = 7, + Left = 8, + Right = 9, } #[derive(Debug, Clone, Copy, PartialEq, Eq)] @@ -155,6 +185,8 @@ impl PortRole { 5 => Some(Self::Subject), 6 => Some(Self::Premise), 7 => Some(Self::Conclusion), + 8 => Some(Self::Left), + 9 => Some(Self::Right), _ => None, } } diff --git a/l64-native/src/kernel/validation.rs b/l64-native/src/kernel/validation.rs index aa1d3e9..3837442 100644 --- a/l64-native/src/kernel/validation.rs +++ b/l64-native/src/kernel/validation.rs @@ -79,6 +79,7 @@ impl Graph { }); } } + self.validate_equality_authority()?; Ok(()) } } diff --git a/l64-native/src/rna.rs b/l64-native/src/rna.rs index 294c7b3..fce714d 100644 --- a/l64-native/src/rna.rs +++ b/l64-native/src/rna.rs @@ -1,5 +1,6 @@ use std::collections::BTreeMap; +use crate::kernel::EqualityRule; use crate::{ ConstraintKind, ContextId, Dimension, DnaError, Graph, LocusWord, NodeId, Obstruction, OpCode, Proposal, ROOT_CONTEXT, Route, decode_dna, dna_bytes, diff --git a/l64-native/src/rna/compile.rs b/l64-native/src/rna/compile.rs index 5e13694..dbcea6e 100644 --- a/l64-native/src/rna/compile.rs +++ b/l64-native/src/rna/compile.rs @@ -116,7 +116,28 @@ pub fn compile_rna(source: &[u8]) -> Result { .transact(Proposal::square_root(route, context, input, output))? .node } - b"a" | b"m" | b"f" | b"q" | b"v" | b"k" | b"c" | b"x" | b"+" | b"*" | b"/" | b"r" => { + b"e" if parts.len() >= 6 => { + let rule_raw = parse_u8_part(&parts, 2, line)?; + let rule = EqualityRule::from_raw(rule_raw) + .ok_or(RnaError::InvalidNumber { line })?; + let left = resolve_part(&slots, &parts, 3, line)?; + let right = resolve_part(&slots, &parts, 4, line)?; + let context = parse_u32_part(&parts, 5, line)?; + let premises = parts[6..] + .iter() + .map(|part| { + let slot = parse_u64(part).ok_or(RnaError::InvalidNumber { line })?; + slots + .get(&slot) + .copied() + .ok_or(RnaError::UnknownSlot { line, slot }) + }) + .collect::, _>>()?; + graph + .prove_equality(route, context, left, right, rule, &premises)? + .node + } + b"a" | b"m" | b"f" | b"q" | b"v" | b"k" | b"c" | b"x" | b"+" | b"*" | b"/" | b"r" | b"e" => { return Err(RnaError::InvalidArity { line }); } _ => return Err(RnaError::UnknownInstruction { line }), diff --git a/l64-native/src/rna/sequence.rs b/l64-native/src/rna/sequence.rs index 6c2e663..421dd6b 100644 --- a/l64-native/src/rna/sequence.rs +++ b/l64-native/src/rna/sequence.rs @@ -36,7 +36,10 @@ pub fn rna_bytes(graph: &Graph) -> Result, RnaError> { .filter(|node| { !matches!( node.opcode(), - OpCode::TypeJudgment | OpCode::KernelWitness | OpCode::Obligation + OpCode::TypeJudgment + | OpCode::KernelWitness + | OpCode::Obligation + | OpCode::EqualityWitness ) }) .count(); @@ -180,6 +183,17 @@ fn emit_node( ); push_context(out, node.context()); } + OpCode::TypeEquality if ports.len() == 2 => { + push_prefix(out, b'e', slot); + let (rule, premises) = graph.equality_evidence_parts(node_id)?; + push_space_decimal(out, rule as u64); + push_space_decimal(out, slot_for(slots, ports[0].target())?); + push_space_decimal(out, slot_for(slots, ports[1].target())?); + push_space_decimal(out, u64::from(node.context())); + for premise in premises { + push_space_decimal(out, slot_for(slots, premise)?); + } + } _ => return Err(RnaError::UnrepresentableGraph), } out.push(b'\n'); diff --git a/l64-native/tests/architecture.rs b/l64-native/tests/architecture.rs index 6b8cc5d..fd0ff69 100644 --- a/l64-native/tests/architecture.rs +++ b/l64-native/tests/architecture.rs @@ -24,15 +24,21 @@ fn compact_layout_budgets_hold() { #[test] fn native_source_rejects_coordination_heavy_dependencies() { - let source_root = Path::new(env!("CARGO_MANIFEST_DIR")).join("src"); - let mut source = std::string::String::new(); - for entry in fs::read_dir(source_root).unwrap() { - let path = entry.unwrap().path(); - if path.extension().and_then(|part| part.to_str()) == Some("rs") { - source.push_str(&fs::read_to_string(path).unwrap()); + fn collect_rust(path: &Path, source: &mut std::string::String) { + for entry in fs::read_dir(path).unwrap() { + let path = entry.unwrap().path(); + if path.is_dir() { + collect_rust(&path, source); + } else if path.extension().and_then(|part| part.to_str()) == Some("rs") { + source.push_str(&fs::read_to_string(path).unwrap()); + } } } + let source_root = Path::new(env!("CARGO_MANIFEST_DIR")).join("src"); + let mut source = std::string::String::new(); + collect_rust(&source_root, &mut source); + let forbidden = [ ["Str", "ing"].concat(), ["HashMap", "<", "Str", "ing"].concat(), diff --git a/l64-native/tests/equality.rs b/l64-native/tests/equality.rs new file mode 100644 index 0000000..886ff7a --- /dev/null +++ b/l64-native/tests/equality.rs @@ -0,0 +1,273 @@ +use l64_native::{ + ConstraintKind, DecodeError, Dimension, Graph, LocusWord, OpCode, ROOT_CONTEXT, Route, + canonical_bytes, decode_canonical, dna_to_rna, rna_to_dna, +}; + +fn route(slot: u64) -> Route { + Route::root(LocusWord(0x4551)).composed(LocusWord(slot)) +} + +#[test] +fn primitive_equality_is_a_judgment_with_checked_witness() { + let mut graph = Graph::new(); + let left = graph.declare_atom_type(route(1), LocusWord(0x41)).unwrap(); + let right = graph.declare_atom_type(route(2), LocusWord(0x41)).unwrap(); + + let structural = graph + .prove_structural_equality(route(3), ROOT_CONTEXT, left, right) + .unwrap(); + assert_eq!( + graph.node(structural.node).unwrap().opcode(), + OpCode::TypeEquality + ); + assert_eq!( + graph.node(structural.evidence).unwrap().opcode(), + OpCode::EqualityWitness + ); + assert_eq!( + graph.node(structural.evidence).unwrap().ty(), + Some(structural.node) + ); + + let reflexive = graph + .prove_reflexive_equality(route(4), ROOT_CONTEXT, left) + .unwrap(); + assert_eq!( + graph.node(reflexive.node).unwrap().opcode(), + OpCode::TypeEquality + ); + + let bytes = canonical_bytes(&graph); + let decoded = decode_canonical(&bytes).unwrap(); + assert_eq!(canonical_bytes(&decoded), bytes); +} + +#[test] +fn symmetry_transitivity_and_route_canonicalization_follow_proof_paths() { + let mut graph = Graph::new(); + let left = graph.declare_atom_type(route(10), LocusWord(0x41)).unwrap(); + let right = graph.declare_atom_type(route(20), LocusWord(0x41)).unwrap(); + let forward = graph + .prove_structural_equality(route(30), ROOT_CONTEXT, left, right) + .unwrap(); + let backward = graph + .prove_symmetric_equality(route(40), ROOT_CONTEXT, forward.node) + .unwrap(); + graph + .prove_transitive_equality(route(50), ROOT_CONTEXT, forward.node, backward.node) + .unwrap(); + + assert_eq!( + graph.canonical_representative(ROOT_CONTEXT, right).unwrap(), + left + ); + assert_eq!( + graph + .canonical_representative_route(ROOT_CONTEXT, right) + .unwrap(), + route(10) + ); +} + +#[test] +fn congruence_lifts_checked_argument_equalities() { + let mut graph = Graph::new(); + let carrier_left = graph.declare_atom_type(route(1), LocusWord(0x52)).unwrap(); + let carrier_right = graph.declare_atom_type(route(2), LocusWord(0x52)).unwrap(); + let carrier_eq = graph + .prove_structural_equality(route(3), ROOT_CONTEXT, carrier_left, carrier_right) + .unwrap(); + + let dimension = Dimension::new([1, 0, 0, 0, 0, 0, 0]); + let quantity_left = graph + .declare_quantity_type(route(4), carrier_left, dimension) + .unwrap(); + let quantity_right = graph + .declare_quantity_type(route(5), carrier_right, dimension) + .unwrap(); + let quantity_eq = graph + .prove_congruent_equality( + route(6), + ROOT_CONTEXT, + quantity_left, + quantity_right, + &[carrier_eq.node], + ) + .unwrap(); + + let function_left = graph + .declare_function_type(route(7), quantity_left, quantity_left) + .unwrap(); + let function_right = graph + .declare_function_type(route(8), quantity_right, quantity_right) + .unwrap(); + graph + .prove_congruent_equality( + route(9), + ROOT_CONTEXT, + function_left, + function_right, + &[quantity_eq.node, quantity_eq.node], + ) + .unwrap(); + + assert_eq!( + graph + .canonical_representative(ROOT_CONTEXT, function_right) + .unwrap(), + function_left + ); +} + +#[test] +fn child_context_equality_does_not_escape_to_parent() { + let mut graph = Graph::new(); + let carrier = graph.declare_atom_type(route(1), LocusWord(0x52)).unwrap(); + let quantity = graph + .declare_quantity_type(route(2), carrier, Dimension::new([0, 0, 0, 0, 0, 0, 0])) + .unwrap(); + let value = graph + .insert_value(route(3), ROOT_CONTEXT, quantity) + .unwrap(); + let guard = graph + .declare_constraint( + route(4), + ROOT_CONTEXT, + value, + ConstraintKind::NonNegative, + true, + ) + .unwrap(); + let child = graph.extend_context(ROOT_CONTEXT, guard).unwrap(); + + let left = graph.declare_atom_type(route(5), LocusWord(0x41)).unwrap(); + let right = graph.declare_atom_type(route(6), LocusWord(0x41)).unwrap(); + graph + .prove_structural_equality(route(7), child, left, right) + .unwrap(); + + assert_eq!( + graph.canonical_representative(ROOT_CONTEXT, right).unwrap(), + right + ); + assert_eq!(graph.canonical_representative(child, right).unwrap(), left); +} + +#[test] +fn forged_equality_rule_is_rejected_during_decode() { + let mut graph = Graph::new(); + let left = graph.declare_atom_type(route(1), LocusWord(0x41)).unwrap(); + let right = graph.declare_atom_type(route(2), LocusWord(0x41)).unwrap(); + let proof = graph + .prove_structural_equality(route(3), ROOT_CONTEXT, left, right) + .unwrap(); + let mut bytes = canonical_bytes(&graph); + + const HEADER_BYTES: usize = 22; + const NODE_BYTES: usize = 24; + const PAYLOAD_OFFSET: usize = 10; + let offset = HEADER_BYTES + proof.evidence as usize * NODE_BYTES + PAYLOAD_OFFSET; + bytes[offset..offset + 8].copy_from_slice(&1_u64.to_le_bytes()); + + assert!(matches!( + decode_canonical(&bytes), + Err(DecodeError::InvalidAuthority) + )); +} + +#[test] +fn equality_path_exposes_deterministic_checked_provenance() { + let mut graph = Graph::new(); + let first = graph.declare_atom_type(route(10), LocusWord(0x41)).unwrap(); + let second = graph.declare_atom_type(route(20), LocusWord(0x41)).unwrap(); + let third = graph.declare_atom_type(route(30), LocusWord(0x41)).unwrap(); + let first_proof = graph + .prove_structural_equality(route(40), ROOT_CONTEXT, first, second) + .unwrap(); + let second_proof = graph + .prove_structural_equality(route(50), ROOT_CONTEXT, second, third) + .unwrap(); + + assert_eq!( + graph.equality_path(ROOT_CONTEXT, first, third).unwrap(), + vec![first_proof.node, second_proof.node] + ); +} + +#[test] +fn invalid_merges_are_rejected_before_state_mutation() { + let mut graph = Graph::new(); + let left = graph.declare_atom_type(route(1), LocusWord(0x41)).unwrap(); + let right = graph.declare_atom_type(route(2), LocusWord(0x42)).unwrap(); + let before = ( + graph.node_count(), + graph.port_count(), + graph.journal_len(), + graph.state_commitment(), + ); + + assert!(matches!( + graph.prove_structural_equality(route(3), ROOT_CONTEXT, left, right), + Err(l64_native::Obstruction::InvalidEqualityRule) + )); + assert_eq!( + ( + graph.node_count(), + graph.port_count(), + graph.journal_len(), + graph.state_commitment(), + ), + before + ); +} + +#[test] +fn forged_congruence_premise_path_is_rejected_during_decode() { + let mut graph = Graph::new(); + let carrier_left = graph.declare_atom_type(route(1), LocusWord(0x52)).unwrap(); + let carrier_right = graph.declare_atom_type(route(2), LocusWord(0x52)).unwrap(); + let carrier_eq = graph + .prove_structural_equality(route(3), ROOT_CONTEXT, carrier_left, carrier_right) + .unwrap(); + let dimension = Dimension::new([1, 0, 0, 0, 0, 0, 0]); + let quantity_left = graph + .declare_quantity_type(route(4), carrier_left, dimension) + .unwrap(); + let quantity_right = graph + .declare_quantity_type(route(5), carrier_right, dimension) + .unwrap(); + let proof = graph + .prove_congruent_equality( + route(6), + ROOT_CONTEXT, + quantity_left, + quantity_right, + &[carrier_eq.node], + ) + .unwrap(); + let evidence = graph.node(proof.evidence).unwrap(); + let premise_port = evidence.port_range().start; + let mut bytes = canonical_bytes(&graph); + + const HEADER_BYTES: usize = 22; + const NODE_BYTES: usize = 24; + const PORT_BYTES: usize = 8; + let port_base = HEADER_BYTES + graph.node_count() * NODE_BYTES; + let target_offset = port_base + premise_port * PORT_BYTES; + bytes[target_offset..target_offset + 4].copy_from_slice(&carrier_left.to_le_bytes()); + + assert!(matches!( + decode_canonical(&bytes), + Err(DecodeError::InvalidAuthority) + )); +} + +#[test] +fn equality_proofs_reach_exact_rna_dna_fixed_point() { + let source = b"L64R1 0x4551\na 1 0x41\na 2 0x41\ne 3 2 1 2 0\ne 4 3 2 1 0 3\ne 5 4 1 1 0 3 4\n"; + let dna = rna_to_dna(source).unwrap(); + let canonical_rna = dna_to_rna(&dna).unwrap(); + let rebuilt = rna_to_dna(&canonical_rna).unwrap(); + assert_eq!(rebuilt, dna); + assert!(canonical_rna.windows(2).any(|window| window == b"e ")); +}