PrimeCert windowed powModK: same-kernel replay and complete certificate builds

README.md

Windowed PrimeCert powModK replay (Lean 4.33.0)

Put PowModBench.lean at PrimeCertTest/PowModBench.lean on the windowed-power PR branch, then run:

POWMOD_CASES=/absolute/path/cases.json POWMOD_SAMPLES=/tmp/powmod.csv POWMOD_BLOCKS=4 lake build PrimeCertTest.PowModBench

The baseline is the exact previous wrapper around the retained powModK.aux, checked with the same kernel, imports, numerical inputs, and equality application as the new wrapper. Each timed sample uses a fresh Kernel.check; input construction and independent expected-value calculation are outside the timer. Both implementations must reject wrong-result controls at 255 and 521 bits. Four adjacent AB/BA blocks. Native powMod is unchanged by this PR.

The dispatch thresholds are inherited from Lean #15167, whose tuning evidence is attached there. This artifact compares that complete policy with the former binary implementation on Lean 4.33.0; it does not retune individual window widths on this toolchain. The full-base fallback is retained from that policy, not justified by the policy-versus-baseline comparison alone.

Median milliseconds (small base 2; full base floor(modulus/3); exponent modulus−1):

Input	Previous binary	Window policy	Ratio
255-small	1.795	0.520	3.45×
255-full	1.733	0.591	2.93×
521-small	3.727	1.231	3.03×
521-full	3.666	1.621	2.26×
2048-small	19.309	9.693	1.99×
2048-full	18.657	15.633	1.19×
8192-small	647.944	153.114	4.23×
8192-full	249.363	246.830	1.01×
16384-small	99007.895	697.826	141.88×
16384-full	55469.559	56039.591	0.99×

samples.csv contains every completed main-run sample; record-final.json records affinity, host load and command output. The large full-base cases use the retained binary fallback. These absolute times are observations on a shared host, not budgets or asymptotic claims.

certificate-builds.json contains all eight adjacent full Curve25519 certificate builds, including the first baseline build which rebuilt a dependency. Medians: 1.731 s previous, 1.621 s windowed. This end-to-end build cost includes imports and elaboration; it does not show the full ratio of the isolated arithmetic check.

Earlier harness runs are retained separately: record.json records a missing-meta-import error before any timing; invalid-unfolded-baseline-samples.csv used an inlined/precomputed baseline expression instead of the original wrapper and is unsuitable for the comparison; large-negative-control-run-samples.csv contains completed checks before stopping a costly large wrong-result control. Corresponding records retain failure/termination status. The final harness uses exact wrappers and small wrong-result controls.

cases.json

