From 06df9a03e55ab5aabe338b28a268a13131ce6dc7 Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Mon, 2 Nov 2026 13:31:22 +0000 Subject: [PATCH] Record an independent scalar audit of the four PR6349 input lifts. The separate replay checks directions, inverse bases, both dirty-carrier sandwiches, and the local paid and target debits. It does not rerun native phases, the caller, or the price engines, and it does not change kappa. Co-authored-by: unpaidmoon --- .../p104-input-lift-direction-audit/README.md | 83 ++++ .../SOURCES.json | 36 ++ .../p104-input-lift-direction-audit/TASK.json | 123 ++++++ .../VERIFY.json | 36 ++ .../p104-input-lift-direction-audit/verify.py | 391 ++++++++++++++++++ 5 files changed, 669 insertions(+) create mode 100644 research/p104-input-lift-direction-audit/README.md create mode 100644 research/p104-input-lift-direction-audit/SOURCES.json create mode 100644 research/p104-input-lift-direction-audit/TASK.json create mode 100644 research/p104-input-lift-direction-audit/VERIFY.json create mode 100644 research/p104-input-lift-direction-audit/verify.py diff --git a/research/p104-input-lift-direction-audit/README.md b/research/p104-input-lift-direction-audit/README.md new file mode 100644 index 0000000000..112493a6b8 --- /dev/null +++ b/research/p104-input-lift-direction-audit/README.md @@ -0,0 +1,83 @@ +# Independent audit of four helper-input lifts + +This package checks the scalar schedule in Ali Romman's merged +[PR #6349](https://github.com/CrocSwap/integer-mult-bounds/pull/6349), +head `af7cb6c67f8fc7d82a2e4aee2dd2f07481bf6690`, archived on canonical main +`7c49fe32c55de02c2c873655c804b16e4c3fef0a`. It answers the review requested in +[discussion #1166 comment 19341394](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19341394). + +No new kappa is claimed. The selected frontier stays +`781451/250000000`. The reported conditional value `0.003129111` is not +re-derived here. + +## What was checked + +On the pinned PR6314 source word and the pinned lifted word, a separate +replay agrees with the proof's local invoice: + +- All 799 scalar columns of both words end at the identity. Owned lifetimes + are 32 and peak ownership is 13. +- The only initial-chart changes are roles 496, 649, 663 and 508, from frame + 3 to frames 595, 597, 105 and 1093. Final frames are unchanged. +- Each input direction `h` has a unit primary coordinate, disjoint support, + and an inverse `I - (h - e_p) e_p^T`. Replaying `h` through the source + chronology reproduces the stated departure response. +- The new chart is contained in every nonzero departure frame of that + response. Frame 1093, basis `[30, 42, 384]`, is the GF(2) span intersection + of frames 118 and 733. +- The two dirty-carrier sandwiches leave the wide carrier short one primary + input and the narrow carrier short half a primary input, including the + intervening additions that do not use those carriers. The six trailing + output additions are the inverse basis. +- Ten frame-3 reads of the four primaries are absent from the lifted word. + Role 649 is injected into 198 at frame 597, and role 663 into 179 at frame + 105, with the stated carrier subtractions. +- Helper rank is `dim(final) - dim(initial)` off the 208 main roles. The four + lifts change ranks `9→8`, `9→8`, `9→8` and `9→6`. The histograms therefore + move by paid `H1+H2+H3+2H4-4H5` and productive `H6+3H8-4H9`. Scalar + allowances are 127042 and 127088. Paid rank masses are 5952 and 5946. + +Four mutations fail closed: deleting the first carrier subtraction, deleting +one output correction, reversing the 649 injection, and replacing frame 1093 +by `[1, 2, 4]`. + +## What was not checked + +Native Pauli images, absolute phases, the physical caller, both rational +price engines, the compiler threshold and the 58 outer predicates were not +run. The five framework assumptions remain. This audit does not accept +PR6349 and does not cover PR6350 or PR6353. + +## Reproduce + +Python 3.12, standard library, from the repository root: + +```sh +python3 -W error -B research/p104-input-lift-direction-audit/verify.py +python3 -O -W error -B research/p104-input-lift-direction-audit/verify.py +python3 scripts/research_package.py --package research/p104-input-lift-direction-audit --check-only +python3 scripts/research_package.py --package research/p104-input-lift-direction-audit +``` + +The direct verifier hashes the three pinned inputs and does not need Git or +network. The registered runner also checks provenance blobs. Each scientific +command finishes in a few seconds. Status: +`PASS_P104_INPUT_LIFT_DIRECTION_AUDIT`. + +## Open next questions + +The signed Pauli image of one changed helper normalizer is still unchecked. +That is the smallest native gate for this word; the predecessor checker and +`native_all_columns` are the blocker. Separately, PR6353's later word needs +its own initial-frame reading before these four ranks are reused. [TASK.json](TASK.json) +records both first steps. + +## Credit + +Audit: unpaidmoon, with substantial Cursor Grok assistance. Apache-2.0. + +Construction and author checks: Ali Romman, with substantial OpenAI Codex +assistance, in PR6349. Source word: DreamingOfClouds, with Claude Opus 5.5 +assistance, in PR6314, retaining PR6167. The frame and endpoint rules follow +the published scalar model of that chain; this package reimplements them and +does not vendor the checker. diff --git a/research/p104-input-lift-direction-audit/SOURCES.json b/research/p104-input-lift-direction-audit/SOURCES.json new file mode 100644 index 0000000000..b186bec7da --- /dev/null +++ b/research/p104-input-lift-direction-audit/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/p104-frontier-compression-2/WORD.json.gz", + "usage": "input", + "git_blob": "cb3aed1d5604eb290f18759b37becaad428ac27a", + "sha256": "889f0f5d193d993dabee1e20dcfbcf63f9d88cfe5bd6973d564276c744d1e190" + }, + { + "path": "research/p104-native-input-lifting/PROOF.md", + "usage": "input", + "git_blob": "85499c9eb7b6413f460ef0e77430957ec94e6620", + "sha256": "7207c047aa18aa97f304df99057978c37f612ef710f35354216b9956f906fe81" + }, + { + "path": "research/p104-native-input-lifting/WORD.json.gz", + "usage": "input", + "git_blob": "f21f7ac451c3f2e1ae8d5ca1dcad839a0b0d844f", + "sha256": "1415a62059ed62d0b4657db91f7ec01b23c117f5f2744746d93c880bd777be92" + } + ] +} diff --git a/research/p104-input-lift-direction-audit/TASK.json b/research/p104-input-lift-direction-audit/TASK.json new file mode 100644 index 0000000000..d8582a8a80 --- /dev/null +++ b/research/p104-input-lift-direction-audit/TASK.json @@ -0,0 +1,123 @@ +{ + "schema_version": 1, + "task_id": "p104-side-correction", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "p104-side-correction", + "question": "Can joint helper bases and a legal causal split improve the complete P104 productive/paid invoice?", + "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", + "research/p104-helper-subspace-splits/README.md", + "research/dyadic-helper-channel-capacity/README.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": "An exact arbitrary-input identity, source/target frame availability and restoration at the chosen cut, plus the complete channel+correction+idle/hosting bill or an explicit favorable bound. The native channel alone is not a supplier. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "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": "Start with the selected #5599 emitted word and review pending #5718 distinct input/output bases plus #5717/#5719 coverage before claiming work. Pick one uncovered source word, helper group and cut region. Prove the arbitrary-input relation and legal entry/exit corrections, then compare full target and paid profiles. Reject if completion, owned lifetimes or consumer costs repay the gain. A static pairing rank alone is not a physical split.", + "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": [ + "P104", + "helper basis", + "helper split", + "5718", + "dyadic capacity" + ], + "existing_checks": [ + { + "scope": "PR #4133: literal-slot defect", + "evidence": "research/p104-literal-slot-defect/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "88666f1dee93fbd85b31fd5d6f91a219e111b5f4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4136: uniform commutation gap", + "evidence": "research/p104-uniform-commutation-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "281ce601a8be9db470de630759179c23e1dfaa88", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4140: uniform encoding gap", + "evidence": "research/p104-uniform-encoding-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "de25c6525aa866962309df5d107b32d55e6e5628", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4153: source-chart shortcut exhausts its optimistic allowance", + "evidence": "research/p104-source-chart-shortcut/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "9123241fea53df77e51ffe30d9aca1625d4bf3a8", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4154: fiber-tag seam mismatch", + "evidence": "research/p104-fiber-tag-seam/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "4ffcdaee5d6255a9cea1fe53a5424435068089d0", + "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": "Independent scalar audit of PR6349 four delayed helper-input lifts: directions, inverse output basis, two dirty-carrier subtractions, and the local native target debit on the PR6314 word.", + "scope_change_reason": "The card asks for one uncovered helper cut on a pinned source word. This package does not build a new cut of selected #5599. It audits the published PR6349 lifts, whose source is the PR6314 compression of PR6167, because discussion 1166 comment 19341394 requests that review.", + "bottleneck_link": "The local signed target debit H6+3H8-4H9 and paid change H1+H2+H3+2H4-4H5 are necessary for PR6349's reported kappa increase. Confirming them does not admit the outer compiler, native phases, or a new selected frontier.", + "budget_minutes": 60, + "stop_rule": "Stop if a direction, carrier sandwich, endpoint row, frame inclusion, or the paid/target histogram disagrees with the pinned word. Do not extend the audit into the native Clifford checker or a new lift search.", + "outcome": "completed", + "evidence": "verify.py endpoint replays, carrier sandwiches, and four failure controls", + "author": "unpaidmoon", + "ai_assistance": "Substantial Cursor Grok assistance. The predecessor construction and author checks are not this audit.", + "open_questions": [ + { + "question": "Do the four changed helper normalizers keep their signed Pauli images and absolute phases at the new charts?", + "why_it_matters": "The scalar endpoint and target debit do not discharge native_all_columns. PR6349's kappa claim stays conditional until that gate, the caller, and the other four framework assumptions are checked.", + "first_step": "Pin PR6349 head af7cb6c67f8fc7d82a2e4aee2dd2f07481bf6690 and compare one changed helper normalizer, including its absolute phase, against an independent Pauli multiplication on every column of that chart.", + "blocked_by": "This package does not run the predecessor native or caller checkers. Those checks remain author-side." + }, + { + "question": "Do these four input charts still account for the same target debit after PR6353's nine output contractions?", + "why_it_matters": "PR6353 reports a higher conditional kappa on a later word. An input-lift audit of PR6349 does not transfer to that head.", + "first_step": "On the frozen PR6353 word, read the initial frames of roles 496, 649, 663 and 508 and recompute only their dim(final)-dim(initial) ranks.", + "blocked_by": "PR6353 is a different construction and a separate handoff. Its physical-contact gate is not this package." + } + ] +} diff --git a/research/p104-input-lift-direction-audit/VERIFY.json b/research/p104-input-lift-direction-audit/VERIFY.json new file mode 100644 index 0000000000..3f3acabc26 --- /dev/null +++ b/research/p104-input-lift-direction-audit/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-frontier-compression-2/WORD.json.gz", + "research/p104-native-input-lifting/PROOF.md", + "research/p104-native-input-lifting/WORD.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "SHA256 pins; four directions and inverses; carrier sandwiches; endpoint rows; paid and target histograms; four failure controls." + }, + { + "argv": [ + "{python}", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Repeat the same explicit checks with assertion-stripping enabled." + } + ] +} diff --git a/research/p104-input-lift-direction-audit/verify.py b/research/p104-input-lift-direction-audit/verify.py new file mode 100644 index 0000000000..112027dfbb --- /dev/null +++ b/research/p104-input-lift-direction-audit/verify.py @@ -0,0 +1,391 @@ +#!/usr/bin/env python3 +"""Independent scalar audit of the four PR6349 helper-input lifts. + +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. +The audited word and proof are Ali Romman's. The source word is +DreamingOfClouds' PR6314 compression of PR6167. This verifier does not import +those packages or their checker chain. +""" +from collections import Counter +from copy import deepcopy +from fractions import Fraction as Q +from hashlib import sha256 +from pathlib import Path +import gzip +import json + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +STATUS = 'PASS_P104_INPUT_LIFT_DIRECTION_AUDIT' +SOURCE = 'research/p104-frontier-compression-2/WORD.json.gz' +LIFT = 'research/p104-native-input-lifting/WORD.json.gz' +PROOF = 'research/p104-native-input-lifting/PROOF.md' +PRIMARIES = (496, 649, 663, 508) +DIRECTIONS = ( + (496, {496: Q(1), 639: Q(-1), 643: Q(-1, 2)}, + {496: Q(1), 639: Q(-1), 643: Q(-1, 2)}, 595, (52,)), + (649, {649: Q(1), 648: Q(-1)}, + {649: Q(1), 648: Q(-1), 198: Q(1)}, 597, (82,)), + (663, {663: Q(1), 665: Q(-1)}, + {663: Q(1), 665: Q(-1), 179: Q(1, 2)}, 105, (51,)), + (508, {508: Q(1), 631: Q(-1), 635: Q(-1, 2)}, + {508: Q(1), 631: Q(-1), 635: Q(-1, 2)}, 1093, (30, 42, 384)), +) +RESTORE = ( + ['ADD', 639, 496, '1', 127], + ['ADD', 643, 496, '1/2', 127], + ['ADD', 648, 649, '1', 127], + ['ADD', 665, 663, '1', 127], + ['ADD', 631, 508, '1', 127], + ['ADD', 635, 508, '1/2', 127], +) +PROOF_PHRASES = ( + 'e496 - e639 - e643/2', + 'e649 - e648', + 'e663 - e665', + 'e508 - e631 - e635/2', + '639 += 496; 643 += 496/2; 648 += 649;', + '665 += 663; 631 += 508; 635 += 508/2.', + 'H1 + H2 + H3 + 2 H4 - 4 H5', + 'H6 + 3 H8 - 4 H9', + 'Frame 1093 is the intersection of frames 118 and 733.', +) + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def load_words(): + pins = {row['path']: row for row in json.loads((HERE / 'SOURCES.json').read_text())['files'] + if row['usage'] == 'input'} + need(set(pins) == {SOURCE, LIFT, PROOF}, 'Pinned input inventory') + raw = {} + for path, pin in pins.items(): + data = (ROOT / path).read_bytes() + need(sha256(data).hexdigest() == pin['sha256'], 'SHA256 ' + path) + raw[path] = data + proof = raw[PROOF].decode() + for phrase in PROOF_PHRASES: + need(phrase in proof, 'Proof phrase ' + phrase) + source = json.loads(gzip.decompress(raw[SOURCE])) + lifted = json.loads(gzip.decompress(raw[LIFT])) + return source, lifted + + +def span(basis): + out = {0} + for value in basis: + need(type(value) is int and 0 < value < 512 and value not in out, + 'Independent binary basis') + out |= {item ^ value for item in tuple(out)} + return frozenset(out) + + +def replay(word): + """Scalar endpoint, MOVE-rank histogram and helper ranks. + + Helper rank is dim(final frame) - dim(initial frame) for every public role + outside the 104 live ports and their +112 copies. A MOVE of rank + |dim(destination) - dim(source)| is one paid job. Both rules are the + finite GF(2) frame model: a later public frame must strictly contain the + earlier one, and a private owned move must strictly shrink it. + """ + public = word['public'] + owned = word['owned_fields'] + need(public == 770 and owned == 29, 'Public and owned inventory') + frames = [span(basis) for basis in word['frames']] + rows = [{role: Q(1)} for role in range(public + owned)] + current = list(word['initial']) + [None] * owned + paid = Counter() + scalar = 0 + live = set() + peak = 0 + lifetimes = 0 + for event in word['program']: + op, role = event[:2] + need(0 <= role < public + owned, 'Role index') + if op == 'MOVE': + _, role, start, end, private = event + need(current[role] == start and (role in live) is private, + 'Transport source and ownership') + if private: + need(frames[end] < frames[start], 'Nested private transport') + else: + need(frames[start] < frames[end], 'Nested public transport') + paid[abs(len(word['frames'][end]) - len(word['frames'][start]))] += 1 + current[role] = end + continue + if op == 'INIT': + need(role >= public and role not in live, 'Owned initialization') + live.add(role) + lifetimes += 1 + peak = max(peak, len(live)) + rows[role] = {} + current[role] = event[2] + scalar += 2 + continue + if op == 'CLEAR': + need(role in live and current[role] == event[2], 'Owned erasure') + rows[role] = {} + current[role] = None + live.remove(role) + scalar += 2 + continue + coefficient, frame = Q(event[-2]), event[-1] + need(coefficient and current[role] == frame, 'Scalar destination and coefficient') + numerator, denominator = abs(coefficient.numerator), coefficient.denominator + need(denominator & (denominator - 1) == 0, 'Dyadic scalar coefficient') + if op == 'SCALE': + need(numerator & (numerator - 1) == 0, 'Dyadic unit SCALE') + rows[role] = {key: coefficient * value for key, value in rows[role].items()} + scalar += 2 * (abs(numerator.bit_length() - denominator.bit_length()) + + int(coefficient < 0)) + continue + source = event[2] + need(source != role and current[source] == frame, 'Common scalar chart') + if op == 'COPY': + need(role in live and not rows[role], 'COPY into a cleared owned field') + rows[role] = {key: coefficient * value for key, value in rows[source].items()} + else: + need(op == 'ADD', 'Scalar opcode') + row = rows[role] + for key, value in rows[source].items(): + total = row.get(key, 0) + coefficient * value + if total: + row[key] = total + else: + row.pop(key, None) + scalar += 2 * (3 + numerator.bit_length() - 1 + numerator.bit_count() + + denominator.bit_length() - 1) + need(not live and peak == 13 and lifetimes == 32 and current[:public] == word['final'], + 'Public exits and owned lifetimes') + ports = set(word['live']) + for role, row in enumerate(rows): + expected = {role: Q(1)} if role < public else {} + if role - 112 in ports: + expected[role - 112] = Q(1) + need(row == expected, 'Endpoint row ' + str(role)) + main = ports | {role + 112 for role in ports} + need(len(ports) == 104 and len(main) == 208, 'Port and main inventory') + helpers = Counter(len(word['frames'][word['final'][role]]) + - len(word['frames'][word['initial'][role]]) + for role in range(public) if role not in main) + need(min(helpers) > 0, 'Positive helper ranks') + return {'paid': dict(paid), 'helpers': dict(helpers), 'scalar': scalar, + 'paid_rank_mass': sum(rank * count for rank, count in paid.items())} + + +def difference(after, before): + ranks = set(after) | set(before) + return {rank: after.get(rank, 0) - before.get(rank, 0) + for rank in ranks if after.get(rank, 0) != before.get(rank, 0)} + + +def departures(program, direction, public, owned): + values = [Q(0)] * (public + owned) + for role, coefficient in direction.items(): + values[role] = coefficient + first = {} + response = {} + for event in program: + op, role = event[:2] + if op == 'MOVE' and event[2] == 3 and event[4] is False: + need(role not in first, 'One departure from the zero chart') + first[role] = event[3] + if values[role]: + response[role] = values[role] + elif op in ('INIT', 'CLEAR'): + values[role] = Q(0) + elif op == 'SCALE': + values[role] *= Q(event[2]) + elif op == 'COPY': + values[role] = Q(event[3]) * values[event[2]] + elif op == 'ADD': + values[role] += Q(event[3]) * values[event[2]] + return response, first + + +def apply_update(vector, direction, primary, sign): + updated = dict(vector) + factor = sign * vector.get(primary, 0) + for role, coefficient in direction.items(): + if role == primary: + continue + total = updated.get(role, 0) + factor * coefficient + if total: + updated[role] = total + else: + updated.pop(role, None) + return updated + + +def check_bases(source): + occupied = set() + for primary, direction, response, frame, basis in DIRECTIONS: + need(direction[primary] == response[primary] == 1, 'Unit primary coordinate') + need(not occupied.intersection(direction), 'Disjoint input supports') + occupied.update(direction) + need(apply_update(apply_update( + {primary: Q(3), 700: Q(5)}, direction, primary, 1), direction, primary, -1) + == {primary: Q(3), 700: Q(5)}, 'Inverse basis') + update = {role: coefficient for role, coefficient in direction.items() if role != primary} + need(all(apply_update({role: amount}, direction, primary, 1) == {role: amount} + for role, amount in update.items()), + 'Carrier update is nilpotent') + found, first = departures(source['program'], direction, source['public'], + source['owned_fields']) + need(found == response, 'Departure response of primary ' + str(primary)) + common = span(basis) + for role in direction: + need(source['initial'][role] == 3 and source['final'][role] == 127, + 'Full helper before the lift') + for role in response: + need(common <= span(source['frames'][first[role]]), + 'Common native input subspace') + + +def index(program, event): + hits = [position for position, item in enumerate(program) if item == event] + need(len(hits) == 1, 'Unique event ' + str(event)) + return hits[0] + + +def carrier_sandwich(program, opening, closing, primary, wide, narrow): + start, end = index(program, opening), index(program, closing) + need(start < end, 'Carrier subtraction precedes its closing addition') + values = {wide: {'v': Q(1)}, narrow: {'z': Q(1)}, primary: {'x': Q(1)}} + + def coefficient(role): + return values.setdefault(role, {('external', role): Q(1)}) + + for event in program[start:end + 1]: + if event[0] != 'ADD': + continue + destination, source, scale = event[1], event[2], Q(event[3]) + if destination not in (primary, wide, narrow) and source not in (primary, wide, narrow): + continue + row = dict(coefficient(destination)) + for key, amount in coefficient(source).items(): + row[key] = row.get(key, 0) + scale * amount + if row[key] == 0: + del row[key] + values[destination] = row + need(values[wide].get('v') == 1 and values[wide].get('x') == -1 + and values[wide].get('z', 0) == 0, 'Wide carrier loses one primary input') + need(values[narrow].get('z') == 1 and values[narrow].get('x') == Q(-1, 2) + and values[narrow].get('v', 0) == 0, 'Narrow carrier loses half a primary input') + need(values[primary] == {'x': Q(1)}, 'Primary input is unchanged inside the sandwich') + + +def check_schedule(source, lifted): + need(len(source['program']) == 17445 and len(lifted['program']) == 17452, + 'Event counts') + need(lifted['frames'][:-1] == source['frames'], 'Inherited frames') + need(lifted['frames'][1093] == [30, 42, 384], 'Appended three-dimensional frame') + need(span(lifted['frames'][1093]) == span(source['frames'][118]) & span(source['frames'][733]), + 'Frame 1093 is the span intersection of frames 118 and 733') + need(source['frames'][1091:1093] == lifted['frames'][1091:1093], + 'Frames 1091 and 1092 are unchanged') + need(source['final'] == lifted['final'], 'Final frames unchanged') + initial = [role for role, (before, after) in enumerate(zip(source['initial'], lifted['initial'])) + if before != after] + need(initial == [496, 508, 649, 663], 'Only the four lifted inputs change chart') + for primary, _direction, _response, frame, basis in DIRECTIONS: + need(source['initial'][primary] == 3 and lifted['initial'][primary] == frame, 'New chart') + need(tuple(lifted['frames'][frame]) == basis, 'Chart basis') + source_rank = (len(source['frames'][source['final'][primary]]) + - len(source['frames'][source['initial'][primary]])) + lifted_rank = (len(lifted['frames'][lifted['final'][primary]]) + - len(lifted['frames'][lifted['initial'][primary]])) + expected = {496: 8, 649: 8, 663: 8, 508: 6}[primary] + need(source_rank == 9 and lifted_rank == expected, 'Individual target rank') + omitted = [event for event in source['program'] + if event[0] == 'ADD' and event[-1] == 3 and event[2] in PRIMARIES] + need(len(omitted) == 10 and all(event not in lifted['program'] for event in omitted), + 'Ten initial-chart uses of the lifted inputs are removed') + need(not any(event[0] == 'ADD' and event[-1] == 3 and event[2] in PRIMARIES + for event in lifted['program']), + 'No lifted input is read in the zero chart') + need(tuple(lifted['program'][-6:]) == RESTORE, 'Six inverse-basis output additions') + carrier_sandwich(lifted['program'], ['ADD', 639, 643, '-2', 3], + ['ADD', 639, 643, '2', 1027], 496, 639, 643) + carrier_sandwich(lifted['program'], ['ADD', 631, 635, '-2', 3], + ['ADD', 631, 635, '2', 118], 508, 631, 635) + block = ( + ['MOVE', 179, 3, 105, False], + ['ADD', 179, 663, '1/2', 105], + ['MOVE', 665, 3, 1051, False], + ['MOVE', 663, 105, 1051, False], + ['ADD', 665, 663, '-1', 1051], + ) + need(any(tuple(lifted['program'][pos:pos + 5]) == block + for pos in range(len(lifted['program']) - 4)), + 'Contiguous 663 injection and carrier subtraction') + move_648 = index(lifted['program'], ['MOVE', 648, 3, 120, False]) + move_649 = index(lifted['program'], ['MOVE', 649, 597, 120, False]) + subtract_649 = index(lifted['program'], ['ADD', 648, 649, '-1', 120]) + need(move_648 < move_649 < subtract_649, '648 receives 649 after both arrive at frame 120') + need(['MOVE', 649, 3, 120, False] not in lifted['program'], '649 no longer departs from zero') + need(['MOVE', 663, 3, 1051, False] not in lifted['program'], '663 no longer departs from zero') + need(index(lifted['program'], ['MOVE', 198, 3, 597, False]) + < index(lifted['program'], ['ADD', 198, 649, '1', 597]), + '198 receives 649 at its first frame') + + +def reject(mutator): + _source, lifted = load_words() + mutated = deepcopy(lifted) + mutator(mutated) + try: + replay(mutated) + except ValueError as error: + return str(error) + raise ValueError('Mutated word was accepted') + + +def controls(): + def drop(event): + def mutate(word): + position = word['program'].index(event) + del word['program'][position] + return mutate + + messages = { + 'missing first carrier subtraction': reject(drop(['ADD', 639, 643, '-2', 3])), + 'missing output correction': reject(drop(['ADD', 635, 508, '1/2', 127])), + 'wrong 649 injection': reject(lambda word: word['program'].__setitem__( + word['program'].index(['ADD', 198, 649, '1', 597]), + ['ADD', 198, 649, '-1', 597])), + } + + def wrong_intersection(word): + word['frames'][1093] = [1, 2, 4] + + messages['wrong intersection'] = reject(wrong_intersection) + for label, message in messages.items(): + need('Endpoint row' in message or 'Nested public transport' in message + or 'Nested private transport' in message or 'Transport source' in message, + 'Control did not fail closed: ' + label + ': ' + message) + return messages + + +def main(): + source, lifted = load_words() + check_bases(source) + check_schedule(source, lifted) + before, after = replay(source), replay(lifted) + need(difference(after['paid'], before['paid']) == {1: 1, 2: 1, 3: 1, 4: 2, 5: -4}, + 'Local paid change') + need(difference(after['helpers'], before['helpers']) == {6: 1, 8: 3, 9: -4}, + 'Native target debit') + need((before['scalar'], before['paid_rank_mass'], after['scalar'], after['paid_rank_mass']) + == (127042, 5952, 127088, 5946), 'Scalar allowance and paid rank mass') + failed = controls() + need(len(failed) == 4, 'Four failure controls') + print(STATUS) + + +if __name__ == '__main__': + main()