// 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 }; }; }