diff --git a/research/p104-ordinary-event-compression/README.md b/research/p104-ordinary-event-compression/README.md new file mode 100644 index 0000000000..24b801f472 --- /dev/null +++ b/research/p104-ordinary-event-compression/README.md @@ -0,0 +1,72 @@ +# Ordinary-event compression of the PR5907 P104 word: 25,998 → 25,861 events, same invoice + +**Result (tooling and a rewritten word, no new κ).** The latest conditional P104 word, +[PR #5907](https://github.com/CrocSwap/integer-mult-bounds/pull/5907) (DreamingOfClouds, κ 0.003125282), sits at +25,998 of the retained 26,000-event cap, which its author names as the main constraint on further steps. Three +semantics-preserving peephole passes over its ordinary events free **137 events** (25,861 remain) while every MOVE, +INIT and CLEAR event, every chart, every owned lifetime, every endpoint row and the complete paid and helper +profiles stay exactly the same. The rewritten word is shipped as [WORD.json.gz](WORD.json.gz) and is regenerated +by [compress.py](compress.py) from the pinned PR5907 word. + +The passes: (M1) two `ADD r <- s` at the same chart with no intervening event that reads or writes `r` or writes +`s` become one ADD with the summed coefficient (deleted when the sum is zero); (M2) two consecutive `SCALE r` +become one SCALE; (D1) a write into an owned field that is CLEARed before being read again is deleted. The three +passes run to a fixed point: 98 merges and 3 dead writes. ADD count 21,706 → 21,599, SCALE 753 → 724, COPY 23 → 22. +Merged coefficients stay dyadic and within the author's growth bound; the author's scalar allowance falls from +228,664 to 227,372 units. + +Base: canonical main `19fdb086ea96af9a9f87936a2b888e10af4ed810`. Live inputs are pinned in [SOURCES.json](SOURCES.json). + +## Why this matters + +Every recent P104 step (helper hubs #5786, rung removal #5907) adds ordinary events, and the word had two events +of headroom left. The freed 137 events are room for about four more hubs or rung removals of the kind already +in the ladder. The rewrite does not change κ: the invoice is a function of the paid and helper profiles only. + +It also records a negative result obtained with that headroom. A search for further #5786-style asynchronous +hubs on this word (one buffer, one frame, collection before and injection after the cut, over all 385 full-boundary +helpers, all frames of dimension 1–8 and the cut times where the available contacts change) found no hub using +only free contacts; every one of the 298 feasible (frame, helper, cut) triples needs paid subdivisions of other +queries, and the cheapest complete bills are all negative (best −0.00051 in the local concave moment at the PR5907 +exponent, with two subdivisions costing 0.01028 against a split gain of 0.00977 at dimension 8). Rank-two blocks +in which two helpers share the same subdivided queries (the S09 route of the #5803 atlas) are feasible at frames +245 and 246 but no block with at most four shared subdivisions exists, and five or more subdivisions always exceed +the two-helper gain. The search code is not part of this package; its logs are available on request. + +## Verification + +```sh +python3.12 -B research/p104-ordinary-event-compression/verify.py +``` + +About six seconds, standard library only. It authenticates the pinned inputs; regenerates the word with +`compress.py` and compares the decompressed payload with the shipped file; replays both words with its own exact +checker and requires the identical sequence of MOVE/INIT/CLEAR events with identical rows of every moved field and +all 799 endpoint rows; loads PR5827's `local.py` unmodified and requires equal paid profile, helper profile, +storage inventory and rank mass plus a passing dense transpose; rejects two controls (a doubled merged coefficient, +a deleted live ADD); and compares [RESULT.json](RESULT.json) in full. Marker: `PASS_P104_ORDINARY_EVENT_COMPRESSION`. + +## Scope and limits + +Only the ordinary alphabet is rewritten. The native maps, the physical caller, the complete invoice, the compiler +and outer checks of PR5907 are untouched and were not rerun here; their inputs (profiles, inventory) are shown +equal. The five inherited framework assumptions remain. This is an agent check, not human acceptance. The selected +record is unchanged. The passes are local and greedy; a global re-synthesis of the ordinary events could free more. + +## Open next questions + +- Does a further-compressed word admit a positive-bill hub or rung removal that the 26,000 cap had blocked? + First step: rerun the #5907 "same rung structure" search on this word with the 137 spare events. + Blocked by: a search over itineraries, not by this package. +- Can a global ordinary re-synthesis (recomputing each register's reads from a minimal set of ADDs) free + substantially more than the peephole passes? First step: count, per register and chart, the rank of the rows + actually read against the number of ADDs spent. Blocked by: nothing; a bounded experiment. +- Should the event cap itself be revisited in the retained contract rather than worked around? First step: a + maintainer statement on which allowance (events, scalar units, labels) is contractual. Blocked by: maintainers. + +## Credit + +DreamingOfClouds (PR5907 word), Ali Romman (PR5827 word, `local.py` checker and the P104 lineage, with OpenAI +Codex assistance), Mason Hale (PR5811), and the P104 native, controller, compiler and analytic contributors credited +in those packages. The hub-search negative result uses the mechanism of Ali Romman's PR5786. Prepared for +Matarener with Claude (Anthropic), via Claude Code. Apache-2.0. diff --git a/research/p104-ordinary-event-compression/RESULT.json b/research/p104-ordinary-event-compression/RESULT.json new file mode 100644 index 0000000000..e1bfa1c771 --- /dev/null +++ b/research/p104-ordinary-event-compression/RESULT.json @@ -0,0 +1,73 @@ +{ + "author_replay": { + "helpers": { + "1": 15, + "2": 7, + "3": 5, + "4": 107, + "5": 14, + "6": 1, + "7": 10, + "8": 18, + "9": 385 + }, + "owned_fields": 29, + "owned_lifetimes": 31, + "paid": { + "1": 2221, + "2": 456, + "3": 498, + "4": 99, + "5": 163, + "6": 10, + "7": 7 + }, + "paid_rank_mass": 5947, + "peak_owned_fields": 13, + "public_inputs": 770, + "real_scalar_allowance": 227372 + }, + "author_replay_source_scalar_allowance": 228664, + "controls": { + "deleted_live_add": "rejected", + "doubled_coefficient": "rejected" + }, + "events_after": 25861, + "events_before": 25998, + "freed": 137, + "ops_after": { + "ADD": 21599, + "CLEAR": 31, + "COPY": 22, + "INIT": 31, + "MOVE": 3454, + "SCALE": 724 + }, + "ops_before": { + "ADD": 21706, + "CLEAR": 31, + "COPY": 23, + "INIT": 31, + "MOVE": 3454, + "SCALE": 753 + }, + "passes": [ + { + "dead": 2, + "events": 25862, + "merged": 98 + }, + { + "dead": 1, + "events": 25861, + "merged": 0 + }, + { + "dead": 0, + "events": 25861, + "merged": 0 + } + ], + "source": "research/p104-helper468-rung-removal/WORD.json.gz", + "word_payload_sha256": "a033f1ef2d7a2767053330ada477d8072687a72df751a0c76407f44fa0880c10" +} diff --git a/research/p104-ordinary-event-compression/SOURCES.json b/research/p104-ordinary-event-compression/SOURCES.json new file mode 100644 index 0000000000..d9bf66c210 --- /dev/null +++ b/research/p104-ordinary-event-compression/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "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" + }, + { + "path": "research/p104-helper468-rung-removal/RESULT.json", + "usage": "input", + "git_blob": "21a900ef8a49eab504cedc5f171a01efaa8a5be1", + "sha256": "577c39f6c9b017a543692e85ac6f497974f561eb197e0e3fad4b50baa72e5f3d" + }, + { + "path": "research/p104-helper468-rung-removal/WORD.json.gz", + "usage": "input", + "git_blob": "7ffe7b500b02b9d0de49a85ec53e36004f1a411f", + "sha256": "b69a9cb3a26d4f40aa7ad14f814b188fe16a782999f6f56292538e447d67b284" + }, + { + "path": "research/p104-unread-path-resynthesis/local.py", + "usage": "input", + "git_blob": "b7be846b10c4c54a4e1558d7b563bc8c3a170223", + "sha256": "7201df8e32f5c99f7403150e8664042322037906088bc754c67293a241368597" + } + ] +} diff --git a/research/p104-ordinary-event-compression/TASK.json b/research/p104-ordinary-event-compression/TASK.json new file mode 100644 index 0000000000..57e14762e1 --- /dev/null +++ b/research/p104-ordinary-event-compression/TASK.json @@ -0,0 +1,129 @@ +{ + "schema_version": 1, + "task_id": "p104-side-correction", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "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": "Semantics-preserving compression of the ordinary (ADD/SCALE/COPY) events of the PR5907 P104 word: 25,998 -> 25,861 events with identical paid and helper profiles, charts, lifetimes and endpoint rows; plus a recorded negative search for further PR5786-style hubs and rank-two shared-subdivision blocks on that word.", + "scope_change_reason": "Side result on the latest conditional P104 word: the 26,000-event cap, not a helper basis or causal split, was the binding constraint; the rewrite frees headroom without changing the invoice.", + "bottleneck_link": "The P104 ladder is limited by the retained 26,000-event cap (PR5907: 25,998). Freed ordinary events are the resource any further helper split needs; the attached hub search shows no positive-bill split on this word even with that headroom.", + "budget_minutes": 240, + "stop_rule": "Stop when the compressed word passes the own replay and the unmodified author checker with equal profiles, and when the hub search has covered all frames and full-boundary helpers.", + "outcome": "completed", + "evidence": "research/p104-ordinary-event-compression/RESULT.json", + "author": "Matarener", + "ai_assistance": "Prepared with Claude (Anthropic) via Claude Code.", + "open_questions": [ + { + "question": "Does the compressed word admit a positive-bill hub or rung removal that the event cap had blocked?", + "why_it_matters": "137 spare events are room for about four more ladder steps of the existing kinds.", + "first_step": "Rerun the PR5907 same-rung-structure search on research/p104-ordinary-event-compression/WORD.json.gz.", + "blocked_by": "An itinerary search, not this package." + }, + { + "question": "Can a global ordinary re-synthesis free substantially more events than the peephole passes?", + "why_it_matters": "More headroom widens every later construction.", + "first_step": "Per register and chart, compare the rank of the rows actually read with the number of ADDs spent.", + "blocked_by": "Nothing; a bounded experiment." + }, + { + "question": "Which allowances (events, scalar units, labels) are contractual in the retained P104 model?", + "why_it_matters": "Working around a non-contractual cap wastes effort; changing a contractual one needs a new admission.", + "first_step": "Maintainer statement in the intake ledger.", + "blocked_by": "Maintainers." + } + ] +} diff --git a/research/p104-ordinary-event-compression/VERIFY.json b/research/p104-ordinary-event-compression/VERIFY.json new file mode 100644 index 0000000000..b0c560b240 --- /dev/null +++ b/research/p104-ordinary-event-compression/VERIFY.json @@ -0,0 +1,22 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-helper468-rung-removal/RESULT.json", + "research/p104-helper468-rung-removal/WORD.json.gz", + "research/p104-unread-path-resynthesis/local.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Authenticate pinned inputs; regenerate the compressed word with compress.py and compare the decompressed payload; own exact replay of both words with identical MOVE/INIT/CLEAR sequences, rows of every moved field and all 799 endpoint rows; PR5827 local.py unmodified: equal paid/helper profiles, inventory, rank mass, passing dense transpose; two rejected controls; RESULT.json compared in full." + } + ] +} diff --git a/research/p104-ordinary-event-compression/WORD.json.gz b/research/p104-ordinary-event-compression/WORD.json.gz new file mode 100644 index 0000000000..63b7b536a4 Binary files /dev/null and b/research/p104-ordinary-event-compression/WORD.json.gz differ diff --git a/research/p104-ordinary-event-compression/compress.py b/research/p104-ordinary-event-compression/compress.py new file mode 100644 index 0000000000..e066ec2c3a --- /dev/null +++ b/research/p104-ordinary-event-compression/compress.py @@ -0,0 +1,98 @@ +#!/usr/bin/env python3 +"""Semantics-preserving peephole compression of a P104 local word. Apache-2.0. + +Prepared for Matarener with Claude (Anthropic), via Claude Code. Standard library only. +Three passes, repeated to a fixed point, change only ordinary ADD/SCALE/COPY/CLEAR events; MOVE, INIT and CLEAR +events, every chart, every owned lifetime and every endpoint row are unchanged: + M1 two ADD r <- s at the same chart with no intervening event that reads or writes r or writes s merge into + one ADD with the summed coefficient (both are deleted when the sum is zero); + M2 two SCALE r with no intervening event touching r merge into one SCALE with the product coefficient; + D1 an ADD/COPY/SCALE into an owned field that is CLEARed before that field is read again is deleted. +compress(word) returns the new word; it is deterministic. The merged coefficients stay dyadic because sums and +products of dyadic rationals are dyadic. +""" +from collections import defaultdict +from fractions import Fraction as Q +from copy import deepcopy + + +def reads_writes(e): + op = e[0] + if op in ('MOVE', 'SCALE'): return {e[1]}, {e[1]} + if op in ('INIT', 'CLEAR'): return set(), {e[1]} + if op == 'COPY': return {e[2]}, {e[1]} + return {e[1], e[2]}, {e[1]} # ADD reads r and s, writes r + + +def pass_merge(prog): + n = len(prog); dead = [False]*n; merged = 0 + last_add, last_scale = {}, {} + for i, e in enumerate(prog): + op = e[0] + if op == 'ADD': + key = (e[1], e[2]); j = last_add.get(key) + if j is not None and prog[j][-1] == e[-1]: + q = Q(prog[j][-2])+Q(e[-2]) + if q == 0: + dead[j] = dead[i] = True; del last_add[key] + else: + prog[j] = ['ADD', e[1], e[2], str(q), e[-1]]; dead[i] = True + merged += 1 + continue + if op == 'SCALE': + j = last_scale.get(e[1]) + if j is not None and prog[j][-1] == e[-1]: + prog[j] = ['SCALE', e[1], str(Q(prog[j][-2])*Q(e[-2])), e[-1]]; dead[i] = True; merged += 1 + continue + rd, wr = reads_writes(e); touched = rd | wr + for key in [k for k in last_add if k[0] in touched or k[1] in wr]: + del last_add[key] + for key in [k for k in last_scale if k in touched]: + del last_scale[key] + if op == 'ADD': last_add[(e[1], e[2])] = i + elif op == 'SCALE': last_scale[e[1]] = i + return [e for e, d in zip(prog, dead) if not d], merged + + +def pass_dead(prog, public): + n = len(prog); dead = [False]*n; count = 0 + pending = defaultdict(list) + for i, e in enumerate(prog): + op, r = e[0], e[1] + if op == 'CLEAR' and r >= public: + for j in pending.pop(r, []): + dead[j] = True; count += 1 + continue + rd, wr = reads_writes(e) + for x in rd: + if x >= public and x in pending: + pending[x] = [] + if op in ('ADD', 'COPY', 'SCALE') and r >= public: + pending[r].append(i) + elif op == 'INIT' and r >= public: + pending[r] = [] + return [e for e, d in zip(prog, dead) if not d], count + + +def compress(word): + prog = [list(e) for e in word['program']] + passes = [] + while True: + before = len(prog) + prog, m = pass_merge(prog) + prog, d = pass_dead(prog, word['public']) + passes.append({'merged': m, 'dead': d, 'events': len(prog)}) + if len(prog) == before and m == 0: + break + out = deepcopy(word) + out['program'] = prog + return out, passes + + +if __name__ == '__main__': + import gzip, json, sys + w = json.loads(gzip.decompress(open(sys.argv[1], 'rb').read())) + out, passes = compress(w) + print(json.dumps(passes)) + if len(sys.argv) > 2: + open(sys.argv[2], 'wb').write(gzip.compress(json.dumps(out, separators=(',', ':')).encode())) diff --git a/research/p104-ordinary-event-compression/verify.py b/research/p104-ordinary-event-compression/verify.py new file mode 100644 index 0000000000..1cc71beeca --- /dev/null +++ b/research/p104-ordinary-event-compression/verify.py @@ -0,0 +1,151 @@ +#!/usr/bin/env python3 +"""Verify the ordinary-event compression of the PR5907 P104 word. Apache-2.0. + +Prepared for Matarener with Claude (Anthropic), via Claude Code. Python 3.12, standard library only. +Checks: (0) pinned live inputs; (1) compress.py regenerates the shipped word (decompressed payload equality); +(2) own exact replay of the source and compressed words: identical MOVE/INIT/CLEAR sequences, identical charts, +identical rows of all 799 roles at every MOVE and at the end; (3) the PR5827 author checker local.py (loaded +unmodified) accepts the compressed word with the same paid profile, helper profile and storage inventory, and its +dense transpose check passes; (4) two controls: a changed merged coefficient and a deleted live ADD are rejected +by the row comparison; (5) RESULT.json equals the recomputed receipt. +""" +from collections import Counter +from fractions import Fraction as Q +from hashlib import sha256 +from pathlib import Path +import gzip, importlib.util, json, sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SOURCE = ROOT/'research/p104-helper468-rung-removal/WORD.json.gz' +LOCAL = ROOT/'research/p104-unread-path-resynthesis/local.py' + + +def need(ok, why): + if not ok: + raise ValueError(why) + + +def read(path): + raw = Path(path).read_bytes() + return json.loads(gzip.decompress(raw) if str(path).endswith('.gz') else raw) + + +def load(name, path): + spec = importlib.util.spec_from_file_location(name, path) + mod = importlib.util.module_from_spec(spec); sys.modules[name] = mod; spec.loader.exec_module(mod) + return mod + + +def span(basis): + s = {0} + for v in basis: + need(type(v) is int and 0 < v < 512 and v not in s, 'independent binary basis') + s |= {x ^ v for x in s} + return frozenset(s) + + +def replay(w): + """Own exact replay: returns (trace of (MOVE/INIT/CLEAR events, rows of the moved role), final rows, charts).""" + S = [span(f) for f in w['frames']] + n, m = w['public'], w['owned_fields'] + cur = list(w['initial'])+[None]*m + rows = [{r: Q(1)} for r in range(n)] + [{} for _ in range(m)] + owned, trace = set(), [] + for i, e in enumerate(w['program']): + op, r = e[0], e[1] + need(0 <= r < n+m, 'role index') + if op == 'MOVE': + a, b, private = e[2], e[3], e[4] + need(cur[r] == a and (r in owned) == private, 'transport source and ownership at %d' % i) + need(S[b] < S[a] if private else S[a] < S[b], 'strict nesting at %d' % i) + trace.append((tuple(e), tuple(sorted(rows[r].items())))) + cur[r] = b + elif op == 'INIT': + need(r >= n and r not in owned, 'owned init'); owned.add(r); rows[r], cur[r] = {}, e[2] + trace.append((tuple(e), ())) + elif op == 'CLEAR': + need(r in owned and cur[r] == e[2], 'owned erasure'); owned.discard(r); rows[r], cur[r] = {}, None + trace.append((tuple(e), ())) + else: + q, f = Q(e[-2]), e[-1] + need(q != 0 and cur[r] == f and q.denominator & (q.denominator-1) == 0, 'ordinary event at %d' % i) + if op == 'SCALE': + rows[r] = {k: q*v for k, v in rows[r].items()} + else: + s = e[2]; need(s != r and cur[s] == f, 'common chart at %d' % i) + if op == 'COPY': + need(r in owned and not rows[r], 'COPY into cleared owned field') + rows[r] = {k: q*v for k, v in rows[s].items()} + else: + need(op == 'ADD', 'opcode') + t = dict(rows[r]) + for k, v in rows[s].items(): + t[k] = t.get(k, 0)+q*v + rows[r] = {k: v for k, v in t.items() if v} + need(not owned and cur[:n] == w['final'], 'exits') + live = set(w['live']) + for r in range(n+m): + expected = {r: Q(1)} if r < n else {} + if r-112 in live: + expected[r-112] = Q(1) + need(rows[r] == expected, 'endpoint row %d' % r) + return trace + + +def main(): + pins = read(HERE/'SOURCES.json') + for row in pins['files']: + if row['usage'] == 'input': + need(sha256((ROOT/row['path']).read_bytes()).hexdigest() == row['sha256'], 'source pin '+row['path']) + source = read(SOURCE) + C = load('p104_event_compress', HERE/'compress.py') + word, passes = C.compress(source) + shipped = read(HERE/'WORD.json.gz') + need(word == shipped, 'regenerated word equals the shipped decompressed payload') + print('regenerated', json.dumps(passes), flush=True) + # (2) own replay: identical paid/owned event sequences and identical rows at every one of them + t0, t1 = replay(source), replay(word) + need(t0 == t1, 'identical MOVE/INIT/CLEAR sequence and identical rows of every moved field') + need(sum(1 for e in word['program'] if e[0] == 'MOVE') == 3454, 'MOVE count') + need({k: v for k, v in source.items() if k != 'program'} == {k: v for k, v in word.items() if k != 'program'}, 'unchanged header') + print('own replay', len(t0), 'paid/owned events compared', flush=True) + # (3) the author checker, loaded unmodified + L = load('p104_local_5827', LOCAL) + before, after = L.replay(source), L.replay(word) + for key in ('paid', 'helpers', 'public_inputs', 'owned_fields', 'owned_lifetimes', 'peak_owned_fields', 'paid_rank_mass'): + need(before[key] == after[key], 'author replay: unchanged '+key) + need(after['real_scalar_allowance'] < before['real_scalar_allowance'], 'scalar allowance does not grow') + L.reverse_columns(word) + print('author checker', {k: after[k] for k in ('paid', 'helpers', 'real_scalar_allowance')}, flush=True) + # (4) controls + def reject(mutant, why): + try: + replay(mutant) + except ValueError: + return + raise ValueError('control accepted: '+why) + bad = json.loads(json.dumps(word)) + i = next(i for i, e in enumerate(bad['program']) if e[0] == 'ADD' and e[1] < word['public']) + bad['program'][i][-2] = str(Q(bad['program'][i][-2])*2) + reject(bad, 'doubled coefficient of a public ADD') + bad = json.loads(json.dumps(word)) + del bad['program'][i] + reject(bad, 'deleted live public ADD') + ops_in, ops_out = Counter(e[0] for e in source['program']), Counter(e[0] for e in word['program']) + result = {'source': 'research/p104-helper468-rung-removal/WORD.json.gz', 'events_before': len(source['program']), + 'events_after': len(word['program']), 'freed': len(source['program'])-len(word['program']), + 'passes': passes, 'ops_before': dict(ops_in), 'ops_after': dict(ops_out), + 'author_replay': {k: after[k] for k in ('paid', 'helpers', 'public_inputs', 'owned_fields', 'owned_lifetimes', 'peak_owned_fields', 'paid_rank_mass', 'real_scalar_allowance')}, + 'author_replay_source_scalar_allowance': before['real_scalar_allowance'], + 'word_payload_sha256': sha256(json.dumps(word, sort_keys=True, separators=(',', ':')).encode()).hexdigest(), + 'controls': {'doubled_coefficient': 'rejected', 'deleted_live_add': 'rejected'}} + result['author_replay'] = {k: ({str(a): b for a, b in v.items()} if isinstance(v, dict) else v) for k, v in result['author_replay'].items()} + if '--write' in sys.argv: + (HERE/'RESULT.json').write_text(json.dumps(result, indent=1, sort_keys=True)+'\n') + need(read(HERE/'RESULT.json') == result, 'RESULT.json equals the recomputed receipt') + print('PASS_P104_ORDINARY_EVENT_COMPRESSION') + + +if __name__ == '__main__': + main()