[{"id": "255-small", "b": 2, "e": 57896044618658097711785492504343953926634992332820282019728792003956564819948, "m": 57896044618658097711785492504343953926634992332820282019728792003956564819949, "expected": 1, "widths": []}, {"id": "255-full", "b": 19298681539552699237261830834781317975544997444273427339909597334652188273316, "e": 57896044618658097711785492504343953926634992332820282019728792003956564819948, "m": 57896044618658097711785492504343953926634992332820282019728792003956564819949, "expected": 1, "widths": []}, {"id": "521-small", "b": 2, "e": 6864797660130609714981900799081393217269435300143305409394463459185543183397656052122559640661454554977296311391480858037121987999716643812574028291115057132, "m": 6864797660130609714981900799081393217269435300143305409394463459185543183397656052122559640661454554977296311391480858037121987999716643812574028291115057133, "expected": 6341977776515012037371017477607177781901636667504072209909105029498795296673585651309770774959209789489726800616347760841250249349033043084705559209418792842, "widths": []}, {"id": "521-full", "b": 2288265886710203238327300266360464405756478433381101803131487819728514394465885350707519880220484851659098770463826952679040662666572214604191342763705019044, "e": 6864797660130609714981900799081393217269435300143305409394463459185543183397656052122559640661454554977296311391480858037121987999716643812574028291115057132, "m": 6864797660130609714981900799081393217269435300143305409394463459185543183397656052122559640661454554977296311391480858037121987999716643812574028291115057133, "expected": 4504973764097948787357213033572406812215607807736721270428748515998241795059443061646787470592148178529578846658936995391600407640406250007759674986836753031, "widths": []}, {"id": "2048-small", "b": 2, "e": 32317006071311007300714876688669951960444102669715484032130345427524655138867890893197201411522913463688717960921898019494119559150490921095088152386448283120630877367300996091750197750389652106796057638384067568276792218642619756161838094338476170470581645852036305042887575891541065808607552399123930385521914333389668342420684974786564569494856176035326322058077805659331026192708460314150258592864177116725943603718461857357598351152301645904403697613233287231227125684710820209725157101726931323469678542580656697935045997268352998638215525166389437335543602135433229604645318478604952148193555853611059596230636, "m": 32317006071311007300714876688669951960444102669715484032130345427524655138867890893197201411522913463688717960921898019494119559150490921095088152386448283120630877367300996091750197750389652106796057638384067568276792218642619756161838094338476170470581645852036305042887575891541065808607552399123930385521914333389668342420684974786564569494856176035326322058077805659331026192708460314150258592864177116725943603718461857357598351152301645904403697613233287231227125684710820209725157101726931323469678542580656697935045997268352998638215525166389437335543602135433229604645318478604952148193555853611059596230637, "expected": 25711037585651407290107336349901574251460544433433301874384737755304707966513172939792838060177141818162905181434785490783956291493871552849166953401681818560183213918501861060074958873135985996593586861307607811979719455664023253778083405321810030959847639726014492664415369096028092011797599731794116705144939106901914600787498269006699327529871967191586498008925266606409322416178219132672280645685231899191505067282396839404971863617951589893846005587112229507877024506309988011579642999828738343988626141549951557716659330170893996895600302928514099192848818872397778432258649900093486416200378916748174546942263, "widths": []}, {"id": "2048-full", "b": 10772335357103669100238292229556650653481367556571828010710115142508218379622630297732400470507637821229572653640632673164706519716830307031696050795482761040210292455766998697250065916796550702265352546128022522758930739547539918720612698112825390156860548617345435014295858630513688602869184133041310128507304777796556114140228324928854856498285392011775440686025935219777008730902820104716752864288059038908647867906153952452532783717433881968134565871077762410409041894903606736575052367242310441156559514193552232645015332422784332879405175055463145778514534045144409868215106159534984049397851951203686532076879, "e": 32317006071311007300714876688669951960444102669715484032130345427524655138867890893197201411522913463688717960921898019494119559150490921095088152386448283120630877367300996091750197750389652106796057638384067568276792218642619756161838094338476170470581645852036305042887575891541065808607552399123930385521914333389668342420684974786564569494856176035326322058077805659331026192708460314150258592864177116725943603718461857357598351152301645904403697613233287231227125684710820209725157101726931323469678542580656697935045997268352998638215525166389437335543602135433229604645318478604952148193555853611059596230636, "m": 32317006071311007300714876688669951960444102669715484032130345427524655138867890893197201411522913463688717960921898019494119559150490921095088152386448283120630877367300996091750197750389652106796057638384067568276792218642619756161838094338476170470581645852036305042887575891541065808607552399123930385521914333389668342420684974786564569494856176035326322058077805659331026192708460314150258592864177116725943603718461857357598351152301645904403697613233287231227125684710820209725157101726931323469678542580656697935045997268352998638215525166389437335543602135433229604645318478604952148193555853611059596230637, "expected": 10772335357103669100238292229556650653481367556571828010710115142508218379622630297732400470507637821229572653640632673164706519716830307031696050795482761040210292455766998697250065916796550702265352546128022522758930739547539918720612698112825390156860548617345435014295858630513688602869184133041310128507304777796556114140228324928854856498285392011775440686025935219777008730902820104716752864288059038908647867906153952452532783717433881968134565871077762410409041894903606736575052367242310441156559514193552232645015332422784332879405175055463145778514534045144409868215106159534984049397851951203686532076879, "widths": []}, {"id": "8192-small", "b": 2, "e": 1090748135619415929462984244733782862448264161996232692431832786189721331849119295216264234525201987223957291796157025273109870820177184063610979765077554799078906298842192989538609825228048205159696851613591638196771886542609324560121290553901886301017900252535799917200010079600026535836800905297805880952350501630195475653911005312364560014847426035293551245843928918752768696279344088055617515694349945406677825140814900616105920256438504578013326493565836047242407382442812245131517757519164899226365743722432277368075027627883045206501792761700945699168497257879683851737049996900961120515655050115561271491492515342105748966629547032786321505730828430221664970324396138635251626409516168005427623435996308921691446181187406395310665404885739434832877428167407495370993511868756359970390117021823616749458620969857006263612082706715408157066575137281027022310927564910276759160520878304632411049364568754920967322982459184763427383790272448438018526977764941072715611580434690827459339991961414242741410599117426060556483763756314527611362658628383368621157993638020878537675545336789915694234433955666315070087213535470255670312004130725495834508357439653828936077080978550578912967907352780054935621561090795845172954115972927479877527738560008204118558930004777748727761853813510493840581861598652211605960308356405941821189714037868726219481498727603653616298856174822413033485438785324024751419417183012281078209729303537372804574372095228703622776363945290869806258422355148507571039619387449629866808188769662815778153079393179093143648340761738581819563002994422790754955061288818308430079648693232179158765918035565216157115402992120276155607873107937477466841528362987708699450152031231862594203085693838944657061346236704234026821102958954951197087076546186622796294536451620756509351018906023773821539532776208676978589731966330308893304665169436185078350641568336944530051437491311298834367265238595404904273455928723949525227184617404367854754610474377019768025576605881038077270707717942221977090385438585844095492116099852538903974655703943973086090930596963360767529964938414598185705963754561497355827813623833288906309004288017321424808663962671333528009232758350873059614118723781422101460198615747386855096896089189180441339558524822867541113212638793675567650340362970031930023397828465318547238244232028015189689660418822976000815437610652254270163595650875433851147123214227266605403581781469090806576468950587661997186505665475715792876, "m": 1090748135619415929462984244733782862448264161996232692431832786189721331849119295216264234525201987223957291796157025273109870820177184063610979765077554799078906298842192989538609825228048205159696851613591638196771886542609324560121290553901886301017900252535799917200010079600026535836800905297805880952350501630195475653911005312364560014847426035293551245843928918752768696279344088055617515694349945406677825140814900616105920256438504578013326493565836047242407382442812245131517757519164899226365743722432277368075027627883045206501792761700945699168497257879683851737049996900961120515655050115561271491492515342105748966629547032786321505730828430221664970324396138635251626409516168005427623435996308921691446181187406395310665404885739434832877428167407495370993511868756359970390117021823616749458620969857006263612082706715408157066575137281027022310927564910276759160520878304632411049364568754920967322982459184763427383790272448438018526977764941072715611580434690827459339991961414242741410599117426060556483763756314527611362658628383368621157993638020878537675545336789915694234433955666315070087213535470255670312004130725495834508357439653828936077080978550578912967907352780054935621561090795845172954115972927479877527738560008204118558930004777748727761853813510493840581861598652211605960308356405941821189714037868726219481498727603653616298856174822413033485438785324024751419417183012281078209729303537372804574372095228703622776363945290869806258422355148507571039619387449629866808188769662815778153079393179093143648340761738581819563002994422790754955061288818308430079648693232179158765918035565216157115402992120276155607873107937477466841528362987708699450152031231862594203085693838944657061346236704234026821102958954951197087076546186622796294536451620756509351018906023773821539532776208676978589731966330308893304665169436185078350641568336944530051437491311298834367265238595404904273455928723949525227184617404367854754610474377019768025576605881038077270707717942221977090385438585844095492116099852538903974655703943973086090930596963360767529964938414598185705963754561497355827813623833288906309004288017321424808663962671333528009232758350873059614118723781422101460198615747386855096896089189180441339558524822867541113212638793675567650340362970031930023397828465318547238244232028015189689660418822976000815437610652254270163595650875433851147123214227266605403581781469090806576468950587661997186505665475715792877, "expected": 548042481143298373235690990840209098898548331767986460742092796091393922275142548130682518429032272947191063276892163921199586132662696033019473126714120958043270252615779448237301188629773791670403875888695413681352733731824776362672115840366126342227189426028195142202767049227532008599152987477449546152039910472973615934088969385312164141529454123238649392165609645365235986751356726071315093945819687490915489735937466181832495830932965506403791992612521822301270481108488589285727730897945636840657881696432441217204881204053473761569684279570110949114906894712065914327389451430695196274452372462125380208498638453997086811879444458348701601204474281837832454445136010851405177593647610528179573555502918991289707413988286227225088292727590193373749978438071324892383212522386303560046388041904786683418784175776521297141064740186519582693881333497848540535679956498033224013606035464389541251436825165496588385232057604022035143571517224406179939218573099342858969951438581849470593571879997846718107988119669000340005381317220426290836085643217437655209399131980663477783465611116328576581495514080428763437616024177371885112707569776134933815444776563677732562703990683450315034933651818189465029314342121513584533251485864213797448651582394458480580886950187181945277035574332758560053043853540740966043488359001545685520783993523309490035035909573061527043462362841879690056872125219356453305858956241048262792231726608561377063150003328594682531341238068400360145444211470484314531246424931154711508849412277724770021083774153232841628186065483798089214454117032637868694305569353989440227985383461731912096440739781499079469142691778261006670491271510785129729628961017356494294993515168232664726946405481088991901711231594868004705657427554554716227374563593518971459160639691743401752847716246109784914242969301562298320275579182936681368029182099472925168286170923438456407541595720660552396208727537194896497919068232813598111634619058286216982177766684847543333605681659952888022350569485409798333210206431442733130474686978925711908474911540017825408875681076051434441540858133021251122105925465084624500885600370137373707793987152233061066442527698763136131430037781420903256815212729262388085457618583365102555364037716247816988325370902917772949268027061037561572751450170657244537270233047954675527446813483876869831542156774705463796948564281536157610669442177225283411163851053922440645887951037308877555487255927072234570037291177236050094, "widths": []}, {"id": "8192-full", "b": 363582711873138643154328081577927620816088053998744230810610928729907110616373098405421411508400662407985763932052341757703290273392394687870326588359184933026302099614064329846203275076016068386565617204530546065590628847536441520040430184633962100339300084178599972400003359866675511945600301765935293650783500543398491884637001770788186671615808678431183748614642972917589565426448029351872505231449981802225941713604966872035306752146168192671108831188612015747469127480937415043839252506388299742121914574144092456025009209294348402167264253900315233056165752626561283912349998966987040171885016705187090497164171780701916322209849010928773835243609476740554990108132046211750542136505389335142541145332102973897148727062468798436888468295246478277625809389135831790331170622918786656796705673941205583152873656619002087870694235571802719022191712427009007436975854970092253053506959434877470349788189584973655774327486394921142461263424149479339508992588313690905203860144896942486446663987138080913803533039142020185494587918771509203787552876127789540385997879340292845891848445596638564744811318555438356695737845156751890104001376908498611502785813217942978692360326183526304322635784260018311873853696931948390984705324309159959175912853336068039519643334925916242587284604503497946860620532884070535320102785468647273729904679289575406493832909201217872099618724940804344495146261774674917139805727670760359403243101179124268191457365076234540925454648430289935419474118382835857013206462483209955602729589887605259384359797726364381216113587246193939854334331474263584985020429606102810026549564410726386255306011855072052371800997373425385202624369312492488947176120995902899816717343743954198067695231279648219020448745568078008940367652984983732362358848728874265431512150540252169783672968674591273846510925402892326196577322110102964434888389812061692783547189445648176683812497103766278122421746198468301424485309574649841742394872468122618251536824792339922675192201960346025756902572647407325696795146195281365164038699950846301324885234647991028696976865654453589176654979471532728568654584853832451942604541277762968769668096005773808269554654223777842669744252783624353204706241260474033820066205249128951698965363063060147113186174940955847037737546264558522550113454323343976674465942821772849079414744009338396563220139607658666938479203550751423387865216958477950382374404742422201801193927156363602192156316862553999062168555158571930959, "e": 1090748135619415929462984244733782862448264161996232692431832786189721331849119295216264234525201987223957291796157025273109870820177184063610979765077554799078906298842192989538609825228048205159696851613591638196771886542609324560121290553901886301017900252535799917200010079600026535836800905297805880952350501630195475653911005312364560014847426035293551245843928918752768696279344088055617515694349945406677825140814900616105920256438504578013326493565836047242407382442812245131517757519164899226365743722432277368075027627883045206501792761700945699168497257879683851737049996900961120515655050115561271491492515342105748966629547032786321505730828430221664970324396138635251626409516168005427623435996308921691446181187406395310665404885739434832877428167407495370993511868756359970390117021823616749458620969857006263612082706715408157066575137281027022310927564910276759160520878304632411049364568754920967322982459184763427383790272448438018526977764941072715611580434690827459339991961414242741410599117426060556483763756314527611362658628383368621157993638020878537675545336789915694234433955666315070087213535470255670312004130725495834508357439653828936077080978550578912967907352780054935621561090795845172954115972927479877527738560008204118558930004777748727761853813510493840581861598652211605960308356405941821189714037868726219481498727603653616298856174822413033485438785324024751419417183012281078209729303537372804574372095228703622776363945290869806258422355148507571039619387449629866808188769662815778153079393179093143648340761738581819563002994422790754955061288818308430079648693232179158765918035565216157115402992120276155607873107937477466841528362987708699450152031231862594203085693838944657061346236704234026821102958954951197087076546186622796294536451620756509351018906023773821539532776208676978589731966330308893304665169436185078350641568336944530051437491311298834367265238595404904273455928723949525227184617404367854754610474377019768025576605881038077270707717942221977090385438585844095492116099852538903974655703943973086090930596963360767529964938414598185705963754561497355827813623833288906309004288017321424808663962671333528009232758350873059614118723781422101460198615747386855096896089189180441339558524822867541113212638793675567650340362970031930023397828465318547238244232028015189689660418822976000815437610652254270163595650875433851147123214227266605403581781469090806576468950587661997186505665475715792876, "m": 1090748135619415929462984244733782862448264161996232692431832786189721331849119295216264234525201987223957291796157025273109870820177184063610979765077554799078906298842192989538609825228048205159696851613591638196771886542609324560121290553901886301017900252535799917200010079600026535836800905297805880952350501630195475653911005312364560014847426035293551245843928918752768696279344088055617515694349945406677825140814900616105920256438504578013326493565836047242407382442812245131517757519164899226365743722432277368075027627883045206501792761700945699168497257879683851737049996900961120515655050115561271491492515342105748966629547032786321505730828430221664970324396138635251626409516168005427623435996308921691446181187406395310665404885739434832877428167407495370993511868756359970390117021823616749458620969857006263612082706715408157066575137281027022310927564910276759160520878304632411049364568754920967322982459184763427383790272448438018526977764941072715611580434690827459339991961414242741410599117426060556483763756314527611362658628383368621157993638020878537675545336789915694234433955666315070087213535470255670312004130725495834508357439653828936077080978550578912967907352780054935621561090795845172954115972927479877527738560008204118558930004777748727761853813510493840581861598652211605960308356405941821189714037868726219481498727603653616298856174822413033485438785324024751419417183012281078209729303537372804574372095228703622776363945290869806258422355148507571039619387449629866808188769662815778153079393179093143648340761738581819563002994422790754955061288818308430079648693232179158765918035565216157115402992120276155607873107937477466841528362987708699450152031231862594203085693838944657061346236704234026821102958954951197087076546186622796294536451620756509351018906023773821539532776208676978589731966330308893304665169436185078350641568336944530051437491311298834367265238595404904273455928723949525227184617404367854754610474377019768025576605881038077270707717942221977090385438585844095492116099852538903974655703943973086090930596963360767529964938414598185705963754561497355827813623833288906309004288017321424808663962671333528009232758350873059614118723781422101460198615747386855096896089189180441339558524822867541113212638793675567650340362970031930023397828465318547238244232028015189689660418822976000815437610652254270163595650875433851147123214227266605403581781469090806576468950587661997186505665475715792877, "expected": 363582711873138643154328081577927620816088053998744230810610928729907110616373098405421411508400662407985763932052341757703290273392394687870326588359184933026302099614064329846203275076016068386565617204530546065590628847536441520040430184633962100339300084178599972400003359866675511945600301765935293650783500543398491884637001770788186671615808678431183748614642972917589565426448029351872505231449981802225941713604966872035306752146168192671108831188612015747469127480937415043839252506388299742121914574144092456025009209294348402167264253900315233056165752626561283912349998966987040171885016705187090497164171780701916322209849010928773835243609476740554990108132046211750542136505389335142541145332102973897148727062468798436888468295246478277625809389135831790331170622918786656796705673941205583152873656619002087870694235571802719022191712427009007436975854970092253053506959434877470349788189584973655774327486394921142461263424149479339508992588313690905203860144896942486446663987138080913803533039142020185494587918771509203787552876127789540385997879340292845891848445596638564744811318555438356695737845156751890104001376908498611502785813217942978692360326183526304322635784260018311873853696931948390984705324309159959175912853336068039519643334925916242587284604503497946860620532884070535320102785468647273729904679289575406493832909201217872099618724940804344495146261774674917139805727670760359403243101179124268191457365076234540925454648430289935419474118382835857013206462483209955602729589887605259384359797726364381216113587246193939854334331474263584985020429606102810026549564410726386255306011855072052371800997373425385202624369312492488947176120995902899816717343743954198067695231279648219020448745568078008940367652984983732362358848728874265431512150540252169783672968674591273846510925402892326196577322110102964434888389812061692783547189445648176683812497103766278122421746198468301424485309574649841742394872468122618251536824792339922675192201960346025756902572647407325696795146195281365164038699950846301324885234647991028696976865654453589176654979471532728568654584853832451942604541277762968769668096005773808269554654223777842669744252783624353204706241260474033820066205249128951698965363063060147113186174940955847037737546264558522550113454323343976674465942821772849079414744009338396563220139607658666938479203550751423387865216958477950382374404742422201801193927156363602192156316862553999062168555158571930959, "widths": []}, {"id": "16384-small", "b": 2, "e": 1189731495357231765085759326628007130763444687096510237472674821233261358180483686904488595472612039915115437484839309258897667381308687426274524698341565006080871634366004897522143251619531446845952345709482135847036647464830984784714280967845614138476044338404886122905286855313236158695999885790106357018120815363320780964323712757164290613406875202417365323950267880089067517372270610835647545755780793431622213451903817859630690311343850657539360649645193283178291767658965405285113556134369793281725888015908414675289832538063419234888599898980623114025121674472051872439321323198402942705341366951274739014593816898288994445173400364617928377138074411345791848573595077170437644191743889644885377684738322240608239079061399475675334739784016491742621485229014847672335977897158397334226349734811441653077758250988926030894789604676153104257260141806823027588003441951455327701598071281589597169413965608439504983171255062282026626200048042149808200002060993433681237623857880627479727072877482838438705048034164633337013385405998040701908662387301605018188262573723766279240798931717708807901740265407930976419648877869604017517691938687988088008944251258826969688364194133945780157844364946052713655454906327187428531895100278695119323496808703630436193927592692344820812834297364478686862064169042458555136532055050508189891866846863799917647547291371573500701015197559097453040033031520683518216494195636696077748110598284901343611469214274121810495077979275556645164983850062051066517084647369464036640569339464837172183352956873912042640003611618789278195710052094562761306703551840330110645101995435167626688669627763820604342480357906415354212732946756073006907088870496125050068156659252761297664065498347492661798824062312210409274584565587264846417650160123175874034726261957289081466197651553830744424709698634753627770356227126145052549125229448040149114795681359875968512808575244271871455454084894986155020794806980939215658055319165641681105966454159951476908583129721503298816585142073061480888021769818338417129396878371459575846052583142928447249703698548125295775920936450022651427249949580708203966082847550921891152133321048011973883636577825533325988852156325439335021315312134081390451021255363707903495916963125924201167877190108935255914539488216897117943269373608639074472792751116715127106396425081353553137213552890539802602978645319795100976432939091924660228878912900654210118287298298707382159717184569540515403029173307292454391789568674219640761451173600617752186991913366837033887201582071625868247133104513315097274713442728340606642890406496636104443217752811227470029162858093727701049646499540220983981932786613204254226464243689610107429923197638681545837561773535568984536053627234424277105760924864023781629665526314910906960488073475217005121136311870439925762508666032566213750416695719919674223210606724721373471234021613540712188239909701971943944347480314217903886317767779921539892177334344368907550318800833546852344370327089284147501640589448482001254237386680074457341910933774891959681016516069106149905572425810895586938833067490204900368624166301968553005687040285095450484840073528643826570403767157286512380255109954518857013476588189300004138849715883139866071547574816476727635116435462804401112711392529180570794193422686818353212799068972247697191474268157912195973794192807298886952361100880264258801320928040011928153970801130741339550003299015924978259936974358726286143980520112454369271114083747919007803406596321353417004068869443405472140675963640997405009225803505672726465095506267339268892424364561897661906898424186770491035344080399248327097911712881140170384182058601614758284200750183500329358499691864066590539660709069537381601887679046657759654588001937117771344698326428792622894338016112445533539447087462049763409147542099248815521395929388007711172017894897793706604273480985161028815458787911160979113422433557549170905442026397275695283207305331845419990749347810524006194197200591652147867193696254337864981603833146354201700628817947177518115217674352016511172347727727075220056177748218928597158346744541337107358427757919660562583883823262178961691787226118865632764934288772405859754877759869235530653929937901193611669007472354746360764601872442031379944139824366828698790212922996174192728625891720057612509349100482545964152046477925114446500732164109099345259799455690095576788686397487061948854749024863607921857834205793797188834779656273479112388585706424836379072355410286787018527401653934219888361061949671961055068686961468019035629749424086587195041004404915266476272761070511568387063401264136517237211409916458796347624949215904533937210937520465798300175408017538862312719042361037129338896586028150046596078872444365564480545689033575955702988396719744528212984142578483954005084264327730840985420021409069485412320805268520094146798876110414583170390473982488899228091818213934288295679717369943152460447027290669964066796, "m": 1189731495357231765085759326628007130763444687096510237472674821233261358180483686904488595472612039915115437484839309258897667381308687426274524698341565006080871634366004897522143251619531446845952345709482135847036647464830984784714280967845614138476044338404886122905286855313236158695999885790106357018120815363320780964323712757164290613406875202417365323950267880089067517372270610835647545755780793431622213451903817859630690311343850657539360649645193283178291767658965405285113556134369793281725888015908414675289832538063419234888599898980623114025121674472051872439321323198402942705341366951274739014593816898288994445173400364617928377138074411345791848573595077170437644191743889644885377684738322240608239079061399475675334739784016491742621485229014847672335977897158397334226349734811441653077758250988926030894789604676153104257260141806823027588003441951455327701598071281589597169413965608439504983171255062282026626200048042149808200002060993433681237623857880627479727072877482838438705048034164633337013385405998040701908662387301605018188262573723766279240798931717708807901740265407930976419648877869604017517691938687988088008944251258826969688364194133945780157844364946052713655454906327187428531895100278695119323496808703630436193927592692344820812834297364478686862064169042458555136532055050508189891866846863799917647547291371573500701015197559097453040033031520683518216494195636696077748110598284901343611469214274121810495077979275556645164983850062051066517084647369464036640569339464837172183352956873912042640003611618789278195710052094562761306703551840330110645101995435167626688669627763820604342480357906415354212732946756073006907088870496125050068156659252761297664065498347492661798824062312210409274584565587264846417650160123175874034726261957289081466197651553830744424709698634753627770356227126145052549125229448040149114795681359875968512808575244271871455454084894986155020794806980939215658055319165641681105966454159951476908583129721503298816585142073061480888021769818338417129396878371459575846052583142928447249703698548125295775920936450022651427249949580708203966082847550921891152133321048011973883636577825533325988852156325439335021315312134081390451021255363707903495916963125924201167877190108935255914539488216897117943269373608639074472792751116715127106396425081353553137213552890539802602978645319795100976432939091924660228878912900654210118287298298707382159717184569540515403029173307292454391789568674219640761451173600617752186991913366837033887201582071625868247133104513315097274713442728340606642890406496636104443217752811227470029162858093727701049646499540220983981932786613204254226464243689610107429923197638681545837561773535568984536053627234424277105760924864023781629665526314910906960488073475217005121136311870439925762508666032566213750416695719919674223210606724721373471234021613540712188239909701971943944347480314217903886317767779921539892177334344368907550318800833546852344370327089284147501640589448482001254237386680074457341910933774891959681016516069106149905572425810895586938833067490204900368624166301968553005687040285095450484840073528643826570403767157286512380255109954518857013476588189300004138849715883139866071547574816476727635116435462804401112711392529180570794193422686818353212799068972247697191474268157912195973794192807298886952361100880264258801320928040011928153970801130741339550003299015924978259936974358726286143980520112454369271114083747919007803406596321353417004068869443405472140675963640997405009225803505672726465095506267339268892424364561897661906898424186770491035344080399248327097911712881140170384182058601614758284200750183500329358499691864066590539660709069537381601887679046657759654588001937117771344698326428792622894338016112445533539447087462049763409147542099248815521395929388007711172017894897793706604273480985161028815458787911160979113422433557549170905442026397275695283207305331845419990749347810524006194197200591652147867193696254337864981603833146354201700628817947177518115217674352016511172347727727075220056177748218928597158346744541337107358427757919660562583883823262178961691787226118865632764934288772405859754877759869235530653929937901193611669007472354746360764601872442031379944139824366828698790212922996174192728625891720057612509349100482545964152046477925114446500732164109099345259799455690095576788686397487061948854749024863607921857834205793797188834779656273479112388585706424836379072355410286787018527401653934219888361061949671961055068686961468019035629749424086587195041004404915266476272761070511568387063401264136517237211409916458796347624949215904533937210937520465798300175408017538862312719042361037129338896586028150046596078872444365564480545689033575955702988396719744528212984142578483954005084264327730840985420021409069485412320805268520094146798876110414583170390473982488899228091818213934288295679717369943152460447027290669964066797, "expected": 141194100056593707410852577180765761601173237374861369052923103366628782741144056595639606008694471792764517069102163255331830417474393388792602537179195995722397943194351326164336056672970509617916985826418714626164903759067712120221289355214631076134868288067695822338463965685596885144218524610375619075641211295073082035020466940629622425006537168203082088455647909310717169148032885546816783512022451914063931828507240588169651765788152380435587809815196081094419671191798984178873075115544996591329609194274097650418224955620422165229717637237213961280681770507015585627661463890931805841338096018293087701020061183678065757478513513289094312690534395551362996027413817167577626238489895782378223870775784310411796065642440061163824523275980608642243934930456397675384492328308309013091140929956593053464321811290485157569358017387960421749334417750874425564027950526099682327526897380359280518740444878384177011814053035782597101524239057324558058077175475762524046761036096266966122339041689764075173057179174137910658751731237791339120808558923690106444164055491176102776484284680000618439629175793434832069496239811597133530213154554515755276370950249019136385240367276250076153383633910059535375429222915451946911674377571259712318754450761679354325304326512783253289795274865470385091188502679710595333379431681755703521261824105342332003014246223705932542815211595093166904028293431355129176300027144290276306448187771020670599762440543866046601941448641224204410457435651573722634719700971350418028776215755075282570531587382847744947806722927857743279163003439770335066115961744894961214578982236517173610759054515626049204677081000676430375372321547141754885589869716104506475889011805136922226986646000505608417411573814501005981615287698012387510433092137038568718944985253815752343657012379318641938654926817562618996105984851845290645875131342538095170269417477567361218578150279992536696276175000213670968289408830593865409257530218625996767269181239753319233188114744513063074710784956290898492236956667621628049997440042144296866130151330096369116010751390659052370141438659333652375578114640629139579976877029328389975917545497783850196792565277114597979811709168429909808777746694515670283094275752302424653050554837035608651279775256002261258114823791200490137249972266411355392621399939830463427121766761360985395457191732314145406742391330241305236998818148551019245120285835155361977906044476801540765414164128662869926700632077639203659509171384796077210063035327089700377831086104074990597720162484759571437499017354618689869140965436920124501725794064444436878530972528076595335863208049554709164715819175650789944059490911374584475932407167679545509930015492213292047103486061899124941800786210589953760337951974929628282693805553350130270038158036079073532126309190107259343152634903970488550287179236726097278903199083438091591147461964708706982690751261889678251247661874355232818782776707845787484810381016783796173142743638741747663311193036474505526882185149423245643936966422039110840529120398453472725736625223360954243337389466687587798420037582415400301066903236456614608507509930313873507771575671456503492942076530131390240626704770793643307839067400387221809603193800830881650826850949194955941492595014298320438326136664504893997830676772471945761280244238687415656238702046453807758345976630314826139921197708107568846805334128126817744894219564395240384865292655513054449484997780312295113439685135832710738223311593134274631626690093432407214771213009510363981304591968650696663651798684287491474647394238233751224985103342255312975964948267308433932198536937188391065738039866408954657009752814813069317056851373128230811122985913691363613398415193466810085976369192815104514426248897691561720444894226880804738035625296374436653589779589103585180355436199383446332381814504230686758880164720874563875434323939721897151611462124458271092690105883413630243783226570294467642478157320884186806020335097257524195335905660692359728288210385344707257242066780134821355691127283960851642986283849925718385336618376288414460576910580910653868357717159672634709368502035166014281847349455907504569492160705701295018175270870903464324488012031927994736821321365428402758090511194481024328013879339511025697598163107150670472315557791080697943771207982587689259469792762008870939611392840035564939329744972300316168198948922024589308295168065361273054393363309561515374213710874729928001843752996789388653631984427346192649516807293431112387784826590317727342658064043495378784211302632607480882127792103599339885759750699737049411855892703131110711455574425985726860772595857894092599525342700881747018675300901332768415421055697084770366009035118839832114635589152870347699369539161928534019965972453691063386163006331880518839408589683500402274968783550937395442231910305600422137004879467266341295783383884867266642639731204409397644231164929120535860788199802014086017044694047664618825, "widths": []}, {"id": "16384-full", "b": 396577165119077255028586442209335710254481562365503412490891607077753786060161228968162865157537346638371812494946436419632555793769562475424841566113855002026957211455334965840714417206510482281984115236494045282345549154943661594904760322615204712825348112801628707635095618437745386231999961930035452339373605121106926988107904252388096871135625067472455107983422626696355839124090203611882515251926931143874071150634605953210230103781283552513120216548397761059430589219655135095037852044789931093908629338636138225096610846021139744962866632993541038008373891490683957479773774399467647568447122317091579671531272299429664815057800121539309459046024803781930616191198359056812548063914629881628459228246107413536079693020466491891778246594672163914207161743004949224111992632386132444742116578270480551025919416996308676964929868225384368085753380602274342529334480650485109233866023760529865723137988536146501661057085020760675542066682680716602733334020331144560412541285960209159909024292494279479568349344721544445671128468666013567302887462433868339396087524574588759746932977239236269300580088469310325473216292623201339172563979562662696002981417086275656562788064711315260052614788315350904551818302109062476177298366759565039774498936234543478731309197564114940270944765788159562287354723014152851712177351683502729963955615621266639215849097123857833567005065853032484346677677173561172738831398545565359249370199428300447870489738091373936831692659758518881721661283354017022172361549123154678880189779821612390727784318957970680880001203872929759398570017364854253768901183946776703548367331811722542229556542587940201447493452635471784737577648918691002302362956832041683356052219750920432554688499449164220599608020770736803091528188529088282139216720041058624678242087319096360488732550517943581474903232878251209256785409042048350849708409816013383038265227119958656170936191748090623818484694964995385006931602326979738552685106388547227035322151386650492302861043240501099605528380691020493629340589939446139043132292790486525282017527714309482416567899516041765258640312150007550475749983193569401322027615850307297050711107016003991294545525941844441996284052108479778340438437378027130150340418454569301165305654375308067055959063369645085304846496072299039314423124536213024824264250372238375702132141693784517712404517630179934200992881773265033658810979697308220076292970966884736706095766099569127386572394856513505134343057769097484797263189558073213587150391200205917395663971122279011295733860690541956082377701504438365758237814242780202214296802165545368147739250937075823343054286031242567016548833180073661327310928871068084742154747896536702476641065879560515279187257845189661512017875744808092368586974954674593876555175438303635653496024491739001707045437290146641920836222010855404583472231906639891407736868908240457823744673871180237396079969900657314648115826771405967962105922593307179964059111448122969183439600277848950781456775696428049167213529816160667084745795560024819113970311258297319893672172023035383301857475270298528979611022496734966789541388767322851001895680095031816828280024509547942190134589052428837460085036651506285671158862729766668046283238627713288690515858272158909211705478487601467037570464176393523598064474228939451070933022990749232397158089385970731991264730935766295650787033626754752933773642680003976051323600376913779850001099671974992753312324786242095381326840037484789757038027915973002601135532107117805668022956481135157380225321213665801669741934501890908821698502089113089630808121520632553968966141395590163678448026799749442365970570960380056794727352867204919428066916727833443119499897288022196846553569689845793867295893015552586551529333979039257114899442142930874298112672037481844513149029154016587803049180699749605173798643129335903724005964965931235534757826995053676271819595970386993037807477852516390301814008799091898427735768443948473330249782603508002064732400197217382622397898751445954993867944382118067233542939315725839371739224784005503724115909242358406685392582739642865719448914847112369119475919306553520861294607754059653897262408706288544254978096257468619918292586623078510217976645967064537223002490784915453588200624147343793314713274788942899596737640998724730909541963906685870836449700160848654717348825975038148833577388036366448419933151896698525596228799162353982951583008287869307285944735264599062944926552091159704129528568808278793024118470095595672842467217978073296120353983223987018356228987156006345209916474695529065013668134971755492090920356837189462354467088045505745737136638819598782541649738634844645736979173488599433391802672512954104239680787012376446298862009383348865359624148121854826848563011191985234329465573248176070994714192827984668361421442576946995140007136356495137440268422840031382266292036804861056796824660829633076030606071311429431893239123314384153482342430223321355599, "e": 1189731495357231765085759326628007130763444687096510237472674821233261358180483686904488595472612039915115437484839309258897667381308687426274524698341565006080871634366004897522143251619531446845952345709482135847036647464830984784714280967845614138476044338404886122905286855313236158695999885790106357018120815363320780964323712757164290613406875202417365323950267880089067517372270610835647545755780793431622213451903817859630690311343850657539360649645193283178291767658965405285113556134369793281725888015908414675289832538063419234888599898980623114025121674472051872439321323198402942705341366951274739014593816898288994445173400364617928377138074411345791848573595077170437644191743889644885377684738322240608239079061399475675334739784016491742621485229014847672335977897158397334226349734811441653077758250988926030894789604676153104257260141806823027588003441951455327701598071281589597169413965608439504983171255062282026626200048042149808200002060993433681237623857880627479727072877482838438705048034164633337013385405998040701908662387301605018188262573723766279240798931717708807901740265407930976419648877869604017517691938687988088008944251258826969688364194133945780157844364946052713655454906327187428531895100278695119323496808703630436193927592692344820812834297364478686862064169042458555136532055050508189891866846863799917647547291371573500701015197559097453040033031520683518216494195636696077748110598284901343611469214274121810495077979275556645164983850062051066517084647369464036640569339464837172183352956873912042640003611618789278195710052094562761306703551840330110645101995435167626688669627763820604342480357906415354212732946756073006907088870496125050068156659252761297664065498347492661798824062312210409274584565587264846417650160123175874034726261957289081466197651553830744424709698634753627770356227126145052549125229448040149114795681359875968512808575244271871455454084894986155020794806980939215658055319165641681105966454159951476908583129721503298816585142073061480888021769818338417129396878371459575846052583142928447249703698548125295775920936450022651427249949580708203966082847550921891152133321048011973883636577825533325988852156325439335021315312134081390451021255363707903495916963125924201167877190108935255914539488216897117943269373608639074472792751116715127106396425081353553137213552890539802602978645319795100976432939091924660228878912900654210118287298298707382159717184569540515403029173307292454391789568674219640761451173600617752186991913366837033887201582071625868247133104513315097274713442728340606642890406496636104443217752811227470029162858093727701049646499540220983981932786613204254226464243689610107429923197638681545837561773535568984536053627234424277105760924864023781629665526314910906960488073475217005121136311870439925762508666032566213750416695719919674223210606724721373471234021613540712188239909701971943944347480314217903886317767779921539892177334344368907550318800833546852344370327089284147501640589448482001254237386680074457341910933774891959681016516069106149905572425810895586938833067490204900368624166301968553005687040285095450484840073528643826570403767157286512380255109954518857013476588189300004138849715883139866071547574816476727635116435462804401112711392529180570794193422686818353212799068972247697191474268157912195973794192807298886952361100880264258801320928040011928153970801130741339550003299015924978259936974358726286143980520112454369271114083747919007803406596321353417004068869443405472140675963640997405009225803505672726465095506267339268892424364561897661906898424186770491035344080399248327097911712881140170384182058601614758284200750183500329358499691864066590539660709069537381601887679046657759654588001937117771344698326428792622894338016112445533539447087462049763409147542099248815521395929388007711172017894897793706604273480985161028815458787911160979113422433557549170905442026397275695283207305331845419990749347810524006194197200591652147867193696254337864981603833146354201700628817947177518115217674352016511172347727727075220056177748218928597158346744541337107358427757919660562583883823262178961691787226118865632764934288772405859754877759869235530653929937901193611669007472354746360764601872442031379944139824366828698790212922996174192728625891720057612509349100482545964152046477925114446500732164109099345259799455690095576788686397487061948854749024863607921857834205793797188834779656273479112388585706424836379072355410286787018527401653934219888361061949671961055068686961468019035629749424086587195041004404915266476272761070511568387063401264136517237211409916458796347624949215904533937210937520465798300175408017538862312719042361037129338896586028150046596078872444365564480545689033575955702988396719744528212984142578483954005084264327730840985420021409069485412320805268520094146798876110414583170390473982488899228091818213934288295679717369943152460447027290669964066796, "m": 1189731495357231765085759326628007130763444687096510237472674821233261358180483686904488595472612039915115437484839309258897667381308687426274524698341565006080871634366004897522143251619531446845952345709482135847036647464830984784714280967845614138476044338404886122905286855313236158695999885790106357018120815363320780964323712757164290613406875202417365323950267880089067517372270610835647545755780793431622213451903817859630690311343850657539360649645193283178291767658965405285113556134369793281725888015908414675289832538063419234888599898980623114025121674472051872439321323198402942705341366951274739014593816898288994445173400364617928377138074411345791848573595077170437644191743889644885377684738322240608239079061399475675334739784016491742621485229014847672335977897158397334226349734811441653077758250988926030894789604676153104257260141806823027588003441951455327701598071281589597169413965608439504983171255062282026626200048042149808200002060993433681237623857880627479727072877482838438705048034164633337013385405998040701908662387301605018188262573723766279240798931717708807901740265407930976419648877869604017517691938687988088008944251258826969688364194133945780157844364946052713655454906327187428531895100278695119323496808703630436193927592692344820812834297364478686862064169042458555136532055050508189891866846863799917647547291371573500701015197559097453040033031520683518216494195636696077748110598284901343611469214274121810495077979275556645164983850062051066517084647369464036640569339464837172183352956873912042640003611618789278195710052094562761306703551840330110645101995435167626688669627763820604342480357906415354212732946756073006907088870496125050068156659252761297664065498347492661798824062312210409274584565587264846417650160123175874034726261957289081466197651553830744424709698634753627770356227126145052549125229448040149114795681359875968512808575244271871455454084894986155020794806980939215658055319165641681105966454159951476908583129721503298816585142073061480888021769818338417129396878371459575846052583142928447249703698548125295775920936450022651427249949580708203966082847550921891152133321048011973883636577825533325988852156325439335021315312134081390451021255363707903495916963125924201167877190108935255914539488216897117943269373608639074472792751116715127106396425081353553137213552890539802602978645319795100976432939091924660228878912900654210118287298298707382159717184569540515403029173307292454391789568674219640761451173600617752186991913366837033887201582071625868247133104513315097274713442728340606642890406496636104443217752811227470029162858093727701049646499540220983981932786613204254226464243689610107429923197638681545837561773535568984536053627234424277105760924864023781629665526314910906960488073475217005121136311870439925762508666032566213750416695719919674223210606724721373471234021613540712188239909701971943944347480314217903886317767779921539892177334344368907550318800833546852344370327089284147501640589448482001254237386680074457341910933774891959681016516069106149905572425810895586938833067490204900368624166301968553005687040285095450484840073528643826570403767157286512380255109954518857013476588189300004138849715883139866071547574816476727635116435462804401112711392529180570794193422686818353212799068972247697191474268157912195973794192807298886952361100880264258801320928040011928153970801130741339550003299015924978259936974358726286143980520112454369271114083747919007803406596321353417004068869443405472140675963640997405009225803505672726465095506267339268892424364561897661906898424186770491035344080399248327097911712881140170384182058601614758284200750183500329358499691864066590539660709069537381601887679046657759654588001937117771344698326428792622894338016112445533539447087462049763409147542099248815521395929388007711172017894897793706604273480985161028815458787911160979113422433557549170905442026397275695283207305331845419990749347810524006194197200591652147867193696254337864981603833146354201700628817947177518115217674352016511172347727727075220056177748218928597158346744541337107358427757919660562583883823262178961691787226118865632764934288772405859754877759869235530653929937901193611669007472354746360764601872442031379944139824366828698790212922996174192728625891720057612509349100482545964152046477925114446500732164109099345259799455690095576788686397487061948854749024863607921857834205793797188834779656273479112388585706424836379072355410286787018527401653934219888361061949671961055068686961468019035629749424086587195041004404915266476272761070511568387063401264136517237211409916458796347624949215904533937210937520465798300175408017538862312719042361037129338896586028150046596078872444365564480545689033575955702988396719744528212984142578483954005084264327730840985420021409069485412320805268520094146798876110414583170390473982488899228091818213934288295679717369943152460447027290669964066797, "expected": 793154330238154510057172884418671420508963124731006824981783214155507572120322457936325730315074693276743624989892872839265111587539124950849683132227710004053914422910669931681428834413020964563968230472988090564691098309887323189809520645230409425650696225603257415270191236875490772463999923860070904678747210242213853976215808504776193742271250134944910215966845253392711678248180407223765030503853862287748142301269211906420460207562567105026240433096795522118861178439310270190075704089579862187817258677272276450193221692042279489925733265987082076016747782981367914959547548798935295136894244634183159343062544598859329630115600243078618918092049607563861232382396718113625096127829259763256918456492214827072159386040932983783556493189344327828414323486009898448223985264772264889484233156540961102051838833992617353929859736450768736171506761204548685058668961300970218467732047521059731446275977072293003322114170041521351084133365361433205466668040662289120825082571920418319818048584988558959136698689443088891342256937332027134605774924867736678792175049149177519493865954478472538601160176938620650946432585246402678345127959125325392005962834172551313125576129422630520105229576630701809103636604218124952354596733519130079548997872469086957462618395128229880541889531576319124574709446028305703424354703367005459927911231242533278431698194247715667134010131706064968693355354347122345477662797091130718498740398856600895740979476182747873663385319517037763443322566708034044344723098246309357760379559643224781455568637915941361760002407745859518797140034729708507537802367893553407096734663623445084459113085175880402894986905270943569475155297837382004604725913664083366712104439501840865109376998898328441199216041541473606183056377058176564278433440082117249356484174638192720977465101035887162949806465756502418513570818084096701699416819632026766076530454239917312341872383496181247636969389929990770013863204653959477105370212777094454070644302773300984605722086481002199211056761382040987258681179878892278086264585580973050564035055428618964833135799032083530517280624300015100951499966387138802644055231700614594101422214032007982589091051883688883992568104216959556680876874756054260300680836909138602330611308750616134111918126739290170609692992144598078628846249072426049648528500744476751404264283387569035424809035260359868401985763546530067317621959394616440152585941933769473412191532199138254773144789713027010268686115538194969594526379116146427174300782400411834791327942244558022591467721381083912164755403008876731516475628485560404428593604331090736295478501874151646686108572062485134033097666360147322654621857742136169484309495793073404953282131759121030558374515690379323024035751489616184737173949909349187753110350876607271306992048983478003414090874580293283841672444021710809166944463813279782815473737816480915647489347742360474792159939801314629296231653542811935924211845186614359928118222896245938366879200555697901562913551392856098334427059632321334169491591120049638227940622516594639787344344046070766603714950540597057959222044993469933579082777534645702003791360190063633656560049019095884380269178104857674920170073303012571342317725459533336092566477255426577381031716544317818423410956975202934075140928352787047196128948457878902141866045981498464794316178771941463982529461871532591301574067253509505867547285360007952102647200753827559700002199343949985506624649572484190762653680074969579514076055831946005202271064214235611336045912962270314760450642427331603339483869003781817643397004178226179261616243041265107937932282791180327356896053599498884731941141920760113589454705734409838856133833455666886238999794576044393693107139379691587734591786031105173103058667958078514229798884285861748596225344074963689026298058308033175606098361399499210347597286258671807448011929931862471069515653990107352543639191940773986075614955705032780603628017598183796855471536887896946660499565207016004129464800394434765244795797502891909987735888764236134467085878631451678743478449568011007448231818484716813370785165479285731438897829694224738238951838613107041722589215508119307794524817412577088509956192514937239836585173246157020435953291934129074446004981569830907176401248294687586629426549577885799193475281997449461819083927813371741672899400321697309434697651950076297667154776072732896839866303793397051192457598324707965903166016575738614571889470529198125889853104182319408259057137616557586048236940191191345684934435956146592240707966447974036712457974312012690419832949391058130027336269943510984181840713674378924708934176091011491474273277639197565083299477269689291473958346977198866783605345025908208479361574024752892597724018766697730719248296243709653697126022383970468658931146496352141989428385655969336722842885153893990280014272712990274880536845680062764532584073609722113593649321659266152061212142622858863786478246628768306964684860446642711198, "widths": []}]

