diff --git a/.github/workflows/p112-common-slice.yml b/.github/workflows/p112-common-slice.yml index 37f99ca573..48047f61c4 100644 --- a/.github/workflows/p112-common-slice.yml +++ b/.github/workflows/p112-common-slice.yml @@ -15,9 +15,9 @@ jobs: if: github.repository == 'CrocSwap/integer-mult-bounds' runs-on: ubuntu-24.04 timeout-minutes: 20 - env: - TMPDIR: ${{ runner.temp }}/p112-common-slice steps: + - name: Initialise P112 work directory + run: echo "TMPDIR=$RUNNER_TEMP/p112-common-slice" >> "$GITHUB_ENV" - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 with: fetch-depth: 0 diff --git a/research/rank-profile-retiming-obstruction/.gitattributes b/research/rank-profile-retiming-obstruction/.gitattributes new file mode 100644 index 0000000000..fa1385d99a --- /dev/null +++ b/research/rank-profile-retiming-obstruction/.gitattributes @@ -0,0 +1 @@ +* -text diff --git a/research/rank-profile-retiming-obstruction/.gitignore b/research/rank-profile-retiming-obstruction/.gitignore new file mode 100644 index 0000000000..43ae0e2a6c --- /dev/null +++ b/research/rank-profile-retiming-obstruction/.gitignore @@ -0,0 +1,2 @@ +__pycache__/ +*.py[cod] diff --git a/research/rank-profile-retiming-obstruction/CENSUS.json b/research/rank-profile-retiming-obstruction/CENSUS.json new file mode 100644 index 0000000000..c9db55a477 --- /dev/null +++ b/research/rank-profile-retiming-obstruction/CENSUS.json @@ -0,0 +1 @@ +{"base":{"candidates":1776295,"deltas":[{"caps":[0,2,0,0,0,0,0,0,0],"certificate":true,"count":5404,"delta":{"1":-2,"2":4,"3":-2}},{"caps":[0,1,1,0,0,0,0,0,0],"certificate":true,"count":8908,"delta":{"1":-1,"2":1,"3":1,"4":-1}},{"caps":[0,0,0,0,0,0,0,0,0],"certificate":true,"count":1536697,"delta":{}},{"caps":[1,2,1,0,0,0,0,0,0],"certificate":true,"count":9311,"delta":{"2":2,"4":-1}},{"caps":[1,2,0,0,0,0,0,0,0],"certificate":true,"count":2498,"delta":{"2":3,"3":-2}},{"caps":[2,4,2,0,0,0,0,0,0],"certificate":true,"count":18680,"delta":{"2":4,"4":-2}},{"caps":[1,1,1,0,0,0,0,0,0],"certificate":true,"count":7458,"delta":{"1":1,"3":1,"4":-1}},{"caps":[1,1,0,0,0,0,0,0,0],"certificate":true,"count":31273,"delta":{"1":1,"2":1,"3":-1}},{"caps":[1,1,-1,0,0,0,0,0,0],"certificate":true,"count":2755,"delta":{"1":1,"2":2,"3":-3,"4":1}},{"caps":[2,3,1,0,0,0,0,0,0],"certificate":true,"count":7120,"delta":{"1":1,"2":3,"3":-1,"4":-1}},{"caps":[1,0,1,1,0,0,0,0,0],"certificate":true,"count":1630,"delta":{"1":2,"2":-2,"3":1,"4":1,"5":-1}},{"caps":[1,0,1,0,0,0,0,0,0],"certificate":true,"count":294,"delta":{"1":2,"2":-2,"3":2,"4":-1}},{"caps":[1,0,0,0,0,0,0,0,0],"certificate":true,"count":3762,"delta":{"1":2,"2":-1}},{"caps":[2,2,2,0,0,0,0,0,0],"certificate":true,"count":37360,"delta":{"1":2,"3":2,"4":-2}},{"caps":[2,2,1,0,0,0,0,0,0],"certificate":true,"count":7120,"delta":{"1":2,"2":1,"4":-1}},{"caps":[2,2,0,0,0,0,0,0,0],"certificate":true,"count":40432,"delta":{"1":2,"2":2,"3":-2}},{"caps":[2,1,1,0,0,0,0,0,0],"certificate":true,"count":84,"delta":{"1":3,"2":-1,"3":1,"4":-1}},{"caps":[2,1,0,0,0,0,0,0,0],"certificate":true,"count":5695,"delta":{"1":3,"3":-1}},{"caps":[2,0,0,0,0,0,0,0,0],"certificate":true,"count":49814,"delta":{"1":4,"2":-2}}],"per_section":{"A":1451231,"B":308890,"restore":16174},"source_profile":{"1":2440,"2":725,"3":224,"4":102,"5":20,"8":8}},"extra":{"candidates":1776295,"deltas":[{"caps":[0,2,0,0,0,0,0,0,0],"certificate":true,"count":5404,"delta":{"1":-2,"2":4,"3":-2}},{"caps":[0,1,1,0,0,0,0,0,0],"certificate":true,"count":8908,"delta":{"1":-1,"2":1,"3":1,"4":-1}},{"caps":[0,0,0,0,0,0,0,0,0],"certificate":true,"count":1536697,"delta":{}},{"caps":[1,2,1,0,0,0,0,0,0],"certificate":true,"count":9311,"delta":{"2":2,"4":-1}},{"caps":[1,2,0,0,0,0,0,0,0],"certificate":true,"count":2498,"delta":{"2":3,"3":-2}},{"caps":[2,4,2,0,0,0,0,0,0],"certificate":true,"count":18680,"delta":{"2":4,"4":-2}},{"caps":[1,1,1,0,0,0,0,0,0],"certificate":true,"count":7458,"delta":{"1":1,"3":1,"4":-1}},{"caps":[1,1,0,0,0,0,0,0,0],"certificate":true,"count":31273,"delta":{"1":1,"2":1,"3":-1}},{"caps":[1,1,-1,0,0,0,0,0,0],"certificate":true,"count":2755,"delta":{"1":1,"2":2,"3":-3,"4":1}},{"caps":[2,3,1,0,0,0,0,0,0],"certificate":true,"count":7120,"delta":{"1":1,"2":3,"3":-1,"4":-1}},{"caps":[1,0,1,1,0,0,0,0,0],"certificate":true,"count":1630,"delta":{"1":2,"2":-2,"3":1,"4":1,"5":-1}},{"caps":[1,0,1,0,0,0,0,0,0],"certificate":true,"count":294,"delta":{"1":2,"2":-2,"3":2,"4":-1}},{"caps":[1,0,0,0,0,0,0,0,0],"certificate":true,"count":3762,"delta":{"1":2,"2":-1}},{"caps":[2,2,2,0,0,0,0,0,0],"certificate":true,"count":37360,"delta":{"1":2,"3":2,"4":-2}},{"caps":[2,2,1,0,0,0,0,0,0],"certificate":true,"count":7120,"delta":{"1":2,"2":1,"4":-1}},{"caps":[2,2,0,0,0,0,0,0,0],"certificate":true,"count":40432,"delta":{"1":2,"2":2,"3":-2}},{"caps":[2,1,1,0,0,0,0,0,0],"certificate":true,"count":84,"delta":{"1":3,"2":-1,"3":1,"4":-1}},{"caps":[2,1,0,0,0,0,0,0,0],"certificate":true,"count":5695,"delta":{"1":3,"3":-1}},{"caps":[2,0,0,0,0,0,0,0,0],"certificate":true,"count":49814,"delta":{"1":4,"2":-2}}],"per_section":{"A":1451231,"B":308890,"restore":16174},"source_profile":{"1":2440,"2":725,"3":224,"4":102,"5":20,"8":8}}} diff --git a/research/rank-profile-retiming-obstruction/PROOF.md b/research/rank-profile-retiming-obstruction/PROOF.md new file mode 100644 index 0000000000..a565bbb9ed --- /dev/null +++ b/research/rank-profile-retiming-obstruction/PROOF.md @@ -0,0 +1,128 @@ +# Finite retiming obstruction and its scope + +## 1. Scalar correctness does not license arbitrary rank exchanges + +For a scalar addition `g = I + c E_ds`, an addition `h = I + b E_uv` +commutes under the sufficient condition `d != v` and `u != s`. This is obtained +by multiplying the two elementary matrices. A diagonal scale by q at d changes +c to qc when g is moved right across the scale; a scale at s changes c to c/q. +Moving left reverses those factors. These identities hold on arbitrary inputs, +including dirty helpers. All source scales in the retained words are nonzero +powers of two. The transformed addition remains dyadic. No new gate is inserted. + +The class fixes every other instruction, frame, native warp cut, entrance, +centre/target boundary, and helper exit. It is deliberately narrower than all +semantics-preserving circuit rewrites. In particular, the scalar identities do +not make arbitrary pairs of recursive children exchangeable. + +## 2. Complete local frame-price enumeration + +On one of the moved ADD's registers let its old preceding, gate, and following +frames have dimensions p, u, q. Removing this occurrence changes its price by + + f(q-p) - f(u-p) - f(q-u), f(r) = r^(1-a), f(0) = 0. + +The first following fixed constraint may be a true charged climb or a zero-cost +boundary check. For pricing only, the latter is relaxed to a virtual climb to +its required frame. Its charge is zero in the original word and in every legal +candidate, so this is a sound over-approximation. Native maps are preceded by +explicit entrance checks in the trace, and no moved gate crosses such a cut. +The temporary centre descents are billed separately; they do not overwrite the +main forward register's frame. This distinction is checked against the retained +full invoice. + +After removing the ADD, let P1,P2 be the frames immediately before its proposed +position, and Q1,Q2 the first subsequent constraints. The new common frame F +must satisfy + + L = P1 + P2 <= F <= H = Q1 intersect Q2. + +If L is not contained in H, the position is impossible in the relaxation. If +L is contained in H, a basis of L can be extended to a basis of H. Taking each +prefix gives a frame of every dimension from dim L through dim H. Its added +price on register j is + + f(dim F - dim Pj) + f(dim Qj - dim F) - f(dim Qj - dim Pj). + +There are no other changing costs in this relaxed frame invoice. The cost +depends only on dim F. Consequently checking every integer in that interval is +complete over all binary subspaces, not just the chosen basis representatives. +Every legal candidate has exactly one of the enumerated signed histograms. + +The implementation scans every permissible insertion cut in each maximal +scalar corridor, including unchanged placement with a changed frame. Corridors +end at noncommuting ADDs, phase boundaries, the A prelude, or native B warp cuts. +A different corridor is not inferred from an earlier neutral move. Per-register +entry and exit constraints are taken at the actual segment boundaries, so a +pre-warp frame cannot be mistaken for its post-warp image. + +## 3. Exact all-exponent certificate for all 19 deltas + +For a signed new-minus-old histogram d of equal rank mass, put + + C_k = sum_r d_r min(r,k). + +The retained discrete-curvature expansion gives + + sum_r d_r f(r) = sum_{k=1}^{T-1} C_k theta_k, + theta_k = 2 f(k) - f(k-1) - f(k+1). + +For `f(x)=x^(1-a)` and `0= 0` for all j suffices for non-improvement for every a in (0,1). +If d is nonzero and has zero rank mass, at least one S_j is positive, so the +inequality is strict. The zero histogram has equal price. + +All 19 independently regenerated histogram types have zero rank mass and +nonnegative S_j. Eighteen have the simpler nonnegative caps already. The one +mixed-cap type is + + d = {1:1, 2:2, 3:-3, 4:1}, C = (1,1,-1,0,...), + +so its difference is theta_1 + theta_2 - theta_3 > 0. This illustrates why +checking only signs of the individual caps would leave a genuine gap. The +verifier does not infer the all-exponent result from floating-point samples. + +In particular, the proposed `2+2 -> 1+3` change has C_2=-1 and cannot occur among +these candidates. Added nonnegative charges cannot repair a lack of savings +when all normalisers and common costs are held fixed. A simultaneous multi-gate +change, a new frame at another instruction, or a changed boundary escapes the +class and is not excluded. + +## 4. A literal improving control and conditional overhead reserve + +The counterfactual rollback and recovery of the credited PR2957 swap have exact +new-minus-old profile `{1:1,2:-1,3:-1,4:1}`, with C_2=C_3=-1. They pass the +retained arbitrary-dirty free-operator semantics in both orientations after +literal inverse cleanup is rederived. The recovered word is the pinned PR3734 +word, not a newly discovered current improvement. + +PR3863's uniform lower bound at l=17/10000, u=18/10000 gives the raw credit + + L = l(1-u)/(3(1+2u)) + l(1-u)/(4(1+3u)) + = 1491695107/1513529160000. + +For 3240 copies, 3240L-3 = 2437538889/12612743000 > 0. Thus three added rank-1 +children are affordable in this conditional comparison of otherwise unchanged +invoices. This calculation neither supplies those three physical operations nor +admits the counterfactual full supplier. Its purpose is to attach the inherited +pricing theorem to an actual source-level rewrite with checked local boundaries. + +The proof is informal mathematics supported by finite exact Python replay. It +is not a kernel proof of the continuum inequalities or of integer multiplication. diff --git a/research/rank-profile-retiming-obstruction/README.md b/research/rank-profile-retiming-obstruction/README.md new file mode 100644 index 0000000000..9d0fe3b037 --- /dev/null +++ b/research/rank-profile-retiming-obstruction/README.md @@ -0,0 +1,148 @@ +# Source-bound obstruction to single-ADD rank-profile retiming + +**Result.** On both literal PR3734 staged544 providers, no transformation in the +single-ADD class below strictly lowers the raw recursive moment for any real +`0 < a < 1`. The exact over-approximation has **1,776,295 insertion-cut/frame- +dimension candidates per provider**, and just **19 signed histogram changes**. +Every change has an exact all-exponent non-improvement certificate. This rules +out PR3863's proposed `2+2 -> 1+3` exchange through this particular class. It does +not rule out coupled edits, neutral intermediate words, or changed interfaces. + +This is a user-assigned investigation of converting rank-profile savings into +actual circuit transformations, on canonical main +`20ecf2891d80b5acf18d980b2164fb44ea7faa90`, priority revision 6. It is a scoped +negative result and a constructive positive control, not a new supplier or a +new value of kappa. The selected certificate is unchanged. + +## Exact transformation class + +Move exactly one existing scalar ADD within its A, B, or restore phase, after +the A prelude and without crossing any native B warp cut. All other gates and +their frames stay fixed. Crossed ADDs must satisfy the sufficient commuting +condition `destination(g) != source(h)` and `destination(h) != source(g)`. +Crossed nonzero SCALEs are allowed, with the moved coefficient conjugated +exactly. Choose any binary subspace of F_2^9 as the moved gate's common frame. +Keep entrances, target/centre cuts, helper exits, and the rest of the caller +contract fixed. Reconstruct inverse cleanup from the edited word. + +The census includes frame-only changes at the original position. It has no +radius limit. It does not cover crossing a warp, moving a SCALE, cancellation +or deletion, a commutator correction gate, two variable gate frames, moving +across phases, or subsequent edits of a neutral intermediate word. + +For a fixed placement, legal frames lie between the join of the two preceding +frames and the intersection of the two successor constraints. Every intermediate +dimension is achievable. The invoice depends on that dimension, not on which +subspace of that dimension was chosen. Therefore the verifier enumerates every +possible price, rather than sampling bases. Fixed checks are relaxed to virtual +climbs when pricing candidates. Such climbs are zero in every genuinely legal +witness. Proving non-improvement in this larger class proves the stated scoped +obstruction. See PROOF.md for the exact boundary argument. + +| Phase | Candidate cut/dimension pairs, each provider | +| --- | ---: | +| A | 1,451,231 | +| B | 308,890 | +| restore | 16,174 | +| Total | 1,776,295 | + +Counts include distinct placements with the same price. They are not a count of +distinct circuits or all binary frame assignments. CENSUS.json retains every +signed profile and its multiplicity, not only a success flag. The two providers +are checked separately; their literal B frames and native warp maps differ. + +## Constructive control and actual paid credit + +The verifier rolls back one already-retained **Jeremy Kothe PR2957** swap on the +current word, then recovers the original word by an explicit retiming. In current +zero-based addresses, the rollback changes A[4043:4045] from the additions to +register 81 using sources 40 then 17, into sources 17 then 40, with both at the +first gate's rank-7 frame. Moving source 17 back after source 40 and using the +retained rank-8 frame recovers the literal source word, after basis spelling and +the derived report are normalised. + +The per-call profile changes from `{1:2439,2:726,3:225,4:101,5:20,8:8}` to +`{1:2440,2:725,3:224,4:102,5:20,8:8}`. Thus this actual circuit performs the +mass-preserving **`2+3 -> 1+4`** replacement, with no extra scalar gate, helper, +private cleanup buffer, or helper-width change. Both orientations and all 632 +live inputs plus 91 arbitrary dirty buffers are replayed through the retained +free-operator interpreter. This rollback is a counterfactual local control, +not a claim to reproduce the complete historical PR2957 parent supplier. + +Applying Dugongue's PR3863 rational credit to the two negative caps gives +`1491695107/1513529160000` per call, uniformly for +`17/10000 <= a <= 18/10000`. For 3,240 repetitions, this is +`40275767889/12612743000`, strictly greater than three by +`2437538889/12612743000`. Under unchanged normalisers and the complete common +invoice, this can pay three additional rank-1 children. It is an accounting +reserve attached to a credited circuit, not an implemented new overhead or a +new improvement over current staged544, which already contains this swap. +No new physical allocation or outer admission is asserted for the rollback. + +## Reproduce + +Python 3.12, standard library only, no network, solver, native build, or Lean. + +```sh +python3 -B research/rank-profile-retiming-obstruction/verify.py --summary +python3 -O -B research/rank-profile-retiming-obstruction/verify.py --summary +python3 -B scripts/research_package.py --package research/rank-profile-retiming-obstruction +``` + +The standalone verifier authenticates every vendored input before executing the +retained interpreter source without a bytecode-cache import. It independently +reconstructs the chronological invoice, regenerates both complete censuses, +checks every exact sign certificate, recovers the literal positive-control word, +and runs eight rejecting/sensitivity controls. A wrong coefficient is tested +after cleanup has been freshly rederived, so an obsolete inverse is not what +causes rejection. Normal and optimised-Python execution are separate checks. + +The standalone source-export runs are the scientific evidence. Registration is +provided for the existing repository hook; its metadata/history validation and +any hosted CI result are separate from these finite mathematical checks. The +native Clifford phase, physical allocation, full admission wrapper, precision, +all-size/compiler, analytic, and BIT chains have not been freshly replayed here. +They remain inherited or open as appropriate. No formal-kernel proof, +independent human review, architectural optimum, or unconditional multiplication +theorem is claimed. + +## Open next questions + +Can a neutral first retiming enable a second, strictly improving edit? The +certificate is tied to the exact baseline and cannot be iterated as a global +barrier. A useful first experiment would pin one neutral source-level witness, +then alter one interacting frame or gate, with the same dirty-state and complete +cost checks. The second move's geometry and complete invoice remain unresolved. + +Can a coordinated two-frame or boundary-changing rewrite realise PR3863's +`2+2 -> 1+3` target? The first step is a literal before/after word and helper/caller +boundary, not selecting children solely from the aggregate histogram. Stock, +chronology, native semantics, restoration, and any added physical calls must be +charged. These questions are also structured in TASK.json. + +## Provenance and credit + +PR3734, dataisfire, commit `fa041037a3374eaa08feeca0b26a5d6893194147`, supplies both +literal words and the retained auditors. Jeremy Kothe's PR2957 supplies the +already-present commuting-swap mechanism; its re-addressed records are on main +under `research/rank7-joint-endframes/data/REWRITES-2957.json`. PR2979 and the +subsequent staged-entry/retiming chain retain their construction credit. +Dugongue's PR3863, commit `635fe84596c19016f3d0316a5cf7abbe48285490`, supplies the +quantitative credit theorem and proposed rank-2 exchange target. The capped-mass +and discrete-curvature identities retain ranked-pair-verification and its +credited predecessor authors' attribution. + +Sagar Thakrar's exact interpreter is vendored unchanged, including its attribution +to Arham Tahir's frame-bill contract; roger-sato's semantic adapter is also reused +unchanged. Neither is called a newly independent interpreter here. The new +chronological trace, census, sign reduction, source binding, and controls are by +Chris R / Clear1nsight, with substantial OpenAI assistance. This AI-assisted +verification is not independent human review. See vendor/SOURCE-CREDITS.md and +SOURCES.json. Apache-2.0 terms and retained notices apply. + +The overlap refresh read the contribution guides, revision-6 guidance, PR3863, +PR3734/3815, PR2979/2957 records, and live commuting/3734-retiming PR searches. +Discussion HTML coverage was partial. This is not an exhaustive novelty claim. +The source acquisition used a temporary fork-only, read-only Actions export; +that workflow is not part of this proposed package. No frontier, other PR, or +canonical default branch was modified. diff --git a/research/rank-profile-retiming-obstruction/SOURCES.json b/research/rank-profile-retiming-obstruction/SOURCES.json new file mode 100644 index 0000000000..9cc2447ae5 --- /dev/null +++ b/research/rank-profile-retiming-obstruction/SOURCES.json @@ -0,0 +1,84 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + } + ], + "snapshots": [ + { + "local": "vendor/audit_core.py", + "source_path": "research/staged544-producer-return/audit_core.py", + "source_repository": "dataisfire/integer-mult-bounds", + "source_commit": "fa041037a3374eaa08feeca0b26a5d6893194147", + "bytes": 19364, + "sha256": "888679ca8502cdcb100420fe5382a052529a494bf76cb332928b86e62612b951", + "git_blob": "8b5e1d5f2a106402f036b63028ecef31a4e4c462" + }, + { + "local": "vendor/audit_verify.py", + "source_path": "research/staged544-producer-return/audit_verify.py", + "source_repository": "dataisfire/integer-mult-bounds", + "source_commit": "fa041037a3374eaa08feeca0b26a5d6893194147", + "bytes": 12382, + "sha256": "99971d3cc143cc894600e08c8cfbad3e8f537a544212f21dfbe4271cfa97354d", + "git_blob": "7f9fc1df424ae1d459616e49bda7a5dd17e40491" + }, + { + "local": "vendor/SOURCE-CREDITS.md", + "source_path": "research/staged544-producer-return/SOURCE-CREDITS.md", + "source_repository": "dataisfire/integer-mult-bounds", + "source_commit": "fa041037a3374eaa08feeca0b26a5d6893194147", + "bytes": 2882, + "sha256": "d4a13d8b8ed9cdb594f00efb3d1a336e09d934423330f02a1514308a720c278b", + "git_blob": "c054fad87eeaa510865e682ee0c976c4cd728da2" + }, + { + "local": "inputs/PROFILE.json", + "source_path": "research/staged544-producer-return/inputs/PROFILE.json", + "source_repository": "dataisfire/integer-mult-bounds", + "source_commit": "fa041037a3374eaa08feeca0b26a5d6893194147", + "bytes": 130, + "sha256": "06b4e2abe8d56b49bad3bdc8f8504082404b40609d548fa8de2618eb7373fd48", + "git_blob": "d1000454afc30925dc4b447a6f007e4b7dcbbab3" + }, + { + "local": "inputs/BORROW-WORD-43base.json.gz", + "source_path": "research/staged544-producer-return/words/BORROW-WORD-43base.json.gz", + "source_repository": "dataisfire/integer-mult-bounds", + "source_commit": "fa041037a3374eaa08feeca0b26a5d6893194147", + "bytes": 72769, + "sha256": "5ca4be99851f8878cbfe0fd6c454df926b11218f17feefa1664721cf03156699", + "git_blob": "674ea18ade4af85ca865fb08dc973637a09e30e6" + }, + { + "local": "inputs/BORROW-WORD-43extra.json.gz", + "source_path": "research/staged544-producer-return/words/BORROW-WORD-43extra.json.gz", + "source_repository": "dataisfire/integer-mult-bounds", + "source_commit": "fa041037a3374eaa08feeca0b26a5d6893194147", + "bytes": 72766, + "sha256": "965268a9be73d3f62e7ef680d18f108cf064bfe1f44b82157baa61443232904e", + "git_blob": "b17e2be67e327f04802fd034c344fe4253c13a4a" + } + ], + "method_predecessors": [ + { + "pr": 3863, + "author": "Dugongue", + "head": "635fe84596c19016f3d0316a5cf7abbe48285490", + "scope": "Uniform rational paid-profile credit and proposed 2+2 to 1+3 target; read, not reimplemented as new mathematics." + }, + { + "pr": 2957, + "author": "Jeremy Kothe", + "retained_record": "research/rank7-joint-endframes/data/REWRITES-2957.json", + "retained_record_base": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "scope": "Already-retained commuting swap used as a counterfactual rollback/recovery positive control." + } + ], + "external_snapshot_contract": "Package-local exact source snapshots are authenticated by byte count, SHA256, and Git blob. Their source heads are attribution pins, not runtime Git ancestry requirements. The standalone verifier is Git-free." +} diff --git a/research/rank-profile-retiming-obstruction/TASK.json b/research/rank-profile-retiming-obstruction/TASK.json new file mode 100644 index 0000000000..eaa540efaa --- /dev/null +++ b/research/rank-profile-retiming-obstruction/TASK.json @@ -0,0 +1,73 @@ +{ + "schema_version": 1, + "task_id": "scalar-to-moment", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "original_card": { + "id": "scalar-to-moment", + "question": "Can one known scalar simplification be converted into an actual paid-profile improvement?", + "starting_points": [ + "research/r439-bsection-stars-seed01/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Derive the changed legal frame itinerary and exact child histogram.", + "Prove a scoped obstruction showing why that scalar gain cannot change the paid contract." + ], + "acceptance_gate": "An unchanged histogram is not a kappa gain; record any separate runtime or proof benefit explicitly.", + "first_step": { + "command": [ + "python3", + "-B", + "research/r439-bsection-stars-seed01/verify.py" + ], + "expected": "PASS_R439_BSECTION_STARS", + "inspect": "Observe that the positive control improves scalar counts while retaining the paid histogram.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Choose one simplification and derive the complete changed frame itinerary, or prove why it cannot change the histogram.", + "bottleneck_link": "A legal change to the histogram, not addition count alone, is the bridge to an exponent gain.", + "allowed_variations": [ + "One existing scalar simplification and one proposed frame-path change." + ], + "scope_change_triggers": [ + "Submitting only another scalar count as completion of a paid-profile task." + ], + "overlap_terms": [ + "scalar simplification", + "paid profile", + "R439" + ] + }, + "scope_status": "refined", + "scope_change_reason": "The donor explicitly assigned converting rank-profile savings into actual circuit transformations. Test PR3863 against the literal PR3734 word by deriving all single-ADD retiming prices, with an already-retained PR2957 improving circuit as a positive control. The older R439 example is not the scientific baseline for this task.", + "actual_scope": "Exclude all-power moment improvement from one scalar ADD retiming with exactly one variable gate frame on each frozen PR3734 provider; bind the paid credit to a credited literal improving control.", + "bottleneck_link": "The rank-2 histogram supply alone does not establish legal circuit exchanges. An exhaustive scoped exclusion identifies which next implementation search must change another gate, frame, or boundary.", + "budget_minutes": 60, + "author": "Chris R / Clear1nsight", + "outcome": "negative-result", + "evidence": "Exact source-bound complete finite census and informal all-exponent sign proof; retained arbitrary-dirty free-operator replay of a constructive control. No new supplier or kappa.", + "open_questions": [ + { + "question": "Can a neutral first retiming unlock a profitable second move?", + "why_it_matters": "The certificate is baseline-specific, so sequential coordinated changes may escape it.", + "first_step": "Pin one neutral literal word and change one interacting frame or gate, then rederive the complete invoice.", + "blocked_by": "A concrete interacting pair and its dirty-restoration and physical-cost ledger." + }, + { + "question": "Can a coordinated two-frame or boundary-changing rewrite realise the PR3863 rank-2 exchange?", + "why_it_matters": "It directly addresses the gap between a profile reserve and a legal circuit.", + "first_step": "Supply literal before/after words, caller boundaries, and actual added children before a larger search.", + "blocked_by": "Native semantics, chronological stock, cleanup, and full consumer costs." + } + ], + "stop_rule": "Stop after the exact single-ADD class certificate, positive circuit control, and bounded verification. No automatic expansion into a multi-gate search and no selected-frontier change.", + "ai_assistance": "Substantial OpenAI assistance in mathematics, code, verification, and packaging. No independent human review or formal proof-kernel claim.", + "upstream_checkpoint": { + "utc": "2026-10-19T02:21:30.197573+00:00", + "main": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "priority_revision": 6, + "changed_frontier": false + }, + "overlap_coverage": "Read live GitHub guides and relevant PR sources and search commuting/3734 retiming PRs. Discussion HTML is partial; the connector rejects Discussion endpoints. The repository overlap helper was not executed. No exhaustive novelty claim." +} diff --git a/research/rank-profile-retiming-obstruction/VALIDATION.json b/research/rank-profile-retiming-obstruction/VALIDATION.json new file mode 100644 index 0000000000..d245d54856 --- /dev/null +++ b/research/rank-profile-retiming-obstruction/VALIDATION.json @@ -0,0 +1,53 @@ +{ + "schema_version": 1, + "evidence_status": "author-checked with substantial OpenAI assistance; no independent human or proof-kernel review", + "environment": { + "python": "CPython 3.13.5 (main, Jul 15 2026, 20:25:40), GCC 14.2.0", + "platform": "Linux-6.18.55-x86_64-with-glibc2.41", + "dependencies": "Python standard library only" + }, + "scientific_runs": [ + { + "command": "python3 -B research/rank-profile-retiming-obstruction/verify.py --summary", + "status": "PASS_SOURCE_BOUND_RETIMING_SCOPE", + "elapsed_seconds": "26.24", + "max_rss_kb": 128796 + }, + { + "command": "python3 -O -B research/rank-profile-retiming-obstruction/verify.py --summary", + "status": "PASS_SOURCE_BOUND_RETIMING_SCOPE", + "elapsed_seconds": "33.34", + "max_rss_kb": 129800 + } + ], + "coverage": { + "providers": 2, + "candidates_per_provider": 1776295, + "histogram_types_per_provider": 19, + "all_exponent_certificates": true, + "source_authentication": "byte count, SHA256, and Git blob for each retained snapshot before source execution", + "positive_control": "Counterfactual rollback and literal recovery of Jeremy Kothe's retained PR2957 swap, giving 2+3 to 1+4", + "interpreter": "Retained exact arbitrary-dirty free-operator interpreter and adapter, unchanged; not a newly independent interpreter", + "controls": [ + "source drift", + "profitable 2+2 to 1+3 rejected by non-improvement certificate", + "base wrong scalar with refreshed cleanup", + "base invalid gate frame", + "base noncommuting barrier", + "extra wrong scalar with refreshed cleanup", + "extra invalid gate frame", + "extra noncommuting barrier" + ], + "local_credit": "1491695107/1513529160000", + "replications": 3240, + "three_rank1_margin": "2437538889/12612743000" + }, + "unrun": [ + "Local Python 3.12 registered hook and full Git metadata/history check; Python 3.13 standalone source-export checks were run instead", + "Fresh native Clifford phase and all-size compilation", + "Fresh physical allocation and stock/precision/consumer verification", + "Full supplier admission and outer release", + "Formal proof-kernel or independent human review" + ], + "publication_note": "Hosted CI status is separate and must be read from the current PR head. The temporary fork-only source-export workflow is not included in this package. No selected-frontier change or new current supplier is claimed." +} diff --git a/research/rank-profile-retiming-obstruction/VERIFY.json b/research/rank-profile-retiming-obstruction/VERIFY.json new file mode 100644 index 0000000000..d4d879d8c4 --- /dev/null +++ b/research/rank-profile-retiming-obstruction/VERIFY.json @@ -0,0 +1,19 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": ["{python}", "-B", "{package}/verify.py", "--summary"], + "timeout_seconds": 180, + "checks": "Authenticate frozen sources, regenerate both complete retiming censuses and all-exponent sign certificates, and replay the literal positive control and eight sensitivity/rejection checks." + }, + { + "argv": ["{python}", "-O", "-B", "{package}/verify.py", "--summary"], + "timeout_seconds": 180, + "checks": "Repeat all scientific checks with assertions disabled." + } + ] +} diff --git a/research/rank-profile-retiming-obstruction/inputs/BORROW-WORD-43base.json.gz b/research/rank-profile-retiming-obstruction/inputs/BORROW-WORD-43base.json.gz new file mode 100644 index 0000000000..674ea18ade Binary files /dev/null and b/research/rank-profile-retiming-obstruction/inputs/BORROW-WORD-43base.json.gz differ diff --git a/research/rank-profile-retiming-obstruction/inputs/BORROW-WORD-43extra.json.gz b/research/rank-profile-retiming-obstruction/inputs/BORROW-WORD-43extra.json.gz new file mode 100644 index 0000000000..b17e2be67e Binary files /dev/null and b/research/rank-profile-retiming-obstruction/inputs/BORROW-WORD-43extra.json.gz differ diff --git a/research/rank-profile-retiming-obstruction/inputs/PROFILE.json b/research/rank-profile-retiming-obstruction/inputs/PROFILE.json new file mode 100644 index 0000000000..d1000454af --- /dev/null +++ b/research/rank-profile-retiming-obstruction/inputs/PROFILE.json @@ -0,0 +1,10 @@ +{ + "1": 7990332, + "2": 2349000, + "3": 748971, + "4": 330480, + "5": 69479, + "8": 25920, + "32": 1, + "48": 137911 +} diff --git a/research/rank-profile-retiming-obstruction/retiming.py b/research/rank-profile-retiming-obstruction/retiming.py new file mode 100644 index 0000000000..c33d7bbcdf --- /dev/null +++ b/research/rank-profile-retiming-obstruction/retiming.py @@ -0,0 +1,269 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Exact, fixed-neighbour single-ADD retiming relaxation. + +Chris R / Clear1nsight, with substantial OpenAI assistance. The BORROW-WORD +frame contract and scalar-retiming mechanism are credited in README.md. +This module does not import the retained auditor or a numerical optimiser. +""" +from bisect import bisect_left +from collections import Counter +from copy import deepcopy +from fractions import Fraction +from functools import lru_cache + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +@lru_cache(maxsize=None) +def span(vectors): + points = {0} + for v in vectors: + need(type(v) is int and 0 <= v < 512, 'invalid frame vector') + points |= {x ^ v for x in tuple(points)} + return sum(1 << x for x in points) + + +@lru_cache(maxsize=None) +def basis(mask): + answer = [] + have = 1 + for v in range(1, 512): + if (mask >> v) & 1 and not (have >> v) & 1: + answer.append(v) + have = span(tuple(answer)) + need(have == mask, 'not a binary subspace') + return tuple(answer) + + +@lru_cache(maxsize=None) +def join(a, b): + return span(basis(a) + basis(b)) + + +@lru_cache(maxsize=None) +def rank(mask): + n = mask.bit_count() + need(n > 0 and n & (n - 1) == 0, 'invalid subspace cardinality') + return n.bit_length() - 1 + + +def contained(a, b): + return not a & ~b + + +def touched(gate): + return gate[1:3] if gate[0] == 'add' else gate[1:2] + + +def tracing(word): + """Own chronological trace; centre descent is NOT persistent state. + + A check node is a fixed boundary, not a charged instruction. The census + relaxes it to a virtual climb. Every legal witness has zero such charge. + """ + full = (1 << 512) - 1 + live = set(range(704)) - set(word['removed']) + start, end = {}, {} + for r in live: + if r < 112: + start[r], end[r] = span((word['ports'][r],)), full + elif r < 224: + p = word['ports'][r - 112] + start[r] = 1 + end[r] = sum(1 << x for x in range(512) if (x & p).bit_count() % 2 == 0) + else: + start[r], end[r] = 1, full + for r, fr in word['start_extra'].items(): + start[int(r)] = span(tuple(fr)) + for r, fr in word['helper_final'].items(): + end[int(r)] = span(tuple(fr)) + current = dict(start) + nodes = {r: [] for r in live} + where = {} + bill = Counter() + + def event(r, frame, address, kind='climb'): + before = current[r] + if kind != 'map': + need(contained(before, frame), 'source frame containment') + d = rank(frame) - rank(before) + if kind == 'check': + need(d == 0, 'source fixed boundary') + elif d: + bill[d] += 1 + if kind == 'climb': + where[(address, r)] = len(nodes[r]) + nodes[r].append((address, kind, before, frame)) + current[r] = frame + + for i, gate in enumerate(word['A']): + if gate[0] == 'warp': + event(gate[1], span(tuple(gate[3])), ('check-A', i), 'check') + event(gate[1], span(tuple(gate[4])), ('map-A', i), 'map') + else: + for r in touched(gate): + event(r, span(tuple(gate[-1])), ('A', i)) + levels = {112 + int(r): span(tuple(fr)) for r, fr in word['target_levels'].items()} + for r in range(112, 224): + event(r, levels.get(r, 1), ('target-cut', r), 'check') + for r, fr in zip(word['centers'], word['center_frames']): + u = span(tuple(fr)) + event(r, u, ('centre-cut', r), 'check') + served = {levels.get(g[1], 1) for g in word['cut'] if g[2] == r} + for v in sorted(served, key=lambda x: -rank(x)): + need(contained(v, u), 'centre nesting') + if rank(u) > rank(v): + bill[rank(u) - rank(v)] += 1 + u = v + # The main forward register remains at its declared centre entry. + warps = {} + for j, rec in enumerate(word['warps']): + warps.setdefault(rec[0], []).append((j, rec)) + for i in range(len(word['B']) + 1): + for j, rec in warps.get(i, []): + event(rec[1], span(tuple(rec[3])), ('check-B', j), 'check') + event(rec[1], span(tuple(rec[4])), ('map-B', j), 'map') + if i < len(word['B']): + gate = word['B'][i] + for r in touched(gate): + event(r, span(tuple(gate[-1])), ('B', i)) + for i, gate in enumerate(word['restore']): + for r in touched(gate): + event(r, span(tuple(gate[-1])), ('restore', i)) + for r in live: + event(r, end[r], ('end',)) + return nodes, where, dict(sorted(bill.items())) + + +def crosses(g, h): + """Sufficient exact scalar normal form, not all algebraic commutations.""" + if h[0] == 'add': + return g[1] != h[2] and h[1] != g[2] + return h[0] == 'scale' and h[2] != 0 + + +def segments(word, section): + if section == 'A': + cuts = [word['prelude_events'], len(word['A'])] + elif section == 'B': + cuts = sorted({0, len(word['B'])} | {rec[0] for rec in word['warps']}) + else: + cuts = [0, len(word[section])] + return list(zip(cuts, cuts[1:])) + + +def caps(delta): + return [sum(n * min(r, k) for r, n in enumerate(delta)) for k in range(1, 10)] + + +def all_power_nonnegative(delta): + """Sufficient exact certificate using decreasing positive curvatures.""" + values = caps(delta) + prefix = 0 + for value in values[:-1]: + prefix += value + if prefix < 0: + return False + return values[-1] == 0 + + +def census(word): + nodes, where, bill = tracing(word) + deltas = Counter() + counts = {} + for section in ('A', 'B', 'restore'): + gates = word[section] + count = 0 + for lo, hi in segments(word, section): + occurrences = {} + for i in range(lo, hi): + need(gates[i][0] in ('add', 'scale'), 'unexpected scalar segment') + for r in touched(gates[i]): + occurrences.setdefault(r, []).append(i) + for i in range(lo, hi): + g = gates[i] + if g[0] != 'add': + continue + lower = i + while lower > lo and crosses(g, gates[lower - 1]): + lower -= 1 + upper = i + 1 + while upper < hi and crosses(g, gates[upper]): + upper += 1 + removal = [0] * 10 + reduced, entries, exits = {}, {}, {} + for r in touched(g): + seq = nodes[r] + pos = where[((section, i), r)] + _, _, p, u = seq[pos] + need(pos + 1 < len(seq) and seq[pos + 1][1] != 'map', 'missing successor') + q = seq[pos + 1][3] + removal[rank(u) - rank(p)] -= 1 + removal[rank(q) - rank(u)] -= 1 + removal[rank(q) - rank(p)] += 1 + indices = occurrences[r] + reduced[r] = [x for x in indices if x != i] + entries[r] = seq[where[((section, indices[0]), r)]][2] + last = where[((section, indices[-1]), r)] + need(seq[last + 1][1] != 'map', 'missing exit check') + exits[r] = seq[last + 1][3] + for cut in range(lower, upper + 1): + if cut == i + 1: # Same placement as cut i, counted once. + continue + boundaries = [] + for r in touched(g): + indices = reduced[r] + j = bisect_left(indices, cut) + p = span(tuple(gates[indices[j - 1]][-1])) if j else entries[r] + q = span(tuple(gates[indices[j]][-1])) if j < len(indices) else exits[r] + boundaries.append((p, q)) + lower_frame = join(boundaries[0][0], boundaries[1][0]) + upper_frame = boundaries[0][1] & boundaries[1][1] + if not contained(lower_frame, upper_frame): + continue + dims = [(rank(p), rank(q)) for p, q in boundaries] + for d in range(rank(lower_frame), rank(upper_frame) + 1): + delta = removal.copy() + for p, q in dims: + delta[q - p] -= 1 + delta[d - p] += 1 + delta[q - d] += 1 + delta[0] = 0 + need(sum(r * n for r, n in enumerate(delta)) == 0, 'rank mass drift') + deltas[tuple(delta)] += 1 + count += 1 + counts[section] = count + return {'per_section': counts, 'candidates': sum(counts.values()), + 'source_profile': bill, + 'deltas': [{'delta': {r: n for r, n in enumerate(d) if n}, 'count': n, + 'caps': caps(d), 'certificate': all_power_nonnegative(d)} + for d, n in sorted(deltas.items())]} + + +def apply_move(word, section, index, cut, frame): + """Apply one exact scalar retiming. Caller must rederive cleanup and audit.""" + need(section in ('A', 'B', 'restore'), 'unknown section') + gates = word[section] + need(type(index) is int and 0 <= index < len(gates), 'bad source index') + need(type(cut) is int and 0 <= cut <= len(gates), 'bad insertion cut') + need(any(lo <= index < hi and lo <= cut <= hi for lo, hi in segments(word, section)), + 'crosses prelude or native warp boundary') + g = deepcopy(gates[index]) + need(g[0] == 'add', 'only ADD moves are covered') + crossed = gates[index + 1:cut] if cut > index else gates[cut:index] + need(all(crosses(g, h) for h in crossed), 'noncommuting scalar barrier') + coefficient = Fraction(g[3], g[4]) + for h in crossed: + if h[0] == 'scale' and h[1] in touched(g): + power = (1 if h[1] == g[1] else -1) * (1 if cut > index else -1) + coefficient *= Fraction(h[2], h[3]) ** power + g[3:5] = [coefficient.numerator, coefficient.denominator] + g[-1] = list(basis(span(tuple(frame)))) + result = deepcopy(word) + result[section].pop(index) + result[section].insert(cut - (cut > index), g) + # Segment length and all warp cuts are unchanged. No warp is crossed. + return result diff --git a/research/rank-profile-retiming-obstruction/vendor/SOURCE-CREDITS.md b/research/rank-profile-retiming-obstruction/vendor/SOURCE-CREDITS.md new file mode 100644 index 0000000000..c054fad87e --- /dev/null +++ b/research/rank-profile-retiming-obstruction/vendor/SOURCE-CREDITS.md @@ -0,0 +1,14 @@ +# Source credit and independence + +New work: dataisfire with substantial OpenAI Codex assistance, Apache-2.0. No independent human review, fresh third-party AI review or proof-kernel verification is claimed. + +The construction extends [PR3682](https://github.com/CrocSwap/integer-mult-bounds/pull/3682), head431e6c6023ef352c41696469de7fb614cd4ded8c. Its retimed word, actual T360 source clock and immutable native/parent framework are retained. The complete new source/receipt snapshot is bound by REPLAY-INPUTS.json. The new ordinary source stage is an explicit pinned record applied after the unchanged predecessor reconstruction. + +- [PR3605](https://github.com/CrocSwap/integer-mult-bounds/pull/3605), Ross Richardson, supplies the staged-entrance mechanism, literal cleanup and exact Gaussian residual-check pattern. staged_pair.py is retained; the new544 shear and its proof are separate. +- [PR3638](https://github.com/CrocSwap/integer-mult-bounds/pull/3638), head d62e1acd7518a231440383f0d0dddf54d6edf8c1, supplies the T360 source-window clock, chronological aggregate model and integral-network/literal construction, with its retained PR3605 and earlier credits. The new inventory, integer incumbent and literal fill are recomputed. No predecessor owner receipt is used as proof of the new fill. +- [PR3687](https://github.com/CrocSwap/integer-mult-bounds/pull/3687) and [PR3693](https://github.com/CrocSwap/integer-mult-bounds/pull/3693), Sagar Thakrar and roger-sato with their credited AI assistance, supply audit_core.py and the whole-word semantics adapter audit_verify.py. These bytes are retained and reused. They are independent of the current constructor in the stated interpreter scope, not a newly written independent audit or new reviewer approval. +- The coupled-word source lineage includes PR3133, PR2979, Marius-Paul Dumitrean, dcharb78, Jeremy Kothe and the retained native/owner/block-norm/outer authors. All notices and scientific engines inside the source snapshot remain intact. + +owner_audit.py is a standalone standard-library adaptation of the source-window/family/prefix/invoice predicates in PR3638's independent_literal.py. It imports no producer, optimizer or retained owner checker. Its source template, plan and actual native canonical words are authenticated inputs. Three controls mutate actual literal roles and must fail for the intended reason. It shares the credited contract interpretation; it is not evidence of independent human agreement. + +The rational finite-price enclosure is retained from the PR3682 sources. New script adapters bind it to the actual finite histogram. Native forward/backward scalar replay, wrapper/phase lowering and all-column warp recipes were freshly run for both new words; unchanged native and parent ancestry is explicitly reused. The separate new544 span(414,51) residual check includes global Gaussian phase. diff --git a/research/rank-profile-retiming-obstruction/vendor/audit_core.py b/research/rank-profile-retiming-obstruction/vendor/audit_core.py new file mode 100644 index 0000000000..8b5e1d5f2a --- /dev/null +++ b/research/rank-profile-retiming-obstruction/vendor/audit_core.py @@ -0,0 +1,480 @@ +"""Independent exact semantics and binary-frame bill for the BORROW-WORD format. + +Standard library only. Nothing is imported from the audited authors' code +(PR3133/PR3605 producers, cleanup generator, evaluator or frame solver); the word +format and its semantic contract were read from those pinned sources and are +credited there. The frame-bill and free-word structure (point-set spans, warp +frame and lifted-frame checks, target levels keyed by register, dual symbol +naming) re-implements, without importing, Arham Tahir's +research/coupled-carrier-independent-audit/verify.py (Apache-2.0) and shares its +reading of the contract, so this module is not independent of that audit. + +Sagar Thakrar (thakrarsagar), with substantial AI assistance from Claude +(Anthropic, Claude Opus 5.5). Apache-2.0. +""" +from collections import Counter +from fractions import Fraction as Q + +V, N, H = 112, 704, 9 # sources 0..111, targets 112..223, helpers 224..703 +DUAL = 10 ** 6 # offset naming the independent dual symbols D_k = K_k^(-T) + + +class AuditFailure(Exception): + """Explicit failure; never disabled by python -O.""" + + +def need(ok, *why): + if not ok: + raise AuditFailure(' '.join(map(str, why))) + + +def is_target(r): + return V <= r < 2 * V + + +def touched(g): + return g[1:3] if g[0] == 'add' else g[1:2] + + +# ---------------------------------------------------------------------------- +# Binary frames: a subspace of F_2^9 is stored as a 512-bit point-set mask +# (bit x set iff x lies in the subspace). Containment is mask inclusion. +# ---------------------------------------------------------------------------- +_SPAN = {} + + +def span(vectors): + key = tuple(vectors) + mask = _SPAN.get(key) + if mask is None: + points = {0} + for u in key: + need(type(u) is int and 0 <= u < 512, 'frame vector out of range', u) + if u not in points: + points |= {p ^ u for p in points} + mask = sum(1 << p for p in points) + _SPAN[key] = mask + return mask + + +def points(mask): + return [x for x in range(512) if mask >> x & 1] + + +def dim(mask): + size = bin(mask).count('1') + need(size and size & (size - 1) == 0, 'not a subspace point set') + return size.bit_length() - 1 + + +FULL = (1 << 512) - 1 +ZERO = 1 + + +def hyperplane(port): + return sum(1 << x for x in range(512) if bin(x & port).count('1') % 2 == 0) + + +def warp_images(columns): + """Images of all 512 vectors under the F_2-linear map with columns G e_i.""" + need(len(columns) == H and all(type(c) is int and 0 <= c < 512 for c in columns), 'warp columns') + images = [0] * 512 + for x in range(1, 512): + low = x & -x + images[x] = images[x ^ low] ^ columns[low.bit_length() - 1] + need(len(set(images)) == 512, 'singular warp') + return images + + +def image_mask(images, mask): + return sum(1 << images[x] for x in points(mask)) + + +def lagrangian_action_ok(images, U, E): + """K_G(x,z)=(Gx, Gx+G^{-T}(x+z)) is symplectic and maps L_U to L_E, L_0 and L_FULL to themselves. + + L_U={(x,x+p): x in U, p in U^perp}. This is the binary frame action only; it + is not a Clifford phase or Gaussian-product certificate. For invertible G with + G(U)=E it is implied by the frame-map check ( = ), so it is a + consistency check of the implementation, not extra evidence. + """ + inverse = [0] * 512 + for x, y in enumerate(images): + inverse[y] = x + # G^{-T} z: bit j of the result is . + git = lambda z: sum((bin(inverse[1 << j] & z).count('1') & 1) << j for j in range(H)) + lift = lambda x, z: (images[x], images[x] ^ git(x ^ z)) + pair = lambda a, b: (bin(a[0] & b[1]).count('1') + bin(a[1] & b[0]).count('1')) & 1 + basis = [(1 << i, 0) for i in range(H)] + [(0, 1 << i) for i in range(H)] + lifted = [lift(*b) for b in basis] + if any(pair(lifted[i], lifted[j]) != pair(basis[i], basis[j]) for i in range(18) for j in range(i + 1, 18)): + return False + + def frame(mask): + us = points(mask) + perp = [p for p in range(512) if all(bin(p & u).count('1') % 2 == 0 for u in us)] + return {(u, u ^ p) for u in us for p in perp} + return all({lift(*pt) for pt in frame(a)} == frame(b) for a, b in ((ZERO, ZERO), (FULL, FULL), (U, E))) + + +# ---------------------------------------------------------------------------- +# Chronological binary-frame bill (BORROW-WORD contract) +# ---------------------------------------------------------------------------- +def frame_bill(w, lagrangian=False): + rep = w['report'] + need((rep['v'], 2 * rep['v'] + rep['R'], rep['h']) == (V, N, H), 'word geometry') + removed = set(w['removed']) + need(len(removed) == len(w['removed']) and all(2 * V <= r < N for r in removed), 'removed helpers') + live = [r for r in range(N) if r not in removed] + liveset = set(live) + B, warps = w['B'], w['warps'] + for k, (pos, lender, cols, U, E) in enumerate(warps, 1): + need(0 <= pos <= len(B), 'warp position', k) + need(lender in liveset and not is_target(lender), 'warp lender', k) + images = warp_images(cols) + su, se = span(U), span(E) + need(dim(su) == len(U) == len(E) == dim(se), 'warp frame bases', k) + need(image_mask(images, su) == se, 'warp does not map its frame', k) + if lagrangian: + need(lagrangian_action_ok(images, su, se), 'lifted frame action', k) + for name in ('A', 'B', 'restore'): + for g in w[name]: + if g[0] != 'warp': + need(all(r in liveset for r in touched(g)), 'removed/out-of-range register', name, g) + if g[0] == 'add' and not is_target(g[1]): + need(not is_target(g[2]), 'non-target reads a target', name, g) + need(all(g[-1] is None and is_target(g[1]) and g[0] == 'add' for g in w['cut']), 'cut gates') + need(all(g[-1] == [] and is_target(g[1]) for g in w['precondition'] + w['compensation']), 'zero-frame wrapper writes') + need(all(not is_target(g[1]) for g in w['restore']), 'restore writes a target') + + ports = w['ports'] + start, end = {}, {} + for r in live: + if r < V: + start[r], end[r] = span((ports[r],)), FULL + elif r < 2 * V: + start[r], end[r] = ZERO, hyperplane(ports[r - V]) + else: + start[r], end[r] = ZERO, FULL + for q, U in w['start_extra'].items(): + need(int(q) in liveset and int(q) >= 2 * V, 'entrance names a live helper', q) + start[int(q)] = span(U) + for q, U in w['helper_final'].items(): + need(int(q) in liveset and int(q) >= 2 * V, 'terminal names a live helper', q) + end[int(q)] = span(U) + + current, bill, chain = dict(start), Counter(), {} + + def climb(r, mask, where): + need(current[r] & ~mask == 0, 'frame containment fails', where, r) + d = dim(mask) - dim(current[r]) + if d: + bill[d] += 1 + chain.setdefault(r, []).append((where, d, mask)) + current[r] = mask + + npre = w['prelude_events'] + for i, g in enumerate(w['A']): + if g[0] == 'warp': + need(i < npre and len(g) == 5, 'warp outside the prelude', i) + _, r, op, fr, to = g + need(op != 0 and abs(op) <= len(warps) and warps[abs(op) - 1][1] == r, 'prelude warp lender', i) + images = warp_images(warps[abs(op) - 1][2]) + if op < 0: + inverse = [0] * 512 + for x, y in enumerate(images): + inverse[y] = x + images = inverse + need(image_mask(images, span(fr)) == span(to), 'prelude warp frame action', i) + need(current[r] == span(fr), 'prelude warp entry frame', i, r) + current[r] = span(to) + chain.setdefault(r, []).append((('A', i), 'warp', span(to))) + else: + if i < npre: + need(is_target(g[1]), 'prelude scalar writes a non-target', i) + for r in touched(g): + climb(r, span(g[-1]), ('A', i)) + levels = {V + int(t): span(U) for t, U in w['target_levels'].items()} + need(all(current[t] == levels.get(t, ZERO) for t in range(V, 2 * V)), 'target cut levels') + for q, U in zip(w['centers'], w['center_frames']): + U = span(U) + need(current[q] == U, 'centre entry frame', q) + served = {levels.get(g[1], ZERO) for g in w['cut'] if g[2] == q} + for T in sorted(served, key=lambda m: -dim(m)): + need(T & ~U == 0, 'centre descent not nested', q) + d = dim(U) - dim(T) + if d: + bill[d] += 1 + chain.setdefault(q, []).append((('centre',), d, T)) + U = T + at = {} + for k, rec in enumerate(warps, 1): + at.setdefault(rec[0], []).append(k) + for p in range(len(B) + 1): + for k in at.get(p, ()): + _, lender, _, U, E = warps[k - 1] + need(current[lender] == span(U), 'native warp entry frame', k, lender) + current[lender] = span(E) + chain.setdefault(lender, []).append((('warp', k), 'warp', span(E))) + if p < len(B): + for r in touched(B[p]): + climb(r, span(B[p][-1]), ('B', p)) + for i, g in enumerate(w['restore']): + for r in touched(g): + climb(r, span(g[-1]), ('restore', i)) + for r in live: + climb(r, end[r], ('end',)) + restored = set(map(int, w['helper_final'])) + need(all(end[r] == FULL for r in live if r not in restored and not is_target(r)), 'a FULL-cleanup register ends low') + widths = Counter(dim(end[r]) - dim(start[r]) for r in live if r >= 2 * V) + return dict(sorted(bill.items())), dict(sorted(widths.items())), chain, start, end + + +def hygiene(w): + """Inherited structural contract: dyadic scalars, power-of-two scales, wrapper and correction access.""" + entering = set(map(int, w['start_extra'])) + restored = set(map(int, w['helper_final'])) + live = set(range(N)) - set(w['removed']) + for name in ('precondition', 'compensation', 'A', 'cut', 'B', 'restore', 'cleanup'): + for g in w[name]: + if g[0] == 'warp': + continue + q = Q(g[3], g[4]) if g[0] == 'add' else Q(g[2], g[3]) + need(q != 0 and q.denominator & (q.denominator - 1) == 0, 'non-dyadic scalar', name, g) + if g[0] == 'scale': + need(abs(q.numerator) & (abs(q.numerator) - 1) == 0, 'non power-of-two scale', name, g) + for g in w['precondition'] + w['compensation']: + need(not any(r in entering | restored for r in touched(g)), 'wrapper touches an entering or restored helper', g) + for c in w['initial_corrections']: + word = c['operator_word'] + need(is_target(c['target']) and c['source'] in live and c['source'] >= 2 * V + and c['source'] not in entering, 'correction access', c) + need(word and all(w['warps'][abs(o) - 1][1] == c['source'] for o in word), 'correction operator lender', c) + q = Q(c['coefficient']) + need(q != 0 and q.denominator & (q.denominator - 1) == 0, 'correction coefficient', c) + return True + + +# ---------------------------------------------------------------------------- +# Literal inverse cleanup, derived from the contract +# ---------------------------------------------------------------------------- +def ordinary_forward(w): + """Chronological non-wrapper actions whose inverse forms cleanup.""" + out = [g for g in w['A'][w['prelude_events']:]] + at = {} + for k, rec in enumerate(w['warps'], 1): + at.setdefault(rec[0], []).append(['warp', rec[1], k]) + for p in range(len(w['B']) + 1): + out += at.get(p, []) + if p < len(w['B']): + out.append(w['B'][p]) + return out + list(w['restore']) + + +def derive_cleanup(w): + restored = set(map(int, w['helper_final'])) + buf = lambda r: r + N if r in restored else r + full = [256, 128, 64, 32, 16, 8, 4, 2, 1] + out = [] + for g in reversed(ordinary_forward(w)): + if g[0] == 'warp': + out.append(['warp', buf(g[1]), -g[2], full]) + elif is_target(g[1]): + continue + elif g[0] == 'add': + out.append(['add', buf(g[1]), buf(g[2]), -g[3], g[4], full]) + else: + need(g[0] == 'scale', 'unknown primitive', g) + out.append(['scale', buf(g[1]), g[3], g[2], full]) + return out + + +def same_cleanup(a, b): + norm = lambda c: [(g[:-1], span(g[-1])) for g in c] + return len(a) == len(b) and norm(a) == norm(b) + + +# ---------------------------------------------------------------------------- +# Exact free-operator semantics. A value is a dict {(input, word): Fraction}; +# word is a reduced tuple of signed operator ids (leftmost = applied last). +# ---------------------------------------------------------------------------- +def program(w, cleanup=None): + """Literal executed sequence: corrections, wrapper, A, cut, B+warps, restore | cleanup.""" + items = [('corr', c['target'], c['source'], tuple(c['operator_word']), Q(c['coefficient'])) + for c in w['initial_corrections']] + items += w['precondition'] + w['compensation'] + w['A'] + w['cut'] + at = {} + for k, rec in enumerate(w['warps'], 1): + at.setdefault(rec[0], []).append(['warp', rec[1], k]) + for p in range(len(w['B']) + 1): + items += at.get(p, []) + if p < len(w['B']): + items.append(w['B'][p]) + items += w['restore'] + return items, list(w['cleanup'] if cleanup is None else cleanup) + + +def dual_op(op): + return (1 if op > 0 else -1) * (abs(op) + DUAL) + + +def _left(op, word): + return word[1:] if word and word[0] == -op else (op,) + word + + +def _right(word, op): + return word[:-1] if word and word[-1] == -op else word + (op,) + + +def _axpy(dst, src, q): + for key, x in src.items(): + y = dst.get(key, 0) + q * x + if y: + dst[key] = y + else: + dst.pop(key, None) + + +def forward_rows(w, cleanup=None, dual=False, symbolic_buffers=True, snapshot=None): + """Schrodinger pass: every register's value as a combination of initial inputs. + + Live inputs are independent symbols. Private buffers are independent symbols + when symbolic_buffers is set (dirty), otherwise zero. The optional snapshot + callback sees the rows at the cleanup boundary. + """ + removed = set(w['removed']) + live = [r for r in range(N) if r not in removed] + restored = sorted(map(int, w['helper_final'])) + rows = {r: {(r, ()): Q(1)} for r in live} + for c in restored: + rows[c + N] = {(c + N, ()): Q(1)} if symbolic_buffers else {} + prefix, tail = program(w, cleanup) + + def apply(g): + kind = g[0] + if kind == 'add': + t, s, q = g[1], g[2], Q(g[3], g[4]) + need(t != s and q, 'add gate', g) + if dual: + t, s, q = s, t, -q + _axpy(rows[t], rows[s], q) + elif kind == 'scale': + q = Q(g[2], g[3]) + need(q != 0, 'zero scale', g) + if dual: + q = 1 / q + rows[g[1]] = {k: q * x for k, x in rows[g[1]].items()} + elif kind == 'warp': + op = dual_op(g[2]) if dual else g[2] + rows[g[1]] = {(var, _left(op, word)): x for (var, word), x in rows[g[1]].items()} + elif kind == 'corr': + _, t, s, word, c = g + if dual: + src, ops, dst, c = rows[t], [-dual_op(o) for o in word], s, -c + else: + src, ops, dst = rows[s], list(reversed(word)), t + moved = {} + for (var, wd), x in src.items(): + for o in ops: + wd = _left(o, wd) + moved[var, wd] = x + _axpy(rows[dst], moved, c) + else: + raise AuditFailure('unknown primitive ' + repr(g)) + + for g in prefix: + apply(g) + if snapshot is not None: + snapshot(rows) + for g in tail: + apply(g) + return rows + + +def reverse_columns(w, cleanup=None, upto_cleanup=False): + """Heisenberg pull-back: process the forward program backwards. + + cols[s] = {(output, word): coefficient}: the final output register 'output' + contains coefficient*word*x_s. Words grow on the right. Every live input and + every private buffer is an independent symbol. + """ + removed = set(w['removed']) + live = [r for r in range(N) if r not in removed] + restored = sorted(map(int, w['helper_final'])) + regs = live + [c + N for c in restored] + cols = {r: {(r, ()): Q(1)} for r in regs} + prefix, tail = program(w, cleanup) + seq = prefix if upto_cleanup else prefix + tail + for g in reversed(seq): + kind = g[0] + if kind == 'add': + t, s, q = g[1], g[2], Q(g[3], g[4]) + need(t != s and q, 'add gate', g) + _axpy(cols[s], cols[t], q) + elif kind == 'scale': + q = Q(g[2], g[3]) + need(q != 0, 'zero scale', g) + cols[g[1]] = {k: q * x for k, x in cols[g[1]].items()} + elif kind == 'warp': + op = g[2] + cols[g[1]] = {(out, _right(word, op)): x for (out, word), x in cols[g[1]].items()} + elif kind == 'corr': + _, t, s, word, c = g + moved = {} + for (out, wd), x in cols[t].items(): + for o in word: + wd = _right(wd, o) + moved[out, wd] = x + _axpy(cols[s], moved, c) + else: + raise AuditFailure('unknown primitive ' + repr(g)) + return cols + + +def transpose(cols): + rows = {} + for s, col in cols.items(): + for (r, word), x in col.items(): + rows.setdefault(r, {})[s, word] = x + return rows + + +def endpoint_defects(w, rows, dual=False): + """Compare final rows with the contract on the zero-buffer (live-input) domain. + + Returns (bad live registers, dirty buffers, buffer->live leaks, buffer self-map identity). + """ + removed = set(w['removed']) + live = [r for r in range(N) if r not in removed] + restored = sorted(map(int, w['helper_final'])) + bad = [] + for r in live: + expect = {(r, ()): Q(1)} + if dual and r < V: + expect[r + V, ()] = Q(-1) + if not dual and is_target(r): + expect[r - V, ()] = Q(1) + got = {k: x for k, x in rows.get(r, {}).items() if k[0] < N} + if got != expect: + bad.append(r) + dirty = [c for c in restored if any(k[0] < N for k in rows.get(c + N, {}))] + leaks = sorted({r for r in live for k in rows.get(r, {}) if k[0] >= N}) + buffer_identity = all({k: x for k, x in rows.get(c + N, {}).items() if k[0] >= N} == {(c + N, ()): Q(1)} + for c in restored) + return bad, dirty, leaks, buffer_identity + + +def boundary_defects(w, rows): + """Contract at the cleanup boundary (forward): targets sheared, restored helpers clean and isolated.""" + restored = set(map(int, w['helper_final'])) + out = [] + for t in range(V, 2 * V): + if {k: x for k, x in rows[t].items() if k[0] < N} != {(t, ()): Q(1), (t - V, ()): Q(1)}: + out.append(('target', t)) + for c in restored: + if rows[c] != {(c, ()): Q(1)}: + out.append(('restored', c)) + for r, row in rows.items(): + if r < N and r not in restored and any(k[0] in restored for k in row): + out.append(('restored input read', r)) + return out diff --git a/research/rank-profile-retiming-obstruction/vendor/audit_verify.py b/research/rank-profile-retiming-obstruction/vendor/audit_verify.py new file mode 100644 index 0000000000..7f9fc1df42 --- /dev/null +++ b/research/rank-profile-retiming-obstruction/vendor/audit_verify.py @@ -0,0 +1,254 @@ +#!/usr/bin/env python3 +"""Whole-word cross-check of published RETIMED and DELAYED supplier words. + +Reuses Sagar Thakrar's exact PR3687 audit_core, unchanged and authenticated +before execution. This is not a new interpreter. No construction/native checker +is imported. roger-sato with substantial OpenAI Codex assistance; Apache-2.0. +""" +from collections import Counter +from copy import deepcopy +import gzip +import hashlib +import json +from pathlib import Path +import sys +import types + +HERE = Path(__file__).resolve().parent +STAGED = {1: 2439, 2: 726, 3: 224, 4: 102, 5: 20, 8: 8} +RETIMED = {1: 2437, 2: 724, 3: 226, 4: 102, 5: 20, 8: 8} +WIDTHS = {4: 26, 5: 2, 6: 18, 7: 52, 8: 97, 9: 213} +MOVES = ((591, 1045, 640, 644, 2, [423, 65, 20, 10]), + (641, 1085, 656, 660, -1, [427, 96, 24, 6])) +SOURCE_COMMITS = { + 3605: '3efbb5de06a49ffeea6684482f2d3fe48cdca3fb', + 3642: '044d24f12e74f228dd462c07ae2d7f3ea35e2be9', + 3653: '607a09ff441c79b215a8127a81f4cc70021d0d9b', + 3682: '431e6c6023ef352c41696469de7fb614cd4ded8c', + 3687: 'f798838eb8ede4178e94f240e7b7e54b3f80c82d', +} + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def authenticate(): + rows = json.loads((HERE / 'SOURCES.json').read_text())['snapshots'] + expected = {(3687, 'vendor/audit_core.py')} + for provider in ('base', 'extra'): + expected.update((number, f'inputs/{kind}-{provider}.json.gz') for number, kind in + ((3605, 'STAGED'), (3642, 'RETIMED'), (3653, 'RETIMED'), (3682, 'DELAYED'))) + keys = [(row['source_pr'], row['local']) for row in rows] + need(len(keys) == len(expected) and set(keys) == expected, 'source mapping inventory differs') + for row in rows: + need(row['source_commit'] == SOURCE_COMMITS[row['source_pr']], 'source commit differs') + raw = (HERE / row['local']).read_bytes() + need(len(raw) == row['bytes'], 'source byte length: ' + row['local']) + need(hashlib.sha256(raw).hexdigest() == row['sha256'], 'source SHA256: ' + row['local']) + blob = hashlib.sha1(b'blob ' + str(len(raw)).encode() + b'\0' + raw).hexdigest() + need(blob == row['git_blob'], 'source Git blob: ' + row['local']) + core = types.ModuleType('retained_audit_core') + path = HERE / 'vendor/audit_core.py' + # Execute the authenticated source bytes, without accepting a .pyc cache. + exec(compile(path.read_bytes(), str(path), 'exec'), core.__dict__) + return core + + +def load(kind, provider): + return json.loads(gzip.decompress((HERE / 'inputs' / f'{kind}-{provider}.json.gz').read_bytes())) + + +def events(w): + result = [] + for pos in range(len(w['B']) + 1): + result += [('warp', k, deepcopy(rec)) for k, rec in enumerate(w['warps']) if rec[0] == pos] + if pos < len(w['B']): + result.append(('gate', pos, deepcopy(w['B'][pos]))) + return result + + +def replace_events(w, seq): + result = deepcopy(w) + body, warps = [], [None] * len(w['warps']) + for kind, label, gate in seq: + gate = deepcopy(gate) + if kind == 'gate': + body.append(gate) + else: + gate[0] = len(body) + warps[label] = gate + need(all(rec is not None for rec in warps), 'lost warp in reconstruction') + result['B'], result['warps'] = body, warps + return result + + +def reconstruct(C, staged, kind): + """Literal prose recipes: adjacent shear swap, or move before first producer. + + This repeats the credited local structural arguments as an input control; + the new evidence is the full word calculation below. + """ + seq = events(staged) + for start, stop, donor, pivot, coefficient, frame in MOVES: + source = next(x for x in seq if x[:2] == ('gate', start)) + need(source[2] == ['add', donor, pivot, coefficient, 1, [429, 30]], 'source release') + if kind == 'RETIMED': + target = next(x for x in seq if x[:2] == ('gate', start + 1)) + need(target[2][0] == 'add' and target[2][2] == pivot, 'adjacent same-pivot shear') + need(not any(rec[0] == start + 1 for rec in staged['warps']), 'unexpected crossed warp') + where = seq.index(target) + 1 + else: + target = next(x for x in seq if x[:2] == ('gate', stop)) + writes = [i for i, g in enumerate(staged['B']) if i > start and g[1] == pivot] + need(writes[0] == stop, 'first producer cut') + where = seq.index(target) + changed = deepcopy(source[2]) + changed[-1] = frame + seq.insert(where, ('gate', -pivot, changed)) + seq.remove(source) + result = replace_events(staged, seq) + result['cleanup'] = C.derive_cleanup(result) + result['report']['local_profile'] = {str(k): v for k, v in RETIMED.items()} + return result + + +def semantics(C, w): + """All live and buffer inputs are symbols, with no zero-buffer assumption.""" + def endpoint(name, result): + bad_live, dirty_buffers, leaks, buffer_identity = result + need(not bad_live and not dirty_buffers and not leaks and buffer_identity, + name + ' endpoint: ' + repr(result)) + boundary = {} + rows = C.forward_rows(w, symbolic_buffers=True, + snapshot=lambda values: boundary.setdefault('defects', C.boundary_defects(w, values))) + endpoint('forward', C.endpoint_defects(w, rows)) + dual_rows = C.forward_rows(w, dual=True, symbolic_buffers=True) + endpoint('dual', C.endpoint_defects(w, dual_rows, dual=True)) + need(not boundary['defects'], 'cleanup boundary: ' + repr(boundary['defects'])) + pulled = C.transpose(C.reverse_columns(w)) + need(pulled == {r: row for r, row in rows.items() if row}, 'reverse pull-back differs from forward') + pre = C.transpose(C.reverse_columns(w, upto_cleanup=True)) + pre = {r: pre.get(r, {}) for r in set(pre) | set(range(C.N))} + need(not C.boundary_defects(w, pre), 'reverse cleanup-boundary contract') + live = C.N - len(w['removed']) + buffers = len(w['helper_final']) + need((live, buffers, len(rows)) == (632, 91, 723), 'complete symbolic domain') + # Endpoint expectations are derived by the retained checker: live x,y,h + # map to x,y+x,h; all private buffer symbols return unchanged. + return {'live_inputs': live, 'dirty_buffers': buffers, 'matrix_dimension': len(rows), + 'forward': 'PASS', 'dual': 'PASS', 'reverse_pullback_equals_forward': True, + 'cleanup_boundary_forward_and_reverse': 'PASS', + 'buffer_to_live_leaks': 0, 'buffer_self_map': 'identity', + 'nonzero_endpoint_terms': sum(len(row) for row in rows.values())} + + +def inspect(C, w, profile): + C.hygiene(w) + bill, widths, chain, _, _ = C.frame_bill(w) + need(bill == profile, 'computed profile differs') + need(w['report']['local_profile'] == {str(k): v for k, v in bill.items()}, 'declared profile differs') + need(widths == WIDTHS, 'helper widths differ') + need(w['cleanup'] == C.derive_cleanup(w), 'literal cleanup differs') + return {'semantics': semantics(C, w), 'profile': bill, 'widths': widths, + 'rank_mass': sum(r * n for r, n in bill.items())}, chain + + +def expect_rejection(C, fn, phrase): + try: + fn() + except (ValueError, C.AuditFailure) as exc: + need(phrase in str(exc), 'wrong rejection: ' + str(exc)) + return phrase + raise ValueError('mutant unexpectedly passed: ' + phrase) + + +def negative_controls(C, staged, w, kind): + controls = [] + for _, _, donor, pivot, _, _ in MOVES: + seq = events(w) + release = next(x for x in seq if x[0] == 'gate' and x[2][0] == 'add' and x[2][1:3] == [donor, pivot]) + for defect in ('omit', 'flip', 'cross_first_producer'): + changed = deepcopy(seq) + index = seq.index(release) + if defect == 'omit': + changed.pop(index) + elif defect == 'flip': + changed[index][2][3] *= -1 + else: + producer = next(x for x in changed[index + 1:] if x[0] == 'gate' and x[2][1] == pivot) + moved = changed.pop(index) + changed.insert(changed.index(producer) + 1, moved) + bad = replace_events(w, changed) + bad['cleanup'] = C.derive_cleanup(bad) + # Repair the literal inverse so stale cleanup is not the rejection. + reason = expect_rejection(C, lambda: semantics(C, bad), 'forward endpoint') + controls.append({'defect': defect, 'pivot': pivot, 'rejected_by': reason}) + old_cleanup = deepcopy(w) + old_cleanup['cleanup'] = staged['cleanup'] + # The inverse shears commute: this is a format failure, not a wrong operator. + semantic_control = semantics(C, old_cleanup) + need(old_cleanup['cleanup'] != C.derive_cleanup(old_cleanup), 'old cleanup unexpectedly literal') + controls.append({'defect': 'old_cleanup_order', 'semantics': semantic_control, + 'rejected_by': expect_rejection(C, lambda: inspect(C, old_cleanup, RETIMED), 'literal cleanup differs')}) + old_frames = deepcopy(w) + for gate in old_frames['B']: + if gate[0] == 'add' and gate[1:3] in ([640, 644], [656, 660]): + gate[-1] = [429, 30] + need(semantics(C, old_frames) == semantic_control, 'frame-only mutation changed operator') + if kind == 'RETIMED': + need(C.frame_bill(old_frames)[0] == STAGED, 'old frame control does not restore staged bill') + controls.append({'defect': 'old_release_frames', 'semantic_operator': 'PASS', + 'profile': STAGED, 'rejected_by': expect_rejection(C, lambda: inspect(C, old_frames, RETIMED), 'computed profile differs')}) + else: + # The later release encounters a donor that has already climbed, so + # the original rank-2 frame is now illegal, despite the same operator. + controls.append({'defect': 'old_release_frames', 'semantic_operator': 'PASS', + 'rejected_by': expect_rejection(C, lambda: inspect(C, old_frames, RETIMED), 'frame containment fails')}) + fake_report = deepcopy(w) + fake_report['report']['local_profile']['1'] += 1 + controls.append({'defect': 'wrong_declared_profile', 'rejected_by': + expect_rejection(C, lambda: inspect(C, fake_report, RETIMED), 'declared profile differs')}) + return controls + + +def run(C): + results = {} + for provider in ('base', 'extra'): + staged = load('STAGED', provider) + control, old_chain = inspect(C, staged, STAGED) + records = {'STAGED': control} + for kind in ('RETIMED', 'DELAYED'): + w = load(kind, provider) + need(reconstruct(C, staged, kind) == w, 'prose reconstruction differs: ' + kind) + record, chain = inspect(C, w, RETIMED) + deltas = {} + for register in set(chain) | set(old_chain): + before = Counter(d for _, d, _ in old_chain.get(register, []) if type(d) is int and d > 0) + after = Counter(d for _, d, _ in chain.get(register, []) if type(d) is int and d > 0) + delta = {r: after[r] - before[r] for r in set(after) | set(before) if after[r] != before[r]} + if delta: + deltas[register] = delta + need(deltas == {640: {1: -1, 2: -1, 3: 1}, 656: {1: -1, 2: -1, 3: 1}}, 'per-register invoice differs') + record['prose_reconstruction'] = 'exact complete JSON equality' + record['changed_register_bills'] = deltas + record['controls'] = negative_controls(C, staged, w, kind) + records[kind] = record + print('CHECKED', provider, kind, '723-register forward/dual/pull-back and 9 controls', flush=True) + results[provider] = records + return {'status': 'PASS_RETIMED_AND_DELAYED_WHOLE_WORD_AUDIT', + 'scope': 'Reused PR3687 interpreter; finite exact operator/frame audit only. No native Gaussian, owner, root, or complete supplier claim.', + 'providers': results} + + +if __name__ == '__main__': + need(sys.argv[1:] in ([], ['--write']), 'usage: verify.py [--write]') + C = authenticate() + result = run(C) + output = json.dumps(result, sort_keys=True, indent=2) + '\n' + if sys.argv[1:] == ['--write']: + (HERE / 'RESULT.json').write_text(output) + else: + need((HERE / 'RESULT.json').read_text() == output, 'committed result differs') + print(result['status']) diff --git a/research/rank-profile-retiming-obstruction/verify.py b/research/rank-profile-retiming-obstruction/verify.py new file mode 100644 index 0000000000..7fb8b291d7 --- /dev/null +++ b/research/rank-profile-retiming-obstruction/verify.py @@ -0,0 +1,117 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Read-only source binding, exact census, and retained dirty-word controls.""" +import gzip +import hashlib +import json +from pathlib import Path +import sys +import types +from copy import deepcopy +from fractions import Fraction as Q + +P = Path(__file__).resolve().parent +# Execute this package's actual source, not any adjacent bytecode cache. +R = types.ModuleType('retiming_source') +exec(compile((P / 'retiming.py').read_bytes(), str(P / 'retiming.py'), 'exec'), R.__dict__) +need = R.need + + +def json_normal(value): + return json.loads(json.dumps(value, sort_keys=True)) + + +def rejects(fn, name): + try: + fn() + except (ValueError, C.AuditFailure): + return name + raise ValueError('control accepted: ' + name) + + +def authenticate(raw, row): + need(len(raw) == row['bytes'], 'source length: ' + row['local']) + need(hashlib.sha256(raw).hexdigest() == row['sha256'], 'source SHA256: ' + row['local']) + blob = hashlib.sha1(b'blob ' + str(len(raw)).encode() + b'\0' + raw).hexdigest() + need(blob == row['git_blob'], 'source Git blob: ' + row['local']) + + +def module(name, path): + value = types.ModuleType(name) + value.__file__ = str(path) + exec(compile(path.read_bytes(), str(path), 'exec'), value.__dict__) + return value + + +sources = json.loads((P / 'SOURCES.json').read_text()) +for row in sources['snapshots']: + authenticate((P / row['local']).read_bytes(), row) +C = module('retained_audit_core', P / 'vendor/audit_core.py') +A = module('retained_audit_adapter', P / 'vendor/audit_verify.py') +expected = json.loads((P / 'CENSUS.json').read_text()) +controls = [] +first = sources['snapshots'][0] +controls.append(rejects(lambda: authenticate((P / first['local']).read_bytes() + b'x', first), 'source drift')) +need(not R.all_power_nonnegative((0, 1, -2, 1, 0, 0, 0, 0, 0, 0)), 'profitable exchange must not be excluded') +controls.append('profitable 2+2 to 1+3 rejected by non-improvement certificate') +results = {} +for tag in ('base', 'extra'): + word = json.loads(gzip.decompress((P / 'inputs' / ('BORROW-WORD-43' + tag + '.json.gz')).read_bytes())) + profile, inventory, *_ = C.frame_bill(word) + need(profile == {1:2440, 2:725, 3:224, 4:102, 5:20, 8:8}, 'source profile') + need(word['cleanup'] == C.derive_cleanup(word), 'source literal cleanup') + need(R.tracing(word)[2] == profile, 'independent chronological bill') + result = R.census(word) + need(json_normal(result) == expected[tag], 'complete census differs') + need(all(row['certificate'] for row in result['deltas']), 'uncertified retiming delta') + need(sum(row['count'] for row in result['deltas']) == result['candidates'], 'census partition') + # Counterfactual rollback of one already-retained Jeremy Kothe PR2957 swap. + # This is not asserted to be the complete historical PR2957 parent word. + old = deepcopy(word) + g, h = old['A'][4043:4045] + need(g[:5] == ['add',81,40,1,1] and h[:5] == ['add',81,17,1,1], 'control preimages') + old['A'][4043:4045] = [h[:-1] + [g[-1]], g] + old['cleanup'] = C.derive_cleanup(old) + before, widths, *_ = C.frame_bill(old) + old['report']['local_profile'] = {str(r): n for r, n in before.items()} + need(before == {1:2439, 2:726, 3:225, 4:101, 5:20, 8:8}, 'rollback bill') + need(widths == inventory and R.tracing(old)[2] == before, 'rollback boundary ledger') + new = R.apply_move(old, 'A', 4043, 4045, h[-1]) + need(R.span(tuple(new['A'][4044][-1])) == R.span(tuple(h[-1])), 'recovered frame') + new['A'][4044][-1] = deepcopy(h[-1]) # Restore the source basis spelling. + new['cleanup'] = C.derive_cleanup(new) + after, new_widths, *_ = C.frame_bill(new) + new['report']['local_profile'] = {str(r): n for r, n in after.items()} + need(new == word, 'literal source word recovered') + need(new_widths == widths, 'no inventory changes') + delta = [0] + [after.get(r,0) - before.get(r,0) for r in range(1,10)] + need(delta == [0,1,-1,-1,1,0,0,0,0,0], 'actual 2+3 to 1+4 circuit delta') + need(not R.all_power_nonnegative(tuple(delta)), 'known gain must escape obstruction') + semantics = {'rollback': A.semantics(C, old), 'retained': A.semantics(C, new)} + bad = deepcopy(new) + bad['A'][4044][3] *= -1 + bad['cleanup'] = C.derive_cleanup(bad) + controls.append(rejects(lambda: A.semantics(C, bad), tag + ' wrong scalar with refreshed cleanup')) + bad = deepcopy(new) + bad['A'][4044][-1] = [] + controls.append(rejects(lambda: C.frame_bill(bad), tag + ' invalid gate frame')) + barrier = next(i for i in range(word['prelude_events'], len(word['A'])-1) + if word['A'][i][0] == 'add' and not R.crosses(word['A'][i], word['A'][i+1])) + controls.append(rejects(lambda: R.apply_move(word, 'A', barrier, barrier+2, word['A'][barrier][-1]), + tag + ' noncommuting barrier')) + result['positive_control'] = {'before_profile': before, 'after_profile': after, + 'delta': {r:n for r,n in enumerate(delta) if n}, + 'semantics': semantics} + results[tag] = result +# PR3863's sufficient credit, now attached to this actual credited rewrite. +lower, upper = Q(17,10000), Q(18,10000) +credit = sum(lower*(1-upper)/((k+1)*(1+upper*k)) for k in (2,3)) +need(credit == Q(1491695107,1513529160000), 'exact local credit') +need(3240 * credit - 3 == Q(2437538889,12612743000), 'strict three-child reserve') +report = {'status': 'PASS_SOURCE_BOUND_RETIMING_SCOPE', 'providers': results, + 'controls': controls, 'local_credit': str(credit), 'replications': 3240, + 'three_rank1_margin': str(3240*credit-3), 'new_current_supplier': False} +if '--summary' in sys.argv: + print(json.dumps({k:v for k,v in report.items() if k != 'providers'}, sort_keys=True)) +else: + print(json.dumps(report, sort_keys=True))