diff --git a/research/bit-row-padding-physical/PROOF.md b/research/bit-row-padding-physical/PROOF.md new file mode 100644 index 0000000000..8fff5bc0c0 --- /dev/null +++ b/research/bit-row-padding-physical/PROOF.md @@ -0,0 +1,185 @@ +# Complete-fibre compatible-row padding on fifteen fixed tapes + +JoyboyBrian, substantial OpenAI Codex assistance. Apache-2.0. +The compatible-row semantics are Jose Manuel's PR2786, and the wider strict +volume criterion and bounded Count adapter are Nick Petalas's PR3503. This +package does not claim either arithmetic fact as new. + +## Contract and machine + +Let P,R,S,B be positive integers with S<=R, V=PRB, and +R'=S ceil(R/S), Delta=R'-R. Input is an arbitrary binary function serialized +in lexicographic [P][R][B] order. B is the COMPLETE body/spectator fibre, +including the other high field and any supplied intermediate coordinates. +P contains all preceding complete coordinates. No coordinates are silently +dropped or replaced by one representative bit. + +The source and four descriptors are borrowed. Descriptors are canonical +least-significant-first binary words (last digit1). Each tape has a unique +left marker followed by its finite word, then blanks. Every head initially +points one cell right of its own marker; origins can differ independently. +Nine work/call tapes begin blank; a distinct final output tape begins blank. +These are fifteen physically distinct tapes, not fifteen aliases of a bank. +A fixed physical tape is the ownership identity; distinctness is an input +ABI premise, not an uncharged pointer comparison. The Python simulator checks +identity at construction and resumption to reject aliased representations; +that structural validation is not an extra physical routing instruction. + +The controller creates the padded word [P][R'][B], inserting Delta complete +zero rows AFTER the R genuine rows of EACH prefix. It exposes this tape and +a canonical binary R' at CALL. The callee borrows padded input, row count and +all original borrowed state, returns a distinct owned tape [P][R'][B], restores +all borrowed contents/heads, and closes its own scratch. The private P,R,S,B,Delta and temporary control +tapes are not exposed to the callee and must remain untouched. Its completed endpoint +preserves each row ordinal and permutes inside that row. Consequently padded +rows are again zero. More generally an explicitly proved zero-preserving +rowwise endpoint can satisfy the same adapter contract. + +The controller then copies genuine rows, checks and discards all added row +bits, rejects wrong returned lengths, and clears all nine owned work/call +tapes. Final output is a distinct owned [P][R][B] tape. Borrowed source, +descriptors and their backing/heads are unchanged. All heads are at their +own local first cell and all owned visited cells except fixed left markers +and final output are blank. + +The callee's row semantics and source preservation are premises. Local +zero checks do NOT establish them. A returned all-zero word can pass the +shape checks while destroying genuine data; the verifier intentionally +exhibits this. Test snapshots/oracles are not executable semantic admission. +The callee itself, its time/space/precision and native admission are excluded +from the adapter theorem. If the callee violates the contract, local malformed +return guards may reject; successful semantic correctness is not promised. +For canonical marked tapes, data/extent/length/padding-zero failures enter a +fixed cleanup epilogue: all owned work and partial output are erased, and +original borrowed heads rewind without changing their bytes. Post-CALL head +guard failure instead quarantines state: a violating callee may have moved +a head left of its marker, so a one-direction rewind is not a valid recovery +argument. Foreign alphabet symbols or misplaced left markers also quarantine. +No recovery of bytes maliciously changed by a callee, arbitrary exception +unwinding or drop-in replacement of Python try/finally is claimed. On invalid +inputs the valid-volume bound is not asserted; cleanup pays the actual finite +word lengths it scans. Canonical positive descriptors/valid callee are the +success theorem domain. + +## Fixed control and positive-width invariant + +machine.py emits one constant table, without input arguments. Its only +instructions are local read-and-branch, one-cell write, unit move, fixed jump, +CALL and DONE. Each references at most one fixed tape. The alphabet is +{0,1,left,blank}; one local instruction is one transition for this model. +The simulator's counters/dictionaries and visited-cell observation are a +representation of this machine, not runtime arithmetic instructions. +No instruction decodes extents, addresses a nonlocal cell, slices data, +multiplies, divides, allocates tapes or chooses an input-dependent unbounded control program. +Static labels and assembly resolve once, independently of P,R,S,B. + +Four descriptor passes copy bits to one reusable temporary binary tape. +The finite copy state remembers only the last bit, so empty/zero/noncanonical +positive descriptors reject. Each descriptor is rewound and preserved. +The temporary is decremented to zero, emitting one unary1 per decrement. +A decrement flips low zeros to ones, clears the next one and, if that one +was the highest digit, removes it. It rewinds only the digits just crossed. +Thus the temporary remains canonical or empty, and yields exactly n unary +ones for descriptor n. There is no4096-bit or other width capacity. + +Planning first scans unary R and S together, rejecting S>R, then rewinds. +It consumes all R row marks and cyclically traverses S group marks. At each +consumed mark it increments a canonical binary R' counter. If R ends on a +group boundary, Delta is empty. Otherwise it drains the remaining group, +appending one Delta mark and incrementing R' once per mark. Exactly +S ceil(R/S) positions are counted. This is a paid sequential implementation +of round-up, not a host division. + +At every prefix the first row loop processes exactly R rows and the second +exactly Delta rows. For every row the unary B counter advances once per bit +and rewinds at its right end. Padding copies genuine bits and writes literal +zeros on additional rows; restriction copies genuine bits and requires every +additional source bit to be0. The prefix counter advances once per complete +pair of loops. End-of-word guards enforce the exact supplied volume. All +counter rewinds and payload head moves are actual local instructions. + +At CALL the original source, descriptors, padded source and R' are all +rewound. After return, the machine locally steps left and reads the unique +left marker on each exposed tape, then steps right. This checks returned +head positions; it does not compare borrowed contents. Restoration of those +contents remains the callee premise. Restriction then runs only AFTER CALL. + +## Uniform costs, including setup + +Every positive extent is at most V: P,R,B<=PRB and S<=R. Also +Delta=1) floor(n/2^j) < n. +The total number of changed/crossed digits is <2n. Rewinding follows only +those crossed digits plus at most two boundary cells: it never scans the +original full descriptor width on each decrement. Copy, rewind, trim and +unary-output overhead are bounded by60n+40 instructions, directly allowing +eight instructions per borrow/return edge and all fixed tests. Four +conversions therefore cost at most240V+160. + +For increments1..r, the number of carried low ones sums to less than r. +Counting writes, local branch/goto, carry moves and rewind gives at most +16r+8 instructions. Group planning includes the cover comparison, all group +rewinds, remaining-row and group tests, Delta writes, and counter increments. +Every group rewind is charged to its consumed marks; total consumed group +marks is R'<2R. A conservative bound is80R+80<=80V+80. + +For one transform, every processed genuine/added cell has at most ten +instructions in the bit loop. B rewinds cost at most3(B+2) per row; row and +prefix guards/rewinds cost at most a further twenty per row plus twenty per +prefix. Since B,R>=1 and processed row count is PR'<2PR,80V+80 bounds a +transform including source/output rewinds and terminal guards. The two +transforms therefore cost at most160V+160. + +Nine owned tapes are cleared by one forward erase scan and one backward +rewind, at most eight instructions per cell plus fixed boundary overhead. +Their maximum occupied lengths total at most +P+R+S+B+Delta+max(ell(P),ell(R),ell(S),ell(B))+ell(R')+2V+2V < 11V+2. +Thus100V+200 is a conservative cleanup bound; the eight post-CALL local +boundary checks cost24. Summing these deliberately loose allocations is +less than2048V+2048 transitions for all V>=1. This bounds the actual table, +not the host Python interpreter's elapsed time. + +For space, all four unary extents and Delta total at most5V; the two binary +work/count extents total at most2V+1. Original source, padded source, +returned source and final output occupy at most6V altogether. Borrowed +descriptors have total length at most4V. Include all fifteen fixed markers, +the blank cells observed at right boundaries and any one-cell guard/rewind +overrun: fewer than64V+64 distinct visited cells on all tapes suffice. +The callee must deliver a returned word of length PR'B and must charge its +own other scratch separately. No global-origin span is counted: independent +tape origins are translation-invariant. + +These bounds need not be optimal. They prove supplied-width linear movement +and preparation with fixed tape/control resources. For the T=10Nf sequential +matcher lifetimes, the adapter charge is the SUM of these per-call bounds +at their actual complete volumes. It cannot replace the2T raw bodies, +3T body additive maps or T older high-part swaps. Physical P3 constants, +precision, the full native body and outer admission remain separate. + +## Actual source boundary and discriminator + +#4989's generator uses the borrowed branch exactly when2k2 and R=q^k=5. It schedules +inner_borrow, row_pad, body_sub, raw_reverse_swap, body_add, +raw_reverse_swap, body_rsub, inner_return, row_unpad, older_high_swap. +This adapter supplies the padding/restriction interface around that completed +inner body; it does NOT implement that body. The source owners462 and461 +remain distinct; the latter is a complete spectator encoded in the fibre. + +At P2,B6, sixty genuine bits become seventy-two padded bits. Twelve actual +zeros are written in two six-bit rows. The old addressed interpreter's +zeros=[0]*(total-size) is valid row metadata, but is not this physical bit +allocation; no predecessor bug is asserted. All sixty individual dirty basis +inputs and an all-one translated-origin fixture test the complete fibre, +together with boundary cases around binary carries. A synthetic completed +rowwise reversal witnesses the adapter composition only. + +The conditional proof applies at arbitrary positive extents, including the +actual much larger body/spectator product. P2,B6 is a discriminating interface +fixture, not an execution of the full GL64 cover. Small q5 is source scheduling +calibration, not proof of the source's large-prime admissibility bound. diff --git a/research/bit-row-padding-physical/README.md b/research/bit-row-padding-physical/README.md new file mode 100644 index 0000000000..e38796c80e --- /dev/null +++ b/research/bit-row-padding-physical/README.md @@ -0,0 +1,61 @@ +# Physical complete-fibre ROW padding + +This package lowers the compatible-row padding/return/restriction boundary +to one fixed589-instruction controller on fifteen tapes. For runtime positive +binary P,R,S,B with S<=R and V=PRB, it pays descriptor preparation and +round-up, inserts complete zero fibres, restricts only after the completed +callee returns, and erases every owned temporary. The written bound is +2048V+2048 transitions excluding the callee and64V+64 visited cells. +There is no fixed descriptor bit-width limit. + +The actual #4989 helper462/frame506 borrowed branch at q5,w4,k1,S3 pads +five rows to six. With P2 and body/spectator fibre B6,60 bits become72: +twelve physical zeros, not one metadata marker. All sixty basis inputs, +binary carry boundaries, arbitrary dirty data and independently translated +tape origins are checked. [PROOF.md](PROOF.md) separates this finite evidence +from the all-width argument. + +The completed row-pointwise, source-preserving callee remains a semantic +premise. Local zero/length/head checks do not certify it; a registered +counterexample demonstrates that distinction. No native_canonical or +raw_reverse_swap implementation, full GL64 payload, new supplier, P3 reserve, +precision/outer admission or new kappa is claimed. Canonical data/shape failures execute owned cleanup and rewind borrowed +heads; callee head violations quarantine state instead of promising recovery. + +Jose Manuel's PR2786 supplies the original compatible-row scans and callback +contract. Nick Petalas's PR3503 supplies the exact strict-volume criterion +and capped Count/Tape adapter. Their ratio/least-borrowing results and scans +are credited, not republished as new results. This adds fixed local control +and a uniform complete-fibre cost, while keeping the actual source S<=R domain. +The wider S<2R change is outside scope. #4957's conditional completed BIT API +and #4989's addressed matcher/ROW schedule supply the actual caller boundary. + +Run from repository root with standard-library Python3.12: + +```sh +python3.12 -Werror -B scripts/research_package.py --package research/bit-row-padding-physical +``` + +Registered normal/optimized replay checks immutable inputs, complete bytes, +cleanup, malformed returns and the fixed table receipt. Committed bytes, +source history and official Git-free export are separate publication checks. +The simulator uses dictionaries to represent tapes; only its declared local +instructions define the proved machine cost. Test oracles and synthetic +callee execution are not hidden machine instructions. + +Canonical claim: +https://github.com/CrocSwap/integer-mult-bounds/discussions/4945#discussioncomment-19141335 + +## Open next questions + +- Supply an actual completed native/raw callback with this exact source, + row-pointwise, distinct-output and restored-head contract; begin at the + source inner_return boundary, preserving complete other-high-field fibres. +- Bind this controller to the full selected serialization and actual P3 + reserve/precision constants. The interface calibration alone does not + instantiate the astronomical complete matcher cover. + +JoyboyBrian, substantial OpenAI Codex assistance. Apache-2.0. Preserve credit +to ai-nanachi, Jose Manuel, Nick Petalas, Chris R/Clear1nsight, David Arias +and the full source-native/ordinary/ROW lineage in the authenticated inputs. +No independent human or proof-kernel acceptance claim. diff --git a/research/bit-row-padding-physical/RESULT.json b/research/bit-row-padding-physical/RESULT.json new file mode 100644 index 0000000000..481e979462 --- /dev/null +++ b/research/bit-row-padding-physical/RESULT.json @@ -0,0 +1,75 @@ +{ + "actual_fixture": [ + 2, + 5, + 3, + 6, + 2055, + 4675, + 327 + ], + "basis_columns": 60, + "bounds": { + "transitions": "2048*V+2048 excluding callee", + "visited_cells": "64*V+64 including endpoints and callee return" + }, + "callee_semantics_remain_conditional": true, + "cases_sha256": "3c3c584c2fa23e5c024579e778fb693938feb0f8446dacb239ba66289ec07c74", + "instructions": 589, + "max_steps": 16217, + "negative_checker_rejects_bad_cleanup": true, + "program_sha256": "0c1c46c163311ac03ce95ab456d53cae0584c7071b4464c3c3b9a1cbb652b545", + "rejected": [ + "aliased-physical-port", + "aliased-return-port", + "zero-descriptor", + "noncanonical-descriptor", + "empty-descriptor", + "nonbinary-descriptor", + "stock-exceeds-rows", + "short-source", + "long-source", + "short-return", + "long-return", + "dirty-added-fibre", + "wrong-return-head", + "wrong-borrowed-head" + ], + "scope": "All-width written local-controller proof; finite source-bound adapter calibration, no native supplier admission", + "source": { + "actual_fixture": { + "S": 3, + "added_bits": 12, + "body": 6, + "borrowed": true, + "f": 1, + "genuine_bits": 60, + "high_width": 3, + "k": 1, + "padded_bits": 72, + "prefixes": 2, + "q": 5, + "rows": 5, + "w": 4 + }, + "inputs": 11, + "retained_padding_sha256": "9f58bf2d343e13a70dc765d86c590b912d5987669d507ab14bd36deed94a76ee", + "source_owners": [ + 462, + 461 + ], + "source_padding_lifetimes": 80 + }, + "status": "PASS_COMPLETE_FIBRE_ROW_PADDING", + "successful_cases": 126, + "tapes": 15, + "translated_fixture": [ + 2, + 5, + 3, + 6, + 1996, + 4557, + 327 + ] +} diff --git a/research/bit-row-padding-physical/SOURCES.json b/research/bit-row-padding-physical/SOURCES.json new file mode 100644 index 0000000000..c8f4c16909 --- /dev/null +++ b/research/bit-row-padding-physical/SOURCES.json @@ -0,0 +1,84 @@ +{ + "schema_version": 1, + "base_commit": "4c0a359d88f22f05189d51f48387750b801a45d4", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/bit-completed-backend-api/BUDGET.md", + "usage": "input", + "git_blob": "e2d2b15230a944370835628efbd775ab31f5c25f", + "sha256": "800643f2176563aea7e58465e0ffda83ad1c84b79ec5b7be5d27095d077117e6" + }, + { + "path": "research/bit-completed-backend-api/science/PROOF.md", + "usage": "input", + "git_blob": "a2db2c2babcff7bfaec3f9a9fdec8fc113c7cf8a", + "sha256": "61d40f649f0afc6116c05dbe370323dd5f38849214d37eb983a4101410818b0b" + }, + { + "path": "research/bit-row-route-generator/PROGRAM.json.gz", + "usage": "input", + "git_blob": "2df37028f46614301118980ad14d2b3f80e43c31", + "sha256": "83448ca22ef773847b748d62f19ea80b2a51c53913ce22624003b6170be7044c" + }, + { + "path": "research/bit-row-route-generator/PROOF.md", + "usage": "input", + "git_blob": "358ba70e944e8bbef3504da5d59089255b4ded9f", + "sha256": "b620b2fbca0261972f96585f5adfd170fc0aa9591a9952d8cc6d7aac327737c3" + }, + { + "path": "research/bit-row-route-generator/README.md", + "usage": "input", + "git_blob": "a9ba8ecf5890b72c9dc51dc31f312e39023f8d7e", + "sha256": "9b392af5561fc6669ea3b049940f194087132c0937821869e0a429c732630fe8" + }, + { + "path": "research/bit-row-route-generator/generator.py", + "usage": "input", + "git_blob": "30015c270b483fae9889246aa7a66768012bbed7", + "sha256": "c3721d4f52bf431b2f1d4464e08088fcf2b453215308dd4a8bef221e61122885" + }, + { + "path": "research/bit-row-route-generator/interpreter.py", + "usage": "input", + "git_blob": "90f79f9d7e7bf57d392ca51232596809d51fc0a8", + "sha256": "10b68232a7b642e7746393b505326fbf6832e7d64c1e0ddc3858835ae74283f9" + }, + { + "path": "research/physical-ordinary-interchange/inputs/pr2808.tar", + "usage": "input", + "git_blob": "191b0b3342d12a630d60643439afa3284641c2d5", + "sha256": "2ab59c6d0ad00c001ecbe44090b66871ec3d2c1fdc51daa503109e56f3285cab" + }, + { + "path": "research/strict-padding-borrowing/ENGINEERING.md", + "usage": "input", + "git_blob": "8fabb603faab8091b49f175fd171e01352199be6", + "sha256": "eaefc1fed8a9b98dd2caf53974e5ef171544e79f78574941e2ec2edf9984e230" + }, + { + "path": "research/strict-padding-borrowing/README.md", + "usage": "input", + "git_blob": "74a0e31f8e11479357d5acca83587f9c7ac8afcb", + "sha256": "3bfd84b54082ae9c9ee029a9f9bdb446d1fcfb4e936bad5c72ca9b7c63bb15ea" + }, + { + "path": "research/strict-padding-borrowing/tape_padding.py", + "usage": "input", + "git_blob": "e689e619cb39c454a666eb2b23be6edb2b8b279b", + "sha256": "6b3598647102a64ef6f5c513a9a5c414f2872f1705b979b6d96177c418273e60" + } + ] +} diff --git a/research/bit-row-padding-physical/TASK.json b/research/bit-row-padding-physical/TASK.json new file mode 100644 index 0000000000..bdcd5e4c28 --- /dev/null +++ b/research/bit-row-padding-physical/TASK.json @@ -0,0 +1,96 @@ +{ + "schema_version": 1, + "task_id": "supplier-boundary-audit", + "priority_revision": 7, + "base_commit": "4c0a359d88f22f05189d51f48387750b801a45d4", + "original_card": { + "id": "supplier-boundary-audit", + "question": "Can the #4088 four-provider dispatch satisfy the complete ordinary/outer admission contract?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/staged544-mixed-fourth-entry/README.md", + "research/scatter-boundary-decision/README.md" + ], + "methods": [ + "Trace one hypothesis through the source, checker and complete caller.", + "Construct one semantically invalid but superficially well-formed fixture and test rejection." + ], + "acceptance_gate": "Pin the current sources and one obligation; the historical owner audit is an example, not evidence of a current bug.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #4088 Scope and Open next questions: local words, native receipts and literal fill do not include a rerun of the mixed four-provider ordinary/outer engine. #3801 is the newer scatter-boundary decision; do not restart #2977 as if untouched.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Pin the provider registry, four native source closures and dispatch. Make a bounded acceptance coverage map or one registry adapter preserving every inherited admission predicate and rejection control (including an omitted fourth provider). Record remaining ordinary/outer obligations and a resource estimate before heavy execution. Stop at unresolved source/caller dependencies; no selected-result promotion from a local pass.", + "bottleneck_link": "Closing a current acceptance gap or proof obligation strengthens reliability even without changing kappa.", + "allowed_variations": [ + "One provider-registry, dispatch, native-closure or admission-predicate obligation; separate branches must name distinct coverage." + ], + "scope_change_triggers": [ + "Reporting the historical timing-only diagnostic as a new current acceptance bug.", + "Calling a malformed mutant a failure of the selected construction, or importing an opt-in repair without testing the exporter boundary.", + "Running another root enclosure instead of validating dispatch or weakening an inherited predicate to make mixed admission pass." + ], + "overlap_terms": [ + "owner boundary", + "bridge omission", + "hosting", + "2977", + "scatter export", + "duplicate index", + "parity semantics", + "4088", + "3801", + "staged544-mixed-fourth-entry", + "scatter-boundary-decision" + ], + "existing_checks": [ + { + "scope": "PR #4088: author-checked local words, native receipts, owner/phase fill and exact moment.", + "evidence": "research/staged544-mixed-fourth-entry/README.md", + "remaining": "Rebind and validate ordinary/outer admission with all four providers; full mixed release not established.", + "status": "author-checked", + "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3801: successor scatter-boundary decision package.", + "evidence": "research/scatter-boundary-decision/README.md", + "remaining": "Consult its exact acceptance scope before any new exporter audit; not proof of a selected failure.", + "status": "author-checked", + "source_commit": "911f8800ba7a4b03603ef62c5ffc6240e53cb5fd", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Fixed finite local-tape complete-fibre ROW padding, completed-return restriction and owned cleanup at the actual helper462/frame506 borrowed matcher boundary.", + "scope_change_reason": "The older four-provider finite registry gap is covered by PR4180. This answers the public PR4957/PR4989 physical primitive handoff, retaining PR3503 arithmetic and bounded scans while supplying all-width local control and explicit costs.", + "bottleneck_link": "Replaces host Count loops and row metadata at one actual paid ROW interface with a fixed tape controller; native callee and P3 admission remain explicit.", + "budget_minutes": 60, + "stop_rule": "Stop at an unpriced operation or missing callee invariant; do not repeat padding ratio arithmetic or promote full supplier admission.", + "outcome": "completed", + "evidence": "PROOF.md, machine.py, verify.py and RESULT.json; 126 finite cases, full actual 80-call schedule binding, semantic and cleanup controls. Canonical discussioncomment-19141335.", + "author": "JoyboyBrian", + "ai_assistance": "JoyboyBrian with substantial OpenAI Codex assistance; separate agent code/proof review, no human or proof-kernel acceptance.", + "open_questions": [ + { + "question": "Can an actual completed native/raw callback satisfy this physical ROW boundary?", + "why_it_matters": "Adapter correctness alone does not admit the completed supplier.", + "first_step": "Bind source inner_return to an actual row-pointwise distinct-output callback and account for every original/other high field.", + "blocked_by": "Native/compiler/precision and physical callee contracts remain inherited." + }, + { + "question": "Can the controller be installed into the full selected serialization with actual P3 constants?", + "why_it_matters": "The complete matcher cover is much larger than its bounded interface calibration.", + "first_step": "Map every actual body and spectator factor into P and B and retain per-call volumes.", + "blocked_by": "Full selected fixed-program reserve, precision and tape contracts." + } + ] +} diff --git a/research/bit-row-padding-physical/VERIFY.json b/research/bit-row-padding-physical/VERIFY.json new file mode 100644 index 0000000000..ee2c47c6f4 --- /dev/null +++ b/research/bit-row-padding-physical/VERIFY.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/bit-completed-backend-api/BUDGET.md", + "research/bit-completed-backend-api/science/PROOF.md", + "research/bit-row-route-generator/PROGRAM.json.gz", + "research/bit-row-route-generator/PROOF.md", + "research/bit-row-route-generator/README.md", + "research/bit-row-route-generator/generator.py", + "research/bit-row-route-generator/interpreter.py", + "research/physical-ordinary-interchange/inputs/pr2808.tar", + "research/strict-padding-borrowing/ENGINEERING.md", + "research/strict-padding-borrowing/README.md", + "research/strict-padding-borrowing/tape_padding.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-Werror", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Complete source-bound fibre controller, finite byte oracle and cleanup controls" + }, + { + "argv": [ + "{python}", + "-Werror", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Same explicit guards and semantic-premise controls without assertions" + } + ] +} diff --git a/research/bit-row-padding-physical/machine.py b/research/bit-row-padding-physical/machine.py new file mode 100644 index 0000000000..1e3533efa9 --- /dev/null +++ b/research/bit-row-padding-physical/machine.py @@ -0,0 +1,321 @@ +"""Finite local control for full-fibre compatible ROW padding. + +JoyboyBrian, with substantial OpenAI Codex assistance. Apache-2.0. +Semantics follow Jose Manuel PR2786 and Nick Petalas PR3503; neither frozen +implementation is changed. Each executed instruction observes one local cell. +""" +from dataclasses import dataclass + +BLANK = "_" +LEFT = "|" +SOURCE, PD, RD, SD, BD, P, R, S, B, D, TEMP, ROWS, PAD, RETURN, OUTPUT = range(15) +TAPES = 15 + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +class Builder: + def __init__(self): + self.code = [] + self.labels = {} + self.serial = 0 + self.rejection = "reject" + + def fresh(self, prefix): + self.serial += 1 + return prefix + str(self.serial) + + def mark(self, name): + need(name not in self.labels, "unique control label") + self.labels[name] = len(self.code) + + def read(self, tape, branches): + complete = {symbol: ("quarantine" if symbol == LEFT else self.rejection) + for symbol in ("0", "1", BLANK, LEFT)} + complete.update(branches) + self.code.append(("read", tape, complete)) + + def write(self, tape, symbol): + self.code.append(("write", tape, symbol)) + + def move(self, tape, direction): + self.code.append(("move", tape, direction)) + + def go(self, label): + self.code.append(("goto", label)) + + def rewind(self, tape): + loop, done = self.fresh("rewind"), self.fresh("rewound") + self.mark(loop) + self.read(tape, {LEFT: done, "0": loop + "step", "1": loop + "step", BLANK: loop + "step"}) + self.mark(loop + "step") + self.move(tape, -1) + self.go(loop) + self.mark(done) + self.move(tape, 1) + + def clear(self, tape): + self.rewind(tape) + loop, erase, done = self.fresh("clear"), self.fresh("erase"), self.fresh("cleared") + self.mark(loop) + self.read(tape, {"0": erase, "1": erase, BLANK: done}) + self.mark(erase) + self.write(tape, BLANK) + self.move(tape, 1) + self.go(loop) + self.mark(done) + self.rewind(tape) + + def boundary(self, tape): + good = self.fresh("boundary") + previous = self.rejection + self.rejection = "quarantine" + self.move(tape, -1) + self.read(tape, {LEFT: good}) + self.mark(good) + self.move(tape, 1) + self.rejection = previous + + def unary(self, descriptor, output): + # Canonical LSF positive binary input; last digit must be one. + zero, one, done = self.fresh("lastzero"), self.fresh("lastone"), self.fresh("copied") + self.mark(zero) + self.read(descriptor, {"0": zero + "bit", "1": one + "bit"}) + self.mark(one) + self.read(descriptor, {"0": zero + "bit", "1": one + "bit", BLANK: done}) + for state, bit in ((zero, "0"), (one, "1")): + self.mark(state + "bit") + self.write(TEMP, bit) + self.move(TEMP, 1) + self.move(descriptor, 1) + self.go(state) + self.mark(done) + self.rewind(descriptor) + self.rewind(TEMP) + loop, borrow, unit, tail, trim, append, end = [self.fresh("decode") for _ in range(7)] + self.mark(loop) + self.read(TEMP, {BLANK: end, "0": borrow, "1": unit}) + self.mark(borrow) + self.write(TEMP, "1") + self.move(TEMP, 1) + self.read(TEMP, {"0": borrow, "1": unit}) + self.mark(unit) + self.write(TEMP, "0") + self.move(TEMP, 1) + self.read(TEMP, {BLANK: trim, "0": tail, "1": tail}) + self.mark(trim) + self.move(TEMP, -1) + self.write(TEMP, BLANK) + self.mark(tail) + self.rewind(TEMP) + self.mark(append) + self.write(output, "1") + self.move(output, 1) + self.go(loop) + self.mark(end) + self.rewind(output) + + def increment(self, tape): + loop, carry, setone, done = [self.fresh("increment") for _ in range(4)] + self.mark(loop) + self.read(tape, {"1": carry, "0": setone, BLANK: setone}) + self.mark(carry) + self.write(tape, "0") + self.move(tape, 1) + self.go(loop) + self.mark(setone) + self.write(tape, "1") + self.mark(done) + self.rewind(tape) + + def plan(self): + compare, more, fits = [self.fresh("cover") for _ in range(3)] + self.mark(compare) + self.read(S, {BLANK: fits, "1": more}) + self.mark(more) + good = self.fresh("covered") + self.read(R, {"1": good}) + self.mark(good) + self.move(S, 1) + self.move(R, 1) + self.go(compare) + self.mark(fits) + self.rewind(R) + self.rewind(S) + row, group, exact, partial, drain, padding, finish = [self.fresh("plan") for _ in range(7)] + self.mark(row) + self.increment(ROWS) + self.move(R, 1) + self.move(S, 1) + self.read(S, {BLANK: exact, "1": partial}) + self.mark(exact) + self.rewind(S) + self.read(R, {BLANK: finish, "1": row}) + self.mark(partial) + self.read(R, {BLANK: drain, "1": row}) + self.mark(drain) + self.read(S, {BLANK: finish, "1": padding}) + self.mark(padding) + self.write(D, "1") + self.move(D, 1) + self.increment(ROWS) + self.move(S, 1) + self.go(drain) + self.mark(finish) + for tape in (R, S, D): + self.rewind(tape) + + def rows(self, source, output, count, mode): + rows, row, body, bit, zero, one, endbody, end = [self.fresh("scan") for _ in range(8)] + self.mark(rows) + self.read(count, {"1": row, BLANK: end}) + self.mark(row) + self.mark(body) + self.read(B, {"1": bit, BLANK: endbody}) + self.mark(bit) + if mode == "zero": + self.write(output, "0") + self.move(output, 1) + else: + self.read(source, {"0": zero, **({"1": one} if mode == "copy" else {})}) + self.mark(zero) + if mode == "copy": + self.write(output, "0") + self.go(one + "copied") + self.mark(one) + self.write(output, "1") + self.mark(one + "copied") + self.move(output, 1) + self.move(source, 1) + self.move(B, 1) + self.go(body) + self.mark(endbody) + self.rewind(B) + self.move(count, 1) + self.go(rows) + self.mark(end) + self.rewind(count) + + def transform(self, source, output, restricting): + prefix, run, end, exact = [self.fresh("transform") for _ in range(4)] + self.mark(prefix) + self.read(P, {"1": run, BLANK: end}) + self.mark(run) + self.rows(source, output, R, "copy") + self.rows(source, output, D, "discard" if restricting else "zero") + self.move(P, 1) + self.go(prefix) + self.mark(end) + self.read(source, {BLANK: exact}) + self.mark(exact) + for tape in (P, source, output): + self.rewind(tape) + + def finish(self): + result = [] + for instruction in self.code: + if instruction[0] == "goto": + result.append(("goto", self.labels[instruction[1]])) + elif instruction[0] == "read": + result.append(("read", instruction[1], + {k: self.labels[v] for k, v in instruction[2].items()})) + else: + result.append(instruction) + return tuple(result) + + +def program(): + b = Builder() + for descriptor, output in ((PD, P), (RD, R), (SD, S), (BD, B)): + b.unary(descriptor, output) + b.plan() + b.transform(SOURCE, PAD, False) + b.code.append(("call",)) + # Borrowed contents are a semantic callee premise. These local checks + # enforce only the returned boundary-marker positions, not that premise. + for tape in (SOURCE, PD, RD, SD, BD, ROWS, PAD, RETURN): + b.boundary(tape) + b.transform(RETURN, OUTPUT, True) + for tape in (P, R, S, B, D, TEMP, ROWS, PAD, RETURN): + b.clear(tape) + b.code.append(("done",)) + # Well-formed-tape data errors retain reliable left markers. Recover + # borrowed heads and erase owned work using the same local scans. + b.mark("reject") + b.rejection = "quarantine" + for tape in (P, R, S, B, D, TEMP, ROWS, PAD, RETURN, OUTPUT): + b.clear(tape) + for tape in (SOURCE, PD, RD, SD, BD): + b.rewind(tape) + b.code.append(("rejected",)) + b.mark("quarantine") + b.code.append(("quarantined",)) + return b.finish() + + +PROGRAM = program() + + +@dataclass +class Tape: + cells: dict + head: int = 1 + low: int = 0 + high: int = 0 + + @classmethod + def fixture(cls, text="", origin=0): + return cls({origin: LEFT, **{origin + i + 1: c for i, c in enumerate(text)}}, + origin + 1, origin, origin + len(text)) + + def read(self): + self.low = min(self.low, self.head) + self.high = max(self.high, self.head) + return self.cells.get(self.head, BLANK) + + +class Machine: + """A table interpreter, not a host implementation of padding/counting.""" + def __init__(self, tapes): + need(len(tapes) == TAPES, "fixed fifteen tapes") + need(len({id(tape) for tape in tapes}) == TAPES, "distinct physical tape ports") + self.tapes = tapes + self.pc = 0 + self.steps = 0 + self.calls = 0 + + def run(self, budget=10000000): + need(len({id(tape) for tape in self.tapes}) == TAPES, "distinct physical tape ports") + while self.steps < budget: + instruction = PROGRAM[self.pc] + op = instruction[0] + self.steps += 1 + if op in ("rejected", "quarantined"): + raise ValueError(op) + if op in ("done", "call"): + if op == "call": + self.pc += 1 + self.calls += 1 + return op + if op == "goto": + self.pc = instruction[1] + continue + tape = self.tapes[instruction[1]] + if op == "read": + symbol = tape.read() + need(symbol in instruction[2], "local guard rejected at state " + str(self.pc)) + self.pc = instruction[2][symbol] + continue + if op == "write": + tape.read() + tape.cells[tape.head] = instruction[2] + elif op == "move": + tape.head += instruction[2] + tape.read() + else: + raise ValueError("unknown local opcode") + self.pc += 1 + raise ValueError("test execution budget exhausted") diff --git a/research/bit-row-padding-physical/verify.py b/research/bit-row-padding-physical/verify.py new file mode 100644 index 0000000000..3fc6f54a04 --- /dev/null +++ b/research/bit-row-padding-physical/verify.py @@ -0,0 +1,269 @@ +#!/usr/bin/env python3 +"""Independent byte oracle and source-bound finite calibration; not callee admission.""" +import argparse +import gzip +import hashlib +import json +from pathlib import Path +import tarfile + +from machine import (Machine, Tape, PROGRAM, TAPES, BLANK, LEFT, SOURCE, PD, RD, + SD, BD, P, R, S, B, D, TEMP, ROWS, PAD, RETURN, OUTPUT, need) + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def binary(value): + return bin(value)[2:][::-1] + + +def word(tape, origin): + # Test observation only, never called by the finite controller. + result = [] + position = origin + 1 + while tape.cells.get(position, BLANK) != BLANK: + result.append(tape.cells[position]) + position += 1 + return "".join(result) + + +def snapshot(tape): + return dict(tape.cells), tape.head + + +def fixture(p, r, s, b, payload, origins=None): + origins = origins or [0] * TAPES + tapes = [Tape.fixture(origin=origin) for origin in origins] + tapes[SOURCE] = Tape.fixture(payload, origins[SOURCE]) + for index, value in zip((PD, RD, SD, BD), (p, r, s, b)): + tapes[index] = Tape.fixture(binary(value), origins[index]) + return tapes, origins + + +def oracle_pad(payload, p, r, s, b): + padded_rows = (r + s - 1) // s * s + return "".join(payload[i*r*b:(i+1)*r*b] + "0"*((padded_rows-r)*b) + for i in range(p)), padded_rows + + +def oracle_callee(payload, b): + # Explicit synthetic completed row-pointwise callback, not a native body. + return "".join(payload[i:i+b][::-1] for i in range(0, len(payload), b)) + + +def trial(p, r, s, b, payload, origins=None): + tapes, origins = fixture(p, r, s, b, payload, origins) + borrowed = [snapshot(tapes[i]) for i in range(5)] + machine = Machine(tapes) + need(machine.run() == "call", "one completed-row call boundary") + padded, padded_rows = oracle_pad(payload, p, r, s, b) + need(word(tapes[PAD], origins[PAD]) == padded, "all padded fibres") + need(word(tapes[ROWS], origins[ROWS]) == binary(padded_rows), "paid binary row count") + before_call = machine.steps + # The theorem retains this callee premise. Its semantic check here is + # an oracle observation, not a hidden instruction or runtime admission. + tapes[RETURN] = Tape.fixture(oracle_callee(padded, b), origins[RETURN]) + need(machine.run() == "done" and machine.calls == 1, "one complete return") + need(word(tapes[OUTPUT], origins[OUTPUT]) == oracle_callee(payload, b), + "genuine rows and spectators through restriction") + need([snapshot(tapes[i]) for i in range(5)] == borrowed, "borrowed bytes and heads") + for index in (P, R, S, B, D, TEMP, ROWS, PAD, RETURN): + tape = tapes[index] + need(tape.head == origins[index] + 1 and + all(symbol == BLANK or (position == origins[index] and symbol == LEFT) + for position, symbol in tape.cells.items()), "owned visited backing erased") + need(tapes[OUTPUT].head == origins[OUTPUT] + 1, "owned output boundary") + volume = p*r*b + visited = sum(t.high-t.low+1 for t in tapes) + need(machine.steps <= 2048*volume + 2048, "proved transition envelope") + need(visited <= 64*volume + 64, "proved visited-space envelope") + return [p, r, s, b, before_call, machine.steps, visited] + + +def rejects(label, operation): + try: + operation() + except ValueError as error: + expected={"aliased-physical-port":"distinct physical tape ports", + "aliased-return-port":"distinct physical tape ports", + "wrong-return-head":"quarantined", + "wrong-borrowed-head":"quarantined"}.get(label,"rejected") + if label=="nonbinary-descriptor": + if not str(error).startswith("local guard rejected at state "): + raise RuntimeError("wrong nonbinary rejection") from error + elif str(error)!=expected: + raise RuntimeError("wrong rejection for "+label+": "+str(error)) from error + return label + raise ValueError("invalid case accepted: " + label) + + +def check(condition, message): + if not condition: + raise RuntimeError(message) + + +def checked_rejection(machine, recover=True): + tapes=machine.tapes + before=[dict(t.cells) for t in tapes[:5]] + origins=[next(k for k,v in t.cells.items() if v==LEFT) for t in tapes] + try: + machine.run() + except ValueError as error: + if recover: + check(str(error)=="rejected", "fixed cleanup rejection") + check([dict(t.cells) for t in tapes[:5]]==before, "reject preserves borrowed bytes") + check(all(t.head==origins[i]+1 for i,t in enumerate(tapes)), "reject rewinds all heads") + check(all(all(v==BLANK or (k==origins[i] and v==LEFT) for k,v in t.cells.items()) + for i,t in enumerate(tapes) if i>=5), "reject erases all owned backing") + raise + raise RuntimeError("expected failure did not occur") + + +def failure_controls(): + rejected = [] + def aliased(): + tapes, _ = fixture(2,5,3,6,"1"*60) + tapes[PAD] = tapes[SOURCE] + Machine(tapes) + rejected.append(rejects("aliased-physical-port", aliased)) + def return_alias(): + tapes,_=fixture(2,5,3,6,"1"*60) + machine=Machine(tapes) + check(machine.run()=="call", "return alias reaches call") + tapes[RETURN]=tapes[SOURCE] + machine.run() + rejected.append(rejects("aliased-return-port", return_alias)) + for label, descriptor in (("zero", "0"), ("noncanonical", "10"), + ("empty", ""), ("nonbinary", "x")): + def bad(value=descriptor): + tapes, _ = fixture(2, 5, 3, 6, "1"*60) + tapes[PD] = Tape.fixture(value) + checked_rejection(Machine(tapes), value!="x") + rejected.append(rejects(label + "-descriptor", bad)) + rejected.append(rejects("stock-exceeds-rows", + lambda: checked_rejection(Machine(fixture(1, 2, 3, 2, "1010")[0])))) + for label, payload in (("short-source", "1"*59), ("long-source", "1"*61)): + rejected.append(rejects(label, lambda data=payload: + checked_rejection(Machine(fixture(2, 5, 3, 6, data)[0])))) + for label in ("short-return", "long-return", "dirty-added-fibre", + "wrong-return-head", "wrong-borrowed-head"): + def bad(kind=label): + tapes, origins = fixture(2, 5, 3, 6, "1"*60) + machine = Machine(tapes) + check(machine.run() == "call", "failure control call") + data = oracle_callee(word(tapes[PAD], 0), 6) + if kind == "short-return": + data = data[:-1] + elif kind == "long-return": + data += "0" + elif kind == "dirty-added-fibre": + data = data[:30] + "1" + data[31:] + tapes[RETURN] = Tape.fixture(data) + if kind == "wrong-return-head": + tapes[RETURN].head += 1 + if kind == "wrong-borrowed-head": + tapes[RD].head += 1 + checked_rejection(machine, kind not in ("wrong-return-head", "wrong-borrowed-head")) + rejected.append(rejects(label, bad)) + # Complete-return ownership and semantics are NOT runtime oracle checks. + # A mutation violating the semantic premise can preserve padding zeros. + tapes, _ = fixture(2, 5, 3, 6, "1"*60) + machine = Machine(tapes) + check(machine.run() == "call", "premise separation call") + tapes[RETURN] = Tape.fixture("0"*72) + check(machine.run() == "done" and word(tapes[OUTPUT], 0) == "0"*60, + "zero checks do not certify the completed-callee semantic premise") + # A faulty cleanup assertion must escape the expected-rejection catcher. + class BadCleanup: + def __init__(self): + self.tapes=fixture(2,5,3,6,"1"*60)[0] + self.tapes[P]=Tape.fixture("1") + def run(self): + raise ValueError("rejected") + try: + rejects("zero-descriptor", lambda: checked_rejection(BadCleanup())) + except RuntimeError as error: + check(str(error)=="reject erases all owned backing", "precise checker mutation") + else: + raise RuntimeError("negative-control checker swallowed bad cleanup") + return rejected + + +def source_binding(): + manifest = json.loads((HERE / "SOURCES.json").read_text()) + rows = [row for row in manifest["files"] if row["usage"] == "input"] + for row in rows: + need(hashlib.sha256((ROOT / row["path"]).read_bytes()).hexdigest() == row["sha256"], + "exact input " + row["path"]) + source = ROOT / "research/bit-row-route-generator" + generator = (source / "generator.py").read_text() + interpreter = (source / "interpreter.py").read_text() + need("if 2*borrowed_digits