File size: 3,848 Bytes
518343a
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
// 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 };
  };
}