diff --git a/research/two-resource-migration-tariff/PROOF.md b/research/two-resource-migration-tariff/PROOF.md new file mode 100644 index 0000000000..ce6381a69d --- /dev/null +++ b/research/two-resource-migration-tariff/PROOF.md @@ -0,0 +1,123 @@ +# Exact tariffs for two reusable resources + +This is a scoped written proof. The finite verifier corroborates it; it is +not a formal proof-kernel certificate or a physical implementation theorem. + +## Model + +There are n>=1 labelled consumers. Consumer i is live on a nonempty half-open +interval [s_i,t_i), has a fixed nonempty eligibility list L_i contained in +{0,1}, and pays w_i>=0 each time it moves between the two resources while +remaining live. Initial placement and release are free. Simultaneously live +consumers occupy distinct resources. There is no reserved initial or final +placement. The lists do not change during a lifetime. + +Partition time at the distinct endpoints. A schedule gives a legal injection +on every elementary time interval, including intervals with no live consumers. +At a boundary its charge is the sum of w_i over consumers present on both +sides whose resource changes. Atomic exchanges are allowed. This is an +optimistic transfer model: a physical realization may need extra storage, +movement, restoration and time. We prove no zero-cost physical migration. + +Pointwise Hall feasibility means every active set has an injective eligible +placement. In this two-resource model this says that at most two consumers +are live and, when two are live, their lists have union {0,1}. It guarantees a +schedule when migrations are allowed, since independent legal placements can +be chosen at every elementary interval. + +## Theorem 1: exact weighted optimum and a checkable certificate + +For each elementary interval k let S_k be its set of legal placements. +Pointwise feasibility implies 1<=|S_k|<=2. For consecutive placements a,b set + + c(a,b) = sum_{i live in both, a(i)!=b(i)} w_i. + +Then the exact minimum charge is the shortest layered-path cost with every +initial placement free and every terminal placement accepted. In particular, + + D_0(a) = 0, + D_k(b) = min_{a in S_{k-1}} [D_{k-1}(a)+c(a,b)], + optimum = min_{b in S_last} D_last(b). + +Every schedule is one such path with exactly that charge, and every path is +an allowed atomic schedule. Induction on the layer proves the recurrence. +There are at most 2n-1 layers and four arcs per layer boundary. After endpoints +are sorted, a sweep constructs the states and optimum in O(n) steps. Sorting +costs O(n log n). These bounds count exact arithmetic operations. + +The implementation emits a path and integer potentials p_k(a). A separate +checker tests the path's cost M, p_0(a)<=0 for every initial state, + + p_k(b)-p_{k-1}(a) <= c(a,b) on every arc, + p_last(b) >= M for every terminal state. + +Along every competing path these inequalities telescope to charge>=M. +The supplied path attains M. Thus the checker does not need to repeat the +minimization. The optimizer's distances satisfy these certificate conditions. +Integer weights are the executable interface; the mathematical recurrence +also holds for arbitrary nonnegative real weights with exact comparisons. + +Allowing extra changes inside an elementary interval cannot defeat the lower +bound. Sample the placement once in each interval. A consumer whose sampled +resources differ across a boundary must move at least once between samples. +For a fixed consumer these sampling windows are disjoint, and its lifetime +contains each such window. Nonnegative charges therefore dominate the sampled +path's charge. The event model already attains its own optimum. + +## Theorem 2: the sharp worst-case migration count is max(0,n-2) + +Set every weight to one. Every pointwise-feasible instance admits a schedule +with at most max(0,n-2) migrations. For every n>=1 there is an instance whose +minimum is exactly this number. + +For the upper bound, separate the connected components of the interval +overlap graph, using positive-length overlap. Isolated consumers cost zero. +In a component with k>=2 consumers, process starts in time order, with endings +before starts at the same time. At most two consumers can be live. + +Choose the initial placement of the first consumer to accommodate the first +consumer overlapping it. Such a choice exists by pointwise feasibility, and +no intervening consumer belongs to that component. If both begin together, +choose any feasible placement of the pair. This first pair costs no migration. + +At every later start there is at most one continuing consumer. If its current +resource permits the new consumer's placement, do nothing. Otherwise the new +consumer must have a singleton list equal to that occupied resource. Hall +feasibility forces the continuing consumer to be eligible for the other +resource; move it once and start the new consumer. With no continuing consumer, +the new placement is free. Two simultaneous new starts also need no migration. +Thus each start after the first pair incurs at most one migration. The component +cost is at most k-2. Summing components is at most n-2 whenever n>=2 and there +is a nontrivial component. With only isolated consumers it is zero. This proves +the stated bound, including n=1. + +For sharpness at n>=2, use one flexible consumer on [0,2n-1) with list {0,1}. +For i=1,...,n-1 put a blocker on [2i-1,2i), whose singleton resource is +(i-1) modulo 2. Blockers are disjoint and the instance is pointwise feasible. +During consecutive blockers the long consumer must occupy opposite resources. +It therefore moves at least n-2 times. It can move once in each intervening +gap, attaining the bound. At n=1 a single consumer attains zero. + +Giving the long consumer weight W yields exact optimum W(n-2), since no +blocker can move. Consequently pointwise compatibility leaves an unbounded +additive migration bill even at concurrency two. At n=3 the family is the +smallest pointwise-feasible instance without a constant-per-lifetime eligible +assignment. One or two consumers always admit a fixed assignment: assign +disjoint consumers independently, or use their common feasible placement if +they overlap. + +## Research consequence and limits + +Ali Romman's [PR #5781](https://github.com/CrocSwap/integer-mult-bounds/pull/5781) +explicitly excludes temporal reuse from its static assignment model. The new +step solves this particular temporal extension and quantifies an obligation +that a per-time matching relaxation omits. This does not exhibit an error in +that predecessor, nor was its matcher run to establish this result. Hall's +theorem and layered shortest paths are classical; the scoped tariff, sharp +family and independently checked implementation are the contribution here. + +The two-resource assumption, fixed lists, free initial/final placement and +atomic migration contract matter. This is no theorem about arbitrary coupled +native consumers or three or more resources. No actual helper lifetime export, +physical transfer word, selected supplier invoice, new kappa, uniform compiler, +stock/precision/tape proof or complete multiplication theorem is supplied. diff --git a/research/two-resource-migration-tariff/README.md b/research/two-resource-migration-tariff/README.md new file mode 100644 index 0000000000..8def80ffa8 --- /dev/null +++ b/research/two-resource-migration-tariff/README.md @@ -0,0 +1,85 @@ +# Sharp migration tariffs for two reusable resources + +Claim type: scoped written proof with finite corroboration. This contribution +was produced by Nick Petalas. Apache-2.0. + +For n>=1 consumers with fixed half-open lifetimes and nonempty fixed lists of +eligible resources from {0,1}, pointwise Hall feasibility guarantees a schedule +with at most max(0,n-2) migrations. This bound is sharp for every n. One long +flexible consumer and alternating resource-fixed short consumers attain it. +Giving the long consumer transfer price W makes the exact bill W(n-2) at n>=2. +Thus independent per-time matching can omit arbitrarily large transfer charges. +Three consumers already give the smallest obstruction to a placement that stays +fixed throughout each lifetime. + +The package also constructs a minimum-cost schedule for arbitrary nonnegative +integer per-consumer transfer prices. There are at most two assignments per +elementary interval. A layered shortest path gives the optimum in O(n log n) +arithmetic operations including endpoint sorting. A path and dual arc potentials +certify optimality without repeating the optimization. See [PROOF.md](PROOF.md). + +This answers the temporal-reuse boundary left outside Ali Romman's +[PR #5781](https://github.com/CrocSwap/integer-mult-bounds/pull/5781), exact head +`cb06de3a4f6e2a2c927eb3aa3f9f43a578f73a1f`, specifically its +`docs/research/compatible-resource-assignment.md` Open next questions. The +predecessor supplies the question and static interface, and is cited without +rerunning its matcher. Hall's theorem and layered shortest paths are classical +inputs. No new general matching algorithm is claimed. + +## Evidence and reproduction + +From the repository root, run: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/two-resource-migration-tariff/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/two-resource-migration-tariff/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/two-resource-migration-tariff +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/two-resource-migration-tariff --check-source-history +``` + +Another CPython 3.12 interpreter path can replace the absolute path. The verifier +uses only the standard library, writes no files, and emits a generated receipt +bound to the six package files by SHA-256. It enumerates all labelled lifetimes +with endpoints in {0,1,2,3,4}, all three nonempty eligibility lists and one to +three consumers, using both unit and labelled integer prices. Its independent +oracle enumerates literal assignments on every integer unit cell, including +cells without an endpoint. Additional checks cover seeded weighted timelines, +the sharp family through 512 consumers, half-open touching lifetimes, invalid +inputs and forged optimality certificates. Counts are printed by the verifier. + +## Scope and limits + +The executable interface accepts 1..512 consumers, integer endpoints in +0..10^6 and integer migration prices in 0..10^12. The written theorem has no +consumer bound and depends only on endpoint order; its weighted recurrence also +allows nonnegative real prices with exact comparisons. + +Initial placement and release are free, and migrations are atomic. Fixed +initial/final owners, changing lists, coupled consumers, physical movement, +spare storage for exchanges and more than two resources are outside this model. +No actual caller's ownership schedule has been exported. These are abstract +transfer costs, not an admitted physical bill. No new kappa, selected-frontier +change or complete multiplication theorem is claimed. Independent human and +formal proof-kernel review are unclaimed. + +## Open next questions + +1. Bind one actual caller's pair of owners, fixed lifetimes and paid transfers + to this interface. Start by exporting every live interval and legal transfer + including restoration. A physical source adapter and transfer word are absent. +2. Determine the sharp migration count with three resources and fixed lists. + Start with exact small timelines. A separate argument is needed; the two-state + bound does not transfer. + +Structured relevance, first steps and blockers are in [TASK.json](TASK.json). + +## Implementation limits + +All production loops are bounded by 512 consumers, 1024 endpoints and two states +per cell. The independent oracle is bounded by six consumers and nine integer +time units. Functions remain below 60 lines. Python necessarily allocates dynamic +objects; the fixed input bounds limit live collections. Runtime allocation and +ordinary library dispatch are explicit Power of Ten deviations. No recursion, +dynamic code execution, external programs or inherited source imports are used. +Warning-strict normal and optimized runs keep the explicit certificate and input +checks active. The two internal assertions are redundant dimension invariants. diff --git a/research/two-resource-migration-tariff/SOURCES.json b/research/two-resource-migration-tariff/SOURCES.json new file mode 100644 index 0000000000..fdb80ada25 --- /dev/null +++ b/research/two-resource-migration-tariff/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + } + ] +} diff --git a/research/two-resource-migration-tariff/TASK.json b/research/two-resource-migration-tariff/TASK.json new file mode 100644 index 0000000000..d8fc8dd712 --- /dev/null +++ b/research/two-resource-migration-tariff/TASK.json @@ -0,0 +1,113 @@ +{ + "schema_version": 1, + "task_id": "supplier-boundary-audit", + "priority_revision": 8, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "original_card": { + "id": "supplier-boundary-audit", + "question": "Does one changed supplier have complete source-bound native, caller, ordinary and outer admission coverage?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "Pin the current sources and one obligation; the historical owner audit is an example, not evidence of a current bug.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Choose one latest uncovered candidate and build a delta coverage map against the selected review. For P104, #5717 changes owned-lifetime assumptions and #5719 covers exact #5713 causal premises; neither automatically transfers to #5718. For BIT, #5679/#5708 need component admission and compatible outer use. Check controls and exact source identity before reuse; stop with one resolved gap or explicit remaining obligation. A heavy full replay requires a separate serial resource budget.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "supplier admission", + "5717", + "5719", + "5708", + "owned lifetime" + ], + "existing_checks": [ + { + "scope": "PR #4088: author-checked local words, native receipts, owner/phase fill and exact moment.", + "evidence": "research/staged544-mixed-fourth-entry/README.md", + "remaining": "Rebind and validate ordinary/outer admission with all four providers; full mixed release not established.", + "status": "author-checked", + "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3801: successor scatter-boundary decision package.", + "evidence": "research/scatter-boundary-decision/README.md", + "remaining": "Consult its exact acceptance scope before any new exporter audit; not proof of a selected failure.", + "status": "author-checked", + "source_commit": "911f8800ba7a4b03603ef62c5ffc6240e53cb5fd", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Exact weighted migration tariffs and sharp max(0,n-2) transfer count for two reusable compatible resources over fixed half-open lifetimes.", + "scope_change_reason": "The assigned card concerns supplier admission. This is a self-contained interface side result on the temporal-reuse boundary explicitly excluded by PR5781, rather than an audit or supplier-admission claim.", + "bottleneck_link": "Pointwise compatible reuse does not price moves of a continuing helper. The exact temporal relaxation can expose an omitted transfer obligation before physical caller expansion.", + "budget_minutes": 60, + "stop_rule": "Ship the first proved and independently enumerated temporal tariff; do not extend to more resources or physical installation.", + "outcome": "completed", + "evidence": "PROOF.md supplies the universal argument; verify.py prints PASS_TWO_RESOURCE_MIGRATION_TARIFF with complete finite-oracle counts and generated SHA-256 bindings.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can an actual caller export authenticated fixed lifetimes, eligible owner pairs and nonzero migration tariffs for this two-resource model?", + "why_it_matters": "Only source-bound data makes the temporal lower bound relevant to a complete supplier invoice.", + "first_step": "Export one pair of physical owners and list every live interval and legal transfer, including restoration.", + "blocked_by": "No physical source adapter or transfer word is supplied." + }, + { + "question": "What replaces the sharp n-2 migration bound for three reusable resources with fixed lists?", + "why_it_matters": "The two-state proof depends on two resources and does not establish a general hosting limit.", + "first_step": "Test three resources on small exact lifetimes with fixed lists and count charged persistent changes.", + "blocked_by": "A separate combinatorial argument and larger state space are required." + } + ], + "predecessors": [ + { + "pr": 5781, + "author": "Ali Romman", + "head": "cb06de3a4f6e2a2c927eb3aa3f9f43a578f73a1f", + "question_source": "docs/research/compatible-resource-assignment.md, Open next questions", + "usage": "Question and static-interface context only; no executable dependency or predecessor replay." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19215637", + "environment": { + "python": "CPython 3.12.15", + "platform": "macOS 27.0.1 arm64", + "dependencies": "Python standard library only" + }, + "claim_type": "scoped written proof with finite corroboration" +} diff --git a/research/two-resource-migration-tariff/VERIFY.json b/research/two-resource-migration-tariff/VERIFY.json new file mode 100644 index 0000000000..394591f9b9 --- /dev/null +++ b/research/two-resource-migration-tariff/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact new temporal tariffs, independent exhaustive schedules, sharp family, invalid-input and forged-certificate controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same complete coverage under optimized Python with explicit checks active." + } + ] +} diff --git a/research/two-resource-migration-tariff/verify.py b/research/two-resource-migration-tariff/verify.py new file mode 100644 index 0000000000..ea97e20b7f --- /dev/null +++ b/research/two-resource-migration-tariff/verify.py @@ -0,0 +1,246 @@ +#!/usr/bin/env python3 +"""Exact two-resource migration certificates and bounded independent oracles.""" + +from dataclasses import dataclass, replace +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path +import random + + +@dataclass(frozen=True) +class Job: + start: int + stop: int + mask: int + weight: int = 1 + + +@dataclass(frozen=True) +class Certificate: + cost: int + choices: tuple[int, ...] + potentials: tuple[tuple[int, ...], ...] + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def layers(jobs): + """At most 1023 layers, each with at most two injective assignments.""" + require(1 <= len(jobs) <= 512, "job count") + events = {} + for i, job in enumerate(jobs): + require(all(type(x) is int for x in + (job.start, job.stop, job.mask, job.weight)), "integer input") + require(0 <= job.start < job.stop <= 10**6, "lifetime") + require(1 <= job.mask <= 3, "resource list") + require(0 <= job.weight <= 10**12, "migration weight") + events.setdefault(job.start, [[], []])[1].append(i) + events.setdefault(job.stop, [[], []])[0].append(i) + times = sorted(events) + active = set() + result = [] + for time in times[:-1]: + endings, beginnings = events[time] + active.difference_update(endings) + active.update(beginnings) + require(len(active) <= 2, "pointwise Hall shortage") + ids = tuple(sorted(active)) + options = tuple(tuple(r for r in range(2) if jobs[i].mask & (1 << r)) + for i in ids) + states = tuple(tuple(zip(ids, colors)) for colors in product(*options) + if len(set(colors)) == len(colors)) + require(bool(states), "pointwise Hall shortage") + assert 1 <= len(states) <= 2 + result.append(states) + assert len(result) <= 2 * len(jobs) - 1 + return tuple(result) + + +def transition(jobs, previous, current): + old = dict(previous) + return sum(jobs[i].weight for i, color in current + if i in old and old[i] != color) + + +def optimize(jobs): + states = layers(jobs) + distances = [(0,) * len(states[0])] + parents = [(-1,) * len(states[0])] + for before, after in zip(states, states[1:]): + entries = tuple(min((distances[-1][p] + transition(jobs, a, b), p) + for p, a in enumerate(before)) for b in after) + distances.append(tuple(x[0] for x in entries)) + parents.append(tuple(x[1] for x in entries)) + final = min(range(len(states[-1])), key=lambda i: distances[-1][i]) + cost = distances[-1][final] + choices = [0] * len(states) + for k in range(len(states) - 1, -1, -1): + choices[k] = final + final = parents[k][final] + return Certificate(cost, tuple(choices), tuple(distances)) + + +def check_certificate(jobs, certificate): + """Check a primal path and dual arc inequalities, without optimization.""" + states = layers(jobs) + require(type(certificate.cost) is int and certificate.cost >= 0, "cost") + require(len(certificate.choices) == len(states), "path length") + require(len(certificate.potentials) == len(states), "potential length") + path = [] + for k, options in enumerate(states): + choice = certificate.choices[k] + require(type(choice) is int and 0 <= choice < len(options), "choice") + values = certificate.potentials[k] + require(len(values) == len(options), "potential width") + require(all(type(x) is int for x in values), "integer potentials") + path.append(options[choice]) + require(all(x <= 0 for x in certificate.potentials[0]), "initial bound") + for k in range(1, len(states)): + for p, before in enumerate(states[k - 1]): + for q, after in enumerate(states[k]): + require(certificate.potentials[k][q] <= + certificate.potentials[k - 1][p] + + transition(jobs, before, after), "dual arc") + require(all(x >= certificate.cost for x in certificate.potentials[-1]), + "terminal bound") + actual = sum(transition(jobs, a, b) for a, b in zip(path, path[1:])) + require(actual == certificate.cost, "primal cost") + return actual + + +def brute(jobs): + """Enumerate literal assignments on every integer unit cell independently.""" + require(len(jobs) <= 6 and max(j.stop for j in jobs) <= 9, "oracle bound") + options = [] + for time in range(min(j.start for j in jobs), max(j.stop for j in jobs)): + active = tuple(i for i, j in enumerate(jobs) if j.start <= time < j.stop) + cell = [] + for colors in product(range(2), repeat=len(active)): + if len(set(colors)) != len(colors): + continue + if all(jobs[i].mask & (1 << c) for i, c in zip(active, colors)): + cell.append(dict(zip(active, colors))) + if not cell: + return None + options.append(cell) + best = None + for path in product(*options): + cost = 0 + for before, after in zip(path, path[1:]): + for i in before.keys() & after.keys(): + if before[i] != after[i]: + cost += jobs[i].weight + best = cost if best is None else min(best, cost) + return best + + +def compare(jobs): + expected = brute(jobs) + if expected is None: + try: + optimize(jobs) + except ValueError as error: + require(str(error) == "pointwise Hall shortage", "wrong rejection") + return False + raise ValueError("accepted infeasible timeline") + certificate = optimize(jobs) + require(check_certificate(jobs, certificate) == expected, "oracle mismatch") + if all(j.weight == 1 for j in jobs): + require(expected <= max(0, len(jobs) - 2), "count bound") + return True + + +def exhaustive(): + intervals = tuple((a, b) for a in range(4) for b in range(a + 1, 5)) + counts = {"instances": 0, "feasible": 0, "infeasible": 0} + for n in range(1, 4): + for lifetimes in product(intervals, repeat=n): + for masks in product(range(1, 4), repeat=n): + for weighted in range(2): + jobs = tuple(Job(a, b, mask, i + 1 if weighted else 1) + for i, ((a, b), mask) in + enumerate(zip(lifetimes, masks))) + feasible = compare(jobs) + counts["instances"] += 1 + counts["feasible" if feasible else "infeasible"] += 1 + return counts + + +def alternating(n, weight=1): + require(1 <= n <= 512, "family bound") + return (Job(0, 2 * n - 1, 3, weight),) + tuple( + Job(2 * i - 1, 2 * i, 1 << ((i - 1) % 2)) for i in range(1, n)) + + +def controls(): + jobs = alternating(3, 7) + certificate = optimize(jobs) + rejected = 0 + corruptions = [replace(certificate, cost=0), + replace(certificate, choices=()), + replace(certificate, choices=(9,) + certificate.choices[1:]), + replace(certificate, potentials=()), + replace(certificate, potentials=((1, 1),) + + certificate.potentials[1:])] + potentials = list(certificate.potentials) + potentials[-1] = tuple(x + 1 for x in potentials[-1]) + corruptions.append(replace(certificate, potentials=tuple(potentials))) + for bad in corruptions: + try: + check_certificate(jobs, bad) + except ValueError: + rejected += 1 + require(rejected == len(corruptions), "accepted forged certificate") + invalid = [(), (Job(0, 0, 3),), (Job(0, 1, 0),), (Job(0, 1, 4),), + (Job(0, 1, True),), (Job(0, 1, 3, -1),), + (Job(0, 1, 3, 10**12 + 1),), (Job(0, 10**6 + 1, 3),), + (Job(0, 1, 3),) * 513] + for bad in invalid: + try: + optimize(bad) + except ValueError: + rejected += 1 + require(rejected == len(corruptions) + len(invalid), "accepted bad input") + return rejected + + +def corroborate(): + rng = random.Random(5781) + random_cases = 400 + for _ in range(random_cases): + jobs = [] + for _ in range(rng.randint(1, 6)): + a = rng.randrange(6) + jobs.append(Job(a, rng.randrange(a + 1, 8), rng.randrange(1, 4), + rng.randrange(8))) + compare(tuple(jobs)) + for n in range(1, 513): + jobs = alternating(n, 7) + require(check_certificate(jobs, optimize(jobs)) == 7 * max(0, n - 2), + "sharp family") + # Touching half-open jobs need neither simultaneous capacity nor migration. + require(check_certificate((Job(0, 1, 1), Job(1, 2, 1)), + optimize((Job(0, 1, 1), Job(1, 2, 1)))) == 0, + "half-open boundary") + return {"random_weighted_cases": random_cases, "sharp_family_sizes": 512, + "rejection_controls": controls(), "half_open_controls": 1} + + +def main(): + counts = exhaustive() + counts.update(corroborate()) + root = Path(__file__).resolve().parent + names = ("verify.py", "PROOF.md", "README.md", "TASK.json", + "SOURCES.json", "VERIFY.json") + hashes = {name: sha256((root / name).read_bytes()).hexdigest() for name in names} + print(json.dumps({"status": "PASS_TWO_RESOURCE_MIGRATION_TARIFF", + "counts": counts, "sha256": hashes}, sort_keys=True)) + + +if __name__ == "__main__": + main()