diff --git a/research/staged544-a2-composition-audit/README.md b/research/staged544-a2-composition-audit/README.md new file mode 100644 index 0000000000..2ac2d3a710 --- /dev/null +++ b/research/staged544-a2-composition-audit/README.md @@ -0,0 +1,88 @@ +# Independent acceptance of the separated A2 composition + +**Audit of an existing scalar identity. No new κ. Selected κ stays 0.001672660197076918.** + +## Scope and evidence + +Original card: `independent-moment`, scope **changed**. The card's #2979 group audit is already +covered by open V45 work (#3543, #3911) and the merged group A–D native-width audits. This package +takes the still-open handoff on +[discussion #1166](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19036786): +independently accept the composition and projected-cleanup argument in +[PR #4019](https://github.com/CrocSwap/integer-mult-bounds/pull/4019), head +`f408e09df300b575235f7f77f81948071397e16d`. + +The two rational identities, for distinct registers `x, y, z` and nonzero rationals `a, b`, are + +```text +[S(a), T(b), U(-ab)] = [T(b), S(a)] +[U(ab), T(b), S(a)] = [S(a), T(b)] +``` + +with `S(a): y += a*z`, `T(b): x += b*y`, and `U(c): x += c*z`. Both sides of the first identity end at +`(x + b*y, y + a*z, z)`. Both sides of the second end at `(x + b*y + ab*z, y + a*z, z)`, for an +arbitrary initial triple. The checker proves those endpoints, and the same maps as 3×3 matrices, +before it looks at a word. + +On both vendored provider words the eight published sites each match exactly one identity: + +| Section | Indices | Identity | Removed record | New-site cleanup effect | +|---|---|---|---|---| +| A | 1858, 1859, 1860 | first, drop `U` | credited PR #3998 site | not counted in the new split | +| B | 4, 53, 54 | second, drop `U` | target write | helper ADD unchanged | +| B | 7, 49, 50 | second, drop `U` | target write | helper ADD unchanged | +| restore | 20, 21, 36 | first, drop `U` | non-target write | one cleanup ADD | +| restore | 22, 23, 38 | first, drop `U` | non-target write | one cleanup ADD | +| restore | 26, 27, 51 | first, drop `U` | non-target write | one cleanup ADD | +| restore | 30, 31, 62 | first, drop `U` | non-target write | one cleanup ADD | +| restore | 32, 33, 73 | first, drop `U` | non-target write | one cleanup ADD | + +Every intervening scalar event misses the site's three registers. The eight supports are pairwise +disjoint. No new B window contains a native-warp index, and the A site starts at or after the +prelude. The seven new published replacements equal the identity's right-hand side, including the +ordered frame list. The credited A1858 replacement has the same ADD edges and the same frame span, +but the ordered frame is `[42, 82]` rather than the source `[82, 42]`, which PR #4019 already +discloses. The new record split is **7 forward ADD deletions and 5 projected-cleanup ADD deletions**. +That is one forward deletion at each new site, and a cleanup deletion only where the deleted ADD +does not write a target. + +This is an acceptance of that composition and record split. It is not a second recursive-histogram +replay, not a check that PR #4041's later-word transfer is valid, and not a κ claim. The predecessor +states that the histogram stays `{1:2440, 2:725, 3:224, 4:102, 5:20, 8:8}`. This package does not +recompute those ranks. + +## Reproduce + +Python 3.12, standard library only, from the repository root: + +```sh +python3.12 -B scripts/research_package.py --package research/staged544-a2-composition-audit +``` + +Expected marker: + +```text +PASS_A2_COMPOSITION_AUDIT providers=2 sites=8 new_forward_adds=7 new_cleanup_adds=5 known_frame_order_swaps=2 controls=3 no_new_kappa +``` + +The three controls reject a flipped B4 coefficient, an intervening read of register 518, and the +identity-one endpoint under the wrong `U` sign. Inputs are the two compressed provider words and +`inputs/data.json` taken from PR #4019 at the head above. Their SHA256 pins are checked before use. +Base commit is `bb4bccbf42844d2801487450727c2f63e10d1d0f`. Priority revision 6. + +## Open next questions + +- Does one later exact provider word, in particular a PR #3945 word, admit these same contractions? + Pin that word and recheck every index, boundary, intervening support, cleanup count and paid + profile. This package has only the two PR3734 providers. +- Can a different scalar graph remove a paid frame transition? Name the changed boundary and a + complete favorable bill first. These seven sites do not, by themselves, move a rank count. + +## Credit + +Chris R / Clear1nsight, PR #3998, for the A2 identity and the consecutive A1858 contraction. +ToikY, PR #4019, for the seven separated witnesses, the published receipt, and the stated endpoint +argument accepted here. Dataisfire for the PR3734 words retained by that package. The ordered-frame +swap on the credited site is their disclosure, not a new defect. New audit by unpaidmoon with +substantial Cursor Grok assistance. Apache-2.0. No independent human or formal-kernel review is +claimed. diff --git a/research/staged544-a2-composition-audit/SOURCES.json b/research/staged544-a2-composition-audit/SOURCES.json new file mode 100644 index 0000000000..a604c6a640 --- /dev/null +++ b/research/staged544-a2-composition-audit/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + } + ] +} diff --git a/research/staged544-a2-composition-audit/TASK.json b/research/staged544-a2-composition-audit/TASK.json new file mode 100644 index 0000000000..362ae77eb3 --- /dev/null +++ b/research/staged544-a2-composition-audit/TASK.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 6, + "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f", + "original_card": { + "id": "independent-moment", + "question": "Does one changed supplier or assembly claim lack a source-bound independent check of a specific new implication?", + "starting_points": [ + "certificates/selected-result.json", + "research/rank7-joint-endframes/README.md", + "docs/research/research-family-status.md" + ], + "methods": [ + "Independently reconstruct a coordinated frame/circuit change and its single-change control, then derive the complete rank and physical ledger.", + "Implement certified moment inequalities through a different exact enclosure method." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #2979 joint rank-7 end-frame proposal and the revision-6 evidence status. Its claimed kappa is not selected. Compare coordinated changes with the losing single-change controls and locate the complete physical ledger; an aggregate moment alone does not validate the mechanism.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Prioritize a bounded independent audit of #2979: reconstruct one joint group and its single-lowering control, check the declared frames/chronology, then trace changed children, idle widths and cleanup buffers into the complete invoice and both supplier caps. Choose one still-missing implication after checking existing audits. Stop with exact unresolved dependencies if full admission exceeds the session; do not launch a new lowering census on an unvalidated premise or substitute extra root digits for mechanism checking.", + "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.", + "allowed_variations": [ + "Reconstruct either a source ledger or a numeric enclosure with a different method." + ], + "scope_change_triggers": [ + "Importing the primary function and calling its output independent verification.", + "Promoting #2979 from merged source archive to validated supplier solely from author PASS receipts or aggregate pricing." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure", + "2979", + "rank7 joint endframes", + "paired extraction", + "joint lowering" + ] + }, + "scope_status": "changed", + "actual_scope": "Independently accept or refute the two rational A2 identities and the projected-cleanup record split on the eight frozen PR3734 sites published by PR #4019, for both providers.", + "scope_change_reason": "The catalogue card's stated first audit is one #2979 rank-7 group and its single-change control. That group work is already in open PRs, including #3543 and #3911 for V45 and the merged group A-D native-width audits. This package instead takes the still-open #1166 request to independently accept PR #4019's separated A2 composition and projected-cleanup argument. The scalar-record identity is a different implication from the #2979 joint-frame invoice.", + "bottleneck_link": "A scalar ADD deletion changes the multiplication exponent only when the paid profile changes. Accepting this contraction, while its seven new sites remove no rank, blocks treating the ADD count as a moment improvement.", + "budget_minutes": 60, + "stop_rule": "Stop after both frozen providers and all eight published sites are classified, the seven-site record split is checked, and the three negative controls reject. Do not search for further sites or reprice the recursive histogram.", + "outcome": "completed", + "evidence": "Separate exact-rational endpoint and matrix checks accept both proof identities. On both vendored PR #4019 provider words, all eight sites match exactly one identity, intervening scalar events miss the three-register support, the eight supports are pairwise disjoint, and the seven new published replacements equal the identity right-hand side including ordered frames. The new record split is 7 forward ADD deletions and 5 projected-cleanup ADD deletions. The credited A1858 replacement differs only by the disclosed ordered-frame swap [82, 42] versus [42, 82]. Three semantic controls reject.", + "author": "unpaidmoon", + "ai_assistance": "Substantial Cursor Grok assistance with the audit implementation and write-up.", + "open_questions": [ + { + "question": "Does one later exact provider word, in particular a PR #3945 word, admit these same contractions?", + "why_it_matters": "PR #4041 reports a transfer onto later words. This audit certifies only the two PR3734 providers vendored from PR #4019, so that transfer is not accepted here.", + "first_step": "Pin the later word bytes, recheck every source index, section boundary, intervening support and projected-cleanup count, then compare the full paid profile.", + "blocked_by": "The vendored inputs are only BORROW-WORD-base and BORROW-WORD-extra at the PR #4019 head. No later word is in this package." + }, + { + "question": "Can a different scalar graph remove a paid frame transition rather than only an ADD record?", + "why_it_matters": "These seven sites leave every rank count unchanged, so they do not move the recursive moment.", + "first_step": "Name one changed frame boundary and a complete favorable bill before searching another separated motif.", + "blocked_by": "This audit does not recompute the recursive histogram; the predecessor states that histogram is unchanged, and that claim is outside this certificate." + } + ] +} diff --git a/research/staged544-a2-composition-audit/VERIFY.json b/research/staged544-a2-composition-audit/VERIFY.json new file mode 100644 index 0000000000..551d196975 --- /dev/null +++ b/research/staged544-a2-composition-audit/VERIFY.json @@ -0,0 +1,22 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/staged544-a2-composition-audit/inputs/BORROW-WORD-base.json.gz", + "research/staged544-a2-composition-audit/inputs/BORROW-WORD-extra.json.gz", + "research/staged544-a2-composition-audit/inputs/data.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Exact endpoint formulas, both provider words, eight site classifications, projected-cleanup record split, and three rejection controls" + } + ] +} diff --git a/research/staged544-a2-composition-audit/inputs/BORROW-WORD-base.json.gz b/research/staged544-a2-composition-audit/inputs/BORROW-WORD-base.json.gz new file mode 100644 index 0000000000..674ea18ade Binary files /dev/null and b/research/staged544-a2-composition-audit/inputs/BORROW-WORD-base.json.gz differ diff --git a/research/staged544-a2-composition-audit/inputs/BORROW-WORD-extra.json.gz b/research/staged544-a2-composition-audit/inputs/BORROW-WORD-extra.json.gz new file mode 100644 index 0000000000..b17e2be67e Binary files /dev/null and b/research/staged544-a2-composition-audit/inputs/BORROW-WORD-extra.json.gz differ diff --git a/research/staged544-a2-composition-audit/inputs/data.json b/research/staged544-a2-composition-audit/inputs/data.json new file mode 100644 index 0000000000..f91c78bed3 --- /dev/null +++ b/research/staged544-a2-composition-audit/inputs/data.json @@ -0,0 +1,1839 @@ +{ + "providers": { + "base": { + "additional_cleanup_add_saving": 5, + "additional_forward_add_saving": 7, + "known_sites": 1, + "native_operators_changed": false, + "new_kappa": false, + "new_sites": 7, + "new_supplier": false, + "provider": "base", + "recursive_moment_changed": false, + "schema_version": 1, + "sites": [ + { + "crossed_disjoint_events": 0, + "gates": [ + [ + "add", + 457, + 475, + -1, + 1, + [ + 82, + 42 + ] + ], + [ + "add", + 456, + 457, + 1, + 1, + [ + 82, + 42 + ] + ], + [ + "add", + 456, + 475, + 1, + 1, + [ + 82, + 42 + ] + ] + ], + "indices": [ + 1858, + 1859, + 1860 + ], + "known": true, + "removed_position": 2, + "replacement": [ + [ + "add", + 456, + 457, + 1, + 1, + [ + 42, + 82 + ] + ], + [ + "add", + 457, + 475, + -1, + 1, + [ + 42, + 82 + ] + ] + ], + "section": "A", + "support": [ + 456, + 457, + 475 + ] + }, + { + "crossed_disjoint_events": 48, + "gates": [ + [ + "add", + 196, + 518, + 1, + 1, + [ + 30 + ] + ], + [ + "add", + 196, + 588, + -1, + 1, + [ + 30 + ] + ], + [ + "add", + 588, + 518, + -1, + 1, + [ + 30 + ] + ] + ], + "indices": [ + 4, + 53, + 54 + ], + "known": false, + "removed_position": 0, + "replacement": [ + [ + "add", + 588, + 518, + -1, + 1, + [ + 30 + ] + ], + [ + "add", + 196, + 588, + -1, + 1, + [ + 30 + ] + ] + ], + "section": "B", + "support": [ + 196, + 518, + 588 + ] + }, + { + "crossed_disjoint_events": 41, + "gates": [ + [ + "add", + 187, + 506, + 1, + 1, + [ + 30 + ] + ], + [ + "add", + 187, + 586, + 1, + 2, + [ + 30 + ] + ], + [ + "add", + 586, + 506, + 2, + 1, + [ + 30 + ] + ] + ], + "indices": [ + 7, + 49, + 50 + ], + "known": false, + "removed_position": 0, + "replacement": [ + [ + "add", + 586, + 506, + 2, + 1, + [ + 30 + ] + ], + [ + "add", + 187, + 586, + 1, + 2, + [ + 30 + ] + ] + ], + "section": "B", + "support": [ + 187, + 506, + 586 + ] + }, + { + "crossed_disjoint_events": 14, + "gates": [ + [ + "add", + 448, + 231, + -1, + 1, + [ + 256, + 128, + 64, + 34, + 17, + 11, + 4 + ] + ], + [ + "add", + 484, + 448, + -1, + 1, + [ + 256, + 128, + 64, + 34, + 17, + 11, + 4 + ] + ], + [ + "add", + 484, + 231, + -1, + 1, + [ + 256, + 128, + 64, + 34, + 17, + 11, + 4 + ] + ] + ], + "indices": [ + 20, + 21, + 36 + ], + "known": false, + "removed_position": 2, + "replacement": [ + [ + "add", + 484, + 448, + -1, + 1, + [ + 256, + 128, + 64, + 34, + 17, + 11, + 4 + ] + ], + [ + "add", + 448, + 231, + -1, + 1, + [ + 256, + 128, + 64, + 34, + 17, + 11, + 4 + ] + ] + ], + "section": "restore", + "support": [ + 231, + 448, + 484 + ] + }, + { + "crossed_disjoint_events": 14, + "gates": [ + [ + "add", + 449, + 226, + -1, + 1, + [ + 256, + 128, + 64, + 34, + 17, + 11, + 4 + ] + ], + [ + "add", + 485, + 449, + -1, + 1, + [ + 256, + 128, + 64, + 34, + 17, + 11, + 4 + ] + ], + [ + "add", + 485, + 226, + -1, + 1, + [ + 256, + 128, + 64, + 34, + 17, + 11, + 4 + ] + ] + ], + "indices": [ + 22, + 23, + 38 + ], + "known": false, + "removed_position": 2, + "replacement": [ + [ + "add", + 485, + 449, + -1, + 1, + [ + 256, + 128, + 64, + 34, + 17, + 11, + 4 + ] + ], + [ + "add", + 449, + 226, + -1, + 1, + [ + 256, + 128, + 64, + 34, + 17, + 11, + 4 + ] + ] + ], + "section": "restore", + "support": [ + 226, + 449, + 485 + ] + }, + { + "crossed_disjoint_events": 23, + "gates": [ + [ + "add", + 451, + 228, + -1, + 1, + [ + 256, + 128, + 64, + 38, + 20, + 10, + 1 + ] + ], + [ + "add", + 509, + 451, + -1, + 1, + [ + 256, + 128, + 64, + 38, + 20, + 10, + 1 + ] + ], + [ + "add", + 509, + 228, + -1, + 1, + [ + 256, + 128, + 64, + 38, + 20, + 10, + 1 + ] + ] + ], + "indices": [ + 26, + 27, + 51 + ], + "known": false, + "removed_position": 2, + "replacement": [ + [ + "add", + 509, + 451, + -1, + 1, + [ + 256, + 128, + 64, + 38, + 20, + 10, + 1 + ] + ], + [ + "add", + 451, + 228, + -1, + 1, + [ + 256, + 128, + 64, + 38, + 20, + 10, + 1 + ] + ] + ], + "section": "restore", + "support": [ + 228, + 451, + 509 + ] + }, + { + "crossed_disjoint_events": 30, + "gates": [ + [ + "add", + 453, + 7, + -1, + 1, + [ + 256, + 128, + 64, + 32, + 19, + 11, + 6 + ] + ], + [ + "add", + 533, + 453, + 2, + 1, + [ + 256, + 128, + 64, + 32, + 19, + 11, + 6 + ] + ], + [ + "add", + 533, + 7, + 2, + 1, + [ + 256, + 128, + 64, + 32, + 19, + 11, + 6 + ] + ] + ], + "indices": [ + 30, + 31, + 62 + ], + "known": false, + "removed_position": 2, + "replacement": [ + [ + "add", + 533, + 453, + 2, + 1, + [ + 256, + 128, + 64, + 32, + 19, + 11, + 6 + ] + ], + [ + "add", + 453, + 7, + -1, + 1, + [ + 256, + 128, + 64, + 32, + 19, + 11, + 6 + ] + ] + ], + "section": "restore", + "support": [ + 7, + 453, + 533 + ] + }, + { + "crossed_disjoint_events": 39, + "gates": [ + [ + "add", + 454, + 236, + -1, + 1, + [ + 256, + 128, + 64, + 37, + 21, + 8, + 3 + ] + ], + [ + "add", + 556, + 454, + 2, + 1, + [ + 256, + 128, + 64, + 37, + 21, + 8, + 3 + ] + ], + [ + "add", + 556, + 236, + 2, + 1, + [ + 256, + 128, + 64, + 37, + 21, + 8, + 3 + ] + ] + ], + "indices": [ + 32, + 33, + 73 + ], + "known": false, + "removed_position": 2, + "replacement": [ + [ + "add", + 556, + 454, + 2, + 1, + [ + 256, + 128, + 64, + 37, + 21, + 8, + 3 + ] + ], + [ + "add", + 454, + 236, + -1, + 1, + [ + 256, + 128, + 64, + 37, + 21, + 8, + 3 + ] + ] + ], + "section": "restore", + "support": [ + 236, + 454, + 556 + ] + } + ], + "words": { + "credited_3998": { + "canonical_word_sha256": "32415e93a50f0fdab5fa144da05977fe34bc8340bf967b91c7f7f0bc312df994", + "cleanup_sha256": "7c2a181ac7fc6a087f5c7cce346650e0bb773f5dafa82ca966081a4a6440c336", + "helper_widths": { + "4": 26, + "5": 2, + "6": 18, + "7": 53, + "8": 96, + "9": 213 + }, + "lengths": { + "A": 4078, + "B": 1869, + "cleanup": 5223, + "restore": 212 + }, + "native_operations": 72, + "primitive_counts": { + "A": { + "add": 3556, + "scale": 498, + "warp": 24 + }, + "B": { + "add": 1796, + "scale": 73, + "warp": 0 + }, + "cleanup": { + "add": 4632, + "scale": 519, + "warp": 72 + }, + "restore": { + "add": 196, + "scale": 16, + "warp": 0 + } + }, + "profile": { + "1": 2440, + "2": 725, + "3": 224, + "4": 102, + "5": 20, + "8": 8 + }, + "semantics": { + "arbitrary_dirty_buffers": 91, + "buffer_self_map": "identity", + "buffer_to_live_leaks": 0, + "cleanup_boundary_both_directions": true, + "dual": true, + "dual_matrix_sha256": "9bace9fb7525f64d5418ab54af173df7d320c898e980e89be8a90d280adb3744", + "live_inputs": 632, + "matrix_dimension": 723, + "ordinary": true, + "ordinary_matrix_sha256": "c8ea87b1598c9bbc2b0be63217772110ff450ad12eff19aaf05a84239eb5d380", + "reverse_equals_ordinary": true + } + }, + "separated": { + "canonical_word_sha256": "0a36faedd98f7b80304469c16e6c2f074850d6bd054030366713a08805cd3300", + "cleanup_sha256": "a20cef30d1adbaa529d96f2055bf3f203cbf1f15438de04ec34c3fb7a7372906", + "helper_widths": { + "4": 26, + "5": 2, + "6": 18, + "7": 53, + "8": 96, + "9": 213 + }, + "lengths": { + "A": 4078, + "B": 1867, + "cleanup": 5218, + "restore": 207 + }, + "native_operations": 72, + "primitive_counts": { + "A": { + "add": 3556, + "scale": 498, + "warp": 24 + }, + "B": { + "add": 1794, + "scale": 73, + "warp": 0 + }, + "cleanup": { + "add": 4627, + "scale": 519, + "warp": 72 + }, + "restore": { + "add": 191, + "scale": 16, + "warp": 0 + } + }, + "profile": { + "1": 2440, + "2": 725, + "3": 224, + "4": 102, + "5": 20, + "8": 8 + }, + "semantics": { + "arbitrary_dirty_buffers": 91, + "buffer_self_map": "identity", + "buffer_to_live_leaks": 0, + "cleanup_boundary_both_directions": true, + "dual": true, + "dual_matrix_sha256": "9bace9fb7525f64d5418ab54af173df7d320c898e980e89be8a90d280adb3744", + "live_inputs": 632, + "matrix_dimension": 723, + "ordinary": true, + "ordinary_matrix_sha256": "c8ea87b1598c9bbc2b0be63217772110ff450ad12eff19aaf05a84239eb5d380", + "reverse_equals_ordinary": true + } + }, + "source": { + "canonical_word_sha256": "a140d980692fb1688b6b85021e06e2aea7d97eb3fd2b09cbd6c47afb0cc7f9da", + "cleanup_sha256": "cfcb7fbc44fb3e14c6edd781f1fb57ea25ade9a96c0ef4873bf8d4c1eb7a02e2", + "helper_widths": { + "4": 26, + "5": 2, + "6": 18, + "7": 53, + "8": 96, + "9": 213 + }, + "lengths": { + "A": 4079, + "B": 1869, + "cleanup": 5224, + "restore": 212 + }, + "native_operations": 72, + "primitive_counts": { + "A": { + "add": 3557, + "scale": 498, + "warp": 24 + }, + "B": { + "add": 1796, + "scale": 73, + "warp": 0 + }, + "cleanup": { + "add": 4633, + "scale": 519, + "warp": 72 + }, + "restore": { + "add": 196, + "scale": 16, + "warp": 0 + } + }, + "profile": { + "1": 2440, + "2": 725, + "3": 224, + "4": 102, + "5": 20, + "8": 8 + }, + "semantics": { + "arbitrary_dirty_buffers": 91, + "buffer_self_map": "identity", + "buffer_to_live_leaks": 0, + "cleanup_boundary_both_directions": true, + "dual": true, + "dual_matrix_sha256": "9bace9fb7525f64d5418ab54af173df7d320c898e980e89be8a90d280adb3744", + "live_inputs": 632, + "matrix_dimension": 723, + "ordinary": true, + "ordinary_matrix_sha256": "c8ea87b1598c9bbc2b0be63217772110ff450ad12eff19aaf05a84239eb5d380", + "reverse_equals_ordinary": true + } + } + } + }, + "extra": { + "additional_cleanup_add_saving": 5, + "additional_forward_add_saving": 7, + "known_sites": 1, + "native_operators_changed": false, + "new_kappa": false, + "new_sites": 7, + "new_supplier": false, + "provider": "extra", + "recursive_moment_changed": false, + "schema_version": 1, + "sites": [ + { + "crossed_disjoint_events": 0, + "gates": [ + [ + "add", + 457, + 475, + -1, + 1, + [ + 82, + 42 + ] + ], + [ + "add", + 456, + 457, + 1, + 1, + [ + 82, + 42 + ] + ], + [ + "add", + 456, + 475, + 1, + 1, + [ + 82, + 42 + ] + ] + ], + "indices": [ + 1858, + 1859, + 1860 + ], + "known": true, + "removed_position": 2, + "replacement": [ + [ + "add", + 456, + 457, + 1, + 1, + [ + 42, + 82 + ] + ], + [ + "add", + 457, + 475, + -1, + 1, + [ + 42, + 82 + ] + ] + ], + "section": "A", + "support": [ + 456, + 457, + 475 + ] + }, + { + "crossed_disjoint_events": 48, + "gates": [ + [ + "add", + 196, + 518, + 1, + 1, + [ + 30 + ] + ], + [ + "add", + 196, + 588, + -1, + 1, + [ + 30 + ] + ], + [ + "add", + 588, + 518, + -1, + 1, + [ + 30 + ] + ] + ], + "indices": [ + 4, + 53, + 54 + ], + "known": false, + "removed_position": 0, + "replacement": [ + [ + "add", + 588, + 518, + -1, + 1, + [ + 30 + ] + ], + [ + "add", + 196, + 588, + -1, + 1, + [ + 30 + ] + ] + ], + "section": "B", + "support": [ + 196, + 518, + 588 + ] + }, + { + "crossed_disjoint_events": 41, + "gates": [ + [ + "add", + 187, + 506, + 1, + 1, + [ + 30 + ] + ], + [ + "add", + 187, + 586, + 1, + 2, + [ + 30 + ] + ], + [ + "add", + 586, + 506, + 2, + 1, + [ + 30 + ] + ] + ], + "indices": [ + 7, + 49, + 50 + ], + "known": false, + "removed_position": 0, + "replacement": [ + [ + "add", + 586, + 506, + 2, + 1, + [ + 30 + ] + ], + [ + "add", + 187, + 586, + 1, + 2, + [ + 30 + ] + ] + ], + "section": "B", + "support": [ + 187, + 506, + 586 + ] + }, + { + "crossed_disjoint_events": 14, + "gates": [ + [ + "add", + 448, + 231, + -1, + 1, + [ + 256, + 128, + 64, + 34, + 17, + 11, + 4 + ] + ], + [ + "add", + 484, + 448, + -1, + 1, + [ + 256, + 128, + 64, + 34, + 17, + 11, + 4 + ] + ], + [ + "add", + 484, + 231, + -1, + 1, + [ + 256, + 128, + 64, + 34, + 17, + 11, + 4 + ] + ] + ], + "indices": [ + 20, + 21, + 36 + ], + "known": false, + "removed_position": 2, + "replacement": [ + [ + "add", + 484, + 448, + -1, + 1, + [ + 256, + 128, + 64, + 34, + 17, + 11, + 4 + ] + ], + [ + "add", + 448, + 231, + -1, + 1, + [ + 256, + 128, + 64, + 34, + 17, + 11, + 4 + ] + ] + ], + "section": "restore", + "support": [ + 231, + 448, + 484 + ] + }, + { + "crossed_disjoint_events": 14, + "gates": [ + [ + "add", + 449, + 226, + -1, + 1, + [ + 256, + 128, + 64, + 34, + 17, + 11, + 4 + ] + ], + [ + "add", + 485, + 449, + -1, + 1, + [ + 256, + 128, + 64, + 34, + 17, + 11, + 4 + ] + ], + [ + "add", + 485, + 226, + -1, + 1, + [ + 256, + 128, + 64, + 34, + 17, + 11, + 4 + ] + ] + ], + "indices": [ + 22, + 23, + 38 + ], + "known": false, + "removed_position": 2, + "replacement": [ + [ + "add", + 485, + 449, + -1, + 1, + [ + 256, + 128, + 64, + 34, + 17, + 11, + 4 + ] + ], + [ + "add", + 449, + 226, + -1, + 1, + [ + 256, + 128, + 64, + 34, + 17, + 11, + 4 + ] + ] + ], + "section": "restore", + "support": [ + 226, + 449, + 485 + ] + }, + { + "crossed_disjoint_events": 23, + "gates": [ + [ + "add", + 451, + 228, + -1, + 1, + [ + 256, + 128, + 64, + 38, + 20, + 10, + 1 + ] + ], + [ + "add", + 509, + 451, + -1, + 1, + [ + 256, + 128, + 64, + 38, + 20, + 10, + 1 + ] + ], + [ + "add", + 509, + 228, + -1, + 1, + [ + 256, + 128, + 64, + 38, + 20, + 10, + 1 + ] + ] + ], + "indices": [ + 26, + 27, + 51 + ], + "known": false, + "removed_position": 2, + "replacement": [ + [ + "add", + 509, + 451, + -1, + 1, + [ + 256, + 128, + 64, + 38, + 20, + 10, + 1 + ] + ], + [ + "add", + 451, + 228, + -1, + 1, + [ + 256, + 128, + 64, + 38, + 20, + 10, + 1 + ] + ] + ], + "section": "restore", + "support": [ + 228, + 451, + 509 + ] + }, + { + "crossed_disjoint_events": 30, + "gates": [ + [ + "add", + 453, + 7, + -1, + 1, + [ + 256, + 128, + 64, + 32, + 19, + 11, + 6 + ] + ], + [ + "add", + 533, + 453, + 2, + 1, + [ + 256, + 128, + 64, + 32, + 19, + 11, + 6 + ] + ], + [ + "add", + 533, + 7, + 2, + 1, + [ + 256, + 128, + 64, + 32, + 19, + 11, + 6 + ] + ] + ], + "indices": [ + 30, + 31, + 62 + ], + "known": false, + "removed_position": 2, + "replacement": [ + [ + "add", + 533, + 453, + 2, + 1, + [ + 256, + 128, + 64, + 32, + 19, + 11, + 6 + ] + ], + [ + "add", + 453, + 7, + -1, + 1, + [ + 256, + 128, + 64, + 32, + 19, + 11, + 6 + ] + ] + ], + "section": "restore", + "support": [ + 7, + 453, + 533 + ] + }, + { + "crossed_disjoint_events": 39, + "gates": [ + [ + "add", + 454, + 236, + -1, + 1, + [ + 256, + 128, + 64, + 37, + 21, + 8, + 3 + ] + ], + [ + "add", + 556, + 454, + 2, + 1, + [ + 256, + 128, + 64, + 37, + 21, + 8, + 3 + ] + ], + [ + "add", + 556, + 236, + 2, + 1, + [ + 256, + 128, + 64, + 37, + 21, + 8, + 3 + ] + ] + ], + "indices": [ + 32, + 33, + 73 + ], + "known": false, + "removed_position": 2, + "replacement": [ + [ + "add", + 556, + 454, + 2, + 1, + [ + 256, + 128, + 64, + 37, + 21, + 8, + 3 + ] + ], + [ + "add", + 454, + 236, + -1, + 1, + [ + 256, + 128, + 64, + 37, + 21, + 8, + 3 + ] + ] + ], + "section": "restore", + "support": [ + 236, + 454, + 556 + ] + } + ], + "words": { + "credited_3998": { + "canonical_word_sha256": "439ce3544b68e3dffdb0cb4496fbc92330e825592515bc28c95580807c9d232d", + "cleanup_sha256": "7c2a181ac7fc6a087f5c7cce346650e0bb773f5dafa82ca966081a4a6440c336", + "helper_widths": { + "4": 26, + "5": 2, + "6": 18, + "7": 53, + "8": 96, + "9": 213 + }, + "lengths": { + "A": 4078, + "B": 1869, + "cleanup": 5223, + "restore": 212 + }, + "native_operations": 72, + "primitive_counts": { + "A": { + "add": 3556, + "scale": 498, + "warp": 24 + }, + "B": { + "add": 1796, + "scale": 73, + "warp": 0 + }, + "cleanup": { + "add": 4632, + "scale": 519, + "warp": 72 + }, + "restore": { + "add": 196, + "scale": 16, + "warp": 0 + } + }, + "profile": { + "1": 2440, + "2": 725, + "3": 224, + "4": 102, + "5": 20, + "8": 8 + }, + "semantics": { + "arbitrary_dirty_buffers": 91, + "buffer_self_map": "identity", + "buffer_to_live_leaks": 0, + "cleanup_boundary_both_directions": true, + "dual": true, + "dual_matrix_sha256": "9bace9fb7525f64d5418ab54af173df7d320c898e980e89be8a90d280adb3744", + "live_inputs": 632, + "matrix_dimension": 723, + "ordinary": true, + "ordinary_matrix_sha256": "c8ea87b1598c9bbc2b0be63217772110ff450ad12eff19aaf05a84239eb5d380", + "reverse_equals_ordinary": true + } + }, + "separated": { + "canonical_word_sha256": "0cc6001f57d842b39ccc8d508d26d86a8e2eda976161130940746f4b1d02bd96", + "cleanup_sha256": "a20cef30d1adbaa529d96f2055bf3f203cbf1f15438de04ec34c3fb7a7372906", + "helper_widths": { + "4": 26, + "5": 2, + "6": 18, + "7": 53, + "8": 96, + "9": 213 + }, + "lengths": { + "A": 4078, + "B": 1867, + "cleanup": 5218, + "restore": 207 + }, + "native_operations": 72, + "primitive_counts": { + "A": { + "add": 3556, + "scale": 498, + "warp": 24 + }, + "B": { + "add": 1794, + "scale": 73, + "warp": 0 + }, + "cleanup": { + "add": 4627, + "scale": 519, + "warp": 72 + }, + "restore": { + "add": 191, + "scale": 16, + "warp": 0 + } + }, + "profile": { + "1": 2440, + "2": 725, + "3": 224, + "4": 102, + "5": 20, + "8": 8 + }, + "semantics": { + "arbitrary_dirty_buffers": 91, + "buffer_self_map": "identity", + "buffer_to_live_leaks": 0, + "cleanup_boundary_both_directions": true, + "dual": true, + "dual_matrix_sha256": "9bace9fb7525f64d5418ab54af173df7d320c898e980e89be8a90d280adb3744", + "live_inputs": 632, + "matrix_dimension": 723, + "ordinary": true, + "ordinary_matrix_sha256": "c8ea87b1598c9bbc2b0be63217772110ff450ad12eff19aaf05a84239eb5d380", + "reverse_equals_ordinary": true + } + }, + "source": { + "canonical_word_sha256": "309e6b90bad582081b90cce08f820da62ab11602a8298852cb7ef6f16b8942c8", + "cleanup_sha256": "cfcb7fbc44fb3e14c6edd781f1fb57ea25ade9a96c0ef4873bf8d4c1eb7a02e2", + "helper_widths": { + "4": 26, + "5": 2, + "6": 18, + "7": 53, + "8": 96, + "9": 213 + }, + "lengths": { + "A": 4079, + "B": 1869, + "cleanup": 5224, + "restore": 212 + }, + "native_operations": 72, + "primitive_counts": { + "A": { + "add": 3557, + "scale": 498, + "warp": 24 + }, + "B": { + "add": 1796, + "scale": 73, + "warp": 0 + }, + "cleanup": { + "add": 4633, + "scale": 519, + "warp": 72 + }, + "restore": { + "add": 196, + "scale": 16, + "warp": 0 + } + }, + "profile": { + "1": 2440, + "2": 725, + "3": 224, + "4": 102, + "5": 20, + "8": 8 + }, + "semantics": { + "arbitrary_dirty_buffers": 91, + "buffer_self_map": "identity", + "buffer_to_live_leaks": 0, + "cleanup_boundary_both_directions": true, + "dual": true, + "dual_matrix_sha256": "9bace9fb7525f64d5418ab54af173df7d320c898e980e89be8a90d280adb3744", + "live_inputs": 632, + "matrix_dimension": 723, + "ordinary": true, + "ordinary_matrix_sha256": "c8ea87b1598c9bbc2b0be63217772110ff450ad12eff19aaf05a84239eb5d380", + "reverse_equals_ordinary": true + } + } + } + } + }, + "schema_version": 1 +} diff --git a/research/staged544-a2-composition-audit/verify.py b/research/staged544-a2-composition-audit/verify.py new file mode 100644 index 0000000000..fd3486d58d --- /dev/null +++ b/research/staged544-a2-composition-audit/verify.py @@ -0,0 +1,317 @@ +#!/usr/bin/env python3 +"""Independent acceptance of the PR #4019 separated-A2 composition argument. + +This checker does not import that package. It re-derives the two rational +identities from PROOF.md, classifies each frozen site, and counts the +projected-cleanup record split. It does not replay the recursive frame bill. +""" + +import gzip +import hashlib +import json +from fractions import Fraction +from itertools import permutations +from pathlib import Path + +HERE = Path(__file__).resolve().parent +V = 112 + +PINS = { + "base": "5ca4be99851f8878cbfe0fd6c454df926b11218f17feefa1664721cf03156699", + "extra": "965268a9be73d3f62e7ef680d18f108cf064bfe1f44b82157baa61443232904e", +} +RECEIPT_SHA256 = "cbfefac6c10f68b55208458cf2d07b2a67f2f9ece037fa53fa7070647a21b82e" + +# Section, three increasing indices, removed position, whether the site is the +# credited PR #3998 contraction rather than one of the seven new witnesses. +SITES = ( + ("A", (1858, 1859, 1860), 2, True), + ("B", (4, 53, 54), 0, False), + ("B", (7, 49, 50), 0, False), + ("restore", (20, 21, 36), 2, False), + ("restore", (22, 23, 38), 2, False), + ("restore", (26, 27, 51), 2, False), + ("restore", (30, 31, 62), 2, False), + ("restore", (32, 33, 73), 2, False), +) + + +class Rejected(Exception): + pass + + +def require(condition, message): + if not condition: + raise Rejected(message) + + +def no_duplicates(pairs): + answer = {} + for key, value in pairs: + require(key not in answer, "duplicate JSON key " + str(key)) + answer[key] = value + return answer + + +def sha256(data): + return hashlib.sha256(data).hexdigest() + + +def is_target(register): + return V <= register < 2 * V + + +def coefficient(gate): + require(gate[0] in ("add", "scale"), "scalar alphabet") + index = 3 if gate[0] == "add" else 2 + numerator, denominator = gate[index:index + 2] + require(type(numerator) is int and type(denominator) is int and denominator != 0 + and numerator != 0, "nonzero rational coefficient") + return Fraction(numerator, denominator) + + +def touched(gate): + if gate[0] == "add": + require(len(gate) == 6, "add layout") + registers = gate[1:3] + elif gate[0] == "scale": + require(len(gate) == 5, "scale layout") + registers = gate[1:2] + else: + raise Rejected("unexpected event " + str(gate[0])) + require(all(type(register) is int and 0 <= register < 704 for register in registers), + "register domain") + return set(registers) + + +def apply_matrix(gates, registers): + """Left-action of chronological ADDs on the ordered register basis.""" + index = {register: place for place, register in enumerate(registers)} + matrix = [[Fraction(place == column) for column in range(3)] for place in range(3)] + for gate in gates: + require(gate[0] == "add", "identity alphabet") + weight = coefficient(gate) + destination, source = index[gate[1]], index[gate[2]] + for column in range(3): + matrix[destination][column] += weight * matrix[source][column] + return matrix + + +def endpoint(gates, x_reg, y_reg, z_reg, start): + value = {x_reg: start[0], y_reg: start[1], z_reg: start[2]} + for gate in gates: + value[gate[1]] += coefficient(gate) * value[gate[2]] + return (value[x_reg], value[y_reg], value[z_reg]) + + +def add_gate(destination, source, weight): + return ["add", destination, source, weight.numerator, weight.denominator, []] + + +def check_stated_endpoints(): + """PROOF.md's two endpoint formulas, on exact rationals, including a nonzero start.""" + x_reg, y_reg, z_reg = 0, 1, 2 + samples = ( + (Fraction(2), Fraction(-3), (Fraction(5), Fraction(-2), Fraction(7))), + (Fraction(1, 2), Fraction(4), (Fraction(0), Fraction(1), Fraction(-3))), + (Fraction(-1), Fraction(-1), (Fraction(9), Fraction(1, 3), Fraction(4))), + ) + for weight_a, weight_b, start in samples: + identity_one = [ + add_gate(y_reg, z_reg, weight_a), + add_gate(x_reg, y_reg, weight_b), + add_gate(x_reg, z_reg, -weight_a * weight_b), + ] + right_one = [add_gate(x_reg, y_reg, weight_b), add_gate(y_reg, z_reg, weight_a)] + expect_one = (start[0] + weight_b * start[1], start[1] + weight_a * start[2], start[2]) + identity_two = [ + add_gate(x_reg, z_reg, weight_a * weight_b), + add_gate(x_reg, y_reg, weight_b), + add_gate(y_reg, z_reg, weight_a), + ] + right_two = [add_gate(y_reg, z_reg, weight_a), add_gate(x_reg, y_reg, weight_b)] + expect_two = ( + start[0] + weight_b * start[1] + weight_a * weight_b * start[2], + start[1] + weight_a * start[2], + start[2], + ) + for gates, right, expect in ( + (identity_one, right_one, expect_one), + (identity_two, right_two, expect_two), + ): + require(endpoint(gates, x_reg, y_reg, z_reg, start) == expect, "stated endpoint") + require(endpoint(right, x_reg, y_reg, z_reg, start) == expect, "stated right-hand side") + require(apply_matrix(gates, [x_reg, y_reg, z_reg]) + == apply_matrix(right, [x_reg, y_reg, z_reg]), "matrix form") + wrong = [add_gate(y_reg, z_reg, Fraction(1)), add_gate(x_reg, y_reg, Fraction(1)), + add_gate(x_reg, z_reg, Fraction(1))] + require(endpoint(wrong, x_reg, y_reg, z_reg, (Fraction(0), Fraction(0), Fraction(1))) + != (Fraction(0), Fraction(1), Fraction(1)), "wrong sign must miss the identity-one endpoint") + + +def classify(gates): + """Match one ordered triple to exactly one of the two proof identities.""" + require(len(gates) == 3 and all(gate[0] == "add" for gate in gates), "three ADDs") + edges = [(gate[1], gate[2], coefficient(gate)) for gate in gates] + registers = [] + for register in [edge[0] for edge in edges] + [edge[1] for edge in edges]: + if register not in registers: + registers.append(register) + require(len(registers) == 3 and len({(edge[0], edge[1]) for edge in edges}) == 3, + "three distinct directed edges") + matches = [] + for x_reg, y_reg, z_reg in permutations(registers): + first, second, third = edges + if (first[0] == y_reg and first[1] == z_reg and second[0] == x_reg and second[1] == y_reg + and third[0] == x_reg and third[1] == z_reg and third[2] == -first[2] * second[2]): + matches.append(("id1_remove_last", x_reg, y_reg, z_reg, first[2], second[2])) + if (first[0] == x_reg and first[1] == z_reg and second[0] == x_reg and second[1] == y_reg + and third[0] == y_reg and third[1] == z_reg and first[2] == third[2] * second[2]): + matches.append(("id2_remove_first", x_reg, y_reg, z_reg, third[2], second[2])) + require(len(matches) == 1, "expected exactly one identity match") + return matches[0] + + +def predicted_replacement(kind, gates): + if kind == "id1_remove_last": + return [gates[1], gates[0]] + require(kind == "id2_remove_first", "unknown identity") + return [gates[2], gates[1]] + + +def same_add(left, right): + return left[:5] == right[:5] + + +def frames_same_span(left, right): + return sorted(left) == sorted(right) + + +def load_words(): + words = {} + for name, digest in PINS.items(): + path = HERE / "inputs" / ("BORROW-WORD-" + name + ".json.gz") + require(path.is_file() and not path.is_symlink(), "missing word " + name) + raw = path.read_bytes() + require(sha256(raw) == digest, "word byte pin " + name) + words[name] = json.loads(gzip.decompress(raw), object_pairs_hook=no_duplicates) + receipt_path = HERE / "inputs" / "data.json" + raw_receipt = receipt_path.read_bytes() + require(sha256(raw_receipt) == RECEIPT_SHA256, "published receipt pin") + receipt = json.loads(raw_receipt, object_pairs_hook=no_duplicates) + require(set(receipt) == {"schema_version", "providers"} and receipt["schema_version"] == 1, + "receipt schema") + return words, receipt + + +def audit_provider(word, receipt): + occupied = set() + forward_new = cleanup_new = known_swaps = 0 + for section, indices, central, known in SITES: + require(section in word and isinstance(word[section], list), "missing section") + require(indices[0] < indices[1] < indices[2] < len(word[section]), "site indices") + gates = [word[section][index] for index in indices] + kind, x_reg, y_reg, z_reg, _weight_a, _weight_b = classify(gates) + expected_central = 2 if kind == "id1_remove_last" else 0 + require(central == expected_central, "removed position disagrees with the identity") + replacement = predicted_replacement(kind, gates) + registers = sorted({x_reg, y_reg, z_reg}) + require(apply_matrix(gates, registers) == apply_matrix(replacement, registers), + "replacement operator") + frames = [tuple(gate[-1]) for gate in gates] + require(frames[0] == frames[1] == frames[2], "common ordered source frame") + require(all(tuple(gate[-1]) == frames[0] for gate in replacement), + "replacement keeps the source frame") + support = {x_reg, y_reg, z_reg} + require(occupied.isdisjoint(support), "site supports overlap") + occupied.update(support) + for index in range(indices[0], indices[-1] + 1): + if index in indices: + continue + require(touched(word[section][index]).isdisjoint(support), "intervening dependency") + if section == "A": + require(indices[0] >= word["prelude_events"], "prelude barrier") + if section == "B": + require(not any(indices[0] < warp[0] <= indices[-1] for warp in word["warps"]), + "native warp barrier") + if section == "restore": + require(all(not is_target(gate[1]) for gate in gates), "restore site writes a target") + if kind == "id2_remove_first": + require(is_target(gates[0][1]) and gates[0][1] == gates[1][1] and is_target(gates[1][1]), + "B contraction's first two ADDs must write the same target") + require(not is_target(gates[2][1]), "B contraction must keep one helper ADD") + published = next(site for site in receipt["sites"] if tuple(site["indices"]) == indices) + require(published["gates"] == gates, "receipt gates differ from the frozen word") + require(published["removed_position"] == central, "receipt removed position") + if known: + require(all(same_add(left, right) and frames_same_span(left[-1], right[-1]) + for left, right in zip(published["replacement"], replacement)), + "known-site replacement edges") + if published["replacement"] != replacement: + known_swaps += 1 + else: + require(published["replacement"] == replacement, "new-site replacement") + forward_new += 1 + if not is_target(gates[central][1]): + cleanup_new += 1 + require(len([gate for gate in gates if not is_target(gate[1])]) + == len([gate for gate in replacement if not is_target(gate[1])]) + 1, + "restore projection should drop one record") + else: + require([gate[:5] for gate in gates if not is_target(gate[1])] + == [gate[:5] for gate in replacement if not is_target(gate[1])], + "target deletion must preserve the helper ADD") + require((forward_new, cleanup_new) == (7, 5), "seven forward and five cleanup records") + require(known_swaps == 1, "the credited site's ordered-frame swap is part of the publication") + require(len(occupied) == 24, "eight disjoint three-register supports") + return forward_new, cleanup_new + + +def expect_rejected(label, function): + try: + function() + except Rejected: + return + raise Rejected("negative control escaped: " + label) + + +def negative_controls(words): + word = words["base"] + broken = json.loads(json.dumps(word)) + broken["B"][4][3] = -broken["B"][4][3] + expect_rejected("wrong sign", lambda: classify([broken["B"][index] for index in (4, 53, 54)])) + dependent = json.loads(json.dumps(word)) + dependent["B"][5][2] = 518 + expect_rejected( + "intervening read", + lambda: require(touched(dependent["B"][5]).isdisjoint({196, 518, 588}), "intervening dependency"), + ) + expect_rejected( + "wrong endpoint sign", + lambda: require( + endpoint( + [add_gate(1, 2, Fraction(1)), add_gate(0, 1, Fraction(1)), add_gate(0, 2, Fraction(1))], + 0, 1, 2, (Fraction(0), Fraction(0), Fraction(1)), + ) == (Fraction(0), Fraction(1), Fraction(1)), + "wrong sign must miss the identity-one endpoint", + ), + ) + + +def main(): + check_stated_endpoints() + words, receipt = load_words() + require(set(receipt["providers"]) == {"base", "extra"}, "both providers") + for name in ("base", "extra"): + forward, cleanup = audit_provider(words[name], receipt["providers"][name]) + require((forward, cleanup) == (7, 5), name) + negative_controls(words) + print("PASS_A2_COMPOSITION_AUDIT providers=2 sites=8 new_forward_adds=7 " + "new_cleanup_adds=5 known_frame_order_swaps=2 controls=3 no_new_kappa") + + +if __name__ == "__main__": + try: + main() + except Rejected as error: + raise SystemExit("FAIL_A2_COMPOSITION_AUDIT " + str(error))