diff --git a/research/physical-three-lane-reversal/PROOF.md b/research/physical-three-lane-reversal/PROOF.md new file mode 100644 index 0000000000..39dc08f7c4 --- /dev/null +++ b/research/physical-three-lane-reversal/PROOF.md @@ -0,0 +1,123 @@ +# A paid fixed-three-lane reversal + +JoyboyBrian, with substantial OpenAI Codex assistance. Apache-2.0. + +## Contract and scope + +For every n>=0 and B>=1, SOURCE contains n consecutive B-bit records and +BD contains the canonical least-significant-first positive binary encoding +of B. These are supplied ports, each with a left marker, head at its first +payload cell, and blank tail. OUTPUT and the work ports are blank after +their reliable left markers. Every port, including unused ports1,2,3, +starts with its head at its own origin+1. All15 ports are distinct. +Ports1,2,3 may contain arbitrary payload after their markers and are untouched. +The local alphabet is {0,1,blank,left}; the compiled instruction table is +independent of n and B. The interpreter's step counter and low/high water diagnostics are observers, +not control registers of the mathematical program. The interpreter executes +only single-cell reads, +writes, unit head moves and finite jumps. Its host step cap is a verifier +stop, not an input to the mathematical machine. + +On a valid call OUTPUT contains the same records in reverse order, preserving +bit order within every record. SOURCE and BD retain their payloads. All heads +return to their own origin+1; all work cells are blank. Output is caller-owned; +its later disposal is a separate caller obligation, bounded by a linear scan +of its nB cells if requested. Inputs may be based at independently translated +origins. This is a valid-input service; malformed encodings can reject with +partially written work and displaced heads. There is no transactional failure +restoration claim. + +This realizes the fixed-T=3 instance of Nick Petalas's PR5148 construction, +with the physical costs that its abstract stable-lane model leaves unpaid. +Credit Matarener's PR3825 pass obstruction, James Reed's PR3839 finite census, +and the retained PR5090 local instruction Builder/Tape semantics. No universal +multitape lower bound, full bit-free supplier gain, or selected-frontier update +follows. + +## Local control and refinement + +The retained unary routine copies BD to TEMP, decrements its canonical binary +value until zero, and appends one unit to B per decrement. It preserves BD, +erases TEMP, and returns both descriptor heads. The initial scan copies one +B-bit record at a time from SOURCE to DATA and appends one unit to N. A blank +SOURCE cell is accepted only at a record boundary. Thus N has length n and +DATA is the original record sequence. S starts at unary1. + +At stage i, put s=3^i. The invariant is: DATA is partitioned into consecutive +original-index blocks of length s, with the final block possibly shorter; +each block is internally reversed, and blocks are in original order. Heads +start at their origins and every lane is empty. The coverage loop compares +N and S by local synchronous scans. If s>=n it terminates. + +Otherwise split transfers consecutive chunks of at most s records cyclically +to lane0, lane1, lane2. Chunks remain ordered within each lane, so this is an +actual stable split. Each transferred source cell is erased. The unary S and +B tapes drive every chunk and record loop. No payload record is fabricated for +an absent position. After rewinding the empty DATA and populated lanes, merge +transfers one chunk from lane2, then lane1, then lane0 to DATA. Absent tail +chunks are skipped by reading their blank current cells. Every full group +becomes the reversal of the corresponding three original blocks. A final +one- or two-block group is also reversed because only its real lane chunks +are emitted. Each lane is consumed in its own stream order: the merge is stable. + +Hence DATA has the same invariant with block size3s. The literal tripling +loop consumes S and writes three units to NEXT per unit, then consumes NEXT +back to S. Induction proves the invariant at every stage. The first s>=n +occurs after k=ceil(log_3 n) stages for n>=2, with k=0 for n=0,1. DATA is then +one reversed block. Final transfer consumes it into OUTPUT; fixed cleanup +scans erase N, S, B and all auxiliary cells and return the heads. + +For n7, s1 gives records2,1,0,5,4,3,6, and s3 gives6,5,4,3,2,1,0, +exactly PR5148's first example. The digit-complement and block-reversal +constructions agree because complementing the next ternary digit reverses +the order of these three already-reversed subblocks, including the last +incomplete group. + +## Complete local-action bound + +Let L=floor(log_2 B)+1 and k as above. Count each table instruction, including +reads, jumps, writes and head moves, as one action. A conservative bound is + + T <= 256 ((n+1)(B+1)(k+1) + B(L+1) + 1). + +This is a written upper bound, not a fitted measured slope. The following +summands account for the whole execution. A rewind over h payload positions +costs at most3h+5. A row copy/consume, including the B rewind, costs at most +16B+12. Unary conversion costs at most32B(L+1)+16L+32. Initial copy/counting, +source/data/N rewind, and final payload transfer are together at most +40nB+24n+32. At one nonterminal stage, the2n row transfers and chunk dispatch +cost at most40nB+48n+48; the lane/DATA rewinds cost at most12nB+40. +Coverage scans across the run cost at most12n(k+1)+16(k+1). Tripling and its +transfer cost at most48s+32 per stage. Since sum_{i=2, all tripling costs are at most72n+32k. Final cleanup costs at most +16(B+n+3^k+L+1)+80; n0/1 uses3^k=1. These deliberately loose summands fit the +displayed bound (including B=1,n=0). In particular runtime width is paid; +there is no constant-time B-bit word operation or free lane interleaving. + +## Retained backing, setup and output + +The15 role objects and fixed419-instruction program are constant setup. +No tape is allocated during execution. If K0 counts already allocated tape +backing, newly visited storage is bounded by + + 6nB + 7n + B + 2L + 60. + +This conservatively counts SOURCE, DATA, OUTPUT and each of three lanes at +nB individually. It does not sum only simultaneously live lane payloads: +each lane can retain a different historical high-water mark. N costs n; +S and NEXT each reach3^k<3n for n>=2 (at most1 for n<=1); B costs B; BD and +TEMP cost L each. Markers, terminal blank visits and the n<=1 exception fit +the60 allowance. Thus retained backing is at most K0 plus this expression, +even though the dictionary simulator retains blank written cells after erasure. +This is a tape-cell statement, not a Python allocator-byte claim. Borrowed +input production, input descriptor production and later output disposal are +explicit caller costs, not hidden inside this service. + +## Open next questions + +A complete bit-free supplier must compose this reversal with its other +permutations and numerical consumers and pay their combined bank and costs. +First bind one actual supplier endpoint to the present record layout; pass +optimality alone does not establish a numerical gain. Heterogeneous runtime +lane capacities would require a separate fixed-bank encoding and scheduling +contract; this theorem fixes three lanes. diff --git a/research/physical-three-lane-reversal/README.md b/research/physical-three-lane-reversal/README.md new file mode 100644 index 0000000000..04972b5a5e --- /dev/null +++ b/research/physical-three-lane-reversal/README.md @@ -0,0 +1,56 @@ +# Physical three-lane record reversal + +JoyboyBrian, with substantial OpenAI Codex assistance. Apache-2.0. + +One fixed419-instruction local-symbol program reverses n records of runtime +width B on15 fixed tape ports. It realizes PR5148's three-lane stable route +on actual records, including incomplete final blocks, with no host sorting, +per-record tape allocation, decoded loop bounds or virtual payload padding. +The input and binary width descriptor are borrowed; output is distinct and +caller-owned. All work is erased and heads return. This is a valid-input +contract, not a rollback guarantee for malformed input. + +For L=floor(log2 B)+1 and k=ceil(log3 n) (k0 for n0/1), the complete instruction +count is at most256((n+1)(B+1)(k+1)+B(L+1)+1). Retained tape backing is at most +K0+6nB+7n+B+2L+60, including historical high-water capacity. [PROOF.md](PROOF.md) +gives the all-n refinement, full invoice, supplied-input costs and limitations. +The abstract pass count alone is not a physical tariff or a numerical gain. + +The verifier checks492 cases with independent record-array expectations, +translated origins, full borrowed/unused frames, every work tape and head, +written action/backing bounds, eight additional power-of-three/binary-carry +cases through n244 and B1024, and the exact seven-record two-pass source +example. Eight controls include actual output-bit and guide corruption. +These are finite corroboration of the scoped proof, not a proof kernel or a +complete multiplication theorem. + +Reproduce from the repository root with Python3.12: + +```sh +python3.12 -I -B research/physical-three-lane-reversal/verify.py +python3.12 -I -O -B research/physical-three-lane-reversal/verify.py +python3.12 scripts/research_package.py --package research/physical-three-lane-reversal --check-only +python3.12 scripts/research_package.py --package research/physical-three-lane-reversal +``` + +`--write-result` is the explicit receipt-generation mode. Normal replay +requires both SOURCES.json and RESULT.json; frozen receipts use typed canonical +JSON equality. The source proof from PR5148 is retained byte-for-byte and +hash-checked with exact public head/path metadata. It is external publication +provenance, not a local Git-history assertion. The retained local instruction +source is authenticated by the base Git blob and SHA256 and declared as a live +export input. No predecessor source is modified. + +Credit Nick Petalas's PR5148 construction, Matarener's PR3825 obstruction, +James Reed's PR3839 finite census, and the PR5090 physical instruction semantics +following Jose Manuel PR2786 and Nick Petalas PR3503. The canonical claim is +[discussion1166 comment19144825](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19144825). + +## Open next questions + +Can an actual bit-free supplier consume this layout with its complete numerical, +movement and backing budget? First bind one real supplier call and its other +permutations; this standalone reversal does not establish supplier admission. +Can heterogeneous runtime lane capacities be encoded on a fixed bank with a +complete tariff? That is separate from the present fixed-three-lane theorem. +The selected frontier is unchanged. diff --git a/research/physical-three-lane-reversal/RESULT.json b/research/physical-three-lane-reversal/RESULT.json new file mode 100644 index 0000000000..245a8ce3f1 --- /dev/null +++ b/research/physical-three-lane-reversal/RESULT.json @@ -0,0 +1,115 @@ +{ + "schema_version": 1, + "claim": "fixed-three-lane physical valid-input reversal", + "cases": 492, + "cases_sha256": "534d2e2b3f5888900fc2297bf1e3e57a6e038d5c572d75bee9d5bff26c4b6e95", + "carry_and_stage_boundaries": [ + { + "n": 80, + "B": 2, + "origin": 31, + "steps": 43315, + "backing": 933, + "stage_records": [] + }, + { + "n": 81, + "B": 2, + "origin": 31, + "steps": 43770, + "backing": 942, + "stage_records": [] + }, + { + "n": 82, + "B": 2, + "origin": 31, + "steps": 59151, + "backing": 1381, + "stage_records": [] + }, + { + "n": 242, + "B": 1, + "origin": 31, + "steps": 103806, + "backing": 1744, + "stage_records": [] + }, + { + "n": 243, + "B": 1, + "origin": 31, + "steps": 104155, + "backing": 1749, + "stage_records": [] + }, + { + "n": 244, + "B": 1, + "origin": 31, + "steps": 139928, + "backing": 2887, + "stage_records": [] + }, + { + "n": 7, + "B": 129, + "origin": 31, + "steps": 97401, + "backing": 3956, + "stage_records": [] + }, + { + "n": 3, + "B": 1024, + "origin": 31, + "steps": 235098, + "backing": 13388, + "stage_records": [] + } + ], + "program_instructions": 419, + "max_steps": 126932, + "seven": { + "n": 7, + "B": 3, + "origin": 0, + "steps": 3579, + "backing": 164, + "stage_records": [ + [ + "101", + "000", + "011", + "100", + "111", + "010", + "001" + ], + [ + "001", + "100", + "111", + "010", + "101", + "000", + "011" + ] + ] + }, + "controls": [ + "bad-width:", + "bad-width:0", + "bad-width:10", + "bad-width:1x", + "partial-row", + "port-alias", + "actual-mutant:output-bit", + "actual-mutant:tripled-guide" + ], + "unrun": [ + "production bit-free supplier composition", + "heterogeneous runtime lane counts" + ] +} diff --git a/research/physical-three-lane-reversal/SOURCES.json b/research/physical-three-lane-reversal/SOURCES.json new file mode 100644 index 0000000000..bf18b7943e --- /dev/null +++ b/research/physical-three-lane-reversal/SOURCES.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "base_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13", + "files": [ + { + "path": "research/bit-row-padding-physical/machine.py", + "usage": "input", + "git_blob": "1e3533efa92c3bab35916ae6844290586d18ff27", + "sha256": "24270408e87b028791670cd63908adeb03162f0919237e8644065c5898fecf2f" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + } + ], + "external_public_input": { + "local_path": "inputs/pr5148-PROOF.md", + "source_pr": 5148, + "source_head": "7a49d01908933e044acf96f040b15818ef748051", + "source_path": "research/reversal-stable-lane-tariff/PROOF.md", + "sha256": "98b6d670ae019c3c9365e20f80b872a764d4b0dfc2a7f76d5ce24c50c7c19c39", + "coverage": "Unmodified exact public proof; constructive predecessor, not physical-cost evidence." + } +} diff --git a/research/physical-three-lane-reversal/TASK.json b/research/physical-three-lane-reversal/TASK.json new file mode 100644 index 0000000000..1742f8d05f --- /dev/null +++ b/research/physical-three-lane-reversal/TASK.json @@ -0,0 +1,95 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Physical fixed-three-lane realization of PR5148 reversal for all n and encoded runtime record width B.", + "scope_change_reason": "The public PR5148 handoff leaves stable routing, metadata, movement and cleanup unpriced. This supplies their actual finite program and complete tape tariff.", + "bottleneck_link": "Closes one concrete physical record-layout contract without inferring a full bit-free supplier gain.", + "budget_minutes": 60, + "stop_rule": "Stop if local control, partial tails, restoration or whole cost needs an unpriced host oracle.", + "outcome": "completed", + "evidence": "PROOF.md; machine.py; verify.py and RESULT.json; canonical claim19144825;492 frame/action cases and8 controls.", + "author": "JoyboyBrian", + "ai_assistance": "Substantial OpenAI Codex assistance; finite corroboration, not human or proof-kernel review.", + "open_questions": [ + { + "question": "Can a complete bit-free supplier consume this physical reversal?", + "why_it_matters": "Pass optimality does not establish a numerical improvement.", + "first_step": "Bind one actual supplier endpoint and add all other routing and numerical costs.", + "blocked_by": "Whole supplier composition and budget remain outside scope." + } + ] +} diff --git a/research/physical-three-lane-reversal/VERIFY.json b/research/physical-three-lane-reversal/VERIFY.json new file mode 100644 index 0000000000..a8fa34b2a3 --- /dev/null +++ b/research/physical-three-lane-reversal/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/bit-row-padding-physical/machine.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Source-bound full frames, exact stages, action/backing and mutants" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Same explicit guards and typed receipt without assertions" + } + ] +} diff --git a/research/physical-three-lane-reversal/inputs/pr5148-PROOF.md b/research/physical-three-lane-reversal/inputs/pr5148-PROOF.md new file mode 100644 index 0000000000..487f024811 --- /dev/null +++ b/research/physical-three-lane-reversal/inputs/pr5148-PROOF.md @@ -0,0 +1,115 @@ +# Exact reversal capacity of stable-lane passes + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Model and statement + +There are n distinct records, initially in order 0,...,n-1, with n >= 1. +A pass with capacity T >= 1 assigns each record to one of at most T lanes. +Each lane preserves its input order. The output can be any interleaving of +the lane streams that preserves that order. Empty lanes are permitted. +The record payloads are transported intact, without copying or deletion. +Lane assignments and interleavings are unrestricted routing descriptions. +No cost for selecting or executing them is included in a pass count. + +**Theorem.** For nonnegative k and positive integers T_1,...,T_k, exactly +reversing n records is possible in those k passes if and only if + + n <= T_1 ... T_k. + +The empty product is one. Consequently, with fixed T >= 2 the minimum pass +count is the smallest integer k with T^k >= n, namely ceil(log_T n). +For T=1, only n=1 can be reversed, and its minimum is zero passes. + +This is a scoped combinatorial routing theorem. In particular, a lane is +not an assertion that a physical tape or its head can provide this service +at unit cost. Splitting, merge control, movement, return, storage and +reversible cleanup are separate obligations. + +## Necessity + +Assign each record its k-tuple of lane choices along the route. If two +records have the same tuple, their relative order is preserved in the +first pass. Inductively, it is preserved in every later pass, because +the two records again enter the same order-preserving lane. Full reversal +reverses every pair of distinct records. Thus no two records can have +the same tuple. There are at most product(T_i) tuples, proving necessity. + +This argument permits arbitrary splitting and merge choices. It is the +reversal instance of the decreasing-subsequence obstruction used by +Matarener in #3825. We credit that obstruction and do not claim it as new. + +## Attainment by mixed-radix coordinates + +Set N = product(T_i), and let s_i = product(T_j for j < i), so s_1=1. +Every integer z in [0,N) has a unique mixed-radix representation + + z = sum_i d_i s_i, 0 <= d_i < T_i. + +Use only the actual records x in [0,n), assigning each the initial virtual +coordinate z=x. Coordinates in [n,N) are absent; no padding records or +payload operations on them are required. + +At pass i, assign a record to lane d_i of its current coordinate. Replace +that coordinate by + + z' = z + (T_i - 1 - 2 d_i) s_i. + +This complements exactly digit i. All other digits remain unchanged, +so the operation is a bijection of [0,N). For a fixed lane d_i, the +coordinate change is a constant translation. It therefore preserves the +relative order of every pair in that lane. Output records in increasing +order of z'. Their restriction to each lane is exactly its input stream, +so this is an allowed merge. Only the n real records are sorted or routed. + +After all k passes every digit is complemented, and a record initially +at x has coordinate + + sum_i (T_i - 1 - d_i) s_i = N - 1 - x. + +Here sum_i (T_i-1)s_i = N-1 follows by telescoping +T_i s_i - s_i = s_(i+1) - s_i. Increasing final coordinates therefore give +the record order n-1,...,0. This proves attainment and the theorem. +When k=0, the hypothesis forces n=1 and the empty route already suffices. +Radix-one stages are identity passes and cause no exception. + +For example, n=7 and (T_1,T_2)=(3,3) give the actual record orders + + 0 1 2 3 4 5 6 + 2 1 0 5 4 3 6 + 6 5 4 3 2 1 0. + +The first lane assignments are 0,1,2,0,1,2,0. The second assignments, in +the displayed intermediate order, are 0,0,0,1,1,1,2. No eighth or ninth +record is present. This attains the two-pass lower bound with three lanes. + +## Independent finite minimum check + +For a permutation p, let w(p) be its longest decreasing-subsequence length. +One pass with T lanes exists exactly when w(p) <= T. Necessity holds since +a decreasing subsequence uses different lanes. For sufficiency, label each +entry by the longest decreasing-subsequence length ending at that entry. +If two entries have equal labels, their order in p agrees with their +natural increasing order: an inverted pair would increase the latter +entry's label. Thus each label class is an increasing subsequence, and +these classes give at most T stable lanes. This is the classical chain +partition argument, included to specify the finite check's full alphabet. + +The independent shortest-path checker enumerates every permutation of +orders one through six. It permits every generator with w(p) <= T for +T=2,3,4 and breadth-first searches for reversal. It does not use the +mixed-radix constructor to choose generators or determine distances. +Its finite agreement corroborates the theorem; the proof above supplies +the unrestricted quantifiers. James Reed's #3839 finite composition +census is a credited predecessor and is not replayed. + +## Scope and remaining obligations + +The added step is attainment of the reversal pass obstruction, including +heterogeneous lane counts and arbitrary incomplete virtual grids. No +claim of historical novelty for radix routing, chain partitioning or the +lower-bound method is made. The theorem does not classify the optimal +pass depth of other permutations. It does not price an admitted supplier, +give an unconditional multitape lower bound, alter a selected ledger or +prove a complete multiplication theorem. Independent human and formal +proof-kernel review are unclaimed. diff --git a/research/physical-three-lane-reversal/machine.py b/research/physical-three-lane-reversal/machine.py new file mode 100644 index 0000000000..4d687da7d5 --- /dev/null +++ b/research/physical-three-lane-reversal/machine.py @@ -0,0 +1,177 @@ +"""Fixed three-lane local program; JoyboyBrian with OpenAI assistance, Apache-2.0. +Builder/Tape instruction semantics credited to retained PR5090. +""" +import importlib.util +from pathlib import Path +_spec = importlib.util.spec_from_file_location('reversal_instruction_source', Path(__file__).resolve().parents[1] / 'bit-row-padding-physical/machine.py') +source = importlib.util.module_from_spec(_spec) +import sys +sys.modules[_spec.name] = source +_spec.loader.exec_module(source) +Builder, Tape, BLANK, LEFT, need = source.Builder, source.Tape, source.BLANK, source.LEFT, source.need +SOURCE, BD, B, TEMP = 0, 4, 8, 10 +LANES = (5, 6, 7) +S, N, DATA, NEXT, OUTPUT = 9, 11, 12, 13, 14 +WORK = (*LANES, B, TEMP, S, N, DATA, NEXT) + + +class Control(Builder): + def row(self, src, dst, consume=False): + loop, bit, zero, one, end = [self.fresh('row') for _ in range(5)] + self.mark(loop) + self.read(B, {'1': bit, BLANK: end}) + self.mark(bit) + self.read(src, {'0': zero, '1': one}) + self.mark(zero) + self.write(dst, '0') + self.go(one + 'written') + self.mark(one) + self.write(dst, '1') + self.mark(one + 'written') + if consume: + self.write(src, BLANK) + self.move(src, 1) + self.move(dst, 1) + self.move(B, 1) + self.go(loop) + self.mark(end) + self.rewind(B) + + def chunk(self, src, dst): + loop, available, record, end = [self.fresh('chunk') for _ in range(4)] + self.mark(loop) + self.read(S, {'1': available, BLANK: end}) + self.mark(available) + self.read(src, {'0': record, '1': record, BLANK: end}) + self.mark(record) + self.row(src, dst, True) + self.move(S, 1) + self.go(loop) + self.mark(end) + self.rewind(S) + + def transfer(self, src, dst, consume=False): + loop, zero, one, end = [self.fresh('transfer') for _ in range(4)] + self.mark(loop) + self.read(src, {'0': zero, '1': one, BLANK: end}) + self.mark(zero) + self.write(dst, '0') + self.go(one + 'written') + self.mark(one) + self.write(dst, '1') + self.mark(one + 'written') + if consume: + self.write(src, BLANK) + self.move(src, 1) + self.move(dst, 1) + self.go(loop) + self.mark(end) + self.rewind(src) + self.rewind(dst) + + +def program(): + global STAGE_PC + c = Control() + c.unary(BD, B) + scan, record, copied = [c.fresh('input') for _ in range(3)] + c.mark(scan) + c.read(SOURCE, {'0': record, '1': record, BLANK: copied}) + c.mark(record) + c.row(SOURCE, DATA) + c.write(N, '1') + c.move(N, 1) + c.go(scan) + c.mark(copied) + for t in (SOURCE, DATA, N): c.rewind(t) + c.write(S, '1') + test, nmore, pair, covered, route = [c.fresh('cover') for _ in range(5)] + c.mark(test) + c.read(N, {'1': nmore, BLANK: covered}) + c.mark(nmore) + c.read(S, {'1': pair, BLANK: route}) + c.mark(pair) + c.move(N, 1) + c.move(S, 1) + c.go(test) + c.mark(route) + c.rewind(N) + c.rewind(S) + split, splitmore, splitend = [c.fresh('split') for _ in range(3)] + c.mark(split) + c.read(DATA, {'0': splitmore, '1': splitmore, BLANK: splitend}) + c.mark(splitmore) + for lane in LANES: c.chunk(DATA, lane) + c.go(split) + c.mark(splitend) + for t in (DATA, *LANES): c.rewind(t) + merge, mergemore, mergeend = [c.fresh('merge') for _ in range(3)] + c.mark(merge) + c.read(LANES[0], {'0': mergemore, '1': mergemore, BLANK: mergeend}) + c.mark(mergemore) + for lane in reversed(LANES): c.chunk(lane, DATA) + c.go(merge) + c.mark(mergeend) + STAGE_PC = len(c.code) + for t in (DATA, *LANES): c.rewind(t) + triple, unit, tripled = [c.fresh('triple') for _ in range(3)] + c.mark(triple) + c.read(S, {'1': unit, BLANK: tripled}) + c.mark(unit) + c.write(S, BLANK) + c.move(S, 1) + for _ in range(3): + c.write(NEXT, '1') + c.move(NEXT, 1) + c.go(triple) + c.mark(tripled) + c.rewind(S) + c.rewind(NEXT) + c.transfer(NEXT, S, True) + c.go(test) + c.mark(covered) + c.rewind(N) + c.rewind(S) + c.transfer(DATA, OUTPUT, True) + for t in WORK: c.clear(t) + c.code.append(('done',)) + c.mark('reject') + c.code.append(('rejected',)) + c.mark('quarantine') + c.code.append(('quarantined',)) + return c.finish() + + +PROGRAM = program() + + +class Machine: + def __init__(self, tapes): + need(len(tapes) == 15 and len({id(t) for t in tapes}) == 15, 'fifteen distinct ports') + self.tapes, self.pc, self.steps = tapes, 0, 0 + + def run(self, budget=10000000): + while self.steps < budget: + ins = PROGRAM[self.pc] + op = ins[0] + self.steps += 1 + if op == 'done': return + if op in ('rejected', 'quarantined'): raise ValueError(op) + if op == 'goto': + self.pc = ins[1] + continue + t = self.tapes[ins[1]] + if op == 'read': + symbol = t.read() + need(symbol in ins[2], 'local symbol') + self.pc = ins[2][symbol] + continue + if op == 'write': + t.read() + t.cells[t.head] = ins[2] + elif op == 'move': + t.head += ins[2] + t.read() + else: raise ValueError('unknown opcode') + self.pc += 1 + raise ValueError('execution budget') diff --git a/research/physical-three-lane-reversal/verify.py b/research/physical-three-lane-reversal/verify.py new file mode 100644 index 0000000000..7bff452801 --- /dev/null +++ b/research/physical-three-lane-reversal/verify.py @@ -0,0 +1,129 @@ +"""Exact finite corroboration, full frames and fail-closed frozen inputs.""" +import hashlib +import importlib.util +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + +def need(ok, message): + if not ok: raise ValueError(message) + + +def pins(): + manifest = json.loads((HERE / 'SOURCES.json').read_text()) + for row in manifest['files']: + if row['usage'] != 'input': continue + need(hashlib.sha256((ROOT / row['path']).read_bytes()).hexdigest() == row['sha256'], 'source pin: '+row['path']) + row = manifest['external_public_input'] + need(hashlib.sha256((HERE / row['local_path']).read_bytes()).hexdigest() == row['sha256'], 'PR5148 exact proof') + + +def load(): + spec=importlib.util.spec_from_file_location('reversal_science', HERE/'machine.py') + m=importlib.util.module_from_spec(spec) + spec.loader.exec_module(m) + return m + + +def fixture(m,n,width,shift=0): + rows=[format((i*37+11)%(1<=origins[i], 'no visit before marker') + if i in (m.SOURCE,m.BD,1,2,3):need((t.cells,t.head)==saved[i], 'borrowed/unused full frame') + elif i!=m.OUTPUT:need(all(v==m.BLANK for p,v in t.cells.items() if p!=origins[i]),'work erased') + k=0;s=1 + while s