Spaces:
Running
Running
File size: 5,145 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 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 | /**
* halt_eligibility.ts
*
* Runtime instillation of Lean theorem:
* Lutar.HUKLLA.HaltEligibility
* File: Lutar/HUKLLA/HaltEligibility.lean
* Commit: c4d13795689601324fce0236351bfe0ade990a43
*
* Lean theorems formalised here:
* - `halt_eligibility_monotone` (line ~81): eligibility is monotone in lambda_score
* - `halt_eligibility_decidable` (line ~96): Decidable instance
* - `not_eligible_of_low_score` (line ~103): score < 0.90 → not eligible
*
* Runtime contract:
* Given an ExecutionTrace (lambdaScore, receiptsClosed, rhoClosure),
* emit a DSSE receipt asserting whether the trace is halt-eligible.
* The 0.90 threshold matches A11OY_DOCTRINE_LAMBDA_FLOOR=0.90.
*
* Doctrine v7: No new axioms. No sorries. STAGED label: gate is FULLY WIRED.
*/
import { createHash } from "crypto";
// ---------------------------------------------------------------------------
// Domain types
// ---------------------------------------------------------------------------
/** Mirrors Lean `ExecutionTrace` structure. */
export interface ExecutionTrace {
/** Lambda trust score ∈ [0, 1]. */
lambdaScore: number;
/** Receipts confirmed closed. */
receiptsClosed: boolean;
/** ρ-closure invariant satisfied. */
rhoClosure: boolean;
}
/** DSSE-shaped receipt emitted after each gate evaluation. */
export interface DSSEReceipt {
theorem: string;
lean_commit_sha: string;
inputs_hash: string;
output: boolean;
ts: string;
sig: string;
}
/** Signer interface — production uses ECDSA P-256; tests use a mock. */
export type Signer = (payload: string) => string;
// ---------------------------------------------------------------------------
// Anchor constants (matches a11oy/deploy/manifests/a11oy-deployment.yaml L34–35)
// ---------------------------------------------------------------------------
/** The HUKLLA T01/T02 axis floor. */
export const LAMBDA_FLOOR = 0.90;
const LEAN_THEOREM = "Lutar.HUKLLA.HaltEligibility";
const LEAN_FILE_LINE = "Lutar/HUKLLA/HaltEligibility.lean:70";
const LEAN_COMMIT_SHA = "c4d13795689601324fce0236351bfe0ade990a43";
// ---------------------------------------------------------------------------
// Core predicate — mirrors Lean `isHaltEligible`
// ---------------------------------------------------------------------------
/**
* Evaluates whether an execution trace satisfies HUKLLA halt-eligibility.
*
* Lean proof `halt_eligibility_monotone` guarantees: if `t1.lambdaScore ≤ t2.lambdaScore`
* and booleans are equal, then eligibility is monotone (t1 eligible ⟹ t2 eligible).
*
* Lean proof `not_eligible_of_low_score` guarantees: score < 0.90 → false.
*
* @param trace - The execution trace to evaluate.
* @returns true iff all three conditions hold.
*/
export function isHaltEligible(trace: ExecutionTrace): boolean {
return (
trace.lambdaScore >= LAMBDA_FLOOR &&
trace.receiptsClosed &&
trace.rhoClosure
);
}
// ---------------------------------------------------------------------------
// Inputs hash helper
// ---------------------------------------------------------------------------
function hashInputs(trace: ExecutionTrace): string {
const payload = JSON.stringify({
lambdaScore: trace.lambdaScore,
receiptsClosed: trace.receiptsClosed,
rhoClosure: trace.rhoClosure,
});
return createHash("sha256").update(payload).digest("hex");
}
// ---------------------------------------------------------------------------
// DSSE receipt emitter
// ---------------------------------------------------------------------------
/**
* Evaluates halt-eligibility and emits a DSSE-shaped receipt.
*
* Lean theorem: `Lutar.HUKLLA.HaltEligibility.halt_eligibility_monotone`
* File: Lutar/HUKLLA/HaltEligibility.lean:81
* Commit: c4d13795689601324fce0236351bfe0ade990a43
*
* @param trace - ExecutionTrace to evaluate.
* @param signer - Signing function (ECDSA P-256 in production).
* @returns DSSEReceipt containing the halt-eligibility verdict.
*/
export function emitHaltEligibilityReceipt(
trace: ExecutionTrace,
signer: Signer
): DSSEReceipt {
const output = isHaltEligible(trace);
const inputs_hash = hashInputs(trace);
const ts = new Date().toISOString();
const sigPayload = JSON.stringify({
theorem: LEAN_THEOREM,
lean_commit_sha: LEAN_COMMIT_SHA,
inputs_hash,
output,
ts,
});
return {
theorem: LEAN_THEOREM,
lean_commit_sha: LEAN_COMMIT_SHA,
inputs_hash,
output,
ts,
sig: signer(sigPayload),
};
}
// ---------------------------------------------------------------------------
// Gate entry point (convenience wrapper)
// ---------------------------------------------------------------------------
/**
* The a11oy gate for Lutar.HUKLLA.HaltEligibility.
* Returns `{ eligible, receipt }`.
*
* @param trace - ExecutionTrace
* @param signer - Signing function
*/
export function haltEligibilityGate(
trace: ExecutionTrace,
signer: Signer
): { eligible: boolean; receipt: DSSEReceipt } {
const receipt = emitHaltEligibilityReceipt(trace, signer);
return { eligible: receipt.output, receipt };
}
|