imhotep/Imhotep
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

refactor: missing-fact discipline in proof witness generation

Browse Source 
- Remove defensive ?? 0 fallbacks in buildFailedPredicate that could
  silently report false geometry in proof witnesses
- Require all 4 rect fields present before building subjectRect/referenceRect
  (was only checking subjectLeft)
- Add explicit undefined guards for observed gap, measured values,
  delta, and aspect ratio — return undefined (no failedPredicate)
  when critical metrics are missing instead of fabricating 0 defaults
- Generic synthesizeGenericFailedPredicate checks value presence
  instead of defaulting metrics[keys] to 0
- Option defaults (minGap, maxGap, tolerance, min, max bounds)
  retain ?? 0/?? Infinity as correct neutral values for user parameters
This commit is contained in:
John Dvorak
2026-05-22 16:17:18 -07:00
parent ce04b2b3de
commit 3b7be0aaf0
1 changed files with 72 additions and 51 deletions
Download Patch File Download Diff File Expand all files Collapse all files
packages/imhotep-solver/src/proofs.ts
+72 -51
View File
@@ -59,9 +59,20 @@ function buildFailedPredicate(
// --- Directional gap (leftOf / rightOf / above / below) --- // --- Directional gap (leftOf / rightOf / above / below) ---
if (hasGap) { if (hasGap) {
const gap = metrics.observedGap ?? metrics.gap ?? 0; const gap = metrics.observedGap ?? metrics.gap;
if (gap === undefined) return undefined;
const min = metrics.minGap ?? 0; const min = metrics.minGap ?? 0;
const max = metrics.maxGap ?? Infinity; const max = metrics.maxGap ?? Infinity;
const hasSubjectRect =
metrics.subjectLeft !== undefined &&
metrics.subjectTop !== undefined &&
metrics.subjectRight !== undefined &&
metrics.subjectBottom !== undefined;
const hasRefRect =
metrics.refLeft !== undefined &&
metrics.refTop !== undefined &&
metrics.refRight !== undefined &&
metrics.refBottom !== undefined;
return { return {
...base, ...base,
op: gap < min ? '<' : '>', op: gap < min ? '<' : '>',
@@ -70,68 +81,71 @@ function buildFailedPredicate(
measuredGap: gap, measuredGap: gap,
expectedMinGap: Number.isFinite(min) ? min : undefined, expectedMinGap: Number.isFinite(min) ? min : undefined,
expectedMaxGap: Number.isFinite(max) ? max : undefined, expectedMaxGap: Number.isFinite(max) ? max : undefined,
subjectRect: subjectRect: hasSubjectRect
metrics.subjectLeft !== undefined ? {
? { left: metrics.subjectLeft,
left: metrics.subjectLeft, top: metrics.subjectTop,
top: metrics.subjectTop ?? 0, right: metrics.subjectRight,
right: metrics.subjectRight ?? 0, bottom: metrics.subjectBottom,
bottom: metrics.subjectBottom ?? 0, }
} : undefined,
: undefined, referenceRect: hasRefRect
referenceRect: ? {
metrics.refLeft !== undefined left: metrics.refLeft,
? { top: metrics.refTop,
left: metrics.refLeft, right: metrics.refRight,
top: metrics.refTop ?? 0, bottom: metrics.refBottom,
right: metrics.refRight ?? 0, }
bottom: metrics.refBottom ?? 0, : undefined,
}
: undefined,
}; };
} }
// --- Containment / inside (unique overflow metrics) --- // --- Containment / inside (unique overflow metrics) ---
if (kind === 'inside') { if (kind === 'inside') {
const overflowLeft = metrics.overflowLeft ?? 0; const hasSubjectRect =
const overflowTop = metrics.overflowTop ?? 0; metrics.subjectLeft !== undefined &&
const overflowRight = metrics.overflowRight ?? 0; metrics.subjectTop !== undefined &&
const overflowBottom = metrics.overflowBottom ?? 0; metrics.subjectRight !== undefined &&
metrics.subjectBottom !== undefined;
const hasRefRect =
metrics.refLeft !== undefined &&
metrics.refTop !== undefined &&
metrics.refRight !== undefined &&
metrics.refBottom !== undefined;
return { return {
...base, ...base,
op: 'not-contained', op: 'not-contained',
left: 0, left: 0,
right: 0, right: 0,
overflowEdges: { overflowEdges: {
left: overflowLeft, left: metrics.overflowLeft ?? 0,
top: overflowTop, top: metrics.overflowTop ?? 0,
right: overflowRight, right: metrics.overflowRight ?? 0,
bottom: overflowBottom, bottom: metrics.overflowBottom ?? 0,
}, },
subjectRect: subjectRect: hasSubjectRect
metrics.subjectLeft !== undefined ? {
? { left: metrics.subjectLeft,
left: metrics.subjectLeft, top: metrics.subjectTop,
top: metrics.subjectTop ?? 0, right: metrics.subjectRight,
right: metrics.subjectRight ?? 0, bottom: metrics.subjectBottom,
bottom: metrics.subjectBottom ?? 0, }
} : undefined,
: undefined, referenceRect: hasRefRect
referenceRect: ? {
metrics.refLeft !== undefined left: metrics.refLeft,
? { top: metrics.refTop,
left: metrics.refLeft, right: metrics.refRight,
top: metrics.refTop ?? 0, bottom: metrics.refBottom,
right: metrics.refRight ?? 0, }
bottom: metrics.refBottom ?? 0, : undefined,
}
: undefined,
}; };
} }
// --- Size threshold (atLeast / atMost / between) --- // --- Size threshold (atLeast / atMost / between) ---
if (isSize && kind !== 'aspectRatio') { if (isSize && kind !== 'aspectRatio') {
const observed = metrics.observed ?? metrics.value ?? 0; const observed = metrics.observed ?? metrics.value;
if (observed === undefined) return undefined;
const min = metrics.min ?? -Infinity; const min = metrics.min ?? -Infinity;
const max = metrics.max ?? Infinity; const max = metrics.max ?? Infinity;
return { return {
@@ -147,7 +161,8 @@ function buildFailedPredicate(
// --- Aspect ratio --- // --- Aspect ratio ---
if (kind === 'aspectRatio') { if (kind === 'aspectRatio') {
const observed = metrics.observed ?? 0; const observed = metrics.observed;
if (observed === undefined) return undefined;
const minRatio = metrics.minRatio ?? -Infinity; const minRatio = metrics.minRatio ?? -Infinity;
const maxRatio = metrics.maxRatio ?? Infinity; const maxRatio = metrics.maxRatio ?? Infinity;
return { return {
@@ -163,7 +178,8 @@ function buildFailedPredicate(
// --- Alignment (alignedWith / centeredWithin) --- // --- Alignment (alignedWith / centeredWithin) ---
if (hasAxis || kind === 'centeredWithin') { if (hasAxis || kind === 'centeredWithin') {
const delta = metrics.delta ?? metrics.deltaX ?? metrics.deltaY ?? 0; const delta = metrics.delta ?? metrics.deltaX ?? metrics.deltaY;
if (delta === undefined) return undefined;
const tolerance = metrics.tolerance ?? 0; const tolerance = metrics.tolerance ?? 0;
return { return {
...base, ...base,
@@ -188,16 +204,21 @@ function synthesizeGenericFailedPredicate(
): Proof['failedPredicate'] { ): Proof['failedPredicate'] {
const keys = Object.keys(metrics); const keys = Object.keys(metrics);
if (keys.length >= 2) { if (keys.length >= 2) {
const left = metrics[keys[0]];
const right = metrics[keys[1]];
if (left === undefined || right === undefined) return undefined;
return { return {
op: '<', op: '<',
left: metrics[keys[0]] ?? 0, left,
right: metrics[keys[1]] ?? 0, right,
}; };
} }
if (keys.length === 1) { if (keys.length === 1) {
const val = metrics[keys[0]];
if (val === undefined) return undefined;
return { return {
op: '<', op: '<',
left: metrics[keys[0]] ?? 0, left: val,
right: 0, right: 0,
}; };
} }