From 86e21f34510313508e15363d060609c3f24ef4b7 Mon Sep 17 00:00:00 2001 From: columbia-git <264036636+columbia-git@users.noreply.github.com> Date: Wed, 14 Oct 2026 02:52:54 +0000 Subject: [PATCH] Audit selected PR1094 call-entry norms and conditional 112-bit prefix bound --- .../EXPECTED.json | 1779 +++++++++++++++++ .../selected1094-wire-prefix-audit/README.md | 231 +++ .../SOURCES.json | 96 + .../selected1094-wire-prefix-audit/TASK.json | 105 + .../VERIFY.json | 38 + .../test_verify.py | 182 ++ .../selected1094-wire-prefix-audit/verify.py | 468 +++++ 7 files changed, 2899 insertions(+) create mode 100644 research/selected1094-wire-prefix-audit/EXPECTED.json create mode 100644 research/selected1094-wire-prefix-audit/README.md create mode 100644 research/selected1094-wire-prefix-audit/SOURCES.json create mode 100644 research/selected1094-wire-prefix-audit/TASK.json create mode 100644 research/selected1094-wire-prefix-audit/VERIFY.json create mode 100644 research/selected1094-wire-prefix-audit/test_verify.py create mode 100644 research/selected1094-wire-prefix-audit/verify.py diff --git a/research/selected1094-wire-prefix-audit/EXPECTED.json b/research/selected1094-wire-prefix-audit/EXPECTED.json new file mode 100644 index 0000000000..ed09be2767 --- /dev/null +++ b/research/selected1094-wire-prefix-audit/EXPECTED.json @@ -0,0 +1,1779 @@ +{ + "status": "PASS_SELECTED1094_WIRE_PREFIX_AUDIT", + "source_sha256": { + "research/community-frontier1094-audit/REPLAY.json": "ce0678fa7abaab221de74baeace0c6696d5ea23a36719a58cff230215a06aae7", + "research/community-frontier1094-audit/SELECTED-SOURCE.json": "79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b", + "research/community-frontier1094-audit/selected-replay.tar.gz": "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6", + "research/complex-k492-owner-repair/code/hpe_audit_local.py": "6bd9a1e279c9c9e4f3767d9f82e537b559292906feb2ddab02f380fb6523a810", + "research/gauge44-slots-t16/code/invoice_allcold.py": "71eb57514e28ced97251e0507105f654f59885ec4d40486a780bf166098858a8", + "research/complex-double-replica-owners/PROOF.md": "db99599e3966bec253c577c23915e2a2899c4c4e8568044efc11c7918b137bbc" + }, + "local_replay": { + "status": "PASS_INDEPENDENT_LOCAL_SCALAR_FRAME_AND_WRAPPER_REPLAY", + "exact_columns_per_orientation": 704, + "orientations": [ + "forward", + "backward" + ], + "original_controls_rejected": [ + "wrong_scale", + "missing_center", + "wrong_common_frame", + "wrong_child_rank", + "missing_pre_wrapper", + "missing_post_wrapper", + "wrapper_with_wrong_frame", + "wrapper_in_wrong_phase", + "wrapper_on_a_data_register", + "wrapper_on_a_target_register", + "wrapper_on_a_centre_register", + "hpe_pre_wrapper_resolved_to_full_recipe", + "hpe_post_wrapper_without_terminal_frame", + "hpe_post_wrapper_wrong_terminal_frame", + "hpe_tail_gate_at_full_frame", + "hpe_tail_climb_dropped", + "hpe_helper_exit_adapter_to_full", + "hpe_tail_gate_moved_into_full_cleanup", + "cold_hpe_pre_wrapper_replaced_by_identity_entry_adapter", + "cold_hpe_pre_wrapper_dropped", + "cold_hpe_post_wrapper_replaced_by_exit_adapter", + "cold_hpe_pre_wrapper_resolved_to_cold_full_convention", + "cold_hpe_wrapper_with_nonzero_entrance", + "cold_hpe_post_wrapper_wrong_terminal_frame", + "cold_hpe_premix_gate_before_pre_wrapper" + ], + "receipt_identical": true + }, + "controller": { + "events": 482, + "event_counts": { + "local_cover_sweep": 144, + "idle_cover_sweep": 160, + "bridge": 144, + "terminal_Y_translations": 16, + "terminal": 16, + "bank_padding_cover_sweep": 1, + "translate_every_live_family": 1 + }, + "calls": 144, + "helper_roles": 69120, + "cross_replica_roles": 57480, + "boundary_peak": 14, + "final_replica_bound": [ + 8, + 8, + 14, + 14, + 12, + 12, + 9, + 9 + ], + "all_replica_final_bounds_equal": true, + "local_input_maxima": { + "forward": 8, + "backward": 8 + }, + "borrowed_exceeds_active_calls": 126, + "source_boundary_table": [ + [ + 1, + 2, + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 3, + 2, + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 3, + 2, + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 4, + 3, + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 4, + 7, + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 4, + 7, + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 5, + 8, + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 5, + 8, + 2, + 1, + 1, + 1, + 1, + 1 + ], + [ + 5, + 8, + 2, + 1, + 1, + 1, + 1, + 1 + ], + [ + 5, + 8, + 3, + 2, + 1, + 1, + 1, + 1 + ], + [ + 5, + 8, + 3, + 5, + 1, + 1, + 1, + 1 + ], + [ + 5, + 8, + 3, + 5, + 1, + 1, + 1, + 1 + ], + [ + 5, + 8, + 4, + 6, + 1, + 1, + 1, + 1 + ], + [ + 5, + 8, + 4, + 6, + 2, + 1, + 1, + 1 + ], + [ + 5, + 8, + 4, + 6, + 2, + 1, + 1, + 1 + ], + [ + 5, + 8, + 4, + 6, + 3, + 2, + 1, + 1 + ], + [ + 5, + 8, + 4, + 6, + 3, + 5, + 1, + 1 + ], + [ + 5, + 8, + 4, + 6, + 3, + 5, + 1, + 1 + ], + [ + 5, + 8, + 4, + 6, + 4, + 6, + 1, + 1 + ], + [ + 5, + 8, + 4, + 6, + 4, + 6, + 2, + 1 + ], + [ + 5, + 8, + 4, + 6, + 4, + 6, + 2, + 3 + ], + [ + 5, + 8, + 4, + 6, + 4, + 6, + 2, + 3 + ], + [ + 5, + 8, + 4, + 6, + 4, + 6, + 2, + 3 + ], + [ + 5, + 8, + 4, + 6, + 4, + 6, + 2, + 3 + ], + [ + 5, + 8, + 4, + 6, + 4, + 6, + 2, + 3 + ], + [ + 5, + 8, + 4, + 6, + 4, + 6, + 6, + 9 + ], + [ + 5, + 8, + 4, + 6, + 8, + 12, + 6, + 9 + ], + [ + 5, + 8, + 9, + 14, + 8, + 12, + 6, + 9 + ], + [ + 5, + 8, + 9, + 14, + 8, + 12, + 6, + 9 + ], + [ + 8, + 8, + 14, + 14, + 12, + 12, + 9, + 9 + ] + ], + "call_inputs": [ + { + "event": 0, + "stage": 0, + "replica": 0, + "orientation": "forward", + "active": 1, + "helper": 1, + "input": 1 + }, + { + "event": 1, + "stage": 0, + "replica": 8, + "orientation": "forward", + "active": 1, + "helper": 1, + "input": 1 + }, + { + "event": 2, + "stage": 0, + "replica": 1, + "orientation": "forward", + "active": 1, + "helper": 1, + "input": 1 + }, + { + "event": 3, + "stage": 0, + "replica": 9, + "orientation": "forward", + "active": 1, + "helper": 1, + "input": 1 + }, + { + "event": 4, + "stage": 1, + "replica": 0, + "orientation": "backward", + "active": 2, + "helper": 1, + "input": 2 + }, + { + "event": 7, + "stage": 1, + "replica": 8, + "orientation": "backward", + "active": 2, + "helper": 1, + "input": 2 + }, + { + "event": 10, + "stage": 0, + "replica": 2, + "orientation": "forward", + "active": 1, + "helper": 1, + "input": 1 + }, + { + "event": 11, + "stage": 0, + "replica": 10, + "orientation": "forward", + "active": 1, + "helper": 1, + "input": 1 + }, + { + "event": 12, + "stage": 1, + "replica": 1, + "orientation": "backward", + "active": 2, + "helper": 1, + "input": 2 + }, + { + "event": 15, + "stage": 1, + "replica": 9, + "orientation": "backward", + "active": 2, + "helper": 1, + "input": 2 + }, + { + "event": 18, + "stage": 2, + "replica": 0, + "orientation": "forward", + "active": 4, + "helper": 1, + "input": 4 + }, + { + "event": 21, + "stage": 2, + "replica": 8, + "orientation": "forward", + "active": 4, + "helper": 1, + "input": 4 + }, + { + "event": 24, + "stage": 0, + "replica": 3, + "orientation": "forward", + "active": 1, + "helper": 1, + "input": 1 + }, + { + "event": 25, + "stage": 0, + "replica": 11, + "orientation": "forward", + "active": 1, + "helper": 8, + "input": 8 + }, + { + "event": 26, + "stage": 1, + "replica": 2, + "orientation": "backward", + "active": 2, + "helper": 1, + "input": 2 + }, + { + "event": 29, + "stage": 1, + "replica": 10, + "orientation": "backward", + "active": 2, + "helper": 1, + "input": 2 + }, + { + "event": 32, + "stage": 2, + "replica": 1, + "orientation": "forward", + "active": 4, + "helper": 8, + "input": 8 + }, + { + "event": 35, + "stage": 2, + "replica": 9, + "orientation": "forward", + "active": 4, + "helper": 1, + "input": 4 + }, + { + "event": 38, + "stage": 3, + "replica": 0, + "orientation": "backward", + "active": 1, + "helper": 8, + "input": 8 + }, + { + "event": 41, + "stage": 3, + "replica": 8, + "orientation": "backward", + "active": 1, + "helper": 5, + "input": 5 + }, + { + "event": 44, + "stage": 0, + "replica": 4, + "orientation": "forward", + "active": 1, + "helper": 8, + "input": 8 + }, + { + "event": 45, + "stage": 0, + "replica": 12, + "orientation": "forward", + "active": 1, + "helper": 8, + "input": 8 + }, + { + "event": 46, + "stage": 1, + "replica": 3, + "orientation": "backward", + "active": 2, + "helper": 8, + "input": 8 + }, + { + "event": 49, + "stage": 1, + "replica": 11, + "orientation": "backward", + "active": 2, + "helper": 1, + "input": 2 + }, + { + "event": 52, + "stage": 2, + "replica": 2, + "orientation": "forward", + "active": 4, + "helper": 8, + "input": 8 + }, + { + "event": 55, + "stage": 2, + "replica": 10, + "orientation": "forward", + "active": 4, + "helper": 8, + "input": 8 + }, + { + "event": 58, + "stage": 3, + "replica": 1, + "orientation": "backward", + "active": 1, + "helper": 8, + "input": 8 + }, + { + "event": 61, + "stage": 3, + "replica": 9, + "orientation": "backward", + "active": 1, + "helper": 1, + "input": 1 + }, + { + "event": 64, + "stage": 4, + "replica": 0, + "orientation": "forward", + "active": 3, + "helper": 8, + "input": 8 + }, + { + "event": 67, + "stage": 4, + "replica": 8, + "orientation": "forward", + "active": 3, + "helper": 8, + "input": 8 + }, + { + "event": 70, + "stage": 0, + "replica": 5, + "orientation": "forward", + "active": 1, + "helper": 8, + "input": 8 + }, + { + "event": 71, + "stage": 0, + "replica": 13, + "orientation": "forward", + "active": 1, + "helper": 8, + "input": 8 + }, + { + "event": 72, + "stage": 1, + "replica": 4, + "orientation": "backward", + "active": 2, + "helper": 8, + "input": 8 + }, + { + "event": 75, + "stage": 1, + "replica": 12, + "orientation": "backward", + "active": 2, + "helper": 8, + "input": 8 + }, + { + "event": 78, + "stage": 2, + "replica": 3, + "orientation": "forward", + "active": 4, + "helper": 8, + "input": 8 + }, + { + "event": 81, + "stage": 2, + "replica": 11, + "orientation": "forward", + "active": 4, + "helper": 8, + "input": 8 + }, + { + "event": 84, + "stage": 3, + "replica": 2, + "orientation": "backward", + "active": 1, + "helper": 5, + "input": 5 + }, + { + "event": 87, + "stage": 3, + "replica": 10, + "orientation": "backward", + "active": 1, + "helper": 5, + "input": 5 + }, + { + "event": 90, + "stage": 4, + "replica": 1, + "orientation": "forward", + "active": 3, + "helper": 8, + "input": 8 + }, + { + "event": 93, + "stage": 4, + "replica": 9, + "orientation": "forward", + "active": 3, + "helper": 8, + "input": 8 + }, + { + "event": 96, + "stage": 5, + "replica": 0, + "orientation": "backward", + "active": 1, + "helper": 8, + "input": 8 + }, + { + "event": 99, + "stage": 5, + "replica": 8, + "orientation": "backward", + "active": 1, + "helper": 8, + "input": 8 + }, + { + "event": 102, + "stage": 0, + "replica": 6, + "orientation": "forward", + "active": 1, + "helper": 8, + "input": 8 + }, + { + "event": 103, + "stage": 0, + "replica": 14, + "orientation": "forward", + "active": 1, + "helper": 8, + "input": 8 + }, + { + "event": 104, + "stage": 1, + "replica": 5, + "orientation": "backward", + "active": 2, + "helper": 8, + "input": 8 + }, + { + "event": 107, + "stage": 1, + "replica": 13, + "orientation": "backward", + "active": 2, + "helper": 8, + "input": 8 + }, + { + "event": 110, + "stage": 2, + "replica": 4, + "orientation": "forward", + "active": 4, + "helper": 8, + "input": 8 + }, + { + "event": 113, + "stage": 2, + "replica": 12, + "orientation": "forward", + "active": 4, + "helper": 8, + "input": 8 + }, + { + "event": 116, + "stage": 3, + "replica": 3, + "orientation": "backward", + "active": 1, + "helper": 5, + "input": 5 + }, + { + "event": 119, + "stage": 3, + "replica": 11, + "orientation": "backward", + "active": 1, + "helper": 8, + "input": 8 + }, + { + "event": 122, + "stage": 4, + "replica": 2, + "orientation": "forward", + "active": 3, + "helper": 8, + "input": 8 + }, + { + "event": 125, + "stage": 4, + "replica": 10, + "orientation": "forward", + "active": 3, + "helper": 8, + "input": 8 + }, + { + "event": 128, + "stage": 5, + "replica": 1, + "orientation": "backward", + "active": 1, + "helper": 6, + "input": 6 + }, + { + "event": 131, + "stage": 5, + "replica": 9, + "orientation": "backward", + "active": 1, + "helper": 8, + "input": 8 + }, + { + "event": 134, + "stage": 0, + "replica": 7, + "orientation": "forward", + "active": 1, + "helper": 8, + "input": 8 + }, + { + "event": 135, + "stage": 0, + "replica": 15, + "orientation": "forward", + "active": 1, + "helper": 8, + "input": 8 + }, + { + "event": 136, + "stage": 6, + "replica": 0, + "orientation": "forward", + "active": 3, + "helper": 8, + "input": 8 + }, + { + "event": 139, + "stage": 6, + "replica": 8, + "orientation": "forward", + "active": 3, + "helper": 8, + "input": 8 + }, + { + "event": 142, + "stage": 1, + "replica": 6, + "orientation": "backward", + "active": 2, + "helper": 8, + "input": 8 + }, + { + "event": 145, + "stage": 1, + "replica": 14, + "orientation": "backward", + "active": 2, + "helper": 8, + "input": 8 + }, + { + "event": 148, + "stage": 2, + "replica": 5, + "orientation": "forward", + "active": 4, + "helper": 8, + "input": 8 + }, + { + "event": 151, + "stage": 2, + "replica": 13, + "orientation": "forward", + "active": 4, + "helper": 8, + "input": 8 + }, + { + "event": 154, + "stage": 3, + "replica": 4, + "orientation": "backward", + "active": 1, + "helper": 8, + "input": 8 + }, + { + "event": 157, + "stage": 3, + "replica": 12, + "orientation": "backward", + "active": 1, + "helper": 8, + "input": 8 + }, + { + "event": 160, + "stage": 4, + "replica": 3, + "orientation": "forward", + "active": 3, + "helper": 8, + "input": 8 + }, + { + "event": 163, + "stage": 4, + "replica": 11, + "orientation": "forward", + "active": 3, + "helper": 8, + "input": 8 + }, + { + "event": 166, + "stage": 5, + "replica": 2, + "orientation": "backward", + "active": 1, + "helper": 8, + "input": 8 + }, + { + "event": 169, + "stage": 5, + "replica": 10, + "orientation": "backward", + "active": 1, + "helper": 8, + "input": 8 + }, + { + "event": 172, + "stage": 6, + "replica": 1, + "orientation": "forward", + "active": 3, + "helper": 8, + "input": 8 + }, + { + "event": 175, + "stage": 6, + "replica": 9, + "orientation": "forward", + "active": 3, + "helper": 8, + "input": 8 + }, + { + "event": 178, + "stage": 1, + "replica": 7, + "orientation": "backward", + "active": 2, + "helper": 8, + "input": 8 + }, + { + "event": 181, + "stage": 1, + "replica": 15, + "orientation": "backward", + "active": 2, + "helper": 8, + "input": 8 + }, + { + "event": 184, + "stage": 7, + "replica": 0, + "orientation": "backward", + "active": 1, + "helper": 8, + "input": 8 + }, + { + "event": 185, + "stage": 7, + "replica": 8, + "orientation": "backward", + "active": 1, + "helper": 8, + "input": 8 + }, + { + "event": 186, + "stage": 2, + "replica": 6, + "orientation": "forward", + "active": 4, + "helper": 8, + "input": 8 + }, + { + "event": 189, + "stage": 2, + "replica": 14, + "orientation": "forward", + "active": 4, + "helper": 8, + "input": 8 + }, + { + "event": 192, + "stage": 3, + "replica": 5, + "orientation": "backward", + "active": 1, + "helper": 8, + "input": 8 + }, + { + "event": 195, + "stage": 3, + "replica": 13, + "orientation": "backward", + "active": 1, + "helper": 8, + "input": 8 + }, + { + "event": 198, + "stage": 4, + "replica": 4, + "orientation": "forward", + "active": 3, + "helper": 8, + "input": 8 + }, + { + "event": 201, + "stage": 4, + "replica": 12, + "orientation": "forward", + "active": 3, + "helper": 8, + "input": 8 + }, + { + "event": 204, + "stage": 5, + "replica": 3, + "orientation": "backward", + "active": 1, + "helper": 8, + "input": 8 + }, + { + "event": 207, + "stage": 5, + "replica": 11, + "orientation": "backward", + "active": 1, + "helper": 8, + "input": 8 + }, + { + "event": 210, + "stage": 6, + "replica": 2, + "orientation": "forward", + "active": 3, + "helper": 8, + "input": 8 + }, + { + "event": 213, + "stage": 6, + "replica": 10, + "orientation": "forward", + "active": 3, + "helper": 8, + "input": 8 + }, + { + "event": 216, + "stage": 7, + "replica": 1, + "orientation": "backward", + "active": 1, + "helper": 8, + "input": 8 + }, + { + "event": 217, + "stage": 7, + "replica": 9, + "orientation": "backward", + "active": 1, + "helper": 8, + "input": 8 + }, + { + "event": 218, + "stage": 2, + "replica": 7, + "orientation": "forward", + "active": 4, + "helper": 8, + "input": 8 + }, + { + "event": 221, + "stage": 2, + "replica": 15, + "orientation": "forward", + "active": 4, + "helper": 8, + "input": 8 + }, + { + "event": 224, + "stage": 8, + "replica": 0, + "orientation": "forward", + "active": 2, + "helper": 8, + "input": 8 + }, + { + "event": 234, + "stage": 8, + "replica": 8, + "orientation": "forward", + "active": 2, + "helper": 8, + "input": 8 + }, + { + "event": 244, + "stage": 3, + "replica": 6, + "orientation": "backward", + "active": 1, + "helper": 8, + "input": 8 + }, + { + "event": 247, + "stage": 3, + "replica": 14, + "orientation": "backward", + "active": 1, + "helper": 8, + "input": 8 + }, + { + "event": 250, + "stage": 4, + "replica": 5, + "orientation": "forward", + "active": 3, + "helper": 8, + "input": 8 + }, + { + "event": 253, + "stage": 4, + "replica": 13, + "orientation": "forward", + "active": 3, + "helper": 8, + "input": 8 + }, + { + "event": 256, + "stage": 5, + "replica": 4, + "orientation": "backward", + "active": 1, + "helper": 8, + "input": 8 + }, + { + "event": 259, + "stage": 5, + "replica": 12, + "orientation": "backward", + "active": 1, + "helper": 8, + "input": 8 + }, + { + "event": 262, + "stage": 6, + "replica": 3, + "orientation": "forward", + "active": 3, + "helper": 8, + "input": 8 + }, + { + "event": 265, + "stage": 6, + "replica": 11, + "orientation": "forward", + "active": 3, + "helper": 8, + "input": 8 + }, + { + "event": 268, + "stage": 7, + "replica": 2, + "orientation": "backward", + "active": 1, + "helper": 8, + "input": 8 + }, + { + "event": 269, + "stage": 7, + "replica": 10, + "orientation": "backward", + "active": 1, + "helper": 8, + "input": 8 + }, + { + "event": 270, + "stage": 8, + "replica": 1, + "orientation": "forward", + "active": 2, + "helper": 8, + "input": 8 + }, + { + "event": 280, + "stage": 8, + "replica": 9, + "orientation": "forward", + "active": 2, + "helper": 8, + "input": 8 + }, + { + "event": 290, + "stage": 3, + "replica": 7, + "orientation": "backward", + "active": 1, + "helper": 8, + "input": 8 + }, + { + "event": 293, + "stage": 3, + "replica": 15, + "orientation": "backward", + "active": 1, + "helper": 8, + "input": 8 + }, + { + "event": 296, + "stage": 4, + "replica": 6, + "orientation": "forward", + "active": 3, + "helper": 8, + "input": 8 + }, + { + "event": 299, + "stage": 4, + "replica": 14, + "orientation": "forward", + "active": 3, + "helper": 8, + "input": 8 + }, + { + "event": 302, + "stage": 5, + "replica": 5, + "orientation": "backward", + "active": 1, + "helper": 8, + "input": 8 + }, + { + "event": 305, + "stage": 5, + "replica": 13, + "orientation": "backward", + "active": 1, + "helper": 8, + "input": 8 + }, + { + "event": 308, + "stage": 6, + "replica": 4, + "orientation": "forward", + "active": 3, + "helper": 8, + "input": 8 + }, + { + "event": 311, + "stage": 6, + "replica": 12, + "orientation": "forward", + "active": 3, + "helper": 8, + "input": 8 + }, + { + "event": 314, + "stage": 7, + "replica": 3, + "orientation": "backward", + "active": 1, + "helper": 8, + "input": 8 + }, + { + "event": 315, + "stage": 7, + "replica": 11, + "orientation": "backward", + "active": 1, + "helper": 8, + "input": 8 + }, + { + "event": 316, + "stage": 8, + "replica": 2, + "orientation": "forward", + "active": 2, + "helper": 8, + "input": 8 + }, + { + "event": 326, + "stage": 8, + "replica": 10, + "orientation": "forward", + "active": 2, + "helper": 8, + "input": 8 + }, + { + "event": 336, + "stage": 4, + "replica": 7, + "orientation": "forward", + "active": 3, + "helper": 8, + "input": 8 + }, + { + "event": 339, + "stage": 4, + "replica": 15, + "orientation": "forward", + "active": 3, + "helper": 8, + "input": 8 + }, + { + "event": 342, + "stage": 5, + "replica": 6, + "orientation": "backward", + "active": 1, + "helper": 8, + "input": 8 + }, + { + "event": 345, + "stage": 5, + "replica": 14, + "orientation": "backward", + "active": 1, + "helper": 8, + "input": 8 + }, + { + "event": 348, + "stage": 6, + "replica": 5, + "orientation": "forward", + "active": 3, + "helper": 8, + "input": 8 + }, + { + "event": 351, + "stage": 6, + "replica": 13, + "orientation": "forward", + "active": 3, + "helper": 8, + "input": 8 + }, + { + "event": 354, + "stage": 7, + "replica": 4, + "orientation": "backward", + "active": 1, + "helper": 8, + "input": 8 + }, + { + "event": 355, + "stage": 7, + "replica": 12, + "orientation": "backward", + "active": 1, + "helper": 8, + "input": 8 + }, + { + "event": 356, + "stage": 8, + "replica": 3, + "orientation": "forward", + "active": 2, + "helper": 8, + "input": 8 + }, + { + "event": 366, + "stage": 8, + "replica": 11, + "orientation": "forward", + "active": 2, + "helper": 8, + "input": 8 + }, + { + "event": 376, + "stage": 5, + "replica": 7, + "orientation": "backward", + "active": 1, + "helper": 6, + "input": 6 + }, + { + "event": 379, + "stage": 5, + "replica": 15, + "orientation": "backward", + "active": 1, + "helper": 6, + "input": 6 + }, + { + "event": 382, + "stage": 6, + "replica": 6, + "orientation": "forward", + "active": 3, + "helper": 8, + "input": 8 + }, + { + "event": 385, + "stage": 6, + "replica": 14, + "orientation": "forward", + "active": 3, + "helper": 8, + "input": 8 + }, + { + "event": 388, + "stage": 7, + "replica": 5, + "orientation": "backward", + "active": 1, + "helper": 8, + "input": 8 + }, + { + "event": 389, + "stage": 7, + "replica": 13, + "orientation": "backward", + "active": 1, + "helper": 8, + "input": 8 + }, + { + "event": 390, + "stage": 8, + "replica": 4, + "orientation": "forward", + "active": 2, + "helper": 8, + "input": 8 + }, + { + "event": 400, + "stage": 8, + "replica": 12, + "orientation": "forward", + "active": 2, + "helper": 8, + "input": 8 + }, + { + "event": 410, + "stage": 6, + "replica": 7, + "orientation": "forward", + "active": 3, + "helper": 8, + "input": 8 + }, + { + "event": 413, + "stage": 6, + "replica": 15, + "orientation": "forward", + "active": 3, + "helper": 8, + "input": 8 + }, + { + "event": 416, + "stage": 7, + "replica": 6, + "orientation": "backward", + "active": 1, + "helper": 8, + "input": 8 + }, + { + "event": 417, + "stage": 7, + "replica": 14, + "orientation": "backward", + "active": 1, + "helper": 8, + "input": 8 + }, + { + "event": 418, + "stage": 8, + "replica": 5, + "orientation": "forward", + "active": 2, + "helper": 8, + "input": 8 + }, + { + "event": 428, + "stage": 8, + "replica": 13, + "orientation": "forward", + "active": 2, + "helper": 8, + "input": 8 + }, + { + "event": 438, + "stage": 7, + "replica": 7, + "orientation": "backward", + "active": 1, + "helper": 8, + "input": 8 + }, + { + "event": 439, + "stage": 7, + "replica": 15, + "orientation": "backward", + "active": 1, + "helper": 8, + "input": 8 + }, + { + "event": 440, + "stage": 8, + "replica": 6, + "orientation": "forward", + "active": 2, + "helper": 8, + "input": 8 + }, + { + "event": 450, + "stage": 8, + "replica": 14, + "orientation": "forward", + "active": 2, + "helper": 8, + "input": 8 + }, + { + "event": 460, + "stage": 8, + "replica": 7, + "orientation": "forward", + "active": 2, + "helper": 8, + "input": 8 + }, + { + "event": 470, + "stage": 8, + "replica": 15, + "orientation": "forward", + "active": 2, + "helper": 8, + "input": 8 + } + ], + "boundary_trace_sha256": "d06c70894c435567f35da1d1a9952e255dc27bb2640fd4417dc64b13bbbd39f6", + "local_envelopes": { + "forward": "2765345294379392599/1024", + "backward": "14824960514781440791821/64" + }, + "scaled_local_envelopes": { + "forward": "2765345294379392599/128", + "backward": "14824960514781440791821/8" + }, + "combined_norm_bits": 71, + "input_conversion_bits": 37, + "arithmetic_margin_bits": 4, + "old_sufficient_bits": 397, + "refined_sufficient_bits": 112, + "retained_payload_bits": 512 + }, + "borrowed_input_witness": { + "event": 25, + "stage": 0, + "replica": 11, + "helper": 0, + "family": 223, + "owner_replica": 0, + "active_upper": 1, + "helper_attained": 2, + "helper_row": [ + [ + 0, + 1 + ], + [ + 2, + 1 + ] + ], + "input_nonzero": [ + [ + 0, + 1 + ], + [ + 2, + 1 + ] + ], + "model": "Scalar identity unitaries; all other initial coordinates zero. Not a physical supplier replay." + }, + "controls_rejected": [ + { + "name": "doubled_bridge", + "predicate": "source event projection" + }, + { + "name": "bridge_wrong_source", + "predicate": "source event projection" + }, + { + "name": "wrong_local_orientation", + "predicate": "source local orientation/pair" + }, + { + "name": "same_family_two_helpers", + "predicate": "one role per physical family" + }, + { + "name": "helper_aliases_active_data", + "predicate": "one role per physical family" + }, + { + "name": "data_port_permutation", + "predicate": "active data family/port binding" + }, + { + "name": "wrong_program", + "predicate": "call program binding" + }, + { + "name": "missing_event", + "predicate": "source event count" + }, + { + "name": "reordered_events", + "predicate": "source event chronology" + }, + { + "name": "unrecognized_event", + "predicate": "source event projection" + }, + { + "name": "understated_input_cap", + "predicate": "actual owner input cap" + }, + { + "name": "post_terminal_borrow", + "predicate": "actual owner input cap", + "family": 336, + "stage": 8, + "replica": 8 + } + ], + "scope": "Conditional exact family-norm bound for the pinned finite controller. Local scalar/frame checks replayed unchanged; familywise unitary physical realization, cover bijections, recursive internals, roundoff/tape and analytic transfer remain inherited. No production charge or kappa change." +} diff --git a/research/selected1094-wire-prefix-audit/README.md b/research/selected1094-wire-prefix-audit/README.md new file mode 100644 index 0000000000..682d626454 --- /dev/null +++ b/research/selected1094-wire-prefix-audit/README.md @@ -0,0 +1,231 @@ +# Selected PR1094: a 112-bit conditional prefix estimate + +**Scoped precision audit; no new κ and no production reserve change.** +Following the actual data dependencies reduces the selected controller's +sufficient global-prefix estimate from **397 to 112 bits**, using its existing +positive scalar/Horner envelopes. The literal 16-replica controller has maximum +boundary norm majorant **14**. Every actual call's data and borrowed-helper +inputs have majorant at most **8**. The production payload remains **512 bits**. + +This refines Brody Arbon's [PR821](https://github.com/CrocSwap/integer-mult-bounds/pull/821) +replica-counter argument: track each pair and side, then inspect the actual +owners at each call. It is not a transplantation of PR821's historical 160-bit +estimate. Gareth Davidson's [PR1282](https://github.com/CrocSwap/integer-mult-bounds/pull/1282) +tightens the **local** signed envelope; that improvement and its code are not +used here. Both approaches build on eumemic's PR496 maximum-stream norm argument. +Concurrent [PR1093](https://github.com/CrocSwap/integer-mult-bounds/pull/1093) +by @woklerx also uses componentwise majorants, for a different 12-stage +cyclic-inverse word. Its 112-bit working precision is a separate result with +different interfaces and inputs; this package imports neither its code nor its +precision budget. +Gareth Davidson's [PR1309](https://github.com/CrocSwap/integer-mult-bounds/pull/1309) +formalizes a conditional stream-prefix norm implication; it does not bind this +controller's concrete call-input budgets. No Lean code is used or replayed here. + +## Reproduce and evidence + +From the repository root, using the standard library: + +```sh +python3 -I -O -B research/selected1094-wire-prefix-audit/verify.py +python3 -I -O -B research/selected1094-wire-prefix-audit/test_verify.py +python3.12 scripts/research_package.py --package research/selected1094-wire-prefix-audit +``` + +The verifier prints `PASS_SELECTED1094_WIRE_PREFIX_AUDIT` and +`conditional_bits=397->112 retained_payload=512 no_new_kappa`. +It writes only into a temporary directory. An intentional receipt regeneration +uses `--write /new/path.json`; existing output paths are refused. + +[EXPECTED.json](EXPECTED.json) records all 144 call input bounds, the 30 source +boundary vectors, exact envelopes, controls and source hashes. Fresh verification: + +- Binds the actual selected replay archive, provider programs and prefix receipt. +- Replays the unchanged local checker on both **704-column** arbitrary-input + maps and all **25** original rejection controls. Its entire parsed receipt + equals the archived receipt, including the positive coefficient-work bounds. +- Checks all **482** controller events, **144** calls and **69,120** helper + roles, including **57,480** cross-replica helper occurrences. A separate dense + 8×8 transfer calculation agrees at all **480** replica event boundaries. +- Rejects **12** mutations: altered bridges, local direction, physical aliases, + a data-port permutation, program mismatch, missing/reordered/unknown events, + a bound of seven, and a post-terminal helper borrow. + +These are finite source/interface checks. They are not a cold supplier replay +or a complete physical/operator verification. + +Verified on Linux x86_64 with CPython **3.12.13**, using the registered package +command above; all eight test groups passed. The verifier and exact receipt also +agree under CPython **3.11.15**. Tests include 9,600 exact squared-norm comparisons +in nonidentity, noncommuting two-dimensional unitary contract models, an +independent evaluation of the borrowed-input witness, strict bit-boundary cases, +source-corruption controls, and an optimized read-only export without Git. +`make selected-record-check` and the package metadata/source checks pass. + +## Conditional norm proposition and proof + +Use the inherited norm convention: for physical family `f`, let `N_f` be the +maximum, over its cover classes, of the stream's Hilbert norm on `2^73` entries. +Do **not** concatenate every physical family or every cover class into one +Euclidean norm. Let the initial maximum be `B`. Assume the retained interfaces: + +1. A completed forward call has the data endpoints `Y_i += U_i X_i`, and a + backward call `X_i -= U_i* Y_i`, where each `U_i` is unitary. Their physical + family/port pairing is exactly the emitted one. Cover-class permutations + preserve the maximum defining `N_f`. +2. Each borrowed helper's completed residual is unitary **within its own + family**. Its initial dirt does not leak into any other endpoint. Private + work is cleared. Whole calls, including their complete cover sweeps and + wrappers, finish before the next call. +3. Bridges update corresponding sides of two pairs of the same replica, with + their literal signed coefficient. Idle children, phases and translations + preserve individual family norms. A terminal signed exchange is within + its own final pair, after all that replica's local calls and bridges. +4. The inherited complete-cover realization transports the local positive + scalar/Horner envelope to physical streams: each stream is visited once + per call sweep. The original 37-bit input conversion, four-bit arithmetic + margin and recursive primitive-prefix interfaces remain available. + +These are the normalized interfaces behind the pinned invoice and the +[T16 proof](../complex-double-replica-owners/PROOF.md). The fresh local replay +checks their scalar/frame/wrapper premises; it does not prove the all-size or +physical realization statements. + +Index a family by `(replica, pair, side, port)`. Maintain one integer `b` per +replica/pair/side, uniformly over its 112 ports, initially one. At a forward +call set `b_Y := b_Y+b_X`; at a backward call set `b_X := b_X+b_Y`. +For a bridge set `b_dst,side := b_dst,side+|c| b_src,side` on both sides. +All familywise unitary events leave the bounds alone. At a terminal exchange, +replace both bounds in each pair by their maximum, which covers either signed +exchange convention conservatively. + +Induction gives `N_f <= b_f B`: the shear step is the triangle inequality and +unitarity; a helper endpoint leaves its owner's bound unchanged even when that +owner belongs to another replica. No calls are commuted, no helper is assumed +clean, and no signed cancellation between different calls is used. + +The source's eight bounds immediately before its terminal exchange are + +```text +(X0,Y0, X1,Y1, X2,Y2, X3,Y3) = (5,8, 9,14, 8,12, 6,9). +``` + +They increase monotonically up to a maximum of 14. The terminal update gives +`(8,8,14,14,12,12,9,9)`. Every replica has the same source projection; arbitrary +interleaving of those projections therefore preserves the boundary bound 14. +The source transfer matrices give a second exact computation of this table. + +Before each selected call, inspect **every** one of its 704 actual owner +families. Their current majorants are at most eight for both orientations. +This eightfold statement uses the pinned schedule and owner map; it is not +claimed for arbitrary maps or interleavings. Helpers dominate the active +pair's majorant in **126** of the 144 calls. + +The independently replayed **original** positive local envelopes are + +```text +K_forward = 2765345294379392599 / 1024 < 2^52 +K_backward = 14824960514781440791821 / 64 < 2^68. +``` + +Thus every local scalar/Horner prefix is bounded by `8 max(K_forward,K_backward) B`. +This also dominates the completed-boundary bound `14 B`. Exactly, + +```text +max(14, 8 K_forward, 8 K_backward) + = 14824960514781440791821 / 8 < 2^71. +``` + +Keeping the inherited conversion and margin gives **71+37+4 = 112** sufficient +bits. The original invoice charged `68+37+144+144+4 = 397`. +This improves a sufficient bound, not the actual attained physical maximum or +the minimal safe payload. Partial primitive execution and recursive internals +remain covered only to the extent of the inherited arithmetic/compiler contract. + +## Adversarial boundary and limits + +Counting only the active data pair is insufficient. At emitted event 25, +stage 0 of replica 11 borrows helper 0 from physical family 223 in replica 0. +In the exact scalar contract model with identity familywise unitaries, its row +is `initial_X0 + initial_X1` of replica 0. Set those two inputs to one and all +others to zero. This helper is two while the new replica's active inputs are +zero (their unit-input operator bound is one). The receipt supplies the exact +row and input. This instantiates PR821's borrowed-input warning on the selected +map; it is **not** a new physical counterexample to the selected construction. + +The post-terminal control preserves counts, owner ranges and within-call +uniqueness but points a later helper at family 336 after its bound has reached +14. The checker rejects the claimed eightfold input cap. Such a borrow also +violates the production hosting windows; no production acceptance bug is +alleged. Mutations enter the semantic checks after loading the pinned positive +fixture, so their rejection does not rely on a stale checksum. + +Not established here: fresh complete controller/hosting admission; all native +Clifford and phase identities; optimality of 112; roundoff or lattice transport; +the all-size/common-label/mutable-source and tape/analytic interfaces; Lean or +human peer review. The helper chart geometry, window legality and existing +physical implementation remain inherited. A smaller local prefix estimate +alone does not change the paid rank profile, recursive moment or κ. + +## Scope, provenance and coordination + +Base: `ef5f39403610d231a0c27e8a6b4f08c10209bcd6` (current main at entry). +Rebased for submission onto `c5108f0f68d482e5712a8e26a5978d47762dfc16`; +the applicable guidance, selected record and all consumed source bytes are +unchanged between those commits. +Selected PR1094: `0fc329d0bec93ca7cd288eaea1295172e8789810`; parent PR1087: +`589d1cedf5ef5f231182f4ec86408616311a8af0`. +[SOURCES.json](SOURCES.json) pins source bytes and Git blobs. Historical selected +record and catalogue pins do not track later moving selections. + +The chooser's nonce was `2ebb0ab34af6cc7e7d70f4ddf504ef89`, adversarial-audit, +priority revision 2. The `supplier-boundary-audit` card is **refined** to the +global-prefix obligation; [TASK.json](TASK.json) records the claim and stop rule. +The historical owner audit and current baseline-binding orientation commands +passed. Initial overlap covered all 759 public open PR titles/bodies, including +drafts. A complete public REST refresh at **2026-10-14 02:30:51 UTC** covered +781 open PRs. Public Discussion pages and searches were checked, but comments +were not exhaustively enumerated. The overlap helper's 02:31:44 UTC refresh +covered 327 local records and reported unavailable authenticated remote caches; +the public REST check supplies separate open-PR coverage. No novelty claim +follows from these searches. PR1112 independently checks the historical PR1042 +397-bit invoice arithmetic; it does not propagate these current owner bounds. + +The authenticated board refresh at 02:48–02:50 UTC covered 80 Discussion +titles/bodies, all 27 top-level handoff comments, and the empty comment thread +on Discussion1260. Other comment/reply trees remain only partially covered. +The initial claim was retained locally while API access was located. The +subsequent Discussion1260 post was explicitly rejected by GitHub's organization +OAuth-app restriction. The finding and submission material are retained with +this public branch. No original source, selected record, frozen evidence or +production verifier is changed. + +## Open next questions + +1. **Can this bound support a 128-bit production reserve?** It could reduce + physical row overhead, although it need not improve κ. First add this + dependency-bound check to an opt-in successor invoice and replay the complete + local/native/hosting/precision chain with a 128-bit charge. Adoption is blocked + by the inherited recursive/roundoff interfaces and the required complete cold + replay; this note does not authorize changing a frozen invoice. +2. **Can the bound be composed with PR1282's signed local envelopes?** This + could tighten the sufficient norm bound further. First independently replay + and bind that package, then check the partial-component and wrapper interfaces + against the same cover norm and owner inputs. Its estimates are pending + independent adoption and are deliberately not numerical inputs here. + +## Credit + +Credit eumemic's PR496 for the maximum-stream norm and unitary-helper argument; +Brody Arbon's PR821 for historical replica counters and the cross-replica input +caution; Gareth Davidson's PR1282 for the complementary signed-local audit; +@woklerx's PR1093 for the concurrent componentwise-majorant precision work; +Rohan Arun's PR1094, Jeremy Kothe's k8/T16 lineage, Hao Yan's PR858 controller, +Douglas Colkitt's integration and source archives, and icekylinx's credited +PR514/PR433 local checker with the retained HPE/compiler/Clifford contributors. +Their implementations and notices remain unchanged. Triangle-inequality +majorants and transfer matrices are standard methods, with no priority claim. + +Prepared with substantial OpenAI Codex (GPT-6 Astra) assistance in mathematics, +implementation, testing and prose. No subagents or independent human review. +New material is Apache-2.0. diff --git a/research/selected1094-wire-prefix-audit/SOURCES.json b/research/selected1094-wire-prefix-audit/SOURCES.json new file mode 100644 index 0000000000..fb106a2e58 --- /dev/null +++ b/research/selected1094-wire-prefix-audit/SOURCES.json @@ -0,0 +1,96 @@ +{ + "schema_version": 1, + "base_commit": "ef5f39403610d231a0c27e8a6b4f08c10209bcd6", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb", + "sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce" + }, + { + "path": "research/community-frontier1094-audit/REPLAY.json", + "usage": "input", + "git_blob": "2cfb7fffa7cd78f418be16c13224c3206b6d0183", + "sha256": "ce0678fa7abaab221de74baeace0c6696d5ea23a36719a58cff230215a06aae7" + }, + { + "path": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "usage": "input", + "git_blob": "6a75493790b4eff9c4a98051ef8b01d6aad0d5a8", + "sha256": "79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b" + }, + { + "path": "research/community-frontier1094-audit/selected-replay.tar.gz", + "usage": "input", + "git_blob": "c24daf067f9c543421d89ca2eeaa4eb78a57fb6f", + "sha256": "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6" + }, + { + "path": "research/complex-k492-owner-repair/code/hpe_audit_local.py", + "usage": "input", + "git_blob": "17bccb64fdca54f329a3ce16e369449cb76c2802", + "sha256": "6bd9a1e279c9c9e4f3767d9f82e537b559292906feb2ddab02f380fb6523a810" + }, + { + "path": "research/gauge44-slots-t16/code/invoice_allcold.py", + "usage": "input", + "git_blob": "d1dd2212917ad1e7f099287a141f741fd52bdcf6", + "sha256": "71eb57514e28ced97251e0507105f654f59885ec4d40486a780bf166098858a8" + }, + { + "path": "research/complex-double-replica-owners/PROOF.md", + "usage": "input", + "git_blob": "eb980efd5f34eb913714d1e6cb0860ced13ef1bb", + "sha256": "db99599e3966bec253c577c23915e2a2899c4c4e8568044efc11c7918b137bbc" + } + ], + "predecessor_references": [ + { + "pr": 496, + "author": "eumemic", + "head": "00cf70efd6a8637531deafef698157ca83e249ee", + "path": "research/r489-pooled-whole-complex/PROOF.md", + "sha256": "144f1bf6952b3e31e99cf372a2cae9a13f96c9988808fe8a57ec70b09ee2007c", + "usage": "Attribution and inherited norm-interface reference; not a runtime input." + }, + { + "pr": 821, + "author": "Brody Arbon", + "head": "6b832a6ba4dce8dd6e2fb0897dd4543364b932f8", + "path": "research/replica-prefix-audit/PROOF.md", + "usage": "Read for overlap and attribution; no code imported." + }, + { + "pr": 1282, + "author": "Gareth Davidson", + "head": "851e5232f7c9e105fb6e8f3a7be7a070e7524012", + "path": "research/complex-signed-prefix-audit/PROOF.md", + "usage": "Read for overlap; its improved signed local estimates are not used." + }, + { + "pr": 1093, + "author": "woklerx", + "head": "fb60f5753cc76c325b5048612a344c3ea1b7c822", + "usage": "PR body read for overlap and attribution to concurrent componentwise-majorant work on a different word; not a runtime input." + }, + { + "pr": 1112, + "author": "Sagar Thakrar", + "head": "3a6a13cf4fbda16e1d191553f8b08cb6a3d5ed27", + "usage": "PR body read for distinction from historical PR1042 invoice arithmetic; not a runtime input." + }, + { + "pr": 1309, + "author": "Gareth Davidson", + "head": "5bde684f9189b59d1388c089ec5475fb5cf59565", + "usage": "Discussion1291 and PR head read for overlap with conditional stream-prefix formalization; no Lean or runtime dependency." + } + ] +} diff --git a/research/selected1094-wire-prefix-audit/TASK.json b/research/selected1094-wire-prefix-audit/TASK.json new file mode 100644 index 0000000000..62d69178c5 --- /dev/null +++ b/research/selected1094-wire-prefix-audit/TASK.json @@ -0,0 +1,105 @@ +{ + "schema_version": 1, + "task_id": "supplier-boundary-audit", + "priority_revision": 2, + "base_commit": "ef5f39403610d231a0c27e8a6b4f08c10209bcd6", + "original_card": { + "id": "supplier-boundary-audit", + "question": "Does one selected supplier obligation follow from its actual source-bound checks?", + "starting_points": [ + "certificates/selected-result.json", + "research/owner-boundary-audit/README.md" + ], + "methods": [ + "Trace one hypothesis through the source, checker and complete caller.", + "Construct one semantically invalid but superficially well-formed fixture and test rejection." + ], + "acceptance_gate": "Pin the current sources and one obligation; the historical owner audit is an example, not evidence of a current bug.", + "first_step": { + "command": [ + "python3", + "-B", + "research/owner-boundary-audit/verify.py" + ], + "expected": "PASS_PR626_NEXT_TOUCH_BOUNDARY_AUDIT", + "inspect": "Identify why the timing-only omission passes but the full production controller still rejects it.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Choose one current supplier obligation and trace whether its acceptance depends on an independent check.", + "bottleneck_link": "Closing a current acceptance gap or proof obligation strengthens reliability even without changing kappa.", + "allowed_variations": [ + "Audit one named current condition using a new semantic counterexample." + ], + "scope_change_triggers": [ + "Reporting the historical timing-only diagnostic as a new current acceptance bug." + ], + "overlap_terms": [ + "owner boundary", + "bridge omission", + "hosting" + ] + }, + "scope_status": "refined", + "actual_scope": "Audit the current PR1094 global-prefix growth obligation by propagating per-pair/side Hilbert-norm majorants through its literal 16-replica controller. Bind all calls and arbitrary-dirty local endpoints; test semantic mutations of the schedule and local boundary.", + "scope_change_reason": "The supplier-boundary card is narrowed to one current precision obligation. The historical timing-only audit is orientation, not evidence of a current bug. This is a conditional refinement of an existing sufficient norm bound, not a changed supplier.", + "bottleneck_link": "Sharper justified global coefficient growth is relevant to precision and physical row reserves; the production 512-bit charge and recursive paid profile remain unchanged, so no kappa improvement is claimed.", + "budget_minutes": 60, + "stop_rule": "Finish the fixed selected archive: 482 controller events, 144 calls, 69120 helper roles, both local words and focused mutations. Stop if the familywise unitary/shear assumptions cannot justify the bound; no parameter search or new supplier.", + "outcome": "completed", + "evidence": "EXPECTED.json: 482 events, 144 calls, 69120 helper roles, boundary majorant 14 and all call input majorants at most 8. Original two-orientation 704-column local replay and 25 controls reproduce the archived receipt; 12 added semantic controls reject. Conditional sufficient estimate 397 to 112 bits, production charge 512 unchanged.", + "author": "OpenAI Codex (GPT-6 Astra)", + "ai_assistance": "Substantial OpenAI Codex (GPT-6 Astra) assistance in mathematics, implementation, verification and prose. No subagents or independent human review.", + "open_questions": [ + { + "question": "Can the dependency bound support a 128-bit production reserve?", + "why_it_matters": "A smaller certified payload can lower physical row overhead without necessarily changing the recursive moment.", + "first_step": "Build an opt-in successor invoice with this guard and run the complete native, hosting, precision and cold-replay chain at a 128-bit charge.", + "blocked_by": "Inherited recursive and roundoff interfaces, full cold replay, and maintainer adoption of a successor invoice remain required." + }, + { + "question": "Can PR1282 signed local envelopes be combined with the actual-owner input bounds?", + "why_it_matters": "The two arguments tighten different multiplicative factors in the sufficient prefix bound.", + "first_step": "Independently replay and pin PR1282, then reconcile its partial-component and wrapper contracts with the same physical cover norm.", + "blocked_by": "Pending source admission and proof of compatibility; PR1282 values are not inputs to this package." + } + ], + "assignment": { + "nonce": "2ebb0ab34af6cc7e7d70f4ddf504ef89", + "track": "adversarial-audit", + "scope_key": "dcdb0fa8e49b08a958d0:selected1094-wire-prefix" + }, + "coordination": { + "local_claim_utc": "2026-10-14T02:09:00Z", + "claim_expiry_utc": "2026-10-14T04:09:00Z", + "posting": "Initial claim retained locally. Authenticated as columbia-git through the configured Composio connection; GitHub rejected the Discussion1260 addDiscussionComment mutation because CrocSwap restricts OAuth app access. Public fork publication remains available.", + "overlap": "Initial 759 and final 781 open PR title/body records retrieved with complete public REST pagination (final 2026-10-14T02:30:51.682592+00:00). Discussions checked through public pages/searches, not complete comments. The overlap helper refreshed 327 local records at 02:31:44 UTC; authenticated remote caches unavailable. Authenticated refresh at 02:48-02:50 UTC covered 80 Discussion titles/bodies, 27 top-level handoff comments and the empty Discussion1260 comment thread; other replies are partial. Main advanced to submission_base_commit without changing guidance, priorities, selected record or consumed sources.", + "predecessors": [ + { + "pr": 821, + "head": "6b832a6ba4dce8dd6e2fb0897dd4543364b932f8", + "credit": "Brody Arbon; historical per-replica counting, built on eumemic PR496." + }, + { + "pr": 1282, + "head": "851e5232f7c9e105fb6e8f3a7be7a070e7524012", + "credit": "Gareth Davidson; selected signed local prefixes, not used as a computational dependency." + }, + { + "pr": 1093, + "head": "fb60f5753cc76c325b5048612a344c3ea1b7c822", + "credit": "woklerx; parallel componentwise-majorant method for a different 12-stage cyclic-inverse word, not a code or numerical dependency." + }, + { + "pr": 1112, + "head": "3a6a13cf4fbda16e1d191553f8b08cb6a3d5ed27", + "credit": "Sagar Thakrar; historical PR1042 finite invoice arithmetic, not this current dependency-bound computation." + }, + { + "pr": 1309, + "head": "5bde684f9189b59d1388c089ec5475fb5cf59565", + "credit": "Gareth Davidson; conditional stream-prefix norm formalization, not this emitted controller input-bound audit; no Lean replay claimed." + } + ] + }, + "submission_base_commit": "c5108f0f68d482e5712a8e26a5978d47762dfc16" +} diff --git a/research/selected1094-wire-prefix-audit/VERIFY.json b/research/selected1094-wire-prefix-audit/VERIFY.json new file mode 100644 index 0000000000..78235ffea5 --- /dev/null +++ b/research/selected1094-wire-prefix-audit/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/community-frontier1094-audit/REPLAY.json", + "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "research/community-frontier1094-audit/selected-replay.tar.gz", + "research/complex-k492-owner-repair/code/hpe_audit_local.py", + "research/gauge44-slots-t16/code/invoice_allcold.py", + "research/complex-double-replica-owners/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Source-bound controller norm audit, unchanged complete local scalar/frame replay with 25 controls, 12 semantic mutations, exact receipt equality." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 300, + "checks": "Exact rational Hilbert models, independent numeric borrow witness, strict precision boundary, source/inventory corruption and read-only optimized relocation." + } + ] +} diff --git a/research/selected1094-wire-prefix-audit/test_verify.py b/research/selected1094-wire-prefix-audit/test_verify.py new file mode 100644 index 0000000000..963b414f54 --- /dev/null +++ b/research/selected1094-wire-prefix-audit/test_verify.py @@ -0,0 +1,182 @@ +#!/usr/bin/env python3 +"""Exact interface models and fail-closed package checks. Apache-2.0. + +OpenAI Codex (GPT-6 Astra), substantial AI assistance. +""" +import copy +from fractions import Fraction as Q +import importlib.util +import json +import os +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest +from unittest.mock import patch + +PACKAGE = Path(__file__).resolve().parent +spec = importlib.util.spec_from_file_location("wire_prefix", PACKAGE / "verify.py") +audit = importlib.util.module_from_spec(spec) +spec.loader.exec_module(audit) + + +def apply(matrix, vector): + return tuple(sum(x*y for x, y in zip(row, vector)) for row in matrix) + + +def square(vector): + return sum(x*x for x in vector) + + +class VerificationTests(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.context = audit.load() + + def test_rational_hilbert_models(self): + """Nonidentity, noncommuting within-family unitaries at every boundary.""" + matrices = [((Q(1), Q(0)), (Q(0), Q(1))), + ((Q(3, 5), Q(-4, 5)), (Q(4, 5), Q(3, 5))), + ((Q(5, 13), Q(12, 13)), (Q(12, 13), Q(-5, 13))), + ((Q(0), Q(1)), (Q(1), Q(0)))] + vectors = [(Q(1), Q(0)), (Q(0), Q(-1)), (Q(3, 5), Q(4, 5)), + (Q(0), Q(0)), (Q(-5, 13), Q(12, 13))] + for matrix in matrices: + for i in range(2): + for j in range(2): + self.assertEqual(sum(matrix[k][i]*matrix[k][j] for k in range(2)), int(i == j)) + parent = self.context["parent"] + source = {e["stage"]: e for e in parent["recipe"] if e["kind"] == "local"} + table = audit.matrix_boundaries(parent) + comparisons = 0 + for seed in range(40): + states = [vectors[(seed + 3*j) % len(vectors)] for j in range(8)] + for index, event in enumerate(parent["execution_schedule"][:30]): + # These may be nonidentity helper residuals. Only the norm + # property is modeled, not the selected physical phase maps. + states = [apply(matrices[(seed+index+j) % len(matrices)], value) + for j, value in enumerate(states)] + if event["kind"] == "local_cover_sweep": + q = source[event["stage"]] + x, y = 2*q["pair"], 2*q["pair"]+1 + unitary = matrices[(seed+index) % len(matrices)] + if q["reverse"]: + adjoint = tuple(zip(*unitary)) + image = apply(adjoint, states[y]) + states[x] = tuple(a-b for a, b in zip(states[x], image)) + else: + image = apply(unitary, states[x]) + states[y] = tuple(a+b for a, b in zip(states[y], image)) + elif event["kind"] == "bridge": + for side in range(2): + d, s = 2*event["dst"]+side, 2*event["src"]+side + states[d] = tuple(a+event["coefficient"]*b for a, b in zip(states[d], states[s])) + elif event["kind"] == "terminal": + for pair in range(4): + x, y = 2*pair, 2*pair+1 + states[x], states[y] = states[y], tuple(-v for v in states[x]) + for value, bound in zip(states, table[index]): + self.assertLessEqual(square(value), bound*bound) + comparisons += 1 + self.assertEqual(comparisons, 9600) + + def test_familywise_is_material(self): + # A unitary on the concatenation of two scalar families need not + # preserve their maximum individual norm. Same distinction as PR821. + unitary = ((Q(3, 5), Q(4, 5)), (Q(-4, 5), Q(3, 5))) + before = (Q(1), Q(1)) + after = apply(unitary, before) + self.assertEqual(square(before), square(after)) + self.assertGreater(max(map(abs, after)), max(map(abs, before))) + + def test_borrow_witness_by_numeric_execution(self): + context = self.context + witness = audit.scalar_borrow_witness(context) + initial = dict(witness["input_nonzero"]) + values = [Q(initial.get(j, 0)) for j in range(128)] + recipe = {e["stage"]: e for e in context["parent"]["recipe"] if e["kind"] == "local"} + for event in context["template"]["execution_schedule"][:witness["event"]]: + replica = event["replica"] + if event["kind"] == "local_cover_sweep": + q = recipe[event["stage"]] + x, y = 8*replica+2*q["pair"], 8*replica+2*q["pair"]+1 + if q["reverse"]: + values[x] -= values[y] + else: + values[y] += values[x] + elif event["kind"] == "bridge": + for side in range(2): + values[8*replica+2*event["dst"]+side] += ( + event["coefficient"]*values[8*replica+2*event["src"]+side]) + self.assertEqual(abs(values[witness["family"] // audit.V]), witness["helper_attained"]) + self.assertEqual(values[8*witness["replica"]:8*witness["replica"]+2], [0, 0]) + self.assertGreater(witness["helper_attained"], witness["active_upper"]) + + def test_exact_strict_bit_boundary(self): + self.assertEqual(audit.strict_bits(Q(2)**71 - Q(1, 2)**200), 71) + self.assertEqual(audit.strict_bits(Q(2)**71), 72) + self.assertEqual(audit.strict_bits(Q(2)**71 + Q(1, 2)**200), 72) + with self.assertRaisesRegex(audit.AuditError, "positive envelope"): + audit.strict_bits(0) + + def test_cosmetic_metadata_does_not_change_the_bound(self): + template = dict(self.context["template"], note="cosmetic audit annotation") + self.assertEqual(audit.recount(self.context), audit.recount(self.context, template)) + + def test_missing_required_pin_rejected(self): + pins = json.loads((PACKAGE / "SOURCES.json").read_bytes()) + pins["files"] = [p for p in pins["files"] if p["path"] != audit.CHECKER] + with tempfile.TemporaryDirectory(prefix="wire-prefix-pins-") as temporary: + package = Path(temporary) + (package / "SOURCES.json").write_text(json.dumps(pins)) + with patch.object(audit, "PACKAGE", package): + with self.assertRaisesRegex(audit.AuditError, "mandatory source inventory"): + audit.check_pins() + + def test_source_corruption_rejected(self): + with tempfile.TemporaryDirectory(prefix="wire-prefix-source-") as temporary: + root = Path(temporary) + for name in audit.INPUTS: + target = root / name + target.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(audit.ROOT / name, target) + target = root / audit.CHECKER + target.write_bytes(target.read_bytes() + b"\n# source mutation\n") + with self.assertRaisesRegex(audit.AuditError, "source hash:"): + audit.check_pins(root) + + def test_optimized_read_only_relocation_without_git(self): + with tempfile.TemporaryDirectory(prefix="wire-prefix-export-") as temporary: + root = Path(temporary) + for name in audit.INPUTS: + target = root / name + target.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(audit.ROOT / name, target) + package = root / "research" / PACKAGE.name + shutil.copytree(PACKAGE, package, ignore=shutil.ignore_patterns("__pycache__")) + files = [p for p in root.rglob("*") if p.is_file()] + directories = [p for p in root.rglob("*") if p.is_dir()] + for path in files: + path.chmod(0o444) + for path in directories: + path.chmod(0o555) + before = {str(p.relative_to(root)): audit.sha(p.read_bytes()) for p in files} + try: + run = subprocess.run([sys.executable, "-I", "-O", "-B", str(package / "verify.py")], + cwd=root, capture_output=True, text=True, timeout=240) + self.assertEqual(run.returncode, 0, run.stdout + run.stderr) + self.assertIn("conditional_bits=397->112", run.stdout) + self.assertEqual(before, {str(p.relative_to(root)): audit.sha(p.read_bytes()) for p in files}) + self.assertFalse((root / ".git").exists()) + self.assertFalse(list(root.rglob("__pycache__"))) + finally: + for path in directories: + path.chmod(0o755) + for path in files: + path.chmod(0o644) + + +if __name__ == "__main__": + unittest.main(verbosity=2) diff --git a/research/selected1094-wire-prefix-audit/verify.py b/research/selected1094-wire-prefix-audit/verify.py new file mode 100644 index 0000000000..605fbeb1f0 --- /dev/null +++ b/research/selected1094-wire-prefix-audit/verify.py @@ -0,0 +1,468 @@ +#!/usr/bin/env python3 +"""Source-bound family-norm majorants for the selected PR1094 controller. + +OpenAI Codex (GPT-6 Astra), substantial AI assistance. Apache-2.0. +Builds on eumemic's PR496 family-norm argument and Brody Arbon's PR821 +replica counters. The retained local checker is replayed, not reimplemented. +No production precision charge or kappa is changed. +""" +import argparse +from collections import Counter +import copy +from fractions import Fraction as Q +import gzip +import hashlib +import json +import os +from pathlib import Path +import subprocess +import sys +import tarfile +import tempfile + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parent.parent +ARCHIVE = "research/community-frontier1094-audit/selected-replay.tar.gz" +MANIFEST = "research/community-frontier1094-audit/SELECTED-SOURCE.json" +REPLAY = "research/community-frontier1094-audit/REPLAY.json" +CHECKER = "research/complex-k492-owner-repair/code/hpe_audit_local.py" +INVOICE = "research/gauge44-slots-t16/code/invoice_allcold.py" +SUPPLIER_PROOF = "research/complex-double-replica-owners/PROOF.md" +INPUTS = {ARCHIVE, MANIFEST, REPLAY, CHECKER, INVOICE, SUPPLIER_PROOF} +BASE = "candidate/strict/global/base/" +PROVIDER = BASE + "providers/gauge44/" +HOSTED = "candidate/strict/global/hosted/GLOBAL-TEMPLATE.json.gz" +PARENT = BASE + "split-centres/GLOBAL-TEMPLATE.json.gz" +PREFIX = "candidate/strict/global/audit/GLOBAL-PREFIX.json" +V, REPLICAS, PAIRS, HELPERS = 112, 16, 4, 480 +LIVE = V * REPLICAS * PAIRS * 2 + + +class AuditError(ValueError): + pass + + +def need(ok, message): + if not ok: + raise AuditError(message) + + +def canonical(obj): + return json.dumps(obj, sort_keys=True, separators=(",", ":")).encode() + + +def sha(data): + return hashlib.sha256(data).hexdigest() + + +def strict_bits(value): + """Least nonnegative integer b with value < 2**b, using exact arithmetic.""" + value = Q(value) + need(value > 0, "positive envelope") + b = 0 + while value >= 1 << b: + b += 1 + return b + + +def check_pins(root=ROOT): + pins = json.loads((PACKAGE / "SOURCES.json").read_bytes()) + live = [p for p in pins["files"] if p["usage"] == "input"] + need(len(live) == len(INPUTS) and {p["path"] for p in live} == INPUTS, + "mandatory source inventory") + for p in live: + need(sha((root / p["path"]).read_bytes()) == p["sha256"], + "source hash: " + p["path"]) + selected = json.loads((root / MANIFEST).read_bytes())["files"] + need(selected[INVOICE] == sha((root / INVOICE).read_bytes()), "selected invoice binding") + need(selected["research/complex-sw4-frame8/local/hpe_audit_local.py"] + == sha((root / CHECKER).read_bytes()), "selected local checker binding") + return {p["path"]: p["sha256"] for p in live} + + +def load(root=ROOT): + hashes = check_pins(root) + names = [HOSTED, PARENT, PREFIX] + [PROVIDER + n for n in ( + "CANONICAL-WORD.json.gz", "LOCAL-PROGRAMS.json.gz", + "LOCAL-CHECKS.json", "INDEPENDENT-LOCAL-REPLAY.json")] + blobs = {} + with tarfile.open(root / ARCHIVE) as archive: + for name in names: + members = [m for m in archive.getmembers() if m.name == name] + need(len(members) == 1 and members[0].isfile(), "unique regular member: " + name) + blobs[name] = archive.extractfile(members[0]).read() + + def read(name): + data = blobs[name] + return json.loads(gzip.decompress(data) if name.endswith(".gz") else data) + + template, parent, prefix = map(read, (HOSTED, PARENT, PREFIX)) + word = read(PROVIDER + "CANONICAL-WORD.json.gz") + programs = read(PROVIDER + "LOCAL-PROGRAMS.json.gz") + local = read(PROVIDER + "INDEPENDENT-LOCAL-REPLAY.json") + checks = read(PROVIDER + "LOCAL-CHECKS.json") + need(sha(gzip.decompress(blobs[HOSTED])) == prefix["template_sha256"], + "global prefix template binding") + need((word["v"], word["R"], word["h"], template["m"], template["live"]) + == (V, HELPERS, 9, 73, LIVE), "selected dimensions") + need(set(template["local_providers"]) == {"gauge44"}, "one selected provider") + registry = template["local_providers"]["gauge44"] + for name, field in [("CANONICAL-WORD.json.gz", "canonical_word_sha256"), + ("LOCAL-PROGRAMS.json.gz", "local_programs_sha256")]: + need(sha(blobs[PROVIDER + name]) == local[field] == registry[field], + "local artifact binding: " + name) + need(registry["local_programs"] == programs and registry["local_program_checks"] == checks, + "provider program/check binding") + need(set(programs) == {"forward", "backward"}, "both local orientations") + for name, events in programs.items(): + digest = sha(json.dumps(events, separators=(",", ":")).encode()) + need(digest == checks[name]["sha256"], "program digest") + published = json.loads((root / REPLAY).read_bytes()) + need(published["prefix_bits"] == prefix["global_prefix_bits"] == 397 + and published["charged_prefix_bits"] == prefix["retained_payload_bits"] == 512, + "published precision record") + return dict(template=template, parent=parent, prefix=prefix, local=local, + checks=checks, blobs=blobs, hashes=hashes) + + +def replay_local(context, root=ROOT): + """Run the unchanged, pinned original checker with assertions enabled.""" + with tempfile.TemporaryDirectory(prefix="pr1094-wire-prefix-") as temp: + work = Path(temp) + for name in ("CANONICAL-WORD.json.gz", "LOCAL-PROGRAMS.json.gz"): + (work / name).write_bytes(context["blobs"][PROVIDER + name]) + env = dict(os.environ, PYTHONDONTWRITEBYTECODE="1") + env.pop("PYTHONOPTIMIZE", None) + run = subprocess.run([sys.executable, "-B", str(root / CHECKER), str(work)], + cwd=work, env=env, capture_output=True, text=True, timeout=180) + need(run.returncode == 0, "retained local replay failed: " + run.stdout + run.stderr) + result = json.loads((work / "INDEPENDENT-LOCAL-REPLAY.json").read_bytes()) + need(result == context["local"], "fresh local receipt differs") + return dict(status=result["status"], exact_columns_per_orientation=2 * V + HELPERS, + orientations=["forward", "backward"], + original_controls_rejected=result["negative_controls_rejected"], + receipt_identical=True) + + +def stripped(event): + return {k: v for k, v in event.items() + if k not in {"replica", "replicas", "source_event", "time", "provider_id"}} + + +def validate_controller(template, parent, checks): + """Check the specific structural hypotheses consumed by the norm proof.""" + need(template["recipe"] == parent["recipe"], "source recipe") + need("each local invocation completes before the next" in template["loop_order"].lower(), + "atomic invocation contract") + recipe = {e["stage"]: e for e in parent["recipe"] if e["kind"] == "local"} + need(set(recipe) == set(range(9)), "all source stages") + calls = template["calls"] + need(len(calls) == 9 * REPLICAS, "call count") + by_call = {(c["stage"], c["replica"]): c for c in calls} + need(set(by_call) == {(s, r) for s in range(9) for r in range(REPLICAS)}, + "complete distinct calls") + cross = 0 + for c in calls: + r, s = c["replica"], c["stage"] + source = recipe[s] + orientation = "backward" if source["reverse"] else "forward" + need(c["pair"] == source["pair"] and c["orientation"] == orientation, + "source local orientation/pair") + need(c["provider_id"] == "gauge44" and + c["local_program_sha256"] == checks[orientation]["sha256"], "call program binding") + families = [f for f, route in c["owners"]] + need(len(families) == 2 * V + HELPERS and + all(type(f) is int and 0 <= f < LIVE for f in families), "owner family range/count") + need(len(set(families)) == len(families), "one role per physical family") + first = (r * 8 + source["pair"] * 2) * V + need(families[:2 * V] == list(range(first, first + 2 * V)), "active data family/port binding") + cross += sum(f // (8 * V) != r for f in families[2 * V:]) + + schedule = template["execution_schedule"] + need(len(schedule) == 30 * REPLICAS + 2, "source event count") + per_replica = [[] for _ in range(REPLICAS)] + order = [] + last_time = [None] * REPLICAS + for e in schedule[:-2]: + r = e["replica"] + need(type(r) is int and 0 <= r < REPLICAS and e["replicas"] == [r], "event replica") + j = e["source_event"] + need(type(j) is int and j == len(per_replica[r]) and j < 30, "source event chronology") + need(stripped(e) == stripped(parent["execution_schedule"][j]), "source event projection") + if e["kind"] == "local_cover_sweep": + c = by_call[e["stage"], r] + need(e["time"] == c["time"] == len(order) and e["provider_id"] == c["provider_id"], + "call time/provider binding") + order.append([e["stage"], r]) + last_time[r] = e["time"] + need(e["time"] == last_time[r], "event block time") + per_replica[r].append(j) + need(all(row == list(range(30)) for row in per_replica), "complete source projection") + need(order == template["async_schedule"]["order"], "async order binding") + need(schedule[-2] == dict(kind="bank_padding_cover_sweep", source_event=30, + families=[LIVE, LIVE], children_source="bank_padding.children"), + "empty terminal bank sweep") + end = dict(parent["execution_schedule"][31], source_event=31, + families=[0, LIVE], charged_calls_per_cover=LIVE) + need(schedule[-1] == end, "terminal familywise translation") + need(not template["bank_padding"]["children"] and + not template["bank_padding"]["families"], "no bank roles") + return by_call, recipe, cross + + +def norm_step(bounds, event, recipe): + """Nonnegative transfer; no signed cancellation is used.""" + kind = event["kind"] + r = event.get("replica", 0) + if kind == "local_cover_sweep": + call = recipe[event["stage"]] + source, target = 8 * r + 2 * call["pair"], 8 * r + 2 * call["pair"] + 1 + if call["reverse"]: + source, target = target, source + bounds[target] += bounds[source] + elif kind == "bridge": + for side in range(2): + bounds[8 * r + 2 * event["dst"] + side] += ( + abs(event["coefficient"]) * bounds[8 * r + 2 * event["src"] + side]) + elif kind == "terminal": + # Conservatively allow either signed exchange within each final pair. + for pair in range(PAIRS): + a = 8 * r + 2 * pair + bounds[a] = bounds[a + 1] = max(bounds[a:a + 2]) + else: + need(kind in {"idle_cover_sweep", "terminal_Y_translations", + "bank_padding_cover_sweep", "translate_every_live_family"}, "unknown norm event") + + +def matrix_boundaries(parent): + """Separate dense 8x8 transfer calculation on the unexpanded source recipe.""" + recipe = {e["stage"]: e for e in parent["recipe"] if e["kind"] == "local"} + matrix = [[int(i == j) for j in range(8)] for i in range(8)] + table = [] + for event in parent["execution_schedule"][:30]: + step = [[int(i == j) for j in range(8)] for i in range(8)] + if event["kind"] == "local_cover_sweep": + q = recipe[event["stage"]] + target = 2*q["pair"] + (0 if q["reverse"] else 1) + source = 2*q["pair"] + (1 if q["reverse"] else 0) + step[target][source] = 1 + elif event["kind"] == "bridge": + for side in range(2): + step[2*event["dst"]+side][2*event["src"]+side] = abs(event["coefficient"]) + matrix = [[sum(step[i][k]*matrix[k][j] for k in range(8)) + for j in range(8)] for i in range(8)] + if event["kind"] == "terminal": + # Either signed exchange is bounded by the larger row sum. + for pair in range(PAIRS): + a = 2*pair + row = max(matrix[a:a+2], key=sum) + matrix[a], matrix[a+1] = row.copy(), row.copy() + table.append([sum(row) for row in matrix]) + return table + + +def recount(context, template=None, entry_cap=8): + template = context["template"] if template is None else template + calls, recipe, cross = validate_controller(template, context["parent"], context["checks"]) + bounds = [1] * (8 * REPLICAS) + matrix_table = matrix_boundaries(context["parent"]) + trace = hashlib.sha256() + entries = [] + boundary_peak = 1 + for position, event in enumerate(template["execution_schedule"]): + if event["kind"] == "local_cover_sweep": + call = calls[event["stage"], event["replica"]] + values = [bounds[f // V] for f, route in call["owners"]] + need(max(values) <= entry_cap, "actual owner input cap") + entries.append(dict(event=position, stage=call["stage"], replica=call["replica"], + orientation=call["orientation"], + active=max(values[:2 * V]), helper=max(values[2 * V:]), + input=max(values))) + norm_step(bounds, event, recipe) + if "replica" in event: + r = event["replica"] + need(bounds[8*r:8*r+8] == matrix_table[event["source_event"]], + "independent transfer matrix comparison") + boundary_peak = max(boundary_peak, max(bounds)) + trace.update(canonical([position, bounds])) + maxima = {o: max(e["input"] for e in entries if e["orientation"] == o) + for o in ("forward", "backward")} + local = context["local"]["local"] + scaled = {o: Q(local[o]["prefix_l1_upper"]) * maxima[o] for o in maxima} + prefix = context["prefix"] + oldlocal = max(v["prefix_bits_upper"] for v in local.values()) + counts = Counter(e["kind"] for e in template["execution_schedule"]) + need(oldlocal == prefix["local_scalar_coefficient_work_prefix_bits"] and + counts["local_cover_sweep"] == prefix["complete_invocation_cover_sweeps"] and + counts["bridge"] == prefix["bridge_factor_two_sweeps"], "old growth charge binding") + conversion, margin = prefix["stream_input_sup_to_l2_bits"], prefix["primitive_arithmetic_margin_bits"] + need((conversion, margin) == (37, 4), "inherited conversion/margin") + need(oldlocal + conversion + counts["local_cover_sweep"] + counts["bridge"] + margin + == prefix["global_prefix_bits"], "old invoice arithmetic") + combined = strict_bits(max(Q(boundary_peak), *scaled.values())) + return dict(events=len(template["execution_schedule"]), event_counts=dict(counts), + calls=len(entries), helper_roles=len(entries) * HELPERS, cross_replica_roles=cross, + boundary_peak=boundary_peak, final_replica_bound=bounds[:8], + all_replica_final_bounds_equal=all(bounds[8*r:8*r+8] == bounds[:8] for r in range(REPLICAS)), + local_input_maxima=maxima, + borrowed_exceeds_active_calls=sum(e["helper"] > e["active"] for e in entries), + source_boundary_table=matrix_table, + call_inputs=entries, boundary_trace_sha256=trace.hexdigest(), + local_envelopes={o: str(Q(local[o]["prefix_l1_upper"])) for o in maxima}, + scaled_local_envelopes={o: str(value) for o, value in scaled.items()}, + combined_norm_bits=combined, input_conversion_bits=conversion, arithmetic_margin_bits=margin, + old_sufficient_bits=prefix["global_prefix_bits"], + refined_sufficient_bits=combined + conversion + margin, + retained_payload_bits=prefix["retained_payload_bits"]) + + +def scalar_borrow_witness(context): + """Identity-unitary contract model before one actual borrow, not a physical replay.""" + template = context["template"] + calls, recipe, _ = validate_controller(template, context["parent"], context["checks"]) + rows = [{j: 1} for j in range(8 * REPLICAS)] + + def add(target, source, coefficient): + for j, value in list(rows[source].items()): + v = rows[target].get(j, 0) + coefficient * value + if v: + rows[target][j] = v + else: + rows[target].pop(j, None) + + for position, event in enumerate(template["execution_schedule"]): + kind = event["kind"] + r = event.get("replica", 0) + if kind == "local_cover_sweep": + call = calls[event["stage"], r] + active = max(sum(map(abs, rows[f // V].values())) for f, _ in call["owners"][:2 * V]) + for helper, (family, route) in enumerate(call["owners"][2 * V:]): + row = rows[family // V] + value = sum(map(abs, row.values())) + if value > active: + return dict(event=position, stage=event["stage"], replica=r, + helper=helper, family=family, owner_replica=family // (8 * V), + active_upper=active, helper_attained=value, + helper_row=[[j, x] for j, x in sorted(row.items())], + input_nonzero=[[j, 1 if x > 0 else -1] for j, x in sorted(row.items())], + model="Scalar identity unitaries; all other initial coordinates zero. Not a physical supplier replay.") + q = recipe[event["stage"]] + source, target, coefficient = 8 * r + 2 * q["pair"], 8 * r + 2 * q["pair"] + 1, 1 + if q["reverse"]: + source, target, coefficient = target, source, -1 + add(target, source, coefficient) + elif kind == "bridge": + for side in range(2): + add(8 * r + 2 * event["dst"] + side, + 8 * r + 2 * event["src"] + side, event["coefficient"]) + elif kind == "terminal": + raise AuditError("no early borrowed-input witness") + raise AuditError("missing borrowed-input witness") + + +def controls(context): + rejected = [] + + def editable(): + # The immutable local programs are large and are not mutated here. + value = dict(context["template"]) + value["calls"] = copy.deepcopy(value["calls"]) + value["execution_schedule"] = copy.deepcopy(value["execution_schedule"]) + return value + + def reject(name, mutate, reason): + value = editable() + mutate(value) + try: + recount(context, value) + except AuditError as error: + need(str(error) == reason, name + " rejected by unexpected check: " + str(error)) + rejected.append(dict(name=name, predicate=reason)) + else: + raise AuditError("accepted mutation: " + name) + + def bridge(t): + return next(e for e in t["execution_schedule"] if e["kind"] == "bridge") + + reject("doubled_bridge", lambda t: bridge(t).__setitem__("coefficient", 2), "source event projection") + reject("bridge_wrong_source", lambda t: bridge(t).__setitem__("src", 3), "source event projection") + reject("wrong_local_orientation", lambda t: t["calls"][0].__setitem__("orientation", "backward"), + "source local orientation/pair") + reject("same_family_two_helpers", lambda t: t["calls"][0]["owners"][2*V+1].__setitem__( + 0, t["calls"][0]["owners"][2*V][0]), "one role per physical family") + reject("helper_aliases_active_data", lambda t: t["calls"][0]["owners"][2*V].__setitem__(0, 0), + "one role per physical family") + reject("data_port_permutation", lambda t: t["calls"][0]["owners"].__setitem__( + slice(0, 2), t["calls"][0]["owners"][1::-1]), "active data family/port binding") + reject("wrong_program", lambda t: t["calls"][0].__setitem__("local_program_sha256", "0"*64), + "call program binding") + reject("missing_event", lambda t: t["execution_schedule"].pop(6), "source event count") + reject("reordered_events", lambda t: t["execution_schedule"].__setitem__( + slice(5, 7), t["execution_schedule"][6:4:-1]), "source event chronology") + reject("unrecognized_event", lambda t: t["execution_schedule"][0].__setitem__("kind", "mix_families"), + "source event projection") + try: + recount(context, entry_cap=7) + except AuditError as error: + need(str(error) == "actual owner input cap", "understated cap rejection") + rejected.append(dict(name="understated_input_cap", predicate=str(error))) + else: + raise AuditError("accepted input cap seven") + + # Keep counts, family ranges and uniqueness, but borrow a family after its + # final bridges raise its majorant to 14. This breaks the eightfold entry + # bound; it also lies outside the admitted hosting windows. + late = editable() + schedule = late["execution_schedule"] + end = next(i for i, e in enumerate(schedule) if e["kind"] == "terminal") + replica = schedule[end]["replica"] + event = next(e for e in schedule[end+1:] if e["kind"] == "local_cover_sweep") + call = next(c for c in late["calls"] if (c["stage"], c["replica"]) == (event["stage"], event["replica"])) + used = {f for f, _ in call["owners"]} + family = next(f for f in range((8*replica+3)*V, (8*replica+4)*V) if f not in used) + call["owners"][2*V][0] = family + try: + recount(context, late) + except AuditError as error: + need(str(error) == "actual owner input cap", "late helper rejection") + rejected.append(dict(name="post_terminal_borrow", predicate=str(error), family=family, + stage=event["stage"], replica=event["replica"])) + else: + raise AuditError("accepted late helper") + return rejected + + +def result(root=ROOT): + context = load(root) + local_replay = replay_local(context, root) + report = recount(context) + witness = scalar_borrow_witness(context) + need(witness["helper_attained"] > witness["active_upper"], "borrow witness gap") + return dict(status="PASS_SELECTED1094_WIRE_PREFIX_AUDIT", source_sha256=context["hashes"], + local_replay=local_replay, controller=report, borrowed_input_witness=witness, + controls_rejected=controls(context), + scope="Conditional exact family-norm bound for the pinned finite controller. " + "Local scalar/frame checks replayed unchanged; familywise unitary physical " + "realization, cover bijections, recursive internals, roundoff/tape and analytic " + "transfer remain inherited. No production charge or kappa change.") + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", type=Path, help="write a newly checked receipt to a new path") + args = parser.parse_args() + receipt = result() + if args.write: + with args.write.open("x", encoding="utf-8") as stream: + stream.write(json.dumps(receipt, indent=2) + "\n") + else: + need(receipt == json.loads((PACKAGE / "EXPECTED.json").read_bytes()), "committed receipt differs") + c = receipt["controller"] + print(receipt["status"], "calls=" + str(c["calls"]), + "boundary=" + str(c["boundary_peak"]), "entry=8", + "conditional_bits=" + str(c["old_sufficient_bits"]) + "->" + str(c["refined_sufficient_bits"]), + "retained_payload=512 no_new_kappa") + + +if __name__ == "__main__": + main()