From 2f79aebb959aa9e528c5c7d5f1314b685190e11f Mon Sep 17 00:00:00 2001 From: Wentao Li Date: Thu, 15 Oct 2026 12:17:36 +0000 Subject: [PATCH] Research: seed-7 H2-sem matching dominates #1805 F/ADD invoice Answer PR1805 open question 1 with a full H2-sem paid invoice: the same ADD-greedy helper-sharing rule at shuffle seed 7 strictly improves ADD count (-14), forward envelope F (-1576), and B (-8612) versus the published seed-42 matching, with unchanged paid profile mass 5129. Prepared by Wentao Li with substantial AI assistance. --- .../h2sem-matching-f-invoice/CERTIFICATE.json | 118 +++ .../h2sem-matching-f-invoice/MATCHING7.json | 839 ++++++++++++++++++ research/h2sem-matching-f-invoice/NOTICE.md | 6 + research/h2sem-matching-f-invoice/PROOF.md | 57 ++ research/h2sem-matching-f-invoice/README.md | 93 ++ .../h2sem-matching-f-invoice/SOURCES.json | 42 + research/h2sem-matching-f-invoice/SWEEP.json | 156 ++++ research/h2sem-matching-f-invoice/TASK.json | 68 ++ research/h2sem-matching-f-invoice/VERIFY.json | 45 + .../h2sem-matching-f-invoice/test_package.py | 95 ++ research/h2sem-matching-f-invoice/verify.py | 520 +++++++++++ 11 files changed, 2039 insertions(+) create mode 100644 research/h2sem-matching-f-invoice/CERTIFICATE.json create mode 100644 research/h2sem-matching-f-invoice/MATCHING7.json create mode 100644 research/h2sem-matching-f-invoice/NOTICE.md create mode 100644 research/h2sem-matching-f-invoice/PROOF.md create mode 100644 research/h2sem-matching-f-invoice/README.md create mode 100644 research/h2sem-matching-f-invoice/SOURCES.json create mode 100644 research/h2sem-matching-f-invoice/SWEEP.json create mode 100644 research/h2sem-matching-f-invoice/TASK.json create mode 100644 research/h2sem-matching-f-invoice/VERIFY.json create mode 100644 research/h2sem-matching-f-invoice/test_package.py create mode 100644 research/h2sem-matching-f-invoice/verify.py diff --git a/research/h2sem-matching-f-invoice/CERTIFICATE.json b/research/h2sem-matching-f-invoice/CERTIFICATE.json new file mode 100644 index 0000000000..3b8fa65155 --- /dev/null +++ b/research/h2sem-matching-f-invoice/CERTIFICATE.json @@ -0,0 +1,118 @@ +{ + "status": "PASS_H2SEM_MATCHING_F_INVOICE", + "task_id": "bit-helper-contract", + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "columns": 661, + "census42": { + "operands": 430, + "oriented_pairs": 184470, + "positive_pairs": 41404, + "best_saving": 65, + "best_pair": [ + 277, + 434 + ], + "matching_pairs": 205, + "matching_saving": 6231, + "seed": 42 + }, + "census7": { + "operands": 430, + "oriented_pairs": 184470, + "positive_pairs": 41404, + "best_saving": 65, + "best_pair": [ + 382, + 306 + ], + "matching_pairs": 208, + "matching_saving": 6245, + "seed": 7 + }, + "bills": { + "base": { + "native_ADDs": 24305, + "D_adds": 18085, + "F": 49347, + "B": 1113070, + "local_bits": 93, + "nine_stage_bits": 177 + }, + "match42": { + "native_ADDs": 18074, + "D_adds": 11854, + "F": 75381, + "B": 1196402, + "local_bits": 95, + "nine_stage_bits": 180 + }, + "match7": { + "native_ADDs": 18060, + "D_adds": 11840, + "F": 73805, + "B": 1187790, + "local_bits": 95, + "nine_stage_bits": 180 + }, + "prefix50_seed7": { + "native_ADDs": 21556, + "D_adds": 15336, + "F": 56603, + "B": 1113070, + "local_bits": 94, + "nine_stage_bits": 178 + } + }, + "deltas_7_minus_42": { + "add_saving_lift": -14, + "F_lift": -1576, + "B_lift": -8612, + "pairs_lift": 3, + "pair_overlap": 150 + }, + "paid_profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rank_mass": 5129, + "h2sem": { + "shape": true, + "semantic_N_equals_baseline": true, + "syntactic_H2_K": { + "base": { + "H2": true, + "K_equals_D": true + }, + "match42": { + "H2": false, + "K_equals_D": false + }, + "match7": { + "H2": false, + "K_equals_D": false + } + } + }, + "controls": [ + "unrestored_helper_temp", + "wrong_restore_operand", + "target_feeds_helper", + "source_reads_in_D", + "prefix50_not_dominating_full", + "seed42_ne_seed7_pairset", + "mutated_body_changes_N" + ], + "kappa_claim": "none", + "new_kappa": false, + "matching7": { + "path": "MATCHING7.json", + "sha256": "2edd188162f5ec737060c3646ac5ac6924854a0d53e2bf244242b01a265324e5", + "pair_count": 208, + "saving": 6245 + } +} diff --git a/research/h2sem-matching-f-invoice/MATCHING7.json b/research/h2sem-matching-f-invoice/MATCHING7.json new file mode 100644 index 0000000000..3eb2bd59e8 --- /dev/null +++ b/research/h2sem-matching-f-invoice/MATCHING7.json @@ -0,0 +1,839 @@ +{ + "seed": 7, + "pairs": [ + [ + 382, + 306 + ], + [ + 277, + 434 + ], + [ + 351, + 377 + ], + [ + 644, + 593 + ], + [ + 596, + 656 + ], + [ + 295, + 404 + ], + [ + 612, + 625 + ], + [ + 569, + 530 + ], + [ + 639, + 615 + ], + [ + 631, + 624 + ], + [ + 451, + 461 + ], + [ + 597, + 657 + ], + [ + 518, + 554 + ], + [ + 392, + 307 + ], + [ + 443, + 427 + ], + [ + 278, + 268 + ], + [ + 285, + 436 + ], + [ + 290, + 294 + ], + [ + 386, + 286 + ], + [ + 248, + 238 + ], + [ + 492, + 466 + ], + [ + 282, + 435 + ], + [ + 262, + 415 + ], + [ + 342, + 332 + ], + [ + 559, + 528 + ], + [ + 617, + 641 + ], + [ + 643, + 594 + ], + [ + 430, + 257 + ], + [ + 227, + 458 + ], + [ + 444, + 470 + ], + [ + 259, + 424 + ], + [ + 273, + 431 + ], + [ + 287, + 402 + ], + [ + 452, + 224 + ], + [ + 525, + 561 + ], + [ + 504, + 247 + ], + [ + 616, + 640 + ], + [ + 274, + 284 + ], + [ + 514, + 303 + ], + [ + 510, + 487 + ], + [ + 456, + 237 + ], + [ + 374, + 506 + ], + [ + 568, + 531 + ], + [ + 347, + 551 + ], + [ + 418, + 254 + ], + [ + 264, + 536 + ], + [ + 658, + 598 + ], + [ + 634, + 622 + ], + [ + 571, + 326 + ], + [ + 603, + 517 + ], + [ + 629, + 608 + ], + [ + 651, + 558 + ], + [ + 547, + 440 + ], + [ + 538, + 450 + ], + [ + 496, + 313 + ], + [ + 296, + 582 + ], + [ + 501, + 252 + ], + [ + 417, + 423 + ], + [ + 304, + 393 + ], + [ + 361, + 515 + ], + [ + 606, + 469 + ], + [ + 544, + 312 + ], + [ + 486, + 243 + ], + [ + 240, + 425 + ], + [ + 414, + 283 + ], + [ + 488, + 318 + ], + [ + 484, + 499 + ], + [ + 400, + 390 + ], + [ + 511, + 585 + ], + [ + 276, + 437 + ], + [ + 396, + 299 + ], + [ + 465, + 507 + ], + [ + 495, + 438 + ], + [ + 462, + 349 + ], + [ + 447, + 226 + ], + [ + 584, + 468 + ], + [ + 405, + 401 + ], + [ + 245, + 454 + ], + [ + 429, + 490 + ], + [ + 309, + 442 + ], + [ + 449, + 250 + ], + [ + 338, + 334 + ], + [ + 356, + 328 + ], + [ + 389, + 649 + ], + [ + 335, + 239 + ], + [ + 421, + 272 + ], + [ + 261, + 364 + ], + [ + 453, + 230 + ], + [ + 258, + 280 + ], + [ + 292, + 420 + ], + [ + 329, + 270 + ], + [ + 370, + 373 + ], + [ + 464, + 241 + ], + [ + 331, + 249 + ], + [ + 327, + 376 + ], + [ + 279, + 363 + ], + [ + 269, + 387 + ], + [ + 315, + 265 + ], + [ + 300, + 380 + ], + [ + 316, + 242 + ], + [ + 223, + 260 + ], + [ + 403, + 308 + ], + [ + 305, + 394 + ], + [ + 266, + 419 + ], + [ + 317, + 460 + ], + [ + 324, + 337 + ], + [ + 411, + 301 + ], + [ + 271, + 471 + ], + [ + 463, + 319 + ], + [ + 368, + 467 + ], + [ + 459, + 231 + ], + [ + 320, + 225 + ], + [ + 388, + 422 + ], + [ + 346, + 433 + ], + [ + 357, + 233 + ], + [ + 383, + 375 + ], + [ + 344, + 355 + ], + [ + 378, + 379 + ], + [ + 228, + 246 + ], + [ + 416, + 354 + ], + [ + 348, + 352 + ], + [ + 330, + 413 + ], + [ + 281, + 256 + ], + [ + 432, + 336 + ], + [ + 263, + 339 + ], + [ + 297, + 293 + ], + [ + 288, + 391 + ], + [ + 291, + 321 + ], + [ + 367, + 235 + ], + [ + 314, + 406 + ], + [ + 244, + 455 + ], + [ + 407, + 298 + ], + [ + 333, + 343 + ], + [ + 275, + 441 + ], + [ + 362, + 426 + ], + [ + 448, + 251 + ], + [ + 255, + 428 + ], + [ + 253, + 229 + ], + [ + 395, + 311 + ], + [ + 398, + 289 + ], + [ + 234, + 509 + ], + [ + 236, + 457 + ], + [ + 399, + 410 + ], + [ + 310, + 408 + ], + [ + 323, + 381 + ], + [ + 360, + 371 + ], + [ + 341, + 369 + ], + [ + 642, + 439 + ], + [ + 491, + 345 + ], + [ + 562, + 412 + ], + [ + 607, + 445 + ], + [ + 532, + 350 + ], + [ + 626, + 446 + ], + [ + 542, + 384 + ], + [ + 610, + 627 + ], + [ + 545, + 581 + ], + [ + 633, + 621 + ], + [ + 564, + 523 + ], + [ + 565, + 534 + ], + [ + 522, + 553 + ], + [ + 577, + 302 + ], + [ + 646, + 591 + ], + [ + 587, + 548 + ], + [ + 650, + 602 + ], + [ + 527, + 563 + ], + [ + 512, + 494 + ], + [ + 628, + 609 + ], + [ + 648, + 589 + ], + [ + 513, + 372 + ], + [ + 599, + 659 + ], + [ + 497, + 366 + ], + [ + 618, + 637 + ], + [ + 566, + 533 + ], + [ + 502, + 483 + ], + [ + 619, + 636 + ], + [ + 623, + 635 + ], + [ + 560, + 524 + ], + [ + 590, + 647 + ], + [ + 529, + 570 + ], + [ + 654, + 601 + ], + [ + 557, + 521 + ], + [ + 592, + 645 + ], + [ + 508, + 359 + ], + [ + 482, + 503 + ], + [ + 614, + 638 + ], + [ + 552, + 583 + ], + [ + 481, + 232 + ], + [ + 660, + 595 + ], + [ + 556, + 520 + ], + [ + 498, + 353 + ], + [ + 652, + 604 + ], + [ + 567, + 546 + ], + [ + 620, + 632 + ], + [ + 549, + 586 + ], + [ + 605, + 653 + ], + [ + 493, + 365 + ], + [ + 485, + 397 + ], + [ + 575, + 539 + ], + [ + 600, + 655 + ], + [ + 409, + 222 + ], + [ + 519, + 555 + ], + [ + 537, + 573 + ], + [ + 576, + 535 + ], + [ + 579, + 543 + ], + [ + 526, + 385 + ], + [ + 325, + 358 + ], + [ + 630, + 322 + ], + [ + 588, + 267 + ] + ], + "saving": 6245, + "pair_count": 208 +} diff --git a/research/h2sem-matching-f-invoice/NOTICE.md b/research/h2sem-matching-f-invoice/NOTICE.md new file mode 100644 index 0000000000..236ecc1799 --- /dev/null +++ b/research/h2sem-matching-f-invoice/NOTICE.md @@ -0,0 +1,6 @@ +This package is Apache-2.0. + +Predecessor notices and licenses for the consumed R439 word, owner checker, +PR848 matching rule, PR1194 H2-sem contract and PR1805 seed-42 invoice remain +with their original packages and authors. This directory adds only the seed-7 +matching invoice and its verifier. diff --git a/research/h2sem-matching-f-invoice/PROOF.md b/research/h2sem-matching-f-invoice/PROOF.md new file mode 100644 index 0000000000..86b7bb7bfb --- /dev/null +++ b/research/h2sem-matching-f-invoice/PROOF.md @@ -0,0 +1,57 @@ +# Seed-7 matching dominates the published seed-42 H2-sem invoice + +**Scoped priced invoice. No new κ.** + +## Setup + +Let `W` be the selected PR589 R439 word. PR848's helper-temp wrap for an +oriented helper pair `(a,b)` prepends `a ^= b`, rewrites every D row containing +`a` by symmetric difference with `b`, and appends the reverse restoration. +Positive oriented pairs are those with arithmetic source-read saving + +`sum_{rows containing a} (1_{b in row} - 1_{b not in row}) - 2 > 0`. + +An ADD-greedy matching shuffles the positive list with a fixed seed, sorts by +nonincreasing saving (stable), and takes a maximal disjoint subset. + +## Published baseline (PR1805) + +Seed `42` yields 205 pairs and saving 6,231. Under H2-sem the completed wrap +has whole-word ADD count 18,074, forward envelope `F = 75,381`, reverse +envelope `B = 1,196,402`, paid profile mass 5,129, and strict precision guards. + +## Improved matching + +Seed `7` yields 208 pairs and saving **6,245**. The completed wrap has + +- ADD count **18,060** (14 better than seed-42), +- `F = 73,805` (1,576 lower), +- `B = 1,187,790` (8,612 lower), +- the same paid profile `{1:1323,…,7:19}` and rank mass 5,129, +- local/nine-stage bits 95/180 (still under 104/192). + +The unordered pair sets share 150 pairs and differ elsewhere; the saving=65 +champion pair `(277,434)` appears in both. Semantic matrix `N` equals the +baseline on all 661 formal columns; complete forward/reverse COPY/ERASE +boundaries equal the baseline endpoint. H2-sem shape conditions 1–2 hold; +syntactic H2 and `K_equals_D` fail exactly as on the seed-42 wrap. + +## Why the endpoint holds + +The wrap is chronologically `H; D0; H` with `H = H^{-1}` over F2, so the +composite equals the original D map on every F2 column (PR1194 / PR1805). Full +helper restoration is necessary: deleting a restore breaks the helper basis. +Equality of the 661 binary D columns therefore certifies the H2-sem boundary +for every F2-module stream under the common zero-frame reading. + +## Search scope + +Among ADD-greedy shuffles with seeds `0..255` and saving ≥ 6,200 (233 invoiced +matchings), seed-7 uniquely maximises ADD saving and, among savings ≥ 6,231, +minimises `F`. This bounds the stated search; it is not a theorem about every +matching. + +## Limits + +No kappa claim. No optimality outside ADD-greedy tie-breaks. Composition onto +the PR1062 star word is open #2033's object and is not attempted here. diff --git a/research/h2sem-matching-f-invoice/README.md b/research/h2sem-matching-f-invoice/README.md new file mode 100644 index 0000000000..9bf3a9e7fd --- /dev/null +++ b/research/h2sem-matching-f-invoice/README.md @@ -0,0 +1,93 @@ +# H2-sem matching F invoice: seed-7 dominates seed-42 + +**Priced finite invoice under the H2-sem replacement interface; no new κ.** +Answers open question 1 of +[CrocSwap/integer-mult-bounds#1805](https://github.com/CrocSwap/integer-mult-bounds/pull/1805): +can a different disjoint helper-sharing matching lower forward envelope `F` +while keeping most of the ADD saving? + +Yes. The same PR848 ADD-greedy rule with shuffle seed **7** (instead of the +published seed **42**) produces a disjoint matching that **strictly dominates** +the #1805 seed-42 invoice on ADD count, `F`, and `B`: + +| word | pairs | ADDs | D ADDs | F | B | local / nine-stage | +|---|---:|---:|---:|---:|---:|---:| +| baseline PR589 | — | 24,305 | 18,085 | 49,347 | 1,113,070 | 93 / 177 | +| seed-42 matching (#1805) | 205 | **18,074** | 11,854 | **75,381** | 1,196,402 | 95 / 180 | +| **seed-7 matching (this)** | **208** | **18,060** | **11,840** | **73,805** | **1,187,790** | 95 / 180 | +| seed-7 minus seed-42 | +3 | **−14** | −14 | **−1,576** | −8,612 | — | + +Complete dirty F2 boundaries and semantic `N` are unchanged from baseline on +both wraps; paid profile mass **5,129** is unchanged; local/nine-stage guards +remain strict. The unordered pair sets overlap in 150 pairs and differ in the +rest (tie-breaking among equal ADD savings). Champion pair `277→434` is present +in both matchings. + +A bounded screen of ADD-greedy shuffles over seeds `0..255` (233 matchings with +saving ≥ 6,200 invoiced) found no point that beats seed-7 on both ADD saving and +`F` simultaneously; seed-7 is the unique maximum-saving point in that screen and +also the minimum-`F` point among savings ≥ 6,231. This is **not** a claim of +optimality outside ADD-greedy shuffle tie-breaks. + +## Reproduce + +Python **3.12**, standard library only, from the repository root: + +```sh +python3.12 -I -B research/h2sem-matching-f-invoice/verify.py +python3.12 -I -O -B research/h2sem-matching-f-invoice/verify.py +python3.12 -I -B research/h2sem-matching-f-invoice/test_package.py +python3.12 scripts/research_package.py --package research/h2sem-matching-f-invoice +``` + +Expected: + +```text +PASS_H2SEM_MATCHING_F_INVOICE seed42_pairs=205 adds=24305->18074 F=75381 seed7_pairs=208 adds=24305->18060 F=73805 delta_adds=-14 delta_F=-1576 profile_mass=5129 columns=661 controls=7 no_new_kappa +PASS_REGISTERED_RESEARCH_PACKAGE research/h2sem-matching-f-invoice outcome=completed +``` + +Read-only replay compares to [CERTIFICATE.json](CERTIFICATE.json) and +[MATCHING7.json](MATCHING7.json). Pass `--write` only to regenerate those +receipts. Admission uses `need()` (not `assert`); `-O` also passes. + +## Evidence map + +| Claim | Where | +|---|---| +| Seed-42 invoice reproduces #1805 | `verify.py` bills `match42` | +| Seed-7 ADD-greedy matching + full invoice | `MATCHING7.json`, bills `match7` | +| Strict dominance deltas | `CERTIFICATE.json` `deltas_7_minus_42` | +| H2-sem shape, semantic N, 661-column boundary | `verify.py` | +| Paid profile / rank mass 5129 | owner checker `xcheck_p.py` | +| Prefix-50 does not dominate full seed-7 | bill `prefix50_seed7` | +| Bounded seed screen summary | [SWEEP.json](SWEEP.json) | + +## Scope limits + +No new kappa, frontier, native/hosted admission, or compiler/tape claim. Paid +profile unchanged; bit side nonbinding. Does not claim optimality over all +matchings or non-greedy constructions. Does not re-derive #1782/#1194; prices +wraps under that admitted interface. Open #2033 already answers #1805 question 2 +(composition onto the PR1062 star word) and is not consumed. + +## Open next questions + +1. **Is there a non-greedy disjoint matching with saving ≥ 6245 and F < 73805?** + Why it matters: the seed screen only varies ADD-greedy tie-breaks. First step: + local search from seed-7 with single pair swaps scored by exact `F`. Blocked by: + no cheaper exact point is known. +2. **Can a joint (ADD, F) objective on the star word (#2033) recover a net saving?** + Why it matters: #2033 showed the fixed pair costs +3 to +9 on PR1062; a + different matching might still help. First step: port this invoice to the + 11,500-ADD star D. Blocked by: star composition overhead. + +## Credit + +Credit **Aaron Wang / PR848** (pair census and ADD-greedy matching rule), +**navinor / PR1782** (H2-sem admission), **Wentao Li / PR1805** (seed-42 invoice +and the open F question answered here), **woklerx / PR1194** (H2-sem contract), +**DreamingOfClouds / PR589** and **eumemic / PR555** (R439 word). Prepared by +Wentao Li ([VictorLiwentao](https://github.com/VictorLiwentao), +[@Is__Victor](https://x.com/Is__Victor)) with substantial AI assistance. +Apache-2.0. No independent human review or multiplication theorem is claimed. diff --git a/research/h2sem-matching-f-invoice/SOURCES.json b/research/h2sem-matching-f-invoice/SOURCES.json new file mode 100644 index 0000000000..f11faac8ae --- /dev/null +++ b/research/h2sem-matching-f-invoice/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + }, + { + "path": "research/e8-bit-p111-tuned/code/xcheck_p.py", + "usage": "input", + "git_blob": "184f5dcf94a486cc7db91ca4db5865916bf26009", + "sha256": "af3decc877e27c00001cf56f50c6c09566e8e101297ab34c7860aed96a06d80e" + }, + { + "path": "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "usage": "input", + "git_blob": "85a4499bf9e4911a705d50567a2c2ef6cf23739a", + "sha256": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f" + }, + { + "path": "research/r439-copy-path-sharing-barrier/verify.py", + "usage": "input", + "git_blob": "5636566096d20039b3092819b0f4d1a283d66436", + "sha256": "1863b99b132bc5764508a18167303aaff32c815dc73a8693b84fe89a20301c86" + }, + { + "path": "research/r439-semantic-d-contract-seed10/PROOF.md", + "usage": "input", + "git_blob": "2707fdb0d2f34c1c6c4ea41c2a68e44904a3e4fd", + "sha256": "dfbca8c61a92fdf0db8af450dc4466849da37fc296e28b67f357e196e87327db" + } + ] +} diff --git a/research/h2sem-matching-f-invoice/SWEEP.json b/research/h2sem-matching-f-invoice/SWEEP.json new file mode 100644 index 0000000000..ac35129b73 --- /dev/null +++ b/research/h2sem-matching-f-invoice/SWEEP.json @@ -0,0 +1,156 @@ +{ + "screen": "ADD-greedy shuffle seeds 0..255; invoice when saving >= 6200", + "n_seeds": 256, + "n_invoiced": 233, + "seed42_reference": { + "seed": 42, + "pairs": 205, + "saving": 6231, + "F": 75381, + "ADDs": 18074, + "B": 1196402 + }, + "champion": { + "seed": 7, + "pairs": 208, + "saving": 6245, + "F": 73805, + "ADDs": 18060, + "B": 1187790 + }, + "pareto_saving_max_F_min": [ + { + "seed": 7, + "pairs": 208, + "saving": 6245, + "F": 73805, + "B": 1187790, + "ADDs": 18060, + "local": 95, + "nine": 180 + }, + { + "seed": 230, + "pairs": 206, + "saving": 6227, + "F": 73773, + "B": 1196586, + "ADDs": 18078, + "local": 95, + "nine": 180 + }, + { + "seed": 91, + "pairs": 205, + "saving": 6213, + "F": 73533, + "B": 1210534, + "ADDs": 18092, + "local": 95, + "nine": 180 + } + ], + "best_F_among_saving_ge_6231": [ + { + "seed": 7, + "pairs": 208, + "saving": 6245, + "F": 73805, + "B": 1187790, + "ADDs": 18060, + "local": 95, + "nine": 180 + }, + { + "seed": 19, + "pairs": 208, + "saving": 6239, + "F": 74073, + "B": 1171816, + "ADDs": 18066, + "local": 95, + "nine": 180 + }, + { + "seed": 36, + "pairs": 206, + "saving": 6233, + "F": 74117, + "B": 1189540, + "ADDs": 18072, + "local": 95, + "nine": 180 + }, + { + "seed": 140, + "pairs": 205, + "saving": 6232, + "F": 74293, + "B": 1196578, + "ADDs": 18073, + "local": 95, + "nine": 180 + }, + { + "seed": 213, + "pairs": 205, + "saving": 6231, + "F": 74357, + "B": 1170656, + "ADDs": 18074, + "local": 95, + "nine": 180 + }, + { + "seed": 200, + "pairs": 205, + "saving": 6232, + "F": 74401, + "B": 1204574, + "ADDs": 18073, + "local": 95, + "nine": 180 + }, + { + "seed": 33, + "pairs": 205, + "saving": 6231, + "F": 74541, + "B": 1167828, + "ADDs": 18074, + "local": 95, + "nine": 180 + }, + { + "seed": 240, + "pairs": 206, + "saving": 6231, + "F": 74577, + "B": 1218176, + "ADDs": 18074, + "local": 95, + "nine": 180 + }, + { + "seed": 89, + "pairs": 205, + "saving": 6243, + "F": 74641, + "B": 1187996, + "ADDs": 18062, + "local": 95, + "nine": 180 + }, + { + "seed": 215, + "pairs": 207, + "saving": 6232, + "F": 74757, + "B": 1206416, + "ADDs": 18073, + "local": 95, + "nine": 180 + } + ], + "note": "Not an optimality certificate outside ADD-greedy tie-breaks." +} diff --git a/research/h2sem-matching-f-invoice/TASK.json b/research/h2sem-matching-f-invoice/TASK.json new file mode 100644 index 0000000000..5448f45501 --- /dev/null +++ b/research/h2sem-matching-f-invoice/TASK.json @@ -0,0 +1,68 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 3, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "chooser_seed": "765323e87a2a23360fd03e811c6b225f", + "scope_key": "bfb61f829a81535adeae", + "original_card": { + "id": "bit-helper-contract", + "question": "Can one precisely specified helper-mixing word satisfy a replacement for the inherited H2/K interface?", + "starting_points": [ + "research/r439-bsection-stars-seed01/README.md", + "research/r439-copy-path-sharing-barrier/README.md" + ], + "methods": [ + "Derive a replacement interface lemma and price its implementation.", + "Seek an exact dirty-input or chronological-cut counterexample to the proposed replacement." + ], + "acceptance_gate": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient.", + "first_step": { + "command": [ + "python3", + "-B", + "research/r439-bsection-stars-seed01/verify.py" + ], + "expected": "PASS_R439_BSECTION_STARS", + "inspect": "Compare the two false H2/K flags with the unchanged paid profile in its README.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write one replacement H2/K implication for a single helper-star operation, then try to falsify it on dirty inputs.", + "bottleneck_link": "A legitimate replacement could admit a cheaper bit circuit; scalar savings alone do not alter the selected moment.", + "allowed_variations": [ + "Choose one helper-star or quartet instance; narrow to one boundary implication." + ], + "scope_change_triggers": [ + "Changing only source count or scalar addition count without an interface argument." + ], + "overlap_terms": [ + "H2_D_frame0_targets_from_helpers", + "K_equals_D", + "helper-star" + ] + }, + "scope_status": "refined", + "actual_scope": "Answer PR1805 open question 1 by exhibiting and fully invoicing one ADD-greedy H2-sem matching (shuffle seed 7) that strictly dominates the published seed-42 matching on ADD count, F and B, with unchanged paid profile and dirty boundary.", + "scope_change_reason": "PR1782/PR1805 already admit and price the seed-42 wraps under H2-sem. The card's acceptance gate (full boundary and paid profile) is applied to a new matching that improves the published (ADD,F) invoice; this is the stated next experiment of PR1805 rather than a new interface lemma.", + "bottleneck_link": "A lower-F H2-sem-legal D wrap improves precision headroom on the nonbinding bit side without changing the paid recursive profile or selected moment.", + "budget_minutes": 90, + "stop_rule": "Stop once one matching that strictly dominates seed-42 on ADD and F is fully invoiced with dirty controls, or after a bounded seed screen finds no such point.", + "outcome": "completed", + "evidence": "PASS_H2SEM_MATCHING_F_INVOICE: seed-7 matching 208 pairs saves 6245 ADDs (24305->18060) with F=73805 vs seed-42 6231/75381; deltas -14 ADDs and -1576 F; profile mass 5129; 661 columns; 7 controls; seed screen 0..255 recorded in SWEEP.json.", + "author": "Wentao Li", + "ai_assistance": "Substantial AI assistance for matching screen, invoice verifier, and package documentation", + "open_questions": [ + { + "question": "Is there a non-greedy disjoint matching with saving >= 6245 and F < 73805?", + "why_it_matters": "The seed screen only varies ADD-greedy tie-breaks; a genuine joint optimum could improve further.", + "first_step": "Local search from the seed-7 matching with single pair swaps scored by exact F.", + "blocked_by": "No cheaper exact point is known." + }, + { + "question": "Can a joint (ADD, F) objective on the PR1062 star word recover a net saving?", + "why_it_matters": "Open PR2033 showed the fixed pair costs +3 to +9 on the star word; a different matching might still help.", + "first_step": "Port this invoice method to the 11500-ADD star D.", + "blocked_by": "Star composition overhead on every candidate matching." + } + ] +} diff --git a/research/h2sem-matching-f-invoice/VERIFY.json b/research/h2sem-matching-f-invoice/VERIFY.json new file mode 100644 index 0000000000..62beb446c3 --- /dev/null +++ b/research/h2sem-matching-f-invoice/VERIFY.json @@ -0,0 +1,45 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "research/e8-bit-p111-tuned/code/xcheck_p.py", + "research/r439-copy-path-sharing-barrier/verify.py", + "research/r439-semantic-d-contract-seed10/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Pins, seed-42/seed-7 census, H2-sem shape, 661 D columns, full COPY/ERASE boundary, F/B dominance, paid profile, seven controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Identical PASS under -O (admission via need(), not assert)." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/test_package.py" + ], + "timeout_seconds": 300, + "checks": "Relocation smoke plus source-pin, certificate, matching and bill corruption controls." + } + ] +} diff --git a/research/h2sem-matching-f-invoice/test_package.py b/research/h2sem-matching-f-invoice/test_package.py new file mode 100644 index 0000000000..1a624b1028 --- /dev/null +++ b/research/h2sem-matching-f-invoice/test_package.py @@ -0,0 +1,95 @@ +#!/usr/bin/env python3 +"""Relocation smoke and corruption controls for h2sem-matching-f-invoice.""" +from __future__ import annotations + +import json +import os +import shutil +import subprocess +import sys +import tempfile +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +PASS = "PASS_H2SEM_MATCHING_F_INVOICE" + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def run(args, cwd, expect_ok): + env = {k: v for k, v in os.environ.items() if k != "PYTHONOPTIMIZE"} + proc = subprocess.run(args, cwd=cwd, capture_output=True, text=True, env=env) + ok = proc.returncode == 0 and PASS in proc.stdout + if expect_ok: + need(ok, "expected PASS, got code=%s out=%r err=%r" + % (proc.returncode, proc.stdout[-500:], proc.stderr[-500:])) + else: + need(not ok, "corrupt package unexpectedly passed") + return proc + + +def main(): + with tempfile.TemporaryDirectory(prefix="h2sem-matching-f-") as tmp: + tmp = Path(tmp) + dest_root = tmp / "repo with spaces" + pkg = dest_root / "research" / "h2sem-matching-f-invoice" + pkg.parent.mkdir(parents=True) + + shutil.copytree(HERE, pkg) + pins = json.loads((HERE / "SOURCES.json").read_text(encoding="utf-8")) + for item in pins["files"]: + src = ROOT / item["path"] + target = dest_root / item["path"] + target.parent.mkdir(parents=True, exist_ok=True) + shutil.copy2(src, target) + + py = sys.executable + run([py, "-I", "-B", str(pkg / "verify.py")], dest_root, True) + + # Corruption 1: mutate a live input pin byte. + word = dest_root / "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz" + blob = bytearray(word.read_bytes()) + blob[0] ^= 0xFF + word.write_bytes(blob) + run([py, "-I", "-B", str(pkg / "verify.py")], dest_root, False) + shutil.copy2(ROOT / "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", word) + + # Corruption 2: mutate certificate F bill. + cert = pkg / "CERTIFICATE.json" + data = json.loads(cert.read_text(encoding="utf-8")) + data["bills"]["match7"]["F"] += 1 + cert.write_text(json.dumps(data, indent=2) + "\n", encoding="utf-8") + run([py, "-I", "-B", str(pkg / "verify.py")], dest_root, False) + shutil.copy2(HERE / "CERTIFICATE.json", cert) + + # Corruption 3: mutate MATCHING7 pair list. + matching = pkg / "MATCHING7.json" + mdata = json.loads(matching.read_text(encoding="utf-8")) + mdata["pairs"] = mdata["pairs"][:-1] + mdata["pair_count"] = len(mdata["pairs"]) + matching.write_text(json.dumps(mdata, indent=2) + "\n", encoding="utf-8") + run([py, "-I", "-B", str(pkg / "verify.py")], dest_root, False) + shutil.copy2(HERE / "MATCHING7.json", matching) + + # Corruption 4: Boolean substituted for integer rank_mass. + data = json.loads(cert.read_text(encoding="utf-8")) + data["rank_mass"] = True + cert.write_text(json.dumps(data, indent=2) + "\n", encoding="utf-8") + run([py, "-I", "-B", str(pkg / "verify.py")], dest_root, False) + shutil.copy2(HERE / "CERTIFICATE.json", cert) + + # Corruption 5: on-disk certificate duplicate-key style — drop a control. + data = json.loads(cert.read_text(encoding="utf-8")) + data["controls"] = data["controls"][:-1] + cert.write_text(json.dumps(data, indent=2) + "\n", encoding="utf-8") + run([py, "-I", "-B", str(pkg / "verify.py")], dest_root, False) + + print("PASS_H2SEM_MATCHING_F_INVOICE_PACKAGE_CONTROLS relocation=1 corruptions=5") + + +if __name__ == "__main__": + main() diff --git a/research/h2sem-matching-f-invoice/verify.py b/research/h2sem-matching-f-invoice/verify.py new file mode 100644 index 0000000000..27a9ba4327 --- /dev/null +++ b/research/h2sem-matching-f-invoice/verify.py @@ -0,0 +1,520 @@ +#!/usr/bin/env python3 +"""Invoice a seed-7 ADD-greedy H2-sem matching that dominates PR1805's seed-42 invoice. + +Answers PR1805 open question 1: a different disjoint matching lowers F while +keeping (and slightly improving) the ADD saving. No new kappa. Apache-2.0. +""" +from __future__ import annotations + +import copy +import gzip +import hashlib +import importlib.util +import itertools +import json +import random +import sys +from collections import Counter +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +WORD = ROOT / "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz" +CHECKER = ROOT / "research/e8-bit-p111-tuned/code/xcheck_p.py" +SEED_BASELINE = 42 +SEED_IMPROVED = 7 +PROFILE = {1: 1323, 2: 1342, 3: 79, 4: 44, 5: 102, 6: 11, 7: 19} +BASE_BILL = { + "native_ADDs": 24305, + "D_adds": 18085, + "F": 49347, + "B": 1113070, + "local_bits": 93, + "nine_stage_bits": 177, +} +MATCH42_BILL = { + "native_ADDs": 18074, + "D_adds": 11854, + "F": 75381, + "B": 1196402, + "local_bits": 95, + "nine_stage_bits": 180, +} +MATCH7_BILL = { + "native_ADDs": 18060, + "D_adds": 11840, + "F": 73805, + "B": 1187790, + "local_bits": 95, + "nine_stage_bits": 180, +} +# First 50 pairs of the seed-7 matching. +PREFIX50_BILL = { + "native_ADDs": 21556, + "D_adds": 15336, + "F": 56603, + "B": 1113070, + "local_bits": 94, + "nine_stage_bits": 178, +} + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def load_word(): + return json.loads(gzip.decompress(WORD.read_bytes())) + + +def load_checker(): + spec = importlib.util.spec_from_file_location("r439_xcheck_matching_f", CHECKER) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def check_pins(): + pins = json.loads((HERE / "SOURCES.json").read_text(encoding="utf-8")) + need(pins["base_commit"] == "0b1cccf86e2f5132ed286a26ef0a681a495740ea", "unexpected base") + for item in pins["files"]: + digest = hashlib.sha256((ROOT / item["path"]).read_bytes()).hexdigest() + need(digest == item["sha256"], "source pin mismatch: " + item["path"]) + + +def nominate_d(word, seed): + """PR848 oriented-pair census and ADD-greedy matching with stated shuffle seed.""" + v, ret = word["v"], set(word["ret"]) + rows = [set(g[2]) for g in word["D"]] + pool = sorted(set.union(*rows) - ret - set(range(2 * v))) + need(min(pool) >= 2 * v, "D reads a non-helper") + scored = [] + for a, b in itertools.permutations(pool, 2): + saving = sum((1 if b in row else -1) for row in rows if a in row) - 2 + if saving > 0: + scored.append((saving, a, b)) + random.Random(seed).shuffle(scored) + scored.sort(key=lambda item: -item[0]) + chosen, used, total = [], set(), 0 + for saving, a, b in scored: + if a not in used and b not in used: + chosen.append([a, b]) + used.update((a, b)) + total += saving + return chosen, { + "operands": len(pool), + "oriented_pairs": len(pool) * (len(pool) - 1), + "positive_pairs": len(scored), + "best_saving": scored[0][0], + "best_pair": [scored[0][1], scored[0][2]], + "matching_pairs": len(chosen), + "matching_saving": total, + "seed": seed, + } + + +def construct_d(word, pairs): + """PR848 helper-temp wrap: prep, rewritten D body, reverse restore.""" + v, ret = word["v"], set(word["ret"]) + rows_pool = set().union(*(set(g[2]) for g in word["D"])) + flat = [r for pair in pairs for r in pair] + need(all(len(pair) == 2 for pair in pairs), "malformed pair") + need(len(flat) == len(set(flat)), "pairs must be disjoint") + need(all(r >= 2 * v and r not in ret for r in flat) and set(flat) <= rows_pool, + "temps must be non-retained D-operand helpers") + pre = [[0, a, [b]] for a, b in pairs] + body = [] + for frame, dst, srcs in word["D"]: + need(frame == 0 and v <= dst < 2 * v, "D gate not frame-zero target write") + row = set(srcs) + for a, b in pairs: + if a in row: + row.symmetric_difference_update({b}) + body.append([frame, dst, sorted(row)]) + result = copy.deepcopy(word) + result["D"] = pre + body + list(reversed(pre)) + return result + + +def stream(w): + out = [("add", d, s) for sec in ("D", "A") for _, d, ss in w[sec] for s in ss] + tmp = 2 * w["v"] + w["R"] + for j, centre in enumerate(w["ret"]): + out.append(("copy", tmp, centre)) + out += [("add", w["v"] + i, tmp) for i, ss in enumerate(w["scatter"]) if j in ss] + out.append(("erase", tmp, centre)) + out += [("add", d, s) for sec in ("B", "C") for _, d, ss in w[sec] for s in ss] + return out + + +def flip(kind): + return {"copy": "erase", "erase": "copy"}.get(kind, kind) + + +def literal_rows(w, reverse=False): + n = 2 * w["v"] + w["R"] + rows = [{i} for i in range(n)] + [set()] + ins = stream(w) + for kind, d, s in (reversed(ins) if reverse else ins): + kind = flip(kind) if reverse else kind + if kind == "add": + rows[d] ^= rows[s] + elif kind == "copy": + need(not rows[d], "copy into a live temporary") + rows[d] = set(rows[s]) + else: + need(rows[d] == rows[s], "erase of a changed copy") + rows[d] = set() + need(not rows[-1], "temporary not erased") + return rows[:-1] + + +def literal_bounds(w): + peaks = [] + for reverse in (False, True): + val = [1] * (2 * w["v"] + w["R"] + 1) + peak = 1 + ins = stream(w) + for kind, d, s in (reversed(ins) if reverse else ins): + kind = flip(kind) if reverse else kind + val[d] = val[d] + val[s] if kind == "add" else (val[s] if kind == "copy" else 0) + peak = max(peak, val[d]) + peaks.append(peak) + F, B = peaks + return { + "native_ADDs": sum(k == "add" for k, _, _ in stream(w)), + "D_adds": sum(len(g[2]) for g in w["D"]), + "F": F, + "B": B, + "local_bits": (64 * F**3 * B**2).bit_length(), + "nine_stage_bits": ((1 << 18) * F**5 * B**4).bit_length(), + } + + +def frame_paths(w): + fs = [frozenset(f) for f in w["frames"]] + ps = [[f] for f in w["start"]] + for sec in "DABC": + for f, d, ss in w[sec]: + for r in (d, *ss): + if ps[r][-1] != f: + need(fs[ps[r][-1]] < fs[f], "illegal frame move") + ps[r].append(f) + for r, f in enumerate(w["final"]): + if ps[r][-1] != f: + need(fs[ps[r][-1]] < fs[f], "illegal final move") + ps[r].append(f) + return ps + + +def semantic_n(gates, v, R): + """Independent bit-column oracle for D; no row-engine import.""" + n = 2 * v + R + flat = [(d, s) for _, d, ss in gates for s in ss] + mask = (1 << v) - 1 + N = [0] * v + for j in range(n): + state = 1 << j + for d, s in flat: + if (state >> s) & 1: + state ^= 1 << d + delta = state ^ (1 << j) + if j < 2 * v: + need(delta == 0, "source/target column changed in D") + else: + need(delta & ~(mask << v) == 0, "helper restoration failed") + for t in range(v): + if (delta >> (v + t)) & 1: + N[t] |= 1 << (j - 2 * v) + return N + + +def h2sem_shape(w): + """H2-sem conditions 1-2: zero-frame, source-free, no target->helper.""" + v = w["v"] + for frame, dst, srcs in w["D"]: + need(frame == 0, "nonzero D frame") + need(dst >= v, "D writes a source") + for s in srcs: + need(s >= v, "D reads a source") + need(not (v <= s < 2 * v and dst >= 2 * v), "target feeds helper") + need(dst != s, "self XOR") + return True + + +def paid_profile(mod, w): + dim, _labels, flow, hyp, con, _parts = mod.check(w) + prof = Counter(dim.fdim[b] - dim.fdim[a] for p in frame_paths(w) for a, b in itertools.pairwise(p)) + prof.update(t["rank"] for t in flow["totals"]) + return { + "profile": {k: prof[k] for k in sorted(prof)}, + "copy_ranks": [t["rank"] for t in flow["totals"]], + "hypotheses": hyp, + "conclusions": con, + } + + +def invoice_word(name, w, expected): + bill = literal_bounds(w) + need(bill == expected, name + " bill mismatch: " + json.dumps(bill)) + need(bill["local_bits"] <= 104 and bill["nine_stage_bits"] <= 192, + name + " precision guard failed") + return bill + + +def check_profile(mod, name, w, expect_h2, expect_k): + own = paid_profile(mod, w) + need(own["profile"] == PROFILE, name + " paid profile changed") + need(sum(r * c for r, c in own["profile"].items()) == 5129, name + " rank mass") + need(own["copy_ranks"] == [7] * 9, name + " COPY ranks") + need(own["hypotheses"]["H2_D_frame0_targets_from_helpers"] is expect_h2, name + " H2") + need(own["conclusions"]["K_equals_D"] is expect_k, name + " K") + for key in ("H1_no_target_feeds_z", "H3_A_z_only_scatter_targets_B_split", + "H4_C_literal_reverse_at_full", "H5_V_identity"): + need(own["hypotheses"][key] is True, name + " " + key) + for key in ("U_block_form", "J_identity", "C_is_U_inverse"): + need(own["conclusions"][key] is True, name + " " + key) + return own["profile"] + + +def main(): + write = "--write" in sys.argv + check_pins() + word = load_word() + mod = load_checker() + + _w, _g, _f, hyp0, con0, _p = mod.check(word) + need(all(hyp0.values()) and all(con0.values()), "baseline H1-H5 / U-J-K-C failed") + + pairs42, census42 = nominate_d(word, SEED_BASELINE) + pairs7, census7 = nominate_d(word, SEED_IMPROVED) + + need(census42["operands"] == 430, "operand census drift") + need(census42["oriented_pairs"] == 184470, "oriented-pair census drift") + need(census42["positive_pairs"] == 41404, "positive-pair census drift") + need(census42["best_pair"] == [277, 434] and census42["best_saving"] == 65, "best pair drift") + need(census42["matching_pairs"] == 205 and census42["matching_saving"] == 6231, + "seed-42 matching drift") + need(census7["matching_pairs"] == 208 and census7["matching_saving"] == 6245, + "seed-7 matching drift") + need(census7["best_saving"] == 65, "seed-7 best saving drift") + # Tie-break among saving=65 pairs is seed-dependent; require the PR848 + # champion pair is present in the seed-7 matching. + need([277, 434] in pairs7, "seed-7 matching omits champion pair 277->434") + + set42 = {tuple(p) for p in pairs42} + set7 = {tuple(p) for p in pairs7} + need(set42 != set7, "seed-7 matching equals seed-42 pair set") + need(len(set42 & set7) == 150, "unexpected pair-set overlap") + + wrap42 = construct_d(word, pairs42) + wrap7 = construct_d(word, pairs7) + prefix50 = construct_d(word, pairs7[:50]) + + base_n = semantic_n(word["D"], word["v"], word["R"]) + need(semantic_n(wrap42["D"], word["v"], word["R"]) == base_n, "seed-42 semantic N changed") + need(semantic_n(wrap7["D"], word["v"], word["R"]) == base_n, "seed-7 semantic N changed") + need(sum(bin(x).count("1") for x in base_n) == 18085, "baseline N weight drift") + + h2sem_shape(word) + h2sem_shape(wrap42) + h2sem_shape(wrap7) + + base_paths = frame_paths(word) + need(frame_paths(wrap42) == base_paths and frame_paths(wrap7) == base_paths, + "frame paths changed") + + want = [{i, i - word["v"]} if word["v"] <= i < 2 * word["v"] else {i} + for i in range(2 * word["v"] + word["R"])] + for name, w in (("base", word), ("match42", wrap42), ("match7", wrap7)): + for reverse in (False, True): + need(literal_rows(w, reverse) == want, + "%s complete boundary (%s)" % (name, "reverse" if reverse else "forward")) + + prefix_bill = literal_bounds(prefix50) + if write: + print("PREFIX50_BILL =", json.dumps(prefix_bill)) + else: + need(prefix_bill == PREFIX50_BILL, "prefix50 bill mismatch: " + json.dumps(prefix_bill)) + + bills = { + "base": invoice_word("base", word, BASE_BILL), + "match42": invoice_word("match42", wrap42, MATCH42_BILL), + "match7": invoice_word("match7", wrap7, MATCH7_BILL), + "prefix50_seed7": prefix_bill, + } + need(prefix_bill["local_bits"] <= 104 and prefix_bill["nine_stage_bits"] <= 192, + "prefix50 precision guard failed") + + need(bills["match42"]["native_ADDs"] - bills["base"]["native_ADDs"] == -6231, + "seed-42 ADD delta") + need(bills["match7"]["native_ADDs"] - bills["base"]["native_ADDs"] == -6245, + "seed-7 ADD delta") + need(bills["match7"]["native_ADDs"] < bills["match42"]["native_ADDs"], + "seed-7 must strictly improve ADD count") + need(bills["match7"]["F"] < bills["match42"]["F"], + "seed-7 must strictly lower F") + need(bills["match7"]["B"] < bills["match42"]["B"], + "seed-7 must strictly lower B") + need(bills["prefix50_seed7"]["native_ADDs"] > bills["match7"]["native_ADDs"], + "prefix50 ADD not worse than full") + need(bills["prefix50_seed7"]["F"] < bills["match7"]["F"], + "prefix50 F not below full") + + for name, w, expect_h2, expect_k in ( + ("base", word, True, True), + ("match42", wrap42, False, False), + ("match7", wrap7, False, False), + ): + check_profile(mod, name, w, expect_h2, expect_k) + + for w in (wrap42, wrap7): + for key in word: + if key != "D": + need(w[key] == word[key], "non-D field changed: " + key) + + rejected = [] + + unrestored = copy.deepcopy(wrap7) + del unrestored["D"][-1] + try: + semantic_n(unrestored["D"], word["v"], word["R"]) + raise ValueError("unrestored helper temp accepted") + except ValueError as exc: + need("helper restoration" in str(exc), "unexpected unrestored failure") + rejected.append("unrestored_helper_temp") + + a = wrap7["D"][0][1] + b = wrap7["D"][0][2][0] + other = next(h for h in range(2 * word["v"], 2 * word["v"] + word["R"]) if h not in (a, b)) + wrong_restore = copy.deepcopy(wrap7) + wrong_restore["D"][-1] = [0, a, [other]] + failed = False + try: + semantic_n(wrong_restore["D"], word["v"], word["R"]) + except ValueError as exc: + need("helper restoration" in str(exc), "unexpected wrong-restore failure") + failed = True + need(failed, "wrong restore operand accepted") + rejected.append("wrong_restore_operand") + + target = word["D"][0][1] + helper = wrap7["D"][0][2][0] + feedback = copy.deepcopy(word) + feedback["D"] = [[0, helper, [target]]] + [list(g) for g in word["D"]] + [[0, helper, [target]]] + try: + h2sem_shape(feedback) + raise ValueError("target-feedback wrap accepted") + except ValueError as exc: + need("target feeds helper" in str(exc), "unexpected feedback failure") + rejected.append("target_feeds_helper") + + source_read = copy.deepcopy(word) + source_read["D"] = [[0, a, [0]]] + [list(g) for g in word["D"]] + [[0, a, [0]]] + try: + h2sem_shape(source_read) + raise ValueError("source-read wrap accepted") + except ValueError as exc: + need("D reads a source" in str(exc), "unexpected source-read failure") + rejected.append("source_reads_in_D") + + rejected.append("prefix50_not_dominating_full") + rejected.append("seed42_ne_seed7_pairset") + + mutated = copy.deepcopy(wrap7) + body_idx = 208 + dst, srcs = mutated["D"][body_idx][1], list(mutated["D"][body_idx][2]) + need(srcs, "empty body gate") + if len(srcs) > 1: + srcs = srcs[1:] + else: + srcs = srcs + [helper] + mutated["D"][body_idx] = [0, dst, sorted(set(srcs))] + need(semantic_n(mutated["D"], word["v"], word["R"]) != base_n, "body mutation did not change N") + rejected.append("mutated_body_changes_N") + need(len(rejected) == 7, "expected seven controls") + + deltas = { + "add_saving_lift": MATCH7_BILL["native_ADDs"] - MATCH42_BILL["native_ADDs"], + "F_lift": MATCH7_BILL["F"] - MATCH42_BILL["F"], + "B_lift": MATCH7_BILL["B"] - MATCH42_BILL["B"], + "pairs_lift": census7["matching_pairs"] - census42["matching_pairs"], + "pair_overlap": len(set42 & set7), + } + need(deltas["add_saving_lift"] == -14, "ADD lift drift") + need(deltas["F_lift"] == -1576, "F lift drift") + need(deltas["B_lift"] == -8612, "B lift drift") + need(deltas["pairs_lift"] == 3, "pair-count lift drift") + + matching_path = HERE / "MATCHING7.json" + matching_blob = { + "seed": SEED_IMPROVED, + "pairs": pairs7, + "saving": 6245, + "pair_count": 208, + } + if write or not matching_path.exists(): + matching_path.write_text(json.dumps(matching_blob, indent=2) + "\n", encoding="utf-8") + else: + frozen_m = json.loads(matching_path.read_text(encoding="utf-8")) + need(frozen_m == matching_blob, "MATCHING7.json mismatch") + matching_sha = hashlib.sha256(matching_path.read_bytes()).hexdigest() + + report = { + "status": "PASS_H2SEM_MATCHING_F_INVOICE", + "task_id": "bit-helper-contract", + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "columns": 2 * word["v"] + word["R"], + "census42": census42, + "census7": census7, + "bills": bills, + "deltas_7_minus_42": deltas, + "paid_profile": {str(k): PROFILE[k] for k in sorted(PROFILE)}, + "rank_mass": 5129, + "h2sem": { + "shape": True, + "semantic_N_equals_baseline": True, + "syntactic_H2_K": { + "base": {"H2": True, "K_equals_D": True}, + "match42": {"H2": False, "K_equals_D": False}, + "match7": {"H2": False, "K_equals_D": False}, + }, + }, + "controls": rejected, + "kappa_claim": "none", + "new_kappa": False, + "matching7": { + "path": "MATCHING7.json", + "sha256": matching_sha, + "pair_count": 208, + "saving": 6245, + }, + } + + certificate = HERE / "CERTIFICATE.json" + if write or not certificate.exists(): + certificate.write_text(json.dumps(report, indent=2) + "\n", encoding="utf-8") + if write: + print("WROTE_CERTIFICATE", certificate) + else: + frozen = json.loads(certificate.read_text(encoding="utf-8")) + need(report == frozen, "certificate mismatch") + + print( + "PASS_H2SEM_MATCHING_F_INVOICE " + "seed42_pairs=205 adds=24305->18074 F=75381 " + "seed7_pairs=208 adds=24305->18060 F=73805 " + "delta_adds=-14 delta_F=-1576 " + "profile_mass=5129 columns=%d controls=%d no_new_kappa" + % (report["columns"], len(rejected)) + ) + return report + + +if __name__ == "__main__": + try: + main() + except Exception as exc: # noqa: BLE001 - surface exact verifier failure + print("FAIL_H2SEM_MATCHING_F_INVOICE:", exc, file=sys.stderr) + raise