Add Commander-governed proof-producing congruence

.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

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

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

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";

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.

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;

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)

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,

l64-native/src/graph/construction.rs

@@ -187,7 +187,7 @@ impl Graph {
     ) -> Result<NodeId, Obstruction> {
         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,
+        }
+    }
 }

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");

l64-native/src/kernel/equality.rs

@@ -0,0 +1,3 @@
+include!("equality/proof.rs");
+include!("equality/validation.rs");
+include!("equality/canonical.rs");