Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
27 changes: 27 additions & 0 deletions .github/workflows/dirty-stride-fast-phases.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
name: Dirty stride fast phase stream
on:
pull_request:
paths:
- 'research/dirty-stride-fast-phases/**'
- '.github/workflows/dirty-stride-fast-phases.yml'
push:
paths:
- 'research/dirty-stride-fast-phases/**'
- '.github/workflows/dirty-stride-fast-phases.yml'
workflow_dispatch:
permissions:
contents: read
jobs:
verify:
runs-on: ubuntu-latest
timeout-minutes: 20
strategy:
matrix:
python: ['3.11', '3.14']
steps:
- uses: actions/checkout@v4
- uses: actions/setup-python@v5
with:
python-version: ${{ matrix.python }}
- run: python -I -O -B research/dirty-stride-fast-phases/verify.py
- run: python -I -O -B research/dirty-stride-fast-phases/test_package.py
265 changes: 265 additions & 0 deletions research/dirty-stride-fast-phases/BENCHMARK.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,265 @@
{
"platform": "macOS-26.6.1-arm64-arm-64bit-Mach-O",
"python": "3.14.7",
"rows": [
{
"bits": 16,
"length": 32,
"median_seconds": {
"pr1038": 0.042217166163027287,
"stream": 0.1914247078821063
},
"trials": {
"pr1038": [
{
"erase_seconds": 3.3294782042503357e-07,
"phase_divisions": 7056,
"phase_products": 14118,
"prepare_seconds": 0.0006293328478932381,
"seed_divisions": 0,
"seed_peak_bits": null,
"seed_products": 0,
"stream_seconds": 0.04158750036731362,
"tape_moves": 221,
"total_seconds": 0.042217166163027287
},
{
"erase_seconds": 2.0815059542655945e-07,
"phase_divisions": 7056,
"phase_products": 14118,
"prepare_seconds": 0.0006140000186860561,
"seed_divisions": 0,
"seed_peak_bits": null,
"seed_products": 0,
"stream_seconds": 0.04078587470576167,
"tape_moves": 221,
"total_seconds": 0.041400082875043154
},
{
"erase_seconds": 3.7532299757003784e-07,
"phase_divisions": 7056,
"phase_products": 14118,
"prepare_seconds": 0.0006021247245371342,
"seed_divisions": 0,
"seed_peak_bits": null,
"seed_products": 0,
"stream_seconds": 0.04313837504014373,
"tape_moves": 221,
"total_seconds": 0.04374087508767843
}
],
"stream": [
{
"erase_seconds": 0.08656962495297194,
"phase_divisions": 384,
"phase_products": 966,
"prepare_seconds": 0.08834325009956956,
"seed_divisions": 5178,
"seed_peak_bits": 11000,
"seed_products": 5184,
"stream_seconds": 0.01533125014975667,
"tape_moves": 221,
"total_seconds": 0.19024412520229816
},
{
"erase_seconds": 0.09268087521195412,
"phase_divisions": 384,
"phase_products": 966,
"prepare_seconds": 0.09867466613650322,
"seed_divisions": 5178,
"seed_peak_bits": 11000,
"seed_products": 5184,
"stream_seconds": 0.01634766673669219,
"tape_moves": 221,
"total_seconds": 0.20770320808514953
},
{
"erase_seconds": 0.08787808287888765,
"phase_divisions": 384,
"phase_products": 966,
"prepare_seconds": 0.08811087487265468,
"seed_divisions": 5178,
"seed_peak_bits": 11000,
"seed_products": 5184,
"stream_seconds": 0.015435750130563974,
"tape_moves": 221,
"total_seconds": 0.1914247078821063
}
]
}
},
{
"bits": 48,
"length": 257,
"median_seconds": {
"pr1038": 0.6899422500282526,
"stream": 1.2866912498138845
},
"trials": {
"pr1038": [
{
"erase_seconds": 2.9103830456733704e-07,
"phase_divisions": 92340,
"phase_products": 184686,
"prepare_seconds": 0.001130416989326477,
"seed_divisions": 0,
"seed_peak_bits": null,
"seed_products": 0,
"stream_seconds": 0.5955920000560582,
"tape_moves": 1796,
"total_seconds": 0.5967227080836892
},
{
"erase_seconds": 3.334134817123413e-07,
"phase_divisions": 92340,
"phase_products": 184686,
"prepare_seconds": 0.001091458834707737,
"seed_divisions": 0,
"seed_peak_bits": null,
"seed_products": 0,
"stream_seconds": 1.1057697078213096,
"tape_moves": 1796,
"total_seconds": 1.106861500069499
},
{
"erase_seconds": 2.0815059542655945e-07,
"phase_divisions": 92340,
"phase_products": 184686,
"prepare_seconds": 0.001532666850835085,
"seed_divisions": 0,
"seed_peak_bits": null,
"seed_products": 0,
"stream_seconds": 0.6884093750268221,
"tape_moves": 1796,
"total_seconds": 0.6899422500282526
}
],
"stream": [
{
"erase_seconds": 0.59731016587466,
"phase_divisions": 3084,
"phase_products": 7716,
"prepare_seconds": 0.6183066670782864,
"seed_divisions": 7914,
"seed_peak_bits": 25350,
"seed_products": 7920,
"stream_seconds": 0.15272741671651602,
"tape_moves": 1796,
"total_seconds": 1.3683442496694624
},
{
"erase_seconds": 0.5393960415385664,
"phase_divisions": 3084,
"phase_products": 7716,
"prepare_seconds": 0.5949774170294404,
"seed_divisions": 7914,
"seed_peak_bits": 25350,
"seed_products": 7920,
"stream_seconds": 0.15231779124587774,
"tape_moves": 1796,
"total_seconds": 1.2866912498138845
},
{
"erase_seconds": 0.46511820796877146,
"phase_divisions": 3084,
"phase_products": 7716,
"prepare_seconds": 0.5326998331584036,
"seed_divisions": 7914,
"seed_peak_bits": 25350,
"seed_products": 7920,
"stream_seconds": 0.18261054204776883,
"tape_moves": 1796,
"total_seconds": 1.180428583174944
}
]
}
},
{
"bits": 96,
"length": 2048,
"median_seconds": {
"pr1038": 10.187936124857515,
"stream": 9.092779374681413
},
"trials": {
"pr1038": [
{
"erase_seconds": 4.7497451305389404e-06,
"phase_divisions": 1146600,
"phase_products": 2293206,
"prepare_seconds": 0.0018824171274900436,
"seed_divisions": 0,
"seed_peak_bits": null,
"seed_products": 0,
"stream_seconds": 10.785656167194247,
"tape_moves": 14333,
"total_seconds": 10.787543334066868
},
{
"erase_seconds": 1.4170072972774506e-06,
"phase_divisions": 1146600,
"phase_products": 2293206,
"prepare_seconds": 0.0027474593371152878,
"seed_divisions": 0,
"seed_peak_bits": null,
"seed_products": 0,
"stream_seconds": 9.294908415991813,
"tape_moves": 14333,
"total_seconds": 9.297657292336226
},
{
"erase_seconds": 2.250075340270996e-06,
"phase_divisions": 1146600,
"phase_products": 2293206,
"prepare_seconds": 0.0022939168848097324,
"seed_divisions": 0,
"seed_peak_bits": null,
"seed_products": 0,
"stream_seconds": 10.185639957897365,
"tape_moves": 14333,
"total_seconds": 10.187936124857515
}
],
"stream": [
{
"erase_seconds": 2.6205718340352178,
"phase_divisions": 24576,
"phase_products": 61446,
"prepare_seconds": 3.9281516657210886,
"seed_divisions": 11802,
"seed_peak_bits": 55767,
"seed_products": 11808,
"stream_seconds": 2.5440558749251068,
"tape_moves": 14333,
"total_seconds": 9.092779374681413
},
{
"erase_seconds": 3.426748082973063,
"phase_divisions": 24576,
"phase_products": 61446,
"prepare_seconds": 3.2136184577830136,
"seed_divisions": 11802,
"seed_peak_bits": 55767,
"seed_products": 11808,
"stream_seconds": 2.2742746672593057,
"tape_moves": 14333,
"total_seconds": 8.914641208015382
},
{
"erase_seconds": 3.318305708002299,
"phase_divisions": 24576,
"phase_products": 61446,
"prepare_seconds": 4.192794916685671,
"seed_divisions": 11802,
"seed_peak_bits": 55767,
"seed_products": 11808,
"stream_seconds": 1.683004958089441,
"tape_moves": 14333,
"total_seconds": 9.19410558277741
}
]
}
}
],
"scope": "Two opposite phase passes; new seed erasure included; old API has no explicit seed erasure. PR1038 puts all product and division counts in the phase counters. The new seed counters are separate."
}
30 changes: 30 additions & 0 deletions research/dirty-stride-fast-phases/CHECKS.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,30 @@
# Verification contracts

