docs(261026-d95): record seeded oracle and paired NO-GO verdict
This commit is contained in:
@@ -1,6 +1,6 @@
|
||||
# Direction-split ALT: proof gate (research branch only)
|
||||
|
||||
Status: P-1 and P-2 proved for **pair-restricted domain and independent A* stopping** below; measurements pending. This is not a proof for the shipped Ikeda sum-of-tops rule with asymmetric families.
|
||||
**Verdict: NO-GO** for deployment and the 8 ms Worker budget. P-1 and P-2 proved for **pair-restricted domain and independent A* stopping** below; the measured branch-only implementation is 4.35× slower at paired p95 than the original control despite fewer expansions. This is not a proof for the shipped Ikeda sum-of-tops rule with asymmetric families.
|
||||
|
||||
## Graph and tables
|
||||
|
||||
@@ -26,6 +26,22 @@ For each side, consistency gives reduced edge `c+h(next)-h(current)≥0` on that
|
||||
|
||||
Hand checks: oneway ring `0→1→2→0` with a forbidden bit0 mirror `1→0`, forward to[0] labels (0,2,1) for unit edges and backward from[0] (0,1,2); all allowed edges respect their *respective* oriented inequalities while mirror never relaxes. Bridge `A→B` costing 1 with no return, anchor in A: from[B] finite and to[B] sentinel; anchor in B: to[A] finite and from[A] sentinel. For a query A→B, applicable columns require origin/goal finite and S retains the bridge; B→A fails the endpoint reachability check and returns null. Disconnected anchored island vs unanchored component has sentinel endpoint(s); a route wholly in the unanchored component retains an empty active set and can still succeed, while a cross-component route is null. In all three examples, cross-boundary edges are excluded only if they cannot be on an o→g path.
|
||||
|
||||
## Experiment and verdict
|
||||
## Measured experiment and verdict
|
||||
|
||||
Pending runner, adversarial oracle checks and paired host measurements. The 8 ms Worker budget is **NOT MEASURED** here; no synthetic speedup or host-local result can certify the Worker free-plan gate.
|
||||
Branch-only `routing/scripts/experiment-alt-direction-split.mjs` implements these independent A* keys, single-vertex meets, stale-key pruning and a query-domain mask. New suite `routing/test/alt-direction-split-experiment.test.mjs` tests **every pair** across one-way rings with blocked mirrors/spurs and equal costs, both directions of one-way bridges, isolated anchored/unanchored islands, endpoints and interior `0xffff` cells, mixed columns and a finite→sentinel cross-edge per-node skip adversary. Each checks independent O(V²) Dijkstra seconds, null classes and legal reconstructed edges. On real graph, `sweepOracle` uses the *exact* 200 compared snapped cross-metro pairs (seed `0x08f1`, 600 draws, 12 km minimum, 120 rejected snap misses) and independent heap-Dijkstra; **182 routed, 18 unreachable; suboptimal 0, oracle-mismatch 0, class-break 0** at symmetric ±1e-6 s. No synthetic or real pair disproved this conservative stop; the counterexample to naive per-node masking is above, not a measured result of this runner.
|
||||
|
||||
Measured 2026-10-26 on `HAFu`, Node v24.18.0, Linux, binary SHA-256 `366e1be2ca270e5e67cb0debc98887b6dcb66f29849747d59f4e0e58739ec5b8`, ARG2 311,361 nodes / 677,126 edges. This checkout's `routing/data/kl-roadgraph.v1.bin` is an **existing read-only symlink** to the other checkout; no binary modifications. Reproduction: `node routing/scripts/experiment-alt-direction-split.mjs`. The experimental instrumented comparison used an automatically removed temporary *source-identical* shipped clone with only two settled counters injected, and also timed original unmodified `routeAstar` on the same snapped endpoints. Clone/original seconds agreed to ±1e-6 for each routed sample. A dedicated warm-up (not included) took experimental 0.935 ms, original 20.005 ms, clone 27.471 ms.
|
||||
|
||||
The seed `0x08a1` 100-pair, ≥12 km extended draw produced **41 snap misses, 6 unreachable and 53 routed**; each routed pair was measured twice, reversed run order across rounds (106 routed measurements each). Misses are **outside** routed p95; each pair was compared at identical snapped endpoints. Times are Node `hrtime` wall elapsed for search call on this host, *not Cloudflare Worker CPU instrumentation*, so they cannot establish a Worker CPU PASS.
|
||||
|
||||
| Search | n | Median ms | Mean ms | p95 ms | Total settled expansions (106 calls) |
|
||||
|---|---:|---:|---:|---:|---:|
|
||||
| Direction-split / domain-mask experimental | 106 | 150.845 | 197.490 | **516.778** | 9,958,938 (forward/backward split NOT MEASURED) |
|
||||
| Source-identical isolated shipped clone + settled counters | 106 | 73.588 | 72.331 | 129.327 | 14,037,662 (6,764,880 fwd / 7,272,782 bwd) |
|
||||
| Original shipped haversine-only `routeAstar`, unmodified | 106 | 73.619 | 71.864 | **118.923** | NOT MEASURED directly (clone is expansion proxy) |
|
||||
|
||||
Experimental/clone expansion ratio **0.709×**; experimental/original shipped paired p95 **4.35× slower** despite fewer settles. The experiment selected an average of 22.64 to- and 18.87 from-columns per routed call (2400/106 and 2000/106 respectively); shipped has 0/24 clean columns and is the actual haversine-only control. No claim of runtime speedup. Search-scoped domain scanning, per-vertex `Math.max`, and heaps/allocations in this research runner may account for some overhead, but optimization is NOT demonstrated and no performance claim is transferable to an optimized Worker implementation.
|
||||
|
||||
Control gates unchanged: `npm run routing:test` **85 passed, 0 failed**, including shipped A1/625; `npm run routing:typecheck` **PASS**. `node routing/scripts/measure-optimality-gate.mjs` D-03 frozen record **PASS** (53 routed equal, 6 unreachable, 41 unsnappable; 0 class breaks). `node routing/scripts/measure-route-cpu.mjs --extended` shipped-control **FAIL**: 53 routed/100, p95 **127.933 ms**, >8 ms; 47 misses printed separately. Early test invocation lacked installed dependencies and failed L2/tsc; `npm ci --ignore-scripts --no-audit --no-fund` installed local dependencies, and both gates then passed; no source changes to those gates.
|
||||
|
||||
**Proof status:** P-1 PASS for induced pair domain; P-2 PASS for the conservative independent-frontier stopping bound, **NOT** a proof of asymmetric Ikeda sum stopping. **Oracle status:** 0 violations in synthetic exhaustive and real seeded runs. **Budget status:** local original control FAIL on 8 ms test; candidate local p95 FAIL; representative free-plan Worker 8 ms **NOT MEASURED**. **Recommendation:** NO-GO on integration; retain original A*, baseline and bot/web unchanged. A later, separately approved investigation could evaluate typed-array/precomputed component labels and a separately proved stronger meet bound, then rerun identical oracle and actual Worker-host CPU gates. No merge or Worker-budget retirement is justified.
|
||||
|
||||
@@ -1,6 +1,6 @@
|
||||
#!/usr/bin/env node
|
||||
/* Branch-only directional ALT experiment. Neither production nor integrations import this. */
|
||||
import { readFileSync, existsSync } from 'node:fs';
|
||||
import { readFileSync, existsSync, writeFileSync, unlinkSync } from 'node:fs';
|
||||
import { createHash } from 'node:crypto';
|
||||
import { hostname } from 'node:os';
|
||||
import { fileURLToPath } from 'node:url';
|
||||
@@ -11,6 +11,23 @@ import { routeAstar } from '../src/astar.ts';
|
||||
import { generateCrossMetroPairs } from './measure-optimality-baseline.mjs';
|
||||
import { sweepOracle } from './measure-astar-oracle-sweep.mjs';
|
||||
|
||||
// Source-identical isolated instrumented clone: only two settled counters are injected.
|
||||
// The production file is never opened for writing; remove the ephemeral copy in finally.
|
||||
async function instrumentedShipped() {
|
||||
const source = new URL('../src/astar.ts', import.meta.url);
|
||||
const clone = new URL('../src/astar-alt-measure.tmp.ts', import.meta.url);
|
||||
let code = readFileSync(source, 'utf8');
|
||||
const forward = 'if (expandForward) fClosed[u] = 1;', backward = 'else bClosed[u] = 1;';
|
||||
if (!code.includes(forward) || !code.includes(backward)) throw Error('production settled markers changed; instrumentation not valid');
|
||||
code = code.replace(forward, 'if (expandForward) { fClosed[u] = 1; globalThis.__altControlSettled.forward++; }')
|
||||
.replace(backward, 'else { bClosed[u] = 1; globalThis.__altControlSettled.backward++; }');
|
||||
if (existsSync(clone)) throw Error('temporary instrumentation clone already exists');
|
||||
try {
|
||||
writeFileSync(clone, code, { flag: 'wx' });
|
||||
return await import(clone.href);
|
||||
} finally { if (existsSync(clone)) unlinkSync(clone); }
|
||||
}
|
||||
|
||||
const INF = Infinity, SENTINEL = 0xffff;
|
||||
class Heap {
|
||||
a = [];
|
||||
@@ -154,31 +171,39 @@ if (process.argv[1] && fileURLToPath(import.meta.url) === process.argv[1]) {
|
||||
const verdict = sweepOracle(graph, pairs, { snap: snapToGraph, astar: routeDirectionSplit, oracle: dijkstra });
|
||||
console.log(`oracle: compared=${pairs.length} snap-miss=${missing.snap} routed=${verdict.routed} unreachable=${verdict.unreachable} suboptimal=${verdict.suboptimal} oracle-mismatch=${verdict.oracleMismatch} class-break=${verdict.classBreaks} pass=${verdict.pass}`);
|
||||
if (!verdict.pass) { console.error(verdict.rows.filter(r => !['pass', 'unreachable'].includes(r.verdict))); process.exitCode = 1; }
|
||||
globalThis.__altControlSettled = { forward: 0, backward: 0 };
|
||||
const control = (await instrumentedShipped()).routeAstar;
|
||||
const extended = generateCrossMetroPairs(graph.bbox, { count: 100, seed: 0x08a1, minPairKm: 12, haversineM });
|
||||
const warm = (fn) => { const a = process.hrtime.bigint(); fn(); return Number(process.hrtime.bigint() - a) / 1e6; };
|
||||
console.log(`warm-up ms: experimental=${warm(() => routeDirectionSplit(graph, 0, 1)).toFixed(3)} shipped=${warm(() => routeAstar(graph, 0, 1)).toFixed(3)}`);
|
||||
const times = [[], []], counts = [0, 0], misses = { snap: 0, unreachable: 0 }, active = [0, 0];
|
||||
const warmExp = warm(() => routeDirectionSplit(graph, 0, 1));
|
||||
const warmShipped = warm(() => routeAstar(graph, 0, 1));
|
||||
const warmClone = warm(() => control(graph, 0, 1));
|
||||
console.log(`warm-up ms (unmeasured): experimental=${warmExp.toFixed(3)} original-shipped=${warmShipped.toFixed(3)} instrumented-clone=${warmClone.toFixed(3)}`);
|
||||
globalThis.__altControlSettled = { forward: 0, backward: 0 };
|
||||
const times = [[], [], []], counts = [0, 0], misses = { snap: 0, unreachable: 0 }, active = [0, 0];
|
||||
for (let round = 0; round < 2; round++) for (let i = 0; i < extended.length; i++) {
|
||||
const pair = extended[i], s = snapToGraph(graph, pair.origin), t = snapToGraph(graph, pair.destination);
|
||||
if (!s || !t) { if (round === 0) misses.snap++; continue; }
|
||||
const results = [];
|
||||
for (const k of ((i + round) % 2 ? [1, 0] : [0, 1])) {
|
||||
const st = process.hrtime.bigint(), result = k === 0 ? routeDirectionSplit(graph, s.node, t.node) : routeAstar(graph, s.node, t.node);
|
||||
for (const k of ((i + round) % 2 ? [2, 1, 0] : [0, 1, 2])) {
|
||||
const st = process.hrtime.bigint(), result = k === 0 ? routeDirectionSplit(graph, s.node, t.node) : k === 1 ? control(graph, s.node, t.node) : routeAstar(graph, s.node, t.node);
|
||||
const ms = Number(process.hrtime.bigint() - st) / 1e6; results[k] = { result, ms };
|
||||
}
|
||||
if (results[0].result === null || results[1].result === null) {
|
||||
if (results[0].result !== results[1].result) throw Error(`paired reachability mismatch ${pair.pairId}`);
|
||||
if (results[0].result === null || results[1].result === null || results[2].result === null) {
|
||||
if (results[0].result !== results[1].result || results[0].result !== results[2].result) throw Error(`paired reachability mismatch ${pair.pairId}`);
|
||||
if (round === 0) misses.unreachable++; continue;
|
||||
}
|
||||
if (Math.abs(results[0].result.seconds - results[1].result.seconds) > 1e-6) throw Error(`paired cost mismatch ${pair.pairId}`);
|
||||
for (let k = 0; k < 2; k++) times[k].push(results[k].ms);
|
||||
if (Math.abs(results[0].result.seconds - results[1].result.seconds) > 1e-6 || Math.abs(results[1].result.seconds - results[2].result.seconds) > 1e-6) throw Error(`paired cost mismatch ${pair.pairId}`);
|
||||
for (let k = 0; k < 3; k++) times[k].push(results[k].ms);
|
||||
counts[0] += results[0].result.expansionsForward + results[0].result.expansionsBackward;
|
||||
active[0] += results[0].result.activeTo; active[1] += results[0].result.activeFrom;
|
||||
}
|
||||
const stats = a => { a.sort((x, y) => x - y); return `n=${a.length} median=${a[Math.floor(a.length / 2)].toFixed(3)} mean=${(a.reduce((x,y) => x + y,0)/a.length).toFixed(3)} p95=${a[Math.ceil(a.length * .95)-1].toFixed(3)} ms`; };
|
||||
console.log(`extended snap-miss=${misses.snap} unreachable=${misses.unreachable} (outside routed p95), 2 alternating rounds`);
|
||||
console.log(`experimental: ${stats(times[0])} expansions=${counts[0]} active-to/from=${active.join('/')}`);
|
||||
console.log(`shipped: ${stats(times[1])}; shipped expansions and expansion ratio NOT MEASURED (no production instrumentation)`);
|
||||
counts[1] = globalThis.__altControlSettled.forward + globalThis.__altControlSettled.backward;
|
||||
console.log(`shipped isolated instrumented clone: ${stats(times[1])} expansions=${counts[1]} forward/backward=${globalThis.__altControlSettled.forward}/${globalThis.__altControlSettled.backward}; experimental/control expansion ratio=${(counts[0]/counts[1]).toFixed(3)}`);
|
||||
console.log(`original shipped routeAstar (paired unmodified haversine-only control): ${stats(times[2])}`);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
Reference in New Issue
Block a user