Hugging Face's logo

Spaces:
SZLHOLDINGS
/
a11oy
Running

App Files Community
22
a11oy
File size: 4,565 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
// SPDX-License-Identifier: Apache-2.0
// © 2026 Lutar, Stephen P. — SZL Holdings
// ORCID: 0009-0001-0110-4173
//
// Layer 6 — a11oy policy gate for DoctrineCompleteness (A9)
//
// Policy rationale:
//   doctrine.json v1.0.0 must enumerate all 8 forbidden patterns and carry
//   a SHA-256 anchor. Any artifact that fails the SHA-256 check or lacks
//   one of the 8 forbidden pattern entries is denied. This gate is the
//   policy-layer enforcement of doctrine-check.sh.
//
//   Lean axiom cited: `doctrineCompleteness` (A9)
//   Lean file: Lutar/Gate/DoctrineCompleteness.lean
//   Lean commit SHA: 1dca00032dfc9aa8559cc6c2e4b63192fcf52371
//   Lean status: theorem (ENFORCED)
//
//   Policy: if SHA-256 matches AND all 8 FPs present → allow; else → deny
//
// References:
//   https://github.com/szl-holdings/szl-trust
//   Thesis §8: doctrineCompleteness

import { createHash } from 'node:crypto';

export interface DoctrineCompletenessGateConfig {
  /** Canonical SHA-256 of doctrine.json. Required. */
  canonicalSha256: string;
  /** Expected forbidden pattern count. Default: 8. */
  requiredPatternCount?: number;
}

export interface DoctrineCompletenessGateOpts {
  /** Raw JSON string of doctrine.json. */
  doctrineJsonRaw: string;
  /** Array of forbidden pattern keys found in the artifact. */
  detectedPatterns: string[];
}

export interface DoctrineCompletenessDecision {
  allow:              boolean;
  rationale:          string;
  formula:            string;
  leanTheorem:        string;
  leanFile:           string;
  leanCommitSha:      string;
  sha256Match:        boolean;
  detectedSha256:     string;
  patternCount:       number;
  requiredPatterns:   number;
  lambdaScore:        number;
}

const LEAN_THEOREM = "doctrineCompleteness";
const LEAN_FILE    = "Lutar/Gate/DoctrineCompleteness.lean";
const LEAN_COMMIT  = "1dca00032dfc9aa8559cc6c2e4b63192fcf52371";
const DEFAULT_PATTERNS = 8;

// ── Inline formula ────────────────────────────────────────────────────────────
// A9: SHA256(doctrine.json) = canonical ∧ |FP| = 8 ⟹ no forbidden patterns in artifacts

/**
 * DoctrineCompleteness (A9) policy gate.
 *
 * Verifies doctrine.json SHA-256 integrity and that all 8 forbidden patterns
 * are enumerated. Matches the behavior of `scripts/doctrine-check.sh`.
 *
 * Lean axiom: `doctrineCompleteness` (A9)
 * Lean file: Lutar/Gate/DoctrineCompleteness.lean (commit 1dca00032dfc9aa8559cc6c2e4b63192fcf52371)
 * https://github.com/szl-holdings/szl-trust
 */
export function doctrineCompletenessGate(
  config: DoctrineCompletenessGateConfig
): (opts: DoctrineCompletenessGateOpts) => DoctrineCompletenessDecision {
  const { canonicalSha256 } = config;
  const requiredPatterns = config.requiredPatternCount ?? DEFAULT_PATTERNS;
  if (!canonicalSha256 || canonicalSha256.length !== 64) {
    throw new Error(`DoctrineCompletenessGate: canonicalSha256 must be 64-char hex string`);
  }

  return function gate(opts: DoctrineCompletenessGateOpts): DoctrineCompletenessDecision {
    const { doctrineJsonRaw, detectedPatterns } = opts;
    if (typeof doctrineJsonRaw !== 'string' || doctrineJsonRaw.length === 0) {
      throw new Error(`DoctrineCompletenessGate: doctrineJsonRaw must be non-empty`);
    }

    const detectedSha256 = createHash('sha256').update(doctrineJsonRaw).digest('hex');
    const sha256Match    = detectedSha256 === canonicalSha256;
    const patternCount   = detectedPatterns.length;
    const allow          = sha256Match && patternCount >= requiredPatterns;
    const lambdaScore    = (sha256Match ? 0.5 : 0) + (patternCount / requiredPatterns) * 0.5;

    const rationale = allow
      ? `DoctrineCompleteness (A9): SHA-256 matches; ${patternCount} patterns ≥ ${requiredPatterns}. doctrine-check PASS. Lean: ${LEAN_THEOREM} @${LEAN_COMMIT.slice(0, 12)}`
      : sha256Match
        ? `DoctrineCompleteness (A9): SHA-256 OK but only ${patternCount}/${requiredPatterns} patterns. Denied. Lean: ${LEAN_THEOREM} @${LEAN_COMMIT.slice(0, 12)}`
        : `DoctrineCompleteness (A9): SHA-256 mismatch — expected ${canonicalSha256.slice(0,16)}…, got ${detectedSha256.slice(0,16)}…. Denied. Lean: ${LEAN_THEOREM} @${LEAN_COMMIT.slice(0, 12)}`;

    return { allow, rationale, formula: "DoctrineCompleteness", leanTheorem: LEAN_THEOREM, leanFile: LEAN_FILE, leanCommitSha: LEAN_COMMIT, sha256Match, detectedSha256, patternCount, requiredPatterns, lambdaScore };
  };
}