The test authoring gate was applied before the checks were added.

| Contract | Credible failure | Check and distinct coverage |
| --- | --- | --- |
| Uniform state and output error | Wrong second difference, chart, or guard width | Direct quadratic residues and full-angle outward rational intervals |
| Exact stream and seed cleanup | Wrong inverse order or omitted arithmetic uncomputation | Both phase-state registers and seed outputs reach exact zero |
| Dirty operator and inverse | Wrong outer phase direction or target-dependent roundoff omitted | Actual leaf and factor calls with odd lowest bits, large dirt, and geometric-sum oracle |
| Complete access bill | An input read, data move, or inverse pass is not charged | Data banks count literal accesses on two physical tapes and reject copies or slices |
| Linear stream work | Term evaluation remains inside each phase site | Executed product, division, and seed-term counts at three lengths and precisions |
| Reproducible package | Missing local dependency, altered source, or unchecked receipt | Source pins, semantic mutations, and relocated full receipt replay |

These checks extend the phase-interface boundary. They do not duplicate
the full selected-frontier replay or claim the inherited dirty solver has
been re-proved. No production export or injection hook was added for tests.
The new public phase lifecycle is also used by each production data pass.

The small phase domain is all residues for moduli 1 through 9 at `W=2`
and `W=24`, with `L=2m+1`. Seven extra cases cover wider precision,
negative or wide numerators, large moduli, and chart boundaries. One long
case uses `a=12345`, `m=65537`, `W=24`, and `L=16384`; all steps execute,
and indices divisible by 257 plus the last index get interval checks.
There is no random seed or open-ended search. Every stated case completes.

