diff --git a/research/literal-elementary-interchange/PREDECESSOR.json b/research/literal-elementary-interchange/PREDECESSOR.json new file mode 100644 index 0000000000..6bd68fa41c --- /dev/null +++ b/research/literal-elementary-interchange/PREDECESSOR.json @@ -0,0 +1,19 @@ +{ + "pr": 5162, + "head": "ce33bfbf9ec8ecd8b176c74a1b4e2d91daf9c5ed", + "archive": "inputs/pr5162.tar.gz", + "sha256": "eab83a9acc58a4b4dbff383ea2acbfaeeaaead7db47568c19eb5b3a3bcfc60da", + "members": { + "research/standalone-elementary-crt-raw/elementary.py": "746828694062b8f5c7542d5f807622b920a9310108347317d37b5231bf11550b", + "research/standalone-elementary-crt-raw/raw.py": "a9ffd3b53f457003d482dd7bd419f3cedfed4afc3d89ffe4d338956679a5656d", + "research/standalone-elementary-crt-raw/PROOF.md": "db7c44510d30bf218566d2c9e0e8d3fec6cdaefeb13a3a559f5b98d8c4e91856", + "research/standalone-elementary-crt-raw/README.md": "13cdc0078cc048f6e8931ee596e930d43ea07e87cc937f9726ae0e2443805c96", + "research/standalone-elementary-crt-raw/VENDOR.json": "987a372882dbd2765614d06918188e92a87147196274b30e0d1f45e503ae8376", + "research/standalone-elementary-crt-raw/vendor/NOTICE.md": "c446b32b8a621844fb2fbe654810c8122035bdd43fed2132f1137d98cb6f9943", + "research/standalone-elementary-crt-raw/vendor/bitstream.py": "f78bac9641007dbd8824984edcac057274fe016ce78bd9cb512d0c0913274783", + "research/standalone-elementary-crt-raw/vendor/cardinality.py": "505d5e560c5a507e6184edcc19a87cf1fed243eb34a5cb21fbe1e4fe017e7f22", + "research/standalone-elementary-crt-raw/vendor/stream.py": "c7dc7da5b00f27016982ada4c0416f8328568b00df16d97012f33d4b372d79b5", + "research/standalone-elementary-crt-raw/vendor/records.py": "0c9c4b23e998597fb877bb1a29da69ac869b68262abe635b162b4dba9c69b372", + "research/standalone-elementary-crt-raw/vendor/words.py": "5c37f57708ba3131bdcb03139f9dbc29886bee44569c09cbba51b68f75acd7f9" + } +} diff --git a/research/literal-elementary-interchange/PROOF.md b/research/literal-elementary-interchange/PROOF.md new file mode 100644 index 0000000000..d4e14bba3f --- /dev/null +++ b/research/literal-elementary-interchange/PROOF.md @@ -0,0 +1,157 @@ +# Complete local-symbol elementary interchange + +JoyboyBrian, with substantial OpenAI Codex assistance. Apache-2.0. + +## Domain and endpoint + +Let H>=0 and A,G,S>=1 be arbitrary integers and V=A*4^H*G*S. +Five disjoint borrowed tapes contain SOURCE's V opaque binary cells and the +canonical little-endian words H,A,G,S. Each has LEFT at position0 and head1; +numbers have RIGHT after their most significant bit (zero is 0 RIGHT), and all +bodies have blank tails. Fifteen disjoint private tapes are initially entirely +blank with head0. External tapes are disjoint from every private tape. Input +initialization is supplied, not free production of these tapes. A caller with +preexisting erased backing may use it; its capacity is not credited as zero. + +For every such input, init then run halts returned. SOURCE and all four words +are byte-for-byte unchanged, heads1. OUTPUT is a distinct owned V-bit body +with head1. Every other private tape has only its LEFT marker and blank body, +head1. At indices (a,x,g,y,s), with x,y in [0,2^H), output is the source bit at +(a,y,g,x,s). After the caller consumes OUTPUT by the included consume entry, +run may repeat on these same roles with any new admitted borrowed tapes. close +then erases all15 owned markers and returns all private heads1. No malformed +input rejection rollback or external alias detection is promised. + +## What the executable is + +program.assemble executes once offline. Its result has4589 instructions and +five entries; this word is independent of H,A,G,S and payload bits. Assembly +helpers, lambdas and Python loops do not survive into the machine. The only +instructions are test(role,symbol,yes,no), write(role,symbol), move(role,+/-1), +jump(pc), and halt(status). Role names and five symbols0,1,LEFT,RIGHT,BLANK are +finite constants. test performs exactly one local read. No arithmetic, +copy, counter, permutation, method call or allocator opcode exists. The PC +encodes finite carries and route choices. Host integers for heads/PC/censuses +are simulator configuration and observers, never decoded tape operands. +The all-width theorem concerns unbounded program semantics. execute's finite +max_steps is an observer watchdog and may abort a larger admitted instance. + +This is a five-symbol multitape program over binary payloads, not a supplied +implementation over a two-symbol tape alphabet. A separate fixed-block binary +alphabet translation remains open. The result does replace the entire source +callee's host control, including arithmetic and scratch selection. + +## Primitive invariants + +rewind moves left until the owned/borrowed LEFT marker, then right once. clear +first rewinds, overwrites each body symbol up to the first BLANK, then rewinds. +It preserves retained backing. copy(source,target,end) traverses only binary +body symbols, checks each destination cell blank, writes the same bit, and +returns both heads. For a number it appends RIGHT; for a payload it leaves the +blank tail. Its target must be empty. All uses satisfy this premise. + +zero branches true precisely on 0 RIGHT and restores head1 on both branches. +All number words used with it remain canonical. normalize scans to RIGHT, +replaces high zero cells by RIGHT while erasing the previous delimiter; if the +word becomes empty, it writes 0 RIGHT. dec is called only on a positive number: +it changes low zeros to ones up to the first one, changes that one to zero, +then normalizes. This is subtraction of one, including powers of two and one. + +double shifts the little-endian bit stream by one place. Two PC states carry +the old preceding bit, starting at0. At RIGHT a carry1 becomes the new high bit +and a new RIGHT is written. Every use is positive, hence the resulting word +is canonical. half requires the low bit0, then copies each next bit one cell +left and moves the delimiter left, erasing its former cell. Every use divides +an even positive value, so its high bit remains1 and its result is positive. + +counted(number,counter,body) clones the number to an empty dedicated counter, +tests zero, executes body and dec until zero, then clears it. Its source is +preserved. Bodies never alias their enclosing counter. The three nested +counter roles OUTER,BETWEEN,BITS are distinct; all sequential invocations +reuse them only after clear. No depth or role inventory depends on values. + +## Complete digit pass and all-width induction + +PRE,GAP,TAIL have values P,M,T. digit reads order (p,a,m,b,t), a,b in{0,1}, +into four separate queues Qab in order(p,m,t), each of length P*M*T. Each read +and append is performed by counted loops and literal instructions. The second +traversal reads Qba in order(p,a,m,b,t); consequently it swaps those two binary +digits while retaining spectators. It checks source and each queue end, +restores source head, clears queues, and returns the new body head1. Total +volume is4PMT; opaque bits never determine a route or numerical counter. + +SCAN starts at H. It decrements once before each potential doubling, and stops +if zero. Thus GAP=G*2^max(H-1,0), TAIL=S*2^max(H-1,0), PRE=A. REMAIN starts atH. +The first pass uses SOURCE and B0. Subsequent passes alternate B0/B1; each +clears the consumed owned buffer before reuse. Before pass i>0, PRE doubles +and TAIL halves. Therefore at pass i=0,...,H-1: + + PRE=A*2^i, GAP=G*2^(H-1), TAIL=S*2^(H-1-i). + +TAIL is even precisely whenever the next half is taken. Each pass has volume +4*PRE*GAP*TAIL=V. This is exactly the retained atom_swap/digit_swap digit +schedule specialized to q=2, or PR5162 Elementary.run's encoded-H schedule. +The retained source proof's index induction exchanges the two H-bit blocks +in H adjacent digit-pair passes; no new source ordering or padding is assumed. +The program duplicates three finite pass bodies for SOURCE/B0/B1, not H +bodies. H=0 takes the SOURCE return branch and copies to a distinct OUTPUT. +At H>0 the selected owned buffer is copied to OUTPUT and cleared. PRE,GAP, +TAIL,REMAIN are then cleared. This proves the endpoint and repeat-call +invariant. init and close explicitly create and remove all15 markers. + +PREDECESSOR.json pins the exact PR5162 export and all cited source members. +The original vendor notices are inside that unchanged archive. Verification +authenticates it before reading the source. It is evidence for the written +refinement, not a hidden runtime source executor. + +## Complete price and capacity boundary + +Let L=H+bitlen(H)+bitlen(A)+bitlen(G)+bitlen(S)+8, with bitlen(0)=1. +Every numerical body in the proof has length at most L. For example GAP and +TAIL add at most H-1 bits and PRE at most H-1. Each rewind/clear/copy, +normalization/decrement, double/half of a number uses fewer than128(L+1) +literal instructions, by summing the displayed tests, moves, writes and +jumps per scanned cell, including origin/delimiter branches. + +A digit pass traverses2V payload bits. There are at most2V suffix countdown +iterations; enclosing outer/between iterations and counter constructions +are at most8(V+1), since A,G,S and the intermediate extents are positive. +Payload transfer contributes fewer than16(V+1) instructions. Queue clearing +and source/queue returns together traverse fewer than8(V+1) cells. Charging +all these, including countdown setup/normalization/clear, gives the safe +bound4096(V+1)(L+1) instructions per digit pass. Descriptor setup and SCAN +cost at most1024(H+1)(L+1)^2. Updating PRE/TAIL is at most256(L+1) per pass. +Final output transport, clearing the final buffer, caller consume (or paid source installation) and owned +marker disposal cost at most128(V+L+1). These inequalities are conservative +termwise loop bounds, not inferred from elapsed time or finite fixtures. + +In particular the complete init/run/consume/close session is bounded by + + T <= 2^20 * (H+1) * (V+1) * (L+1)^2. + +The finite admission checker independently excludes control-only cycles. +For this word, at most two jumps occur between cell instructions or halt; +thus T<=3(C+k), where C counts actual reads+writes+unit moves and k +is the number of executed entries in the session (k=1 for one execute call). +Tests are paid reads even when merely checking a precondition. +Successful output computation is priced with caller consumption/disposal, +not only the routing core. Reusing a live initialized owner omits only its +already-paid init and eventual close; all per-call costs remain. + +Fifteen private roles is an exact inventory, not a bound on total retained +backing under arbitrary histories. clear does not shrink arrays; total +backing-space grants remain a separate obligation. Simulator allocation and +wall time are not the local-symbol model's instruction price. + +## Actual caller and limits + +The actual PR5162 raw u/back descriptor is H2,A1,G1024,S12, V196608. +The verifier executes the same whole literal callee, compares every output +bit with the independent address permutation and also executes a paid +copy-back to the original source port before disposal in the caller probe. +That extra caller transport is separately metered. No raw12-shear replay, +ROM producer, repair, current selected/native supplier, all-size CRT/full E, +precision, outer multiplication or improved kappa is asserted here. + +Finite single-column and adversarial controls corroborate this written proof; +they do not prove its quantified claims or confer human/kernel acceptance. diff --git a/research/literal-elementary-interchange/README.md b/research/literal-elementary-interchange/README.md new file mode 100644 index 0000000000..b8305335be --- /dev/null +++ b/research/literal-elementary-interchange/README.md @@ -0,0 +1,41 @@ +# Literal all-width elementary interchange + +PR5162's standalone component still executes counters, routing and scratch +selection through Python methods. This package replaces the complete callee +with one4589-instruction local-symbol program, independent of encoded input +width and spectator sizes. No source method, numeric loop bound or allocator +callback survives at runtime. + +For H>=0,A/G/S>=1 and V=A*4^H*G*S binary payload cells, the written refinement +proves exchange of the two H-bit fields, borrowed preservation, a distinct +owned output and repeatable cleanup on15 private tapes. H=0 is a paid owned +identity. The static opcode admission/CFG checker gives at most two free +jumps between charged cell operations. The complete source-sized u/back call +H2/A1/G1024/S12 also includes literal caller copy-back and terminal disposal. + +Run `python3 -B research/literal-elementary-interchange/verify.py`. +PROOF.md states the quantified domain, full conservative price and limitations; +RESULT.json records the finite evidence. PREDECESSOR.json pins the unchanged +PR5162 official export, including its original vendor notices and the retained +PR2809 sources. SOURCES.json pins the original CRT context. Frozen predecessors +and selected result are unchanged. + +The model has five local symbols and binary payloads. It does not silently +claim a two-symbol tape implementation, a total retained-backing bound, a +literal whole raw/repair caller, ROM production, native/selected admission, +all-size multiplication or a new kappa. Input descriptors and valid disjoint +ports are supplied. Error rollback is not promised. Finite checks support the +written source refinement; independent human/kernel acceptance is unclaimed. + +## Open next questions + +- Give a fixed-block two-symbol encoding and actual alignment microprogram. +- Prove a total retained-backing grant across varying call histories, including + erased arrays; fixed tape count alone does not give that bound. +- Compose the complete raw rotation/ROM and repair programs with this callee, + retaining all original input/output and lifecycle costs. + +Credit Jose Manuel's physical ordinary wrapper; retained PR2809/PR2753 +stream/cardinality authors; Cinna Davis's CRT construction; Hiroki KUMAZAKI's +repair lineage; Douglas Colkitt and all archived notices. JoyboyBrian with +substantial OpenAI Codex assistance. Apache-2.0. diff --git a/research/literal-elementary-interchange/RESULT.json b/research/literal-elementary-interchange/RESULT.json new file mode 100644 index 0000000000..d2f4588b53 --- /dev/null +++ b/research/literal-elementary-interchange/RESULT.json @@ -0,0 +1,273 @@ +{ + "status": "PASS_LITERAL_ELEMENTARY_INTERCHANGE", + "sources": { + "archive": "eab83a9acc58a4b4dbff383ea2acbfaeeaaead7db47568c19eb5b3a3bcfc60da", + "source_files": 4 + }, + "program_sha256": "479f477b1e94564ea6abbad304095dc266db50dc0eb1318a94e980c8ee354052", + "code_sha256": { + "program.py": "3b83fbe3451000b00030ff3156222def23ce15d17d00c7d09a324aea5fd92e72", + "machine.py": "66b5c371ff4aebd4391d71b95c59769a067e0a04910521b4881f074f986327bf" + }, + "controls": { + "fixtures": [ + { + "geometry": [ + 0, + 1, + 1, + 1 + ], + "bits": 1, + "private_roles": 15, + "program_length": 4589, + "control_factor": 3, + "calls": 1, + "install": false, + "actions": { + "steps": 401, + "reads": 155, + "writes": 52, + "moves": 143 + }, + "bound_per_session": 354418688, + "output_sha256": "6e340b9cffb37a989ca544e6bb780a2c78901d3fb33738768511a30617afa01d" + }, + { + "geometry": [ + 1, + 1, + 1, + 1 + ], + "bits": 4, + "private_roles": 15, + "program_length": 4589, + "control_factor": 3, + "calls": 1, + "install": false, + "actions": { + "steps": 1865, + "reads": 689, + "writes": 210, + "moves": 685 + }, + "bound_per_session": 2055208960, + "output_sha256": "6b1e73a0094b7b812d3b9e22cffb4f8239319847522c4fa103753b6950020f93" + }, + { + "geometry": [ + 2, + 1, + 1, + 1 + ], + "bits": 16, + "private_roles": 15, + "program_length": 4589, + "control_factor": 3, + "calls": 1, + "install": false, + "actions": { + "steps": 9099, + "reads": 3289, + "writes": 970, + "moves": 3237 + }, + "bound_per_session": 13690208256, + "output_sha256": "b116e45eaf1b476c2c6b66757035eba3b79f07c00af9161dfe2bb0869c6179f9" + }, + { + "geometry": [ + 3, + 1, + 1, + 1 + ], + "bits": 64, + "private_roles": 15, + "program_length": 4589, + "control_factor": 3, + "calls": 1, + "install": false, + "actions": { + "steps": 43055, + "reads": 15577, + "writes": 4396, + "moves": 14985 + }, + "bound_per_session": 78790000640, + "output_sha256": "6f051a17203e354410ba802c49c1db4e126b85b2ed0f88fdd439a3160b1ed91a" + }, + { + "geometry": [ + 4, + 1, + 1, + 1 + ], + "bits": 256, + "private_roles": 15, + "program_length": 4589, + "control_factor": 3, + "calls": 1, + "install": false, + "actions": { + "steps": 202935, + "reads": 73719, + "writes": 19746, + "moves": 69681 + }, + "bound_per_session": 486418677760, + "output_sha256": "64a60276a3bcb19abb3dd1e7cb6daee2a4cb2ef3f8b7f639ef30492288af4105" + }, + { + "geometry": [ + 5, + 1, + 1, + 1 + ], + "bits": 1024, + "private_roles": 15, + "program_length": 4589, + "control_factor": 3, + "calls": 1, + "install": false, + "actions": { + "steps": 946991, + "reads": 345345, + "writes": 87512, + "moves": 322237 + }, + "bound_per_session": 2579496960000, + "output_sha256": "9eef12733c42364563e20230673a47ad93617ae95e4caaa5a8b204bbfa55bae8" + }, + { + "geometry": [ + 0, + 2, + 3, + 2 + ], + "bits": 12, + "private_roles": 15, + "program_length": 4589, + "control_factor": 3, + "calls": 1, + "install": false, + "actions": { + "steps": 695, + "reads": 258, + "writes": 80, + "moves": 227 + }, + "bound_per_session": 3489660928, + "output_sha256": "cc46f022593abeb3274b1b5d96eae89311ac783315555e07caf8241a81988235" + }, + { + "geometry": [ + 1, + 2, + 3, + 2 + ], + "bits": 48, + "private_roles": 15, + "program_length": 4589, + "control_factor": 3, + "calls": 1, + "install": false, + "actions": { + "steps": 11398, + "reads": 4124, + "writes": 1174, + "moves": 3923 + }, + "bound_per_session": 29697769472, + "output_sha256": "d69fa05dce9a0ae592cff765b37341f4b3d7edb325ddbc20fff22fd84d2a7e4a" + }, + { + "geometry": [ + 2, + 2, + 2, + 3 + ], + "bits": 192, + "private_roles": 15, + "program_length": 4589, + "control_factor": 3, + "calls": 1, + "install": false, + "actions": { + "steps": 65241, + "reads": 24194, + "writes": 6044, + "moves": 21905 + }, + "bound_per_session": 219172306944, + "output_sha256": "3c90705e2ea62888cd5506280bb464d96ad319928214b32e7f98cf80cd9423fc" + }, + { + "geometry": [ + 3, + 1, + 2, + 1 + ], + "bits": 128, + "private_roles": 15, + "program_length": 4589, + "control_factor": 3, + "calls": 1, + "install": false, + "actions": { + "steps": 83044, + "reads": 30088, + "writes": 8324, + "moves": 28771 + }, + "bound_per_session": 175305129984, + "output_sha256": "837b0b7ab3f34e616bed5b38d56e03f7bbf239f88ca348f63cbdf7ede0cd928f" + } + ], + "independent_columns": 24, + "repeated_calls": 3, + "rejections": [ + "wrong_queue_read", + "missing_prefix_update", + "missing_owned_erase", + "host_callback_opcode", + "zero_cell_cycle", + "bool_pc", + "boolean_receipt", + "float_receipt", + "source_corruption", + "missing_RESULT_process", + "missing_SOURCES_process" + ] + }, + "actual": { + "geometry": [ + 2, + 1, + 1024, + 12 + ], + "bits": 196608, + "private_roles": 15, + "program_length": 4589, + "control_factor": 3, + "calls": 1, + "install": true, + "actions": { + "steps": 64320991, + "reads": 23811838, + "writes": 4768396, + "moves": 20719513 + }, + "bound_per_session": 520140364972032, + "output_sha256": "3dfc38046f77606b81982bd6c956480fcee9aca0ff1d8587025abe7bf504b81b" + } +} diff --git a/research/literal-elementary-interchange/SOURCES.json b/research/literal-elementary-interchange/SOURCES.json new file mode 100644 index 0000000000..9aa185ce19 --- /dev/null +++ b/research/literal-elementary-interchange/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13", + "files": [ + { + "path": "research/unconditional-batched-crt/CRT.md", + "usage": "input", + "sha256": "02c3a1e38cbee25aefe2640cc72676da62ba10eb7519fbcb9adb9d48b74eff2b", + "git_blob": "d98dd8e368431cac33d5fc1c8c336696663641d6" + }, + { + "path": "research/unconditional-batched-crt/NOTICE.md", + "usage": "input", + "sha256": "924109837e71c52392191710d49c9deb42780878d1094f0b01e8690dbe799461", + "git_blob": "886a8fdee275f01b459cbd68ae2815dc9269502f" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395" + } + ] +} diff --git a/research/literal-elementary-interchange/TASK.json b/research/literal-elementary-interchange/TASK.json new file mode 100644 index 0000000000..dbecea0447 --- /dev/null +++ b/research/literal-elementary-interchange/TASK.json @@ -0,0 +1,87 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test.", + "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision", + "4100", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Complete all-width local-symbol elementary interchange and actual CRT u/back caller", + "scope_change_reason": "PR5162 supplies source-operation semantics but explicitly leaves complete finite instruction lowering open.", + "bottleneck_link": "Replace host-controlled counters and routing by one fixed literal program at the actual source callee.", + "budget_minutes": 60, + "stop_rule": "Stop on source callbacks, decoded cardinalities, variable role inventory or missing all-width refinement.", + "outcome": "completed", + "evidence": "PROOF.md, verify.py, RESULT.json, VALIDATION.md", + "author": "JoyboyBrian", + "ai_assistance": "Substantial OpenAI Codex assistance and separate agent review; no independent human or proof-kernel acceptance.", + "open_questions": [ + { + "question": "Lower five symbols to a two-symbol tape alphabet.", + "why_it_matters": "The current program is literal over a finite five-symbol alphabet.", + "first_step": "Give fixed block encoding and head-alignment microprogram.", + "blocked_by": "Explicit representation refinement." + }, + { + "question": "Bound retained backing across varying call histories.", + "why_it_matters": "Erased backing remains allocated.", + "first_step": "Sum per-role high-water extents.", + "blocked_by": "Separate capacity proof." + }, + { + "question": "Compile the complete raw/repair caller.", + "why_it_matters": "This callee does not lower ROM rotation or repair.", + "first_step": "Compose compatible finite programs and full ownership.", + "blocked_by": "Distinct caller contracts." + } + ], + "coordination": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4709#discussioncomment-19144824" +} diff --git a/research/literal-elementary-interchange/VALIDATION.md b/research/literal-elementary-interchange/VALIDATION.md new file mode 100644 index 0000000000..caee60ee37 --- /dev/null +++ b/research/literal-elementary-interchange/VALIDATION.md @@ -0,0 +1,48 @@ +# Validation evidence + +The author normal verifier passed under CPython3.14.6 on macOS arm64 in +5.4531 seconds. Command: `python3 -B +research/literal-elementary-interchange/verify.py --write-result`. Authoring +mode executes every check and changes only receipt writing versus comparison. + +The whole actual H2/A1/G1024/S12 caller session executes64,320,991 literal +instructions:23,811,838 reads,4,768,396 writes and20,719,513 unit moves, with +15 private roles. This includes initialization, whole callee, paid installation +back to the original source port and disposal. The fixed4589-instruction +program is identical for every fixture. Its maximum zero-cell jump chain is2. + +Light controls cover widths0..5, nontrivial spectators,24 independent columns, +three successive calls on one owner, exact borrowed bytes/heads and private +blank backing. An actual wrong queue read, omitted prefix doubling and omitted +owned-buffer erase reject. The first queue-read control targeted a harmless +marker branch; it was replaced before the frozen run by a payload read and a +discriminating single-column witness. Invalid host-call and zero-cell-cycle +programs reject. Integer-to-Boolean/float receipt changes reject by canonical +JSON. Actual altered archive bytes reject; fresh processes reject missing +RESULT.json and SOURCES.json before scientific execution. All scientific +checks use explicit exceptions, independent of Python assert semantics. + +The complete all-width statement is the written PROOF.md refinement, not an +inference from these finite examples. Exact predecessor files are retained +inside their unchanged official export; they are not invoked as hidden +machine operations. Five-symbol control, supplied input tapes and the absence +of a total retained-backing bound remain explicit limitations. + +Independent agent source review found no blocker within the typed successful +domain. It authenticated the retained digit schedule and independently checked +259 cases each of double/half/decrement (including100-bit values), a small +installed H2/A2/G1/S3 caller and static4589/D3 control. It corrected two proof +bookkeeping statements: there are five named entries, and the multi-entry +CFG bound is3(C+k). These are prose corrections; executable/receipt bytes did +not change. This is agent review, not independent human/kernel acceptance. + +Committed-byte/source-history, metadata and official export checks passed at +f4f22bfa5ce59c10f1b7fa48077b9401b3007ec1. Its frozen archive SHA256 was +bd0f072f591be6bb77684520090e1241058d9bcec9c9340ad9eaea2c2ff1b1ce. +A fresh Git-free extraction ran /opt/local/bin/python3.12 -O -B +research/literal-elementary-interchange/verify.py, CPython3.12.2, empty PATH +and PYTHONDONTWRITEBYTECODE=1, under a hard30s timeout. It passed in5.9944s +whole-process time, all15 exported files unchanged. The final amendment changes +only PROOF.md bookkeeping/watchdog wording and this validation prose; +scientific code, inputs and RESULT remain the exact cold-verified bytes. +No raw12/repair/selected/native replay was run. diff --git a/research/literal-elementary-interchange/VERIFY.json b/research/literal-elementary-interchange/VERIFY.json new file mode 100644 index 0000000000..40b570cb87 --- /dev/null +++ b/research/literal-elementary-interchange/VERIFY.json @@ -0,0 +1,31 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/unconditional-batched-crt/CRT.md", + "research/unconditional-batched-crt/NOTICE.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Exact source authentication, finite-program admission and semantic mutants, repeated lifecycle, full actual196608bit caller and typed receipt." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Identical complete checks under optimized Python." + } + ] +} diff --git a/research/literal-elementary-interchange/inputs/pr5162.tar.gz b/research/literal-elementary-interchange/inputs/pr5162.tar.gz new file mode 100644 index 0000000000..3d217d3a0e Binary files /dev/null and b/research/literal-elementary-interchange/inputs/pr5162.tar.gz differ diff --git a/research/literal-elementary-interchange/machine.py b/research/literal-elementary-interchange/machine.py new file mode 100644 index 0000000000..78dc14bf1c --- /dev/null +++ b/research/literal-elementary-interchange/machine.py @@ -0,0 +1,55 @@ +"""One local-symbol instruction per step. No runtime assembly/source callbacks.""" +from program import ROLES,BLANK + +def validate(code,entries): + for pc,row in enumerate(code): + op,*a=row + if op=='test': + if len(a)!=4 or a[0] not in ROLES or type(a[1]) is not int or not 0<=a[1]<=4:raise ValueError('test domain') + targets=a[2:] + elif op=='write': + if len(a)!=2 or a[0] not in ROLES or type(a[1]) is not int or not 0<=a[1]<=4:raise ValueError('write domain') + targets=[] + elif op=='move': + if len(a)!=2 or a[0] not in ROLES or type(a[1]) is not int or a[1] not in (-1,1):raise ValueError('move domain') + targets=[] + elif op=='jump': + if len(a)!=1:raise ValueError('jump arity') + targets=a + elif op=='halt': + if len(a)!=1 or a[0] not in ('initialized','returned','consumed','installed','closed','rejected'):raise ValueError('halt domain') + targets=[] + else:raise ValueError('nonliteral instruction') + if op in ('write','move') and pc+1>=len(code):raise ValueError('fallthrough boundary') + if any(type(t) is not int or not 0<=t=len(cells):cells.extend([BLANK]*(h+1-len(cells))) + cells[h]=s;writes+=1;pc+=1 + elif op=='move': + _,r,d=row;h=heads[r]+d + if h<0:raise ValueError('left boundary') + heads[r]=h;moves+=1;pc+=1 + elif op=='jump':pc=row[1] + elif op=='halt':return {'status':row[1],'steps':steps,'reads':reads,'writes':writes,'moves':moves} + else:raise ValueError('invalid opcode') + raise ValueError('observer watchdog') diff --git a/research/literal-elementary-interchange/program.py b/research/literal-elementary-interchange/program.py new file mode 100644 index 0000000000..c606ed51a0 --- /dev/null +++ b/research/literal-elementary-interchange/program.py @@ -0,0 +1,132 @@ +"""Static local-symbol program for encoded binary elementary interchange. +JoyboyBrian, with substantial OpenAI Codex assistance. Apache-2.0. +Assembly helpers run only before execution; no helper survives as an opcode. +""" +ZERO,ONE,LEFT,RIGHT,BLANK=range(5) +BORROWED=('SOURCE','H','A','G','S') +PRIVATE=('PRE','GAP','TAIL','SCAN','REMAIN','OUTER','BETWEEN','BITS','Q00','Q01','Q10','Q11','B0','B1','OUTPUT') +ROLES=BORROWED+PRIVATE + +class Builder: + def __init__(self):self.code=[];self.labels={};self.serial=0 + def fresh(self):self.serial+=1;return 'L'+str(self.serial) + def mark(self,label):self.labels[label]=len(self.code) + def emit(self,*x):self.code.append(x) + def jump(self,label):self.emit('jump',label) + def test(self,role,symbol,yes,no):self.emit('test',role,symbol,yes,no) + def write(self,role,symbol):self.emit('write',role,symbol) + def move(self,role,d):self.emit('move',role,d) + def require(self,role,symbol): + ok=self.fresh();self.test(role,symbol,ok,'reject');self.mark(ok) + def rewind(self,role): + loop,end=self.fresh(),self.fresh();self.move(role,-1);self.mark(loop) + more=self.fresh();self.test(role,LEFT,end,more);self.mark(more);self.move(role,-1);self.jump(loop);self.mark(end);self.move(role,1) + def clear(self,role): + self.rewind(role);loop,end,body=self.fresh(),self.fresh(),self.fresh();self.mark(loop) + self.test(role,BLANK,end,body);self.mark(body);self.write(role,BLANK);self.move(role,1);self.jump(loop);self.mark(end);self.rewind(role) + def copy(self,source,target,end_symbol): + loop,end,z,o=self.fresh(),self.fresh(),self.fresh(),self.fresh();self.mark(loop) + bit=self.fresh();self.test(source,end_symbol,end,bit);self.mark(bit) + self.test(source,ZERO,z,o);self.mark(z);self.require(target,BLANK);self.write(target,ZERO);next_=self.fresh();self.jump(next_) + self.mark(o);self.require(source,ONE);self.require(target,BLANK);self.write(target,ONE);self.mark(next_) + self.move(source,1);self.move(target,1);self.jump(loop);self.mark(end) + self.rewind(source) + if end_symbol==RIGHT:self.write(target,RIGHT) + self.rewind(target) + def zero(self,role,yes,no): + # Canonical number: only the word 0 RIGHT denotes zero. + z=self.fresh();self.test(role,ZERO,z,no);self.mark(z);self.move(role,1) + restore_y,restore_n=self.fresh(),self.fresh();self.test(role,RIGHT,restore_y,restore_n) + self.mark(restore_y);self.move(role,-1);self.jump(yes) + self.mark(restore_n);self.move(role,-1);self.jump(no) + def normalize(self,role): + self.rewind(role);loop,end,body=self.fresh(),self.fresh(),self.fresh();self.mark(loop) + self.test(role,RIGHT,end,body);self.mark(body);self.move(role,1);self.jump(loop);self.mark(end);self.move(role,-1) + trim,stop,erase=self.fresh(),self.fresh(),self.fresh();self.mark(trim);self.test(role,ZERO,erase,stop) + self.mark(erase);self.write(role,RIGHT);self.move(role,1);self.write(role,BLANK);self.move(role,-1);self.move(role,-1);self.jump(trim) + self.mark(stop);empty,done=self.fresh(),self.fresh();self.test(role,LEFT,empty,done) + self.mark(empty);self.move(role,1);self.write(role,ZERO);self.move(role,1);self.write(role,RIGHT);self.mark(done);self.rewind(role) + def dec(self,role): + loop,one,zero=self.fresh(),self.fresh(),self.fresh();self.mark(loop);self.test(role,ZERO,zero,one) + self.mark(zero);self.write(role,ONE);self.move(role,1);self.jump(loop) + self.mark(one);self.require(role,ONE);self.write(role,ZERO);self.normalize(role) + def double(self,role): + # Shift a canonical LE positive word right using finite carry in PC. + self.rewind(role) + states=[self.fresh(),self.fresh()];done=self.fresh();self.jump(states[0]) + for carry in (0,1): + self.mark(states[carry]);end,z,o=self.fresh(),self.fresh(),self.fresh();bit=self.fresh() + self.test(role,RIGHT,end,bit);self.mark(bit);self.test(role,ZERO,z,o) + self.mark(z);self.write(role,carry);self.move(role,1);self.jump(states[0]) + self.mark(o);self.require(role,ONE);self.write(role,carry);self.move(role,1);self.jump(states[1]) + self.mark(end) + if carry:self.write(role,ONE);self.move(role,1);self.write(role,RIGHT) + self.jump(done) + self.mark(done);self.rewind(role) + def half(self,role): + self.require(role,ZERO);self.move(role,1);loop=self.fresh();self.mark(loop) + end,z,o=self.fresh(),self.fresh(),self.fresh();bit=self.fresh();self.test(role,RIGHT,end,bit);self.mark(bit);self.test(role,ZERO,z,o) + nxt=self.fresh() + for label,symbol in ((z,ZERO),(o,ONE)): + self.mark(label);self.require(role,symbol);self.move(role,-1);self.write(role,symbol);self.move(role,1);self.move(role,1);self.jump(nxt) + self.mark(nxt);self.jump(loop);self.mark(end);self.write(role,BLANK);self.move(role,-1);self.write(role,RIGHT);self.rewind(role) + def counted(self,number,counter,body): + self.copy(number,counter,RIGHT);loop,end,work=self.fresh(),self.fresh(),self.fresh();self.mark(loop);self.zero(counter,end,work) + self.mark(work);body();self.dec(counter);self.jump(loop);self.mark(end);self.clear(counter) + def block(self,source,target): + def bit(): + z,o,nxt=self.fresh(),self.fresh(),self.fresh();self.test(source,ZERO,z,o) + for label,symbol in ((z,ZERO),(o,ONE)): + self.mark(label);self.require(source,symbol);self.require(target,BLANK);self.write(target,symbol);self.jump(nxt) + self.mark(nxt);self.move(source,1);self.move(target,1) + self.counted('TAIL','BITS',bit) + def digit(self,source,target): + def outer_in(): + for a in range(2):self.counted('GAP','BETWEEN',lambda a=a:[self.block(source,'Q'+str(a)+str(b)) for b in range(2)]) + self.counted('PRE','OUTER',outer_in);self.require(source,BLANK);self.rewind(source) + for q in ('Q00','Q01','Q10','Q11'):self.rewind(q) + def outer_out(): + for a in range(2):self.counted('GAP','BETWEEN',lambda a=a:[self.block('Q'+str(b)+str(a),target) for b in range(2)]) + self.counted('PRE','OUTER',outer_out) + for q in ('Q00','Q01','Q10','Q11'):self.require(q,BLANK);self.clear(q) + self.rewind(target) + def finish(self): + code=[] + for op,*a in self.code: + if op=='jump':a=[self.labels[a[0]]] + elif op=='test':a[-2:]=[self.labels[x] for x in a[-2:]] + code.append((op,*a)) + return tuple(code) + +def assemble(): + b=Builder();entries={} + entries['init']=len(b.code) + for r in PRIVATE:b.require(r,BLANK);b.write(r,LEFT);b.move(r,1) + b.emit('halt','initialized');entries['run']=len(b.code) + for r in PRIVATE:b.require(r,BLANK) + for src,dst in (('A','PRE'),('G','GAP'),('S','TAIL'),('H','SCAN')):b.copy(src,dst,RIGHT) + # SCAN decremented once before each doubling, yielding max(H-1,0). + scan,end,work,again=b.fresh(),b.fresh(),b.fresh(),b.fresh();b.mark(scan);b.zero('SCAN',end,work) + b.mark(work);b.dec('SCAN');b.zero('SCAN',end,again);b.mark(again);b.double('GAP');b.double('TAIL');b.jump(scan);b.mark(end);b.clear('SCAN') + b.copy('H','REMAIN',RIGHT) + loops=[b.fresh() for _ in range(3)];ends=[b.fresh() for _ in range(3)] + b.jump(loops[0]) + for i,(src,dst,next_i) in enumerate((('SOURCE','B0',1),('B0','B1',2),('B1','B0',1))): + b.mark(loops[i]);work=b.fresh();b.zero('REMAIN',ends[i],work);b.mark(work) + if i:b.double('PRE');b.half('TAIL') + b.digit(src,dst) + if i:b.clear(src) + b.dec('REMAIN');b.jump(loops[next_i]) + done=b.fresh() + for i,src in enumerate(('SOURCE','B0','B1')): + b.mark(ends[i]);b.copy(src,'OUTPUT',BLANK) + if i:b.clear(src) + b.jump(done) + b.mark(done) + for r in ('PRE','GAP','TAIL','REMAIN'):b.clear(r) + b.emit('halt','returned');entries['consume']=len(b.code);b.clear('OUTPUT');b.emit('halt','consumed') + entries['install']=len(b.code);b.clear('SOURCE');b.copy('OUTPUT','SOURCE',BLANK);b.clear('OUTPUT');b.emit('halt','installed') + entries['close']=len(b.code) + for r in PRIVATE:b.require(r,BLANK);b.move(r,-1);b.require(r,LEFT);b.write(r,BLANK);b.move(r,1) + b.emit('halt','closed');b.mark('reject');b.emit('halt','rejected') + return b.finish(),entries diff --git a/research/literal-elementary-interchange/verify.py b/research/literal-elementary-interchange/verify.py new file mode 100644 index 0000000000..32a92cc452 --- /dev/null +++ b/research/literal-elementary-interchange/verify.py @@ -0,0 +1,131 @@ +"""Exact literal program controls and actual source-geometry caller probe.""" +from pathlib import Path +from hashlib import sha256 +import json,tarfile,argparse,time,copy,subprocess,tempfile,sys +from unittest.mock import patch +from program import * +from machine import execute,validate +HERE=Path(__file__).resolve().parent +ROOT=HERE.parents[1] +def need(ok,why): + if not ok:raise ValueError(why) +def canonical(x):return json.dumps(x,sort_keys=True,separators=(',',':'),allow_nan=False) +def authenticate(): + spec=json.loads((HERE/'SOURCES.json').read_text()) + for row in spec['files']: + if row['usage']=='input':need(sha256((ROOT/row['path']).read_bytes()).hexdigest()==row['sha256'],'source bytes') + p=json.loads((HERE/'PREDECESSOR.json').read_text());archive=HERE/p['archive'] + need(sha256(archive.read_bytes()).hexdigest()==p['sha256'],'predecessor archive') + with tarfile.open(archive) as t: + for name,digest in p['members'].items():need(sha256(t.extractfile(name).read()).hexdigest()==digest,'predecessor member') + return {'archive':p['sha256'],'source_files':len(spec['files'])} +def setup(h,a,g,s,bits=None): + n=a*4**h*g*s + if bits is None:bits=[((i*13)^(i//3)^(i//4096))&1 for i in range(n)] + need(len(bits)==n,'fixture volume') + tapes={r:bytearray([BLANK]) for r in ROLES};heads={r:0 for r in ROLES} + tapes['SOURCE']=bytearray([LEFT]+bits) + for r,v in zip(('H','A','G','S'),(h,a,g,s)):tapes[r]=bytearray([LEFT]+[int(x) for x in reversed(bin(v)[2:])]+[RIGHT]) + for r in BORROWED:heads[r]=1 + return tapes,heads,bits + +def oracle(bits,h,a,g,s): + out=[] + for prefix in range(a): + for y in range(2**h): + for middle in range(g): + for x in range(2**h): + at=((((prefix*2**h+x)*g+middle)*2**h+y)*s);out.extend(bits[at:at+s]) + return bytearray(out) +def empty(tapes,heads,closed=False): + for r in PRIVATE: + need(heads[r]==1,'private head') + need(tapes[r][0]==(BLANK if closed else LEFT),'private marker') + need(all(v==BLANK for v in tapes[r][1:]),'private body') +def fixture(h,a,g,s,bits=None,program=None,install=False,repeats=1): + code,entries=assemble() if program is None else program + factor=validate(code,entries);tapes,heads,bits=setup(h,a,g,s,bits) + initial={r:bytes(tapes[r]) for r in BORROWED};expected=oracle(bits,h,a,g,s) + total={k:0 for k in ('steps','reads','writes','moves')};events=[] + def call(name): + receipt=execute(code,tapes,heads,entries[name],max_steps=300000000) + need(receipt['status']=={'init':'initialized','run':'returned','consume':'consumed','close':'closed','install':'installed'}[name],'literal status '+name) + for k in total:total[k]+=receipt[k] + events.append(receipt);return receipt + call('init') + for _ in range(repeats): + call('run');need(tapes['OUTPUT'][1:1+len(bits)]==expected,'output permutation') + need(all(v==BLANK for v in tapes['OUTPUT'][1+len(bits):]),'output tail') + for r in BORROWED:need(bytes(tapes[r])==initial[r] and heads[r]==1,'borrowed bytes/head') + need(heads['OUTPUT']==1,'output head') + call('install' if install else 'consume') + if install: + need(tapes['SOURCE'][1:1+len(bits)]==expected and heads['SOURCE']==1,'caller install') + for r in BORROWED[1:]:need(bytes(tapes[r])==initial[r] and heads[r]==1,'caller descriptors') + empty(tapes,heads) + call('close');empty(tapes,heads,True) + need(total['steps']<=factor*(total['reads']+total['writes']+total['moves']+len(events)),'CFG invoice') + L=h+sum(max(1,v.bit_length()) for v in (h,a,g,s))+8 + bound=2**20*(h+1)*(len(bits)+1)*(L+1)**2 + need(total['steps']<=repeats*bound,'whole price') + return {'geometry':[h,a,g,s],'bits':len(bits),'private_roles':len(PRIVATE),'program_length':len(code),'control_factor':factor,'calls':repeats,'install':install,'actions':total,'bound_per_session':bound,'output_sha256':sha256(expected).hexdigest()} + +def rejected(thunk): + try:thunk() + except (ValueError,FileNotFoundError,KeyError,IndexError):return + raise ValueError('control accepted') +def controls(): + receipts=[] + for h in range(6):receipts.append(fixture(h,1,1,1)) + for h,a,g,s in [(0,2,3,2),(1,2,3,2),(2,2,2,3),(3,1,2,1)]:receipts.append(fixture(h,a,g,s)) + for i in range(24): + bits=[0]*24;bits[i]=1;fixture(1,1,2,3,bits) + fixture(2,1,2,3,repeats=3) + code,entries=assemble() + # Mutate an actual queue read, leaving the rest of the program unchanged. + changed=list(code) + pos=next(i for i,row in enumerate(changed) if row[0]=='test' and row[1]=='Q01' and row[2]==ZERO) + row=list(changed[pos]);row[1]='Q10';changed[pos]=tuple(row) + rejected(lambda:fixture(1,1,2,3,[0]*3+[1]+[0]*20,(tuple(changed),entries))) + # Missing phase update violates the full digit input extent. + old=Builder.double + def omit(self,role): + if role!='PRE':old(self,role) + with patch.object(Builder,'double',omit):bad=assemble() + rejected(lambda:fixture(2,1,2,3,program=bad)) + old_clear=Builder.clear + def no_erase(self,role): + if role!='B0':old_clear(self,role) + with patch.object(Builder,'clear',no_erase):bad=assemble() + rejected(lambda:fixture(1,1,2,3,program=bad)) + rejected(lambda:validate((('call',lambda:None),),{'run':0})) + rejected(lambda:validate((('jump',0),),{'run':0})) + rejected(lambda:validate((('jump',True),),{'run':0})) + x={'n':1} + for v in (True,1.0):need(canonical(x)!=canonical({'n':v}),'typed receipt') + real=Path.read_bytes + archive=HERE/'inputs/pr5162.tar.gz' + def corrupt(p):return b'changed' if p==archive else real(p) + with patch.object(Path,'read_bytes',corrupt):rejected(authenticate) + # Real cold process entry failures, before any full scientific work. + with tempfile.TemporaryDirectory() as tmp: + target=Path(tmp)/'research'/'literal';target.mkdir(parents=True) + for name in ('verify.py','program.py','machine.py'): + (target/name).write_bytes((HERE/name).read_bytes()) + for missing in ('RESULT.json','SOURCES.json'): + if missing=='SOURCES.json':(target/'RESULT.json').write_text('{}') + result=subprocess.run([sys.executable,'-B',str(target/'verify.py')],capture_output=True,text=True,timeout=5) + need(result.returncode!=0 and missing in result.stderr,'missing-file process rejection') + return {'fixtures':receipts,'independent_columns':24,'repeated_calls':3,'rejections':['wrong_queue_read','missing_prefix_update','missing_owned_erase','host_callback_opcode','zero_cell_cycle','bool_pc','boolean_receipt','float_receipt','source_corruption','missing_RESULT_process','missing_SOURCES_process']} + +def run(): + auth=authenticate();light=controls();actual=fixture(2,1,1024,12,install=True) + return {'status':'PASS_LITERAL_ELEMENTARY_INTERCHANGE','sources':auth,'program_sha256':sha256(canonical(assemble()).encode()).hexdigest(),'code_sha256':{n:sha256((HERE/n).read_bytes()).hexdigest() for n in ('program.py','machine.py')},'controls':light,'actual':actual} +if __name__=='__main__': + p=argparse.ArgumentParser();p.add_argument('--write-result',action='store_true');args=p.parse_args() + # Require the frozen result before scientific work outside authoring mode. + expected=None if args.write_result else json.loads((HERE/'RESULT.json').read_text()) + start=time.monotonic();result=run() + if args.write_result:(HERE/'RESULT.json').write_text(json.dumps(result,indent=2)+'\n') + else:need(canonical(result)==canonical(expected),'complete typed receipt') + print(json.dumps({'status':result['status'],'seconds':time.monotonic()-start,'actual':result['actual']},indent=2))