certificate-builds.json

{
  "cpu": 53,
  "host": "chungus2",
  "samples": [
    {
      "block": 0,
      "arm": "baseline",
      "seconds": 10.378460630017798,
      "returncode": 0,
      "stdout": "\u2714 [1965/1969] Built PrimeCert.SieveCorrect (5.8s)\n\u2714 [1966/1969] Built PrimeCert.Meta.Sieve (946ms)\n\u2714 [1967/1969] Built PrimeCert.SieveBase (860ms)\n\u2714 [1968/1969] Built PrimeCert.Meta.SieveLookup (956ms)\n\u26a0 [1969/1969] Built PrimeCertTest.CertificateBench (984ms)\nwarning: PrimeCertTest/CertificateBench.lean:18:100: This line exceeds the 100 character limit, please shorten it!\n\nNote: This linter can be disabled with `set_option linter.style.longLine false`\nwarning: PrimeCertTest/CertificateBench.lean:19:100: This line exceeds the 100 character limit, please shorten it!\n\nNote: This linter can be disabled with `set_option linter.style.longLine false`\nBuild completed successfully (1969 jobs).\n",
      "stderr": "",
      "load": [
        42.046875,
        37.58544921875,
        25.70263671875
      ]
    },
    {
      "block": 0,
      "arm": "windowed-powmod",
      "seconds": 1.7631337400525808,
      "returncode": 0,
      "stdout": "\u26a0 [1969/1969] Built PrimeCertTest.CertificateBench (827ms)\nwarning: PrimeCertTest/CertificateBench.lean:18:100: This line exceeds the 100 character limit, please shorten it!\n\nNote: This linter can be disabled with `set_option linter.style.longLine false`\nwarning: PrimeCertTest/CertificateBench.lean:19:100: This line exceeds the 100 character limit, please shorten it!\n\nNote: This linter can be disabled with `set_option linter.style.longLine false`\nBuild completed successfully (1969 jobs).\n",
      "stderr": "",
      "load": [
        42.046875,
        37.58544921875,
        25.70263671875
      ]
    },
    {
      "block": 1,
      "arm": "windowed-powmod",
      "seconds": 1.62148559599882,
      "returncode": 0,
      "stdout": "\u26a0 [1969/1969] Built PrimeCertTest.CertificateBench (769ms)\nwarning: PrimeCertTest/CertificateBench.lean:18:100: This line exceeds the 100 character limit, please shorten it!\n\nNote: This linter can be disabled with `set_option linter.style.longLine false`\nwarning: PrimeCertTest/CertificateBench.lean:19:100: This line exceeds the 100 character limit, please shorten it!\n\nNote: This linter can be disabled with `set_option linter.style.longLine false`\nBuild completed successfully (1969 jobs).\n",
      "stderr": "",
      "load": [
        39.48046875,
        37.12744140625,
        25.6181640625
      ]
    },
    {
      "block": 1,
      "arm": "baseline",
      "seconds": 1.7303050010232255,
      "returncode": 0,
      "stdout": "\u26a0 [1969/1969] Built PrimeCertTest.CertificateBench (918ms)\nwarning: PrimeCertTest/CertificateBench.lean:18:100: This line exceeds the 100 character limit, please shorten it!\n\nNote: This linter can be disabled with `set_option linter.style.longLine false`\nwarning: PrimeCertTest/CertificateBench.lean:19:100: This line exceeds the 100 character limit, please shorten it!\n\nNote: This linter can be disabled with `set_option linter.style.longLine false`\nBuild completed successfully (1969 jobs).\n",
      "stderr": "",
      "load": [
        39.48046875,
        37.12744140625,
        25.6181640625
      ]
    },
    {
      "block": 2,
      "arm": "baseline",
      "seconds": 1.638767767988611,
      "returncode": 0,
      "stdout": "\u26a0 [1969/1969] Built PrimeCertTest.CertificateBench (810ms)\nwarning: PrimeCertTest/CertificateBench.lean:18:100: This line exceeds the 100 character limit, please shorten it!\n\nNote: This linter can be disabled with `set_option linter.style.longLine false`\nwarning: PrimeCertTest/CertificateBench.lean:19:100: This line exceeds the 100 character limit, please shorten it!\n\nNote: This linter can be disabled with `set_option linter.style.longLine false`\nBuild completed successfully (1969 jobs).\n",
      "stderr": "",
      "load": [
        39.48046875,
        37.12744140625,
        25.6181640625
      ]
    },
    {
      "block": 2,
      "arm": "windowed-powmod",
      "seconds": 1.620702183980029,
      "returncode": 0,
      "stdout": "\u26a0 [1969/1969] Built PrimeCertTest.CertificateBench (754ms)\nwarning: PrimeCertTest/CertificateBench.lean:18:100: This line exceeds the 100 character limit, please shorten it!\n\nNote: This linter can be disabled with `set_option linter.style.longLine false`\nwarning: PrimeCertTest/CertificateBench.lean:19:100: This line exceeds the 100 character limit, please shorten it!\n\nNote: This linter can be disabled with `set_option linter.style.longLine false`\nBuild completed successfully (1969 jobs).\n",
      "stderr": "",
      "load": [
        37.68017578125,
        36.79296875,
        25.57177734375
      ]
    },
    {
      "block": 3,
      "arm": "windowed-powmod",
      "seconds": 1.5966738570132293,
      "returncode": 0,
      "stdout": "\u26a0 [1969/1969] Built PrimeCertTest.CertificateBench (750ms)\nwarning: PrimeCertTest/CertificateBench.lean:18:100: This line exceeds the 100 character limit, please shorten it!\n\nNote: This linter can be disabled with `set_option linter.style.longLine false`\nwarning: PrimeCertTest/CertificateBench.lean:19:100: This line exceeds the 100 character limit, please shorten it!\n\nNote: This linter can be disabled with `set_option linter.style.longLine false`\nBuild completed successfully (1969 jobs).\n",
      "stderr": "",
      "load": [
        37.68017578125,
        36.79296875,
        25.57177734375
      ]
    },
    {
      "block": 3,
      "arm": "baseline",
      "seconds": 1.7321891150204465,
      "returncode": 0,
      "stdout": "\u26a0 [1969/1969] Built PrimeCertTest.CertificateBench (847ms)\nwarning: PrimeCertTest/CertificateBench.lean:18:100: This line exceeds the 100 character limit, please shorten it!\n\nNote: This linter can be disabled with `set_option linter.style.longLine false`\nwarning: PrimeCertTest/CertificateBench.lean:19:100: This line exceeds the 100 character limit, please shorten it!\n\nNote: This linter can be disabled with `set_option linter.style.longLine false`\nBuild completed successfully (1969 jobs).\n",
      "stderr": "",
      "load": [
        37.68017578125,
        36.79296875,
        25.57177734375
      ]
    }
  ]
}

