Spaces:
Running
Running
| // SPDX-License-Identifier: Apache-2.0 | |
| // © 2026 Lutar, Stephen P. — SZL Holdings | |
| // ORCID: 0009-0001-0110-4173 | |
| // | |
| // Layer 6 — a11oy policy gate for HashChainIntegrity (A6) | |
| // | |
| // Policy rationale: | |
| // Every spine entry must satisfy: entry.chain = SHA256(prev_entry). | |
| // This gate validates a submitted chain array for sequential hash linkage, | |
| // denying any sequence where a break in the chain is detected. | |
| // | |
| // Lean axiom cited: `hashChainIntegrity` (A6) | |
| // Lean file: Lutar/Gate/HashChainIntegrity.lean | |
| // Lean commit SHA: 1dca00032dfc9aa8559cc6c2e4b63192fcf52371 | |
| // Lean status: theorem (ENFORCED) | |
| // | |
| // Policy: if all chain links are valid → allow; else → deny | |
| // | |
| // References: | |
| // Zenodo: https://doi.org/10.5281/zenodo.20119582 | |
| // Thesis §3.4: hashChainIntegrity | |
| import { createHash } from 'node:crypto'; | |
| export interface HashChainIntegrityGateConfig { | |
| /** Hash algorithm. Default: 'sha256'. */ | |
| algorithm?: string; | |
| } | |
| export interface ChainEntry { | |
| entryId: string; | |
| payload: string; | |
| chainHash: string; // SHA256(JSON.stringify(prevEntry)) | |
| } | |
| export interface HashChainIntegrityGateOpts { | |
| entries: ChainEntry[]; | |
| } | |
| export interface HashChainIntegrityDecision { | |
| allow: boolean; | |
| rationale: string; | |
| formula: string; | |
| leanTheorem: string; | |
| leanFile: string; | |
| leanCommitSha: string; | |
| entryCount: number; | |
| firstBreakIndex: number | null; | |
| lambdaScore: number; | |
| } | |
| const LEAN_THEOREM = "hashChainIntegrity"; | |
| const LEAN_FILE = "Lutar/Gate/HashChainIntegrity.lean"; | |
| const LEAN_COMMIT = "1dca00032dfc9aa8559cc6c2e4b63192fcf52371"; | |
| // ── Inline formula ──────────────────────────────────────────────────────────── | |
| // A6: ∀n≥1: entry[n].chain = SHA256(JSON.stringify(entry[n-1])) | |
| function _hashEntry(entry: ChainEntry, algo: string): string { | |
| return createHash(algo).update(JSON.stringify(entry)).digest('hex'); | |
| } | |
| /** | |
| * HashChainIntegrity (A6) policy gate. | |
| * | |
| * Verifies that each entry's chainHash equals SHA256 of the previous entry. | |
| * The genesis entry (index 0) is accepted without a predecessor check. | |
| * | |
| * Lean axiom: `hashChainIntegrity` (A6) | |
| * Lean file: Lutar/Gate/HashChainIntegrity.lean (commit 1dca00032dfc9aa8559cc6c2e4b63192fcf52371) | |
| * Zenodo: https://doi.org/10.5281/zenodo.20119582 | |
| */ | |
| export function hashChainIntegrityGate( | |
| config: HashChainIntegrityGateConfig = {} | |
| ): (opts: HashChainIntegrityGateOpts) => HashChainIntegrityDecision { | |
| const algorithm = config.algorithm ?? 'sha256'; | |
| return function gate(opts: HashChainIntegrityGateOpts): HashChainIntegrityDecision { | |
| const { entries } = opts; | |
| if (!Array.isArray(entries) || entries.length === 0) { | |
| throw new Error(`HashChainIntegrityGate: entries must be a non-empty array`); | |
| } | |
| let firstBreakIndex: number | null = null; | |
| for (let i = 1; i < entries.length; i++) { | |
| const expected = _hashEntry(entries[i - 1], algorithm); | |
| if (entries[i].chainHash !== expected) { | |
| firstBreakIndex = i; | |
| break; | |
| } | |
| } | |
| const allow = firstBreakIndex === null; | |
| const lambdaScore = allow ? 1.0 : (firstBreakIndex! - 1) / entries.length; | |
| const rationale = allow | |
| ? `HashChainIntegrity (A6): ${entries.length} entries, all ${algorithm} links valid. Passes. Lean: ${LEAN_THEOREM} @${LEAN_COMMIT.slice(0, 12)}` | |
| : `HashChainIntegrity (A6): chain break at entry[${firstBreakIndex}] — expected hash mismatch. Denied. Lean: ${LEAN_THEOREM} @${LEAN_COMMIT.slice(0, 12)}`; | |
| return { allow, rationale, formula: "HashChainIntegrity", leanTheorem: LEAN_THEOREM, leanFile: LEAN_FILE, leanCommitSha: LEAN_COMMIT, entryCount: entries.length, firstBreakIndex, lambdaScore }; | |
| }; | |
| } | |