From bef9060f6b923577ca1d5a78266fd84df00ca93a Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Fri, 16 Oct 2026 16:03:42 +0100 Subject: [PATCH] feat(research): certify the F-star one-interior-label gap --- research/fstar-one-interior-label/README.md | 204 ++ research/fstar-one-interior-label/RESULT.json | 3008 +++++++++++++++++ .../fstar-one-interior-label/SOURCES.json | 24 + research/fstar-one-interior-label/TASK.json | 99 + research/fstar-one-interior-label/VERIFY.json | 26 + .../fstar-one-interior-label/independent.py | 124 + .../fstar-one-interior-label/test_verify.py | 205 ++ research/fstar-one-interior-label/verify.py | 230 ++ 8 files changed, 3920 insertions(+) create mode 100644 research/fstar-one-interior-label/README.md create mode 100644 research/fstar-one-interior-label/RESULT.json create mode 100644 research/fstar-one-interior-label/SOURCES.json create mode 100644 research/fstar-one-interior-label/TASK.json create mode 100644 research/fstar-one-interior-label/VERIFY.json create mode 100644 research/fstar-one-interior-label/independent.py create mode 100644 research/fstar-one-interior-label/test_verify.py create mode 100644 research/fstar-one-interior-label/verify.py diff --git a/research/fstar-one-interior-label/README.md b/research/fstar-one-interior-label/README.md new file mode 100644 index 0000000000..7dfaee6909 --- /dev/null +++ b/research/fstar-one-interior-label/README.md @@ -0,0 +1,204 @@ +# F-star: one exceptional label is necessary and sufficient at v = 11 + +For **each of the twelve eleven-line restrictions of `tied_min`**, the exact +Form-R maximum is **10**. A certificate keeping all eleven lines needs at least +one pair outside Form-R. Exactly one additional pair of the form +`(a,b) = (111,e_c)` suffices, with `c` in that line's column support. All other +pairs in the new witnesses are ordinary repairs or matched pivots. + +This answers the constructive part of [Aaron Wang's PR2963 open question 2][2963] +and settles [PR2914's open Form-R question][2914] on the full twelve-line fixture. +Its Form-R maximum is also exactly 10: any eleven-line certificate would occur +in one of the twelve excluded restrictions, while a ten-line witness exists. +No recorded CP-SAT optimum or predecessor executable is needed for either result. +The [retained review][review] explicitly leaves the Form-R question open and +records objective bugs in the older completion routines. This package imports +none of those routines and does not endorse their other claims. + +This is an author-checked finite result. It is not a proof or refutation of +F-star, a physical decoder construction, supplier admission or a new kappa. +The selected frontier and all predecessor packages are unchanged. + +## Definitions and exact scope + +The source is DreamingOfClouds' `tied_min` fixture from PR2111, retained in +Aaron Wang's PR2869 package on main. Its SHA256 is +`670ed90924b601ade22f0d4adaff46d1667e5449326a0f7ba7b88dd8f5906f93`. +It is byte-identical to the fixture vendored by PR2963 at +`ee755e682b3b30d493e764d3be50003b13b69b4a`. The receipt reconstructs every +zero entry from the integer factors `M = P Q^T`, not a stored zero graph. + +An L8 certificate consists of supported three-bit labels `a(t),b(t)` and an +order of kept lines. It requires `a(t) dot b(t) = 1` over F2 and +`a(t) dot b(s) = 0` whenever `t` precedes `s` and `M[t,s] = 0`. +DreamingOfClouds' PR1590 proves the inherited bound `cost >= cert(M)`. +That bound is context, not newly proved here. + +Every entry of P is odd; Q has exactly two odd nonzero entries per line. +The canonical anchors are therefore `a0(t)=111` and `b0(t)=supp Q(t)`. +All eleven-line restrictions retain these anchors, and `a0 dot b0 = 0`. +The self-certifying Form-R pairs of PR2914 are precisely: + +- repairs `(a,b0(t))` with `a dot b0(t)=1`; +- matched pivots `(e_c,e_c)` with `c` in `supp Q(t)`. + +There are six distinct pairs per line. The anchor itself cannot certify a +kept line and may be discarded. All labels allowed by L8 already lie in the +sub-anchor box on this fixture, because the anchors equal the full supports. +Consequently the minimum number of non-Form-R pairs is also the minimum number +of BOX-INTERIOR pairs under the predecessor's classification. + +The sufficient extension adds only the two pairs `(111,e_c)` per line, with +an occurrence budget of one across the whole certificate. Here `a=a0`, not a +proper subset. The class name BOX-INTERIOR means "inside the box but outside +Form-R"; it does not require both anchor inclusions to be proper. + +## Exact finite exclusion + +The primary checker places the next line from left to right. Its state stores, +for each unplaced line s, the currently allowed b labels. A state value of zero +marks a line already placed. When placing t with pair `(a,b)`, every unplaced +zero-arc successor s loses b labels with `a dot b(s)=1`. An empty remaining +domain rejects the branch. + +The state has all information needed for a completion. Earlier constraints +restrict only future b labels. Future constraints never inspect an earlier b. +For a fixed current a, choose the least-cost available b; that choice cannot +change any later domain. When paths reach the same state, retaining only their +least cost is therefore exact. Induction on the number of unplaced lines proves +that the finite recurrence preserves every possible certificate and introduces +none. The empty state at depth eleven is reachable if and only if an allowed +full certificate exists. + +For budget zero the complete reachable-layer counts, identical on all twelve +restrictions, are: + +```text +1, 44, 338, 652, 652, 434, 210, 87, 30, 7, 0, 0 +``` + +Thus all 2,455 reachable states exhaust without an eleven-line Form-R witness. +The separate reverse-order implementation chooses the *last* line and stores +allowed a labels instead. It uses explicit sets of labels rather than the +primary bitmask domains, and imports no primary or predecessor code. Its +complete layer counts are: + +```text +1, 22, 76, 146, 231, 244, 128, 34, 6, 0, 0, 0 +``` + +These 888 states independently exclude the same twelve full certificates. +Both recurrences reject a capacity overrun rather than interpreting it as an +exclusion. No heuristic search, floating-point arithmetic or solver status is +used for acceptance. + +## Constructive witnesses and minimality + +[RESULT.json](RESULT.json) contains all twelve one-exception eleven-line +witnesses, all twelve ten-line Form-R witnesses, and complete primary frontier +counts and digests. Default replay recomputes the complete receipt. Both +implementations check the supported labels, diagonal parities and every +chronological zero-arc condition of each witness. + +For example, omit original line 0 and index the remaining lines locally as +0 through 10, corresponding to original lines 1 through 11. One full witness +lists `(line,a,b)` in certificate order, with labels encoded as integers: + +```text +(0,1,1), (1,1,1), (2,5,6), (3,5,3), (6,1,5), (4,4,4), +(8,7,2), (5,2,6), (7,2,2), (9,4,4), (10,2,2) +``` + +Only `(8,7,2)` is outside Form-R. Since zero exceptions are impossible and +one succeeds, the minimum is exactly one. This is minimality in the *number +of exceptional kept-line pairs*, not a universal minimality claim about proof +families or physical decoder designs. + +PR2963 reports `named=9` on these restrictions. Taking that separately pinned +claim as context, the gap splits as `named 9 < Form-R 10 < one-exception 11`. +The new result does not recheck the predecessor's named-family optimization. +In particular, unrestricted ordering alone does not close the second point. + +## Reproduce and checks + +Python 3.12 or later, standard library only, from the repository root: + +```sh +python3.12 -I -O -Werror -B research/fstar-one-interior-label/verify.py +python3.12 -I -O -Werror -B research/fstar-one-interior-label/independent.py +python3.12 -I -O -Werror -B research/fstar-one-interior-label/test_verify.py +python3.12 -B scripts/research_package.py --package research/fstar-one-interior-label +``` + +The primary marker is +`PASS_FSTAR_ONE_INTERIOR records=12 form_r=10 minimum_interior=1 full_form_r=10`. +`verify.py --emit` prints the recomputed receipt without writing files. +`--write-result NEW_PATH` creates a new file exclusively. Direct replay needs +only this package and the declared fixture, not Git or network access. + +Seven behavioral test groups include a literal pair-times-order oracle on +all 220 three-line restrictions and four four-line controls, both exception +budgets, reversed witnesses, broken support/diagonal/order, actual weakened +implementations, capacity exhaustion, source corruption before parsing, +duplicate JSON keys, typed receipt drift and optimized Git-free replay. +Ignoring zero-arc restrictions or misclassifying the new pairs as Form-R makes +the actual weakened checker falsely admit eleven, so the controls distinguish +these faults. Local environments and commands are recorded in TASK.json. +Hosted CI is separate; no independent human or formal-kernel review is claimed. + +## Open next questions + +Can a general proof family permit a small number of `(a0,e_c)` exceptions +while preserving an explicit L8 order? This matters because the named families +miss an entire point that one such exception supplies here. A feasible first +step is to inspect the twelve stored orders for one common sufficient rule +and test it against both PR2111 fixtures. The blocker is a proved general +ordering rule, not finding more seeds. This finite result gives no guarantee +for other decoders, anchor normalizations or an arbitrary number of lines. + +Family decision: finish this finite label/ordering question and stop. No +physical construction or dependent search expansion follows from the result. +Native realization, copied information, restoration, physical hosting, full +recursive cost, precision and all-size lifting are unrun and remain separate +obligations before any supplier or kappa claim. + +## Sources and credit + +Scientific base is canonical main `916ecdd9d6e666fcad9b25369d055311f6ce8204`, +priority revision 5. [SOURCES.json](SOURCES.json) records exact live input and +historical assignment pins; [TASK.json](TASK.json) records the changed scope +from complex rank-shape mechanisms to this fresh proof-level handoff. +[Discussion2967][claim] is the canonical investigation thread. + +Credit Aaron Wang for PR2963's explicit handoff, PR2914's Form-R/box ladder, +PR2936's family census, and PR2869's retained fixture/anchor normalization. +Retain his PR2717/2747/2774/2890/2901 certificate, repair, pivot and graph +lineage. Credit DreamingOfClouds for PR2111's fixture and PR1590's L8 definition +and cost bound. No earlier fixture, label family, named optimum or physical +construction is claimed as new. The new content is the two exact Form-R +exclusions, the sharp one-exception result and its twelve constructive orders. + +Nick Petalas. Apache-2.0. Automated assistance was used for computation and +checking. No independent human review is claimed. + +Build the Lever led to the rerunnable finite checker. Prove It Works led to +the reverse-order exclusion and literal witness replay. Test Behavior, Not +Implementation led to the real CLI controls and actual weakened implementations. +Boundary Discipline kept source/receipt validation outside the recurrence. + +Power of Ten rule 3 deviation: Python allocates managed objects. Inputs are +capped at 4 KB, receipts at 2 MB, factors at twelve three-total lines, and each +search at 100,000 cumulative states with at most twelve transitions in depth. +Both frontiers are also capacity-checked while constructed. A deployed checker +for larger or untrusted domains would need a fixed-capacity representation. +Test-only source loading and unittest dispatch are rule 8/9 deviations with +three fixed local modules, bounded child processes, 60-second timeouts and +scoped temporary cleanup. No scientific replay dynamically loads predecessor +code. All changed functions are below 60 lines, contain no recursion and retain +explicit checks under `-O`. Diagnostics run with warnings as errors and Ruff +`E,F,I,UP,B`; shared repository configuration is unchanged. + +[2963]: https://github.com/CrocSwap/integer-mult-bounds/blob/ee755e682b3b30d493e764d3be50003b13b69b4a/research/fstar-gap2-v11-seed42ff0611/README.md +[2914]: https://github.com/CrocSwap/integer-mult-bounds/blob/3f7781efccdf10fa61a1e0a6f11c191579b21280/research/fstar-family-gap-seed1c25f56f/README.md +[claim]: https://github.com/CrocSwap/integer-mult-bounds/discussions/2967 +[review]: https://github.com/CrocSwap/integer-mult-bounds/blob/a23bdc1b07be96bea0101d44ae27d14de67a79ed/research/community-efficient1900-audit/README.md#remaining-review diff --git a/research/fstar-one-interior-label/RESULT.json b/research/fstar-one-interior-label/RESULT.json new file mode 100644 index 0000000000..e7c4277d0f --- /dev/null +++ b/research/fstar-one-interior-label/RESULT.json @@ -0,0 +1,3008 @@ +{ + "full_twelve_form_r_maximum": 10, + "records": [ + { + "extended": { + "layers": [ + { + "sha256": "0d745b36c239ef5780d81b74b4bbdc48c1dfe7d93eba3c59da491886187f1c5e", + "states": 1 + }, + { + "sha256": "a888f54eef02b1cdf734709ed76de25584275042c640c5dec2bfede1bf2d3fb2", + "states": 55 + }, + { + "sha256": "8151787190d16b1c858e005f572af5ac3e0af914350b72fd94490581b868eb87", + "states": 458 + }, + { + "sha256": "ac4033621bfe94184c9dc70bb1bf6735b767b50d7e20f6679087c2aef0dfeb88", + "states": 954 + }, + { + "sha256": "3e793febafede83d573f8c96801bf92b7d80f40cd4101ee611319f6734c8a2f9", + "states": 952 + }, + { + "sha256": "201f903afdbb30856f909f77a336cb1bd0464dda1f13e8379975571594aed48e", + "states": 626 + }, + { + "sha256": "91047a5bff8d1a44fd21ca2ba040acdf51380a0fde4af9c7c3471165d0c873a1", + "states": 348 + }, + { + "sha256": "df0e23adc2ce6b142fffb36a5c48ce3bd601eae4e92f14b8b6c6d111a693ff68", + "states": 167 + }, + { + "sha256": "b8423b372bc887e945794f3fdc01cb2e7aab893247dba1b9ef44d4d1d672ff1e", + "states": 56 + }, + { + "sha256": "b1d1f05773cb3ce2748611024a34e08f991e97b4c34d70a02cdc166e488530ee", + "states": 18 + }, + { + "sha256": "e0e78f75613f296e912d0f3efe5c74936b4de443ee483ab289a06eb97c107c99", + "states": 4 + }, + { + "sha256": "7e96535d62bca620b7133b2e293dea97b5848d810933b35edb45e7ae7efdeef6", + "states": 1 + } + ], + "minimum": 1, + "total_states": 3640, + "witness": [ + [ + 0, + 1, + 1 + ], + [ + 1, + 1, + 1 + ], + [ + 2, + 5, + 6 + ], + [ + 3, + 5, + 3 + ], + [ + 6, + 1, + 5 + ], + [ + 4, + 4, + 4 + ], + [ + 8, + 7, + 2 + ], + [ + 5, + 2, + 6 + ], + [ + 7, + 2, + 2 + ], + [ + 9, + 4, + 4 + ], + [ + 10, + 2, + 2 + ] + ] + }, + "form_r_exclusion": { + "layers": [ + { + "sha256": "0d745b36c239ef5780d81b74b4bbdc48c1dfe7d93eba3c59da491886187f1c5e", + "states": 1 + }, + { + "sha256": "85a10143d2d88157410beafa7a8c8c590dcfc0dead7db803b1f8fd861c5bb216", + "states": 44 + }, + { + "sha256": "5e51bd5322ff2c5ff45ecf6381ed47207806fdf20ece096ef8860d0ca04f07c8", + "states": 338 + }, + { + "sha256": "f41e1e8549818a1d20f0b9c3894e59981219739e8fab849b42daf18aff4ec6ae", + "states": 652 + }, + { + "sha256": "2adf6ee78d9d5e9bccd35636a25280bd141ae63be4b64996b118d12f6dcbd8a4", + "states": 652 + }, + { + "sha256": "51330b19f5b2e24c38308de802b001373a8c591720048aca156590b5d5adfc13", + "states": 434 + }, + { + "sha256": "31052dafff71ea61fdf384619d22955955c1f8902a1812aeb7764c91ae10bd7e", + "states": 210 + }, + { + "sha256": "e5e67ea7db112846ece591cf5af2313bfb824082ddcc094bc217d6fb1ceee738", + "states": 87 + }, + { + "sha256": "33cf45b8e06f20b89c5f267051c1f284a64cab56b0b8e90ba7faf41a83eaf0e7", + "states": 30 + }, + { + "sha256": "9409428f281e974367c143ceb70c754fbe92160dfab85a8d8df743fd7ac12202", + "states": 7 + }, + { + "sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "states": 0 + }, + { + "sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "states": 0 + } + ], + "minimum": null, + "total_states": 2455, + "witness": null + }, + "form_r_maximum": 10, + "indices": [ + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11 + ], + "minimum_interior_for_eleven": 1, + "omitted": 0, + "ten_line": { + "indices": [ + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10 + ], + "witness": [ + [ + 1, + 5, + 6 + ], + [ + 4, + 4, + 4 + ], + [ + 0, + 4, + 5 + ], + [ + 2, + 5, + 3 + ], + [ + 5, + 4, + 5 + ], + [ + 3, + 1, + 1 + ], + [ + 7, + 2, + 2 + ], + [ + 6, + 2, + 2 + ], + [ + 8, + 1, + 1 + ], + [ + 9, + 2, + 2 + ] + ] + } + }, + { + "extended": { + "layers": [ + { + "sha256": "4313a3a55c1dbd868405ba6d289b1e21cd8802bafce1ff605e145fc23b7a2afd", + "states": 1 + }, + { + "sha256": "9f6682a1bbdccf15ec5e410f91e3db86e3b4933b53231a133d35120bcdcaa4b4", + "states": 55 + }, + { + "sha256": "37ff6cf43da1ffd3ab5d1fba08c11c3785f0758a510a4258cbc0c7b608cb4339", + "states": 458 + }, + { + "sha256": "178215c5242afb9bcf0b64a93a9391332de6e628df052518c4945238f888994a", + "states": 954 + }, + { + "sha256": "3e810edc69d125f52cc8f864cbc9d668f557738dce6619463d766a68e5d88eaa", + "states": 952 + }, + { + "sha256": "bbea16944b5dafb32e334da6dafa7b3e07286ab21435228a8ff54e72c48e1363", + "states": 626 + }, + { + "sha256": "fa7012e1c0be7237cc6af36bdfe1bf39ab1957c22b74621c16cda9a5a931156b", + "states": 348 + }, + { + "sha256": "171703b2c59333b198b8d36234b6c429041a950c6c748772f200f222a740d088", + "states": 167 + }, + { + "sha256": "362f5f50941d2d54c2e378e4b6503b07f61efbd117b5670ab9e3e9ea3db429b9", + "states": 56 + }, + { + "sha256": "6430e9ef20e5cff6fea69c39c43f4528572b501d9073b56af97aa8b22615a227", + "states": 18 + }, + { + "sha256": "2433b84822084440aad50d41933c263163b24db4b54767dfec0c34dbe3c4c700", + "states": 4 + }, + { + "sha256": "7e96535d62bca620b7133b2e293dea97b5848d810933b35edb45e7ae7efdeef6", + "states": 1 + } + ], + "minimum": 1, + "total_states": 3640, + "witness": [ + [ + 0, + 4, + 4 + ], + [ + 1, + 4, + 4 + ], + [ + 3, + 7, + 1 + ], + [ + 7, + 6, + 3 + ], + [ + 8, + 5, + 6 + ], + [ + 10, + 5, + 3 + ], + [ + 2, + 2, + 2 + ], + [ + 6, + 4, + 5 + ], + [ + 4, + 1, + 1 + ], + [ + 5, + 2, + 2 + ], + [ + 9, + 1, + 1 + ] + ] + }, + "form_r_exclusion": { + "layers": [ + { + "sha256": "4313a3a55c1dbd868405ba6d289b1e21cd8802bafce1ff605e145fc23b7a2afd", + "states": 1 + }, + { + "sha256": "d6b4394a75af230247d732ae9c3ed4f3479c091e4539932309d4d1214304f925", + "states": 44 + }, + { + "sha256": "df87d25dbc909cea06c708772e302b6c4b8a874604a8916e75939df36e7008ca", + "states": 338 + }, + { + "sha256": "92e10cee7fb8a5c6691b364e73d5e3f60fc7162f754ac7ea1bad094a0bce7af4", + "states": 652 + }, + { + "sha256": "05d3df3041e5961583404e582311c2f530e13bbaad576b0528c69a0d0566fb79", + "states": 652 + }, + { + "sha256": "ed8fa8b67e0b4e99ee15f8071572c45d7caca333efeeb51c38c831b66d162223", + "states": 434 + }, + { + "sha256": "8af05edf51ba67244005818b92fc813d220419eb82971f3bced3c53f8c6e3188", + "states": 210 + }, + { + "sha256": "9e743b7a65b502270a13639a77ef26e4051994814c2c1062f690083a996b2978", + "states": 87 + }, + { + "sha256": "87e5b8a031858d862d684ec1c1af60be4a0bc20bf9b17d8f78eea334f2fe9418", + "states": 30 + }, + { + "sha256": "80e22c1ae576bd9292e3c5a6414d743bd07bf670f3060a204f13459df819a7c0", + "states": 7 + }, + { + "sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "states": 0 + }, + { + "sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "states": 0 + } + ], + "minimum": null, + "total_states": 2455, + "witness": null + }, + "form_r_maximum": 10, + "indices": [ + 0, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11 + ], + "minimum_interior_for_eleven": 1, + "omitted": 1, + "ten_line": { + "indices": [ + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10 + ], + "witness": [ + [ + 1, + 5, + 6 + ], + [ + 4, + 4, + 4 + ], + [ + 0, + 4, + 5 + ], + [ + 2, + 5, + 3 + ], + [ + 5, + 4, + 5 + ], + [ + 3, + 1, + 1 + ], + [ + 7, + 2, + 2 + ], + [ + 6, + 2, + 2 + ], + [ + 8, + 1, + 1 + ], + [ + 9, + 2, + 2 + ] + ] + } + }, + { + "extended": { + "layers": [ + { + "sha256": "f57ce06a02b8af8576fe2505ff09f89bda5050aafaae3b64372579dea9e3ca3f", + "states": 1 + }, + { + "sha256": "77e135dac391b778837005b25429cb08a3265adeb423680be22c11472218d3c4", + "states": 55 + }, + { + "sha256": "2c34b62ae59db2af0b445d1a0bc6a46f819a266c2677b387174d7c5b5eeba26e", + "states": 458 + }, + { + "sha256": "1e243872277e03443b65a3b8d869e5eda5d5e5d65cbcd944da252fbce57ad8fe", + "states": 954 + }, + { + "sha256": "49d9413189272bcbab044d448275443b6d5d4f493ab925b746829e41fe2c6e31", + "states": 952 + }, + { + "sha256": "e201fcba0f94dab2180d2f6246a812b6d593e795d30105675e674d5828854a9f", + "states": 626 + }, + { + "sha256": "b8809d7f6bec7bd0314f9d5ade3b03c179198a8d4cf554e00309ba9fddb7ff1d", + "states": 348 + }, + { + "sha256": "416b1b60123cbd73dec2a06804cfdde243776a094c4e52270b2b5f9956793db7", + "states": 167 + }, + { + "sha256": "1ef061136d297377bb0c560211c61e8270994549dbd2216126c69e15a0c054e3", + "states": 56 + }, + { + "sha256": "dfb1b9fdcd7f4211500dfc48ca121bde5e5e29730204c220037c8eea5f59fac5", + "states": 18 + }, + { + "sha256": "61b0be22bd9f73eb91f654d5928bf1530451f0d0e96ab40fa4360590cc40ac94", + "states": 4 + }, + { + "sha256": "7e96535d62bca620b7133b2e293dea97b5848d810933b35edb45e7ae7efdeef6", + "states": 1 + } + ], + "minimum": 1, + "total_states": 3640, + "witness": [ + [ + 0, + 2, + 2 + ], + [ + 1, + 2, + 2 + ], + [ + 3, + 6, + 3 + ], + [ + 8, + 2, + 6 + ], + [ + 2, + 4, + 4 + ], + [ + 4, + 4, + 4 + ], + [ + 5, + 7, + 4 + ], + [ + 9, + 4, + 5 + ], + [ + 6, + 1, + 1 + ], + [ + 7, + 1, + 1 + ], + [ + 10, + 1, + 1 + ] + ] + }, + "form_r_exclusion": { + "layers": [ + { + "sha256": "f57ce06a02b8af8576fe2505ff09f89bda5050aafaae3b64372579dea9e3ca3f", + "states": 1 + }, + { + "sha256": "6079b87ae11ae5fbb9a22d885a856c8cbd2ed5b0a94838fc3ce1ddd6422affd3", + "states": 44 + }, + { + "sha256": "aaad8bf32bba1b0d7767c7481361bef838d9b0781a4c9a20816de60ddd927a9d", + "states": 338 + }, + { + "sha256": "fdadd9b8db9f0196b5be8f134eedac50a6406582e305a4ec7c5a2024d6d3a83d", + "states": 652 + }, + { + "sha256": "cc0330215367d35b6882068f2e03fed2a71c2efd114e98fffefffc43a91d0ee4", + "states": 652 + }, + { + "sha256": "3e89556bf45e4dd3c49b5913fb2eb8b65504c0c65c0ae5f33de8e5fd48472a0b", + "states": 434 + }, + { + "sha256": "01a4cf8d53daf0e139e6c7e79716d8c28588392bbd139ef8d7a00bedd4256c65", + "states": 210 + }, + { + "sha256": "9c35c79590f9f52843773535fb5c626cd0f35646d209e3da9eb55be498c8dc2e", + "states": 87 + }, + { + "sha256": "16494269b9fd32ea03889ec9c3a5126ba4f0b4b310004accfb1d6010f5f025d9", + "states": 30 + }, + { + "sha256": "66567fe79f950d7ce9ee86103d31843d2745bd5b36333ab94881d9a284d3102e", + "states": 7 + }, + { + "sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "states": 0 + }, + { + "sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "states": 0 + } + ], + "minimum": null, + "total_states": 2455, + "witness": null + }, + "form_r_maximum": 10, + "indices": [ + 0, + 1, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11 + ], + "minimum_interior_for_eleven": 1, + "omitted": 2, + "ten_line": { + "indices": [ + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10 + ], + "witness": [ + [ + 4, + 3, + 6 + ], + [ + 1, + 2, + 2 + ], + [ + 0, + 2, + 3 + ], + [ + 2, + 2, + 3 + ], + [ + 7, + 4, + 4 + ], + [ + 3, + 4, + 4 + ], + [ + 5, + 1, + 1 + ], + [ + 6, + 1, + 1 + ], + [ + 8, + 4, + 4 + ], + [ + 9, + 1, + 1 + ] + ] + } + }, + { + "extended": { + "layers": [ + { + "sha256": "aef05bc773ac0f897e8392244fa252f92162fdd97ac882dd81a5fbd36cf49b7c", + "states": 1 + }, + { + "sha256": "154d42a23ba4090fb7350eb3f1937773b5482729eb0eb82d0bb6f1e0d062b668", + "states": 55 + }, + { + "sha256": "5fd9101e8d7d8cf31580d38d046a08d84ccf0337887f09fd90d3fd32b1da3169", + "states": 458 + }, + { + "sha256": "cb8881ddd8397b4bd59350ce1bbd756fbbcb2ba6a078abb1b29b33189516685c", + "states": 954 + }, + { + "sha256": "1fd8c9e2088375d704978ace4dfc563ccb508f84e0b0a1145db209fb18dc2c57", + "states": 952 + }, + { + "sha256": "924e1c43a4ba87f41a9a39c4fbeb72523398847fcf40818c9d7465e17dd397cc", + "states": 626 + }, + { + "sha256": "826f0309a84b464db4beed39a77465a1b2e90505c9404b56bf1a8d9d0562b997", + "states": 348 + }, + { + "sha256": "194da76b3d3f0bffc52e7b4a6c63b10c3613e0488ad64ff2435c30934ca42a45", + "states": 167 + }, + { + "sha256": "46c5447430e5dbcacff73201f98f14e0fa8a9f26ea1575a6bafa4255934fe3a8", + "states": 56 + }, + { + "sha256": "21ae33970fb32b96a4a00b08d2ae3ece13582084a89b81874683f559feb8897a", + "states": 18 + }, + { + "sha256": "e19ea5b64d229d3c66cb64fdf95c8c7d3f77f8fd292c14b5c2f3f90155bdfa01", + "states": 4 + }, + { + "sha256": "7e96535d62bca620b7133b2e293dea97b5848d810933b35edb45e7ae7efdeef6", + "states": 1 + } + ], + "minimum": 1, + "total_states": 3640, + "witness": [ + [ + 0, + 5, + 6 + ], + [ + 1, + 5, + 3 + ], + [ + 3, + 1, + 1 + ], + [ + 4, + 1, + 5 + ], + [ + 9, + 1, + 5 + ], + [ + 2, + 4, + 4 + ], + [ + 5, + 7, + 2 + ], + [ + 8, + 2, + 6 + ], + [ + 6, + 4, + 4 + ], + [ + 7, + 2, + 2 + ], + [ + 10, + 2, + 2 + ] + ] + }, + "form_r_exclusion": { + "layers": [ + { + "sha256": "aef05bc773ac0f897e8392244fa252f92162fdd97ac882dd81a5fbd36cf49b7c", + "states": 1 + }, + { + "sha256": "99facbec77355f83428c52ddccda146795371a875291f75c2535ccc204ae3023", + "states": 44 + }, + { + "sha256": "5fa22016bf54d1f5865073fe4a91677bd077b4288b53a95c189ae054750316b2", + "states": 338 + }, + { + "sha256": "cb30af05576ac5c8fb8a2891ce59feb09e939d4070f321be4832f08e901dc438", + "states": 652 + }, + { + "sha256": "6f738fe6dcb13bc53383bc78c78c3976af9301b15bf4e3cebd830d379fdc303c", + "states": 652 + }, + { + "sha256": "921d1a3a726358bc21d300a04442bad068688efc814ae53c817922de029a0e63", + "states": 434 + }, + { + "sha256": "97ef8a3d32e9958df0681091717dbef2c104a6b6ed5f9ca3c35dea1a14f86e85", + "states": 210 + }, + { + "sha256": "ade405894ac0613396ec70309bb7ae9d30df643107aa3960fae195e66ab62509", + "states": 87 + }, + { + "sha256": "b9ce043580b75e8b315d55b8ce8b3a732515996ec71b78f6ba0f8ad261b78eba", + "states": 30 + }, + { + "sha256": "c2417f03d275f20ec42beedfb03f67543e5a3a58aa19e7d122245a6f0e93ab0e", + "states": 7 + }, + { + "sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "states": 0 + }, + { + "sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "states": 0 + } + ], + "minimum": null, + "total_states": 2455, + "witness": null + }, + "form_r_maximum": 10, + "indices": [ + 0, + 1, + 2, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11 + ], + "minimum_interior_for_eleven": 1, + "omitted": 3, + "ten_line": { + "indices": [ + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10 + ], + "witness": [ + [ + 0, + 1, + 1 + ], + [ + 1, + 1, + 1 + ], + [ + 5, + 3, + 5 + ], + [ + 2, + 1, + 3 + ], + [ + 7, + 4, + 4 + ], + [ + 3, + 4, + 4 + ], + [ + 4, + 2, + 2 + ], + [ + 6, + 2, + 2 + ], + [ + 8, + 4, + 4 + ], + [ + 9, + 2, + 2 + ] + ] + } + }, + { + "extended": { + "layers": [ + { + "sha256": "7adbd8f4037db9b8f01b49c9de116bbcaa5d34f9e8cad3c4a80aa1ee1860ed77", + "states": 1 + }, + { + "sha256": "7f5f02981286eb5b0ac757ccc6d1cccb355e1e6adab50c240e28021fe47fdd19", + "states": 55 + }, + { + "sha256": "e29644d7f2f82523f6caf165ebab01c9d250ac1c8c4961365c162f964c34f7d6", + "states": 458 + }, + { + "sha256": "88c0514a1def438db7c487cc079455dbab0192e184f1da3fbed3742d0ed13486", + "states": 954 + }, + { + "sha256": "46fb2fd12a3e79cf9d6c740055a216fc60310fbe95d5ee92ea319747f24e0588", + "states": 952 + }, + { + "sha256": "62e80457736e546b7553a64438a51d534dcf36c52a1ae43fed1a8c56f43f5dde", + "states": 626 + }, + { + "sha256": "2d14d0436ca6f7e020e6cc356f2636770e44d621d3fc3943491a6eabaaa54eb9", + "states": 348 + }, + { + "sha256": "4c1d3db9d4e83c94a0a45857c7150c2330ce88ed4c8d9ab3827692ccc82ca47d", + "states": 167 + }, + { + "sha256": "f5950189b7373bee8a82a3ac0825138c465d2e7513f6b72dd7bf1a36dcaba4bd", + "states": 56 + }, + { + "sha256": "a1ae4be40d3100c528c507606877800260fd22e31d6c60e0bdb287b6fed26eea", + "states": 18 + }, + { + "sha256": "427ec887524b1ebafab3b1dbb20205892666580fe4123614ca74c7328307f433", + "states": 4 + }, + { + "sha256": "7e96535d62bca620b7133b2e293dea97b5848d810933b35edb45e7ae7efdeef6", + "states": 1 + } + ], + "minimum": 1, + "total_states": 3640, + "witness": [ + [ + 3, + 4, + 4 + ], + [ + 1, + 7, + 1 + ], + [ + 5, + 5, + 6 + ], + [ + 7, + 5, + 3 + ], + [ + 10, + 2, + 3 + ], + [ + 0, + 2, + 2 + ], + [ + 4, + 4, + 5 + ], + [ + 9, + 4, + 5 + ], + [ + 2, + 1, + 1 + ], + [ + 6, + 1, + 1 + ], + [ + 8, + 2, + 2 + ] + ] + }, + "form_r_exclusion": { + "layers": [ + { + "sha256": "7adbd8f4037db9b8f01b49c9de116bbcaa5d34f9e8cad3c4a80aa1ee1860ed77", + "states": 1 + }, + { + "sha256": "08ac33cb6ecb8a8eb8885cd4b8052f56af38d953f6e65594cb2c28617daa6710", + "states": 44 + }, + { + "sha256": "21d27373b0e8f6f8e69f8ca5747d00706f95e6f7ac2caed510685cf5ba27caf0", + "states": 338 + }, + { + "sha256": "864a00a69957bdf361a86dc2859b2e59c32a81c67375bfd7d4d000eae800048e", + "states": 652 + }, + { + "sha256": "54fea65561c8d3071730514f5b1382c2608e931128709b284db895f3155b60de", + "states": 652 + }, + { + "sha256": "b1b4431ed4c66adefb6af3ab0ea0ef36ac2bacab3465a9d959cfc3a12ab3cd0e", + "states": 434 + }, + { + "sha256": "29a0c13264b5770415560570168b4348fa7ff32ea657ce33c241e092bf58c556", + "states": 210 + }, + { + "sha256": "5c34a562d12829693326ccf11928843f9e3b092a78bbdc04ef64ba4c180cefd6", + "states": 87 + }, + { + "sha256": "564567290b21582da0b5b72cb0e62814bba2f2a13556965fe76ddabd0a794ef8", + "states": 30 + }, + { + "sha256": "41bec06942da77691dc5176987a2978448708adb0f88a25ad6b36490454ca4d2", + "states": 7 + }, + { + "sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "states": 0 + }, + { + "sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "states": 0 + } + ], + "minimum": null, + "total_states": 2455, + "witness": null + }, + "form_r_maximum": 10, + "indices": [ + 0, + 1, + 2, + 3, + 5, + 6, + 7, + 8, + 9, + 10, + 11 + ], + "minimum_interior_for_eleven": 1, + "omitted": 4, + "ten_line": { + "indices": [ + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10 + ], + "witness": [ + [ + 8, + 6, + 5 + ], + [ + 0, + 1, + 1 + ], + [ + 1, + 1, + 1 + ], + [ + 2, + 4, + 6 + ], + [ + 3, + 4, + 4 + ], + [ + 4, + 4, + 6 + ], + [ + 5, + 1, + 1 + ], + [ + 7, + 2, + 2 + ], + [ + 6, + 2, + 2 + ], + [ + 9, + 2, + 2 + ] + ] + } + }, + { + "extended": { + "layers": [ + { + "sha256": "937db6789d25f6cf6f6e3fc42a00de91d06f41724d54b26e5fb6761f12a82382", + "states": 1 + }, + { + "sha256": "8200c8a57c37b54ea4a68406ac63d5910e0ee853b1e0fce73109e316573a7d1d", + "states": 55 + }, + { + "sha256": "bfe2ff2563501f037e5cc66023b40a6331b0404c4d5eddd3d90466db7babd998", + "states": 458 + }, + { + "sha256": "b16842009810b8d8f8441b02ac0cf2206beac6ae7ea447eb15d2600528f2859e", + "states": 954 + }, + { + "sha256": "418e54e995e90190c2581c85a82e6ee5ce25f9c855f4c60efa38a5c81de74ca0", + "states": 952 + }, + { + "sha256": "e63869491c86b9fd799f097f80bace7304fe0aca520744a3ed78e933e2c12ba5", + "states": 626 + }, + { + "sha256": "0a69476fdf3f6513751a52bd1753af1493b8b236bff8f7eb34a5c8f4840690c1", + "states": 348 + }, + { + "sha256": "5c512373e66eaf37dbff1646a0462853bc72f8674735a8694df8e40e7fe5f260", + "states": 167 + }, + { + "sha256": "447e32510296c639e814793f16daf7a58738bb17f0a02eae722f9223abbafdf4", + "states": 56 + }, + { + "sha256": "f7fe6ac008549f144a986060d05b860f5984c94cfc18336b0e27b67754e10a21", + "states": 18 + }, + { + "sha256": "999855480b5fdf153f32c1f0dca74593dda3e2bd9641a8b9da27dfaa3ffc92e1", + "states": 4 + }, + { + "sha256": "7e96535d62bca620b7133b2e293dea97b5848d810933b35edb45e7ae7efdeef6", + "states": 1 + } + ], + "minimum": 1, + "total_states": 3640, + "witness": [ + [ + 3, + 2, + 2 + ], + [ + 1, + 6, + 3 + ], + [ + 4, + 2, + 2 + ], + [ + 5, + 2, + 6 + ], + [ + 0, + 4, + 4 + ], + [ + 2, + 4, + 4 + ], + [ + 9, + 7, + 1 + ], + [ + 6, + 1, + 5 + ], + [ + 7, + 1, + 1 + ], + [ + 8, + 4, + 4 + ], + [ + 10, + 1, + 1 + ] + ] + }, + "form_r_exclusion": { + "layers": [ + { + "sha256": "937db6789d25f6cf6f6e3fc42a00de91d06f41724d54b26e5fb6761f12a82382", + "states": 1 + }, + { + "sha256": "1381b0dc75ba6e120880308126d570150cf98b0936ffac37ae8eb222d593b09b", + "states": 44 + }, + { + "sha256": "8c0e3e590829082851d6f566c343dce50311d3e90db46f79e204ebdaa76624c4", + "states": 338 + }, + { + "sha256": "637b73e10d1f345271afba5943956e44de8497e8a58fb079c84f084c3280684c", + "states": 652 + }, + { + "sha256": "3b7a8af107df514293c29c4cacef96297226817862796d3f96413d5ae0e24d5c", + "states": 652 + }, + { + "sha256": "fd0332937df66df9fc5b6a19e5379ac1ecfa534cd88156cd9137d9128846e720", + "states": 434 + }, + { + "sha256": "9c3f793eb3e3a39aa2b2c4db28100bd8e510d14fc4c54c1bd8e2cc8b14d0f445", + "states": 210 + }, + { + "sha256": "9a60b1d50a290277ed259a88a2ae94e5a61ab6f6478090b32f6ca0b2ee7300f5", + "states": 87 + }, + { + "sha256": "f69b0cbb2ddd3e7e692f6fedc4e02bd18c10349968eb940d34b464b772e372d6", + "states": 30 + }, + { + "sha256": "de62453b8cc0299bc11940cdc79346bc252f7a1547a273f65b593e21b1cacac0", + "states": 7 + }, + { + "sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "states": 0 + }, + { + "sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "states": 0 + } + ], + "minimum": null, + "total_states": 2455, + "witness": null + }, + "form_r_maximum": 10, + "indices": [ + 0, + 1, + 2, + 3, + 4, + 6, + 7, + 8, + 9, + 10, + 11 + ], + "minimum_interior_for_eleven": 1, + "omitted": 5, + "ten_line": { + "indices": [ + 0, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10 + ], + "witness": [ + [ + 0, + 4, + 4 + ], + [ + 1, + 4, + 4 + ], + [ + 7, + 5, + 6 + ], + [ + 2, + 2, + 2 + ], + [ + 3, + 2, + 2 + ], + [ + 4, + 2, + 2 + ], + [ + 5, + 4, + 5 + ], + [ + 8, + 1, + 1 + ], + [ + 6, + 1, + 1 + ], + [ + 9, + 1, + 1 + ] + ] + } + }, + { + "extended": { + "layers": [ + { + "sha256": "d04c0b46f38da7468508298800ba5d9206390693f7df337971844a7bfb7fe36d", + "states": 1 + }, + { + "sha256": "2209550696414ed728d67a1a1a473462ee61fd0f332110d3ab4554fbc89b453e", + "states": 55 + }, + { + "sha256": "82c9490c23a0da3616a885146e4ec2b51355e024f25349a30f0337523bd374b4", + "states": 458 + }, + { + "sha256": "21e52de9794e2a7791e977a3345f3baa77dd12cdc9742eecf39a96cb13e53423", + "states": 954 + }, + { + "sha256": "54e13774e55ac12ca86929f0e66ece9933ee63cc3be02c180f20d9549bb8cc52", + "states": 952 + }, + { + "sha256": "619dccf725b74f31f883d069520600bcfb79c0284c70abe80a4981eaaadf8cf2", + "states": 626 + }, + { + "sha256": "ad35ad41c7ebf70cb8fa6ce8e96d27a5608783fda78f6028d051dc7a955014d5", + "states": 348 + }, + { + "sha256": "c228af130a45f70c6dc527d1c65213665aefd877a1d150fcae6e047c14548c7d", + "states": 167 + }, + { + "sha256": "88b4a6bdb21e2879beb05b09a21734c5e4f14a48220c441de16295eae7e227cd", + "states": 56 + }, + { + "sha256": "2bb3b5c5242856ba1f5a5a30cc4588c87cdee3cbd88e4a52ca7ce3a23b809050", + "states": 18 + }, + { + "sha256": "45dfc12e057e602cc36ac6f824da1ca2563d44f0707d9b0024d1af7860691ff3", + "states": 4 + }, + { + "sha256": "7e96535d62bca620b7133b2e293dea97b5848d810933b35edb45e7ae7efdeef6", + "states": 1 + } + ], + "minimum": 1, + "total_states": 3640, + "witness": [ + [ + 0, + 3, + 6 + ], + [ + 7, + 1, + 3 + ], + [ + 3, + 7, + 4 + ], + [ + 10, + 5, + 3 + ], + [ + 1, + 2, + 2 + ], + [ + 2, + 1, + 5 + ], + [ + 8, + 5, + 6 + ], + [ + 4, + 2, + 2 + ], + [ + 6, + 1, + 5 + ], + [ + 5, + 4, + 4 + ], + [ + 9, + 4, + 4 + ] + ] + }, + "form_r_exclusion": { + "layers": [ + { + "sha256": "d04c0b46f38da7468508298800ba5d9206390693f7df337971844a7bfb7fe36d", + "states": 1 + }, + { + "sha256": "e1ce9653e3035797ddf9926e6f39c0392f85a03fb5e60db9fad4e9db361e56ea", + "states": 44 + }, + { + "sha256": "b146b2abb45f2b51a4f5f2f5cffe4f31172e42104fd5c84433457c73db418556", + "states": 338 + }, + { + "sha256": "c6d9a837a57a3d29ab40ab6b4ac7f819fe3c7fd766517039a816b60a383c3530", + "states": 652 + }, + { + "sha256": "075373406d40e16866ac81e72ba4311d4473cea6083be072af0abfb9dad20c28", + "states": 652 + }, + { + "sha256": "a047845b349b6b0996a55782a007b30b5bc6f87df5e893eb72d60917566e30ac", + "states": 434 + }, + { + "sha256": "917956de4eb499816d509d2dddc41f1ec945246cb578d4b958439c386180c2da", + "states": 210 + }, + { + "sha256": "f3bc295f84a7f29cfde39244c521cf64a4d8bcc8bb2d9f4694d16be65be767ab", + "states": 87 + }, + { + "sha256": "a2ac11dbbafe95c0f9327c5b13bff398ec12c5ff93f9effc09e0c24164e1f0e1", + "states": 30 + }, + { + "sha256": "3d05ac0650f5a5e426e17cdb9dfacdedd421ade519ae3d8771f0306a95c99eab", + "states": 7 + }, + { + "sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "states": 0 + }, + { + "sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "states": 0 + } + ], + "minimum": null, + "total_states": 2455, + "witness": null + }, + "form_r_maximum": 10, + "indices": [ + 0, + 1, + 2, + 3, + 4, + 5, + 7, + 8, + 9, + 10, + 11 + ], + "minimum_interior_for_eleven": 1, + "omitted": 6, + "ten_line": { + "indices": [ + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10 + ], + "witness": [ + [ + 0, + 1, + 1 + ], + [ + 1, + 1, + 1 + ], + [ + 2, + 5, + 6 + ], + [ + 3, + 5, + 3 + ], + [ + 5, + 1, + 5 + ], + [ + 4, + 4, + 4 + ], + [ + 7, + 2, + 2 + ], + [ + 6, + 2, + 2 + ], + [ + 8, + 4, + 4 + ], + [ + 9, + 2, + 2 + ] + ] + } + }, + { + "extended": { + "layers": [ + { + "sha256": "8866a2a575b0147a06be2450faae210e7efbf435e7a68fa46df0a1aa24680ba5", + "states": 1 + }, + { + "sha256": "72ef697a294b94999ee2d4f30bcd11dbb174b5348a0b70fd478fb812e67511a9", + "states": 55 + }, + { + "sha256": "9f5f2e520987c9bd855780d25bbdecbb3fb9b66f9b7412fe3a02978726414b4a", + "states": 458 + }, + { + "sha256": "e62472f84dfe56fe4a764d69689341a95704716eac68eacbfc4c255408cfa129", + "states": 954 + }, + { + "sha256": "07550069db4782541a56aeb68a4b3aa56e64bc597cf420ed3ff092dce6a30c24", + "states": 952 + }, + { + "sha256": "15ebb123445ac82fde61323d320ff8bf16119756a8cf4a623c7208a9a44e9847", + "states": 626 + }, + { + "sha256": "c3e45738bc5089d669604eb056aed027dbae336671160c072949a3a3f7f57807", + "states": 348 + }, + { + "sha256": "3e86492ecebb567609539d6893ffe4f186327fbbd0780821489263f2f994c9c1", + "states": 167 + }, + { + "sha256": "449987cc195df43edbcbf8bc3bae2a0b22a3704396561829c601f8334c68e8c3", + "states": 56 + }, + { + "sha256": "73593cff222466c934d1998c539840b2e52a0d3d24173b19dd0a9fa5cdc4d6cd", + "states": 18 + }, + { + "sha256": "bb9d57d1349c7ef5134b534eafa0715099c0fea2cfc6d6519efe1224de636a02", + "states": 4 + }, + { + "sha256": "7e96535d62bca620b7133b2e293dea97b5848d810933b35edb45e7ae7efdeef6", + "states": 1 + } + ], + "minimum": 1, + "total_states": 3640, + "witness": [ + [ + 6, + 2, + 2 + ], + [ + 2, + 7, + 1 + ], + [ + 3, + 3, + 6 + ], + [ + 5, + 3, + 5 + ], + [ + 9, + 4, + 5 + ], + [ + 0, + 4, + 4 + ], + [ + 7, + 2, + 3 + ], + [ + 10, + 2, + 3 + ], + [ + 1, + 1, + 1 + ], + [ + 4, + 1, + 1 + ], + [ + 8, + 4, + 4 + ] + ] + }, + "form_r_exclusion": { + "layers": [ + { + "sha256": "8866a2a575b0147a06be2450faae210e7efbf435e7a68fa46df0a1aa24680ba5", + "states": 1 + }, + { + "sha256": "0f62348548bba4dc5ed04e35eaef81127b163b3c7950ad6905b1f42532a2ac2c", + "states": 44 + }, + { + "sha256": "0373d69bda56ab91ce1cd20a174f4ef08f4b3f5a9028995e375a48c5f7c8d8ac", + "states": 338 + }, + { + "sha256": "213c63e9a1ff75eb6363065a0db40e414f2072502e61e922009a30e65c0a1159", + "states": 652 + }, + { + "sha256": "737d17d0d57f7a0e4d55ee624d7c5e06de25100b27f4563eeefdd9851f0bf430", + "states": 652 + }, + { + "sha256": "9a4ccb7ac86bdea624162081de26f1e2927026acbf37f2c01d88b2bf627f16cd", + "states": 434 + }, + { + "sha256": "3c97373c7e8c6ea4e95deb055f3e1e24134518b77b94b689c001f41af687c8ba", + "states": 210 + }, + { + "sha256": "d8290ebc5c643e5dbd26faeaa444c411a2d38cc9e85fcd3cbf864505c49b6220", + "states": 87 + }, + { + "sha256": "f07e81625231aeef5c85c95ee790fde22ae4003258a63ced5b61d8101813bc6e", + "states": 30 + }, + { + "sha256": "a72cdf61d5d9421e28a7e5b737c431e47504a79a3c8eed4d82bfceddfd0536f0", + "states": 7 + }, + { + "sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "states": 0 + }, + { + "sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "states": 0 + } + ], + "minimum": null, + "total_states": 2455, + "witness": null + }, + "form_r_maximum": 10, + "indices": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 8, + 9, + 10, + 11 + ], + "minimum_interior_for_eleven": 1, + "omitted": 7, + "ten_line": { + "indices": [ + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10 + ], + "witness": [ + [ + 8, + 6, + 5 + ], + [ + 0, + 1, + 1 + ], + [ + 1, + 1, + 1 + ], + [ + 2, + 4, + 6 + ], + [ + 3, + 1, + 1 + ], + [ + 4, + 4, + 4 + ], + [ + 5, + 4, + 6 + ], + [ + 7, + 2, + 2 + ], + [ + 6, + 2, + 2 + ], + [ + 9, + 2, + 2 + ] + ] + } + }, + { + "extended": { + "layers": [ + { + "sha256": "52d1fcef9d5f0f1c4e095c0b90f74bdbc3c3f768fea094ff824db3514b7c7606", + "states": 1 + }, + { + "sha256": "192f3604009d30d7060121cab081260c3bd32c312df43c8a519819cd1a522c65", + "states": 55 + }, + { + "sha256": "91423e8eb41f34c788d9edd977beb076c95ce7b28ecdd6a9fd4671b779256a94", + "states": 458 + }, + { + "sha256": "7941e663814cd432d13c0625878724ff020ac048ca0df3266e1365a1c9271b69", + "states": 954 + }, + { + "sha256": "3cc587352134871f039ddf8aad31238623da90c9771ea06481909957115984a2", + "states": 952 + }, + { + "sha256": "ea0d60c5709eea112f5d8a56c2a151b867fe66258431ba620a0551e7639dbd56", + "states": 626 + }, + { + "sha256": "d1c745da8f3093714863c100eb81639bffc5fa0ae4bb1af386e0c196d699f366", + "states": 348 + }, + { + "sha256": "94c7ae705f7ec4789aff7bf6b538994b5fc34f3ac7c073cd226c600c708e6d3d", + "states": 167 + }, + { + "sha256": "344c4cd46d22dd34869e9290e42810bd0d157008732f5b7f52758ec913c42fcd", + "states": 56 + }, + { + "sha256": "1b5f6f691d7b2a2f9090e5304a0bb18fc96e4ce08bc43cee01b02b4d8ef21574", + "states": 18 + }, + { + "sha256": "3625e31f20902889d239f9a74fb8222f1c0576acbf059dc1cbe3f33d143bab34", + "states": 4 + }, + { + "sha256": "7e96535d62bca620b7133b2e293dea97b5848d810933b35edb45e7ae7efdeef6", + "states": 1 + } + ], + "minimum": 1, + "total_states": 3640, + "witness": [ + [ + 3, + 5, + 6 + ], + [ + 10, + 7, + 2 + ], + [ + 6, + 4, + 6 + ], + [ + 0, + 2, + 2 + ], + [ + 1, + 2, + 3 + ], + [ + 2, + 4, + 5 + ], + [ + 4, + 5, + 3 + ], + [ + 7, + 4, + 5 + ], + [ + 5, + 1, + 1 + ], + [ + 8, + 2, + 2 + ], + [ + 9, + 1, + 1 + ] + ] + }, + "form_r_exclusion": { + "layers": [ + { + "sha256": "52d1fcef9d5f0f1c4e095c0b90f74bdbc3c3f768fea094ff824db3514b7c7606", + "states": 1 + }, + { + "sha256": "987c13767ddba3b8a5f9d4e887cf056eb413f2b84a738f523f9a8d01aeba74a6", + "states": 44 + }, + { + "sha256": "8205bb201d29f70013e9e8c949f06410ab70b57fc5bf9efaab06c990dd6cae77", + "states": 338 + }, + { + "sha256": "375c6cac22f4a2a682df6e3b860a88bbee32517406e5adf83c53c7856009e402", + "states": 652 + }, + { + "sha256": "dfe5b660740da9e5b2625b36973ba3865e9c2e0f44f4eec14c5d6439c0e5496b", + "states": 652 + }, + { + "sha256": "45bbbee2df0886a3fed5ccc3609ba3f33b700d7b8c638bc1786beebd1ba46dc5", + "states": 434 + }, + { + "sha256": "e2f804ef99e8cb587405d942280ee4980b097aca0f1fd3f59b91e7b8b3218d79", + "states": 210 + }, + { + "sha256": "c5690b9e088ab310d338f74748286e771c12e57df39e1924fecb63f1a0500a0a", + "states": 87 + }, + { + "sha256": "6d445c9c1d7b3b9cfbb8be1a32288bcfa001f7a5a162422e0f3f8d62d9b6d2af", + "states": 30 + }, + { + "sha256": "f885952e79fdf7b2c547add4e9099d54a4c2e9950bcc5f1f630ddf4e7007c5f8", + "states": 7 + }, + { + "sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "states": 0 + }, + { + "sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "states": 0 + } + ], + "minimum": null, + "total_states": 2455, + "witness": null + }, + "form_r_maximum": 10, + "indices": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 9, + 10, + 11 + ], + "minimum_interior_for_eleven": 1, + "omitted": 8, + "ten_line": { + "indices": [ + 0, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10 + ], + "witness": [ + [ + 2, + 5, + 6 + ], + [ + 3, + 5, + 3 + ], + [ + 9, + 2, + 2 + ], + [ + 0, + 2, + 2 + ], + [ + 5, + 4, + 4 + ], + [ + 1, + 4, + 5 + ], + [ + 6, + 4, + 5 + ], + [ + 4, + 1, + 1 + ], + [ + 7, + 2, + 2 + ], + [ + 8, + 1, + 1 + ] + ] + } + }, + { + "extended": { + "layers": [ + { + "sha256": "ada0ab144e28e0bd1f73ac0f2637f9a43697836d845c15ddd9ea89b21b98332d", + "states": 1 + }, + { + "sha256": "b4d67f5eb9af2616413dcc7b7b806eb137b5d3c345bba57e51691b27ddc323ee", + "states": 55 + }, + { + "sha256": "b2db2d7e48c185e19f55d4df072de96b28d186b305d259188984e2e5b18254fc", + "states": 458 + }, + { + "sha256": "4b6992c3ab6ea57263255b3c4256501ababd8276b9c9b9087112c5fa738d543c", + "states": 954 + }, + { + "sha256": "5b6b709a3ddf1bdc538244e69b519f167d2f3e373eb601e2e260278418c8411a", + "states": 952 + }, + { + "sha256": "9a5d716ffbb1772133b5e2da29bd8b1e068168eaa395887708e30b0d7888ec7a", + "states": 626 + }, + { + "sha256": "2e2174545c7395452bcf3725784364136afb9c46c2962710bbe537361d156b15", + "states": 348 + }, + { + "sha256": "900b1a08a1703842324227768e0751f7bb0df271e005530347752a1fd6aac972", + "states": 167 + }, + { + "sha256": "2bee6b6ca061d025d4776caea156874762c4f8b6c03641d84896fbc3e8423478", + "states": 56 + }, + { + "sha256": "5a23b3bd34e196530a7b27a43b29e5f9c237a84c90aa4e6fb50090c8fdbc3f2c", + "states": 18 + }, + { + "sha256": "08052b8a0850c563a597fbc4098e3719b9007bcbc85638a8fd2eaf91e0cdb40d", + "states": 4 + }, + { + "sha256": "7e96535d62bca620b7133b2e293dea97b5848d810933b35edb45e7ae7efdeef6", + "states": 1 + } + ], + "minimum": 1, + "total_states": 3640, + "witness": [ + [ + 0, + 7, + 2 + ], + [ + 6, + 5, + 6 + ], + [ + 3, + 3, + 6 + ], + [ + 8, + 5, + 3 + ], + [ + 10, + 1, + 3 + ], + [ + 1, + 2, + 2 + ], + [ + 5, + 1, + 5 + ], + [ + 9, + 1, + 5 + ], + [ + 2, + 4, + 4 + ], + [ + 4, + 2, + 2 + ], + [ + 7, + 4, + 4 + ] + ] + }, + "form_r_exclusion": { + "layers": [ + { + "sha256": "ada0ab144e28e0bd1f73ac0f2637f9a43697836d845c15ddd9ea89b21b98332d", + "states": 1 + }, + { + "sha256": "c8cbde09f2f6a6c84640382638f90e36a496e238df1391e214acd61d962c50cf", + "states": 44 + }, + { + "sha256": "d053e2d1015515e331320729e039042c542ac60b700e7161799170959078dd47", + "states": 338 + }, + { + "sha256": "102cdc466fdd074e44c688e5e02274d04a48cb77158471090fce7f2cf043d505", + "states": 652 + }, + { + "sha256": "89fef43a458c111fad3050e4b3cdb34d4b9e1ca0ff4c12895704caae7c9b7c7c", + "states": 652 + }, + { + "sha256": "e025cfb8439c2514118bb0b827a2ad39a11fa698c3527df53d1ac4bd61a884bc", + "states": 434 + }, + { + "sha256": "3b00d86361ec994ca45d8ddd1bc812952d9263e424374527c2af5f6f25f9df23", + "states": 210 + }, + { + "sha256": "d2b28269034f4d79da80d7d425efc0ae0c68b43d278885279e8781622958a893", + "states": 87 + }, + { + "sha256": "fa028b8ab5be481284c3868cc3310c99c98574c42bea6e739cb9d4e8dd7580ce", + "states": 30 + }, + { + "sha256": "43b5097d60cffbc70f6689fbdc65e1200fce10b95847fe106d5c6bbe650899da", + "states": 7 + }, + { + "sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "states": 0 + }, + { + "sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "states": 0 + } + ], + "minimum": null, + "total_states": 2455, + "witness": null + }, + "form_r_maximum": 10, + "indices": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 10, + 11 + ], + "minimum_interior_for_eleven": 1, + "omitted": 9, + "ten_line": { + "indices": [ + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10 + ], + "witness": [ + [ + 0, + 1, + 1 + ], + [ + 1, + 1, + 1 + ], + [ + 2, + 5, + 6 + ], + [ + 3, + 5, + 3 + ], + [ + 6, + 1, + 5 + ], + [ + 4, + 4, + 4 + ], + [ + 5, + 2, + 2 + ], + [ + 7, + 2, + 2 + ], + [ + 8, + 4, + 4 + ], + [ + 9, + 2, + 2 + ] + ] + } + }, + { + "extended": { + "layers": [ + { + "sha256": "79687159f66072217be6d18e9a17c0677d5b82fa79746081d2fedc990608a304", + "states": 1 + }, + { + "sha256": "2c6958b580aa8f18f8508e2eec70f3a0990197f7fc28c135f3e130d1063b32fb", + "states": 55 + }, + { + "sha256": "c3f91980bc61eff87c881bbb08bf3d318d4dbdce462e03f11045a8c6ac56e27b", + "states": 458 + }, + { + "sha256": "1f6fc92423dab3666391c34a4e051130b4eee9ce458db6b1824a24f382cd0c74", + "states": 954 + }, + { + "sha256": "64d4ca4ca54114348bd7fdfeaa99c1f97021d333874e3ef230afed69b208d1a9", + "states": 952 + }, + { + "sha256": "e326f393af097e7d62cc44296804216db6220e901fafdf4ef336a9f47d51a47e", + "states": 626 + }, + { + "sha256": "b7ca23c10b23bc9702e80a916820d40e7e9efc4b5431945de0223d4f8ac4a41b", + "states": 348 + }, + { + "sha256": "c7501273ba5aa3ea09ca7ce5200640541d870383a0a0dd6d745d8eb9388e74a8", + "states": 167 + }, + { + "sha256": "6cec7c8cc49db9c27923844a05196c99827042ffa51364098d4db62f7203a036", + "states": 56 + }, + { + "sha256": "7f99abdb3fb0535ed188534b9420ffc3a3aed9eab87f1f7877f79d54b591ef19", + "states": 18 + }, + { + "sha256": "b44e96d470050dcfaba8de7e327f6351a24a26ddc400feb3487db117e555d060", + "states": 4 + }, + { + "sha256": "7e96535d62bca620b7133b2e293dea97b5848d810933b35edb45e7ae7efdeef6", + "states": 1 + } + ], + "minimum": 1, + "total_states": 3640, + "witness": [ + [ + 0, + 3, + 6 + ], + [ + 7, + 1, + 1 + ], + [ + 2, + 3, + 5 + ], + [ + 8, + 1, + 3 + ], + [ + 10, + 1, + 3 + ], + [ + 1, + 2, + 2 + ], + [ + 4, + 7, + 2 + ], + [ + 9, + 2, + 6 + ], + [ + 3, + 4, + 4 + ], + [ + 5, + 4, + 4 + ], + [ + 6, + 4, + 4 + ] + ] + }, + "form_r_exclusion": { + "layers": [ + { + "sha256": "79687159f66072217be6d18e9a17c0677d5b82fa79746081d2fedc990608a304", + "states": 1 + }, + { + "sha256": "9abc33927f7cbc0e4ba1e3e15992ff980196cc2de8003001ccaec001ccb0c6f0", + "states": 44 + }, + { + "sha256": "9814e32b5819723ca172e6aec4b277695a795ea4ca81e57075f1f28226bc298a", + "states": 338 + }, + { + "sha256": "223f493a48452328e24a5aa60209ffab9b69e18a8cc19c03a89df641a699c5c4", + "states": 652 + }, + { + "sha256": "4128bd5d0aea5b90ba5e678c0b299a959b34b4a93718d362763209cbdb111d9c", + "states": 652 + }, + { + "sha256": "28aeba15ba3d9a1b37c951fb8f834cd153984e7b115d2d60b900ecbc90acfcf9", + "states": 434 + }, + { + "sha256": "127b054d0a33cea78fdd6a61b092941d40e24ff2d4d3258028619e9298f16598", + "states": 210 + }, + { + "sha256": "11c3eb0f2667cc47684f125306010daeb6ce9283ba53abb6d718919894423b1f", + "states": 87 + }, + { + "sha256": "881ba5081266ef1282123abfe9f74fe8bf9896224e501272f509913c6a77f49d", + "states": 30 + }, + { + "sha256": "7ad9bc1f862b2579467ed2bcad09e852b285f23ec30fdf418382648826d93922", + "states": 7 + }, + { + "sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "states": 0 + }, + { + "sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "states": 0 + } + ], + "minimum": null, + "total_states": 2455, + "witness": null + }, + "form_r_maximum": 10, + "indices": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 11 + ], + "minimum_interior_for_eleven": 1, + "omitted": 10, + "ten_line": { + "indices": [ + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10 + ], + "witness": [ + [ + 0, + 1, + 1 + ], + [ + 1, + 1, + 1 + ], + [ + 2, + 5, + 6 + ], + [ + 3, + 5, + 3 + ], + [ + 6, + 1, + 5 + ], + [ + 4, + 4, + 4 + ], + [ + 5, + 4, + 4 + ], + [ + 8, + 2, + 2 + ], + [ + 7, + 2, + 2 + ], + [ + 9, + 2, + 2 + ] + ] + } + }, + { + "extended": { + "layers": [ + { + "sha256": "3d416ab95fca936b7d35b4bbb01f0a1f7f89a6bab0048eedeeeaa5e8ef6e417d", + "states": 1 + }, + { + "sha256": "1505ef8e2b0105a4c9a5f5ccce8646d3749403d6b9eaf7e58c98c774ce8f034c", + "states": 55 + }, + { + "sha256": "2f2bfd4cd3ffc3da513a063fb5761cae594282beb06666f40d5f060e1f67c5ff", + "states": 458 + }, + { + "sha256": "13775e8dff2258adca4dc3ba1d6a04e252b9d0c551fcfa3bbf5ac69ffdc9c8ca", + "states": 954 + }, + { + "sha256": "136d040993e9de195813364bbbd143791c64a7182d6a71badd4745da2318a3ba", + "states": 952 + }, + { + "sha256": "da3e336af1efaa4c7a36d6fe33cec981e9efd0c837a1e5fd91a9b6c59f2c04e9", + "states": 626 + }, + { + "sha256": "0257a470bd6459f8b08f002a2960df0a6594804053a48ee0a1dfde2801414854", + "states": 348 + }, + { + "sha256": "118711985c01aa0053f2fca2846da4bc6e46e9b551f5c75879be3e03c2ec4ab7", + "states": 167 + }, + { + "sha256": "c7ffed828b4ba4e96d57f9aa2cb9e2efb5eba503c69dc92b10c511c0ef613502", + "states": 56 + }, + { + "sha256": "7b078ca4cc9c6c875de4ea2684c77debb3e6b3b0770349eb18cd5163163fa01b", + "states": 18 + }, + { + "sha256": "ec7ff91a14936c88b028a349d8370202862143feb526e508793efc51d51b91cb", + "states": 4 + }, + { + "sha256": "7e96535d62bca620b7133b2e293dea97b5848d810933b35edb45e7ae7efdeef6", + "states": 1 + } + ], + "minimum": 1, + "total_states": 3640, + "witness": [ + [ + 0, + 5, + 6 + ], + [ + 1, + 5, + 3 + ], + [ + 8, + 7, + 2 + ], + [ + 5, + 6, + 5 + ], + [ + 10, + 4, + 5 + ], + [ + 2, + 1, + 1 + ], + [ + 9, + 4, + 6 + ], + [ + 3, + 2, + 2 + ], + [ + 4, + 2, + 3 + ], + [ + 6, + 2, + 2 + ], + [ + 7, + 1, + 1 + ] + ] + }, + "form_r_exclusion": { + "layers": [ + { + "sha256": "3d416ab95fca936b7d35b4bbb01f0a1f7f89a6bab0048eedeeeaa5e8ef6e417d", + "states": 1 + }, + { + "sha256": "07ca2b93a24c93e937d1754781b73f5e2a96109422ca1f30871bafdf66864ac4", + "states": 44 + }, + { + "sha256": "c340c1ceba534408570caad8d159a74f13ddfe86534638db23ee369b9008f5b6", + "states": 338 + }, + { + "sha256": "0f0f815117e300f5e75cfe8ea048b21ef5ffc0dd9e7c7c76d403a7a4f19dc1a5", + "states": 652 + }, + { + "sha256": "b011dfb000bb5fe81d82606f8ee4cdf1f222e33d698c8e78e90818f997239cb9", + "states": 652 + }, + { + "sha256": "11dfcb52524b1576fe161c2a1a13803711e4c1373a619afd14a69cf7a341048a", + "states": 434 + }, + { + "sha256": "9ab812161fe8d650fcbf3817f2a3dfe506f1dcebc2dc0282bb298b96dfd9abed", + "states": 210 + }, + { + "sha256": "000b67c86174a20c4d4e5a0876d3a335f9384b10c598314cb4d2fcdc1cd56746", + "states": 87 + }, + { + "sha256": "763050a7253b6bdcee987b0daa7b19280dc6f98b9f28830c821eafd88ee47914", + "states": 30 + }, + { + "sha256": "273ad0e6f39b3e8fb2ef8ae58b677e044dfd09a09d3818f944fd464817e7e25e", + "states": 7 + }, + { + "sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "states": 0 + }, + { + "sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "states": 0 + } + ], + "minimum": null, + "total_states": 2455, + "witness": null + }, + "form_r_maximum": 10, + "indices": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10 + ], + "minimum_interior_for_eleven": 1, + "omitted": 11, + "ten_line": { + "indices": [ + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10 + ], + "witness": [ + [ + 5, + 3, + 6 + ], + [ + 2, + 2, + 2 + ], + [ + 0, + 2, + 3 + ], + [ + 3, + 2, + 3 + ], + [ + 7, + 1, + 1 + ], + [ + 1, + 1, + 1 + ], + [ + 8, + 4, + 4 + ], + [ + 4, + 4, + 4 + ], + [ + 6, + 1, + 1 + ], + [ + 9, + 4, + 4 + ] + ] + } + } + ], + "schema_version": 1, + "scope": "twelve tied_min eleven-line restrictions only", + "source_sha256": "670ed90924b601ade22f0d4adaff46d1667e5449326a0f7ba7b88dd8f5906f93" +} diff --git a/research/fstar-one-interior-label/SOURCES.json b/research/fstar-one-interior-label/SOURCES.json new file mode 100644 index 0000000000..44eea77ca0 --- /dev/null +++ b/research/fstar-one-interior-label/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "916ecdd9d6e666fcad9b25369d055311f6ce8204", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "889b95d936746df124872133ae1e7cc339adcb92", + "sha256": "7d185cd8c2af35988d638d969748ad7b670f902606444dbfc748e4402c340df6" + }, + { + "path": "research/fstar-entry-class-scope-seed63d5f999/data/tied_min.json", + "usage": "input", + "git_blob": "ae11f01fab8b32b07a782ec968186a0af98c8f32", + "sha256": "670ed90924b601ade22f0d4adaff46d1667e5449326a0f7ba7b88dd8f5906f93" + } + ] +} diff --git a/research/fstar-one-interior-label/TASK.json b/research/fstar-one-interior-label/TASK.json new file mode 100644 index 0000000000..382a364eec --- /dev/null +++ b/research/fstar-one-interior-label/TASK.json @@ -0,0 +1,99 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 5, + "base_commit": "916ecdd9d6e666fcad9b25369d055311f6ce8204", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md", + "research/selected-k8-unrestricted-ends/README.md", + "research/eisenstein-reduction-copy-floor/README.md" + ], + "methods": [ + "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.", + "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration." + ], + "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).", + "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.", + "allowed_variations": [ + "One masked, overcomplete or block decoder family with exact labels and supports.", + "A scoped lower bound on effective rank for one alphabet.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Repacking idle remainders of an unchanged word (covered by the packing ceiling).", + "Repeating the eight-term all-pairs search inside its proved scope.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ] + }, + "scope_status": "changed", + "actual_scope": "Settle the exact Form-R maximum and minimum number of non-Form-R label pairs needed to keep all eleven lines in each tied_min v=11 restriction, following PR2963 open question 2.", + "scope_change_reason": "The initial complex-mechanisms draw suggested P104 physical completion or complex decoder work. Existing P104 complete-consumer obstructions made another endpoint refinement unhelpful. Take the fresh unclaimed F-star constructive handoff instead. This is a proof-level side result, not a paid-profile improvement or a claim to meet the original 5% gate.", + "bottleneck_link": "The inherited cost >= cert(M) implication makes supported label/order families relevant to decoder cost lower bounds. This result identifies the exact missing local label occurrence on a pinned finite family. It does not supply a physical decoder or new recursive budget.", + "budget_minutes": 60, + "stop_rule": "Stop after the twelve finite restrictions and one-exception witnesses are checked, or after 100000 states per solve fails closed. No new general family census or physical construction campaign.", + "outcome": "completed", + "evidence": "RESULT.json retains all twelve exact exclusions and constructive witnesses. Primary forward b-domain and independent reverse a-domain recurrences agree. Seven behavioral groups include literal tiny oracles, actual implementation mutants and real CLI rejection controls.", + "author": "Nick Petalas", + "ai_assistance": "Automated assistance was used for computation and checking; no independent human review is claimed.", + "assignment_nonce": "5d2c0e46a5582dcbdea0ca1a680c3614", + "assignment_track": "complex-mechanisms", + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2967", + "upstream_refresh": { + "commit": "a23bdc1b07be96bea0101d44ae27d14de67a79ed", + "priority_revision": 5, + "checked_at_utc": "2026-10-16T15:00:08Z", + "decision": "Fast-forward isolated branch. Guidance, selected record and consumed fixture are unchanged. Scientific provenance remains at the original base.", + "overlap_coverage": "237 open PRs at 14:59:15Z, 1664 Discussion records at 14:59:44Z, 2418 closed/merged PRs at 15:00:07Z; complete pagination and no warnings. No successor on this question found; diffs and unpublished work are outside coverage." + }, + "predecessors": { + "2963": "ee755e682b3b30d493e764d3be50003b13b69b4a", + "2914": "3f7781efccdf10fa61a1e0a6f11c191579b21280" + }, + "expansion_decision": "Finish this scoped label/ordering result and stop; no supplier or dependent physical construction expansion.", + "validation": { + "environment": "Linux x86_64; CPython 3.12.15 and 3.13.5; standard library", + "commands": [ + "python3.12 -I -O -Werror -B research/fstar-one-interior-label/verify.py", + "python3.12 -I -O -Werror -B research/fstar-one-interior-label/independent.py", + "python3.12 -I -O -Werror -B research/fstar-one-interior-label/test_verify.py", + "python3.12 -B scripts/research_package.py --package research/fstar-one-interior-label", + "ruff check --select E,F,I,UP,B research/fstar-one-interior-label" + ], + "results": "Registered CPython 3.12.15 replay passes; normal/optimized direct checks and all seven package groups pass on CPython 3.13.5. All 147 research-workflow tests pass on CPython 3.12 with no skips; CPython 3.13 skips five explicitly Python-3.12-only replay controls. Ruff passes. No package test is skipped.", + "unrun": "Formal-kernel proof, independent human review, general F-star theorem, physical/native/copy/restoration/hosting/precision/all-size supplier admission and selected cold replay. Hosted CI is separate." + }, + "open_questions": [ + { + "question": "Can a general certificate family permit a bounded number of (a0,e_c) exceptions with a proved L8 order?", + "why_it_matters": "One such occurrence supplies the point that unrestricted Form-R ordering still misses on all twelve restrictions.", + "first_step": "Inspect the twelve stored constructive orders for one common sufficient rule, then test it against both PR2111 fixtures.", + "blocked_by": "A general ordering proof. This finite certificate does not justify physical construction or further large searches." + } + ] +} diff --git a/research/fstar-one-interior-label/VERIFY.json b/research/fstar-one-interior-label/VERIFY.json new file mode 100644 index 0000000000..78b67032d1 --- /dev/null +++ b/research/fstar-one-interior-label/VERIFY.json @@ -0,0 +1,26 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/fstar-entry-class-scope-seed63d5f999/data/tied_min.json" + ], + "commands": [ + { + "argv": ["{python}", "-I", "-Werror", "-B", "{package}/verify.py"], + "timeout_seconds": 120, + "checks": "Recompute all twelve exact forward-domain exclusions, one-exception witnesses and complete receipt." + }, + { + "argv": ["{python}", "-I", "-O", "-Werror", "-B", "{package}/independent.py"], + "timeout_seconds": 120, + "checks": "Independent reverse-domain exact exclusions and direct rational-zero L8 witness checks, with no primary imports." + }, + { + "argv": ["{python}", "-I", "-O", "-Werror", "-B", "{package}/test_verify.py"], + "timeout_seconds": 120, + "checks": "Literal tiny oracles, actual weakened implementations, witness/source/receipt controls, capacity exhaustion and real optimized Git-free CLI replay." + } + ] +} diff --git a/research/fstar-one-interior-label/independent.py b/research/fstar-one-interior-label/independent.py new file mode 100644 index 0000000000..68e56d6504 --- /dev/null +++ b/research/fstar-one-interior-label/independent.py @@ -0,0 +1,124 @@ +#!/usr/bin/env python3 +"""Reverse-order exact exclusion and direct L8 replay, no producer imports.""" + +import hashlib +import json +from pathlib import Path + +SOURCE = "research/fstar-entry-class-scope-seed63d5f999/data/tied_min.json" +DIGEST = "670ed90924b601ade22f0d4adaff46d1667e5449326a0f7ba7b88dd8f5906f93" + + +def check(ok, message): + if not ok: + raise ValueError(message) + + +def named(a, b, q): + support = sum(2**j for j in range(3) if q[j] != 0) + return b == support or a == b and a in (1, 2, 4) + + +def even(a, b): + return sum((a >> j & 1) * (b >> j & 1) for j in range(3)) % 2 == 0 + + +def reverse_exclusion(factors): + n = len(factors) + pairs = [] + for _p, q in factors: + support = sum(2**j for j in range(3) if q[j]) + pairs.append(tuple((a, b) for a in range(1, 8) for b in range(1, 8) + if b | support == support and not even(a, b) + and named(a, b, q))) + initial = tuple(tuple(sorted({a for a, _b in line})) for line in pairs) + frontier = {initial} + counts = [] + visited = 0 + for _depth in range(n): + counts.append(len(frontier)) + visited += len(frontier) + check(visited <= 100_000, "independent state capacity exhausted") + following = set() + for state in sorted(frontier): + for last in range(n): + if not state[last]: + continue + for b in sorted({b for a, b in pairs[last] if a in state[last]}): + candidate = list(state) + candidate[last] = () + valid = True + for t in range(n): + scalar = sum(factors[t][0][j] * factors[last][1][j] + for j in range(3)) + if candidate[t] and scalar == 0: + candidate[t] = tuple(a for a in candidate[t] if even(a, b)) + if not candidate[t]: + valid = False + break + if valid: + following.add(tuple(candidate)) + check(len(following) <= 100_000, + "independent frontier capacity") + frontier = following + counts.append(len(frontier)) + check(visited + len(frontier) <= 100_000, "independent state capacity exhausted") + return ((),) * n not in frontier, counts + + +def direct_replay(factors, witness, exceptions): + n = len(factors) + check(type(witness) is list and len(witness) == n, "independent witness length") + check(all(type(row) is list and len(row) == 3 + and all(type(x) is int for x in row) for row in witness), "triples") + check(sorted(row[0] for row in witness) == list(range(n)), "order permutation") + outside = 0 + for position, (t, a, b) in enumerate(witness): + p, q = factors[t] + check(1 <= a <= 7 and 1 <= b <= 7, "nonzero three-bit labels") + check(all(not (a >> j & 1) or p[j] != 0 for j in range(3)), "row support") + check(all(not (b >> j & 1) or q[j] != 0 for j in range(3)), "column support") + check(not even(a, b), "diagonal parity") + if not named(a, b, q): + check(a == 7 and b in (1, 2, 4), "exceptional label class") + outside += 1 + for s, _aa, bb in witness[position + 1:]: + entry = sum(p[j] * factors[s][1][j] for j in range(3)) + check(entry != 0 or even(a, bb), "ordered zero-arc parity") + check(outside == exceptions, "exact exceptional-pair count") + + +def main(): + package = Path(__file__).resolve().parent + with (package.parents[1] / SOURCE).open("rb") as stream: + payload = stream.read(4097) + check(len(payload) <= 4096 and hashlib.sha256(payload).hexdigest() == DIGEST, + "independent source binding") + factors = json.loads(payload) + with (package / "RESULT.json").open("rb") as stream: + receipt = stream.read(2_000_001) + check(len(receipt) <= 2_000_000, "receipt capacity") + records = json.loads(receipt)["records"] + check(len(records) == 12, "complete restriction count") + for omitted, record in enumerate(records): + indices = [t for t in range(12) if t != omitted] + check(record["indices"] == indices and record["omitted"] == omitted, + "restriction binding") + sub = [factors[t] for t in indices] + impossible, counts = reverse_exclusion(sub) + check(impossible, "reverse Form-R exclusion failed") + direct_replay(sub, record["extended"]["witness"], 1) + ten = record["ten_line"] + check(len(set(ten["indices"])) == 10 + and all(type(t) is int and 0 <= t < 11 for t in ten["indices"]), + "ten-line subset") + direct_replay([sub[t] for t in ten["indices"]], ten["witness"], 0) + print("reverse", omitted, "layer_counts=" + ",".join(map(str, counts))) + print("PASS_FSTAR_REVERSE_EXCLUSION records=12 form_r=10 one_exception=11") + + +if __name__ == "__main__": + try: + main() + except (ValueError, OSError, KeyError, TypeError) as error: + raise SystemExit("FAIL_FSTAR_REVERSE: " + str(error)) from error diff --git a/research/fstar-one-interior-label/test_verify.py b/research/fstar-one-interior-label/test_verify.py new file mode 100644 index 0000000000..852e0d62a0 --- /dev/null +++ b/research/fstar-one-interior-label/test_verify.py @@ -0,0 +1,205 @@ +#!/usr/bin/env python3 +"""Behavioral, finite-oracle and real-CLI controls for the scoped result.""" + +import copy +import itertools +import json +import shutil +import subprocess +import sys +import tempfile +import types +import unittest +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] + + +def load_source(name): + path = PACKAGE / (name + ".py") + module = types.ModuleType(name) + module.__file__ = str(path) + exec(compile(path.read_bytes(), str(path), "exec"), module.__dict__) + return module + + +V = load_source("verify") +INDEPENDENT = load_source("independent") + + +def brute_full(rows, budget): + """Literal pairs times all orders; no state-domain merging.""" + n = len(rows) + choices = [] + for _p, q in rows: + d = sum(1 << j for j in range(3) if q[j]) + local = [] + for a in range(1, 8): + for b in range(1, 8): + if b & ~d or (a & b).bit_count() % 2 == 0: + continue + form_r = b == d or a == b and a in (1, 2, 4) + if form_r or a == 7 and b in (1, 2, 4): + local.append((a, b, 0 if form_r else 1)) + choices.append(local) + best = None + for labels in itertools.product(*choices): + price = sum(c for _a, _b, c in labels) + if price > budget or best is not None and price >= best: + continue + for order in itertools.permutations(range(n)): + valid = True + for position, t in enumerate(order): + for s in order[position + 1:]: + dot = sum(rows[t][0][j] * rows[s][1][j] for j in range(3)) + if dot == 0 and (labels[t][0] & labels[s][1]).bit_count() % 2: + valid = False + if valid: + best = price + break + return best + + +class VerificationTests(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.rows = V.decode(V.read_json(ROOT / V.SOURCE, 4096, V.SOURCE_SHA256)) + cls.receipt = V.read_json(PACKAGE / "RESULT.json") + + def test_exact_tiny_oracles(self): + # Every three-line restriction, plus four representative four-line sets. + domains = list(itertools.combinations(range(12), 3)) + domains += [(0, 1, 3, 6), (0, 3, 6, 9), (0, 1, 2, 11), (2, 5, 8, 10)] + for indices in domains: + rows = tuple(self.rows[t] for t in indices) + for budget in (0, 1): + with self.subTest(indices=indices, budget=budget): + answer = V.solve(rows, budget)["minimum"] + self.assertEqual(answer, brute_full(rows, budget)) + excluded, _counts = INDEPENDENT.reverse_exclusion(rows) + self.assertEqual(excluded, V.solve(rows, 0)["minimum"] is None) + + def test_twelve_exact_obstructions_and_witnesses(self): + actual = V.calculate(self.rows) + self.assertEqual(actual, self.receipt) + self.assertEqual([r["form_r_maximum"] for r in actual["records"]], [10] * 12) + self.assertEqual([r["minimum_interior_for_eleven"] for r in actual["records"]], + [1] * 12) + for record in actual["records"]: + sub = tuple(self.rows[t] for t in record["indices"]) + self.assertEqual(INDEPENDENT.reverse_exclusion(sub)[0], True) + INDEPENDENT.direct_replay(sub, record["extended"]["witness"], 1) + + def test_real_constraint_mutants(self): + indices = self.receipt["records"][0]["indices"] + rows = tuple(self.rows[t] for t in indices) + original = V.advance + try: + # Actual weakened implementation ignores all future zero-arc obligations. + def no_constraints(state, t, _a, _zeros): + return tuple(0 if s == t else value for s, value in enumerate(state)) + V.advance = no_constraints + self.assertEqual(V.solve(rows, 0)["minimum"], 0) + finally: + V.advance = original + self.assertIsNone(V.solve(rows, 0)["minimum"]) + # Treating a new (111,e_c) label as old Form-R falsely admits eleven. + original_pairs = V.local_pairs + try: + V.local_pairs = lambda q: tuple((a, b, 0) for a, b, _c in original_pairs(q)) + self.assertEqual(V.solve(rows, 0)["minimum"], 0) + finally: + V.local_pairs = original_pairs + + def test_invalid_witnesses(self): + record = self.receipt["records"][0] + rows = tuple(self.rows[t] for t in record["indices"]) + good = record["extended"]["witness"] + INDEPENDENT.direct_replay(rows, good, 1) + broken = [] + bad = copy.deepcopy(good) + bad[0][1] = 0 + broken.append(bad) + bad = copy.deepcopy(good) + bad[0][2] = 7 + broken.append(bad) + bad = copy.deepcopy(good) + bad[0][0] = bad[1][0] + broken.append(bad) + broken.append(list(reversed(good))) + for witness in broken: + with self.assertRaises(ValueError): + INDEPENDENT.direct_replay(rows, witness, 1) + with self.assertRaises(ValueError): + INDEPENDENT.direct_replay(rows, good, 0) + + def test_input_and_capacity_limits_fail_closed(self): + for bad in ([], [[[True, 1, 1], [1, 1, 0]]], [[[1, 1, 1], [1, -1, 0]]], + [[[1, 1, 1], [1, 0, 0]]], [[[2, 1, 1], [1, 1, 0]]]): + with self.assertRaises(ValueError): + V.decode(bad) + self.assertEqual(V.solve(self.rows[:3], 0)["minimum"], 0) + with self.assertRaisesRegex(ValueError, "capacity exhausted"): + V.solve(self.rows[:3], 0, capacity=1) + for invalid in (-1, 2, True): + with self.assertRaises(ValueError): + V.solve(self.rows[:3], invalid) + + def run_cli(self, script, cwd, *arguments): + return subprocess.run([sys.executable, "-I", "-O", "-Werror", "-B", + str(script), *arguments], cwd=cwd, text=True, + capture_output=True, timeout=60, check=False) + + def test_real_cli_export_and_corruption(self): + with tempfile.TemporaryDirectory() as directory: + root = Path(directory) + package = root / "research/fstar-one-interior-label" + package.mkdir(parents=True) + for name in ("verify.py", "independent.py", "RESULT.json"): + shutil.copyfile(PACKAGE / name, package / name) + source = root / V.SOURCE + source.parent.mkdir(parents=True) + shutil.copyfile(ROOT / V.SOURCE, source) + before = {p: p.read_bytes() for p in root.rglob("*") if p.is_file()} + for script, marker in (("verify.py", "PASS_FSTAR_ONE_INTERIOR"), + ("independent.py", "PASS_FSTAR_REVERSE_EXCLUSION")): + run = self.run_cli(package / script, root) + self.assertEqual(run.returncode, 0, run.stderr) + self.assertIn(marker, run.stdout) + after = {p: p.read_bytes() for p in root.rglob("*") if p.is_file()} + self.assertEqual(before, after) + source.write_bytes(b"not JSON") + run = self.run_cli(package / "verify.py", root) + self.assertNotEqual(run.returncode, 0) + self.assertIn("source hash mismatch", run.stderr) + source.write_bytes(before[source]) + result = package / "RESULT.json" + bad = copy.deepcopy(self.receipt) + bad["records"][0]["extended"]["minimum"] = True + result.write_text(json.dumps(bad), encoding="utf-8") + run = self.run_cli(package / "verify.py", root) + self.assertNotEqual(run.returncode, 0) + self.assertIn("complete receipt mismatch", run.stderr) + result.write_text('{"schema_version":1,"schema_version":1}', + encoding="utf-8") + run = self.run_cli(package / "verify.py", root) + self.assertNotEqual(run.returncode, 0) + self.assertIn("duplicate JSON key", run.stderr) + + def test_exclusive_output_and_json_bounds(self): + with tempfile.TemporaryDirectory() as directory: + path = Path(directory) / "receipt.json" + path.write_text("retained", encoding="utf-8") + run = self.run_cli(PACKAGE / "verify.py", ROOT, "--write-result", str(path)) + self.assertNotEqual(run.returncode, 0) + self.assertEqual(path.read_text(encoding="utf-8"), "retained") + with self.assertRaisesRegex(ValueError, "size limit"): + V.read_json(path, limit=1) + path.write_text('{"value":NaN}', encoding="utf-8") + with self.assertRaisesRegex(ValueError, "nonfinite"): + V.read_json(path) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/fstar-one-interior-label/verify.py b/research/fstar-one-interior-label/verify.py new file mode 100644 index 0000000000..1dfd518838 --- /dev/null +++ b/research/fstar-one-interior-label/verify.py @@ -0,0 +1,230 @@ +#!/usr/bin/env python3 +"""Exact finite Form-R obstruction and one-exception L8 witnesses.""" + +import argparse +import hashlib +import json +from pathlib import Path + +SOURCE = "research/fstar-entry-class-scope-seed63d5f999/data/tied_min.json" +SOURCE_SHA256 = "670ed90924b601ade22f0d4adaff46d1667e5449326a0f7ba7b88dd8f5906f93" +MAX_STATES = 100_000 +ORTHOGONAL = tuple( + sum(1 << b for b in range(1, 8) if (a & b).bit_count() % 2 == 0) + for a in range(8) +) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def unique_object(pairs): + result = {} + for key, value in pairs: + require(key not in result, "duplicate JSON key: " + key) + result[key] = value + return result + + +def reject_constant(value): + raise ValueError("nonfinite JSON constant: " + value) + + +def read_json(path, limit=2_000_000, digest=None): + with path.open("rb") as stream: + payload = stream.read(limit + 1) + require(len(payload) <= limit, "JSON size limit") + if digest is not None: + require(hashlib.sha256(payload).hexdigest() == digest, "source hash mismatch") + return json.loads(payload, object_pairs_hook=unique_object, + parse_constant=reject_constant) + + +def decode(raw): + require(type(raw) is list and 1 <= len(raw) <= 12, "decoder size") + rows = [] + for row in raw: + require(type(row) is list and len(row) == 2, "factor pair") + for factor in row: + require(type(factor) is list and len(factor) == 3, "three totals") + require(all(type(x) is int and -1 <= x <= 1 for x in factor), + "integer factor alphabet") + p, q = map(tuple, row) + require(all(p), "this finite model needs full odd P support") + require(sum(x != 0 for x in q) == 2, "two odd Q entries") + require(sum(p[j] * q[j] for j in range(3)) != 0, "nonzero diagonal") + rows.append((p, q)) + return tuple(rows) + + +def local_pairs(q): + """Cost zero is Form-R; cost one adds only (111, e_c).""" + d = sum(1 << j for j in range(3) if q[j]) + result = [] + for a in range(1, 8): + for b in range(1, 8): + if b & ~d or (a & b).bit_count() % 2 != 1: + continue + form_r = b == d or (a == b and a in (1, 2, 4)) + if form_r or (a == 7 and b in (1, 2, 4)): + result.append((a, b, int(not form_r))) + return tuple(result) + + +def model(rows): + n = len(rows) + zeros = tuple(tuple( + t != s and sum(rows[t][0][j] * rows[s][1][j] for j in range(3)) == 0 + for s in range(n)) for t in range(n)) + options = tuple(local_pairs(q) for _p, q in rows) + return zeros, options + + +def advance(state, t, a, zeros): + following = list(state) + following[t] = 0 + for s in range(len(state)): + if following[s] and zeros[t][s]: + following[s] &= ORTHOGONAL[a] + if following[s] == 0: + return None + return tuple(following) + + +def frontier_hash(frontier): + records = [(state, frontier[state][0]) for state in sorted(frontier)] + payload = json.dumps(records, separators=(",", ":")).encode() + return hashlib.sha256(payload).hexdigest() + + +def next_layer(frontier, zeros, options, budget): + following = {} + for state in sorted(frontier): + cost, prefix = frontier[state] + for t, domain in enumerate(state): + if not domain: + continue + for a in range(1, 8): + choices = [(c, b) for aa, b, c in options[t] + if aa == a and domain & (1 << b)] + if not choices: + continue + extra, b = min(choices) + if cost + extra > budget: + continue + target = advance(state, t, a, zeros) + if target is None: + continue + total = cost + extra + if target not in following or total < following[target][0]: + following[target] = (total, prefix + ((t, a, b),)) + require(len(following) <= MAX_STATES, "state capacity exhausted") + return following + + +def solve(rows, budget, capacity=MAX_STATES): + """Keep every row, minimizing exceptional pairs up to the given budget.""" + require(type(budget) is int and 0 <= budget <= 1, "exception budget") + require(type(capacity) is int and 1 <= capacity <= MAX_STATES, "state capacity") + zeros, options = model(rows) + initial = tuple(sum(1 << b for b in sorted({b for _a, b, _c in pairs})) + for pairs in options) + frontier = {initial: (0, ())} + layers = [] + total_states = 0 + for _depth in range(len(rows) + 1): + total_states += len(frontier) + require(total_states <= capacity, "state capacity exhausted") + layers.append({"states": len(frontier), "sha256": frontier_hash(frontier)}) + if _depth == len(rows): + break + frontier = next_layer(frontier, zeros, options, budget) + answer = frontier.get((0,) * len(rows)) + witness = None if answer is None else [list(item) for item in answer[1]] + return {"minimum": None if answer is None else answer[0], + "witness": witness, "layers": layers, "total_states": total_states} + + +def replay(rows, witness, expected_cost): + n = len(rows) + require(type(witness) is list and len(witness) == n, "witness length") + require(all(type(item) is list and len(item) == 3 + and all(type(x) is int for x in item) for item in witness), + "witness triples") + require(sorted(t for t, _a, _b in witness) == list(range(n)), "witness order") + zeros, options = model(rows) + cost = 0 + for position, (t, a, b) in enumerate(witness): + matches = [c for aa, bb, c in options[t] if (aa, bb) == (a, b)] + require(len(matches) == 1, "invalid local pair") + cost += matches[0] + for s, _aa, bb in witness[position + 1:]: + require(not zeros[t][s] or (a & bb).bit_count() % 2 == 0, + "forward zero-arc conflict") + require(cost == expected_cost, "witness exception count") + + +def find_ten(sub): + for dropped in range(11): + indices = [t for t in range(11) if t != dropped] + rows = tuple(sub[t] for t in indices) + answer = solve(rows, 0) + if answer["minimum"] == 0: + replay(rows, answer["witness"], 0) + return {"indices": indices, "witness": answer["witness"]} + raise ValueError("ten-line Form-R witness missing") + + +def calculate(rows): + require(len(rows) == 12, "the result needs the twelve-line fixture") + records = [] + for omitted in range(12): + indices = [t for t in range(12) if t != omitted] + sub = tuple(rows[t] for t in indices) + excluded = solve(sub, 0) + require(excluded["minimum"] is None, "Form-R unexpectedly attains eleven") + extended = solve(sub, 1) + require(extended["minimum"] == 1, "one-exception witness missing") + replay(sub, extended["witness"], 1) + ten = find_ten(sub) + records.append({"omitted": omitted, "indices": indices, + "form_r_maximum": 10, "minimum_interior_for_eleven": 1, + "form_r_exclusion": excluded, "extended": extended, + "ten_line": ten}) + return {"schema_version": 1, "source_sha256": SOURCE_SHA256, + "scope": "twelve tied_min eleven-line restrictions only", + "records": records, "full_twelve_form_r_maximum": 10} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--source", type=Path) + output = parser.add_mutually_exclusive_group() + output.add_argument("--emit", action="store_true") + output.add_argument("--write-result", type=Path) + args = parser.parse_args() + package = Path(__file__).resolve().parent + source = args.source or package.parents[1] / SOURCE + rows = decode(read_json(source, 4096, SOURCE_SHA256)) + result = calculate(rows) + text = json.dumps(result, indent=2, sort_keys=True) + "\n" + if args.emit: + print(text, end="") + elif args.write_result: + with args.write_result.open("x", encoding="utf-8") as stream: + stream.write(text) + else: + retained = read_json(package / "RESULT.json") + require(json.dumps(retained, sort_keys=True) + == json.dumps(result, sort_keys=True), "complete receipt mismatch") + print("PASS_FSTAR_ONE_INTERIOR records=12 form_r=10 " + "minimum_interior=1 full_form_r=10") + + +if __name__ == "__main__": + try: + main() + except (ValueError, OSError) as error: + raise SystemExit("FAIL_FSTAR_ONE_INTERIOR: " + str(error)) from error