diff --git a/research/p104-unread-early-read/PROOF.md b/research/p104-unread-early-read/PROOF.md new file mode 100644 index 0000000000..202747cf54 --- /dev/null +++ b/research/p104-unread-early-read/PROOF.md @@ -0,0 +1,130 @@ +# Early read on the PR #5827 role-695 interval + +This note checks one published replacement. It does not recompute conditional +kappa, native phases, or the caller bill. + +## Pinned words + +The source word is the PR #5811 word vendored by PR #5827 at +`05cd36e5af06d7a3790e30ce3f449fa89b853768` +(`inputs/pr5811-WORD.json.gz`, canonical SHA256 +`a06445539ad73fe16deae66fef8c52ffc39f5f14c765eab3dc3d98e0e2d8074c`). +The edited word is that pull request's published program +(`inputs/pr5827-WORD.json.gz`, canonical SHA256 +`d1e5ee3b9811ce7be0ad80aecf19b41cd9277e838b3a9fe52d25baa610d58782`). +Those canonical digests are the `source_word_sha256` and `word_sha256` +fields of that pull request's `WITNESS.json`. The programs differ at +indices 13815 through 13821 and nowhere else. Boundaries, frames, ports +and the live set are identical. + +## The interval + +Write a, b, c, d for roles 695, 733, 773, 709. Write A, C, B for frames +3, 597, 1031. Replaying every transport before index 13815 on the source +word, with the same strict nesting rule as a public move into a larger +frame and a private move into a smaller frame, puts a and b in A, d in C +and c in B. + +The unique source block at that index is + +```text +MOVE c: B -> C (private) +ADD d += c in C +MOVE b: A -> C +ADD b += c in C +MOVE a: A -> C +ADD a += b in C +MOVE a: C -> B +``` + +The replacement is + +```text +ADD a += b in A +MOVE a: A -> B +ADD a += c in B +MOVE c: B -> C (private) +ADD d += c in C +MOVE b: A -> C +ADD b += c in C +``` + +Both schedules are legal on these entry frames. Both finish with a in B, +b in C, c in C and d in C, and with images + +```text +a' = a + b + c +b' = b + c +c' = c +d' = d + c +``` + +taken over the interval-entry values. The first replacement event reads b +while b still carries its entry value: b is not the destination of any +earlier event in the block. Omitting that event stays frame-legal and +yields `a' = a + c`. Replacing its coefficient 1 by 2 yields a term `2b`. +Moving that same event to the end of the block is not a legal common-chart +addition: a then sits in B and b sits in C, while the event still names +frame A. + +Reading the post-update value `b + c` and also adding c, which is the +arithmetic content of a late read followed by the direct `a += c`, produces +`a + b + 2c`. That counterfactual is not itself a legal schedule of this +interval. The legal early read is what keeps the coefficient of c equal to 1. + +## Frame ranks + +The frame bases have lengths 0, 1 and 5, and their XOR-spans have sizes +1, 2 and 32, so those lengths are the F_2-dimensions. The spans are strictly +nested: span(A) proper subset span(C) proper subset span(B). A transport +rank is the absolute difference of basis lengths, which is the rank used by +PR #5827's own native boundary check. + +The two role-695 transports in the source block therefore have ranks + +```text +A -> C : |1 - 0| = 1 +C -> B : |5 - 1| = 4 +``` + +and the replacement transport has rank + +```text +A -> B : |5 - 0| = 5. +``` + +The other two moves, private c from B to C (rank 4) and public b from A to C +(rank 1), occur in both schedules. The MOVE-rank multiset therefore changes +by exactly `-H_1 - H_4 + H_5`. + +PR #5827's proof says these frames have dimensions 0, 4 and 5, and that the +public queries A to C and C to B have ranks 4 and 1. The nesting claim is +right. The dimensions and the assignment of the two leg ranks are not. +The histogram change written next to that sentence, `-H_1 - H_4 + H_5`, +still matches the word. + +## Local power sign + +For `H_r(t) = r^t` and `0 < t < 1`, + +```text +1^t + 4^t - 5^t > 0. +``` + +Indeed `1^t = 1`, and dividing by `5^t` gives the equivalent inequality +`(1/5)^t + (4/5)^t > 1`. For `v` in `(0, 1)` and `t` in `(0, 1)`, +`v^(t-1) > 1`, hence `v^t > v`. Both `1/5` and `4/5` lie in `(0, 1)` and +sum to 1, so the two strict comparisons add. At `t = 1` the difference is 0. +At `t = 2` it is `1 + 16 - 25 < 0`. + +One extra coefficient-+1 ADD is present. Under the scalar rule +`2 * (3 + bit_length(n) - 1 + bit_count(n) + bit_length(d) - 1)` with +`n = d = 1`, that ADD costs 8 real scalar primitives. This is a local +charge, not a caller moment. + +## What this does not show + +It does not show that the native phase of either actual map matches the +published receipt, that the full ordinary and outer bill crosses at +0.00312476680, or that any of the five framework assumptions holds. The +selected frontier is unchanged. diff --git a/research/p104-unread-early-read/README.md b/research/p104-unread-early-read/README.md new file mode 100644 index 0000000000..17aefb56fb --- /dev/null +++ b/research/p104-unread-early-read/README.md @@ -0,0 +1,84 @@ +# Early source observation on the PR #5827 unread path + +**Partial audit; no new kappa.** The selected frontier stays the conditional +result recorded at this base. This package does not admit PR #5827. + +## Scope and evidence + +Task card: `p104-side-correction`, scope **refined**. The live handoff on +[Discussion #1166](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166) +for [PR #5827](https://github.com/CrocSwap/integer-mult-bounds/pull/5827) +asks for an independent review of the early source observation, the direct +native phase and the full bill. This package settles the early observation +and the frame ranks it sits on. The native phase and the caller bill are +open. + +On the pinned PR #5811 word, the seven events at index 13815 are the unique +copy of the published source block. The published replacement word differs +only there. Replaying frames up to that cut puts roles 695 and 733 in frame +3, role 709 in frame 597 and role 773 in frame 1031. Both schedules are +legal and realize + +```text +a' = a + b + c, b' = b + c, c' = c, d' = d + c +``` + +with the same exit frames. The first new event is `ADD 695 += 733` in frame +3, while role 733 still holds its interval-entry value. Omitting it drops +`b` from `a`. A coefficient 2 writes `2b`. Placing that event after the +other six is not a legal common-chart addition. + +Frame bases at 3, 597 and 1031 have lengths 0, 1 and 5, and the spans are +strictly nested. The role-695 legs therefore have ranks 1 (frame 3 to 597) +and 4 (frame 597 to 1031). The replacement leg has rank 5. PR #5827's proof +states dimensions 0, 4 and 5 and assigns those two leg ranks in the opposite +order. The nesting claim is right. The MOVE multiset still changes by +`-H_1 - H_4 + H_5`, because the other two moves are common to both +schedules. For every real `t` in `(0, 1)`, `1^t + 4^t - 5^t > 0`. One extra +coefficient-+1 ADD costs 8 real scalar primitives under the retained local +rule. That is not a caller moment. + +The argument, pins and controls are in [PROOF.md](PROOF.md). Source commits, +Git blobs and SHA256 pins for the catalogue and selected record are in +[SOURCES.json](SOURCES.json). The two word files are live inputs; their +gzip and canonical SHA256 pins are constants in `verify.py`, matched to +PR #5827 `WITNESS.json`. + +## Reproduce + +From the repository root, with Python 3.12: + +```sh +python3 scripts/research_package.py --package research/p104-unread-early-read --check-only +python3.12 -B scripts/research_package.py --package research/p104-unread-early-read +``` + +Both registered modes print: + +```text +PASS_P104_UNREAD_EARLY_READ +``` + +No network and no third-party package. The verifier walks the vendored +words directly. It does not import `research/p104-unread-path-resynthesis`. + +## Open next questions + +- Do the native phases of the actual rank-1 map (frame 3 to 597) and the + actual rank-4 map (frame 597 to 1031) match the PR #5827 receipt? The + published sentence points a reviewer at a rank-4 map from frame 3 to + frame 597, which is not this transport. First lower those two frame + pairs. This package does not vendor the Clifford code. +- Does the complete caller bill still lie in + `(0.00312476681507, 0.00312476681508)`? The corrected labels do not + change the paid multiset, so the number can survive, but it was not + recomputed. The five framework assumptions remain, and this audit is + not a reason to move the selected frontier. + +## Credit + +The words, the seven-event plan and the conditional-kappa claim belong to +Mason Hale's PR #5811 and Ali Romman's PR #5827, with the retained +native, helper, controller, compiler and analytic predecessors named there. +The independent frame walk, the rank correction and this verifier are new. +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. diff --git a/research/p104-unread-early-read/SOURCES.json b/research/p104-unread-early-read/SOURCES.json new file mode 100644 index 0000000000..fdb80ada25 --- /dev/null +++ b/research/p104-unread-early-read/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/p104-unread-early-read/TASK.json b/research/p104-unread-early-read/TASK.json new file mode 100644 index 0000000000..9e9775d062 --- /dev/null +++ b/research/p104-unread-early-read/TASK.json @@ -0,0 +1,123 @@ +{ + "schema_version": 1, + "task_id": "p104-side-correction", + "priority_revision": 8, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "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": "refined", + "actual_scope": "Independently check the early source observation of open PR #5827 on the pinned PR #5811 word: the seven-event role-695 interval at index 13815, the legal frames at that cut, and the paid ranks of frames 3, 597 and 1031.", + "scope_change_reason": "The card asks for one uncovered helper group and a complete invoice. This package does not search for a new split and does not replay the caller. It checks the first clause of the live #1166 handoff on PR #5827, whose smallest next task is an independent review of the early source observation, the direct native phase and the full bill. Only the early observation and its frame ranks are settled here.", + "bottleneck_link": "Complex currently binds. PR #5827 claims a small conditional gain by replacing two role-695 transports with one direct transport. The early read is the identity that makes those transports equivalent on arbitrary entry values. Correcting which leg has rank 4 tells a later native-phase audit which maps to inspect. This package does not raise selected kappa.", + "budget_minutes": 60, + "stop_rule": "Stop after the unique seven-event identity, the frame-rank correction and the early-read controls. Do not rerun the sealed caller, Clifford lowering or outer moment.", + "outcome": "partial", + "evidence": "research/p104-unread-early-read/verify.py prints PASS_P104_UNREAD_EARLY_READ. It replays the vendored PR5811 and PR5827 words, checks the four-role images and rejects the proof sentence that frames 3, 597 and 1031 have dimensions 0, 4 and 5.", + "author": "unpaidmoon", + "ai_assistance": "Substantial Cursor Grok assistance.", + "open_questions": [ + { + "question": "Do the actual native phases of the rank-1 frame-3-to-597 map and the rank-4 frame-597-to-1031 map match PR #5827's native receipt?", + "why_it_matters": "The published proof assigns those leg ranks in the opposite order. A phase audit that follows the prose would inspect a rank-4 map from frame 3 to frame 597, and that map is not the word's transport.", + "first_step": "Lower the two actual frame pairs (3, 597) and (597, 1031) with the PR #5827 native checker and compare recipe ranks to 1 and 4.", + "blocked_by": "This package does not vendor the Clifford lowering code and does not rerun PR #5827's native replay." + }, + { + "question": "Does the complete caller bill still cross inside (0.00312476681507, 0.00312476681508)?", + "why_it_matters": "The corrected labels do not change the paid multiset, which is still one rank 1 and one rank 4 removed and one rank 5 added. The numerical claim can therefore survive, but it was not recomputed here, and the selected frontier must not move on this audit alone.", + "first_step": "Run python3.12 -B scripts/research_package.py --package research/p104-unread-path-resynthesis on PR #5827 head 05cd36e5af06d7a3790e30ce3f449fa89b853768.", + "blocked_by": "That package is not on this branch. Its registered replay is a separate serial job, and all five framework assumptions remain." + } + ] +} diff --git a/research/p104-unread-early-read/VERIFY.json b/research/p104-unread-early-read/VERIFY.json new file mode 100644 index 0000000000..1e82423103 --- /dev/null +++ b/research/p104-unread-early-read/VERIFY.json @@ -0,0 +1,22 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-unread-early-read/inputs/pr5811-WORD.json.gz", + "research/p104-unread-early-read/inputs/pr5827-WORD.json.gz" + ], + "commands": [ + { + "argv": ["{python}", "-B", "{package}/verify.py"], + "timeout_seconds": 60, + "checks": "Unique seven-event cut, four-field images, corrected frame ranks 0/1/5, early-read omission and doubled-coefficient controls" + }, + { + "argv": ["{python}", "-O", "-B", "{package}/verify.py"], + "timeout_seconds": 60, + "checks": "Same certificate with assertions removed; require() still rejects a bad schedule" + } + ] +} diff --git a/research/p104-unread-early-read/inputs/pr5811-WORD.json.gz b/research/p104-unread-early-read/inputs/pr5811-WORD.json.gz new file mode 100644 index 0000000000..3633d78556 Binary files /dev/null and b/research/p104-unread-early-read/inputs/pr5811-WORD.json.gz differ diff --git a/research/p104-unread-early-read/inputs/pr5827-WORD.json.gz b/research/p104-unread-early-read/inputs/pr5827-WORD.json.gz new file mode 100644 index 0000000000..6341a49f71 Binary files /dev/null and b/research/p104-unread-early-read/inputs/pr5827-WORD.json.gz differ diff --git a/research/p104-unread-early-read/verify.py b/research/p104-unread-early-read/verify.py new file mode 100644 index 0000000000..d06c9a0b6c --- /dev/null +++ b/research/p104-unread-early-read/verify.py @@ -0,0 +1,269 @@ +#!/usr/bin/env python3 +"""Independent check of the PR #5827 early source observation. + +The vendored words are PR #5811 at the bytes pinned by PR #5827 head +05cd36e5af06d7a3790e30ce3f449fa89b853768 and the published replacement word +from that same head. This verifier does not import that package. + +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. +""" + +from __future__ import annotations + +import gzip +import hashlib +import json +from collections import Counter +from fractions import Fraction +from pathlib import Path + +HERE = Path(__file__).resolve().parent +START = 13815 +A, C, B = 3, 597, 1031 +# Proof names: a=695, b=733, c=773, d=709. +A_ROLE, B_ROLE, C_ROLE, D_ROLE = 695, 733, 773, 709 +ROLES = (A_ROLE, D_ROLE, B_ROLE, C_ROLE) +OLD = ( + ["MOVE", 773, 1031, 597, True], + ["ADD", 709, 773, "1", 597], + ["MOVE", 733, 3, 597, False], + ["ADD", 733, 773, "1", 597], + ["MOVE", 695, 3, 597, False], + ["ADD", 695, 733, "1", 597], + ["MOVE", 695, 597, 1031, False], +) +NEW = ( + ["ADD", 695, 733, "1", 3], + ["MOVE", 695, 3, 1031, False], + ["ADD", 695, 773, "1", 1031], + ["MOVE", 773, 1031, 597, True], + ["ADD", 709, 773, "1", 597], + ["MOVE", 733, 3, 597, False], + ["ADD", 733, 773, "1", 597], +) +SOURCE_GZ_SHA256 = "690656bfca9c6f0366527d158ca4edb14f83c410604d647953c20c7c94bea2e8" +NEW_GZ_SHA256 = "5d50e5654910c9535e9025de0f644bb2dece2396e799b4a766110363448fd0b0" +SOURCE_CANON_SHA256 = "a06445539ad73fe16deae66fef8c52ffc39f5f14c765eab3dc3d98e0e2d8074c" +NEW_CANON_SHA256 = "d1e5ee3b9811ce7be0ad80aecf19b41cd9277e838b3a9fe52d25baa610d58782" +PASS = "PASS_P104_UNREAD_EARLY_READ" + + +class Rejected(Exception): + """An expected illegal schedule or a failed local predicate.""" + + +def require(condition, message): + if not condition: + raise SystemExit("FAIL_P104_UNREAD_EARLY_READ " + message) + + +def sha256(raw): + return hashlib.sha256(raw).hexdigest() + + +def canonical(value): + return sha256(json.dumps(value, sort_keys=True, separators=(",", ":")).encode()) + + +def span(basis): + out = {0} + for vector in basis: + if type(vector) is not int or not 0 < vector < 512 or vector in out: + raise Rejected("frame basis is not independent in F_2^9") + out |= {point ^ vector for point in tuple(out)} + return frozenset(out) + + +def load_word(name, gz_sha, canon_sha): + raw = (HERE / "inputs" / name).read_bytes() + require(sha256(raw) == gz_sha, "gzip pin mismatch for " + name) + word = json.loads(gzip.decompress(raw)) + require(canonical(word) == canon_sha, "canonical word pin mismatch for " + name) + require(word["public"] == 770, "public width") + require(word["owned_fields"] == 29, "owned width") + require(len(word["program"]) == 25984, "event count") + require(len(word["initial"]) == len(word["final"]) == 770, "public boundary width") + return word + + +def hits(program, block): + width = len(block) + return [index for index in range(len(program) - width + 1) + if program[index:index + width] == list(block)] + + +def entry_frames(word, charts): + current = list(word["initial"]) + [None] * word["owned_fields"] + for index, event in enumerate(word["program"]): + if index == START: + return {role: current[role] for role in ROLES} + op, role = event[0], event[1] + if op == "MOVE": + _, role, source, dest, private = event + if current[role] != source: + raise Rejected("transport does not start at the occupied frame") + nested = charts[dest] < charts[source] if private else charts[source] < charts[dest] + if not nested: + raise Rejected("transport is not a strict frame nesting") + current[role] = dest + elif op == "INIT": + current[role] = event[2] + elif op == "CLEAR": + if current[role] != event[2]: + raise Rejected("clear does not name the occupied frame") + current[role] = None + elif op not in ("ADD", "SCALE", "COPY"): + raise Rejected("unknown opcode before the cut") + raise Rejected("cut index is past the program") + + +def simulate(events, frames, charts, occupied): + current = dict(occupied) + image = {role: {role: Fraction(1)} for role in ROLES} + ranks = [] + + def absorb(destination, source, coefficient): + row = image[destination] + for key, value in image[source].items(): + total = row.get(key, 0) + coefficient * value + if total: + row[key] = total + else: + row.pop(key, None) + + for event in events: + op = event[0] + if op == "MOVE": + _, role, source, dest, private = event + if current[role] != source: + raise Rejected("move leaves a frame the role does not occupy") + nested = charts[dest] < charts[source] if private else charts[source] < charts[dest] + if not nested: + raise Rejected("move is not a strict frame nesting") + ranks.append(abs(len(frames[source]) - len(frames[dest]))) + current[role] = dest + elif op == "ADD": + _, role, source, coefficient, frame = event + if current[role] != frame or current[source] != frame: + raise Rejected("ADD operands are not together in the named frame") + absorb(role, source, Fraction(coefficient)) + else: + raise Rejected("interval opcode is not ADD or MOVE") + return current, image, ranks + + +def expect_rejected(action, label): + try: + action() + except Rejected: + return + raise SystemExit("FAIL_P104_UNREAD_EARLY_READ control accepted " + label) + + +def unit_add_charge(): + numerator, denominator = 1, 1 + return 2 * (3 + numerator.bit_length() - 1 + numerator.bit_count() + + denominator.bit_length() - 1) + + +def strict_drop_hypotheses(): + """Hypotheses of the written proof that 1^t + 4^t > 5^t for 0 v because t-1<0. The weights 1/5 + and 4/5 lie in (0,1) and sum to 1, so each strict comparison adds. + Equality holds at t=1. At t=2 the inequality reverses. + """ + one, four = Fraction(1, 5), Fraction(4, 5) + require(0 < one < 1 and 0 < four < 1, "weights leave the open unit interval") + require(one + four == 1, "weights do not recover the rank-5 base") + require(5 < (1 + 2) ** 2, "square-root spot check 5^(1/2) < 1 + 2") + require(1 + 4 == 5, "the paid-power gap must vanish at exponent 1") + require(1 + 16 < 25, "the paid-power gap must reverse at exponent 2") + + +def main(): + source = load_word("pr5811-WORD.json.gz", SOURCE_GZ_SHA256, SOURCE_CANON_SHA256) + edited = load_word("pr5827-WORD.json.gz", NEW_GZ_SHA256, NEW_CANON_SHA256) + for key in ("final", "frames", "initial", "live", "owned_fields", "ports", "public", "schema"): + require(source[key] == edited[key], "boundary field changed: " + key) + require(hits(source["program"], OLD) == [START], "source interval is not the unique cut") + require(edited["program"][START:START + 7] == list(NEW), "replacement block mismatch") + require( + [index for index, (left, right) in enumerate(zip(source["program"], edited["program"])) + if left != right] == list(range(START, START + 7)), + "words differ outside the seven-event interval", + ) + frames = source["frames"] + charts = [span(basis) for basis in frames] + require(len(frames[A]) == 0 and len(charts[A]) == 1, "frame 3 is not dimension 0") + require(len(frames[C]) == 1 and len(charts[C]) == 2, "frame 597 is not dimension 1") + require(len(frames[B]) == 5 and len(charts[B]) == 32, "frame 1031 is not dimension 5") + require(charts[A] < charts[C] < charts[B], "frames 3, 597, 1031 are not strictly nested") + require(not (len(frames[A]) == 0 and len(frames[C]) == 4 and len(frames[B]) == 5), + "the published dimensions 0, 4, 5 were accepted") + rank_ac = abs(len(frames[A]) - len(frames[C])) + rank_cb = abs(len(frames[C]) - len(frames[B])) + rank_ab = abs(len(frames[A]) - len(frames[B])) + require((rank_ac, rank_cb, rank_ab) == (1, 4, 5), "role-695 leg ranks are not 1, 4, 5") + require((rank_ac, rank_cb) != (4, 1), "swapped prose ranks were accepted") + + try: + occupied = entry_frames(source, charts) + except Rejected as exc: + raise SystemExit("FAIL_P104_UNREAD_EARLY_READ " + str(exc)) from exc + require(occupied == {A_ROLE: A, B_ROLE: A, C_ROLE: B, D_ROLE: C}, + "entry frames are not a in 3, b in 3, c in 1031, d in 597") + try: + old_exit, old_image, old_ranks = simulate(OLD, frames, charts, occupied) + new_exit, new_image, new_ranks = simulate(NEW, frames, charts, occupied) + except Rejected as exc: + raise SystemExit("FAIL_P104_UNREAD_EARLY_READ " + str(exc)) from exc + expected = { + A_ROLE: {A_ROLE: Fraction(1), B_ROLE: Fraction(1), C_ROLE: Fraction(1)}, + B_ROLE: {B_ROLE: Fraction(1), C_ROLE: Fraction(1)}, + C_ROLE: {C_ROLE: Fraction(1)}, + D_ROLE: {D_ROLE: Fraction(1), C_ROLE: Fraction(1)}, + } + require(old_exit == new_exit == {A_ROLE: B, B_ROLE: C, C_ROLE: C, D_ROLE: C}, + "exit frames differ") + require(old_image == new_image == expected, "four-field images differ") + require(NEW[0] == ["ADD", A_ROLE, B_ROLE, "1", A], "first new event is not the early read of b") + require(all(event[1] != B_ROLE or event[0] != "ADD" for event in NEW[:-1]), + "b is written before the early read") + require(Counter(new_ranks) - Counter(old_ranks) == Counter({5: 1}), + "the only added transport rank is not 5") + delta = Counter(new_ranks) + delta.subtract(Counter(old_ranks)) + require(dict(delta) == {1: -1, 4: -1, 5: 1}, "paid rank multiset is not -H1-H4+H5") + require(sum(1 for event in NEW if event[0] == "ADD") + == sum(1 for event in OLD if event[0] == "ADD") + 1, + "the schedules do not differ by one ADD") + require(unit_add_charge() == 8, "one coefficient-+1 ADD is not charged at 8") + strict_drop_hypotheses() + + omitted = list(NEW[1:]) + _, omitted_image, _ = simulate(omitted, frames, charts, occupied) + require(omitted_image[A_ROLE] == {A_ROLE: Fraction(1), C_ROLE: Fraction(1)}, + "omitting the early read did not drop b from a") + doubled = [list(event) for event in NEW] + doubled[0][3] = "2" + _, doubled_image, _ = simulate(doubled, frames, charts, occupied) + require(doubled_image[A_ROLE][B_ROLE] == 2, "a doubled early coefficient was not visible") + expect_rejected( + lambda: simulate(list(NEW[1:]) + [list(NEW[0])], frames, charts, occupied), + "deferred early ADD", + ) + post_update = {B_ROLE: Fraction(1), C_ROLE: Fraction(1)} + late_value = {A_ROLE: Fraction(1)} + for key, value in post_update.items(): + late_value[key] = late_value.get(key, 0) + value + late_value[C_ROLE] = late_value.get(C_ROLE, 0) + 1 + require(late_value[C_ROLE] == 2, "reading b after b += c and still adding c does not double c") + extended = list(source["program"]) + list(OLD) + require(hits(extended, OLD) == [START, 25984], "a second copy of the interval was not found") + expect_rejected(lambda: span([82, 82]), "dependent basis") + print(PASS) + + +if __name__ == "__main__": + main()