Spaces:
Running
Running
File size: 2,969 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 | // SPDX-License-Identifier: Apache-2.0
// © 2026 Lutar, Stephen P. — SZL Holdings
// ORCID: 0009-0001-0110-4173
//
// Layer 6 — a11oy policy gate for ReplayDeterminism (T5)
//
// Policy rationale:
// For canonical JSON + pinned PRNG + frozen registry, 5× replay must yield
// the canonical root "1ed4d253…". Any deviation from the expected root is
// a determinism violation that blocks production deployment.
//
// Lean derivation cited: `replayDeterminism` (T5)
// Lean file: Lutar/Gate/ReplayDeterminism.lean
// Lean commit SHA: 1dca00032dfc9aa8559cc6c2e4b63192fcf52371
// Lean status: theorem (ENFORCED)
//
// References:
// Zenodo: https://doi.org/10.5281/zenodo.20119582
// INNOVATIONS.md §2 T5: replay determinism proof
export interface ReplayDeterminismGateConfig {
/** Expected canonical Merkle root. Required. */
canonicalRoot: string;
/** Required replay run count. Default: 5. */
requiredRuns?: number;
}
export interface ReplayDeterminismGateOpts {
replayRoots: string[];
}
export interface ReplayDeterminismDecision {
allow: boolean;
rationale: string;
formula: string;
leanTheorem: string;
leanFile: string;
leanCommitSha: string;
canonicalRoot: string;
matchingRuns: number;
totalRuns: number;
lambdaScore: number;
}
const LEAN_THEOREM = "replayDeterminism";
const LEAN_FILE = "Lutar/Gate/ReplayDeterminism.lean";
const LEAN_COMMIT = "1dca00032dfc9aa8559cc6c2e4b63192fcf52371";
const DEFAULT_RUNS = 5;
export function replayDeterminismGate(
config: ReplayDeterminismGateConfig
): (opts: ReplayDeterminismGateOpts) => ReplayDeterminismDecision {
const { canonicalRoot } = config;
const requiredRuns = config.requiredRuns ?? DEFAULT_RUNS;
if (!canonicalRoot) throw new Error(`ReplayDeterminismGate: canonicalRoot is required`);
return function gate(opts: ReplayDeterminismGateOpts): ReplayDeterminismDecision {
const { replayRoots } = opts;
if (!Array.isArray(replayRoots) || replayRoots.length < requiredRuns) {
throw new Error(`ReplayDeterminismGate: need ${requiredRuns} roots; got ${replayRoots?.length}`);
}
const matchingRuns = replayRoots.slice(0, requiredRuns).filter(r => r === canonicalRoot).length;
const allow = matchingRuns === requiredRuns;
const lambdaScore = matchingRuns / requiredRuns;
const rationale = allow
? `ReplayDeterminism (T5): all ${requiredRuns} runs match canonical root "${canonicalRoot.slice(0,16)}…". Passes. Lean: ${LEAN_THEOREM} @${LEAN_COMMIT.slice(0, 12)}`
: `ReplayDeterminism (T5): ${matchingRuns}/${requiredRuns} runs matched — determinism violation. Denied. Lean: ${LEAN_THEOREM} @${LEAN_COMMIT.slice(0, 12)}`;
return { allow, rationale, formula: "ReplayDeterminism", leanTheorem: LEAN_THEOREM, leanFile: LEAN_FILE, leanCommitSha: LEAN_COMMIT, canonicalRoot, matchingRuns, totalRuns: replayRoots.length, lambdaScore };
};
}
|