CertificateBench.lean

/-
Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kim Morrison
-/

module
public import PrimeCert
public import PrimeCert.SieveBase
public meta import PrimeCert.Meta.SieveLookup
public section
set_option maxRecDepth 65536
set_option exponentiation.threshold 512
theorem result : Nat.Prime (2 ^ 255 - 19) := prime_cert%
  [small {2; 3; 223; 353},
   sieve {4153; 57467},
   pock3 (31757755568855353, 5, 3, 2 ^ 3 * 223 * 4153),
   pock3 (74058212732561358302231226437062788676166966415465897661863160754340907, 2, 3, 2 * 353 * 57467 * 31757755568855353),
   pock (57896044618658097711785492504343953926634992332820282019728792003956564819949, 2, 74058212732561358302231226437062788676166966415465897661863160754340907)]

invalid-unfolded-baseline-samples.csv

large-negative-control-run-samples.csv

PowModBench.lean

/-
Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the Lean repository LICENSE.
Authors: Kim Morrison
-/
module
import Lean
public meta import PrimeCert.PowMod
meta import Lean

/-! Standalone kernel powMod tuning. No declarations are added to the library.
The JSON cases and every timed sample are retained by tune.py. -/

open Lean

structure Case where
  id : String
  b : Nat
  e : Nat
  m : Nat
  widths : List Nat
  expected : Nat
  deriving FromJson

