diff --git a/research/r420-four-wire-cleanup/CERTIFICATE.json b/research/r420-four-wire-cleanup/CERTIFICATE.json new file mode 100644 index 0000000000..2923c25a90 --- /dev/null +++ b/research/r420-four-wire-cleanup/CERTIFICATE.json @@ -0,0 +1,176 @@ +{ + "width": 4, + "original_xors": 2973, + "windows_examined": 7693, + "shorter_windows": 284, + "census": [ + { + "wires": 2, + "saving": 0, + "count": 2973 + }, + { + "wires": 3, + "saving": 0, + "count": 1882 + }, + { + "wires": 3, + "saving": 1, + "count": 45 + }, + { + "wires": 4, + "saving": 0, + "count": 2554 + }, + { + "wires": 4, + "saving": 1, + "count": 194 + }, + { + "wires": 4, + "saving": 2, + "count": 39 + }, + { + "wires": 4, + "saving": 3, + "count": 6 + } + ], + "distance_layers": { + "2": { + "0": 1, + "1": 2, + "2": 2, + "3": 1 + }, + "3": { + "0": 1, + "1": 6, + "2": 24, + "3": 51, + "4": 60, + "5": 24, + "6": 2 + }, + "4": { + "0": 1, + "1": 12, + "2": 96, + "3": 542, + "4": 2058, + "5": 5316, + "6": 7530, + "7": 4058, + "8": 541, + "9": 6 + } + }, + "saving": 137, + "windows": [ + {"start":120,"stop":124,"registers":[47,80,88,119],"old":[[80,119],[88,119],[47,80],[47,119]],"new":[[47,80],[80,119],[88,119]],"saving":1}, + {"start":126,"stop":130,"registers":[33,39,88,119],"old":[[39,119],[33,39],[33,88],[33,119]],"new":[[33,39],[33,88],[39,119]],"saving":1}, + {"start":158,"stop":163,"registers":[16,22,103,118],"old":[[22,118],[103,22],[103,118],[16,22],[16,118]],"new":[[16,22],[103,22],[22,118]],"saving":2}, + {"start":192,"stop":197,"registers":[16,22,98,103],"old":[[103,98],[103,16],[22,98],[22,16],[22,103]],"new":[[22,103],[103,16],[103,98]],"saving":2}, + {"start":205,"stop":210,"registers":[27,106,107,117],"old":[[117,107],[106,117],[106,107],[27,117],[27,107]],"new":[[27,117],[106,117],[117,107]],"saving":2}, + {"start":300,"stop":305,"registers":[19,74,95,100],"old":[[74,100],[95,74],[95,100],[19,74],[19,100]],"new":[[19,74],[95,74],[74,100]],"saving":2}, + {"start":305,"stop":310,"registers":[40,74,84,100],"old":[[84,74],[84,100],[40,84],[40,74],[40,100]],"new":[[40,84],[84,74],[84,100]],"saving":2}, + {"start":311,"stop":314,"registers":[56,100,111],"old":[[111,100],[56,111],[56,100]],"new":[[56,111],[111,100]],"saving":1}, + {"start":326,"stop":329,"registers":[54,56,65],"old":[[65,54],[56,54],[56,65]],"new":[[56,65],[65,54]],"saving":1}, + {"start":349,"stop":352,"registers":[46,60,102],"old":[[46,102],[60,46],[60,102]],"new":[[60,46],[46,102]],"saving":1}, + {"start":404,"stop":408,"registers":[29,45,71,73],"old":[[73,45],[71,45],[29,73],[29,45]],"new":[[29,73],[71,45],[73,45]],"saving":1}, + {"start":432,"stop":436,"registers":[21,53,89,105],"old":[[21,89],[21,53],[105,89],[105,21]],"new":[[21,53],[105,21],[21,89]],"saving":1}, + {"start":456,"stop":460,"registers":[17,25,64,77],"old":[[17,77],[64,77],[25,17],[25,77]],"new":[[25,17],[17,77],[64,77]],"saving":1}, + {"start":477,"stop":481,"registers":[17,25,99,104],"old":[[25,104],[17,104],[17,99],[17,25]],"new":[[17,25],[17,99],[25,104]],"saving":1}, + {"start":495,"stop":499,"registers":[12,66,72,76],"old":[[76,12],[66,12],[72,76],[72,12]],"new":[[66,12],[72,76],[76,12]],"saving":1}, + {"start":543,"stop":548,"registers":[5,48,59,61],"old":[[59,61],[59,5],[48,59],[48,61],[48,5]],"new":[[48,59],[59,5],[59,61]],"saving":2}, + {"start":1158,"stop":1164,"registers":[546,587,614,638],"old":[[587,546],[614,587],[614,546],[638,614],[638,587],[638,546]],"new":[[638,614],[614,587],[587,546]],"saving":3}, + {"start":1169,"stop":1173,"registers":[596,614,638,656],"old":[[614,656],[596,656],[596,638],[596,614]],"new":[[596,614],[596,638],[614,656]],"saving":1}, + {"start":1179,"stop":1183,"registers":[551,615,639,657],"old":[[639,615],[639,551],[657,639],[657,615]],"new":[[639,551],[657,639],[639,615]],"saving":1}, + {"start":1185,"stop":1189,"registers":[597,615,639,657],"old":[[615,657],[597,657],[597,639],[597,615]],"new":[[597,615],[597,639],[615,657]],"saving":1}, + {"start":1197,"stop":1201,"registers":[541,577,605,607],"old":[[577,541],[607,605],[607,577],[607,541]],"new":[[607,577],[577,541],[607,605]],"saving":1}, + {"start":1202,"stop":1207,"registers":[541,577,628,648],"old":[[628,577],[628,541],[648,577],[648,541],[628,648]],"new":[[628,648],[648,541],[648,577]],"saving":2}, + {"start":1207,"stop":1211,"registers":[605,607,628,648],"old":[[607,648],[605,648],[605,628],[605,607]],"new":[[605,607],[605,628],[607,648]],"saving":1}, + {"start":1223,"stop":1227,"registers":[600,610,625,653],"old":[[610,653],[600,653],[600,625],[600,610]],"new":[[600,610],[600,625],[610,653]],"saving":1}, + {"start":1280,"stop":1285,"registers":[528,604,634,652],"old":[[634,604],[634,528],[652,604],[652,528],[634,652]],"new":[[634,652],[652,528],[652,604]],"saving":2}, + {"start":1285,"stop":1289,"registers":[604,622,634,652],"old":[[622,634],[604,652],[604,634],[604,622]],"new":[[604,622],[604,652],[622,634]],"saving":1}, + {"start":1297,"stop":1300,"registers":[529,568,570],"old":[[568,529],[570,568],[570,529]],"new":[[570,568],[568,529]],"saving":1}, + {"start":1318,"stop":1322,"registers":[530,540,581,616],"old":[[581,530],[616,581],[616,540],[616,530]],"new":[[616,540],[616,581],[581,530]],"saving":1}, + {"start":1343,"stop":1346,"registers":[576,613,637],"old":[[613,637],[576,637],[576,613]],"new":[[576,613],[613,637]],"saving":1}, + {"start":1358,"stop":1362,"registers":[532,575,598,658],"old":[[598,532],[658,575],[658,532],[598,658]],"new":[[658,575],[598,658],[658,532]],"saving":1}, + {"start":1371,"stop":1376,"registers":[533,564,619,631],"old":[[564,533],[619,564],[619,533],[631,564],[631,533]],"new":[[619,564],[631,564],[564,533]],"saving":2}, + {"start":1382,"stop":1386,"registers":[601,619,631,649],"old":[[619,649],[601,649],[601,631],[601,619]],"new":[[601,619],[601,631],[619,649]],"saving":1}, + {"start":1394,"stop":1398,"registers":[522,585,620,632],"old":[[620,522],[632,620],[632,585],[632,522]],"new":[[632,585],[632,620],[620,522]],"saving":1}, + {"start":1408,"stop":1412,"registers":[523,559,594,608],"old":[[559,523],[608,594],[608,559],[608,523]],"new":[[608,559],[559,523],[608,594]],"saving":1}, + {"start":1420,"stop":1424,"registers":[594,608,627,659],"old":[[608,659],[594,659],[594,627],[594,608]],"new":[[594,608],[594,627],[608,659]],"saving":1}, + {"start":1429,"stop":1432,"registers":[524,560,579],"old":[[560,524],[579,560],[579,524]],"new":[[579,560],[560,524]],"saving":1}, + {"start":1439,"stop":1442,"registers":[579,593,642],"old":[[593,642],[579,642],[579,593]],"new":[[579,593],[593,642]],"saving":1}, + {"start":1450,"stop":1453,"registers":[542,561,578],"old":[[561,542],[578,561],[578,542]],"new":[[578,561],[561,542]],"saving":1}, + {"start":1462,"stop":1465,"registers":[542,588,647],"old":[[588,647],[542,647],[542,588]],"new":[[542,588],[588,647]],"saving":1}, + {"start":1473,"stop":1478,"registers":[526,599,626,654],"old":[[626,599],[626,526],[654,599],[654,526],[626,654]],"new":[[626,654],[654,526],[654,599]],"saving":2}, + {"start":1478,"stop":1482,"registers":[599,609,626,654],"old":[[609,626],[599,654],[599,626],[599,609]],"new":[[599,609],[599,654],[609,626]],"saving":1}, + {"start":1522,"stop":1527,"registers":[517,535,553,571],"old":[[553,535],[553,517],[571,553],[571,535],[571,517]],"new":[[571,553],[553,517],[553,535]],"saving":2}, + {"start":1533,"stop":1539,"registers":[553,571,611,624],"old":[[611,624],[571,624],[571,611],[553,624],[553,611],[553,571]],"new":[[553,571],[571,611],[611,624]],"saving":3}, + {"start":1598,"stop":1601,"registers":[556,606,629],"old":[[606,629],[556,629],[556,606]],"new":[[556,606],[606,629]],"saving":1}, + {"start":1611,"stop":1616,"registers":[521,586,603,651],"old":[[586,521],[603,586],[603,521],[651,586],[651,521]],"new":[[603,586],[651,586],[586,521]],"saving":2}, + {"start":1616,"stop":1621,"registers":[547,586,603,651],"old":[[586,651],[586,603],[547,651],[547,603],[547,586]],"new":[[547,586],[586,603],[586,651]],"saving":2}, + {"start":1637,"stop":1640,"registers":[368,381,466],"old":[[381,466],[368,466],[368,381]],"new":[[368,381],[381,466]],"saving":1}, + {"start":1648,"stop":1653,"registers":[338,346,348,510],"old":[[346,510],[346,338],[348,346],[348,510],[348,338]],"new":[[348,346],[346,338],[346,510]],"saving":2}, + {"start":1659,"stop":1663,"registers":[243,346,348,476],"old":[[243,476],[348,243],[346,476],[346,243]],"new":[[346,243],[243,476],[348,243]],"saving":1}, + {"start":1671,"stop":1675,"registers":[305,332,493,511],"old":[[511,493],[332,305],[332,511],[332,493]],"new":[[332,305],[332,511],[511,493]],"saving":1}, + {"start":1683,"stop":1686,"registers":[280,305,458],"old":[[458,280],[305,280],[305,458]],"new":[[305,458],[458,280]],"saving":1}, + {"start":1692,"stop":1695,"registers":[339,440,514],"old":[[514,339],[440,514],[440,339]],"new":[[440,514],[514,339]],"saving":1}, + {"start":1702,"stop":1706,"registers":[319,406,440,450],"old":[[440,406],[450,319],[450,406],[450,440]],"new":[[450,319],[450,440],[440,406]],"saving":1}, + {"start":1711,"stop":1717,"registers":[285,456,494,512],"old":[[512,494],[456,512],[456,494],[285,456],[285,512],[285,494]],"new":[[285,456],[456,512],[512,494]],"saving":3}, + {"start":1722,"stop":1726,"registers":[285,309,335,456],"old":[[456,335],[309,335],[309,285],[309,456]],"new":[[309,285],[309,456],[456,335]],"saving":1}, + {"start":1734,"stop":1738,"registers":[297,321,366,402],"old":[[297,366],[321,402],[321,366],[297,321]],"new":[[321,402],[297,321],[321,366]],"saving":1}, + {"start":1738,"stop":1742,"registers":[297,321,402,448],"old":[[402,297],[448,321],[448,297],[448,402]],"new":[[448,321],[448,402],[402,297]],"saving":1}, + {"start":1761,"stop":1765,"registers":[287,310,331,438],"old":[[287,310],[331,310],[438,310],[438,287]],"new":[[331,310],[438,287],[287,310]],"saving":1}, + {"start":1773,"stop":1777,"registers":[354,385,427,453],"old":[[385,354],[453,427],[453,385],[453,354]],"new":[[453,385],[385,354],[453,427]],"saving":1}, + {"start":1784,"stop":1788,"registers":[273,324,427,453],"old":[[453,273],[427,324],[427,273],[427,453]],"new":[[427,324],[427,453],[453,273]],"saving":1}, + {"start":1795,"stop":1799,"registers":[289,307,413,496],"old":[[413,496],[307,289],[307,496],[413,307]],"new":[[307,289],[413,307],[307,496]],"saving":1}, + {"start":1799,"stop":1803,"registers":[289,307,413,434],"old":[[289,413],[434,307],[434,413],[434,289]],"new":[[434,289],[289,413],[434,307]],"saving":1}, + {"start":1811,"stop":1814,"registers":[341,379,424],"old":[[379,341],[424,379],[424,341]],"new":[[424,379],[379,341]],"saving":1}, + {"start":1822,"stop":1826,"registers":[277,405,424,454],"old":[[424,277],[405,277],[405,454],[405,424]],"new":[[405,424],[405,454],[424,277]],"saving":1}, + {"start":1843,"stop":1846,"registers":[269,394,396],"old":[[396,269],[394,269],[394,396]],"new":[[394,396],[396,269]],"saving":1}, + {"start":1862,"stop":1865,"registers":[248,386,471],"old":[[471,248],[386,248],[386,471]],"new":[[386,471],[471,248]],"saving":1}, + {"start":1882,"stop":1885,"registers":[257,382,472],"old":[[472,257],[382,257],[382,472]],"new":[[382,472],[472,257]],"saving":1}, + {"start":1894,"stop":1897,"registers":[342,380,504],"old":[[504,342],[380,504],[380,342]],"new":[[380,504],[504,342]],"saving":1}, + {"start":1905,"stop":1908,"registers":[344,380,504],"old":[[344,380],[504,380],[504,344]],"new":[[504,344],[344,380]],"saving":1}, + {"start":1914,"stop":1919,"registers":[283,333,487,505],"old":[[283,505],[283,487],[333,283],[333,505],[333,487]],"new":[[333,283],[283,487],[283,505]],"saving":2}, + {"start":1938,"stop":1943,"registers":[318,358,412,432],"old":[[432,412],[432,358],[318,412],[318,358],[432,318]],"new":[[432,318],[318,358],[318,412]],"saving":2}, + {"start":1943,"stop":1947,"registers":[318,412,432,459],"old":[[459,318],[412,318],[412,432],[412,459]],"new":[[412,432],[412,459],[459,318]],"saving":1}, + {"start":1979,"stop":1983,"registers":[337,408,418,507],"old":[[507,337],[408,418],[408,507],[408,337]],"new":[[408,418],[408,507],[507,337]],"saving":1}, + {"start":1989,"stop":1994,"registers":[272,301,408,418],"old":[[408,272],[408,301],[418,272],[418,301],[418,408]],"new":[[418,408],[408,272],[408,301]],"saving":2}, + {"start":2000,"stop":2003,"registers":[311,373,489],"old":[[373,489],[311,373],[311,489]],"new":[[311,373],[373,489]],"saving":1}, + {"start":2011,"stop":2014,"registers":[311,330,373],"old":[[330,311],[373,311],[373,330]],"new":[[373,330],[330,311]],"saving":1}, + {"start":2018,"stop":2021,"registers":[343,377,460],"old":[[377,343],[460,377],[460,343]],"new":[[460,377],[377,343]],"saving":1}, + {"start":2037,"stop":2041,"registers":[293,328,392,490],"old":[[392,490],[293,328],[293,392],[293,490]],"new":[[293,328],[293,392],[392,490]],"saving":1}, + {"start":2058,"stop":2063,"registers":[299,327,363,398],"old":[[327,398],[327,363],[299,327],[299,398],[299,363]],"new":[[299,327],[327,363],[327,398]],"saving":2}, + {"start":2082,"stop":2087,"registers":[267,349,467,491],"old":[[349,491],[467,349],[467,491],[267,349],[267,491]],"new":[[267,349],[467,349],[349,491]],"saving":2}, + {"start":2087,"stop":2092,"registers":[267,347,349,467],"old":[[349,267],[349,467],[347,267],[347,467],[347,349]],"new":[[347,349],[349,267],[349,467]],"saving":2}, + {"start":2110,"stop":2114,"registers":[249,357,361,474],"old":[[361,249],[361,474],[357,249],[357,361]],"new":[[361,474],[357,361],[361,249]],"saving":1}, + {"start":2127,"stop":2133,"registers":[465,473,475,479],"old":[[465,479],[475,479],[475,465],[473,479],[473,465],[473,475]],"new":[[473,475],[475,465],[465,479]],"saving":3}, + {"start":2142,"stop":2146,"registers":[250,352,360,364],"old":[[364,250],[360,250],[352,364],[352,250]],"new":[[352,364],[360,250],[364,250]],"saving":1}, + {"start":2146,"stop":2152,"registers":[352,356,360,364],"old":[[360,352],[364,352],[364,360],[356,352],[356,360],[356,364]],"new":[[356,364],[364,360],[360,352]],"saving":3}, + {"start":2162,"stop":2166,"registers":[441,443,455,481],"old":[[455,481],[443,441],[443,481],[455,443]],"new":[[443,441],[455,443],[443,481]],"saving":1}, + {"start":2166,"stop":2170,"registers":[435,441,443,455],"old":[[441,455],[435,443],[435,455],[435,441]],"new":[[435,441],[435,443],[441,455]],"saving":1}, + {"start":2178,"stop":2181,"registers":[258,316,499],"old":[[499,258],[316,499],[316,258]],"new":[[316,499],[499,258]],"saving":1}, + {"start":2197,"stop":2200,"registers":[445,482,501],"old":[[501,482],[445,501],[445,482]],"new":[[445,501],[501,482]],"saving":1}, + {"start":2216,"stop":2221,"registers":[260,314,320,500],"old":[[314,500],[314,260],[320,314],[320,500],[320,260]],"new":[[320,314],[314,260],[314,500]],"saving":2}, + {"start":2227,"stop":2231,"registers":[312,314,320,334],"old":[[312,334],[320,312],[314,334],[314,312]],"new":[[314,312],[312,334],[320,312]],"saving":1}, + {"start":2239,"stop":2244,"registers":[264,403,431,483],"old":[[403,264],[403,483],[431,403],[431,264],[431,483]],"new":[[431,403],[403,264],[403,483]],"saving":2}, + {"start":2251,"stop":2256,"registers":[403,411,423,431],"old":[[423,411],[431,411],[431,423],[403,411],[403,423]],"new":[[403,423],[431,423],[423,411]],"saving":2}, + {"start":2264,"stop":2267,"registers":[259,270,296],"old":[[270,259],[296,270],[296,259]],"new":[[296,270],[270,259]],"saving":1}, + {"start":2283,"stop":2287,"registers":[271,415,421,484],"old":[[271,484],[415,421],[415,271],[415,484]],"new":[[415,271],[271,484],[415,421]],"saving":1}, + {"start":2294,"stop":2297,"registers":[407,417,421],"old":[[407,417],[421,417],[421,407]],"new":[[421,407],[407,417]],"saving":1}, + {"start":2303,"stop":2308,"registers":[241,253,278,298],"old":[[298,241],[298,253],[278,298],[278,241],[278,253]],"new":[[278,298],[298,241],[298,253]],"saving":2}, + {"start":2315,"stop":2320,"registers":[276,278,298,302],"old":[[302,276],[278,276],[278,302],[298,276],[298,302]],"new":[[278,302],[298,302],[302,276]],"saving":2}, + {"start":2328,"stop":2332,"registers":[246,383,395,485],"old":[[246,485],[383,395],[383,246],[383,485]],"new":[[383,246],[246,485],[383,395]],"saving":1}, + {"start":2341,"stop":2345,"registers":[246,383,395,397],"old":[[395,397],[395,383],[246,397],[246,395]],"new":[[395,383],[246,395],[395,397]],"saving":1}, + {"start":2349,"stop":2354,"registers":[254,261,262,265],"old":[[262,265],[262,261],[254,262],[254,265],[254,261]],"new":[[254,262],[262,261],[262,265]],"saving":2} + ] +} diff --git a/research/r420-four-wire-cleanup/CLAIM.md b/research/r420-four-wire-cleanup/CLAIM.md new file mode 100644 index 0000000000..9fbc722321 --- /dev/null +++ b/research/r420-four-wire-cleanup/CLAIM.md @@ -0,0 +1,35 @@ +# Sprint claim: four-wire cleanup synthesis + +- Track: bit supplier. Fresh OS assignment seed **17**, generated with `secrets.randbelow(100)`. +- Base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +- Object: selected #543 R420 cleanup C, expanded into its ordered binary XORs. Width selected as `2 + (17 % 3) = 4`. +- Hypothesis: an arbitrary exact CNOT circuit on a contiguous window's same at-most-four registers can shorten that window. This admits noncommuting identities outside #710's completed commuting-deletion class. +- Method: enumerate GL(k,2), k=2,3,4, with exact shortest-path distances; exhaust contiguous original cleanup windows on at most four registers. If gains exist, choose nonoverlapping windows and check all arbitrary-input maps and complete costs. No extra helpers, copies, source accesses beyond the counted XORs, frame changes or recursive children may be omitted. +- Deliverable: a verified finite circuit improvement, or a complete scoped shortest-circuit census with rejection controls. No global circuit-optimality or new kappa claim. +- Finish target: 2026-10-13 05:43 UTC; reserve the last quarter of actual work for independent verification and handoff. +- Coordination: no pinned issues exist. Open queue initially 566 PRs through #747. Local claim recorded; no reservation issue opened. + +## Three candidates considered + +1. Frame-zero target-donor sharing in D: already crowded by #713/#716/#733/#742. +2. Synthesis of B block 7: resembles #670/#674; #688 already supplies composition and global verification. +3. Exact four-wire cleanup window synthesis: selected because it changes the search class beyond #710's commuting cancellation and specific conjugation. + +## Prior work and scope + +#710 `d97c8d20a8b885271a24c5a4e8446ac7f5697d5c` closes commuting-only deletion on the fixed cleanup and gives a different two-sandwich rewrite. This experiment does not repeat that search or import its patch. #688 `bb05c40c3e6319aa8c131b06a105e3648ac6c95b` concerns B blocks 3 and 5 and their changed cleanup. The archived R715 commuting-cancellation experiment is a different word and a narrower identity class. The selected result and actual #543 construction were inspected through the current selected certificate and #626 review. Previous contribution #739 is complex-side and independent. + +## Result and handoff — 2026-10-13 05:08 UTC + +Completed: [PR #754](https://github.com/CrocSwap/integer-mult-bounds/pull/754), +construction commit `8ee38f714dc80526c05a6653c1ff56a678615d49`. +All 7,693 original windows were examined; 284 admit shorter circuits. +The independently certified optimum over disjoint original windows saves +137 XORs in 101 replacements, taking the complete word from 26,916 to 26,779 +ADDs with unchanged paid paths and no new κ claim. Both words pass native +legality and 5/9/11-stage replay, including 96 omitted-bridge controls. +The final part of the sprint was reserved for independent review, relocated +replay, corruption controls and this handoff. Final queue refresh through +#753 found distinct concurrent decoder/compensation work, credited in the +README without an additive or composed saving claim. No pinned coordination +issue existed, so this is the single local claim update. diff --git a/research/r420-four-wire-cleanup/EXPECTED.json b/research/r420-four-wire-cleanup/EXPECTED.json new file mode 100644 index 0000000000..a0194cf750 --- /dev/null +++ b/research/r420-four-wire-cleanup/EXPECTED.json @@ -0,0 +1,165 @@ +{ + "status": "PASS_R420_FOUR_WIRE_CLEANUP", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "seed": 17, + "saving": 137, + "selected_windows": 101, + "windows_examined": 7693, + "independent_distances": { + "2": { + "states": 6, + "directed_edges_checked": 12, + "diameter": 3, + "layers": { + "0": 1, + "1": 2, + "2": 2, + "3": 1 + } + }, + "3": { + "states": 168, + "directed_edges_checked": 1008, + "diameter": 6, + "layers": { + "0": 1, + "1": 6, + "2": 24, + "3": 51, + "4": 60, + "5": 24, + "6": 2 + } + }, + "4": { + "states": 20160, + "directed_edges_checked": 241920, + "diameter": 9, + "layers": { + "0": 1, + "1": 12, + "2": 96, + "3": 542, + "4": 2058, + "5": 5316, + "6": 7530, + "7": 4058, + "8": 541, + "9": 6 + } + } + }, + "independent_windows": { + "windows_checked": 101, + "boolean_inputs_checked": 1408, + "selected_original_gates": 414, + "selected_replacement_gates": 277, + "saving": 137, + "all_replacements_shortest": true, + "nonnegative_transfer_columns_checked": 756, + "entrywise_dominance_forward_and_reverse": true + }, + "independent_census": { + "binary_gates": 2973, + "windows_checked": 7693, + "shortenable_windows": 284, + "maximum_single_window_saving": 3, + "optimal_disjoint_original_window_saving": 137, + "by_width": { + "2": { + "windows": 2973, + "shortenable": 0, + "maximum_length": 1 + }, + "3": { + "windows": 1927, + "shortenable": 45, + "maximum_length": 3 + }, + "4": { + "windows": 2793, + "shortenable": 239, + "maximum_length": 7 + } + }, + "saving_histogram": { + "0": 7409, + "1": 239, + "2": 39, + "3": 6 + }, + "scope": "All original contiguous windows with at most the stated wires; no extra registers, free permutations or iterative rewrites." + }, + "labels": { + "labels": 120, + "lattice_rank": 8, + "gram_det": 1, + "frames": 672 + }, + "original": { + "records": 29874, + "adds": 26916, + "moves": 2940, + "copies": 9, + "erasures": 9, + "paid_histogram": { + "1": 1320, + "2": 1440, + "4": 60, + "5": 120, + "8": 9 + }, + "rank_mass": 5112, + "phase_adds": { + "1": 19922, + "2": 2376, + "3": 568, + "4": 1077, + "5": 2973 + }, + "forward_prefix": 144651, + "reverse_prefix": 2270064, + "payload_upper": "998206739997057013039187410944", + "payload_bits": 100 + }, + "rewritten": { + "records": 29737, + "adds": 26779, + "moves": 2940, + "copies": 9, + "erasures": 9, + "paid_histogram": { + "1": 1320, + "2": 1440, + "4": 60, + "5": 120, + "8": 9 + }, + "rank_mass": 5112, + "phase_adds": { + "1": 19922, + "2": 2376, + "3": 568, + "4": 1077, + "5": 2836 + }, + "forward_prefix": 109173, + "reverse_prefix": 2270064, + "payload_upper": "429142879200064664450983477248", + "payload_bits": 99 + }, + "negative_controls": [ + "dropped replacement XOR", + "reversed source and destination", + "overlapping windows", + "forged distance potential", + "missing GL state", + "undeclared ancillary register", + "unpaid frame rank", + "missing cleanup" + ], + "rewritten_word_canonical_sha256": "5af46aa89fc362cc3fe9541ab833d4bbb26645ca6d767bce7197e995535afa5d", + "literal_H4": false, + "semantic_H4_prime": true, + "all_input_columns": 660 +} diff --git a/research/r420-four-wire-cleanup/NATIVE-EXPECTED.json b/research/r420-four-wire-cleanup/NATIVE-EXPECTED.json new file mode 100644 index 0000000000..3ae40de02d --- /dev/null +++ b/research/r420-four-wire-cleanup/NATIVE-EXPECTED.json @@ -0,0 +1,1138 @@ +{ + "original": { + "legality": { + "all_final_frames_pass": true, + "common_frame_ADDs": 26916, + "containment_pairs_checked": 2460, + "copies": 9, + "donor_intersections": 0, + "erasures": 9, + "max_inherited_integer_abs": 2, + "nested_MOVEs": 2940, + "new_frame_ids_collision": false, + "nondegeneracy_checked_by_separate_exact_bank_audit": true, + "old_max_frame_id": 671, + "paid_histogram": [ + [ + 1, + 1320 + ], + [ + 2, + 1440 + ], + [ + 4, + 60 + ], + [ + 5, + 120 + ], + [ + 8, + 9 + ] + ], + "rank_mass": 5112, + "records": 29874, + "scope": "Independent chronological geometry/copy/source-owner audit. F2 all-column replay is in the separately freshly compiled transform receipt; address transform theorem and bank completion remain separate.", + "selected_helpers": 0, + "selected_pairs": 0, + "source_owner_intersections": 0, + "status": "PASS_INDEPENDENT_COHORT_LEGALITY_SOURCE_OWNERS_AND_LIFECYCLE" + }, + "columns": { + "5": { + "bridge_additions": 720, + "copied_center_original_source_immutable": true, + "five_stage_additions": 134580, + "formal_columns_checked": 900, + "fresh_center_copies": 45, + "global_live_registers": 900, + "independent_dirty_registers": 420, + "local_odd_scalar_additions": 26916, + "local_raw_H": [ + [ + 1, + 1320 + ], + [ + 2, + 1440 + ], + [ + 4, + 60 + ], + [ + 5, + 120 + ], + [ + 8, + 9 + ] + ], + "local_registers": 660, + "local_scalar_additions": 26916, + "negative_controls": [ + { + "omit_bridge": 0, + "rejected": true + }, + { + "omit_bridge": 1, + "rejected": true + }, + { + "omit_bridge": 2, + "rejected": true + }, + { + "omit_bridge": 3, + "rejected": true + }, + { + "omit_bridge": 4, + "rejected": true + }, + { + "omit_bridge": 5, + "rejected": true + } + ], + "new_Q_categories": [ + 28, + 29 + ], + "payload_prefix_bits": 100, + "payload_prefix_upper": "998206739997057013039187410944", + "reverse_fresh_center_copies": 18, + "scope": "All independent physical input columns over F2, including all arbitrary helper dirt, restored; external copied-center work closes to zero. New cohort scalar lift uses actual signed coefficients and computed cancellation-free bounds; unchanged source527 signed decoder remains separate defining evidence. Physical projector routing and paid rank/bank receipts are independently bound, not inferred from scalar check.", + "signed_lift_prefix": [ + { + "bits": 18, + "cancellation_free_signed_row_l1_upper": "144651", + "reverse": false + }, + { + "bits": 22, + "cancellation_free_signed_row_l1_upper": "2270064", + "reverse": true + } + ], + "signed_reverse_semantics": "Reverse ADD coefficient negated; reverse DISCARD is fresh COPY from recorded unchanged original center; reverse COPY is DISCARD. Each such block is inverse over every commutative coefficient ring, by elementary-shear induction.", + "stages": [ + { + "fresh_copies": 9, + "scalar_additions": 26916, + "signed_inverse": false, + "stage": 0 + }, + { + "fresh_copies": 9, + "scalar_additions": 26916, + "signed_inverse": true, + "stage": 1 + }, + { + "fresh_copies": 9, + "scalar_additions": 26916, + "signed_inverse": false, + "stage": 2 + }, + { + "fresh_copies": 9, + "scalar_additions": 26916, + "signed_inverse": true, + "stage": 3 + }, + { + "fresh_copies": 9, + "scalar_additions": 26916, + "signed_inverse": false, + "stage": 4 + } + ], + "status": "PASS_NEW_COHORT249_ALL_FIVE_STAGE_FORMAL_COLUMNS_AND_PREFIX_BILL" + }, + "9": { + "bridge_additions": 2160, + "copied_center_original_source_immutable": true, + "formal_columns_checked": 1380, + "fresh_center_copies": 81, + "global_live_registers": 1380, + "independent_dirty_registers": 420, + "local_odd_scalar_additions": 26916, + "local_raw_H": [ + [ + 1, + 1320 + ], + [ + 2, + 1440 + ], + [ + 4, + 60 + ], + [ + 5, + 120 + ], + [ + 8, + 9 + ] + ], + "local_registers": 660, + "local_scalar_additions": 26916, + "negative_controls": [ + { + "omit_bridge": 0, + "rejected": true + }, + { + "omit_bridge": 1, + "rejected": true + }, + { + "omit_bridge": 2, + "rejected": true + }, + { + "omit_bridge": 3, + "rejected": true + }, + { + "omit_bridge": 4, + "rejected": true + }, + { + "omit_bridge": 5, + "rejected": true + }, + { + "omit_bridge": 6, + "rejected": true + }, + { + "omit_bridge": 7, + "rejected": true + }, + { + "omit_bridge": 8, + "rejected": true + }, + { + "omit_bridge": 9, + "rejected": true + }, + { + "omit_bridge": 10, + "rejected": true + }, + { + "omit_bridge": 11, + "rejected": true + }, + { + "omit_bridge": 12, + "rejected": true + }, + { + "omit_bridge": 13, + "rejected": true + }, + { + "omit_bridge": 14, + "rejected": true + }, + { + "omit_bridge": 15, + "rejected": true + }, + { + "omit_bridge": 16, + "rejected": true + }, + { + "omit_bridge": 17, + "rejected": true + } + ], + "new_Q_categories": [ + 28, + 29 + ], + "payload_prefix_bits": 100, + "payload_prefix_upper": "998206739997057013039187410944", + "reverse_fresh_center_copies": 36, + "scope": "All independent physical input columns over F2, including all arbitrary helper dirt, restored; external copied-center work closes to zero. New cohort scalar lift uses actual signed coefficients and computed cancellation-free bounds; unchanged source527 signed decoder remains separate defining evidence. Physical projector routing and paid rank/bank receipts are independently bound, not inferred from scalar check.", + "signed_lift_prefix": [ + { + "bits": 18, + "cancellation_free_signed_row_l1_upper": "144651", + "reverse": false + }, + { + "bits": 22, + "cancellation_free_signed_row_l1_upper": "2270064", + "reverse": true + } + ], + "signed_reverse_semantics": "Reverse ADD coefficient negated; reverse DISCARD is fresh COPY from recorded unchanged original center; reverse COPY is DISCARD. Each such block is inverse over every commutative coefficient ring, by elementary-shear induction.", + "stage_additions": 242244, + "stages": [ + { + "fresh_copies": 9, + "scalar_additions": 26916, + "signed_inverse": false, + "stage": 0 + }, + { + "fresh_copies": 9, + "scalar_additions": 26916, + "signed_inverse": true, + "stage": 1 + }, + { + "fresh_copies": 9, + "scalar_additions": 26916, + "signed_inverse": false, + "stage": 2 + }, + { + "fresh_copies": 9, + "scalar_additions": 26916, + "signed_inverse": true, + "stage": 3 + }, + { + "fresh_copies": 9, + "scalar_additions": 26916, + "signed_inverse": false, + "stage": 4 + }, + { + "fresh_copies": 9, + "scalar_additions": 26916, + "signed_inverse": true, + "stage": 5 + }, + { + "fresh_copies": 9, + "scalar_additions": 26916, + "signed_inverse": false, + "stage": 6 + }, + { + "fresh_copies": 9, + "scalar_additions": 26916, + "signed_inverse": true, + "stage": 7 + }, + { + "fresh_copies": 9, + "scalar_additions": 26916, + "signed_inverse": false, + "stage": 8 + } + ], + "status": "PASS_NEW_COHORT249_ALL_BRIDGED_STAGE_FORMAL_COLUMNS_AND_PREFIX_BILL" + }, + "11": { + "bridge_additions": 2880, + "copied_center_original_source_immutable": true, + "formal_columns_checked": 1620, + "fresh_center_copies": 99, + "global_live_registers": 1620, + "independent_dirty_registers": 420, + "local_odd_scalar_additions": 26916, + "local_raw_H": [ + [ + 1, + 1320 + ], + [ + 2, + 1440 + ], + [ + 4, + 60 + ], + [ + 5, + 120 + ], + [ + 8, + 9 + ] + ], + "local_registers": 660, + "local_scalar_additions": 26916, + "negative_controls": [ + { + "omit_bridge": 0, + "rejected": true + }, + { + "omit_bridge": 1, + "rejected": true + }, + { + "omit_bridge": 2, + "rejected": true + }, + { + "omit_bridge": 3, + "rejected": true + }, + { + "omit_bridge": 4, + "rejected": true + }, + { + "omit_bridge": 5, + "rejected": true + }, + { + "omit_bridge": 6, + "rejected": true + }, + { + "omit_bridge": 7, + "rejected": true + }, + { + "omit_bridge": 8, + "rejected": true + }, + { + "omit_bridge": 9, + "rejected": true + }, + { + "omit_bridge": 10, + "rejected": true + }, + { + "omit_bridge": 11, + "rejected": true + }, + { + "omit_bridge": 12, + "rejected": true + }, + { + "omit_bridge": 13, + "rejected": true + }, + { + "omit_bridge": 14, + "rejected": true + }, + { + "omit_bridge": 15, + "rejected": true + }, + { + "omit_bridge": 16, + "rejected": true + }, + { + "omit_bridge": 17, + "rejected": true + }, + { + "omit_bridge": 18, + "rejected": true + }, + { + "omit_bridge": 19, + "rejected": true + }, + { + "omit_bridge": 20, + "rejected": true + }, + { + "omit_bridge": 21, + "rejected": true + }, + { + "omit_bridge": 22, + "rejected": true + }, + { + "omit_bridge": 23, + "rejected": true + } + ], + "new_Q_categories": [ + 28, + 29 + ], + "payload_prefix_bits": 100, + "payload_prefix_upper": "998206739997057013039187410944", + "reverse_fresh_center_copies": 45, + "scope": "All independent physical input columns over F2, including all arbitrary helper dirt, restored; external copied-center work closes to zero. New cohort scalar lift uses actual signed coefficients and computed cancellation-free bounds; unchanged source527 signed decoder remains separate defining evidence. Physical projector routing and paid rank/bank receipts are independently bound, not inferred from scalar check.", + "signed_lift_prefix": [ + { + "bits": 18, + "cancellation_free_signed_row_l1_upper": "144651", + "reverse": false + }, + { + "bits": 22, + "cancellation_free_signed_row_l1_upper": "2270064", + "reverse": true + } + ], + "signed_reverse_semantics": "Reverse ADD coefficient negated; reverse DISCARD is fresh COPY from recorded unchanged original center; reverse COPY is DISCARD. Each such block is inverse over every commutative coefficient ring, by elementary-shear induction.", + "stage_additions": 296076, + "stages": [ + { + "fresh_copies": 9, + "scalar_additions": 26916, + "signed_inverse": false, + "stage": 0 + }, + { + "fresh_copies": 9, + "scalar_additions": 26916, + "signed_inverse": true, + "stage": 1 + }, + { + "fresh_copies": 9, + "scalar_additions": 26916, + "signed_inverse": false, + "stage": 2 + }, + { + "fresh_copies": 9, + "scalar_additions": 26916, + "signed_inverse": true, + "stage": 3 + }, + { + "fresh_copies": 9, + "scalar_additions": 26916, + "signed_inverse": false, + "stage": 4 + }, + { + "fresh_copies": 9, + "scalar_additions": 26916, + "signed_inverse": true, + "stage": 5 + }, + { + "fresh_copies": 9, + "scalar_additions": 26916, + "signed_inverse": false, + "stage": 6 + }, + { + "fresh_copies": 9, + "scalar_additions": 26916, + "signed_inverse": true, + "stage": 7 + }, + { + "fresh_copies": 9, + "scalar_additions": 26916, + "signed_inverse": false, + "stage": 8 + }, + { + "fresh_copies": 9, + "scalar_additions": 26916, + "signed_inverse": true, + "stage": 9 + }, + { + "fresh_copies": 9, + "scalar_additions": 26916, + "signed_inverse": false, + "stage": 10 + } + ], + "status": "PASS_NEW_COHORT249_ALL_BRIDGED_STAGE_FORMAL_COLUMNS_AND_PREFIX_BILL" + } + } + }, + "rewritten": { + "legality": { + "all_final_frames_pass": true, + "common_frame_ADDs": 26779, + "containment_pairs_checked": 2460, + "copies": 9, + "donor_intersections": 0, + "erasures": 9, + "max_inherited_integer_abs": 2, + "nested_MOVEs": 2940, + "new_frame_ids_collision": false, + "nondegeneracy_checked_by_separate_exact_bank_audit": true, + "old_max_frame_id": 671, + "paid_histogram": [ + [ + 1, + 1320 + ], + [ + 2, + 1440 + ], + [ + 4, + 60 + ], + [ + 5, + 120 + ], + [ + 8, + 9 + ] + ], + "rank_mass": 5112, + "records": 29737, + "scope": "Independent chronological geometry/copy/source-owner audit. F2 all-column replay is in the separately freshly compiled transform receipt; address transform theorem and bank completion remain separate.", + "selected_helpers": 0, + "selected_pairs": 0, + "source_owner_intersections": 0, + "status": "PASS_INDEPENDENT_COHORT_LEGALITY_SOURCE_OWNERS_AND_LIFECYCLE" + }, + "columns": { + "5": { + "bridge_additions": 720, + "copied_center_original_source_immutable": true, + "five_stage_additions": 133895, + "formal_columns_checked": 900, + "fresh_center_copies": 45, + "global_live_registers": 900, + "independent_dirty_registers": 420, + "local_odd_scalar_additions": 26779, + "local_raw_H": [ + [ + 1, + 1320 + ], + [ + 2, + 1440 + ], + [ + 4, + 60 + ], + [ + 5, + 120 + ], + [ + 8, + 9 + ] + ], + "local_registers": 660, + "local_scalar_additions": 26779, + "negative_controls": [ + { + "omit_bridge": 0, + "rejected": true + }, + { + "omit_bridge": 1, + "rejected": true + }, + { + "omit_bridge": 2, + "rejected": true + }, + { + "omit_bridge": 3, + "rejected": true + }, + { + "omit_bridge": 4, + "rejected": true + }, + { + "omit_bridge": 5, + "rejected": true + } + ], + "new_Q_categories": [ + 28, + 29 + ], + "payload_prefix_bits": 99, + "payload_prefix_upper": "429142879200064664450983477248", + "reverse_fresh_center_copies": 18, + "scope": "All independent physical input columns over F2, including all arbitrary helper dirt, restored; external copied-center work closes to zero. New cohort scalar lift uses actual signed coefficients and computed cancellation-free bounds; unchanged source527 signed decoder remains separate defining evidence. Physical projector routing and paid rank/bank receipts are independently bound, not inferred from scalar check.", + "signed_lift_prefix": [ + { + "bits": 17, + "cancellation_free_signed_row_l1_upper": "109173", + "reverse": false + }, + { + "bits": 22, + "cancellation_free_signed_row_l1_upper": "2270064", + "reverse": true + } + ], + "signed_reverse_semantics": "Reverse ADD coefficient negated; reverse DISCARD is fresh COPY from recorded unchanged original center; reverse COPY is DISCARD. Each such block is inverse over every commutative coefficient ring, by elementary-shear induction.", + "stages": [ + { + "fresh_copies": 9, + "scalar_additions": 26779, + "signed_inverse": false, + "stage": 0 + }, + { + "fresh_copies": 9, + "scalar_additions": 26779, + "signed_inverse": true, + "stage": 1 + }, + { + "fresh_copies": 9, + "scalar_additions": 26779, + "signed_inverse": false, + "stage": 2 + }, + { + "fresh_copies": 9, + "scalar_additions": 26779, + "signed_inverse": true, + "stage": 3 + }, + { + "fresh_copies": 9, + "scalar_additions": 26779, + "signed_inverse": false, + "stage": 4 + } + ], + "status": "PASS_NEW_COHORT249_ALL_FIVE_STAGE_FORMAL_COLUMNS_AND_PREFIX_BILL" + }, + "9": { + "bridge_additions": 2160, + "copied_center_original_source_immutable": true, + "formal_columns_checked": 1380, + "fresh_center_copies": 81, + "global_live_registers": 1380, + "independent_dirty_registers": 420, + "local_odd_scalar_additions": 26779, + "local_raw_H": [ + [ + 1, + 1320 + ], + [ + 2, + 1440 + ], + [ + 4, + 60 + ], + [ + 5, + 120 + ], + [ + 8, + 9 + ] + ], + "local_registers": 660, + "local_scalar_additions": 26779, + "negative_controls": [ + { + "omit_bridge": 0, + "rejected": true + }, + { + "omit_bridge": 1, + "rejected": true + }, + { + "omit_bridge": 2, + "rejected": true + }, + { + "omit_bridge": 3, + "rejected": true + }, + { + "omit_bridge": 4, + "rejected": true + }, + { + "omit_bridge": 5, + "rejected": true + }, + { + "omit_bridge": 6, + "rejected": true + }, + { + "omit_bridge": 7, + "rejected": true + }, + { + "omit_bridge": 8, + "rejected": true + }, + { + "omit_bridge": 9, + "rejected": true + }, + { + "omit_bridge": 10, + "rejected": true + }, + { + "omit_bridge": 11, + "rejected": true + }, + { + "omit_bridge": 12, + "rejected": true + }, + { + "omit_bridge": 13, + "rejected": true + }, + { + "omit_bridge": 14, + "rejected": true + }, + { + "omit_bridge": 15, + "rejected": true + }, + { + "omit_bridge": 16, + "rejected": true + }, + { + "omit_bridge": 17, + "rejected": true + } + ], + "new_Q_categories": [ + 28, + 29 + ], + "payload_prefix_bits": 99, + "payload_prefix_upper": "429142879200064664450983477248", + "reverse_fresh_center_copies": 36, + "scope": "All independent physical input columns over F2, including all arbitrary helper dirt, restored; external copied-center work closes to zero. New cohort scalar lift uses actual signed coefficients and computed cancellation-free bounds; unchanged source527 signed decoder remains separate defining evidence. Physical projector routing and paid rank/bank receipts are independently bound, not inferred from scalar check.", + "signed_lift_prefix": [ + { + "bits": 17, + "cancellation_free_signed_row_l1_upper": "109173", + "reverse": false + }, + { + "bits": 22, + "cancellation_free_signed_row_l1_upper": "2270064", + "reverse": true + } + ], + "signed_reverse_semantics": "Reverse ADD coefficient negated; reverse DISCARD is fresh COPY from recorded unchanged original center; reverse COPY is DISCARD. Each such block is inverse over every commutative coefficient ring, by elementary-shear induction.", + "stage_additions": 241011, + "stages": [ + { + "fresh_copies": 9, + "scalar_additions": 26779, + "signed_inverse": false, + "stage": 0 + }, + { + "fresh_copies": 9, + "scalar_additions": 26779, + "signed_inverse": true, + "stage": 1 + }, + { + "fresh_copies": 9, + "scalar_additions": 26779, + "signed_inverse": false, + "stage": 2 + }, + { + "fresh_copies": 9, + "scalar_additions": 26779, + "signed_inverse": true, + "stage": 3 + }, + { + "fresh_copies": 9, + "scalar_additions": 26779, + "signed_inverse": false, + "stage": 4 + }, + { + "fresh_copies": 9, + "scalar_additions": 26779, + "signed_inverse": true, + "stage": 5 + }, + { + "fresh_copies": 9, + "scalar_additions": 26779, + "signed_inverse": false, + "stage": 6 + }, + { + "fresh_copies": 9, + "scalar_additions": 26779, + "signed_inverse": true, + "stage": 7 + }, + { + "fresh_copies": 9, + "scalar_additions": 26779, + "signed_inverse": false, + "stage": 8 + } + ], + "status": "PASS_NEW_COHORT249_ALL_BRIDGED_STAGE_FORMAL_COLUMNS_AND_PREFIX_BILL" + }, + "11": { + "bridge_additions": 2880, + "copied_center_original_source_immutable": true, + "formal_columns_checked": 1620, + "fresh_center_copies": 99, + "global_live_registers": 1620, + "independent_dirty_registers": 420, + "local_odd_scalar_additions": 26779, + "local_raw_H": [ + [ + 1, + 1320 + ], + [ + 2, + 1440 + ], + [ + 4, + 60 + ], + [ + 5, + 120 + ], + [ + 8, + 9 + ] + ], + "local_registers": 660, + "local_scalar_additions": 26779, + "negative_controls": [ + { + "omit_bridge": 0, + "rejected": true + }, + { + "omit_bridge": 1, + "rejected": true + }, + { + "omit_bridge": 2, + "rejected": true + }, + { + "omit_bridge": 3, + "rejected": true + }, + { + "omit_bridge": 4, + "rejected": true + }, + { + "omit_bridge": 5, + "rejected": true + }, + { + "omit_bridge": 6, + "rejected": true + }, + { + "omit_bridge": 7, + "rejected": true + }, + { + "omit_bridge": 8, + "rejected": true + }, + { + "omit_bridge": 9, + "rejected": true + }, + { + "omit_bridge": 10, + "rejected": true + }, + { + "omit_bridge": 11, + "rejected": true + }, + { + "omit_bridge": 12, + "rejected": true + }, + { + "omit_bridge": 13, + "rejected": true + }, + { + "omit_bridge": 14, + "rejected": true + }, + { + "omit_bridge": 15, + "rejected": true + }, + { + "omit_bridge": 16, + "rejected": true + }, + { + "omit_bridge": 17, + "rejected": true + }, + { + "omit_bridge": 18, + "rejected": true + }, + { + "omit_bridge": 19, + "rejected": true + }, + { + "omit_bridge": 20, + "rejected": true + }, + { + "omit_bridge": 21, + "rejected": true + }, + { + "omit_bridge": 22, + "rejected": true + }, + { + "omit_bridge": 23, + "rejected": true + } + ], + "new_Q_categories": [ + 28, + 29 + ], + "payload_prefix_bits": 99, + "payload_prefix_upper": "429142879200064664450983477248", + "reverse_fresh_center_copies": 45, + "scope": "All independent physical input columns over F2, including all arbitrary helper dirt, restored; external copied-center work closes to zero. New cohort scalar lift uses actual signed coefficients and computed cancellation-free bounds; unchanged source527 signed decoder remains separate defining evidence. Physical projector routing and paid rank/bank receipts are independently bound, not inferred from scalar check.", + "signed_lift_prefix": [ + { + "bits": 17, + "cancellation_free_signed_row_l1_upper": "109173", + "reverse": false + }, + { + "bits": 22, + "cancellation_free_signed_row_l1_upper": "2270064", + "reverse": true + } + ], + "signed_reverse_semantics": "Reverse ADD coefficient negated; reverse DISCARD is fresh COPY from recorded unchanged original center; reverse COPY is DISCARD. Each such block is inverse over every commutative coefficient ring, by elementary-shear induction.", + "stage_additions": 294569, + "stages": [ + { + "fresh_copies": 9, + "scalar_additions": 26779, + "signed_inverse": false, + "stage": 0 + }, + { + "fresh_copies": 9, + "scalar_additions": 26779, + "signed_inverse": true, + "stage": 1 + }, + { + "fresh_copies": 9, + "scalar_additions": 26779, + "signed_inverse": false, + "stage": 2 + }, + { + "fresh_copies": 9, + "scalar_additions": 26779, + "signed_inverse": true, + "stage": 3 + }, + { + "fresh_copies": 9, + "scalar_additions": 26779, + "signed_inverse": false, + "stage": 4 + }, + { + "fresh_copies": 9, + "scalar_additions": 26779, + "signed_inverse": true, + "stage": 5 + }, + { + "fresh_copies": 9, + "scalar_additions": 26779, + "signed_inverse": false, + "stage": 6 + }, + { + "fresh_copies": 9, + "scalar_additions": 26779, + "signed_inverse": true, + "stage": 7 + }, + { + "fresh_copies": 9, + "scalar_additions": 26779, + "signed_inverse": false, + "stage": 8 + }, + { + "fresh_copies": 9, + "scalar_additions": 26779, + "signed_inverse": true, + "stage": 9 + }, + { + "fresh_copies": 9, + "scalar_additions": 26779, + "signed_inverse": false, + "stage": 10 + } + ], + "status": "PASS_NEW_COHORT249_ALL_BRIDGED_STAGE_FORMAL_COLUMNS_AND_PREFIX_BILL" + } + } + } +} diff --git a/research/r420-four-wire-cleanup/README.md b/research/r420-four-wire-cleanup/README.md new file mode 100644 index 0000000000..52ba8d43d4 --- /dev/null +++ b/research/r420-four-wire-cleanup/README.md @@ -0,0 +1,258 @@ +# R420 cleanup: 137 fewer XORs from exact four-wire synthesis + +**Status: finite bit-supplier construction and independently checked search.** +The selected #543 word's cleanup drops from **2,973 to 2,836 binary XORs**. +The complete native word drops from **26,916 to 26,779 ADDs**, with the same +2,940 frame MOVEs, nine paid copies, nine erasures, 420 dirty helpers and every +register's frame path. The paid recursive histogram is unchanged. This is not +a new supplier exponent or a new κ claim. + +Base commit: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +The [selected certificate](../../certificates/selected-result.json) at that base +selects #626/#622/#623 with #543, conditional +κ = `51110230636731/31250000000000000` = `0.001635527380375392`. +The [current review](../../docs/research/community-k492-review.md), rather than +historical frontier labels, determines that context. + +## Reproduce + +Python 3.11 or newer, standard library only, from the repository root: + +```sh +python3 -I -B research/r420-four-wire-cleanup/verify.py +``` + +Expected final line: + +```text +PASS_R420_FOUR_WIRE_CLEANUP: 101 windows, 137 XORs saved; 26916 -> 26779 native ADDs; 8 negative controls rejected +``` + +The default command uses a temporary directory and leaves the checkout alone. +To retain both complete words, their actual native exports and the receipt: + +```sh +python3 -I -B research/r420-four-wire-cleanup/verify.py --out /tmp/r420-four-wire-check +``` + +The output directory must not exist. The changed word is +`rewritten/word.json`; the record stream is +`rewritten/records/249-records.bin`. The canonical JSON hash of the changed word +is `5af46aa89fc362cc3fe9541ab833d4bbb26645ca6d767bce7197e995535afa5d`. +No compressed-output hash is used as a mathematical equality test. + +[SOURCE.json](SOURCE.json) pins every imported implementation and the source +word by SHA-256, plus its complete canonical payload. [CERTIFICATE.json](CERTIFICATE.json) +contains all 101 exact original slices and replacement circuits. +[EXPECTED.json](EXPECTED.json) is the deterministic verification receipt. + +For the supplementary unchanged C++ legality and five/nine/eleven-stage +checkers, use a C++17 compiler and Boost headers: + +```sh +python3 -I -B research/r420-four-wire-cleanup/native.py /tmp/r420-four-wire-native --boost-include /path/to/boost/include +``` + +This first runs the Python check, then compiles and runs the retained checkers +on both words. It compares all deterministic receipt fields against +[NATIVE-EXPECTED.json](NATIVE-EXPECTED.json). The final line begins +`PASS_NATIVE_R420_FOUR_WIRE`. [VALIDATION.md](VALIDATION.md) records the tested +environment and its compatibility flag. + +## Search class and completed coverage + +The fresh OS assignment seed was **17**, selecting the bit-supplier track and +width `2 + (17 % 3) = 4`. The [claim](CLAIM.md) records three candidate tasks, +the coordination check and the choice of a less explored search class. +The search has no random trials, heuristic timeout or incomplete tail. + +Expand each cleanup gate `[frame, target, sources]` into its listed-source +sequence of binary XORs. Enumerate every nonempty contiguous interval of this +**original** sequence whose union of registers has size at most four. For each +interval, permit any circuit of `target ^= source` with distinct operands from +that same register set. Registers remain labeled: no free permutations, +ancillas, reads of global y/output registers, frame changes or extra wires are +allowed. Stop extending +an interval immediately when its register union exceeds four; the union cannot +shrink. No second synthesis pass is included. + +| Original register count | Windows examined | Shortenable windows | Longest interval | +| --- | ---: | ---: | ---: | +| 2 | 2,973 | 0 | 1 | +| 3 | 1,927 | 45 | 3 | +| 4 | 2,793 | 239 | 7 | +| Total | **7,693** | **284** | 7 | + +Of the 284 shortenable intervals, 239 save one XOR, 39 save two, and six save +three. Weighted interval scheduling selects 101 disjoint intervals, replacing +414 gates by 277. **137 is the maximum saving in this one-layer, +disjoint-original-interval model.** This is not a lower bound on the size of an +arbitrary cleanup circuit: wider windows, different orderings, iterative +rewrites and circuits using other registers remain outside the search. + +For example, interval `[158,163)` acts on registers 16, 22, 103 and 118: + +```text +old: 22^=118; 103^=22; 103^=118; 16^=22; 16^=118 +new: 16^=22; 103^=22; 22^=118 +``` + +Both send `(a,b,c,d)=(x16,x22,x103,x118)` to +`(a+b,b+d,c+b,d)` over F2. This illustrates the search class; the committed +packing may choose a different overlapping interval when maximizing total gain. + +## Independent finite distance and circuit evidence + +The producer in [verify.py](verify.py) performs breadth-first search on packed +**rows** of GL(k,2), for k = 2, 3, 4, using all k(k−1) XOR generators. It then +does interval scheduling by decreasing start position. Equal scores skip the +current start, or retain the first improving stop; this fixes all tie breaking. + +[independent.py](independent.py) imports no producer code. It: + +1. Enumerates all binary matrices and recognizes invertible **columns** by their + generated F2 span. It checks 6, 168 and 20,160 states respectively. +2. Converts the proposed distance labels to columns and checks zero only at the + identity, nonnegative labels, every directed edge's one-Lipschitz inequality, + and a descending neighbor from each nonidentity state. There are 242,940 + directed edges in total. Along any path from the identity the label rises by + at most one; descending neighbors supply a path of the claimed length. + These finite checks certify the exact distances in this gate model. +3. Recomputes its own column BFS and incrementally scans all original intervals. + A separate end-time interval-scheduling implementation confirms the optimum. +4. Replays every selected replacement on **all 1,408 Boolean inputs** across + the individual windows, checks the actual labeled register sets and original + slices, and verifies that every replacement attains its exact distance. + +The whole original and changed words are also replayed on all **660 independent +input columns**, including arbitrary helper dirt, by the unchanged #543 +`xcheck.py`. Its geometric checks certify the original 120 labels and all 672 +unchanged closed frames. The newly exported record bytes receive an additional +chronological frame, copy-lifecycle, rank-charge and full-input replay. + +## Cleanup interface, frames and precision + +The #543 interface's literal-reversal hypothesis H4 intentionally fails on this +word: the cleanup is resynthesized. The verifier preserves that guard and +requires its failure, while checking all other hypotheses and all conclusions. +The applicable replacement, **H4′**, is semantic: + +> C acts on source/helper registers only, at the full frame, and implements +> the inverse of the raw A/B source/helper map U over F2. + +This suffices for the same finite interface conclusion. The unchanged raw word +has the block form `z' = U z`, `y' = y + J x + K s`, with `J = I` and D adding +the same `K s`. Every chosen window is the same labeled linear map, so the new +C is the old C as a matrix and hence is `U^-1`. Applying it restores every +source/helper, independently of the initial target or helper values. Nothing +here asserts that the new positive-integer cleanup is an integer inverse of U. +The inherited **whole-word** signed inverse still reverses the event order and +negates ADD coefficients, interchanging copy and erase. + +All C gates have full frame 1, but an operand can still need a paid climb before +its first cleanup use. The verifier therefore compares the complete per-register +MOVE paths emitted for both words, not just final frame IDs or rank totals. +Every such path and every COPY/ERASE record is identical. Some first-use times +move; their actual common-frame legality is freshly checked. Splitting a +multi-source gate does not introduce an unpaid climb. + +There is also a prefix certificate stronger than fewer gates. For each window, +replace XOR by nonnegative integer addition and compute its transfer matrix. +The new matrix is entrywise at most the old matrix, **both in forward order and +in reversed order**, verified with 756 separate basis-column propagations. +For nonnegative inputs, coordinates during an add-only interval increase +monotonically. Thus every new intermediate coordinate is bounded by its new +endpoint, which is bounded by the old endpoint. Unchanged intervening positive +operations preserve this domination. This proves preservation of these +cancellation-free envelopes for the fixed circuit and its signed reverse. + +The actual native prefix replay gives: + +| Quantity | Original | Rewritten | +| --- | ---: | ---: | +| Forward positive prefix | 144,651 | 109,173 | +| Reverse positive prefix | 2,270,064 | 2,270,064 | +| `64 F^3 B^2` | 998206739997057013039187410944 | 429142879200064664450983477248 | +| Payload upper-bound bit length | 100 | 99 | + +The rewritten value remains below the inherited `2^104` local payload ceiling. +This is a local signed-prefix check, not a fresh global hosted invoice. + +## Complete local cost and limits + +| Count | Original | Rewritten | +| --- | ---: | ---: | +| D / A / scatter / B ADDs | 19,922 / 2,376 / 568 / 1,077 | identical | +| C ADDs, including restoration | 2,973 | 2,836 | +| Total ADDs | 26,916 | 26,779 | +| Paid MOVEs / COPYs / ERASEs | 2,940 / 9 / 9 | identical | +| Total native records | 29,874 | 29,737 | +| Live registers / copied temporary | 660 / 1 | identical | +| Dirty helpers / retained totals | 420 / 9 | identical | +| Rank mass | 5,112 | 5,112 | + +The complete rank histogram remains +`{1:1320, 2:1440, 4:60, 5:120, 8:9}`. All new XORs are actual priced native +ADDs in frame 1; no auxiliary preparation, source access, frame conversion, +restoration, copied information or recursive child is hidden. The scalar +saving does not improve this recursive histogram, and the selected assembly +remains complex-bound. This package does not regenerate a global hosted +program, reprice an outer assembly or alter a selected certificate. + +Eight negative controls reject a dropped XOR, reversed operand orientation, +overlapping windows, a forged distance label, a missing GL state, an undeclared +extra register, an undercharged frame MOVE and omitted cleanup. The unchanged +literal-H4 guard also reports failure as expected. The finite search and replay +do not prove the all-size multiplication theorem; common-label/mutable-basis +realization, compiler, hosting, residual, precision/tape and analytic assumptions +remain those of the selected review. + +## Attribution and relation to concurrent work + +Prepared by **Jeffrey Cox (@namredips)** with substantial **OpenAI Codex** +assistance, including an independently implemented column-based checker and +scoped review. New files use the repository's Apache-2.0 license. + +The source word and `xcheck.py` are **eumemic's #543**, head +`2065fe4f72a914d907f1046603f5a36f17018535`; their +[notice](../e8-bit-r420/NOTICE.md) preserves the earlier contributors and AI +disclosures. The native exporter is retained from **#493**; its author header +credits **Dylan Crow** with Anthropic Claude assistance. No imported source is +edited or reattributed. + +**Sagar Thakrar's [#710](https://github.com/CrocSwap/integer-mult-bounds/pull/710)**, +head `d97c8d20a8b885271a24c5a4e8446ac7f5697d5c`, is the methodological and +semantic-interface predecessor: it closes commuting-only deletion on this word +and saves two XORs by noncontiguous conjugation. This search instead permits +arbitrary circuits inside contiguous four-wire intervals. Its two distant +sandwiches are not among these intervals. Our `[1318,1322)` overlaps two of its +deleted gates, so **no composition or additive 139-XOR saving is claimed**. + +**Ali Romman's [#688](https://github.com/CrocSwap/integer-mult-bounds/pull/688)**, +head `bb05c40c3e6319aa8c131b06a105e3648ac6c95b`, composes B-block changes and +their cleanup with global replay. **@ellipsi2's +[#742](https://github.com/CrocSwap/integer-mult-bounds/pull/742)**, +head `6e7a5d271a123886dc7b54ca3180d0b9f9beda5a`, changes D using target donors. +This package does not import or claim compatibility with either patch. The +archived [R715 commuting experiment](../experiment-log/negative-searches/commuting-cancellations/README.md) +has a different word and narrower gate identities; this is not a repeated +search with a different seed. + +The final queue refresh also inspected **Chinmay Khaladkar's +[#748](https://github.com/CrocSwap/integer-mult-bounds/pull/748)** at +`0ccc0b425d2b9667108d3a0918a5cfa0aa7a5861` (a changed decoder-total source +coset and compensated dirty operator), and **Alluri's +[#681](https://github.com/CrocSwap/integer-mult-bounds/pull/681)** at +`e536f6fc8aad65adef8ac4682d13625598a5c3f9` (a six-package circuit consolidation). +Neither supplies this finite shortest-CNOT window census. Both change the word +to which these original interval indices refer; integrating this mechanism +would require new synthesis and verification rather than adding headline +savings. No priority is claimed over their underlying circuit mechanisms. + +Immediately before submission, **Sagar Thakrar's +[#753](https://github.com/CrocSwap/integer-mult-bounds/pull/753)** appeared at +`2b30b63789f6d9948233fc67d9d79bca6b185c5b`: restored helper stars in decoder +totals, with literal reverse cleanup and a larger positive prefix. That is +another A/C mechanism; this contribution holds A fixed and independently +resynthesizes C with a nonincreasing positive envelope. Its 128-XOR saving is +not combined with the 137 certified here. diff --git a/research/r420-four-wire-cleanup/SOURCE.json b/research/r420-four-wire-cleanup/SOURCE.json new file mode 100644 index 0000000000..b8e18b99bc --- /dev/null +++ b/research/r420-four-wire-cleanup/SOURCE.json @@ -0,0 +1,37 @@ +{ + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "word": "research/e8-bit-r420/data/bitE8mut-r420.json.gz", + "exporter": "research/e8-bit-carrier-skeleton/code/bit/export_records.py", + "xcheck": "research/e8-bit-r420/code/xcheck.py", + "word_canonical_sha256": "e597e3885c0a8daa262afa5985ee2930443329126aece76d33159d81882bdcc2", + "source_pr": 543, + "source_head": "2065fe4f72a914d907f1046603f5a36f17018535", + "selected_result": { + "pr": 626, + "head": "660de893d27bb7abd1d5b01b1640207528a5c851", + "kappa": "51110230636731/31250000000000000" + }, + "prior_work": { + "710": "d97c8d20a8b885271a24c5a4e8446ac7f5697d5c", + "688": "bb05c40c3e6319aa8c131b06a105e3648ac6c95b", + "742": "6e7a5d271a123886dc7b54ca3180d0b9f9beda5a", + "748": "0ccc0b425d2b9667108d3a0918a5cfa0aa7a5861", + "681": "e536f6fc8aad65adef8ac4682d13625598a5c3f9", + "753": "2b30b63789f6d9948233fc67d9d79bca6b185c5b" + }, + "files_sha256": { + "research/e8-bit-r420/data/bitE8mut-r420.json.gz": "9721a3819efd68307f66f00d84a952eb28eb7c3ad2ce79653ce295c98a764784", + "research/e8-bit-carrier-skeleton/code/bit/export_records.py": "8a5999601f917dbb492bb9ae9a344611f18cc7cedc53dc3c76496a369e530eb3", + "research/e8-bit-r420/code/xcheck.py": "5737d18a7826fd51e131035f2d7bebba2e2868af91dd7672a5f11208b036d424", + "research/e8-bit-r420/EXPECTED.json": "06eccee9f6b77e140833df83407e7996dc948c17d49b0779ab171fbe463fd28d", + "research/e8-bit-r420/README.md": "9807be57c6adf26b30e4f54e2f8160075bbc05091f1a6d157e43d2a4620c1c9f", + "research/e8-bit-r420/NOTICE.md": "12ba6e0845f222e9940b00f6c60d261db104246a8d3143da267682973479f811", + "certificates/selected-result.json": "b3bf402f31a69bde0629936a9b569bed48281568d7b16d5fba120b5311ea1f53", + "docs/research/community-k492-review.md": "3b731d30e80010b15408a289b0b32192700885474c8b36d48ee3320a7a8c5c47", + "research/e8-bit-carrier-skeleton/code/bit/regression/stage_cohort.py": "6c288f6f234b528c1a7c0a4adfb724e91e0fe6b18c8dffad96af3f973de1829a", + "research/e8-bit-carrier-skeleton/code/bit/checkers/legality_h.cpp": "6c1ef2b24e57781d6951c172a1024fc4300e6fd392c9d6672079a7806ab663b3", + "research/e8-bit-carrier-skeleton/code/bit/checkers/columns_k.cpp": "1c344d18fcd494eeca93e259f10cafae7705780e6592f6dcb35b34752dab9bc2", + "research/e8-bit-carrier-skeleton/code/bit/checkers/json.hpp": "aaf127c04cb31c406e5b04a63f1ae89369fccde6d8fa7cdda1ed4f32dfc5de63", + "research/e8-bit-carrier-skeleton/portable-include/bits/stdc++.h": "420094be2af295eed03a983dd66debbbe9cfb78d8252859f4498a615a0074b99" + } +} diff --git a/research/r420-four-wire-cleanup/VALIDATION.md b/research/r420-four-wire-cleanup/VALIDATION.md new file mode 100644 index 0000000000..6e18082047 --- /dev/null +++ b/research/r420-four-wire-cleanup/VALIDATION.md @@ -0,0 +1,51 @@ +# Validation receipt + +Base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +Assignment seed: **17**. Validation date: **2026-10-13 UTC**. + +The default command passed on CPython **3.14.7** and **3.11.14**. The complete +deterministic receipt is [EXPECTED.json](EXPECTED.json), including the eight +rejection controls. Ruff and `git diff --check` passed. +`make selected-record-check` passed with the original selected κ and inventory. + +The supplementary native command passed on **macOS 26.5.1 arm64**, +**Apple Clang 21.0.0** (`clang-2100.1.1.101`), and **Boost 1.74**. It freshly +compiled the unchanged legality and `columns_k.cpp` checkers for KPAIRS 2, 4, +and 5. Both words passed 900, 1,380 and 1,620 formal columns; all **96** +bridge-omission controls rejected. Every deterministic receipt field, after +removing only output paths and elapsed seconds, is retained in +[NATIVE-EXPECTED.json](NATIVE-EXPECTED.json). + +Both Python and native commands also passed from a relocated minimal tree +containing only this package and its 13 pinned input files, with an unrelated +working directory. Separate artifact controls rejected a one-byte source +corruption and a certificate with an omitted interval. Reusing an existing +output directory was rejected without overwriting its contents. + +Tested native command, with headers extracted outside the repository: + +```sh +python3.11 -I -B research/r420-four-wire-cleanup/native.py /tmp/r420-native-validation \ + --boost-include /tmp/bit-s17-boost/usr/include \ + --cxxflags=-D_LIBCPP_ENABLE_CXX17_REMOVED_UNARY_BINARY_FUNCTION +``` + +The last flag enables libc++'s compatibility declarations used by this older +Boost release; it changes no checker source or mathematical check. Newer Boost +or a different standard library may not require it. The headers came from +[Debian's libboost1.74-dev package](https://deb.debian.org/debian/pool/main/b/boost1.74/libboost1.74-dev_1.74.0+ds1-21_amd64.deb), +SHA-256 `ba14fe04d7f138f874bd3ab3a20c4fd1e9f654e271449b8f3e48d20f942dbb93`. +Only headers were extracted; no package was installed. An initial compile +without the compatibility flag failed on the removed `std::unary_function` +declaration, before any mathematical replay. + +No global hosted program or outer assembly was regenerated. The selected +construction is untouched, so its repository-wide cold replay, unrelated +research suites, remote CI and Lean were not run. The native check is a finite +multistage scalar/frame replay, not the unresolved all-size compilation theorem. + +Final overlap inspection found no pinned coordination issue. The open queue +had 569 PRs through #750; immediately before submission, new arrivals through +#753 were inspected as well. #748/#753 and the updated #681 concern different +circuit mechanisms and are explicitly credited in the README. Main remained +at the recorded base. The local claim carries the final handoff link. diff --git a/research/r420-four-wire-cleanup/independent.py b/research/r420-four-wire-cleanup/independent.py new file mode 100644 index 0000000000..6acaaca28c --- /dev/null +++ b/research/r420-four-wire-cleanup/independent.py @@ -0,0 +1,229 @@ +"""Independent finite CNOT distances, window maps and interval scheduling. + +Prepared for Jeffrey Cox (@namredips) with substantial OpenAI Codex assistance. +Apache-2.0. No producer imports: this implementation propagates output columns +and complete Boolean inputs rather than the producer's packed matrix rows. +""" + +from bisect import bisect_right +from collections import Counter, deque +from functools import lru_cache +from itertools import product + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def _gates(gates): + normalized = [] + for gate in gates: + require(len(gate) == 2, "CNOT must have exactly two operands") + target, source = gate + require(type(target) is int and type(source) is int + and target >= 0 and source >= 0 and target != source, + "CNOT operands must be distinct nonnegative registers") + normalized.append((target, source)) + return normalized + + +def _step(columns, target, source): + return tuple(value ^ (((value >> source) & 1) << target) for value in columns) + + +@lru_cache(maxsize=3) +def _invertible_columns(width): + """Enumerate all binary matrices; recognize independent columns by span.""" + states = set() + for columns in product(range(1 << width), repeat=width): + span = {0} + for column in columns: + if column in span: + break + span |= {value ^ column for value in span} + else: + states.add(columns) + return frozenset(states) + + +@lru_cache(maxsize=3) +def _column_distances(width): + """Fresh unweighted BFS, with CNOT acting on each output column.""" + identity = tuple(1 << i for i in range(width)) + distances, pending = {identity: 0}, deque([identity]) + while pending: + columns = pending.popleft() + for target in range(width): + for source in range(width): + if target == source: + continue + child = _step(columns, target, source) + if child not in distances: + distances[child] = distances[columns] + 1 + pending.append(child) + require(set(distances) == _invertible_columns(width), + "independent column BFS missed an invertible matrix") + return distances + + +def verify_distances(tables: dict[int, dict[tuple[int, ...], int]]) -> dict: + """Check row-tuple certificates by converting them to output columns. + + Edge Lipschitz inequalities give lower bounds on every CNOT path. A + descending neighbor at every nonidentity state gives matching upper bounds. + Completeness is checked against independent exhaustive matrix enumeration. + """ + require(set(tables) == {2, 3, 4}, "distance certificate must cover widths 2, 3, 4") + evidence = {} + for width, rows_table in sorted(tables.items()): + columns_table = {} + for rows, distance in rows_table.items(): + require(len(rows) == width and all(type(row) is int and 0 <= row < 1 << width + for row in rows), + "malformed distance matrix") + require(type(distance) is int and distance >= 0, "invalid distance label") + columns = tuple(sum(((rows[i] >> j) & 1) << i for i in range(width)) + for j in range(width)) + columns_table[columns] = distance + require(set(columns_table) == _invertible_columns(width), + "distance state set differs from all invertible matrices") + identity = tuple(1 << i for i in range(width)) + require(columns_table[identity] == 0, "identity distance must be zero") + edges = 0 + for columns, distance in columns_table.items(): + require((distance == 0) == (columns == identity), + "nonidentity has zero distance") + descent = columns == identity + for target in range(width): + for source in range(width): + if target == source: + continue + child_distance = columns_table[_step(columns, target, source)] + require(abs(distance - child_distance) <= 1, + "distance edge is not one-Lipschitz") + descent |= child_distance == distance - 1 + edges += 1 + require(descent, "positive distance has no descending neighbor") + evidence[str(width)] = { + "states": len(columns_table), "directed_edges_checked": edges, + "diameter": max(columns_table.values()), + "layers": {str(d): count for d, count in sorted(Counter(columns_table.values()).items())}, + } + return evidence + + +def _run_input(gates, registers, value): + state = {register: (value >> i) & 1 for i, register in enumerate(registers)} + for target, source in gates: + state[target] ^= state[source] + return sum(state[register] << i for i, register in enumerate(registers)) + + +def _integer_column(gates, registers, basis): + """Propagate one basis input using ordinary nonnegative integer addition.""" + state = {register: int(i == basis) for i, register in enumerate(registers)} + for target, source in gates: + state[target] += state[source] + return tuple(state[register] for register in registers) + + +def verify_windows(original: list[tuple[int, int]], windows: list[dict]) -> dict: + """Check maps, shortest costs and positive envelopes, with no extra registers.""" + original = _gates(original) + previous_stop = inputs = old_count = new_count = 0 + positive_columns = 0 + for window in windows: + start, stop = window["start"], window["stop"] + require(type(start) is int and type(stop) is int + and 0 <= start < stop <= len(original), "window interval is out of range") + require(start >= previous_stop, "windows overlap or are out of order") + previous_stop = stop + old, new = _gates(window["old"]), _gates(window["new"]) + require(old == original[start:stop], "window old gates differ from original slice") + registers = sorted({register for gate in old for register in gate}) + require(window["registers"] == registers and 2 <= len(registers) <= 4, + "window register declaration is incorrect") + require(all(register in registers for gate in new for register in gate), + "replacement uses an outside register") + require(window["saving"] == len(old) - len(new) > 0, + "replacement saving is incorrect or not positive") + columns = [] + for value in range(1 << len(registers)): + expected = _run_input(old, registers, value) + actual = _run_input(new, registers, value) + require(actual == expected, "replacement truth table differs from original") + if value and value & (value - 1) == 0: + columns.append(expected) + inputs += 1 + require(len(new) == _column_distances(len(registers))[tuple(columns)], + "replacement is not shortest in the stated CNOT class") + for old_order, new_order in ((old, new), (old[::-1], new[::-1])): + for basis in range(len(registers)): + before = _integer_column(old_order, registers, basis) + after = _integer_column(new_order, registers, basis) + require(all(a <= b for a, b in zip(after, before)), + "replacement increases a nonnegative transfer column") + positive_columns += 1 + old_count += len(old) + new_count += len(new) + return { + "windows_checked": len(windows), "boolean_inputs_checked": inputs, + "selected_original_gates": old_count, "selected_replacement_gates": new_count, + "saving": old_count - new_count, "all_replacements_shortest": True, + "nonnegative_transfer_columns_checked": positive_columns, + "entrywise_dominance_forward_and_reverse": True, + } + + +def census(original: list[tuple[int, int]], max_wires: int = 4) -> dict: + """Exhaust original contiguous windows and independently schedule their gains. + + Register-union size is monotone, so the first oversized interval ends a + start-index scan. Weighted interval scheduling is by increasing finish time. + This optimum concerns disjoint windows in the original word only. + """ + require(type(max_wires) is int and 2 <= max_wires <= 4, "unsupported window width") + original = _gates(original) + tables = {width: _column_distances(width) for width in range(2, max_wires + 1)} + counts, shortenable, longest, gaps = Counter(), Counter(), Counter(), Counter() + candidates = [] + for start in range(len(original)): + positions, columns = {}, [] + for stop in range(start, len(original)): + target, source = original[stop] + for register in (target, source): + if register not in positions: + positions[register] = len(positions) + columns.append(1 << (len(positions) - 1)) + width = len(positions) + if width > max_wires: + break + columns = list(_step(columns, positions[target], positions[source])) + length = stop - start + 1 + distance = tables[width][tuple(columns)] + require(distance <= length, "distance exceeds an existing window circuit") + gap = length - distance + counts[width] += 1 + longest[width] = max(longest[width], length) + gaps[gap] += 1 + if gap: + shortenable[width] += 1 + candidates.append((stop + 1, start, gap)) + candidates.sort() + finishes = [stop for stop, _, _ in candidates] + best = [0] + for stop, start, gain in candidates: + predecessor_count = bisect_right(finishes, start) + require(predecessor_count < len(best), "interval predecessor is not earlier") + best.append(max(best[-1], best[predecessor_count] + gain)) + return { + "binary_gates": len(original), "windows_checked": sum(counts.values()), + "shortenable_windows": len(candidates), "maximum_single_window_saving": max(gaps, default=0), + "optimal_disjoint_original_window_saving": best[-1], + "by_width": {str(width): {"windows": counts[width], "shortenable": shortenable[width], + "maximum_length": longest[width]} + for width in range(2, max_wires + 1)}, + "saving_histogram": {str(gap): count for gap, count in sorted(gaps.items())}, + "scope": "All original contiguous windows with at most the stated wires; no extra registers, free permutations or iterative rewrites.", + } diff --git a/research/r420-four-wire-cleanup/native.py b/research/r420-four-wire-cleanup/native.py new file mode 100644 index 0000000000..2e7c4d33d2 --- /dev/null +++ b/research/r420-four-wire-cleanup/native.py @@ -0,0 +1,83 @@ +"""Supplementary unchanged C++ legality and 5/9/11-stage column replays. + +Jeffrey Cox, with substantial OpenAI assistance; Apache-2.0. +Requires Python 3.11+, a C++17 compiler and Boost headers. +""" + +import argparse +import json +import os +import shlex +import subprocess +import sys +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parent.parent +SKELETON = ROOT / "research/e8-bit-carrier-skeleton" + + +def command(arguments, log: Path) -> None: + with log.open("w") as stream: + subprocess.run([str(a) for a in arguments], stdout=stream, stderr=stream, check=True) + + +def main() -> None: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("out", type=Path, help="new output directory") + parser.add_argument("--boost-include", type=Path, default=Path("/usr/include")) + parser.add_argument("--cxx", default=os.environ.get("CXX", "c++")) + parser.add_argument("--cxxflags", default=os.environ.get("CXXFLAGS", "")) + args = parser.parse_args() + out = args.out.resolve() + subprocess.run([sys.executable, "-I", "-B", str(HERE / "verify.py"), "--out", str(out)], check=True) + common = [*shlex.split(args.cxx), "-O2", "-std=c++17", *shlex.split(args.cxxflags), + "-DHDIM=8", "-DNCOPY=9", f"-I{SKELETON / 'portable-include'}", + f"-I{SKELETON / 'code/bit/checkers'}", f"-I{args.boost_include.resolve()}"] + binaries = out / "bin" + binaries.mkdir() + command([*common, "-o", binaries / "legality", SKELETON / "code/bit/checkers/legality_h.cpp"], + binaries / "legality.compile.log") + for pairs in (2, 4, 5): + command([*common, "-DVPORTS=120", "-DRHELP=420", f"-DKPAIRS={pairs}", + "-o", binaries / f"columns{pairs}", SKELETON / "code/bit/checkers/columns_k.cpp"], + binaries / f"columns{pairs}.compile.log") + + reports = {} + python_receipt = json.loads((out / "REPORT.json").read_text()) + for variant in ("original", "rewritten"): + folder = out / variant + command([sys.executable, "-I", "-B", SKELETON / "code/bit/regression/stage_cohort.py", + folder / "records", folder / "records", folder / "cin", folder / "cout"], + folder / "stage.log") + command([binaries / "legality", folder / "cin", folder / "cout", folder / "legality.json"], + folder / "legality.log") + legality = json.loads((folder / "legality.json").read_text()) + expected = python_receipt[variant] + if (legality["common_frame_ADDs"] != expected["adds"] or + legality["rank_mass"] != expected["rank_mass"] or + legality["copies"] != 9 or legality["erasures"] != 9): + raise ValueError("native legality disagrees with independent Python replay") + columns = {} + for pairs in (2, 4, 5): + command([binaries / f"columns{pairs}", folder / "cout/COHORT249-RECORDS.bin", + folder / f"columns{pairs}.json"], folder / f"columns{pairs}.log") + receipt = json.loads((folder / f"columns{pairs}.json").read_text()) + if (receipt["local_scalar_additions"] != expected["adds"] or + receipt["formal_columns_checked"] != 2 * pairs * 120 + 420 or + receipt["payload_prefix_upper"] != expected["payload_upper"] or + not all(control["rejected"] for control in receipt["negative_controls"])): + raise ValueError("native column checker disagrees with expected circuit") + receipt.pop("local_scalar_stream") + receipt.pop("seconds") + columns[str(2 * pairs + 1)] = receipt + reports[variant] = {"legality": legality, "columns": columns} + (out / "NATIVE-REPORT.json").write_text(json.dumps(reports, indent=2) + "\n") + expected = json.loads((HERE / "NATIVE-EXPECTED.json").read_text()) + if reports != expected: + raise ValueError("native receipts differ from NATIVE-EXPECTED.json") + print("PASS_NATIVE_R420_FOUR_WIRE: legality and 900/1380/1620 columns for both words; all bridge controls rejected") + + +if __name__ == "__main__": + main() diff --git a/research/r420-four-wire-cleanup/verify.py b/research/r420-four-wire-cleanup/verify.py new file mode 100644 index 0000000000..3b6d0954c1 --- /dev/null +++ b/research/r420-four-wire-cleanup/verify.py @@ -0,0 +1,358 @@ +"""Exhaust and verify at-most-four-wire rewrites of the pinned R420 cleanup. + +Jeffrey Cox, with substantial OpenAI assistance; Apache-2.0. +Run from any directory with Python 3.11+: python3 -I -B /path/to/verify.py +""" + +from __future__ import annotations + +import argparse +import copy +import gzip +import hashlib +import importlib.util +import json +import struct +import subprocess +import sys +import tempfile +from collections import Counter, deque +from itertools import permutations +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parent.parent +Gate = tuple[int, int] +Matrix = tuple[int, ...] + + +def need(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def canonical(value: object) -> bytes: + return json.dumps(value, sort_keys=True, separators=(",", ":")).encode() + + +def load_module(name: str, path: Path): + spec = importlib.util.spec_from_file_location(name, path) + need(spec is not None and spec.loader is not None, f"cannot import {path}") + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def load_source() -> tuple[dict, dict]: + pins = json.loads((HERE / "SOURCE.json").read_text()) + for relative, expected in pins["files_sha256"].items(): + actual = hashlib.sha256((ROOT / relative).read_bytes()).hexdigest() + need(actual == expected, f"source pin mismatch: {relative}") + word = json.loads(gzip.decompress((ROOT / pins["word"]).read_bytes())) + need(hashlib.sha256(canonical(word)).hexdigest() == pins["word_canonical_sha256"], + "word canonical hash mismatch") + need(word["v"] == 120 and word["R"] == 420 and word["h"] == 8, "wrong word") + need(all(f == 1 for f, _, _ in word["C"]), "cleanup is not all FULL") + return word, pins + + +def shortest_tables(): + tables, parents = {}, {} + for width in (2, 3, 4): + identity = tuple(1 << i for i in range(width)) + distance, parent = {identity: 0}, {} + queue = deque([identity]) + generators = list(permutations(range(width), 2)) + while queue: + matrix = queue.popleft() + for target, source in generators: + successor = list(matrix) + successor[target] ^= successor[source] + successor = tuple(successor) + if successor not in distance: + distance[successor] = distance[matrix] + 1 + parent[successor] = matrix, (target, source) + queue.append(successor) + tables[width], parents[width] = distance, parent + return tables, parents + + +def search(gates: list[Gate], tables: dict, parents: dict) -> dict: + census, candidates = Counter(), [] + for start in range(len(gates)): + registers: set[int] = set() + for last in range(start, len(gates)): + registers.update(gates[last]) + if len(registers) > 4: + break # The union only grows: all later windows are out of scope. + labels = sorted(registers) + index = {label: i for i, label in enumerate(labels)} + matrix = [1 << i for i in range(len(labels))] + for target, source in gates[start:last + 1]: + matrix[index[target]] ^= matrix[index[source]] + endpoint = tuple(matrix) + saving = last + 1 - start - tables[len(labels)][endpoint] + census[len(labels), saving] += 1 + if saving: + path = [] + while endpoint in parents[len(labels)]: + endpoint, gate = parents[len(labels)][endpoint] + path.append([labels[i] for i in gate]) + candidates.append({"start": start, "stop": last + 1, "registers": labels, + "old": [list(g) for g in gates[start:last + 1]], + "new": list(reversed(path)), "saving": saving}) + + # Maximum saving among disjoint ORIGINAL intervals. Equal-score ties skip + # the current position; otherwise the first (shortest) stop wins. + by_start: dict[int, list[dict]] = {} + for candidate in candidates: + by_start.setdefault(candidate["start"], []).append(candidate) + best = [0] * (len(gates) + 1) + choice = {} + for start in reversed(range(len(gates))): + best[start] = best[start + 1] + for candidate in by_start.get(start, []): + score = candidate["saving"] + best[candidate["stop"]] + if score > best[start]: + best[start], choice[start] = score, candidate + windows, position = [], 0 + while position < len(gates): + if position in choice: + windows.append(choice[position]) + position = choice[position]["stop"] + else: + position += 1 + return {"width": 4, "original_xors": len(gates), + "windows_examined": sum(census.values()), "shorter_windows": len(candidates), + "census": [{"wires": w, "saving": s, "count": n} for (w, s), n in sorted(census.items())], + "distance_layers": {str(w): {str(d): n for d, n in sorted(Counter(t.values()).items())} + for w, t in tables.items()}, + "saving": best[0], "windows": windows} + + +def replace_cleanup(word: dict, windows: list[dict]) -> dict: + gates = [(target, source) for _, target, sources in word["C"] for source in sources] + replacement, position = [], 0 + for window in windows: + replacement.extend(gates[position:window["start"]]) + replacement.extend(window["new"]) + position = window["stop"] + replacement.extend(gates[position:]) + result = copy.deepcopy(word) + result["C"] = [[1, target, [source]] for target, source in replacement] + return result + + +def prefix(records: list[tuple], size: int, reverse: bool) -> int: + values = [1] * (size + 1) + peak, active = 1, None + stream = reversed(records) if reverse else iter(records) + for kind, a, b, coefficient, _, _ in stream: + if kind == 0: + continue + if reverse and kind in (2, 3): + kind = 5 - kind + if kind == 1: + values[a] += abs(coefficient) * values[b] + peak = max(peak, values[a]) + elif kind == 2: + need(active is None, "nested prefix copy") + values[b], active = values[a], (a, b) + else: + need(active == (a, b), "prefix copy mismatch") + values[b], active = 0, None + need(active is None, "unclosed prefix copy") + return peak + + +def audit_records(records: list[tuple], model) -> dict: + """Replay actual exporter bytes, including every MOVE and COPY/ERASE.""" + word, size = model.w, model.n + current = list(word["start"]) + [model.ZERO] + values = [1 << r for r in range(size)] + [0] + paths = [[] for _ in range(size)] + histogram, operations, phases = Counter(), Counter(), Counter() + copies, active = [], None + for kind, a, b, c, f, z in records: + need(0 <= a <= size, "bad native destination") + operations[kind] += 1 + if kind == 0: + need(a < size and current[a] == b and z == 0, "wrong MOVE source frame or reserved field") + need(model.nested(b, c) and model.fdim[c] - model.fdim[b] == f and f > 0, + "non-nested or mispriced MOVE") + current[a] = c + paths[a].append((b, c, f)) + histogram[f] += 1 + elif kind == 1: + need(0 <= b <= size and a != b and c == 1, "bad native ADD") + need(current[a] == current[b] == f, "ADD operands not in a common frame") + need(a < size and (b < size or active is not None), "inactive temporary ADD") + need(active is None or a != active[0], "copied source mutated") + values[a] ^= values[b] + phases[z] += 1 + elif kind == 2: + need(active is None and b == size and current[a] == c and f == model.ZERO, + "invalid COPY") + need(z == model.fdim[c], "mispriced COPY") + values[b], current[b], active = values[a], f, (a, b, c, f) + histogram[z] += 1 + copies.append((kind, a, b, c, f, z)) + elif kind == 3: + need(active == (a, b, c, f) and current[a] == c and current[b] == f and z == 0, + "invalid ERASE") + need(values[b] == values[a], "copied centre changed before ERASE") + values[b], active = 0, None + copies.append((kind, a, b, c, f, z)) + else: + raise ValueError("unknown native operation") + need(active is None and values[size] == 0, "unclosed native copy") + need(current[:size] == word["final"], "wrong native final frames") + expected = [1 << r for r in range(size)] + for source in range(word["v"]): + expected[word["v"] + source] ^= 1 << source + need(values[:size] == expected, "native arbitrary-input identity failed") + forward, backward = prefix(records, size, False), prefix(records, size, True) + payload = 64 * forward**3 * backward**2 + return {"records": len(records), "adds": operations[1], "moves": operations[0], + "copies": operations[2], "erasures": operations[3], + "paid_histogram": {str(k): v for k, v in sorted(histogram.items())}, + "rank_mass": sum(k * v for k, v in histogram.items()), + "phase_adds": {str(k): v for k, v in sorted(phases.items())}, + "forward_prefix": forward, "reverse_prefix": backward, + "payload_upper": str(payload), "payload_bits": payload.bit_length(), + "paths": paths, "copy_records": copies} + + +def export_and_audit(word: dict, model, pins: dict, output: Path) -> tuple[dict, list]: + output.mkdir() + path = output / "word.json" + path.write_bytes(canonical(word) + b"\n") + result = subprocess.run([sys.executable, "-I", "-B", str(ROOT / pins["exporter"]), + str(path), str(output / "records")], + check=True, capture_output=True, text=True) + need("exported" in result.stdout, "native exporter did not report completion") + data = (output / "records/249-records.bin").read_bytes() + need(len(data) % 24 == 0, "truncated native records") + records = list(struct.iter_unpack("<6i", data)) + report = audit_records(records, model) + return report, records + + +def expect_rejection(label: str, action) -> str: + try: + action() + except (ValueError, AssertionError): + return label + raise ValueError(f"negative control was accepted: {label}") + + +def run(output: Path) -> dict: + word, pins = load_source() + gates = [(target, source) for _, target, sources in word["C"] for source in sources] + tables, parents = shortest_tables() + computed = search(gates, tables, parents) + certificate = json.loads((HERE / "CERTIFICATE.json").read_text()) + need(computed == certificate, "certificate differs from exhaustive deterministic search") + independent = load_module("r420_independent", HERE / "independent.py") + distance_evidence = independent.verify_distances(tables) + window_evidence = independent.verify_windows(gates, certificate["windows"]) + independent_census = independent.census(gates) + need(independent_census["windows_checked"] == certificate["windows_examined"], "independent window count") + need(independent_census["shortenable_windows"] == certificate["shorter_windows"], "independent shorter-window count") + need(independent_census["optimal_disjoint_original_window_saving"] == certificate["saving"], "independent packing optimum") + gaps, widths, shorter = Counter(), Counter(), Counter() + for entry in certificate["census"]: + gaps[str(entry["saving"])] += entry["count"] + widths[str(entry["wires"])] += entry["count"] + if entry["saving"]: + shorter[str(entry["wires"])] += entry["count"] + need(dict(gaps) == independent_census["saving_histogram"], "independent gap census") + for width, evidence in independent_census["by_width"].items(): + need(widths[width] == evidence["windows"] and shorter[width] == evidence["shortenable"], + "independent census by width") + changed = replace_cleanup(word, certificate["windows"]) + need(all(word[k] == changed[k] for k in word if k != "C"), "change outside C") + + xcheck = load_module("r420_xcheck", ROOT / pins["xcheck"]) + original_model, changed_model = xcheck.Word(word), xcheck.Word(changed) + labels = original_model.labels() # All label/frame data is pinned and unchanged. + original_model.full() + changed_model.full() + original_h, original_c, _ = original_model.interface() + changed_h, changed_c, _ = changed_model.interface() + need(all(original_h.values()) and all(original_c.values()), "baseline interface") + literal = "H4_C_literal_reverse_at_full" + need(not changed_h[literal], "literal-reversal guard unexpectedly accepts rewrite") + need(all(v for k, v in changed_h.items() if k != literal) and all(changed_c.values()), + "semantic H4-prime interface failed") + before, original_records = export_and_audit(word, original_model, pins, output / "original") + after, changed_records = export_and_audit(changed, changed_model, pins, output / "rewritten") + for key in ("paths", "copy_records", "paid_histogram", "rank_mass", "moves", "copies", "erasures"): + need(before[key] == after[key], f"changed paid work: {key}") + need(before["adds"] - after["adds"] == certificate["saving"], "incorrect complete XOR saving") + need(after["forward_prefix"] <= before["forward_prefix"] and + after["reverse_prefix"] <= before["reverse_prefix"], "larger native prefix envelope") + need(int(after["payload_upper"]) < 1 << 104, "native payload exceeds inherited ceiling") + + controls = [] + first = certificate["windows"][0] + broken = copy.deepcopy(certificate["windows"]) + broken[0]["new"].pop() + broken[0]["saving"] += 1 # Keep the cost declaration honest; the map must fail. + controls.append(expect_rejection("dropped replacement XOR", lambda: independent.verify_windows(gates, broken))) + swapped = copy.deepcopy(certificate["windows"]) + swapped[0]["new"][0].reverse() + controls.append(expect_rejection("reversed source and destination", lambda: independent.verify_windows(gates, swapped))) + controls.append(expect_rejection("overlapping windows", lambda: independent.verify_windows(gates, [first, first]))) + forged = {k: dict(v) for k, v in tables.items()} + nonidentity = next(m for m, d in forged[2].items() if d == 1) + forged[2][nonidentity] += 2 # Still positive, but inconsistent with a one-gate edge. + controls.append(expect_rejection("forged distance potential", lambda: independent.verify_distances(forged))) + incomplete = {k: dict(v) for k, v in tables.items()} + del incomplete[2][nonidentity] + controls.append(expect_rejection("missing GL state", lambda: independent.verify_distances(incomplete))) + outside = copy.deepcopy(certificate["windows"]) + outside[0]["new"][0][0] = original_model.n + controls.append(expect_rejection("undeclared ancillary register", lambda: independent.verify_windows(gates, outside))) + mutated_records = list(changed_records) + move_index = next(i for i, r in enumerate(mutated_records) if r[0] == 0) + record = list(mutated_records[move_index]) + record[4] -= 1 + mutated_records[move_index] = tuple(record) + controls.append(expect_rejection("unpaid frame rank", lambda: audit_records(mutated_records, changed_model))) + controls.append(expect_rejection("missing cleanup", lambda: audit_records( + [r for r in original_records if not (r[0] == 1 and r[5] == 5)], original_model))) + for report in (before, after): + report.pop("paths") + report.pop("copy_records") + report = {"status": "PASS_R420_FOUR_WIRE_CLEANUP", "base_commit": pins["base_commit"], + "seed": 17, "saving": certificate["saving"], "selected_windows": len(certificate["windows"]), + "windows_examined": certificate["windows_examined"], + "independent_distances": distance_evidence, "independent_windows": window_evidence, + "independent_census": independent_census, "labels": labels, + "original": before, "rewritten": after, "negative_controls": controls, + "rewritten_word_canonical_sha256": hashlib.sha256(canonical(changed)).hexdigest(), + "literal_H4": False, "semantic_H4_prime": True, "all_input_columns": original_model.n} + return report + + +def main() -> None: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--out", type=Path, help="retain generated word, native records and report in a NEW directory") + arguments = parser.parse_args() + if arguments.out is None: + with tempfile.TemporaryDirectory(prefix="r420-four-wire-") as temporary: + report = run(Path(temporary)) + else: + arguments.out.mkdir(parents=True, exist_ok=False) + report = run(arguments.out) + (arguments.out / "REPORT.json").write_text(json.dumps(report, indent=2) + "\n") + expected = json.loads((HERE / "EXPECTED.json").read_text()) + need(report == expected, "verification receipt differs from EXPECTED.json") + print(f"{report['status']}: {report['selected_windows']} windows, {report['saving']} XORs saved; " + f"{report['original']['adds']} -> {report['rewritten']['adds']} native ADDs; " + f"{len(report['negative_controls'])} negative controls rejected") + + +if __name__ == "__main__": + main()