diff --git a/CHANGELOG.md b/CHANGELOG.md index 6235492..5e15e7e 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -7,6 +7,22 @@ SPDX-License-Identifier: Apache-2.0 ## Unreleased +## 0.3.0 + +Add the `@workit/core/time-policy` planning subpath for declared async time +policy analysis. The root import remains unchanged. + +- Add `planTimePolicy()` for conservative upper-bound planning across attempt, + series, parallel, retry, hedge, timeout, and deadline policy trees. +- Add `estimateRetry()` and `estimateHedge()` helper planners aligned with the + runtime retry delay and hedge stagger contracts. +- Add bounded correctness evidence for retry/deadline planning, the finite + time-policy cost model, and nested composition rules. +- Add package-consumer coverage for the new subpath across ESM, CommonJS, and + strict TypeScript fixtures. +- Document that the planner analyzes declared policy bounds before execution; it + does not run task bodies or prove wall-clock scheduler behavior. + ## 0.2.0 Add the core ownership and evidence foundation as explicit `@workit/core` diff --git a/README.md b/README.md index f653e2d..d53369b 100644 --- a/README.md +++ b/README.md @@ -67,7 +67,7 @@ cite the software release you used: title = {WorkIt: A TypeScript Structured Concurrency Runtime for Node.js Server Runtimes}, year = {2026}, url = {https://github.com/WorkRuntime/workit}, - version = {0.2.0}, + version = {0.3.0}, license = {Apache-2.0} } ``` @@ -101,6 +101,7 @@ Stable consumer paths for this release line: @workit/core/otel @workit/core/replay @workit/core/resources +@workit/core/time-policy @workit/core/worker ``` diff --git a/package-lock.json b/package-lock.json index e7a2913..5251097 100644 --- a/package-lock.json +++ b/package-lock.json @@ -1,12 +1,12 @@ { "name": "workit", - "version": "0.2.0", + "version": "0.3.0", "lockfileVersion": 3, "requires": true, "packages": { "": { "name": "workit", - "version": "0.2.0", + "version": "0.3.0", "license": "Apache-2.0", "workspaces": [ "packages/core" @@ -3453,7 +3453,7 @@ }, "packages/core": { "name": "@workit/core", - "version": "0.2.0", + "version": "0.3.0", "license": "Apache-2.0", "devDependencies": { "@opentelemetry/api": "1.9.1", diff --git a/package.json b/package.json index a3ef92e..9b18ac5 100644 --- a/package.json +++ b/package.json @@ -1,6 +1,6 @@ { "name": "workit", - "version": "0.2.0", + "version": "0.3.0", "private": true, "description": "WorkIt monorepo.", "type": "module", diff --git a/packages/core/README.md b/packages/core/README.md index 69fe57f..715ddb0 100644 --- a/packages/core/README.md +++ b/packages/core/README.md @@ -290,6 +290,36 @@ ownership helpers live behind explicit subpaths. | Verify receipts and caller-provided protocol specs | `@workit/core/analysis` | bounded verification over supplied evidence, not whole-program analysis | | Record explicit terminal activity boundaries | `@workit/core/activity` | completed activity replay, not in-flight workflow recovery | | Compose lazy, shared, and scope-owned resources | `@workit/core/resources` | cleanup ownership through WorkIt scopes, not automatic resource detection | +| Plan declared retry, hedge, timeout, deadline, series, and parallel time bounds | `@workit/core/time-policy` | conservative planning over declared policies, not wall-clock execution proof | + +### Time Policy Planning + +`@workit/core/time-policy` lets callers inspect declared time policies before +running task bodies. It is useful for admission checks, review tools, and +receipt analysis that need a conservative bound for composed retry, hedge, +timeout, and deadline policies. + +```ts +import { planTimePolicy } from "@workit/core/time-policy"; + +const plan = planTimePolicy({ + type: "timeout", + timeout: "250ms", + policy: { + type: "retry", + attempt: { type: "attempt", duration: "100ms" }, + retry: { times: 4, initialDelay: "50ms", backoff: "fixed", jitter: false }, + }, +}); + +if (plan.warnings.some((warning) => warning.code === "retry_exceeds_timeout")) { + reviewTimeBudget(plan); +} +``` + +The planner does not execute JavaScript, inspect provider latency, or guarantee +operating-system timer precision. Runtime cancellation still depends on task +bodies and providers observing `ctx.signal`. ## Common Use Cases @@ -455,9 +485,9 @@ thresholds, not exact milliseconds. | Evidence | Current result | |---|---:| -| Unit tests | 299 passing | +| Unit tests | 319 passing | | Coverage gate | 100% statements, branches, functions, lines | -| Evidence proof files | 14 passing | +| Evidence proof files | 17 passing | | Runtime dependencies | 0 | | Article benchmark suite | 19/19 passing | | Core group import | 14,175 B minified / 4,835 B gzip | @@ -636,7 +666,7 @@ cite the software release you used: title = {WorkIt: A TypeScript Structured Concurrency Runtime for Node.js Server Runtimes}, year = {2026}, url = {https://github.com/WorkRuntime/workit}, - version = {0.2.0}, + version = {0.3.0}, license = {Apache-2.0} } ``` diff --git a/packages/core/evidence/claims.json b/packages/core/evidence/claims.json index 89f8098..2c05f71 100644 --- a/packages/core/evidence/claims.json +++ b/packages/core/evidence/claims.json @@ -137,6 +137,26 @@ "expectedInvariant": "unbounded retry counts are rejected at the policy boundary", "limitations": "The cap prevents accidental huge retry policies; application-level retry budgets may be stricter." }, + { + "id": "CORR-009", + "title": "time-policy planner computes retry upper bounds", + "class": "correctness", + "status": "proven", + "proof": "tests/evidence/correctness/time-policy-planner.mjs", + "command": "npm run test:evidence", + "expectedInvariant": "retry upper bound includes attempt duration and delays between failed attempts only", + "limitations": "The planner computes declared policy bounds before execution; it does not run user task bodies." + }, + { + "id": "CORR-010", + "title": "time-policy planner reports infeasible deadline", + "class": "correctness", + "status": "proven", + "proof": "tests/evidence/correctness/time-policy-planner.mjs", + "command": "npm run test:evidence", + "expectedInvariant": "deadline planning returns invalid before runtime execution when policy cannot fit", + "limitations": "Deadline feasibility is computed from the supplied clock and policy; applications remain responsible for accurate external deadlines." + }, { "id": "CORR-007", "title": "receipt analysis detects leaked owned work", @@ -177,6 +197,16 @@ "expectedInvariant": "for linear, lazy, and shared resources, every terminal modeled scope releases exactly the resources it acquired", "limitations": "This is a bounded model for WorkIt resource helper contracts, not a proof over arbitrary JavaScript programs or external resources." }, + { + "id": "CORR-016", + "title": "bounded time-policy model preserves cost upper-bound invariant", + "class": "correctness", + "status": "proven", + "proof": "tests/evidence/correctness/formal-time-policy-model.mjs", + "command": "npm run test:evidence", + "expectedInvariant": "for generated bounded policies, planTimePolicy returns an upper bound that dominates the modeled critical path cost", + "limitations": "This is a bounded executable model for WorkIt time-policy planning, not a proof over arbitrary JavaScript, wall-clock scheduling, timer precision, event-loop stalls, provider behavior, jitter, or dynamic backoff functions." + }, { "id": "CORR-017", "title": "source protocol analysis detects missing ownership edges", @@ -187,6 +217,16 @@ "expectedInvariant": "bounded source protocol specs pass when WorkIt ownership edges are present and fail with stable findings when ownership edges are missing", "limitations": "This verifies caller-provided protocol specifications, not arbitrary TypeScript or JavaScript source." }, + { + "id": "CORR-021", + "title": "nested time-policy planner preserves recursive composition bounds", + "class": "correctness", + "status": "proven", + "proof": "tests/evidence/correctness/nested-time-policy-composition.mjs", + "command": "npm run test:evidence", + "expectedInvariant": "generated nested policies match the recursive model for upper bounds, attempts, parallel work, truncation limits, and typed timeout/deadline warnings", + "limitations": "This is a bounded executable proof over generated nested policy trees. It is not a theorem over arbitrary TypeScript programs, wall-clock scheduling, provider latency, or completed mechanized proof." + }, { "id": "SEC-001", "title": "worker offload rejects remote and executable URL schemes", diff --git a/packages/core/evidence/formal-time-policy-model.json b/packages/core/evidence/formal-time-policy-model.json new file mode 100644 index 0000000..a58eaad --- /dev/null +++ b/packages/core/evidence/formal-time-policy-model.json @@ -0,0 +1,40 @@ +{ + "author": "Admilson B. F. Cossa", + "spdxLicense": "Apache-2.0", + "artifact": "workit-bounded-time-policy-model", + "version": 1, + "model": { + "entities": ["time_policy", "attempt", "retry", "hedge", "timeout", "deadline", "composition"], + "policyForms": ["attempt", "series", "parallel", "retry", "hedge", "timeout", "deadline"], + "costSemantics": [ + "attempt_contributes_declared_duration", + "series_sums_child_critical_paths", + "parallel_uses_max_child_critical_path_and_sums_parallel_work", + "retry_repeats_attempt_and_adds_delays_between_failed_attempts", + "hedge_counts_staggered_duplicate_attempts", + "timeout_truncates_critical_path_to_limit", + "deadline_marks_policy_invalid_when_inner_cost_exceeds_remaining_time" + ], + "invariants": [ + "planner_upper_bound_dominates_modeled_cost", + "planner_attempt_count_matches_modeled_attempts", + "planner_parallel_work_matches_modeled_work", + "timeout_and_deadline_costs_do_not_exceed_declared_limits", + "infeasible_deadline_reports_typed_warning" + ] + }, + "bounds": { + "maxDepth": 3, + "maxGeneratedPolicies": 640, + "durationsMs": [0, 1, 5, 10, 25], + "retryTimes": [1, 2, 3], + "delaysMs": [0, 1, 5], + "hedgeMax": [1, 2, 3], + "limitsMs": [1, 10, 30] + }, + "limitations": [ + "This is a bounded executable model for WorkIt time-policy planning, not a proof over arbitrary JavaScript or wall-clock scheduling.", + "The model checks fixed retry backoff without jitter or dynamic backoff functions.", + "Timer precision, event-loop stalls, provider behavior, and operating-system scheduling are outside this model." + ] +} diff --git a/packages/core/evidence/nested-time-policy-composition.json b/packages/core/evidence/nested-time-policy-composition.json new file mode 100644 index 0000000..a54cd50 --- /dev/null +++ b/packages/core/evidence/nested-time-policy-composition.json @@ -0,0 +1,172 @@ +{ + "author": "Admilson B. F. Cossa", + "spdxLicense": "Apache-2.0", + "artifact": "workit-nested-time-policy-composition", + "version": 1, + "status": "bounded_nested_composition_proof", + "publicApi": "@workit/core/time-policy", + "planner": "planTimePolicy", + "compositionRules": [ + { + "policy": "series", + "upperBoundRule": "sum(child.upperBoundMs)", + "workRule": "sum(child.parallelWorkMs)", + "attemptRule": "sum(child.attempts)" + }, + { + "policy": "parallel", + "upperBoundRule": "max(child.upperBoundMs)", + "workRule": "sum(child.parallelWorkMs)", + "attemptRule": "sum(child.attempts)" + }, + { + "policy": "retry", + "upperBoundRule": "attempt.upperBoundMs * times + sum(delay_between_failed_attempts)", + "workRule": "attempt.parallelWorkMs * times", + "attemptRule": "attempt.attempts * times" + }, + { + "policy": "hedge", + "upperBoundRule": "attempt.upperBoundMs + afterMs * (max - 1)", + "workRule": "attempt.parallelWorkMs * max", + "attemptRule": "attempt.attempts * max" + }, + { + "policy": "timeout", + "upperBoundRule": "min(inner.upperBoundMs, timeoutMs)", + "workRule": "inner.parallelWorkMs", + "attemptRule": "inner.attempts" + }, + { + "policy": "deadline", + "upperBoundRule": "min(inner.upperBoundMs, max(0, deadlineAt - now))", + "workRule": "inner.parallelWorkMs", + "attemptRule": "inner.attempts" + } + ], + "bounds": { + "maxCompositionRounds": 5, + "maxTreeDepth": 6, + "maxGeneratedPolicies": 1800, + "durationsMs": [1, 2, 5, 8], + "retryTimes": [1, 2, 3], + "delaysMs": [0, 1, 3], + "hedgeMax": [1, 2, 3], + "limitsMs": [3, 8, 13, 21] + }, + "invariants": [ + "nested_planner_upper_bound_matches_recursive_model", + "nested_planner_attempt_count_matches_recursive_model", + "nested_planner_parallel_work_matches_recursive_model", + "outer_timeout_and_deadline_never_exceed_declared_limit", + "nested_retry_or_hedge_truncation_reports_typed_warning", + "named_review_cases_match_expected_public_plan" + ], + "reviewCases": [ + { + "name": "series_with_parallel_branch", + "policy": { + "type": "series", + "policies": [ + { "type": "attempt", "duration": 5 }, + { + "type": "parallel", + "policies": [ + { "type": "attempt", "duration": 8 }, + { "type": "attempt", "duration": 2 } + ] + } + ] + }, + "expected": { + "valid": true, + "upperBoundMs": 13, + "criticalPathMs": 13, + "parallelWorkMs": 15, + "attempts": 3, + "warnings": [] + } + }, + { + "name": "timeout_truncates_retry_inside_series", + "policy": { + "type": "timeout", + "timeout": 10, + "policy": { + "type": "series", + "policies": [ + { + "type": "retry", + "attempt": { "type": "attempt", "duration": 4 }, + "retry": { "times": 3, "initialDelay": 2, "backoff": "fixed", "jitter": false } + }, + { "type": "attempt", "duration": 1 } + ] + } + }, + "expected": { + "valid": true, + "upperBoundMs": 10, + "criticalPathMs": 10, + "parallelWorkMs": 13, + "attempts": 4, + "warnings": ["retry_exceeds_timeout"] + } + }, + { + "name": "deadline_rejects_parallel_hedge_plan", + "policy": { + "type": "deadline", + "now": 0, + "deadlineAt": 7, + "policy": { + "type": "parallel", + "policies": [ + { + "type": "hedge", + "attempt": { "type": "attempt", "duration": 5 }, + "after": 3, + "max": 2 + }, + { "type": "attempt", "duration": 2 } + ] + } + }, + "expected": { + "valid": false, + "upperBoundMs": 7, + "criticalPathMs": 7, + "parallelWorkMs": 12, + "attempts": 3, + "warnings": ["deadline_infeasible"] + } + }, + { + "name": "timeout_truncates_hedge_budget", + "policy": { + "type": "timeout", + "timeout": 6, + "policy": { + "type": "hedge", + "attempt": { "type": "attempt", "duration": 4 }, + "after": 4, + "max": 3 + } + }, + "expected": { + "valid": true, + "upperBoundMs": 6, + "criticalPathMs": 6, + "parallelWorkMs": 12, + "attempts": 3, + "warnings": ["hedge_exceeds_timeout"] + } + } + ], + "limitations": [ + "This is a bounded executable proof over generated nested policy trees, not a theorem over arbitrary TypeScript programs.", + "The proof models fixed retry backoff without jitter or dynamic backoff functions.", + "Wall-clock scheduler behavior, provider latency, timer precision, and event-loop stalls are outside this model.", + "This artifact strengthens nested composition evidence but does not claim completed mechanized proof." + ] +} diff --git a/packages/core/package.json b/packages/core/package.json index 90d3033..2f5b7b9 100644 --- a/packages/core/package.json +++ b/packages/core/package.json @@ -1,6 +1,6 @@ { "name": "@workit/core", - "version": "0.2.0", + "version": "0.3.0", "description": "Structured concurrency runtime for TypeScript: owned async work, cancellation, budgets, retries, timeouts, worker offload, scopes.", "keywords": [ "structured-concurrency", @@ -115,6 +115,11 @@ "import": "./dist/resources/index.js", "require": "./dist-cjs/resources/index.cjs" }, + "./time-policy": { + "types": "./dist/time-policy/index.d.ts", + "import": "./dist/time-policy/index.js", + "require": "./dist-cjs/time-policy/index.cjs" + }, "./worker": { "types": "./dist/worker/index.d.ts", "node": { diff --git a/packages/core/scripts/build-cjs.mjs b/packages/core/scripts/build-cjs.mjs index 41ddaeb..6ca0dee 100644 --- a/packages/core/scripts/build-cjs.mjs +++ b/packages/core/scripts/build-cjs.mjs @@ -24,6 +24,7 @@ const ENTRIES = [ { entry: "dist/otel/index.js", outfile: "dist-cjs/otel/index.cjs" }, { entry: "dist/replay/index.js", outfile: "dist-cjs/replay/index.cjs" }, { entry: "dist/resources/index.js", outfile: "dist-cjs/resources/index.cjs" }, + { entry: "dist/time-policy/index.js", outfile: "dist-cjs/time-policy/index.cjs" }, ]; await rm("dist-cjs", { recursive: true, force: true }); diff --git a/packages/core/scripts/check-api-surface.mjs b/packages/core/scripts/check-api-surface.mjs index 44b118d..ecde1d5 100644 --- a/packages/core/scripts/check-api-surface.mjs +++ b/packages/core/scripts/check-api-surface.mjs @@ -26,6 +26,7 @@ const EXPECTED_EXPORT_MAP = [ "./otel", "./replay", "./resources", + "./time-policy", "./worker", ]; @@ -104,6 +105,11 @@ const EXPECTED_RUNTIME_EXPORTS = { "bracketShared", "scopeAcquire", ], + "./time-policy": [ + "estimateHedge", + "estimateRetry", + "planTimePolicy", + ], "./worker": [ "offload", ], @@ -121,6 +127,7 @@ const EXPECTED_EXPORT_CONDITIONS = { "./otel": ["import", "require", "types"], "./replay": ["import", "require", "types"], "./resources": ["import", "require", "types"], + "./time-policy": ["import", "require", "types"], "./worker": ["default", "node", "types"], }; @@ -136,6 +143,7 @@ const MODULE_PATHS = { "./otel": "../dist/otel/index.js", "./replay": "../dist/replay/index.js", "./resources": "../dist/resources/index.js", + "./time-policy": "../dist/time-policy/index.js", "./worker": "../dist/worker/index.js", }; @@ -150,6 +158,7 @@ const CJS_MODULE_PATHS = { "./observability": "../dist-cjs/observability/index.cjs", "./replay": "../dist-cjs/replay/index.cjs", "./resources": "../dist-cjs/resources/index.cjs", + "./time-policy": "../dist-cjs/time-policy/index.cjs", }; const packageJson = JSON.parse(await readFile(new URL("../package.json", import.meta.url), "utf8")); diff --git a/packages/core/scripts/check-package-consumer.mjs b/packages/core/scripts/check-package-consumer.mjs index 804763b..1d44b33 100644 --- a/packages/core/scripts/check-package-consumer.mjs +++ b/packages/core/scripts/check-package-consumer.mjs @@ -113,6 +113,7 @@ try { import { attachOpenTelemetry } from "@workit/core/otel"; import { buildReceipt, redactReceipt } from "@workit/core/replay"; import { bracketLazy } from "@workit/core/resources"; + import { planTimePolicy } from "@workit/core/time-policy"; import { offload } from "@workit/core/worker"; const result = await run.all([async () => "sdk", async () => "ok"]); @@ -135,6 +136,15 @@ try { ...receipt, events: [{ type: "task:progress", taskId: "consumer-task", at: 1, data: { token: "secret" } }] }); + const timePlan = planTimePolicy({ + type: "timeout", + timeout: 250, + policy: { + type: "retry", + attempt: { type: "attempt", duration: 100 }, + retry: { times: 4, initialDelay: 50, backoff: "fixed", jitter: false }, + }, + }); const ledger = createMemoryReceiptLedger(); const ledgerRecord = await ledger.append(receipt); const analysis = analyzeReceipt(receipt); @@ -192,6 +202,7 @@ try { if (streamed.join(":") !== "X") throw new Error("ai stream helper failed"); if (receipt.terminal.outcome !== "completed") throw new Error("replay receipt import failed"); if (JSON.stringify(redacted).includes("secret")) throw new Error("replay redaction failed"); + if (timePlan.upperBoundMs !== 250 || !timePlan.warnings.some((warning) => warning.code === "retry_exceeds_timeout")) throw new Error("time-policy import failed"); if (ledgerRecord.receiptId !== "consumer-receipt") throw new Error("ledger import failed"); if (analysis.status !== "pass") throw new Error("analysis import failed"); if (activityFirst !== "activity-ok" || activitySecond !== "activity-ok" || activityRuns !== 1) throw new Error("activity import failed"); @@ -213,6 +224,7 @@ try { const { createMemoryReceiptLedger } = require("@workit/core/ledger"); const { buildReceipt } = require("@workit/core/replay"); const { bracketShared } = require("@workit/core/resources"); + const { estimateRetry } = require("@workit/core/time-policy"); (async () => { const values = await run.all([async () => "cjs", async () => "ok"]); @@ -231,6 +243,10 @@ try { const ledger = createMemoryReceiptLedger(); const record = await ledger.append(receipt); const analysis = verifyReceipt(receipt); + const retryPlan = estimateRetry({ + attempt: { type: "attempt", duration: 100 }, + retry: { times: 3, initialDelay: 50, backoff: "fixed", jitter: false }, + }); const activityStore = createMemoryActivityStore(); const activity = await runActivity( activityStore, @@ -251,6 +267,7 @@ try { if (receipt.terminal.outcome !== "completed") throw new Error("CommonJS replay import failed"); if (record.receiptId !== receipt.receiptId) throw new Error("CommonJS ledger import failed"); if (analysis.status !== "pass") throw new Error("CommonJS analysis import failed"); + if (retryPlan.upperBoundMs !== 400) throw new Error("CommonJS time-policy import failed"); if (activity !== "activity-cjs-ok") throw new Error("CommonJS activity import failed"); if (resource !== "resource-cjs-ok" || released !== 1) throw new Error("CommonJS resources import failed"); })().catch((err) => { @@ -298,6 +315,7 @@ try { import { createMemoryReceiptLedger, type ReceiptLedger } from "@workit/core/ledger"; import { buildReceipt, type WorkItReceipt } from "@workit/core/replay"; import { bracketShared, scopeAcquire, type ResourceRelease } from "@workit/core/resources"; + import { planTimePolicy, type TimePlan, type TimePolicy } from "@workit/core/time-policy"; const RequestKey = createContextKey<{ requestId: string }>("request"); @@ -328,6 +346,13 @@ try { const ledger: ReceiptLedger = createMemoryReceiptLedger(); const ledgerRecord = await ledger.append(receipt); const analysis: AnalysisReport = verifyReceipt(receipt); + const declaredPolicy: TimePolicy = { + type: "deadline", + now: 1_000, + deadlineAt: 1_050, + policy: { type: "attempt", duration: 100 }, + }; + const timePlan: TimePlan = planTimePolicy(declaredPolicy); const activityStore: ActivityStore = createMemoryActivityStore(); const activityValue: string = await group(async (task) => task(runActivity( activityStore, @@ -354,6 +379,7 @@ try { if (value !== "strict") throw new Error("context inference failed"); if (ledgerRecord.receiptId !== receipt.receiptId) throw new Error("ledger typing failed"); if (analysis.status !== "pass") throw new Error("analysis typing failed"); + if (timePlan.valid !== false || timePlan.upperBoundMs !== 50) throw new Error("time-policy typing failed"); if (activityValue !== "strict-activity-ok") throw new Error("activity typing failed"); if (strictResource !== "strict-resource" || strictResourceReleased !== 1) throw new Error("resource typing failed"); if (embedded.mode !== "fail") throw new Error("unexpected embedAll mode"); diff --git a/packages/core/src/time-policy/index.ts b/packages/core/src/time-policy/index.ts new file mode 100644 index 0000000..cf62542 --- /dev/null +++ b/packages/core/src/time-policy/index.ts @@ -0,0 +1,334 @@ +/** + * Declarative time policy planner for WorkIt runtime compositions. + * + * @author Admilson B. F. Cossa + * SPDX-License-Identifier: Apache-2.0 + * + * The planner computes conservative upper bounds for retry, timeout, deadline, + * hedge, series, and parallel compositions. It never runs task bodies. + */ + +import type { Duration, RetryOpts } from "../types/index.js"; +import { parseDuration } from "../engine/duration.js"; +import { normalizeRetry } from "../engine/retry.js"; + +/** Leaf policy representing one bounded task attempt. */ +export interface AttemptTimePolicy { + readonly type: "attempt"; + readonly duration: Duration; + readonly label?: string; +} + +/** Sequential composition: every child policy must settle in order. */ +export interface SeriesTimePolicy { + readonly type: "series"; + readonly policies: readonly TimePolicy[]; +} + +/** Parallel composition: all child policies are active together. */ +export interface ParallelTimePolicy { + readonly type: "parallel"; + readonly policies: readonly TimePolicy[]; +} + +/** Retry composition aligned with `run.retry` delay semantics. */ +export interface RetryTimePolicy { + readonly type: "retry"; + readonly attempt: TimePolicy; + readonly retry: number | RetryOpts; +} + +/** Hedge composition aligned with `run.hedge` stagger semantics. */ +export interface HedgeTimePolicy { + readonly type: "hedge"; + readonly attempt: TimePolicy; + readonly after: Duration; + readonly max: number; +} + +/** Timeout composition that can truncate an inner policy. */ +export interface TimeoutTimePolicy { + readonly type: "timeout"; + readonly timeout: Duration; + readonly policy: TimePolicy; +} + +/** Deadline composition evaluated against an explicit or current clock. */ +export interface DeadlineTimePolicy { + readonly type: "deadline"; + readonly deadlineAt: number | Date; + readonly now?: number; + readonly policy: TimePolicy; +} + +/** Supported declarative time policy tree. */ +export type TimePolicy = + | AttemptTimePolicy + | SeriesTimePolicy + | ParallelTimePolicy + | RetryTimePolicy + | HedgeTimePolicy + | TimeoutTimePolicy + | DeadlineTimePolicy; + +/** Stable warning codes returned by the planner. */ +export type TimePlanWarningCode = + | "deadline_infeasible" + | "dynamic_backoff_upper_bound" + | "empty_composition" + | "hedge_exceeds_timeout" + | "jitter_upper_bound" + | "retry_exceeds_timeout" + | "time_exceeds_timeout"; + +/** One safe, typed planning warning. */ +export interface TimePlanWarning { + readonly code: TimePlanWarningCode; + readonly message: string; + readonly estimatedMs?: number; + readonly limitMs?: number; +} + +/** Planning result for one policy tree. */ +export interface TimePlan { + readonly valid: boolean; + readonly upperBoundMs: number; + readonly criticalPathMs: number; + readonly parallelWorkMs: number; + readonly attempts: number; + readonly warnings: readonly TimePlanWarning[]; +} + +const MAX_POLICY_DEPTH = 64; + +/** Plans a declarative time policy without executing user task bodies. */ +export function planTimePolicy(policy: TimePolicy): TimePlan { + return plan(policy, 0); +} + +/** Computes retry upper bounds using WorkIt's runtime retry semantics. */ +export function estimateRetry(policy: Pick): TimePlan { + return estimateRetryAtDepth(policy, 1); +} + +/** Computes hedge upper bounds using WorkIt's staggered duplicate attempts. */ +export function estimateHedge(policy: Pick): TimePlan { + return estimateHedgeAtDepth(policy, 1); +} + +function estimateRetryAtDepth(policy: Pick, depth: number): TimePlan { + const attemptPlan = plan(policy.attempt, depth); + const retry = normalizeRetry(policy.retry); + const warnings: TimePlanWarning[] = [...attemptPlan.warnings]; + let delayMs = 0; + + for (let attempt = 1; attempt < retry.times; attempt++) { + const plannedDelay = estimateRetryDelay(attempt, retry); + delayMs += plannedDelay.delayMs; + if (plannedDelay.warning !== undefined) warnings.push(plannedDelay.warning); + } + + if (retry.jitter) { + warnings.push({ + code: "jitter_upper_bound", + message: "retry jitter is planned with the maximum non-jittered delay as an upper bound", + }); + } + + const upperBoundMs = attemptPlan.upperBoundMs * retry.times + delayMs; + return { + valid: attemptPlan.valid, + upperBoundMs, + criticalPathMs: upperBoundMs, + parallelWorkMs: attemptPlan.parallelWorkMs * retry.times, + attempts: attemptPlan.attempts * retry.times, + warnings, + }; +} + +function estimateHedgeAtDepth(policy: Pick, depth: number): TimePlan { + if (!Number.isInteger(policy.max) || policy.max < 1) throw new RangeError("hedge max must be a positive integer"); + + const attemptPlan = plan(policy.attempt, depth); + const afterMs = parseDuration(policy.after); + const upperBoundMs = attemptPlan.upperBoundMs + afterMs * (policy.max - 1); + + return { + valid: attemptPlan.valid, + upperBoundMs, + criticalPathMs: upperBoundMs, + parallelWorkMs: attemptPlan.parallelWorkMs * policy.max, + attempts: attemptPlan.attempts * policy.max, + warnings: attemptPlan.warnings, + }; +} + +function plan(policy: TimePolicy, depth: number): TimePlan { + if (depth > MAX_POLICY_DEPTH) throw new RangeError("time policy depth exceeded"); + + switch (policy.type) { + case "attempt": + return leafPlan(parseDuration(policy.duration)); + case "series": + return combineSeries(policy.policies, depth); + case "parallel": + return combineParallel(policy.policies, depth); + case "retry": + return estimateRetryAtDepth(policy, depth + 1); + case "hedge": + return estimateHedgeAtDepth(policy, depth + 1); + case "timeout": + return planTimeout(policy, depth); + case "deadline": + return planDeadline(policy, depth); + } +} + +function leafPlan(durationMs: number): TimePlan { + return { + valid: true, + upperBoundMs: durationMs, + criticalPathMs: durationMs, + parallelWorkMs: durationMs, + attempts: 1, + warnings: [], + }; +} + +function combineSeries(policies: readonly TimePolicy[], depth: number): TimePlan { + if (policies.length === 0) return emptyPlan(); + const children = policies.map((child) => plan(child, depth + 1)); + return { + valid: children.every((child) => child.valid), + upperBoundMs: children.reduce((total, child) => total + child.upperBoundMs, 0), + criticalPathMs: children.reduce((total, child) => total + child.criticalPathMs, 0), + parallelWorkMs: children.reduce((total, child) => total + child.parallelWorkMs, 0), + attempts: children.reduce((total, child) => total + child.attempts, 0), + warnings: children.flatMap((child) => child.warnings), + }; +} + +function combineParallel(policies: readonly TimePolicy[], depth: number): TimePlan { + if (policies.length === 0) return emptyPlan(); + const children = policies.map((child) => plan(child, depth + 1)); + return { + valid: children.every((child) => child.valid), + upperBoundMs: Math.max(...children.map((child) => child.upperBoundMs)), + criticalPathMs: Math.max(...children.map((child) => child.criticalPathMs)), + parallelWorkMs: children.reduce((total, child) => total + child.parallelWorkMs, 0), + attempts: children.reduce((total, child) => total + child.attempts, 0), + warnings: children.flatMap((child) => child.warnings), + }; +} + +function emptyPlan(): TimePlan { + return { + valid: true, + upperBoundMs: 0, + criticalPathMs: 0, + parallelWorkMs: 0, + attempts: 0, + warnings: [{ + code: "empty_composition", + message: "empty time composition has zero cost", + }], + }; +} + +function planTimeout(policy: TimeoutTimePolicy, depth: number): TimePlan { + const inner = plan(policy.policy, depth + 1); + const timeoutMs = parseDuration(policy.timeout); + if (inner.upperBoundMs <= timeoutMs) return inner; + + const containedTypes = collectPolicyTypes(policy.policy); + const code = containedTypes.has("retry") + ? "retry_exceeds_timeout" + : containedTypes.has("hedge") + ? "hedge_exceeds_timeout" + : "time_exceeds_timeout"; + + return { + ...inner, + upperBoundMs: timeoutMs, + criticalPathMs: Math.min(inner.criticalPathMs, timeoutMs), + warnings: [ + ...inner.warnings, + { + code, + message: "inner time policy exceeds timeout and will be truncated by runtime cancellation", + estimatedMs: inner.upperBoundMs, + limitMs: timeoutMs, + }, + ], + }; +} + +function planDeadline(policy: DeadlineTimePolicy, depth: number): TimePlan { + const inner = plan(policy.policy, depth + 1); + const deadlineAt = typeof policy.deadlineAt === "number" ? policy.deadlineAt : policy.deadlineAt.getTime(); + const now = policy.now ?? Date.now(); + const remainingMs = Math.max(0, deadlineAt - now); + if (inner.upperBoundMs <= remainingMs) return inner; + + return { + ...inner, + valid: false, + upperBoundMs: remainingMs, + criticalPathMs: Math.min(inner.criticalPathMs, remainingMs), + warnings: [ + ...inner.warnings, + { + code: "deadline_infeasible", + message: "inner time policy cannot fit before the declared deadline", + estimatedMs: inner.upperBoundMs, + limitMs: remainingMs, + }, + ], + }; +} + +function collectPolicyTypes(policy: TimePolicy, types = new Set()): Set { + types.add(policy.type); + switch (policy.type) { + case "series": + case "parallel": + for (const child of policy.policies) collectPolicyTypes(child, types); + return types; + case "retry": + case "hedge": + collectPolicyTypes(policy.attempt, types); + return types; + case "timeout": + case "deadline": + collectPolicyTypes(policy.policy, types); + return types; + case "attempt": + return types; + } +} + +function estimateRetryDelay( + attempt: number, + policy: ReturnType, +): { delayMs: number; warning?: TimePlanWarning } { + const initialMs = parseDuration(policy.initialDelay); + const maxMs = parseDuration(policy.maxDelay); + if (typeof policy.backoff === "function") { + return { + delayMs: maxMs, + warning: { + code: "dynamic_backoff_upper_bound", + message: "dynamic retry backoff functions are not executed by the planner; maxDelay is used as an upper bound", + estimatedMs: maxMs, + }, + }; + } + + const rawDelay = policy.backoff === "linear" + ? initialMs * attempt + : policy.backoff === "exponential" + ? initialMs * Math.pow(2, attempt - 1) + : initialMs; + + return { delayMs: Math.min(rawDelay, maxMs) }; +} diff --git a/packages/core/tests/evidence/correctness/formal-time-policy-model.mjs b/packages/core/tests/evidence/correctness/formal-time-policy-model.mjs new file mode 100644 index 0000000..5e6ef11 --- /dev/null +++ b/packages/core/tests/evidence/correctness/formal-time-policy-model.mjs @@ -0,0 +1,300 @@ +/** + * Correctness evidence: bounded time-policy cost model. + * + * @author Admilson B. F. Cossa + * SPDX-License-Identifier: Apache-2.0 + * + * This finite model checks that WorkIt's public time-policy planner does not + * underestimate modeled policy cost for bounded retry, hedge, timeout, + * deadline, series, and parallel compositions. + */ + +import { readFile } from "node:fs/promises"; + +import { planTimePolicy } from "../../../dist/time-policy/index.js"; +import { createSuite } from "../harness.mjs"; + +const suite = createSuite("correctness"); +const root = new URL("../../../", import.meta.url); + +await suite.proof( + "CORR-016", + "bounded time-policy model preserves cost upper-bound invariant", + "for generated bounded policies, planTimePolicy returns an upper bound that dominates the modeled critical path cost", + async () => { + const spec = JSON.parse(await readFile(new URL("evidence/formal-time-policy-model.json", root), "utf8")); + const policies = generatePolicies(spec); + const violations = []; + + for (const policy of policies) { + const modeled = modelCost(policy); + const planned = planTimePolicy(policy); + const violation = checkPlan(policy, modeled, planned); + if (violation !== null) violations.push(violation); + } + + return { + ok: spec.author === "Admilson B. F. Cossa" + && spec.spdxLicense === "Apache-2.0" + && spec.model.policyForms.includes("retry") + && spec.model.policyForms.includes("hedge") + && spec.model.invariants.includes("planner_upper_bound_dominates_modeled_cost") + && policies.length > 0 + && policies.length <= spec.bounds.maxGeneratedPolicies + && violations.length === 0, + generatedPolicies: policies.length, + violations, + limitations: spec.limitations, + }; + }, +); + +const summary = suite.summary(); +process.stdout.write(JSON.stringify(summary, null, 2) + "\n"); +process.exit(summary.failed > 0 ? 1 : 0); + +function generatePolicies(spec) { + const bounds = spec.bounds; + const policies = []; + const seen = new Set(); + let previous = bounds.durationsMs.map((duration) => ({ type: "attempt", duration })); + + for (const policy of previous) addPolicy(policies, seen, bounds.maxGeneratedPolicies, policy); + + for (let depth = 1; depth <= bounds.maxDepth; depth++) { + const selected = previous.slice(0, 8); + const next = []; + + for (const left of selected) { + for (const right of selected.slice(0, 4)) { + next.push({ type: "series", policies: [left, right] }); + next.push({ type: "parallel", policies: [left, right] }); + } + } + + for (const child of selected) { + for (const times of bounds.retryTimes) { + for (const delay of bounds.delaysMs) { + next.push({ + type: "retry", + attempt: child, + retry: { times, initialDelay: delay, backoff: "fixed", jitter: false }, + }); + } + } + + for (const max of bounds.hedgeMax) { + for (const after of bounds.delaysMs) { + next.push({ type: "hedge", attempt: child, after, max }); + } + } + + for (const limit of bounds.limitsMs) { + next.push({ type: "timeout", timeout: limit, policy: child }); + next.push({ type: "deadline", now: 0, deadlineAt: limit, policy: child }); + } + } + + for (const policy of next) addPolicy(policies, seen, bounds.maxGeneratedPolicies, policy); + previous = next; + } + + return policies; +} + +function addPolicy(policies, seen, maxGeneratedPolicies, policy) { + if (policies.length >= maxGeneratedPolicies) return; + const key = JSON.stringify(policy); + if (seen.has(key)) return; + seen.add(key); + policies.push(policy); +} + +function modelCost(policy) { + switch (policy.type) { + case "attempt": + return modelLeaf(policy.duration); + case "series": + return modelSeries(policy.policies); + case "parallel": + return modelParallel(policy.policies); + case "retry": + return modelRetry(policy); + case "hedge": + return modelHedge(policy); + case "timeout": + return modelTimeout(policy); + case "deadline": + return modelDeadline(policy); + } +} + +function modelLeaf(durationMs) { + return { + valid: true, + upperBoundMs: durationMs, + criticalPathMs: durationMs, + parallelWorkMs: durationMs, + attempts: 1, + warnings: [], + }; +} + +function modelSeries(policies) { + if (policies.length === 0) return modelEmpty(); + const children = policies.map(modelCost); + return { + valid: children.every((child) => child.valid), + upperBoundMs: sum(children, "upperBoundMs"), + criticalPathMs: sum(children, "criticalPathMs"), + parallelWorkMs: sum(children, "parallelWorkMs"), + attempts: sum(children, "attempts"), + warnings: children.flatMap((child) => child.warnings), + }; +} + +function modelParallel(policies) { + if (policies.length === 0) return modelEmpty(); + const children = policies.map(modelCost); + return { + valid: children.every((child) => child.valid), + upperBoundMs: Math.max(...children.map((child) => child.upperBoundMs)), + criticalPathMs: Math.max(...children.map((child) => child.criticalPathMs)), + parallelWorkMs: sum(children, "parallelWorkMs"), + attempts: sum(children, "attempts"), + warnings: children.flatMap((child) => child.warnings), + }; +} + +function modelRetry(policy) { + const attempt = modelCost(policy.attempt); + const times = policy.retry.times; + const delay = policy.retry.initialDelay * Math.max(0, times - 1); + const upperBoundMs = attempt.upperBoundMs * times + delay; + + return { + valid: attempt.valid, + upperBoundMs, + criticalPathMs: upperBoundMs, + parallelWorkMs: attempt.parallelWorkMs * times, + attempts: attempt.attempts * times, + warnings: attempt.warnings, + }; +} + +function modelHedge(policy) { + const attempt = modelCost(policy.attempt); + const upperBoundMs = attempt.upperBoundMs + policy.after * Math.max(0, policy.max - 1); + + return { + valid: attempt.valid, + upperBoundMs, + criticalPathMs: upperBoundMs, + parallelWorkMs: attempt.parallelWorkMs * policy.max, + attempts: attempt.attempts * policy.max, + warnings: attempt.warnings, + }; +} + +function modelTimeout(policy) { + const inner = modelCost(policy.policy); + if (inner.upperBoundMs <= policy.timeout) return inner; + + return { + ...inner, + upperBoundMs: policy.timeout, + criticalPathMs: Math.min(inner.criticalPathMs, policy.timeout), + warnings: [ + ...inner.warnings, + { + code: timeoutWarningCode(policy.policy), + estimatedMs: inner.upperBoundMs, + limitMs: policy.timeout, + }, + ], + }; +} + +function modelDeadline(policy) { + const inner = modelCost(policy.policy); + const remainingMs = Math.max(0, policy.deadlineAt - policy.now); + if (inner.upperBoundMs <= remainingMs) return inner; + + return { + ...inner, + valid: false, + upperBoundMs: remainingMs, + criticalPathMs: Math.min(inner.criticalPathMs, remainingMs), + warnings: [...inner.warnings, { code: "deadline_infeasible", limitMs: remainingMs }], + }; +} + +function modelEmpty() { + return { + valid: true, + upperBoundMs: 0, + criticalPathMs: 0, + parallelWorkMs: 0, + attempts: 0, + warnings: [{ code: "empty_composition" }], + }; +} + +function checkPlan(policy, modeled, planned) { + if (planned.upperBoundMs < modeled.upperBoundMs) { + return { kind: "underestimated_upper_bound", policy, modeled, planned }; + } + if (planned.criticalPathMs < modeled.criticalPathMs) { + return { kind: "underestimated_critical_path", policy, modeled, planned }; + } + if (planned.parallelWorkMs !== modeled.parallelWorkMs) { + return { kind: "parallel_work_mismatch", policy, modeled, planned }; + } + if (planned.attempts !== modeled.attempts) { + return { kind: "attempt_count_mismatch", policy, modeled, planned }; + } + if (planned.valid !== modeled.valid) { + return { kind: "validity_mismatch", policy, modeled, planned }; + } + + const modeledWarnings = new Set(modeled.warnings.map((warning) => warning.code)); + const plannedWarnings = new Set(planned.warnings.map((warning) => warning.code)); + for (const warning of modeledWarnings) { + if (!plannedWarnings.has(warning)) { + return { kind: "missing_warning", warning, policy, modeled, planned }; + } + } + + return null; +} + +function timeoutWarningCode(policy) { + const types = collectPolicyTypes(policy); + if (types.has("retry")) return "retry_exceeds_timeout"; + if (types.has("hedge")) return "hedge_exceeds_timeout"; + return "time_exceeds_timeout"; +} + +function collectPolicyTypes(policy, types = new Set()) { + types.add(policy.type); + switch (policy.type) { + case "series": + case "parallel": + for (const child of policy.policies) collectPolicyTypes(child, types); + return types; + case "retry": + case "hedge": + collectPolicyTypes(policy.attempt, types); + return types; + case "timeout": + case "deadline": + collectPolicyTypes(policy.policy, types); + return types; + case "attempt": + return types; + } +} + +function sum(items, field) { + return items.reduce((total, item) => total + item[field], 0); +} diff --git a/packages/core/tests/evidence/correctness/nested-time-policy-composition.mjs b/packages/core/tests/evidence/correctness/nested-time-policy-composition.mjs new file mode 100644 index 0000000..c7fd616 --- /dev/null +++ b/packages/core/tests/evidence/correctness/nested-time-policy-composition.mjs @@ -0,0 +1,384 @@ +/** + * Correctness evidence: nested time-policy composition. + * + * @author Admilson B. F. Cossa + * SPDX-License-Identifier: Apache-2.0 + * + * This proof checks recursive composition laws for generated nested + * time-policy trees against the public `planTimePolicy` API. It is bounded + * executable evidence, not a mechanized theorem. + */ + +import { readFile } from "node:fs/promises"; + +import { planTimePolicy } from "../../../dist/time-policy/index.js"; +import { createSuite } from "../harness.mjs"; + +const suite = createSuite("correctness"); +const root = new URL("../../../", import.meta.url); + +await suite.proof( + "CORR-021", + "nested time-policy planner preserves recursive composition bounds", + "generated nested policies match the recursive model for upper bounds, attempts, parallel work, truncation limits, and typed timeout/deadline warnings", + async () => { + const spec = JSON.parse(await readFile(new URL("evidence/nested-time-policy-composition.json", root), "utf8")); + const policies = generateNestedPolicies(spec.bounds); + const reports = policies.map((policy) => checkPolicy(policy)); + const reviewReports = spec.reviewCases.map(checkReviewCase); + const violations = reports.filter((report) => !report.ok); + const reviewViolations = reviewReports.filter((report) => !report.ok); + const maxTreeDepth = maxPolicyDepth(policies); + const timeoutReports = reports.filter((report) => report.policy.type === "timeout"); + const deadlineReports = reports.filter((report) => report.policy.type === "deadline"); + + return { + ok: spec.author === "Admilson B. F. Cossa" + && spec.spdxLicense === "Apache-2.0" + && spec.publicApi === "@workit/core/time-policy" + && spec.planner === "planTimePolicy" + && spec.compositionRules.length === 6 + && spec.invariants.includes("nested_planner_upper_bound_matches_recursive_model") + && spec.invariants.includes("nested_retry_or_hedge_truncation_reports_typed_warning") + && spec.invariants.includes("named_review_cases_match_expected_public_plan") + && spec.reviewCases.length >= 4 + && policies.length > 0 + && policies.length <= spec.bounds.maxGeneratedPolicies + && maxTreeDepth <= spec.bounds.maxTreeDepth + && timeoutReports.some((report) => report.warningCodes.includes("retry_exceeds_timeout")) + && timeoutReports.some((report) => report.warningCodes.includes("hedge_exceeds_timeout")) + && deadlineReports.some((report) => report.warningCodes.includes("deadline_infeasible")) + && spec.limitations.every(hasExplicitLimitation) + && violations.length === 0 + && reviewViolations.length === 0, + generatedPolicies: policies.length, + reviewCases: reviewReports.length, + maxTreeDepth, + timeoutCases: timeoutReports.length, + deadlineCases: deadlineReports.length, + violations, + reviewViolations, + limitations: spec.limitations, + }; + }, +); + +const summary = suite.summary(); +process.stdout.write(JSON.stringify(summary, null, 2) + "\n"); +process.exit(summary.failed > 0 ? 1 : 0); + +function generateNestedPolicies(bounds) { + const policies = []; + const seen = new Set(); + const leaves = bounds.durationsMs.map((duration) => ({ type: "attempt", duration })); + let frontier = leaves; + + for (const policy of leaves) addPolicy(policies, seen, bounds.maxGeneratedPolicies, policy); + + for (let depth = 1; depth <= bounds.maxCompositionRounds; depth++) { + const selected = selectFrontier(frontier, depth); + const next = []; + + for (let index = 0; index < selected.length; index++) { + const left = selected[index]; + const right = selected[(index + depth) % selected.length] ?? selected[0]; + next.push({ type: "series", policies: [left, right] }); + next.push({ type: "parallel", policies: [left, right] }); + } + + for (const child of selected) { + for (const times of bounds.retryTimes) { + for (const delay of bounds.delaysMs) { + next.push({ + type: "retry", + attempt: child, + retry: { times, initialDelay: delay, backoff: "fixed", jitter: false }, + }); + } + } + + for (const max of bounds.hedgeMax) { + for (const after of bounds.delaysMs) { + next.push({ type: "hedge", attempt: child, after, max }); + } + } + + for (const limit of bounds.limitsMs) { + next.push({ type: "timeout", timeout: limit, policy: child }); + next.push({ type: "deadline", now: 0, deadlineAt: limit, policy: child }); + } + } + + for (const policy of next) addPolicy(policies, seen, bounds.maxGeneratedPolicies, policy); + frontier = next; + } + + return policies; +} + +function selectFrontier(frontier, depth) { + const selected = []; + const stride = Math.max(1, Math.floor(frontier.length / 12)); + for (let index = depth % stride; index < frontier.length && selected.length < 16; index += stride) { + selected.push(frontier[index]); + } + return selected.length > 0 ? selected : frontier.slice(0, 16); +} + +function addPolicy(policies, seen, maxGeneratedPolicies, policy) { + if (policies.length >= maxGeneratedPolicies) return; + const key = JSON.stringify(policy); + if (seen.has(key)) return; + seen.add(key); + policies.push(policy); +} + +function checkPolicy(policy) { + const modeled = modelCost(policy); + const planned = planTimePolicy(policy); + const warningCodes = planned.warnings.map((warning) => warning.code); + const failures = []; + + if (planned.upperBoundMs !== modeled.upperBoundMs) failures.push("upper_bound_mismatch"); + if (planned.criticalPathMs !== modeled.criticalPathMs) failures.push("critical_path_mismatch"); + if (planned.parallelWorkMs !== modeled.parallelWorkMs) failures.push("parallel_work_mismatch"); + if (planned.attempts !== modeled.attempts) failures.push("attempt_count_mismatch"); + if (planned.valid !== modeled.valid) failures.push("validity_mismatch"); + + for (const modeledWarning of modeled.warnings) { + if (!warningCodes.includes(modeledWarning.code)) failures.push(`missing_warning:${modeledWarning.code}`); + } + + return { + ok: failures.length === 0, + policy, + modeled, + planned, + warningCodes, + failures, + }; +} + +function checkReviewCase(reviewCase) { + const planned = planTimePolicy(reviewCase.policy); + const warningCodes = planned.warnings.map((warning) => warning.code); + const expected = reviewCase.expected; + const failures = []; + + if (planned.valid !== expected.valid) failures.push("valid"); + if (planned.upperBoundMs !== expected.upperBoundMs) failures.push("upperBoundMs"); + if (planned.criticalPathMs !== expected.criticalPathMs) failures.push("criticalPathMs"); + if (planned.parallelWorkMs !== expected.parallelWorkMs) failures.push("parallelWorkMs"); + if (planned.attempts !== expected.attempts) failures.push("attempts"); + for (const warning of expected.warnings) { + if (!warningCodes.includes(warning)) failures.push(`warning:${warning}`); + } + + return { + ok: failures.length === 0, + name: reviewCase.name, + planned, + expected, + warningCodes, + failures, + }; +} + +function modelCost(policy) { + switch (policy.type) { + case "attempt": + return modelLeaf(policy.duration); + case "series": + return modelSeries(policy.policies); + case "parallel": + return modelParallel(policy.policies); + case "retry": + return modelRetry(policy); + case "hedge": + return modelHedge(policy); + case "timeout": + return modelTimeout(policy); + case "deadline": + return modelDeadline(policy); + } +} + +function modelLeaf(durationMs) { + return { + valid: true, + upperBoundMs: durationMs, + criticalPathMs: durationMs, + parallelWorkMs: durationMs, + attempts: 1, + warnings: [], + }; +} + +function modelSeries(policies) { + if (policies.length === 0) return modelEmpty(); + const children = policies.map(modelCost); + return { + valid: children.every((child) => child.valid), + upperBoundMs: sum(children, "upperBoundMs"), + criticalPathMs: sum(children, "criticalPathMs"), + parallelWorkMs: sum(children, "parallelWorkMs"), + attempts: sum(children, "attempts"), + warnings: children.flatMap((child) => child.warnings), + }; +} + +function modelParallel(policies) { + if (policies.length === 0) return modelEmpty(); + const children = policies.map(modelCost); + return { + valid: children.every((child) => child.valid), + upperBoundMs: Math.max(...children.map((child) => child.upperBoundMs)), + criticalPathMs: Math.max(...children.map((child) => child.criticalPathMs)), + parallelWorkMs: sum(children, "parallelWorkMs"), + attempts: sum(children, "attempts"), + warnings: children.flatMap((child) => child.warnings), + }; +} + +function modelRetry(policy) { + const attempt = modelCost(policy.attempt); + const times = policy.retry.times; + const delay = policy.retry.initialDelay * Math.max(0, times - 1); + const upperBoundMs = attempt.upperBoundMs * times + delay; + + return { + valid: attempt.valid, + upperBoundMs, + criticalPathMs: upperBoundMs, + parallelWorkMs: attempt.parallelWorkMs * times, + attempts: attempt.attempts * times, + warnings: attempt.warnings, + }; +} + +function modelHedge(policy) { + const attempt = modelCost(policy.attempt); + const upperBoundMs = attempt.upperBoundMs + policy.after * Math.max(0, policy.max - 1); + + return { + valid: attempt.valid, + upperBoundMs, + criticalPathMs: upperBoundMs, + parallelWorkMs: attempt.parallelWorkMs * policy.max, + attempts: attempt.attempts * policy.max, + warnings: attempt.warnings, + }; +} + +function modelTimeout(policy) { + const inner = modelCost(policy.policy); + if (inner.upperBoundMs <= policy.timeout) return inner; + + return { + ...inner, + upperBoundMs: policy.timeout, + criticalPathMs: Math.min(inner.criticalPathMs, policy.timeout), + warnings: [ + ...inner.warnings, + { + code: timeoutWarningCode(policy.policy), + estimatedMs: inner.upperBoundMs, + limitMs: policy.timeout, + }, + ], + }; +} + +function modelDeadline(policy) { + const inner = modelCost(policy.policy); + const remainingMs = Math.max(0, policy.deadlineAt - policy.now); + if (inner.upperBoundMs <= remainingMs) return inner; + + return { + ...inner, + valid: false, + upperBoundMs: remainingMs, + criticalPathMs: Math.min(inner.criticalPathMs, remainingMs), + warnings: [ + ...inner.warnings, + { + code: "deadline_infeasible", + estimatedMs: inner.upperBoundMs, + limitMs: remainingMs, + }, + ], + }; +} + +function modelEmpty() { + return { + valid: true, + upperBoundMs: 0, + criticalPathMs: 0, + parallelWorkMs: 0, + attempts: 0, + warnings: [{ code: "empty_composition" }], + }; +} + +function timeoutWarningCode(policy) { + const types = collectPolicyTypes(policy); + if (types.has("retry")) return "retry_exceeds_timeout"; + if (types.has("hedge")) return "hedge_exceeds_timeout"; + return "time_exceeds_timeout"; +} + +function collectPolicyTypes(policy, types = new Set()) { + types.add(policy.type); + switch (policy.type) { + case "series": + case "parallel": + for (const child of policy.policies) collectPolicyTypes(child, types); + return types; + case "retry": + case "hedge": + collectPolicyTypes(policy.attempt, types); + return types; + case "timeout": + case "deadline": + collectPolicyTypes(policy.policy, types); + return types; + case "attempt": + return types; + } +} + +function maxPolicyDepth(policies) { + return Math.max(...policies.map((policy) => policyDepth(policy))); +} + +function policyDepth(policy) { + switch (policy.type) { + case "attempt": + return 1; + case "series": + case "parallel": + return 1 + Math.max(0, ...policy.policies.map(policyDepth)); + case "retry": + case "hedge": + return 1 + policyDepth(policy.attempt); + case "timeout": + case "deadline": + return 1 + policyDepth(policy.policy); + } +} + +function sum(items, field) { + return items.reduce((total, item) => total + item[field], 0); +} + +function hasExplicitLimitation(text) { + return typeof text === "string" + && text.length > 40 + && ( + text.includes("not ") + || text.includes("does not") + || text.includes("without") + || text.includes("outside") + ); +} diff --git a/packages/core/tests/evidence/correctness/time-policy-planner.mjs b/packages/core/tests/evidence/correctness/time-policy-planner.mjs new file mode 100644 index 0000000..bf2da25 --- /dev/null +++ b/packages/core/tests/evidence/correctness/time-policy-planner.mjs @@ -0,0 +1,57 @@ +/** + * Correctness evidence: time policy planning without task execution. + * + * @author Admilson B. F. Cossa + * SPDX-License-Identifier: Apache-2.0 + */ + +import { estimateRetry, planTimePolicy } from "../../../dist/time-policy/index.js"; +import { createSuite } from "../harness.mjs"; + +const suite = createSuite("correctness"); + +await suite.proof( + "CORR-009", + "time-policy planner computes retry upper bounds", + "retry upper bound includes attempt duration and delays between failed attempts only", + async () => { + const plan = estimateRetry({ + attempt: { type: "attempt", duration: 100 }, + retry: { times: 3, initialDelay: 50, backoff: "fixed", jitter: false }, + }); + + return { + ok: plan.valid && plan.upperBoundMs === 400 && plan.attempts === 3, + upperBoundMs: plan.upperBoundMs, + attempts: plan.attempts, + warnings: plan.warnings.map((warning) => warning.code), + }; + }, +); + +await suite.proof( + "CORR-010", + "time-policy planner reports infeasible deadline", + "deadline planning returns invalid before runtime execution when policy cannot fit", + async () => { + const plan = planTimePolicy({ + type: "deadline", + now: 1_000, + deadlineAt: 1_050, + policy: { type: "attempt", duration: 100 }, + }); + + return { + ok: !plan.valid + && plan.upperBoundMs === 50 + && plan.warnings.some((warning) => warning.code === "deadline_infeasible"), + valid: plan.valid, + upperBoundMs: plan.upperBoundMs, + warnings: plan.warnings.map((warning) => warning.code), + }; + }, +); + +const summary = suite.summary(); +process.stdout.write(JSON.stringify(summary, null, 2) + "\n"); +process.exit(summary.failed > 0 ? 1 : 0); diff --git a/packages/core/tests/evidence/run-all.mjs b/packages/core/tests/evidence/run-all.mjs index f609c93..31671b2 100644 --- a/packages/core/tests/evidence/run-all.mjs +++ b/packages/core/tests/evidence/run-all.mjs @@ -21,6 +21,9 @@ const files = [ "correctness/resource-ownership-model.mjs", "correctness/runtime-contracts.mjs", "correctness/source-protocol-analysis.mjs", + "correctness/time-policy-planner.mjs", + "correctness/formal-time-policy-model.mjs", + "correctness/nested-time-policy-composition.mjs", "security/worker-boundary.mjs", "release/release-integrity.mjs", "release/receipt-ledger.mjs", diff --git a/packages/core/tests/unit/time-policy.test.js b/packages/core/tests/unit/time-policy.test.js new file mode 100644 index 0000000..b1d0b49 --- /dev/null +++ b/packages/core/tests/unit/time-policy.test.js @@ -0,0 +1,263 @@ +/** + * Time policy planner subpath tests. + * + * @author Admilson B. F. Cossa + * SPDX-License-Identifier: Apache-2.0 + */ + +import assert from "node:assert/strict"; +import { test } from "vitest"; + +import { estimateHedge, estimateRetry, planTimePolicy } from "../../dist/time-policy/index.js"; + +test("Given fixed retry policy, estimateRetry computes runtime-aligned worst-case delay", () => { + const plan = estimateRetry({ + attempt: { type: "attempt", duration: 100 }, + retry: { times: 3, initialDelay: 50, backoff: "fixed", jitter: false }, + }); + + assert.equal(plan.valid, true); + assert.equal(plan.upperBoundMs, 400); + assert.equal(plan.attempts, 3); + assert.deepEqual(plan.warnings, []); +}); + +test("Given retry under timeout, planTimePolicy reports timeout truncation before execution", () => { + const plan = planTimePolicy({ + type: "timeout", + timeout: 250, + policy: { + type: "retry", + attempt: { type: "attempt", duration: 100 }, + retry: { times: 4, initialDelay: 50, backoff: "fixed", jitter: false }, + }, + }); + + assert.equal(plan.valid, true); + assert.equal(plan.upperBoundMs, 250); + assert.equal(plan.warnings.some((warning) => warning.code === "retry_exceeds_timeout"), true); +}); + +test("Given hedge policy, estimateHedge includes staggered attempt cost", () => { + const plan = estimateHedge({ + attempt: { type: "attempt", duration: 100 }, + after: 25, + max: 3, + }); + + assert.equal(plan.valid, true); + assert.equal(plan.upperBoundMs, 150); + assert.equal(plan.attempts, 3); + assert.equal(plan.parallelWorkMs, 300); +}); + +test("Given impossible deadline, planTimePolicy returns invalid plan before execution", () => { + const plan = planTimePolicy({ + type: "deadline", + now: 1_000, + deadlineAt: 1_050, + policy: { type: "attempt", duration: 100 }, + }); + + assert.equal(plan.valid, false); + assert.equal(plan.upperBoundMs, 50); + assert.equal(plan.warnings.some((warning) => warning.code === "deadline_infeasible"), true); +}); + +test("Given series and parallel policies, planTimePolicy composes critical path and work", () => { + const series = planTimePolicy({ + type: "series", + policies: [ + { type: "attempt", duration: 10 }, + { type: "attempt", duration: 20 }, + ], + }); + const parallel = planTimePolicy({ + type: "parallel", + policies: [ + { type: "attempt", duration: 10 }, + { type: "attempt", duration: 20 }, + ], + }); + + assert.equal(series.upperBoundMs, 30); + assert.equal(series.parallelWorkMs, 30); + assert.equal(parallel.upperBoundMs, 20); + assert.equal(parallel.parallelWorkMs, 30); +}); + +test("Given empty compositions, planTimePolicy returns explicit zero-cost warning", () => { + const series = planTimePolicy({ type: "series", policies: [] }); + const parallel = planTimePolicy({ type: "parallel", policies: [] }); + + assert.equal(series.upperBoundMs, 0); + assert.equal(parallel.upperBoundMs, 0); + assert.equal(series.warnings[0].code, "empty_composition"); + assert.equal(parallel.warnings[0].code, "empty_composition"); +}); + +test("Given dynamic backoff and jitter, estimateRetry uses conservative upper-bound warnings", () => { + const plan = estimateRetry({ + attempt: { type: "attempt", duration: 10 }, + retry: { + times: 3, + initialDelay: 5, + maxDelay: 20, + backoff: () => 1, + jitter: true, + }, + }); + + assert.equal(plan.upperBoundMs, 70); + assert.equal(plan.warnings.some((warning) => warning.code === "dynamic_backoff_upper_bound"), true); + assert.equal(plan.warnings.some((warning) => warning.code === "jitter_upper_bound"), true); +}); + +test("Given linear and exponential retry policies, estimateRetry respects maxDelay", () => { + const linear = estimateRetry({ + attempt: { type: "attempt", duration: 10 }, + retry: { times: 3, initialDelay: 10, maxDelay: 15, backoff: "linear", jitter: false }, + }); + const exponential = estimateRetry({ + attempt: { type: "attempt", duration: 10 }, + retry: { times: 3, initialDelay: 10, maxDelay: 15, backoff: "exponential", jitter: false }, + }); + + assert.equal(linear.upperBoundMs, 55); + assert.equal(exponential.upperBoundMs, 55); +}); + +test("Given timeout policies, planTimePolicy distinguishes retry, hedge, and generic truncation", () => { + const retry = planTimePolicy({ + type: "timeout", + timeout: 10, + policy: { type: "retry", attempt: { type: "attempt", duration: 20 }, retry: 2 }, + }); + const hedge = planTimePolicy({ + type: "timeout", + timeout: 10, + policy: { type: "hedge", attempt: { type: "attempt", duration: 20 }, after: 1, max: 2 }, + }); + const generic = planTimePolicy({ + type: "timeout", + timeout: 10, + policy: { type: "attempt", duration: 20 }, + }); + + assert.equal(retry.warnings.at(-1).code, "retry_exceeds_timeout"); + assert.equal(hedge.warnings.at(-1).code, "hedge_exceeds_timeout"); + assert.equal(generic.warnings.at(-1).code, "time_exceeds_timeout"); +}); + +test("Given nested timeout policies, planTimePolicy finds retry and hedge inside composition wrappers", () => { + const seriesRetry = planTimePolicy({ + type: "timeout", + timeout: 10, + policy: { + type: "series", + policies: [ + { type: "retry", attempt: { type: "attempt", duration: 20 }, retry: 2 }, + ], + }, + }); + const nestedHedge = planTimePolicy({ + type: "timeout", + timeout: 10, + policy: { + type: "timeout", + timeout: 1_000, + policy: { type: "hedge", attempt: { type: "attempt", duration: 20 }, after: 1, max: 2 }, + }, + }); + + assert.equal(seriesRetry.warnings.at(-1).code, "retry_exceeds_timeout"); + assert.equal(nestedHedge.warnings.at(-1).code, "hedge_exceeds_timeout"); +}); + +test("Given nested parallel and deadline wrappers, planTimePolicy classifies timeout warnings through the policy tree", () => { + const parallelRetry = planTimePolicy({ + type: "timeout", + timeout: 10, + policy: { + type: "parallel", + policies: [ + { type: "retry", attempt: { type: "attempt", duration: 20 }, retry: 2 }, + ], + }, + }); + const deadlineHedge = planTimePolicy({ + type: "timeout", + timeout: 10, + policy: { + type: "deadline", + now: 1_000, + deadlineAt: 2_000, + policy: { type: "hedge", attempt: { type: "attempt", duration: 20 }, after: 1, max: 2 }, + }, + }); + + assert.equal(parallelRetry.warnings.at(-1).code, "retry_exceeds_timeout"); + assert.equal(deadlineHedge.warnings.at(-1).code, "hedge_exceeds_timeout"); +}); + +test("Given feasible timeout and deadline policies, planTimePolicy returns the inner plan unchanged", () => { + const timeout = planTimePolicy({ + type: "timeout", + timeout: 100, + policy: { type: "attempt", duration: 20 }, + }); + const deadline = planTimePolicy({ + type: "deadline", + now: 1_000, + deadlineAt: new Date(1_100), + policy: { type: "attempt", duration: 20 }, + }); + + assert.equal(timeout.upperBoundMs, 20); + assert.equal(deadline.upperBoundMs, 20); + assert.deepEqual(timeout.warnings, []); + assert.deepEqual(deadline.warnings, []); +}); + +test("Given deadline without explicit now, planTimePolicy uses the current clock", () => { + const plan = planTimePolicy({ + type: "deadline", + deadlineAt: Date.now() + 1_000, + policy: { type: "attempt", duration: 1 }, + }); + + assert.equal(plan.valid, true); + assert.equal(plan.upperBoundMs, 1); +}); + +test("Given invalid hedge and excessive nesting, planner rejects invalid contracts", () => { + assert.throws( + () => estimateHedge({ attempt: { type: "attempt", duration: 1 }, after: 1, max: 0 }), + /hedge max/, + ); + + let nested = { type: "attempt", duration: 1 }; + for (let index = 0; index < 66; index++) { + nested = { type: "timeout", timeout: 10_000, policy: nested }; + } + + assert.throws(() => planTimePolicy(nested), /time policy depth exceeded/); + + let nestedRetry = { type: "attempt", duration: 1 }; + let nestedHedge = { type: "attempt", duration: 1 }; + for (let index = 0; index < 66; index++) { + nestedRetry = { type: "retry", attempt: nestedRetry, retry: 1 }; + nestedHedge = { type: "hedge", attempt: nestedHedge, after: 1, max: 1 }; + } + + assert.throws(() => planTimePolicy(nestedRetry), /time policy depth exceeded/); + assert.throws(() => planTimePolicy(nestedHedge), /time policy depth exceeded/); +}); + +test("Given the root import, time-policy helpers are not exported from the root runtime", async () => { + const root = await import("../../dist/index.js"); + + assert.equal("planTimePolicy" in root, false); + assert.equal("estimateRetry" in root, false); + assert.equal("estimateHedge" in root, false); +});