@[expose] noncomputable def binary (a b n : Nat) : Nat :=
  powModK.aux n b.succ (a.mod n) b 1

def power (c : Case) (width : Option Nat) : Expr :=
  mkApp3 (mkConst (if width.isSome then ``binary else ``powModK))
    (mkRawNatLit c.b) (mkRawNatLit c.e) (mkRawNatLit c.m)

-- Checking the identity application forces the supplied equality's endpoints
-- to agree; merely checking Eq.refl's inferred type would not test the power.
def proof (lhs : Expr) (value : Nat) : Expr :=
  let n := mkConst ``Nat
  let rhs := mkRawNatLit value
  let type := mkApp3 (mkConst ``Eq [.succ .zero]) n lhs rhs
  mkApp (mkLambda `h .default type (mkBVar 0))
    (mkApp2 (mkConst ``Eq.refl [.succ .zero]) n rhs)

run_cmd do
  let path ← IO.getEnv "POWMOD_CASES"
  let some path := path | throwError "set POWMOD_CASES to the generated JSON file"
  let cases : List Case ← ofExcept <| (Json.parse (← IO.FS.readFile path)).bind fromJson?
  let some output ← IO.getEnv "POWMOD_SAMPLES" | throwError "set POWMOD_SAMPLES"
  let samples ← IO.FS.Handle.mk output .write
  let blocks := ((← IO.getEnv "POWMOD_BLOCKS").getD "4").toNat!
  -- Drain asynchronous checking before creating the reusable import environment.
  let ready ← IO.mkRef (← getEnv).toKernelEnv
  let env := Environment.ofKernelEnv (← ready.get)
  for block in [:blocks] do
    for c in cases do
      -- The compiled GMP implementation supplies an untrusted reference outside
      -- the timer. Each fresh kernel checker must establish the equality itself.
      let value := powMod c.b c.e c.m
      if value != c.expected then throwError "GMP disagrees with Python reference"
      let candidates := ("policy", none) :: c.widths.map (fun w => (s!"w{w}", some w))
      if block == 0 && c.m < 2^1024 then
        for width in some 0 :: candidates.map Prod.snd do
          let bad ← IO.mkRef (Kernel.check env {} (proof (power c width) (value + 1)))
          if (← bad.get).isOk then throwError "incorrect-result control was accepted"
      -- Equal preparation in every block; kernel caches are still fresh per call.
      let warm ← IO.mkRef (Kernel.check env {} (proof (power c none) value))
      let _ ← ofExceptKernelException (← warm.get)
      for (name, width) in candidates do
        let arms := [("binary", some 0), (name, width)]
        let arms := if block % 2 == 0 then arms else arms.reverse
        for (arm, width) in arms do
          -- References prevent the pure check from moving across the IO timer.
          let input ← IO.mkRef (env, proof (power c width) value)
          let (env, term) ← input.get
          let start ← IO.monoNanosNow
          let checked ← IO.mkRef (Kernel.check env {} term)
          let checked ← checked.get
          let stop ← IO.monoNanosNow
          let _ ← ofExceptKernelException checked
          samples.putStrLn s!"SAMPLE,{block},{c.id},{name},{arm},{stop - start}"
          samples.flush
  IO.println "COMPLETE"

record-final.json

{
  "cpu": 25,
  "host": "chungus2",
  "load_before": [
    6.80029296875,
    19.4716796875,
    21.919921875
  ],
  "stdout": "\u26a0 [598/598] Built PrimeCertTest.PowModBench (1102s)\nwarning: PrimeCertTest/PowModBench.lean:25:2: Redundant `[expose]` attribute, it is meaningful on public definitions only\ninfo: PrimeCertTest/PowModBench.lean:41:0: COMPLETE\nBuild completed successfully (598 jobs).\n",
  "stderr": "",
  "returncode": 0,
  "elapsed": 1102.7113275527954,
  "load_after": [
    4.6962890625,
    5.84716796875,
    11.0966796875
  ]
}

record-fixed.json

{
  "cpu": 13,
  "host": "chungus2",
  "load_before": [
    41.61962890625,
    37.2724609375,
    25.4091796875
  ],
  "stdout": "\u2716 [598/598] Building PrimeCertTest.PowModBench (148s)\ntrace: .> LEAN_PATH=/tmp/hex10268-primecert/.lake/packages/Cli/.lake/build/lib/lean:/tmp/hex10268-primecert/.lake/packages/batteries/.lake/build/lib/lean:/tmp/hex10268-primecert/.lake/packages/Qq/.lake/build/lib/lean:/tmp/hex10268-primecert/.lake/packages/aesop/.lake/build/lib/lean:/tmp/hex10268-primecert/.lake/packages/proofwidgets/.lake/build/lib/lean:/tmp/hex10268-primecert/.lake/packages/importGraph/.lake/build/lib/lean:/tmp/hex10268-primecert/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/tmp/hex10268-primecert/.lake/packages/plausible/.lake/build/lib/lean:/tmp/hex10268-primecert/.lake/packages/mathlib/.lake/build/lib/lean:/home/kim/worktrees/PrimeCert/primecert-windowed-powmod/.lake/build/lib/lean /home/kim/.elan/toolchains/leanprover--lean4---v4.33.0/bin/lean /home/kim/worktrees/PrimeCert/primecert-windowed-powmod/PrimeCertTest/PowModBench.lean -o /home/kim/worktrees/PrimeCert/primecert-windowed-powmod/.lake/build/lib/lean/PrimeCertTest/PowModBench.olean -i /home/kim/worktrees/PrimeCert/primecert-windowed-powmod/.lake/build/lib/lean/PrimeCertTest/PowModBench.ilean -c /home/kim/worktrees/PrimeCert/primecert-windowed-powmod/.lake/build/ir/PrimeCertTest/PowModBench.c --setup /home/kim/worktrees/PrimeCert/primecert-windowed-powmod/.lake/build/ir/PrimeCertTest/PowModBench.setup.json --json\nerror: Lean exited with code 143\nSome required targets logged failures:\n- PrimeCertTest.PowModBench\n",
  "stderr": "error: build failed\n",
  "returncode": 1,
  "elapsed": 148.96576571464539,
  "load_after": [
    23.271484375,
    33.8115234375,
    26.04638671875
  ]
}

record-wrapper.json

{
  "cpu": 0,
  "host": "chungus2",
  "load_before": [
    23.271484375,
    33.8115234375,
    26.04638671875
  ],
  "stdout": "\u2716 [598/598] Building PrimeCertTest.PowModBench (232s)\ntrace: .> LEAN_PATH=/tmp/hex10268-primecert/.lake/packages/Cli/.lake/build/lib/lean:/tmp/hex10268-primecert/.lake/packages/batteries/.lake/build/lib/lean:/tmp/hex10268-primecert/.lake/packages/Qq/.lake/build/lib/lean:/tmp/hex10268-primecert/.lake/packages/aesop/.lake/build/lib/lean:/tmp/hex10268-primecert/.lake/packages/proofwidgets/.lake/build/lib/lean:/tmp/hex10268-primecert/.lake/packages/importGraph/.lake/build/lib/lean:/tmp/hex10268-primecert/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/tmp/hex10268-primecert/.lake/packages/plausible/.lake/build/lib/lean:/tmp/hex10268-primecert/.lake/packages/mathlib/.lake/build/lib/lean:/home/kim/worktrees/PrimeCert/primecert-windowed-powmod/.lake/build/lib/lean /home/kim/.elan/toolchains/leanprover--lean4---v4.33.0/bin/lean /home/kim/worktrees/PrimeCert/primecert-windowed-powmod/PrimeCertTest/PowModBench.lean -o /home/kim/worktrees/PrimeCert/primecert-windowed-powmod/.lake/build/lib/lean/PrimeCertTest/PowModBench.olean -i /home/kim/worktrees/PrimeCert/primecert-windowed-powmod/.lake/build/lib/lean/PrimeCertTest/PowModBench.ilean -c /home/kim/worktrees/PrimeCert/primecert-windowed-powmod/.lake/build/ir/PrimeCertTest/PowModBench.c --setup /home/kim/worktrees/PrimeCert/primecert-windowed-powmod/.lake/build/ir/PrimeCertTest/PowModBench.setup.json --json\nerror: Lean exited with code 143\nSome required targets logged failures:\n- PrimeCertTest.PowModBench\n",
  "stderr": "error: build failed\n",
  "returncode": 1,
  "elapsed": 233.26748514175415,
  "load_after": [
    6.80029296875,
    19.4716796875,
    21.919921875
  ]
}

record.json

{
  "cpu": 27,
  "host": "chungus2",
  "load_before": [
    19.08984375,
    15.0791015625,
    15.72412109375
  ],
  "stdout": "\u2716 [598/598] Building PrimeCertTest.PowModBench (115s)\ntrace: .> LEAN_PATH=/tmp/hex10268-primecert/.lake/packages/Cli/.lake/build/lib/lean:/tmp/hex10268-primecert/.lake/packages/batteries/.lake/build/lib/lean:/tmp/hex10268-primecert/.lake/packages/Qq/.lake/build/lib/lean:/tmp/hex10268-primecert/.lake/packages/aesop/.lake/build/lib/lean:/tmp/hex10268-primecert/.lake/packages/proofwidgets/.lake/build/lib/lean:/tmp/hex10268-primecert/.lake/packages/importGraph/.lake/build/lib/lean:/tmp/hex10268-primecert/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/tmp/hex10268-primecert/.lake/packages/plausible/.lake/build/lib/lean:/tmp/hex10268-primecert/.lake/packages/mathlib/.lake/build/lib/lean:/home/kim/worktrees/PrimeCert/primecert-windowed-powmod/.lake/build/lib/lean /home/kim/.elan/toolchains/leanprover--lean4---v4.33.0/bin/lean /home/kim/worktrees/PrimeCert/primecert-windowed-powmod/PrimeCertTest/PowModBench.lean -o /home/kim/worktrees/PrimeCert/primecert-windowed-powmod/.lake/build/lib/lean/PrimeCertTest/PowModBench.olean -i /home/kim/worktrees/PrimeCert/primecert-windowed-powmod/.lake/build/lib/lean/PrimeCertTest/PowModBench.ilean -c /home/kim/worktrees/PrimeCert/primecert-windowed-powmod/.lake/build/ir/PrimeCertTest/PowModBench.c --setup /home/kim/worktrees/PrimeCert/primecert-windowed-powmod/.lake/build/ir/PrimeCertTest/PowModBench.setup.json --json\nerror: PrimeCertTest/PowModBench.lean:43:0: Invalid `meta` definition `_eval`, `powMod` is not accessible here; consider adding `public meta import PrimeCert.PowMod`\nerror: Lean exited with code 1\nSome required targets logged failures:\n- PrimeCertTest.PowModBench\n",
  "stderr": "error: build failed\n",
  "returncode": 1,
  "elapsed": 125.59212923049927,
  "load_after": [
    94.900390625,
    40.771484375,
    24.69775390625
  ]
}

samples.csv