The dirty-word domain has lengths 1, 5, 8, and 17, strides 0, 2, -3,
and 7, both signs, and one or three factors. Each call is followed by
its exact inverse. One-factor cases use no borrowed array; three-factor
cases retain two arbitrary borrowed arrays. This is finite coverage of
the written all-length theorem, not an exhaustive input audit.
30 changes: 30 additions & 0 deletions research/dirty-stride-fast-phases/CLAIM.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,30 @@
# Local route 8 claim

Base: `abdc6a7002abdbcd9e21bfc5e1a795784deacfdf`.
Branch: `codex/k9-fast-phases`. Start: 2026-10-13 18:04 UTC.

No pinned sprint issue was supplied. The coordinator records the claim locally.
The current PR metadata lists PR1038 at `99c71d385171480ecc2c43287aa4a04e1027fcd9`
and PR1054 at `6bc675be1554b3a3be771147f21f9dc2c6dae50a`.

Candidate 1: use two reversible rounded complex phase states, a fixed second
difference, and exact backward reconstruction. Pay logarithmic guard precision.
Candidate 2: use exact modular angle state and blocks of polynomial values.
This needs a paid polynomial table or repeated evaluation at block boundaries.
Candidate 3: prove a work/error tradeoff for noninvertible rounded products.
This does not give the requested reversible implementation.

Chosen object: the first candidate, for all integer numerators, positive moduli,
finite positive lengths, and working precision at least two bits. Prove a uniform
quadratic drift bound. Use bounded three-shear charts. Prepare two seeds with
exact rational series, then clear their arithmetic state. Reverse the phase
state after every data pass. Keep the inherited borrowed-array count fixed.

Expected result: an executable scalar phase interface with O(L) stream work,
polynomial seed work, full dirty-target error, and a separate bit/tape bill.
The complete kappa calculation is still complex-supplier bound. This result
can remove a phase-interface expense; it does not change a supplier invoice.
No new kappa is claimed. Expected finish: this research session, after checks.

No random search is used. PR479, PR948, PR985, PR1038 and PR1054 are
predecessor or scope references. PR1054 is not combined by assumption.
Loading
Loading